Re: [isabelle] Track sorry



On Mon, 7 Apr 2014, Lars Noschinski wrote:

On 07.04.2014 15:11, Makarius wrote:

Above I propose two conceptually different ways to check some Isabelle
development;

  (1) In the Prover IDE, using hypersearch to look at the concrete
syntax.

  (2) In batch mode, by using knowledge about the LCF kernel works.

When Lars says "This will only tell the user whether all theorems are
valid" he seems to refer to (2), while ignoring (1) -- and the
fantastic hypersearch tool of jEdit.
Hypersearch doesn't help when the theorem is declared as simp (or similar). And building a transitive closure using hypersearch is cumbersome.

So we are back to the initial question, ``which theorems in a development depend in some way upon "sorry"'' and if the Prover IDE could show that. Of course it could, but it still doesn't. It is one of the many things I would have liked to see already some years ago.

What is conceptually missing here is a way to "wrap up" the content of the interactive document model, like "isabelle build" does in batch mode.


Moreover the resulting graph of formal entities, or failure to produce them, could be visualized, but the student project that was meant to replace the old graph browser by something that works with Scala and Swing did not produce anything apart from wasting substantial time.

I need to emphasize explicitly here that the "keen student" rarely works as wild-card: first one needs to find one, then one needs to turn the result into generally usable form, beyond mere experiments.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.