RFC: Absorb scattered functionalities back into leanblueprint

[utensil]

There is a common issue of the blueprint ecosystem, namely every project is using a slightly different setup with a few loosely coupled building blocks, in Python, in Github Actions workflows, in LaTeX etc. This issue is a RFC to absorb some if not all of them into leanblueprint.

Here is a potential list:

Existing inv tasks

Blueprint can provide a default implementation for the common tasks which are almost identical with trivial differences, and users can selectively import or improve them:

• inv bp: builds the LaTeX to a PDF file, it also generates the .bbl file for the web version to have proper bibliography
• inv web: builds the LaTeX to a website
• inv decls: deprecated, it was for Lean 3, replaced by doc-gen4 declarations extraction which is non-trivial task to distill and maintain particularly because the implementation highly depends on the involving lake and the process is quite time-consuming to run
• inv all: it depends on inv bp and inv web, some projects include copying of some of the products of previous tasks
• inv dev: I use this and provided it to some projects, for auto-rebuilding the PDF and the website after each edit, the downside is if some LaTeX goes wrong, the user has to use X to exit LaTeX then restart inv dev which could be improved

Some potential tasks

• inv create: it could set up an optimal Github Actions workflow with caches (there are some variants with longer CI time, due to the complexity of getting all of LaTeX, Python, Lean work in CI efficiently ), default blueprint directory layout with the correct project name, and dummy LaTeX macros, python dependencies, unlike now people copy setup from another project then change the project name, a potential issue of this is colliding with existing LaTeX code or Lean code, which could be mitigated by discovering the existing equivalent files and gives a warning/hint for the user to check manually -- not implemented as a inv task yet
• inv check or inv lint: it checks the correspondence between the blueprint and the Lean code, in a loosely coupled way, it can check \leanok nodes against doc-gen4 declaration files (naively implemented in Check for broken references in blueprint to Lean declarations teorth/pfr#97 ), and check sorries in Lean code but marked \leanok in blueprint.

These are what I can think of for now. If there is a consensus on this, I can break them into smaller issues or PRs but unfortunately no promises on a timeline except hopefully not slower than the emergence of new formalization projects.

P.S. I'm motivated to do the work as keeping multiple projects running OK and fixing usability issues across them (with subtle differences) has become quite some overhead, also people are asking for project setup or instructions, and they develop their own variants of instructions for doing the same thing which has variants of caveats or inconveniences . If these functionalities are indeed absorbed into leanblueprint, it would be much easier to write documents for instructions.

P.P.S. I understand that there are possibly plans to rewrite or incorporate leanblueprint into the new Lean documentation system, but they are not an imminent future for the coming formalization projects, so a little investment into these tiny details of quality of life seems to be still worth the while.

[utensil]

There are 2 features that inv create could include:

1. Implement links to Lean doc in PDF as well, because it can generate lean blueprint macros for the LaTeX, unlike the empty ones now.
2. Add dep graph to the PDF as well, which has a circular dependency issue: web depends on the bib file generated during PDF generation, now PDF would depend on the dot file generated during web generation.

[utensil]

There is also a bootstrap issue for inv create as tasks.py is not even created by then, so possibly leanblueprint create but it's too long a name to type (not so much for just copy-paste though).

[PatrickMassot]

Sorry I forgot about the existence of this issue. Almost all of this was completed a long time ago (and was already planned before this issue was opened). Let’s open separate issues for the little remaining bits if needed.