[Merged by Bors] - chore(*): update to lean 3.15.0

[gebner]

The main effect for mathlib comes from leanprover-community/lean#282, which changes the elaboration strategy for structure instance literals ({ foo := 42 }). There are two points where we need to pay attention:

1. Avoid sourcing ({ ..e } where e.g. e : euclidean_domain α) for fields like add, mul, zero, etc. Instead write { add := (+), mul := (*), zero := 0, ..e }. The reason is that { ..e } is equivalent to { mul := euclidean_domain.mul, ..e }. And euclidean_domain.mul should never be mentioned.

I'm not completely sure if this issue remains visible once the structure literal has been elaborated, but this hasn't changed since 3.14. For now, my advice is: if you get weird errors like "cannot unify a * b and ?m_1 * ?m_2 in a structure literal, add mul := (*).

2. refine { le := (≤), .. }; simp is slower. This is because references to (≤) are no longer reduced to le in the subgoals. If a subgoal like a ≤ b → b ≤ a → a = b was stated for preorders (because partial_order extends preorder), then the (≤) will contain a preorder subterm. This subterm also contains other subgoals (proofs of reflexivity and transitivity). Therefore the goals are larger than you might expect:

∀ (a b : α),
    @has_le.le.{u} α
      (@preorder.to_has_le.{u} α
         (@preorder.mk.{u} α le (@lattice.lt._default.{u} α le)
            (@conditionally_complete_lattice.copy._aux_1.{u} α c le eq_le sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf)
            (@conditionally_complete_lattice.copy._aux_2.{u} α c le eq_le sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf)
            (λ (a b : α), iff.refl (@has_lt.lt.{u} α (@has_lt.mk.{u} α (@lattice.lt._default.{u} α le)) a b))))
      a
      b →
    @has_le.le.{u} α
      (@preorder.to_has_le.{u} α
         (@preorder.mk.{u} α le (@lattice.lt._default.{u} α le)
            (@conditionally_complete_lattice.copy._aux_1.{u} α c le eq_le sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf)
            (@conditionally_complete_lattice.copy._aux_2.{u} α c le eq_le sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf)
            (λ (a b : α), iff.refl (@has_lt.lt.{u} α (@has_lt.mk.{u} α (@lattice.lt._default.{u} α le)) a b))))
      b
      a →
    @eq.{u+1} α a b

Advice: in cases such as this, try refine { le := (≤), .. }; abstract { simp } to reduce the size of the (dependent) subgoals.

Zulip thread.

[bryangingechen]

It'd be nice to add tactic docs for all the new stuff in core like #html (I can try to help with this, but later).

[gebner]

Let me quickly explain the cause of this timeout before I forget it. With the new structure instances, terms contain the unreduced fields, e.g. (≤). In particular, these fields now contain a full copy of the structure as it is stated in the definition. For example antisymmetry is stated in terms of a preorder:

∀ (a b : α),
    @has_le.le.{u} α
      (@preorder.to_has_le.{u} α
         (@preorder.mk.{u} α le (@lattice.lt._default.{u} α le)
            (@conditionally_complete_lattice.copy._aux_1.{u} α c le eq_le sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf)
            (@conditionally_complete_lattice.copy._aux_2.{u} α c le eq_le sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf)
            (λ (a b : α), iff.refl (@has_lt.lt.{u} α (@has_lt.mk.{u} α (@lattice.lt._default.{u} α le)) a b))))
      a
      b →
    @has_le.le.{u} α
      (@preorder.to_has_le.{u} α
         (@preorder.mk.{u} α le (@lattice.lt._default.{u} α le)
            (@conditionally_complete_lattice.copy._aux_1.{u} α c le eq_le sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf)
            (@conditionally_complete_lattice.copy._aux_2.{u} α c le eq_le sup eq_sup inf eq_inf Sup eq_Sup Inf eq_Inf)
            (λ (a b : α), iff.refl (@has_lt.lt.{u} α (@has_lt.mk.{u} α (@lattice.lt._default.{u} α le)) a b))))
      b
      a →
    @eq.{u+1} α a b

The abstract tactic introduces these *._aux* definitions to abbreviate the generated proofs. Otherwise they would be expanded and we'd need to substitute (subst_vars) the previous proofs in every goal, leading to horrible performance.

[bryangingechen]

Linting failures are all due to missing docstrings. Unfortunately I don't understand what's going on well enough to add them.

@digama0 do you mind adding docstrings for data/erased.lean?

[gebner]

I've added docs for erased. Documentation for #html is not as urgent since the vscode extension is not ready yet.

[EdAyers]

Where should the docs for #html live?

[jcommelin]

LGTM

[semorrison]

bors merge

[bors]

Build failed (retrying...):

• Build mathlib

[rwbarton]

Do we understand the story with the universe parameters that were made more explicit?

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Build failed:

• Build mathlib

[sgouezel]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests and docs