Zulip Chat Archive

Stream: general

Topic: misdeclared imports

Yaël Dillies (Aug 02 2021 at 04:46):

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 (Aug 02 2021 at 04:48):

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 (Aug 02 2021 at 04:52):

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

Bryan Gin-ge Chen (Aug 02 2021 at 04:54):

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 (Aug 02 2021 at 04:54):

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

Bryan Gin-ge Chen (Aug 02 2021 at 04:57):

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

Yaël Dillies (Aug 02 2021 at 04:58):

Yeah okay that would make sense.

Yaël Dillies (Aug 02 2021 at 05:00):

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 (Aug 02 2021 at 05:03):

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 (Aug 02 2021 at 08:36):

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

Last updated: Dec 20 2023 at 11:08 UTC