[isabelle-dev] Code export to Haskell and lower-case theory names

[Makarius]

On Thu, 28 Mar 2013, Manuel Eberl wrote:

> I just noticed that when exporting code to Haskell, there is a 
> complication when some of the theories involved have lower-case names. 
> The code export itself will work with no error or warning, but when 
> ghc/ghci are invoked on the generated code, they will report the 
> lower-case module name of the module that corresponds to the theory as a 
> parse error, as Haskell apparently does not allow lower-case module 
> names.
>
> Is this a known issue, or even intended behaviour? I think the code 
> export tool should automatically rename this to an upper case version, 
> similarly to what it does with name clashes and Unicode tokens in 
> identifiers, or at least abort with an error message.

Florian Haftmann can say if he feels like supporting this deviation from 
hard and fast Isabelle conventions about Isabelle theories names: 
capitalized words (usually in singular) that are separated by underscore. 
Moreover locale / class names are in lower case, like most material within 
a theory body.

I occasioanlly see users making theory names lower case and locale names 
capitalized, probably in imitation of Java packages and classes.  Bad 
consequences will come from that, as can be seen here.

The Prover IDE should probably point to such confusions via some funny 
highlighting, but it is just one more feature to be taken care of, and 
there are more pressing things to do.


 	Makarius