[isabelle] Track sorry · Archive Mirror: Isabelle Users Mailing List

Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Track sorry

Email Gateway (Aug 19 2022 at 14:04):

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".

Best
Benedikt

Email Gateway (Aug 19 2022 at 14:04):

From: Lars Noschinski <noschinl@in.tum.de>
This information is stored in a theorem. I think when you "using" this
theorem, it is shown with a trailing "[!]".

-- Lars

Email Gateway (Aug 19 2022 at 14:04):

From: Makarius <makarius@sketis.net>
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.

The following discussion from last year about "Sandboxed evaluation of
Isabelle theories?" might be also of interest:
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-February/msg00156.html

Makarius

Email Gateway (Aug 19 2022 at 14:05):

From: Lars Noschinski <noschinl@in.tum.de>
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.

-- Lars

Email Gateway (Aug 19 2022 at 14:13):

From: Makarius <makarius@sketis.net>
On Sat, 5 Apr 2014, Julian Brunner wrote:

On Wed, Mar 26, 2014 at 12:14 PM, Lars Noschinski <noschinl@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

Email Gateway (Aug 19 2022 at 14:14):

From: Lars Noschinski <noschinl@in.tum.de>
Hypersearch doesn't help when the theorem is declared as simp (or
similar). And building a transitive closure using hypersearch is cumbersome.

-- Lars

Email Gateway (Aug 19 2022 at 14:15):

From: Makarius <makarius@sketis.net>
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

Last updated: Nov 21 2024 at 12:39 UTC