doc-gen4

Stream: mathlib4

[Yury G. Kudryashov]

I've just noticed that theorems like docs#Pi.subNegMonoid.proof_3 are visible in the API docs. IMHO, they should not be there.

[Henrik Böving]

Does someone know the blacklist API for this one? doc-gen does already filter a lot of definitions and theorems so I must've missed an API

[Yury G. Kudryashov]

I don't know. There was a function https://leanprover-community.github.io/mathlib_docs/meta/expr.html#declaration.is_auto_or_internal in mathlib3

[Mario Carneiro]

the mathlib linter framework uses docs#Std.Tactic.Lint.isAutoDecl for this. It would be nice if either the naming convention was more strictly adhered to or there was an attribute on definitions to reliably determine this

[Yury G. Kudryashov]

If we use an attribute, then I would love to have something like @[doc_ignore] to hide auxiliary lemmas from the doc-gen output.

[Yury G. Kudryashov]

Another feature request is to add support for library notes.

[Henrik Böving]

Yury G. Kudryashov said:

If we use an attribute, then I would love to have something like @[doc_ignore] to hide auxiliary lemmas from the doc-gen output.

Per the Rust design heuristic this is a good idea :P

[Yury G. Kudryashov]

I know nothing about Rust, what do they use?

[Henrik Böving]

Well rust also has an attribute that does exactly what you describe. And since the fallback heuristic for Lean design is: Do what Rust does, this is a good idea

[Henrik Böving]

To be precise they have an even more powerful attribute: https://doc.rust-lang.org/rustdoc/write-documentation/the-doc-attribute.html but among other things you can do this: https://doc.rust-lang.org/rustdoc/write-documentation/the-doc-attribute.html#hidden

[Scott Morrison]

Yury G. Kudryashov said:

Another feature request is to add support for library notes.

Just noting that I've now opened an issue to track this, at https://github.com/leanprover/doc-gen4/issues/135.