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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and