Issues with syntax highlighting in docstring codeblocks

Stream: lean4

[Thomas Murrills]

I noticed two issues with codeblocks in hovers:

In editor hovers: markdown codeblocks that use “lean4” as the language are syntax-highlighted correctly, but ones that use “lean” aren’t. Currently almost all of the codeblocks in mathlib use “lean”, not “lean4”, and so aren’t highlighted.

Should (can?) “lean” be supported, or should we stick to "lean4" (possibly providing a linter that corrects lean to lean4)?

In infoview hovers: although there is code in the extension that attempts to syntax highlight codeblocks, it doesn’t seem to be working; no language seems to get highlighted.

I'm happy to open issues on the extension repo, but thought I ought to bring them up here first (in case there's an easy fix, or if we're already collectively aware of the behavior).

MWE:

/--
Compare the syntax highlighting in these code blocks when hovering on `x`:

```lean
example : True := by trivial -- 'lean': Not highlighted
```

```lean4
example : True := by trivial -- 'lean4': Highlighted
```

```
example : True := by trivial -- none: Highlighted by fallback to editor highlighting
```

```js
function foo() { return "bar" } // Might be highlighted or not depending on system
```
-/
theorem x : True := True.intro

example : x = x := by
  -- Hover on `x` in the infoview; no highlighting
  trivial

[Eric Wieser]

If you install the lean3 extension, then both will work

[Eric Wieser]

My guess would be that vscode is using its syntax database (keyed by language name) to format markdown code blocks

[Eric Wieser]

And registering both lean3 and lean4 with the same name would make it impossible to use both extensions at the same time

[Eric Wieser]

Another consideration here is that pygments, which Zulip and \usepackage{minted} use, calls the languages lean and lean4

[Thomas Murrills]

But to be clear, if I install the lean3 extension, these codeblocks will be highlighted in lean3, right?

[Eric Wieser]

Yes

[Thomas Murrills]

That makes me wonder if we ought to have lean mean lean4 now, and lean3 reserved for lean3

[Thomas Murrills]

(Though I suppose that might break old repos...)

[Eric Wieser]

Does ```lean vs ```lean4 make any difference to doc-gen?

[Eric Wieser]

Thomas Murrills said:

(Though I suppose that might break old repos...)

Optimistically things would be ok (within vscode), but this would require a re-release of the lean3 extension

[Eric Wieser]

Changing pygments is slightly more obnoxious, as this would cause rebuilds of old LaTeX documents to start highlighting lean3 code as lean4, and makes it harder to spot whether zulip code is lean3 or lean4

[Eric Wieser]

(and also changes to pygments are on a 6-month release cycle)

[Thomas Murrills]

Hmmm, I guess that means the benefits of consistency ought to be taken into account: it might be odd for lean to mean lean4 in VS code and lean3 in e.g. LaTeX. Though I personally could get on board with pushing for lean to mean lean4 in as many places as reasonably possible...

[Eric Wieser]

Perhaps also of note:

-- this is a ```lean codeblock, which links to both playgrounds to avoid confusion
macro not_in_lean3
abbreviation i_only_exist_in_lean3

-- this is a ```lean3 codeblock, which zulip cannot treat differently from the above
macro not_in_lean3
abbreviation i_only_exist_in_lean3

-- this is a ```lean4 codeblock, which links only to the lean4 playground
macro i_only_exist_in_lean4
abbreviation not_in_lean4

which is controlled by a mixture of these lines in Pygments and the Zulip settings

[Thomas Murrills]

Eric Wieser said:

Does ```lean vs ```lean4 make any difference to doc-gen?

It seems like doc-gen doesn't do any lean syntax highlighting for code blocks (whether lean, lean4, or no language specified).

[Thomas Murrills]

(Here's lean, here's lean4, and here's no language specified. I'm not sure if it influences the linkification of constants in any way...)