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

[Manuel Eberl]

Be that as it may, even in that case, I would like the code export tool
to at least output a warning or an error message. Having the code export
tool export produce faulty Haskell code can hardly be intended behaviour.

As an analogy: when I give invalid code to a compiler, I expect it to
complain instead of silently produce an invalid executable that will
refuse to run and give me some obscure error message about ELF.


On 02/04/13 12:38, Makarius wrote:
> On Fri, 29 Mar 2013, Brian Huffman wrote:
>
>>> Then it should be a hard rule enforced by the system. If that is not
>>> the case, then it should be fully supported and up to the user to
>>> choose his naming, even if it deviate from what others use (she
>>> might have reasons for that).
>>
>> I completely agree.
>
> Enforcing rules in a strict manner is always a very painful process.
> We've done that over the years where it was absolutely necessary, e.g.
> making the theorem name space conform to the policies of any other
> name space (types, consts, etc.), despite all the complaints that were
> coming from it.  Now it is difficult to imagine that theorems would
> work otherwise.
>
> Generally, I see a variety of levels of checking by the system, a
> spectrum between enforcement to encourgement: error, warning,
> hilighting. BTW, in Isabelle/jEdit a plain warning already looks quite
> prominent.
>
>
>     Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>