doc-gen error

Stream: FLT

[Kevin Buzzard]

We got an auto-generated issue FLT#471 two days ago saying that bumping needed to be done manually. I just spent over an hour bumping, fixing deprecations, shaking (which took surprisingly long because lake exe shake --fix is broken right now for some reason, it doesn't delete imports, I opened #24743) and linting, and made FLT#476 , but CI is failing for some reason to do with doc-gen:

Run scripts/build_docs.sh
info: docbuild: no previous manifest, creating one from scratch
info: leanprover/doc-gen4: cloning https://github.com/leanprover/doc-gen4
error: /home/runner/work/FLT/FLT/docbuild/../.lake/packages/doc-gen4: revision not found 'v4.20.0-rc5'
Error: Process completed with exit code 1.

Is this just a case of "someone else has to bump doc-gen to rc5 so we just wait" or is this still FLT's problem? I have very little understanding of FLT's relation with doc-gen now.

[Henrik Böving]

CC @Kim Morrison I think we forgot the tag for rc3/4/5?

[Kevin Buzzard]

What do I watch to check what's going on? I'm assuming it's not https://github.com/leanprover-community/doc-gen ? I am totally lost about how to track this issue. Edit: oh found it, it's https://github.com/leanprover/doc-gen4 (as it indeed says in the error message :face_palm: )

[Pietro Monticone]

You can check the toolchain version here.

[Kevin Buzzard]

I would try and bump doc-gen4 but this seems to involve understanding https://github.com/mhuisi/lean4-cli and https://github.com/fgdorais/lean4-unicode-basic , neither of which I have even heard of :-/

[Kevin Buzzard]

I should perhaps stress that I am not at all in a hurry here :-)

[Pietro Monticone]

For release-tagging purposes I've opened the three related PRs.

[Kim Morrison]

Henrik Böving said:

CC Kim Morrison I think we forgot the tag for rc3/4/5?

Indeed... I never wrote any documentation for the "lightweight release" process, where we only try to bump the minimal set of repositories to the latest release candidate, so was only tagging lean4checker and mathlib4, but doc-gen4 needs to be done too.

[Kim Morrison]

Okay, those PRs are merged, and doc-gen4 is tagged at rc3, rc4, and rc5. Hopefully this should unblock people bumping downstream repos to rc5.

[Pietro Monticone]

Thank you, Kim!

[Kevin Buzzard]

I still have

error: /home/runner/work/FLT/FLT/docbuild/../.lake/packages/doc-gen4: revision not found 'v4.20.0-rc5'

on FLT#476 CI, even though https://github.com/leanprover/doc-gen4/pull/281 is merged. Does doc-gen need a tag or something? Or am I just being impatient and I have to wait for some other task to finish? Sorry for being so clueless, I'm no longer sure what I should be tracking.

[Yaël Dillies]

Indeed @Kim Morrison it looks like you missed rc5

[Kim Morrison]

Sigh, done now.

[Kevin Buzzard]

Thanks! Looks like the job is running in FLT#476 ! It's interesting the chaos that this caused; they ran into it in 8d sphere-packing and at least one other project.