Re: [isabelle] Sandboxed evaluation of Isabelle theories?


Am Dienstag, den 12.02.2013, 13:46 +0100 schrieb Makarius:
> On Tue, 12 Feb 2013, Joachim Breitner wrote:
> > Am Dienstag, den 12.02.2013, 13:27 +0100 schrieb Tjark Weber:
> >> Anyway, I am guessing that Joachim is more concerned about features
> >> like unrestricted file system or network access than about soundness
> >> of Isabelle.
> >
> > Should -S be sufficient for that?
> To some extent, yes.  It makes doing bad things harder.

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

For the first one it seems I have to somehow disable the quick_and_dirty mode, but passing
"-e 'quick_and_dirty := false'" did not have the desired effect.

Any suggestions on how to proceed here?


Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

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

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