perf: consider at most one answer for type class resolution subgoals not containing metavariables

closes #3996

.github/workflows/check-stage0.yml

@@ -0,0 +1,57 @@
+name: Check for stage0 changes
+
+on:
+  merge_group:
+  pull_request:
+
+jobs:
+  check-stage0-on-queue:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v4
+      with:
+        ref: ${{ github.event.pull_request.head.sha }}
+        filter: blob:none
+        fetch-depth: 0
+
+    - name: Find base commit
+      if: github.event_name == 'pull_request'
+      run: echo "BASE=$(git merge-base origin/${{ github.base_ref }} HEAD)" >> "$GITHUB_ENV"
+
+    - name: Identify stage0 changes
+      run: |
+        git diff "${BASE:-HEAD^}..HEAD" --name-only -- stage0 |
+          grep -v -x -F $'stage0/src/stdlib_flags.h\nstage0/src/lean.mk.in' \
+          > "$RUNNER_TEMP/stage0" || true
+        if test -s "$RUNNER_TEMP/stage0"
+        then
+          echo "CHANGES=yes" >> "$GITHUB_ENV"
+        else
+          echo "CHANGES=no" >> "$GITHUB_ENV"
+        fi
+      shell: bash
+
+    - if: github.event_name == 'pull_request'
+      name: Set label
+      uses: actions/github-script@v7
+      with:
+        script: |
+          const { owner, repo, number: issue_number  } = context.issue;
+          if (process.env.CHANGES == 'yes') {
+            await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['changes-stage0'] }).catch(() => {});
+          } else {
+            await github.rest.issues.removeLabel({ owner, repo, issue_number, name: 'changes-stage0' }).catch(() => {});
+          }
+
+    - if: env.CHANGES == 'yes'
+      name: Report changes
+      run: |
+        echo "Found changes to stage0/, please do not merge using the merge queue." | tee "$GITHUB_STEP_SUMMARY"
+        # shellcheck disable=SC2129
+        echo '```'                  >> "$GITHUB_STEP_SUMMARY"
+        cat  "$RUNNER_TEMP/stage0"  >> "$GITHUB_STEP_SUMMARY"
+        echo '```'                  >> "$GITHUB_STEP_SUMMARY"
+
+    - if: github.event_name == 'merge_group' && env.CHANGES == 'yes'
+      name: Fail when on the merge queue
+      run: exit 1

CODEOWNERS

@@ -6,7 +6,6 @@
 
 /.github/ @Kha @semorrison
 /RELEASES.md @semorrison
-/src/Init/IO.lean @joehendrix
 /src/kernel/ @leodemoura
 /src/lake/ @tydeu
 /src/Lean/Compiler/ @leodemoura
@@ -20,7 +19,11 @@
 /src/Lean/PrettyPrinter/Delaborator/ @kmill
 /src/Lean/Server/ @mhuisi
 /src/Lean/Widget/ @Vtec234
-/src/runtime/io.cpp @joehendrix
+/src/Init/Data/ @semorrison
+/src/Init/Data/Array/Lemmas.lean @digama0
+/src/Init/Data/List/Lemmas.lean @digama0
+/src/Init/Data/List/BasicAux.lean @digama0
+/src/Init/Data/Array/Subarray.lean @david-christiansen
 /src/Lean/Elab/Tactic/RCases.lean @digama0
 /src/Init/RCases.lean @digama0
 /src/Lean/Elab/Tactic/Ext.lean @digama0
@@ -39,5 +42,4 @@
 /src/Lean/Elab/Tactic/Guard.lean @digama0
 /src/Init/Guard.lean @digama0
 /src/Lean/Server/CodeActions/ @digama0
-/src/Init/Data/Array/Subarray.lean @david-christiansen
 

RELEASES.md

@@ -79,10 +79,11 @@ v4.8.0 (development in progress)
   Field notation can be disabled on a function-by-function basis using the `@[pp_nodot]` attribute.
 
 * Added options `pp.mvars` (default: true) and `pp.mvars.withType` (default: false).
