blogging platform for lean prover

Stream: new members

[Asei Inoue]

I write a blog post about lean prover. However, none of the existing services work with lean syntax highlighting, and I hope that a blog service will be created to talk about lean.

Does anyone else feel the same way?

[Asei Inoue]

The features I want in a blogging service for lean include:

• (required) syntax highlighting for lean4
• (Required) automatic link to lean web editor from code blocks.
• (Want) GitHub integration, so I can git manage my posts.

[Mario Carneiro]

I think the zulip code formatter is from prettier

[Mario Carneiro]

which supports lean

[Mario Carneiro]

github uses a different formatter which also supports lean

[Mario Carneiro]

Generally for a blog you would be responsible for installing the extensions to support the languages you work with if they aren't built in to the platform

[Asei Inoue]

Does prettier have plugin for lean prover?

[Asei Inoue]

How is the jump to the lean web editor in Zulip implemented?

[Markus Schmaus]

Code Block Pro is a WordPress plugin and I've asked it's maintainer to add Lean 4 support ((Github: Adding Lean 4)[https://github.com/KevinBatdorf/code-block-pro/issues/247]). Though progress on this seems to be stuck for some weeks now.

[Eric Wieser]

Mario Carneiro said:

I think the zulip code formatter is from prettier

I'm pretty sure it's pygments

[Alex J. Best]

You could just copy the lean community blog set-up via github pages, https://github.com/leanprover-community/blog/tree/master.