Zulip Chat Archive

Stream: general

Topic: default files


Yaël Dillies (Sep 27 2021 at 18:48):

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 (Sep 27 2021 at 18:49):

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

Patrick Massot (Sep 27 2021 at 18:56):

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 (Sep 27 2021 at 18:57):

(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 (Sep 27 2021 at 19:15):

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

Yaël Dillies (Sep 27 2021 at 19:45):

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 (Sep 27 2021 at 19:49):

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 (Sep 27 2021 at 23:21):

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 (Sep 28 2021 at 00:02):

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 (Sep 28 2021 at 00:02):

And I think that pattern is a bit cleaner.

Sebastian Ullrich (Sep 28 2021 at 09:26):

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

Johan Commelin (Sep 28 2021 at 09:27):

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

Sebastian Ullrich (Sep 28 2021 at 09:28):

Yes


Last updated: Dec 20 2023 at 11:08 UTC