The Coq mailing list

[Makarius <makarius AT sketis.net>]

On Fri, 26 Feb 2016, Clément Pit--Claudel wrote:

> On 02/26/2016 05:53 PM, Makarius wrote:
> > This is why I said we are more and more departing from official
> > Unicode -- and were actually never really using it. The task is not
> > to comply with a monster standard, but to support mathematical
> > symbols in formal texts (including sub/superscripts and bold face).
>
> Aren't subscripts and superscripts a markup issue? They seem to have 
> little to do with Unicode.

Which is a problem of Unicode, and thus we are back to the key issue: to 
define the problem that should be solved. For me it is as follows:

  * Provide nice mathematical symbols for formal theory sources.

  * Make this "just work" for all users on all platforms, such that there
    is no reason not to use it by default everywhere (especially in the
    basic libraries).

  * Minimize assumptions about available technology, e.g. the editor
    and/or browser, to make it feasible for IDE implementors to support
    that by default.

  * Stretch it is as far as feasible, without changing the game of plain
    text editing into rich-text editing: e.g. support sub/superscripts and
    potentially some alternative text styles.

For example, it should be easy to use arrows with some decoration via 
superscripts. Bold symbols are also nice to have, to produce a second copy 
of popular symbols for applications.


> Is this approach superior to just using a smarter display layer, like 
> Emacs does with prettify-symbols-mode or Proof General's unicode-tokens 
> (which supported HOL and Isar a while ago)?

I am familiar with the classic approach in Proof General 3.x and 4.x, 
first X-Symbol mode, later unicode-tokens, but not with the most recent
version of it.

After a lot of elisp hacking, Emacs can do many things, but it also 
imposes a burden to anyone else who wants to implement something in a 
proper IDE framework: these usually lack smart display layers.


> It seems that the core Isabelle is essentially ASCII only, but the IDE 
> comes with a rendering engine that uses a translation to and from a 
> non-ASCII string to display pretty math into a basic text box. Is this 
> better than using a smarter text box (one that would be aware of 
> Isabelle's markup)?

This is again in conflict with "minimize assumptions about available 
technology".

I recall the Matita guys trying to provide smarter text boxes for OCaml 
GTK (based on MathML). Did this ever reach the big masses of users on all 
platforms?


> > The principle is this: authentic sources are stored as plain text with 
> > explicit symbol names.  Thus the repertoire of symbols is easily 
> > extensible and decodable by archeologists who find our proof 
> > repositories in distant future.
>
> I see; thanks. Most Coq developments seem to follow this principle too, 
> using plain text only. It's easy then to set up one's editor to display 
> plain text documents with pretty symbols (Proof General does it 
> optionally with unicode-tokens; company-coq does it by default). If I 
> understand correctly, though, Prof. Pierce doesn't seem fully satisfied 
> with this solution.

The difference is that Isabelle users hardly ever see this plain text 
representation of mathematical symbols. For all practical purposes of 
editing and browsing, proper mathematical notation is used by default.
This is also what appears in the printed documents (via LaTeX).


> > There are more such traps hidden in Unicode, e.g. "Combining 
> > Characters". This means you can never be quite sure what the equality 
> > on character strings really is.
>
> Unicode defines various level of language-awareness in string 
> comparisons, all under the headline of collation 
> (http://www.unicode.org/collation/). Is this relevant to that issue?

Maybe.  It looks like one of these massive Unicode documents that answer 
questions that I never intended to ask. Thus it is just a diversion from 
the problem to support basic mathematical typesetting in formal sources.


        Makarius