[isabelle-dev] Testing of generated code

[Andreas Lochbihler]

Hi all,

we have hardly any check that the code generated by the code generator is correct. There 
is only the checking option of the command export_code. It calls a target language 
compiler to see whether the compiler accepts the code. Since there are more and more 
adaptations to serialisation phase in Isabelle and the AFP, I have written a testing 
framework for the code generator (pushed on testboard/469a375212c1), which has already 
helped me in finding a number of oversights in my AFP entry Native_Word.

The framework provides a command for regression tests of lists of boolean expressions 
(command test_code) and for evaluation of single terms (command eval_term). They both 
generate code in the given target language(s) plus language-specific drivers, compile and 
run the whole and parse back the result using a YXML encoding. The commit contains drivers 
for PolyML, MLton, SML/NJ, OCaml, GHC and Scala.

The framework requires some configuration for the target languages. In detail, the 
following environment variables have to be set as follows for the different implementations:

ISABELLE_POLYML_PATH point to a PolyML executable poly
ISABELLE_MLTON       point to an MLton executable mlton
ISABELLE_SMLNJ       point to the SML/NJ executable sml
ISABELLE_OCAMLC      point to the OCaml executable ocamlc
ISABELLE_GHC         point to the GHC executable ghc (same as for Quickcheck_Narrowing)
ISABELLE_SCALA       point to the Scala binary folder (which contains scala and scalac)

I do not know how the test systems for the repository are configures w.r.t.

   export_code ... checking ...

but this framework only makes sense if we have each supported implementation of a target 
language installed on at least one system. In July, Gerwin set up the machines for GHC. 
Could anyone take care of the other implementations?

If this works well across all platforms, one might think about moving this upwards into 
Main and generalise value [code] accordingly.

Best,
Andreas

PS: Feedback on the code is always welcome.