Re: [isabelle] skip_proofs in Isabelle2012



On 27/07/2012, at 4:34 AM, Makarius <makarius at 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




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