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

Makarius makarius at sketis.net
Thu Jul 18 14:40:42 CEST 2013

This crash happens in Isabelle/38466f4f3483, e.g. on Mac OS X:

HOL-Codegenerator_Test FAILED
(see also 

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 
Unfinished session(s): HOL-Codegenerator_Test


More information about the isabelle-dev mailing list