[isabelle-dev] Testing of generated code

[Florian Haftmann]

>> Ultimately there is this error:
>>
>> ### java.lang.NoClassDefFoundError: Generated_Code$Typerep (wrong name:
>> Generated_Code$typerep)
>>
>>
>> That looks like a general weakness of the code generator.  I have
>> called the file-system
>> "insensible" in the log message, but such file-systems are
>> common-place on Windows and Mac
>> OS X, i.e. the majority of user platforms.
> Yes, this is a current limitation of the code generator. A hack would be
> to manually ename such clashing names with code_printing, but this is
> neither robust nor scalable. I'd prefer to have the code generator treat
> Scala names case-insensitively. Maybe Florian can look into this.

This will require a second round of thought.  Generally, the problem
occurs always if code is to be emitted into files.  E.g. in Haskell also
two theories named foo.thy vs. Foo.thy would produce a clash, and only
the capital convention for theory names has saved as so far from that.
On the other hand, on the theory name level this can always be
circumvented using just one generated file (»module_name«) and can thus
be left to the user entirely.

With Scala, the problem explodes since for one source file various
generated files are produced.  This requires an analysis with entities
are mapped to class files later on and implement a different name clash
resolving strategy for their names.  Maybe a mimicry of the file system
itself: keep case as it is, but avoid clashes with same name in
different case.

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

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