HOL
HOL copied to clipboard
HOL-Theorem-Prover
tactic application cache
The proof manager could keep a cache of previously seen and proved subgoals, and prove them immediately if they are seen again. This might speed up interactive development with long-running tactics. Of course it also makes testing/debugging changes to proof scripts harder - but this could be mitigated with an easily modifiable "use cache" flag.
Actually I think what I mean is not a subgoal cache, but a resulting-goal-state cache keyed on tactic code, to speed up expand (e). This assumes the tactics are pure. (This is a step towards what I think Isabelle provides to support its document model.)
To make a cache work on tactic text at the REPL level, you'd have to make a version of e that actually took a string as argument. The editor modes could make this invisible. Of course, you'd have to have the lookup be keyed on the combination of tactic-text and goal-state. This probably wouldn't be helpful if replaying proofs after a redefinition of constants, because the goal-state terms would then be different.
What about parallelising THENL and >-?
