Zulip Chat Archive

I am getting totally confused about making a documentation for my lean3 project. I have a project and I have properly commented on every theorem (describing them) is there a way to generate a documentation for my project?
It is a small library with some theorems. I want to generate a documentation for it from the comments (or any other way), like you do in python using sphinx in python or doxygen in c/c++. I cant seem to figure it out
(sorry for the silly question)

Patrick Massot (Jul 14 2023 at 18:43):

Do you mean something that looks like https://leanprover-community.github.io/mathlib_docs/linear_algebra/quotient.html? this is done by docgen.

Yaël Dillies (Jul 14 2023 at 18:53):

Have a look at non-mathlib projects to see how they do it, eg github.com/YaelDillies/LeanAPAP. I'm linking you to my project because many things broke in our general setup and I fixed them in my project last week.

Sayantan Majumdar (Jul 14 2023 at 19:17):

yes, I want to make something like that for my project @Patrick Massot

Notification Bot (Jul 14 2023 at 19:17):

Sayantan Majumdar has marked this topic as resolved.

Notification Bot (Jul 14 2023 at 19:18):

Sayantan Majumdar has marked this topic as unresolved.

Patrick Massot (Jul 14 2023 at 19:18):

You should still be warned that investing time in learning Lean 3 tooling is very unwise. That time would be much better invested in porting your project to Lean 4, and then learn Lean 4 tooling.