More principled logging and observation of proof state

[martinberger]

Currently, the implementation follows [1] in that we have the Thm class, tactics and all proof state handling use the Option monad. Logging, and observation of proof state is done by printing to the command line. It might be worthwhile to be more principle here, and using an Either monad instead or similar abstractions.

---

1. D. P. Mulligan, Mosquito: an implementation of higher-order logic (Rough diamond)

[martinberger]

Here is an elaboration of the issues with several possible approaches. Currently debugging is difficult because ad-hoc, and needs recompilation to switch on/off debugging and logging. Typically we want to hone in on where a proof starts to fail, but not how we got there. So we are interested in getting:

• Which tactic used just before the proof fails?
• What was the proof state just before failure?

This suggests that we add principled mechanisms for logging and printing:

• proof state
• tactics used
• mechanisms for switching on/off the above

Here are some ideas on how to do this (not mutually exclusive):

• Ideal: trace state + tactics and by default, if proof fails, return last $N$ used tactic, and proof states before failure (with $N=1$ being the default). This could be implemented in several ways:

  • Stateful: maintain a list of tactics used and proof state. (Trivial to implement.)
  • Pure: with a logging monad. (Clean but more work.)

• Have suitable (pre-)tactics "switch on printing" and "switch off printing" with options for state and used-tactic printing. This is really easy to implement. This should be at the pre-tactic level and not tactics (as it is now) since most proofs are specified as a list of pre-tactics.

• Augment the Try tactic so it automatically prints out used tactic and state in case of failure. When this integrated with the makeGeneric function, this requires no changes with current test suite.

• Even less invasive than the last bullet is also using the OrElse and FailWith tactics as follows. Typically a proof is a list of pretactics like so

   Apply(pt1), ..., Apply(pt17)
  

  which we replace by

   OrElse(Apply(pt1), AndThen(PrintState(), FailWith(s"last used: ${pt1.toString}"))), ...
  

  Note that this transformation cannot be expressed in the tactics DSL, but uses the meta-language. Should this be seen as an expressive weakness of the tactics DSL?