On Mon, 25 Aug 2014, Andreas Lochbihler wrote:
we have hardly any check that the code generated by the code generator is
correct.
I have written a testing framework for the code generator
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.
Based on this changeset 469a375212c1, I have augmented some isatest
configurations which had already ISABELLE_FULL_TEST=true, see now:
changeset: 58414:8392d221bd91
tag: tip
user: wenzelm
date: Mon Sep 22 10:18:41 2014 +0200
files: Admin/isatest/settings/mac-poly-M4
Admin/isatest/settings/mac-poly-M8 src/HOL/Codegenerator_Test/code_test.ML
src/HOL/ROOT
description:
clarified ISABELLE_POLYML;
added some isatests -- ISABELLE_SCALA still inactive due to problems with
case-insensible file-system;
This means it works, except for Scala. Here is one of the many warnings
issued by scalac:
### /tmp/isabelle-makarius76888/Code_Test3541773/Generated_Code.scala:4:
warning: Class Generated_Code$Typerep differs only in case from
Generated_Code$typerep. Such classes will overwrite one another on
case-insensitive filesystems.
### final case class Typerep(a: String, b: List[typerepa]) extends typerepa
Ultimately there is this error:
### java.lang.NoClassDefFoundError: Generated_Code$Typerep (wrong name:
Generated_Code$typerep)
That looks like a general weakness of the code generator. I have called
the file-system "insensible" in the log message, but such file-systems are
common-place on Windows and Mac OS X, i.e. the majority of user platforms.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev