Lean4 react-syntax-highlighter on streamlit

Stream: general

[Anirudh Gupta]

Hi, This is Anirudh, from IISc Bengaluru.
I am trying to create a streamlit website for a project, which requires me to print the lean code on the website. Now Streamlit is very convenient and it provides a st.code API which can do the same, with syntax highlighting of any language present in react-syntax-highlighter.
I found out that Lean4 has this highlightjs-lean, which is great.
So I had made an issue on GitHub at react-syntax-highlighter/react-syntax-highlighter #587 so that lean4 can be added to the list and hence ill be able to use it on streamlit, but the repo seems unmaintained.

I would like to know if there is any other way/any ideas on how to get lean4 syntax highlighting on react-syntax-highligher or atleast streamlit.

Thanks!

[Marc Huisinga]

highlightjs-lean seems like your best bet for react-syntax-highlighter. There are a number of different grammars for Lean (none of which can provide proper semantic highlighting), but the highlight-js one seems like the only one that can be consumed by react-syntax-highlighter.

[Eric Wieser]

Note that highlight-js lean is:

• On an old highlight-js version
• Not adapted to Lean 4

I have a local version of the latter I can try to PR in the new few weeks

[Anirudh Gupta]

Eric Wieser said:

Note that highlight-js lean is:

• On an old highlight-js version
• Not adapted to Lean 4

I have a local version of the latter I can try to PR in the new few weeks

Yes that would help a lot! Great thanks

[Anirudh Gupta]

Marc Huisinga said:

highlightjs-lean seems like your best bet for react-syntax-highlighter. There are a number of different grammars for Lean (none of which can provide proper semantic highlighting), but the highlight-js one seems like the only one that can be consumed by react-syntax-highlighter.

Yes, true.
But I am looking for a way to add lean4 syntax highlighting within streamlit, since the repo is unmaintained(as mentioned previously), I donno any other way on the syntax-highlighter to work.

[Anirudh Gupta]

Eric Wieser said:

Note that highlight-js lean is:

• On an old highlight-js version
• Not adapted to Lean 4

I have a local version of the latter I can try to PR in the new few weeks

Hi @Eric Wieser , I have got some response and method on how to get this done in this comment.
Can you pls share the latest version of the syntax-highlighter, so that I can try the mentioned steps in the commet?

Thanks! :blush: