Re: [isabelle] Calling external provers from Isabelle



On Wed, 27 Feb 2013, Moa Johansson wrote:

1) We currently use the Isar commad "export_code" to generate a Haskell-file, followed by some custom ML commands to call our prover. It would be nice to bake this together into one command. Where can I find the ML-function corresponding to "export_code" (for Haskell in this case)?

I am no expert on the code generator, but to get to the ML definition of things there is a standard way in Isabelle/jEdit: use C-hover-click to follow the implicit hyperlink of the command keyword in the theory source where you see it. This directs you quickly to ~~/src/Tools/Code/code_target.ML where you can then follow 2-3 more indirections to the main functions.

Maybe someone should make a video to explain the important C-hover-click gesture in Isabelle/jEdit.


2) To run our tool we use some bash commands, called from a ML-block using the OS.Process.system function. This takes a few seconds in Proof General (as I'd expect), but in JEdit it gets mysteriously stuck and takes a very long time to process the command and seem to just increasingly gobble up memory.

OS.Process.system is one of these critical functions of the NJ Basis library that are better avoided in Isabelle/ML. In 2008 we've spent many weeks to wrap it up in a way that works with interrupts.

The proper entry point is now called Isabelle_System.bash.


	Makarius





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