default files

Stream: general

[Yaël Dillies]

I noticed that some .default files weren't for importing all other files in the directory, but rather were basic theory setup. i think those should become .basic, unless people are really attached to be able to not write .basic. Here's the list (thanks Shing!):

• category_theory.category.default
• category_theory.linear.default
• category_theory.preadditive.default
• tactic.lint.default (this one seems to actually be about something default)
• tactic.nth_rewrite.default
• topology.category.CompHaus.default
• topology.category.Profinite.default

[Yaël Dillies]

I already opened #9412 for category_theory.category.default.

[Patrick Massot]

This has been discussed many times. We don't want .default to import everything, we want them to import the default things.

[Shing Tak Lam]

(I don't think Yaël's point was about what .default imports, but rather the files in the list above are definitions and basic theory, and not just importing other files in the directory. Eg. category_theory.category.default was being imported by other files in category_theory.category/)

[Johan Commelin]

Yup, I think it would be good if .default would contain only import statements.

[Yaël Dillies]

Yeah I didn't mean .default files were bad. I meant those were making for bad .default files and should probably be called .basic instead.

[Yaël Dillies]

I think tactic.lint.default is justified though. It's not quite only imports, because there is also the default linter. But I think that's on point?

[Reid Barton]

The name of the module is category_theory.category, because it contains the definition of a category. It was moved to a default.lean file when other modules category_theory.category.foo were added. Is the rule we can't have both X.Y and X.Y.Z (if, say, X.Y.Z imports X.Y)?

[Johan Commelin]

I don't think there are strict rules. On the other hand, I think there are plenty of examples where the definition of X.Y is contained in X.Y.basic.

[Johan Commelin]

And I think that pattern is a bit cleaner.

[Sebastian Ullrich]

Note that Lean 4 uses X.Y in place of X.Y.default

[Johan Commelin]

As in X/Y.lean instead of X/Y/default.lean?

[Sebastian Ullrich]

Yes