Zulip Chat Archive

Stream: general

Topic: some declarations do not show up in the docs

Floris van Doorn (Mar 04 2021 at 21:16):

Any declaration in this region https://github.com/leanprover-community/lean/blob/de35266fe59614a98ea8a3460a158583fde4fa0d/library/init/meta/widget/basic.lean#L196-L305
does not show up in the docs for that page: https://leanprover-community.github.io/mathlib_docs/init/meta/widget/basic.html

Any idea why?

Floris van Doorn (Mar 04 2021 at 21:28):

(@Rob Lewis )

Rob Lewis (Mar 04 2021 at 22:43):

Every declaration in that block is either a mutual inductive type, or its name has a prefix that's a mutual inductive type. That means they're considered autogenerated: https://github.com/leanprover-community/mathlib/blob/1cc59b9dc6c1efdcda3270750bd7711987266ece/src/meta/expr.lean#L950 and so they don't get printed in the docs

Rob Lewis (Mar 04 2021 at 22:43):

Not sure what the intent of that line is

Floris van Doorn (Mar 04 2021 at 23:21):

Ah, I see.
I think the original intent was to remove false positives from the linter generated by mutual inductives. From the docstring:

There is no cheap way to check whether a declaration in the namespace of a generalized
  inductive type is automatically generated, so for now we say that all of them are automatically

I guess we should remove that check from is_auto_generated and maybe add it back as a check for the linter.

Rob Lewis (Mar 05 2021 at 11:09):

Problem is, that check seems to be the only thing that identifies things like widget.component.cases_on as auto generated

Rob Lewis (Mar 05 2021 at 11:11):

The only check in is_auto_generated right now, that is. So we can't just remove it, we'd need to replace it with something more refined

Last updated: Aug 03 2023 at 10:10 UTC