highlightjs

Stream: general

[Patrick Massot]

Two years ago, we were using gitter which was using highlighthjs for syntax highlighting. This lib knew nothing about Lean so I quickly hacked a syntax file and opened a PR. But highlightjs had no maintainer at that time, and that PR fell into a black-hole. Two days ago I was asked to create a third party repository hosting that syntax file. The community no longer needs Gitter, and we couldn't even find enough energy to fix the pygments issue in Zulip (all those red rectangles we see in code blocks). But it's still nice to have more online syntax highlighting options. So I'm tempted to answer we could host that Lean highlightjs module on our leanprover-community organization. It looks like I would need to spend an hour setting things, but then it wouldn't need more time unless people start sending bug reports. What do you think?

[Bryan Gin-ge Chen]

I just found this thread again when thinking about the pygments stuff. @Patrick Massot I would actually appreciate this since Observable notebooks use highlightjs for syntax highlighting.

[Patrick Massot]

Ok, so what is the plan here? Do you want to create that highlightjs-js repository? We need to decide whether it should be hosted by the highlightjs organization or by leanprover-community. A tiny advantage of highlightjs is that it would be more visible to people wanting to make a custom build of highlightjs including all third-party languages. Otherwise self-hosting probably makes more sense.

[Bryan Gin-ge Chen]

I don't mind creating it. I'll ask again here when I'm done to see how to get it transferred to leanprover-community.

[Patrick Massot]

I could have created the project directly in leanprover-community, I only waited for some decision regarding the organization choice.

[Bryan Gin-ge Chen]

Oh, I assumed we would just create it under leanprover-community. Anyways, here's the repository I made: https://github.com/bryangingechen/highlightjs-lean

I copied what some other highlightjs grammars did for the overall structure and testing. Let me know if you want me to change the license or anything in the readme. I defaulted to BSD-3-Clause since that's what highlightjs itself uses. If you're more or less OK with it go ahead and make a leanprover-community/highlightjs-lean and give me push privileges and I'll move everything over (with URLs changed to leanprover-community).