[isabelle-dev] Font license compatibility

Makarius makarius at sketis.net
Thu Feb 6 16:04:54 CET 2020

On 06/02/2020 13:56, Joshua Chen wrote:
> Would anyone know if the BSD-3 license on the Isabelle DejaVu fonts
> plays well with the SIL OFL (Open Font License)? For my own visual
> comfort I've merged whatever Isabelle symbols were missing into the Fira
> Code and Source Code Pro fonts for use in Isabelle/jEdit, and have been
> using these as replacements for the default font without problems.
> I think it would be nice to be able to put these online as alternative
> options, but am not sure about licensing. The OFL must be kept in
> derivative works, but I wonder if the BSD license can be attached on?

I don't know much about complex license merges, but the main problem will be
actually longterm maintenance: by producing adhoc manual patches of fonts, you
will rather quickly fall behind ongoing Isabelle development. The very point
of Isabelle symbols is that its infinite name space is mapped to a finite
selection of commonly used symbols, together with glyphs in the Isabelle fonts
and corresponding LaTeX macros.

To apply this principle to different base fonts than DejaVu, the proper way is
to refine the "isabelle build_fonts" tool:

This approach (when done properly) will provide repeatable results. Moreover,
the licensing question disappears: the Isabelle/Scala sources remain under the
existing BSD3 license, and the resulting fonts emerge only for the user who
invokes the tool.


More information about the isabelle-dev mailing list