Updating blueprint?

Stream: sphere eversion

[Michael Rothgang]

Can somebody update the blueprint (or help me do it), please? 5487c1421a7894567e0b211f505f4b6c97edec73 (current HEAD on master) updated a type; it would be nice to update the blueprint accordingly. (Not urgent, of course.)

[Michael Rothgang]

I tried to do this myself, by following the instructions in the README. inv all errors for me, with the following output

$ inv all
Traceback (most recent call last):
  File "/home/michael/VENV_mercurial/bin/inv", line 8, in <module>
    sys.exit(program.run())
             ^^^^^^^^^^^^^
  File "/home/michael/VENV_mercurial/lib/python3.11/site-packages/invoke/program.py", line 387, in run
    self.parse_collection()
  File "/home/michael/VENV_mercurial/lib/python3.11/site-packages/invoke/program.py", line 479, in parse_collection
    self.load_collection()
  File "/home/michael/VENV_mercurial/lib/python3.11/site-packages/invoke/program.py", line 716, in load_collection
    module, parent = loader.load(coll_name)
                     ^^^^^^^^^^^^^^^^^^^^^^
  File "/home/michael/VENV_mercurial/lib/python3.11/site-packages/invoke/loader.py", line 91, in load
    spec.loader.exec_module(module)
  File "<frozen importlib._bootstrap_external>", line 940, in exec_module
  File "<frozen importlib._bootstrap>", line 241, in _call_with_frames_removed
  File "[redacted]/sphere-eversion/tasks.py", line 6, in <module>
    from mathlibtools.lib import LeanProject
ModuleNotFoundError: No module named 'mathlibtools'

[Michael Rothgang]

(I am installing plastex etc. in a virtual environment VENV_mercurial.) What am I missing?

[Ruben Van de Velde]

Are you sure the blueprint works with lean 4?

[Ruben Van de Velde]

This works:

--- tasks.py
+++ tasks.py
@@ -3,8 +3,6 @@ import shutil
 from pathlib import Path
 from invoke import run, task

-from mathlibtools.lib import LeanProject
-
 from blueprint.tasks import web, bp, print, serve

 ROOT = Path(__file__).parent
@@ -17,12 +15,7 @@ def doc(ctx):
         run(f'pandoc -t html --mathjax -f markdown+tex_math_dollars+raw_tex {path.name} --template template.html -o ../docs/{path.with_suffix(".html").name}')
     os.chdir(cwd)

-@task
-def decls(ctx):
-    proj = LeanProject.from_path(ROOT)
-    proj.pickle_decls(ROOT/'decls.pickle')
-
-@task(doc, decls, bp, web)
+@task(doc, bp, web)
 def all(ctx):
     shutil.rmtree(ROOT/'docs'/'blueprint', ignore_errors=True)
     shutil.copytree(ROOT/'blueprint'/'web', ROOT/'docs'/'blueprint')

[Michael Rothgang]

Ruben Van de Velde said:

Are you sure the blueprint works with lean 4?

I have no idea. I assumed it would, but that might have been way too optimistic :big_smile:

[Michael Rothgang]

Your proposed change worked. (I had to install the Asana Math font locally, then it compiled.)

[Michael Rothgang]

The links to Lean declarations are broken; they were not migrated during the port.

[Michael Rothgang]

I pushed the regenerated blueprint to the update-blueprint branch. It's a mixed bag of changes

• generated the "local to global" chapter was never added to version control
• some layout changes are clearly for the better (e.g. triangle for collapsing/expanding output)
• some changes seem for the worse (lots of trailing whitespace now)
• other are a matter of taste (existing output is hard-wrapped at 80 characters; I'd argue that's not necessary). For just viewing the HTML, it probably doesn't matter much.

The last two are more minor (but lots of churn).

[Patrick Massot]

The blueprint has not been ported at all. I completely forgot about it at the end of the port.

[Michael Rothgang]

Makes sense! I had some free time and went over all lean commands in the blueprint, updating lemma names as needed (and also doing the same in doc comments). Two follow-up questions

• are there further commands I should check?
• does the blueprint need further updates?

[Patrick Massot]

Thanks! In this project the blueprint is built locally and the result is pushed to the repo because it was the first project using this blueprint plugin and I hate CI setup. So if it builds for you then you can push it.

[Michael Rothgang]

Just pushed the updated version. While at it, I stumbled across some lemma names which appear to be Lean3-isms to me. Some I renamed directly; I am less sure about

• one_jet_eucl_bundle_mk and friends
• Smooth{At}.one_jet_comp and Smooth.one_jet_add

[Patrick Massot]

Yes, I think there are lots of Lean 3 names that could be fixed.

[Floris van Doorn]

In non-mathlib projects the naming can be quite sloppy. Feel free to improve them (without worrying that they must resemble the bad Lean 3 name)!

[Michael Rothgang]

Thanks, that is helpful. I've tweaked a few names (pushed already). I will leave it at that for now.

[Kevin Buzzard]

I just marked a student project where several of the declaration names were swearwords.

[Johan Commelin]

Don't look up Lurie's LaTeX labels in old versions of Higher Topos Theory :grinning: