[isabelle-dev] Testing of generated code

[Andreas Lochbihler]

Hi Makarius,

On 22/09/14 11:08, Makarius wrote:
> Based on this changeset 469a375212c1, I have augmented some isatest configurations which
> had already ISABELLE_FULL_TEST=true
Thanks for adding this.


> ### /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.
Yes, this is a current limitation of the code generator. A hack would be to manually ename 
such clashing names with code_printing, but this is neither robust nor scalable. I'd 
prefer to have the code generator treat Scala names case-insensitively. Maybe Florian can 
look into this.

Andreas