import all

.github/workflows/check-prelude.yml

@@ -14,7 +14,6 @@ jobs:
           sparse-checkout: |
             src/Lean
             src/Std
-            src/lake/Lake
       - name: Check Prelude
         run: |
           failed_files=""
@@ -22,7 +21,7 @@ jobs:
             if ! grep -q "^prelude$" "$file"; then
               failed_files="$failed_files$file\n"
             fi
-          done < <(find src/Lean src/Std src/lake/Lake -name '*.lean' -print0)
+          done < <(find src/Lean src/Std -name '*.lean' -print0)
           if [ -n "$failed_files" ]; then
             echo -e "The following files should use 'prelude':\n$failed_files"
             exit 1

.github/workflows/pr-release.yml

@@ -34,7 +34,7 @@ jobs:
       - name: Download artifact from the previous workflow.
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         id: download-artifact
-        uses: dawidd6/action-download-artifact@v7 # https://github.com/marketplace/actions/download-workflow-artifact
+        uses: dawidd6/action-download-artifact@v6 # https://github.com/marketplace/actions/download-workflow-artifact
         with:
           run_id: ${{ github.event.workflow_run.id }}
           path: artifacts
@@ -111,7 +111,7 @@ jobs:
 
       - name: 'Setup jq'
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: dcarbone/install-jq-action@v3.0.1
+        uses: dcarbone/install-jq-action@v2.1.0
 
       # Check that the most recently nightly coincides with 'git merge-base HEAD master'
       - name: Check merge-base and nightly-testing-YYYY-MM-DD

RELEASES.md

