blueprint docs 404

Stream: Polynomial Freiman-Ruzsa conjecture

[Kevin Buzzard]

Screenshot-from-2023-11-26-19-20-20.png
If I click on "concave" on the blueprint and then on "Lean" in the top left above then I get some kind of 404 page on the docs.

[Kevin Buzzard]

Do others get this?
Screenshot-from-2023-11-26-19-23-16.png

[Terence Tao]

Kevin Buzzard said:

Do others get this?
Screenshot-from-2023-11-26-19-23-16.png

Hmm, looks like a case match issue (should be Real.strictConcaveOn_negIdMulLog rather than Real.StrictConcaveOn_negIdMulLog). I just pushed a fix which should propagate to the blueprint in about 30 mins. Thanks for reporting it!

[Kevin Buzzard]

Aah I see! I'm learning how the blueprint software works by reading the source latex in this repo and I was confused because I didn't spot the capital/small issue.

[Terence Tao]

Yeah, because Blueprint goes through LaTeX macros it's difficult to implement any sort of Lean reference checking until one builds the entire blueprint and so one has to rely on manually entering in the references and hoping that there are no typos. It's hard to see how to get around this without abandoning LaTeX (or somehow integrating AI features into the software, which opens a whole different can of worms...).

[Utensil Song]

This can be fixed by adding an optional task inv check which checks the \lean nodes against doc-gen4 collected Lean defs/theorems. This can be checked in CI or locally if you have also run doc-gen4 locally. Lean 4 blueprint is more decoupled from Lean but can be re-integrated optionally.

[Heather Macbeth]

The main theorem (PFR_conjecture) has a broken link in the blueprint, too.

[Terence Tao]

Looks like some lemmas got absorbed into the ProbabilityTheory namespace by mistake. I've pushed a correction which should propagate in the next 30 mins or so.

[Utensil Song]

Just submited a PR to fix a few issues of blueprint: teorth/pfr#93 per discussions with @Kevin Buzzard and @Yaël Dillies .

Checking \lean nodes against Lean defs/theorems will come later as a seperate PR.

[Utensil Song]

My local quick-and-dirty inv check reports the following:

[WARN] The following Lean declarations are referenced in the blueprint but not in Lean:

ent_of_cond_indep -- incomplete, should be a full `ProbabilityTheory.ent_of_cond_indep`
construct_good-prelim -- dash issue, should be `construct_good_prelim`
IdentDistrib.entropy_eq -- incomplete, should be a full `ProbabilityTheory.IdentDistrib.entropy_eq`
eta -- incorrect, should be `η`
tau_min_exists -- spell issue, seems to be `tau_minimizer_exists`
IsUniform.entropy_eq -- incomplete, should be `ProbabilityTheory.IsUniform.entropy_eq`
ProbabilityTheory.entropy_of_uniform -- missing

Issues after -- are marked manually, and they should be fixed, maybe except the incomplete ones.

[Utensil Song]

teorth/pfr#97 is not meant for merging before these issues are fixed.

[Utensil Song]

Utensil Song said:

Just submited a PR to fix a few issues of blueprint: teorth/pfr#93 per discussions with Kevin Buzzard and Yaël Dillies .

Checking \lean nodes against Lean defs/theorems will come later as a seperate PR.

Particularly, CI has reduced from ~24 min to ~14 min as long as Mathlib version is not bumped in the commit.

image.png