[isabelle-dev] Testing of generated code

[Makarius]

On Thu, 25 Sep 2014, Florian Haftmann wrote:

>>> 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.

For now I have added more isatests in 5dbb09cc5a01, such that we have a 
complete coverage of HOL-Codegenerator_Test on lxbroy4 and macbroy2 
together.


> With Scala, the problem explodes since for one source file various
> generated files are produced.  This requires an analysis with entities
> are mapped to class files later on and implement a different name clash
> resolving strategy for their names.  Maybe a mimicry of the file system
> itself: keep case as it is, but avoid clashes with same name in
> different case.

I wonder if Scala has some options to change the name manginling on its 
side. We have had https://issues.scala-lang.org/browse/SI-3623 before, and 
their might be something similar elsewhere.


 	Makarius