Highlighting and running Lean code online

Stream: new members

[RexWang]

Hello everyone, I'm planning to develop a website of learning notes of LEAN.

As I work on the development of this site, I have come to a couple of questions that I would greatly appreciate your guidance on:

Q1: Where can I find a code snippet similar to the one used for Python highlighting?

I'm looking for something like this:

<script src="//unpkg.com/prismjs/components/prism-python.js"></script>

Q2: How can I incorporate Lean code execution on the website?

For example, I came across the Lean4game engine, which is used for NNG4. However, this may be too advanced for my specific use cases.

Furthermore, I recently discovered an elegant website written in French that beautifully illustrates Lean proofs. Take a look at Learn Math 114.


The presentation style on this site is truly impressive and serves as a great source of inspiration for my own website.

Thanks in advance for your valuable assistance!

[Patrick Massot]

About Q1, there are two main options. You could use pygment to prerender the web pages. This is what we do on the community website for instance. Then you only need the pygment css file. You could also try some javascript syntax highlighting. At some point we created https://github.com/leanprover-community/highlightjs-lean/ but the reason we did that is no longer relevant and I think nobody is maintaining it.

[Eric Wieser]

I still use highlightjs-lean, though it needs some updates for Lean 4

[Patrick Massot]

Your screenshot of my lecture notes uses https://leanprover-community.github.io/format_lean/ which I very quickly wrote in early 2019 because no such thing existed at that time. But this is only for Lean 3. It was meant to be replaced by LeanInk but I'm afraid this is no longer actively maintained (but I'd be delighted to see someone investing time there).