Lean4 highlight.js name conflicts

Stream: lean4

[David Thrane Christiansen]

As I finish up _Functional Programming in Lean_, I'm encountering more and more situations where tactic names collide with other names. For instance, the intro tactic collides with the name of And.intro and True.intro,.

I'd very much like the rendered version of the book to have accurate highlighting. This implies that And.intro should be highlighted like any other constructor of a structure, and that the intro tactic should be highlighted just like the case or induction or split tactics. I think that it's not feasible to extract accurate highlighting from Lean itself with the time and resources that are available, unfortunately, so I think I'm looking for the best kludge.

One thing that seems doable is to have two highlight.js languages configured, one with keywords defined for the tactics used in the book, and one without. Then I can make sure that every tactic proof uses the leanTac language, and that ordinary programs use leanProg. This seems tedious and error-prone, but I can make it work. Does anyone else have another way to achieve accurate highlighting of a restricted set of examples?

[Eric Wieser]

It ought to be possible to hightlight intro and .intro separately

[Eric Wieser]

Where does the lean4 highlight.js code live?

[David Thrane Christiansen]

Unfortunately intro occurs bare in the definition of And:

structure And (a b : Prop) : Prop where
  intro ::
  left : a
  right : b

I'll be opening up the repo for FP Lean very soon - it has a highlight.js based on a version that intended to highlight both Lean 3 and 4, and required lots of manual tweaking to achieve accuracy on the book's examples.

[David Thrane Christiansen]

In other words, I don't know a good way in a regexp-based highlighter to make this intro look one way, and the intro tactic look another way. At least not one that isn't quite brittle and tricky.

[David Thrane Christiansen]

(I do suspect that there's some kind of way to make things under by highlight differently than other things, but now it's starting to remind of hacking font-lock configs, and I unfortunately don't have the time for that)

[Eric Wieser]

I'd claim that trying to highlight both versions of lean with a single highlighter is a mistake

[David Thrane Christiansen]

Don't worry - the code no longer tries to do that. Nonetheless, trying to highlight Lean with regular expressions is also a mistake, but that's a mistake that I have no alternatives to at this stage in the project :-)