Verso and the FPiL Book

Stream: general

[Alexandre Rademaker]

Regarding the FPiL book, I appreciate the ongoing efforts to develop the new Verso format. However, the transition to Verso feels like a step backward in some ways. We lost the search functionality, and the formatting seems less polished compared to resources like Mathematics in Lean and The Mechanics of Proof. What do you all think? I am planning to start writing a book and am curious to know what other authors have to say about Verso or alternative approaches for an online book.

[suhr]

The Lean Reference has search though, so the lack of search in FPiL does not seem to be due to a limitation of Verso.

[suhr]

It seems like the search is still somewhat limited though.

[Sebastian Ullrich]

Full-text search is coming!

[Patrick Massot]

I think starting a new Lean book using anything else than Verso would be extremely unwise.

[Patrick Massot]

I agree the cosmetic aspect is not yet great, but anyone can contribute CSS to Verso, you don’t to wait for David to turn into a web designer.

[Alexandre Rademaker]

Thanks @Sebastian Ullrich for the update.

I agree @Patrick Massot, and I am willing to try Verso. Yes, perhaps my personal preferences regarding the cosmetic aspect (as you mentioned) can be easily addressed with some CSS adjustments.

That said, let me emphasize that I really respect the work @David Thrane Christiansen is doing with Verso. I was trying to contribute my personal perspective on the current Verso documents, have updates from the community, and see what directions people are considering. @Terence Tao is using Verso in https://github.com/teorth/analysis. Does anyone know what the difference is between the 'documentation' and 'Verso page' links? Are both sources produced with Verso? Or perhaps the documentation was extracted from the code and comments, and the 'verso pages' refer to the ones produced in Verso. I guess the README itself is maintained manually, right?

[Henrik Böving]

The documentation links are built with https://github.com/leanprover/doc-gen4/

[Terence Tao]

In the analysis repo, the documentation is generated by doc-gen from the source lean as part of the blueprint package, but the Verso pages are generated (from the same source lean files) by a separate tool (with its own lake files, etc.). So a certain amount of manual updating of multiple config files are needed (as well as the main README) for both outputs whenever I add a new section. In principle this could be done in a more integrated fashion, but I anticipate the sectioning will in fact stabilize in a few weeks, so it would become moot for that project at least.

[David Thrane Christiansen]

@Alexandre Rademaker Thanks for the feedback! I finished implementing full-text search for the language reference yesterday (before it searched just the tagged metadata, like technical terms, section headers, and function or option names - like the index of a book). That will be rolling out in the next RC/release cycle.

After a couple of weeks vacation, I'll be upstreaming it so every Verso-based online book can have both quick access to specifically-tagged items and a proper text based search.

[Asei Inoue]

@David Thrane Christiansen

I don't think Verso has a feature to convert books into PDFs, but I would like it to have one.
That's because when using an AI like Notebook LM to learn from what I've written, it's easier to train it with content in PDF format.

[Niels Voss]

My understanding from #new members > Printable form of language reference? is that Verso might eventually have the ability to export to PDF, but it's very low priority. I can definitely see a few advantages of being able to do so, although requesting PDFs because they are easier to train LLMs on is certainly a niche use case (surely it would be better to just use a generic program that converts web pages to pdfs?)

[Pim Otte]

Some background with respect to the Analysis Book project: The reason we have this setup is because Terence explicitly set "gateway to mathlib usage" as a goal. The idea here is that the Verso pages are just a pretty and readable view to example proofs and that students who want to do the exercises can just clone the repository and work in the ./analysis subfolder without being confronted with Verso.

In general, I would also recommend Verso: It's powerful for anything involving Lean code and currently in a very useable state (with the rough edges discussed above).

[David Thrane Christiansen]

A PDF feature would be great, and the foundations of it are available. So far, it's not been high enough up the priority list to spend the (significant) time that a quality PDF output would require, however - for example, a system based on print has to format cross-references differently, and the text should read naturally whether it's a clickable link to a given section or a "on page 378"-style cross-reference. All these little details add up. I'd personally also really like an epub version. This is something where a dedicated external contributor could make a big impact.

[Alexandre Rademaker]

Hi @David Thrane Christiansen, would you consider giving a presentation about the Verso architecture? In one of the office hours? A step-by-step guide on how to start a book/website using Verso.

I finally managed to create a first version of the book I started writing. Still, I didn't really understand why I need to define the code blocks (see the definition of savedLean). I would like to avoid having two lake projects and duplicate the dependencies; maybe you can advise on a better structure in my case.

Finally, in VS Code, within a code block, the InfoView is not functioning as expected; it fails to update the proof state.

[David Thrane Christiansen]

In the near future, I'll be substantially improving the documentation for getting started with Verso. I'd be happy to give a presentation once that's been done - right now, I think it would be a duplication of effort, and I think a presentation is more useful as a way to start Q&A based on decent docs, rather than as a way to get started with it. How does that sound?

[Alexandre Rademaker]

Of course — who am I to impose anything different? But deadlines are critical to me... I'm just starting this project of turning the repository https://github.com/arademaker/fad into a book, and I must admit I haven’t made much progress yet because I am confused by the structure of Verso and its examples. I’m already convinced that not using Verso at this point would be a mistake, but I had hoped it would be simpler to use. Understanding how block declarations and other basics work seems essential to avoid a lot of rework later when adapting the material.

[David Thrane Christiansen]

What are your deadlines?

[Alexandre Rademaker]

Sorry, I forgot to answer. The second semester started this week. I would like to have an initial version of the book online as soon as possible so the students can follow its progress as the course evolves.

[David Thrane Christiansen]

I'm working on better, more explanatory examples this week. I'll post here when they're up.