running doc-gen4 on lean4

Stream: lean4

[Siddharth Bhat]

It seems that doc-gen4 cannot be run on the lean4 repo. I was wondering if this is supposed to work in the first place.

[Siddharth Bhat]

(deleted)

[Henrik Böving]

doc-gen4 is supposed to run on repos that use lake as a build system...since lean4 does not do that no it is not. Note however that it will generate documentation for the compiler along with any other project that has the compiler included in the sources it can load (which is really any lake project).

[Siddharth Bhat]

Ah, interesting. So a way to generate docs for just the compiler would be to have a dummy project? Thanks!

[Henrik Böving]

I honestly haven't tried it on anything besides itself and mathlib yet but that should work yes.