Email Gateway (Aug 19 2022 at 10:21): Email Gateway (Aug 19 2022 at 10:21):From: Moa Johansson <moa.johansson@chalmers.se>
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
Email Gateway (Aug 19 2022 at 10:21):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 19 2022 at 10:22):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Moa,
1) Call Isabelle's code generator to produce a Haskell file of a given
theory.
as a first entry try
Code_Target.produce_code …
This should suffice for a proof of concept.
Building code from own snippets and generated code is a black art on its
own -- if your project evolves into something persistent, get back here
and I'll try my best to provide you with the most robust and convenient
ways available to arrange things then.
Cheers,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 10:41):From: Lukas Bulwahn <bulwahn@in.tum.de>
Hi Moa,
For the narrowing-based Quickcheck in Isabelle, I already use
Isabelle's code generator to produce a Haskell file,
pass it to the Haskell compiler, and read back its result.
The implementation is in
http://isabelle.in.tum.de/repos/isabelle/file/e6524a89c9e3/src/HOL/Tools/Quickcheck/narrowing_generators.ML
Function value and dynamic_value_strict provide the compilation and the
execution.
Maybe you can reuse part of it, or generalize it to be useful for a
larger audience.
Florian and I discussed extracting this part into a more general
"Haskell evaluator" module.
However as it was of low priority on my todo list and time is generally
rare, we never
did this.
Lukas
Email Gateway (Aug 19 2022 at 10:42):From: Makarius <makarius@sketis.net>
Here is the public release version of that file:
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2013/src/HOL/Tools/Quickcheck/narrowing_generators.ML
As a rule of thumb: changset id -> isabelle-dev, proper releases ->
isabelle-users.
Makarius
Last updated: Apr 19 2024 at 04:17 UTC