>> 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.
This will require a second round of thought. Generally, the problem occurs always if code is to be emitted into files. E.g. in Haskell also two theories named foo.thy vs. Foo.thy would produce a clash, and only the capital convention for theory names has saved as so far from that. On the other hand, on the theory name level this can always be circumvented using just one generated file (»module_name«) and can thus be left to the user entirely. 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. Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev