Re: [isabelle] Sandboxed evaluation of Isabelle theories?
On Tue, 12 Feb 2013, Joachim Breitner wrote:
/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