doc-gen personal projects?

Stream: general

[Vaibhav Karve]

Is https://github.com/leanprover-community/doc-gen a tool for generating documentation only for mathlib or can it be used for making Mathlib API style documentation for any (personal) lean project? As my lean files grow, I am starting to want a nice and searchable documentation for my projects

[Bryan Gin-ge Chen]

Unfortunately it's not ready for non-mathlib projects as-is. I think @Eric Wieser has gotten it working (with some modifications) on another project though?

[Eric Wieser]

Yes, I have - https://pygae.github.io/lean-ga-docs is my build, and the config file is https://github.com/pygae/lean-ga/blob/master/.github/workflows/lean_doc.yml

[Bryan Gin-ge Chen]

Ah, so it works without modifying doc-gen, great!

[Vaibhav Karve]

Whoa! That's a nicely written up workflow. Unfortunately, it is still to complex for me to use. Thanks either way :+1: :smile: I will take this as indication that the tooling is not yet ready for a noob like me and move on to other problems.

[Eric Wieser]

All you should need to do is copy that file to your project, and replace any occurences of pygae/lean-ga with your repo name

[Eric Wieser]

Ah, so it works without modifying doc-gen, great!

Well, it modifies it at runtime via monkey-patching...