Setup doc-gen

Stream: new members

[Christian Merten]

I just tried to add doc-gen4 to a new package but failed. I did the following:

lake new doctest

Following the README at https://github.com/leanprover/doc-gen4 I added

meta if get_config? env = some "dev" then -- dev is so not everyone has to build it
require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"

to lakefile.lean. Then I did

lake -R -Kenv=dev update
lake -R -Kenv=dev build Doctest:docs

Both commands did a lot, but .lake/build/doc was not created. A second run of lake -R Kenv=dev build caused:

error: git exited with code 2 while looking for the git remote in .

What am I doing wrong?

[Henrik Böving]

https://github.com/leanprover/doc-gen4#source-locations

Your project most likely has no git remote with a github style URL so you need to use a different mode to infer source URLs.

[Christian Merten]

Thanks, with the prefix DOCGEN_SRC="file" it worked flawlessly!

[Henrik Böving]

https://github.com/leanprover/doc-gen4/commit/94e10377bef4e64820ffd7dcab6affef3304af62 added a change to make this more clear in the error.