UnicodeBasic: 'git' exited with code 128

Stream: lean4

[David Renshaw]

If I lake init a new project at v4.26.0-rc2 with this lakefile.toml:

name = "test-lake"
version = "0.1.0"
defaultTargets = ["test-lake"]

[[lean_lib]]
name = "TestLake"

[[require]]
name = "«doc-gen4»"
git = "https://github.com/leanprover/doc-gen4"
rev = "v4.26.0-rc2"

and do lake build, I see this error:

% lake build
info: test-lake: no previous manifest, creating one from scratch
info: doc-gen4: cloning https://github.com/leanprover/doc-gen4
info: doc-gen4: checking out revision '8b1135b818a03f16d69fb796589ebb4ad448d5ea'
info: toolchain not updated; already up-to-date
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '7e1ced9e049a4fab2508980ec4877ca9c46dffc9'
info: UnicodeBasic: cloning https://github.com/fgdorais/lean4-unicode-basic
info: UnicodeBasic: checking out revision '378b62cdf3bb90d3cd9aa12dc2be43b42bdda339'
error: external command 'git' exited with code 128

The commit 378b62cdf3bb90d3cd9aa12dc2be43b42bdda339 appears to not exist in https://github.com/fgdorais/lean4-unicode-basic, even though doc-gen4's lake-manifest.json points to it.

[David Renshaw]

doc-gen4's lakefile.lean points to the nightly-testing branch of https://github.com/fgdorais/lean4-unicode-basic, which should work fine.

[David Renshaw]

So I guess the problem here is that my lake build is using doc-gen4's broken lake-manifest.json.
This is surprising to me, as I was under the impression that a library's lake-manifest.json is not visible to projects that depend on the library. (I believe that's how Cargo.lock works in Rust land.)

[David Renshaw]

This problem has broken our CI build on Noperthedron: https://github.com/jcreedcmu/Noperthedron/actions/runs/19719146140

[Riccardo Brasca]

I have the same error in various projects

[Riccardo Brasca]

No idea how to solve it

[David Renshaw]

correction: the commit currently does exist, just not on any branch: https://github.com/fgdorais/lean4-unicode-basic/tree/378b62cdf3bb90d3cd9aa12dc2be43b42bdda339

[Markus Himmel]

I have updated the v4.26.0-rc2 tag of doc-gen4 to a new commit that should work. Please try lake update (or restarting CI if the error happened in docgen-action) and see if the build succeeds.

[Riccardo Brasca]

It works for me, thanks!

[David Renshaw]

It works for me, too! (After a lake update.) Thanks!

[Malvin Gattinger]

I had the same problem here and here but both times could solve it with lake update doc-gen4.

I guess the "right thing to do" and to avoid breakage like this would be to switch to docgen-action? And/or to stick with non-rc versions?

[Anne Baanen]

docgen-action does a lot of work for you, so I would recommend you use it :) It would unfortunately not solve this specific error (but not leave you worse off either), since the action makes use of the doc-gen release corresponding with the Lean version in lean-toolchain.

Sticking with release candidates of Lean should be okay. Because Mathlib runs under release candidates of Lean, we'll quickly see (and fix, hopefully!) any breakage.

[Malvin Gattinger]

We are running into this issue again here and would like to avoid updating the Lean or mathlib versions used in this project (for now). Is there a way to tell docgen-action to use a working UnicodeBasic without updating Lean? Should it suffice to pin a newer docgen-action version? Cc @Amos Nicodemus

[Markus Himmel]

I suspect that this is due to doc-gen4 not having a v4.25.2 tag. I have now pushed such a tag, so please try again and let me know if it is working now for your repository.

[Amos Nicodemus]

We ended up updating to v4.27.0-rc1 anyway, now it works.