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