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

[Manuel Eberl]

Hallo,

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.

Cheers,
Manuel