Syntax highlighting in doc-gen

Stream: general

[Hanson Char]

On a completely different topic, apparently syntax highlighting of lean is still not supported at Github. Seems this has been discussed since 2023.

But the support for Lean 4 seems to have been merged. So perhaps it's already supported?

In any case, markdown code block using the tag lean or lean4 doesn't work wrt syntax highlighting in lean doc (using doc-gen4) :(

[Eric Wieser]

Are you asking about github or doc-gen?

[Eric Wieser]

some.knowit said:

apparently

I don't think that an omission from a random github repository is a particularly strong signal. You could make a PR against that repo to prove that lean is supported after all.

[Hanson Char]

Eric Wieser said:

Are you asking about github or doc-gen?

Both.

[Eric Wieser]

I created #general > Markdown codeblocks: `lean4` or `lean-4`? @ 💬 about github

[Hanson Char]

Interesting! btw, perhaps it should just be lean instead of having a version number suffix, unless there is a strong reason to believe that the next version of lean is going to be so completely different from lean 4, I guess?

On the other hand, I tried lean, lean4 and lean-4, but none of them worked in the markdown of doc-gen4. Guess I can open an issue to see how it goes.

[Eric Wieser]

lean was already taken by lean 3 code

[Notification Bot]

7 messages were moved here from #general > Is there a way to skip doc gen of mathlib4? by Eric Wieser.

[Eric Wieser]

but none of them worked in the markdown of doc-gen4. Guess I can open an issue to see how it goes.

I think what's missing here is including highlight-js or similar

[Hanson Char]

I've just opened an issue at doc-gen4.

[Jz Pan]

some.knowit said:

On the other hand, I tried lean, lean4 and lean-4, but none of them worked in the markdown of doc-gen4. Guess I can open an issue to see how it goes.

No, doc-gen4 does not support any form of syntax highlighting for markdown codes for now. And syntax highlighting may be conflict to some built-in feature of doc-gen4, i.e. currently doc-gen4 will try to identify theorem names in code block and link them to corresponding page.

[François G. Dorais]

Jz Pan said:

some.knowit said:

On the other hand, I tried lean, lean4 and lean-4, but none of them worked in the markdown of doc-gen4. Guess I can open an issue to see how it goes.

No, doc-gen4 does not support any form of syntax highlighting for markdown codes for now. And syntax highlighting may be conflict to some built-in feature of doc-gen4, i.e. currently doc-gen4 will try to identify theorem names in code block and link them to corresponding page.

Conflicting in what sense?

[Jz Pan]

Conflicting in what sense?

I don't know so I just say "may be"...

Maybe you can try manually load that javascript on the current doc page and see if it works?