blueprint changes

Stream: general

[Patrick Massot]

An important announcement for people who currently use my plasTeX blueprint plugin and install it directly from the git master branch (probably at least @Terence Tao, @Yaël Dillies, @Riccardo Brasca, @Chris Birkbeck). I just pushed a series of changes that require a little adjustment. The disturbance comes from the very long overdue split of the plugin into three pieces. A new tiny piece which adds the eye buttons and have nothing to do with graphs or Lean. A new dependency graph plugin which allows to build dependency graphs using \uses and \proves but has nothing to do with Lean. And the blueprint plugin which is now built on top of the graph plugin. Hopefully you should have nothing to change in your TeX code. However you need to install three python packages instead of one. I opened the corresponding PR to the PFR project as a migration example. Of course you shouldn't hesitate to tell me whether something broke even after installing the three new packages.

[Kevin Buzzard]

Thanks! You can add me to the list, with a not-yet-public FLT blueprint.

[Patrick Massot]

This change was a substantial piece of work that I wanted to do before more modifications, although it is barely visible for users. There are also a couple of user-visible changes.

• The dependency graph is now automatically reduced by default, so you can use \uses everywhere without cluttering the graph with redundant edges. You can turn-off this reduction using the nonreducedgraph option when loading the blueprint package in your TeX code.
• You can mark a theorem statement or definition using the \notready LaTeX command to flag it as not ready for formalization (presumably because its blueprint is not yet fleshed-out). It will appear with an orange border in the graph.
• Nodes which are fully formalized including all their dependencies are now darker (you can see it in the PFR graph already).
• Speaking of colors, you can now changes the colors appearing in the graph from the TeX code. But I haven't written the documentation yet.
• You can use \discussion{NNN} inside a theorem statement or a definition, where NNN is a GitHub issue number. This will create a link to GitHub visible from the theorem header in the main text and at the bottom of statements in the graph.

[Patrick Massot]

Still on my TODO list for the near future:

• replace the invoke script tradition by a leanblueprint command line client doing the same thing, and can also be used to create with a file layout and GitHub scripts.
• Write documentation.
  My longer term TODO also has graph filtering but I cannot say when this will happen because Lean Together 2024 will clearly come first and then the second term will start.

[Kevin Buzzard]

\discussion is a great addition!

[Alex Kontorovich]

This is great! Also: @Ian Jauslin and I have been playing around with a tool which allows the following: rather than separately writing a TeX blueprint file, and bouncing back and forth between that and Lean, you write the TeX directly inside the comments of the Lean file, and then scrape that TeX into corresponding blueprint files. Please see: https://github.com/ianjauslin-rutgers/leanblueprint-extract Any comments/suggestions are welcome!

[Alex Kontorovich]

Also, @Paul Nelson has an even cooler setup, where inside Emacs, his TeX shows already rendered inline. So he "sees" the blueprint as he types the Lean. The closest thing I could find that works with VS Code is "conceal": https://marketplace.visualstudio.com/items?itemName=BRBoer.vsc-conceal but it's not as good...

[Chris Birkbeck]

This all looks really great, thank you for all the work!

[Patrick Massot]

This idea has been discussed in the past, and already implemented in format_lean (Lean 3 only) but the consensus is that we want the TeX code to be autonomous so that people with no Lean knowledge can write and maintain Lean blueprints.

[Alex Kontorovich]

Sure, it's not a good idea in every project. But another benefit to those who may want to use it is the following: with copilot running in the background, it often takes the natural language (TeX) immediately above the cursor and literally spits out exactly the corresponding Lean statement... (It doesn't do quite as well nearly as often if not prompted in this way...)

[Paul Nelson]

Alex Kontorovich said:

Also, Paul Nelson has an even cooler setup, where inside Emacs, his TeX shows already rendered inline. So he "sees" the blueprint as he types the Lean. The closest thing I could find that works with VS Code is "conceal": https://marketplace.visualstudio.com/items?itemName=BRBoer.vsc-conceal but it's not as good...

in case anyone's curious, this is what Alex mentioned (although to be honest, I usually fold away the tex to focus on the code)
preview-lean4.png