[isabelle] programmatically running isabelle



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




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