Re: [isabelle] Calling external provers from Isabelle



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.


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





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