default files

Stream: mathlib4

[Johan Commelin]

Continuing the discussion from https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/data.2Esigma.2Edefault: is it helpful if I make PRs to mathlib that rename default.lean to basic.lean iff default.lean contains more than just import statements?

[Mario Carneiro]

no, default -> basic is not correct. Generally, T.basic will contain the beginnings of theory T, the minimum required to give you the vocabulary and some theorems about it (sometimes this still turned out to be too much stuff and we made an even more basic basic called T.defs), while T.default (which can be imported as just T) is a more kitchen-sink import of everything about T. This latter thing is inherently problematic for imports in mathlib because you can easily get into dependency bloat and import cycles this way, but it is easier for users outside of mathlib to be able to pull in "everything" about T.

[Mario Carneiro]

Lean 4 does not have the T vs T.default ambiguity anymore. You would just name the file T.lean if you want the equivalent behavior, so if we are talking about lean 3 refactors to make it more similar to lean 4, we should move all T/default.lean files to T.lean.

[Johan Commelin]

Ok, a more generic question: should we try to converge to a mathlib3 in which default.lean files only contain import statements?

[Mario Carneiro]

We should probably have a rule about that, but I would be okay with it either way - we could put real files there or require import-only files

[Mario Carneiro]

I guess we would need to come up with a naming convention for the frontend file that brings it all together if that's required not to be T.lean itself

[Johan Commelin]

frontend.lean.

[Johan Commelin]

But I think there are several default.lean files right now that duplicate the role of a basic.lean.

[Johan Commelin]

❯ git ls-files | rg default | xargs wc -l
    9 src/algebra/big_operators/default.lean
    4 src/algebra/category/Group/default.lean
    1 src/algebra/category/Mon/default.lean
    3 src/algebra/category/Ring/default.lean
    5 src/algebra/char_p/default.lean
   14 src/algebra/continued_fractions/computation/default.lean
   14 src/algebra/continued_fractions/default.lean
    2 src/algebra/default.lean
   15 src/algebra/group/default.lean
    1 src/algebra/group_power/default.lean
    1 src/algebra/group_with_zero/default.lean
   12 src/algebra/module/default.lean
   11 src/algebra/ring/default.lean
    3 src/category_theory/adjunction/default.lean
    1 src/category_theory/concrete_category/default.lean
    1 src/category_theory/functor/default.lean
   65 src/category_theory/limits/constructions/over/default.lean
   12 src/category_theory/limits/shapes/default.lean
  144 src/category_theory/linear/default.lean
    2 src/category_theory/monad/default.lean
  346 src/category_theory/preadditive/default.lean
    2 src/category_theory/products/default.lean
    5 src/category_theory/subobject/default.lean
    1 src/category_theory/sums/default.lean
    2 src/control/traversable/default.lean
    1 src/data/fin/tuple/default.lean
    1 src/data/finite/default.lean
    9 src/data/finset/default.lean
   10 src/data/finsupp/default.lean
   28 src/data/list/default.lean
   14 src/data/multiset/default.lean
    4 src/data/mv_polynomial/default.lean
    3 src/data/nat/choose/default.lean
    2 src/data/pfunctor/univariate/default.lean
    5 src/data/polynomial/default.lean
    1 src/data/polynomial/degree/default.lean
    9 src/data/qpf/multivariate/default.lean
    9 src/data/rat/default.lean
  370 src/data/rbmap/default.lean
    6 src/data/rbtree/default.lean
    7 src/data/rbtree/default_lt.lean
    2 src/data/set/default.lean
    2 src/data/set/intervals/default.lean
    1 src/data/sigma/default.lean
    5 src/geometry/euclidean/default.lean
    1 src/group_theory/group_action/default.lean
    1 src/group_theory/submonoid/default.lean
    2 src/linear_algebra/clifford_algebra/default.lean
    1 src/linear_algebra/default.lean
    8 src/linear_algebra/matrix/default.lean
    1 src/number_theory/padics/default.lean
    2 src/order/default.lean
    1 src/order/filter/default.lean
    1 src/ring_theory/adjoin/default.lean
    1 src/ring_theory/polynomial/default.lean
   41 src/tactic/default.lean
    1 src/tactic/linarith/default.lean
  104 src/tactic/lint/default.lean
    7 src/tactic/monotonicity/default.lean
  128 src/tactic/nth_rewrite/default.lean
    0 src/tactic/omega/default.lean
    1 src/tactic/rewrite_search/default.lean
  248 src/topology/category/CompHaus/default.lean
  296 src/topology/category/Profinite/default.lean
    3 src/topology/category/Top/default.lean

[Mario Carneiro]

Even for tactics, frontend doesn't necessarily convey that it is the whole tactic, only the... front end

[Mario Carneiro]

for mathematics it doesn't make sense at all

[Mario Carneiro]

(In fact, it is quite possible to have files that define just the frontend of a tactic without the backend. Tactic.NormNum.Core is exactly that - you get a tactic called norm_num with all the bells and whistles but it does almost nothing until you import the NormNum.Basic file)

