doc-gen4 stalling on empty zero-dependency project

Stream: general

[runofff]

Hello, I am trying to locally build documentation for my standalone lean project.
I am running into an issue where DOCGEN_SRC="vscode" lake build DocTest2:docs completely seems to stall at the very last step. I waited more than ten minutes.

The steps that I took were:
1) use the VS Code command palette to "Create Standalone Lean project"
2) create a docbuild/ folder in the new project
3) add the lakefile.toml as specified in the doc-gen4 readme https://github.com/leanprover/doc-gen4 and run lake update doc-gen4 in docbuild/
4) ran DOCGEN_SRC="vscode" lake build DocTest2:docs

This ran for 10 minutes before I killed it. The project has no dependencies and no theorems yet it seems to stall.
Can anyone help? Thanks

anand@jain ~/s/l/D/docbuild (main)> DOCGEN_SRC="vscode" lake build DocTest2:docs
ℹ [132/143] Replayed «doc-gen4»/bibPrepass
info: stdout:
INFO: reference page disabled
⣽ [143/144] Running DocTest2/DocTest2:docs

[Henrik Böving]

The most likely thing it is doing is building the documentation for Lean, Std and Init which it always does in the background. On a weak machine this can definitely take a little while the first time you do it.

[runofff]

but does that happen in step 143/144? I thought I saw that stuff building in earlier steps

[runofff]

I can keep it running though, but is there a way to then skip building these since it's taking so long?

[Henrik Böving]

You can also check htop or whatever other process manager is your favorite to see what it is up to of course.

[runofff]

That's helpful, it is still building Std and Lean. I will go make some food and see if it finishes over lunch