Hi. We ran into this problem with Scala on Windows, our "workaround" was to either build a jar-file on linux, or do manual renaming in the Isabelle-sources.
Isn't it possible to integrate case-insensitivity in the renaming that is performed by the code-generator anyway (to rename identifiers matching target-language keywords, etc). -- Peter On Do, 2013-07-18 at 15:03 +0200, Florian Haftmann wrote: > > This crash happens in Isabelle/38466f4f3483, e.g. on Mac OS X: > > > > HOL-Codegenerator_Test FAILED > > (see also > > /Volumes/Macintosh_HD/Users/makarius/.isabelle/heaps/polyml-5.5.1_x86-darwin/log/HOL-Codegenerator_Test) > > > > > > ROOT.scala:696: warning: Class Generated_Code$Pattern differs only in > > case from Generated_Code$pattern. Such classes will overwrite one > > another on case-insensitive filesystems. > > final case class Pattern() extends pattern > > ... > > *** Code check failed for SML: "$ISABELLE_PROCESS" -r -q -e 'datatype > > ref = datatype Unsynchronized.ref; use "ROOT.ML" handle _ => exit 1' Pure > > *** At command "export_code" (line 19 of > > "~~/src/HOL/Codegenerator_Test/Generate_Pretty_Char.thy") > > Unfinished session(s): HOL-Codegenerator_Test > > Interestingly, the code generator test for Scala (which indeed is > brittle on case-insensitive file systems) gives a warning but seems to > succeed. What really fails is the SML test which is not sensitve > towards case-insensitive file systems. Does this also occur on other > platforms? > > Florian > > _______________________________________________ > isabelle-dev mailing list > [email protected] > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
