Email Gateway (Aug 18 2022 at 19:24): Email Gateway (Aug 18 2022 at 19:24):From: John Wickerson <jpw48@cam.ac.uk>
Hello Isabelle,
I want to write a program that dynamically generates a .thy file, passes it to isabelle for processing, and then proceeds depending on whether isabelle succeeds or not. I'm imagining something like this:
let mytheory = "theory mytheory imports Main begin blah blah blah end" in
output_to_file "mytheory.thy" mytheory;
let result = run_isabelle "mytheory.thy" in
if result then
printf "It worked.";
else
printf "It failed.";
How might I go about writing this code? Thanks very much.
John
Email Gateway (Aug 18 2022 at 19:24):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi John,
The system.pdf manual included with Isabelle (invocable as "isabelle doc system" on the command-line) documents the options you need. In this case, you need the following:
isabelle-process -e "use_thy \"mytheory\";"
If you have Isabelle2011-1 installed, you can look in "src/HOL/Tools/Nitpick/lib/Tools/nitrox" for an example of a program that does just that.
Regards,
Jasmin
Last updated: Apr 24 2024 at 16:18 UTC