misdeclared imports

Stream: general

[Yaël Dillies]

I was very confused. number_theory.bernoulli_polynomials uses the lemma nat.choose_eq_factorial_div_factorial' which is declared in data.nat.choose.dvd. But the latter is said by the docs to never be imported.

[Yaël Dillies]

Then I noticed it wasn't namely imported, but instead some files import data.nat.choose. And docgen missed it. Any way to solve that?

[Bryan Gin-ge Chen]

This might be the same as doc-gen#108? I guess default.lean files are skipped somewhere.

[Bryan Gin-ge Chen]

Hmm, tracking things down it looks like doc-gen relies on lean --deps? https://github.com/leanprover-community/doc-gen/blob/71a727905c46c265cf4ec9c108a2434c920380ae/print_docs.py#L306

[Yaël Dillies]

Is importing folder data.x the same as importing data.x.default?

[Bryan Gin-ge Chen]

I believe so: if data/x.lean doesn't exist, lean will look for data/x/default.lean.

[Yaël Dillies]

Yeah okay that would make sense.

[Yaël Dillies]

It's actually worse than just having imports not declared through default files. default files themselves are not declared as imports: https://leanprover-community.github.io/mathlib_docs/algebra/char_p/basic.html

[Yaël Dillies]

I don't know how deps works but maybe it has to do with "data.nat.choose" not being the same as "data.nat.choose.default".

[Eric Wieser]

I think some of the problem is that most of the default.lean files have no docstring, and so doc-gen skips them because there is nothing to write