chore: code convention

closes #2575

.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

.github/workflows/ci.yml

@@ -110,7 +110,7 @@ jobs:
               },*/
               {
                 "name": "macOS",
-                "os": "macos-latest",
+                "os": "macos-13",
                 "release": true,
                 "quick": false,
                 "shell": "bash -euxo pipefail {0}",
@@ -121,7 +121,7 @@ jobs:
               },
               {
                 "name": "macOS aarch64",
-                "os": "macos-latest",
+                "os": "macos-13",
                 "release": true,
                 "quick": false,
                 "cross": true,
@@ -277,18 +277,18 @@ jobs:
         uses: cachix/install-nix-action@v18
         with:
           install_url: https://releases.nixos.org/nix/nix-2.12.0/install
-        if: matrix.os == 'ubuntu-latest' && !matrix.cmultilib
+        if: runner.os == 'Linux' && !matrix.cmultilib
       - name: Install MSYS2
         uses: msys2/setup-msys2@v2
         with:
           msystem: clang64
           # `:p` means prefix with appropriate msystem prefix
           pacboy: "make python cmake:p clang:p ccache:p gmp:p git zip unzip diffutils binutils tree zstd:p tar"
-        if: matrix.os == 'windows-2022'
+        if: runner.os == 'Windows'
       - name: Install Brew Packages
         run: |
           brew install ccache tree zstd coreutils gmp
-        if: matrix.os == 'macos-latest'
+        if: runner.os == 'macOS'
       - name: Setup emsdk
         uses: mymindstorm/setup-emsdk@v12
         with:
@@ -312,13 +312,13 @@ jobs:
         run: |
           # open nix-shell once for initial setup
           true
-        if: matrix.os == 'ubuntu-latest'
+        if: runner.os == 'Linux'
       - name: Set up core dumps
         run: |
           mkdir -p $PWD/coredumps
           # store in current directory, for easy uploading together with binary
           echo $PWD/coredumps/%e.%p.%t | sudo tee /proc/sys/kernel/core_pattern
-        if: matrix.os == 'ubuntu-latest'
+        if: runner.os == 'Linux'
       - name: Build
         run: |
           mkdir build
@@ -423,7 +423,7 @@ jobs:
       - name: CCache stats
         run: ccache -s
       - name: Show stacktrace for coredumps
-        if: ${{ failure() && matrix.os == 'ubuntu-latest' }}
+        if: ${{ failure() && runner.os == 'Linux' }}
         run: |
           for c in coredumps/*; do
             progbin="$(file $c | sed "s/.*execfn: '\([^']*\)'.*/\1/")"
@@ -433,7 +433,7 @@ jobs:
       # shared libs
       #- name: Upload coredumps
       #  uses: actions/upload-artifact@v3
-      #  if: ${{ failure() && matrix.os == 'ubuntu-latest' }}
+      #  if: ${{ failure() && runner.os == 'Linux' }}
       #  with:
       #    name: coredumps-${{ matrix.name }}
       #    path: |

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/Classical.lean

@@ -15,6 +15,13 @@ namespace Classical
 noncomputable def indefiniteDescription {α : Sort u} (p : α → Prop) (h : ∃ x, p x) : {x // p x} :=
   choice <| let ⟨x, px⟩ := h; ⟨⟨x, px⟩⟩
 
+/--
+Given that there exists an element satisfying `p`, returns one such element.
+
+This is a straightforward consequence of, and equivalent to, `Classical.choice`.
+
+See also `choose_spec`, which asserts that the returned value has property `p`.
+-/
 noncomputable def choose {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : α :=
   (indefiniteDescription p h).val
 

src/Init/Control/Option.lean

@@ -10,7 +10,7 @@ import Init.Control.Except
 
 universe u v
 
-instance : ToBool (Option α) := ⟨Option.toBool⟩
+instance : ToBool (Option α) := ⟨Option.isSome⟩
 
 def OptionT (m : Type u → Type v) (α : Type u) : Type v :=
   m (Option α)

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/Data/Option/Basic.lean

@@ -21,15 +21,13 @@ def getM [Alternative m] : Option α → m α
 @[deprecated getM] def toMonad [Monad m] [Alternative m] : Option α → m α :=
   getM
 
-@[inline] def toBool : Option α → Bool
-  | some _ => true
-  | none   => false
-
 /-- Returns `true` on `some x` and `false` on `none`. -/
 @[inline] def isSome : Option α → Bool
   | some _ => true
   | none   => false
 
+@[deprecated isSome, inline] def toBool : Option α → Bool := isSome
+
 /-- Returns `true` on `none` and `false` on `some x`. -/
 @[inline] def isNone : Option α → Bool
   | some _ => false

src/Init/Data/Ord.lean

@@ -182,15 +182,13 @@ instance [Ord α] : Ord (Option α) where
 
 /-- The lexicographic order on pairs. -/
 def lexOrd [Ord α] [Ord β] : Ord (α × β) where
-  compare p1 p2 := match compare p1.1 p2.1 with
-    | .eq => compare p1.2 p2.2
-    | o   => o
+  compare := compareLex (compareOn (·.1)) (compareOn (·.2))
 
 def ltOfOrd [Ord α] : LT α where
-  lt a b := compare a b == Ordering.lt
+  lt a b := compare a b = Ordering.lt
 
 instance [Ord α] : DecidableRel (@LT.lt α ltOfOrd) :=
-  inferInstanceAs (DecidableRel (fun a b => compare a b == Ordering.lt))
+  inferInstanceAs (DecidableRel (fun a b => compare a b = Ordering.lt))
 
 def leOfOrd [Ord α] : LE α where
   le a b := (compare a b).isLE

src/Init/Data/String/Extra.lean

@@ -17,13 +17,69 @@ def toNat! (s : String) : Nat :=
   else
     panic! "Nat expected"
 
+def utf8DecodeChar? (a : ByteArray) (i : Nat) : Option Char := do
+  let c ← a[i]?
+  if c &&& 0x80 == 0 then
+    some ⟨c.toUInt32, .inl (Nat.lt_trans c.1.2 (by decide))⟩
+  else if c &&& 0xe0 == 0xc0 then
+    let c1 ← a[i+1]?
+    guard (c1 &&& 0xc0 == 0x80)
+    let r := ((c &&& 0x1f).toUInt32 <<< 6) ||| (c1 &&& 0x3f).toUInt32
+    guard (0x80 ≤ r)
+    -- TODO: Prove h from the definition of r once we have the necessary lemmas
+    if h : r < 0xd800 then some ⟨r, .inl h⟩ else none
+  else if c &&& 0xf0 == 0xe0 then
+    let c1 ← a[i+1]?
+    let c2 ← a[i+2]?
+    guard (c1 &&& 0xc0 == 0x80 && c2 &&& 0xc0 == 0x80)
+    let r :=
+      ((c &&& 0x0f).toUInt32 <<< 12) |||
+      ((c1 &&& 0x3f).toUInt32 <<< 6) |||
+      (c2 &&& 0x3f).toUInt32
+    guard (0x800 ≤ r)
+    -- TODO: Prove `r < 0x110000` from the definition of r once we have the necessary lemmas
+    if h : r < 0xd800 ∨ 0xdfff < r ∧ r < 0x110000 then some ⟨r, h⟩ else none
+  else if c &&& 0xf8 == 0xf0 then
+    let c1 ← a[i+1]?
+    let c2 ← a[i+2]?
+    let c3 ← a[i+3]?
+    guard (c1 &&& 0xc0 == 0x80 && c2 &&& 0xc0 == 0x80 && c3 &&& 0xc0 == 0x80)
+    let r :=
+      ((c &&& 0x07).toUInt32 <<< 18) |||
+      ((c1 &&& 0x3f).toUInt32 <<< 12) |||
+      ((c2 &&& 0x3f).toUInt32 <<< 6) |||
+      (c3 &&& 0x3f).toUInt32
+    if h : 0x10000 ≤ r ∧ r < 0x110000 then
+      some ⟨r, .inr ⟨Nat.lt_of_lt_of_le (by decide) h.1, h.2⟩⟩
+    else none
+  else
+    none
+
 /-- Returns true if the given byte array consists of valid UTF-8. -/
 @[extern "lean_string_validate_utf8"]
-opaque validateUTF8 (a : @& ByteArray) : Bool
+def validateUTF8 (a : @& ByteArray) : Bool :=
+  (loop 0).isSome
+where
+  loop (i : Nat) : Option Unit := do
+    if i < a.size then
+      let c ← utf8DecodeChar? a i
+      loop (i + csize c)
+    else pure ()
+  termination_by a.size - i
+  decreasing_by exact Nat.sub_lt_sub_left ‹_› (Nat.lt_add_of_pos_right (one_le_csize c))
 
 /-- Converts a [UTF-8](https://en.wikipedia.org/wiki/UTF-8) encoded `ByteArray` string to `String`. -/
 @[extern "lean_string_from_utf8"]
-opaque fromUTF8 (a : @& ByteArray) (h : validateUTF8 a) : String
+def fromUTF8 (a : @& ByteArray) (h : validateUTF8 a) : String :=
+  loop 0 ""
+where
+  loop (i : Nat) (acc : String) : String :=
+    if i < a.size then
+      let c := (utf8DecodeChar? a i).getD default
+      loop (i + csize c) (acc.push c)
+    else acc
+  termination_by a.size - i
+  decreasing_by exact Nat.sub_lt_sub_left ‹_› (Nat.lt_add_of_pos_right (one_le_csize c))
 
 /-- Converts a [UTF-8](https://en.wikipedia.org/wiki/UTF-8) encoded `ByteArray` string to `String`,
 or returns `none` if `a` is not properly UTF-8 encoded. -/
@@ -35,13 +91,42 @@ or panics if `a` is not properly UTF-8 encoded. -/
 @[inline] def fromUTF8! (a : ByteArray) : String :=
   if h : validateUTF8 a then fromUTF8 a h else panic! "invalid UTF-8 string"
 
+def utf8EncodeChar (c : Char) : List UInt8 :=
+  let v := c.val
+  if v ≤ 0x7f then
+    [v.toUInt8]
+  else if v ≤ 0x7ff then
+    [(v >>>  6).toUInt8 &&& 0x1f ||| 0xc0,
+              v.toUInt8 &&& 0x3f ||| 0x80]
+  else if v ≤ 0xffff then
+    [(v >>> 12).toUInt8 &&& 0x0f ||| 0xe0,
+     (v >>>  6).toUInt8 &&& 0x3f ||| 0x80,
+              v.toUInt8 &&& 0x3f ||| 0x80]
+  else
+    [(v >>> 18).toUInt8 &&& 0x07 ||| 0xf0,
+     (v >>> 12).toUInt8 &&& 0x3f ||| 0x80,
+     (v >>>  6).toUInt8 &&& 0x3f ||| 0x80,
+              v.toUInt8 &&& 0x3f ||| 0x80]
+
+@[simp] theorem length_utf8EncodeChar (c : Char) : (utf8EncodeChar c).length = csize c := by
+  simp [csize, utf8EncodeChar, Char.utf8Size]
+  cases Decidable.em (c.val ≤ 0x7f) <;> simp [*]
+  cases Decidable.em (c.val ≤ 0x7ff) <;> simp [*]
+  cases Decidable.em (c.val ≤ 0xffff) <;> simp [*]
+
 /-- Converts the given `String` to a [UTF-8](https://en.wikipedia.org/wiki/UTF-8) encoded byte array. -/
 @[extern "lean_string_to_utf8"]
-opaque toUTF8 (a : @& String) : ByteArray
+def toUTF8 (a : @& String) : ByteArray :=
+  ⟨⟨a.data.bind utf8EncodeChar⟩⟩
+
+@[simp] theorem size_toUTF8 (s : String) : s.toUTF8.size = s.utf8ByteSize := by
+  simp [toUTF8, ByteArray.size, Array.size, utf8ByteSize, List.bind]
+  induction s.data <;> simp [List.map, List.join, utf8ByteSize.go, Nat.add_comm, *]
 
 /-- Accesses a byte in the UTF-8 encoding of the `String`. O(1) -/
 @[extern "lean_string_get_byte_fast"]
-opaque getUtf8Byte (s : @& String) (n : Nat) (h : n < s.utf8ByteSize) : UInt8
+def getUtf8Byte (s : @& String) (n : Nat) (h : n < s.utf8ByteSize) : UInt8 :=
+  (toUTF8 s).get ⟨n, size_toUTF8 _ ▸ h⟩
 
 theorem Iterator.sizeOf_next_lt_of_hasNext (i : String.Iterator) (h : i.hasNext) : sizeOf i.next < sizeOf i := by
   cases i; rename_i s pos; simp [Iterator.next, Iterator.sizeOf_eq]; simp [Iterator.hasNext] at h

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

@@ -1125,11 +1125,14 @@ normalizes `h` with `norm_cast` and tries to use that to close the goal. -/
 macro "assumption_mod_cast" : tactic => `(tactic| norm_cast0 at * <;> assumption)
 
 /--
-The `norm_cast` family of tactics is used to normalize casts inside expressions.
-It is basically a `simp` tactic with a specific set of lemmas to move casts
+The `norm_cast` family of tactics is used to normalize certain coercions (*casts*) in expressions.
+- `norm_cast` normalizes casts in the target.
+- `norm_cast at h` normalizes casts in hypothesis `h`.
+
+The tactic is basically a version of `simp` with a specific set of lemmas to move casts
 upwards in the expression.
 Therefore even in situations where non-terminal `simp` calls are discouraged (because of fragility),
-`norm_cast` is considered safe.
+`norm_cast` is considered to be safe.
 It also has special handling of numerals.
 
 For instance, given an assumption
@@ -1137,22 +1140,22 @@ For instance, given an assumption
 a b : ℤ
 h : ↑a + ↑b < (10 : ℚ)
 ```
-
 writing `norm_cast at h` will turn `h` into
 ```lean
 h : a + b < 10
 ```
 
-There are also variants of `exact`, `apply`, `rw`, and `assumption` that
-work modulo `norm_cast` - in other words, they apply `norm_cast` to make
-them more flexible. They are called `exact_mod_cast`, `apply_mod_cast`,
-`rw_mod_cast`, and `assumption_mod_cast`, respectively.
-Writing `exact_mod_cast h` and `apply_mod_cast h` will normalize casts
-in the goal and `h` before using `exact h` or `apply h`.
-Writing `assumption_mod_cast` will normalize casts in the goal and, for
-every hypothesis `h` in the context, it will try to normalize casts in `h` and use
-`exact h`.
-`rw_mod_cast` acts like the `rw` tactic but it applies `norm_cast` between steps.
+There are also variants of basic tactics that use `norm_cast` to normalize expressions during
+their operation, to make them more flexible about the expressions they accept
+(we say that it is a tactic *modulo* the effects of `norm_cast`):
+- `exact_mod_cast` for `exact` and `apply_mod_cast` for `apply`.
+  Writing `exact_mod_cast h` and `apply_mod_cast h` will normalize casts
+  in the goal and `h` before using `exact h` or `apply h`.
+- `rw_mod_cast` for `rw`. It applies `norm_cast` between rewrites.
+- `assumption_mod_cast` for `assumption`.
+  This is effectively `norm_cast at *; assumption`, but more efficient.
+  It normalizes casts in the goal and, for every hypothesis `h` in the context,
+  it will try to normalize casts in `h` and use `exact h`.
 
 See also `push_cast`, which moves casts inwards rather than lifting them outwards.
 -/
@@ -1160,22 +1163,37 @@ macro "norm_cast" loc:(location)? : tactic =>
   `(tactic| norm_cast0 $[$loc]? <;> try trivial)
 
 /--
-`push_cast` rewrites the goal to move casts inward, toward the leaf nodes.
+`push_cast` rewrites the goal to move certain coercions (*casts*) inward, toward the leaf nodes.
 This uses `norm_cast` lemmas in the forward direction.
 For example, `↑(a + b)` will be written to `↑a + ↑b`.
-It is equivalent to `simp only with push_cast`.
-It can also be used at hypotheses with `push_cast at h`
-and with extra simp lemmas with `push_cast [int.add_zero]`.
+- `push_cast` moves casts inward in the goal.
+- `push_cast at h` moves casts inward in the hypothesis `h`.
+It can be used with extra simp lemmas with, for example, `push_cast [Int.add_zero]`.
 
+Example:
 ```lean
-example (a b : ℕ) (h1 : ((a + b : ℕ) : ℤ) = 10) (h2 : ((a + b + 0 : ℕ) : ℤ) = 10) :
-  ((a + b : ℕ) : ℤ) = 10 :=
-begin
-  push_cast,
-  push_cast at h1,
-  push_cast [int.add_zero] at h2,
-end
+example (a b : Nat)
+    (h1 : ((a + b : Nat) : Int) = 10)
+    (h2 : ((a + b + 0 : Nat) : Int) = 10) :
+    ((a + b : Nat) : Int) = 10 := by
+  /-
+  h1 : ↑(a + b) = 10
+  h2 : ↑(a + b + 0) = 10
+  ⊢ ↑(a + b) = 10
+  -/
+  push_cast
+  /- Now
+  ⊢ ↑a + ↑b = 10
+  -/
+  push_cast at h1
+  push_cast [Int.add_zero] at h2
+  /- Now
+  h1 h2 : ↑a + ↑b = 10
+  -/
+  exact h1
 ```
+
+See also `norm_cast`.
 -/
 syntax (name := pushCast) "push_cast" (config)? (discharger)? (&" only")?
   (" [" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic
@@ -1524,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/Data/Parsec.lean

@@ -43,11 +43,19 @@ def fail (msg : String) : Parsec α := fun it =>
   error it msg
 
 @[inline]
-def orElse (p : Parsec α) (q : Unit → Parsec α) : Parsec α := fun it =>
+def tryCatch (p : Parsec α)
+    (csuccess : α → Parsec β)
+    (cerror : Unit → Parsec β)
+    : Parsec β := fun it =>
   match p it with
-  | success rem a => success rem a
-  | error rem err =>
-    if it = rem then q () it else error rem err
+  | .success rem a => csuccess a rem
+  | .error rem err =>
+    -- We assume that it.s never changes as the `Parsec` monad only modifies `it.pos`.
+    if it.pos = rem.pos then cerror () rem else .error rem err
+
+@[inline]
+def orElse (p : Parsec α) (q : Unit → Parsec α) : Parsec α :=
+  tryCatch p pure q
 
 @[inline]
 def attempt (p : Parsec α) : Parsec α := λ it =>
@@ -74,8 +82,7 @@ def eof : Parsec Unit := fun it =>
 
 @[specialize]
 partial def manyCore (p : Parsec α) (acc : Array α) : Parsec $ Array α :=
-  (do manyCore p (acc.push $ ←p))
-  <|> pure acc
+  tryCatch p (manyCore p <| acc.push ·) (fun _ => pure acc)
 
 @[inline]
 def many (p : Parsec α) : Parsec $ Array α := manyCore p #[]
@@ -85,8 +92,7 @@ def many1 (p : Parsec α) : Parsec $ Array α := do manyCore p #[←p]
 
 @[specialize]
 partial def manyCharsCore (p : Parsec Char) (acc : String) : Parsec String :=
-  (do manyCharsCore p (acc.push $ ←p))
-  <|> pure acc
+  tryCatch p (manyCharsCore p <| acc.push ·) (fun _ => pure acc)
 
 @[inline]
 def manyChars (p : Parsec Char) : Parsec String := manyCharsCore p ""

src/Lean/Data/Position.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
 import Lean.Data.Format
+import Lean.Data.Json
 import Lean.ToExpr
 
 namespace Lean
@@ -12,7 +13,7 @@ namespace Lean
 structure Position where
   line   : Nat
   column : Nat
-  deriving Inhabited, DecidableEq, Repr
+  deriving Inhabited, DecidableEq, Repr, ToJson, FromJson
 
 namespace Position
 protected def lt : Position → Position → Bool

src/Lean/Elab/Frontend.lean

@@ -109,6 +109,7 @@ def runFrontend
     (mainModuleName : Name)
     (trustLevel : UInt32 := 0)
     (ileanFileName? : Option String := none)
+    (jsonOutput : Bool := false)
     : IO (Environment × Bool) := do
   let startTime := (← IO.monoNanosNow).toFloat / 1000000000
   let inputCtx := Parser.mkInputContext input fileName
@@ -129,8 +130,7 @@ def runFrontend
       commandState := { commandState with infoState.enabled := true }
 
     let s ← IO.processCommands inputCtx parserState commandState
-    for msg in s.commandState.messages.toList do
-      IO.print (← msg.toString (includeEndPos := Language.printMessageEndPos.get opts))
+    Language.reportMessages s.commandState.messages opts jsonOutput
 
     if let some ileanFileName := ileanFileName? then
       let trees := s.commandState.infoState.trees.toArray
@@ -158,7 +158,7 @@ def runFrontend
   let processor := Language.Lean.process
   let snap ← processor none ctx
   let snaps := Language.toSnapshotTree snap
-  snaps.runAndReport opts
+  snaps.runAndReport opts jsonOutput
   if let some ileanFileName := ileanFileName? then
     let trees := snaps.getAll.concatMap (match ·.infoTree? with | some t => #[t] | _ => #[])
     let references := Lean.Server.findModuleRefs inputCtx.fileMap trees (localVars := false)

src/Lean/Elab/Inductive.lean

@@ -25,6 +25,11 @@ open Meta
 builtin_initialize
   registerTraceClass `Elab.inductive
 
+register_builtin_option inductive.autoPromoteIndices : Bool := {
+    defValue := true
+    descr    := "Promote indices to parameters in inductive types whenever possible."
+  }
+
 def checkValidInductiveModifier [Monad m] [MonadError m] (modifiers : Modifiers) : m Unit := do
   if modifiers.isNoncomputable then
     throwError "invalid use of 'noncomputable' in inductive declaration"
@@ -714,10 +719,12 @@ private def isDomainDefEq (arrowType : Expr) (type : Expr) : MetaM Bool := do
   Convert fixed indices to parameters.
 -/
 private partial def fixedIndicesToParams (numParams : Nat) (indTypes : Array InductiveType) (indFVars : Array Expr) : MetaM Nat := do
+  if !inductive.autoPromoteIndices.get (← getOptions) then
+    return numParams
   let masks ← indTypes.mapM (computeFixedIndexBitMask numParams · indFVars)
+  trace[Elab.inductive] "masks: {masks}"
   if masks.all fun mask => !mask.contains true then
     return numParams
-  trace[Elab.inductive] "masks: {masks}"
   -- We process just a non-fixed prefix of the indices for now. Reason: we don't want to change the order.
   -- TODO: extend it in the future. For example, it should be reasonable to change
   -- the order of indices generated by the auto implicit feature.

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/StructInst.lean

@@ -821,7 +821,9 @@ partial def reduce (structNames : Array Name) (e : Expr) : MetaM Expr := do
     | some r => reduce structNames r
     | none   => return e.updateProj! (← reduce structNames b)
   | .app f .. =>
-    match (← reduceProjOf? e structNames.contains) with
+    -- Recall that proposition fields are theorems. Thus, we must set transparency to .all
+    -- to ensure they are unfolded here
+    match (← withTransparency .all <| reduceProjOf? e structNames.contains) with
     | some r => reduce structNames r
     | none   =>
       let f := f.getAppFn

src/Lean/Elab/Structure.lean

@@ -82,15 +82,6 @@ def StructFieldInfo.isSubobject (info : StructFieldInfo) : Bool :=
   | StructFieldKind.subobject => true
   | _                         => false
 
-structure ElabStructResult where
-  decl            : Declaration
-  projInfos       : List ProjectionInfo
-  projInstances   : List Name -- projections (to parent classes) that must be marked as instances.
-  mctx            : MetavarContext
-  lctx            : LocalContext
-  localInsts      : LocalInstances
-  defaultAuxDecls : Array (Name × Expr × Expr)
-
 private def defaultCtorName := `mk
 
 /-
@@ -713,8 +704,8 @@ private def registerStructure (structName : Name) (infos : Array StructFieldInfo
           subobject? :=
             if info.kind == StructFieldKind.subobject then
               match env.find? info.declName with
-              | some (ConstantInfo.defnInfo val) =>
-                match val.type.getForallBody.getAppFn with
+              | some info =>
+                match info.type.getForallBody.getAppFn with
                 | Expr.const parentName .. => some parentName
                 | _ => panic! "ill-formed structure"
               | _ => panic! "ill-formed environment"

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/Elab/Tactic/Split.lean

@@ -21,12 +21,12 @@ open Meta
       throwErrorAt stx[2] "'split' tactic failed, select a single target to split"
     if simplifyTarget then
       liftMetaTactic fun mvarId => do
-       let some mvarIds ← splitTarget? mvarId | Meta.throwTacticEx `split mvarId ""
+       let some mvarIds ← splitTarget? mvarId | Meta.throwTacticEx `split mvarId
         return mvarIds
     else
       let fvarId ← getFVarId hyps[0]!
       liftMetaTactic fun mvarId => do
-        let some mvarIds ← splitLocalDecl? mvarId fvarId | Meta.throwTacticEx `split mvarId ""
+        let some mvarIds ← splitLocalDecl? mvarId fvarId | Meta.throwTacticEx `split mvarId
         return mvarIds
   | Location.wildcard =>
     liftMetaTactic fun mvarId => do
@@ -34,7 +34,7 @@ open Meta
       for fvarId in fvarIds do
         if let some mvarIds ← splitLocalDecl? mvarId fvarId then
           return mvarIds
-      let some mvarIds ← splitTarget? mvarId | Meta.throwTacticEx `split mvarId ""
+      let some mvarIds ← splitTarget? mvarId | Meta.throwTacticEx `split mvarId
       return mvarIds
 
 end Lean.Elab.Tactic

src/Lean/Language/Basic.lean

@@ -209,6 +209,16 @@ def DynamicSnapshot.toTyped? (α : Type) [TypeName α] (snap : DynamicSnapshot)
     Option α :=
   snap.val.get? α
 
+/--
+  Runs a tree of snapshots to conclusion, incrementally performing `f` on each snapshot in tree
+  preorder. -/
+@[specialize] partial def SnapshotTree.forM [Monad m] (s : SnapshotTree)
+    (f : Snapshot → m PUnit) : m PUnit := do
+  match s with
+  | mk element children =>
+    f element
+    children.forM (·.get.forM f)
+
 /--
   Option for printing end position of each message in addition to start position. Used for testing
   message ranges in the test suite. -/
@@ -216,25 +226,24 @@ register_builtin_option printMessageEndPos : Bool := {
   defValue := false, descr := "print end position of each message in addition to start position"
 }
 
+/-- Reports messages on stdout. If `json` is true, prints messages as JSON (one per line). -/
+def reportMessages (msgLog : MessageLog) (opts : Options) (json := false) : IO Unit := do
+  if json then
+    msgLog.forM (·.toJson <&> (·.compress) >>= IO.println)
+  else
+    msgLog.forM (·.toString (includeEndPos := printMessageEndPos.get opts) >>= IO.print)
+
 /--
   Runs a tree of snapshots to conclusion and incrementally report messages on stdout. Messages are
   reported in tree preorder.
   This function is used by the cmdline driver; see `Lean.Server.FileWorker.reportSnapshots` for how
   the language server reports snapshots asynchronously.  -/
-partial def SnapshotTree.runAndReport (s : SnapshotTree) (opts : Options) : IO Unit := do
-  s.element.diagnostics.msgLog.forM
-    (·.toString (includeEndPos := printMessageEndPos.get opts) >>= IO.print)
-  for t in s.children do
-    t.get.runAndReport opts
+def SnapshotTree.runAndReport (s : SnapshotTree) (opts : Options) (json := false) : IO Unit := do
+  s.forM (reportMessages ·.diagnostics.msgLog opts json)
 
 /-- Waits on and returns all snapshots in the tree. -/
-partial def SnapshotTree.getAll (s : SnapshotTree) : Array Snapshot :=
-  go s |>.run #[] |>.2
-where
-  go s : StateM (Array Snapshot) Unit := do
-    modify (·.push s.element)
-    for t in s.children do
-      go t.get
+def SnapshotTree.getAll (s : SnapshotTree) : Array Snapshot :=
+  s.forM (m := StateM _) (fun s => modify (·.push s)) |>.run #[] |>.2
 
 /-- Metadata that does not change during the lifetime of the language processing process. -/
 structure ModuleProcessingContext where
@@ -287,7 +296,7 @@ end Language
 /--
   Builds a function for processing a language using incremental snapshots by passing the previous
   snapshot to `Language.process` on subsequent invocations. -/
-partial def Language.mkIncrementalProcessor (process : Option InitSnap → ProcessingM InitSnap)
+def Language.mkIncrementalProcessor (process : Option InitSnap → ProcessingM InitSnap)
     (ctx : ModuleProcessingContext) : BaseIO (Parser.InputContext → BaseIO InitSnap) := do
   let oldRef ← IO.mkRef none
   return fun ictx => do

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

@@ -23,7 +23,7 @@ def mkErrorStringWithPos (fileName : String) (pos : Position) (msg : String) (en
 
 inductive MessageSeverity where
   | information | warning | error
-  deriving Inhabited, BEq
+  deriving Inhabited, BEq, ToJson, FromJson
 
 structure MessageDataContext where
   env  : Environment
@@ -82,17 +82,6 @@ inductive MessageData where
 
 namespace MessageData
 
-/-- Determines whether the message contains any content. -/
-def isEmpty : MessageData → Bool
-  | ofFormat f => f.isEmpty
-  | withContext _ m => m.isEmpty
-  | withNamingContext _ m => m.isEmpty
-  | nest _ m => m.isEmpty
-  | group m => m.isEmpty
-  | compose m₁ m₂ => m₁.isEmpty && m₂.isEmpty
-  | tagged _ m => m.isEmpty
-  | _ => false
-
 variable (p : Name → Bool) in
 /-- Returns true when the message contains a `MessageData.tagged tag ..` constructor where `p tag` is true. -/
 partial def hasTag : MessageData → Bool
@@ -131,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 :=
@@ -220,9 +215,15 @@ instance : Coe (List Expr) MessageData := ⟨fun es => ofList <| es.map ofExpr
 
 end MessageData
 
-/-- A `Message` is a richly formatted piece of information emitted by Lean.
-They are rendered by client editors in the infoview and in diagnostic windows. -/
-structure Message where
+/--
+A `BaseMessage` is a richly formatted piece of information emitted by Lean.
+They are rendered by client editors in the infoview and in diagnostic windows.
+There are two varieties in the Lean core:
+* `Message`: Uses structured, effectful `MessageData` for formatting content.
+* `SerialMessage`: Stores pure `String` data. Obtained by running the effectful
+`Message.serialize`.
+-/
+structure BaseMessage (α : Type u) where
   fileName      : String
   pos           : Position
   endPos        : Option Position := none
@@ -231,24 +232,53 @@ structure Message where
   severity      : MessageSeverity := MessageSeverity.error
   caption       : String          := ""
   /-- The content of the message. -/
-  data          : MessageData
-  deriving Inhabited
+  data          : α
+  deriving Inhabited, ToJson, FromJson
 
-namespace Message
+/-- A `Message` is a richly formatted piece of information emitted by Lean.
+They are rendered by client editors in the infoview and in diagnostic windows. -/
+abbrev Message := BaseMessage MessageData
 
-protected def toString (msg : Message) (includeEndPos := false) : IO String := do
-  let mut str ← msg.data.toString
+/-- A `SerialMessage` is a `Message` whose `MessageData` has been eagerly
+serialized and is thus appropriate for use in pure contexts where the effectful
+`MessageData.toString` cannot be used. -/
+abbrev SerialMessage := BaseMessage String
+
+namespace SerialMessage
+
+@[inline] def toMessage (msg : SerialMessage) : Message :=
+  {msg with data := msg.data}
+
+protected def toString (msg : SerialMessage) (includeEndPos := false) : String := Id.run do
+  let mut str := msg.data
   let endPos := if includeEndPos then msg.endPos else none
   unless msg.caption == "" do
     str := msg.caption ++ ":\n" ++ str
   match msg.severity with
-  | MessageSeverity.information => pure ()
-  | MessageSeverity.warning     => str := mkErrorStringWithPos msg.fileName msg.pos (endPos := endPos) "warning: " ++ str
-  | MessageSeverity.error       => str := mkErrorStringWithPos msg.fileName msg.pos (endPos := endPos) "error: " ++ str
+  | .information => pure ()
+  | .warning     => str := mkErrorStringWithPos msg.fileName msg.pos (endPos := endPos) "warning: " ++ str
+  | .error       => str := mkErrorStringWithPos msg.fileName msg.pos (endPos := endPos) "error: " ++ str
   if str.isEmpty || str.back != '\n' then
     str := str ++ "\n"
   return str
 
+instance : ToString SerialMessage := ⟨SerialMessage.toString⟩
+
+end SerialMessage
+
+namespace Message
+
+@[inline] def serialize (msg : Message) : IO SerialMessage := do
+  return {msg with data := ← msg.data.toString}
+
+protected def toString (msg : Message) (includeEndPos := false) : IO String := do
+  -- Remark: The inline here avoids a new message allocation when `msg` is shared
+  return inline <| (← msg.serialize).toString includeEndPos
+
+protected def toJson (msg : Message) : IO Json := do
+  -- Remark: The inline here avoids a new message allocation when `msg` is shared
+  return inline <| toJson (← msg.serialize)
+
 end Message
 
 /-- A persistent array of messages. -/

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,17 @@ 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
+  /--
+  `inTypeClassResolution := true` when `isDefEq` is invoked at `tryResolve` in the type class
+   resolution module. We don't use `isDefEqProjDelta` when performing TC resolution due to performance issues.
+   This is not a great solution, but a proper solution would require a more sophisticased caching mechanism.
+  -/
+  inTypeClassResolution : Bool := false
 
 /--
 The `MetaM` monad is a core component of Lean's metaprogramming framework, facilitating the
@@ -1690,6 +1709,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

@@ -1731,8 +1731,86 @@ private def isDefEqOnFailure (t s : Expr) : MetaM Bool := do
     unstuckMVar s (fun s => Meta.isExprDefEqAux t s) <|
     tryUnificationHints t s <||> tryUnificationHints s t
 
+/--
+Result type for `isDefEqDelta`
+-/
+inductive DeltaStepResult where
+  | eq | unknown
+  | cont (t s : Expr)
+  | diff (t s : Expr)
+
+/--
+Perform one step of lazy delta reduction. This function decides whether to perform delta-reduction on `t`, `s`, or both.
+It is currently used to solve contraints of the form `(f a).i =?= (g a).i` where `i` is a numeral at `isDefEqProjDelta`.
+It is also a simpler version of `isDefEqDelta`. In the future, we may decide to combine these two functions like we do
+in the kernel.
+-/
+private def isDefEqDeltaStep (t s : Expr) : MetaM DeltaStepResult := do
+  let tInfo? ← isDeltaCandidate? t
+  let sInfo? ← isDeltaCandidate? s
+  match tInfo?, sInfo? with
+  | none,       none       => return .unknown
+  | some _,     none       => unfold t (return .unknown) (k · s)
+  | none,       some _     => unfold s (return .unknown) (k t ·)
+  | some tInfo, some sInfo =>
+    match compare tInfo.hints sInfo.hints with
+    | .lt => unfold t (return .unknown) (k · s)
+    | .gt => unfold s (return .unknown) (k t ·)
+    | .eq =>
+      -- 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 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
+    match (← isDefEqQuick t s) with
+    | .true  => return .eq
+    | .false => return .diff t s
+    | .undef => return .cont t s
+
+/--
+Helper function for solving contraints of the form `t.i =?= s.i`.
+-/
+private partial def isDefEqProjDelta (t s : Expr) (i : Nat) : MetaM Bool := do
+  let t ← whnfCore t
+  let s ← whnfCore s
+  match (← isDefEqQuick t s) with
+  | .true  => return true
+  | .false | .undef  => loop t s
+where
+  loop (t s : Expr) : MetaM Bool := do
+    match (← isDefEqDeltaStep t s) with
+    | .cont t s => loop t s
+    | .eq => return true
+    | .unknown => tryReduceProjs t s
+    | .diff t s => tryReduceProjs t s
+
+  tryReduceProjs (t s : Expr) : MetaM Bool := do
+    match (← projectCore? t i), (← projectCore? s i) with
+    | some t, some s => Meta.isExprDefEqAux t s
+    | _, _ => Meta.isExprDefEqAux t s
+
 private def isDefEqProj : Expr → Expr → MetaM Bool
-  | .proj m i t, .proj n j s => pure (i == j && m == n) <&&> Meta.isExprDefEqAux t s
+  | .proj m i t, .proj n j s => do
+    if (← read).inTypeClassResolution then
+      -- See comment at `inTypeClassResolution`
+      pure (i == j && m == n) <&&> Meta.isExprDefEqAux t s
+    else if i == j && m == n then
+      isDefEqProjDelta t s i
+    else
+      return false
   | .proj structName 0 s, v  => isDefEqSingleton structName s v
   | v, .proj structName 0 s  => isDefEqSingleton structName s v
   | _, _ => pure false

src/Lean/Meta/ExprLens.lean

@@ -21,27 +21,28 @@ section ExprLens
 
 open Lean.SubExpr
 
-variable {M} [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] [MonadError M]
+variable [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] [MonadError M]
 
 /-- Given a constructor index for Expr, runs `g` on the value of that subexpression and replaces it.
 If the subexpression is under a binder it will instantiate and abstract the binder body correctly.
 Mdata is ignored. An index of 3 is interpreted as the type of the expression. An index of 3 will throw since we can't replace types.
 
 See also `Lean.Meta.transform`, `Lean.Meta.traverseChildren`. -/
-private def lensCoord (g : Expr → M Expr) : Nat → Expr → M Expr
-  | 0, e@(Expr.app f a)         => return e.updateApp! (← g f) a
-  | 1, e@(Expr.app f a)         => return e.updateApp! f (← g a)
-  | 0, e@(Expr.lam _ y b _)     => return e.updateLambdaE! (← g y) b
-  | 1,   (Expr.lam n y b c)     => withLocalDecl n c y fun x => do mkLambdaFVars #[x] <|← g <| b.instantiateRev #[x]
-  | 0, e@(Expr.forallE _ y b _) => return e.updateForallE! (← g y) b
-  | 1,   (Expr.forallE n y b c) => withLocalDecl n c y fun x => do mkForallFVars #[x] <|← g <| b.instantiateRev #[x]
-  | 0, e@(Expr.letE _ y a b _)  => return e.updateLet! (← g y) a b
-  | 1, e@(Expr.letE _ y a b _)  => return e.updateLet! y (← g a) b
-  | 2,   (Expr.letE n y a b _)  => withLetDecl n y a fun x => do mkLetFVars #[x] <|← g <| b.instantiateRev #[x]
-  | 0, e@(Expr.proj _ _ b)      => e.updateProj! <$> g b
-  | n, e@(Expr.mdata _ a)       => e.updateMData! <$> lensCoord g n a
-  | 3, _                        => throwError "Lensing on types is not supported"
-  | c, e                        => throwError "Invalid coordinate {c} for {e}"
+private def lensCoord (g : Expr → M Expr) (n : Nat) (e : Expr) : M Expr := do
+  match n, e with
+  | 0, .app f a         => return e.updateApp! (← g f) a
+  | 1, .app f a         => return e.updateApp! f (← g a)
+  | 0, .lam _ y b _     => return e.updateLambdaE! (← g y) b
+  | 1, .lam n y b c     => withLocalDecl n c y fun x => do mkLambdaFVars #[x] <|← g <| b.instantiateRev #[x]
+  | 0, .forallE _ y b _ => return e.updateForallE! (← g y) b
+  | 1, .forallE n y b c => withLocalDecl n c y fun x => do mkForallFVars #[x] <|← g <| b.instantiateRev #[x]
+  | 0, .letE _ y a b _  => return e.updateLet! (← g y) a b
+  | 1, .letE _ y a b _  => return e.updateLet! y (← g a) b
+  | 2, .letE n y a b _  => withLetDecl n y a fun x => do mkLetFVars #[x] <|← g <| b.instantiateRev #[x]
+  | 0, .proj _ _ b      => e.updateProj! <$> g b
+  | n, .mdata _ a       => e.updateMData! <$> lensCoord g n a
+  | 3, _                => throwError "Lensing on types is not supported"
+  | c, e                => throwError "Invalid coordinate {c} for {e}"
 
 private def lensAux (g : Expr → M Expr) : List Nat → Expr → M Expr
   | [], e => g e
@@ -56,20 +57,21 @@ def replaceSubexpr (replace : (subexpr : Expr) → M Expr) (p : Pos) (root : Exp
 /-- Runs `k` on the given coordinate, including handling binders properly.
 The subexpression value passed to `k` is not instantiated with respect to the
 array of free variables. -/
-private def viewCoordAux (k : Array Expr → Expr → M α) (fvars: Array Expr) : Nat → Expr → M α
-  | 3, _                      => throwError "Internal: Types should be handled by viewAux"
-  | 0, (Expr.app f _)         => k fvars f
-  | 1, (Expr.app _ a)         => k fvars a
-  | 0, (Expr.lam _ y _ _)     => k fvars y
-  | 1, (Expr.lam n y b c)     => withLocalDecl n c (y.instantiateRev fvars) fun x => k (fvars.push x) b
-  | 0, (Expr.forallE _ y _ _) => k fvars y
-  | 1, (Expr.forallE n y b c) => withLocalDecl n c (y.instantiateRev fvars) fun x => k (fvars.push x) b
-  | 0, (Expr.letE _ y _ _ _)  => k fvars y
-  | 1, (Expr.letE _ _ a _ _)  => k fvars a
-  | 2, (Expr.letE n y a b _)  => withLetDecl n (y.instantiateRev fvars) (a.instantiateRev fvars) fun x => k (fvars.push x) b
-  | 0, (Expr.proj _ _ b)      => k fvars b
-  | n, (Expr.mdata _ a)       => viewCoordAux k fvars n a
-  | c, e                      => throwError "Invalid coordinate {c} for {e}"
+private def viewCoordAux (k : Array Expr → Expr → M α) (fvars: Array Expr) (n : Nat) (e : Expr) : M α := do
+  match n, e with
+  | 3, _                => throwError "Internal: Types should be handled by viewAux"
+  | 0, .app f _         => k fvars f
+  | 1, .app _ a         => k fvars a
+  | 0, .lam _ y _ _     => k fvars y
+  | 1, .lam n y b c     => withLocalDecl n c (y.instantiateRev fvars) fun x => k (fvars.push x) b
+  | 0, .forallE _ y _ _ => k fvars y
+  | 1, .forallE n y b c => withLocalDecl n c (y.instantiateRev fvars) fun x => k (fvars.push x) b
+  | 0, .letE _ y _ _ _  => k fvars y
+  | 1, .letE _ _ a _ _  => k fvars a
+  | 2, .letE n y a b _  => withLetDecl n (y.instantiateRev fvars) (a.instantiateRev fvars) fun x => k (fvars.push x) b
+  | 0, .proj _ _ b      => k fvars b
+  | n, .mdata _ a       => viewCoordAux k fvars n a
+  | c, e                => throwError "Invalid coordinate {c} for {e}"
 
 private def viewAux (k : Array Expr → Expr → M α) (fvars : Array Expr) : List Nat → Expr → M α
   | [],         e => k fvars <| e.instantiateRev fvars
@@ -119,24 +121,24 @@ open Lean.SubExpr
 
 section ViewRaw
 
-variable {M} [Monad M] [MonadError M]
+variable [Monad M] [MonadError M]
 
 /-- Get the raw subexpression without performing any instantiation. -/
-private def viewCoordRaw: Expr → Nat → M Expr
-  | e                     , 3 => throwError "Can't viewRaw the type of {e}"
-  | (Expr.app f _)        , 0 => pure f
-  | (Expr.app _ a)        , 1 => pure a
-  | (Expr.lam _ y _ _)    , 0 => pure y
-  | (Expr.lam _ _ b _)    , 1 => pure b
-  | (Expr.forallE _ y _ _), 0 => pure y
-  | (Expr.forallE _ _ b _), 1 => pure b
-  | (Expr.letE _ y _ _ _) , 0 => pure y
-  | (Expr.letE _ _ a _ _) , 1 => pure a
-  | (Expr.letE _ _ _ b _) , 2 => pure b
-  | (Expr.proj _ _ b)     , 0 => pure b
-  | (Expr.mdata _ a)      , n => viewCoordRaw a n
-  | e                     , c => throwError "Bad coordinate {c} for {e}"
-
+private def viewCoordRaw (e : Expr) (n : Nat) : M Expr := do
+  match e, n with
+  | e,                3 => throwError "Can't viewRaw the type of {e}"
+  | .app f _,         0 => pure f
+  | .app _ a,         1 => pure a
+  | .lam _ y _ _,     0 => pure y
+  | .lam _ _ b _,     1 => pure b
+  | .forallE _ y _ _, 0 => pure y
+  | .forallE _ _ b _, 1 => pure b
+  | .letE _ y _ _ _,  0 => pure y
+  | .letE _ _ a _ _,  1 => pure a
+  | .letE _ _ _ b _,  2 => pure b
+  | .proj _ _ b,      0 => pure b
+  | .mdata _ a,       n => viewCoordRaw a n
+  | e,                c => throwError "Bad coordinate {c} for {e}"
 
 /-- Given a valid `SubExpr`, return the raw current expression without performing any instantiation.
 If the given `SubExpr` has a type subexpression coordinate, then throw an error.
@@ -148,21 +150,20 @@ def viewSubexpr (p : Pos) (root : Expr) : M Expr :=
   p.foldlM viewCoordRaw root
 
 private def viewBindersCoord : Nat → Expr → Option (Name × Expr)
-  | 1, (Expr.lam n y _ _)     => some (n, y)
-  | 1, (Expr.forallE n y _ _) => some (n, y)
-  | 2, (Expr.letE n y _ _ _)  => some (n, y)
-  | _, _                      => none
+  | 1, .lam n y _ _     => some (n, y)
+  | 1, .forallE n y _ _ => some (n, y)
+  | 2, .letE n y _ _ _  => some (n, y)
+  | _, _                => none
 
 /-- `viewBinders p e` returns a list of all of the binders (name, type) above the given position `p` in the root expression `e` -/
 def viewBinders (p : Pos) (root : Expr) : M (Array (Name × Expr)) := do
-  let (acc, _) ← p.foldlM (fun (acc, e) c => do
+  let (acc, _) ← p.foldlM (init := (#[], root)) fun (acc, e) c => do
     let e₂ ← viewCoordRaw e c
     let acc :=
       match viewBindersCoord c e with
       | none => acc
       | some b => acc.push b
     return (acc, e₂)
-  ) (#[], root)
   return acc
 
 /-- Returns the number of binders above a given subexpr position. -/

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

@@ -25,6 +25,12 @@ register_builtin_option synthInstance.maxSize : Nat := {
   descr := "maximum number of instances used to construct a solution in the type class instance synthesis procedure"
 }
 
+register_builtin_option backward.synthInstance.canonInstances : Bool := {
+  defValue := true
+  group    := "backward compatibility"
+  descr := "use optimization that relies on 'morally canonical' instances during type class resolution"
+}
+
 namespace SynthInstance
 
 def getMaxHeartbeats (opts : Options) : Nat :=
@@ -41,6 +47,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 +70,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 +112,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 +132,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 +216,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 +248,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 +366,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 +388,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 +398,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 +429,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 +441,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 +554,18 @@ def generate : SynthM Unit := do
     let inst := gNode.instances.get! idx
     let mctx := gNode.mctx
     let mvar := gNode.mvar
+    /- See comment at `typeHasMVars` -/
+    if backward.synthInstance.canonInstances.get (← getOptions) then
+      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 +694,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 +717,8 @@ 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
+  withReader (fun ctx => { ctx with inTypeClassResolution := true }) do
     let localInsts ← getLocalInstances
     let type ← instantiateMVars type
     let type ← preprocess type
@@ -775,8 +803,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/Meta/Tactic/Assumption.lean

@@ -33,7 +33,7 @@ def assumptionCore (mvarId : MVarId) : MetaM Bool :=
 /-- Close goal `mvarId` using an assumption. Throw error message if failed. -/
 def _root_.Lean.MVarId.assumption (mvarId : MVarId) : MetaM Unit :=
   unless (← mvarId.assumptionCore) do
-    throwTacticEx `assumption mvarId ""
+    throwTacticEx `assumption mvarId
 
 @[deprecated MVarId.assumption]
 def assumption (mvarId : MVarId) : MetaM Unit :=

src/Lean/Meta/Tactic/Contradiction.lean

@@ -224,7 +224,7 @@ Throw exception if goal failed to be closed.
 -/
 def _root_.Lean.MVarId.contradiction (mvarId : MVarId) (config : Contradiction.Config := {}) : MetaM Unit :=
   unless (← mvarId.contradictionCore config) do
-    throwTacticEx `contradiction mvarId ""
+    throwTacticEx `contradiction mvarId
 
 @[deprecated MVarId.contradiction]
 def contradiction (mvarId : MVarId) (config : Contradiction.Config := {}) : MetaM Unit :=

src/Lean/Meta/Tactic/Refl.lean

@@ -67,6 +67,6 @@ Close given goal using `HEq.refl`.
 def _root_.Lean.MVarId.hrefl (mvarId : MVarId) : MetaM Unit := do
   mvarId.withContext do
     let some [] ← observing? do mvarId.apply (mkConst ``HEq.refl [← mkFreshLevelMVar])
-      | throwTacticEx `hrefl mvarId ""
+      | throwTacticEx `hrefl mvarId
 
 end Lean.Meta

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -241,7 +241,17 @@ def getSimpLetCase (n : Name) (t : Expr) (b : Expr) : MetaM SimpLetCase := do
     else
       return SimpLetCase.dep
 
-def withNewLemmas {α} (xs : Array Expr) (f : SimpM α) : SimpM α := do
+/--
+We use `withNewlemmas` whenever updating the local context.
+We use `withFreshCache` because the local context affects `simp` rewrites
+even when `contextual := false`.
+For example, the `discharger` may inspect the current local context. The default
+discharger does that when applying equational theorems, and the user may
+use `(discharger := assumption)` or `(discharger := omega)`.
+If the `wishFreshCache` introduces performance issues, we can design a better solution
+for the default discharger which is used most of the time.
+-/
+def withNewLemmas {α} (xs : Array Expr) (f : SimpM α) : SimpM α := withFreshCache do
   if (← getConfig).contextual then
     let mut s ← getSimpTheorems
     let mut updated := false
@@ -250,7 +260,7 @@ def withNewLemmas {α} (xs : Array Expr) (f : SimpM α) : SimpM α := do
         s ← s.addTheorem (.fvar x.fvarId!) x
         updated := true
     if updated then
-      withSimpTheorems s f
+      withTheReader Context (fun ctx => { ctx with simpTheorems := s }) f
     else
       f
   else
@@ -304,30 +314,27 @@ def simpArrow (e : Expr) : SimpM Result := do
   trace[Debug.Meta.Tactic.simp] "arrow [{(← getConfig).contextual}] {p} [{← isProp p}] -> {q} [{← isProp q}]"
   if (← pure (← getConfig).contextual <&&> isProp p <&&> isProp q) then
     trace[Debug.Meta.Tactic.simp] "ctx arrow {rp.expr} -> {q}"
-    withLocalDeclD e.bindingName! rp.expr fun h => do
-      let s ← getSimpTheorems
-      let s ← s.addTheorem (.fvar h.fvarId!) h
-      withSimpTheorems s do
-        let rq ← simp q
-        match rq.proof? with
-        | none    => mkImpCongr e rp rq
-        | some hq =>
-          let hq ← mkLambdaFVars #[h] hq
-          /-
-            We use the default reducibility setting at `mkImpDepCongrCtx` and `mkImpCongrCtx` because they use the theorems
-            ```lean
-            @implies_dep_congr_ctx : ∀ {p₁ p₂ q₁ : Prop}, p₁ = p₂ → ∀ {q₂ : p₂ → Prop}, (∀ (h : p₂), q₁ = q₂ h) → (p₁ → q₁) = ∀ (h : p₂), q₂ h
-            @implies_congr_ctx : ∀ {p₁ p₂ q₁ q₂ : Prop}, p₁ = p₂ → (p₂ → q₁ = q₂) → (p₁ → q₁) = (p₂ → q₂)
-            ```
-            And the proofs may be from `rfl` theorems which are now omitted. Moreover, we cannot establish that the two
-            terms are definitionally equal using `withReducible`.
-            TODO (better solution): provide the problematic implicit arguments explicitly. It is more efficient and avoids this
-            problem.
-            -/
-          if rq.expr.containsFVar h.fvarId! then
-            return { expr := (← mkForallFVars #[h] rq.expr), proof? := (← withDefault <| mkImpDepCongrCtx (← rp.getProof) hq) }
-          else
-            return { expr := e.updateForallE! rp.expr rq.expr, proof? := (← withDefault <| mkImpCongrCtx (← rp.getProof) hq) }
+    withLocalDeclD e.bindingName! rp.expr fun h => withNewLemmas #[h] do
+      let rq ← simp q
+      match rq.proof? with
+      | none    => mkImpCongr e rp rq
+      | some hq =>
+        let hq ← mkLambdaFVars #[h] hq
+        /-
+          We use the default reducibility setting at `mkImpDepCongrCtx` and `mkImpCongrCtx` because they use the theorems
+          ```lean
+          @implies_dep_congr_ctx : ∀ {p₁ p₂ q₁ : Prop}, p₁ = p₂ → ∀ {q₂ : p₂ → Prop}, (∀ (h : p₂), q₁ = q₂ h) → (p₁ → q₁) = ∀ (h : p₂), q₂ h
+          @implies_congr_ctx : ∀ {p₁ p₂ q₁ q₂ : Prop}, p₁ = p₂ → (p₂ → q₁ = q₂) → (p₁ → q₁) = (p₂ → q₂)
+          ```
+          And the proofs may be from `rfl` theorems which are now omitted. Moreover, we cannot establish that the two
+          terms are definitionally equal using `withReducible`.
+          TODO (better solution): provide the problematic implicit arguments explicitly. It is more efficient and avoids this
+          problem.
+          -/
+        if rq.expr.containsFVar h.fvarId! then
+          return { expr := (← mkForallFVars #[h] rq.expr), proof? := (← withDefault <| mkImpDepCongrCtx (← rp.getProof) hq) }
+        else
+          return { expr := e.updateForallE! rp.expr rq.expr, proof? := (← withDefault <| mkImpCongrCtx (← rp.getProof) hq) }
   else
     mkImpCongr e rp (← simp q)
 
@@ -389,7 +396,7 @@ def simpLet (e : Expr) : SimpM Result := do
     | SimpLetCase.dep => return { expr := (← dsimp e) }
     | SimpLetCase.nondep =>
       let rv ← simp v
-      withLocalDeclD n t fun x => do
+      withLocalDeclD n t fun x => withNewLemmas #[x] do
         let bx := b.instantiate1 x
         let rbx ← simp bx
         let hb? ← match rbx.proof? with
@@ -402,7 +409,7 @@ def simpLet (e : Expr) : SimpM Result := do
         | _,      some h => return { expr := e', proof? := some (← mkLetCongr (← rv.getProof) h) }
     | SimpLetCase.nondepDepVar =>
       let v' ← dsimp v
-      withLocalDeclD n t fun x => do
+      withLocalDeclD n t fun x => withNewLemmas #[x] do
         let bx := b.instantiate1 x
         let rbx ← simp bx
         let e' := mkLet n t v' (← rbx.expr.abstractM #[x])

src/Lean/Meta/Tactic/Simp/Types.lean

@@ -21,7 +21,11 @@ structure Result where
   /-- A proof that `$e = $expr`, where the simplified expression is on the RHS.
   If `none`, the proof is assumed to be `refl`. -/
   proof?         : Option Expr := none
-  /-- If `cache := true` the result is cached. -/
+  /--
+  If `cache := true` the result is cached.
+  Warning: we will remove this field in the future. It is currently used by
+  `arith := true`, but we can now refactor the code to avoid the hack.
+  -/
   cache          : Bool := true
   deriving Inhabited
 
@@ -284,9 +288,6 @@ Save current cache, reset it, execute `x`, and then restore original cache.
   modify fun s => { s with cache := {} }
   try x finally modify fun s => { s with cache := cacheSaved }
 
-@[inline] def withSimpTheorems (s : SimpTheoremsArray) (x : SimpM α) : SimpM α := do
-  withFreshCache <| withTheReader Context (fun ctx => { ctx with simpTheorems := s }) x
-
 @[inline] def withDischarger (discharge? : Expr → SimpM (Option Expr)) (x : SimpM α) : SimpM α :=
   withFreshCache <| withReader (fun r => { MethodsRef.toMethods r with discharge? }.toMethodsRef) x
 

src/Lean/Meta/Tactic/SolveByElim.lean

@@ -68,7 +68,7 @@ We use this in `apply_rules` and `apply_assumption` where backtracking is not ne
 -/
 def applyFirst (cfg : ApplyConfig := {}) (transparency : TransparencyMode := .default)
     (lemmas : List Expr) (g : MVarId) : MetaM (List MVarId) := do
-  (←applyTactics cfg transparency lemmas g).head
+  (← applyTactics cfg transparency lemmas g).head
 
 open Lean.Meta.Tactic.Backtrack (BacktrackConfig backtrack)
 
@@ -168,7 +168,7 @@ applied to the instantiations of the original goals, fails or returns `false`.
 def testPartialSolutions (cfg : SolveByElimConfig := {}) (test : List Expr → MetaM Bool) : SolveByElimConfig :=
   { cfg with
     proc := fun orig goals => do
-      let .true ← test (← orig.mapM fun m => m.withContext do instantiateMVars (.mvar m)) | failure
+      guard <| ← test (← orig.mapM fun m => m.withContext do instantiateMVars (.mvar m))
       cfg.proc orig goals }
 
 /--
@@ -204,22 +204,24 @@ end SolveByElimConfig
 Elaborate a list of lemmas and local context.
 See `mkAssumptionSet` for an explanation of why this is needed.
 -/
-def elabContextLemmas (g : MVarId) (lemmas : List (TermElabM Expr)) (ctx : TermElabM (List Expr)) :
+def elabContextLemmas (cfg : SolveByElimConfig) (g : MVarId)
+    (lemmas : List (TermElabM Expr)) (ctx : SolveByElimConfig → TermElabM (List Expr)) :
     MetaM (List Expr) := do
-  g.withContext (Elab.Term.TermElabM.run' do pure ((← ctx) ++ (← lemmas.mapM id)))
+  g.withContext (Elab.Term.TermElabM.run' do pure ((← ctx cfg) ++ (← lemmas.mapM id)))
 
 /-- Returns the list of tactics corresponding to applying the available lemmas to the goal. -/
-def applyLemmas (cfg : SolveByElimConfig) (lemmas : List (TermElabM Expr)) (ctx : TermElabM (List Expr))
-    (g : MVarId)
-    : MetaM (Meta.Iterator (List MVarId)) := do
-  let es ← elabContextLemmas g lemmas ctx
+def applyLemmas (cfg : SolveByElimConfig)
+    (lemmas : List (TermElabM Expr)) (ctx : SolveByElimConfig → TermElabM (List Expr))
+    (g : MVarId) : MetaM (Meta.Iterator (List MVarId)) := do
+  let es ← elabContextLemmas cfg g lemmas ctx
   applyTactics cfg.toApplyConfig cfg.transparency es g
 
 /-- Applies the first possible lemma to the goal. -/
-def applyFirstLemma (cfg : SolveByElimConfig) (lemmas : List (TermElabM Expr)) (ctx : TermElabM (List Expr))
+def applyFirstLemma (cfg : SolveByElimConfig)
+    (lemmas : List (TermElabM Expr)) (ctx : SolveByElimConfig → TermElabM (List Expr))
     (g : MVarId) : MetaM (List MVarId) := do
-let es ← elabContextLemmas g lemmas ctx
-applyFirst cfg.toApplyConfig cfg.transparency es g
+  let es ← elabContextLemmas cfg g lemmas ctx
+  applyFirst cfg.toApplyConfig cfg.transparency es g
 
 /--
 Solve a collection of goals by repeatedly applying lemmas, backtracking as necessary.
@@ -237,21 +239,16 @@ By default `cfg.suspend` is `false,` `cfg.discharge` fails, and `cfg.failAtMaxDe
 and so the returned list is always empty.
 Custom wrappers (e.g. `apply_assumption` and `apply_rules`) may modify this behaviour.
 -/
-def solveByElim (cfg : SolveByElimConfig) (lemmas : List (TermElabM Expr)) (ctx : TermElabM (List Expr))
+def solveByElim (cfg : SolveByElimConfig)
+    (lemmas : List (TermElabM Expr)) (ctx : SolveByElimConfig → TermElabM (List Expr))
     (goals : List MVarId) : MetaM (List MVarId) := do
   let cfg := cfg.processOptions
-  -- We handle `cfg.symm` by saturating hypotheses of all goals using `symm`.
-  -- This has better performance that the mathlib3 approach.
-  let preprocessedGoals ← if cfg.symm then
-    goals.mapM fun g => g.symmSaturate
-  else
-    pure goals
   try
-    run cfg preprocessedGoals
+    run cfg goals
   catch e => do
     -- Implementation note: as with `cfg.symm`, this is different from the mathlib3 approach,
     -- for (not as severe) performance reasons.
-    match preprocessedGoals, cfg.exfalso with
+    match goals, cfg.exfalso with
     | [g], true =>
       withTraceNode `Meta.Tactic.solveByElim
           (fun _ => return m!"⏮️ starting over using `exfalso`") do
@@ -265,6 +262,16 @@ where
     else
       Lean.Meta.repeat1' (maxIters := cfg.maxDepth) (applyFirstLemma cfg lemmas ctx)
 
+/--
+If `symm` is `true`, then adds in symmetric versions of each hypothesis.
+-/
+def saturateSymm (symm : Bool) (hyps : List Expr) : MetaM (List Expr) := do
+  if symm then
+    let extraHyps ← hyps.filterMapM fun hyp => try some <$> hyp.applySymm catch _ => pure none
+    return hyps ++ extraHyps
+  else
+    return hyps
+
 /--
 A `MetaM` analogue of the `apply_rules` user tactic.
 
@@ -276,7 +283,9 @@ If you need to remove particular local hypotheses, call `solveByElim` directly.
 -/
 def _root_.Lean.MVarId.applyRules (cfg : SolveByElimConfig) (lemmas : List (TermElabM Expr))
     (only : Bool := false) (g : MVarId) : MetaM (List MVarId) := do
-  let ctx : TermElabM (List Expr) := if only then pure [] else do pure (← getLocalHyps).toList
+  let ctx (cfg : SolveByElimConfig) : TermElabM (List Expr) :=
+    if only then pure []
+    else do saturateSymm cfg.symm (← getLocalHyps).toList
   solveByElim { cfg with backtracking := false } lemmas ctx [g]
 
 open Lean.Parser.Tactic
@@ -330,7 +339,7 @@ that have been explicitly removed via `only` or `[-h]`.)
 -- These `TermElabM`s must be run inside a suitable `g.withContext`,
 -- usually using `elabContextLemmas`.
 def mkAssumptionSet (noDefaults star : Bool) (add remove : List Term) (use : Array Ident) :
-    MetaM (List (TermElabM Expr) × TermElabM (List Expr)) := do
+    MetaM (List (TermElabM Expr) × (SolveByElimConfig → TermElabM (List Expr))) := do
   if star && !noDefaults then
     throwError "It doesn't make sense to use `*` without `only`."
 
@@ -345,13 +354,12 @@ def mkAssumptionSet (noDefaults star : Bool) (add remove : List Term) (use : Arr
 
   if !remove.isEmpty && noDefaults && !star then
     throwError "It doesn't make sense to remove local hypotheses when using `only` without `*`."
-  let locals : TermElabM (List Expr) := if noDefaults && !star then do
-    pure []
-  else do
-    pure <| (← getLocalHyps).toList.removeAll (← remove.mapM elab')
+  let locals (cfg : SolveByElimConfig) : TermElabM (List Expr) :=
+    if noDefaults && !star then do pure []
+    else do saturateSymm cfg.symm <| (← getLocalHyps).toList.removeAll (← remove.mapM elab')
 
   return (lemmas, locals)
-  where
+where
   /-- Run `elabTerm`. -/
   elab' (t : Term) : TermElabM Expr := Elab.Term.elabTerm t.raw none
 

src/Lean/Meta/Tactic/Util.lean

@@ -36,11 +36,10 @@ def appendTagSuffix (mvarId : MVarId) (suffix : Name) : MetaM Unit := do
 def mkFreshExprSyntheticOpaqueMVar (type : Expr) (tag : Name := Name.anonymous) : MetaM Expr :=
   mkFreshExprMVar type MetavarKind.syntheticOpaque tag
 
-def throwTacticEx (tacticName : Name) (mvarId : MVarId) (msg : MessageData) : MetaM α :=
-  if msg.isEmpty then
-    throwError "tactic '{tacticName}' failed\n{mvarId}"
-  else
-    throwError "tactic '{tacticName}' failed, {msg}\n{mvarId}"
+def throwTacticEx (tacticName : Name) (mvarId : MVarId) (msg? : Option MessageData := none) : MetaM α :=
+  match msg? with
+  | none => throwError "tactic '{tacticName}' failed\n{mvarId}"
+  | some msg => throwError "tactic '{tacticName}' failed, {msg}\n{mvarId}"
 
 def throwNestedTacticEx {α} (tacticName : Name) (ex : Exception) : MetaM α := do
   throwError "tactic '{tacticName}' failed, nested error:\n{ex.toMessageData}"

src/Lean/Meta/WHNF.lean

@@ -529,7 +529,7 @@ def reduceMatcher? (e : Expr) : MetaM ReduceMatcherResult := do
       i := i + 1
     return ReduceMatcherResult.stuck auxApp
 
-private def projectCore? (e : Expr) (i : Nat) : MetaM (Option Expr) := do
+def projectCore? (e : Expr) (i : Nat) : MetaM (Option Expr) := do
   let e := e.toCtorIfLit
   matchConstCtor e.getAppFn (fun _ => pure none) fun ctorVal _ =>
     let numArgs := e.getAppNumArgs

src/Lean/Parser/Command.lean

@@ -208,10 +208,36 @@ def «structure»          := leading_parser
   "deriving " >> "instance " >> derivingClasses >> " for " >> sepBy1 (recover ident skip) ", "
 @[builtin_command_parser] def noncomputableSection := leading_parser
   "noncomputable " >> "section" >> optional (ppSpace >> checkColGt >> ident)
+/--
+A `section`/`end` pair delimits the scope of `variable`, `open`, `set_option`, and `local` commands.
+Sections can be nested. `section <id>` provides a label to the section that has to appear with the
+matching `end`. In either case, the `end` can be omitted, in which case the section is closed at the
+end of the file.
+-/
 @[builtin_command_parser] def «section»      := leading_parser
   "section" >> optional (ppSpace >> checkColGt >> ident)
+/--
+`namespace <id>` opens a section with label `<id>` that influences naming and name resolution inside
+the section:
+* Declarations names are prefixed: `def seventeen : ℕ := 17` inside a namespace `Nat` is given the
+  full name `Nat.seventeen`.
+* Names introduced by `export` declarations are also prefixed by the identifier.
+* All names starting with `<id>.` become available in the namespace without the prefix. These names
+  are preferred over names introduced by outer namespaces or `open`.
+* Within a namespace, declarations can be `protected`, which excludes them from the effects of
+  opening the namespace.
+
+As with `section`, namespaces can be nested and the scope of a namespace is terminated by a
+corresponding `end <id>` or the end of the file.
+
+`namespace` also acts like `section` in delimiting the scope of `variable`, `open`, and other scoped commands.
+-/
 @[builtin_command_parser] def «namespace»    := leading_parser
   "namespace " >> checkColGt >> ident
+/--
+`end` closes a `section` or `namespace` scope. If the scope is named `<id>`, it has to be closed
+with `end <id>`.
+-/
 @[builtin_command_parser] def «end»          := leading_parser
   "end" >> optional (ppSpace >> checkColGt >> ident)
 /-- Declares one or more typed variables, or modifies whether already-declared variables are
@@ -393,6 +419,21 @@ structure Pair (α : Type u) (β : Type v) : Type (max u v) where
 @[builtin_command_parser] def «init_quot»    := leading_parser
   "init_quot"
 def optionValue := nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> strLit <|> numLit
+/--
+`set_option <id> <value>` sets the option `<id>` to `<value>`. Depending on the type of the option,
+the value can be `true`, `false`, a string, or a numeral. Options are used to configure behavior of
+Lean as well as user-defined extensions. The setting is active until the end of the current `section`
+or `namespace` or the end of the file.
+Auto-completion is available for `<id>` to list available options.
+
+`set_option <id> <value> in <command>` sets the option for just a single command:
+```
+set_option pp.all true in
+#check 1 + 1
+```
+Similarly, `set_option <id> <value> in` can also be used inside terms and tactics to set an option
+only in a single term or tactic.
+-/
 @[builtin_command_parser] def «set_option»   := leading_parser
   "set_option " >> identWithPartialTrailingDot >> ppSpace >> optionValue
 def eraseAttr := leading_parser

src/Lean/Parser/Term.lean

@@ -870,7 +870,7 @@ def matchExprElseAlt (rhsParser : Parser) := leading_parser "| " >> ppIndent (ho
 def matchExprAlts (rhsParser : Parser) :=
   leading_parser withPosition $
     many (ppLine >> checkColGe "irrelevant" >> notFollowedBy (symbol "| " >> " _ ") "irrelevant" >> matchExprAlt rhsParser)
-    >> (ppLine >> checkColGe "irrelevant" >> matchExprElseAlt rhsParser)
+    >> (ppLine >> checkColGe "else-alternative for `match_expr`, i.e., `| _ => ...`" >> matchExprElseAlt rhsParser)
 @[builtin_term_parser] def matchExpr := leading_parser:leadPrec
   "match_expr " >> termParser >> " with" >> ppDedent (matchExprAlts termParser)
 

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/SubExpr.lean

@@ -54,24 +54,24 @@ def push (p : Pos) (c : Nat) : Pos :=
 variable {α : Type} [Inhabited α]
 
 /-- Fold over the position starting at the root and heading to the leaf-/
-partial def foldl  (f : α → Nat → α) (a : α) (p : Pos) : α :=
-  if p.isRoot then a else f (foldl f a p.tail) p.head
+partial def foldl  (f : α → Nat → α) (init : α) (p : Pos) : α :=
+  if p.isRoot then init else f (foldl f init p.tail) p.head
 
 /-- Fold over the position starting at the leaf and heading to the root-/
-partial def foldr  (f : Nat → α → α) (p : Pos) (a : α) : α :=
-  if p.isRoot then a else foldr f p.tail (f p.head a)
+partial def foldr  (f : Nat → α → α) (p : Pos) (init : α) : α :=
+  if p.isRoot then init else foldr f p.tail (f p.head init)
 
 /-- monad-fold over the position starting at the root and heading to the leaf -/
-partial def foldlM  [Monad M] (f : α → Nat → M α) (a : α) (p : Pos) : M α :=
+partial def foldlM  [Monad M] (f : α → Nat → M α) (init : α) (p : Pos) : M α :=
   have : Inhabited (M α) := inferInstance
-  if p.isRoot then pure a else do foldlM f a p.tail >>= (f · p.head)
+  if p.isRoot then pure init else do foldlM f init p.tail >>= (f · p.head)
 
 /-- monad-fold over the position starting at the leaf and finishing at the root. -/
-partial def foldrM [Monad M] (f : Nat → α → M α) (p : Pos) (a : α) : M α :=
-  if p.isRoot then pure a else f p.head a >>= foldrM f p.tail
+partial def foldrM [Monad M] (f : Nat → α → M α) (p : Pos) (init : α) : M α :=
+  if p.isRoot then pure init else f p.head init >>= foldrM f p.tail
 
 def depth (p : Pos) :=
-  p.foldr (fun _ => Nat.succ) 0
+  p.foldr (init := 0) fun _ => Nat.succ
 
 /-- Returns true if `pred` is true for each coordinate in `p`.-/
 def all (pred : Nat → Bool) (p : Pos) : Bool :=
@@ -134,8 +134,8 @@ protected def fromString? : String → Except String Pos
 
 protected def fromString! (s : String) : Pos :=
   match Pos.fromString? s with
-  | Except.ok a => a
-  | Except.error e => panic! e
+  | .ok a => a
+  | .error e => panic! e
 
 instance : Ord Pos := show Ord Nat by infer_instance
 instance : DecidableEq Pos := show DecidableEq Nat by infer_instance
@@ -213,7 +213,7 @@ open SubExpr in
 `SubExpr.Pos` argument for tracking subexpression position. -/
 def Expr.traverseAppWithPos {M} [Monad M] (visit : Pos → Expr → M Expr) (p : Pos) (e : Expr) : M Expr :=
   match e with
-  | Expr.app f a =>
+  | .app f a =>
     e.updateApp!
       <$> traverseAppWithPos visit p.pushAppFn f
       <*> visit p.pushAppArg a

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/Heartbeats.lean

@@ -1,19 +1,15 @@
 /-
-Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Copyright (c) 2023 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Author: Leonardo de Moura
+Author: Kim Morrison
 -/
 prelude
 import Lean.CoreM
 
 /-!
-# Lean.Heartbeats
-
-This provides some utilities is the first file in the Lean import hierarchy. It is responsible for setting
-up basic definitions, most of which Lean already has "built in knowledge" about,
-so it is important that they be set up in exactly this way. (For example, Lean will
-use `PUnit` in the desugaring of `do` notation, or in the pattern match compiler.)
+# Heartbeats
 
+Functions for interacting with the deterministic timeout heartbeat mechanism.
 -/
 
 namespace Lean

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/kernel/declaration.cpp

@@ -30,7 +30,6 @@ int compare(reducibility_hints const & h1, reducibility_hints const & h2) {
                 return -1; /* unfold f1 */
             else
                 return 1;  /* unfold f2 */
-            return h1.get_height() > h2.get_height() ? -1 : 1;
         } else {
             return 0; /* reduce both */
         }
@@ -206,6 +205,10 @@ declaration mk_definition(environment const & env, name const & n, names const &
     return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Definition), mk_definition_val(env, n, params, t, v, safety)));
 }
 
+declaration mk_theorem(name const & n, names const & lparams, expr const & type, expr const & val) {
+    return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Theorem), theorem_val(n, lparams, type, val)));
+}
+
 declaration mk_opaque(name const & n, names const & params, expr const & t, expr const & v, bool is_unsafe) {
     return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Opaque), opaque_val(n, params, t, v, is_unsafe, names(n))));
 }

src/kernel/declaration.h

@@ -223,10 +223,12 @@ inline optional<declaration> none_declaration() { return optional<declaration>()
 inline optional<declaration> some_declaration(declaration const & o) { return optional<declaration>(o); }
 inline optional<declaration> some_declaration(declaration && o) { return optional<declaration>(std::forward<declaration>(o)); }
 
+bool use_unsafe(environment const & env, expr const & e);
 declaration mk_definition(name const & n, names const & lparams, expr const & t, expr const & v,
                           reducibility_hints const & hints, definition_safety safety = definition_safety::safe);
 declaration mk_definition(environment const & env, name const & n, names const & lparams, expr const & t, expr const & v,
                           definition_safety safety = definition_safety::safe);
+declaration mk_theorem(name const & n, names const & lparams, expr const & type, expr const & val);
 declaration mk_opaque(name const & n, names const & lparams, expr const & t, expr const & v, bool unsafe);
 declaration mk_axiom(name const & n, names const & lparams, expr const & t, bool unsafe = false);
 declaration mk_inductive_decl(names const & lparams, nat const & nparams, inductive_types const & types, bool is_unsafe);

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

src/library/constructions/projection.cpp

@@ -86,7 +86,8 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
             throw exception(sstream() << "generating projection '" << proj_name << "', '"
                             << n << "' does not have sufficient data");
         expr result_type   = consume_type_annotations(binding_domain(cnstr_type));
-        if (is_predicate && !type_checker(new_env, lctx).is_prop(result_type)) {
+        bool is_prop       = type_checker(new_env, lctx).is_prop(result_type);
+        if (is_predicate && !is_prop) {
             throw exception(sstream() << "failed to generate projection '" << proj_name << "' for '" << n << "', "
                             << "type is an inductive predicate, but field is not a proposition");
         }
@@ -97,13 +98,24 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
         proj_type      = infer_implicit_params(proj_type, nparams, implicit_infer_kind::RelaxedImplicit);
         expr proj_val  = mk_proj(n, i, c);
         proj_val = lctx.mk_lambda(proj_args, proj_val);
-        declaration new_d = mk_definition_inferring_unsafe(env, proj_name, lvl_params, proj_type, proj_val,
+        declaration new_d;
+        if (is_prop) {
+            bool unsafe = use_unsafe(env, proj_type) || use_unsafe(env, proj_val);
+            if (unsafe) {
+                // theorems cannot be unsafe
+                new_d = mk_opaque(proj_name, lvl_params, proj_type, proj_val, unsafe);
+            } else {
+                new_d = mk_theorem(proj_name, lvl_params, proj_type, proj_val);
+            }
+        } else {
+            new_d = mk_definition_inferring_unsafe(env, proj_name, lvl_params, proj_type, proj_val,
                                                            reducibility_hints::mk_abbreviation());
+        }
         new_env = new_env.add(new_d);
-        if (!inst_implicit)
+        if (!inst_implicit && !is_prop)
             new_env = set_reducible(new_env, proj_name, reducible_status::Reducible, true);
         new_env = save_projection_info(new_env, proj_name, cnstr_info.get_name(), nparams, i, inst_implicit);
-        expr proj         = mk_app(mk_app(mk_constant(proj_name, lvls), params), c);
+        expr proj    = mk_app(mk_app(mk_constant(proj_name, lvls), params), c);
         cnstr_type   = instantiate(binding_body(cnstr_type), proj);
         i++;
     }

src/runtime/utf8.cpp

@@ -247,7 +247,7 @@ bool validate_utf8(uint8_t const * str, size_t size) {
             if ((c1 & 0xc0) != 0x80 || (c2 & 0xc0) != 0x80) return false;
 
             unsigned r = ((c & 0x0f) << 12) | ((c1 & 0x3f) << 6) | (c2 & 0x3f);
-            if (r < 0x800 || (r >= 0xD800 && r < 0xDFFF)) return false;
+            if (r < 0x800 || (r >= 0xD800 && r <= 0xDFFF)) return false;
 
             i += 3;
         } else if ((c & 0xf8) == 0xf0) {

src/util/shell.cpp

@@ -217,6 +217,7 @@ static void display_help(std::ostream & out) {
 #endif
     std::cout << "  --plugin=file      load and initialize Lean shared library for registering linters etc.\n";
     std::cout << "  --load-dynlib=file load shared library to make its symbols available to the interpreter\n";
+    std::cout << "  --json             report Lean output (e.g., messages) as JSON (one per line)\n";
     std::cout << "  --deps             just print dependencies of a Lean input\n";
     std::cout << "  --print-prefix     print the installation prefix for Lean and exit\n";
     std::cout << "  --print-libdir     print the installation directory for Lean's built-in libraries and exit\n";
@@ -230,6 +231,7 @@ static void display_help(std::ostream & out) {
 
 static int print_prefix = 0;
 static int print_libdir = 0;
+static int json_output = 0;
 
 static struct option g_long_options[] = {
     {"version",      no_argument,       0, 'v'},
@@ -260,6 +262,7 @@ static struct option g_long_options[] = {
 #endif
     {"plugin",       required_argument, 0, 'p'},
     {"load-dynlib",  required_argument, 0, 'l'},
+    {"json",         no_argument,       &json_output, 1},
     {"print-prefix", no_argument,       &print_prefix, 1},
     {"print-libdir", no_argument,       &print_libdir, 1},
 #ifdef LEAN_DEBUG
@@ -346,6 +349,7 @@ extern "C" object * lean_run_frontend(
     object * main_module_name,
     uint32_t trust_level,
     object * ilean_filename,
+    uint8_t  json_output,
     object * w
 );
 pair_ref<environment, object_ref> run_new_frontend(
@@ -353,7 +357,8 @@ pair_ref<environment, object_ref> run_new_frontend(
     options const & opts, std::string const & file_name,
     name const & main_module_name,
     uint32_t trust_level,
-    optional<std::string> const & ilean_file_name
+    optional<std::string> const & ilean_file_name,
+    uint8_t json
 ) {
     object * oilean_file_name = mk_option_none();
     if (ilean_file_name) {
@@ -366,6 +371,7 @@ pair_ref<environment, object_ref> run_new_frontend(
         main_module_name.to_obj_arg(),
         trust_level,
         oilean_file_name,
+        json_output,
         io_mk_world()
     ));
 }
@@ -716,7 +722,7 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) {
 
         if (!main_module_name)
             main_module_name = name("_stdin");
-        pair_ref<environment, object_ref> r = run_new_frontend(contents, opts, mod_fn, *main_module_name, trust_lvl, ilean_fn);
+        pair_ref<environment, object_ref> r = run_new_frontend(contents, opts, mod_fn, *main_module_name, trust_lvl, ilean_fn, json_output);
         env = r.fst();
         bool ok = unbox(r.snd().raw());
 

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/3989_1.lean

@@ -0,0 +1,3 @@
+def foo (ty : Expr) : MetaM Expr :=
+  match_expr ty with
+  | Nat => sorry

tests/lean/3989_1.lean.expected.out

@@ -0,0 +1 @@
+3989_1.lean:4:0: error: expected else-alternative for `match_expr`, i.e., `| _ => ...`

tests/lean/3989_2.lean

@@ -0,0 +1,6 @@
+def foo (ty : Expr) : MetaM Expr :=
+  match_expr ty with
+  | Nat => sorry
+  | BitVec n => sorry
+
+#check Nat

tests/lean/3989_2.lean.expected.out

@@ -0,0 +1,2 @@
+3989_2.lean:6:0: error: expected else-alternative for `match_expr`, i.e., `| _ => ...`
+Nat : Type

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/2575.lean

@@ -0,0 +1,12 @@
+structure AtLeastThirtySeven where
+  val : Nat
+  le : 37 ≤ val
+
+theorem AtLeastThirtySeven.lt (x : AtLeastThirtySeven) : 36 < x.val := x.le
+
+/--
+info: theorem AtLeastThirtySeven.le : ∀ (self : AtLeastThirtySeven), 37 ≤ self.val :=
+fun self => self.2
+-/
+#guard_msgs in
+#print AtLeastThirtySeven.le

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