VersoManual: get code and docstring from external Lean

Stream: lean4

[Gaëtan Serré]

I'm very new to verso and I would like to use the manual genre of Verso (which I find beautiful) to create a documentation for some proofs. However, I don't want to rewrite the proofs and I want the docstring I already written to show on the website. I saw in the Verso examples that something very similiar have been done for the demo website using def_literate_page or def_literate_post. I'm wondering if there is a way to do the same with the manual genre. The final result I would like would be a front page like the example of the Zippers package with an introductory text and links to pages that represent an external Lean file.
I apologize if this is not clear or if my vocabulary is not correct.

[David Thrane Christiansen]

Thanks!

Your question is very clear, I'm pretty sure I understand exactly what you're going for :)

This particular use case is not very well-supported at the moment, but I plan to put significant effort into it in the next few months. Do you have a deadline?

[Gaëtan Serré]

Thanks for your reply!

For now, I've just created a CSS that sort of mimics VersoManual's style for the Blog genre. I don't have a deadline, I'm just doing this to get to know the tool. Thanks for all the work you've done, I'm enjoying using Verso more and more!

[Alexandre Rademaker]

Hi @Gaëtan Serré, what is this Zippers package? Can you provide a link to it?

[Gaëtan Serré]

Alexandre Rademaker said:

Hi Gaëtan Serré, what is this Zippers package? Can you provide a link to it?

Hi @Alexandre Rademaker , it's an example package from the Verso repository.

I'm not sure it is online. If you want to see it, you should built it from source using the Verso documentation.

[Alexandre Rademaker]

Thanks. I saw Zippers at documented-package actually, but maybe the two examples are related. Not clear to me.

[David Thrane Christiansen]

It's not a real package - there's just enough code there to be usable as a template, illustrating one way to use Verso.

[Alexandre Rademaker]

I see, but I really didn't understand these examples in https://github.com/leanprover/verso/tree/main/examples.

In the textbook, there is this file that seems to contain some code necessary to define the code blocks.

In the package manual, similar functions are defined in this file.

Therefore, I guess I also need to declare some preliminary elements before starting to write the text and code.