Re: [isabelle] programmatically running isabelle
Am 27.04.2012 um 15:50 schrieb John Wickerson:
> 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.";
> printf "It failed.";
> How might I go about writing this code? Thanks very much.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and