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