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

[Makarius]

On Thu, 18 Jul 2013, 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?

There seem to be two issues here: the warning (harmless or not?) and the 
SML test failure.  The latter was caused by myself trying an SVN snapshot 
of Poly/ML, so we can ignore that incident for now.


 	Makarius