Re: [isabelle-dev] Deprecating legacy ASCII symbols?
This thread is still pending. At the Isabelle tutorial at CADE-25, we've had again the situation that new users got very confused by the odd ASCII syntax in basic theories of Main Isabelle/HOL. Including the results from the discussion on this thread, the plan is now as follows: * print mode xsymbols looses its special status eventually, and Isabelle symbols are used by default * print mode ASCII retains some important old-style ASCII syntax, e.g. basic things like !! == ALL EX -- | : * strange and/or rarely used ASCII notation is eliminated -- depending on actual use in the visible universe of Isabelle + AFP applications * \Colon is eliminated and :: used exclusively This is quite conservative. It mainly means that theory sources are cleaned up a bit, and the default print mode setup is simplified. Questions about particular syntax may be discussed on this thread eventually. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Deprecating legacy ASCII symbols?
It is interesting to look at competing systems and note that every one of them appears to be fully committed to a plain ASCII syntax as the only way of writing a formula. I think it may still be premature to abolish having ASCII even as an alternative syntax. I wonder whether the appearance of HOL.thy is that important to a typical beginner. Although it sets out the basic logic, it is full of implementation-specific details. I don’t really see how having ∧ in place of would improve its legibility. Then allowing users to use the symbol with some other meaning seems quite risky, at least in the short term. Larry Paulson On 29 Jun 2015, at 23:23, C. Diekmann diekm...@in.tum.de wrote: Dear list, the following mail may contain a stupid idea. In HOL.thy, the conjunction (conj) is first introduced with the symbol. Later, the notation ∧ is introduced. In order to clean up this difficult-to-understand theory, would it be possible to directly introduce conjunction with the ∧ symbol? I see three advantages: 1) It simplifies the axiomatizations (a very critical part). 2) It may help in getting started with Isabelle since no confusing symbol would appear anywhere. Currently, if a ctrl-click on a lemma sends me to HOL.thy, things look pretty scary. 3) It would free up the symbol for custom theories. This could also be done for %, --, ==, ~, and many more. I guess this would break a lot, that's why I'm posting on dev. Best, Cornelius ___ 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] Deprecating legacy ASCII symbols?
On Tue, 30 Jun 2015, Lars Noschinski wrote: In the editor buffer in Isabelle/jEdit, everything is mapped to unicode, so this is no longer an issue. You are right at a certain level of abstraction, but there is also a different thread by Lars Hupel about Unicode that I did not answer yet. The principle we have in Isabelle today is this: * Isabelle symbols are a plain ASCII notation for infinitely many mathematical (or other) characters, as specified in the implementation manual. * Unicode 3.x and a derivate of UTF-8 encoding is used to render that in the front-end. This works to the extent that most people think it is all perfect (which is not the case, because anything involving Unicode cannot be perfect). But the margin of error is sufficiently small to challange old ASCII replacement syntax now. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Deprecating legacy ASCII symbols?
On Tue, 30 Jun 2015, Larry Paulson wrote: It is interesting to look at competing systems and note that every one of them appears to be fully committed to a plain ASCII syntax as the only way of writing a formula. I think it may still be premature to abolish having ASCII even as an alternative syntax. Maybe some HOL4 guy can explain the details. They certainly do have ways to use non-ASCII, probably not as pervasive as for Isabelle. (I think they also have blue, green, brown variables.) In Coq the situation is mostly ASCII + some add-on modules that provide UTF-8 for a few important concepts. Some core Coq guys have told me that they would love to see more, but they are not there yet. So my general impression is that we are merely 10 years ahead of everybody else. Even more, we are conservative about ASCII: Isabelle symbols at the bottom *are* ASCII, just the front-end pretends something else. This means that the actual theory sources, if or when they are discovered by some archeologists in distant future, have a chance to be recognizable as something that makes sense: \forallx. x \le y \and y \le x etc. I wonder whether the appearance of HOL.thy is that important to a typical beginner. Although it sets out the basic logic, it is full of implementation-specific details. I don’t really see how having ∧ in place of would improve its legibility. Fresh users from the past 2-3 years often don't know the old ASCII syntax at all. Of course, basic HOL theories can be updated without any reform on old notation. This is just a good opportunity to sort out other problems: variance is always bad, and variance in pretty-printing syntax produces erratic results. We never managed to get the default vs. xsymbols output annotations right, just to keep them in sync concerning priorities, blocks, and breaks. Here are some recent examples: changeset: 60497:e726f88232d3 user:paulson l...@cam.ac.uk date:Wed Jun 17 15:15:52 2015 +0100 files: src/HOL/Groups_Big.thy description: correccted the pretty-printing specs for setsum and setprod changeset: 60585:1d31e3a50373 user:wenzelm date:Fri Jun 26 11:07:04 2015 +0200 files: src/HOL/HOLCF/Porder.thy src/HOL/Set_Interval.thy src/HOL/UNITY/Union.thy description: proper spacing, as for other syntax for these symbols; In such situations, one needs to look three times if it is more correct before or after, knowing that the results will be never sure. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Deprecating legacy ASCII symbols?
On Tue, 30 Jun 2015, Jasmin Blanchette wrote: This apparatus is rather heavy on beginners, and even experts will sometimes pause for a second to wonder whether they want to type :: or \Colon or whatever. I suspect one reason why John Harrison is so fast is that in HOL Light you don’t have to make such trivial decisions all the time. You are probably right about John Harrison and HOL-Light. Concerning :: versus \Colon I am in favour to get rid of \Colon altogether: there is visually no difference in final LaTeX documents, and in the editor it introduces a bit too much complication to my taste. The special \Colon symbol goes back to a request from David von Oheimb, when he still maintained the so-called 8bit package, i.e. the non-ASCII mode before the classic X-Symbol package of Proof General 2.x. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Deprecating legacy ASCII symbols?
Makarius wrote: * Convenience: users somethings find it too combersome to type proper Isabelle symbols. I never do that myself, but take the time to type things nicely. It is actually not much time for me, since I implemented the input methods myself and know how they work. Today we have at least three concepts: ASCII symbols—e.g., - xsymbols—e.g., \longleftrightarrow typing shortcuts (or whatever they are called)—e.g., - or -- To be complete, I should mention that xsymbols appear in two variants: the backslash-less-than-greater-than variant, the Unicode-like symbol one gets in jEdit. There used to be a third, wrong variant, at least in Proof General: the actual Unicode symbol, which paradoxically didn’t work when copy-pasted back from e.g. an email. (This is no longer an issue?) This apparatus is rather heavy on beginners, and even experts will sometimes pause for a second to wonder whether they want to type :: or \Colon or whatever. I suspect one reason why John Harrison is so fast is that in HOL Light you don’t have to make such trivial decisions all the time. Hence, I would be in favor of any process towards simplifying the situation. In particular, phasing out ASCII symbols gradually (and is as much this is possible w.r.t. compatibility) would make a lot of sense to me, as long as the corresponding typing shortcuts stay (and are documented). Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Deprecating legacy ASCII symbols?
I have no objection to phasing out some of the ASCII symbols. For me the main advantage is that they provide a graphic image that one can quickly recall as an input shortcut: == comes to mind more quickly than some alphabetic name and I would not want to lose that. But freeing them up in the input syntax (as opposed to the shortcuts) is not much of a gain because one cannot reasonably reuse them. But there is indeed quite a bit of duplication, eg and /\, | and \/. Some symbols like ! and ? are quick to type but I wouldn't call them graphical and am not particularly attached to them. In fact, one could then give factorial its standard syntax. Tobias On 30/06/2015 14:13, Makarius wrote: On Tue, 30 Jun 2015, C. Diekmann wrote: In HOL.thy, the conjunction (conj) is first introduced with the symbol. Later, the notation ∧ is introduced. In order to clean up this difficult-to-understand theory, would it be possible to directly introduce conjunction with the ∧ symbol? I see three advantages: 1) It simplifies the axiomatizations (a very critical part). 2) It may help in getting started with Isabelle since no confusing symbol would appear anywhere. Currently, if a ctrl-click on a lemma sends me to HOL.thy, things look pretty scary. 3) It would free up the symbol for custom theories. This could also be done for %, --, ==, ~, and many more. Interesting that you call this legacy ASCII syntax. In the manner it is done until today, the ASCII syntax is still the official syntax and the xsymbols variant some add-on. Only recently, the system default has changed to have xsymbols always enabled by default. Historically, there were good reasons of having the system act in plain ASCII by default, due to a general lack of reliability in rendering Isabelle symbols on various operating systems, terminal emulators, and versions of Emacs. Now that the TTY loop and Proof General are removed, there is nothing to prevent a fresh look at the situation. Here are just the canonical questions (which are never meant rhetoric): (1) Are there remaining uses of plain ASCII syntax in Isabelle output? (2) Are there remaining uses of plain ASCII syntax in Isabelle input? As a start to the collection of material some possible points: Concerning output: * Seemingly modern web frameworks might lack Unicode rendering quality to work with Isabelle symbols relibly. 1-2 years ago there were still problems on Stackoverflow. Do they still exist? In contrast, plain HTML pages should be able to provide the IsabelleText font from the server side. There is no need for the old HTML print mode. Concerning input: * Compatibility: huge amounts of existing sources still use ASCII input. There are chances to make a systematic upgrade for formally checked text, but not for unchecked comments. * Convenience: users somethings find it too combersome to type proper Isabelle symbols. I never do that myself, but take the time to type things nicely. It is actually not much time for me, since I implemented the input methods myself and know how they work. Anything further points? Once the collection of observation is complete, we can come up with further migration plans to improve on the historical situation. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Deprecating legacy ASCII symbols?
Concerning :: versus \Colon I am in favour to get rid of \Colon altogether: there is visually no difference in final LaTeX documents, and in the editor it introduces a bit too much complication to my taste. As far as I am concerned: By all means, kill it! At some point in 2014, I realized \Colon only made my life more miserable and stopped using it. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Deprecating legacy ASCII symbols?
On 1 Jul 2015, at 00:57, Makarius makar...@sketis.net wrote: On Tue, 30 Jun 2015, Larry Paulson wrote: It is interesting to look at competing systems and note that every one of them appears to be fully committed to a plain ASCII syntax as the only way of writing a formula. I think it may still be premature to abolish having ASCII even as an alternative syntax. Maybe some HOL4 guy can explain the details. They certainly do have ways to use non-ASCII, probably not as pervasive as for Isabelle. (I think they also have blue, green, brown variables.) We’ve had support for arbitrary user-chosen UTF8-encoded Unicode symbols since 2008, both in input and output. Emacs has pretty reasonable support for inputting Unicode if you turn on the TeX-input-method. Our emacs and vim editing modes further provide keybindings for common symbols (C-S-1 for ∀ is one more modifier key to press than S-1 (assuming that ! is shift-1)). We keep material under src/ as pure ASCII, but our examples/ directory is full of Unicode. E.g., val oleast_intro = store_thm( oleast_intro, ``∀Q P. (∃α. P α) ∧ (∀α. (∀β. β α == ¬ P β) ∧ P α == Q α) == Q ($oleast P)``, rw[oleast_def] SELECT_ELIM_TAC conj_tac - (match_mp_tac ordlt_WF0 metis_tac[]) rw[]); val ordSUC_def = Define` ordSUC α = oleast β. α β ` I’m not sure why I used the ASCII implication above rather than the Unicode version, but it does illustrate the way in which the input symbols can be freely mixed. Perhaps as a leap of faith, we believe that UTF8-encoded Unicode will be just as readable as ASCII to the archaeologists of the future. Certainly, in the present day, it’s nice to be able to read and access sources with tools such as less, grep etc. and to see stuff like the above. Michael The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Deprecating legacy ASCII symbols?
Dear list, the following mail may contain a stupid idea. In HOL.thy, the conjunction (conj) is first introduced with the symbol. Later, the notation ∧ is introduced. In order to clean up this difficult-to-understand theory, would it be possible to directly introduce conjunction with the ∧ symbol? I see three advantages: 1) It simplifies the axiomatizations (a very critical part). 2) It may help in getting started with Isabelle since no confusing symbol would appear anywhere. Currently, if a ctrl-click on a lemma sends me to HOL.thy, things look pretty scary. 3) It would free up the symbol for custom theories. This could also be done for %, --, ==, ~, and many more. I guess this would break a lot, that's why I'm posting on dev. Best, Cornelius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