-  When `pp.mvars` is false, metavariables pretty print as `?_`,
-  and when `pp.mvars.withType` is true, metavariables pretty print with a type ascription.
-  These can be set when using `#guard_msgs` to make tests not rely on the unique ids assigned to anonymous metavariables.
-  [#3798](https://github.com/leanprover/lean4/pull/3798).
+  When `pp.mvars` is false, expression metavariables pretty print as `?_` and universe metavariables pretty print as `_`.
+  When `pp.mvars.withType` is true, expression metavariables pretty print with a type ascription.
+  These can be set when using `#guard_msgs` to make tests not depend on the particular names of metavariables.
+  [#3798](https://github.com/leanprover/lean4/pull/3798) and
+  [#3978](https://github.com/leanprover/lean4/pull/3978).
 
 * Added `@[induction_eliminator]` and `@[cases_eliminator]` attributes to be able to define custom eliminators
   for the `induction` and `cases` tactics, replacing the `@[eliminator]` attribute.

doc/dev/bootstrap.md

@@ -75,14 +75,25 @@ The github repository will automatically update stage0 on `master` once
 
 If you have write access to the lean4 repository, you can also also manually
 trigger that process, for example to be able to use new features in the compiler itself.
-You can do that on <https://github.com/nomeata/lean4/actions/workflows/update-stage0.yml>
+You can do that on <https://github.com/leanprover/lean4/actions/workflows/update-stage0.yml>
 or using Github CLI with
 ```
 gh workflow run update-stage0.yml
 ```
 
-Leaving stage0 updates to the CI automation is preferable, but should you need to do it locally, you can use `make update-stage0-commit` in `build/release` to update `stage0` from `stage1` or `make -C stageN update-stage0-commit` to update from another stage.
-This command will automatically stage the updated files and introduce a commit, so make sure to commit your work before that. Then coordinate with the admins to not squash your PR so that stage 0 updates are preserved as separate commits.
+Leaving stage0 updates to the CI automation is preferable, but should you need
+to do it locally, you can use `make update-stage0-commit` in `build/release` to
+update `stage0` from `stage1` or `make -C stageN update-stage0-commit` to
+update from another stage.
+
+This command will automatically stage the updated files and introduce a commit,
+so make sure to commit your work before that.
+
+The CI should prevent PRs with changes to stage0 (besides `stdlib_flags.h`)
+from entering `master` through the (squashing!) merge queue, and label such PRs
+with the `changes-stage0` label. Such PRs should have a cleaned up history,
+with separate stage0 update commits; then coordinate with the admins to merge
+your PR using rebase merge, bypassing the merge queue.
 
 ## Further Bootstrapping Complications
 

doc/examples/Certora2022/ex8.lean

@@ -4,16 +4,16 @@ def ack : Nat → Nat → Nat
   | 0,   y   => y+1
   | x+1, 0   => ack x 1
   | x+1, y+1 => ack x (ack (x+1) y)
-termination_by ack x y => (x, y)
+termination_by x y => (x, y)
 
 def sum (a : Array Int) : Int :=
   let rec go (i : Nat) :=
-     if i < a.size then
+     if _ : i < a.size then
         a[i] + go (i+1)
      else
         0
+  termination_by a.size - i
   go 0
-termination_by go i => a.size - i
 
 set_option pp.proofs true
 #print sum.go

doc/examples/ICERM2022/ctor.lean

@@ -4,43 +4,42 @@ open Lean Meta
 
 def ctor (mvarId : MVarId) (idx : Nat) : MetaM (List MVarId) := do
   /- Set `MetaM` context using `mvarId` -/
-  withMVarContext mvarId do 
+  mvarId.withContext do
     /- Fail if the metavariable is already assigned. -/
-    checkNotAssigned mvarId `ctor
+    mvarId.checkNotAssigned `ctor
     /- Retrieve the target type, instantiateMVars, and use `whnf`. -/
-    let target ← getMVarType' mvarId
+    let target ← mvarId.getType'
     let .const declName us := target.getAppFn
       | throwTacticEx `ctor mvarId "target is not an inductive datatype"
     let .inductInfo { ctors, .. } ← getConstInfo declName
       | throwTacticEx `ctor mvarId "target is not an inductive datatype"
     if idx = 0 then
-      throwTacticEx `ctor mvarId "invalid index, it must be > 0"  
+      throwTacticEx `ctor mvarId "invalid index, it must be > 0"
     else if h : idx - 1 < ctors.length then
-      apply mvarId (.const ctors[idx - 1] us)
+      mvarId.apply (.const ctors[idx - 1] us)
     else
-      throwTacticEx `ctor mvarId "invalid index, inductive datatype has only {ctors.length} contructors"  
+      throwTacticEx `ctor mvarId "invalid index, inductive datatype has only {ctors.length} contructors"
 
 open Elab Tactic
 
-elab "ctor" idx:num : tactic => 
+elab "ctor" idx:num : tactic =>
   liftMetaTactic (ctor · idx.getNat)
 
-example (p : Prop) : p := by 
+example (p : Prop) : p := by
   ctor 1 -- Error
 
-example (h : q) : p ∨ q := by 
+example (h : q) : p ∨ q := by
   ctor 0 -- Error
   exact h
 
-example (h : q) : p ∨ q := by 
+example (h : q) : p ∨ q := by
   ctor 3 -- Error
   exact h
 
-example (h : q) : p ∨ q := by 
+example (h : q) : p ∨ q := by
   ctor 2
   exact h
 
-example (h : q) : p ∨ q := by 
+example (h : q) : p ∨ q := by
   ctor 1
-  exact h -- Error 
-
+  exact h -- Error

doc/examples/ICERM2022/meta.lean

@@ -5,15 +5,15 @@ open Lean Meta
 def ex1 (declName : Name) : MetaM Unit := do
   let info ← getConstInfo declName
   IO.println s!"{declName} : {← ppExpr info.type}"
-  if let some val := info.value? then 
+  if let some val := info.value? then
     IO.println s!"{declName} : {← ppExpr val}"
-    
+
 #eval ex1 ``Nat
 
 def ex2 (declName : Name) : MetaM Unit := do
   let info ← getConstInfo declName
   trace[Meta.debug] "{declName} : {info.type}"
-  if let some val := info.value? then 
+  if let some val := info.value? then
     trace[Meta.debug] "{declName} : {val}"
 
 #eval ex2 ``Add.add
@@ -30,9 +30,9 @@ def ex3 (declName : Name) : MetaM Unit := do
       trace[Meta.debug] "{x} : {← inferType x}"
 
 def myMin [LT α] [DecidableRel (α := α) (·<·)] (a b : α) : α :=
-  if a < b then 
+  if a < b then
     a
-  else 
+  else
     b
 
 set_option trace.Meta.debug true in
@@ -40,7 +40,7 @@ set_option trace.Meta.debug true in
 
 def ex4 : MetaM Unit := do
   let nat := mkConst ``Nat
-  withLocalDeclD `a nat fun a => 
+  withLocalDeclD `a nat fun a =>
   withLocalDeclD `b nat fun b => do
     let e ← mkAppM ``HAdd.hAdd #[a, b]
     trace[Meta.debug] "{e} : {← inferType e}"
@@ -66,15 +66,17 @@ open Elab Term
 
 def ex5 : TermElabM Unit := do
   let nat := Lean.mkConst ``Nat
-  withLocalDeclD `a nat fun a => do 
+  withLocalDeclD `a nat fun a => do
   withLocalDeclD `b nat fun b => do
     let ab ← mkAppM ``HAdd.hAdd #[a, b]
-    let stx ← `(fun x => if x < 10 then $(← exprToSyntax ab) + x else x + $(← exprToSyntax a))
+    let abStx ← exprToSyntax ab
+    let aStx ← exprToSyntax a
+    let stx ← `(fun x => if x < 10 then $abStx + x else x + $aStx)
     let e ← elabTerm stx none
     trace[Meta.debug] "{e} : {← inferType e}"
     let e := mkApp e (mkNatLit 5)
     let e ← whnf e
     trace[Meta.debug] "{e}"
-       
+
 set_option trace.Meta.debug true in
 #eval ex5

doc/examples/NFM2022/nfm8.lean

@@ -4,16 +4,16 @@ def ack : Nat → Nat → Nat
   | 0,   y   => y+1
   | x+1, 0   => ack x 1
   | x+1, y+1 => ack x (ack (x+1) y)
-termination_by ack x y => (x, y)
+termination_by x y => (x, y)
 
 def sum (a : Array Int) : Int :=
   let rec go (i : Nat) :=
-     if i < a.size then
+     if _ : i < a.size then
         a[i] + go (i+1)
      else
         0
+  termination_by a.size - i
   go 0
-termination_by go i => a.size - i
 
 set_option pp.proofs true
 #print sum.go

script/issues_summary.sh

@@ -0,0 +1,39 @@
+#!/bin/bash
+
+# https://chat.openai.com/share/7469c7c3-aceb-4d80-aee5-62982e1f1538
+
+# Output CSV Header
+echo '"Issue URL","Title","Days Since Creation","Days Since Last Update","Total Reactions","Assignee","Labels"'
+
+# Get the current date in YYYY-MM-DD format
+today=$(date +%Y-%m-%d)
+
+# Fetch only open issues (excluding PRs and closed issues) from the repository 'leanprover/lean4'
+issues=$(gh api repos/leanprover/lean4/issues --paginate --jq '.[] | select(.pull_request == null and .state == "open") | {url: .html_url, title: .title, created_at: (.created_at | split("T")[0]), updated_at: (.updated_at | split("T")[0]), number: .number, assignee: (.assignee.login // ""), labels: [.labels[].name] | join(",")}')
+
+# Process each JSON object
+echo "$issues" | while IFS= read -r issue; do
+    # Extract fields from JSON
+    url=$(echo "$issue" | jq -r '.url')
+    title=$(echo "$issue" | jq -r '.title')
+    created_at=$(echo "$issue" | jq -r '.created_at')
+    updated_at=$(echo "$issue" | jq -r '.updated_at')
+    issue_number=$(echo "$issue" | jq -r '.number')
+    assignee=$(echo "$issue" | jq -r '.assignee')
+    labels=$(echo "$issue" | jq -r '.labels')
+
+    # Calculate days since creation and update using macOS compatible date calculation
+    days_since_created=$(( ($(date -jf "%Y-%m-%d" "$today" +%s) - $(date -jf "%Y-%m-%d" "$created_at" +%s)) / 86400 ))
+    days_since_updated=$(( ($(date -jf "%Y-%m-%d" "$today" +%s) - $(date -jf "%Y-%m-%d" "$updated_at" +%s)) / 86400 ))
+
+    # Fetch the total number of reactions for each issue
+    reaction_data=$(gh api repos/leanprover/lean4/issues/$issue_number/reactions --paginate --jq 'length' 2>&1)
+    if [[ $reaction_data == *"Not Found"* ]]; then
+        total_reactions="Error fetching reactions"
+    else
+        total_reactions=$reaction_data
+    fi
+
+    # Format output as CSV by escaping quotes and delimiting with commas
+    echo "\"$url\",\"${title//\"/\"\"}\",\"$days_since_created\",\"$days_since_updated\",\"$total_reactions\",\"$assignee\",\"$labels\""
+done

src/Init/Core.lean

@@ -2040,4 +2040,8 @@ class LawfulCommIdentity (op : α → α → α) (o : outParam α) [hc : Commuta
   left_id a := Eq.trans (hc.comm o a) (right_id a)
   right_id a := Eq.trans (hc.comm a o) (left_id a)
 
+instance : Commutative Or := ⟨fun _ _ => propext or_comm⟩
+instance : Commutative And := ⟨fun _ _ => propext and_comm⟩
+instance : Commutative Iff := ⟨fun _ _ => propext iff_comm⟩
+
 end Std

src/Init/Data/Array/Lemmas.lean

@@ -5,6 +5,7 @@ Authors: Mario Carneiro
 -/
 prelude
 import Init.Data.Nat.MinMax
+import Init.Data.Nat.Lemmas
 import Init.Data.List.Lemmas
 import Init.Data.Fin.Basic
 import Init.Data.Array.Mem
@@ -187,7 +188,8 @@ theorem anyM_stop_le_start [Monad m] (p : α → m Bool) (as : Array α) (start
 theorem mem_def (a : α) (as : Array α) : a ∈ as ↔ a ∈ as.data :=
   ⟨fun | .mk h => h, Array.Mem.mk⟩
 
-/-- # get -/
+/-! # get -/
+
 @[simp] theorem get_eq_getElem (a : Array α) (i : Fin _) : a.get i = a[i.1] := rfl
 
 theorem getElem?_lt
@@ -217,7 +219,7 @@ theorem get!_eq_getD [Inhabited α] (a : Array α) : a.get! n = a.getD n default
 @[simp] theorem get!_eq_getElem? [Inhabited α] (a : Array α) (i : Nat) : a.get! i = (a.get? i).getD default := by
   by_cases p : i < a.size <;> simp [getD_get?, get!_eq_getD, p]
 
-/-- # set -/
+/-! # set -/
 
 @[simp] theorem getElem_set_eq (a : Array α) (i : Fin a.size) (v : α) {j : Nat}
       (eq : i.val = j) (p : j < (a.set i v).size) :
@@ -240,7 +242,7 @@ theorem getElem_set (a : Array α) (i : Fin a.size) (v : α) (j : Nat)
     (ne : i.val ≠ j) : (a.set i v)[j]? = a[j]? := by
   by_cases h : j < a.size <;> simp [getElem?_lt, getElem?_ge, Nat.ge_of_not_lt, ne, h]
 
-/- # setD -/
+/-! # setD -/
 
 @[simp] theorem set!_is_setD : @set! = @setD := rfl
 
@@ -266,4 +268,44 @@ theorem getElem?_setD_eq (a : Array α) {i : Nat} (p : i < a.size) (v : α) : (a
   by_cases h : i < a.size <;>
     simp [setD, Nat.not_lt_of_le, h,  getD_get?]
 
+/-! # ofFn -/
+
+@[simp] theorem size_ofFn_go {n} (f : Fin n → α) (i acc) :
+    (ofFn.go f i acc).size = acc.size + (n - i) := by
+  if hin : i < n then
+    unfold ofFn.go
+    have : 1 + (n - (i + 1)) = n - i :=
+      Nat.sub_sub .. ▸ Nat.add_sub_cancel' (Nat.le_sub_of_add_le (Nat.add_comm .. ▸ hin))
+    rw [dif_pos hin, size_ofFn_go f (i+1), size_push, Nat.add_assoc, this]
+  else
+    have : n - i = 0 := Nat.sub_eq_zero_of_le (Nat.le_of_not_lt hin)
+    unfold ofFn.go
+    simp [hin, this]
+termination_by n - i
+
+@[simp] theorem size_ofFn (f : Fin n → α) : (ofFn f).size = n := by simp [ofFn]
+
+theorem getElem_ofFn_go (f : Fin n → α) (i) {acc k}
+    (hki : k < n) (hin : i ≤ n) (hi : i = acc.size)
+    (hacc : ∀ j, ∀ hj : j < acc.size, acc[j] = f ⟨j, Nat.lt_of_lt_of_le hj (hi ▸ hin)⟩) :
+    haveI : acc.size + (n - acc.size) = n := Nat.add_sub_cancel' (hi ▸ hin)
+    (ofFn.go f i acc)[k]'(by simp [*]) = f ⟨k, hki⟩ := by
+  unfold ofFn.go
+  if hin : i < n then
+    have : 1 + (n - (i + 1)) = n - i :=
+      Nat.sub_sub .. ▸ Nat.add_sub_cancel' (Nat.le_sub_of_add_le (Nat.add_comm .. ▸ hin))
+    simp only [dif_pos hin]
+    rw [getElem_ofFn_go f (i+1) _ hin (by simp [*]) (fun j hj => ?hacc)]
+    cases (Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ (by simpa using hj)) with
+    | inl hj => simp [get_push, hj, hacc j hj]
+    | inr hj => simp [get_push, *]
+  else
+    simp [hin, hacc k (Nat.lt_of_lt_of_le hki (Nat.le_of_not_lt (hi ▸ hin)))]
+termination_by n - i
+
+@[simp] theorem getElem_ofFn (f : Fin n → α) (i : Nat) (h) :
+    (ofFn f)[i] = f ⟨i, size_ofFn f ▸ h⟩ :=
+  getElem_ofFn_go _ _ _ (by simp) (by simp) nofun
+
+
 end Array

src/Init/Data/BitVec/Lemmas.lean

@@ -826,13 +826,18 @@ theorem ofNat_add_ofNat {n} (x y : Nat) : x#n + y#n = (x + y)#n :=
 
 protected theorem add_assoc (x y z : BitVec n) : x + y + z = x + (y + z) := by
   apply eq_of_toNat_eq ; simp [Nat.add_assoc]
+instance : Std.Associative (α := BitVec n) (· + ·) := ⟨BitVec.add_assoc⟩
 
 protected theorem add_comm (x y : BitVec n) : x + y = y + x := by
   simp [add_def, Nat.add_comm]
+instance : Std.Commutative (α := BitVec n) (· + ·) := ⟨BitVec.add_comm⟩
 
 @[simp] protected theorem add_zero (x : BitVec n) : x + 0#n = x := by simp [add_def]
 
 @[simp] protected theorem zero_add (x : BitVec n) : 0#n + x = x := by simp [add_def]
+instance : Std.LawfulIdentity (α := BitVec n) (· + ·) 0#n where
+  left_id := BitVec.zero_add
+  right_id := BitVec.add_zero
 
 theorem truncate_add (x y : BitVec w) (h : i ≤ w) :
     (x + y).truncate i = x.truncate i + y.truncate i := by

src/Init/Data/Bool.lean

@@ -74,6 +74,7 @@ Added for confluence with `not_and_self` `and_not_self` on term
 @[simp] theorem eq_false_and_eq_true_self : ∀(b : Bool), (b = false ∧ b = true) ↔ False := by decide
 
 theorem and_comm : ∀ (x y : Bool), (x && y) = (y && x) := by decide
+instance : Std.Commutative (· && ·) := ⟨and_comm⟩
 
 theorem and_left_comm : ∀ (x y z : Bool), (x && (y && z)) = (y && (x && z)) := by decide
 theorem and_right_comm : ∀ (x y z : Bool), ((x && y) && z) = ((x && z) && y) := by decide
@@ -120,6 +121,7 @@ Needed for confluence of term `(a || b) ↔ a` which reduces to `(a || b) = a` v
 @[simp] theorem iff_or_self : ∀(a b : Bool), (b = (a || b)) ↔ (a → b) := by decide
 
 theorem or_comm : ∀ (x y : Bool), (x || y) = (y || x) := by decide
+instance : Std.Commutative (· || ·) := ⟨or_comm⟩
 
 theorem or_left_comm : ∀ (x y z : Bool), (x || (y || z)) = (y || (x || z)) := by decide
 theorem or_right_comm : ∀ (x y z : Bool), ((x || y) || z) = ((x || z) || y) := by decide
@@ -186,12 +188,18 @@ in false_eq and true_eq.
 @[simp] theorem true_beq  : ∀b, (true  == b) =  b := by decide
 @[simp] theorem false_beq : ∀b, (false == b) = !b := by decide
 @[simp] theorem beq_true  : ∀b, (b == true)  =  b := by decide
+instance : Std.LawfulIdentity (· == ·) true where
+  left_id := true_beq
+  right_id := beq_true
 @[simp] theorem beq_false : ∀b, (b == false) = !b := by decide
 
 @[simp] theorem true_bne  : ∀(b : Bool), (true  != b) = !b := by decide
 @[simp] theorem false_bne : ∀(b : Bool), (false != b) =  b := by decide
 @[simp] theorem bne_true  : ∀(b : Bool), (b != true)  = !b := by decide
 @[simp] theorem bne_false : ∀(b : Bool), (b != false) =  b := by decide
+instance : Std.LawfulIdentity (· != ·) false where
+  left_id := false_bne
+  right_id := bne_false
 
 @[simp] theorem not_beq_self : ∀ (x : Bool), ((!x) == x) = false := by decide
 @[simp] theorem beq_not_self : ∀ (x : Bool), (x   == !x) = false := by decide
@@ -214,6 +222,7 @@ due to `beq_iff_eq`.
 @[simp] theorem not_bne_not : ∀ (x y : Bool), ((!x) != (!y)) = (x != y) := by decide
 
 @[simp] theorem bne_assoc : ∀ (x y z : Bool), ((x != y) != z) = (x != (y != z)) := by decide
+instance : Std.Associative (· != ·) := ⟨bne_assoc⟩
 
 @[simp] theorem bne_left_inj  : ∀ (x y z : Bool), (x != y) = (x != z) ↔ y = z := by decide
 @[simp] theorem bne_right_inj : ∀ (x y z : Bool), (x != z) = (y != z) ↔ x = y := by decide

src/Init/Data/Fin/Lemmas.lean

@@ -793,15 +793,20 @@ protected theorem mul_one (k : Fin (n + 1)) : k * 1 = k := by
 
 protected theorem mul_comm (a b : Fin n) : a * b = b * a :=
   ext <| by rw [mul_def, mul_def, Nat.mul_comm]
+instance : Std.Commutative (α := Fin n) (· * ·) := ⟨Fin.mul_comm⟩
 
 protected theorem mul_assoc (a b c : Fin n) : a * b * c = a * (b * c) := by
   apply eq_of_val_eq
   simp only [val_mul]
   rw [← Nat.mod_eq_of_lt a.isLt, ← Nat.mod_eq_of_lt b.isLt, ← Nat.mod_eq_of_lt c.isLt]
   simp only [← Nat.mul_mod, Nat.mul_assoc]
+instance : Std.Associative (α := Fin n) (· * ·) := ⟨Fin.mul_assoc⟩
 
 protected theorem one_mul (k : Fin (n + 1)) : (1 : Fin (n + 1)) * k = k := by
   rw [Fin.mul_comm, Fin.mul_one]
+instance : Std.LawfulIdentity (α := Fin (n + 1)) (· * ·) 1 where
+  left_id := Fin.one_mul
+  right_id := Fin.mul_one
 
 protected theorem mul_zero (k : Fin (n + 1)) : k * 0 = 0 := by simp [ext_iff, mul_def]
 

src/Init/Data/Int/Lemmas.lean

@@ -137,12 +137,16 @@ protected theorem add_comm : ∀ a b : Int, a + b = b + a
   | ofNat _, -[_+1]  => rfl
   | -[_+1],  ofNat _ => rfl
   | -[_+1],  -[_+1]  => by simp [Nat.add_comm]
+instance : Std.Commutative (α := Int) (· + ·) := ⟨Int.add_comm⟩
 
 @[simp] protected theorem add_zero : ∀ a : Int, a + 0 = a
   | ofNat _ => rfl
   | -[_+1]  => rfl
 
 @[simp] protected theorem zero_add (a : Int) : 0 + a = a := Int.add_comm .. ▸ a.add_zero
+instance : Std.LawfulIdentity (α := Int) (· + ·) 0 where
+  left_id := Int.zero_add
+  right_id := Int.add_zero
 
 theorem ofNat_add_negSucc_of_lt (h : m < n.succ) : ofNat m + -[n+1] = -[n - m+1] :=
   show subNatNat .. = _ by simp [succ_sub (le_of_lt_succ h), subNatNat]
@@ -196,6 +200,7 @@ where
     simp
     rw [Int.add_comm, subNatNat_add_negSucc]
     simp [Nat.add_comm, Nat.add_left_comm, Nat.add_assoc]
+instance : Std.Associative (α := Int) (· + ·) := ⟨Int.add_assoc⟩
 
 protected theorem add_left_comm (a b c : Int) : a + (b + c) = b + (a + c) := by
   rw [← Int.add_assoc, Int.add_comm a, Int.add_assoc]
@@ -351,6 +356,7 @@ protected theorem sub_right_inj (i j k : Int) : (i - k = j - k) ↔ i = j := by
 
 protected theorem mul_comm (a b : Int) : a * b = b * a := by
   cases a <;> cases b <;> simp [Nat.mul_comm]
+instance : Std.Commutative (α := Int) (· * ·) := ⟨Int.mul_comm⟩
 
 theorem ofNat_mul_negOfNat (m n : Nat) : (m : Nat) * negOfNat n = negOfNat (m * n) := by
   cases n <;> rfl
@@ -369,6 +375,7 @@ attribute [local simp] ofNat_mul_negOfNat negOfNat_mul_ofNat
 
 protected theorem mul_assoc (a b c : Int) : a * b * c = a * (b * c) := by
   cases a <;> cases b <;> cases c <;> simp [Nat.mul_assoc]
+instance : Std.Associative (α := Int) (· * ·) := ⟨Int.mul_assoc⟩
 
 protected theorem mul_left_comm (a b c : Int) : a * (b * c) = b * (a * c) := by
   rw [← Int.mul_assoc, ← Int.mul_assoc, Int.mul_comm a]
@@ -458,6 +465,9 @@ protected theorem sub_mul (a b c : Int) : (a - b) * c = a * c - b * c := by
   | -[n+1]  => show -[1 * n +1] = -[n+1] by rw [Nat.one_mul]
 
 @[simp] protected theorem mul_one (a : Int) : a * 1 = a := by rw [Int.mul_comm, Int.one_mul]
+instance : Std.LawfulIdentity (α := Int) (· * ·) 1 where
+  left_id := Int.one_mul
+  right_id := Int.mul_one
 
 protected theorem mul_neg_one (a : Int) : a * -1 = -a := by rw [Int.mul_neg, Int.mul_one]
 

src/Init/Data/Int/Order.lean

@@ -187,6 +187,7 @@ protected theorem min_comm (a b : Int) : min a b = min b a := by
   by_cases h₁ : a ≤ b <;> by_cases h₂ : b ≤ a <;> simp [h₁, h₂]
   · exact Int.le_antisymm h₁ h₂
   · cases not_or_intro h₁ h₂ <| Int.le_total ..
+instance : Std.Commutative (α := Int) min := ⟨Int.min_comm⟩
 
 protected theorem min_le_right (a b : Int) : min a b ≤ b := by rw [Int.min_def]; split <;> simp [*]
 
@@ -206,6 +207,7 @@ protected theorem max_comm (a b : Int) : max a b = max b a := by
   by_cases h₁ : a ≤ b <;> by_cases h₂ : b ≤ a <;> simp [h₁, h₂]
   · exact Int.le_antisymm h₂ h₁
   · cases not_or_intro h₁ h₂ <| Int.le_total ..
+instance : Std.Commutative (α := Int) max := ⟨Int.max_comm⟩
 
 protected theorem le_max_left (a b : Int) : a ≤ max a b := by rw [Int.max_def]; split <;> simp [*]
 

src/Init/Data/List/Basic.lean

@@ -127,6 +127,9 @@ instance : Append (List α) := ⟨List.append⟩
   | nil => rfl
   | cons a as ih =>
     simp_all [HAppend.hAppend, Append.append, List.append]
+instance : Std.LawfulIdentity (α := List α) (· ++ ·) [] where
+  left_id := nil_append
+  right_id := append_nil
 
 @[simp] theorem cons_append (a : α) (as bs : List α) : (a::as) ++ bs = a::(as ++ bs) := rfl
 
@@ -136,6 +139,7 @@ theorem append_assoc (as bs cs : List α) : (as ++ bs) ++ cs = as ++ (bs ++ cs)
   induction as with
   | nil => rfl
   | cons a as ih => simp [ih]
+instance : Std.Associative (α := List α) (· ++ ·) := ⟨append_assoc⟩
 
 theorem append_cons (as : List α) (b : α) (bs : List α) : as ++ b :: bs = as ++ [b] ++ bs := by
   induction as with

src/Init/Data/List/BasicAux.lean

@@ -5,6 +5,7 @@ Author: Leonardo de Moura
 -/
 prelude
 import Init.Data.Nat.Linear
+import Init.Ext
 
 universe u
 
@@ -43,6 +44,14 @@ See also `get?` and `get!`.
 def getD (as : List α) (i : Nat) (fallback : α) : α :=
   (as.get? i).getD fallback
 
+@[ext] theorem ext : ∀ {l₁ l₂ : List α}, (∀ n, l₁.get? n = l₂.get? n) → l₁ = l₂
+  | [], [], _ => rfl
+  | a :: l₁, [], h => nomatch h 0
+  | [], a' :: l₂, h => nomatch h 0
+  | a :: l₁, a' :: l₂, h => by
+    have h0 : some a = some a' := h 0
+    injection h0 with aa; simp only [aa, ext fun n => h (n+1)]
+
 /--
 Returns the first element in the list.
 
@@ -148,6 +157,13 @@ def getLastD : (as : List α) → (fallback : α) → α
   | [],   a₀ => a₀
   | a::as, _ => getLast (a::as) (fun h => List.noConfusion h)
 
+/--
+`O(n)`. Rotates the elements of `xs` to the left such that the element at
+`xs[i]` rotates to `xs[(i - n) % l.length]`.
+* `rotateLeft [1, 2, 3, 4, 5] 3 = [4, 5, 1, 2, 3]`
+* `rotateLeft [1, 2, 3, 4, 5] 5 = [1, 2, 3, 4, 5]`
+* `rotateLeft [1, 2, 3, 4, 5] = [2, 3, 4, 5, 1]`
+-/
 def rotateLeft (xs : List α) (n : Nat := 1) : List α :=
   let len := xs.length
   if len ≤ 1 then
@@ -158,6 +174,13 @@ def rotateLeft (xs : List α) (n : Nat := 1) : List α :=
     let e := xs.drop n
     e ++ b
 
+/--
+`O(n)`. Rotates the elements of `xs` to the right such that the element at
+`xs[i]` rotates to `xs[(i + n) % l.length]`.
+* `rotateRight [1, 2, 3, 4, 5] 3 = [3, 4, 5, 1, 2]`
+* `rotateRight [1, 2, 3, 4, 5] 5 = [1, 2, 3, 4, 5]`
+* `rotateRight [1, 2, 3, 4, 5] = [5, 1, 2, 3, 4]`
+-/
 def rotateRight (xs : List α) (n : Nat := 1) : List α :=
   let len := xs.length
   if len ≤ 1 then
@@ -288,6 +311,15 @@ def mapMono (as : List α) (f : α → α) : List α :=
 Monadic generalization of `List.partition`.
 
 This uses `Array.toList` and which isn't imported by `Init.Data.List.Basic`.
+```
+def posOrNeg (x : Int) : Except String Bool :=
+  if x > 0 then pure true
+  else if x < 0 then pure false
+  else throw "Zero is not positive or negative"
+
+partitionM posOrNeg [-1, 2, 3] = Except.ok ([2, 3], [-1])
+partitionM posOrNeg [0, 2, 3] = Except.error "Zero is not positive or negative"
+```
 -/
 @[inline] def partitionM [Monad m] (p : α → m Bool) (l : List α) : m (List α × List α) :=
   go l #[] #[]

src/Init/Data/List/Lemmas.lean

@@ -274,6 +274,19 @@ theorem get?_reverse {l : List α} (i) (h : i < length l) :
 
 @[simp] theorem getD_cons_succ : getD (x :: xs) (n + 1) d = getD xs n d := rfl
 
+theorem ext_get {l₁ l₂ : List α} (hl : length l₁ = length l₂)
+    (h : ∀ n h₁ h₂, get l₁ ⟨n, h₁⟩ = get l₂ ⟨n, h₂⟩) : l₁ = l₂ :=
+  ext fun n =>
+    if h₁ : n < length l₁ then by
+      rw [get?_eq_get, get?_eq_get, h n h₁ (by rwa [← hl])]
+    else by
+      have h₁ := Nat.le_of_not_lt h₁
+      rw [get?_len_le h₁, get?_len_le]; rwa [← hl]
+
+@[simp] theorem get_map (f : α → β) {l n} :
+    get (map f l) n = f (get l ⟨n, length_map l f ▸ n.2⟩) :=
+  Option.some.inj <| by rw [← get?_eq_get, get?_map, get?_eq_get]; rfl
+
 /-! ### take and drop -/
 
 @[simp] theorem take_append_drop : ∀ (n : Nat) (l : List α), take n l ++ drop n l = l
@@ -391,6 +404,14 @@ theorem foldr_eq_foldrM (f : α → β → β) (b) (l : List α) :
 
 theorem foldr_self (l : List α) : l.foldr cons [] = l := by simp
 
+theorem foldl_map (f : β₁ → β₂) (g : α → β₂ → α) (l : List β₁) (init : α) :
+    (l.map f).foldl g init = l.foldl (fun x y => g x (f y)) init := by
+  induction l generalizing init <;> simp [*]
+
+theorem foldr_map (f : α₁ → α₂) (g : α₂ → β → β) (l : List α₁) (init : β) :
+    (l.map f).foldr g init = l.foldr (fun x y => g (f x) y) init := by
+  induction l generalizing init <;> simp [*]
+
 /-! ### mapM -/
 
 /-- Alternate (non-tail-recursive) form of mapM for proofs. -/

src/Init/Data/Nat/Basic.lean

@@ -137,6 +137,9 @@ instance : LawfulBEq Nat where
 @[simp] protected theorem zero_add : ∀ (n : Nat), 0 + n = n
   | 0   => rfl
   | n+1 => congrArg succ (Nat.zero_add n)
+instance : Std.LawfulIdentity (α := Nat) (· + ·) 0 where
+  left_id := Nat.zero_add
+  right_id := Nat.add_zero
 
 theorem succ_add : ∀ (n m : Nat), (succ n) + m = succ (n + m)
   | _, 0   => rfl
@@ -160,10 +163,12 @@ protected theorem add_comm : ∀ (n m : Nat), n + m = m + n
     have : succ (n + m) = succ (m + n) := by apply congrArg; apply Nat.add_comm
     rw [succ_add m n]
     apply this
+instance : Std.Commutative (α := Nat) (· + ·) := ⟨Nat.add_comm⟩
 
 protected theorem add_assoc : ∀ (n m k : Nat), (n + m) + k = n + (m + k)
   | _, _, 0      => rfl
   | n, m, succ k => congrArg succ (Nat.add_assoc n m k)
+instance : Std.Associative (α := Nat) (· + ·) := ⟨Nat.add_assoc⟩
 
 protected theorem add_left_comm (n m k : Nat) : n + (m + k) = m + (n + k) := by
   rw [← Nat.add_assoc, Nat.add_comm n m, Nat.add_assoc]
@@ -207,12 +212,16 @@ theorem succ_mul (n m : Nat) : (succ n) * m = (n * m) + m := by
 protected theorem mul_comm : ∀ (n m : Nat), n * m = m * n
   | n, 0      => (Nat.zero_mul n).symm ▸ (Nat.mul_zero n).symm ▸ rfl
   | n, succ m => (mul_succ n m).symm ▸ (succ_mul m n).symm ▸ (Nat.mul_comm n m).symm ▸ rfl
+instance : Std.Commutative (α := Nat) (· * ·) := ⟨Nat.mul_comm⟩
 
 @[simp] protected theorem mul_one : ∀ (n : Nat), n * 1 = n :=
   Nat.zero_add
 
 @[simp] protected theorem one_mul (n : Nat) : 1 * n = n :=
   Nat.mul_comm n 1 ▸ Nat.mul_one n
+instance : Std.LawfulIdentity (α := Nat) (· * ·) 1 where
+  left_id := Nat.one_mul
+  right_id := Nat.mul_one
 
 protected theorem left_distrib (n m k : Nat) : n * (m + k) = n * m + n * k := by
   induction n with
@@ -231,6 +240,7 @@ protected theorem add_mul (n m k : Nat) : (n + m) * k = n * k + m * k :=
 protected theorem mul_assoc : ∀ (n m k : Nat), (n * m) * k = n * (m * k)
   | n, m, 0      => rfl
   | n, m, succ k => by simp [mul_succ, Nat.mul_assoc n m k, Nat.left_distrib]
+instance : Std.Associative (α := Nat) (· * ·) := ⟨Nat.mul_assoc⟩
 
 protected theorem mul_left_comm (n m k : Nat) : n * (m * k) = m * (n * k) := by
   rw [← Nat.mul_assoc, Nat.mul_comm n m, Nat.mul_assoc]

src/Init/Data/Nat/Gcd.lean

@@ -54,9 +54,13 @@ theorem gcd_succ (x y : Nat) : gcd (succ x) y = gcd (y % succ x) (succ x) :=
     -- `simp [gcd_succ]` produces an invalid term unless `gcd_succ` is proved with `id rfl` instead
     rw [gcd_succ]
     exact gcd_zero_left _
+instance : Std.LawfulIdentity gcd 0 where
+  left_id := gcd_zero_left
+  right_id := gcd_zero_right
 
 @[simp] theorem gcd_self (n : Nat) : gcd n n = n := by
   cases n <;> simp [gcd_succ]
+instance : Std.IdempotentOp gcd := ⟨gcd_self⟩
 
 theorem gcd_rec (m n : Nat) : gcd m n = gcd (n % m) m :=
   match m with
@@ -97,6 +101,7 @@ theorem gcd_comm (m n : Nat) : gcd m n = gcd n m :=
   Nat.dvd_antisymm
     (dvd_gcd (gcd_dvd_right m n) (gcd_dvd_left m n))
     (dvd_gcd (gcd_dvd_right n m) (gcd_dvd_left n m))
+instance : Std.Commutative gcd := ⟨gcd_comm⟩
 
 theorem gcd_eq_left_iff_dvd : m ∣ n ↔ gcd m n = m :=
   ⟨fun h => by rw [gcd_rec, mod_eq_zero_of_dvd h, gcd_zero_left],

src/Init/Data/Nat/Lcm.lean

@@ -14,6 +14,7 @@ def lcm (m n : Nat) : Nat := m * n / gcd m n
 
 theorem lcm_comm (m n : Nat) : lcm m n = lcm n m := by
   rw [lcm, lcm, Nat.mul_comm n m, gcd_comm n m]
+instance : Std.Commutative lcm := ⟨lcm_comm⟩
 
 @[simp] theorem lcm_zero_left (m : Nat) : lcm 0 m = 0 := by simp [lcm]
 
@@ -22,11 +23,15 @@ theorem lcm_comm (m n : Nat) : lcm m n = lcm n m := by
 @[simp] theorem lcm_one_left (m : Nat) : lcm 1 m = m := by simp [lcm]
 
 @[simp] theorem lcm_one_right (m : Nat) : lcm m 1 = m := by simp [lcm]
+instance : Std.LawfulIdentity lcm 1 where
+  left_id := lcm_one_left
+  right_id := lcm_one_right
 
 @[simp] theorem lcm_self (m : Nat) : lcm m m = m := by
   match eq_zero_or_pos m with
   | .inl h => rw [h, lcm_zero_left]
   | .inr h => simp [lcm, Nat.mul_div_cancel _ h]
+instance : Std.IdempotentOp lcm := ⟨lcm_self⟩
 
 theorem dvd_lcm_left (m n : Nat) : m ∣ lcm m n :=
   ⟨n / gcd m n, by rw [← Nat.mul_div_assoc m (Nat.gcd_dvd_right m n)]; rfl⟩
@@ -54,6 +59,7 @@ Nat.dvd_antisymm
     (Nat.dvd_trans (dvd_lcm_left m n) (dvd_lcm_left (lcm m n) k))
     (lcm_dvd (Nat.dvd_trans (dvd_lcm_right m n) (dvd_lcm_left (lcm m n) k))
       (dvd_lcm_right (lcm m n) k)))
+instance : Std.Associative lcm := ⟨lcm_assoc⟩
 
 theorem lcm_ne_zero (hm : m ≠ 0) (hn : n ≠ 0) : lcm m n ≠ 0 := by
   intro h

src/Init/Data/Nat/Lemmas.lean

@@ -200,6 +200,7 @@ theorem succ_min_succ (x y) : min (succ x) (succ y) = succ (min x y) := by
   | inr h => rw [Nat.min_eq_right h, Nat.min_eq_right (Nat.succ_le_succ h)]
 
 @[simp] protected theorem min_self (a : Nat) : min a a = a := Nat.min_eq_left (Nat.le_refl _)
+instance : Std.IdempotentOp (α := Nat) min := ⟨Nat.min_self⟩
 
 @[simp] protected theorem zero_min (a) : min 0 a = 0 := Nat.min_eq_left (Nat.zero_le _)
 
@@ -210,6 +211,7 @@ protected theorem min_assoc : ∀ (a b c : Nat), min (min a b) c = min a (min b
   | _, 0, _ => by rw [Nat.zero_min, Nat.min_zero, Nat.zero_min]
   | _, _, 0 => by rw [Nat.min_zero, Nat.min_zero, Nat.min_zero]
   | _+1, _+1, _+1 => by simp only [Nat.succ_min_succ]; exact congrArg succ <| Nat.min_assoc ..
+instance : Std.Associative (α := Nat) min := ⟨Nat.min_assoc⟩
 
 protected theorem sub_sub_eq_min : ∀ (a b : Nat), a - (a - b) = min a b
   | 0, _ => by rw [Nat.zero_sub, Nat.zero_min]
@@ -249,16 +251,21 @@ protected theorem max_lt {a b c : Nat} : max a b < c ↔ a < c ∧ b < c := by
   rw [← Nat.succ_le, ← Nat.succ_max_succ a b]; exact Nat.max_le
 
 @[simp] protected theorem max_self (a : Nat) : max a a = a := Nat.max_eq_right (Nat.le_refl _)
+instance : Std.IdempotentOp (α := Nat) max := ⟨Nat.max_self⟩
 
 @[simp] protected theorem zero_max (a) : max 0 a = a := Nat.max_eq_right (Nat.zero_le _)
 
 @[simp] protected theorem max_zero (a) : max a 0 = a := Nat.max_eq_left (Nat.zero_le _)
+instance : Std.LawfulIdentity (α := Nat) max 0 where
+  left_id := Nat.zero_max
+  right_id := Nat.max_zero
 
 protected theorem max_assoc : ∀ (a b c : Nat), max (max a b) c = max a (max b c)
   | 0, _, _ => by rw [Nat.zero_max, Nat.zero_max]
   | _, 0, _ => by rw [Nat.zero_max, Nat.max_zero]
   | _, _, 0 => by rw [Nat.max_zero, Nat.max_zero]
   | _+1, _+1, _+1 => by simp only [Nat.succ_max_succ]; exact congrArg succ <| Nat.max_assoc ..
+instance : Std.Associative (α := Nat) max := ⟨Nat.max_assoc⟩
 
 protected theorem sub_add_eq_max (a b : Nat) : a - b + b = max a b := by
   match Nat.le_total a b with

src/Init/Data/Nat/MinMax.lean

@@ -17,6 +17,7 @@ protected theorem min_comm (a b : Nat) : min a b = min b a := by
   | .inl h => simp [Nat.min_def, h, Nat.le_of_lt, Nat.not_le_of_lt]
   | .inr (.inl h) => simp [Nat.min_def, h]
   | .inr (.inr h) => simp [Nat.min_def, h, Nat.le_of_lt, Nat.not_le_of_lt]
+instance : Std.Commutative (α := Nat) min := ⟨Nat.min_comm⟩
 
 protected theorem min_le_right (a b : Nat) : min a b ≤ b := by
   by_cases (a <= b) <;> simp [Nat.min_def, *]
@@ -47,6 +48,7 @@ protected theorem max_comm (a b : Nat) : max a b = max b a := by
   by_cases h₁ : a ≤ b <;> by_cases h₂ : b ≤ a <;> simp [h₁, h₂]
   · exact Nat.le_antisymm h₂ h₁
   · cases not_or_intro h₁ h₂ <| Nat.le_total ..
+instance : Std.Commutative (α := Nat) max := ⟨Nat.max_comm⟩
 
 protected theorem le_max_left ( a b : Nat) : a ≤ max a b := by
   by_cases (a <= b) <;> simp [Nat.max_def, *]

src/Init/Notation.lean

@@ -492,9 +492,12 @@ The attribute `@[deprecated]` on a declaration indicates that the declaration
 is discouraged for use in new code, and/or should be migrated away from in
 existing code. It may be removed in a future version of the library.
 
-`@[deprecated myBetterDef]` means that `myBetterDef` is the suggested replacement.
+* `@[deprecated myBetterDef]` means that `myBetterDef` is the suggested replacement.
+* `@[deprecated myBetterDef "use myBetterDef instead"]` allows customizing the deprecation message.
+* `@[deprecated (since := "2024-04-21")]` records when the deprecation was first applied.
 -/
-syntax (name := deprecated) "deprecated" (ppSpace ident)? : attr
+syntax (name := deprecated) "deprecated" (ppSpace ident)? (ppSpace str)?
+    (" (" &"since" " := " str ")")? : attr
 
 /--
 The `@[coe]` attribute on a function (which should also appear in a

src/Init/Prelude.lean

@@ -4335,8 +4335,13 @@ def addMacroScope (mainModule : Name) (n : Name) (scp : MacroScope) : Name :=
     Name.mkNum (Name.mkStr (Name.appendCore (Name.mkStr n "_@") mainModule) "_hyg") scp
 
 /--
-Append two names that may have macro scopes. The macro scopes in `b` are always erased.
-If `a` has macro scopes, then they are propagated to the result of `append a b`.
+Appends two names `a` and `b`, propagating macro scopes from `a` or `b`, if any, to the result.
+Panics if both `a` and `b` have macro scopes.
+
+This function is used for the `Append Name` instance.
+
+See also `Lean.Name.appendCore`, which appends names without any consideration for macro scopes.
+Also consider `Lean.Name.eraseMacroScopes` to erase macro scopes before appending, if appropriate.
 -/
 def Name.append (a b : Name) : Name :=
   match a.hasMacroScopes, b.hasMacroScopes with

src/Init/SimpLemmas.lean

@@ -103,18 +103,26 @@ end SimprocHelperLemmas
 
 @[simp] theorem and_true (p : Prop) : (p ∧ True) = p := propext ⟨(·.1), (⟨·, trivial⟩)⟩
 @[simp] theorem true_and (p : Prop) : (True ∧ p) = p := propext ⟨(·.2), (⟨trivial, ·⟩)⟩
+instance : Std.LawfulIdentity And True where
+  left_id := true_and
+  right_id := and_true
 @[simp] theorem and_false (p : Prop) : (p ∧ False) = False := eq_false (·.2)
 @[simp] theorem false_and (p : Prop) : (False ∧ p) = False := eq_false (·.1)
 @[simp] theorem and_self (p : Prop) : (p ∧ p) = p := propext ⟨(·.left), fun h => ⟨h, h⟩⟩
+instance : Std.IdempotentOp And := ⟨and_self⟩
 @[simp] theorem and_not_self : ¬(a ∧ ¬a) | ⟨ha, hn⟩ => absurd ha hn
 @[simp] theorem not_and_self : ¬(¬a ∧ a) := and_not_self ∘ And.symm
 @[simp] theorem and_imp : (a ∧ b → c) ↔ (a → b → c) := ⟨fun h ha hb => h ⟨ha, hb⟩, fun h ⟨ha, hb⟩ => h ha hb⟩
 @[simp] theorem not_and : ¬(a ∧ b) ↔ (a → ¬b) := and_imp
 @[simp] theorem or_self (p : Prop) : (p ∨ p) = p := propext ⟨fun | .inl h | .inr h => h, .inl⟩
+instance : Std.IdempotentOp Or := ⟨or_self⟩
 @[simp] theorem or_true (p : Prop) : (p ∨ True) = True := eq_true (.inr trivial)
 @[simp] theorem true_or (p : Prop) : (True ∨ p) = True := eq_true (.inl trivial)
 @[simp] theorem or_false (p : Prop) : (p ∨ False) = p := propext ⟨fun (.inl h) => h, .inl⟩
 @[simp] theorem false_or (p : Prop) : (False ∨ p) = p := propext ⟨fun (.inr h) => h, .inr⟩
+instance : Std.LawfulIdentity Or False where
+  left_id := false_or
+  right_id := or_false
 @[simp] theorem iff_self (p : Prop) : (p ↔ p) = True := eq_true .rfl
 @[simp] theorem iff_true (p : Prop) : (p ↔ True) = p := propext ⟨(·.2 trivial), fun h => ⟨fun _ => trivial, fun _ => h⟩⟩
 @[simp] theorem true_iff (p : Prop) : (True ↔ p) = p := propext ⟨(·.1 trivial), fun h => ⟨fun _ => h, fun _ => trivial⟩⟩
@@ -140,6 +148,7 @@ theorem and_congr_left (h : c → (a ↔ b)) : a ∧ c ↔ b ∧ c :=
 theorem and_assoc : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) :=
   Iff.intro (fun ⟨⟨ha, hb⟩, hc⟩ => ⟨ha, hb, hc⟩)
             (fun ⟨ha, hb, hc⟩ => ⟨⟨ha, hb⟩, hc⟩)
+instance : Std.Associative And := ⟨fun _ _ _ => propext and_assoc⟩
 
 @[simp] theorem and_self_left  : a ∧ (a ∧ b) ↔ a ∧ b := by rw [←propext and_assoc, and_self]
 @[simp] theorem and_self_right : (a ∧ b) ∧ b ↔ a ∧ b := by rw [ propext and_assoc, and_self]
@@ -167,6 +176,7 @@ theorem Or.imp_right (f : b → c) : a ∨ b → a ∨ c := .imp id f
 theorem or_assoc : (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) :=
   Iff.intro (.rec (.imp_right .inl) (.inr ∘ .inr))
             (.rec (.inl ∘ .inl) (.imp_left .inr))
+instance : Std.Associative Or := ⟨fun _ _ _ => propext or_assoc⟩
 
 @[simp] theorem or_self_left  : a ∨ (a ∨ b) ↔ a ∨ b := by rw [←propext or_assoc, or_self]
 @[simp] theorem or_self_right : (a ∨ b) ∨ b ↔ a ∨ b := by rw [ propext or_assoc, or_self]
@@ -187,8 +197,12 @@ theorem or_iff_left_of_imp  (hb : b → a) : (a ∨ b) ↔ a  := Iff.intro (Or.r
 @[simp] theorem Bool.or_false (b : Bool) : (b || false) = b  := by cases b <;> rfl
 @[simp] theorem Bool.or_true (b : Bool) : (b || true) = true := by cases b <;> rfl
 @[simp] theorem Bool.false_or (b : Bool) : (false || b) = b  := by cases b <;> rfl
+instance : Std.LawfulIdentity (· || ·) false where
+  left_id := Bool.false_or
+  right_id := Bool.or_false
 @[simp] theorem Bool.true_or (b : Bool) : (true || b) = true := by cases b <;> rfl
 @[simp] theorem Bool.or_self (b : Bool) : (b || b) = b       := by cases b <;> rfl
+instance : Std.IdempotentOp (· || ·) := ⟨Bool.or_self⟩
 @[simp] theorem Bool.or_eq_true (a b : Bool) : ((a || b) = true) = (a = true ∨ b = true) := by
   cases a <;> cases b <;> decide
 
@@ -196,14 +210,20 @@ theorem or_iff_left_of_imp  (hb : b → a) : (a ∨ b) ↔ a  := Iff.intro (Or.r
 @[simp] theorem Bool.and_true (b : Bool) : (b && true) = b       := by cases b <;> rfl
 @[simp] theorem Bool.false_and (b : Bool) : (false && b) = false := by cases b <;> rfl
 @[simp] theorem Bool.true_and (b : Bool) : (true && b) = b       := by cases b <;> rfl
+instance : Std.LawfulIdentity (· && ·) true where
+  left_id := Bool.true_and
+  right_id := Bool.and_true
 @[simp] theorem Bool.and_self (b : Bool) : (b && b) = b          := by cases b <;> rfl
+instance : Std.IdempotentOp (· && ·) := ⟨Bool.and_self⟩
 @[simp] theorem Bool.and_eq_true (a b : Bool) : ((a && b) = true) = (a = true ∧ b = true) := by
   cases a <;> cases b <;> decide
 
 theorem Bool.and_assoc (a b c : Bool) : (a && b && c) = (a && (b && c)) := by
   cases a <;> cases b <;> cases c <;> decide
+instance : Std.Associative (· && ·) := ⟨Bool.and_assoc⟩
 theorem Bool.or_assoc (a b c : Bool) : (a || b || c) = (a || (b || c)) := by
   cases a <;> cases b <;> cases c <;> decide
+instance : Std.Associative (· || ·) := ⟨Bool.or_assoc⟩
 
 @[simp] theorem Bool.not_not (b : Bool) : (!!b) = b := by cases b <;> rfl
 @[simp] theorem Bool.not_true  : (!true) = false := by decide

src/Init/Tactics.lean

@@ -1542,7 +1542,7 @@ macro "get_elem_tactic" : tactic =>
 
 /--
 Searches environment for definitions or theorems that can be substituted in
-for `exact?% to solve the goal.
+for `exact?%` to solve the goal.
  -/
 syntax (name := Lean.Parser.Syntax.exact?) "exact?%" : term
 

src/Lean/Attributes.lean

@@ -183,7 +183,6 @@ structure ParametricAttribute (α : Type) where
   deriving Inhabited
 
 structure ParametricAttributeImpl (α : Type) extends AttributeImplCore where
-  /-- This is used as the target for go-to-definition queries for simple attributes -/
   getParam : Name → Syntax → AttrM α
   afterSet : Name → α → AttrM Unit := fun _ _ _ => pure ()
   afterImport : Array (Array (Name × α)) → ImportM Unit := fun _ => pure ()

src/Lean/Elab/Print.lean

@@ -65,8 +65,36 @@ private def printInduct (id : Name) (levelParams : List Name) (numParams : Nat)
     m := m ++ Format.line ++ ctor ++ " : " ++ cinfo.type
   logInfo m
 
+open Meta in
+private def printStructure (id : Name) (levelParams : List Name) (numParams : Nat) (type : Expr)
+    (ctor : Name) (fields : Array Name) (isUnsafe : Bool) (isClass : Bool) : CommandElabM Unit := do
+  let kind := if isClass then "class" else "structure"
+  let mut m ← mkHeader' kind id levelParams type isUnsafe
+  m := m ++ Format.line ++ "number of parameters: " ++ toString numParams
+  m := m ++ Format.line ++ "constructor:"
+  let cinfo ← getConstInfo ctor
+  m := m ++ Format.line ++ ctor ++ " : " ++ cinfo.type
+  m := m ++ Format.line ++ "fields:" ++ (← doFields)
+  logInfo m
+where
+  doFields := liftTermElabM do
+    forallTelescope (← getConstInfo id).type fun params type =>
+      withLocalDeclD `self type fun self => do
+        let params := params.push self
+        let mut m : Format := ""
+        for field in fields do
+          match getProjFnForField? (← getEnv) id field with
+          | some proj =>
+            let field : Format := if isPrivateName proj then "private " ++ toString field else toString field
+            let cinfo ← getConstInfo proj
+            let ftype ← instantiateForall cinfo.type params
+            m := m ++ Format.line ++ field ++ " : " ++ (← ppExpr ftype) -- Why ppExpr here?
+          | none => panic! "missing structure field info"
+        return m
+
 private def printIdCore (id : Name) : CommandElabM Unit := do
-  match (← getEnv).find? id with
+  let env ← getEnv
+  match env.find? id with
   | ConstantInfo.axiomInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "axiom" id us t u
   | ConstantInfo.defnInfo  { levelParams := us, type := t, value := v, safety := s, .. } => printDefLike "def" id us t v s
   | ConstantInfo.thmInfo  { levelParams := us, type := t, value := v, .. } => printDefLike "theorem" id us t v
@@ -75,7 +103,11 @@ private def printIdCore (id : Name) : CommandElabM Unit := do
   | ConstantInfo.ctorInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "constructor" id us t u
   | ConstantInfo.recInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "recursor" id us t u
   | ConstantInfo.inductInfo { levelParams := us, numParams, type := t, ctors, isUnsafe := u, .. } =>
-    printInduct id us numParams t ctors u
+    match getStructureInfo? env id with
+    | some { fieldNames, .. } =>
+      let [ctor] := ctors | panic! "structures have only one constructor"
+      printStructure id us numParams t ctor fieldNames u (isClass env id)
+    | none => printInduct id us numParams t ctors u
   | none => throwUnknownId id
 
 private def printId (id : Syntax) : CommandElabM Unit := do

src/Lean/Elab/Tactic/LibrarySearch.lean

@@ -68,11 +68,8 @@ def elabExact?Term : TermElab := fun stx expectedType? => do
     let (_, introdGoal) ← goal.mvarId!.intros
     introdGoal.withContext do
       if let some suggestions ← librarySearch introdGoal then
-        reportOutOfHeartbeats `library_search stx
-        for suggestion in suggestions do
-          withMCtx suggestion.2 do
-            addTermSuggestion stx (← instantiateMVars goal).headBeta
-        if suggestions.isEmpty then logError "exact?# didn't find any relevant lemmas"
+        if suggestions.isEmpty then logError "`exact?%` didn't find any relevant lemmas"
+        else logError "`exact?%` could not close the goal. Try `by apply` to see partial suggestions."
         mkSorry expectedType (synthetic := true)
       else
         addTermSuggestion stx (← instantiateMVars goal).headBeta

src/Lean/Level.lean

@@ -428,15 +428,18 @@ def Result.imax : Result → Result → Result
   | f, Result.imaxNode Fs => Result.imaxNode (f::Fs)
   | f₁, f₂                => Result.imaxNode [f₁, f₂]
 
-def toResult : Level → Result
+def toResult (l : Level) (mvars : Bool) : Result :=
+  match l with
   | zero       => Result.num 0
-  | succ l     => Result.succ (toResult l)
-  | max l₁ l₂  => Result.max (toResult l₁) (toResult l₂)
-  | imax l₁ l₂ => Result.imax (toResult l₁) (toResult l₂)
+  | succ l     => Result.succ (toResult l mvars)
+  | max l₁ l₂  => Result.max (toResult l₁ mvars) (toResult l₂ mvars)
+  | imax l₁ l₂ => Result.imax (toResult l₁ mvars) (toResult l₂ mvars)
   | param n    => Result.leaf n
   | mvar n     =>
-    let n := n.name.replacePrefix `_uniq (Name.mkSimple "?u");
-    Result.leaf n
+    if mvars then
+      Result.leaf <| n.name.replacePrefix `_uniq (Name.mkSimple "?u")
+    else
+      Result.leaf `_
 
 private def parenIfFalse : Format → Bool → Format
   | f, true  => f
@@ -471,17 +474,17 @@ protected partial def Result.quote (r : Result) (prec : Nat) : Syntax.Level :=
 
 end PP
 
-protected def format (u : Level) : Format :=
-  (PP.toResult u).format true
+protected def format (u : Level) (mvars : Bool) : Format :=
+  (PP.toResult u mvars).format true
 
 instance : ToFormat Level where
-  format u := Level.format u
+  format u := Level.format u (mvars := true)
 
 instance : ToString Level where
-  toString u := Format.pretty (Level.format u)
+  toString u := Format.pretty (format u)
 
-protected def quote (u : Level) (prec : Nat := 0) : Syntax.Level :=
-  (PP.toResult u).quote prec
+protected def quote (u : Level) (prec : Nat := 0) (mvars : Bool := true) : Syntax.Level :=
+  (PP.toResult u (mvars := mvars)).quote prec
 
 instance : Quote Level `level where
   quote := Level.quote

src/Lean/Linter/Deprecated.lean

@@ -15,17 +15,23 @@ register_builtin_option linter.deprecated : Bool := {
   descr := "if true, generate deprecation warnings"
 }
 
-builtin_initialize deprecatedAttr : ParametricAttribute (Option Name) ←
+structure DeprecationEntry where
+  newName? : Option Name := none
+  text? : Option String := none
+  since? : Option String := none
+  deriving Inhabited
+
+builtin_initialize deprecatedAttr : ParametricAttribute DeprecationEntry ←
   registerParametricAttribute {
     name := `deprecated
     descr := "mark declaration as deprecated",
     getParam := fun _ stx => do
-     match stx with
-     | `(attr| deprecated $[$id?]?) =>
-       let some id := id? | return none
-       let declNameNew ← Elab.realizeGlobalConstNoOverloadWithInfo id
-       return some declNameNew
-     | _  => throwError "invalid `[deprecated]` attribute"
+      let `(attr| deprecated $[$id?]? $[$text?]? $[(since := $since?)]?) := stx
+        | throwError "invalid `[deprecated]` attribute"
+      let newName? ← id?.mapM Elab.realizeGlobalConstNoOverloadWithInfo
+      let text? := text?.map TSyntax.getString
+      let since? := since?.map TSyntax.getString
+      return { newName?, text?, since? }
   }
 
 def isDeprecated (env : Environment) (declName : Name) : Bool :=
@@ -34,12 +40,13 @@ def isDeprecated (env : Environment) (declName : Name) : Bool :=
 def _root_.Lean.MessageData.isDeprecationWarning (msg : MessageData) : Bool :=
   msg.hasTag (· == ``deprecatedAttr)
 
-def getDeprecatedNewName (env : Environment) (declName : Name) : Option Name :=
-  (deprecatedAttr.getParam? env declName).getD none
+def getDeprecatedNewName (env : Environment) (declName : Name) : Option Name := do
+  (← deprecatedAttr.getParam? env declName).newName?
 
 def checkDeprecated [Monad m] [MonadEnv m] [MonadLog m] [AddMessageContext m] [MonadOptions m] (declName : Name) : m Unit := do
   if getLinterValue linter.deprecated (← getOptions) then
-    match deprecatedAttr.getParam? (← getEnv) declName with
-    | none => pure ()
-    | some none => logWarning <| .tagged ``deprecatedAttr m!"`{declName}` has been deprecated"
-    | some (some newName) => logWarning <| .tagged ``deprecatedAttr m!"`{declName}` has been deprecated, use `{newName}` instead"
+    let some attr := deprecatedAttr.getParam? (← getEnv) declName | pure ()
+    logWarning <| .tagged ``deprecatedAttr <| attr.text?.getD <|
+      match attr.newName? with
+      | none => s!"`{declName}` has been deprecated"
+      | some newName => s!"`{declName}` has been deprecated, use `{newName}` instead"

src/Lean/Message.lean

@@ -120,7 +120,13 @@ def ofExpr (e : Expr) : MessageData :=
     hasSyntheticSorry := (instantiateMVarsCore · e |>.1.hasSyntheticSorry)
   }
 
-def ofLevel (l : Level) : MessageData := ofFormat (format l)
+def ofLevel (l : Level) : MessageData :=
+  .ofPPFormat {
+    pp := fun
+      | some ctx => ppLevel ctx l
+      | none => return format l
+  }
+
 def ofName (n : Name) : MessageData := ofFormat (format n)
 
 partial def hasSyntheticSorry (msg : MessageData) : Bool :=

src/Lean/Meta/Basic.lean

@@ -110,6 +110,14 @@ structure Config where
   trackZetaDelta     : Bool := false
   /-- Eta for structures configuration mode. -/
   etaStruct          : EtaStructMode := .all
+  /--
+  When `univApprox` is set to true,
+  we use approximations when solving postponed universe constraints.
+  Examples:
+  - `max u ?v =?= u` is solved with `?v := u` and ignoring the solution `?v := 0`.
+  - `max u w =?= mav u ?v` is solved with `?v := w` ignoring the solution `?v := max u w`
+  -/
+  univApprox : Bool := true
 
 /--
   Function parameter information cache.
@@ -300,6 +308,11 @@ structure Context where
     A predicate to control whether a constant can be unfolded or not at `whnf`.
     Note that we do not cache results at `whnf` when `canUnfold?` is not `none`. -/
   canUnfold?        : Option (Config → ConstantInfo → CoreM Bool) := none
+  /--
+  When `Config.univApprox := true`, this flag is set to `true` when there is no
+  progress processing universe constraints.
+  -/
+  univApprox        : Bool := false
 
 /--
 The `MetaM` monad is a core component of Lean's metaprogramming framework, facilitating the
@@ -1690,6 +1703,10 @@ partial def processPostponed (mayPostpone : Bool := true) (exceptionOnFailure :=
               return true
             else if numPostponed' < numPostponed then
               loop
+            -- If we cannot pospone anymore, `Config.univApprox := true`, but we haven't tried universe approximations yet,
+            -- then try approximations before failing.
+            else if !mayPostpone && (← getConfig).univApprox && !(← read).univApprox then
+              withReader (fun ctx => { ctx with univApprox := true }) loop
             else
               trace[Meta.isLevelDefEq.postponed] "no progress solving pending is-def-eq level constraints"
               return mayPostpone

src/Lean/Meta/ExprDefEq.lean

@@ -1757,10 +1757,21 @@ private def isDefEqDeltaStep (t s : Expr) : MetaM DeltaStepResult := do
     | .lt => unfold t (return .unknown) (k · s)
     | .gt => unfold s (return .unknown) (k t ·)
     | .eq =>
-      unfold t
-        (unfold s (return .unknown) (k t ·))
-        (fun t => unfold s (k t s) (k t ·))
+      -- Remark: if `t` and `s` are both some `f`-application, we use `tryHeuristic`
+      -- if `f` is not a projection. The projection case generates a performance regression.
+      if tInfo.name == sInfo.name && !(← isProjectionFn tInfo.name) then
+        if t.isApp && s.isApp && (← tryHeuristic t s) then
+          return .eq
+        else
+          unfoldBoth t s
+      else
+        unfoldBoth t s
 where
+  unfoldBoth (t s : Expr) : MetaM DeltaStepResult := do
+    unfold t
+      (unfold s (return .unknown) (k t ·))
+      (fun t => unfold s (k t s) (k t ·))
+
   k (t s : Expr) : MetaM DeltaStepResult := do
     let t ← whnfCore t
     let s ← whnfCore s

src/Lean/Meta/Instances.lean

@@ -114,7 +114,7 @@ For example:
 
 (The type of `inst` must not contain mvars.)
 -/
-partial def computeSynthOrder (inst : Expr) : MetaM (Array Nat) :=
+private partial def computeSynthOrder (inst : Expr) : MetaM (Array Nat) :=
   withReducible do
   let instTy ← inferType inst
 

src/Lean/Meta/LevelDefEq.lean

@@ -16,26 +16,62 @@ namespace Lean.Meta
   That is, `lvl` is a proper level subterm of some `u_i`. -/
 private def strictOccursMax (lvl : Level) : Level → Bool
   | Level.max u v => visit u || visit v
-  | _               => false
+  | _             => false
 where
   visit : Level → Bool
     | Level.max u v => visit u || visit v
-    | u               => u != lvl && lvl.occurs u
+    | u             => u != lvl && lvl.occurs u
 
 /-- `mkMaxArgsDiff mvarId (max u_1 ... (mvar mvarId) ... u_n) v` => `max v u_1 ... u_n` -/
 private def mkMaxArgsDiff (mvarId : LMVarId) : Level → Level → Level
   | Level.max u v,     acc => mkMaxArgsDiff mvarId v <| mkMaxArgsDiff mvarId u acc
   | l@(Level.mvar id), acc => if id != mvarId then mkLevelMax' acc l else acc
-  | l,                   acc => mkLevelMax' acc l
+  | l,                 acc => mkLevelMax' acc l
 
 /--
-  Solve `?m =?= max ?m v` by creating a fresh metavariable `?n`
-  and assigning `?m := max ?n v` -/
+Solves `?m =?= max ?m v` by creating a fresh metavariable `?n`
+and assigning `?m := max ?n v`
+-/
 private def solveSelfMax (mvarId : LMVarId) (v : Level) : MetaM Unit := do
   assert! v.isMax
   let n ← mkFreshLevelMVar
   assignLevelMVar mvarId <| mkMaxArgsDiff mvarId v n
 
+/--
+Returns true if `v` is `max u ?m` (or variant). That is, we solve `u =?= max u ?m` as `?m := u`.
+This is an approximation. For example, we ignore the solution `?m := 0`.
+-/
+-- TODO: investigate whether we need to improve this approximation.
+private def tryApproxSelfMax (u v : Level) : MetaM Bool := do
+  match v with
+  | .max v' (.mvar mvarId) => solve v' mvarId
+  | .max (.mvar mvarId) v' => solve v' mvarId
+  | _ => return false
+where
+  solve (v' : Level) (mvarId : LMVarId) : MetaM Bool := do
+    if u == v' then
+      assignLevelMVar mvarId u
+      return true
+    else
+      return false
+
+/--
+Returns true if `u` of the form `max u₁ u₂` and `v` of the form `max u₁ ?w` (or variant).
+That is, we solve `max u₁ u₂ =?= max u₁ ?v` as `?v := u₂`.
+This is an approximation. For example, we ignore the solution `?w := max u₁ u₂`.
+-/
+-- TODO: investigate whether we need to improve this approximation.
+private def tryApproxMaxMax (u v : Level) : MetaM Bool := do
+  match u, v with
+  | .max u₁ u₂, .max v' (.mvar mvarId) => solve u₁ u₂ v' mvarId
+  | .max u₁ u₂, .max (.mvar mvarId) v' => solve u₁ u₂ v' mvarId
+  | _, _ => return false
+where
+  solve (u₁ u₂ v' : Level) (mvarId : LMVarId) : MetaM Bool := do
+    if u₁ == v' then assignLevelMVar mvarId u₂; return true
+    else if u₂ == v' then assignLevelMVar mvarId u₁; return true
+    else return false
+
 private def postponeIsLevelDefEq (lhs : Level) (rhs : Level) : MetaM Unit := do
   let ref ← getRef
   let ctx ← read
@@ -82,7 +118,13 @@ mutual
         match (← Meta.decLevel? v) with
         | some v => Bool.toLBool <$> isLevelDefEqAux u v
         | none   => return LBool.undef
-    | _, _ => return LBool.undef
+    | _, _ =>
+      if (← read).univApprox then
+        if (← tryApproxSelfMax u v) then
+          return LBool.true
+        if (← tryApproxMaxMax u v) then
+          return LBool.true
+      return LBool.undef
 
   @[export lean_is_level_def_eq]
   partial def isLevelDefEqAuxImpl : Level → Level → MetaM Bool

src/Lean/Meta/SynthInstance.lean

@@ -41,6 +41,14 @@ structure GeneratorNode where
   mctx            : MetavarContext
   instances       : Array Instance
   currInstanceIdx : Nat
+  /--
+  `typeHasMVars := true` if type of `mvar` contains metavariables.
+  We store this information to implement an optimization that relies on the fact
+  that instances are "morally canonical."
+  That is, we need to find at most one answer for this generator node if the type
+  does not have metavariables.
+  -/
+  typeHasMVars    : Bool
   deriving Inhabited
 
 structure ConsumerNode where
@@ -56,8 +64,8 @@ inductive Waiter where
   | root         : Waiter
 
 def Waiter.isRoot : Waiter → Bool
-  | Waiter.consumerNode _ => false
-  | Waiter.root           => true
+  | .consumerNode _ => false
+  | .root           => true
 
 /-!
   In tabled resolution, we creating a mapping from goals (e.g., `Coe Nat ?x`) to
@@ -98,10 +106,10 @@ partial def normLevel (u : Level) : M Level := do
   if !u.hasMVar then
     return u
   else match u with
-    | Level.succ v      => return u.updateSucc! (← normLevel v)
-    | Level.max v w     => return u.updateMax! (← normLevel v) (← normLevel w)
-    | Level.imax v w    => return u.updateIMax! (← normLevel v) (← normLevel w)
-    | Level.mvar mvarId =>
+    | .succ v      => return u.updateSucc! (← normLevel v)
+    | .max v w     => return u.updateMax! (← normLevel v) (← normLevel w)
+    | .imax v w    => return u.updateIMax! (← normLevel v) (← normLevel w)
+    | .mvar mvarId =>
       if (← getMCtx).getLevelDepth mvarId != (← getMCtx).depth then
         return u
       else
@@ -118,15 +126,15 @@ partial def normExpr (e : Expr) : M Expr := do
   if !e.hasMVar then
     pure e
   else match e with
-    | Expr.const _ us      => return e.updateConst! (← us.mapM normLevel)
-    | Expr.sort u          => return e.updateSort! (← normLevel u)
-    | Expr.app f a         => return e.updateApp! (← normExpr f) (← normExpr a)
-    | Expr.letE _ t v b _  => return e.updateLet! (← normExpr t) (← normExpr v) (← normExpr b)
-    | Expr.forallE _ d b _ => return e.updateForallE! (← normExpr d) (← normExpr b)
-    | Expr.lam _ d b _     => return e.updateLambdaE! (← normExpr d) (← normExpr b)
-    | Expr.mdata _ b       => return e.updateMData! (← normExpr b)
-    | Expr.proj _ _ b      => return e.updateProj! (← normExpr b)
-    | Expr.mvar mvarId     =>
+    | .const _ us      => return e.updateConst! (← us.mapM normLevel)
+    | .sort u          => return e.updateSort! (← normLevel u)
+    | .app f a         => return e.updateApp! (← normExpr f) (← normExpr a)
+    | .letE _ t v b _  => return e.updateLet! (← normExpr t) (← normExpr v) (← normExpr b)
+    | .forallE _ d b _ => return e.updateForallE! (← normExpr d) (← normExpr b)
+    | .lam _ d b _     => return e.updateLambdaE! (← normExpr d) (← normExpr b)
+    | .mdata _ b       => return e.updateMData! (← normExpr b)
+    | .proj _ _ b      => return e.updateProj! (← normExpr b)
+    | .mvar mvarId     =>
       if !(← mvarId.isAssignable) then
         return e
       else
@@ -202,7 +210,7 @@ def getInstances (type : Expr) : MetaM (Array Instance) := do
       let result := result.insertionSort fun e₁ e₂ => e₁.priority < e₂.priority
       let erasedInstances ← getErasedInstances
       let mut result ← result.filterMapM fun e => match e.val with
-        | Expr.const constName us =>
+        | .const constName us =>
           if erasedInstances.contains constName then
             return none
           else
@@ -234,6 +242,7 @@ def mkGeneratorNode? (key mvar : Expr) : MetaM (Option GeneratorNode) := do
     let mctx ← getMCtx
     return some {
       mvar, key, mctx, instances
+      typeHasMVars := mvarType.hasMVar
       currInstanceIdx := instances.size
     }
 
@@ -351,7 +360,7 @@ def tryResolve (mvar : Expr) (inst : Instance) : MetaM (Option (MetavarContext
   let lctx       ← getLCtx
   let localInsts ← getLocalInstances
   forallTelescopeReducing mvarType fun xs mvarTypeBody => do
-    let ⟨subgoals, instVal, instTypeBody⟩ ← getSubgoals lctx localInsts xs inst
+    let { subgoals, instVal, instTypeBody } ← getSubgoals lctx localInsts xs inst
     withTraceNode `Meta.synthInstance.tryResolve (withMCtx (← getMCtx) do
         return m!"{exceptOptionEmoji ·} {← instantiateMVars mvarTypeBody} ≟ {← instantiateMVars instTypeBody}") do
     if (← isDefEq mvarTypeBody instTypeBody) then
@@ -373,7 +382,7 @@ def tryAnswer (mctx : MetavarContext) (mvar : Expr) (answer : Answer) : SynthM (
 
 /-- Move waiters that are waiting for the given answer to the resume stack. -/
 def wakeUp (answer : Answer) : Waiter → SynthM Unit
-  | Waiter.root               => do
+  | .root               => do
     /- Recall that we now use `ignoreLevelMVarDepth := true`. Thus, we should allow solutions
        containing universe metavariables, and not check `answer.result.paramNames.isEmpty`.
        We use `openAbstractMVarsResult` to construct the universe metavariables
@@ -383,7 +392,7 @@ def wakeUp (answer : Answer) : Waiter → SynthM Unit
     else
       let (_, _, answerExpr) ← openAbstractMVarsResult answer.result
       trace[Meta.synthInstance] "skip answer containing metavariables {answerExpr}"
-  | Waiter.consumerNode cNode =>
+  | .consumerNode cNode =>
     modify fun s => { s with resumeStack := s.resumeStack.push (cNode, answer) }
 
 def isNewAnswer (oldAnswers : Array Answer) (answer : Answer) : Bool :=
@@ -414,11 +423,11 @@ def addAnswer (cNode : ConsumerNode) : SynthM Unit := do
     let answer ← mkAnswer cNode
     -- Remark: `answer` does not contain assignable or assigned metavariables.
     let key := cNode.key
-    let entry ← getEntry key
-    if isNewAnswer entry.answers answer then
-      let newEntry := { entry with answers := entry.answers.push answer }
+    let { waiters, answers } ← getEntry key
+    if isNewAnswer answers answer then
+      let newEntry := { waiters, answers := answers.push answer }
       modify fun s => { s with tableEntries := s.tableEntries.insert key newEntry }
-      entry.waiters.forM (wakeUp answer)
+      waiters.forM (wakeUp answer)
 
 /--
   Return `true` if a type of the form `(a_1 : A_1) → ... → (a_n : A_n) → B` has an unused argument `a_i`.
@@ -426,7 +435,7 @@ def addAnswer (cNode : ConsumerNode) : SynthM Unit := do
   Remark: This is syntactic check and no reduction is performed.
 -/
 private def hasUnusedArguments : Expr → Bool
-  | Expr.forallE _ _ b _ => !b.hasLooseBVar 0 || hasUnusedArguments b
+  | .forallE _ _ b _ => !b.hasLooseBVar 0 || hasUnusedArguments b
   | _ => false
 
 /--
@@ -539,6 +548,17 @@ def generate : SynthM Unit := do
     let inst := gNode.instances.get! idx
     let mctx := gNode.mctx
     let mvar := gNode.mvar
+    /- See comment at `typeHasMVars` -/
+    unless gNode.typeHasMVars do
+      if let some entry := (← get).tableEntries.find? key then
+        unless entry.answers.isEmpty do
+          /-
+          We already have an answer for this node, and since its type does not have metavariables,
+          we can skip other solutions because we assume instances are "morally canonical".
+          We have added this optimization to address issue #3996.
+          -/
+          modify fun s => { s with generatorStack := s.generatorStack.pop }
+          return
     discard do withMCtx mctx do
       withTraceNode `Meta.synthInstance
         (return m!"{exceptOptionEmoji ·} apply {inst.val} to {← instantiateMVars (← inferType mvar)}") do
@@ -667,7 +687,7 @@ private partial def preprocessArgs (type : Expr) (i : Nat) (args : Array Expr) (
 private def preprocessOutParam (type : Expr) : MetaM Expr :=
   forallTelescope type fun xs typeBody => do
     match typeBody.getAppFn with
-    | c@(Expr.const declName _) =>
+    | c@(.const declName _) =>
       let env ← getEnv
       if let some outParamsPos := getOutParamPositions? env declName then
         unless outParamsPos.isEmpty do
@@ -690,7 +710,7 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
   withTraceNode `Meta.synthInstance
     (return m!"{exceptOptionEmoji ·} {← instantiateMVars type}") do
   withConfig (fun config => { config with isDefEqStuckEx := true, transparency := TransparencyMode.instances,
-                                          foApprox := true, ctxApprox := true, constApprox := false }) do
+                                          foApprox := true, ctxApprox := true, constApprox := false, univApprox := false }) do
     let localInsts ← getLocalInstances
     let type ← instantiateMVars type
     let type ← preprocess type
@@ -775,8 +795,7 @@ def synthInstance (type : Expr) (maxResultSize? : Option Nat := none) : MetaM Ex
 private def synthPendingImp (mvarId : MVarId) : MetaM Bool := withIncRecDepth <| mvarId.withContext do
   let mvarDecl ← mvarId.getDecl
   match mvarDecl.kind with
-  | MetavarKind.syntheticOpaque =>
-    return false
+  | .syntheticOpaque => return false
   | _ =>
     /- Check whether the type of the given metavariable is a class or not. If yes, then try to synthesize
        it using type class resolution. We only do it for `synthetic` and `natural` metavariables. -/

src/Lean/PrettyPrinter.lean

@@ -86,6 +86,7 @@ builtin_initialize
   ppFnsRef.set {
     ppExprWithInfos := fun ctx e => ctx.runMetaM <| withoutContext <| ppExprWithInfos e,
     ppTerm := fun ctx stx => ctx.runCoreM <| withoutContext <| ppTerm stx,
+    ppLevel := fun ctx l => return l.format (mvars := getPPMVars ctx.opts),
     ppGoal := fun ctx mvarId => ctx.runMetaM <| withoutContext <| Meta.ppGoal mvarId
   }
 

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -71,9 +71,11 @@ def delabSort : Delab := do
   match l with
   | Level.zero => `(Prop)
   | Level.succ .zero => `(Type)
-  | _ => match l.dec with
-    | some l' => `(Type $(Level.quote l' max_prec))
-    | none    => `(Sort $(Level.quote l max_prec))
+  | _ =>
+    let mvars ← getPPOption getPPMVars
+    match l.dec with
+    | some l' => `(Type $(Level.quote l' (prec := max_prec) (mvars := mvars)))
+    | none    => `(Sort $(Level.quote l (prec := max_prec) (mvars := mvars)))
 
 /--
 Delaborator for `const` expressions.
@@ -96,7 +98,8 @@ def delabConst : Delab := do
         c := c₀
     pure <| mkIdent c
   else
-    `($(mkIdent c).{$[$(ls.toArray.map quote)],*})
+    let mvars ← getPPOption getPPMVars
+    `($(mkIdent c).{$[$(ls.toArray.map (Level.quote · (prec := 0) (mvars := mvars)))],*})
 
   let stx ← maybeAddBlockImplicit stx
   if (← getPPOption getPPTagAppFns) then

src/Lean/PrettyPrinter/Delaborator/Options.lean

@@ -82,7 +82,8 @@ register_builtin_option pp.instantiateMVars : Bool := {
 register_builtin_option pp.mvars : Bool := {
   defValue := true
   group    := "pp"
-  descr    := "(pretty printer) display names of metavariables when true, and otherwise display them as '?_'"
+  descr    := "(pretty printer) display names of metavariables when true, \
+    and otherwise display them as '?_' (for expression metavariables) and as '_' (for universe level metavariables)"
 }
 register_builtin_option pp.mvars.withType : Bool := {
   defValue := false

src/Lean/ResolveName.lean

@@ -404,7 +404,7 @@ where
     for _ in [:revComponents.length] do
       match revComponents with
       | [] => return none
-      | cmpt::rest => candidate := cmpt ++ candidate; revComponents := rest
+      | cmpt::rest => candidate := Name.appendCore cmpt candidate; revComponents := rest
       match (← resolveGlobalName candidate) with
       | [(potentialMatch, _)] => if potentialMatch == n₀ then return some candidate else continue
       | _ => continue

src/Lean/Util/FindExpr.lean

@@ -11,17 +11,17 @@ namespace Lean
 namespace Expr
 namespace FindImpl
 
-unsafe abbrev FindM := StateT (PtrSet Expr) Id
+unsafe abbrev FindM (m) := StateT (PtrSet Expr) m
 
-@[inline] unsafe def checkVisited (e : Expr) : OptionT FindM Unit := do
+@[inline] unsafe def checkVisited [Monad m] (e : Expr) : OptionT (FindM m) Unit := do
   if (← get).contains e then
     failure
   modify fun s => s.insert e
 
-unsafe def findM? (p : Expr → Bool) (e : Expr) : OptionT FindM Expr :=
+unsafe def findM? [Monad m] (p : Expr → m Bool) (e : Expr) : OptionT (FindM m) Expr :=
   let rec visit (e : Expr) := do
     checkVisited e
-    if p e then
+    if ← p e then
       pure e
     else match e with
       | .forallE _ d b _ => visit d <|> visit b
@@ -33,29 +33,35 @@ unsafe def findM? (p : Expr → Bool) (e : Expr) : OptionT FindM Expr :=
       | _                => failure
   visit e
 
-unsafe def findUnsafe? (p : Expr → Bool) (e : Expr) : Option Expr :=
-  Id.run <| findM? p e |>.run' mkPtrSet
+unsafe def findUnsafeM? {m} [Monad m] (p : Expr → m Bool) (e : Expr) : m (Option Expr) :=
+  findM? p e |>.run' mkPtrSet
+
+@[inline] unsafe def findUnsafe? (p : Expr → Bool) (e : Expr) : Option Expr := findUnsafeM? (m := Id) p e
 
 end FindImpl
 
-@[implemented_by FindImpl.findUnsafe?]
-def find? (p : Expr → Bool) (e : Expr) : Option Expr :=
-  /- This is a reference implementation for the unsafe one above -/
-  if p e then
-    some e
+@[implemented_by FindImpl.findUnsafeM?]
+/- This is a reference implementation for the unsafe one above -/
+def findM? [Monad m] (p : Expr → m Bool) (e : Expr) : m (Option Expr) := do
+  if ← p e then
+    return some e
   else match e with
-    | .forallE _ d b _ => find? p d <|> find? p b
-    | .lam _ d b _     => find? p d <|> find? p b
-    | .mdata _ b       => find? p b
-    | .letE _ t v b _  => find? p t <|> find? p v <|> find? p b
-    | .app f a         => find? p f <|> find? p a
-    | .proj _ _ b      => find? p b
-    | _                => none
+    | .forallE _ d b _ => findM? p d <||> findM? p b
+    | .lam _ d b _     => findM? p d <||> findM? p b
+    | .mdata _ b       => findM? p b
+    | .letE _ t v b _  => findM? p t <||> findM? p v <||> findM? p b
+    | .app f a         => findM? p f <||> findM? p a
+    | .proj _ _ b      => findM? p b
+    | _                => pure none
+
+@[implemented_by FindImpl.findUnsafe?]
+def find? (p : Expr → Bool) (e : Expr) : Option Expr := findM? (m := Id) p e
 
 /-- Return true if `e` occurs in `t` -/
 def occurs (e : Expr) (t : Expr) : Bool :=
   (t.find? fun s => s == e).isSome
 
+
 /--
   Return type for `findExt?` function argument.
 -/
@@ -66,7 +72,7 @@ inductive FindStep where
 
 namespace FindExtImpl
 
-unsafe def findM? (p : Expr → FindStep) (e : Expr) : OptionT FindImpl.FindM Expr :=
+unsafe def findM? (p : Expr → FindStep) (e : Expr) : OptionT (FindImpl.FindM Id) Expr :=
   visit e
 where
   visitApp (e : Expr) :=

src/Lean/Util/PPExt.lean

@@ -49,6 +49,7 @@ instance : Coe Format FormatWithInfos where
 structure PPFns where
   ppExprWithInfos : PPContext → Expr → IO FormatWithInfos
   ppTerm : PPContext → Term → IO Format
+  ppLevel : PPContext → Level → IO Format
   ppGoal : PPContext → MVarId → IO Format
   deriving Inhabited
 
@@ -56,6 +57,7 @@ builtin_initialize ppFnsRef : IO.Ref PPFns ←
   IO.mkRef {
     ppExprWithInfos := fun _ e => return format (toString e)
     ppTerm := fun ctx stx => return stx.raw.formatStx (some <| pp.raw.maxDepth.get ctx.opts)
+    ppLevel := fun _ l => return format l
     ppGoal := fun _ _ => return "goal"
   }
 
@@ -88,7 +90,10 @@ def ppTerm (ctx : PPContext) (stx : Term) : IO Format :=
       else
         pure f!"failed to pretty print term (use 'set_option pp.rawOnError true' for raw representation)"
 
+def ppLevel (ctx : PPContext) (l : Level) : IO Format :=
+  ppExt.getState ctx.env |>.ppLevel ctx l
+
 def ppGoal (ctx : PPContext) (mvarId : MVarId) : IO Format :=
-    ppExt.getState ctx.env |>.ppGoal ctx mvarId
+  ppExt.getState ctx.env |>.ppGoal ctx mvarId
 
 end Lean

src/Lean/Util/TestExtern.lean

@@ -8,8 +8,9 @@ import Lean.Elab.SyntheticMVars
 import Lean.Elab.Command
 import Lean.Meta.Tactic.Unfold
 import Lean.Meta.Eval
+import Lean.Compiler.ImplementedByAttr
 
-open Lean Elab Meta Command Term
+open Lean Elab Meta Command Term Compiler
 
 syntax (name := testExternCmd) "test_extern " term : command
 
@@ -18,14 +19,15 @@ syntax (name := testExternCmd) "test_extern " term : command
     let t ← elabTermAndSynthesize t none
     match t.getAppFn with
     | .const f _ =>
-      if isExtern (← getEnv) f then
+      let env ← getEnv
+      if isExtern env f || (getImplementedBy? env f).isSome then
         let t' := (← unfold t f).expr
-        let r := mkApp (.const ``reduceBool []) (← mkAppM ``BEq.beq #[t, t'])
+        let r := mkApp (.const ``reduceBool []) (← mkDecide (← mkEq t t'))
         if ! (← evalExpr Bool (.const ``Bool []) r) then
           throwError
             ("native implementation did not agree with reference implementation!\n" ++
             m!"Compare the outputs of:\n#eval {t}\n and\n#eval {t'}")
       else
-        throwError "test_extern: {f} does not have an @[extern] attribute"
+        throwError "test_extern: {f} does not have an @[extern] attribute or @[implemented_by] attribute"
     | _ => throwError "test_extern: expects a function application"
   | _ => throwUnsupportedSyntax

src/Lean/Widget/InteractiveDiagnostic.lean

@@ -144,7 +144,9 @@ where
   | ctx,       compose d₁ d₂            => do let d₁ ← go nCtx ctx d₁; let d₂ ← go nCtx ctx d₂; pure $ d₁ ++ d₂
   | ctx,       group d                  => Format.group <$> go nCtx ctx d
   | ctx,       .trace data header children => do
-    let header := (← go nCtx ctx header).nest 4
+    let mut header := (← go nCtx ctx header).nest 4
+    if data.startTime != 0 then
+      header := f!"[{data.stopTime - data.startTime}] {header}"
     let nodes ←
       if data.collapsed && !children.isEmpty then
         let children := children.map fun child =>

src/lake/Lake/Load/Main.lean

@@ -174,6 +174,8 @@ def Workspace.updateAndMaterialize
         liftM (m := IO) <| throw e -- only ignore manifest on a bare `lake update`
       logWarning s!"{rootName}: ignoring previous manifest because it failed to load: {e}"
     resolveDepsAcyclic ws.root fun pkg resolve => do
+      if let some pkg := (← getThe Workspace).findPackage? pkg.name then
+        return pkg
       let inherited := pkg.name != ws.root.name
       -- Materialize this package's dependencies first
       let deps ← pkg.depConfigs.mapM fun dep => fetchOrCreate dep.name do
@@ -243,6 +245,8 @@ def Workspace.materializeDeps
   let rootPkg := ws.root
   let (root, ws) ← StateT.run (s := ws) <| StateT.run' (s := mkNameMap Package) do
     resolveDepsAcyclic rootPkg fun pkg resolve => do
+      if let some pkg := (← getThe Workspace).findPackage? pkg.name then
+        return pkg
       let topLevel := pkg.name = rootPkg.name
       let deps := pkg.depConfigs
       if topLevel then

src/lake/examples/deps/bar/lake-manifest.expected.json

@@ -0,0 +1,29 @@
+{"version": 7,
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"type": "path",
+   "name": "root",
+   "manifestFile": "lake-manifest.json",
+   "inherited": true,
+   "dir": "./../foo/../a/../root",
+   "configFile": "lakefile.lean"},
+  {"type": "path",
+   "name": "a",
+   "manifestFile": "lake-manifest.json",
+   "inherited": true,
+   "dir": "./../foo/../a",
+   "configFile": "lakefile.lean"},
+  {"type": "path",
+   "name": "b",
+   "manifestFile": "lake-manifest.json",
+   "inherited": true,
+   "dir": "./../foo/../b",
+   "configFile": "lakefile.lean"},
+  {"type": "path",
+   "name": "foo",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "./../foo",
+   "configFile": "lakefile.lean"}],
+ "name": "bar",
+ "lakeDir": ".lake"}

src/lake/examples/deps/test.sh

@@ -6,6 +6,11 @@ LAKE=${LAKE:-../../.lake/build/bin/lake}
 ./clean.sh
 
 $LAKE -d bar build --update
+# Test that the update produces the expected manifest.
+# Serves as a regression test to ensure that multiples of a package in
+# the dependency tree do not produce duplicate entries in the manifest.
+# https://github.com/leanprover/lean4/pull/3957
+diff --strip-trailing-cr bar/lake-manifest.expected.json bar/lake-manifest.json
 $LAKE -d foo build --update
 
 ./foo/.lake/build/bin/foo
@@ -29,6 +34,7 @@ test ! -d foo/.lake/build
 ./clean.sh
 
 $LAKE -d bar -f lakefile.toml build --update
+diff --strip-trailing-cr bar/lake-manifest.expected.json bar/lake-manifest.json
 $LAKE -d foo -f lakefile.toml build --update
 
 ./foo/.lake/build/bin/foo

tests/lean/343.lean

@@ -1,30 +0,0 @@
-structure CatIsh where
-  Obj : Type o
-  Hom : Obj → Obj → Type m
-
-infixr:75 " ~> " => (CatIsh.Hom _)
-
-structure FunctorIsh (C D : CatIsh) where
-  onObj : C.Obj → D.Obj
-  onHom : ∀ {s d : C.Obj}, (s ~> d) → (onObj s ~> onObj d)
-
-abbrev Catish : CatIsh :=
-  {
-    Obj := CatIsh
-    Hom := FunctorIsh
-  }
-
-universe m o
-unif_hint (mvar : CatIsh) where
-  Catish.{m, o} =?= mvar |- mvar.Obj =?= CatIsh.{o, m}
-
-structure CtxSyntaxLayerParamsObj where
-  Ct : CatIsh
-
-def CtxSyntaxLayerParams : CatIsh :=
-  {
-    Obj := CtxSyntaxLayerParamsObj
-    Hom := sorry
-  }
-
-def CtxSyntaxLayerTy := CtxSyntaxLayerParams ~> Catish

tests/lean/343.lean.expected.out

@@ -1,17 +0,0 @@
-343.lean:24:4-24:24: warning: declaration uses 'sorry'
-343.lean:30:0-30:54: error: stuck at solving universe constraint
-  max (?u+1) (?u+1) =?= max (?u+1) (?u+1)
-while trying to unify
-  CatIsh.Obj.{max (max (?u + 1) (?u + 1)) ?u ?u,
-      max ((max (?u + 1) (?u + 1)) + 1) ((max ?u ?u) + 1)}
-    Catish.{max (?u + 1) (?u + 1),
-      max ?u ?u} : Type (max ((max (?u + 1) (?u + 1)) + 1) ((max ?u ?u) + 1))
-with
-  CatIsh.{max ?u ?u,
-    max (?u + 1) (?u + 1)} : Type (max ((max ?u ?u) + 1) ((max (?u + 1) (?u + 1)) + 1))
-343.lean:30:0-30:54: error: failed to solve universe constraint
-  max (?u+1) (?u+1) =?= max (?u+1) (?u+1)
-while trying to unify
-  Catish.Obj : Type (max ((max (u_1 + 1) (u_2 + 1)) + 1) ((max u_3 u_4) + 1))
-with
-  CatIsh : Type (max ((max u_4 u_3) + 1) ((max (u_4 + 1) (u_3 + 1)) + 1))

tests/lean/456.lean

@@ -1 +0,0 @@
-def A : Sort u := { s : Prop // _ }

tests/lean/456.lean.expected.out

@@ -1,6 +0,0 @@
-456.lean:1:18-1:35: error: failed to solve universe constraint
-  u =?= max 1 ?u
-while trying to unify
-  Sort u : Type u
-with
-  Type : Type 1

tests/lean/deprecated.lean

@@ -17,14 +17,14 @@ def f1 (x : Nat) := x + 1
 
 def Foo.g1 := 10
 
-@[deprecated Foo.g1]
+@[deprecated Foo.g1 (since := "2022-07-24")]
 def f2 (x : Nat) := x + 1
 
 @[deprecated g1]
 def f3 (x : Nat) := x + 1
 
 open Foo
-@[deprecated g1]
+@[deprecated g1 "use g1 instead, f4 is not a good name"]
 def f4 (x : Nat) := x + 1
 
 #eval f2 0 + 1

tests/lean/deprecated.lean.expected.out

@@ -7,5 +7,5 @@ deprecated.lean:23:13-23:15: error: unknown constant 'g1'
 deprecated.lean:30:6-30:8: warning: `f2` has been deprecated, use `Foo.g1` instead
 2
 2
-deprecated.lean:33:6-33:8: warning: `f4` has been deprecated, use `Foo.g1` instead
+deprecated.lean:33:6-33:8: warning: use g1 instead, f4 is not a good name
 2

tests/lean/diamond1.lean.expected.out

@@ -2,10 +2,14 @@ diamond1.lean:11:40-11:45: error: parent field type mismatch, field 'a' from par
   α → α : Type
 but is expected to have type
   α : Type
-inductive Foo : Type → Type
+structure Foo : Type → Type
 number of parameters: 1
-constructors:
+constructor:
 Foo.mk : {α : Type} → Bar (α → α) → (Bool → α) → Nat → Foo α
+fields:
+toBar : Bar (α → α)
+c : Bool → α
+d : Nat
 def f : Nat → Foo Nat :=
 fun x => { a := fun y => x + y, b := fun x x_1 => x + x_1, c := fun x_1 => x, d := x }
 diamond1.lean:27:47-27:52: warning: field 'a' from 'Baz' has already been declared

tests/lean/diamond8.lean.expected.out

@@ -1,4 +1,7 @@
-inductive Semiring.{u} : Type u → Type u
+class Semiring.{u} : Type u → Type u
 number of parameters: 1
-constructors:
+constructor:
 Semiring.mk : {R : Type u} → [toAddCommMonoid : AddCommMonoid R] → [toMonoid : Monoid R] → Semiring R
+fields:
+toAddCommMonoid : AddCommMonoid R
+toMonoid : Monoid R

tests/lean/librarySearch.lean

@@ -43,6 +43,14 @@ example (_ha : a > 0) (w : b ∣ c) : a * b ∣ a * c := by apply?
 #guard_msgs in
 example : x < x + 1 := exact?%
 
+/-- error: `exact?%` didn't find any relevant lemmas -/
+#guard_msgs in
+example {α : Sort u} (x y : α) : Eq x y := exact?%
+
+/-- error: `exact?%` could not close the goal. Try `by apply` to see partial suggestions. -/
+#guard_msgs in
+example (x y : Nat) : x ≤ y := exact?%
+
 /-- info: Try this: exact p -/
 #guard_msgs in
 example (P : Prop) (p : P) : P := by apply?

tests/lean/printStructure.lean

@@ -0,0 +1,103 @@
+/-!
+  Test #print command for structures and classes
+-/
+
+/- Structure -/
+/--
+info: structure Prod.{u, v} : Type u → Type v → Type (max u v)
+number of parameters: 2
+constructor:
+Prod.mk : {α : Type u} → {β : Type v} → α → β → α × β
+fields:
+fst : α
+snd : β
+-/
+#guard_msgs in
+#print Prod
+
+/- Class -/
+/--
+info: class Inhabited.{u} : Sort u → Sort (max 1 u)
+number of parameters: 1
+constructor:
+Inhabited.mk : {α : Sort u} → α → Inhabited α
+fields:
+default : α
+-/
+#guard_msgs in
+#print Inhabited
+
+/- Structure with private field -/
+/--
+info: structure Thunk.{u} : Type u → Type u
+number of parameters: 1
+constructor:
+Thunk.mk : {α : Type u} → (Unit → α) → Thunk α
+fields:
+private fn : Unit → α
+-/
+#guard_msgs in
+#print Thunk
+
+/- Extended class -/
+/--
+info: class Alternative.{u, v} : (Type u → Type v) → Type (max (u + 1) v)
+number of parameters: 1
+constructor:
+Alternative.mk : {f : Type u → Type v} →
+  [toApplicative : Applicative f] → ({α : Type u} → f α) → ({α : Type u} → f α → (Unit → f α) → f α) → Alternative f
+fields:
+toApplicative : Applicative f
+failure : {α : Type u} → f α
+orElse : {α : Type u} → f α → (Unit → f α) → f α
+-/
+#guard_msgs in
+#print Alternative
+
+/- Multiply extended class -/
+/--
+info: class Applicative.{u, v} : (Type u → Type v) → Type (max (u + 1) v)
+number of parameters: 1
+constructor:
+Applicative.mk : {f : Type u → Type v} →
+  [toFunctor : Functor f] →
+    [toPure : Pure f] → [toSeq : Seq f] → [toSeqLeft : SeqLeft f] → [toSeqRight : SeqRight f] → Applicative f
+fields:
+toFunctor : Functor f
+toPure : Pure f
+toSeq : Seq f
+toSeqLeft : SeqLeft f
+toSeqRight : SeqRight f
+-/
+#guard_msgs in
+#print Applicative
+
+/- Structure with unused parameter -/
+
+structure Weird (α β : Type _) where
+  a : α
+
+/--
+info: structure Weird.{u_1, u_2} : Type u_1 → Type u_2 → Type u_1
+number of parameters: 2
+constructor:
+Weird.mk : {α : Type u_1} → {β : Type u_2} → α → Weird α β
+fields:
+a : α
+-/
+#guard_msgs in
+#print Weird
+
+/- Structure-like inductive -/
+
+inductive Fake (α : Type _) where
+  | mk : (x : α) → Fake α
+
+/--
+info: inductive Fake.{u_1} : Type u_1 → Type u_1
+number of parameters: 1
+constructors:
+Fake.mk : {α : Type u_1} → α → Fake α
+-/
+#guard_msgs in
+#print Fake

tests/lean/run/2291.lean

@@ -0,0 +1,8 @@
+/-!
+Issue #2291
+
+The following example would cause the pretty printer to panic.
+-/
+
+set_option trace.compiler.simp true in
+#eval [0]

tests/lean/run/343.lean

@@ -0,0 +1,51 @@
+set_option pp.mvars false
+
+structure CatIsh where
+  Obj : Type o
+  Hom : Obj → Obj → Type m
+
+infixr:75 " ~> " => (CatIsh.Hom _)
+
+structure FunctorIsh (C D : CatIsh) where
+  onObj : C.Obj → D.Obj
+  onHom : ∀ {s d : C.Obj}, (s ~> d) → (onObj s ~> onObj d)
+
+abbrev Catish : CatIsh :=
+  {
+    Obj := CatIsh
+    Hom := FunctorIsh
+  }
+
+universe m o
+unif_hint (mvar : CatIsh) where
+  Catish.{m, o} =?= mvar |- mvar.Obj =?= CatIsh.{o, m}
+
+structure CtxSyntaxLayerParamsObj where
+  Ct : CatIsh
+
+/-- warning: declaration uses 'sorry' -/
+#guard_msgs in
+def CtxSyntaxLayerParams : CatIsh :=
+  {
+    Obj := CtxSyntaxLayerParamsObj
+    Hom := sorry
+  }
+
+/--
+error: stuck at solving universe constraint
+  max (_+1) (_+1) =?= max (_+1) (_+1)
+while trying to unify
+  CatIsh.Obj.{max (max (_ + 1) (_ + 1)) _ _, max ((max (_ + 1) (_ + 1)) + 1) ((max _ _) + 1)}
+    Catish.{max (_ + 1) (_ + 1), max _ _} : Type (max ((max (_ + 1) (_ + 1)) + 1) ((max _ _) + 1))
+with
+  CatIsh.{max _ _, max (_ + 1) (_ + 1)} : Type (max ((max _ _) + 1) ((max (_ + 1) (_ + 1)) + 1))
+---
+error: failed to solve universe constraint
+  max (_+1) (_+1) =?= max (_+1) (_+1)
+while trying to unify
+  Catish.Obj : Type (max ((max (u_1 + 1) (u_2 + 1)) + 1) ((max u_3 u_4) + 1))
+with
+  CatIsh : Type (max ((max u_4 u_3) + 1) ((max (u_4 + 1) (u_3 + 1)) + 1))
+-/
+#guard_msgs in
+def CtxSyntaxLayerTy := CtxSyntaxLayerParams ~> Catish

tests/lean/run/3965.lean

@@ -0,0 +1,207 @@
+section Mathlib.Logic.Function.Iterate
+
+universe u v
+
+variable {α : Type u}
+
+/-- Iterate a function. -/
+def Nat.iterate {α : Sort u} (op : α → α) : Nat → α → α := sorry
+
+notation:max f "^["n"]" => Nat.iterate f n
+
+theorem Function.iterate_succ' (f : α → α) (n : Nat) : f^[n.succ] = f ∘ f^[n] := sorry
+
+end Mathlib.Logic.Function.Iterate
+
+section Mathlib.Data.Quot
+
+variable {α : Sort _}
+
+noncomputable def Quot.out {r : α → α → Prop} (q : Quot r) : α := sorry
+
+end Mathlib.Data.Quot
+
+section Mathlib.Init.Order.Defs
+
+universe u
+variable {α : Type u}
+
+section Preorder
+
+class Preorder (α : Type u) extends LE α, LT α where
+
+variable [Preorder α]
+
+theorem lt_of_lt_of_le : ∀ {a b c : α}, a < b → b ≤ c → a < c := sorry
+
+end Preorder
+
+variable [LE α]
+
+theorem le_total : ∀ a b : α, a ≤ b ∨ b ≤ a := sorry
+
+end Mathlib.Init.Order.Defs
+
+section Mathlib.Order.RelClasses
+
+universe u
+
+class IsWellOrder (α : Type u) (r : α → α → Prop) : Prop
+
+end Mathlib.Order.RelClasses
+
+section Mathlib.Order.SetNotation
+
+universe u v
+variable {α : Type u} {ι : Sort v}
+
+class SupSet (α : Type _) where
+
+def iSup [SupSet α] (s : ι → α) : α := sorry
+
+end Mathlib.Order.SetNotation
+
+section Mathlib.SetTheory.Ordinal.Basic
+
+noncomputable section
+
+universe u v w
+
+variable {α : Type u}
+
+structure WellOrder : Type (u + 1) where
+  α : Type u
+
+instance Ordinal.isEquivalent : Setoid WellOrder := sorry
+
+def Ordinal : Type (u + 1) := Quotient Ordinal.isEquivalent
+
+instance (o : Ordinal) : LT o.out.α := sorry
+
+namespace Ordinal
+
+def typein (r : α → α → Prop) [IsWellOrder α r] (a : α) : Ordinal := sorry
+
+instance partialOrder : Preorder Ordinal := sorry
+
+theorem typein_lt_self {o : Ordinal} (i : o.out.α) :
+    @typein _ (· < ·) sorry i < o := sorry
+
+instance : SupSet Ordinal := sorry
+
+end Ordinal
+
+end
+
+end Mathlib.SetTheory.Ordinal.Basic
+
+section Mathlib.SetTheory.Ordinal.Arithmetic
+
+noncomputable section
+
+universe u v w
+
+namespace Ordinal
+
+def sup {ι : Type u} (f : ι → Ordinal.{max u v}) : Ordinal.{max u v} :=
+  iSup f
+
+def lsub {ι} (f : ι → Ordinal) : Ordinal :=
+  sup f
+
+def blsub₂ (o₁ o₂ : Ordinal) (op : {a : Ordinal} → (a < o₁) → {b : Ordinal} → (b < o₂) → Ordinal) :
+    Ordinal :=
+  lsub (fun x : o₁.out.α × o₂.out.α => op (typein_lt_self x.1) (typein_lt_self x.2))
+
+theorem lt_blsub₂ {o₁ o₂ : Ordinal}
+    (op : {a : Ordinal} → (a < o₁) → {b : Ordinal} → (b < o₂) → Ordinal) {a b : Ordinal}
+    (ha : a < o₁) (hb : b < o₂) : op ha hb < blsub₂ o₁ o₂ op := sorry
+
+
+end Ordinal
+
+end
+
+end Mathlib.SetTheory.Ordinal.Arithmetic
+
+section Mathlib.SetTheory.Ordinal.FixedPoint
+
+noncomputable section
+
+universe u v
+
+namespace Ordinal
+
+section
+
+variable {ι : Type u} {f : ι → Ordinal.{max u v} → Ordinal.{max u v}}
+
+def nfpFamily (f : ι → Ordinal → Ordinal) (a : Ordinal) : Ordinal :=
+  sup (List.foldr f a)
+
+end
+
+section
+
+variable {f : Ordinal.{u} → Ordinal.{u}}
+
+def nfp (f : Ordinal → Ordinal) : Ordinal → Ordinal :=
+  nfpFamily fun _ : Unit => f
+
+theorem lt_nfp {a b} : a < nfp f b ↔ ∃ n, a < f^[n] b := sorry
+
+end
+
+end Ordinal
+
+end
+
+end Mathlib.SetTheory.Ordinal.FixedPoint
+
+section Mathlib.SetTheory.Ordinal.Principal
+
+universe u v w
+
+namespace Ordinal
+
+def Principal (op : Ordinal → Ordinal → Ordinal) (o : Ordinal) : Prop :=
+  ∀ ⦃a b⦄, a < o → b < o → op a b < o
+
+theorem principal_nfp_blsub₂ (op : Ordinal → Ordinal → Ordinal) (o : Ordinal) :
+    Principal op (nfp (fun o' => blsub₂.{u, u, u} o' o' (@fun a _ b _ => op a b)) o) :=
+  fun a b ha hb => by
+  rw [lt_nfp] at *
+  rcases ha with ⟨m, hm⟩
+  rcases hb with ⟨n, hn⟩
+  rcases le_total
+    ((fun o' => blsub₂.{u, u, u} o' o' (@fun a _ b _ => op a b))^[m] o)
+    ((fun o' => blsub₂.{u, u, u} o' o' (@fun a _ b _ => op a b))^[n] o) with h | h
+  · refine ⟨n+1, ?_⟩
+    rw [Function.iterate_succ']
+    -- after https://github.com/leanprover/lean4/pull/3965 this requires `lt_blsub₂.{u}` or we get
+    -- `stuck at solving universe constraint max u ?v =?= u`
+    -- Note that there are two solutions: 0 and u. Both of them work.
+    -- However, when `Meta.Config.univApprox := true`, we solve using `?v := u`
+    exact lt_blsub₂ (@fun a _ b _ => op a b) (lt_of_lt_of_le hm h) hn
+  · sorry
+
+-- Trying again with 0
+theorem principal_nfp_blsub₂' (op : Ordinal → Ordinal → Ordinal) (o : Ordinal) :
+    Principal op (nfp (fun o' => blsub₂.{u, u, u} o' o' (@fun a _ b _ => op a b)) o) :=
+  fun a b ha hb => by
+  rw [lt_nfp] at *
+  rcases ha with ⟨m, hm⟩
+  rcases hb with ⟨n, hn⟩
+  rcases le_total
+    ((fun o' => blsub₂.{u, u, u} o' o' (@fun a _ b _ => op a b))^[m] o)
+    ((fun o' => blsub₂.{u, u, u} o' o' (@fun a _ b _ => op a b))^[n] o) with h | h
+  · refine ⟨n+1, ?_⟩
+    rw [Function.iterate_succ']
+    -- universe 0 also works here
+    exact lt_blsub₂.{0} (@fun a _ b _ => op a b) (lt_of_lt_of_le hm h) hn
+  · sorry
+
+
+end Ordinal
+
+end Mathlib.SetTheory.Ordinal.Principal

tests/lean/run/3965_2.lean

@@ -0,0 +1,98 @@
+section Mathlib.Init.Order.Defs
+
+universe u
+
+variable {α : Type u}
+
+class PartialOrder (α : Type u) extends LE α, LT α where
+
+theorem le_antisymm [PartialOrder α] : ∀ {a b : α}, a ≤ b → b ≤ a → a = b := sorry
+
+end Mathlib.Init.Order.Defs
+
+section Mathlib.Init.Data.Nat.Lemmas
+
+namespace Nat
+
+instance : PartialOrder Nat where
+  le := Nat.le
+  lt := Nat.lt
+
+section Find
+
+variable {p : Nat → Prop}
+
+private def lbp (m n : Nat) : Prop :=
+  m = n + 1 ∧ ∀ k ≤ n, ¬p k
+
+variable [DecidablePred p] (H : ∃ n, p n)
+
+private def wf_lbp {p : Nat → Prop} (H : ∃ n, p n) : WellFounded (@lbp p) := sorry
+
+protected noncomputable def findX : { n // p n ∧ ∀ m < n, ¬p m } :=
+  @WellFounded.fix _ (fun k => (∀ n < k, ¬p n) → { n // p n ∧ ∀ m < n, ¬p m }) lbp (wf_lbp H)
+    sorry 0 sorry
+
+protected noncomputable def find {p : Nat → Prop} [DecidablePred p] (H : ∃ n, p n) : Nat :=
+  (Nat.findX H).1
+
+protected theorem find_spec : p (Nat.find H) := sorry
+
+protected theorem find_min' {m : Nat} (h : p m) : Nat.find H ≤ m := sorry
+
+end Find
+
+end Nat
+
+end Mathlib.Init.Data.Nat.Lemmas
+
+section Mathlib.Logic.Basic
+
+theorem Exists.fst {b : Prop} {p : b → Prop} : Exists p → b
+  | ⟨h, _⟩ => h
+
+end Mathlib.Logic.Basic
+
+section Mathlib.Order.Basic
+
+open Function
+
+def PartialOrder.lift {α β} [PartialOrder β] (f : α → β) : PartialOrder α where
+  le x y := f x ≤ f y
+  lt x y := f x < f y
+
+end Mathlib.Order.Basic
+
+section Mathlib.Data.Fin.Basic
+
+instance {n : Nat} : PartialOrder (Fin n) :=
+  PartialOrder.lift Fin.val
+
+end Mathlib.Data.Fin.Basic
+
+section Mathlib.Data.Fin.Tuple.Basic
+
+universe u v
+
+namespace Fin
+
+variable {n : Nat}
+
+def find : ∀ {n : Nat} (p : Fin n → Prop) [DecidablePred p], Option (Fin n)
+  | 0, _p, _ => none
+  | n + 1, p, _ => by
+    exact
+      Option.casesOn (@find n (fun i ↦ p (i.castLT sorry)) _)
+        (if _ : p (Fin.last n) then some (Fin.last n) else none) fun i ↦
+        some (i.castLT sorry)
+
+theorem nat_find_mem_find {p : Fin n → Prop} [DecidablePred p]
+    (h : ∃ i, ∃ hin : i < n, p ⟨i, hin⟩) :
+    (⟨Nat.find h, (Nat.find_spec h).fst⟩ : Fin n) ∈ find p := by
+  rcases hf : find p with f | f
+  · sorry
+  · exact Option.some_inj.2 (le_antisymm sorry (Nat.find_min' _ ⟨f.2, sorry⟩))
+
+end Fin
+
+end Mathlib.Data.Fin.Tuple.Basic

tests/lean/run/3996.lean

@@ -0,0 +1,43 @@
+namespace Ex1
+
+class A where
+
+class B (n : Nat) where
+
+class C where
+
+instance test [B 10000] [C] : A where
+
+instance Bsucc {n : Nat} [B n] : B n.succ where
+
+instance instB0 : B 0 where
+
+instance instB10000 : B 10000 where
+
+/--
+error: failed to synthesize
+  A
+-/
+#guard_msgs in
+#synth A -- should fail quickly
+
+end Ex1
+
+namespace Ex2
+
+class A where
+class B (n : Nat) where
+class C where
+
+instance test' [B 10] : A where
+instance test [B 0] [C] : A where
+instance foo {n : Nat} [B n.succ] : B n where
+instance instB (n : Nat) : B n where
+
+/--
+info: test'
+-/
+#guard_msgs in
+#synth A
+
+end Ex2

tests/lean/run/456.lean

@@ -0,0 +1,12 @@
+set_option pp.mvars false
+
+/--
+error: failed to solve universe constraint
+  u =?= max 1 _
+while trying to unify
+  Sort u : Type u
+with
+  Type : Type 1
+-/
+#guard_msgs in
+def A : Sort u := { s : Prop // _ }

tests/lean/run/ac_rfl.lean

@@ -1,65 +1,3 @@
-open Std
-
-instance : Associative (α := Nat) HAdd.hAdd := ⟨Nat.add_assoc⟩
-instance : Commutative (α := Nat) HAdd.hAdd := ⟨Nat.add_comm⟩
-instance : LawfulCommIdentity HAdd.hAdd 0 where right_id := Nat.add_zero
-
-instance : Associative (α := Nat) HMul.hMul := ⟨Nat.mul_assoc⟩
-instance : Commutative (α := Nat) HMul.hMul := ⟨Nat.mul_comm⟩
-instance : LawfulCommIdentity HMul.hMul 1 where right_id := Nat.mul_one
-
-@[simp] theorem succ_le_succ_iff {x y : Nat} : x.succ ≤ y.succ ↔ x ≤ y :=
-  ⟨Nat.le_of_succ_le_succ, Nat.succ_le_succ⟩
-
-@[simp] theorem add_le_add_right_iff {x y z : Nat} : x + z ≤ y + z ↔ x ≤ y := by
-  induction z <;> simp_all [← Nat.add_assoc]
-
-set_option linter.unusedVariables false in
-theorem le_ext : ∀ {x y : Nat} (h : ∀ z, z ≤ x ↔ z ≤ y), x = y
-  | 0, 0, _ => rfl
-  | x+1, y+1, h => congrArg (· + 1) <| le_ext fun z => have := h (z + 1); by simp at this; assumption
-  | 0, y+1, h => have := h 1; by clear h; simp_all
-  | x+1, 0, h => have := h 1; by simp at this
-
-theorem le_or_le : ∀ (a b : Nat), a ≤ b ∨ b ≤ a
-  | x+1, y+1 => by simp [le_or_le x y]
-  | 0, 0 | x+1, 0 | 0, y+1 => by simp
-
-theorem le_of_not_le {a b : Nat} (h : ¬ a ≤ b) : b ≤ a :=
-  match le_or_le a b with | .inl ab => (h ab).rec | .inr ba => ba
-
-@[simp] theorem le_max_iff {x y z : Nat} : x ≤ max y z ↔ x ≤ y ∨ x ≤ z := by
-  simp only [Nat.max_def]
-  split
-  · exact Iff.intro .inr fun | .inl xy => Nat.le_trans ‹_› ‹_› | .inr xz => ‹_›
-  · exact Iff.intro .inl fun | .inl xy => ‹_› | .inr xz => Nat.le_trans ‹_› (le_of_not_le ‹_›)
-
-theorem max_assoc (n m k : Nat) : max (max n m) k = max n (max m k) :=
-  le_ext (by simp [or_assoc])
-
-theorem max_comm (n m : Nat) : max n m = max m n :=
-  le_ext (by simp [or_comm])
-
-theorem max_idem (n : Nat) : max n n = n := le_ext (by simp)
-
-instance : Associative (α := Nat) max := ⟨max_assoc⟩
-instance : Commutative (α := Nat) max := ⟨max_comm⟩
-instance : IdempotentOp (α := Nat) max := ⟨max_idem⟩
-instance : LawfulCommIdentity max 0 where
-  right_id := Nat.max_zero
-
-instance : Associative And := ⟨λ _p _q _r => propext ⟨λ ⟨⟨hp, hq⟩, hr⟩ => ⟨hp, hq, hr⟩, λ ⟨hp, hq, hr⟩ => ⟨⟨hp, hq⟩, hr⟩⟩⟩
-instance : Commutative And := ⟨λ _p _q => propext ⟨λ ⟨hp, hq⟩ => ⟨hq, hp⟩, λ ⟨hq, hp⟩ => ⟨hp, hq⟩⟩⟩
-instance : IdempotentOp And := ⟨λ _p => propext ⟨λ ⟨hp, _⟩ => hp, λ hp => ⟨hp, hp⟩⟩⟩
-instance : LawfulCommIdentity And True where
-  right_id _p := propext ⟨λ ⟨hp, _⟩ => hp, λ hp => ⟨hp, True.intro⟩⟩
-
-instance : Associative Or := ⟨by simp [or_assoc]⟩
-instance : Commutative Or := ⟨λ_p _q => propext ⟨λ hpq => hpq.elim Or.inr Or.inl, λ hqp => hqp.elim Or.inr Or.inl⟩⟩
-instance : IdempotentOp Or := ⟨λ_p => propext ⟨λ hp => hp.elim id id, Or.inl⟩⟩
-instance : LawfulCommIdentity Or False where
-  right_id _p := propext ⟨λ hpf => hpf.elim id False.elim, Or.inl⟩
-
 example (x y z : Nat) : x + y + 0 + z = z + (x + y) := by ac_rfl
 
 example (x y z : Nat) : (x + y) * (0 + z) = (x + y) * z:= by ac_rfl
@@ -96,3 +34,5 @@ example (p q : Prop) : (p ∨ p ∨ q ∧ True) = (q ∨ p) := by
 
 -- Repro: missing withContext
 example : ∀ x : Nat, x = x := by intro x; ac_rfl
+
+example : [1, 2] ++ ([] ++ [2+4, 8] ++ [4]) = [1, 2] ++ [4+2, 8] ++ [4] := by ac_rfl

tests/lean/run/ppMVars.lean

@@ -1,3 +1,4 @@
+import Lean.Elab.BuiltinNotation
 /-!
 # Testing `pp.mvars`
 -/
@@ -9,6 +10,12 @@ Default values
 /-- info: ?a : Nat -/
 #guard_msgs in #check (?a : Nat)
 
+/-- info: ⊢ Sort ?u.1 -/
+#guard_msgs (info, drop all) in
+example : (by_elab do return .sort (.mvar (.mk (.num `_uniq 1)))) := by
+  trace_state
+  sorry
+
 /-!
 Turning off `pp.mvars`
 -/
@@ -21,6 +28,18 @@ set_option pp.mvars false
 /-- info: ?_ : Nat -/
 #guard_msgs in #check (_ : Nat)
 
+/-- info: ⊢ Sort _ -/
+#guard_msgs (info, drop all) in
+example : (by_elab do return .sort (.mvar (.mk (.num `_uniq 1)))) := by
+  trace_state
+  sorry
+
+/-- info: ⊢ Type _ -/
+#guard_msgs (info, drop all) in
+example : Type _ := by
+  trace_state
+  sorry
+
 end
 
 /-!

tests/lean/run/univCnstrApprox.lean

@@ -0,0 +1,20 @@
+universe u v
+
+-- This is a mock-up of the `HasLimitsOfSize` typeclass in mathlib4.
+class HLOS.{a,b} (C : Type b) where
+  P : Type a
+
+-- We only have an instance when there is a "universe inequality".
+instance HLOS_max : HLOS.{a} (Type max a b) := sorry
+
+-- In mathlib4 we currently make use of the following workaround:
+abbrev TypeMax := Type max u v
+
+instance (priority := high) HLOS_max' : HLOS.{a} (TypeMax.{a, b}) := sorry
+
+example : HLOS.{a} (TypeMax.{a, b}) := HLOS_max'.{a} -- Success
+example : HLOS.{a} (TypeMax.{a, b}) := inferInstance -- Success
+
+-- We solve the following examples using approximations
+example : Type max v u = TypeMax.{v} := rfl -- Previously failed with: `max u v =?= max v ?u`
+example : Type max v u = TypeMax.{u} := rfl -- Previously failed with: `max u v =?= max u ?u`

tests/lean/run/utf8英語.lean

@@ -1,7 +1,6 @@
 import Lean.Util.TestExtern
 
-instance : BEq ByteArray where
-  beq x y := x.data == y.data
+deriving instance DecidableEq for ByteArray
 
 test_extern String.toUTF8 ""
 test_extern String.toUTF8 "\x00"

tests/lean/structAutoBound.lean.expected.out

@@ -1,10 +1,16 @@
-inductive Foo.{v, u_1} : {α : Sort u_1} → (α → Type v) → Sort (max u_1 (v + 1))
+structure Foo.{v, u_1} : {α : Sort u_1} → (α → Type v) → Sort (max u_1 (v + 1))
 number of parameters: 2
-constructors:
+constructor:
 Foo.mk : {α : Sort u_1} → {β : α → Type v} → (a : α) → β a → Foo β
+fields:
+a : α
+b : β self.a
 structAutoBound.lean:9:15-9:16: error: a universe level named 'u' has already been declared
-inductive Boo.{u, v} : Type u → Type v → Type (max u v)
+structure Boo.{u, v} : Type u → Type v → Type (max u v)
 number of parameters: 2
-constructors:
+constructor:
 Boo.mk : {α : Type u} → {β : Type v} → α → β → Boo α β
+fields:
+a : α
+b : β
 structAutoBound.lean:18:0-20:7: error: unused universe parameter 'w'

tests/lean/test_extern.lean

@@ -1,9 +1,15 @@
 import Lean.Util.TestExtern
 
-instance : BEq ByteArray where
-  beq x y := x.data == y.data
+deriving instance DecidableEq for ByteArray
 
 test_extern Nat.add 12 37
 test_extern 4 + 5
 
 test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 1 ⟨#[4, 5, 6, 7, 8, 9, 10, 11, 12, 13]⟩ 0 6
+
+def f := 3
+
+@[implemented_by f]
+def g := 4
+
+test_extern g

tests/lean/test_extern.lean.expected.out

@@ -1 +1,3 @@
-test_extern.lean:7:0-7:17: error: test_extern: HAdd.hAdd does not have an @[extern] attribute
+test_extern.lean:6:0-6:17: error: test_extern: HAdd.hAdd does not have an @[extern] attribute or @[implemented_by] attribute
+test_extern.lean:15:0-15:13: error: native implementation did not agree with reference implementation!
+Compare the outputs of: #eval g  and #eval 4