[isabelle] Calling external provers from Isabelle



Hello,

We are currently thinking of trying to connect an external inductive prover (which works on Haskell programs) with Isabelle. For some very early experiments, we're looking to do something like:

1) Call Isabelle's code generator to produce a Haskell file of a given theory.
2) Call our tool on the generated Haskell file (via a bash command).

Got two questions on how to set this up a bit nicer than currently:

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)?

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. 

I'm guessing that there is some preferred way to call out to shell commands/external provers in Isabelle (as Sledgehammer does it), probably using threads? Any tips here to make it run more smootly?

Best,
Moa







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