On Thu, 14 Jan 2016, Thomas Sewell wrote:
The second proposal is probably more contentious. I'm hoping to
reimplement a tool we had in the past that speeds up proof maintenance
work by selectively skipping proofs that are very likely to succeed. To
support that, I'm proposing adding a couple of hooks to Pure/goal.ML,
similar to the hook in Pure/Isar/toplevel.ML. One hook will allow the
tool to install an oberver (context -> thm -> unit) for completed
proofs. Another (context -> thm -> bool) will allow the tool to observe
proofs as they commence, and to optionally recommend they be skipped.
This second change essentially just gives the user a little more
control, they could skip the proofs with skip_proofs anyway. Still, I'm
sure it will provoke some interesting discussion.
A discussion without sources to look at is difficult.
Generally, these hooks are rather old, predating the managed evaluation of
the PIDE document model. There used to be more hooks in ancient times,
but we have managed to get rid of most of them.
The general plan (for many years already) is to unify the batch build mode
further with the managed evaluation of PIDE interaction. In particular
there should be proper ways to fork (and maybe ignore) proofs in the
document model. Odd flags like skip_proofs or quick_and_dirty/sorry might
eventually disappear.
As usual there is a conflict of proper principles done right, and small
adhoc patches to an already complex system.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
