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.
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
