Re: [isabelle] Sandboxed evaluation of Isabelle theories?

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


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