fix: mismatch between TheoremVal in Lean and C++

This is a major refactor of Lake's build code.  The key changes:

* **Job Registration**: Significant build jobs are now registered by
build functions. The DSL inserts this registration automatically into
user-defined targets and facets, so this change should require no
end-user adaption. Registered jobs are incrementally awaited by the main
build function and the progress counter now indicates how many of these
jobs are completed and left-to-await. On the positive side, this means
the counter is now always accurate. On the negative side, this means
that jobs are displayed even if they are no-ops (i.e., if the target is
already up-to-date).

* **Log Retention**: Logs are now part of a Lake monad's state instead
of being eagerly printed. As a result, build jobs retain their logs.
Using this change, logs are are now always printed after their
associated caption (e.g., `[X/Y] Building Foo`) and are not arbitrarily
interleaved with the output of other jobs.

* **Simplify the build monad stack**: Previously, there was a lot of
confused mixing between the various build monads in the codebase (i.e.,
`JobM`, `ScedulerM`, `BuildM`, `RecBuildM`, and `IndexBuildM` ). This
refactor attempts to make there use more consistent and straightforward:
* `FetchM` (formerly `IndexBuildM`) is the top-level build monad used by
targets and facets and is now uniformly used in the codebase for all
top-level build functions.
* `JobM` is the monad of asynchronous build jobs. It is more limited
than `FetchM` due to the fact that the build cache can not be modified
asynchronously.
* `SpawnM` (formerly `SchedulerM`) is the monad used to spawn build
jobs. It lifts into `FetchM`.
* `RecBuildM` and `CoreBuildM` (formerly `BuildM`) have been relegated
to internal details of how `FetchM` / `JobM` are implemented / run and
are no longer used outside of that context.

* **Pretty progress.** Build progress (e.g., `[X/Y] Building Foo`) is
now updated on a single line via ANSI escape sequences when Lake is
outputting to a terminal. Redirected Lake output still sees progress on
separate lines.

* **Warnings-as-error option.** Adds a `--wfail` option to Lake that
will cause a build to fail if Lake logs any warnings doing a build.
Unlike some systems, this does not convert warnings into errors and it
does not abort jobs which log warnings. Instead, only the top-level
build fails.

* **Build log cache.** Logs from builds are now cached to a file and
replayed when the build is revisited. For example, this means multiple
runs of a `--wfail` Lean build (without changes) will still produce the
same warnings even though there is now an up-to-date `.olean` for the
module.

 Closes #2349. Closes #2764.

.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,6 @@
 /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

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/CMakeLists.txt

@@ -315,6 +315,12 @@ endif()
 string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
 string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
 
