[isabelle-dev] next release

[Makarius]

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