[isabelle] License for Isabelle fonts

Makarius

2018-09-20 10:17:01 UTC

Post by Sebastien Gouezel
I would like to distribute a TeX file using Isabelle fonts (the ones
used in jEdit) to typeset some Isabelle code. I did not find a clear
license for these fonts, so I am wondering if this is permitted. There
is a README file in the Isabelle fonts directory describing all the
(free) licenses of the fonts they are made of, so I guess Isabelle fonts
are meant to be free, but I would prefer to have something more explicit
(especially if this ends up being published in a journal).

I am responsible for the Isabelle fonts and would say that is OK.

Maybe the confusion is that the fonts used to be part of the Isabelle
repository and were thus implicitly subject to its BSD-style licensing.
The README was meant to justify its inclusion into that license model:
these somewhat non-standard font licenses are very liberal and seem to
allow that.

Later I moved the fonts into a "contrib" component, because binary
artifacts inside a repository are bad style. I should probably have
changed the README as well.

BTW, "Isabelle code" is an unfitting term for the formal document
sources that we have in Isabelle/Isar. Historically, "code" is something
that is only machine readable, but the point of Isar is to make it both
machine-readable and human-readable.

The general trend is to make Isabelle source more and more look like the
actual document, such that it can be printed mostly verbatim. E.g. see
the recent addition of fancy markdown list notation.

To this end, I intend to replace the hand-edited Isabelle fonts by a
little Isabelle/Scala front-end to fontforge that turns suitable base
fonts into ones containing our Isabelle symbols. In particular, I would
like to see non-monospaced Isabelle fonts for really high-quality
printing of Isabelle document sources.

Makarius