Re: [isabelle-dev] Code export to Haskell and lower-case theory names
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 breit...@kit.edu wrote: Am Freitag, den 29.03.2013, 13:24 +0100 schrieb Makarius: This has got nothing to do with Isabelle's informal conventions but is all about the target language's formal rules. The conventions about theory names and locale/class names are not that informal. If you violate them systematically, certain name space policies will break down. That is then a general user error. Are there really things that break if I deviate from the convention? The main problem I know about is that qualified names can become ambiguous: e.g. if foo.bar.baz and bar.boo.baz are both in scope, then bar.baz could refer to either of them. The problem is avoided if theory names and locale/type/constant names are kept disjoint. See also this old thread: https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2011-July/001674.html but in every case there is a more qualified name that can be used to identify each entity? I would not consider that a hard problem, just an annoyance. I read this as “if you deviate from the suggested scheme, things might become a little bit less convenient, but everything still works” which I find fair enough. When name spaces were introduced in 1998 and locales in 1999, the people behind all that (including myself) looked very carefully what can be achieved with minimal extra complexity. The result of that was to keep theory names always capitalized and locales lower-case, in accordance to what was established practice for a long time already. This very simple scheme allows to refer to the outer two levels of the name space hiearchy and the reliably without extra worries. Otherwise, certain name accesses can become inaccesible, which I would call more that just inconvenient, especially since the whole name space business has become a bit more complex in the years after 2005. So far there were no reasons given on this thread why the convention should not be followed first place. Are there any? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Code export to Haskell and lower-case theory names
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 before I learned that not following them can cause severe issues. As I said: If it can cause issues beyond inconvenience (and you say it can), then the convention should become the rule and enforced by the system, to prevent users from accidentally not following the rule. Greetings, Joachim -- Dipl.-Math. Dipl.-Inform. Joachim Breitner Wissenschaftlicher Mitarbeiter http://pp.ipd.kit.edu/~breitner signature.asc Description: This is a digitally signed message part ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Code export to Haskell and lower-case theory names
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-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Code export to Haskell and lower-case theory names
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-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Code export to Haskell and lower-case theory names
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, with all the baggage and complexity that has accumulated, especially on the Java (and Scala) platform. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Code export to Haskell and lower-case theory names
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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Code export to Haskell and lower-case theory names
Am 29/03/2013 11:24, schrieb 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. Manuel is absolutely right. If you translate into a language with certain rules you have to obey those rules. Which the translator into Haskell mostly does: types are capitalized (despite the fact that they are typically lower case in Isabelle, nothing bad comes of it), function names are lowered where needed, type variables are called a, not 'a, etc. But theory/module names are not capitalized. An omission. This has got nothing to do with Isabelle's informal conventions but is all about the target language's formal rules. Tobias 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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Code export to Haskell and lower-case theory names
On Fri, 29 Mar 2013, Tobias Nipkow wrote: Am 29/03/2013 11:24, schrieb 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. Manuel is absolutely right. If you translate into a language with certain rules you have to obey those rules. Which the translator into Haskell mostly does: types are capitalized (despite the fact that they are typically lower case in Isabelle, nothing bad comes of it), function names are lowered where needed, type variables are called a, not 'a, etc. But theory/module names are not capitalized. An omission. So that's something to be refined by Florian Haftmann. This has got nothing to do with Isabelle's informal conventions but is all about the target language's formal rules. The conventions about theory names and locale/class names are not that informal. If you violate them systematically, certain name space policies will break down. That is then a general user error. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Code export to Haskell and lower-case theory names
Hi, Am Freitag, den 29.03.2013, 13:24 +0100 schrieb Makarius: This has got nothing to do with Isabelle's informal conventions but is all about the target language's formal rules. The conventions about theory names and locale/class names are not that informal. If you violate them systematically, certain name space policies will break down. That is then a general user error. Are there really things that break if I deviate from the convention? 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). Greetings and happy easter to those who care, Joachim -- Dipl.-Math. Dipl.-Inform. Joachim Breitner Wissenschaftlicher Mitarbeiter http://pp.ipd.kit.edu/~breitner signature.asc Description: This is a digitally signed message part ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Code export to Haskell and lower-case theory names
Hi Manuel, 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. maybe it never worked that way, maybe it never got noticed. However, the produced module names should indeed be valid wrt. to the underlying target language. I have some reform related to code naming on my agenda, where I can reexamine and amend this. Cheers, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Code export to Haskell and lower-case theory names
On Fri, Mar 29, 2013 at 10:40 AM, Joachim Breitner breit...@kit.edu wrote: Hi, Am Freitag, den 29.03.2013, 13:24 +0100 schrieb Makarius: This has got nothing to do with Isabelle's informal conventions but is all about the target language's formal rules. The conventions about theory names and locale/class names are not that informal. If you violate them systematically, certain name space policies will break down. That is then a general user error. Are there really things that break if I deviate from the convention? The main problem I know about is that qualified names can become ambiguous: e.g. if foo.bar.baz and bar.boo.baz are both in scope, then bar.baz could refer to either of them. The problem is avoided if theory names and locale/type/constant names are kept disjoint. See also this old thread: https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2011-July/001674.html 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. - Brian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Code export to Haskell and lower-case theory names
Hi, Am Freitag, den 29.03.2013, 15:32 -0700 schrieb Brian Huffman: On Fri, Mar 29, 2013 at 10:40 AM, Joachim Breitner breit...@kit.edu wrote: Am Freitag, den 29.03.2013, 13:24 +0100 schrieb Makarius: This has got nothing to do with Isabelle's informal conventions but is all about the target language's formal rules. The conventions about theory names and locale/class names are not that informal. If you violate them systematically, certain name space policies will break down. That is then a general user error. Are there really things that break if I deviate from the convention? The main problem I know about is that qualified names can become ambiguous: e.g. if foo.bar.baz and bar.boo.baz are both in scope, then bar.baz could refer to either of them. The problem is avoided if theory names and locale/type/constant names are kept disjoint. See also this old thread: https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2011-July/001674.html but in every case there is a more qualified name that can be used to identify each entity? I would not consider that a hard problem, just an annoyance. I read this as “if you deviate from the suggested scheme, things might become a little bit less convenient, but everything still works” which I find fair enough. Greetings, Joachim -- Dipl.-Math. Dipl.-Inform. Joachim Breitner Wissenschaftlicher Mitarbeiter http://pp.ipd.kit.edu/~breitner signature.asc Description: This is a digitally signed message part ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Code export to Haskell and lower-case theory names
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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
