[isabelle-dev] Code export to Haskell and lower-case theory names
eberlm at in.tum.de
Tue Apr 2 12:45:28 CEST 2013
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
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev