Zulip Chat Archive
Stream: lean4
Topic: doc-gen4: Declaration decorator hook for external tools
Nicolas Rouquette (Jan 15 2026 at 22:30):
@Henrik Böving I'm close to wrapping up my new tool to answer "What theorems assume, prove,
validate, and depend on?"
This approach leverages the doc-gen4 tool to produce a combined API doc (via doc-gen4) and API coverage (via my tool). I want to provide bi-directional links between these docs. To do this, I need to "inject" into the doc-gen4 pipeline links to the corresponding API coverage pages.
To enable this kind of doc-gen4 extension, I'm proposing exposing an optional argument as described in this issue: https://github.com/leanprover/doc-gen4/issues/343
I prepared a PR for it: https://github.com/leanprover/doc-gen4/pull/344
Last updated: Feb 28 2026 at 14:05 UTC