Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] skip_proofs in Isabelle2012

Email Gateway (Aug 19 2022 at 07:54):

From: Gerwin Klein <gerwin.klein@nicta.com.au>
The skip_proofs option seems to clash with something in Isabelle2012. I'm getting "Messed-up outer syntax for presentation".

Initially I thought this may be a PG problem, but it's not. I tried the following on the tty level:

serenity:~ kleing$ /Applications/Isabelle2012.app/Isabelle/bin/isabelle tty

val it = (): unit
val commit = fn: unit -> bool
Welcome to Isabelle/HOL (Isabelle2012: May 2012)
theory X imports Main begin
theory X
ML "quick_and_dirty := true";
val it = (): unit

ML "Toplevel.skip_proofs := true";
val it = (): unit

end;
theory A imports "~~/src/HOL/Library/List_Prefix" begin
Loading theory "List_Prefix"
*** Messed-up outer syntax for presentation
*** At command "theory"

I'm only seeing the error when I refer to paths explicitly in the import section and Isabelle actually resolves that path. That is, if I manually (in skip_proof mode) step through List_Prefix first and the theory is loaded, the import works fine. (That defeats the purpose of skip_proof mode, of course, because I'm trying to avoid stepping through 30 files and waiting for an hour).

Any ideas?

Cheers,
Gerwin

Email Gateway (Aug 19 2022 at 07:56):

From: Makarius <makarius@sketis.net>
The above should work if you include this as well:

ML "Goal.parallel_proofs := 0;"

I can't say on the spot what is the reason for this behaviour. A bit too
many features have accumulated in the system, and everytime I pass by that
part of the Isar toplevel, I wonder which combinations of the various
flags actually work.

In the longer run, quick_and_dirty, 'sorry', skip_proofs and forked proofs
should be all unified to forked proofs.

Makarius

Email Gateway (Aug 19 2022 at 07:57):

From: Gerwin Klein <gerwin.klein@nicta.com.au>
On 27/07/2012, at 4:34 AM, Makarius <makarius@sketis.net> wrote:

On Thu, 26 Jul 2012, Gerwin Klein wrote:

The skip_proofs option seems to clash with something in Isabelle2012. I'm getting "Messed-up outer syntax for presentation".

Initially I thought this may be a PG problem, but it's not. I tried the following on the tty level:

serenity:~ kleing$ /Applications/Isabelle2012.app/Isabelle/bin/isabelle tty

val it = (): unit
val commit = fn: unit -> bool
Welcome to Isabelle/HOL (Isabelle2012: May 2012)
theory X imports Main begin
theory X
ML "quick_and_dirty := true";
val it = (): unit

ML "Toplevel.skip_proofs := true";
val it = (): unit

end;
theory A imports "~~/src/HOL/Library/List_Prefix" begin
Loading theory "List_Prefix"
*** Messed-up outer syntax for presentation
*** At command "theory"

The above should work if you include this as well:

ML "Goal.parallel_proofs := 0;"

Thanks, I can confirm that this works on our side.

I can't say on the spot what is the reason for this behaviour. A bit too many features have accumulated in the system, and everytime I pass by that part of the Isar toplevel, I wonder which combinations of the various flags actually work.

I had a brief look at that code before I wrote the message and gave up, yes :-)

In the longer run, quick_and_dirty, 'sorry', skip_proofs and forked proofs should be all unified to forked proofs.

That sounds reasonable.

Cheers,
Gerwin

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

From: Makarius <makarius@sketis.net>
On Fri, 27 Jul 2012, Gerwin Klein wrote:

The above should work if you include this as well:

ML "Goal.parallel_proofs := 0;"

Thanks, I can confirm that this works on our side.

I can't say on the spot what is the reason for this behaviour. A bit
too many features have accumulated in the system, and everytime I pass
by that part of the Isar toplevel, I wonder which combinations of the
various flags actually work.

I had a brief look at that code before I wrote the message and gave up,
yes :-)

Included is a changeset exported from the Isabelle repository that also
happens to work with Isabelle2012. I can't say that it fixes the problem,
because skip_proofs has never worked reliably in its history. It produces
an invalid Isar toplevel state that makes many tools crash on it.

More substantial reforms are required ...

In the longer run, quick_and_dirty, 'sorry', skip_proofs and forked
proofs should be all unified to forked proofs.

Makarius
skip_proofs

Last updated: Apr 25 2024 at 08:20 UTC