Quickly generate docgen (or verso) for a single file

Stream: general

[Joseph Tooby-Smith]

I would like to do something along the following lines:

Take a single file in PhysLean, and from that quickly generate it's documentation page (using docgen4), or something similar (using e.g. verso). All of the links to other files etc. don't need to be present.

The idea is to just give someone a quick idea of what the documentation for that file is going to look like, without them having to generate it for the whole project (which takes a long time).

Is something along these lines possible?

[Henrik Böving]

You can in principle coerce doc-gen into doing this through manual invocations of the binary but it is not at all supported and can break at any moment in time.

Note that generating documentation only takes long once as the build should be incremental after that.

[Eric Wieser]

Can't you also do lake build PhysLean.MyModule:docs?

[Henrik Böving]

No that's going to build transitive things: https://github.com/leanprover/doc-gen4/blob/main/lakefile.lean#L228-L233

[Thomas Zhu]

You can do the following:

lake exe doc-gen4 single Example.Module ""
lake exe doc-gen4 index

where the "" is sourceUri, but since you don't need links, this is left blank.

Then the generated HTML documentation is at .lake/build/doc/Example/Module.html

(This is probably not a standard usage of doc-gen4.)

[Henrik Böving]

Yes this is the way I was alluding to above. I didn't write it out on purpose to discourage people from relying on an unstable API :P