[isabelle-dev] Deprecating legacy ASCII symbols?
makarius at sketis.net
Tue Jun 30 16:57:09 CEST 2015
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: \<forall>x. 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:
user: paulson <lp15 at cam.ac.uk>
date: Wed Jun 17 15:15:52 2015 +0100
correccted the pretty-printing specs for setsum and setprod
date: Fri Jun 26 11:07:04 2015 +0200
files: src/HOL/HOLCF/Porder.thy src/HOL/Set_Interval.thy
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.
More information about the isabelle-dev