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

[Peter Lammich]

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
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev