Using doc-gen4 to generate documentation

Stream: general

[Ian Jauslin]

Hello! I am trying to generate the documentation for a lean 4 project using doc-gen4. I managed to generate the documentation by 'requiring' the doc-gen4 package and running lake build ProjectName:docs, but it seems that none of the 'static' files (i.e. style files, .js files etc) are copied to the 'build/doc' directory. Why is that?

Also, when I copy those files over manually, and I run a server using python -m http.server, I then try to use the 'find' script by opening 'http://localhost:8000/find/#doc/...', but I just get a 'Directory listing' for the 'find' directory. How can I use the 'find' feature in the generated doc?

[Henrik Böving]

Re a) That has been working every 8 hours for months, if this is broken you'll have to provide much more detail about your setup

b) check the format of the links that appear on: docs#Nat

[Ian Jauslin]

Thank you for your reply! After much struggle, I figured it out: one needs to run lake exe doc-gen4 index to generate the supporting css, js, html and bmp files.

[Henrik Böving]

Ian Jauslin said:

Thank you for your reply! After much struggle, I figured it out: one needs to run lake exe doc-gen4 index to generate the supporting css, js, html and bmp files.

that hasn't been the case for months by now, what version are you using? What is your setup?

[Ian Jauslin]

I'm using the latest commit of doc-gen4 (96147ea), and a copy of mathlib from November 8.

[Ian Jauslin]

and lean v4.3.0-rc1

[Ian Jauslin]

The relevant lines from lakefile.lean are
require mathlib from git "https://github.com/leanprover-community/mathlib4.git"@"11572f182a36a4441f9a62246985ed9d2e1f3e32"
require «doc-gen4» from git "https://github.com/leanprover/doc-gen4"@"main"

[Ian Jauslin]

I generated the doc with
lake build RMT4:docs
(RMT4 is the name of the project)

[Henrik Böving]

Ian Jauslin said:

I'm using the latest commit of doc-gen4 (96147ea), and a copy of mathlib from November 8.

Cant reproduce this locally and doc-gen is capable of doing this automatically both on its CI and the mathlib docs CI. Do you have a link to your repo?

[Ian Jauslin]

Thank you for taking an interest in this!
I just double checked, and here are steps to reproduce.
The git repo is https://github.com/ianjauslin-rutgers/RMT4/tree/rutgers_leangroup
Here's what I just did to reproduce the issue:
git clone https://github.com/ianjauslin-rutgers/RMT4.git
cd RMT4
git fetch origin rutgers_leangroup
git checkout rutgers_leangroup
lake update
lake exe cache get
lake build
lake build RMT4:docs

This takes a little while to execute, and, after it's done, I have a build/doc folder, but no index.html or style.css etc...
In fact, this is the output of running find ./ -name '*.css' in the project folder:
./lake-packages/doc-gen4/static/alectryon/alectryon.css
./lake-packages/doc-gen4/static/alectryon/docutils_basic.css
./lake-packages/doc-gen4/static/alectryon/pygments.css
./lake-packages/doc-gen4/static/style.css
so all the css files are still in the doc-gen4 package.

[Henrik Böving]

@Ian Jauslin your branch is currently not compiling:

[3907/3909] Building RMT4.Covering
error: > LEAN_PATH=./lake-packages/std/build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./lake-packages/Cli/build/lib:./lake-packages/proofwidgets/build/lib:./lake-packages/mathlib/build/lib:./lake-packages/CMark/build/lib:./lake-packages/UnicodeBasic/build/lib:./lake-packages/leanInk/build/lib:./lake-packages/doc-gen4/build/lib:./build/lib LD_LIBRARY_PATH=./build/lib /home/nix/.elan/toolchains/leanprover--lean4---v4.3.0-rc1/bin/lean ./././RMT4/Covering.lean -R ././. -o ./build/lib/RMT4/Covering.olean -i ./build/lib/RMT4/Covering.ilean -c ./build/ir/RMT4/Covering.c
error: stdout:
./././RMT4/Covering.lean:230:21: error: unknown identifier 'lift''
./././RMT4/Covering.lean:230:2: error: expected a term of the shape `∀xs, ∃a, p xs a` or `∀xs, p xs ∧ q xs`
error: external command `/home/nix/.elan/toolchains/leanprover--lean4---v4.3.0-rc1/bin/lean` exited with code 1

In addition to that I would recommend against all of Mathlib to be imported because doc-gen will generate docs for all of your import closure, meaning that you'll get drastically faster generation times if you just import what you need

If i comment out the import of RMT4.Covering and run doc generation everything works so I suspect the error you are actually hitting here is as follows: You run lake build and overlook the error output. You then run lake build RMT4:docs which generates a lot of documentation and somewhere along the line also notices the error. Which then causes lake to abort the rest of the jobs as soon as possible. After this is done you are left in an incomplete state that you are observing right now

[Ian Jauslin]

I see. The reason I need the doc is to write a blueprint for our project, which is actually based on RMT4 (RMT4 is written and maintained by V beffara, not me). As such, we are going to need to generate the docs in situations where the project is incomplete, and the lean code still has errors. After all, that's what the blueprint is for: to organize the development of this project. So, if I understand correctly, we will need to run lake exe doc-gen4 index manually whenever the project has an error in it. Right?

It might be worth adding this to the README on https://github.com/leanprover/doc-gen4, as I think my use case is not necessarily terribly niche. And it would have saved me a good 4 hours.

[Ian Jauslin]

Also, FYI, I wrote some documentation in the Arch Linux wiki about this https://wiki.archlinux.org/title/Lean_Theorem_Prover#Automatically_generating_documentation . You might want to have a look, and correct things if need be.

[Patrick Massot]

Ian, there is a huge difference between "the project is incomplete" and "the lean code still has errors". The first case is obviously fine, but the second one is not. You should never commit code with errors in your project. Sorries are fine, errors are not.

[Ian Jauslin]

Well, that's all well and good in principle, but when a project involves a number of people, some of which are newcomers to lean (or to git for that matter), and others are writing code without necessarily thinking about how it will be used by others, one inevitably will end up with errors in the committed lean code. When that is the case, I would still like to be able to generate the blueprint for the code that does work, without having to sift through the errors committed by others. So for someone in my situation, it is very good to know that the doc can be indexed even when there are errors in the lean code.

[Ian Jauslin]

Not to mention that with the continuous progress of mathlib, things are always breaking, so I don't think it's unreasonable to publicize a feature that makes the doc usable even when there are issues with the code or the environment.

[Henrik Böving]

Ian Jauslin said:

I see. The reason I need the doc is to write a blueprint for our project, which is actually based on RMT4 (RMT4 is written and maintained by V beffara, not me). As such, we are going to need to generate the docs in situations where the project is incomplete, and the lean code still has errors. After all, that's what the blueprint is for: to organize the development of this project. So, if I understand correctly, we will need to run lake exe doc-gen4 index manually whenever the project has an error in it. Right?

It might be worth adding this to the README on https://github.com/leanprover/doc-gen4, as I think my use case is not necessarily terribly niche. And it would have saved me a good 4 hours.

As patrick says, you can happily put a sorry there, the point is that your project doesn't compile, it's like you are asking doc-gen to generate documentation for a file that is not Lean, it's not going to work. If you fix your errors (and sorry them out if you wish, that's none of my business, you only have to get Lean to accept your code) everything is going to work.

If you are familiar with other languages like say Python, this is as if you are asking a python tool to generate documentation for a file that is syntactically not valid, yes of course the process won't work.

Ian Jauslin said:

Also, FYI, I wrote some documentation in the Arch Linux wiki about this https://wiki.archlinux.org/title/Lean_Theorem_Prover#Automatically_generating_documentation . You might want to have a look, and correct things if need be.

As such please change this wrong documentation to fit the one from the README. In addition to that: There is no reason to use the way of search via the /find URL, you can just use the search bar that the documentation has on every page in the top right corner. The /find feature is merely meant for automatic linking from the Zulip in the form of docs#Nat.add, not for a human interactive user.

In general, if you are observing weird behavior from a tool and are being told that your behavior is not what everyone (and given that most usages are automated, everything) else who is using it is observing, you should probably not be writing general documentation that demonstrates the workaround for your misuse of the tool.

Ian Jauslin said:

Well, that's all well and good in principle, but when a project involves a number of people, some of which are newcomers to lean (or to git for that matter), and others are writing code without necessarily thinking about how it will be used by others, one inevitably will end up with errors in the committed lean code. When that is the case, I would still like to be able to generate the blueprint for the code that does work, without having to sift through the errors committed by others. So for someone in my situation, it is very good to know that the doc can be indexed even when there are errors in the lean code.

Your documentation is not getting fully indexed with your command, doc-gen is not generating documentation for your entire project. Every file that has an error will be completely left out, including all of the files that import the erroring ones (transitvely all the way through). And there is literally no way for doc-gen to change this, the Lean compiler is saying "This code is so wrong I cannot fix it myself, help me human".

In addition to this is is (as Patrick also said) never a good idea to have code that is completely broken on a branch, you will want to have a CI setup that tells you if your code at least compiles (again, compiles can mean that there is a million sorries in there) and only then you should generate a blueprint for it.

Ian Jauslin said:

Not to mention that with the continuous progress of mathlib, things are always breaking, so I don't think it's unreasonable to publicize a feature that makes the doc usable even when there are issues with the code or the environment.

No it is not at all, it's quite simple in fact: The normal state is that people pin mathlib to specific commits, just like you are doing right now. Once you decide to upgrade mathlib you do that once on a different branch, fix all the errors on that branch (and during this period you simply wont be able to generate a blueprint for that branch and that is okay, everything else still works), then merge it in and now everyone can use the new mathlib without errors.

[Henrik Böving]

To illustrate the error vs sorry point further.

Doing this:

def FermatsLastTheorem : Prop := sorry

theorem flt : FermatsLastTheorem := by sorry

is completely fine. So even leaving out the definition of theorem statements, types, functions, proofs, whatever you want and instead using sorry is completely acceptable for the Lean compiler. What is not fine would be just writing

theorem flt : MyModule.DefinitionThatIDidntDo := by sorry

and expecting this to be processed by Lean and doc-gen

[Patrick Massot]

Ian Jauslin said:

Well, that's all well and good in principle, but when a project involves a number of people, some of which are newcomers to lean (or to git for that matter), and others are writing code without necessarily thinking about how it will be used by others, one inevitably will end up with errors in the committed lean code.

Then you have something a lot more urgent to do than building your doc. You need to teach those people to never ever commit code with errors. This will save them a huge amount of time. Ignoring errors is the biggest source of confusion when using Lean. Indeed beginners do that. They ignore an error and happily continue to edit code, sometimes in the very same proof. And they get super confused because Lean is in a completely incoherent state and nothing makes sense. As a teacher or collaborator, you need to help them getting rid of that habit as soon as possible.

[Kevin Buzzard]

https://xenaproject.wordpress.com/2020/03/24/no-errors/ (completely out of date explanation about what to do about the problem, but the sentiment is the main point)

[Ian Jauslin]

I understand the point of sorry's versus errors. Again, I'm not the one who wrote or committed the code that has lean errors in it. I forked a repository that is setting up tools for complex analysis, whose author I barely know (i met them once over zoom), and certainly have no business remonstrating for committing code that has an error in it. I am in a situation where I need to make do with what I have.

So, I come to this problem, without ever having used doc-gen4 or blueprint, and I have to figure out how to use them. I follow the instructions in the doc-gen4 README. The doc comes out unusable. The first thing I do, is to try to generate the doc for a brand new blank project. That works even less: it doesn't generate any doc for my test project. I later understand that this is because the new version of lean has moved lake-packages to .lake, and the current version of doc-gen4 does not use .lake. But at the time, I still had no idea how doc-gen4 was supposed to work, so I don't know why things are going bad. So, I go back to my project, and try to figure out what is wrong. I use the dev-tools to find out that all of the .js and .css files are missing. So I grep through the source code for doc-gen4 to try to understand when they were supposed to be installed. That's a hell of a job to do: the code is complex and written in lean, which is not my programming language of choice. After about 4 hours of this, I eventually find out that running lake exe doc-gen4 index adds these files. Keep in mind, that before arriving to that state, I have no idea why things went wrong, because I have no idea how things are supposed to work, and what state I'm supposed to find the documentation in. Only after I generate the index, and see the documentation, can I find out that the documentation for the error-laden files is not there. The command lake exe doc-gen4 index is very useful, it allows me to see enough that I can understand what is happening. This is why manual overrides are good: they allow one to understand what is happening when not everything went according to plan.

This all goes to show that the documentation for doc-gen4 was insufficient for me. To someone who is unfamiliar with the tools, the README file just does not say enough. In particular, it does not say that the documentation is unusable if there are errors in the lean code. Also, it does not talk about this feature: lake exe doc-gen4 index (this feature is not a work-around, it's a feature: it allows one to index the documentation manually, which is a useful thing to do when things go wrong).

I do not understand why anyone would oppose the notion that features should be documented.

[Ian Jauslin]

Henrik Böving said:

As such please change this wrong documentation to fit the one from the README. In addition to that: There is no reason to use the way of search via the /find URL, you can just use the search bar that the documentation has on every page in the top right corner. The /find feature is merely meant for automatic linking from the Zulip in the form of docs#Nat.add, not for a human interactive user.

Could you be more specific? Do you mean the 'env=dev' part? I don't see anything in the README about the 'find' feature.

Similarly to my comment above, why should the 'find' feature not be documented? It is used in blueprints, and in fact, I would never have been able to get our blueprint to work, if I hadn't understood how the find feature can be accessed via a url. So I'm not sure what your objection is here.

[Henrik Böving]

Ian Jauslin said:

Also, it does not talk about this feature: lake exe doc-gen4 index (this feature is not a work-around, it's a feature: it allows one to index the documentation manually, which is a useful thing to do when things go wrong).

I do not understand why anyone would oppose the notion that features should be documented.

This is not a feature, it is a detail of how the :docs facet is implemented and not a publicly exposed API and thus has zero guarantees that it will continue working. You are not ever supposed to interact with doc-gen through the lake exe doc-gen interface.

This all goes to show that the documentation for doc-gen4 was insufficient for me. To someone who is unfamiliar with the tools, the README file just does not say enough. In particular, it does not say that the documentation is unusable if there are errors in the lean code.

The basic assumption that doc-gen makes is that your code is able to compile. It does error out while generating your documentation and boldly tells you so. If I run the command with your broken branch I get the output that I said before:

[3907/3909] Building RMT4.Covering
error: > LEAN_PATH=./lake-packages/std/build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./lake-packages/Cli/build/lib:./lake-packages/proofwidgets/build/lib:./lake-packages/mathlib/build/lib:./lake-packages/CMark/build/lib:./lake-packages/UnicodeBasic/build/lib:./lake-packages/leanInk/build/lib:./lake-packages/doc-gen4/build/lib:./build/lib LD_LIBRARY_PATH=./build/lib /home/nix/.elan/toolchains/leanprover--lean4---v4.3.0-rc1/bin/lean ./././RMT4/Covering.lean -R ././. -o ./build/lib/RMT4/Covering.olean -i ./build/lib/RMT4/Covering.ilean -c ./build/ir/RMT4/Covering.c
error: stdout:
./././RMT4/Covering.lean:230:21: error: unknown identifier 'lift''
./././RMT4/Covering.lean:230:2: error: expected a term of the shape `∀xs, ∃a, p xs a` or `∀xs, p xs ∧ q xs`
error: external command `/home/nix/.elan/toolchains/leanprover--lean4---v4.3.0-rc1/bin/lean` exited with code 1

I don't see why you would expect build artifacts of a command that is clearly failing to be usable? Do you want doc-gen to delete all of the documentation that it has generated so far and start from scratch if it fails?

Could you be more specific? Do you mean the 'env=dev' part? I don't see anything in the README about the 'find' feature.

I'm referring to the index "feature" which as explained above is not a feature and has zero guarantees to work in the future. The only suppported stable API for doc-gen is the :docs facet.

Similarly to my comment above, why should the 'find' feature not be documented? It is used in blueprints, and in fact, I would never have been able to get our blueprint to work, if I hadn't understood how the find feature can be accessed via a url. So I'm not sure what your objection is here.

I do agree that we should document the /find feature, but this is not the way that 99.9% of the people will interact with the doc-gen search, instead they will just go to the page, click the search bar in the top right and enter their query.

[Ian Jauslin]

Henrik Böving said:

The basic assumption that doc-gen makes is that your code is able to compile. It does error out while generating your documentation and boldly tells you so.

If that basic assumption were spelled out in the documentation for the doc-gen4 project, that would have saved me an afternoon of fumbling around trying to get this to work. But that was only my experience. If you don't want to add details to your documentation to help people who think like me, then that's fine. I just wanted to share how inefficient my interaction with this was, in the hope that it might lead to future improvements. I'll remove the command in the arch linux wiki if you indeed have no intention of maintaining it in future releases.

I also did not catch the error when running lake build RMT4:docs, as it was buried up a number of lines. I saw the error when running lake build but I had no reason to think this would cause a problem with documenting the other files.

[Ian Jauslin]

Henrik Böving said:

I don't see why you would expect build artifacts of a command that is clearly failing to be usable? Do you want doc-gen to delete all of the documentation that it has generated so far and start from scratch if it fails?

I am not asking for anything. The only thing I did earlier is to point out that it might be helpful to expand the documentation of doc-gen4 so that newcomers can have an easier time learning to use it.

[Kevin Buzzard]

Lean is a huge ongoing project which until very recently was basically entirely run by volunteers. I'm sure that PRs improving the documentation of doc-gen4 or indeed any other aspect of Lean would be very welcome :-)

[Ian Jauslin]

Kevin Buzzard said:

Lean is a huge ongoing project which until very recently was basically entirely run by volunteers. I'm sure that PRs improving the documentation of doc-gen4 or indeed any other aspect of Lean would be very welcome :-)

I would love to do a PR for the README of doc-gen4, I'm just not sure how this would be received. I have no desire to step on anyone's toes.

[Henrik Böving]

https://github.com/leanprover/doc-gen4/tree/doc-failing-projects#assumptions-that-doc-gen4-makes @Ian Jauslin is this sufficient or would you like any additional explanation or details?

[Kevin Buzzard]

Ian I suspect that people would be happy to work together to find a solution to your frustrations.

[Ian Jauslin]

Henrik Böving said:

https://github.com/leanprover/doc-gen4/tree/doc-failing-projects#assumptions-that-doc-gen4-makes Ian Jauslin is this sufficient or would you like any additional explanation or details?

That's perfect!

[Ian Jauslin]

And thank you for your time and effort!

[Henrik Böving]

Okay it's merged, I also fixed the build changing to .lake stuff, that was an unannoucned breaking change by lake that wasn't on my radar.

[Ian Jauslin]

The doc looks great, thank you!

[Ian Jauslin]

I also just checked the compatibility with the new mathlib and lean version, and it seems to work well!

[Ian Jauslin]

One thing I noticed though, is that the documentation generation failed when it is run in a directory that is not a git repo. Looking through the source, it looks like the git repo is needed to link to the source.

After some basic tests, it seems that linking to the source works for github repos, but not necessarily for other git systems. (I tried this with a local git repo, and I also checked that '.../blob/...' doesn't seem to work on my gitea repos, e.g. https://jauslin.org/git/software/Nstrophy/blob/6c12e47105b218e3bfecae4f8541833e913cdfe9 returns a 404 error.) Is it correct that doc-gen4 may not work on non-github repos?

[Henrik Böving]

Yes both of those are intended behavior at the moment. The "is not a git repo" should not matter for quite a long while as lake always uses git repos. The github one I am planning on eventually changing although I haven't found a solution that makes me happy yet, just implementing individual linking support for every platform seems a little silly.

[Utensil Song]

@Ian Jauslin I've just noticed this topic and the doc you have written for a minimal blueprint setup here.

Installing this is not as easy as plasTeX. Here's a simple procedure

That series of commands can actually be a one-liner: pip install git+https://github.com/utensil/leanblueprint.git@lean4-only-dev

Or better, follow one of these projects using Lean 4 blueprint to use requirements.txt for both plastex and leanblueprint then install with pip install -r requirements.txt.

If you have any issue about the Lean 4 blueprint, you can ping me. I haven't made improvements to its documentation yet as I realized that it's more of a "documenting it by making example projects work" process as there are many moving parts when using it.

[Ian Jauslin]

Henrik Böving said:

Yes both of those are intended behavior at the moment. The "is not a git repo" should not matter for quite a long while as lake always uses git repos. The github one I am planning on eventually changing although I haven't found a solution that makes me happy yet, just implementing individual linking support for every platform seems a little silly.

Yeah it seems that having separate code for each git server would not be a great solution. Perhaps a configuration file/optional argument in which one can specify the url format? I don't know how easy such a thing would be in lean...

[Ian Jauslin]

Utensil Song said:

That series of commands can actually be a one-liner: pip install git+https://github.com/utensil/leanblueprint.git@lean4-only-dev

Or better, follow one of these projects using Lean 4 blueprint to use requirements.txt for both plastex and leanblueprint then install with pip install -r requirements.txt.

Thanks for the info! This is indeed helpful! (I myself don't use pip, I use my distro's package manager, and I created a package for leanblueprint, which I'm planning on uploading to the Arch User Repository; I'll keep you posted. I wrote that file for the users in my project that are on windows or macs, and they will be much happier with a one-line pip command than what I wrote!)

Utensil Song said:

If you have any issue about the Lean 4 blueprint, you can ping me. I haven't made improvements to its documentation yet as I realized that it's more of a "documenting it by making example projects work" process as there are many moving parts when using it.

It may be worth considering having a list of links to example projects in the README on your github. It would take a minute to write, and be very helpful.

[Ian Jauslin]

@Utensil Song There is currently no license on your project, so I should ask: may I package leanblueprint and post it on the Arch User Repository?

[Alex J. Best]

You should ask Patrick Massot as Utensil's repo is a fork with some modifications but still primarily the code Patrick wrote if I understand correctly.

[Ruben Van de Velde]

Sounds like it would be a good idea to add a license, then :)

[Patrick Massot]

I merged the Lean4 support PR. Is there any other modification in Utenseil's repo that is not in mine?

[Patrick Massot]

I'm very skeptical about packaging it for Arch Linux. This seems to be a great recipe for having confused users using outdated versions. We've seen so many people struggling here because of people who tried to package Lean itself...

[Frédéric Dupuis]

Back when I first started using Lean, I tried to make an Arch package out of it and I can confirm that it's a very bad idea.

[Ian Jauslin]

Lean is very different from blueprint though. Lean is under extremely active development, to the extent that from one month to the next, a lean project will often stop working with the latest version of lean. Lean could absolutely be packaged if it had a very active maintainer (which is essentially what elan is). And, when it stabilizes, it will be packaged by most major distributions, and we won't have to go through the headache of installing yet another package manager (elan) to get lean, and our binaries will be check-summed and installed by root, thus following the safety procedures that two generations of Linux users have converged on for some time.

Is blueprint under that heavy of a development that it cannot be packaged? In other words, if I use the current master branch in a month, will my workflows be broken?

For comparison, plastex is packaged, and the Arch User Repository package works great!

[Ian Jauslin]

PS: Lean 3 was packaged at Arch, and that worked perfectly fine. So when lean 4 reaches a level of stability that is comparable to how lean 3 was before the switch, we'll be in business!

[Yaël Dillies]

LeanBlueprint is currently not under active development, but that will change soon-ish, when David Thrane Christiansen's documentation tooling comes out and Sky Wilshaw and I rewrite the whole thing.

[Utensil Song]

Patrick Massot said:

I merged the Lean4 support PR. Is there any other modification in Utenseil's repo that is not in mine?

Thanks. Currently, the projects using Lean 4 blueprint are using my PR branch (I used another branch with an extra -dev for developing/staging), so everything is in after the merge.

Now the one-liner is simplified to

pip install git+https://github.com/PatrickMassot/leanblueprint

and no more worries that it's a fork or using an unstable branch.

Ian Jauslin said:

Is blueprint under that heavy of a development that it cannot be packaged? In other words, if I use the current master branch in a month, will my workflows be broken?

Personally I'm not actively working on adding new features to blueprint, the whole idea was to revive all the great stuff @Patrick Massot made for Lean 3 available to Lean 4 projects, @Henrik Böving 's work on doc-gen4 made it possible and my work minimal. But I'll be actively fixing issues, or adding nice little things that help projects using blueprint on request via PRs if needed. So, to answer your rephrased question, it's highly unlikely to break your workflow if you use the master branch of https://github.com/PatrickMassot/leanblueprint .

About packaging, the Lean 4 version is not even released as leanblueprint on pip yet (it could be done now, but I'll rather keep observing if the last few commits in the PR branch are working OK for the projects for a while), so packaging for AUR might be something after that.

Also, in the current Lean 4 world, packaging seems to have more ramifications. Lean 4 version of blueprint is highly dependent on doc-gen4, lake etc. and these are rapidly involving, and things might actually break or behave drastically differently between versions (most likely in a positive way, but things might still break if one dependency is not up-to-date with other up-to-date stuff you're using). The relevant fixes would be available on the master branch in time, much earlier than the packaged version.

[Patrick Massot]

Yaël Dillies said:

LeanBlueprint is currently not under active development, but that will change soon-ish, when David Thrane Christiansen's documentation tooling comes out and Sky Wilshaw and I rewrite the whole thing.

This sentence sounds very weird to me. The Lean blueprint plugin is something that took me a lot of time to implement as a first approximation of my vision for an infrastructure allowing collaboration on large formalization projects. This vision came from my experience in the perfectoid spaces project where we had no such tool. I developed it as a preliminary for my sphere eversion project. Since then, many projects showed that my vision for this had some relevance and that the current implementation is already very usable. So I am a bit surprised to see a message that seem to imply that I did such a bad job that there is a clear need to restart from scratch without asking me whether I would be interested in contributing. Of course I agree this tool could be much better, and it was always presented as an experimentation. But I don't see the need to announce: "don't worry, we'll get rid of Patrick and do it properly".

[Mario Carneiro]

A rewrite doesn't necessarily imply that the original code isn't useful for doing the spec work and setting expectations. For example doc-gen4 is a complete rewrite of doc-gen3, but having an already implemented and working doc-gen saved all the trouble choosing colors and designing the sidebar, so it could be focused on just swapping out the backend while preserving existing functionality.

So this kind of claim is a little bit closer to saying that the code is not architectured well, which is also kind of bad but maybe doesn't reflect on the whole design. In the context of the post I think what it is actually trying to say is that it should be rewritten using the new docs architecture when it comes out, and the extent to which this is warranted remains to be seen (since the new architecture is not out nor sufficiently well defined as to evaluate the claim).

[Yaël Dillies]

Yes certainly! I can't write much text because I need to work. But our plan for a rewrite in Lean 4 is so that we get to use Lean 4's capabilities for a tool that's already great.

[Utensil Song]

One thing to note is that handling mathematical content is a non-trivial task, e.g. doc-gen4 still has Math render glitches compared to its Lean 3 version, and authoring a blueprint might be more demanding on macros, packages and other features available in LaTeX, e.g. commutative diagrams or tikz . Transition from a LaTeX based solution to a Lean DSL based solution might be much more difficult than porting Markdown between Markdown flavors, and I can't immediately see how it can be done smoothly and lossless, and probably blueprint would wait longer than other documentations for the features in DSL to make it possible.

The current design of blueprint, besides reusing the LaTeX ecosystem that's familiar to mathematicians, and very efficient on converting existing literatures with most concentration on the mathematical content instead of technical details, it's also very decoupled from the Lean code, which facilitates division of labor and large scale collaboration. These are still the gems of the vision of the blueprint (along with the dep graph), and less likely the immediate emphasis of the new documentation tooling, which shines most when it interacts with Lean code, i.e. you can freely navigate between code and doc as a coherent whole, both in code editor and (I hope) web browser.

[Scott Morrison]

I think it's particularly nice that the blueprint tooling can be steered by someone with "conventional" mathematician technical skills (i.e. no Lean!). This makes collaborations between Leaners and non-Leaners more productive.