How are the HTML example pages created?

Stream: new members

[Matthias Geier]

I'm talking about those examples: https://lean-lang.org/documentation/examples/

... and more importantly, how can I create similar pages for my own examples?

I have seen https://github.com/leanprover/lean4/blob/master/doc/dev/mdbook.md, but it seems outdated, because I have the feeling that the examples are not rendered with Alectryon but with Verso, right?

Are there any instructions how to create a bunch of HTML files from a bunch of Lean files with "literate" comments (if that's the right word)?

There is an example at https://github.com/leanprover/verso/tree/main/examples/website-literate, but it seems to be embedded in another example and the overall setup is quite a bit more involved than what I hoped for.

I would like to have auto-generated outputs for #eval and maybe also for #check.

[Kevin Buzzard]

Yes, the examples in the documentation are using Verso. I thuink the mdbook.md link you posted must be quite old.

[Matthias Geier]

Thanks! So I guess Verso is the way to go. Does anyone have a simple example how to set up a few "literate" Lean files to be turned into HTML pages? Something that's less complicated than https://github.com/leanprover/verso/tree/main/examples/website-literate?