doc-gen4: git exited with code 128

Stream: new members

[Casuan]

Hello, I am new to Lean and I was trying out doc-gen4 on a simple hello world project but I am getting the following error:
uncaught exception: git exited with code 128

I am using lean4 nightly (I was using stable at first but it's incompatible with the current version of doc-gen4; and i'm not sure how to find the stable version of doc-gen4).

I'm also wondering if there is a generated documentation for Lean's standard library that can be browsed online?

[Alex J. Best]

https://leanprover-community.github.io/mathlib4_docs/ contains doc for Lean, Init, Std, and mathlib4

[Casuan]

thank you!

[Henrik Böving]

If you still want that error to be fixed you'll have to provide more detail, just some git error isn't enough.

The version that doc-gen4 works for guaranteed is in its lean-toolchain file, the one it is used against for mathlib is in mathlib4's lean-toolchain file

[Casuan]

I just tried with the specified toolchain version but I got the same error.

I am doing this in the default project created with lake init hello. I added this to lakefile.lean, as specified on doc-gen4's readme:

meta if get_config? env = some "dev" then
require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"

Then I tried to build with lake build -Kenv=dev Hello:docs and I got the following output:

Documenting Lean core: Init and Lean
Documenting module: Hello
error: > LEAN_PATH=./lean_packages/Cli/build/lib:... ./lean_packages/doc-gen4/build/bin/doc-gen4 single Hello --ink
error: stdout:
Processing modules
Outputting HTML
error: stderr:
uncaught exception: git exited with code 128
error: external command: `./lean_packages/doc-gen4/build/bin/doc-gen4` exited with code 1
...

[Henrik Böving]

doc-gen4 does assume that your project is a git one because every lake project should be git based, is that the case for you?

[Casuan]

Yes, it is the default project created by lake init which is already a git project.