[Johan Commelin]

❯ cat src/category_theory/limits/constructions/over/default.lean
/-
Copyright (c) 2018 Johan Commelin. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johan Commelin, Reid Barton, Bhavik Mehta
-/
import category_theory.limits.connected
import category_theory.limits.constructions.over.products
import category_theory.limits.constructions.over.connected
import category_theory.limits.constructions.limits_of_products_and_equalizers
import category_theory.limits.constructions.equalizers

/-!
# Limits in the over category

Declare instances for limits in the over category: If `C` has finite wide pullbacks, `over B` has
finite limits, and if `C` has arbitrary wide pullbacks then `over B` has limits.
-/
universes w v u -- morphism levels before object levels. See note [category_theory universes].

open category_theory category_theory.limits

variables {C : Type u} [category.{v} C]
variable {X : C}

namespace category_theory.over

/-- Make sure we can derive pullbacks in `over B`. -/
instance {B : C} [has_pullbacks C] : has_pullbacks (over B) :=
begin
  letI : has_limits_of_shape (ulift_hom.{v} (ulift.{v} walking_cospan)) C :=
    has_limits_of_shape_of_equivalence (ulift_hom_ulift_category.equiv.{v} _),
  letI : category (ulift_hom.{v} (ulift.{v} walking_cospan)) := infer_instance,
  exact has_limits_of_shape_of_equivalence (ulift_hom_ulift_category.equiv.{v v} _).symm,
end

/-- Make sure we can derive equalizers in `over B`. -/
instance {B : C} [has_equalizers C] : has_equalizers (over B) :=
begin
  letI : has_limits_of_shape (ulift_hom.{v} (ulift.{v} walking_parallel_pair)) C :=
    has_limits_of_shape_of_equivalence (ulift_hom_ulift_category.equiv.{v} _),
  letI : category (ulift_hom.{v} (ulift.{v} walking_parallel_pair)) := infer_instance,
  exact has_limits_of_shape_of_equivalence (ulift_hom_ulift_category.equiv.{v v} _).symm,
end

instance has_finite_limits {B : C} [has_finite_wide_pullbacks C] : has_finite_limits (over B) :=
begin
  apply @has_finite_limits_of_has_equalizers_and_finite_products _ _ _ _,
  { exact construct_products.over_finite_products_of_finite_wide_pullbacks, },
  { apply @has_equalizers_of_has_pullbacks_and_binary_products _ _ _ _,
    { haveI : has_pullbacks C := ⟨by apply_instance⟩,
      exact construct_products.over_binary_product_of_pullback },
    { apply_instance, } }
end

instance has_limits {B : C} [has_wide_pullbacks.{w} C] : has_limits_of_size.{w} (over B) :=
begin
  apply @has_limits_of_has_equalizers_and_products _ _ _ _,
  { exact construct_products.over_products_of_wide_pullbacks },
  { apply @has_equalizers_of_has_pullbacks_and_binary_products _ _ _ _,
    { haveI : has_pullbacks C := ⟨infer_instance⟩,
      exact construct_products.over_binary_product_of_pullback },
    { apply_instance, } }
end

end category_theory.over

[Johan Commelin]

I think this is an example of a file that I would like to rename.

[Johan Commelin]

It can be replaced by a default.lean file that imports whatever the new name of this file is.

[Johan Commelin]

I think limits.lean would be a good name.

[Mario Carneiro]

would the new default.lean have the same imports as this one?

[Mario Carneiro]

so this is just about moving things out of the "central file"

[Johan Commelin]

And in addition it would have the new import bla/bla/limits.lean

[Mario Carneiro]

would people import bla/bla or bla/bla/limits?

[Johan Commelin]

mathlib should not import default files

[Johan Commelin]

but other people can

[Johan Commelin]

It is likely that limits.lean would need less imports than the current default.lean.

[Eric Wieser]

Maybe we should use *.lean instead of default.lean, and then users can write import data.int.«*» to import everything from the module

[Eric Wieser]

(mostly joking)

[Kevin Buzzard]

When I'm teaching I just want to do import tactic to get all the tactics, import topology to get a chunk of topology etc. Fancy stuff which I can never remember how to even type into VS Code and looks more confusing would not be ideal :-)

[Scott Morrison]

Shall I tell the port_status.py script to not list default.lean files?

[Scott Morrison]

And on the mathlib side, we should move all content out of default.lean files.

[Scott Morrison]

Okay, #17724 does the cleanup of default.lean files, I think. This touches lots of files, so speedy merge appreciated. :-)

[Scott Morrison]

Related, #17725 skips listing default.leanfiles in the output of port_status.py.

[Kevin Buzzard]

#17724 doesn't build. Does anyone know what failed?

[Richard Osborn]

It looks like category_theory.additive.basic needs to import category_theory.preadditive.basic. Link to the broken line of code.

[Scott Morrison]

Fixed. (Anyone should feel free to edit my PRs directly, or, for that matter, be bold about editing everyone else's PRs too. :-)