LeanVerso BookExamples

Stream: new members

[HenriqueBorges6]

Hello ! I am new to Lean !
I would like to learn about the Lean Verso to write some documents with Lean code
someone has examples of books and others

[Tyler Josephson ⚛️]

There are examples here:
https://github.com/leanprover/verso/tree/main/examples

Here’s another one:
https://lecopivo.github.io/scientific-computing-lean/

If you’re new to Lean, though, I recommend learning more about Lean, through resources like https://lean-lang.org/functional_programming_in_lean/ and https://leanprover-community.github.io/mathematics_in_lean/

[Tyler Josephson ⚛️]

Furthermore, the main author of Verso, David Christiansen, recommends talking with him first before embarking on any serious authoring projects, since he’s still developing Verso and it’s likely to change in the short term.

[Filippo A. E. Nuccio]

Speaking about Verso, is there a way to visualize a Verso document inside VSCode? I am preparing my classes, and I have a md with a lot of lean code snippets that I normally show in VSCode before opening the lean window to show this code "live". Is there anything similar using Verso? Can I ping @David Thrane Christiansen ?

[David Thrane Christiansen]

I'm knee-deep in writing an updated Lean reference manual in Verso, which will be a great example just as soon as it's ready for release! Right now, I don't want the incomplete draft to confuse readers, so it's not public quite yet.

I don't expect the fundamentals of Verso to change much, but many of the details will. The biggest issue for other users is going to be, ironically enough, the lack of documentation

[Filippo A. E. Nuccio]

Oh I see, thanks. I have just tried to download verso from github and to run lake build but got some errors (mainly about a lean4:v4.5.0 not being installed, which shocked me as it is a bit out-of-date). Indeed, I thought that after all if I can produce a html, VSCode is able to render it quite well and I was wondering if this is actually what the md reader of VSCode does, so that it would work smoothly with a verso-generated html. But if all this is premature I will stick to my md files for the time being.

[David Thrane Christiansen]

Filippo A. E. Nuccio said:

Is there anything similar using Verso? Can I ping @David Thrane Christiansen ?

No and yes :-)

[Filippo A. E. Nuccio]

Oh, so my above text is nonsensical.

[David Thrane Christiansen]

I didn't see any nonsense. It would absolutely be possible to build a Verso genre and a little plugin to render things, but nobody has yet done so and it's not currently at a place on my priority list where it's likely to get worked on. Verso is designed to be extended by users, though, so you are absolutely free to build such a thing yourself, and you don't need my permission :)

[Filippo A. E. Nuccio]

It is probably well beyond my paygrade at the time being, but thanks! I might think about it...

[Britt Anderson]

I just installed verso, but reading this I wonder if the advice at this time for "new members" is not to use Verso until the new manual is ready?

[Kevin Buzzard]

I think verso is fine to use if you just want to knock up a web page. For example DeepMind seem to have figured out how to use it here. I would imagine that people will be happy to help out if you have questions.

[Eric Wieser]

DeepMind figured out how to use it largely because David was very generous with his time even while on vacation!