Re: [isabelle] Track sorry



On Sat, 5 Apr 2014, Julian Brunner wrote:

On Wed, Mar 26, 2014 at 12:14 PM, Lars Noschinski <noschinl at in.tum.de> wrote:
On 25.03.2014 18:36, Makarius wrote:
On Tue, 25 Mar 2014, bnord wrote:

is there a tool (or similar) to track which theorems in a development
depend in some way upon "sorry"? I've to assess student developments
and doing this manually is a pain. ;) I'd imagine an Isabelle/jEdit
"plugin".

For a quick and dirty check, I usually just use the hypersearch of
jEdit, which is one of the big assets of that text editor.  The
keywords "sorry" and "axiomatization" are the two main things to check.

Further note that the Prover IDE is not obliged to be 100% authentic,
although it tries its best to be so -- there might be optical
illusions even if the system works properly. At the end of the day
only batch builds count, with quick_and_dirty = false.
This will only tell the user whether all theorems are valid; when
grading student exercises it is often valuable to know which theorems
can be trusted despite having some (invalid) sorry'd theorem present.

(This thread is getting a bit complex by copy-pasting several text snippets with slightly different aspects back and forth.)

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.


This will only tell the user whether all theorems are valid; when
grading student exercises it is often valuable to know which theorems
can be trusted despite having some (invalid) sorry'd theorem present.

I second this, I've always found that very useful. Unfortunately, the [!] marker seems to have been removed in one of the recent versions. I don't know exactly when or even whether it's just me, but I remember it being there two years ago, and it's gone now. Unfortunately, the NEWS file only mentions its introduction.

I read two times "Unfortunately" here, and two times wrong. See also Isabelle2013/NEWS:

* Theorem status about oracles and unfinished/failed future proofs is
no longer printed by default, since it is incompatible with
incremental / parallel checking of the persistent document model.  ML
function Thm.peek_status may be used to inspect a snapshot of the
ongoing evaluation process.  Note that in batch mode --- notably
isabelle build --- the system ensures that future proofs of all
accessible theorems in the theory context are finished (as before).


Printing of conceptually inaccesible kernel derivations has been removed gradually since parallel processing became routine in Isabelle2008. I don't think you really want to go back to the old sequential times, with full information about low-level inferences produced in a painfully slow way. (HOL4 and Coq do this until today, but the Coq guys slowly discover that it might be done differently.)


	Makarius





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