Re: [isabelle] Track sorry
On Mon, 7 Apr 2014, Lars Noschinski wrote:
On 07.04.2014 15:11, Makarius wrote:
Hypersearch doesn't help when the theorem is declared as simp (or
similar). And building a transitive closure using hypersearch is
Above I propose two conceptually different ways to check some Isabelle
(1) In the Prover IDE, using hypersearch to look at the concrete
(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.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and