[isabelle-dev] Testing of generated code

[Makarius]

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