Re: [isabelle] programmatically running isabelle



Hi John,

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.";
> else
>  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.

Regards,

Jasmin






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