@@ -8,15 +8,10 @@ This file contains work-in-progress notes for the upcoming release, as well as p
 Please check the [releases](https://github.com/leanprover/lean4/releases) page for the current status
 of each version.
 
-v4.16.0
-----------
-
-Development in progress.
-
 v4.15.0
 ----------
 
-Release candidate, release notes will be copied from the branch `releases/v4.15.0` once completed.
+Development in progress.
 
 v4.14.0
 ----------
@@ -93,7 +88,7 @@ v4.13.0
   * [#4768](https://github.com/leanprover/lean4/pull/4768) fixes a parse error when `..` appears with a `.` on the next line
 
 * Metaprogramming
-  * [#3090](https://github.com/leanprover/lean4/pull/3090) handles level parameters in `Meta.evalExpr` (@eric-wieser)
+  * [#3090](https://github.com/leanprover/lean4/pull/3090) handles level parameters in `Meta.evalExpr` (@eric-wieser)  
   * [#5401](https://github.com/leanprover/lean4/pull/5401) instance for `Inhabited (TacticM α)` (@alexkeizer)
   * [#5412](https://github.com/leanprover/lean4/pull/5412) expose Kernel.check for debugging purposes
   * [#5556](https://github.com/leanprover/lean4/pull/5556) improves the "invalid projection" type inference error in `inferType`.

debug.log

@@ -0,0 +1 @@
+[0829/202002.254:ERROR:crashpad_client_win.cc(868)] not connected

script/mathlib-bench

@@ -1,12 +0,0 @@
-#! /bin/env bash
-# Open a Mathlib4 PR for benchmarking a given Lean 4 PR
-
-set -euo pipefail
-
-[ $# -eq 1 ] || (echo "usage: $0 <lean4 PR #>"; exit 1)
-
-LEAN_PR=$1
-PR_RESPONSE=$(gh api repos/leanprover-community/mathlib4/pulls -X POST -f head=lean-pr-testing-$LEAN_PR -f base=nightly-testing -f title="leanprover/lean4#$LEAN_PR benchmarking" -f draft=true -f body="ignore me")
-PR_NUMBER=$(echo "$PR_RESPONSE" | jq '.number')
-echo "opened https://github.com/leanprover-community/mathlib4/pull/$PR_NUMBER"
-gh api repos/leanprover-community/mathlib4/issues/$PR_NUMBER/comments -X POST -f body="!bench" > /dev/null

src/CMakeLists.txt

@@ -10,7 +10,7 @@ endif()
 include(ExternalProject)
 project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
-set(LEAN_VERSION_MINOR 16)
+set(LEAN_VERSION_MINOR 15)
 set(LEAN_VERSION_PATCH 0)
 set(LEAN_VERSION_IS_RELEASE 0)  # This number is 1 in the release revision, and 0 otherwise.
 set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")

src/Init/Data/Array/Attach.lean

@@ -251,7 +251,7 @@ theorem getElem?_attach {xs : Array α} {i : Nat} :
 theorem getElem_attachWith {xs : Array α} {P : α → Prop} {H : ∀ a ∈ xs, P a}
     {i : Nat} (h : i < (xs.attachWith P H).size) :
     (xs.attachWith P H)[i] = ⟨xs[i]'(by simpa using h), H _ (getElem_mem (by simpa using h))⟩ :=
-  getElem_pmap _ _ h
+  getElem_pmap ..
 
 @[simp]
 theorem getElem_attach {xs : Array α} {i : Nat} (h : i < xs.attach.size) :

src/Init/Data/Array/Lemmas.lean

@@ -59,14 +59,6 @@ namespace List
 
 open Array
 
-theorem toArray_inj {a b : List α} (h : a.toArray = b.toArray) : a = b := by
-  cases a with
-  | nil => simpa using h
-  | cons a as =>
-    cases b with
-    | nil => simp at h
-    | cons b bs => simpa using h
-
 @[simp] theorem size_toArrayAux {a : List α} {b : Array α} :
     (a.toArrayAux b).size = b.size + a.length := by
   simp [size]
@@ -404,11 +396,6 @@ namespace Array
 
 /-! ## Preliminaries -/
 
-/-! ### toList -/
-
-theorem toList_inj {a b : Array α} (h : a.toList = b.toList) : a = b := by
-  cases a; cases b; simpa using h
-
 /-! ### empty -/
 
 @[simp] theorem empty_eq {xs : Array α} : #[] = xs ↔ xs = #[] := by

src/Init/Data/Int/DivModLemmas.lean

@@ -125,7 +125,7 @@ theorem eq_one_of_mul_eq_one_right {a b : Int} (H : 0 ≤ a) (H' : a * b = 1) :
   eq_one_of_dvd_one H ⟨b, H'.symm⟩
 
 theorem eq_one_of_mul_eq_one_left {a b : Int} (H : 0 ≤ b) (H' : a * b = 1) : b = 1 :=
-  eq_one_of_mul_eq_one_right (b := a) H <| by rw [Int.mul_comm, H']
+  eq_one_of_mul_eq_one_right H <| by rw [Int.mul_comm, H']
 
 /-! ### *div zero  -/
 

src/Init/Data/List/BasicAux.lean

@@ -155,8 +155,7 @@ def mapMono (as : List α) (f : α → α) : List α :=
 
 /-! ## Additional lemmas required for bootstrapping `Array`. -/
 
-theorem getElem_append_left {as bs : List α} (h : i < as.length) {h' : i < (as ++ bs).length} :
-    (as ++ bs)[i] = as[i] := by
+theorem getElem_append_left {as bs : List α} (h : i < as.length) {h'} : (as ++ bs)[i] = as[i] := by
   induction as generalizing i with
   | nil => trivial
   | cons a as ih =>

src/Init/Data/List/Count.lean

@@ -162,10 +162,6 @@ theorem countP_filterMap (p : β → Bool) (f : α → Option β) (l : List α)
 
 @[deprecated countP_flatten (since := "2024-10-14")] abbrev countP_join := @countP_flatten
 
-theorem countP_flatMap (p : β → Bool) (l : List α) (f : α → List β) :
-    countP p (l.flatMap f) = sum (map (countP p ∘ f) l) := by
-  rw [List.flatMap, countP_flatten, map_map]
-
 @[simp] theorem countP_reverse (l : List α) : countP p l.reverse = countP p l := by
   simp [countP_eq_length_filter, filter_reverse]
 
@@ -330,9 +326,6 @@ theorem count_filterMap {α} [BEq β] (b : β) (f : α → Option β) (l : List
   · simp
   · simp
 
-theorem count_flatMap {α} [BEq β] (l : List α) (f : α → List β) (x : β) :
-    count x (l.flatMap f) = sum (map (count x ∘ f) l) := countP_flatMap _ _ _
-
 theorem count_erase (a b : α) :
     ∀ l : List α, count a (l.erase b) = count a l - if b == a then 1 else 0
   | [] => by simp

src/Init/Data/List/Lemmas.lean

@@ -416,9 +416,8 @@ theorem getElem_of_mem : ∀ {a} {l : List α}, a ∈ l → ∃ (n : Nat) (h : n
   | _, _ :: _, .head .. => ⟨0, Nat.succ_pos _, rfl⟩
   | _, _ :: _, .tail _ m => let ⟨n, h, e⟩ := getElem_of_mem m; ⟨n+1, Nat.succ_lt_succ h, e⟩
 
-theorem getElem?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n : Nat, l[n]? = some a := by
-  let ⟨n, _, e⟩ := getElem_of_mem h
-  exact ⟨n, e ▸ getElem?_eq_getElem _⟩
+theorem getElem?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n : Nat, l[n]? = some a :=
+  let ⟨n, _, e⟩ := getElem_of_mem h; ⟨n, e ▸ getElem?_eq_getElem _⟩
 
 theorem mem_of_getElem? {l : List α} {n : Nat} {a : α} (e : l[n]? = some a) : a ∈ l :=
   let ⟨_, e⟩ := getElem?_eq_some_iff.1 e; e ▸ getElem_mem ..
@@ -950,7 +949,7 @@ theorem getLast_eq_getElem : ∀ (l : List α) (h : l ≠ []),
   | _ :: _ :: _, _ => by
     simp [getLast, get, Nat.succ_sub_succ, getLast_eq_getElem]
 
-theorem getElem_length_sub_one_eq_getLast (l : List α) (h : l.length - 1 < l.length) :
+theorem getElem_length_sub_one_eq_getLast (l : List α) (h) :
     l[l.length - 1] = getLast l (by cases l; simp at h; simp) := by
   rw [← getLast_eq_getElem]
 
@@ -1078,8 +1077,7 @@ theorem head_eq_getElem (l : List α) (h : l ≠ []) : head l h = l[0]'(length_p
   | nil => simp at h
   | cons _ _ => simp
 
-theorem getElem_zero_eq_head (l : List α) (h : 0 < l.length) :
-    l[0] = head l (by simpa [length_pos] using h) := by
+theorem getElem_zero_eq_head (l : List α) (h) : l[0] = head l (by simpa [length_pos] using h) := by
   cases l with
   | nil => simp at h
   | cons _ _ => simp
@@ -1671,7 +1669,7 @@ theorem filterMap_eq_cons_iff {l} {b} {bs} :
 @[simp] theorem cons_append_fun (a : α) (as : List α) :
     (fun bs => ((a :: as) ++ bs)) = fun bs => a :: (as ++ bs) := rfl
 
-theorem getElem_append {l₁ l₂ : List α} (n : Nat) (h : n < (l₁ ++ l₂).length) :
+theorem getElem_append {l₁ l₂ : List α} (n : Nat) (h) :
     (l₁ ++ l₂)[n] = if h' : n < l₁.length then l₁[n] else l₂[n - l₁.length]'(by simp at h h'; exact Nat.sub_lt_left_of_lt_add h' h) := by
   split <;> rename_i h'
   · rw [getElem_append_left h']
@@ -2213,11 +2211,6 @@ theorem flatMap_def (l : List α) (f : α → List β) : l.flatMap f = flatten (
 
 @[simp] theorem flatMap_id (l : List (List α)) : List.flatMap l id = l.flatten := by simp [flatMap_def]
 
-@[simp]
-theorem length_flatMap (l : List α) (f : α → List β) :
-    length (l.flatMap f) = sum (map (length ∘ f) l) := by
-  rw [List.flatMap, length_flatten, map_map]
-
 @[simp] theorem mem_flatMap {f : α → List β} {b} {l : List α} : b ∈ l.flatMap f ↔ ∃ a, a ∈ l ∧ b ∈ f a := by
   simp [flatMap_def, mem_flatten]
   exact ⟨fun ⟨_, ⟨a, h₁, rfl⟩, h₂⟩ => ⟨a, h₁, h₂⟩, fun ⟨a, h₁, h₂⟩ => ⟨_, ⟨a, h₁, rfl⟩, h₂⟩⟩
@@ -2874,7 +2867,7 @@ are often used for theorems about `Array.pop`.
 @[simp] theorem getElem_dropLast : ∀ (xs : List α) (i : Nat) (h : i < xs.dropLast.length),
     xs.dropLast[i] = xs[i]'(Nat.lt_of_lt_of_le h (length_dropLast .. ▸ Nat.pred_le _))
   | _::_::_, 0, _ => rfl
-  | _::_::_, i+1, h => getElem_dropLast _ i (Nat.add_one_lt_add_one_iff.mp h)
+  | _::_::_, i+1, _ => getElem_dropLast _ i _
 
 @[deprecated getElem_dropLast (since := "2024-06-12")]
 theorem get_dropLast (xs : List α) (i : Fin xs.dropLast.length) :

src/Init/Data/List/Sublist.lean

@@ -841,7 +841,7 @@ theorem isPrefix_iff : l₁ <+: l₂ ↔ ∀ i (h : i < l₁.length), l₂[i]? =
 theorem isPrefix_iff_getElem {l₁ l₂ : List α} :
     l₁ <+: l₂ ↔ ∃ (h : l₁.length ≤ l₂.length), ∀ x (hx : x < l₁.length),
       l₁[x] = l₂[x]'(Nat.lt_of_lt_of_le hx h) where
-  mp h := ⟨h.length_le, fun _ h' ↦ h.getElem h'⟩
+  mp h := ⟨h.length_le, fun _ _ ↦ h.getElem _⟩
   mpr h := by
     obtain ⟨hl, h⟩ := h
     induction l₂ generalizing l₁ with

src/Init/Data/List/TakeDrop.lean

@@ -65,13 +65,13 @@ theorem lt_length_of_take_ne_self {l : List α} {n} (h : l.take n ≠ l) : n < l
 theorem getElem_cons_drop : ∀ (l : List α) (i : Nat) (h : i < l.length),
     l[i] :: drop (i + 1) l = drop i l
   | _::_, 0, _ => rfl
-  | _::_, i+1, h => getElem_cons_drop _ i (Nat.add_one_lt_add_one_iff.mp h)
+  | _::_, i+1, _ => getElem_cons_drop _ i _
 
 @[deprecated getElem_cons_drop (since := "2024-06-12")]
 theorem get_cons_drop (l : List α) (i) : get l i :: drop (i + 1) l = drop i l := by
   simp
 
-theorem drop_eq_getElem_cons {n} {l : List α} (h : n < l.length) : drop n l = l[n] :: drop (n + 1) l :=
+theorem drop_eq_getElem_cons {n} {l : List α} (h) : drop n l = l[n] :: drop (n + 1) l :=
   (getElem_cons_drop _ n h).symm
 
 @[deprecated drop_eq_getElem_cons (since := "2024-06-12")]

src/Init/Data/Nat/Dvd.lean

@@ -39,9 +39,9 @@ protected theorem dvd_add_iff_right {k m n : Nat} (h : k ∣ m) : k ∣ n ↔ k
 protected theorem dvd_add_iff_left {k m n : Nat} (h : k ∣ n) : k ∣ m ↔ k ∣ m + n := by
   rw [Nat.add_comm]; exact Nat.dvd_add_iff_right h
 
-theorem dvd_mod_iff {k m n : Nat} (h: k ∣ n) : k ∣ m % n ↔ k ∣ m := by
-  have := Nat.dvd_add_iff_left (m := m % n) <| Nat.dvd_trans h <| Nat.dvd_mul_right n (m / n)
-  rwa [mod_add_div] at this
+theorem dvd_mod_iff {k m n : Nat} (h: k ∣ n) : k ∣ m % n ↔ k ∣ m :=
+  have := Nat.dvd_add_iff_left <| Nat.dvd_trans h <| Nat.dvd_mul_right n (m / n)
+  by rwa [mod_add_div] at this
 
 theorem le_of_dvd {m n : Nat} (h : 0 < n) : m ∣ n → m ≤ n
   | ⟨k, e⟩ => by

src/Init/Data/UInt/Bitwise.lean

@@ -1,39 +1,25 @@
 /-
 Copyright (c) 2024 Lean FRO, LLC. All Rights Reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel, Mac Malone
+Authors: Markus Himmel
 -/
 prelude
-import Init.Data.UInt.Lemmas
+import Init.Data.UInt.Basic
 import Init.Data.Fin.Bitwise
 import Init.Data.BitVec.Lemmas
 
 set_option hygiene false in
-macro "declare_bitwise_uint_theorems" typeName:ident bits:term:arg : command =>
+macro "declare_bitwise_uint_theorems" typeName:ident : command =>
 `(
 namespace $typeName
 
-@[simp] protected theorem toBitVec_and (a b : $typeName) : (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec := rfl
-@[simp] protected theorem toBitVec_or (a b : $typeName) : (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec := rfl
-@[simp] protected theorem toBitVec_xor (a b : $typeName) : (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec := rfl
-@[simp] protected theorem toBitVec_shiftLeft (a b : $typeName) : (a <<< b).toBitVec = a.toBitVec <<< (b.toBitVec % $bits) := rfl
-@[simp] protected theorem toBitVec_shiftRight (a b : $typeName) : (a >>> b).toBitVec = a.toBitVec >>> (b.toBitVec % $bits) := rfl
-
-@[simp] protected theorem toNat_and (a b : $typeName) : (a &&& b).toNat = a.toNat &&& b.toNat := by simp [toNat]
-@[simp] protected theorem toNat_or (a b : $typeName) : (a ||| b).toNat = a.toNat ||| b.toNat := by simp [toNat]
-@[simp] protected theorem toNat_xor (a b : $typeName) : (a ^^^ b).toNat = a.toNat ^^^ b.toNat := by simp [toNat]
-@[simp] protected theorem toNat_shiftLeft (a b : $typeName) : (a <<< b).toNat = a.toNat <<< (b.toNat % $bits) % 2 ^ $bits := by simp [toNat]
-@[simp] protected theorem toNat_shiftRight (a b : $typeName) : (a >>> b).toNat = a.toNat >>> (b.toNat % $bits) := by simp [toNat]
-
-open $typeName (toNat_and) in
-@[deprecated toNat_and (since := "2024-11-28")]
-protected theorem and_toNat (a b : $typeName) : (a &&& b).toNat = a.toNat &&& b.toNat := BitVec.toNat_and ..
+@[simp] protected theorem and_toNat (a b : $typeName) : (a &&& b).toNat = a.toNat &&& b.toNat := BitVec.toNat_and ..
 
 end $typeName
 )
 
-declare_bitwise_uint_theorems UInt8 8
-declare_bitwise_uint_theorems UInt16 16
-declare_bitwise_uint_theorems UInt32 32
-declare_bitwise_uint_theorems UInt64 64
-declare_bitwise_uint_theorems USize System.Platform.numBits
+declare_bitwise_uint_theorems UInt8
+declare_bitwise_uint_theorems UInt16
+declare_bitwise_uint_theorems UInt32
+declare_bitwise_uint_theorems UInt64
+declare_bitwise_uint_theorems USize

src/Init/Data/Vector/Lemmas.lean

@@ -11,15 +11,6 @@ import Init.Data.Vector.Basic
 Lemmas about `Vector α n`
 -/
 
-namespace Array
-
-theorem toVector_inj {a b : Array α} (h₁ : a.size = b.size) (h₂ : a.toVector.cast h₁ = b.toVector) : a = b := by
-  ext i ih₁ ih₂
-  · exact h₁
-  · simpa using congrArg (fun a => a[i]) h₂
-
-end Array
-
 namespace Vector
 
 @[simp] theorem getElem_mk {data : Array α} {size : data.size = n} {i : Nat} (h : i < n) :
@@ -248,11 +239,6 @@ theorem length_toList {α n} (xs : Vector α n) : xs.toList.length = n := by sim
 theorem getElem_toList {α n} (xs : Vector α n) (i : Nat) (h : i < xs.toList.length) :
     xs.toList[i] = xs[i]'(by simpa using h) := by simp
 
-theorem toList_inj {a b : Vector α n} (h : a.toList = b.toList) : a = b := by
-  rcases a with ⟨⟨a⟩, ha⟩
-  rcases b with ⟨⟨b⟩, hb⟩
-  simpa using h
-
 /-! ### Decidable quantifiers. -/
 
 theorem forall_zero_iff {P : Vector α 0 → Prop} :

src/Init/GetElem.lean

@@ -231,7 +231,7 @@ theorem getElem_cons_drop_succ_eq_drop {as : List α} {i : Nat} (h : i < as.leng
     as[i] :: as.drop (i+1) = as.drop i :=
   match as, i with
   | _::_, 0   => rfl
-  | _::_, i+1 => getElem_cons_drop_succ_eq_drop (i := i) (Nat.add_one_lt_add_one_iff.mp h)
+  | _::_, i+1 => getElem_cons_drop_succ_eq_drop (i := i) _
 
 @[deprecated getElem_cons_drop_succ_eq_drop (since := "2024-11-05")]
 abbrev get_drop_eq_drop := @getElem_cons_drop_succ_eq_drop

src/Init/System/IO.lean

@@ -981,14 +981,3 @@ not used concurrently or which are already persistent.
 -/
 @[extern "lean_runtime_mark_persistent"]
 unsafe def Runtime.markPersistent (a : α) : BaseIO α := return a
-
-set_option linter.unusedVariables false in
-/--
-Discards the passed owned reference. This leads to `a` any any object reachable from it never being
-freed. This can be a useful optimization for eliding deallocation time of big object graphs that are
-kept alive close to the end of the process anyway (in which case calling `Runtime.markPersistent`
-would be similarly costly to deallocation). It is still considered a safe operation as it cannot
-lead to undefined behavior.
--/
-@[extern "lean_runtime_forget"]
-def Runtime.forget (a : α) : BaseIO Unit := return

src/Lean/CoreM.lean

@@ -32,7 +32,7 @@ register_builtin_option maxHeartbeats : Nat := {
 }
 
 register_builtin_option Elab.async : Bool := {
-  defValue := true
+  defValue := false
   descr := "perform elaboration using multiple threads where possible"
 }
 
@@ -356,7 +356,9 @@ Returns the current log and then resets its messages while adjusting `MessageLog
 for incremental reporting during elaboration of a single command.
 -/
 def getAndEmptyMessageLog : CoreM MessageLog :=
-  modifyGet fun s => (s.messages, { s with messages := s.messages.markAllReported })
+  modifyGet fun s => (s.messages, { s with
+    messages.unreported := {}
+    messages.hadErrors  := s.messages.hasErrors })
 
 instance : MonadLog CoreM where
   getRef      := getRef
@@ -415,7 +417,7 @@ def wrapAsyncAsSnapshot (act : Unit → CoreM Unit) (desc : String := by exact d
     IO.FS.withIsolatedStreams (isolateStderr := stderrAsMessages.get (← getOptions)) do
       let tid ← IO.getTID
       -- reset trace state and message log so as not to report them twice
-      modify fun st => { st with messages := st.messages.markAllReported, traceState := { tid } }
+      modify ({ · with messages := {}, traceState := { tid } })
       try
         withTraceNode `Elab.async (fun _ => return desc) do
           act ()

src/Lean/Elab/BuiltinCommand.lean

@@ -488,9 +488,6 @@ where
     let mut lines : Array MessageData := #[]
     let decls ← getOptionDecls
     for (name, val) in opts do
-      -- `#guard_msgs` sets this option internally, we don't want it to end up in its output
-      if name == `Elab.async then
-        continue
       let (isSet, isUnknown) :=
         match decls.find? name with
         | some decl => (decl.defValue != val, false)

src/Lean/Elab/Command.lean

@@ -287,9 +287,7 @@ def runLinters (stx : Syntax) : CommandElabM Unit := do
               | Exception.internal _ _ =>
                 logException ex
             finally
-              -- TODO: it would be good to preserve even more state (#4363) but preserving info
-              -- trees currently breaks from linters adding context-less info nodes
-              modify fun s => { savedState with messages := s.messages, traceState := s.traceState }
+              modify fun s => { savedState with messages := s.messages }
 
 /--
 Catches and logs exceptions occurring in `x`. Unlike `try catch` in `CommandElabM`, this function
@@ -313,7 +311,7 @@ def wrapAsyncAsSnapshot (act : Unit → CommandElabM Unit)
     IO.FS.withIsolatedStreams (isolateStderr := Core.stderrAsMessages.get (← getOptions)) do
       let tid ← IO.getTID
       -- reset trace state and message log so as not to report them twice
-      modify fun st => { st with messages := st.messages.markAllReported, traceState := { tid } }
+      modify ({ · with messages := {}, traceState := { tid } })
       try
         withTraceNode `Elab.async (fun _ => return desc) do
           act ()
@@ -346,17 +344,6 @@ def wrapAsyncAsSnapshot (act : Unit → CommandElabM Unit)
 def logSnapshotTask (task : Language.SnapshotTask Language.SnapshotTree) : CommandElabM Unit :=
   modify fun s => { s with snapshotTasks := s.snapshotTasks.push task }
 
-def runLintersAsync (stx : Syntax) : CommandElabM Unit := do
-  if !Elab.async.get (← getOptions) then
-    withoutModifyingEnv do
-      runLinters stx
-    return
-
-  -- We only start one task for all linters for now as most linters are fast and we simply want
-  -- to unblock elaboration of the next command
-  let lintAct ← wrapAsyncAsSnapshot fun _ => runLinters stx
-  logSnapshotTask { range? := none, task := (← BaseIO.asTask lintAct) }
-
 protected def getCurrMacroScope : CommandElabM Nat  := do pure (← read).currMacroScope
 protected def getMainModule     : CommandElabM Name := do pure (← getEnv).mainModule
 
@@ -560,7 +547,7 @@ def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do pro
     -- rather than engineer a general solution.
     unless (stx.find? (·.isOfKind ``Lean.guardMsgsCmd)).isSome do
       withLogging do
-        runLintersAsync stx
+        runLinters stx
   finally
     -- note the order: first process current messages & info trees, then add back old messages & trees,
     -- then convert new traces to messages

src/Lean/Elab/Frontend.lean

@@ -169,8 +169,6 @@ def runFrontend
     IO.FS.writeFile ⟨out⟩ <| Json.compress <| toJson profile
 
   let hasErrors := snaps.getAll.any (·.diagnostics.msgLog.hasErrors)
-  -- no point in freeing the snapshot graph and all referenced data this close to process exit
-  Runtime.forget snaps
   pure (cmdState.env, !hasErrors)
 
 

src/Lean/Elab/GuardMsgs.lean

@@ -140,12 +140,8 @@ def MessageOrdering.apply (mode : MessageOrdering) (msgs : List String) : List S
         |>.trim |> removeTrailingWhitespaceMarker
     let (whitespace, ordering, specFn) ← parseGuardMsgsSpec spec?
     let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
-    -- disable async elaboration for `cmd` so `msgs` will contain all messages
-    let async := Elab.async.get (← getOptions)
-    modifyScope fun scope => { scope with opts := Elab.async.set scope.opts false }
     -- The `#guard_msgs` command is special-cased in `elabCommandTopLevel` to ensure linters only run once.
     elabCommandTopLevel cmd
-    modifyScope fun scope => { scope with opts := Elab.async.set scope.opts async }
     let msgs := (← get).messages
     let mut toCheck : MessageLog := .empty
     let mut toPassthrough : MessageLog := .empty

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean

@@ -8,7 +8,6 @@ import Std.Data.HashMap
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
 import Lean.Meta.AppBuilder
 import Lean.ToExpr
-import Lean.Data.RArray
 
 /-!
 This module contains the implementation of the reflection monad, used by all other components of this
@@ -139,11 +138,9 @@ structure State where
   -/
   atoms : Std.HashMap Expr Atom := {}
   /--
-  A cache for `atomsAssignment`. We maintain the invariant that this value is only used if
-  `atoms` is non empty. The reason for not using an `Option` is that it would pollute a lot of code
-  with error handling that is never hit as this invariant is enforced before all of this code.
+  A cache for `atomsAssignment`.
   -/
-  atomsAssignmentCache : Expr := mkConst `illegal
+  atomsAssignmentCache : Expr := mkConst ``List.nil [.zero]
 
 /--
 The reflection monad, used to track `BitVec` variables that we see as we traverse the context.
@@ -160,9 +157,9 @@ structure ReifiedBVExpr where
   -/
   bvExpr : BVExpr width
   /--
-  A proof that `bvExpr.eval atomsAssignment = originalBVExpr`, none if it holds by `rfl`.
+  A proof that `bvExpr.eval atomsAssignment = originalBVExpr`.
   -/
-  evalsAtAtoms : M (Option Expr)
+  evalsAtAtoms : M Expr
   /--
   A cache for `toExpr bvExpr`.
   -/
@@ -177,9 +174,9 @@ structure ReifiedBVPred where
   -/
   bvPred : BVPred
   /--
-  A proof that `bvPred.eval atomsAssignment = originalBVPredExpr`, none if it holds by `rfl`.
+  A proof that `bvPred.eval atomsAssignment = originalBVPredExpr`.
   -/
-  evalsAtAtoms : M (Option Expr)
+  evalsAtAtoms : M Expr
   /--
   A cache for `toExpr bvPred`
   -/
@@ -194,9 +191,9 @@ structure ReifiedBVLogical where
   -/
   bvExpr : BVLogicalExpr
   /--
-  A proof that `bvExpr.eval atomsAssignment = originalBVLogicalExpr`, none if it holds by `rfl`.
+  A proof that `bvExpr.eval atomsAssignment = originalBVLogicalExpr`.
   -/
-  evalsAtAtoms : M (Option Expr)
+  evalsAtAtoms : M Expr
   /--
   A cache for `toExpr bvExpr`
   -/
@@ -231,9 +228,9 @@ def run (m : M α) : MetaM α :=
 /--
 Retrieve the atoms as pairs of their width and expression.
 -/
-def atoms : M (Array (Nat × Expr)) := do
+def atoms : M (List (Nat × Expr)) := do
   let sortedAtoms := (← getThe State).atoms.toArray.qsort (·.2.atomNumber < ·.2.atomNumber)
-  return sortedAtoms.map (fun (expr, {width, ..}) => (width, expr))
+  return sortedAtoms.map (fun (expr, {width, ..}) => (width, expr)) |>.toList
 
 /--
 Retrieve a `BitVec.Assignment` representing the atoms we found so far.
@@ -260,37 +257,11 @@ def lookup (e : Expr) (width : Nat) (synthetic : Bool) : M Nat := do
 where
   updateAtomsAssignment : M Unit := do
     let as ← atoms
-    if h : 0 < as.size then
-      let ras := Lean.RArray.ofArray as h
-      let packedType := mkConst ``BVExpr.PackedBitVec
-      let pack := fun (width, expr) => mkApp2 (mkConst ``BVExpr.PackedBitVec.mk) (toExpr width) expr
-      let newAtomsAssignment := ras.toExpr packedType pack
-      modify fun s => { s with atomsAssignmentCache := newAtomsAssignment }
-    else
-      throwError "updateAtomsAssignment should only be called when there is an atom"
-
-@[specialize]
-def simplifyBinaryProof' (mkFRefl : Expr → Expr) (fst : Expr) (fproof : Option Expr)
-    (mkSRefl : Expr → Expr) (snd : Expr) (sproof : Option Expr) : Option (Expr × Expr) := do
-  match fproof, sproof with
-  | some fproof, some sproof => some (fproof, sproof)
-  | some fproof, none => some (fproof, mkSRefl snd)
-  | none, some sproof => some (mkFRefl fst, sproof)
-  | none, none => none
-
-@[specialize]
-def simplifyBinaryProof (mkRefl : Expr → Expr) (fst : Expr) (fproof : Option Expr) (snd : Expr)
-    (sproof : Option Expr) : Option (Expr × Expr) := do
-  simplifyBinaryProof' mkRefl fst fproof mkRefl snd sproof
-
-@[specialize]
-def simplifyTernaryProof (mkRefl : Expr → Expr) (fst : Expr) (fproof : Option Expr) (snd : Expr)
-    (sproof : Option Expr) (thd : Expr) (tproof : Option Expr) : Option (Expr × Expr × Expr) := do
-  match fproof, simplifyBinaryProof mkRefl snd sproof thd tproof with
-  | some fproof, some stproof => some (fproof, stproof)
-  | some fproof, none => some (fproof, mkRefl snd, mkRefl thd)
-  | none, some stproof => some (mkRefl fst, stproof)
-  | none, none => none
+    let packed :=
+      as.map (fun (width, expr) => mkApp2 (mkConst ``BVExpr.PackedBitVec.mk) (toExpr width) expr)
+    let packedType := mkConst ``BVExpr.PackedBitVec
+    let newAtomsAssignment ← mkListLit packedType packed
+    modify fun s => { s with atomsAssignmentCache := newAtomsAssignment }
 
 end M
 

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean

@@ -37,8 +37,9 @@ Register `e` as an atom of `width` that might potentially be `synthetic`.
 def mkAtom (e : Expr) (width : Nat) (synthetic : Bool) : M ReifiedBVExpr := do
   let ident ← M.lookup e width synthetic
   let expr := mkApp2 (mkConst ``BVExpr.var) (toExpr width) (toExpr ident)
-  -- This is safe because this proof always holds definitionally.
-  let proof := pure none
+  let proof := do
+    let evalExpr ← mkEvalExpr width expr
+    return mkBVRefl width evalExpr
   return ⟨width, .var ident, proof, expr⟩
 
 /--
@@ -69,8 +70,9 @@ Build a reified version of the constant `val`.
 def mkBVConst (val : BitVec w) : M ReifiedBVExpr := do
   let bvExpr : BVExpr w := .const val
   let expr := mkApp2 (mkConst ``BVExpr.const) (toExpr w) (toExpr val)
-  -- This is safe because this proof always holds definitionally.
-  let proof := pure none
+  let proof := do
+    let evalExpr ← ReifiedBVExpr.mkEvalExpr w expr
+    return ReifiedBVExpr.mkBVRefl w evalExpr
   return ⟨w, bvExpr, proof, expr⟩
 
 end ReifiedBVExpr

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean

@@ -49,8 +49,7 @@ Build a reified version of the constant `val`.
 def mkBoolConst (val : Bool) : M ReifiedBVLogical := do
   let boolExpr := .const val
   let expr := mkApp2 (mkConst ``BoolExpr.const) (mkConst ``BVPred) (toExpr val)
-  -- This is safe because this proof always holds definitionally.
-  let proof := pure none
+  let proof := pure <| ReifiedBVLogical.mkRefl (toExpr val)
   return ⟨boolExpr, proof, expr⟩
 
 /--
@@ -72,13 +71,8 @@ def mkGate (lhs rhs : ReifiedBVLogical) (lhsExpr rhsExpr : Expr) (gate : Gate) :
   let proof := do
     let lhsEvalExpr ← ReifiedBVLogical.mkEvalExpr lhs.expr
     let rhsEvalExpr ← ReifiedBVLogical.mkEvalExpr rhs.expr
-    let lhsProof? ← lhs.evalsAtAtoms
-    let rhsProof? ← rhs.evalsAtAtoms
-    let some (lhsProof, rhsProof) :=
-      M.simplifyBinaryProof
-        ReifiedBVLogical.mkRefl
-        lhsEvalExpr lhsProof?
-        rhsEvalExpr rhsProof? | return none
+    let lhsProof ← lhs.evalsAtAtoms
+    let rhsProof ← rhs.evalsAtAtoms
     return mkApp6
       (mkConst congrThm)
       lhsExpr rhsExpr
@@ -101,9 +95,8 @@ def mkNot (sub : ReifiedBVLogical) (subExpr : Expr) : M ReifiedBVLogical := do
   let boolExpr := .not sub.bvExpr
   let expr := mkApp2 (mkConst ``BoolExpr.not) (mkConst ``BVPred) sub.expr
   let proof := do
-    -- This is safe as `not_congr` holds definitionally if the arguments are defeq.
-    let some subProof ← sub.evalsAtAtoms | return none
     let subEvalExpr ← ReifiedBVLogical.mkEvalExpr sub.expr
+    let subProof ← sub.evalsAtAtoms
     return mkApp3 (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.not_congr) subExpr subEvalExpr subProof
   return ⟨boolExpr, proof, expr⟩
 
@@ -126,15 +119,9 @@ def mkIte (discr lhs rhs : ReifiedBVLogical) (discrExpr lhsExpr rhsExpr : Expr)
     let discrEvalExpr ← ReifiedBVLogical.mkEvalExpr discr.expr
     let lhsEvalExpr ← ReifiedBVLogical.mkEvalExpr lhs.expr
     let rhsEvalExpr ← ReifiedBVLogical.mkEvalExpr rhs.expr
-    let discrProof? ← discr.evalsAtAtoms
-    let lhsProof? ← lhs.evalsAtAtoms
-    let rhsProof? ← rhs.evalsAtAtoms
-    let some (discrProof, lhsProof, rhsProof) :=
-      M.simplifyTernaryProof
-        ReifiedBVLogical.mkRefl
-        discrEvalExpr discrProof?
-        lhsEvalExpr lhsProof?
-        rhsEvalExpr rhsProof? | return none
+    let discrProof ← discr.evalsAtAtoms
+    let lhsProof ← lhs.evalsAtAtoms
+    let rhsProof ← rhs.evalsAtAtoms
     return mkApp9
       (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.ite_congr)
       discrExpr lhsExpr rhsExpr

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean

@@ -35,10 +35,8 @@ def boolAtom (t : Expr) : M (Option ReifiedBVPred) := do
   let bvExpr : BVPred := .getLsbD atom.bvExpr 0
   let expr := mkApp3 (mkConst ``BVPred.getLsbD) (toExpr 1) atom.expr (toExpr 0)
   let proof := do
-    -- ofBool_congr does not hold definitionally, if this ever becomes an issue we need to find
-    -- a more clever encoding for boolean atoms
     let atomEval ← ReifiedBVExpr.mkEvalExpr atom.width atom.expr
-    let atomProof := (← atom.evalsAtAtoms).getD (ReifiedBVExpr.mkBVRefl atom.width atomEval)
+    let atomProof ← atom.evalsAtAtoms
     return mkApp3
       (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.ofBool_congr)
       t
@@ -65,14 +63,9 @@ def mkBinPred (lhs rhs : ReifiedBVExpr) (lhsExpr rhsExpr : Expr) (pred : BVBinPr
         rhs.expr
     let proof := do
       let lhsEval ← ReifiedBVExpr.mkEvalExpr lhs.width lhs.expr
+      let lhsProof ← lhs.evalsAtAtoms
       let rhsEval ← ReifiedBVExpr.mkEvalExpr rhs.width rhs.expr
-      let lhsProof? ← lhs.evalsAtAtoms
-      let rhsProof? ← rhs.evalsAtAtoms
-      let some (lhsProof, rhsProof) :=
-        M.simplifyBinaryProof
-          (ReifiedBVExpr.mkBVRefl lhs.width)
-          lhsEval lhsProof?
-          rhsEval rhsProof? | return none
+      let rhsProof ← rhs.evalsAtAtoms
       return mkApp7
         (mkConst congrThm)
         (toExpr lhs.width)
@@ -97,9 +90,8 @@ def mkGetLsbD (sub : ReifiedBVExpr) (subExpr : Expr) (idx : Nat) : M ReifiedBVPr
   let idxExpr := toExpr idx
   let expr := mkApp3 (mkConst ``BVPred.getLsbD) (toExpr sub.width) sub.expr idxExpr
   let proof := do
-    -- This is safe as `getLsbD_congr` holds definitionally if the arguments are defeq.
-    let some subProof ← sub.evalsAtAtoms | return none
     let subEval ← ReifiedBVExpr.mkEvalExpr sub.width sub.expr
+    let subProof ← sub.evalsAtAtoms
     return mkApp5
       (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.getLsbD_congr)
       idxExpr

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedLemmas.lean

@@ -62,7 +62,7 @@ where
 
     let proof := do
       let evalExpr ← ReifiedBVLogical.mkEvalExpr imp.expr
-      let congrProof := (← imp.evalsAtAtoms).getD (ReifiedBVLogical.mkRefl evalExpr)
+      let congrProof ← imp.evalsAtAtoms
       let lemmaProof := mkApp4 (mkConst lemmaName) (toExpr lhs.width) discrExpr lhsExpr rhsExpr
 
       let trueExpr := mkConst ``Bool.true

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean

@@ -112,8 +112,7 @@ where
           inner.expr
       let proof := do
         let innerEval ← ReifiedBVExpr.mkEvalExpr inner.width inner.expr
-        -- This is safe as `zeroExtend_congr` holds definitionally if the arguments are defeq.
-        let some innerProof ← inner.evalsAtAtoms | return none
+        let innerProof ← inner.evalsAtAtoms
         return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.zeroExtend_congr)
           newWidthExpr
           (toExpr inner.width)
@@ -133,8 +132,7 @@ where
           inner.expr
       let proof := do
         let innerEval ← ReifiedBVExpr.mkEvalExpr inner.width inner.expr
-        -- This is safe as `zeroExtend_congr` holds definitionally if the arguments are defeq.
-        let some innerProof ← inner.evalsAtAtoms | return none
+        let innerProof ← inner.evalsAtAtoms
         return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.signExtend_congr)
           newWidthExpr
           (toExpr inner.width)
@@ -152,13 +150,9 @@ where
         lhs.expr rhs.expr
       let proof := do
         let lhsEval ← ReifiedBVExpr.mkEvalExpr lhs.width lhs.expr
+        let lhsProof ← lhs.evalsAtAtoms
+        let rhsProof ← rhs.evalsAtAtoms
         let rhsEval ← ReifiedBVExpr.mkEvalExpr rhs.width rhs.expr
-        let lhsProof? ← lhs.evalsAtAtoms
-        let rhsProof? ← rhs.evalsAtAtoms
-        let some (lhsProof, rhsProof) :=
-          M.simplifyBinaryProof'
-            (ReifiedBVExpr.mkBVRefl lhs.width) lhsEval lhsProof?
-            (ReifiedBVExpr.mkBVRefl rhs.width) rhsEval rhsProof? | return none
         return mkApp8 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.append_congr)
           (toExpr lhs.width) (toExpr rhs.width)
           lhsExpr lhsEval
@@ -175,8 +169,7 @@ where
         inner.expr
       let proof := do
         let innerEval ← ReifiedBVExpr.mkEvalExpr inner.width inner.expr
-        -- This is safe as `zeroExtend_congr` holds definitionally if the arguments are defeq.
-        let some innerProof ← inner.evalsAtAtoms | return none
+        let innerProof ← inner.evalsAtAtoms
         return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.replicate_congr)
           (toExpr n)
           (toExpr inner.width)
@@ -196,8 +189,7 @@ where
         inner.expr
       let proof := do
         let innerEval ← ReifiedBVExpr.mkEvalExpr inner.width inner.expr
-        -- This is safe as `zeroExtend_congr` holds definitionally if the arguments are defeq.
-        let some innerProof ← inner.evalsAtAtoms | return none
+        let innerProof ← inner.evalsAtAtoms
         return mkApp6 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.extract_congr)
           startExpr
           lenExpr
@@ -309,16 +301,11 @@ where
       return none
 
   binaryCongrProof (lhs rhs : ReifiedBVExpr) (lhsExpr rhsExpr : Expr) (congrThm : Expr) :
-      M (Option Expr) := do
+      M Expr := do
     let lhsEval ← ReifiedBVExpr.mkEvalExpr lhs.width lhs.expr
+    let lhsProof ← lhs.evalsAtAtoms
+    let rhsProof ← rhs.evalsAtAtoms
     let rhsEval ← ReifiedBVExpr.mkEvalExpr rhs.width rhs.expr
-    let lhsProof? ← lhs.evalsAtAtoms
-    let rhsProof? ← rhs.evalsAtAtoms
-    let some (lhsProof, rhsProof) :=
-      M.simplifyBinaryProof
-        (ReifiedBVExpr.mkBVRefl lhs.width)
-        lhsEval lhsProof?
-        rhsEval rhsProof? | return none
     return mkApp6 congrThm lhsExpr rhsExpr lhsEval rhsEval lhsProof rhsProof
 
   unaryReflection (innerExpr : Expr) (op : BVUnOp) (congrThm : Name) :
@@ -329,9 +316,9 @@ where
     let proof := unaryCongrProof inner innerExpr (mkConst congrThm)
     return some ⟨inner.width, bvExpr, proof, expr⟩
 
-  unaryCongrProof (inner : ReifiedBVExpr) (innerExpr : Expr) (congrProof : Expr) : M (Option Expr) := do
+  unaryCongrProof (inner : ReifiedBVExpr) (innerExpr : Expr) (congrProof : Expr) : M Expr := do
     let innerEval ← ReifiedBVExpr.mkEvalExpr inner.width inner.expr
-    let some innerProof ← inner.evalsAtAtoms | return none
+    let innerProof ← inner.evalsAtAtoms
     return mkApp4 congrProof (toExpr inner.width) innerExpr innerEval innerProof
 
   goBvLit (x : Expr) : M (Option ReifiedBVExpr) := do

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/SatAtBVLogical.lean

@@ -37,7 +37,7 @@ partial def of (h : Expr) : LemmaM (Option SatAtBVLogical) := do
     let proof := do
       let evalLogic ← ReifiedBVLogical.mkEvalExpr bvLogical.expr
       -- this is evalLogic = lhsExpr
-      let evalProof := (← bvLogical.evalsAtAtoms).getD (ReifiedBVLogical.mkRefl evalLogic)
+      let evalProof ← bvLogical.evalsAtAtoms
       -- h is lhsExpr = true
       -- we prove evalLogic = true by evalLogic = lhsExpr = true
       return ReifiedBVLogical.mkTrans evalLogic lhsExpr (mkConst ``Bool.true) evalProof h
@@ -61,16 +61,13 @@ def and (x y : SatAtBVLogical) : SatAtBVLogical where
 
 /-- Given a proof that `x.expr.Unsat`, produce a proof of `False`. -/
 def proveFalse (x : SatAtBVLogical) (h : Expr) : M Expr := do
-  if (← get).atoms.isEmpty then
-    throwError "Unable to identify any relevant atoms."
-  else
-    let atomsList ← M.atomsAssignment
-    let evalExpr := mkApp2 (mkConst ``BVLogicalExpr.eval) atomsList x.expr
-    return mkApp3
-      (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.false_of_eq_true_of_eq_false)
-      evalExpr
-      (← x.satAtAtoms)
-      (.app h atomsList)
+  let atomsList ← M.atomsAssignment
+  let evalExpr := mkApp2 (mkConst ``BVLogicalExpr.eval) atomsList x.expr
+  return mkApp3
+    (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.false_of_eq_true_of_eq_false)
+    evalExpr
+    (← x.satAtAtoms)
+    (.app h atomsList)
 
 
 end SatAtBVLogical

src/Lean/Elab/Tactic/Omega/Frontend.lean

@@ -228,7 +228,6 @@ partial def asLinearComboImpl (e : Expr) : OmegaM (LinearCombo × OmegaM Expr ×
     | .app (.app (.app (.app (.const ``Prod.mk [u, v]) _) _) x) y =>
       rewrite e (mkApp4 (.const ``Prod.snd_mk [u, v]) α x β y)
     | _ => mkAtomLinearCombo e
-  | (``Int.negSucc, #[n]) => rewrite e (mkApp (.const ``Int.negSucc_eq []) n)
   | _ => mkAtomLinearCombo e
 where
   /--

src/Lean/Linter/Deprecated.lean

@@ -51,8 +51,8 @@ def checkDeprecated [Monad m] [MonadEnv m] [MonadLog m] [AddMessageContext m] [M
   if getLinterValue linter.deprecated (← getOptions) then
     let some attr := deprecatedAttr.getParam? (← getEnv) declName | pure ()
     logWarning <| .tagged ``deprecatedAttr <|
-      m!"`{.ofConstName declName true}` has been deprecated" ++ match attr.text? with
+      s!"`{declName}` has been deprecated" ++ match attr.text? with
       | some text => s!": {text}"
       | none => match attr.newName? with
-        | some newName => m!": use `{.ofConstName newName true}` instead"
+        | some newName => s!": use `{newName}` instead"
         | none => ""

src/Lean/Message.lean

@@ -441,10 +441,6 @@ instance : Append MessageLog :=
 def hasErrors (log : MessageLog) : Bool :=
   log.hadErrors || log.unreported.any (·.severity matches .error)
 
-/-- Clears unreported messages while preserving `hasErrors`. -/
-def markAllReported (log : MessageLog) : MessageLog :=
-  { log with unreported := {}, hadErrors  := log.hasErrors }
-
 def errorsToWarnings (log : MessageLog) : MessageLog :=
   { unreported := log.unreported.map (fun m => match m.severity with | MessageSeverity.error => { m with severity := MessageSeverity.warning } | _ => m) }
 

src/Lean/Meta/CtorRecognizer.lean

@@ -35,27 +35,11 @@ def isConstructorApp? (e : Expr) : MetaM (Option ConstructorVal) := do
 
 /--
 Similar to `isConstructorApp?`, but uses `whnf`.
-It also uses `isOffset?` for `Nat`.
-
-See also `Lean.Meta.constructorApp'?`.
 -/
 def isConstructorApp'? (e : Expr) : MetaM (Option ConstructorVal) := do
-  if let some (_, k) ← isOffset? e then
-    if k = 0 then
-      return none
-    else
-      let .ctorInfo val ← getConstInfo ``Nat.succ | return none
-      return some val
-  else if let some r ← isConstructorApp? e then
+  if let some r ← isConstructorApp? e then
     return r
-  else try
-    /-
-    We added the `try` block here because `whnf` fails at terms `n ^ m`
-    when `m` is a big numeral, and `n` is a numeral. This is a little bit hackish.
-    -/
-    isConstructorApp? (← whnf e)
-  catch _ =>
-    return none
+  isConstructorApp? (← whnf e)
 
 /--
 Returns `true`, if `e` is constructor application of builtin literal defeq to
@@ -86,9 +70,7 @@ def constructorApp? (e : Expr) : MetaM (Option (ConstructorVal × Array Expr)) :
 
 /--
 Similar to `constructorApp?`, but on failure it puts `e` in WHNF and tries again.
-It also uses `isOffset?` for `Nat`.
-
-See also `Lean.Meta.isConstructorApp'?`.
+It also `isOffset?`
 -/
 def constructorApp'? (e : Expr) : MetaM (Option (ConstructorVal × Array Expr)) := do
   if let some (e, k) ← isOffset? e then

src/Lean/Server/Completion/SyntheticCompletion.lean

@@ -100,6 +100,20 @@ private def findSyntheticIdentifierCompletion?
       HoverInfo.after
   some { hoverInfo, ctx, info := .id stx id danglingDot info.lctx none }
 
+private partial def getIndentationAmount (fileMap : FileMap) (line : Nat) : Nat := Id.run do
+  let lineStartPos := fileMap.lineStart line
+  let lineEndPos := fileMap.lineStart (line + 1)
+  let mut it : String.Iterator := ⟨fileMap.source, lineStartPos⟩
+  let mut indentationAmount := 0
+  while it.pos < lineEndPos do
+    let c := it.curr
+    if c = ' ' || c = '\t' then
+      indentationAmount := indentationAmount + 1
+    else
+      break
+    it := it.next
+  return indentationAmount
+
 private partial def isCursorOnWhitespace (fileMap : FileMap) (hoverPos : String.Pos) : Bool :=
   fileMap.source.atEnd hoverPos || (fileMap.source.get hoverPos).isWhitespace
 
@@ -113,10 +127,15 @@ private partial def isSyntheticTacticCompletion
     (cmdStx   : Syntax)
     : Bool := Id.run do
   let hoverFilePos := fileMap.toPosition hoverPos
-  go hoverFilePos cmdStx 0
+  let mut hoverLineIndentation := getIndentationAmount fileMap hoverFilePos.line
+  if hoverFilePos.column < hoverLineIndentation then
+    -- Ignore trailing whitespace after the cursor
+    hoverLineIndentation := hoverFilePos.column
+  go hoverFilePos hoverLineIndentation cmdStx 0
 where
   go
       (hoverFilePos : Position)
+      (hoverLineIndentation : Nat)
       (stx : Syntax)
       (leadingWs : Nat)
       : Bool := Id.run do
@@ -129,7 +148,7 @@ where
         return false
       let mut wsBeforeArg := leadingWs
       for arg in stx.getArgs do
-        if go hoverFilePos arg wsBeforeArg then
+        if go hoverFilePos hoverLineIndentation arg wsBeforeArg then
           return true
         -- We must account for the whitespace before an argument because the syntax nodes we use
         -- to identify tactic blocks only start *after* the whitespace following a `by`, and we
@@ -139,7 +158,7 @@ where
         wsBeforeArg := arg.getTrailingSize
       return isCompletionInEmptyTacticBlock stx
         || isCompletionAfterSemicolon stx
-        || isCompletionOnTacticBlockIndentation hoverFilePos stx
+        || isCompletionOnTacticBlockIndentation hoverFilePos hoverLineIndentation stx
     | _, _ =>
       -- Empty tactic blocks typically lack ranges since they do not contain any tokens.
       -- We do not perform more precise range checking in this case because we assume that empty
@@ -150,17 +169,24 @@ where
 
   isCompletionOnTacticBlockIndentation
       (hoverFilePos : Position)
+      (hoverLineIndentation : Nat)
       (stx : Syntax)
       : Bool := Id.run do
+    let isCursorInIndentation := hoverFilePos.column <= hoverLineIndentation
+    if ! isCursorInIndentation then
+      -- Do not trigger tactic completion at the end of a properly indented tactic block line since
+      -- that line might already have entered term mode by that point.
+      return false
     let some tacticsNode := getTacticsNode? stx
       | return false
     let some firstTacticPos := tacticsNode.getPos?
       | return false
-    let firstTacticColumn := fileMap.toPosition firstTacticPos |>.column
+    let firstTacticLine := fileMap.toPosition firstTacticPos |>.line
+    let firstTacticIndentation := getIndentationAmount fileMap firstTacticLine
     -- This ensures that we do not accidentally provide tactic completions in a term mode proof -
     -- tactic completions are only provided at the same indentation level as the other tactics in
     -- that tactic block.
-    let isCursorInTacticBlock := hoverFilePos.column == firstTacticColumn
+    let isCursorInTacticBlock := hoverLineIndentation == firstTacticIndentation
     return isCursorInProperWhitespace fileMap hoverPos && isCursorInTacticBlock
 
   isCompletionAfterSemicolon (stx : Syntax) : Bool := Id.run do
@@ -289,6 +315,10 @@ private def isSyntheticStructFieldCompletion
     return false
 
   let hoverFilePos := fileMap.toPosition hoverPos
+  let mut hoverLineIndentation := getIndentationAmount fileMap hoverFilePos.line
+  if hoverFilePos.column < hoverLineIndentation then
+    -- Ignore trailing whitespace after the cursor
+    hoverLineIndentation := hoverFilePos.column
 
   return Option.isSome <| findWithLeadingToken? (stx := cmdStx) fun leadingToken? stx => Id.run do
     let some leadingToken := leadingToken?
@@ -325,10 +355,14 @@ private def isSyntheticStructFieldCompletion
     let isCompletionOnIndentation := Id.run do
       if ! isCursorInProperWhitespace then
         return false
+      let isCursorInIndentation := hoverFilePos.column <= hoverLineIndentation
+      if ! isCursorInIndentation then
+        return false
       let some firstFieldPos := stx.getPos?
         | return false
-      let firstFieldColumn := fileMap.toPosition firstFieldPos |>.column
-      let isCursorInBlock := hoverFilePos.column == firstFieldColumn
+      let firstFieldLine := fileMap.toPosition firstFieldPos |>.line
+      let firstFieldIndentation := getIndentationAmount fileMap firstFieldLine
+      let isCursorInBlock := hoverLineIndentation == firstFieldIndentation
       return isCursorInBlock
     return isCompletionOnIndentation
 

src/Std/Data/DHashMap/Internal/Index.lean

@@ -46,11 +46,19 @@ cf. https://github.com/leanprover/lean4/issues/4157
 @[irreducible, inline] def mkIdx (sz : Nat) (h : 0 < sz) (hash : UInt64) :
     { u : USize // u.toNat < sz } :=
   ⟨(scrambleHash hash).toUSize &&& (sz.toUSize - 1), by
-    -- This proof is a good test for our USize API
+    -- Making this proof significantly less painful will be a good test for our USize API
     by_cases h' : sz < USize.size
-    · rw [USize.toNat_and, USize.toNat_sub_of_le, USize.toNat_ofNat_of_lt h']
-      · exact Nat.lt_of_le_of_lt Nat.and_le_right (Nat.sub_lt h (by simp))
-      · simp [USize.le_iff_toNat_le, Nat.mod_eq_of_lt h', Nat.succ_le_of_lt h]
+    · rw [USize.and_toNat, ← USize.ofNat_one, USize.toNat_sub_of_le, USize.toNat_ofNat_of_lt]
+      · refine Nat.lt_of_le_of_lt Nat.and_le_right (Nat.sub_lt h ?_)
+        rw [USize.toNat_ofNat_of_lt]
+        · exact Nat.one_pos
+        · exact Nat.lt_of_le_of_lt h h'
+      · exact h'
+      · rw [USize.le_def, BitVec.le_def]
+        change _ ≤ (_ % _)
+        rw [Nat.mod_eq_of_lt h', USize.ofNat, BitVec.toNat_ofNat, Nat.mod_eq_of_lt]
+        · exact h
+        · exact Nat.lt_of_le_of_lt h h'
     · exact Nat.lt_of_lt_of_le (USize.toNat_lt_size _) (Nat.le_of_not_lt h')⟩
 
 end Std.DHashMap.Internal

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean

@@ -6,7 +6,6 @@ Authors: Henrik Böving
 prelude
 import Init.Data.Hashable
 import Init.Data.BitVec
-import Init.Data.RArray
 import Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
 
 /-!
@@ -280,20 +279,20 @@ structure PackedBitVec where
 /--
 The notion of variable assignments for `BVExpr`.
 -/
-abbrev Assignment := Lean.RArray PackedBitVec
+abbrev Assignment := List PackedBitVec
 
 /--
 Get the value of a `BVExpr.var` from an `Assignment`.
 -/
-def Assignment.get (assign : Assignment) (idx : Nat) : PackedBitVec :=
-  Lean.RArray.get assign idx
+def Assignment.getD (assign : Assignment) (idx : Nat) : PackedBitVec :=
+  List.getD assign idx ⟨BitVec.zero 0⟩
 
 /--
 The semantics for `BVExpr`.
 -/
 def eval (assign : Assignment) : BVExpr w → BitVec w
   | .var idx =>
-    let ⟨bv⟩ := assign.get idx
+    let ⟨bv⟩ := assign.getD idx
     bv.truncate w
   | .const val => val
   | .zeroExtend v expr => BitVec.zeroExtend v (eval assign expr)
@@ -308,7 +307,7 @@ def eval (assign : Assignment) : BVExpr w → BitVec w
   | .arithShiftRight lhs rhs => BitVec.sshiftRight' (eval assign lhs) (eval assign rhs)
 
 @[simp]
-theorem eval_var : eval assign ((.var idx) : BVExpr w) = (assign.get idx).bv.truncate _ := by
+theorem eval_var : eval assign ((.var idx) : BVExpr w) = (assign.getD idx).bv.truncate _ := by
   rfl
 
 @[simp]

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Basic.lean

@@ -18,11 +18,11 @@ namespace Std.Tactic.BVDecide
 namespace BVExpr
 
 def Assignment.toAIGAssignment (assign : Assignment) : BVBit → Bool :=
-  fun bit => (assign.get bit.var).bv.getLsbD bit.idx
+  fun bit => (assign.getD bit.var).bv.getLsbD bit.idx
 
 @[simp]
 theorem Assignment.toAIGAssignment_apply (assign : Assignment) (bit : BVBit) :
-    assign.toAIGAssignment bit = (assign.get bit.var).bv.getLsbD bit.idx := by
+    assign.toAIGAssignment bit = (assign.getD bit.var).bv.getLsbD bit.idx := by
   rfl
 
 end BVExpr

src/Std/Time/DateTime/Timestamp.lean

@@ -6,7 +6,6 @@ Authors: Sofia Rodrigues
 prelude
 import Std.Time.Internal
 import Init.Data.Int
-import Init.System.IO
 import Std.Time.Time
 import Std.Time.Date
 import Std.Time.Duration

src/Std/Time/Internal/UnitVal.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sofia Rodrigues
 -/
 prelude
+import Init.Data
 import Std.Internal.Rat
 
 namespace Std

src/Std/Time/Zoned/Database/Windows.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sofia Rodrigues
 -/
 prelude
-import Init.Data.SInt.Basic
 import Std.Time.DateTime
 import Std.Time.Zoned.TimeZone
 import Std.Time.Zoned.ZoneRules

src/lake/Lake.lean

@@ -3,7 +3,6 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-prelude
 import Lake.Build
 import Lake.Config
 import Lake.DSL

src/lake/Lake/Build.lean

@@ -3,7 +3,6 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-prelude
 import Lake.Build.Run
 import Lake.Build.Module
 import Lake.Build.Package

src/lake/Lake/Build/Actions.lean

@@ -3,7 +3,6 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone, Siddharth Bhat
 -/
-prelude
 import Lake.Util.Proc
 import Lake.Util.NativeLib
 import Lake.Util.IO
@@ -106,16 +105,6 @@ def compileExe
   proc {
     cmd := linker.toString
     args := #["-o", binFile.toString] ++ linkFiles.map toString ++ linkArgs
-    env := ← do
-      -- It is difficult to identify the correct minor version here, leading to linking warnings like:
-      -- `ld64.lld: warning: /usr/lib/system/libsystem_kernel.dylib has version 13.5.0, which is newer than target minimum of 13.0.0`
-      -- In order to suppress these we set the MACOSX_DEPLOYMENT_TARGET variable into the far future.
-      if System.Platform.isOSX then
-        match (← IO.getEnv "MACOSX_DEPLOYMENT_TARGET") with
-        | some _ => pure #[]
-        | none => pure #[("MACOSX_DEPLOYMENT_TARGET", some "99.0")]
-      else
-        pure #[]
   }
 
 /-- Download a file using `curl`, clobbering any existing file. -/

src/lake/Lake/Build/Basic.lean

@@ -3,7 +3,6 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-prelude
 import Lake.Util.Log
 import Lake.Util.Exit
 import Lake.Util.Lift

src/lake/Lake/Build/Common.lean

@@ -3,7 +3,6 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-prelude
 import Lake.Config.Monad
 import Lake.Build.Actions
 import Lake.Util.JsonObject
@@ -307,8 +306,7 @@ which will be computed in the resulting `BuildJob` before building.
   let extraDepTrace :=
     return (← getLeanTrace).mix <| (pureHash traceArgs).mix platformTrace
   buildFileAfterDep oFile srcJob (extraDepTrace := extraDepTrace) fun srcFile => do
-    let lean ← getLeanInstall
-    compileO oFile srcFile (lean.ccFlags ++ weakArgs ++ traceArgs) lean.cc
+     compileO oFile srcFile (weakArgs ++ traceArgs) (← getLeanc)
 
 /-- Build a static library from object file jobs using the `ar` packaged with Lean. -/
 def buildStaticLib
@@ -317,10 +315,7 @@ def buildStaticLib
   buildFileAfterDepArray libFile oFileJobs fun oFiles => do
     compileStaticLib libFile oFiles (← getLeanAr)
 
-/--
-Build a shared library by linking the results of `linkJobs`
-using the Lean toolchain's C compiler.
--/
+/-- Build a shared library by linking the results of `linkJobs` using `leanc`. -/
 def buildLeanSharedLib
   (libFile : FilePath) (linkJobs : Array (BuildJob FilePath))
   (weakArgs traceArgs : Array String := #[])
@@ -328,31 +323,19 @@ def buildLeanSharedLib
   let extraDepTrace :=
     return (← getLeanTrace).mix <| (pureHash traceArgs).mix platformTrace
   buildFileAfterDepArray libFile linkJobs (extraDepTrace := extraDepTrace) fun links => do
-    let lean ← getLeanInstall
-    let args := links.map toString ++ weakArgs ++ traceArgs ++ lean.ccLinkSharedFlags
-    compileSharedLib libFile args lean.cc
+    compileSharedLib libFile (links.map toString ++ weakArgs ++ traceArgs) (← getLeanc)
 
-
-/--
-Build an executable by linking the results of `linkJobs`
-using the Lean toolchain's linker.
--/
+/-- Build an executable by linking the results of `linkJobs` using `leanc`. -/
 def buildLeanExe
   (exeFile : FilePath) (linkJobs : Array (BuildJob FilePath))
-  (weakArgs traceArgs : Array String := #[]) (sharedLean : Bool := false)
+  (weakArgs traceArgs : Array String := #[])
 : SpawnM (BuildJob FilePath) :=
   let extraDepTrace :=
-    return (← getLeanTrace).mix <|
-      (pureHash sharedLean).mix <| (pureHash traceArgs).mix platformTrace
+    return (← getLeanTrace).mix <| (pureHash traceArgs).mix platformTrace
   buildFileAfterDepArray exeFile linkJobs (extraDepTrace := extraDepTrace) fun links => do
-    let lean ← getLeanInstall
-    let args := weakArgs ++ traceArgs ++ lean.ccLinkFlags sharedLean
-    compileExe exeFile links args lean.cc
+    compileExe exeFile links (weakArgs ++ traceArgs) (← getLeanc)
 
-/--
-Build a shared library from a static library using `leanc`
-using the Lean toolchain's linker.
--/
+/-- Build a shared library from a static library using `leanc`. -/
 def buildLeanSharedLibOfStatic
   (staticLibJob : BuildJob FilePath)
   (weakArgs traceArgs : Array String := #[])
@@ -364,12 +347,11 @@ def buildLeanSharedLibOfStatic
         #[s!"-Wl,-force_load,{staticLib}"]
       else
         #["-Wl,--whole-archive", staticLib.toString, "-Wl,--no-whole-archive"]
-    let lean ← getLeanInstall
     let depTrace := staticTrace.mix <|
       (← getLeanTrace).mix <| (pureHash traceArgs).mix <| platformTrace
-    let args := baseArgs ++ weakArgs ++ traceArgs ++ lean.ccLinkSharedFlags
+    let args := baseArgs ++ weakArgs ++ traceArgs
     let trace ← buildFileUnlessUpToDate dynlib depTrace do
-      compileSharedLib dynlib args lean.cc
+      compileSharedLib dynlib args (← getLeanc)
     return (dynlib, trace)
 
 /-- Construct a `Dynlib` object for a shared library target. -/

src/lake/Lake/Build/Data.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
 -/
-prelude
 import Lake.Build.Key
 import Lake.Util.Family
 

src/lake/Lake/Build/Executable.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
 -/
-prelude
 import Lake.Build.Common
 
 namespace Lake
@@ -30,4 +29,4 @@ def LeanExe.recBuildExe (self : LeanExe) : FetchM (BuildJob FilePath) :=
   let deps := (← fetch <| self.pkg.facet `deps).push self.pkg
   for dep in deps do for lib in dep.externLibs do
     linkJobs := linkJobs.push <| ← lib.static.fetch
-  buildLeanExe self.file linkJobs self.weakLinkArgs self.linkArgs self.sharedLean
+  buildLeanExe self.file linkJobs self.weakLinkArgs self.linkArgs

src/lake/Lake/Build/Facets.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
 -/
-prelude
 import Lake.Build.Job
 import Lake.Build.Data
 

src/lake/Lake/Build/Fetch.lean

@@ -3,7 +3,6 @@ Copyright (c) 2024 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-prelude
 import Lake.Util.Error
 import Lake.Util.Cycle
 import Lake.Util.EquipT
@@ -93,12 +92,10 @@ def ensureJob (x : FetchM (Job α))
   let iniPos := log.endPos
   match (← (withLoggedIO x) fetch stack ctx log store) with
   | (.ok job log, store) =>
-    if iniPos < log.endPos then
-      let (log, jobLog) := log.split iniPos
-      let job := job.mapResult (sync := true) (·.prependLog jobLog)
-      return (.ok job log, store)
-    else
-      return (.ok job log, store)
+    let (log, jobLog) := log.split iniPos
+    let job := if jobLog.isEmpty then job else job.mapResult (sync := true)
+      (·.modifyState (.modifyLog (jobLog ++  ·)))
+    return (.ok job log, store)
   | (.error _ log, store) =>
     let (log, jobLog) := log.split iniPos
     return (.ok (.error jobLog) log, store)

src/lake/Lake/Build/Imports.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
 -/
-prelude
 import Lake.Build.Module
 
 /-!

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
 -/
-prelude
 import Lake.Build.Executable
 import Lake.Build.Topological
 

src/lake/Lake/Build/Info.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
 -/
-prelude
 import Lake.Config.LeanExe
 import Lake.Config.ExternLib
 import Lake.Build.Facets

src/lake/Lake/Build/Job.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
 -/
-prelude
 import Lake.Util.Task
 import Lake.Build.Basic
 
@@ -64,12 +63,6 @@ def JobState.merge (a b : JobState) : JobState where
 /-- The result of a Lake job. -/
 abbrev JobResult α := EResult Log.Pos JobState α
 
-/-- Add log entries to the beginning of the job's log. -/
-def JobResult.prependLog (log : Log) (self : JobResult α) : JobResult α :=
-  match self with
-  | .ok a s => .ok a <| s.modifyLog (log ++ ·)
-  | .error e s => .error ⟨log.size + e.val⟩ <| s.modifyLog (log ++ ·)
-
 /-- The `Task` of a Lake job. -/
 abbrev JobTask α := BaseIOTask (JobResult α)
 

src/lake/Lake/Build/Key.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
 -/
-prelude
 import Lake.Util.Name
 
 namespace Lake

src/lake/Lake/Build/Library.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
 -/
-prelude
 import Lake.Build.Common
 import Lake.Build.Targets
 

src/lake/Lake/Build/Module.lean

@@ -3,7 +3,6 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich, Mac Malone, Siddharth Bhat
 -/
-prelude
 import Lake.Util.OrdHashSet
 import Lake.Util.List
 import Lean.Elab.ParseImportsFast

src/lake/Lake/Build/Package.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
 -/
-prelude
 import Lake.Util.Git
 import Lake.Util.Sugar
 import Lake.Build.Common

src/lake/Lake/Build/Run.lean

@@ -3,7 +3,6 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone, Gabriel Ebner, Sebastian Ullrich
 -/
-prelude
 import Lake.Util.Lock
 import Lake.Build.Index
 

src/lake/Lake/Build/Store.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
 -/
-prelude
 import Lake.Build.Data
 import Lake.Util.StoreInsts
 

src/lake/Lake/Build/Targets.lean

@@ -3,7 +3,6 @@ Copyright (c) 2023 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-prelude
 import Lake.Config.Monad
 
 /-! # Build Target Fetching

src/lake/Lake/Build/Topological.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
 -/
-prelude
 import Lake.Util.Cycle
 import Lake.Util.Store
 import Lake.Util.EquipT

src/lake/Lake/Build/Trace.lean

@@ -3,7 +3,6 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-prelude
 import Lake.Util.IO
 import Lean.Data.Json
 
@@ -126,9 +125,6 @@ instance : ToString Hash := ⟨Hash.toString⟩
 @[inline] def ofByteArray (bytes : ByteArray) : Hash :=
   ⟨hash bytes⟩
 
-@[inline] def ofBool (b : Bool) :=
-  mk (hash b)
-
 @[inline] protected def toJson (self : Hash) : Json :=
   toJson self.val
 
@@ -155,7 +151,6 @@ instance [ComputeHash α m] : ComputeTrace α m Hash := ⟨ComputeHash.computeHa
 @[inline] def computeHash [ComputeHash α m] [MonadLiftT m n] (a : α) : n Hash :=
   liftM <| ComputeHash.computeHash a
 
-instance : ComputeHash Bool Id := ⟨Hash.ofBool⟩
 instance : ComputeHash String Id := ⟨Hash.ofString⟩
 
 /--

src/lake/Lake/CLI.lean

@@ -3,5 +3,4 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-prelude
 import Lake.CLI.Main

src/lake/Lake/CLI/Actions.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
 -/
-prelude
 import Lake.Build.Run
 import Lake.Build.Targets
 import Lake.CLI.Build

src/lake/Lake/CLI/Build.lean

@@ -3,7 +3,6 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-prelude
 import Lake.Build.Index
 import Lake.CLI.Error
 

src/lake/Lake/CLI/Error.lean

@@ -3,9 +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
 -/
-prelude
-import Init.Data.ToString
-import Init.System.FilePath
 
 namespace Lake
 open Lean (Name)

src/lake/Lake/CLI/Help.lean

@@ -3,7 +3,6 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
-prelude
 import Lake.Version
 
 namespace Lake

src/lake/Lake/CLI/Init.lean

@@ -3,7 +3,6 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
-prelude
 import Lake.Util.Git
 import Lake.Util.Sugar
 import Lake.Util.Version

src/lake/Lake/CLI/Main.lean

@@ -3,7 +3,6 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-prelude
 import Lake.Load
 import Lake.Build.Imports
 import Lake.Util.Error

src/lake/Lake/CLI/Serve.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
 -/
-prelude
 import Lake.Load
 import Lake.Build
 import Lake.Util.MainM

src/lake/Lake/CLI/Translate.lean

@@ -3,7 +3,6 @@ Copyright (c) 2024 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-prelude
 import Lake.Config.Lang
 import Lake.Config.Package
 import Lake.CLI.Translate.Toml

src/lake/Lake/CLI/Translate/Lean.lean

@@ -3,7 +3,6 @@ Copyright (c) 2024 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-prelude
 import Lake.DSL
 import Lake.Config.Package
 import Lean.Parser.Module

src/lake/Lake/CLI/Translate/Toml.lean

@@ -3,7 +3,6 @@ Copyright (c) 2024 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-prelude
 import Lake.Toml.Encode
 import Lake.Config.Package
 

src/lake/Lake/Config.lean

@@ -3,5 +3,4 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-prelude
 import Lake.Config.Monad

src/lake/Lake/Config/Context.lean

@@ -3,7 +3,6 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-prelude
 import Lake.Config.Opaque
 import Lake.Config.InstallPath
 

src/lake/Lake/Config/Defaults.lean

@@ -3,11 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-prelude
-import Init.System.FilePath
-
 namespace Lake
-
 open System (FilePath)
 
 /--

src/lake/Lake/Config/Dependency.lean

@@ -3,8 +3,6 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
-prelude
-import Init.System.FilePath
 import Lean.Data.NameMap
 
 /- # Package Dependency Configuration

src/lake/Lake/Config/Env.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
 -/
-prelude
 import Lake.Util.Name
 import Lake.Util.NativeLib
 import Lake.Config.InstallPath

src/lake/Lake/Config/ExternLib.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
 -/
-prelude
 import Lake.Config.Package
 
 namespace Lake

src/lake/Lake/Config/ExternLibConfig.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
 -/
-prelude
 import Lake.Build.Job
 import Lake.Build.Data
 

src/lake/Lake/Config/FacetConfig.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, Mario Carneiro
 -/
-prelude
 import Lake.Build.Fetch
 
 namespace Lake

src/lake/Lake/Config/Glob.lean

@@ -3,7 +3,6 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Mac Malone
 -/
-prelude
 import Lean.Util.Path
 import Lake.Util.Name
 

src/lake/Lake/Config/InstallPath.lean

@@ -3,15 +3,10 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-
-prelude
-import Init.Control.Option
-import Lean.Compiler.FFI
 import Lake.Util.NativeLib
 import Lake.Config.Defaults
 
-open System Lean.Compiler.FFI
-
+open System
 namespace Lake
 
 /-- Convert the string value of an environment variable to a boolean. -/
@@ -76,13 +71,7 @@ structure LeanInstall where
   initSharedLib := leanSharedLibDir sysroot / initSharedLib
   ar : FilePath := "ar"
   cc : FilePath := "cc"
-  customCc : Bool := true
-  cFlags := getCFlags sysroot |>.push "-Wno-unused-command-line-argument"
-  linkStaticFlags := getLinkerFlags sysroot (linkStatic := true)
-  linkSharedFlags := getLinkerFlags sysroot (linkStatic := false)
-  ccFlags := cFlags
-  ccLinkStaticFlags := linkStaticFlags
-  ccLinkSharedFlags := linkSharedFlags
+  customCc : Bool := false
   deriving Inhabited, Repr
 
 /--
@@ -99,10 +88,6 @@ def LeanInstall.sharedLibPath (self : LeanInstall) : SearchPath :=
 def LeanInstall.leanCc? (self : LeanInstall) : Option String :=
   if self.customCc then self.cc.toString else none
 
-/-- The link-time flags for the C compiler of the Lean installation. -/
-def LeanInstall.ccLinkFlags (shared : Bool) (self : LeanInstall) : Array String :=
-  if shared then self.ccLinkSharedFlags else self.ccLinkStaticFlags
-
 /-- Lake executable file name. -/
 def lakeExe : FilePath :=
   FilePath.addExtension "lake" FilePath.exeExtension
@@ -193,7 +178,8 @@ def LeanInstall.get (sysroot : FilePath) (collocated : Bool := false) : BaseIO L
       -- Remark: This is expensive (at least on Windows), so try to avoid it.
       getGithash
   let ar ← findAr
-  setCc {sysroot, githash, ar}
+  let (cc, customCc) ← findCc
+  return {sysroot, githash, ar, cc, customCc}
 where
   getGithash := do
     EIO.catchExceptions (h := fun _ => pure "") do
@@ -201,7 +187,7 @@ where
         cmd := leanExe sysroot |>.toString,
         args := #["--githash"]
       }
-      return out.stdout.trim
+      pure <| out.stdout.trim
   findAr := do
     if let some ar ← IO.getEnv "LEAN_AR" then
       return FilePath.mk ar
@@ -213,27 +199,19 @@ where
         return ar
       else
         return "ar"
-  setCc i := do
+  findCc := do
     if let some cc ← IO.getEnv "LEAN_CC" then
-      return withCustomCc i cc
+      return (FilePath.mk cc, true)
     else
       let cc := leanCcExe sysroot
-      if (← cc.pathExists) then
-        return withInternalCc i cc
-      else if let some cc ← IO.getEnv "CC" then
-        return withCustomCc i cc
-      else
-        return withCustomCc i "cc"
-  @[inline] withCustomCc (i : LeanInstall) cc :=
-    {i with cc}
-  withInternalCc (i : LeanInstall) cc :=
-    let ccLinkFlags := getInternalLinkerFlags sysroot
-    {i with
-      cc, customCc := false
-      ccFlags := i.cFlags ++ getInternalCFlags sysroot
-      ccLinkStaticFlags := ccLinkFlags ++ i.linkStaticFlags
-      ccLinkSharedFlags := ccLinkFlags ++ i.linkSharedFlags
-    }
+      let cc ←
+        if (← cc.pathExists) then
+          pure cc
+        else if let some cc ← IO.getEnv "CC" then
+          pure cc
+        else
+          pure "cc"
+      return (cc, false)
 
 /--
 Attempt to detect the installation of the given `lean` command

src/lake/Lake/Config/Lang.lean

@@ -3,9 +3,6 @@ Copyright (c) 2024 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-prelude
-import Init.Data.ToString.Basic
-
 namespace Lake
 
 /-- Lake configuration language identifier. -/

src/lake/Lake/Config/LeanConfig.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
 -/
-prelude
 import Lean.Util.LeanOptions
 
 namespace Lake

src/lake/Lake/Config/LeanExe.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-prelude
+import Lean.Compiler.FFI
 import Lake.Config.Module
 
 namespace Lake
@@ -74,27 +74,21 @@ The file name of binary executable
 
 /--
 The arguments to pass to `leanc` when linking the binary executable.
-
 By default, the package's plus the executable's `moreLinkArgs`.
-If `supportInterpreter := true`, Lake prepends `-rdynamic` on non-Windows
-systems.
+
+If `supportInterpreter := true`, Lake links directly to the Lean shared
+libraries on Windows by prepending `-leanshared` and adds `-rdynamic` on
+other systems.
 -/
 def linkArgs (self : LeanExe) : Array String :=
-  if self.config.supportInterpreter && !Platform.isWindows then
-    #["-rdynamic"] ++ self.pkg.moreLinkArgs ++ self.config.moreLinkArgs
+  if self.config.supportInterpreter then
+    if Platform.isWindows then
+      #["-leanshared"] ++ self.pkg.moreLinkArgs ++ self.config.moreLinkArgs
+    else
+      #["-rdynamic"] ++ self.pkg.moreLinkArgs ++ self.config.moreLinkArgs
   else
     self.pkg.moreLinkArgs ++ self.config.moreLinkArgs
 
-/--
-Whether the Lean shared library should be dynamically linked to the executable.
-
-If `supportInterpreter := true`, Lean symbols must be visible to the
-interpreter. On Windows, it is not possible to statically include these
-symbols in the executable due to symbol limits, so Lake dynamically links to
-the Lean shared library. Otherwise, Lean is linked statically.
--/
-@[inline] def sharedLean (self : LeanExe) : Bool :=
-  strictAnd Platform.isWindows self.config.supportInterpreter
 
 /--
 The arguments to weakly pass to `leanc` when linking the binary executable.

src/lake/Lake/Config/LeanExeConfig.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
 -/
-prelude
 import Lake.Build.Facets
 import Lake.Config.LeanConfig
 

src/lake/Lake/Config/LeanLib.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
 -/
-prelude
 import Lake.Config.Package
 
 namespace Lake

src/lake/Lake/Config/LeanLibConfig.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
 -/
-prelude
 import Lake.Util.Casing
 import Lake.Build.Facets
 import Lake.Config.InstallPath

src/lake/Lake/Config/Module.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
 -/
-prelude
 import Lake.Build.Trace
 import Lake.Config.LeanLib
 import Lake.Util.OrdHashSet

src/lake/Lake/Config/Monad.lean

@@ -3,7 +3,6 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-prelude
 import Lake.Config.Context
 import Lake.Config.Workspace
 

src/lake/Lake/Config/Opaque.lean

@@ -3,7 +3,6 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-prelude
 import Lake.Util.Name
 import Lake.Util.Opaque
 

src/lake/Lake/Config/Package.lean

@@ -3,7 +3,6 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
-prelude
 import Lake.Config.Opaque
 import Lake.Config.Defaults
 import Lake.Config.LeanLibConfig

src/lake/Lake/Config/Script.lean

@@ -3,7 +3,6 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-prelude
 import Lake.Util.Exit
 import Lake.Config.Context
 

src/lake/Lake/Config/TargetConfig.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
 -/
-prelude
 import Lake.Build.Fetch
 
 namespace Lake

src/lake/Lake/Config/Workspace.lean

@@ -3,7 +3,6 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-prelude
 import Lean.Util.Paths
 import Lake.Config.FacetConfig
 import Lake.Config.TargetConfig

src/lake/Lake/Config/WorkspaceConfig.lean

@@ -3,7 +3,6 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-prelude
 import Lake.Config.Defaults
 
 open System

src/lake/Lake/DSL.lean

@@ -3,7 +3,6 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-prelude
 import Lake.DSL.DeclUtil
 import Lake.DSL.Attributes
 import Lake.DSL.Extensions