Re: [isabelle] Sandboxed evaluation of Isabelle theories?



Dear Makarius,

Am Dienstag, den 12.02.2013, 17:57 +0100 schrieb Makarius:
> On Tue, 12 Feb 2013, Joachim Breitner wrote:
> > Next question:
> >
> > /opt/isabelle/Isabelle2013-RC2/bin/isabelle-process -S -r -I HOL < Foo.thy
> >
> > will tell me about wrong proofs (*** Failed to finish proof), but not about
> > 1. uses of sorry
> > 2. unexpected end of the file.
> 
> Piping directly into the Isar toplevel gives indeed very little static 
> consistency checking.  You would have to emulate Proof General in 
> imitating some of that, but it never really managed > 10 years.
> 
> 
> It is better to work in batch mode, by telling the raw ML toplevel to 
> invoke use_thys like this:
> 
>    isabelle-process -S -r -q -e 'use_thys ["~/tmp/A"];'
> 
> Batch mode then also says something like this by default:
> 
> Loading theory "A"
> *** Cheating requires quick_and_dirty mode!
> *** At command "sorry" (line 4 of "/Volumes/Macintosh_HD/Users/makarius/tmp/A.thy")

thanks for the hint. Now it does detect sorry and partial theories well,
and this invocation is also easier for out system as the filename can be
passed in a parameter.

I noticed that -S had no effect any more (due to how the MLTEXT variable
in isabelle-process is assembled), but passing 
        -e 'Secure.set_secure (); use_thys ["/tmp/Deduction"];'
works.

Greetings,
Joachim


-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



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