utensil
commented
7 months ago There are 2 features that inv create could include:
- Implement links to Lean doc in PDF as well, because it can generate lean blueprint macros for the LaTeX, unlike the empty ones now.
- 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.
PatrickMassot
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
invtasksBlueprint 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.bblfile for the web version to have proper bibliographyinv web: builds the LaTeX to a websiteinv 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 runinv all: it depends oninv bpandinv web, some projects include copying of some of the products of previous tasksinv 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 restartinv devwhich could be improvedSome 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 ainvtask yetinv checkorinv lint: it checks the correspondence between the blueprint and the Lean code, in a loosely coupled way, it can check\leanoknodes against doc-gen4 declaration files (naively implemented in teorth/pfr#97 ), and check sorries in Lean code but marked\leanokin 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.