search

HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
https://hol-theorem-prover.org
Other
626 stars 143 forks source link

tactic application cache #488

Open xrchz opened 7 years ago

xrchz commented 7 years ago

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.

xrchz commented 7 years ago

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.)

xrchz commented 7 years ago

@barakeel would the tactictoe infrastructure support this?

mn200 commented 6 years ago

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 >-?