[isabelle-dev] Deprecating legacy ASCII symbols?

[Makarius]

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:

changeset:   60497:e726f88232d3
user:        paulson <lp15 at 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