Isabelle symbols outside its editor

If you’ve ever used Isabelle, and taken a peak at the files you’re writing in any editor that is not one Isabelle is intended to be used with, you’ll be familiar with the funny escape sequences it uses to represent non-ASCII characters:

Perhaps you’ve even gone through a stage of wondering “well why does it do that? Surely it could just use Unicode for everything, the way Lean and Agda do?”

It may be surprising, but even today, not everything one might want to write in mathematical writing is available in Unicode. Mainly, this is there’s some things Unicode itself considers to be out of scope: layout, subscripts, emphasis, non-horizontal writing directions … and so, while historical accident has forced the inclusion of some subscript characters and some superscript characters, these don’t even cover a full Latin alphabet!

So in a bid to do things properly, Isabelle instead stores pure ASCII files, and implements its own escape sequences. Isabelle’s blessed editor (be that its modified version of Jedit, or now also of VSCode—or even Emacs, if you dare be a renegade and use a fork) will render them for you.

So in a way, Isabelle agrees with Unicode on what should be done: store things which are not obviously text elsewhere. Only it goes a step further, and simply disregards unicode as a whole: all non-ASCII symbols use the same system of escape sequences.

And this works wonderfully for writing mathematics!

Unfortunately, I like to read the files on my disk! In particular, I like grepping the Isabelle sources for fitting definitions. I also like putting my projects into version control, and occasionally (and in academia, it seems this is controversial) I even like to look at the diffs! Worse, sometimes I collaborate with people and have to make sense of their diffs!

There’s ample tooling for creating nice HTML and L^AT_EX versions of Isabelle theories. Or I could just read them in Jedit. But that requires starting Isabelle, loading the file, waiting for proofs to be checked … and even then, for diffs I am out of luck. And sometimes I simply do not want to leave my habitual environment.

So what to do?

Symbols

There are multiple kinds of symbols that Isabelle can use. Some information on these is given in Annex B of its reference manual [IsB]:

• Those that denote a non-ASCII character, e.g. \<Forall> or \<Rightarrow>; helpfully there is a defined Unicode equivalent for each of them.
• Those that control type setting of the next character, e.g. \<^sub> and \<^sup> for sub- and superscript, or \<^bold>. These also have a defined Unicode representation (e.g. ⇩ for \<^sub>), still readable as in-kind markup
• Arbitrary names, which appear to mainly be used by the new-style ML antiquotations, e.g. \<^make_string> in place of the old @{make_string}. These have no Unicode equivalents, but I also find them readable enough on their own.
• There are also \<^bsub> ... \<^esub> and similar constructs to control type setting of whole text ranges. The manual cautions: “note that there are limitations in the typographic rendering quality of this form”. I have never seen these used.

Conversion

So if you have a theory file, and an output that cannot do fancy layouting, there’s a pretty obvious thing to do: for all symbols that do have Unicode representations, simply render them as that. In fact, Isabelle’s own programming interface in Scala even exposes a ready-made Symbol.decode function (thanks to Fabian Huch who wrote a little script demonstrating its use on the zulip).

Unfortunately, as this is Scala, using it requires loading an entire JVM (and parts of Isabelle) on startup. Doing this for a single string is beyond abysmal in performance for any practical task.

isabelle2unicode

So instead I wrote a little rust crate which does the same.

And as we all know, anything written in rust is blazingly fast probably faster then starting a one-shot JVM for a single-pass edit over a string 🙃

(how does it find Isabelle’s home directory? It doesn’t, it just has the default symbols list compiled in statically. So far I was never tempted to define my own symbols, so probably this is fine …)

This’ll incur some losses: if whole words are set in subscript, this results in:

Variable⇩I⇩n⇩d⇩e⇩x⇩e⇩d⇩_⇩a⇩_⇩m⇩u⇩c⇩h⇩_⇩t⇩o⇩o⇩_⇩l⇩o⇩n⇩g⇩_⇩w⇩o⇩r⇩d

Obviously, it’s not too hard to recognise a couple such special cases. But I never really bothered to do so — I’ll leave that as an exercise for the people who like naming their variables like that.

Use in git

I’ve sat on this tool for an almost embarrassingly long time, using it only occasionally to read up on Isabelle sources when (rip)grepping through them to find some specific function or definition or two, before I thought of using it in other places.

