some declarations do not show up in the docs

Stream: general

[Floris van Doorn]

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]

(@Rob Lewis )

[Rob Lewis]

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]

Not sure what the intent of that line is

[Floris van Doorn]

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
  generated.

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

[Rob Lewis]

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

[Rob Lewis]

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