Re: [isabelle-dev] Interpretation in arbitrary targets.

2013-04-02 Thread Clemens Ballarin
Quoting Florian Haftmann : Let those thoughts sink further few days. If there is no veto until Apr 7th, I would go ahead to turn the patches upstream. Well, here is my veto. I don't see that much of a discussion has taken place yet, and I am very unhappy about the concepts and terminology

[isabelle-dev] PLMMS at CICM, July 2013, Bath, UK

2013-04-02 Thread Makarius
N¬™ë,j¢²)Ì Á¢¹šµ8^~*춖«¶ÈhºW[z·šu¦åz×±·b•ëaz·¦j)➠Z®Û­éb‘érºzÞi֛•ì"¶.´Â ¬­ëh¢[

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

2013-04-02 Thread Makarius
On Tue, 2 Apr 2013, Manuel Eberl wrote: 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. Funnily such things happen routinely these days, w

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

2013-04-02 Thread 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

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

2013-04-02 Thread Makarius
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.

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

2013-04-02 Thread Joachim Breitner
Hi, Am Dienstag, den 02.04.2013, 12:31 +0200 schrieb Makarius: > So far there were no reasons given on this thread why the convention > should not be followed first place. Are there any? ignorance? I was using Isabelle for quite a while before I heard about these conventions, and even longer be

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

2013-04-02 Thread Makarius
On Fri, 29 Mar 2013, Joachim Breitner wrote: Hi, Am Freitag, den 29.03.2013, 15:32 -0700 schrieb Brian Huffman: On Fri, Mar 29, 2013 at 10:40 AM, Joachim Breitner wrote: Am Freitag, den 29.03.2013, 13:24 +0100 schrieb Makarius: This has got nothing to do with Isabelle's informal conventions

Re: [isabelle-dev] [PATCH 0 of 1] Fix top-level printing of exception messages containing forced-line breaks

2013-04-02 Thread Makarius
On Tue, 2 Apr 2013, David Greenaway wrote: I would appreciate it if an Isabelle expert could review that patch and, if acceptable, apply it to mainline. (This can be easily done with "hg import "). Dear David, before you send more patches, can you please go back to the very start of the mai