+# in local builds, link executables and not just dynlibs against C++ stdlib as well,
+# which is required for e.g. asan
+if(NOT LEAN_STANDALONE)
+  string(APPEND CMAKE_EXE_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
+endif()
+
 # flags for user binaries = flags for toolchain binaries + Lake
 string(APPEND LEANC_STATIC_LINKER_FLAGS " ${TOOLCHAIN_STATIC_LINKER_FLAGS} -lLake")
 

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

@@ -31,6 +31,7 @@ def ofFn {n} (f : Fin n → α) : Array α := go 0 (mkEmpty n) where
   go (i : Nat) (acc : Array α) : Array α :=
     if h : i < n then go (i+1) (acc.push (f ⟨i, h⟩)) else acc
 termination_by n - i
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 /-- The array `#[0, 1, ..., n - 1]`. -/
 def range (n : Nat) : Array Nat :=
@@ -306,6 +307,7 @@ def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α
     else
       pure r
   termination_by as.size - i
+  decreasing_by simp_wf; decreasing_trivial_pre_omega
   map 0 (mkEmpty as.size)
 
 @[inline]
@@ -378,6 +380,7 @@ def anyM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as :
       else
         pure false
       termination_by stop - j
+      decreasing_by simp_wf; decreasing_trivial_pre_omega
     loop start
   if h : stop ≤ as.size then
     any stop h
@@ -463,6 +466,7 @@ def findIdx? {α : Type u} (as : Array α) (p : α → Bool) : Option Nat :=
       if p as[j] then some j else loop (j + 1)
     else none
     termination_by as.size - j
+    decreasing_by simp_wf; decreasing_trivial_pre_omega
   loop 0
 
 def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat :=
@@ -557,6 +561,7 @@ def isEqvAux (a b : Array α) (hsz : a.size = b.size) (p : α → α → Bool) (
   else
     true
 termination_by a.size - i
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 @[inline] def isEqv (a b : Array α) (p : α → α → Bool) : Bool :=
   if h : a.size = b.size then
@@ -661,6 +666,7 @@ def indexOfAux [BEq α] (a : Array α) (v : α) (i : Nat) : Option (Fin a.size)
     else indexOfAux a v (i+1)
   else none
 termination_by a.size - i
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 def indexOf? [BEq α] (a : Array α) (v : α) : Option (Fin a.size) :=
   indexOfAux a v 0
@@ -703,6 +709,7 @@ def popWhile (p : α → Bool) (as : Array α) : Array α :=
   else
     as
 termination_by as.size
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 def takeWhile (p : α → Bool) (as : Array α) : Array α :=
   let rec go (i : Nat) (r : Array α) : Array α :=
@@ -715,6 +722,7 @@ def takeWhile (p : α → Bool) (as : Array α) : Array α :=
     else
       r
     termination_by as.size - i
+    decreasing_by simp_wf; decreasing_trivial_pre_omega
   go 0 #[]
 
 /-- Remove the element at a given index from an array without bounds checks, using a `Fin` index.
@@ -731,6 +739,7 @@ def feraseIdx (a : Array α) (i : Fin a.size) : Array α :=
   else
     a.pop
 termination_by a.size - i.val
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 theorem size_feraseIdx (a : Array α) (i : Fin a.size) : (a.feraseIdx i).size = a.size - 1 := by
   induction a, i using Array.feraseIdx.induct with
@@ -763,6 +772,7 @@ def erase [BEq α] (as : Array α) (a : α) : Array α :=
     else
       as
     termination_by j.1
+    decreasing_by simp_wf; decreasing_trivial_pre_omega
   let j := as.size
   let as := as.push a
   loop as ⟨j, size_push .. ▸ j.lt_succ_self⟩
@@ -816,6 +826,7 @@ def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : N
   else
     true
 termination_by as.size - i
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 /-- Return true iff `as` is a prefix of `bs`.
 That is, `bs = as ++ t` for some `t : List α`.-/
@@ -837,6 +848,7 @@ private def allDiffAux [BEq α] (as : Array α) (i : Nat) : Bool :=
   else
     true
 termination_by as.size - i
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 def allDiff [BEq α] (as : Array α) : Bool :=
   allDiffAux as 0
@@ -852,6 +864,7 @@ def allDiff [BEq α] (as : Array α) : Bool :=
   else
     cs
 termination_by as.size - i
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 @[inline] def zipWith (as : Array α) (bs : Array β) (f : α → β → γ) : Array γ :=
   zipWithAux f as bs 0 #[]

src/Init/Data/Array/BasicAux.lean

@@ -48,6 +48,7 @@ where
       let b ← f as[i]
       go (i+1) ⟨acc.val.push b, by simp [acc.property]⟩ hlt
   termination_by as.size - i
+  decreasing_by decreasing_trivial_pre_omega
 
 @[inline] private unsafe def mapMonoMImp [Monad m] (as : Array α) (f : α → m α) : m (Array α) :=
   go 0 as

src/Init/Data/Array/DecidableEq.lean

@@ -21,6 +21,8 @@ theorem eq_of_isEqvAux [DecidableEq α] (a b : Array α) (hsz : a.size = b.size)
     subst heq
     exact absurd (Nat.lt_of_lt_of_le high low) (Nat.lt_irrefl j)
 termination_by a.size - i
+decreasing_by decreasing_trivial_pre_omega
+
 
 theorem eq_of_isEqv [DecidableEq α] (a b : Array α) : Array.isEqv a b (fun x y => x = y) → a = b := by
   simp [Array.isEqv]
@@ -37,6 +39,7 @@ theorem isEqvAux_self [DecidableEq α] (a : Array α) (i : Nat) : Array.isEqvAux
   case inl h => simp [h, isEqvAux_self a (i+1)]
   case inr h => simp [h]
 termination_by a.size - i
+decreasing_by decreasing_trivial_pre_omega
 
 theorem isEqv_self [DecidableEq α] (a : Array α) : Array.isEqv a a (fun x y => x = y) = true := by
   simp [isEqv, isEqvAux_self]

src/Init/Data/Array/Lemmas.lean

@@ -131,6 +131,7 @@ where
       simp [aux (i+1), map_eq_pure_bind]; rfl
     · rw [List.drop_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
   termination_by arr.size - i
+  decreasing_by decreasing_trivial_pre_omega
 
 @[simp] theorem map_data (f : α → β) (arr : Array α) : (arr.map f).data = arr.data.map f := by
   rw [map, mapM_eq_foldlM]

src/Init/Data/Array/Mem.lean

@@ -27,13 +27,20 @@ theorem sizeOf_lt_of_mem [SizeOf α] {as : Array α} (h : a ∈ as) : sizeOf a <
   cases as with | _ as =>
   exact Nat.lt_trans (List.sizeOf_get ..) (by simp_arith)
 
+@[simp] theorem sizeOf_getElem [SizeOf α] (as : Array α) (i : Nat) (h : i < as.size) :
+  sizeOf (as[i]'h) < sizeOf as := sizeOf_get _ _
+
 /-- This tactic, added to the `decreasing_trivial` toolbox, proves that
 `sizeOf arr[i] < sizeOf arr`, which is useful for well founded recursions
 over a nested inductive like `inductive T | mk : Array T → T`. -/
 macro "array_get_dec" : tactic =>
   `(tactic| first
-    | apply sizeOf_get
-    | apply Nat.lt_trans (sizeOf_get ..); simp_arith)
+    -- subsumed by simp
+    -- | with_reducible apply sizeOf_get
+    -- | with_reducible apply sizeOf_getElem
+    | (with_reducible apply Nat.lt_trans (sizeOf_get ..)); simp_arith
+    | (with_reducible apply Nat.lt_trans (sizeOf_getElem ..)); simp_arith
+    )
 
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| array_get_dec)
 
@@ -43,9 +50,10 @@ provided that `a ∈ arr` which is useful for well founded recursions over a nes
 -- NB: This is analogue to tactic `sizeOf_list_dec`
 macro "array_mem_dec" : tactic =>
   `(tactic| first
-    | apply Array.sizeOf_lt_of_mem; assumption; done
-    | apply Nat.lt_trans (Array.sizeOf_lt_of_mem ?h)
-      case' h => assumption
+    | with_reducible apply Array.sizeOf_lt_of_mem; assumption; done
+    | with_reducible
+        apply Nat.lt_trans (Array.sizeOf_lt_of_mem ?h)
+        case' h => assumption
       simp_arith)
 
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| array_mem_dec)

src/Init/Data/Array/QSort.lean

@@ -27,6 +27,7 @@ def qpartition (as : Array α) (lt : α → α → Bool) (lo hi : Nat) : Nat ×
       let as := as.swap! i hi
       (i, as)
     termination_by hi - j
+    decreasing_by all_goals simp_wf; decreasing_trivial_pre_omega
   loop as lo lo
 
 @[inline] partial def qsort (as : Array α) (lt : α → α → Bool) (low := 0) (high := as.size - 1) : 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/Fold.lean

@@ -12,6 +12,7 @@ import Init.Data.Nat.Linear
   loop (x : α) (i : Nat) : α :=
     if h : i < n then loop (f x ⟨i, h⟩) (i+1) else x
   termination_by n - i
+  decreasing_by decreasing_trivial_pre_omega
 
 /-- Folds over `Fin n` from the right: `foldr 3 f x = f 0 (f 1 (f 2 x))`. -/
 @[inline] def foldr (n) (f : Fin n → α → α) (init : α) : α := loop ⟨n, Nat.le_refl n⟩ init where

src/Init/Data/Fin/Iterate.lean

@@ -23,6 +23,7 @@ def hIterateFrom (P : Nat → Sort _) {n} (f : ∀(i : Fin n), P i.val → P (i.
     have p : i = n := (or_iff_left g).mp (Nat.eq_or_lt_of_le ubnd)
     _root_.cast (congrArg P p) a
   termination_by n - i
+  decreasing_by decreasing_trivial_pre_omega
 
 /--
 `hIterate` is a heterogenous iterative operation that applies a

src/Init/Data/Fin/Lemmas.lean

@@ -602,6 +602,7 @@ A version of `Fin.succRec` taking `i : Fin n` as the first argument. -/
     @Fin.succRecOn (n + 1) i.succ motive zero succ = succ n i (Fin.succRecOn i zero succ) := by
   cases i; rfl
 
+
 /-- Define `motive i` by induction on `i : Fin (n + 1)` via induction on the underlying `Nat` value.
 This function has two arguments: `zero` handles the base case on `motive 0`,
 and `succ` defines the inductive step using `motive i.castSucc`.
@@ -610,8 +611,12 @@ and `succ` defines the inductive step using `motive i.castSucc`.
 @[elab_as_elim] def induction {motive : Fin (n + 1) → Sort _} (zero : motive 0)
     (succ : ∀ i : Fin n, motive (castSucc i) → motive i.succ) :
     ∀ i : Fin (n + 1), motive i
-  | ⟨0, hi⟩ => by rwa [Fin.mk_zero]
-  | ⟨i+1, hi⟩ => succ ⟨i, Nat.lt_of_succ_lt_succ hi⟩ (induction zero succ ⟨i, Nat.lt_of_succ_lt hi⟩)
+  | ⟨i, hi⟩ => go i hi
+where
+  -- Use a curried function so that this is structurally recursive
+  go : ∀ (i : Nat) (hi : i < n + 1), motive ⟨i, hi⟩
+  | 0, hi => by rwa [Fin.mk_zero]
+  | i+1, hi => succ ⟨i, Nat.lt_of_succ_lt_succ hi⟩ (go i (Nat.lt_of_succ_lt hi))
 
 @[simp] theorem induction_zero {motive : Fin (n + 1) → Sort _} (zero : motive 0)
     (hs : ∀ i : Fin n, motive (castSucc i) → motive i.succ) :
@@ -793,15 +798,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

@@ -157,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
@@ -167,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
@@ -212,9 +226,10 @@ theorem sizeOf_lt_of_mem [SizeOf α] {as : List α} (h : a ∈ as) : sizeOf a <
 over a nested inductive like `inductive T | mk : List T → T`. -/
 macro "sizeOf_list_dec" : tactic =>
   `(tactic| first
-    | apply sizeOf_lt_of_mem; assumption; done
-    | apply Nat.lt_trans (sizeOf_lt_of_mem ?h)
-      case' h => assumption
+    | with_reducible apply sizeOf_lt_of_mem; assumption; done
+    | with_reducible
+        apply Nat.lt_trans (sizeOf_lt_of_mem ?h)
+        case' h => assumption
       simp_arith)
 
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| sizeOf_list_dec)
@@ -297,6 +312,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/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/String/Extra.lean

@@ -132,13 +132,17 @@ theorem Iterator.sizeOf_next_lt_of_hasNext (i : String.Iterator) (h : i.hasNext)
   cases i; rename_i s pos; simp [Iterator.next, Iterator.sizeOf_eq]; simp [Iterator.hasNext] at h
   exact Nat.sub_lt_sub_left h (String.lt_next s pos)
 
-macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply String.Iterator.sizeOf_next_lt_of_hasNext; assumption)
+macro_rules
+| `(tactic| decreasing_trivial) =>
+  `(tactic| with_reducible apply String.Iterator.sizeOf_next_lt_of_hasNext; assumption)
 
 theorem Iterator.sizeOf_next_lt_of_atEnd (i : String.Iterator) (h : ¬ i.atEnd = true) : sizeOf i.next < sizeOf i :=
   have h : i.hasNext := decide_eq_true <| Nat.gt_of_not_le <| mt decide_eq_true h
   sizeOf_next_lt_of_hasNext i h
 
-macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply String.Iterator.sizeOf_next_lt_of_atEnd; assumption)
+macro_rules
+| `(tactic| decreasing_trivial) =>
+  `(tactic| with_reducible apply String.Iterator.sizeOf_next_lt_of_atEnd; assumption)
 
 namespace Iterator
 

src/Init/Meta.lean

@@ -1057,6 +1057,7 @@ where
     else
       Syntax.mkCApp (Name.mkStr2 "Array" ("mkArray" ++ toString xs.size)) args
   termination_by xs.size - i
+  decreasing_by decreasing_trivial_pre_omega
 
 instance [Quote α `term] : Quote (Array α) `term where
   quote := quoteArray

src/Init/Notation.lean

@@ -296,7 +296,7 @@ macro_rules | `($x - $y)   => `(binop% HSub.hSub $x $y)
 macro_rules | `($x * $y)   => `(binop% HMul.hMul $x $y)
 macro_rules | `($x / $y)   => `(binop% HDiv.hDiv $x $y)
 macro_rules | `($x % $y)   => `(binop% HMod.hMod $x $y)
--- exponentiation should be considered a right action (#2220)
+-- exponentiation should be considered a right action (#2854)
 macro_rules | `($x ^ $y)   => `(rightact% HPow.hPow $x $y)
 macro_rules | `($x ++ $y)  => `(binop% HAppend.hAppend $x $y)
 macro_rules | `(- $x)      => `(unop% Neg.neg $x)
@@ -492,9 +492,12 @@ The attribute `@[deprecated]` on a declaration indicates that the declaration
 is discouraged for use in new code, and/or should be migrated away from in
 existing code. It may be removed in a future version of the library.
 
-`@[deprecated myBetterDef]` means that `myBetterDef` is the suggested replacement.
+* `@[deprecated myBetterDef]` means that `myBetterDef` is the suggested replacement.
+* `@[deprecated myBetterDef "use myBetterDef instead"]` allows customizing the deprecation message.
+* `@[deprecated (since := "2024-04-21")]` records when the deprecation was first applied.
 -/
-syntax (name := deprecated) "deprecated" (ppSpace ident)? : attr
+syntax (name := deprecated) "deprecated" (ppSpace ident)? (ppSpace str)?
+    (" (" &"since" " := " str ")")? : attr
 
 /--
 The `@[coe]` attribute on a function (which should also appear in a

src/Init/Prelude.lean

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

src/Init/SimpLemmas.lean

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

src/Init/Tactics.lean

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

src/Init/WFTactics.lean

@@ -25,9 +25,16 @@ syntax "decreasing_trivial" : tactic
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| (simp (config := { arith := true, failIfUnchanged := false })) <;> done)
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| omega)
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| assumption)
-macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply Nat.sub_succ_lt_self; assumption) -- a - (i+1) < a - i if i < a
-macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply Nat.pred_lt'; assumption) -- i-1 < i if j < i
-macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply Nat.pred_lt; assumption)  -- i-1 < i if i ≠ 0
+
+/--
+Variant of `decreasing_trivial` that does not use `omega`, intended to be used in core modules
+before `omega` is available.
+-/
+syntax "decreasing_trivial_pre_omega" : tactic
+macro_rules | `(tactic| decreasing_trivial_pre_omega) => `(tactic| apply Nat.sub_succ_lt_self; assumption) -- a - (i+1) < a - i if i < a
+macro_rules | `(tactic| decreasing_trivial_pre_omega) => `(tactic| apply Nat.pred_lt'; assumption) -- i-1 < i if j < i
+macro_rules | `(tactic| decreasing_trivial_pre_omega) => `(tactic| apply Nat.pred_lt; assumption)  -- i-1 < i if i ≠ 0
+
 
 /-- Constructs a proof of decreasing along a well founded relation, by applying
 lexicographic order lemmas and using `ts` to solve the base case. If it fails,

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/Compiler/ExternAttr.lean

@@ -66,12 +66,13 @@ builtin_initialize externAttr : ParametricAttribute ExternAttrData ←
     descr := "builtin and foreign functions"
     getParam := fun _ stx => syntaxToExternAttrData stx
     afterSet := fun declName _ => do
-      let mut env ← getEnv
-      if env.isProjectionFn declName || env.isConstructor declName then do
-        env ← ofExcept <| addExtern env declName
+      let env ← getEnv
+      if env.isProjectionFn declName || env.isConstructor declName then
+        if let some (.thmInfo ..) := env.find? declName then
+          -- We should not mark theorems as extern
+          return ()
+        let env ← ofExcept <| addExtern env declName
         setEnv env
-      else
-        pure ()
   }
 
 @[export lean_get_extern_attr_data]
@@ -155,7 +156,7 @@ private def getExternConstArity (declName : Name) : CoreM Nat := do
 @[export lean_get_extern_const_arity]
 def getExternConstArityExport (env : Environment) (declName : Name) : IO (Option Nat) := do
   try
-    let (arity, _) ← (getExternConstArity declName).toIO { fileName := "<compiler>", fileMap := default } { env := env }
+    let (arity, _) ← (getExternConstArity declName).toIO { fileName := "<compiler>", fileMap := default, diag := false } { env := env }
     return some arity
   catch
    | IO.Error.userError _   => return none

src/Lean/Compiler/IR/RC.lean

@@ -9,9 +9,10 @@ import Lean.Compiler.IR.CompilerM
 import Lean.Compiler.IR.LiveVars
 
 namespace Lean.IR.ExplicitRC
-/-! Insert explicit RC instructions. So, it assumes the input code does not contain `inc` nor `dec` instructions.
-   This transformation is applied before lower level optimizations
-   that introduce the instructions `release` and `set`
+/-!
+Insert explicit RC instructions. So, it assumes the input code does not contain `inc` nor `dec` instructions.
+This transformation is applied before lower level optimizations
+that introduce the instructions `release` and `set`
 -/
 
 structure VarInfo where

src/Lean/Compiler/IR/ResetReuse.lean

@@ -9,21 +9,24 @@ import Lean.Compiler.IR.LiveVars
 import Lean.Compiler.IR.Format
 
 namespace Lean.IR.ResetReuse
-/-! Remark: the insertResetReuse transformation is applied before we have
-   inserted `inc/dec` instructions, and performed lower level optimizations
-   that introduce the instructions `release` and `set`. -/
+/-!
+Remark: the insertResetReuse transformation is applied before we have
+inserted `inc/dec` instructions, and performed lower level optimizations
+that introduce the instructions `release` and `set`.
+-/
 
-/-! Remark: the functions `S`, `D` and `R` defined here implement the
-  corresponding functions in the paper "Counting Immutable Beans"
+/-!
+Remark: the functions `S`, `D` and `R` defined here implement the
+corresponding functions in the paper "Counting Immutable Beans"
 
-  Here are the main differences:
-  - We use the State monad to manage the generation of fresh variable names.
-  - Support for join points, and `uset` and `sset` instructions for unboxed data.
-  - `D` uses the auxiliary function `Dmain`.
-  - `Dmain` returns a pair `(b, found)` to avoid quadratic behavior when checking
-    the last occurrence of the variable `x`.
-  - Because we have join points in the actual implementation, a variable may be live even if it
-    does not occur in a function body. See example at `livevars.lean`.
+Here are the main differences:
+- We use the State monad to manage the generation of fresh variable names.
+- Support for join points, and `uset` and `sset` instructions for unboxed data.
+- `D` uses the auxiliary function `Dmain`.
+- `Dmain` returns a pair `(b, found)` to avoid quadratic behavior when checking
+  the last occurrence of the variable `x`.
+- Because we have join points in the actual implementation, a variable may be live even if it
+  does not occur in a function body. See example at `livevars.lean`.
 -/
 
 private def mayReuse (c₁ c₂ : CtorInfo) : Bool :=
@@ -33,39 +36,68 @@ private def mayReuse (c₁ c₂ : CtorInfo) : Bool :=
      because it produces counterintuitive behavior. -/
   c₁.name.getPrefix == c₂.name.getPrefix
 
+/--
+Replace `ctor` applications with `reuse` applications if compatible.
+`w` contains the "memory cell" being reused.
+-/
 private partial def S (w : VarId) (c : CtorInfo) : FnBody → FnBody
-  | FnBody.vdecl x t v@(Expr.ctor c' ys) b   =>
+  | .vdecl x t v@(.ctor c' ys) b   =>
     if mayReuse c c' then
       let updtCidx := c.cidx != c'.cidx
-      FnBody.vdecl x t (Expr.reuse w c' updtCidx ys) b
+      .vdecl x t (.reuse w c' updtCidx ys) b
     else
-      FnBody.vdecl x t v (S w c b)
-  | FnBody.jdecl j ys v b   =>
+      .vdecl x t v (S w c b)
+  | .jdecl j ys v b   =>
     let v' := S w c v
-    if v == v' then FnBody.jdecl j ys v (S w c b)
-    else FnBody.jdecl j ys v' b
-  | FnBody.case tid x xType alts    => FnBody.case tid x xType <| alts.map fun alt => alt.modifyBody (S w c)
+    if v == v' then
+      .jdecl j ys v (S w c b)
+    else
+      .jdecl j ys v' b
+  | .case tid x xType alts =>
+    .case tid x xType <| alts.map fun alt => alt.modifyBody (S w c)
   | b =>
-    if b.isTerminal then b
+    if b.isTerminal then
+      b
     else let
       (instr, b) := b.split
       instr.setBody (S w c b)
 
+structure Context where
+  lctx      : LocalContext := {}
+  /--
+  Contains all variables in `cases` statements in the current path.
+  We use this information to prevent double-reset in code such as
+  ```
+  case x_i : obj of
+  Prod.mk →
+    case x_i : obj of
+    Prod.mk →
+    ...
+  ```
+  -/
+  casesVars : PHashSet VarId := {}
+
 /-- We use `Context` to track join points in scope. -/
-abbrev M := ReaderT LocalContext (StateT Index Id)
+abbrev M := ReaderT Context (StateT Index Id)
 
 private def mkFresh : M VarId := do
-  let idx ← getModify (fun n => n + 1)
-  pure { idx := idx }
+  let idx ← getModify fun n => n + 1
+  return { idx := idx }
 
+/--
+Helper function for applying `S`. We only introduce a `reset` if we managed
+to replace a `ctor` withe `reuse` in `b`.
+-/
 private def tryS (x : VarId) (c : CtorInfo) (b : FnBody) : M FnBody := do
   let w ← mkFresh
   let b' := S w c b
-  if b == b' then pure b
-  else pure $ FnBody.vdecl w IRType.object (Expr.reset c.size x) b'
+  if b == b' then
+    return b
+  else
+    return .vdecl w IRType.object (.reset c.size x) b'
 
 private def Dfinalize (x : VarId) (c : CtorInfo) : FnBody × Bool → M FnBody
-  | (b, true)  => pure b
+  | (b, true)  => return b
   | (b, false) => tryS x c b
 
 private def argsContainsVar (ys : Array Arg) (x : VarId) : Bool :=
@@ -75,75 +107,85 @@ private def argsContainsVar (ys : Array Arg) (x : VarId) : Bool :=
 
 private def isCtorUsing (b : FnBody) (x : VarId) : Bool :=
   match b with
-  | (FnBody.vdecl _ _ (Expr.ctor _ ys) _) => argsContainsVar ys x
+  | .vdecl _ _ (.ctor _ ys) _ => argsContainsVar ys x
   | _ => false
 
-/-- Given `Dmain b`, the resulting pair `(new_b, flag)` contains the new body `new_b`,
-   and `flag == true` if `x` is live in `b`.
+/--
+Given `Dmain b`, the resulting pair `(new_b, flag)` contains the new body `new_b`,
+and `flag == true` if `x` is live in `b`.
 
-   Note that, in the function `D` defined in the paper, for each `let x := e; F`,
-   `D` checks whether `x` is live in `F` or not. This is great for clarity but it
-   is expensive: `O(n^2)` where `n` is the size of the function body. -/
-private partial def Dmain (x : VarId) (c : CtorInfo) : FnBody → M (FnBody × Bool)
-  | e@(FnBody.case tid y yType alts) => do
-    let ctx ← read
-    if e.hasLiveVar ctx x then do
+Note that, in the function `D` defined in the paper, for each `let x := e; F`,
+`D` checks whether `x` is live in `F` or not. This is great for clarity but it
+is expensive: `O(n^2)` where `n` is the size of the function body. -/
+private partial def Dmain (x : VarId) (c : CtorInfo) (e : FnBody) : M (FnBody × Bool) := do
+  match e with
+  | .case tid y yType alts =>
+    if e.hasLiveVar (← read).lctx x then
       /- If `x` is live in `e`, we recursively process each branch. -/
       let alts ← alts.mapM fun alt => alt.mmodifyBody fun b => Dmain x c b >>= Dfinalize x c
-      pure (FnBody.case tid y yType alts, true)
-    else pure (e, false)
-  | FnBody.jdecl j ys v b   => do
-    let (b, found) ← withReader (fun ctx => ctx.addJP j ys v) (Dmain x c b)
+      return (.case tid y yType alts, true)
+    else
+      return (e, false)
+  | .jdecl j ys v b =>
+    let (b, found) ← withReader (fun ctx => { ctx with lctx := ctx.lctx.addJP j ys v }) (Dmain x c b)
     let (v, _ /- found' -/) ← Dmain x c v
     /- If `found' == true`, then `Dmain b` must also have returned `(b, true)` since
        we assume the IR does not have dead join points. So, if `x` is live in `j` (i.e., `v`),
        then it must also live in `b` since `j` is reachable from `b` with a `jmp`.
        On the other hand, `x` may be live in `b` but dead in `j` (i.e., `v`). -/
-    pure (FnBody.jdecl j ys v b, found)
-  | e => do
-    let ctx ← read
+    return (.jdecl j ys v b, found)
+  | e =>
     if e.isTerminal then
-      pure (e, e.hasLiveVar ctx x)
+      return (e, e.hasLiveVar (← read).lctx x)
     else do
       let (instr, b) := e.split
       if isCtorUsing instr x then
         /- If the scrutinee `x` (the one that is providing memory) is being
            stored in a constructor, then reuse will probably not be able to reuse memory at runtime.
            It may work only if the new cell is consumed, but we ignore this case. -/
-        pure (e, true)
+        return (e, true)
       else
         let (b, found) ← Dmain x c b
         /- Remark: it is fine to use `hasFreeVar` instead of `hasLiveVar`
-           since `instr` is not a `FnBody.jmp` (it is not a terminal) nor it is a `FnBody.jdecl`. -/
+           since `instr` is not a `FnBody.jmp` (it is not a terminal) nor
+           it is a `FnBody.jdecl`. -/
         if found || !instr.hasFreeVar x then
-          pure (instr.setBody b, found)
+          return (instr.setBody b, found)
         else
           let b ← tryS x c b
-          pure (instr.setBody b, true)
+          return (instr.setBody b, true)
 
 private def D (x : VarId) (c : CtorInfo) (b : FnBody) : M FnBody :=
   Dmain x c b >>= Dfinalize x c
 
-partial def R : FnBody → M FnBody
-  | FnBody.case tid x xType alts   => do
+partial def R (e : FnBody) : M FnBody := do
+  match e with
+  | .case tid x xType alts =>
+    let alreadyFound := (← read).casesVars.contains x
+    withReader (fun ctx => { ctx with casesVars := ctx.casesVars.insert x }) do
       let alts ← alts.mapM fun alt => do
         let alt ← alt.mmodifyBody R
         match alt with
-        | Alt.ctor c b =>
-          if c.isScalar then pure alt
-          else Alt.ctor c <$> D x c b
-        | _            => pure alt
-      pure $ FnBody.case tid x xType alts
-  | FnBody.jdecl j ys v b   => do
+        | .ctor c b =>
+          if c.isScalar || alreadyFound then
+            -- If `alreadyFound`, then we don't try to reuse memory cell to avoid
+            -- double reset.
+            return alt
+          else
+            .ctor c <$> D x c b
+        | _ => return alt
+      return .case tid x xType alts
+  | .jdecl j ys v b =>
     let v ← R v
-    let b ← withReader (fun ctx => ctx.addJP j ys v) (R b)
-    pure $ FnBody.jdecl j ys v b
-  | e => do
-    if e.isTerminal then pure e
-    else do
+    let b ← withReader (fun ctx => { ctx with lctx := ctx.lctx.addJP j ys v }) (R b)
+    return .jdecl j ys v b
+  | e =>
+    if e.isTerminal then
+      return e
+    else
       let (instr, b) := e.split
       let b ← R b
-      pure (instr.setBody b)
+      return instr.setBody b
 
 end ResetReuse
 
@@ -151,7 +193,7 @@ open ResetReuse
 
 def Decl.insertResetReuse (d : Decl) : Decl :=
   match d with
-  | .fdecl (body := b) ..=>
+  | .fdecl (body := b) .. =>
     let nextIndex := d.maxIndex + 1
     let bNew      := (R b {}).run' nextIndex
     d.updateBody! bNew

src/Lean/CoreM.lean

@@ -13,13 +13,25 @@ import Lean.Elab.InfoTree.Types
 import Lean.MonadEnv
 
 namespace Lean
-namespace Core
+register_builtin_option diagnostics : Bool := {
+  defValue := false
+  group    := "diagnostics"
+  descr    := "collect diagnostic information"
+}
+
+register_builtin_option diagnostics.threshold : Nat := {
+  defValue := 20
+  group    := "diagnostics"
+  descr    := "only diagnostic counters above this threshold are reported by the definitional equality"
+}
 
 register_builtin_option maxHeartbeats : Nat := {
   defValue := 200000
   descr := "maximum amount of heartbeats per command. A heartbeat is number of (small) memory allocations (in thousands), 0 means no limit"
 }
 
+namespace Core
+
 builtin_initialize registerTraceClass `Kernel
 
 def getMaxHeartbeats (opts : Options) : Nat :=
@@ -72,6 +84,11 @@ structure Context where
   Recall that runtime exceptions are `maxRecDepth` or `maxHeartbeats`.
   -/
   catchRuntimeEx : Bool := false
+  /--
+  If `diag := true`, different parts of the system collect diagnostics.
+  Use the `set_option diag true` to set it to true.
+  -/
+  diag           : Bool := false
   deriving Nonempty
 
 /-- CoreM is a monad for manipulating the Lean environment.
@@ -206,7 +223,7 @@ def mkFreshUserName (n : Name) : CoreM Name :=
 instance [MetaEval α] : MetaEval (CoreM α) where
   eval env opts x _ := do
     let x : CoreM α := do try x finally printTraces
-    let (a, s) ← x.toIO { maxRecDepth := maxRecDepth.get opts, options := opts, fileName := "<CoreM>", fileMap := default } { env := env }
+    let (a, s) ← x.toIO { maxRecDepth := maxRecDepth.get opts, options := opts, fileName := "<CoreM>", fileMap := default, diag := diagnostics.get opts } { env := env }
     MetaEval.eval s.env opts a (hideUnit := true)
 
 -- withIncRecDepth for a monad `m` such that `[MonadControlT CoreM n]`
@@ -372,9 +389,17 @@ def addAndCompile (decl : Declaration) : CoreM Unit := do
   addDecl decl;
   compileDecl decl
 
+def getDiag (opts : Options) : Bool :=
+  diagnostics.get opts
+
+/-- Return `true` if diagnostic information collection is enabled. -/
+def isDiagnosticsEnabled : CoreM Bool :=
+  return (← read).diag
+
 def ImportM.runCoreM (x : CoreM α) : ImportM α := do
   let ctx ← read
-  let (a, _) ← x.toIO { options := ctx.opts, fileName := "<ImportM>", fileMap := default } { env := ctx.env }
+  let opts := ctx.opts
+  let (a, _) ← x.toIO { options := opts, fileName := "<ImportM>", fileMap := default, diag := getDiag opts } { env := ctx.env }
   return a
 
 /-- Return `true` if the exception was generated by one our resource limits. -/

src/Lean/Data/HashMap.lean

@@ -92,6 +92,7 @@ def moveEntries [Hashable α] (i : Nat) (source : Array (AssocList α β)) (targ
      moveEntries (i+1) source target
   else target
 termination_by source.size - i
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 def expand [Hashable α] (size : Nat) (buckets : HashMapBucket α β) : HashMapImp α β :=
   let bucketsNew : HashMapBucket α β := ⟨

src/Lean/Data/HashSet.lean

@@ -84,6 +84,7 @@ def moveEntries [Hashable α] (i : Nat) (source : Array (List α)) (target : Has
   else
     target
 termination_by source.size - i
+decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 def expand [Hashable α] (size : Nat) (buckets : HashSetBucket α) : HashSetImp α :=
   let bucketsNew : HashSetBucket α := ⟨

src/Lean/Declaration.lean

@@ -135,6 +135,11 @@ structure TheoremVal extends ConstantVal where
   all : List Name := [name]
   deriving Inhabited, BEq
 
+@[export lean_mk_theorem_val]
+def mkTheoremValEx (name : Name) (levelParams : List Name) (type : Expr) (value : Expr) (all : List Name) : TheoremVal := {
+  name, levelParams, type, value, all
+}
+
 /-- Value for an opaque constant declaration `opaque x : t := e` -/
 structure OpaqueVal extends ConstantVal where
   value : Expr

src/Lean/Elab/BuiltinNotation.lean

@@ -409,6 +409,8 @@ private def withLocalIdentFor (stx : Term) (e : Expr) (k : Term → TermElabM Ex
          let h ← elabTerm hStx none
          let hType ← inferType h
          let hTypeAbst ← kabstract hType lhs
+         unless hTypeAbst.hasLooseBVars do
+           throwError "invalid `▸` notation, the equality{indentExpr heq}\nhas type {indentExpr heqType}\nbut its left hand side is not mentioned in the type{indentExpr hType}"
          let motive ← mkMotive lhs hTypeAbst
          unless (← isTypeCorrect motive) do
            throwError "invalid `▸` notation, failed to compute motive for the substitution"

src/Lean/Elab/BuiltinTerm.lean

@@ -313,7 +313,7 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
 
 @[builtin_term_elab «set_option»] def elabSetOption : TermElab := fun stx expectedType? => do
   let options ← Elab.elabSetOption stx[1] stx[3]
-  withTheReader Core.Context (fun ctx => { ctx with maxRecDepth := maxRecDepth.get options, options := options }) do
+  withTheReader Core.Context (fun ctx => { ctx with maxRecDepth := maxRecDepth.get options, options := options, diag := getDiag options }) do
     elabTerm stx[5] expectedType?
 
 @[builtin_term_elab withAnnotateTerm] def elabWithAnnotateTerm : TermElab := fun stx expectedType? => do

src/Lean/Elab/Command.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Gabriel Ebner
 -/
 prelude
+import Lean.Meta.Diagnostics
 import Lean.Elab.Binders
 import Lean.Elab.SyntheticMVars
 import Lean.Elab.SetOption
@@ -138,7 +139,8 @@ private def mkCoreContext (ctx : Context) (s : State) (heartbeats : Nat) : Core.
     currNamespace  := scope.currNamespace
     openDecls      := scope.openDecls
     initHeartbeats := heartbeats
-    currMacroScope := ctx.currMacroScope }
+    currMacroScope := ctx.currMacroScope
+    diag           := getDiag scope.opts }
 
 private def addTraceAsMessagesCore (ctx : Context) (log : MessageLog) (traceState : TraceState) : MessageLog := Id.run do
   if traceState.traces.isEmpty then return log
@@ -411,7 +413,7 @@ def liftTermElabM (x : TermElabM α) : CommandElabM α := do
   -- make sure `observing` below also catches runtime exceptions (like we do by default in
   -- `CommandElabM`)
   let _ := MonadAlwaysExcept.except (m := TermElabM)
-  let x : MetaM _      := (observing x).run (mkTermContext ctx s) { levelNames := scope.levelNames }
+  let x : MetaM _      := (observing (try x finally Meta.reportDiag)).run (mkTermContext ctx s) { levelNames := scope.levelNames }
   let x : CoreM _      := x.run mkMetaContext {}
   let x : EIO _ _      := x.run (mkCoreContext ctx s heartbeats) { env := s.env, ngen := s.ngen, nextMacroScope := s.nextMacroScope, infoState.enabled := s.infoState.enabled, traceState := s.traceState }
   let (((ea, _), _), coreS) ← liftEIO x

src/Lean/Elab/Extra.lean

@@ -96,7 +96,7 @@ Here are brief descriptions of each of the operator types:
 - `rightact% f a b` elaborates `f a b` as a right action (the `b` operand "acts upon" the `a` operand).
   Only `a` participates in the protocol since `b` can have an unrelated type.
   This is used by `HPow` since, for example, there are both `Real -> Nat -> Real` and `Real -> Real -> Real`
-  exponentiation functions, and we prefer the former in the case of `x ^ 2`, but `binop%` would choose the latter. (#2220)
+  exponentiation functions, and we prefer the former in the case of `x ^ 2`, but `binop%` would choose the latter. (#2854)
 - There are also `binrel%` and `binrel_no_prop%` (see the docstring for `elabBinRelCore`).
 
 The elaborator works as follows:
@@ -449,7 +449,7 @@ def elabOp : TermElab := fun stx expectedType? => do
 
   - `binrel% R x y` elaborates `R x y` using the `binop%/...` expression trees in both `x` and `y`.
     It is similar to how `binop% R x y` elaborates but with a significant difference:
-    it does not use the expected type when computing the types of the operads.
+    it does not use the expected type when computing the types of the operands.
   - `binrel_no_prop% R x y` elaborates `R x y` like `binrel% R x y`, but if the resulting type for `x` and `y`
     is `Prop` they are coerced to `Bool`.
     This is used for relations such as `==` which do not support `Prop`, but we still want

src/Lean/Elab/InfoTree/Main.lean

@@ -102,7 +102,8 @@ def ContextInfo.runCoreM (info : ContextInfo) (x : CoreM α) : IO α := do
     have been used in `lctx` and `info.mctx`.
   -/
   (·.1) <$>
-    x.toIO { options := info.options, currNamespace := info.currNamespace, openDecls := info.openDecls, fileName := "<InfoTree>", fileMap := default }
+    x.toIO { options := info.options, currNamespace := info.currNamespace, openDecls := info.openDecls
+             fileName := "<InfoTree>", fileMap := default, diag := getDiag info.options }
            { env := info.env, ngen := info.ngen }
 
 def ContextInfo.runMetaM (info : ContextInfo) (lctx : LocalContext) (x : MetaM α) : IO α := do

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

@@ -163,7 +163,7 @@ private def getOptRotation (stx : Syntax) : Nat :=
 
 @[builtin_tactic Parser.Tactic.set_option] def elabSetOption : Tactic := fun stx => do
   let options ← Elab.elabSetOption stx[1] stx[3]
-  withTheReader Core.Context (fun ctx => { ctx with maxRecDepth := maxRecDepth.get options, options := options }) do
+  withTheReader Core.Context (fun ctx => { ctx with maxRecDepth := maxRecDepth.get options, options := options, diag := getDiag options }) do
     evalTactic stx[5]
 
 @[builtin_tactic Parser.Tactic.allGoals] def evalAllGoals : Tactic := fun stx => do

src/Lean/Elab/Tactic/LibrarySearch.lean

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

src/Lean/Level.lean

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

src/Lean/Linter/Deprecated.lean

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

src/Lean/Message.lean

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

src/Lean/Meta.lean

@@ -49,3 +49,4 @@ import Lean.Meta.LazyDiscrTree
 import Lean.Meta.LitValues
 import Lean.Meta.CheckTactic
 import Lean.Meta.Canonicalizer
+import Lean.Meta.Diagnostics

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.
@@ -258,6 +266,15 @@ structure PostponedEntry where
   ctx? : Option DefEqContext
   deriving Inhabited
 
+structure Diagnostics where
+  /-- Number of times each declaration has been unfolded -/
+  unfoldCounter : PHashMap Name Nat := {}
+  /-- Number of times `f a =?= f b` heuristic has been used per function `f`. -/
+  heuristicCounter : PHashMap Name Nat := {}
+  /-- Number of times a TC instance is used. -/
+  instanceCounter : PHashMap Name Nat := {}
+  deriving Inhabited
+
 /--
   `MetaM` monad state.
 -/
@@ -268,6 +285,7 @@ structure State where
   zetaDeltaFVarIds : FVarIdSet := {}
   /-- Array of postponed universe level constraints -/
   postponed        : PersistentArray PostponedEntry := {}
+  diag             : Diagnostics := {}
   deriving Inhabited
 
 /--
@@ -300,6 +318,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
@@ -421,7 +450,7 @@ section Methods
 variable [MonadControlT MetaM n] [Monad n]
 
 @[inline] def modifyCache (f : Cache → Cache) : MetaM Unit :=
-  modify fun { mctx, cache, zetaDeltaFVarIds, postponed } => { mctx, cache := f cache, zetaDeltaFVarIds, postponed }
+  modify fun { mctx, cache, zetaDeltaFVarIds, postponed, diag } => { mctx, cache := f cache, zetaDeltaFVarIds, postponed, diag }
 
 @[inline] def modifyInferTypeCache (f : InferTypeCache → InferTypeCache) : MetaM Unit :=
   modifyCache fun ⟨ic, c1, c2, c3, c4, c5, c6⟩ => ⟨f ic, c1, c2, c3, c4, c5, c6⟩
@@ -435,6 +464,28 @@ variable [MonadControlT MetaM n] [Monad n]
 @[inline] def resetDefEqPermCaches : MetaM Unit :=
   modifyDefEqPermCache fun _ => {}
 
+@[inline] def modifyDiag (f : Diagnostics → Diagnostics) : MetaM Unit := do
+  if (← isDiagnosticsEnabled) then
+    modify fun { mctx, cache, zetaDeltaFVarIds, postponed, diag } => { mctx, cache, zetaDeltaFVarIds, postponed, diag := f diag }
+
+/-- If diagnostics are enabled, record that `declName` has been unfolded. -/
+def recordUnfold (declName : Name) : MetaM Unit := do
+  modifyDiag fun { unfoldCounter, heuristicCounter, instanceCounter } =>
+    let newC := if let some c := unfoldCounter.find? declName then c + 1 else 1
+    { unfoldCounter := unfoldCounter.insert declName newC, heuristicCounter, instanceCounter }
+
+/-- If diagnostics are enabled, record that heuristic for solving `f a =?= f b` has been used. -/
+def recordDefEqHeuristic (declName : Name) : MetaM Unit := do
+  modifyDiag fun { unfoldCounter, heuristicCounter, instanceCounter } =>
+    let newC := if let some c := heuristicCounter.find? declName then c + 1 else 1
+    { unfoldCounter, heuristicCounter := heuristicCounter.insert declName newC, instanceCounter }
+
+/-- If diagnostics are enabled, record that instance `declName` was used during TC resolution. -/
+def recordInstance (declName : Name) : MetaM Unit := do
+  modifyDiag fun { unfoldCounter, heuristicCounter, instanceCounter } =>
+    let newC := if let some c := instanceCounter.find? declName then c + 1 else 1
+    { unfoldCounter, heuristicCounter, instanceCounter := instanceCounter.insert declName newC }
+
 def getLocalInstances : MetaM LocalInstances :=
   return (← read).localInstances
 
@@ -1690,6 +1741,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/Diagnostics.lean

@@ -0,0 +1,66 @@
+/-
+Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.PrettyPrinter
+import Lean.Meta.Basic
+import Lean.Meta.Instances
+
+namespace Lean.Meta
+
+private def collectAboveThreshold (counters : PHashMap Name Nat) (threshold : Nat) (p : Name → Bool) : Array (Name × Nat) := Id.run do
+  let mut r := #[]
+  for (declName, counter) in counters do
+    if counter > threshold then
+    if p declName then
+      r := r.push (declName, counter)
+  return r.qsort fun (d₁, c₁) (d₂, c₂) => if c₁ == c₂ then d₁.lt d₂ else c₁ > c₂
+
+private def mkMessageBodyFor? (counters : PHashMap Name Nat) (threshold : Nat) (p : Name → Bool := fun _ => true) : MetaM (Option MessageData) := do
+  let entries := collectAboveThreshold counters threshold p
+  if entries.isEmpty then
+    return none
+  else
+    let mut m := MessageData.nil
+    for (declName, counter) in entries do
+      unless m matches .nil do
+        m := m ++ "\n"
+      m := m ++ m!"{MessageData.ofConst (← mkConstWithLevelParams declName)} ↦ {counter}"
+    return some m
+
+private def appendOptMessageData (m : MessageData) (header : String) (m? : Option MessageData) : MessageData :=
+  if let some m' := m? then
+    if m matches .nil then
+      header ++ indentD m'
+    else
+      m ++ "\n" ++ header ++ indentD m'
+  else
+    m
+
+def reportDiag : MetaM Unit := do
+  if (← isDiagnosticsEnabled) then
+    let threshold := diagnostics.threshold.get (← getOptions)
+    let mut m := MessageData.nil
+    let env ← getEnv
+    let unfoldDefault? ← mkMessageBodyFor? (← get).diag.unfoldCounter threshold fun declName =>
+      getReducibilityStatusCore env declName matches .semireducible
+      && !isInstanceCore env declName
+    let unfoldInstance? ← mkMessageBodyFor? (← get).diag.unfoldCounter threshold fun declName =>
+      getReducibilityStatusCore env declName matches .semireducible
+      && isInstanceCore env declName
+    let unfoldReducible? ← mkMessageBodyFor? (← get).diag.unfoldCounter threshold fun declName =>
+      getReducibilityStatusCore env declName matches .reducible
+    let heu? ← mkMessageBodyFor? (← get).diag.heuristicCounter threshold
+    let inst? ← mkMessageBodyFor? (← get).diag.instanceCounter threshold
+    if unfoldDefault?.isSome || unfoldInstance?.isSome || unfoldReducible?.isSome || heu?.isSome || inst?.isSome then
+      m := appendOptMessageData m "unfolded declarations:" unfoldDefault?
+      m := appendOptMessageData m "unfolded instances:" unfoldInstance?
+      m := appendOptMessageData m "unfolded reducible declarations:" unfoldReducible?
+      m := appendOptMessageData m "used instances:" inst?
+      m := appendOptMessageData m "`isDefEq` heuristic:" heu?
+      m := m ++ "\nuse `set_option diagnostics.threshold <num>` to control threshold for reporting counters"
+      logInfo m
+
+end Lean.Meta

src/Lean/Meta/ExprDefEq.lean

@@ -10,6 +10,18 @@ import Lean.Util.OccursCheck
 
 namespace Lean.Meta
 
+register_builtin_option backward.isDefEq.lazyProjDelta : Bool := {
+  defValue := true
+  group    := "backward compatibility"
+  descr    := "use lazy delta reduction when solving unification constrains of the form `(f a).i =?= (g b).i`"
+}
+
+register_builtin_option backward.isDefEq.lazyWhnfCore : Bool := {
+  defValue := true
+  group    := "backward compatibility"
+  descr    := "specifies transparency mode when normalizing constraints of the form `(f a).i =?= s`, if `true` only reducible definitions and instances are unfolded when reducing `f a`. Otherwise, the default setting is used"
+}
+
 /--
   Return `true` if `e` is of the form `fun (x_1 ... x_n) => ?m y_1 ... y_k)`, and `?m` is unassigned.
   Remark: `n`, `k` may be 0.
@@ -1239,6 +1251,7 @@ private def tryHeuristic (t s : Expr) : MetaM Bool := do
     unless t.hasExprMVar || s.hasExprMVar do
       return false
   withTraceNodeBefore `Meta.isDefEq.delta (return m!"{t} =?= {s}") do
+    recordDefEqHeuristic tFn.constName!
     /-
       We process arguments before universe levels to reduce a source of brittleness in the TC procedure.
 
@@ -1757,10 +1770,21 @@ private def isDefEqDeltaStep (t s : Expr) : MetaM DeltaStepResult := do
     | .lt => unfold t (return .unknown) (k · s)
     | .gt => unfold s (return .unknown) (k t ·)
     | .eq =>
-      unfold t
-        (unfold s (return .unknown) (k t ·))
-        (fun t => unfold s (k t s) (k t ·))
+      -- Remark: if `t` and `s` are both some `f`-application, we use `tryHeuristic`
+      -- if `f` is not a projection. The projection case generates a performance regression.
+      if tInfo.name == sInfo.name 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
@@ -1792,8 +1816,13 @@ where
     | _, _ => Meta.isExprDefEqAux t s
 
 private def isDefEqProj : Expr → Expr → MetaM Bool
-  | .proj m i t, .proj n j s =>
-    if i == j && m == n then
+  | .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 !backward.isDefEq.lazyProjDelta.get (← getOptions) then
+      pure (i == j && m == n) <&&> Meta.isExprDefEqAux t s
+    else if i == j && m == n then
       isDefEqProjDelta t s i
     else
       return false
@@ -1966,6 +1995,12 @@ private def cacheResult (keyInfo : DefEqCacheKeyInfo) (result : Bool) : MetaM Un
     let key := (← instantiateMVars key.1, ← instantiateMVars key.2)
     modifyDefEqTransientCache fun c => c.update mode key result
 
+private def whnfCoreAtDefEq (e : Expr) : MetaM Expr := do
+  if backward.isDefEq.lazyWhnfCore.get (← getOptions) then
+    whnfCore e (config := { proj := .yesWithDeltaI })
+  else
+    whnfCore e
+
 @[export lean_is_expr_def_eq]
 partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecDepth do
   withTraceNodeBefore `Meta.isDefEq (return m!"{t} =?= {s}") do
@@ -1978,7 +2013,7 @@ partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecD
     we only want to unify negation (and not all other field operations as well).
     Unifying the field instances slowed down unification: https://github.com/leanprover/lean4/issues/1986
 
-    Note that ew use `proj := .yesWithDeltaI` to ensure `whnfAtMostI` is used to reduce the projection structure.
+    Note that we use `proj := .yesWithDeltaI` to ensure `whnfAtMostI` is used to reduce the projection structure.
     We added this refinement to address a performance issue in code such as
     ```
     let val : Test := bar c1 key
@@ -2007,8 +2042,8 @@ partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecD
     `whnfCore t (config := { proj := .yes })` which more conservative than `.yesWithDeltaI`,
     and it only created performance issues when handling TC unification problems.
   -/
-  let t' ← whnfCore t (config := { proj := .yesWithDeltaI })
-  let s' ← whnfCore s (config := { proj := .yesWithDeltaI })
+  let t' ← whnfCoreAtDefEq t
+  let s' ← whnfCoreAtDefEq s
   if t != t' || s != s' then
     isExprDefEqAuxImpl t' s'
   else

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
 
@@ -217,8 +217,11 @@ def getGlobalInstancesIndex : CoreM (DiscrTree InstanceEntry) :=
 def getErasedInstances : CoreM (PHashSet Name) :=
   return Meta.instanceExtension.getState (← getEnv) |>.erased
 
+def isInstanceCore (env : Environment) (declName : Name) : Bool :=
+  Meta.instanceExtension.getState env |>.instanceNames.contains declName
+
 def isInstance (declName : Name) : CoreM Bool :=
-  return Meta.instanceExtension.getState (← getEnv) |>.instanceNames.contains declName
+  return isInstanceCore (← getEnv) declName
 
 def getInstancePriority? (declName : Name) : CoreM (Option Nat) := do
   let some entry := Meta.instanceExtension.getState (← getEnv) |>.instanceNames.find? declName | return none

src/Lean/Meta/LazyDiscrTree.lean

@@ -978,12 +978,13 @@ def createImportedDiscrTree [Monad m] [MonadLog m] [AddMessageContext m] [MonadO
 
 /-- Creates the core context used for initializing a tree using the current context. -/
 private def createTreeCtx (ctx : Core.Context) : Core.Context := {
-    fileName := ctx.fileName,
-    fileMap := ctx.fileMap,
-    options := ctx.options,
-    maxRecDepth := ctx.maxRecDepth,
-    maxHeartbeats := 0,
-    ref := ctx.ref,
+    fileName := ctx.fileName
+    fileMap := ctx.fileMap
+    options := ctx.options
+    maxRecDepth := ctx.maxRecDepth
+    maxHeartbeats := 0
+    ref := ctx.ref
+    diag := getDiag ctx.options
   }
 
 def findImportMatches

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
     }
 
@@ -347,11 +362,14 @@ private def mkLambdaFVars' (xs : Array Expr) (e : Expr) : MetaM Expr :=
   If it succeeds, the result is a new updated metavariable context and a new list of subgoals.
   A subgoal is created for each instance implicit parameter of `inst`. -/
 def tryResolve (mvar : Expr) (inst : Instance) : MetaM (Option (MetavarContext × List Expr)) := do
+  if (← isDiagnosticsEnabled) then
+    if let .const declName _ := inst.val.getAppFn then
+      recordInstance declName
   let mvarType   ← inferType mvar
   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 +391,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 +401,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 :=
@@ -407,18 +425,18 @@ private def mkAnswer (cNode : ConsumerNode) : MetaM Answer :=
 def addAnswer (cNode : ConsumerNode) : SynthM Unit := do
   withMCtx cNode.mctx do
   if cNode.size ≥ (← read).maxResultSize then
-      trace[Meta.synthInstance.answer] "{crossEmoji} {← instantiateMVars (← inferType cNode.mvar)}{Format.line}(size: {cNode.size} ≥ {(← read).maxResultSize})"
+    trace[Meta.synthInstance.answer] "{crossEmoji} {← instantiateMVars (← inferType cNode.mvar)}{Format.line}(size: {cNode.size} ≥ {(← read).maxResultSize})"
   else
     withTraceNode `Meta.synthInstance.answer
       (fun _ => return m!"{checkEmoji} {← instantiateMVars (← inferType cNode.mvar)}") 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 +444,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 +557,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 +697,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 +720,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 +806,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/LinearArith/Solver.lean

@@ -81,6 +81,7 @@ def Poly.add (e₁ e₂ : Poly) : Poly :=
       else
         { val := r }
     termination_by (e₁.size - i₁, e₂.size - i₂)
+    decreasing_by all_goals decreasing_with decreasing_trivial_pre_omega
   go 0 0 #[]
 
 def Poly.combine (d₁ : Int) (e₁ : Poly) (d₂ : Int) (e₂ : Poly) : Poly :=
@@ -108,6 +109,7 @@ def Poly.combine (d₁ : Int) (e₁ : Poly) (d₂ : Int) (e₂ : Poly) : Poly :=
       else
         { val := r }
     termination_by (e₁.size - i₁, e₂.size - i₂)
+    decreasing_by all_goals decreasing_with decreasing_trivial_pre_omega
   go 0 0 #[]
 
 def Poly.eval? (e : Poly) (a : Assignment) : Option Rat := Id.run do

src/Lean/Meta/WHNF.lean

@@ -344,7 +344,7 @@ inductive ProjReductionKind where
   | yesWithDelta
   /--
   Projections `s.i` are reduced at `whnfCore`, and `whnfAtMostI` is used at `s` during the process.
-  Recall that `whnfAtMostII` is like `whnf` but uses transparency at most `instances`.
+  Recall that `whnfAtMostI` is like `whnf` but uses transparency at most `instances`.
   This option is stronger than `yes`, but weaker than `yesWithDelta`.
   We use this option to ensure we reduce projections to prevent expensive defeq checks when unifying TC operations.
   When unifying e.g. `(@Field.toNeg α inst1).1 =?= (@Field.toNeg α inst2).1`,
@@ -608,10 +608,11 @@ where
           | .notMatcher   =>
             matchConstAux f' (fun _ => return e) fun cinfo lvls =>
               match cinfo with
-              | .recInfo rec    => reduceRec rec lvls e.getAppArgs (fun _ => return e) go
-              | .quotInfo rec   => reduceQuotRec rec e.getAppArgs (fun _ => return e) go
+              | .recInfo rec    => reduceRec rec lvls e.getAppArgs (fun _ => return e) (fun e => do recordUnfold cinfo.name; go e)
+              | .quotInfo rec   => reduceQuotRec rec e.getAppArgs (fun _ => return e) (fun e => do recordUnfold cinfo.name; go e)
               | c@(.defnInfo _) => do
                 if (← isAuxDef c.name) then
+                  recordUnfold c.name
                   deltaBetaDefinition c lvls e.getAppRevArgs (fun _ => return e) go
                 else
                   return e
@@ -706,7 +707,7 @@ mutual
         | some e =>
           match (← withReducibleAndInstances <| reduceProj? e.getAppFn) with
           | none   => return none
-          | some r => return mkAppN r e.getAppArgs |>.headBeta
+          | some r => recordUnfold declName; return mkAppN r e.getAppArgs |>.headBeta
       | _ => return none
     | _ => return none
 
@@ -729,8 +730,9 @@ mutual
         if fInfo.levelParams.length != fLvls.length then
           return none
         else
-          let unfoldDefault (_ : Unit) : MetaM (Option Expr) :=
+          let unfoldDefault (_ : Unit) : MetaM (Option Expr) := do
             if fInfo.hasValue then
+              recordUnfold fInfo.name
               deltaBetaDefinition fInfo fLvls e.getAppRevArgs (fun _ => pure none) (fun e => pure (some e))
             else
               return none
@@ -778,11 +780,13 @@ mutual
                   Thus, we should keep `return some r` until Mathlib has been ported to Lean 3.
                   Note that the `Vector` example above does not even work in Lean 3.
                 -/
-                let some recArgPos ← getStructuralRecArgPos? fInfo.name | return some r
+                let some recArgPos ← getStructuralRecArgPos? fInfo.name
+                  | recordUnfold fInfo.name; return some r
                 let numArgs := e.getAppNumArgs
                 if recArgPos >= numArgs then return none
                 let recArg := e.getArg! recArgPos numArgs
                 if !(← isConstructorApp (← whnfMatcher recArg)) then return none
+                recordUnfold fInfo.name
                 return some r
             | _ =>
               if (← getMatcherInfo? fInfo.name).isSome then
@@ -800,7 +804,7 @@ mutual
         unless cinfo.hasValue do return none
         deltaDefinition cinfo lvls
           (fun _ => pure none)
-          (fun e => pure (some e))
+          (fun e => do recordUnfold declName; pure (some e))
     | _ => return none
 end
 
@@ -833,11 +837,11 @@ def reduceRecMatcher? (e : Expr) : MetaM (Option Expr) := do
     | .reduced e => return e
     | _ => matchConstAux e.getAppFn (fun _ => pure none) fun cinfo lvls => do
       match cinfo with
-      | .recInfo «rec»  => reduceRec «rec» lvls e.getAppArgs (fun _ => pure none) (fun e => pure (some e))
-      | .quotInfo «rec» => reduceQuotRec «rec» e.getAppArgs (fun _ => pure none) (fun e => pure (some e))
+      | .recInfo «rec»  => reduceRec «rec» lvls e.getAppArgs (fun _ => pure none) (fun e => do recordUnfold cinfo.name; pure (some e))
+      | .quotInfo «rec» => reduceQuotRec «rec» e.getAppArgs (fun _ => pure none) (fun e => do recordUnfold cinfo.name; pure (some e))
       | c@(.defnInfo _) =>
         if (← isAuxDef c.name) then
-          deltaBetaDefinition c lvls e.getAppRevArgs (fun _ => pure none) (fun e => pure (some e))
+          deltaBetaDefinition c lvls e.getAppRevArgs (fun _ => pure none) (fun e => do recordUnfold c.name; pure (some e))
         else
           return none
       | _ => return none

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

@@ -13,7 +13,10 @@ import Lean.ParserCompiler
 namespace Lean
 
 def PPContext.runCoreM {α : Type} (ppCtx : PPContext) (x : CoreM α) : IO α :=
-  Prod.fst <$> x.toIO { options := ppCtx.opts, currNamespace := ppCtx.currNamespace, openDecls := ppCtx.openDecls, fileName := "<PrettyPrinter>", fileMap := default }
+  Prod.fst <$> x.toIO { options := ppCtx.opts, currNamespace := ppCtx.currNamespace
+                        openDecls := ppCtx.openDecls
+                        fileName := "<PrettyPrinter>", fileMap := default
+                        diag     := getDiag ppCtx.opts }
                       { env := ppCtx.env, ngen := { namePrefix := `_pp_uniq } }
 
 def PPContext.runMetaM {α : Type} (ppCtx : PPContext) (x : MetaM α) : IO α :=
@@ -48,7 +51,9 @@ def ppExprWithInfos (e : Expr) (optsPerPos : Delaborator.OptionsPerPos := {}) (d
 
 @[export lean_pp_expr]
 def ppExprLegacy (env : Environment) (mctx : MetavarContext) (lctx : LocalContext) (opts : Options) (e : Expr) : IO Format :=
-  Prod.fst <$> ((ppExpr e).run' { lctx := lctx } { mctx := mctx }).toIO { options := opts, fileName := "<PrettyPrinter>", fileMap := default } { env := env }
+  Prod.fst <$> ((ppExpr e).run' { lctx := lctx } { mctx := mctx }).toIO {
+    options := opts, fileName := "<PrettyPrinter>", fileMap := default, diag := getDiag opts
+  } { env := env }
 
 def ppTactic (stx : TSyntax `tactic) : CoreM Format := ppCategory `tactic stx
 
@@ -86,6 +91,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/ReducibilityAttrs.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Attributes
+import Lean.ScopedEnvExtension
 
 namespace Lean
 
@@ -13,36 +14,100 @@ Reducibility status for a definition.
 -/
 inductive ReducibilityStatus where
   | reducible | semireducible | irreducible
-  deriving Inhabited, Repr
+  deriving Inhabited, Repr, BEq
 
-/--
-Environment extension for storing the reducibility attribute for definitions.
--/
-builtin_initialize reducibilityAttrs : EnumAttributes ReducibilityStatus ←
-  registerEnumAttributes
-    [(`reducible, "reducible", ReducibilityStatus.reducible),
-     (`semireducible, "semireducible", ReducibilityStatus.semireducible),
-     (`irreducible, "irreducible", ReducibilityStatus.irreducible)]
+builtin_initialize reducibilityCoreExt : PersistentEnvExtension (Name × ReducibilityStatus) (Name × ReducibilityStatus) (NameMap ReducibilityStatus) ←
+  registerPersistentEnvExtension {
+    name            := `reducibilityCore
+    mkInitial       := pure {}
+    addImportedFn   := fun _ _ => pure {}
+    addEntryFn      := fun (s : NameMap ReducibilityStatus) (p : Name × ReducibilityStatus) => s.insert p.1 p.2
+    exportEntriesFn := fun m =>
+      let r : Array (Name × ReducibilityStatus) := m.fold (fun a n p => a.push (n, p)) #[]
+      r.qsort (fun a b => Name.quickLt a.1 b.1)
+    statsFn         := fun s => "reducibility attribute core extension" ++ Format.line ++ "number of local entries: " ++ format s.size
+  }
+
+builtin_initialize reducibilityExtraExt : SimpleScopedEnvExtension (Name × ReducibilityStatus) (SMap Name ReducibilityStatus) ←
+  registerSimpleScopedEnvExtension {
+    name := `reducibilityExtra
+    initial := {}
+    addEntry := fun d (declName, status) => d.insert declName status
+    finalizeImport := fun d => d.switch
+  }
 
 @[export lean_get_reducibility_status]
-private def getReducibilityStatusImp (env : Environment) (declName : Name) : ReducibilityStatus :=
-  match reducibilityAttrs.getValue env declName with
-  | some s => s
-  | none   => ReducibilityStatus.semireducible
+def getReducibilityStatusCore (env : Environment) (declName : Name) : ReducibilityStatus :=
+  let m := reducibilityExtraExt.getState env
+  if let some status := m.find? declName then
+    status
+  else match env.getModuleIdxFor? declName with
+  | some modIdx =>
+    match (reducibilityCoreExt.getModuleEntries env modIdx).binSearch (declName, .semireducible) (fun a b => Name.quickLt a.1 b.1) with
+    | some (_, status) => status
+    | none => .semireducible
+  | none => (reducibilityCoreExt.getState env).find? declName |>.getD .semireducible
+
+def setReducibilityStatusCore (env : Environment) (declName : Name) (status : ReducibilityStatus) (attrKind : AttributeKind) (currNamespace : Name) : Environment :=
+  if attrKind matches .global then
+    match env.getModuleIdxFor? declName with
+    | some _ =>
+      -- Trying to set the attribute of a declaration defined in an imported module.
+      reducibilityExtraExt.addEntry env (declName, status)
+    | none =>
+      --
+      reducibilityCoreExt.addEntry env (declName, status)
+  else
+    -- `scoped` and `local` must be handled by `reducibilityExtraExt`
+    reducibilityExtraExt.addCore env (declName, status) attrKind currNamespace
 
 @[export lean_set_reducibility_status]
-private def setReducibilityStatusImp (env : Environment) (declName : Name) (s : ReducibilityStatus) : Environment :=
-  match reducibilityAttrs.setValue env declName s with
-  | Except.ok env => env
-  | _ => env -- TODO(Leo): we should extend EnumAttributes.setValue in the future and ensure it never fails
+private def setReducibilityStatusImp (env : Environment) (declName : Name) (status : ReducibilityStatus) : Environment :=
+  setReducibilityStatusCore env declName status .global .anonymous
+
+builtin_initialize
+  registerBuiltinAttribute {
+    ref             := by exact decl_name%
+    name            := `irreducible
+    descr           := "irreducible declaration"
+    add             := fun declName stx attrKind => do
+      Attribute.Builtin.ensureNoArgs stx
+      let ns ← getCurrNamespace
+      modifyEnv fun env => setReducibilityStatusCore env declName .irreducible attrKind ns
+    applicationTime := .afterTypeChecking
+ }
+
+builtin_initialize
+  registerBuiltinAttribute {
+    ref             := by exact decl_name%
+    name            := `reducible
+    descr           := "reducible declaration"
+    add             := fun declName stx attrKind => do
+      Attribute.Builtin.ensureNoArgs stx
+      let ns ← getCurrNamespace
+      modifyEnv fun env => setReducibilityStatusCore env declName .reducible attrKind ns
+    applicationTime := .afterTypeChecking
+ }
+
+builtin_initialize
+  registerBuiltinAttribute {
+    ref             := by exact decl_name%
+    name            := `semireducible
+    descr           := "semireducible declaration"
+    add             := fun declName stx attrKind => do
+      Attribute.Builtin.ensureNoArgs stx
+      let ns ← getCurrNamespace
+      modifyEnv fun env => setReducibilityStatusCore env declName .reducible attrKind ns
+    applicationTime := .afterTypeChecking
+ }
 
 /-- Return the reducibility attribute for the given declaration. -/
 def getReducibilityStatus [Monad m] [MonadEnv m] (declName : Name) : m ReducibilityStatus := do
-  return getReducibilityStatusImp (← getEnv) declName
+  return getReducibilityStatusCore (← getEnv) declName
 
 /-- Set the reducibility attribute for the given declaration. -/
 def setReducibilityStatus [Monad m] [MonadEnv m] (declName : Name) (s : ReducibilityStatus) : m Unit := do
-  modifyEnv fun env => setReducibilityStatusImp env declName s
+  modifyEnv fun env => setReducibilityStatusCore env declName s .global .anonymous
 
 /-- Set the given declaration as `[reducible]` -/
 def setReducibleAttribute [Monad m] [MonadEnv m] (declName : Name) : m Unit := do
@@ -51,13 +116,13 @@ def setReducibleAttribute [Monad m] [MonadEnv m] (declName : Name) : m Unit := d
 /-- Return `true` if the given declaration has been marked as `[reducible]`. -/
 def isReducible [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
   match (← getReducibilityStatus declName) with
-  | ReducibilityStatus.reducible => return true
+  | .reducible => return true
   | _ => return false
 
 /-- Return `true` if the given declaration has been marked as `[irreducible]` -/
 def isIrreducible [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
   match (← getReducibilityStatus declName) with
-  | ReducibilityStatus.irreducible => return true
+  | .irreducible => return true
   | _ => return false
 
 end Lean

src/Lean/Replay.lean

@@ -50,7 +50,7 @@ def isTodo (name : Name) : M Bool := do
 
 /-- Use the current `Environment` to throw a `KernelException`. -/
 def throwKernelException (ex : KernelException) : M Unit := do
-    let ctx := { fileName := "", options := ({} : KVMap), fileMap := default }
+    let ctx := { fileName := "", options := ({} : KVMap), fileMap := default, diag := false }
     let state := { env := (← get).env }
     Prod.fst <$> (Lean.Core.CoreM.toIO · ctx state) do Lean.throwKernelException ex
 

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

@@ -146,11 +146,15 @@ def ScopedEnvExtension.addLocalEntry (ext : ScopedEnvExtension α β σ) (env :
     let top := { top with state := ext.descr.addEntry top.state b }
     ext.ext.setState env { s with stateStack := top :: states }
 
-def ScopedEnvExtension.add [Monad m] [MonadResolveName m] [MonadEnv m] (ext : ScopedEnvExtension α β σ) (b : β) (kind := AttributeKind.global) : m Unit := do
+def ScopedEnvExtension.addCore (env : Environment) (ext : ScopedEnvExtension α β σ) (b : β) (kind : AttributeKind) (namespaceName : Name) : Environment :=
   match kind with
-  | AttributeKind.global => modifyEnv (ext.addEntry · b)
-  | AttributeKind.local  => modifyEnv (ext.addLocalEntry · b)
-  | AttributeKind.scoped => modifyEnv (ext.addScopedEntry · (← getCurrNamespace) b)
+  | AttributeKind.global => ext.addEntry env b
+  | AttributeKind.local  => ext.addLocalEntry env b
+  | AttributeKind.scoped => ext.addScopedEntry env namespaceName b
+
+def ScopedEnvExtension.add [Monad m] [MonadResolveName m] [MonadEnv m] (ext : ScopedEnvExtension α β σ) (b : β) (kind := AttributeKind.global) : m Unit := do
+  let ns ← getCurrNamespace
+  modifyEnv (ext.addCore · b kind ns)
 
 def ScopedEnvExtension.getState [Inhabited σ] (ext : ScopedEnvExtension α β σ) (env : Environment) : σ :=
   match ext.ext.getState env |>.stateStack with

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/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/CMakeLists.txt

@@ -2,4 +2,4 @@ add_library(kernel OBJECT level.cpp expr.cpp expr_eq_fn.cpp
 for_each_fn.cpp replace_fn.cpp abstract.cpp instantiate.cpp
 local_ctx.cpp declaration.cpp environment.cpp type_checker.cpp
 init_module.cpp expr_cache.cpp equiv_manager.cpp quot.cpp
-inductive.cpp)
+inductive.cpp trace.cpp)

src/kernel/declaration.cpp

@@ -71,8 +71,10 @@ definition_val::definition_val(name const & n, names const & lparams, expr const
 
 definition_safety definition_val::get_safety() const { return static_cast<definition_safety>(lean_definition_val_get_safety(to_obj_arg())); }
 
-theorem_val::theorem_val(name const & n, names const & lparams, expr const & type, expr const & val):
-    object_ref(mk_cnstr(0, constant_val(n, lparams, type), val)) {
+extern "C" object * lean_mk_theorem_val(object * n, object * lparams, object * type, object * value, object * all);
+
+theorem_val::theorem_val(name const & n, names const & lparams, expr const & type, expr const & val, names const & all):
+    object_ref(lean_mk_theorem_val(n.to_obj_arg(), lparams.to_obj_arg(), type.to_obj_arg(), val.to_obj_arg(), all.to_obj_arg())) {
 }
 
 extern "C" object * lean_mk_opaque_val(object * n, object * lparams, object * type, object * value, uint8 is_unsafe, object * all);
@@ -205,6 +207,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, names(n))));
+}
+
 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

@@ -112,12 +112,13 @@ public:
 typedef list_ref<definition_val> definition_vals;
 
 /*
-structure theorem_val extends constant_val :=
-(value : task expr)
+structure TheoremVal extends ConstantVal where
+  value : Expr
+  all : List Name := [name]
 */
 class theorem_val : public object_ref {
 public:
-    theorem_val(name const & n, names const & lparams, expr const & type, expr const & val);
+    theorem_val(name const & n, names const & lparams, expr const & type, expr const & val, names const & all);
     theorem_val(theorem_val const & other):object_ref(other) {}
     theorem_val(theorem_val && other):object_ref(other) {}
     theorem_val & operator=(theorem_val const & other) { object_ref::operator=(other); return *this; }
@@ -223,10 +224,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/kernel/init_module.cpp

@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "kernel/local_ctx.h"
 #include "kernel/inductive.h"
 #include "kernel/quot.h"
+#include "kernel/trace.h"
 
 namespace lean {
 void initialize_kernel_module() {
@@ -23,9 +24,11 @@ void initialize_kernel_module() {
     initialize_local_ctx();
     initialize_inductive();
     initialize_quot();
+    initialize_trace();
 }
 
 void finalize_kernel_module() {
+    finalize_trace();
     finalize_quot();
     finalize_inductive();
     finalize_local_ctx();

src/kernel/trace.cpp

@@ -10,7 +10,7 @@ Author: Leonardo de Moura
 #include "util/option_declarations.h"
 #include "kernel/environment.h"
 #include "kernel/local_ctx.h"
-#include "library/trace.h"
+#include "kernel/trace.h"
 
 namespace lean {
 static name_set *            g_trace_classes = nullptr;

src/lake/Lake/Build.lean

@@ -3,10 +3,9 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-import Lake.Build.Monad
-import Lake.Build.Actions
-import Lake.Build.Index
+import Lake.Build.Run
 import Lake.Build.Module
 import Lake.Build.Package
 import Lake.Build.Library
 import Lake.Build.Imports
+import Lake.Build.Targets

src/lake/Lake/Build/Actions.lean

@@ -5,22 +5,24 @@ Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone, Siddharth Bhat
 -/
 import Lake.Util.Proc
 import Lake.Util.NativeLib
-import Lake.Build.Context
+import Lake.Build.Basic
 
 /-! # Common Build Actions
-Low level actions to build common Lean artfiacts via the Lean toolchain.
+Low level actions to build common Lean artifacts via the Lean toolchain.
 -/
 
-namespace Lake
 open System
+open Lean hiding SearchPath
 
-def compileLeanModule (name : String) (leanFile : FilePath)
-(oleanFile? ileanFile? cFile? bcFile?: Option FilePath)
-(leanPath : SearchPath := []) (rootDir : FilePath := ".")
-(dynlibs : Array FilePath := #[]) (dynlibPath : SearchPath := {})
-(leanArgs : Array String := #[]) (lean : FilePath := "lean")
-: BuildM Unit := do
-  logStep s!"Building {name}"
+namespace Lake
+
+def compileLeanModule
+  (leanFile : FilePath)
+  (oleanFile? ileanFile? cFile? bcFile?: Option FilePath)
+  (leanPath : SearchPath := []) (rootDir : FilePath := ".")
+  (dynlibs : Array FilePath := #[]) (dynlibPath : SearchPath := {})
+  (leanArgs : Array String := #[]) (lean : FilePath := "lean")
+: JobM Unit := do
   let mut args := leanArgs ++
     #[leanFile.toString, "-R", rootDir.toString]
   if let some oleanFile := oleanFile? then
@@ -37,7 +39,10 @@ def compileLeanModule (name : String) (leanFile : FilePath)
     args := args ++ #["-b", bcFile.toString]
   for dynlib in dynlibs do
     args := args.push s!"--load-dynlib={dynlib}"
-  proc {
+  args := args.push "--json"
+  show LogIO _ from do
+  let iniSz ← getLogSize
+  let out ← rawProc {
     args
     cmd := lean.toString
     env := #[
@@ -45,37 +50,59 @@ def compileLeanModule (name : String) (leanFile : FilePath)
       (sharedLibPathEnvVar, (← getSearchPath sharedLibPathEnvVar) ++ dynlibPath |>.toString)
     ]
   }
+  unless out.stdout.isEmpty do
+    let txt ← out.stdout.split (· == '\n') |>.foldlM (init := "") fun txt ln => do
+      if let .ok (msg : SerialMessage) := Json.parse ln >>= fromJson? then
+        unless txt.isEmpty do
+          logInfo s!"stdout:\n{txt}"
+        logSerialMessage msg
+        return txt
+      else if txt.isEmpty && ln.isEmpty then
+        return txt
+      else
+        return txt ++ ln ++ "\n"
+    unless txt.isEmpty do
+      logInfo s!"stdout:\n{txt}"
+  unless out.stderr.isEmpty do
+    logInfo s!"stderr:\n{out.stderr}"
+  if out.exitCode ≠ 0 then
+    logError s!"Lean exited with code {out.exitCode}"
+    throw iniSz
 
-def compileO (name : String) (oFile srcFile : FilePath)
-(moreArgs : Array String := #[]) (compiler : FilePath := "cc") : BuildM Unit := do
-  logStep s!"Compiling {name}"
+def compileO
+  (oFile srcFile : FilePath)
+  (moreArgs : Array String := #[]) (compiler : FilePath := "cc")
+: JobM Unit := do
   createParentDirs oFile
   proc {
     cmd := compiler.toString
     args := #["-c", "-o", oFile.toString, srcFile.toString] ++ moreArgs
   }
 
-def compileStaticLib (name : String) (libFile : FilePath)
-(oFiles : Array FilePath) (ar : FilePath := "ar") : BuildM Unit := do
-  logStep s!"Creating {name}"
+def compileStaticLib
+  (libFile : FilePath) (oFiles : Array FilePath)
+  (ar : FilePath := "ar")
+: JobM Unit := do
   createParentDirs libFile
   proc {
     cmd := ar.toString
     args := #["rcs", libFile.toString] ++ oFiles.map toString
   }
 
-def compileSharedLib (name : String) (libFile : FilePath)
-(linkArgs : Array String) (linker : FilePath := "cc") : BuildM Unit := do
-  logStep s!"Linking {name}"
+def compileSharedLib
+  (libFile : FilePath) (linkArgs : Array String)
+  (linker : FilePath := "cc")
+: JobM Unit := do
   createParentDirs libFile
   proc {
     cmd := linker.toString
     args := #["-shared", "-o", libFile.toString] ++ linkArgs
   }
 
-def compileExe (name : String) (binFile : FilePath) (linkFiles : Array FilePath)
-(linkArgs : Array String := #[]) (linker : FilePath := "cc") : BuildM Unit := do
-  logStep s!"Linking {name}"
+def compileExe
+  (binFile : FilePath) (linkFiles : Array FilePath)
+  (linkArgs : Array String := #[]) (linker : FilePath := "cc")
+: JobM Unit := do
   createParentDirs binFile
   proc {
     cmd := linker.toString
@@ -83,46 +110,39 @@ def compileExe (name : String) (binFile : FilePath) (linkFiles : Array FilePath)
   }
 
 /-- Download a file using `curl`, clobbering any existing file. -/
-def download (name : String) (url : String) (file : FilePath) : LogIO PUnit := do
-  logVerbose s!"Downloading {name}"
+def download  (url : String) (file : FilePath) : LogIO PUnit := do
   if (← file.pathExists) then
     IO.FS.removeFile file
   else
     createParentDirs file
-  let args :=
-    if (← getIsVerbose) then #[] else #["-s"]
   proc (quiet := true) {
     cmd := "curl"
-    args := args ++ #["-f", "-o", file.toString, "-L", url]
+    args := #["-f", "-o", file.toString, "-L", url]
   }
 
 /-- Unpack an archive `file` using `tar` into the directory `dir`. -/
-def untar (name : String) (file : FilePath) (dir : FilePath) (gzip := true) : LogIO PUnit := do
-  logVerbose s!"Unpacking {name}"
+def untar (file : FilePath) (dir : FilePath) (gzip := true) : LogIO PUnit := do
   IO.FS.createDirAll dir
-  let mut opts := "-x"
-  if (← getIsVerbose) then
-    opts := opts.push 'v'
+  let mut opts := "-xvv"
   if gzip then
     opts := opts.push 'z'
-  proc {
+  proc (quiet := true) {
     cmd := "tar",
     args := #[opts, "-f", file.toString, "-C", dir.toString]
   }
 
 /-- Pack a directory `dir` using `tar` into the archive `file`. -/
-def tar (name : String) (dir : FilePath) (file : FilePath)
-(gzip := true) (excludePaths : Array FilePath := #[]) : LogIO PUnit := do
-  logVerbose s!"Packing {name}"
+def tar
+  (dir : FilePath) (file : FilePath)
+  (gzip := true) (excludePaths : Array FilePath := #[])
+: LogIO PUnit := do
   createParentDirs file
-  let mut args := #["-c"]
+  let mut args := #["-cvv"]
   if gzip then
     args := args.push "-z"
-  if (← getIsVerbose) then
-    args := args.push "-v"
   for path in excludePaths do
     args := args.push s!"--exclude={path}"
-  proc {
+  proc (quiet := true) {
     cmd := "tar"
     args := args ++ #["-f", file.toString, "-C", dir.toString, "."]
     -- don't pack `._` files on MacOS

src/lake/Lake/Build/Basic.lean

@@ -6,12 +6,9 @@ Authors: Mac Malone
 import Lake.Util.Log
 import Lake.Util.Exit
 import Lake.Util.Task
-import Lake.Util.Error
-import Lake.Util.OptionIO
+import Lake.Util.Lift
 import Lake.Config.Context
 import Lake.Build.Trace
-import Lake.Build.Store
-import Lake.Build.Topological
 
 open System
 namespace Lake
@@ -25,16 +22,35 @@ structure BuildConfig where
   trustHash : Bool := true
   /-- Early exit if a target has to be rebuilt. -/
   noBuild : Bool := false
+  verbosity : Verbosity := .normal
+  /--
+  Fail the top-level build if warnings have been logged.
+  Unlike some build systems, this does **NOT** convert warnings to errors,
+  and it does not abort jobs when warnings are logged (i.e., dependent jobs
+  will still continue unimpeded).
+  -/
+  failIfWarnings : Bool := false
+  /-- Report build output on `stdout`. Otherwise, Lake uses `stderr`. -/
+  useStdout : Bool := false
+
+abbrev JobResult α := EResult Nat Log α
+abbrev JobTask α := BaseIOTask (JobResult α)
+
+/-- A Lake job. -/
+structure Job (α : Type u)  where
+  task : JobTask α
 
 /-- A Lake context with a build configuration and additional build data. -/
 structure BuildContext extends BuildConfig, Context where
   leanTrace : BuildTrace
-  startedBuilds : IO.Ref Nat
-  finishedBuilds : IO.Ref Nat
+  registeredJobs : IO.Ref (Array (String × Job Unit))
 
 /-- A transformer to equip a monad with a `BuildContext`. -/
 abbrev BuildT := ReaderT BuildContext
 
+instance [Pure m] : MonadLift LakeM (BuildT m) where
+  monadLift x := fun ctx => pure <| x.run ctx.toContext
+
 @[inline] def getLeanTrace [Monad m] : BuildT m BuildTrace :=
   (·.leanTrace) <$> readThe BuildContext
 
@@ -50,37 +66,23 @@ abbrev BuildT := ReaderT BuildContext
 @[inline] def getNoBuild [Monad m] : BuildT m Bool :=
   (·.noBuild) <$> getBuildConfig
 
-/-- The monad for the Lake build manager. -/
-abbrev SchedulerM := BuildT <| LogT BaseIO
+@[inline] def getVerbosity [Monad m] : BuildT m Verbosity :=
+  (·.verbosity) <$> getBuildConfig
 
-/-- The core monad for Lake builds. -/
-abbrev BuildM := BuildT LogIO
+@[inline] def getIsVerbose [Monad m] : BuildT m Bool :=
+  (· == .verbose) <$> getVerbosity
 
-/-- A transformer to equip a monad with a Lake build store. -/
-abbrev BuildStoreT := StateT BuildStore
+@[inline] def getIsQuiet [Monad m] : BuildT m Bool :=
+  (· == .quiet) <$> getVerbosity
 
-/-- A Lake build cycle. -/
-abbrev BuildCycle := Cycle BuildKey
+/-- The internal core monad of Lake builds.  Not intended for user use. -/
+abbrev CoreBuildM := BuildT LogIO
 
-/-- A transformer for monads that may encounter a build cycle. -/
-abbrev BuildCycleT := CycleT BuildKey
+/-- The monad of asynchronous Lake jobs. -/
+abbrev JobM := CoreBuildM
 
-/-- A recursive build of a Lake build store that may encounter a cycle. -/
-abbrev RecBuildM := BuildCycleT <| BuildStoreT BuildM
+/-- The monad used to spawn asynchronous Lake build jobs. Lifts into `FetchM`. -/
+abbrev SpawnM := BuildT BaseIO
 
-instance [Pure m] : MonadLift LakeM (BuildT m) where
-  monadLift x := fun ctx => pure <| x.run ctx.toContext
-
-@[inline] def BuildM.run (ctx : BuildContext) (self : BuildM α) : LogIO α :=
-  self ctx
-
-def BuildM.catchFailure (f : Unit → BaseIO α) (self : BuildM α) : SchedulerM α :=
-  fun ctx logMethods => self ctx logMethods |>.catchFailure f
-
-def logStep (message : String) : BuildM Unit := do
-  let done ← (← read).finishedBuilds.get
-  let started ← (← read).startedBuilds.get
-  logInfo s!"[{done}/{started}] {message}"
-
-def createParentDirs (path : FilePath) : IO Unit := do
-  if let some dir := path.parent then IO.FS.createDirAll dir
+/-- The monad used to spawn asynchronous Lake build jobs. **Replaced by `SpawnM`.** -/
+@[deprecated SpawnM] abbrev SchedulerM := SpawnM

src/lake/Lake/Build/Common.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-import Lake.Build.Monad
+import Lake.Config.Monad
 import Lake.Build.Actions
 
 /-! # Common Build Tools
@@ -11,7 +11,8 @@ This file defines general utilities that abstract common
 build functionality and provides some common concrete build functions.
 -/
 
-open System
+open System Lean
+
 namespace Lake
 
 /-! ## General Utilities -/
@@ -24,8 +25,10 @@ and will be rebuilt on different host platforms.
 def platformTrace := pureHash System.Platform.target
 
 /-- Check if the `info` is up-to-date by comparing `depTrace` with `traceFile`. -/
-@[specialize] def BuildTrace.checkUpToDate [CheckExists ι] [GetMTime ι]
-(info : ι) (depTrace : BuildTrace) (traceFile : FilePath) : JobM Bool := do
+@[specialize] def BuildTrace.checkUpToDate
+  [CheckExists ι] [GetMTime ι]
+  (info : ι) (depTrace : BuildTrace) (traceFile : FilePath)
+: JobM Bool := do
   if (← getIsOldMode) then
     depTrace.checkAgainstTime info
   else
@@ -36,13 +39,15 @@ Build `info` unless it already exists and `depTrace` matches that
 of the `traceFile`. If rebuilt, save the new `depTrace` to the `tracefile`.
 Returns whether `info` was already up-to-date.
 -/
-@[inline] def buildUnlessUpToDate' [CheckExists ι] [GetMTime ι] (info : ι)
-(depTrace : BuildTrace) (traceFile : FilePath) (build : JobM PUnit) : JobM Bool := do
+@[inline] def buildUnlessUpToDate?
+  [CheckExists ι] [GetMTime ι] (info : ι)
+  (depTrace : BuildTrace) (traceFile : FilePath) (build : JobM PUnit)
+: JobM Bool := do
   if (← depTrace.checkUpToDate info traceFile) then
     return true
+  else if (← getNoBuild) then
+    IO.Process.exit noBuildCode.toUInt8
   else
-    if (← getNoBuild) then
-      IO.Process.exit noBuildCode.toUInt8
     build
     depTrace.writeToFile traceFile
     return false
@@ -51,12 +56,14 @@ Returns whether `info` was already up-to-date.
 Build `info` unless it already exists and `depTrace` matches that
 of the `traceFile`. If rebuilt, save the new `depTrace` to the `tracefile`.
 -/
-@[inline] def buildUnlessUpToDate [CheckExists ι] [GetMTime ι] (info : ι)
-(depTrace : BuildTrace) (traceFile : FilePath) (build : JobM PUnit) : JobM PUnit := do
-  discard <| buildUnlessUpToDate' info depTrace traceFile build
+@[inline] def buildUnlessUpToDate
+  [CheckExists ι] [GetMTime ι] (info : ι)
+  (depTrace : BuildTrace) (traceFile : FilePath) (build : JobM PUnit)
+: JobM PUnit := do
+  discard <| buildUnlessUpToDate? info depTrace traceFile build
 
 /-- Fetch the trace of a file that may have its hash already cached in a `.hash` file. -/
-def fetchFileTrace (file : FilePath) : BuildM BuildTrace := do
+def fetchFileTrace (file : FilePath) : JobM BuildTrace := do
   if (← getTrustHash) then
     let hashFile := FilePath.mk <| file.toString ++ ".hash"
     if let some hash ← Hash.load? hashFile then
@@ -76,24 +83,48 @@ def cacheFileHash (file : FilePath) : IO Hash := do
   return hash
 
 /--
-Build `file` using `build` unless it already exists and `depTrace` matches
+Replays the JSON log in `logFile` (if it exists).
+If the log file is malformed, logs a warning.
+-/
+def replayBuildLog (logFile : FilePath) : LogIO PUnit := do
+  match (← IO.FS.readFile logFile |>.toBaseIO) with
+  | .ok contents =>
+    match Json.parse contents >>= fromJson? with
+    | .ok entries => Log.mk entries |>.replay
+    | .error e => logWarning s!"cached build log is corrupted: {e}"
+  | .error (.noFileOrDirectory ..) => pure ()
+  | .error e => logWarning s!"failed to read cached build log: {e}"
+
+/-- Saves the log produce by `build` as JSON to `logFile`. -/
+def cacheBuildLog (logFile : FilePath) (build : JobM PUnit) : JobM PUnit := do
+  let iniSz ← getLogSize
+  build
+  let log ← getLog
+  let log := log.entries.extract iniSz log.entries.size
+  unless log.isEmpty do
+    IO.FS.writeFile logFile (toJson log).pretty
+
+/--
+Builds `file` using `build` unless it already exists and `depTrace` matches
 the trace stored in the `.trace` file. If built, save the new `depTrace` and
 cache `file`'s hash in a `.hash` file. Otherwise, try to fetch the hash from
-the `.hash` file using `fetchFileTrace`.
+the `.hash` file using `fetchFileTrace`. Build logs (if any) are saved to
+a `.log.json` file and replayed from there if the build is skipped.
 
-By example, for `file := "foo.c"`, compare `depTrace` with that in `foo.c.trace`
-and cache the hash using `foo.c.hash`.
+For example, given `file := "foo.c"`, compares `depTrace` with that in
+`foo.c.trace` with the hash cache in `foo.c.hash` and the log cache in
+`foo.c.log.json`.
 -/
-def buildFileUnlessUpToDate (file : FilePath)
-(depTrace : BuildTrace) (build : BuildM PUnit) : BuildM BuildTrace := do
+def buildFileUnlessUpToDate (
+  file : FilePath) (depTrace : BuildTrace) (build : JobM PUnit)
+: JobM BuildTrace := do
   let traceFile := FilePath.mk <| file.toString ++ ".trace"
-  if (← depTrace.checkUpToDate file traceFile) then
+  let logFile := FilePath.mk <| file.toString ++ ".log.json"
+  let build := cacheBuildLog logFile build
+  if (← buildUnlessUpToDate? file depTrace traceFile build) then
+    replayBuildLog logFile
     fetchFileTrace file
   else
-    if (← getNoBuild) then
-      IO.Process.exit noBuildCode.toUInt8
-    build
-    depTrace.writeToFile traceFile
     return .mk (← cacheFileHash file) (← getMTime file)
 
 /--
@@ -101,8 +132,9 @@ Build `file` using `build` after `dep` completes if the dependency's
 trace (and/or `extraDepTrace`) has changed.
 -/
 @[inline] def buildFileAfterDep
-(file : FilePath) (dep : BuildJob α) (build : α → BuildM PUnit)
-(extraDepTrace : BuildM _ := pure BuildTrace.nil) : SchedulerM (BuildJob FilePath) :=
+  (file : FilePath) (dep : BuildJob α) (build : α → JobM PUnit)
+  (extraDepTrace : JobM _ := pure BuildTrace.nil)
+: SpawnM (BuildJob FilePath) :=
   dep.bindSync fun depInfo depTrace => do
     let depTrace := depTrace.mix (← extraDepTrace)
     let trace ← buildFileUnlessUpToDate file depTrace <| build depInfo
@@ -110,20 +142,22 @@ trace (and/or `extraDepTrace`) has changed.
 
 /-- Build `file` using `build` after `deps` have built if any of their traces change. -/
 @[inline] def buildFileAfterDepList
-(file : FilePath) (deps : List (BuildJob α)) (build : List α → BuildM PUnit)
-(extraDepTrace : BuildM _ := pure BuildTrace.nil) : SchedulerM (BuildJob FilePath) := do
+  (file : FilePath) (deps : List (BuildJob α)) (build : List α → JobM PUnit)
+  (extraDepTrace : JobM _ := pure BuildTrace.nil)
+: SpawnM (BuildJob FilePath) := do
   buildFileAfterDep file (← BuildJob.collectList deps) build extraDepTrace
 
 /-- Build `file` using `build` after `deps` have built if any of their traces change. -/
 @[inline] def buildFileAfterDepArray
-(file : FilePath) (deps : Array (BuildJob α)) (build : Array α → BuildM PUnit)
-(extraDepTrace : BuildM _ := pure BuildTrace.nil) : SchedulerM (BuildJob FilePath) := do
+  (file : FilePath) (deps : Array (BuildJob α)) (build : Array α → JobM PUnit)
+  (extraDepTrace : JobM _ := pure BuildTrace.nil)
+: SpawnM (BuildJob FilePath) := do
   buildFileAfterDep file (← BuildJob.collectArray deps) build extraDepTrace
 
 /-! ## Common Builds -/
 
 /-- A build job for file that is expected to already exist (e.g., a source file). -/
-def inputFile (path : FilePath) : SchedulerM (BuildJob FilePath) :=
+def inputFile (path : FilePath) : SpawnM (BuildJob FilePath) :=
   Job.async <| (path, ·) <$> computeTrace path
 
 /--
@@ -141,54 +175,58 @@ be `weakArgs` to avoid build artifact incompatibility between systems
 You can add more components to the trace via `extraDepTrace`,
 which will be computed in the resulting `BuildJob` before building.
 -/
-@[inline] def buildO (name : String)
-(oFile : FilePath) (srcJob : BuildJob FilePath)
-(weakArgs traceArgs : Array String := #[]) (compiler : FilePath := "cc")
-(extraDepTrace : BuildM _ := pure BuildTrace.nil) : SchedulerM (BuildJob FilePath) :=
+@[inline] def buildO
+  (oFile : FilePath) (srcJob : BuildJob FilePath)
+  (weakArgs traceArgs : Array String := #[]) (compiler : FilePath := "cc")
+  (extraDepTrace : JobM _ := pure BuildTrace.nil)
+: SpawnM (BuildJob FilePath) :=
   let extraDepTrace :=
     return (← extraDepTrace).mix <| (pureHash traceArgs).mix platformTrace
   buildFileAfterDep oFile srcJob (extraDepTrace := extraDepTrace) fun srcFile => do
-    compileO name oFile srcFile (weakArgs ++ traceArgs) compiler
+    compileO oFile srcFile (weakArgs ++ traceArgs) compiler
 
 /-- Build an object file from a source fie job (i.e, a `lean -c` output) using `leanc`. -/
-@[inline] def buildLeanO (name : String)
-(oFile : FilePath) (srcJob : BuildJob FilePath)
-(weakArgs traceArgs : Array String := #[]) : SchedulerM (BuildJob FilePath) :=
+@[inline] def buildLeanO
+  (oFile : FilePath) (srcJob : BuildJob FilePath)
+  (weakArgs traceArgs : Array String := #[])
+: SpawnM (BuildJob FilePath) :=
   let extraDepTrace :=
     return (← getLeanTrace).mix <| (pureHash traceArgs).mix platformTrace
   buildFileAfterDep oFile srcJob (extraDepTrace := extraDepTrace) fun srcFile => do
-     compileO name oFile srcFile (weakArgs ++ traceArgs) (← getLeanc)
+     compileO oFile srcFile (weakArgs ++ traceArgs) (← getLeanc)
 
 /-- Build a static library from object file jobs using the `ar` packaged with Lean. -/
-def buildStaticLib (libFile : FilePath)
-(oFileJobs : Array (BuildJob FilePath)) : SchedulerM (BuildJob FilePath) :=
-  let name := libFile.fileName.getD libFile.toString
+def buildStaticLib
+  (libFile : FilePath) (oFileJobs : Array (BuildJob FilePath))
+: SpawnM (BuildJob FilePath) :=
   buildFileAfterDepArray libFile oFileJobs fun oFiles => do
-    compileStaticLib name libFile oFiles (← getLeanAr)
+    compileStaticLib libFile oFiles (← getLeanAr)
 
 /-- Build a shared library by linking the results of `linkJobs` using `leanc`. -/
 def buildLeanSharedLib
-(libFile : FilePath) (linkJobs : Array (BuildJob FilePath))
-(weakArgs traceArgs : Array String := #[]) : SchedulerM (BuildJob FilePath) :=
-  let name := libFile.fileName.getD libFile.toString
+  (libFile : FilePath) (linkJobs : Array (BuildJob FilePath))
+  (weakArgs traceArgs : Array String := #[])
+: SpawnM (BuildJob FilePath) :=
   let extraDepTrace :=
     return (← getLeanTrace).mix <| (pureHash traceArgs).mix platformTrace
   buildFileAfterDepArray libFile linkJobs (extraDepTrace := extraDepTrace) fun links => do
-    compileSharedLib name libFile (links.map toString ++ weakArgs ++ traceArgs) (← getLeanc)
+    compileSharedLib libFile (links.map toString ++ weakArgs ++ traceArgs) (← getLeanc)
 
 /-- Build an executable by linking the results of `linkJobs` using `leanc`. -/
 def buildLeanExe
-(exeFile : FilePath) (linkJobs : Array (BuildJob FilePath))
-(weakArgs traceArgs : Array String := #[]) : SchedulerM (BuildJob FilePath) :=
-  let name := exeFile.fileName.getD exeFile.toString
+  (exeFile : FilePath) (linkJobs : Array (BuildJob FilePath))
+  (weakArgs traceArgs : Array String := #[])
+: SpawnM (BuildJob FilePath) :=
   let extraDepTrace :=
     return (← getLeanTrace).mix <| (pureHash traceArgs).mix platformTrace
   buildFileAfterDepArray exeFile linkJobs (extraDepTrace := extraDepTrace) fun links => do
-    compileExe name exeFile links (weakArgs ++ traceArgs) (← getLeanc)
+    compileExe exeFile links (weakArgs ++ traceArgs) (← getLeanc)
 
 /-- Build a shared library from a static library using `leanc`. -/
-def buildLeanSharedLibOfStatic (staticLibJob : BuildJob FilePath)
-(weakArgs traceArgs : Array String := #[]) : SchedulerM (BuildJob FilePath) :=
+def buildLeanSharedLibOfStatic
+  (staticLibJob : BuildJob FilePath)
+  (weakArgs traceArgs : Array String := #[])
+: SpawnM (BuildJob FilePath) :=
   staticLibJob.bindSync fun staticLib staticTrace => do
     let dynlib := staticLib.withExtension sharedLibExt
     let baseArgs :=
@@ -200,13 +238,11 @@ def buildLeanSharedLibOfStatic (staticLibJob : BuildJob FilePath)
       (← getLeanTrace).mix <| (pureHash traceArgs).mix <| platformTrace
     let args := baseArgs ++ weakArgs ++ traceArgs
     let trace ← buildFileUnlessUpToDate dynlib depTrace do
-      let name := dynlib.fileName.getD dynlib.toString
-      compileSharedLib name dynlib args (← getLeanc)
+      compileSharedLib dynlib args (← getLeanc)
     return (dynlib, trace)
 
 /-- Construct a `Dynlib` object for a shared library target. -/
-def computeDynlibOfShared
-(sharedLibTarget : BuildJob FilePath) : SchedulerM (BuildJob Dynlib) :=
+def computeDynlibOfShared (sharedLibTarget : BuildJob FilePath) : SpawnM (BuildJob Dynlib) :=
   sharedLibTarget.bindSync fun sharedLib trace => do
     if let some stem := sharedLib.fileStem then
       if Platform.isWindows then

src/lake/Lake/Build/Data.lean

@@ -83,10 +83,11 @@ abbrev BuildData : BuildKey → Type
 | .targetFacet _ _ f => TargetData f
 | .customTarget p t => CustomData (p, t)
 
+instance (priority := low) : FamilyDef BuildData k (BuildData k) := ⟨rfl⟩
 instance (priority := low) : FamilyDef BuildData (.moduleFacet m f) (ModuleData f) := ⟨rfl⟩
 instance (priority := low) : FamilyDef BuildData (.packageFacet p f) (PackageData f) := ⟨rfl⟩
 instance (priority := low) : FamilyDef BuildData (.targetFacet p t f) (TargetData f) := ⟨rfl⟩
-instance (priority := low)  : FamilyDef BuildData (.customTarget p t) (CustomData (p,t)) := ⟨rfl⟩
+instance (priority := low) : FamilyDef BuildData (.customTarget p t) (CustomData (p,t)) := ⟨rfl⟩
 
 --------------------------------------------------------------------------------
 /-! ## Macros for Declaring Build Data                                        -/

src/lake/Lake/Build/Executable.lean

@@ -11,8 +11,8 @@ namespace Lake
 The build function definition for a Lean executable.
 -/
 
-protected def LeanExe.recBuildExe
-(self : LeanExe) : IndexBuildM (BuildJob FilePath) := do
+def LeanExe.recBuildExe (self : LeanExe) : FetchM (BuildJob FilePath) :=
+  withRegisterJob s!"Linking {self.fileName}" do
   let imports ← self.root.transImports.fetch
   let mut linkJobs := #[← self.root.o.fetch]
   for mod in imports do for facet in mod.nativeFacets self.supportInterpreter do

src/lake/Lake/Build/Fetch.lean

@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2024 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.Util.Error
+import Lake.Util.Cycle
+import Lake.Util.EquipT
+import Lake.Build.Info
+import Lake.Build.Store
+
+/-! # Recursive Building
+
+This module defines Lake's top-level build monad, `FetchM`, used
+for performing recursive builds. A recursive build is a build function
+which can fetch the results of other (recursive) builds. This is done
+using the `fetch` function defined in this module.
+-/
+
+namespace Lake
+
+/-- A recursive build of a Lake build store that may encounter a cycle. -/
+abbrev RecBuildM := CallStackT BuildKey <| StateT BuildStore <| CoreBuildM
+
+/-- Run a recursive build. -/
+@[inline] def RecBuildM.run
+  (stack : CallStack BuildKey) (store : BuildStore) (build : RecBuildM α)
+: CoreBuildM (α × BuildStore) := do
+  build stack store
+
+/-- Run a recursive build in a fresh build store. -/
+@[inline] def RecBuildM.run' (build : RecBuildM α) : CoreBuildM α := do
+  (·.1) <$> build.run {} {}
+
+/-- Log build cycle and error. -/
+@[specialize] def buildCycleError [MonadError m] (cycle : Cycle BuildKey) : m α :=
+  error s!"build cycle detected:\n{"\n".intercalate <| cycle.map (s!"  {·}")}"
+
+instance : MonadCycleOf BuildKey RecBuildM where
+  throwCycle := buildCycleError
+
+/-- A build function for any element of the Lake build index. -/
+abbrev IndexBuildFn (m : Type → Type v) :=
+  -- `DFetchFn BuildInfo (BuildData ·.key) m` with less imports
+  (info : BuildInfo) → m (BuildData info.key)
+
+/-- A transformer to equip a monad with a build function for the Lake index. -/
+abbrev IndexT (m : Type → Type v) := EquipT (IndexBuildFn m) m
+
+/-- The top-level monad for Lake build functions. -/
+abbrev FetchM := IndexT RecBuildM
+
+/-- The top-level monad for Lake build functions. **Renamed `FetchM`.** -/
+@[deprecated FetchM] abbrev IndexBuildM := FetchM
+
+/-- The old build monad. **Uses should generally be replaced by `FetchM`.** -/
+@[deprecated FetchM] abbrev BuildM := CoreBuildM
+
+/-- Fetch the result associated with the info using the Lake build index. -/
+@[inline] def BuildInfo.fetch (self : BuildInfo) [FamilyOut BuildData self.key α] : FetchM α :=
+  fun build => cast (by simp) <| build self
+
+export BuildInfo (fetch)

src/lake/Lake/Build/Imports.lean

@@ -18,7 +18,7 @@ the build jobs of their precompiled modules and the build jobs of said modules'
 external libraries.
 -/
 def recBuildImports (imports : Array Module)
-: IndexBuildM (Array (BuildJob Unit) × Array (BuildJob Dynlib) × Array (BuildJob Dynlib)) := do
+: FetchM (Array (BuildJob Unit) × Array (BuildJob Dynlib) × Array (BuildJob Dynlib)) := do
   let mut modJobs := #[]
   let mut precompileImports := OrdModuleSet.empty
   for mod in imports do
@@ -37,18 +37,23 @@ Builds an `Array` of module imports. Used by `lake setup-file` to build modules
 for the Lean server and by `lake lean` to build the imports of a file.
 Returns the set of module dynlibs built (so they can be loaded by Lean).
 -/
-def buildImportsAndDeps (imports : Array Module) : BuildM (Array FilePath) := do
-  let ws ← getWorkspace
+def buildImportsAndDeps (imports : Array Module) : FetchM (BuildJob (Array FilePath)) := do
   if imports.isEmpty then
     -- build the package's (and its dependencies') `extraDepTarget`
-    ws.root.extraDep.build >>= (·.materialize)
-    return #[]
+    (← getRootPackage).extraDep.fetch <&> (·.map fun _ => #[])
   else
     -- build local imports from list
     let (modJobs, precompileJobs, externLibJobs) ←
-      recBuildImports imports |>.run.run
-    modJobs.forM (·.await)
-    let modLibs ← precompileJobs.mapM (·.await <&> (·.path))
-    let externLibs ← externLibJobs.mapM (·.await <&> (·.path))
-    -- NOTE: Lean wants the external library symbols before module symbols
-    return externLibs ++ modLibs
+      recBuildImports imports
+    let modJob ← BuildJob.mixArray modJobs
+    let precompileJob ← BuildJob.collectArray precompileJobs
+    let externLibJob ← BuildJob.collectArray externLibJobs
+    let job ←
+      modJob.bindAsync fun _ modTrace =>
+      precompileJob.bindAsync fun modLibs modLibTrace =>
+      externLibJob.bindSync fun externLibs externTrace => do
+        -- NOTE: Lean wants the external library symbols before module symbols
+        let libs := (externLibs ++ modLibs).map (·.path)
+        let trace := modTrace.mix modLibTrace |>.mix externTrace
+        return (libs, trace)
+    return job

src/lake/Lake/Build/Index.lean

@@ -3,7 +3,6 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-import Lake.Build.Targets
 import Lake.Build.Executable
 import Lake.Build.Topological
 
@@ -20,20 +19,25 @@ open Lean
 namespace Lake
 
 /--
-Converts a conveniently typed target facet build function into its
-dynamically typed equivalent.
+Converts a conveniently-typed target facet build function into its
+dynamically-typed equivalent.
 -/
-@[macro_inline] def mkTargetFacetBuild (facet : Name) (build : IndexBuildM α)
-[h : FamilyOut TargetData facet α] : IndexBuildM (TargetData facet) :=
+@[macro_inline] def mkTargetFacetBuild
+  (facet : Name) (build : FetchM (BuildJob α))
+  [h : FamilyOut TargetData facet (BuildJob α)]
+: FetchM (TargetData facet) :=
   cast (by rw [← h.family_key_eq_type]) build
 
-def ExternLib.recBuildStatic (lib : ExternLib) : IndexBuildM (BuildJob FilePath) := do
+def ExternLib.recBuildStatic (lib : ExternLib) : FetchM (BuildJob FilePath) :=
+  withRegisterJob s!"Building {lib.staticTargetName.toString}" do
   lib.config.getJob <$> fetch (lib.pkg.target lib.staticTargetName)
 
-def ExternLib.recBuildShared (lib : ExternLib) : IndexBuildM (BuildJob FilePath) := do
+def ExternLib.recBuildShared (lib : ExternLib) : FetchM (BuildJob FilePath) :=
+  withRegisterJob s!"Linking {lib.staticTargetName.toString}" do
   buildLeanSharedLibOfStatic (← lib.static.fetch) lib.linkArgs
 
-def ExternLib.recComputeDynlib (lib : ExternLib) : IndexBuildM (BuildJob Dynlib) := do
+def ExternLib.recComputeDynlib (lib : ExternLib) : FetchM (BuildJob Dynlib) := do
+  withRegisterJob s!"Computing {lib.staticTargetName.toString} dynlib" do
   computeDynlibOfShared (← lib.shared.fetch)
 
 /-!
@@ -41,7 +45,7 @@ def ExternLib.recComputeDynlib (lib : ExternLib) : IndexBuildM (BuildJob Dynlib)
 -/
 
 /-- Recursive build function for anything in the Lake build index. -/
-def recBuildWithIndex : (info : BuildInfo) → IndexBuildM (BuildData info.key)
+def recBuildWithIndex : (info : BuildInfo) → FetchM (BuildData info.key)
 | .moduleFacet mod facet => do
   if let some config := (← getWorkspace).findModuleFacetConfig? facet then
     config.build mod
@@ -72,41 +76,8 @@ def recBuildWithIndex : (info : BuildInfo) → IndexBuildM (BuildData info.key)
   mkTargetFacetBuild ExternLib.dynlibFacet lib.recComputeDynlib
 
 /--
-Run the given recursive build using the Lake build index
+Run a recursive Lake build using the Lake build index
 and a topological / suspending scheduler.
 -/
-def IndexBuildM.run (build : IndexBuildM α) : RecBuildM α :=
-  build <| recFetchMemoize BuildInfo.key recBuildWithIndex
-
-/--
-Recursively build the given info using the Lake build index
-and a topological / suspending scheduler.
--/
-def buildIndexTop' (info : BuildInfo) : RecBuildM (BuildData info.key) :=
-  recFetchMemoize BuildInfo.key recBuildWithIndex info
-
-/--
-Recursively build the given info using the Lake build index
-and a topological / suspending scheduler and return the dynamic result.
--/
-@[macro_inline] def buildIndexTop (info : BuildInfo)
-[FamilyOut BuildData info.key α] : RecBuildM α := do
-  cast (by simp) <| buildIndexTop' info
-
-/-- Build the given Lake target in a fresh build store. -/
-@[inline] def BuildInfo.build
-(self : BuildInfo) [FamilyOut BuildData self.key α] : BuildM α :=
-  buildIndexTop self |>.run
-
-export BuildInfo (build)
-
-/-! ### Lean Executable Builds -/
-
-@[inline] protected def LeanExe.build (self : LeanExe) : BuildM (BuildJob FilePath) :=
-  self.exe.build
-
-@[inline] protected def LeanExeConfig.build (self : LeanExeConfig) : BuildM (BuildJob FilePath) := do
-  (← self.get).build
-
-@[inline] protected def LeanExe.fetch (self : LeanExe) : IndexBuildM (BuildJob FilePath) :=
-  self.exe.fetch
+def FetchM.run (x : FetchM α) : RecBuildM α :=
+  x (inline <| recFetchMemoize BuildInfo.key recBuildWithIndex)

src/lake/Lake/Build/Info.lean

@@ -6,7 +6,6 @@ Authors: Mac Malone
 import Lake.Config.LeanExe
 import Lake.Config.ExternLib
 import Lake.Build.Facets
-import Lake.Util.EquipT
 
 /-!
 # Build Info
@@ -62,7 +61,7 @@ abbrev ExternLib.dynlibBuildKey (self : ExternLib) : BuildKey :=
 /-! ### Build Info to Key -/
 
 /-- The key that identifies the build in the Lake build store. -/
-abbrev BuildInfo.key : (self : BuildInfo) → BuildKey
+@[reducible] def BuildInfo.key : (self : BuildInfo) → BuildKey
 | moduleFacet m f => m.facetBuildKey f
 | packageFacet p f => p.facetBuildKey f
 | libraryFacet l f => l.facetBuildKey f
@@ -109,27 +108,6 @@ instance [FamilyOut TargetData ExternLib.dynlibFacet α]
 : FamilyDef BuildData (BuildInfo.key (.dynlibExternLib l)) α where
   family_key_eq_type := by unfold BuildData; simp
 
---------------------------------------------------------------------------------
-/-! ## Recursive Building                                                     -/
---------------------------------------------------------------------------------
-
-/-- A build function for any element of the Lake build index. -/
-abbrev IndexBuildFn (m : Type → Type v) :=
-  -- `DBuildFn BuildInfo (BuildData ·.key) m` with less imports
-  (info : BuildInfo) → m (BuildData info.key)
-
-/-- A transformer to equip a monad with a build function for the Lake index. -/
-abbrev IndexT (m : Type → Type v) := EquipT (IndexBuildFn m) m
-
-/-- The monad for build functions that are part of the index. -/
-abbrev IndexBuildM := IndexT RecBuildM
-
-/-- Fetch the result associated with the info using the Lake build index. -/
-@[inline] def BuildInfo.fetch (self : BuildInfo) [FamilyOut BuildData self.key α] : IndexBuildM α :=
-  fun build => cast (by simp) <| build self
-
-export BuildInfo (fetch)
-
 --------------------------------------------------------------------------------
 /-! ## Build Info & Facets                                                    -/
 --------------------------------------------------------------------------------