[isabelle-dev] Testing of generated code
makarius at sketis.net
Thu Sep 25 21:41:18 CEST 2014
On Thu, 25 Sep 2014, Florian Haftmann wrote:
>>> Ultimately there is this error:
>>> ### java.lang.NoClassDefFoundError: Generated_Code$Typerep (wrong name:
>>> 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
> 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.
More information about the isabelle-dev