[isabelle-dev] HOL-Codegenerator_Test fails in case-insensitive file-systems

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Thu Jul 18 15:03:44 CEST 2013

> 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



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130718/2ef58522/attachment.sig>

More information about the isabelle-dev mailing list