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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