For example, git has a neat little switch to apply a textual transformation before it displays files! While intended to make changes in binary files intelligible on git’s cli interface, git will happily pretend that ASCII-only Isabelle theory files are binary if you put something like this into its config:

[diff "thy"]
   binary = true
   textconv = "isabelle2unicode"

And then also specify for which files these diff settings should be used:

*.thy -diff=thy

Together, these make git diff produce nice, delightfully readable output:

Use in cgit

Trivially, other programs can use isabelle2unicode as a little pipe in appropriate places. As an easy example, my cgit instance uses in its syntax highlighting script when generating output, so on there Isabelle files are readable now, too.

(Well. The one Isabelle file I actually keep on there, that is)

Similar usage could be integrated in other git forges, probably; but I’m not currently running an instance of any of them, so doing so is left as an exercise for you readers :D

Mail Client Extension

How nice would the world be if we only ever interacted with code through tools built specifically for that purpose, with easy extension hooks!

Alas, someone invented Emails. And webservers. And web-based UIs.

Even less fortunately, when I collaborate with people, we might set up a shared git repository. And if it’s not the kind of project I check every day, the easiest way to stay in the loop with what the others are doing is everyone’s beloved notification email containing a diff.

Obviously, neither the git forge, nor my mail client, nor anything else in this whole chain of tools knows about Isabelle’s markup. Perhaps, if I controlled every git server I use even tangentially, it would be feasible to patch them all. Alas.

However! Thunderbird, my chosen mail client at-work, is extensible, and it’s not too hard to write a little plugin which will traverse all the document nodes, scan each node’s inner text for Isabelle-style escape sequences, and perform the same conversion to Unicode:

There is an unfortunate wrinkle here: some forges like to perform syntax highlighting in their diffs, which inserts little <span> tags into the text for colours. If such a <span> is rude enough to interrupt an escape sequence, we are in trouble:

To be honest, I’m not sure what to do about this one; however obvious the problem, a clear solution seems hard to formulate. Should it move the <span>, at a guess? In which direction? We cannot know what semantic content these carry while performing the substitution, so it’s not clear at all how to do anything at all that won’t turn out to be unhelpful.

Firefox

HTML emails are basically web pages, and mail clients basically browsers. So there’s no trouble at all in tweaking the extension a little to also work as a general web extension for FireFox.

I should probably note that, in fact, there already is a similar extension for FireFox called Matisa, which is much fancier than mine: it converts the markup to equations displayed with MathJax. Unlike the pure Unicode substitution, it can thus handle subscripts reasonably!

So if you want that, you probably want to use that plugin instead.

Comfortable software

To be honest, this blog post feels almost trivial, to the point that I’m wondering why I wrote it, and spent so many words belabouring the point that “you can tweak this thing a little make it look nicer”. It’s so trivial; Isabelle is research-software, but nothing in the way of research is going on. Nor is the symbol replacement difficult at all; it fits into a single regex, looking up captures, and replacing those for which an entry was found.

It feels completely implausible that anyone who can use Isabelle can not also write the exact same tool.

Still, here is a blog post. Why? Maybe I should just be happy, reading my diffs in git, enjoying collaborations where I can read the notification emails without squinting. I can assume everyone else is doing the same, and not write this many words about it.

Except, well — it’s been over half a decade since I first encountered Isabelle. I wrote the initial version of isabelle2unicode pretty soon afterwards; the initial commit was on 2021-06-23. Writing it felt trivial; I remember the main thought I had while doing it was “huh, kinda odd that the isabelle executable seemingly doesn’t have a ready-made subcommand for that, probably I just missed it”.

And yet, it took me five years to find all the little crooks where I could use it. And yet, nobody I’ve ever collaborated with on an Isabelle-based project seemed to do something similar. And while I do sometimes feel the cynic thoughts whispering to me that nobody else in academia actually reads their collaborator’s commits before once again hacking the project into entirely surprising and undiscussed directions, I can’t believe that’s wholly true.

But also, because I appreciate this kind of software. I wish to be writing it more, I wish we’d prioritise creating tools that are bent towards working well for their users more. So here you go. I’ve told you about a little trivial tool that makes the things I do friendlier to spend time with. Perhaps you could tell me about your trivial-but-friendly tools, too?

References