chore: upstream List.modify, add lemmas, relate to Array.modify

.github/workflows/nix-ci.yml

@@ -96,7 +96,7 @@ jobs:
           nix build $NIX_BUILD_ARGS .#cacheRoots -o push-build
       - name: Test
         run: |
-          nix build --keep-failed $NIX_BUILD_ARGS .#test -o push-test || (ln -s /tmp/nix-build-*/build/source/src/build ./push-test; false)
+          nix build --keep-failed $NIX_BUILD_ARGS .#test -o push-test || (ln -s /tmp/nix-build-*/source/src/build/ ./push-test; false)
       - name: Test Summary
         uses: test-summary/action@v2
         with:

doc/make/msys2.md

@@ -15,13 +15,6 @@ Mode](https://docs.microsoft.com/en-us/windows/apps/get-started/enable-your-devi
 which will allow Lean to create symlinks that e.g. enable go-to-definition in
 the stdlib.
 
-## Installing the Windows SDK
-
-Install the Windows SDK from [Microsoft](https://developer.microsoft.com/en-us/windows/downloads/windows-sdk/).
-The oldest supported version is 10.0.18362.0. If you installed the Windows SDK to the default location,
-then there should be a directory with the version number at `C:\Program Files (x86)\Windows Kits\10\Include`.
-If there are multiple directories, only the highest version number matters.
-
 ## Installing dependencies
 
 [The official webpage of MSYS2][msys2] provides one-click installers.

doc/setup.md

@@ -7,7 +7,7 @@ Platforms built & tested by our CI, available as binary releases via elan (see b
 * x86-64 Linux with glibc 2.27+
 * x86-64 macOS 10.15+
 * aarch64 (Apple Silicon) macOS 10.15+
-* x86-64 Windows 11 (any version), Windows 10 (version 1903 or higher), Windows Server 2022
+* x86-64 Windows 10+
 
 ### Tier 2
 

script/prepare-llvm-mingw.sh

@@ -31,20 +31,14 @@ cp /clang64/lib/{crtbegin,crtend,crt2,dllcrt2}.o stage1/lib/
 # runtime
 (cd llvm; cp --parents lib/clang/*/lib/*/libclang_rt.builtins* ../stage1)
 # further dependencies
-# Note: even though we're linking against libraries like `libbcrypt.a` which appear to be static libraries from the file name,
-# we're not actually linking statically against the code.
-# Rather, `libbcrypt.a` is an import library (see https://en.wikipedia.org/wiki/Dynamic-link_library#Import_libraries) that just
-# tells the compiler how to dynamically link against `bcrypt.dll` (which is located in the System32 folder).
-# This distinction is relevant specifically for `libicu.a`/`icu.dll` because there we want updates to the time zone database to
-# be delivered to users via Windows Update without having to recompile Lean or Lean programs.
-cp /clang64/lib/lib{m,bcrypt,mingw32,moldname,mingwex,msvcrt,pthread,advapi32,shell32,user32,kernel32,ucrtbase,psapi,iphlpapi,userenv,ws2_32,dbghelp,ole32,icu}.* /clang64/lib/libgmp.a /clang64/lib/libuv.a llvm/lib/lib{c++,c++abi,unwind}.a stage1/lib/
+cp /clang64/lib/lib{m,bcrypt,mingw32,moldname,mingwex,msvcrt,pthread,advapi32,shell32,user32,kernel32,ucrtbase,psapi,iphlpapi,userenv,ws2_32,dbghelp,ole32}.* /clang64/lib/libgmp.a /clang64/lib/libuv.a llvm/lib/lib{c++,c++abi,unwind}.a stage1/lib/
 echo -n " -DLEAN_STANDALONE=ON"
 echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang.exe -DCMAKE_C_COMPILER_WORKS=1 -DCMAKE_CXX_COMPILER=$PWD/llvm/bin/clang++.exe -DCMAKE_CXX_COMPILER_WORKS=1 -DLEAN_CXX_STDLIB='-lc++ -lc++abi'"
 echo -n " -DSTAGE0_CMAKE_C_COMPILER=clang -DSTAGE0_CMAKE_CXX_COMPILER=clang++"
 echo -n " -DLEAN_EXTRA_CXX_FLAGS='--sysroot $PWD/llvm -idirafter /clang64/include/'"
 echo -n " -DLEANC_INTERNAL_FLAGS='--sysroot ROOT -nostdinc -isystem ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang.exe"
 echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -static-libgcc -Wl,-Bstatic -lgmp $(pkg-config --static --libs libuv) -lunwind -Wl,-Bdynamic -fuse-ld=lld'"
-# when not using the above flags, link GMP dynamically/as usual. Always link ICU dynamically.
+# when not using the above flags, link GMP dynamically/as usual
 echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp $(pkg-config --libs libuv) -lucrtbase'"
 # do not set `LEAN_CC` for tests
 echo -n " -DAUTO_THREAD_FINALIZATION=OFF -DSTAGE0_AUTO_THREAD_FINALIZATION=OFF"

src/CMakeLists.txt

@@ -297,23 +297,6 @@ if(NOT LEAN_STANDALONE)
   string(APPEND LEAN_EXTRA_LINKER_FLAGS " ${LIBUV_LIBRARIES}")
 endif()
 
-# Windows SDK (for ICU)
-if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
-  # Pass 'tools' to skip MSVC version check (as MSVC/Visual Studio is not necessarily installed)
-  find_package(WindowsSDK REQUIRED COMPONENTS tools)
-
-  # This will give a semicolon-separated list of include directories
-  get_windowssdk_include_dirs(${WINDOWSSDK_LATEST_DIR} WINDOWSSDK_INCLUDE_DIRS)
-
-  # To successfully build against Windows SDK headers, the Windows SDK headers must have lower
-  # priority than other system headers, so use `-idirafter`. Unfortunately, CMake does not
-  # support this using `include_directories`.
-  string(REPLACE ";" "\" -idirafter \"" WINDOWSSDK_INCLUDE_DIRS "${WINDOWSSDK_INCLUDE_DIRS}")
-  string(APPEND CMAKE_CXX_FLAGS " -idirafter \"${WINDOWSSDK_INCLUDE_DIRS}\"")
-
-  string(APPEND LEAN_EXTRA_LINKER_FLAGS " -licu")
-endif()
-
 # ccache
 if(CCACHE AND NOT CMAKE_CXX_COMPILER_LAUNCHER AND NOT CMAKE_C_COMPILER_LAUNCHER)
   find_program(CCACHE_PATH ccache)
@@ -497,7 +480,7 @@ endif()
 # Git HASH
 if(USE_GITHASH)
   include(GetGitRevisionDescription)
-  get_git_head_revision(GIT_REFSPEC GIT_SHA1 ALLOW_LOOKING_ABOVE_CMAKE_SOURCE_DIR)
+  get_git_head_revision(GIT_REFSPEC GIT_SHA1)
   if(${GIT_SHA1} MATCHES "GITDIR-NOTFOUND")
     message(STATUS "Failed to read git_sha1")
     set(GIT_SHA1 "")

src/Init/Control/Basic.lean

@@ -8,28 +8,6 @@ import Init.Core
 
 universe u v w
 
-/--
-A `ForIn'` instance, which handles `for h : x in c do`,
-can also handle `for x in x do` by ignoring `h`, and so provides a `ForIn` instance.
--/
-instance (priority := low) instForInOfForIn' [ForIn' m ρ α d] : ForIn m ρ α where
-  forIn x b f := forIn' x b fun a _ => f a
-
-@[simp] theorem forIn'_eq_forIn [d : Membership α ρ] [ForIn' m ρ α d] {β} [Monad m] (x : ρ) (b : β)
-    (f : (a : α) → a ∈ x → β → m (ForInStep β)) (g : (a : α) → β → m (ForInStep β))
-    (h : ∀ a m b, f a m b = g a b) :
-    forIn' x b f = forIn x b g := by
-  simp [instForInOfForIn']
-  congr
-  apply funext
-  intro a
-  apply funext
-  intro m
-  apply funext
-  intro b
-  simp [h]
-  rfl
-
 @[reducible]
 def Functor.mapRev {f : Type u → Type v} [Functor f] {α β : Type u} : f α → (α → β) → f β :=
   fun a f => f <$> a

src/Init/Control/StateRef.lean

@@ -6,7 +6,8 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 The State monad transformer using IO references.
 -/
 prelude
-import Init.System.ST
+import Init.System.IO
+import Init.Control.State
 
 def StateRefT' (ω : Type) (σ : Type) (m : Type → Type) (α : Type) : Type := ReaderT (ST.Ref ω σ) m α
 

src/Init/Core.lean

@@ -324,6 +324,7 @@ class ForIn' (m : Type u₁ → Type u₂) (ρ : Type u) (α : outParam (Type v)
 
 export ForIn' (forIn')
 
+
 /--
 Auxiliary type used to compile `do` notation. It is used when compiling a do block
 nested inside a combinator like `tryCatch`. It encodes the possible ways the

src/Init/Data/Array/Basic.lean

@@ -82,22 +82,6 @@ theorem ext' {as bs : Array α} (h : as.toList = bs.toList) : as = bs := by
 
 @[simp] theorem getElem_toList {a : Array α} {i : Nat} (h : i < a.size) : a.toList[i] = a[i] := rfl
 
-/-- `a ∈ as` is a predicate which asserts that `a` is in the array `as`. -/
--- NB: This is defined as a structure rather than a plain def so that a lemma
--- like `sizeOf_lt_of_mem` will not apply with no actual arrays around.
-structure Mem (as : Array α) (a : α) : Prop where
-  val : a ∈ as.toList
-
-instance : Membership α (Array α) where
-  mem := Mem
-
-theorem mem_def {a : α} {as : Array α} : a ∈ as ↔ a ∈ as.toList :=
-  ⟨fun | .mk h => h, Array.Mem.mk⟩
-
-@[simp] theorem getElem_mem {l : Array α} {i : Nat} (h : i < l.size) : l[i] ∈ l := by
-  rw [Array.mem_def, ← getElem_toList]
-  apply List.getElem_mem
-
 end Array
 
 namespace List
@@ -257,15 +241,12 @@ def swapAt! (a : Array α) (i : Nat) (v : α) : α × Array α :=
     have : Inhabited (α × Array α) := ⟨(v, a)⟩
     panic! ("index " ++ toString i ++ " out of bounds")
 
-/-- `take a n` returns the first `n` elements of `a`. -/
-def take (a : Array α) (n : Nat) : Array α :=
+def shrink (a : Array α) (n : Nat) : Array α :=
   let rec loop
     | 0,   a => a
     | n+1, a => loop n a.pop
   loop (a.size - n) a
 
-@[deprecated take (since := "2024-10-22")] abbrev shrink := @take
-
 @[inline]
 unsafe def modifyMUnsafe [Monad m] (a : Array α) (i : Nat) (f : α → m α) : m (Array α) := do
   if h : i < a.size then
@@ -332,37 +313,6 @@ protected def forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m
 instance : ForIn m (Array α) α where
   forIn := Array.forIn
 
-/-- See comment at `forInUnsafe` -/
-@[inline] unsafe def forIn'Unsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (b : β) (f : (a : α) → a ∈ as → β → m (ForInStep β)) : m β :=
-  let sz := as.usize
-  let rec @[specialize] loop (i : USize) (b : β) : m β := do
-    if i < sz then
-      let a := as.uget i lcProof
-      match (← f a lcProof b) with
-      | ForInStep.done  b => pure b
-      | ForInStep.yield b => loop (i+1) b
-    else
-      pure b
-  loop 0 b
-
-/-- Reference implementation for `forIn'` -/
-@[implemented_by Array.forIn'Unsafe]
-protected def forIn' {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (b : β) (f : (a : α) → a ∈ as → β → m (ForInStep β)) : m β :=
-  let rec loop (i : Nat) (h : i ≤ as.size) (b : β) : m β := do
-    match i, h with
-    | 0,   _ => pure b
-    | i+1, h =>
-      have h' : i < as.size            := Nat.lt_of_lt_of_le (Nat.lt_succ_self i) h
-      have : as.size - 1 < as.size     := Nat.sub_lt (Nat.zero_lt_of_lt h') (by decide)
-      have : as.size - 1 - i < as.size := Nat.lt_of_le_of_lt (Nat.sub_le (as.size - 1) i) this
-      match (← f as[as.size - 1 - i] (getElem_mem this) b) with
-      | ForInStep.done b  => pure b
-      | ForInStep.yield b => loop i (Nat.le_of_lt h') b
-  loop as.size (Nat.le_refl _) b
-
-instance : ForIn' m (Array α) α inferInstance where
-  forIn' := Array.forIn'
-
 /-- See comment at `forInUnsafe` -/
 @[inline]
 unsafe def foldlMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : β → α → m β) (init : β) (as : Array α) (start := 0) (stop := as.size) : m β :=

src/Init/Data/Array/Lemmas.lean

@@ -21,7 +21,8 @@ namespace Array
 
 @[simp] theorem getElem_mk {xs : List α} {i : Nat} (h : i < xs.length) : (Array.mk xs)[i] = xs[i] := rfl
 
-theorem getElem_eq_getElem_toList {a : Array α} (h : i < a.size) : a[i] = a.toList[i] := rfl
+theorem getElem_eq_getElem_toList {a : Array α} (h : i < a.size) : a[i] = a.toList[i] := by
+  by_cases i < a.size <;> (try simp [*]) <;> rfl
 
 theorem getElem?_eq_getElem {a : Array α} {i : Nat} (h : i < a.size) : a[i]? = some a[i] :=
   getElem?_pos ..
@@ -84,9 +85,6 @@ We prefer to pull `List.toArray` outwards.
     (a.toArrayAux b).size = b.size + a.length := by
   simp [size]
 
-@[simp] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
-  simp [mem_def]
-
 @[simp] theorem push_toArray (l : List α) (a : α) : l.toArray.push a = (l ++ [a]).toArray := by
   apply ext'
   simp
@@ -104,49 +102,6 @@ We prefer to pull `List.toArray` outwards.
 @[simp] theorem back_toArray [Inhabited α] (l : List α) : l.toArray.back = l.getLast! := by
   simp only [back, size_toArray, Array.get!_eq_getElem!, getElem!_toArray, getLast!_eq_getElem!]
 
-@[simp] theorem forIn_loop_toArray [Monad m] (l : List α) (f : α → β → m (ForInStep β)) (i : Nat)
-    (h : i ≤ l.length) (b : β) :
-    Array.forIn.loop l.toArray f i h b = (l.drop (l.length - i)).forIn b f := by
-  induction i generalizing l b with
-  | zero => simp [Array.forIn.loop]
-  | succ i ih =>
-    simp only [Array.forIn.loop, size_toArray, getElem_toArray, ih, forIn_eq_forIn]
-    rw [Nat.sub_add_eq, List.drop_sub_one (by omega), List.getElem?_eq_getElem (by omega)]
-    simp only [Option.toList_some, singleton_append, forIn_cons]
-    have t : l.length - 1 - i = l.length - i - 1 := by omega
-    simp only [t]
-    congr
-
-@[simp] theorem forIn_toArray [Monad m] (l : List α) (b : β) (f : α → β → m (ForInStep β)) :
-    forIn l.toArray b f = forIn l b f := by
-  change l.toArray.forIn b f = l.forIn b f
-  rw [Array.forIn, forIn_loop_toArray]
-  simp
-
-@[simp] theorem forIn'_loop_toArray [Monad m] (l : List α) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) (i : Nat)
-    (h : i ≤ l.length) (b : β) :
-    Array.forIn'.loop l.toArray f i h b =
-      forIn' (l.drop (l.length - i)) b (fun a m b => f a (by simpa using mem_of_mem_drop m) b) := by
-  induction i generalizing l b with
-  | zero =>
-    simp [Array.forIn'.loop]
-  | succ i ih =>
-    simp only [Array.forIn'.loop, size_toArray, getElem_toArray, ih, forIn_eq_forIn]
-    have t : drop (l.length - (i + 1)) l = l[l.length - i - 1] :: drop (l.length - i) l := by
-      simp only [Nat.sub_add_eq]
-      rw [List.drop_sub_one (by omega), List.getElem?_eq_getElem (by omega)]
-      simp only [Option.toList_some, singleton_append]
-    simp [t]
-    have t : l.length - 1 - i = l.length - i - 1 := by omega
-    simp only [t]
-    congr
-
-@[simp] theorem forIn'_toArray [Monad m] (l : List α) (b : β) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) :
-    forIn' l.toArray b f = forIn' l b (fun a m b => f a (mem_toArray.mpr m) b) := by
-  change Array.forIn' _ _ _ = List.forIn' _ _ _
-  rw [Array.forIn', forIn'_loop_toArray]
-  simp [List.forIn_eq_forIn]
-
 theorem foldrM_toArray [Monad m] (f : α → β → m β) (init : β) (l : List α) :
     l.toArray.foldrM f init = l.foldrM f init := by
   rw [foldrM_eq_reverse_foldlM_toList]
@@ -291,6 +246,9 @@ theorem anyM_stop_le_start [Monad m] (p : α → m Bool) (as : Array α) (start
     (h : min stop as.size ≤ start) : anyM p as start stop = pure false := by
   rw [anyM_eq_anyM_loop, anyM.loop, dif_neg (Nat.not_lt.2 h)]
 
+theorem mem_def {a : α} {as : Array α} : a ∈ as ↔ a ∈ as.toList :=
+  ⟨fun | .mk h => h, Array.Mem.mk⟩
+
 @[simp] theorem not_mem_empty (a : α) : ¬(a ∈ #[]) := by
   simp [mem_def]
 
@@ -480,6 +438,10 @@ theorem lt_of_getElem {x : α} {a : Array α} {idx : Nat} {hidx : idx < a.size}
     idx < a.size :=
   hidx
 
+@[simp] theorem getElem_mem {l : Array α} {i : Nat} (h : i < l.size) : l[i] ∈ l := by
+  erw [Array.mem_def, getElem_eq_getElem_toList]
+  apply List.get_mem
+
 theorem getElem_fin_eq_getElem_toList (a : Array α) (i : Fin a.size) : a[i] = a.toList[i] := rfl
 
 @[simp] theorem ugetElem_eq_getElem (a : Array α) {i : USize} (h : i.toNat < a.size) :
@@ -710,45 +672,6 @@ theorem getElem_range {n : Nat} {x : Nat} (h : x < (Array.range n).size) : (Arra
         true_and, Nat.not_lt] at h
       rw [List.getElem?_eq_none_iff.2 ‹_›, List.getElem?_eq_none_iff.2 (a.toList.length_reverse ▸ ‹_›)]
 
-/-! ### take -/
-
-@[simp] theorem size_take_loop (a : Array α) (n : Nat) : (take.loop n a).size = a.size - n := by
-  induction n generalizing a with
-  | zero => simp [take.loop]
-  | succ n ih =>
-    simp [take.loop, ih]
-    omega
-
-@[simp] theorem getElem_take_loop (a : Array α) (n : Nat) (i : Nat) (h : i < (take.loop n a).size) :
-    (take.loop n a)[i] = a[i]'(by simp at h; omega) := by
-  induction n generalizing a i with
-  | zero => simp [take.loop]
-  | succ n ih =>
-    simp [take.loop, ih]
-
-@[simp] theorem size_take (a : Array α) (n : Nat) : (a.take n).size = min n a.size  := by
-  simp [take]
-  omega
-
-@[simp] theorem getElem_take (a : Array α) (n : Nat) (i : Nat) (h : i < (a.take n).size) :
-    (a.take n)[i] = a[i]'(by simp at h; omega) := by
-  simp [take]
-
-@[simp] theorem toList_take (a : Array α) (n : Nat) : (a.take n).toList = a.toList.take n := by
-  apply List.ext_getElem <;> simp
-
-/-! ### forIn -/
-
-@[simp] theorem forIn_toList [Monad m] (as : Array α) (b : β) (f : α → β → m (ForInStep β)) :
-    forIn as.toList b f = forIn as b f := by
-  cases as
-  simp
-
-@[simp] theorem forIn'_toList [Monad m] (as : Array α) (b : β) (f : (a : α) → a ∈ as.toList → β → m (ForInStep β)) :
-    forIn' as.toList b f = forIn' as b (fun a m b => f a (mem_toList.mpr m) b) := by
-  cases as
-  simp
-
 /-! ### foldl / foldr -/
 
 @[simp] theorem foldlM_loop_empty [Monad m] (f : β → α → m β) (init : β) (i j : Nat) :
@@ -1412,6 +1335,9 @@ namespace List
 Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
 -/
 
+@[simp] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
+  simp [mem_def]
+
 @[simp] theorem toListRev_toArray (l : List α) : l.toArray.toListRev = l.reverse := by
   simp
 
@@ -1420,10 +1346,6 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
   apply ext'
   simp
 
-@[simp] theorem take_toArray (l : List α) (n : Nat) : l.toArray.take n = (l.take n).toArray := by
-  apply ext'
-  simp
-
 @[simp] theorem mapM_toArray [Monad m] [LawfulMonad m] (f : α → m β) (l : List α) :
     l.toArray.mapM f = List.toArray <$> l.mapM f := by
   simp only [← mapM'_eq_mapM, mapM_eq_foldlM]

src/Init/Data/Array/Mem.lean

@@ -10,6 +10,15 @@ import Init.Data.List.BasicAux
 
 namespace Array
 
+/-- `a ∈ as` is a predicate which asserts that `a` is in the array `as`. -/
+-- NB: This is defined as a structure rather than a plain def so that a lemma
+-- like `sizeOf_lt_of_mem` will not apply with no actual arrays around.
+structure Mem (as : Array α) (a : α) : Prop where
+  val : a ∈ as.toList
+
+instance : Membership α (Array α) where
+  mem := Mem
+
 theorem sizeOf_lt_of_mem [SizeOf α] {as : Array α} (h : a ∈ as) : sizeOf a < sizeOf as := by
   cases as with | _ as =>
   exact Nat.lt_trans (List.sizeOf_lt_of_mem h.val) (by simp_arith)

src/Init/Data/List/Basic.lean

@@ -29,7 +29,7 @@ The operations are organized as follow:
 * Lexicographic ordering: `lt`, `le`, and instances.
 * Head and tail operators: `head`, `head?`, `headD?`, `tail`, `tail?`, `tailD`.
 * Basic operations:
-  `map`, `filter`, `filterMap`, `foldr`, `append`, `flatten`, `pure`, `flatMap`, `replicate`, and
+  `map`, `filter`, `filterMap`, `foldr`, `append`, `flatten`, `pure`, `bind`, `replicate`, and
   `reverse`.
 * Additional functions defined in terms of these: `leftpad`, `rightPad`, and `reduceOption`.
 * Operations using indexes: `mapIdx`.

src/Init/Data/List/Control.lean

@@ -254,8 +254,6 @@ instance : ForIn m (List α) α where
 instance : ForIn' m (List α) α inferInstance where
   forIn' := List.forIn'
 
-@[simp] theorem forIn'_eq_forIn' [Monad m] : @List.forIn' α β m _ = forIn' := rfl
-
 @[simp] theorem forIn'_eq_forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : List α) (init : β) (f : α → β → m (ForInStep β)) : forIn' as init (fun a _ b => f a b) = forIn as init f := by
   simp [forIn', forIn, List.forIn, List.forIn']
   have : ∀ cs h, List.forIn'.loop cs (fun a _ b => f a b) as init h = List.forIn.loop f as init := by

src/Init/Data/List/Find.lean

@@ -595,14 +595,15 @@ theorem findIdx_eq {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs.length
 
 theorem findIdx_append (p : α → Bool) (l₁ l₂ : List α) :
     (l₁ ++ l₂).findIdx p =
-      if l₁.findIdx p < l₁.length then l₁.findIdx p else l₂.findIdx p + l₁.length := by
+      if ∃ x, x ∈ l₁ ∧ p x = true then l₁.findIdx p else l₂.findIdx p + l₁.length := by
   induction l₁ with
   | nil => simp
   | cons x xs ih =>
     simp only [findIdx_cons, length_cons, cons_append]
     by_cases h : p x
     · simp [h]
-    · simp only [h, ih, cond_eq_if, Bool.false_eq_true, ↓reduceIte, add_one_lt_add_one_iff]
+    · simp only [h, ih, cond_eq_if, Bool.false_eq_true, ↓reduceIte, mem_cons, exists_eq_or_imp,
+        false_or]
       split <;> simp [Nat.add_assoc]
 
 theorem IsPrefix.findIdx_le {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <+: l₂) :

src/Init/Data/List/Lemmas.lean

@@ -492,6 +492,10 @@ theorem getElem?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n : Nat, l[n]? = s
 theorem get?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n, l.get? n = some a :=
   let ⟨⟨n, _⟩, e⟩ := get_of_mem h; ⟨n, e ▸ get?_eq_get _⟩
 
+@[simp] theorem getElem_mem : ∀ {l : List α} {n} (h : n < l.length), l[n]'h ∈ l
+  | _ :: _, 0, _ => .head ..
+  | _ :: l, _+1, _ => .tail _ (getElem_mem (l := l) ..)
+
 theorem get_mem : ∀ (l : List α) n h, get l ⟨n, h⟩ ∈ l
   | _ :: _, 0, _ => .head ..
   | _ :: l, _+1, _ => .tail _ (get_mem l ..)

src/Init/Data/List/Monadic.lean

@@ -87,68 +87,6 @@ theorem mapM_eq_reverse_foldlM_cons [Monad m] [LawfulMonad m] (f : α → m β)
     (l₁ ++ l₂).forM f = (do l₁.forM f; l₂.forM f) := by
   induction l₁ <;> simp [*]
 
-/-! ### forIn' -/
-
-@[simp] theorem forIn'_nil [Monad m] (f : (a : α) → a ∈ [] → β → m (ForInStep β)) (b : β) : forIn' [] b f = pure b :=
-  rfl
-
-theorem forIn'_loop_congr [Monad m] {as bs : List α}
-    {f : (a' : α) → a' ∈ as → β → m (ForInStep β)}
-    {g : (a' : α) → a' ∈ bs → β → m (ForInStep β)}
-    {b : β} (ha : ∃ ys, ys ++ xs = as) (hb : ∃ ys, ys ++ xs = bs)
-    (h : ∀ a m m' b, f a m b = g a m' b) : forIn'.loop as f xs b ha = forIn'.loop bs g xs b hb  := by
-  induction xs generalizing b with
-  | nil => simp [forIn'.loop]
-  | cons a xs ih =>
-    simp only [forIn'.loop] at *
-    congr 1
-    · rw [h]
-    · funext s
-      obtain b | b := s
-      · rfl
-      · simp
-        rw [ih]
-
-@[simp] theorem forIn'_cons [Monad m] {a : α} {as : List α}
-    (f : (a' : α) → a' ∈ a :: as → β → m (ForInStep β)) (b : β) :
-    forIn' (a::as) b f = f a (mem_cons_self a as) b >>=
-      fun | ForInStep.done b => pure b | ForInStep.yield b => forIn' as b fun a' m b => f a' (mem_cons_of_mem a m) b := by
-  simp only [forIn', List.forIn', forIn'.loop]
-  congr 1
-  funext s
-  obtain b | b := s
-  · rfl
-  · apply forIn'_loop_congr
-    intros
-    rfl
-
-@[congr] theorem forIn'_congr [Monad m] {as bs : List α} (w : as = bs)
-    {b b' : β} (hb : b = b')
-    {f : (a' : α) → a' ∈ as → β → m (ForInStep β)}
-    {g : (a' : α) → a' ∈ bs → β → m (ForInStep β)}
-    (h : ∀ a m b, f a (by simpa [w] using m) b = g a m b) :
-    forIn' as b f = forIn' bs b' g := by
-  induction bs generalizing as b b' with
-  | nil =>
-    subst w
-    simp [hb, forIn'_nil]
-  | cons b bs ih =>
-    cases as with
-    | nil => simp at w
-    | cons a as =>
-      simp only [cons.injEq] at w
-      obtain ⟨rfl, rfl⟩ := w
-      simp only [forIn'_cons]
-      congr 1
-      · simp [h, hb]
-      · funext s
-        obtain b | b := s
-        · rfl
-        · simp
-          rw [ih rfl rfl]
-          intro a m b
-          exact h a (mem_cons_of_mem _ m) b
-
 /-! ### allM -/
 
 theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] (p : α → m Bool) (as : List α) :

src/Init/Data/List/Nat/Modify.lean

@@ -6,110 +6,14 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
 
 prelude
 import Init.Data.List.Nat.TakeDrop
-import Init.Data.List.Nat.Erase
 
 namespace List
 
 /-! ### modifyHead -/
 
-@[simp] theorem length_modifyHead {f : α → α} {l : List α} : (l.modifyHead f).length = l.length := by
-  cases l <;> simp [modifyHead]
-
-theorem modifyHead_eq_set [Inhabited α] (f : α → α) (l : List α) :
-    l.modifyHead f = l.set 0 (f (l[0]?.getD default)) := by cases l <;> simp [modifyHead]
-
-@[simp] theorem modifyHead_eq_nil_iff {f : α → α} {l : List α} :
-    l.modifyHead f = [] ↔ l = [] := by cases l <;> simp [modifyHead]
-
-@[simp] theorem modifyHead_modifyHead {l : List α} {f g : α → α} :
+@[simp] theorem modifyHead_modifyHead (l : List α) (f g : α → α) :
     (l.modifyHead f).modifyHead g = l.modifyHead (g ∘ f) := by cases l <;> simp [modifyHead]
 
-theorem getElem_modifyHead {l : List α} {f : α → α} {n} (h : n < (l.modifyHead f).length) :
-    (l.modifyHead f)[n] = if h' : n = 0 then f (l[0]'(by simp at h; omega)) else l[n]'(by simpa using h) := by
-  cases l with
-  | nil => simp at h
-  | cons hd tl => cases n <;> simp
-
-@[simp] theorem getElem_modifyHead_zero {l : List α} {f : α → α} {h} :
-    (l.modifyHead f)[0] = f (l[0]'(by simpa using h)) := by simp [getElem_modifyHead]
-
-@[simp] theorem getElem_modifyHead_succ {l : List α} {f : α → α} {n} (h : n + 1 < (l.modifyHead f).length) :
-    (l.modifyHead f)[n + 1] = l[n + 1]'(by simpa using h) := by simp [getElem_modifyHead]
-
-theorem getElem?_modifyHead {l : List α} {f : α → α} {n} :
-    (l.modifyHead f)[n]? = if n = 0 then l[n]?.map f else l[n]? := by
-  cases l with
-  | nil => simp
-  | cons hd tl => cases n <;> simp
-
-@[simp] theorem getElem?_modifyHead_zero {l : List α} {f : α → α} :
-    (l.modifyHead f)[0]? = l[0]?.map f := by simp [getElem?_modifyHead]
-
-@[simp] theorem getElem?_modifyHead_succ {l : List α} {f : α → α} {n} :
-    (l.modifyHead f)[n + 1]? = l[n + 1]? := by simp [getElem?_modifyHead]
-
-@[simp] theorem head_modifyHead (f : α → α) (l : List α) (h) :
-    (l.modifyHead f).head h = f (l.head (by simpa using h)) := by
-  cases l with
-  | nil => simp at h
-  | cons hd tl => simp
-
-@[simp] theorem head?_modifyHead {l : List α} {f : α → α} :
-    (l.modifyHead f).head? = l.head?.map f := by cases l <;> simp
-
-@[simp] theorem tail_modifyHead {f : α → α} {l : List α} :
-    (l.modifyHead f).tail = l.tail := by cases l <;> simp
-
-@[simp] theorem take_modifyHead {f : α → α} {l : List α} {n} :
-    (l.modifyHead f).take n = (l.take n).modifyHead f := by
-  cases l <;> cases n <;> simp
-
-@[simp] theorem drop_modifyHead_of_pos {f : α → α} {l : List α} {n} (h : 0 < n) :
-    (l.modifyHead f).drop n = l.drop n := by
-  cases l <;> cases n <;> simp_all
-
-@[simp] theorem eraseIdx_modifyHead_zero {f : α → α} {l : List α} :
-    (l.modifyHead f).eraseIdx 0 = l.eraseIdx 0 := by cases l <;> simp
-
-@[simp] theorem eraseIdx_modifyHead_of_pos {f : α → α} {l : List α} {n} (h : 0 < n) :
-    (l.modifyHead f).eraseIdx n = (l.eraseIdx n).modifyHead f := by cases l <;> cases n <;> simp_all
-
-@[simp] theorem modifyHead_id : modifyHead (id : α → α) = id := by funext l; cases l <;> simp
-
-/-! ### modifyTailIdx -/
-
-@[simp] theorem modifyTailIdx_id : ∀ n (l : List α), l.modifyTailIdx id n = l
-  | 0, _ => rfl
-  | _+1, [] => rfl
-  | n+1, a :: l => congrArg (cons a) (modifyTailIdx_id n l)
-
-theorem eraseIdx_eq_modifyTailIdx : ∀ n (l : List α), eraseIdx l n = modifyTailIdx tail n l
-  | 0, l => by cases l <;> rfl
-  | _+1, [] => rfl
-  | _+1, _ :: _ => congrArg (cons _) (eraseIdx_eq_modifyTailIdx _ _)
-
-@[simp] theorem length_modifyTailIdx (f : List α → List α) (H : ∀ l, length (f l) = length l) :
-    ∀ n l, length (modifyTailIdx f n l) = length l
-  | 0, _ => H _
-  | _+1, [] => rfl
-  | _+1, _ :: _ => congrArg (·+1) (length_modifyTailIdx _ H _ _)
-
-theorem modifyTailIdx_add (f : List α → List α) (n) (l₁ l₂ : List α) :
-    modifyTailIdx f (l₁.length + n) (l₁ ++ l₂) = l₁ ++ modifyTailIdx f n l₂ := by
-  induction l₁ <;> simp [*, Nat.succ_add]
-
-theorem modifyTailIdx_eq_take_drop (f : List α → List α) (H : f [] = []) :
-    ∀ n l, modifyTailIdx f n l = take n l ++ f (drop n l)
-  | 0, _ => rfl
-  | _ + 1, [] => H.symm
-  | n + 1, b :: l => congrArg (cons b) (modifyTailIdx_eq_take_drop f H n l)
-
-theorem exists_of_modifyTailIdx (f : List α → List α) {n} {l : List α} (h : n ≤ l.length) :
-    ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁.length = n ∧ modifyTailIdx f n l = l₁ ++ f l₂ :=
-  have ⟨_, _, eq, hl⟩ : ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁.length = n :=
-    ⟨_, _, (take_append_drop n l).symm, length_take_of_le h⟩
-  ⟨_, _, eq, hl, hl ▸ eq ▸ modifyTailIdx_add (n := 0) ..⟩
-
 /-! ### modify -/
 
 @[simp] theorem modify_nil (f : α → α) (n) : [].modify f n = [] := by cases n <;> rfl
@@ -120,11 +24,15 @@ theorem exists_of_modifyTailIdx (f : List α → List α) {n} {l : List α} (h :
 @[simp] theorem modify_succ_cons (f : α → α) (a : α) (l : List α) (n) :
     (a :: l).modify f (n + 1) = a :: l.modify f n := by rfl
 
-theorem modifyHead_eq_modify_zero (f : α → α) (l : List α) :
-    l.modifyHead f = l.modify f 0 := by cases l <;> simp
+theorem modifyTailIdx_id : ∀ n (l : List α), l.modifyTailIdx id n = l
+  | 0, _ => rfl
+  | _+1, [] => rfl
+  | n+1, a :: l => congrArg (cons a) (modifyTailIdx_id n l)
 
-@[simp] theorem modify_eq_nil_iff (f : α → α) (n) (l : List α) :
-    l.modify f n = [] ↔ l = [] := by cases l <;> cases n <;> simp
+theorem eraseIdx_eq_modifyTailIdx : ∀ n (l : List α), eraseIdx l n = modifyTailIdx tail n l
+  | 0, l => by cases l <;> rfl
+  | _+1, [] => rfl
+  | _+1, _ :: _ => congrArg (cons _) (eraseIdx_eq_modifyTailIdx _ _)
 
 theorem getElem?_modify (f : α → α) :
     ∀ n (l : List α) m, (modify f n l)[m]? = (fun a => if n = m then f a else a) <$> l[m]?
@@ -137,6 +45,16 @@ theorem getElem?_modify (f : α → α) :
     cases h' : l[m]? <;> by_cases h : n = m <;>
       simp [h, if_pos, if_neg, Option.map, mt Nat.succ.inj, not_false_iff, h']
 
+@[simp] theorem length_modifyTailIdx (f : List α → List α) (H : ∀ l, length (f l) = length l) :
+    ∀ n l, length (modifyTailIdx f n l) = length l
+  | 0, _ => H _
+  | _+1, [] => rfl
+  | _+1, _ :: _ => congrArg (·+1) (length_modifyTailIdx _ H _ _)
+
+theorem modifyTailIdx_add (f : List α → List α) (n) (l₁ l₂ : List α) :
+    modifyTailIdx f (l₁.length + n) (l₁ ++ l₂) = l₁ ++ modifyTailIdx f n l₂ := by
+  induction l₁ <;> simp [*, Nat.succ_add]
+
 @[simp] theorem length_modify (f : α → α) : ∀ n l, length (modify f n l) = length l :=
   length_modifyTailIdx _ fun l => by cases l <;> rfl
 
@@ -155,141 +73,30 @@ theorem getElem_modify (f : α → α) (n) (l : List α) (m) (h : m < (modify f
   simp at h
   simp [h]
 
-@[simp] theorem getElem_modify_eq (f : α → α) (n) (l : List α) (h) :
-    (modify f n l)[n] = f (l[n]'(by simpa using h)) := by simp [getElem_modify]
-
-@[simp] theorem getElem_modify_ne (f : α → α) {m n} (l : List α) (h : m ≠ n) (h') :
-    (modify f m l)[n] = l[n]'(by simpa using h') := by simp [getElem_modify, h]
-
-theorem modify_eq_self {f : α → α} {n} {l : List α} (h : l.length ≤ n) :
-    l.modify f n = l := by
-  apply ext_getElem
-  · simp
-  · intro m h₁ h₂
-    simp only [getElem_modify, ite_eq_right_iff]
-    intro h
-    omega
-
-theorem modify_modify_eq (f g : α → α) (n) (l : List α) :
-    (modify f n l).modify g n = modify (g ∘ f) n l := by
-  apply ext_getElem
-  · simp
-  · intro m h₁ h₂
-    simp only [getElem_modify, Function.comp_apply]
-    split <;> simp
-
-theorem modify_modify_ne (f g : α → α) {m n} (l : List α) (h : m ≠ n) :
-    (modify f m l).modify g n = (l.modify g n).modify f m := by
-  apply ext_getElem
-  · simp
-  · intro m' h₁ h₂
-    simp only [getElem_modify, getElem_modify_ne, h₂]
-    split <;> split <;> first | rfl | omega
-
-theorem modify_eq_set [Inhabited α] (f : α → α) (n) (l : List α) :
-    modify f n l = l.set n (f (l[n]?.getD default)) := by
-  apply ext_getElem
-  · simp
-  · intro m h₁ h₂
-    simp [getElem_modify, getElem_set, h₂]
-    split <;> rename_i h
-    · subst h
-      simp only [length_modify] at h₁
-      simp [h₁]
-    · rfl
+theorem modifyTailIdx_eq_take_drop (f : List α → List α) (H : f [] = []) :
+    ∀ n l, modifyTailIdx f n l = take n l ++ f (drop n l)
+  | 0, _ => rfl
+  | _ + 1, [] => H.symm
+  | n + 1, b :: l => congrArg (cons b) (modifyTailIdx_eq_take_drop f H n l)
 
 theorem modify_eq_take_drop (f : α → α) :
     ∀ n l, modify f n l = take n l ++ modifyHead f (drop n l) :=
   modifyTailIdx_eq_take_drop _ rfl
 
-theorem modify_eq_take_cons_drop {f : α → α} {n} {l : List α} (h : n < l.length) :
+theorem modify_eq_take_cons_drop (f : α → α) {n l} (h : n < length l) :
     modify f n l = take n l ++ f l[n] :: drop (n + 1) l := by
   rw [modify_eq_take_drop, drop_eq_getElem_cons h]; rfl
 
+theorem exists_of_modifyTailIdx (f : List α → List α) {n} {l : List α} (h : n ≤ l.length) :
+    ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁.length = n ∧ modifyTailIdx f n l = l₁ ++ f l₂ :=
+  have ⟨_, _, eq, hl⟩ : ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁.length = n :=
+    ⟨_, _, (take_append_drop n l).symm, length_take_of_le h⟩
+  ⟨_, _, eq, hl, hl ▸ eq ▸ modifyTailIdx_add (n := 0) ..⟩
+
 theorem exists_of_modify (f : α → α) {n} {l : List α} (h : n < l.length) :
     ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ l₁.length = n ∧ modify f n l = l₁ ++ f a :: l₂ :=
   match exists_of_modifyTailIdx _ (Nat.le_of_lt h) with
   | ⟨_, _::_, eq, hl, H⟩ => ⟨_, _, _, eq, hl, H⟩
   | ⟨_, [], eq, hl, _⟩ => nomatch Nat.ne_of_gt h (eq ▸ append_nil _ ▸ hl)
 
-@[simp] theorem modify_id (n) (l : List α) : l.modify id n = l := by
-  simp [modify]
-
-theorem take_modify (f : α → α) (n m) (l : List α) :
-    (modify f m l).take n = (take n l).modify f m := by
-  induction n generalizing l m with
-  | zero => simp
-  | succ n ih =>
-    cases l with
-    | nil => simp
-    | cons hd tl =>
-      cases m with
-      | zero => simp
-      | succ m => simp [ih]
-
-theorem drop_modify_of_lt (f : α → α) (n m) (l : List α) (h : n < m) :
-    (modify f n l).drop m = l.drop m := by
-  apply ext_getElem
-  · simp
-  · intro m' h₁ h₂
-    simp only [getElem_drop, getElem_modify, ite_eq_right_iff]
-    intro h'
-    omega
-
-theorem drop_modify_of_ge (f : α → α) (n m) (l : List α) (h : n ≥ m) :
-    (modify f n l).drop m = modify f (n - m) (drop m l) := by
-  apply ext_getElem
-  · simp
-  · intro m' h₁ h₂
-    simp [getElem_drop, getElem_modify, ite_eq_right_iff]
-    split <;> split <;> first | rfl | omega
-
-theorem eraseIdx_modify_of_eq (f : α → α) (n) (l : List α) :
-    (modify f n l).eraseIdx n = l.eraseIdx n := by
-  apply ext_getElem
-  · simp [length_eraseIdx]
-  · intro m h₁ h₂
-    simp only [getElem_eraseIdx, getElem_modify]
-    split <;> split <;> first | rfl | omega
-
-theorem eraseIdx_modify_of_lt (f : α → α) (i j) (l : List α) (h : j < i) :
-    (modify f i l).eraseIdx j = (l.eraseIdx j).modify f (i - 1) := by
-  apply ext_getElem
-  · simp [length_eraseIdx]
-  · intro k h₁ h₂
-    simp only [getElem_eraseIdx, getElem_modify]
-    by_cases h' : i - 1 = k
-    repeat' split
-    all_goals (first | rfl | omega)
-
-theorem eraseIdx_modify_of_gt (f : α → α) (i j) (l : List α) (h : j > i) :
-    (modify f i l).eraseIdx j = (l.eraseIdx j).modify f i := by
-  apply ext_getElem
-  · simp [length_eraseIdx]
-  · intro k h₁ h₂
-    simp only [getElem_eraseIdx, getElem_modify]
-    by_cases h' : i = k
-    repeat' split
-    all_goals (first | rfl | omega)
-
-theorem modify_eraseIdx_of_lt (f : α → α) (i j) (l : List α) (h : j < i) :
-    (l.eraseIdx i).modify f j = (l.modify f j).eraseIdx i := by
-  apply ext_getElem
-  · simp [length_eraseIdx]
-  · intro k h₁ h₂
-    simp only [getElem_eraseIdx, getElem_modify]
-    by_cases h' : j = k + 1
-    repeat' split
-    all_goals (first | rfl | omega)
-
-theorem modify_eraseIdx_of_ge (f : α → α) (i j) (l : List α) (h : j ≥ i) :
-    (l.eraseIdx i).modify f j = (l.modify f (j + 1)).eraseIdx i := by
-  apply ext_getElem
-  · simp [length_eraseIdx]
-  · intro k h₁ h₂
-    simp only [getElem_eraseIdx, getElem_modify]
-    by_cases h' : j + 1 = k + 1
-    repeat' split
-    all_goals (first | rfl | omega)
-
 end List

src/Init/Data/List/Nat/TakeDrop.lean

@@ -187,9 +187,6 @@ theorem take_add (l : List α) (m n : Nat) : l.take (m + n) = l.take m ++ (l.dro
   · apply length_take_le
   · apply Nat.le_add_right
 
-theorem take_one {l : List α} : l.take 1 = l.head?.toList := by
-  induction l <;> simp
-
 theorem dropLast_take {n : Nat} {l : List α} (h : n < l.length) :
     (l.take n).dropLast = l.take (n - 1) := by
   simp only [dropLast_eq_take, length_take, Nat.le_of_lt h, Nat.min_eq_left, take_take, sub_le]
@@ -285,14 +282,14 @@ theorem mem_drop_iff_getElem {l : List α} {a : α} :
   · rintro ⟨i, hm, rfl⟩
     refine ⟨i, by simp; omega, by rw [getElem_drop]⟩
 
-@[simp] theorem head?_drop (l : List α) (n : Nat) :
+theorem head?_drop (l : List α) (n : Nat) :
     (l.drop n).head? = l[n]? := by
   rw [head?_eq_getElem?, getElem?_drop, Nat.add_zero]
 
-@[simp] theorem head_drop {l : List α} {n : Nat} (h : l.drop n ≠ []) :
+theorem head_drop {l : List α} {n : Nat} (h : l.drop n ≠ []) :
     (l.drop n).head h = l[n]'(by simp_all) := by
   have w : n < l.length := length_lt_of_drop_ne_nil h
-  simp [getElem?_eq_getElem, h, w, head_eq_iff_head?_eq_some]
+  simpa [getElem?_eq_getElem, h, w, head_eq_iff_head?_eq_some] using head?_drop l n
 
 theorem getLast?_drop {l : List α} : (l.drop n).getLast? = if l.length ≤ n then none else l.getLast? := by
   rw [getLast?_eq_getElem?, getElem?_drop]
@@ -303,7 +300,7 @@ theorem getLast?_drop {l : List α} : (l.drop n).getLast? = if l.length ≤ n th
     congr
     omega
 
-@[simp] theorem getLast_drop {l : List α} (h : l.drop n ≠ []) :
+theorem getLast_drop {l : List α} (h : l.drop n ≠ []) :
     (l.drop n).getLast h = l.getLast (ne_nil_of_length_pos (by simp at h; omega)) := by
   simp only [ne_eq, drop_eq_nil_iff] at h
   apply Option.some_inj.1
@@ -452,26 +449,6 @@ theorem reverse_drop {l : List α} {n : Nat} :
     rw [w, take_zero, drop_of_length_le, reverse_nil]
     omega
 
-theorem take_add_one {l : List α} {n : Nat} :
-    l.take (n + 1) = l.take n ++ l[n]?.toList := by
-  simp [take_add, take_one]
-
-theorem drop_eq_getElem?_toList_append {l : List α} {n : Nat} :
-    l.drop n = l[n]?.toList ++ l.drop (n + 1) := by
-  induction l generalizing n with
-  | nil => simp
-  | cons hd tl ih =>
-    cases n
-    · simp
-    · simp only [drop_succ_cons, getElem?_cons_succ]
-      rw [ih]
-
-theorem drop_sub_one {l : List α} {n : Nat} (h : 0 < n) :
-    l.drop (n - 1) = l[n - 1]?.toList ++ l.drop n := by
-  rw [drop_eq_getElem?_toList_append]
-  congr
-  omega
-
 /-! ### findIdx -/
 
 theorem false_of_mem_take_findIdx {xs : List α} {p : α → Bool} (h : x ∈ xs.take (xs.findIdx p)) :

src/Init/Data/Option/Basic.lean

@@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mario Carneiro
 -/
 prelude
+import Init.Core
 import Init.Control.Basic
+import Init.Coe
 
 namespace Option
 

src/Init/Data/Option/List.lean

@@ -11,28 +11,4 @@ namespace Option
 @[simp] theorem mem_toList {a : α} {o : Option α} : a ∈ o.toList ↔ a ∈ o := by
   cases o <;> simp [eq_comm]
 
-@[simp] theorem forIn'_none [Monad m] (b : β) (f : (a : α) → a ∈ none → β → m (ForInStep β)) :
-    forIn' none b f = pure b := by
-  rfl
-
-@[simp] theorem forIn'_some [Monad m] (a : α) (b : β) (f : (a' : α) → a' ∈ some a → β → m (ForInStep β)) :
-    forIn' (some a) b f = bind (f a rfl b) (fun | .done r | .yield r => pure r) := by
-  rfl
-
-@[simp] theorem forIn_none [Monad m] (b : β) (f : α → β → m (ForInStep β)) :
-    forIn none b f = pure b := by
-  rfl
-
-@[simp] theorem forIn_some [Monad m] (a : α) (b : β) (f : α → β → m (ForInStep β)) :
-    forIn (some a) b f = bind (f a b) (fun | .done r | .yield r => pure r) := by
-  rfl
-
-@[simp] theorem forIn'_toList [Monad m] (o : Option α) (b : β) (f : (a : α) → a ∈ o.toList → β → m (ForInStep β)) :
-    forIn' o.toList b f = forIn' o b fun a m b => f a (by simpa using m) b := by
-  cases o <;> rfl
-
-@[simp] theorem forIn_toList [Monad m] (o : Option α) (b : β) (f : α → β → m (ForInStep β)) :
-    forIn o.toList b f = forIn o b f := by
-  cases o <;> rfl
-
 end Option

src/Init/Data/Repr.lean

@@ -5,6 +5,10 @@ Author: Leonardo de Moura
 -/
 prelude
 import Init.Data.Format.Basic
+import Init.Data.Int.Basic
+import Init.Data.Nat.Div
+import Init.Data.UInt.BasicAux
+import Init.Control.Id
 open Sum Subtype Nat
 
 open Std

src/Init/Data/String/Basic.lean

@@ -6,6 +6,7 @@ Author: Leonardo de Moura, Mario Carneiro
 prelude
 import Init.Data.List.Basic
 import Init.Data.Char.Basic
+import Init.Data.Option.Basic
 
 universe u
 

src/Init/Data/ToString/Basic.lean

@@ -4,9 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
+import Init.Data.String.Basic
+import Init.Data.UInt.BasicAux
+import Init.Data.Nat.Div
 import Init.Data.Repr
-import Init.Data.Option.Basic
-
+import Init.Data.Int.Basic
+import Init.Data.Format.Basic
+import Init.Control.Id
+import Init.Control.Option
 open Sum Subtype Nat
 
 open Std

src/Init/GetElem.lean

@@ -144,26 +144,22 @@ instance (priority := low) [GetElem coll idx elem valid] [∀ xs i, Decidable (v
     LawfulGetElem coll idx elem valid where
 
 theorem getElem?_pos [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
-    (c : cont) (i : idx) (h : dom c i) : c[i]? = some (c[i]'h) := by
-  have : Decidable (dom c i) := .isTrue h
+    (c : cont) (i : idx) (h : dom c i) [Decidable (dom c i)] : c[i]? = some (c[i]'h) := by
   rw [getElem?_def]
   exact dif_pos h
 
 theorem getElem?_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
-    (c : cont) (i : idx) (h : ¬dom c i) : c[i]? = none := by
-  have : Decidable (dom c i) := .isFalse h
+    (c : cont) (i : idx) (h : ¬dom c i) [Decidable (dom c i)] : c[i]? = none := by
   rw [getElem?_def]
   exact dif_neg h
 
 theorem getElem!_pos [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
-    [Inhabited elem] (c : cont) (i : idx) (h : dom c i) :
+    [Inhabited elem] (c : cont) (i : idx) (h : dom c i) [Decidable (dom c i)] :
     c[i]! = c[i]'h := by
-  have : Decidable (dom c i) := .isTrue h
   simp [getElem!_def, getElem?_def, h]
 
 theorem getElem!_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
-    [Inhabited elem] (c : cont) (i : idx) (h : ¬dom c i) : c[i]! = default := by
-  have : Decidable (dom c i) := .isFalse h
+    [Inhabited elem] (c : cont) (i : idx) (h : ¬dom c i) [Decidable (dom c i)] : c[i]! = default := by
   simp [getElem!_def, getElem?_def, h]
 
 namespace Fin
@@ -207,10 +203,6 @@ instance : GetElem (List α) Nat α fun as i => i < as.length where
 
 @[deprecated (since := "2024-06-12")] abbrev cons_getElem_succ := @getElem_cons_succ
 
-@[simp] theorem getElem_mem : ∀ {l : List α} {n} (h : n < l.length), l[n]'h ∈ l
-  | _ :: _, 0, _ => .head ..
-  | _ :: l, _+1, _ => .tail _ (getElem_mem (l := l) ..)
-
 theorem get_drop_eq_drop (as : List α) (i : Nat) (h : i < as.length) : as[i] :: as.drop (i+1) = as.drop i :=
   match as, i with
   | _::_, 0   => rfl

src/Init/System/FilePath.lean

@@ -5,6 +5,8 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
 import Init.System.Platform
+import Init.Data.String.Basic
+import Init.Data.Repr
 import Init.Data.ToString.Basic
 
 namespace System

src/Init/System/IO.lean

@@ -4,9 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Luke Nelson, Jared Roesch, Leonardo de Moura, Sebastian Ullrich, Mac Malone
 -/
 prelude
+import Init.Control.Reader
+import Init.Data.String
+import Init.Data.ByteArray
 import Init.System.IOError
 import Init.System.FilePath
 import Init.System.ST
+import Init.Data.ToString.Macro
 import Init.Data.Ord
 
 open System

src/Init/System/IOError.lean

@@ -5,7 +5,10 @@ Authors: Simon Hudon
 -/
 
 prelude
+import Init.Core
+import Init.Data.UInt.Basic
 import Init.Data.ToString.Basic
+import Init.Data.String.Basic
 
 /--
 Imitate the structure of IOErrorType in Haskell:

src/Init/Tactics.lean

@@ -495,7 +495,7 @@ macro (name := rwSeq) "rw " c:(config)? s:rwRuleSeq l:(location)? : tactic =>
     `(tactic| (rewrite $(c)? [$rs,*] $(l)?; with_annotate_state $rbrak (try (with_reducible rfl))))
   | _ => Macro.throwUnsupported
 
-/-- `rwa` is short-hand for `rw; assumption`. -/
+/-- `rwa` calls `rw`, then closes any remaining goals using `assumption`. -/
 macro "rwa " rws:rwRuleSeq loc:(location)? : tactic =>
   `(tactic| (rw $rws:rwRuleSeq $[$loc:location]?; assumption))
 

src/Lean/Compiler/LCNF/PullLetDecls.lean

@@ -46,7 +46,7 @@ partial def withCheckpoint (x : PullM Code) : PullM Code := do
     else
       return c
   let (c, keep) := go toPullSizeSaved (← read).included |>.run #[]
-  modify fun s => { s with toPull := s.toPull.take toPullSizeSaved ++ keep }
+  modify fun s => { s with toPull := s.toPull.shrink toPullSizeSaved ++ keep }
   return c
 
 def attachToPull (c : Code) : PullM Code := do

src/Lean/Declaration.lean

@@ -472,10 +472,6 @@ def isInductive : ConstantInfo → Bool
   | inductInfo _ => true
   | _            => false
 
-def isTheorem : ConstantInfo → Bool
-  | thmInfo _ => true
-  | _         => false
-
 def inductiveVal! : ConstantInfo → InductiveVal
   | .inductInfo val => val
   | _ => panic! "Expected a `ConstantInfo.inductInfo`."

src/Lean/Elab/BuiltinCommand.lean

@@ -343,7 +343,7 @@ def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do
     if let .none ← findDeclarationRangesCore? declName then
       -- this is only relevant for declarations added without a declaration range
       -- in particular `Quot.mk` et al which are added by `init_quot`
-      addDeclarationRangesFromSyntax declName stx id
+      addAuxDeclarationRanges declName stx id
     addDocString declName (← getDocStringText doc)
   | _ => throwUnsupportedSyntax
 

src/Lean/Elab/BuiltinEvalCommand.lean

@@ -84,7 +84,7 @@ private def addAndCompileExprForEval (declName : Name) (value : Expr) (allowSorr
   -- An alternative design would be to make `elabTermForEval` into a term elaborator and elaborate the command all at once
   -- with `unsafe def _eval := term_for_eval% $t`, which we did try, but unwanted error messages
   -- such as "failed to infer definition type" can surface.
-  let defView := mkDefViewOfDef { isUnsafe := true }
+  let defView := mkDefViewOfDef { isUnsafe := true, stx := ⟨.missing⟩ }
     (← `(Parser.Command.definition|
           def $(mkIdent <| `_root_ ++ declName) := $(← Term.exprToSyntax value)))
   Term.elabMutualDef #[] { header := "" } #[defView]

src/Lean/Elab/Command.lean

@@ -711,54 +711,21 @@ def addUnivLevel (idStx : Syntax) : CommandElabM Unit := withRef idStx do
   else
     modifyScope fun scope => { scope with levelNames := id :: scope.levelNames }
 
+def expandDeclId (declId : Syntax) (modifiers : Modifiers) : CommandElabM ExpandDeclIdResult := do
+  let currNamespace ← getCurrNamespace
+  let currLevelNames ← getLevelNames
+  let r ← Elab.expandDeclId currNamespace currLevelNames declId modifiers
+  for id in (← (← getScope).varDecls.flatMapM getBracketedBinderIds) do
+    if id == r.shortName then
+      throwError "invalid declaration name '{r.shortName}', there is a section variable with the same name"
+  return r
+
 end Elab.Command
 
 open Elab Command MonadRecDepth
 
-private def liftCommandElabMCore (cmd : CommandElabM α) (throwOnError : Bool) : CoreM α := do
-  let s : Core.State ← get
-  let ctx : Core.Context ← read
-  let (a, commandState) ←
-    cmd.run {
-      fileName := ctx.fileName
-      fileMap := ctx.fileMap
-      currRecDepth := ctx.currRecDepth
-      currMacroScope := ctx.currMacroScope
-      ref := ctx.ref
-      tacticCache? := none
-      snap? := none
-      cancelTk? := ctx.cancelTk?
-      suppressElabErrors := ctx.suppressElabErrors
-    } |>.run {
-      env := s.env
-      nextMacroScope := s.nextMacroScope
-      maxRecDepth := ctx.maxRecDepth
-      ngen := s.ngen
-      scopes := [{ header := "", opts := ctx.options }]
-      infoState.enabled := s.infoState.enabled
-    }
-  modify fun coreState => { coreState with
-    env := commandState.env
-    nextMacroScope := commandState.nextMacroScope
-    ngen := commandState.ngen
-    traceState.traces := coreState.traceState.traces ++ commandState.traceState.traces
-  }
-  if throwOnError then
-    if let some err := commandState.messages.toArray.find? (·.severity matches .error) then
-      throwError err.data
-  modify fun coreState => { coreState with
-    infoState.trees := coreState.infoState.trees.append commandState.infoState.trees
-    messages := coreState.messages ++ commandState.messages
-  }
-  return a
-
 /--
-Lifts an action in `CommandElabM` into `CoreM`, updating the environment,
-messages, info trees, traces, the name generator, and macro scopes.
-The action is run in a context with an empty message log, empty trace state, and empty info trees.
-
-If `throwOnError` is true, then if the command produces an error message, it is converted into an exception.
-In this case, info trees and messages are not carried over.
+Lifts an action in `CommandElabM` into `CoreM`, updating the traces and the environment.
 
 Commands that modify the processing of subsequent commands,
 such as `open` and `namespace` commands,
@@ -771,9 +738,27 @@ to reset the instance cache.
 While the `modifyEnv` function for `MetaM` clears its caches entirely,
 `liftCommandElabM` has no way to reset these caches.
 -/
-def liftCommandElabM (cmd : CommandElabM α) (throwOnError : Bool := true) : CoreM α := do
-  -- `observing` ensures that if `cmd` throws an exception we still thread state back to `CoreM`.
-  MonadExcept.ofExcept (← liftCommandElabMCore (observing cmd) throwOnError)
+def liftCommandElabM (cmd : CommandElabM α) : CoreM α := do
+  let (a, commandState) ←
+    cmd.run {
+      fileName := ← getFileName
+      fileMap := ← getFileMap
+      ref := ← getRef
+      tacticCache? := none
+      snap? := none
+      cancelTk? := (← read).cancelTk?
+    } |>.run {
+      env := ← getEnv
+      maxRecDepth := ← getMaxRecDepth
+      scopes := [{ header := "", opts := ← getOptions }]
+    }
+  modify fun coreState => { coreState with
+    traceState.traces := coreState.traceState.traces ++ commandState.traceState.traces
+    env := commandState.env
+  }
+  if let some err := commandState.messages.toArray.find? (·.severity matches .error) then
+    throwError err.data
+  pure a
 
 /--
 Given a command elaborator `cmd`, returns a new command elaborator that

src/Lean/Elab/DeclModifiers.lean

@@ -57,8 +57,7 @@ inductive RecKind where
 
 /-- Flags and data added to declarations (eg docstrings, attributes, `private`, `unsafe`, `partial`, ...). -/
 structure Modifiers where
-  /-- Input syntax, used for adjusting declaration range (unless missing) -/
-  stx             : TSyntax ``Parser.Command.declModifiers := ⟨.missing⟩
+  stx             : TSyntax ``Parser.Command.declModifiers
   docString?      : Option String := none
   visibility      : Visibility := Visibility.regular
   isNoncomputable : Bool := false

src/Lean/Elab/Declaration.lean

@@ -102,16 +102,14 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
   -- leading_parser "axiom " >> declId >> declSig
   let declId             := stx[1]
   let (binders, typeStx) := expandDeclSig stx[2]
-  runTermElabM fun vars => do
-    let scopeLevelNames ← Term.getLevelNames
-    let ⟨shortName, declName, allUserLevelNames⟩ ← Term.expandDeclId (← getCurrNamespace) scopeLevelNames declId modifiers
-    addDeclarationRangesForBuiltin declName modifiers.stx stx
-    Term.withAutoBoundImplicitForbiddenPred (fun n => shortName == n) do
+  let scopeLevelNames ← getLevelNames
+  let ⟨_, declName, allUserLevelNames⟩ ← expandDeclId declId modifiers
+  addDeclarationRanges declName modifiers.stx stx
+  runTermElabM fun vars =>
     Term.withDeclName declName <| Term.withLevelNames allUserLevelNames <| Term.elabBinders binders.getArgs fun xs => do
       Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.beforeElaboration
       let type ← Term.elabType typeStx
       Term.synthesizeSyntheticMVarsNoPostponing
-      let xs ← Term.addAutoBoundImplicits xs
       let type ← instantiateMVars type
       let type ← mkForallFVars xs type
       let type ← mkForallFVars vars type (usedOnly := true)
@@ -137,6 +135,63 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
           compileDecl decl
         Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.afterCompilation
 
+/-
+leading_parser "inductive " >> declId >> optDeclSig >> optional ("where" <|> ":=") >> many ctor
+leading_parser atomic (group ("class " >> "inductive ")) >> declId >> optDeclSig >> optional ("where" <|> ":=") >> many ctor >> optDeriving
+-/
+private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : CommandElabM InductiveView := do
+  checkValidInductiveModifier modifiers
+  let (binders, type?) := expandOptDeclSig decl[2]
+  let declId           := decl[1]
+  let ⟨name, declName, levelNames⟩ ← expandDeclId declId modifiers
+  addDeclarationRanges declName modifiers.stx decl
+  let ctors      ← decl[4].getArgs.mapM fun ctor => withRef ctor do
+    -- def ctor := leading_parser optional docComment >> "\n| " >> declModifiers >> rawIdent >> optDeclSig
+    let mut ctorModifiers ← elabModifiers ⟨ctor[2]⟩
+    if let some leadingDocComment := ctor[0].getOptional? then
+      if ctorModifiers.docString?.isSome then
+        logErrorAt leadingDocComment "duplicate doc string"
+      ctorModifiers := { ctorModifiers with docString? := TSyntax.getDocString ⟨leadingDocComment⟩ }
+    if ctorModifiers.isPrivate && modifiers.isPrivate then
+      throwError "invalid 'private' constructor in a 'private' inductive datatype"
+    if ctorModifiers.isProtected && modifiers.isPrivate then
+      throwError "invalid 'protected' constructor in a 'private' inductive datatype"
+    checkValidCtorModifier ctorModifiers
+    let ctorName := ctor.getIdAt 3
+    let ctorName := declName ++ ctorName
+    let ctorName ← withRef ctor[3] <| applyVisibility ctorModifiers.visibility ctorName
+    let (binders, type?) := expandOptDeclSig ctor[4]
+    addDocString' ctorName ctorModifiers.docString?
+    addAuxDeclarationRanges ctorName ctor ctor[3]
+    return { ref := ctor, modifiers := ctorModifiers, declName := ctorName, binders := binders, type? := type? : CtorView }
+  let computedFields ← (decl[5].getOptional?.map (·[1].getArgs) |>.getD #[]).mapM fun cf => withRef cf do
+    return { ref := cf, modifiers := cf[0], fieldId := cf[1].getId, type := ⟨cf[3]⟩, matchAlts := ⟨cf[4]⟩ }
+  let classes ← liftCoreM <| getOptDerivingClasses decl[6]
+  if decl[3][0].isToken ":=" then
+    -- https://github.com/leanprover/lean4/issues/5236
+    withRef decl[0] <| Linter.logLintIf Linter.linter.deprecated decl[3]
+      "'inductive ... :=' has been deprecated in favor of 'inductive ... where'."
+  return {
+    ref             := decl
+    shortDeclName   := name
+    derivingClasses := classes
+    declId, modifiers, declName, levelNames
+    binders, type?, ctors
+    computedFields
+  }
+
+private def classInductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : CommandElabM InductiveView :=
+  inductiveSyntaxToView modifiers decl
+
+def elabInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
+  let v ← inductiveSyntaxToView modifiers stx
+  elabInductiveViews #[v]
+
+def elabClassInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
+  let modifiers := modifiers.addAttr { name := `class }
+  let v ← classInductiveSyntaxToView modifiers stx
+  elabInductiveViews #[v]
+
 /--
 Macro that expands a declaration with a complex name into an explicit `namespace` block.
 Implementing this step as a macro means that reuse checking is handled by `elabCommand`.
@@ -175,6 +230,19 @@ def elabDeclaration : CommandElab := fun stx => do
     else
       throwError "unexpected declaration"
 
+/-- Return true if all elements of the mutual-block are inductive declarations. -/
+private def isMutualInductive (stx : Syntax) : Bool :=
+  stx[1].getArgs.all fun elem =>
+    let decl     := elem[1]
+    let declKind := decl.getKind
+    declKind == `Lean.Parser.Command.inductive
+
+private def elabMutualInductive (elems : Array Syntax) : CommandElabM Unit := do
+  let views ← elems.mapM fun stx => do
+     let modifiers ← elabModifiers ⟨stx[0]⟩
+     inductiveSyntaxToView modifiers stx[1]
+  elabInductiveViews views
+
 /-- Return true if all elements of the mutual-block are definitions/theorems/abbrevs. -/
 private def isMutualDef (stx : Syntax) : Bool :=
   stx[1].getArgs.all fun elem =>
@@ -332,7 +400,7 @@ def elabMutual : CommandElab := fun stx => do
       -- We need to add `id`'s ranges *before* elaborating `initFn` (and then `id` itself) as
       -- otherwise the info context created by `with_decl_name` will be incomplete and break the
       -- call hierarchy
-      addDeclarationRangesForBuiltin fullId ⟨defStx.raw[0]⟩ defStx.raw[1]
+      addDeclarationRanges fullId ⟨defStx.raw[0]⟩ defStx.raw[1]
       elabCommand (← `(
         $[unsafe%$unsafe?]? def initFn : IO $type := with_decl_name% $(mkIdent fullId) do $doSeq
         $defStx:command))

src/Lean/Elab/DeclarationRange.lean

@@ -49,31 +49,29 @@ def getDeclarationSelectionRef (stx : Syntax) : Syntax :=
     else
       stx[0]
 
-/--
-Derives and adds declaration ranges from given syntax trees. If `rangeStx` does not have a range,
-nothing is added. If `selectionRangeStx` does not have a range, it is defaulted to that of
-`rangeStx`.
--/
-def addDeclarationRangesFromSyntax [Monad m] [MonadEnv m] [MonadFileMap m] (declName : Name)
-    (rangeStx : Syntax) (selectionRangeStx : Syntax := .missing) : m Unit := do
-  -- may fail on partial syntax, ignore in that case
-  let some range ← getDeclarationRange? rangeStx | return
-  let selectionRange ← (·.getD range) <$> getDeclarationRange? selectionRangeStx
-  Lean.addDeclarationRanges declName { range, selectionRange }
 
 /--
 Stores the `range` and `selectionRange` for `declName` where `modsStx` is the modifier part and
 `cmdStx` the remaining part of the syntax tree for `declName`.
 
 This method is for the builtin declarations only. User-defined commands should use
-`Lean.Elab.addDeclarationRangesFromSyntax` or `Lean.addDeclarationRanges` to store this information
-for their commands.
+`Lean.addDeclarationRanges` to store this information for their commands.
 -/
-def addDeclarationRangesForBuiltin [Monad m] [MonadEnv m] [MonadFileMap m] (declName : Name)
+def addDeclarationRanges [Monad m] [MonadEnv m] [MonadFileMap m] (declName : Name)
     (modsStx : TSyntax ``Parser.Command.declModifiers) (declStx : Syntax) : m Unit := do
   if declStx.getKind == ``Parser.Command.«example» then
     return ()
   let stx := mkNullNode #[modsStx, declStx]
-  addDeclarationRangesFromSyntax declName stx (getDeclarationSelectionRef declStx)
+  -- may fail on partial syntax, ignore in that case
+  let some range ← getDeclarationRange? stx | return
+  let some selectionRange ← getDeclarationRange? (getDeclarationSelectionRef declStx) | return
+  Lean.addDeclarationRanges declName { range, selectionRange }
+
+/-- Auxiliary method for recording ranges for auxiliary declarations (e.g., fields, nested declarations, etc. -/
+def addAuxDeclarationRanges [Monad m] [MonadEnv m] [MonadFileMap m] (declName : Name) (stx : Syntax) (header : Syntax) : m Unit := do
+  -- may fail on partial syntax, ignore in that case
+  let some range ← getDeclarationRange? stx | return
+  let some selectionRange ← getDeclarationRange? header | return
+  Lean.addDeclarationRanges declName { range, selectionRange }
 
 end Lean.Elab

src/Lean/Elab/Frontend.lean

@@ -145,7 +145,7 @@ def runFrontend
     : IO (Environment × Bool) := do
   let startTime := (← IO.monoNanosNow).toFloat / 1000000000
   let inputCtx := Parser.mkInputContext input fileName
-  let opts := Language.Lean.internal.cmdlineSnapshots.setIfNotSet opts true
+  let opts := Language.Lean.internal.cmdlineSnapshots.set opts true
   let ctx := { inputCtx with }
   let processor := Language.Lean.process
   let snap ← processor (fun _ => pure <| .ok { mainModuleName, opts, trustLevel }) none ctx

src/Lean/Elab/Inductive.lean

@@ -18,7 +18,6 @@ import Lean.Elab.ComputedFields
 import Lean.Elab.DefView
 import Lean.Elab.DeclUtil
 import Lean.Elab.Deriving.Basic
-import Lean.Elab.DeclarationRange
 
 namespace Lean.Elab.Command
 open Meta
@@ -80,56 +79,10 @@ structure ElabHeaderResult where
   view       : InductiveView
   lctx       : LocalContext
   localInsts : LocalInstances
-  levelNames : List Name
   params     : Array Expr
   type       : Expr
   deriving Inhabited
 
-/-
-leading_parser "inductive " >> declId >> optDeclSig >> optional ("where" <|> ":=") >> many ctor
-leading_parser atomic (group ("class " >> "inductive ")) >> declId >> optDeclSig >> optional ("where" <|> ":=") >> many ctor >> optDeriving
--/
-private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : TermElabM InductiveView := do
-  checkValidInductiveModifier modifiers
-  let (binders, type?) := expandOptDeclSig decl[2]
-  let declId           := decl[1]
-  let ⟨name, declName, levelNames⟩ ← Term.expandDeclId (← getCurrNamespace) (← Term.getLevelNames) declId modifiers
-  addDeclarationRangesForBuiltin declName modifiers.stx decl
-  let ctors      ← decl[4].getArgs.mapM fun ctor => withRef ctor do
-    -- def ctor := leading_parser optional docComment >> "\n| " >> declModifiers >> rawIdent >> optDeclSig
-    let mut ctorModifiers ← elabModifiers ⟨ctor[2]⟩
-    if let some leadingDocComment := ctor[0].getOptional? then
-      if ctorModifiers.docString?.isSome then
-        logErrorAt leadingDocComment "duplicate doc string"
-      ctorModifiers := { ctorModifiers with docString? := TSyntax.getDocString ⟨leadingDocComment⟩ }
-    if ctorModifiers.isPrivate && modifiers.isPrivate then
-      throwError "invalid 'private' constructor in a 'private' inductive datatype"
-    if ctorModifiers.isProtected && modifiers.isPrivate then
-      throwError "invalid 'protected' constructor in a 'private' inductive datatype"
-    checkValidCtorModifier ctorModifiers
-    let ctorName := ctor.getIdAt 3
-    let ctorName := declName ++ ctorName
-    let ctorName ← withRef ctor[3] <| applyVisibility ctorModifiers.visibility ctorName
-    let (binders, type?) := expandOptDeclSig ctor[4]
-    addDocString' ctorName ctorModifiers.docString?
-    addDeclarationRangesFromSyntax ctorName ctor ctor[3]
-    return { ref := ctor, modifiers := ctorModifiers, declName := ctorName, binders := binders, type? := type? : CtorView }
-  let computedFields ← (decl[5].getOptional?.map (·[1].getArgs) |>.getD #[]).mapM fun cf => withRef cf do
-    return { ref := cf, modifiers := cf[0], fieldId := cf[1].getId, type := ⟨cf[3]⟩, matchAlts := ⟨cf[4]⟩ }
-  let classes ← getOptDerivingClasses decl[6]
-  if decl[3][0].isToken ":=" then
-    -- https://github.com/leanprover/lean4/issues/5236
-    withRef decl[0] <| Linter.logLintIf Linter.linter.deprecated decl[3]
-      "'inductive ... :=' has been deprecated in favor of 'inductive ... where'."
-  return {
-    ref             := decl
-    shortDeclName   := name
-    derivingClasses := classes
-    declId, modifiers, declName, levelNames
-    binders, type?, ctors
-    computedFields
-  }
-
 private partial def elabHeaderAux (views : Array InductiveView) (i : Nat) (acc : Array ElabHeaderResult) : TermElabM (Array ElabHeaderResult) :=
   Term.withAutoBoundImplicitForbiddenPred (fun n => views.any (·.shortDeclName == n)) do
     if h : i < views.size then
@@ -141,8 +94,7 @@ private partial def elabHeaderAux (views : Array InductiveView) (i : Nat) (acc :
           let type := mkSort u
           Term.synthesizeSyntheticMVarsNoPostponing
           Term.addAutoBoundImplicits' params type fun params type => do
-            let levelNames ← Term.getLevelNames
-            return acc.push { lctx := (← getLCtx), localInsts := (← getLocalInstances), levelNames, params, type, view }
+            return acc.push { lctx := (← getLCtx), localInsts := (← getLocalInstances), params, type, view }
         | some typeStx =>
           let (type, _) ← Term.withAutoBoundImplicit do
             let type ← Term.elabType typeStx
@@ -153,8 +105,7 @@ private partial def elabHeaderAux (views : Array InductiveView) (i : Nat) (acc :
             return (← mkForallFVars indices type, indices.size)
           Term.addAutoBoundImplicits' params type fun params type => do
             trace[Elab.inductive] "header params: {params}, type: {type}"
-            let levelNames ← Term.getLevelNames
-            return acc.push { lctx := (← getLCtx), localInsts := (← getLocalInstances), levelNames, params, type, view }
+            return acc.push { lctx := (← getLCtx), localInsts := (← getLocalInstances), params, type, view }
       elabHeaderAux views (i+1) acc
     else
       return acc
@@ -172,20 +123,13 @@ private def checkUnsafe (rs : Array ElabHeaderResult) : TermElabM Unit := do
     unless r.view.modifiers.isUnsafe == isUnsafe do
       throwErrorAt r.view.ref "invalid inductive type, cannot mix unsafe and safe declarations in a mutually inductive datatypes"
 
-private def InductiveView.checkLevelNames (views : Array InductiveView) : TermElabM Unit := do
+private def checkLevelNames (views : Array InductiveView) : TermElabM Unit := do
   if views.size > 1 then
     let levelNames := views[0]!.levelNames
     for view in views do
       unless view.levelNames == levelNames do
         throwErrorAt view.ref "invalid inductive type, universe parameters mismatch in mutually inductive datatypes"
 
-private def ElabHeaderResult.checkLevelNames (rs : Array ElabHeaderResult) : TermElabM Unit := do
-  if rs.size > 1 then
-    let levelNames := rs[0]!.levelNames
-    for r in rs do
-      unless r.levelNames == levelNames do
-        throwErrorAt r.view.ref "invalid inductive type, universe parameters mismatch in mutually inductive datatypes"
-
 private def mkTypeFor (r : ElabHeaderResult) : TermElabM Expr := do
   withLCtx r.lctx r.localInsts do
     mkForallFVars r.params r.type
@@ -847,15 +791,12 @@ private partial def fixedIndicesToParams (numParams : Nat) (indTypes : Array Ind
 private def mkInductiveDecl (vars : Array Expr) (views : Array InductiveView) : TermElabM Unit := Term.withoutSavingRecAppSyntax do
   let view0 := views[0]!
   let scopeLevelNames ← Term.getLevelNames
-  InductiveView.checkLevelNames views
+  checkLevelNames views
   let allUserLevelNames := view0.levelNames
   let isUnsafe          := view0.modifiers.isUnsafe
   withRef view0.ref <| Term.withLevelNames allUserLevelNames do
     let rs ← elabHeader views
     Term.synthesizeSyntheticMVarsNoPostponing
-    ElabHeaderResult.checkLevelNames rs
-    let allUserLevelNames := rs[0]!.levelNames
-    trace[Elab.inductive] "level names: {allUserLevelNames}"
     withInductiveLocalDecls rs fun params indFVars => do
       trace[Elab.inductive] "indFVars: {indFVars}"
       let mut indTypesArray := #[]
@@ -947,55 +888,19 @@ private def applyComputedFields (indViews : Array InductiveView) : CommandElabM
   liftTermElabM do Term.withDeclName indViews[0]!.declName do
     ComputedFields.setComputedFields computedFields
 
-def elabInductiveViews (vars : Array Expr) (views : Array InductiveView) : TermElabM Unit := do
+def elabInductiveViews (views : Array InductiveView) : CommandElabM Unit := do
   let view0 := views[0]!
   let ref := view0.ref
-  Term.withDeclName view0.declName do withRef ref do
+  runTermElabM fun vars => Term.withDeclName view0.declName do withRef ref do
     mkInductiveDecl vars views
     mkSizeOfInstances view0.declName
     Lean.Meta.IndPredBelow.mkBelow view0.declName
     for view in views do
       mkInjectiveTheorems view.declName
-
-def elabInductiveViewsPostprocessing (views : Array InductiveView) : CommandElabM Unit := do
-  let view0 := views[0]!
-  let ref := view0.ref
   applyComputedFields views -- NOTE: any generated code before this line is invalid
   applyDerivingHandlers views
   runTermElabM fun _ => Term.withDeclName view0.declName do withRef ref do
     for view in views do
       Term.applyAttributesAt view.declName view.modifiers.attrs .afterCompilation
 
-def elabInductives (inductives : Array (Modifiers × Syntax)) : CommandElabM Unit := do
-  let vs ← runTermElabM fun vars => do
-    let vs ← inductives.mapM fun (modifiers, stx) => inductiveSyntaxToView modifiers stx
-    elabInductiveViews vars vs
-    pure vs
-  elabInductiveViewsPostprocessing vs
-
-def elabInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
-  elabInductives #[(modifiers, stx)]
-
-def elabClassInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
-  let modifiers := modifiers.addAttr { name := `class }
-  elabInductive modifiers stx
-
-/--
-Returns true if all elements of the `mutual` block (`Lean.Parser.Command.mutual`) are inductive declarations.
--/
-def isMutualInductive (stx : Syntax) : Bool :=
-  stx[1].getArgs.all fun elem =>
-    let decl     := elem[1]
-    let declKind := decl.getKind
-    declKind == `Lean.Parser.Command.inductive
-
-/--
-Elaborates a `mutual` block satisfying `Lean.Elab.Command.isMutualInductive`.
--/
-def elabMutualInductive (elems : Array Syntax) : CommandElabM Unit := do
-  let inductives ← elems.mapM fun stx => do
-    let modifiers ← elabModifiers ⟨stx[0]⟩
-    pure (modifiers, stx[1])
-  elabInductives inductives
-
 end Lean.Elab.Command

src/Lean/Elab/LetRec.lean

@@ -51,7 +51,7 @@ private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do
       checkNotAlreadyDeclared declName
       applyAttributesAt declName attrs AttributeApplicationTime.beforeElaboration
       addDocString' declName docStr?
-      addDeclarationRangesFromSyntax declName decl declId
+      addAuxDeclarationRanges declName decl declId
       let binders := decl[1].getArgs
       let typeStx := expandOptType declId decl[2]
       let (type, binderIds) ← elabBindersEx binders fun xs => do

src/Lean/Elab/MutualDef.lean

@@ -887,6 +887,7 @@ def getKindForLetRecs (mainHeaders : Array DefViewElabHeader) : DefKind :=
   else DefKind.«def»
 
 def getModifiersForLetRecs (mainHeaders : Array DefViewElabHeader) : Modifiers := {
+  stx             := ⟨mkNullNode #[]⟩  -- ignore when computing declaration range
   isNoncomputable := mainHeaders.any fun h => h.modifiers.isNoncomputable
   recKind         := if mainHeaders.any fun h => h.modifiers.isPartial then RecKind.partial else RecKind.default
   isUnsafe        := mainHeaders.any fun h => h.modifiers.isUnsafe
@@ -997,7 +998,7 @@ where
       for view in views, header in headers do
         -- NOTE: this should be the full `ref`, and thus needs to be done after any snapshotting
         -- that depends only on a part of the ref
-        addDeclarationRangesForBuiltin header.declName view.modifiers.stx view.ref
+        addDeclarationRanges header.declName view.modifiers.stx view.ref
 
 
   processDeriving (headers : Array DefViewElabHeader) := do

src/Lean/Elab/ParseImportsFast.lean

@@ -182,7 +182,7 @@ partial def moduleIdent (runtimeOnly : Bool) : Parser := fun input s =>
   let s := p input s
   match s.error? with
   | none => many p input s
-  | some _ => { pos, error? := none, imports := s.imports.take size }
+  | some _ => { pos, error? := none, imports := s.imports.shrink size }
 
 @[inline] partial def preludeOpt (k : String) : Parser :=
   keywordCore k (fun _ s => s.pushModule `Init false) (fun _ s => s)

src/Lean/Elab/PreDefinition/MkInhabitant.lean

@@ -5,24 +5,9 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Meta.AppBuilder
-import Lean.PrettyPrinter
 namespace Lean.Elab
 open Meta
 
-private def withInhabitedInstances (xs : Array Expr) (k : Array Expr → MetaM α) : MetaM α := do
-  let rec go (i : Nat) (insts : Array Expr) : MetaM α := do
-    if h : i < xs.size then
-      let x := xs[i]
-      let xTy ← inferType x
-      let u ← getLevel xTy
-      let instTy := mkApp (.const ``Inhabited [u]) xTy
-      let instVal := mkApp2 (.const ``Inhabited.mk [u]) xTy x
-      withLetDecl `inst instTy instVal fun inst =>
-        go (i + 1) (insts.push inst)
-    else
-      k insts
-  go 0 #[]
-
 private def mkInhabitant? (type : Expr) (useOfNonempty : Bool) : MetaM (Option Expr) := do
   try
     if useOfNonempty then
@@ -32,41 +17,36 @@ private def mkInhabitant? (type : Expr) (useOfNonempty : Bool) : MetaM (Option E
   catch _ =>
     return none
 
-/--
-Find an inhabitant while doing delta unfolding.
--/
-private partial def mkInhabitantForAux? (xs insts : Array Expr) (type : Expr) (useOfNonempty : Bool) : MetaM (Option Expr) := withIncRecDepth do
-  if let some val ← mkInhabitant? type useOfNonempty then
-    mkLambdaFVars xs (← mkLetFVars (usedLetOnly := true) insts val)
-  else
-    let type ← whnfCore type
-    if type.isForall then
-      forallTelescope type fun xs' type' =>
-        withInhabitedInstances xs' fun insts' =>
-          mkInhabitantForAux? (xs ++ xs') (insts ++ insts') type' useOfNonempty
-    else if let some type' ← unfoldDefinition? type then
-      mkInhabitantForAux? xs insts type' useOfNonempty
-    else
-      return none
+private def findAssumption? (xs : Array Expr) (type : Expr) : MetaM (Option Expr) := do
+  xs.findM? fun x => do isDefEq (← inferType x) type
+
+private def mkFnInhabitant? (xs : Array Expr) (type : Expr) (useOfNonempty : Bool) : MetaM (Option Expr) :=
+  let rec loop
+    | 0,   type => mkInhabitant? type useOfNonempty
+    | i+1, type => do
+      let x := xs[i]!
+      let type ← mkForallFVars #[x] type;
+      match (← mkInhabitant? type useOfNonempty) with
+      | none     => loop i type
+      | some val => return some (← mkLambdaFVars xs[0:i] val)
+  loop xs.size type
 
 /- TODO: add a global IO.Ref to let users customize/extend this procedure -/
-def mkInhabitantFor (declName : Name) (xs : Array Expr) (type : Expr) : MetaM Expr :=
-  withInhabitedInstances xs fun insts => do
-    if let some val ← mkInhabitantForAux? xs insts type false <||> mkInhabitantForAux? xs insts type true then
-      return val
-    else
-      throwError "\
-        failed to compile 'partial' definition '{declName}', could not prove that the type\
-        {indentExpr (← mkForallFVars xs type)}\n\
-        is nonempty.\n\
-        \n\
-        This process uses multiple strategies:\n\
-        - It looks for a parameter that matches the return type.\n\
-        - It tries synthesizing '{MessageData.ofConstName ``Inhabited}' and '{MessageData.ofConstName ``Nonempty}' \
-          instances for the return type, while making every parameter into a local '{MessageData.ofConstName ``Inhabited}' instance.\n\
-        - It tries unfolding the return type.\n\
-        \n\
-        If the return type is defined using the 'structure' or 'inductive' command, \
-        you can try adding a 'deriving Nonempty' clause to it."
+def mkInhabitantFor (declName : Name) (xs : Array Expr) (type : Expr) : MetaM Expr := do
+  let go? (useOfNonempty : Bool) : MetaM (Option Expr) := do
+    match (← mkInhabitant? type useOfNonempty) with
+    | some val => mkLambdaFVars xs val
+    | none     =>
+    match (← findAssumption? xs type) with
+    | some x => mkLambdaFVars xs x
+    | none   =>
+    match (← mkFnInhabitant? xs type useOfNonempty) with
+    | some val => return val
+    | none     => return none
+  match (← go? false) with
+  | some val => return val
+  | none     => match (← go? true) with
+    | some val => return val
+    | none     => throwError "failed to compile partial definition '{declName}', failed to show that type is inhabited and non empty"
 
 end Lean.Elab

src/Lean/Elab/StructInst.lean

@@ -826,22 +826,9 @@ def mkDefaultValue? (struct : Struct) (cinfo : ConstantInfo) : TermElabM (Option
 /-- Reduce default value. It performs beta reduction and projections of the given structures. -/
 partial def reduce (structNames : Array Name) (e : Expr) : MetaM Expr := do
   match e with
+  | .lam ..       => lambdaLetTelescope e fun xs b => do mkLambdaFVars xs (← reduce structNames b)
   | .forallE ..   => forallTelescope e fun xs b => do mkForallFVars xs (← reduce structNames b)
-  | .lam ..
-  | .letE ..      => lambdaLetTelescope e fun xs b => do
-    /- The bodies of let-declarations also need to be reduced.
-       Otherwise, some metavariables may be kept in the terms, leading to errors
-       when trying to generate default values.
-       Fixes `#3146`
-    -/
-    let localInsts ← Meta.getLocalInstances
-    let mut lctx ← getLCtx
-    for e in xs do
-      let some lcdl := lctx.findFVar? e | unreachable!
-      let some value := lcdl.value? | continue
-      let value ← Meta.withLCtx lctx localInsts (reduce structNames value)
-      lctx := lctx.modifyLocalDecl e.fvarId! (·.setValue value)
-    Meta.withLCtx lctx localInsts (mkLetFVars xs (← reduce structNames b))
+  | .letE ..      => lambdaLetTelescope e fun xs b => do mkLetFVars xs (← reduce structNames b)
   | .proj _ i b   =>
     match (← Meta.project? b i) with
     | some r => reduce structNames r

src/Lean/Elab/Structure.lean

@@ -94,7 +94,7 @@ private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (struc
   let useDefault := do
     let declName := structDeclName ++ defaultCtorName
     let ref := structStx[1].mkSynthetic
-    addDeclarationRangesFromSyntax declName ref
+    addAuxDeclarationRanges declName ref ref
     pure { ref, modifiers := default, name := defaultCtorName, declName }
   if structStx[5].isNone then
     useDefault
@@ -115,7 +115,7 @@ private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (struc
       let declName := structDeclName ++ name
       let declName ← applyVisibility ctorModifiers.visibility declName
       addDocString' declName ctorModifiers.docString?
-      addDeclarationRangesFromSyntax declName ctor[1]
+      addAuxDeclarationRanges declName ctor[1] ctor[1]
       pure { ref := ctor[1], name, modifiers := ctorModifiers, declName }
 
 def checkValidFieldModifier (modifiers : Modifiers) : TermElabM Unit := do
@@ -815,7 +815,7 @@ private def elabStructureView (view : StructView) : TermElabM Unit := do
   view.fields.forM fun field => do
     if field.declName == view.ctor.declName then
       throwErrorAt field.ref "invalid field name '{field.name}', it is equal to structure constructor name"
-    addDeclarationRangesFromSyntax field.declName field.ref
+    addAuxDeclarationRanges field.declName field.ref field.ref
   let type ← Term.elabType view.type
   unless validStructType type do throwErrorAt view.type "expected Type"
   withRef view.ref do
@@ -912,7 +912,7 @@ def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
       let scopeLevelNames ← Term.getLevelNames
       let ⟨name, declName, allUserLevelNames⟩ ← Elab.expandDeclId (← getCurrNamespace) scopeLevelNames declId modifiers
       Term.withAutoBoundImplicitForbiddenPred (fun n => name == n) do
-        addDeclarationRangesForBuiltin declName modifiers.stx stx
+        addDeclarationRanges declName modifiers.stx stx
         Term.withDeclName declName do
           let ctor ← expandCtor stx modifiers declName
           let fields ← expandFields stx modifiers declName

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

@@ -29,7 +29,6 @@ instance : ToExpr BVBinOp where
     | .mul => mkConst ``BVBinOp.mul
     | .udiv => mkConst ``BVBinOp.udiv
     | .umod => mkConst ``BVBinOp.umod
-    | .sdiv => mkConst ``BVBinOp.sdiv
   toTypeExpr := mkConst ``BVBinOp
 
 instance : ToExpr BVUnOp where

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

@@ -102,8 +102,6 @@ where
       binaryReflection lhsExpr rhsExpr .udiv ``Std.Tactic.BVDecide.Reflect.BitVec.udiv_congr
     | HMod.hMod _ _ _ _ lhsExpr rhsExpr =>
       binaryReflection lhsExpr rhsExpr .umod ``Std.Tactic.BVDecide.Reflect.BitVec.umod_congr
-    | BitVec.sdiv _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .sdiv ``Std.Tactic.BVDecide.Reflect.BitVec.sdiv_congr
     | Complement.complement _ _ innerExpr =>
       unaryReflection innerExpr .not ``Std.Tactic.BVDecide.Reflect.BitVec.not_congr
     | HShiftLeft.hShiftLeft _ β _ _ innerExpr distanceExpr =>

src/Lean/Elab/Tactic/Conv/Unfold.lean

@@ -12,16 +12,13 @@ open Meta
 
 @[builtin_tactic Lean.Parser.Tactic.Conv.unfold] def evalUnfold : Tactic := fun stx => withMainContext do
   for declNameId in stx[1].getArgs do
-    withRef declNameId do
-      let e ← elabTermForApply declNameId (mayPostpone := false)
-      match e with
-      | .const declName _ =>
-        applySimpResult (← unfold (← getLhs) declName)
-      | .fvar declFVarId =>
-        unless ← declFVarId.isLetVar do
-          throwError "conv tactic 'unfold' failed, local variable '{Expr.fvar declFVarId}' has no definition"
-        let lhs ← instantiateMVars (← getLhs)
-        changeLhs (← Meta.zetaDeltaFVars lhs #[declFVarId])
-      | _ => throwError "conv tactic 'unfold' failed, expression {e} is not a global or local constant"
+    let e ← elabTermForApply declNameId (mayPostpone := false)
+    match e with
+    | .const declName _ =>
+      applySimpResult (← unfold (← getLhs) declName)
+    | .fvar declFVarId =>
+      let lhs ← instantiateMVars (← getLhs)
+      changeLhs (← Meta.zetaDeltaFVars lhs #[declFVarId])
+    | _ => throwErrorAt declNameId m!"'unfold' conv tactic failed, expression {e} is not a global or local constant"
 
 end Lean.Elab.Tactic.Conv

src/Lean/Elab/Tactic/Ext.lean

@@ -123,7 +123,7 @@ def realizeExtTheorem (structName : Name) (flat : Bool) : Elab.Command.CommandEl
           levelParams := info.levelParams
         }
         modifyEnv fun env => addProtected env extName
-        addDeclarationRangesFromSyntax extName (← getRef)
+        addAuxDeclarationRanges extName (← getRef) (← getRef)
     catch e =>
       throwError m!"\
         Failed to generate an 'ext' theorem for '{MessageData.ofConstName structName}': {e.toMessageData}"
@@ -161,7 +161,7 @@ def realizeExtIffTheorem (extName : Name) : Elab.Command.CommandElabM Name := do
         -- Only declarations in a namespace can be protected:
         unless extIffName.isAtomic do
           modifyEnv fun env => addProtected env extIffName
-        addDeclarationRangesFromSyntax extName (← getRef)
+        addAuxDeclarationRanges extName (← getRef) (← getRef)
     catch e =>
       throwError m!"\
         Failed to generate an 'ext_iff' theorem from '{MessageData.ofConstName extName}': {e.toMessageData}\n\

src/Lean/Elab/Tactic/Unfold.lean

@@ -29,15 +29,13 @@ def zetaDeltaTarget (declFVarId : FVarId) : TacticM Unit := do
   for declNameId in stx[1].getArgs do
     go declNameId loc
 where
-  go (declNameId : Syntax) (loc : Location) : TacticM Unit := withMainContext <| withRef declNameId do
+  go (declNameId : Syntax) (loc : Location) : TacticM Unit := withMainContext do
     let e ← elabTermForApply declNameId (mayPostpone := false)
     match e with
     | .const declName _ =>
       withLocation loc (unfoldLocalDecl declName) (unfoldTarget declName) (throwTacticEx `unfold · m!"did not unfold '{declName}'")
     | .fvar declFVarId =>
-      unless ← declFVarId.isLetVar do
-        throwError "tactic 'unfold' failed, local variable '{Expr.fvar declFVarId}' has no definition"
       withLocation loc (zetaDeltaLocalDecl declFVarId) (zetaDeltaTarget declFVarId) (throwTacticEx `unfold · m!"did not unfold '{e}'")
-    | _ => throwTacticEx `unfold (← getMainGoal) m!"expression {e} is not a global or local constant"
+    | _ => withRef declNameId <| throwTacticEx `unfold (← getMainGoal) m!"expression {e} is not a global or local constant"
 
 end Lean.Elab.Tactic

src/Lean/Language/Lean.lean

@@ -300,9 +300,7 @@ General notes:
 * We must make sure to trigger `oldCancelTk?` as soon as discarding `old?`.
 * Control flow up to finding the last still-valid snapshot (which should be quick) is synchronous so
   as not to report this "fast forwarding" to the user as well as to make sure the next run sees all
-  fast-forwarded snapshots without having to wait on tasks. It also ensures this part cannot be
-  delayed by threadpool starvation. We track whether we are still on the fast-forwarding path using
-  the `sync` parameter on `parseCmd` and spawn an elaboration task when we leave it.
+  fast-forwarded snapshots without having to wait on tasks.
 -/
 partial def process
     (setupImports : Syntax → ProcessingT IO (Except HeaderProcessedSnapshot SetupImportsResult))
@@ -332,7 +330,7 @@ where
                 -- elaboration reuse
                 oldProcSuccess.firstCmdSnap.bindIO (sync := true) fun oldCmd => do
                   let prom ← IO.Promise.new
-                  parseCmd oldCmd newParserState oldProcSuccess.cmdState prom (sync := true) ctx
+                  let _ ← IO.asTask (parseCmd oldCmd newParserState oldProcSuccess.cmdState prom ctx)
                   return .pure {
                     diagnostics := oldProcessed.diagnostics
                     result? := some {
@@ -448,7 +446,7 @@ where
       let parserState := Runtime.markPersistent parserState
       let cmdState := Runtime.markPersistent cmdState
       let ctx := Runtime.markPersistent ctx
-      parseCmd none parserState cmdState prom (sync := true) ctx
+      let _ ← IO.asTask (parseCmd none parserState cmdState prom ctx)
       return {
         diagnostics
         infoTree? := cmdState.infoState.trees[0]!
@@ -459,10 +457,24 @@ where
       }
 
   parseCmd (old? : Option CommandParsedSnapshot) (parserState : Parser.ModuleParserState)
-      (cmdState : Command.State) (prom : IO.Promise CommandParsedSnapshot) (sync : Bool) :
+      (cmdState : Command.State) (prom : IO.Promise CommandParsedSnapshot) :
       LeanProcessingM Unit := do
     let ctx ← read
 
+    -- check for cancellation, most likely during elaboration of previous command, before starting
+    -- processing of next command
+    if (← ctx.newCancelTk.isSet) then
+      -- this is a bit ugly as we don't want to adjust our API with `Option`s just for cancellation
+      -- (as no-one should look at this result in that case) but anything containing `Environment`
+      -- is not `Inhabited`
+      prom.resolve <| .mk (nextCmdSnap? := none) {
+        diagnostics := .empty, stx := .missing, parserState
+        elabSnap := .pure <| .ofTyped { diagnostics := .empty : SnapshotLeaf }
+        finishedSnap := .pure { diagnostics := .empty, cmdState }
+        tacticCache := (← IO.mkRef {})
+      }
+      return
+
     let unchanged old newParserState : BaseIO Unit :=
       -- when syntax is unchanged, reuse command processing task as is
       -- NOTE: even if the syntax tree is functionally unchanged, the new parser state may still
@@ -470,11 +482,11 @@ where
       -- from `old`
       if let some oldNext := old.nextCmdSnap? then do
         let newProm ← IO.Promise.new
-        let _ ← old.data.finishedSnap.bindIO (sync := true) fun oldFinished =>
+        let _ ← old.data.finishedSnap.bindIO fun oldFinished =>
           -- also wait on old command parse snapshot as parsing is cheap and may allow for
           -- elaboration reuse
           oldNext.bindIO (sync := true) fun oldNext => do
-            parseCmd oldNext newParserState oldFinished.cmdState newProm sync ctx
+            parseCmd oldNext newParserState oldFinished.cmdState newProm ctx
             return .pure ()
         prom.resolve <| .mk (data := old.data) (nextCmdSnap? := some { range? := none, task := newProm.result })
       else prom.resolve old  -- terminal command, we're done!
@@ -509,61 +521,44 @@ where
       if let some tk := ctx.oldCancelTk? then
         tk.set
 
-    -- check for cancellation, most likely during elaboration of previous command, before starting
-    -- processing of next command
-    if (← ctx.newCancelTk.isSet) then
-      -- this is a bit ugly as we don't want to adjust our API with `Option`s just for cancellation
-      -- (as no-one should look at this result in that case) but anything containing `Environment`
-      -- is not `Inhabited`
-      prom.resolve <| .mk (nextCmdSnap? := none) {
-        diagnostics := .empty, stx := .missing, parserState
-        elabSnap := .pure <| .ofTyped { diagnostics := .empty : SnapshotLeaf }
-        finishedSnap := .pure { diagnostics := .empty, cmdState }
-        tacticCache := (← IO.mkRef {})
-      }
-      return
+    -- definitely resolved in `doElab` task
+    let elabPromise ← IO.Promise.new
+    let finishedPromise ← IO.Promise.new
+    -- (Try to) use last line of command as range for final snapshot task. This ensures we do not
+    -- retract the progress bar to a previous position in case the command support incremental
+    -- reporting but has significant work after resolving its last incremental promise, such as
+    -- final type checking; if it does not support incrementality, `elabSnap` constructed in
+    -- `parseCmd` and containing the entire range of the command will determine the reported
+    -- progress and be resolved effectively at the same time as this snapshot task, so `tailPos` is
+    -- irrelevant in this case.
+    let endRange? := stx.getTailPos?.map fun pos => ⟨pos, pos⟩
+    let finishedSnap := { range? := endRange?, task := finishedPromise.result }
+    let tacticCache ← old?.map (·.data.tacticCache) |>.getDM (IO.mkRef {})
 
-    -- Start new task when leaving fast-forwarding path; see "General notes" above
-    let _ ← (if sync then BaseIO.asTask else (.pure <$> ·)) do
-      -- definitely resolved in `doElab` task
-      let elabPromise ← IO.Promise.new
-      let finishedPromise ← IO.Promise.new
-      -- (Try to) use last line of command as range for final snapshot task. This ensures we do not
-      -- retract the progress bar to a previous position in case the command support incremental
-      -- reporting but has significant work after resolving its last incremental promise, such as
-      -- final type checking; if it does not support incrementality, `elabSnap` constructed in
-      -- `parseCmd` and containing the entire range of the command will determine the reported
-      -- progress and be resolved effectively at the same time as this snapshot task, so `tailPos` is
-      -- irrelevant in this case.
-      let endRange? := stx.getTailPos?.map fun pos => ⟨pos, pos⟩
-      let finishedSnap := { range? := endRange?, task := finishedPromise.result }
-      let tacticCache ← old?.map (·.data.tacticCache) |>.getDM (IO.mkRef {})
-
-      let minimalSnapshots := internal.cmdlineSnapshots.get cmdState.scopes.head!.opts
-      let next? ← if Parser.isTerminalCommand stx then pure none
-        -- for now, wait on "command finished" snapshot before parsing next command
-        else some <$> IO.Promise.new
-      let diagnostics ← Snapshot.Diagnostics.ofMessageLog msgLog
-      let data := if minimalSnapshots && !Parser.isTerminalCommand stx then {
-        diagnostics
-        stx := .missing
-        parserState := {}
-        elabSnap := { range? := stx.getRange?, task := elabPromise.result }
-        finishedSnap
-        tacticCache
-      } else {
-        diagnostics, stx, parserState, tacticCache
-        elabSnap := { range? := stx.getRange?, task := elabPromise.result }
-        finishedSnap
-      }
-      prom.resolve <| .mk (nextCmdSnap? := next?.map
-        ({ range? := some ⟨parserState.pos, ctx.input.endPos⟩, task := ·.result })) data
-      let cmdState ← doElab stx cmdState beginPos
-        { old? := old?.map fun old => ⟨old.data.stx, old.data.elabSnap⟩, new := elabPromise }
-        finishedPromise tacticCache ctx
-      if let some next := next? then
-        -- We're definitely off the fast-forwarding path now
-        parseCmd none parserState cmdState next (sync := false) ctx
+    let minimalSnapshots := internal.cmdlineSnapshots.get cmdState.scopes.head!.opts
+    let next? ← if Parser.isTerminalCommand stx then pure none
+      -- for now, wait on "command finished" snapshot before parsing next command
+      else some <$> IO.Promise.new
+    let diagnostics ← Snapshot.Diagnostics.ofMessageLog msgLog
+    let data := if minimalSnapshots && !Parser.isTerminalCommand stx then {
+      diagnostics
+      stx := .missing
+      parserState := {}
+      elabSnap := { range? := stx.getRange?, task := elabPromise.result }
+      finishedSnap
+      tacticCache
+    } else {
+      diagnostics, stx, parserState, tacticCache
+      elabSnap := { range? := stx.getRange?, task := elabPromise.result }
+      finishedSnap
+    }
+    prom.resolve <| .mk (nextCmdSnap? := next?.map
+      ({ range? := some ⟨parserState.pos, ctx.input.endPos⟩, task := ·.result })) data
+    let cmdState ← doElab stx cmdState beginPos
+      { old? := old?.map fun old => ⟨old.data.stx, old.data.elabSnap⟩, new := elabPromise }
+      finishedPromise tacticCache ctx
+    if let some next := next? then
+      parseCmd none parserState cmdState next ctx
 
   doElab (stx : Syntax) (cmdState : Command.State) (beginPos : String.Pos)
       (snap : SnapshotBundle DynamicSnapshot) (finishedPromise : IO.Promise CommandFinishedSnapshot)
@@ -630,7 +625,7 @@ def processCommands (inputCtx : Parser.InputContext) (parserState : Parser.Modul
     (old? : Option (Parser.InputContext × CommandParsedSnapshot) := none) :
     BaseIO (Task CommandParsedSnapshot) := do
   let prom ← IO.Promise.new
-  process.parseCmd (old?.map (·.2)) parserState commandState prom (sync := true)
+  process.parseCmd (old?.map (·.2)) parserState commandState prom
     |>.run (old?.map (·.1))
     |>.run { inputCtx with }
   return prom.result

src/Lean/Meta/AppBuilder.lean

@@ -28,7 +28,6 @@ def mkExpectedTypeHint (e : Expr) (expectedType : Expr) : MetaM Expr := do
 /--
 `mkLetFun x v e` creates the encoding for the `let_fun x := v; e` expression.
 The expression `x` can either be a free variable or a metavariable, and the function suitably abstracts `x` in `e`.
-NB: `x` must not be a let-bound free variable.
 -/
 def mkLetFun (x : Expr) (v : Expr) (e : Expr) : MetaM Expr := do
   let f ← mkLambdaFVars #[x] e

src/Lean/Meta/LitValues.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Meta.Basic
-import Init.Control.Option
 
 namespace Lean.Meta
 

src/Lean/Meta/Offset.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Control.Option
 import Lean.Data.LBool
 import Lean.Meta.InferType
 import Lean.Meta.NatInstTesters

src/Lean/Meta/Tactic/FunInd.lean

@@ -262,8 +262,8 @@ partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option E
     if let some (n, t, v, b) := e.letFun? then
       let t' ← foldAndCollect oldIH newIH isRecCall t
       let v' ← foldAndCollect oldIH newIH isRecCall v
-      return ← withLocalDeclD n t' fun x => do
-        M.localMapM (mkLetFun x v' ·) do
+      return ← withLetDecl n t' v' fun x => do
+        M.localMapM (mkLetFVars (usedLetOnly := true) #[x] ·) do
           let b' ← foldAndCollect oldIH newIH isRecCall (b.instantiate1 x)
           mkLetFun x v' b'
 
@@ -598,11 +598,6 @@ partial def buildInductionBody (toClear : Array FVarId) (goal : Expr)
           buildInductionBody toClear expAltType oldIH newIH isRecCall alt)
       return matcherApp'.toExpr
 
-  -- we look through mdata
-  if e.isMData then
-    let b ← buildInductionBody toClear goal oldIH newIH isRecCall e.mdataExpr!
-    return e.updateMData! b
-
   if let .letE n t v b _ := e then
     let t' ← foldAndCollect oldIH newIH isRecCall t
     let v' ← foldAndCollect oldIH newIH isRecCall v
@@ -613,7 +608,7 @@ partial def buildInductionBody (toClear : Array FVarId) (goal : Expr)
   if let some (n, t, v, b) := e.letFun? then
     let t' ← foldAndCollect oldIH newIH isRecCall t
     let v' ← foldAndCollect oldIH newIH isRecCall v
-    return ← withLocalDeclD n t' fun x => M2.branch do
+    return ← withLocalDecl n .default t' fun x => M2.branch do
       let b' ← buildInductionBody toClear goal oldIH newIH isRecCall (b.instantiate1 x)
       mkLetFun x v' b'
 

src/Lean/Meta/Tactic/LinearArith/Solver.lean

@@ -36,8 +36,8 @@ abbrev Assignment.get? (a : Assignment) (x : Var) : Option Rat :=
 abbrev Assignment.push (a : Assignment) (v : Rat) : Assignment :=
   { a with val := a.val.push v }
 
-abbrev Assignment.take (a : Assignment) (newSize : Nat) : Assignment :=
-  { a with val := a.val.take newSize }
+abbrev Assignment.shrink (a : Assignment) (newSize : Nat) : Assignment :=
+  { a with val := a.val.shrink newSize }
 
 structure Poly where
   val : Array (Int × Var)
@@ -242,7 +242,7 @@ def resolve (s : State) (cl : Cnstr) (cu : Cnstr) : Sum Result State :=
     let maxVarIdx := c.lhs.getMaxVar.id
     match s with -- Hack: we avoid { s with ... } to make sure we get a destructive update
     | { lowers, uppers, int, assignment, } =>
-      let assignment := assignment.take maxVarIdx
+      let assignment := assignment.shrink maxVarIdx
       if c.lhs.getMaxVarCoeff < 0 then
         let lowers := lowers.modify maxVarIdx (·.push c)
         Sum.inr { lowers, uppers, int, assignment }

src/Lean/Meta/WHNF.lean

@@ -84,7 +84,7 @@ private def mkNullaryCtor (type : Expr) (nparams : Nat) : MetaM (Option Expr) :=
   let .const d lvls := type.getAppFn
     | return none
   let (some ctor) ← getFirstCtor d | pure none
-  return mkAppN (mkConst ctor lvls) (type.getAppArgs.take nparams)
+  return mkAppN (mkConst ctor lvls) (type.getAppArgs.shrink nparams)
 
 private def getRecRuleFor (recVal : RecursorVal) (major : Expr) : Option RecursorRule :=
   match major.getAppFn with
@@ -152,7 +152,7 @@ private def toCtorWhenStructure (inductName : Name) (major : Expr) : MetaM Expr
       else
         let some ctorName ← getFirstCtor d | pure major
         let ctorInfo ← getConstInfoCtor ctorName
-        let params := majorType.getAppArgs.take ctorInfo.numParams
+        let params := majorType.getAppArgs.shrink ctorInfo.numParams
         let mut result := mkAppN (mkConst ctorName us) params
         for i in [:ctorInfo.numFields] do
           result := mkApp result (← mkProjFn ctorInfo us params i major)

src/Lean/Parser/Basic.lean

@@ -1305,7 +1305,7 @@ namespace ParserState
 
 def keepTop (s : SyntaxStack) (startStackSize : Nat) : SyntaxStack :=
   let node  := s.back
-  s.take startStackSize |>.push node
+  s.shrink startStackSize |>.push node
 
 def keepNewError (s : ParserState) (oldStackSize : Nat) : ParserState :=
   match s with
@@ -1314,13 +1314,13 @@ def keepNewError (s : ParserState) (oldStackSize : Nat) : ParserState :=
 def keepPrevError (s : ParserState) (oldStackSize : Nat) (oldStopPos : String.Pos) (oldError : Option Error) (oldLhsPrec : Nat) : ParserState :=
   match s with
   | ⟨stack, _, _, cache, _, errs⟩ =>
-    ⟨stack.take oldStackSize, oldLhsPrec, oldStopPos, cache, oldError, errs⟩
+    ⟨stack.shrink oldStackSize, oldLhsPrec, oldStopPos, cache, oldError, errs⟩
 
 def mergeErrors (s : ParserState) (oldStackSize : Nat) (oldError : Error) : ParserState :=
   match s with
   | ⟨stack, lhsPrec, pos, cache, some err, errs⟩ =>
     let newError := if oldError == err then err else oldError.merge err
-    ⟨stack.take oldStackSize, lhsPrec, pos, cache, some newError, errs⟩
+    ⟨stack.shrink oldStackSize, lhsPrec, pos, cache, some newError, errs⟩
   | other                         => other
 
 def keepLatest (s : ParserState) (startStackSize : Nat) : ParserState :=
@@ -1363,7 +1363,7 @@ def runLongestMatchParser (left? : Option Syntax) (startLhsPrec : Nat) (p : Pars
     s -- success or error with the expected number of nodes
   else if s.hasError then
     -- error with an unexpected number of nodes.
-    s.takeStack startSize |>.pushSyntax Syntax.missing
+    s.shrinkStack startSize |>.pushSyntax Syntax.missing
   else
     -- parser succeeded with incorrect number of nodes
     invalidLongestMatchParser s

src/Lean/Parser/Term.lean

@@ -819,7 +819,6 @@ We use them to implement `macro_rules` and `elab_rules`
 
 def namedArgument  := leading_parser (withAnonymousAntiquot := false)
   atomic ("(" >> ident >> " := ") >> withoutPosition termParser >> ")"
-/-- In a function application, `..` notation inserts zero or more `_` placeholders. -/
 def ellipsis       := leading_parser (withAnonymousAntiquot := false)
   ".." >> notFollowedBy (checkNoWsBefore >> ".") "`.` immediately after `..`"
 def argument       :=

src/Lean/Parser/Types.lean

@@ -158,10 +158,8 @@ def size (stack : SyntaxStack) : Nat :=
 def isEmpty (stack : SyntaxStack) : Bool :=
   stack.size == 0
 
-def take (stack : SyntaxStack) (n : Nat) : SyntaxStack :=
-  { stack with raw := stack.raw.take (stack.drop + n) }
-
-@[deprecated take (since := "2024-10-22")] abbrev shrink := @take
+def shrink (stack : SyntaxStack) (n : Nat) : SyntaxStack :=
+  { stack with raw := stack.raw.shrink (stack.drop + n) }
 
 def push (stack : SyntaxStack) (a : Syntax) : SyntaxStack :=
   { stack with raw := stack.raw.push a }
@@ -214,7 +212,7 @@ def stackSize (s : ParserState) : Nat :=
   s.stxStack.size
 
 def restore (s : ParserState) (iniStackSz : Nat) (iniPos : String.Pos) : ParserState :=
-  { s with stxStack := s.stxStack.take iniStackSz, errorMsg := none, pos := iniPos }
+  { s with stxStack := s.stxStack.shrink iniStackSz, errorMsg := none, pos := iniPos }
 
 def setPos (s : ParserState) (pos : String.Pos) : ParserState :=
   { s with pos := pos }
@@ -228,10 +226,8 @@ def pushSyntax (s : ParserState) (n : Syntax) : ParserState :=
 def popSyntax (s : ParserState) : ParserState :=
   { s with stxStack := s.stxStack.pop }
 
-def takeStack (s : ParserState) (iniStackSz : Nat) : ParserState :=
-  { s with stxStack := s.stxStack.take iniStackSz }
-
-@[deprecated takeStack (since := "2024-10-22")] abbrev shrinkStack := @takeStack
+def shrinkStack (s : ParserState) (iniStackSz : Nat) : ParserState :=
+  { s with stxStack := s.stxStack.shrink iniStackSz }
 
 def next (s : ParserState) (input : String) (pos : String.Pos) : ParserState :=
   { s with pos := input.next pos }
@@ -254,7 +250,7 @@ def mkNode (s : ParserState) (k : SyntaxNodeKind) (iniStackSz : Nat) : ParserSta
       ⟨stack, lhsPrec, pos, cache, err, recovered⟩
     else
       let newNode := Syntax.node SourceInfo.none k (stack.extract iniStackSz stack.size)
-      let stack   := stack.take iniStackSz
+      let stack   := stack.shrink iniStackSz
       let stack   := stack.push newNode
       ⟨stack, lhsPrec, pos, cache, err, recovered⟩
 
@@ -262,7 +258,7 @@ def mkTrailingNode (s : ParserState) (k : SyntaxNodeKind) (iniStackSz : Nat) : P
   match s with
   | ⟨stack, lhsPrec, pos, cache, err, errs⟩ =>
     let newNode := Syntax.node SourceInfo.none k (stack.extract (iniStackSz - 1) stack.size)
-    let stack   := stack.take (iniStackSz - 1)
+    let stack   := stack.shrink (iniStackSz - 1)
     let stack   := stack.push newNode
     ⟨stack, lhsPrec, pos, cache, err, errs⟩
 
@@ -287,7 +283,7 @@ def mkEOIError (s : ParserState) (expected : List String := []) : ParserState :=
 def mkErrorsAt (s : ParserState) (ex : List String) (pos : String.Pos) (initStackSz? : Option Nat := none) : ParserState := Id.run do
   let mut s := s.setPos pos
   if let some sz := initStackSz? then
-    s := s.takeStack sz
+    s := s.shrinkStack sz
   s := s.setError { expected := ex }
   s.pushSyntax .missing
 

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -1014,7 +1014,7 @@ Delaborates an `OfNat.ofNat` literal.
 `@OfNat.ofNat _ n _` ~> `n`.
 -/
 @[builtin_delab app.OfNat.ofNat]
-def delabOfNat : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPCoercions <| withOverApp 3 do
+def delabOfNat : Delab := whenPPOption getPPCoercions <| withOverApp 3 do
   delabOfNatCore (showType := (← getPPOption getPPNumericTypes))
 
 /--
@@ -1022,7 +1022,7 @@ Delaborates the negative of an `OfNat.ofNat` literal.
 `-@OfNat.ofNat _ n _` ~> `-n`
 -/
 @[builtin_delab app.Neg.neg]
-def delabNeg : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPCoercions do
+def delabNeg : Delab := whenPPOption getPPCoercions do
   delabNegIntCore (showType := (← getPPOption getPPNumericTypes))
 
 /--
@@ -1031,12 +1031,12 @@ Delaborates a rational number literal.
 and `-@OfNat.ofNat _ n _ / @OfNat.ofNat _ m` ~> `-n / m`
 -/
 @[builtin_delab app.HDiv.hDiv]
-def delabHDiv : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPCoercions do
+def delabHDiv : Delab := whenPPOption getPPCoercions do
   delabDivRatCore (showType := (← getPPOption getPPNumericTypes))
 
 -- `@OfDecimal.ofDecimal _ _ m s e` ~> `m*10^(sign * e)` where `sign == 1` if `s = false` and `sign = -1` if `s = true`
 @[builtin_delab app.OfScientific.ofScientific]
-def delabOfScientific : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPCoercions <| withOverApp 5 do
+def delabOfScientific : Delab := whenPPOption getPPCoercions <| withOverApp 5 do
   let expr ← getExpr
   guard <| expr.getAppNumArgs == 5
   let .lit (.natVal m) ← pure (expr.getArg! 2) | failure
@@ -1080,9 +1080,6 @@ def coeDelaborator : Delab := whenPPOption getPPCoercions do
   let e ← getExpr
   let .const declName _ := e.getAppFn | failure
   let some info ← Meta.getCoeFnInfo? declName | failure
-  if (← getPPOption getPPExplicit) && info.coercee != 0 then
-    -- Approximation: the only implicit arguments come before the coercee
-    failure
   let n := e.getAppNumArgs
   withOverApp info.numArgs do
     match info.type with
@@ -1095,7 +1092,7 @@ def coeDelaborator : Delab := whenPPOption getPPCoercions do
     | .coeSort => `(↥$(← withNaryArg info.coercee delab))
 
 @[builtin_delab app.dite]
-def delabDIte : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPNotation <| withOverApp 5 do
+def delabDIte : Delab := whenPPOption getPPNotation <| withOverApp 5 do
   -- Note: we keep this as a delaborator for now because it actually accesses the expression.
   guard $ (← getExpr).getAppNumArgs == 5
   let c ← withAppFn $ withAppFn $ withAppFn $ withAppArg delab
@@ -1112,7 +1109,7 @@ where
         return (← delab, h.getId)
 
 @[builtin_delab app.cond]
-def delabCond : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPNotation <| withOverApp 4 do
+def delabCond : Delab := whenPPOption getPPNotation <| withOverApp 4 do
   guard $ (← getExpr).getAppNumArgs == 4
   let c ← withAppFn $ withAppFn $ withAppArg delab
   let t ← withAppFn $ withAppArg delab
@@ -1132,7 +1129,7 @@ def delabNamedPattern : Delab := do
   `($x:ident@$h:ident:$p:term)
 
 -- Sigma and PSigma delaborators
-def delabSigmaCore (sigma : Bool) : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPNotation do
+def delabSigmaCore (sigma : Bool) : Delab := whenPPOption getPPNotation do
   guard $ (← getExpr).getAppNumArgs == 2
   guard $ (← getExpr).appArg!.isLambda
   withAppArg do
@@ -1212,7 +1209,7 @@ partial def delabDoElems : DelabM (List Syntax) := do
     prependAndRec x : DelabM _ := List.cons <$> x <*> delabDoElems
 
 @[builtin_delab app.Bind.bind]
-def delabDo : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPNotation do
+def delabDo : Delab := whenPPOption getPPNotation do
   guard <| (← getExpr).isAppOfArity ``Bind.bind 6
   let elems ← delabDoElems
   let items ← elems.toArray.mapM (`(doSeqItem|$(·):doElem))

src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean

@@ -398,7 +398,7 @@ mutual
       let fType ← replaceLPsWithVars (← inferType f)
       let (mvars, bInfos, resultType) ← forallMetaBoundedTelescope fType args.size
       let rest := args.extract mvars.size args.size
-      let args := args.take mvars.size
+      let args := args.shrink mvars.size
 
       -- Unify with the expected type
       if (← read).knowsType then tryUnify (← inferType (mkAppN f args)) resultType

src/Lean/PrettyPrinter/Formatter.lean

@@ -144,7 +144,7 @@ def fold (fn : Array Format → Format) (x : FormatterM Unit) : FormatterM Unit
   x
   let stack ← getStack
   let f := fn $ stack.extract sp stack.size
-  setStack $ (stack.take sp).push f
+  setStack $ (stack.shrink sp).push f
 
 /-- Execute `x` and concatenate generated Format objects. -/
 def concat (x : FormatterM Unit) : FormatterM Unit := do

src/Lean/Server/Completion.lean

@@ -207,8 +207,6 @@ private def getCompletionKindForDecl (constInfo : ConstantInfo) : M CompletionIt
       return CompletionItemKind.enum
     else
       return CompletionItemKind.struct
-  else if constInfo.isTheorem then
-    return CompletionItemKind.event
   else if (← isProjectionFn constInfo.name) then
     return CompletionItemKind.field
   else if (← whnf constInfo.type).isForall then

src/Lean/SubExpr.lean

@@ -7,7 +7,6 @@ prelude
 import Lean.Meta.Basic
 import Lean.Data.Json
 import Lean.Data.RBMap
-import Init.Control.Option
 
 namespace Lean
 

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

@@ -73,10 +73,6 @@ inductive BVBinOp where
   Unsigned modulo.
   -/
   | umod
-  /--
-  Signed division.
-  -/
-  | sdiv
 
 namespace BVBinOp
 
@@ -88,7 +84,6 @@ def toString : BVBinOp → String
   | mul => "*"
   | udiv => "/ᵤ"
   | umod => "%ᵤ"
-  | sdiv => "/ₛ"
 
 instance : ToString BVBinOp := ⟨toString⟩
 
@@ -103,7 +98,6 @@ def eval : BVBinOp → (BitVec w → BitVec w → BitVec w)
   | mul => (· * ·)
   | udiv => (· / ·)
   | umod => (· % · )
-  | sdiv => BitVec.sdiv
 
 @[simp] theorem eval_and : eval .and = ((· &&& ·) : BitVec w → BitVec w → BitVec w) := by rfl
 @[simp] theorem eval_or : eval .or = ((· ||| ·) : BitVec w → BitVec w → BitVec w) := by rfl
@@ -112,7 +106,6 @@ def eval : BVBinOp → (BitVec w → BitVec w → BitVec w)
 @[simp] theorem eval_mul : eval .mul = ((· * ·) : BitVec w → BitVec w → BitVec w) := by rfl
 @[simp] theorem eval_udiv : eval .udiv = ((· / ·) : BitVec w → BitVec w → BitVec w) := by rfl
 @[simp] theorem eval_umod : eval .umod = ((· % ·) : BitVec w → BitVec w → BitVec w) := by rfl
-@[simp] theorem eval_sdiv : eval .sdiv = (BitVec.sdiv : BitVec w → BitVec w → BitVec w) := by rfl
 
 end BVBinOp
 

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean

@@ -21,7 +21,6 @@ import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.SignExtend
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Mul
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Umod
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Sdiv
 
 /-!
 This module contains the implementation of a bitblaster for `BitVec` expressions (`BVExpr`).
@@ -118,13 +117,6 @@ where
           dsimp only at hlaig hraig
           omega
         ⟨res, this⟩
-      | .sdiv =>
-        let res := bitblast.blastSdiv aig ⟨lhs, rhs⟩
-        have := by
-          apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastSdiv)
-          dsimp only at hlaig hraig
-          omega
-        ⟨res, this⟩
     | .un op expr =>
       let ⟨⟨eaig, evec⟩, heaig⟩ := go aig expr
       match op with
@@ -235,7 +227,7 @@ theorem bitblast.go_decl_eq (aig : AIG BVBit) (expr : BVExpr w) :
     rw [AIG.LawfulVecOperator.decl_eq (f := blastConst)]
   | bin lhs op rhs lih rih =>
     match op with
-    | .and | .or | .xor | .add | .mul | .udiv | .umod | .sdiv =>
+    | .and | .or | .xor | .add | .mul | .udiv | .umod =>
       dsimp only [go]
       have := (bitblast.go aig lhs).property
       have := (go (go aig lhs).1.aig rhs).property

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Sdiv.lean

@@ -1,230 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Henrik Böving
--/
-prelude
-import Std.Sat.AIG.If
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Neg
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
-
-/-!
-This module contains the implementation of a bitblaster for `BitVec.sdiv`. The implemented
-circuit is the reduction to udiv.
--/
-
-namespace Std.Tactic.BVDecide
-
-open Std.Sat
-
-namespace BVExpr
-namespace bitblast
-
-variable [Hashable α] [DecidableEq α]
-
-namespace blastSdiv
-
-structure SignBranchInput (aig : AIG α) (len : Nat) where
-  w : Nat
-  lhs : AIG.RefVec aig w
-  rhs : AIG.RefVec aig w
-  lposRpos : AIG.RefVec aig len
-  lposRneg : AIG.RefVec aig len
-  lnegRpos : AIG.RefVec aig len
-  lnegRneg : AIG.RefVec aig len
-  hnezero : w ≠ 0
-
-def signBranch (aig : AIG α) (input : SignBranchInput aig len) : AIG.RefVecEntry α len :=
-  let ⟨w, lhs, rhs, lposRpos, lposRneg, lnegRpos, lnegRneg, hnezero⟩ := input
-  let res := AIG.RefVec.ite aig ⟨rhs.get (w - 1) (by omega), lposRneg, lposRpos⟩
-  let aig := res.aig
-  let lposHalf := res.vec
-  have := AIG.LawfulVecOperator.le_size (f := AIG.RefVec.ite) ..
-  let lhs := lhs.cast this
-  let rhs := rhs.cast this
-  let lnegRneg := lnegRneg.cast this
-  let lnegRpos := lnegRpos.cast this
-
-  let res := AIG.RefVec.ite aig ⟨rhs.get (w - 1) (by omega), lnegRneg, lnegRpos⟩
-  let aig := res.aig
-  let lnegHalf := res.vec
-  have := AIG.LawfulVecOperator.le_size (f := AIG.RefVec.ite) ..
-  let lhs := lhs.cast this
-  let lposHalf := lposHalf.cast this
-
-  AIG.RefVec.ite aig ⟨lhs.get (w - 1) (by omega), lnegHalf, lposHalf⟩
-
-instance : AIG.LawfulVecOperator α SignBranchInput signBranch where
-  le_size := by
-    intros
-    unfold signBranch
-    dsimp only
-    apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := AIG.RefVec.ite)
-    apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := AIG.RefVec.ite)
-    apply AIG.LawfulVecOperator.le_size (f := AIG.RefVec.ite)
-  decl_eq := by
-    intros
-    unfold signBranch
-    dsimp only
-    rw [AIG.LawfulVecOperator.decl_eq (f := AIG.RefVec.ite)]
-    rw [AIG.LawfulVecOperator.decl_eq (f := AIG.RefVec.ite)]
-    rw [AIG.LawfulVecOperator.decl_eq (f := AIG.RefVec.ite)]
-    · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := AIG.RefVec.ite)
-      assumption
-    · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := AIG.RefVec.ite)
-      apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := AIG.RefVec.ite)
-      assumption
-
-end blastSdiv
-
-def blastSdiv (aig : AIG α) (input : AIG.BinaryRefVec aig w) : AIG.RefVecEntry α w :=
-  if h : w = 0 then
-    ⟨aig, h ▸ AIG.RefVec.empty⟩
-  else
-    let ⟨lhs, rhs⟩ := input
-    let res := blastNeg aig lhs
-    let aig := res.aig
-    let negLhs := res.vec
-    have := AIG.LawfulVecOperator.le_size (f := blastNeg) ..
-    let lhs := lhs.cast this
-    let rhs := rhs.cast this
-    let res := blastNeg aig rhs
-    let aig := res.aig
-    let negRhs := res.vec
-    have := AIG.LawfulVecOperator.le_size (f := blastNeg) ..
-    let lhs := lhs.cast this
-    let rhs := rhs.cast this
-    let negLhs := negLhs.cast this
-
-    let res := blastUdiv aig ⟨lhs, rhs⟩
-    let aig := res.aig
-    let lposRpos := res.vec
-    have := AIG.LawfulVecOperator.le_size (f := blastUdiv) ..
-    let lhs := lhs.cast this
-    let rhs := rhs.cast this
-    let negRhs := negRhs.cast this
-    let negLhs := negLhs.cast this
-
-    let res := blastUdiv aig ⟨lhs, negRhs⟩
-    let aig := res.aig
-    let ldivnr := res.vec
-    let res := blastNeg aig ldivnr
-    let aig := res.aig
-    let lposRneg := res.vec
-    have := by
-      apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastNeg)
-      apply AIG.LawfulVecOperator.le_size (f := blastUdiv)
-    let lhs := lhs.cast this
-    let rhs := rhs.cast this
-    let negRhs := negRhs.cast this
-    let negLhs := negLhs.cast this
-    let lposRpos := lposRpos.cast this
-
-    let res := blastUdiv aig ⟨negLhs, rhs⟩
-    let aig := res.aig
-    let nldivr := res.vec
-    let res := blastNeg aig nldivr
-    let aig := res.aig
-    let lnegRpos := res.vec
-    have := by
-      apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastNeg)
-      apply AIG.LawfulVecOperator.le_size (f := blastUdiv)
-    let lhs := lhs.cast this
-    let rhs := rhs.cast this
-    let negRhs := negRhs.cast this
-    let negLhs := negLhs.cast this
-    let lposRpos := lposRpos.cast this
-    let lposRneg := lposRneg.cast this
-
-    let res := blastUdiv aig ⟨negLhs, negRhs⟩
-    let aig := res.aig
-    let lnegRneg := res.vec
-    have := AIG.LawfulVecOperator.le_size (f := blastUdiv) ..
-    let lhs := lhs.cast this
-    let rhs := rhs.cast this
-    let lposRpos := lposRpos.cast this
-    let lposRneg := lposRneg.cast this
-    let lnegRpos := lnegRpos.cast this
-
-    blastSdiv.signBranch aig ⟨w, lhs, rhs, lposRpos, lposRneg, lnegRpos, lnegRneg, h⟩
-
-instance : AIG.LawfulVecOperator α AIG.BinaryRefVec blastSdiv where
-  le_size := by
-    intros
-    unfold blastSdiv
-    dsimp only
-    split
-    · simp
-    · apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastSdiv.signBranch)
-      apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastUdiv)
-      apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastNeg)
-      apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastUdiv)
-      apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastNeg)
-      apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastUdiv)
-      apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastUdiv)
-      apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastNeg)
-      apply AIG.LawfulVecOperator.le_size (f := blastNeg)
-  decl_eq := by
-    intros
-    unfold blastSdiv
-    dsimp only
-    split
-    · simp
-    · rw [AIG.LawfulVecOperator.decl_eq (f := blastSdiv.signBranch)]
-      rw [AIG.LawfulVecOperator.decl_eq (f := blastUdiv)]
-      rw [AIG.LawfulVecOperator.decl_eq (f := blastNeg)]
-      rw [AIG.LawfulVecOperator.decl_eq (f := blastUdiv)]
-      rw [AIG.LawfulVecOperator.decl_eq (f := blastNeg)]
-      rw [AIG.LawfulVecOperator.decl_eq (f := blastUdiv)]
-      rw [AIG.LawfulVecOperator.decl_eq (f := blastUdiv)]
-      rw [AIG.LawfulVecOperator.decl_eq (f := blastNeg)]
-      rw [AIG.LawfulVecOperator.decl_eq (f := blastNeg)]
-      · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        assumption
-      · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        assumption
-      · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        assumption
-      · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        assumption
-      · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        assumption
-      · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        assumption
-      · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        assumption
-      · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        assumption
-
-end bitblast
-end BVExpr
-
-end Std.Tactic.BVDecide

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

@@ -21,7 +21,6 @@ import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.SignExtend
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Mul
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Udiv
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Umod
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Sdiv
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
 
 /-!
@@ -219,18 +218,6 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
         · simp [Ref.hgate]
       · intros
         rw [← rih]
-    | sdiv =>
-      simp only [go, eval_bin, BVBinOp.eval_sdiv]
-      apply denote_blastSdiv
-      · intros
-        dsimp only
-        rw [go_denote_mem_prefix]
-        rw [← lih (aig := aig)]
-        · simp
-        · assumption
-        · simp [Ref.hgate]
-      · intros
-        rw [← rih]
   | un op expr ih =>
     cases op with
     | not => simp [go, ih, hidx]

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Sdiv.lean

@@ -1,201 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Henrik Böving
--/
-prelude
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Udiv
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Neg
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Sdiv
-import Std.Tactic.BVDecide.Normalize.BitVec
-
-/-!
-This module contains the verification of the `BitVec.sdiv` bitblaster from `Impl.Operations.Sdiv`.
--/
-
-namespace Std.Tactic.BVDecide
-
-open Std.Sat
-open Std.Sat.AIG
-
-namespace BVExpr
-namespace bitblast
-
-variable [Hashable α] [DecidableEq α]
-
-namespace blastSdiv
-
-theorem denote_signBranch {aig : AIG α} (input : SignBranchInput aig len) (lhs rhs : BitVec input.w)
-    (lposRpos lposRneg lnegRpos lnegRneg : BitVec len)
-    (hleft : ∀ (idx : Nat) (hidx : idx < input.w), ⟦aig, input.lhs.get idx hidx, assign⟧ = lhs.getLsbD idx)
-    (hright : ∀ (idx : Nat) (hidx : idx < input.w), ⟦aig, input.rhs.get idx hidx, assign⟧ = rhs.getLsbD idx)
-    (hlprp : ∀ (idx : Nat) (hidx : idx < len), ⟦aig, input.lposRpos.get idx hidx, assign⟧ = lposRpos.getLsbD idx)
-    (hlprn : ∀ (idx : Nat) (hidx : idx < len), ⟦aig, input.lposRneg.get idx hidx, assign⟧ = lposRneg.getLsbD idx)
-    (hlnrp : ∀ (idx : Nat) (hidx : idx < len), ⟦aig, input.lnegRpos.get idx hidx, assign⟧ = lnegRpos.getLsbD idx)
-    (hlnrn : ∀ (idx : Nat) (hidx : idx < len), ⟦aig, input.lnegRneg.get idx hidx, assign⟧ = lnegRneg.getLsbD idx) :
-    ∀ (idx : Nat) (hidx : idx < len),
-      ⟦(signBranch aig input).aig, (signBranch aig input).vec.get idx hidx, assign⟧
-        =
-      (match lhs.msb, rhs.msb with
-      | false, false => lposRpos
-      | false, true => lposRneg
-      | true, false => lnegRpos
-      | true, true => lnegRneg).getLsbD idx
-      := by
-  intros
-  unfold signBranch
-  simp only [ne_eq, RefVec.denote_ite, RefVec.get_cast, Ref.cast_eq]
-  split
-  · next h1 =>
-    rw [AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix] at h1
-    rw [hleft, ← BitVec.msb_eq_getLsbD_last] at h1
-    rw [h1]
-    split
-    · next h2 =>
-      rw [AIG.LawfulVecOperator.denote_mem_prefix] at h2
-      rw [hright, ← BitVec.msb_eq_getLsbD_last] at h2
-      rw [h2]
-      rw [AIG.LawfulVecOperator.denote_mem_prefix, hlnrn]
-    · next h2 =>
-      rw [AIG.LawfulVecOperator.denote_mem_prefix] at h2
-      rw [hright, ← BitVec.msb_eq_getLsbD_last, Bool.not_eq_true] at h2
-      rw [h2]
-      rw [AIG.LawfulVecOperator.denote_mem_prefix, hlnrp]
-  · next h1 =>
-    rw [AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix] at h1
-    rw [hleft, ← BitVec.msb_eq_getLsbD_last, Bool.not_eq_true] at h1
-    rw [h1]
-    rw [AIG.LawfulVecOperator.denote_mem_prefix]
-    rw [AIG.RefVec.denote_ite]
-    split
-    · next h2 =>
-      rw [hright, ← BitVec.msb_eq_getLsbD_last] at h2
-      rw [h2]
-      simp [hlprn]
-    · next h2 =>
-      rw [hright, ← BitVec.msb_eq_getLsbD_last, Bool.not_eq_true] at h2
-      rw [h2]
-      simp [hlprp]
-
-end blastSdiv
-
-theorem denote_blastSdiv (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bool)
-    (input : BinaryRefVec aig w)
-    (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.lhs.get idx hidx, assign⟧ = lhs.getLsbD idx)
-    (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.rhs.get idx hidx, assign⟧ = rhs.getLsbD idx) :
-    ∀ (idx : Nat) (hidx : idx < w),
-      ⟦(blastSdiv aig input).aig, (blastSdiv aig input).vec.get idx hidx, assign⟧
-        =
-      (BitVec.sdiv lhs rhs).getLsbD idx := by
-  intros
-  generalize hres : blastSdiv aig input = res
-  unfold blastSdiv at hres
-  split at hres
-  · omega
-  · dsimp only at hres
-    rw [← hres]
-    clear hres
-    rw [blastSdiv.denote_signBranch
-        (lhs := lhs)
-        (rhs := rhs)
-        (lposRpos := lhs / rhs)
-        (lposRneg := -(lhs / (-rhs)))
-        (lnegRpos := -((-lhs) / rhs))
-        (lnegRneg := ((-lhs) / (-rhs)))
-      ]
-    · rw [BitVec.sdiv_eq]
-      rfl
-    · simp only [RefVec.get_cast, Ref.cast_eq]
-      intros
-      rw [AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix,
-        AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix,
-        AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix,
-        AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix]
-      rw [hleft]
-    · simp only [RefVec.get_cast, Ref.cast_eq]
-      intros
-      rw [AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix,
-        AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix,
-        AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix,
-        AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix]
-      rw [hright]
-    · simp only [RefVec.get_cast, Ref.cast_eq]
-      intros
-      rw [AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix,
-        AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix,
-        AIG.LawfulVecOperator.denote_mem_prefix]
-      rw [denote_blastUdiv (lhs := lhs) (rhs := rhs)]
-      · intros
-        rw [AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix]
-        · simp [hleft]
-        · simp [Ref.hgate]
-      · intros
-        rw [AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix]
-        · simp [hright]
-        · simp [Ref.hgate]
-    · simp only [RefVec.get_cast, Ref.cast_eq]
-      intros
-      rw [AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix,
-        AIG.LawfulVecOperator.denote_mem_prefix]
-      rw [denote_blastNeg (value := lhs / (-rhs))]
-      intros
-      rw [denote_blastUdiv (lhs := lhs) (rhs := -rhs)]
-      · intros
-        rw [AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix,
-          AIG.LawfulVecOperator.denote_mem_prefix]
-        · simp [hleft]
-        · simp [Ref.hgate]
-      · intros
-        rw [AIG.LawfulVecOperator.denote_mem_prefix]
-        · simp only [RefVec.get_cast, Ref.cast_eq]
-          rw [denote_blastNeg (value := rhs)]
-          intros
-          rw [AIG.LawfulVecOperator.denote_mem_prefix]
-          · simp [hright]
-          · simp [Ref.hgate]
-        · simp [Ref.hgate]
-    · simp only [RefVec.get_cast, Ref.cast_eq]
-      intros
-      rw [AIG.LawfulVecOperator.denote_mem_prefix]
-      rw [denote_blastNeg (value := (-lhs) / rhs)]
-      intros
-      rw [denote_blastUdiv (lhs := -lhs) (rhs := rhs)]
-      · intros
-        rw [AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix,
-          AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix]
-        · simp only [RefVec.get_cast, Ref.cast_eq]
-          rw [denote_blastNeg (value := lhs)]
-          simp [hleft]
-        · simp [Ref.hgate]
-      · intros
-        rw [AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix,
-          AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix,
-          AIG.LawfulVecOperator.denote_mem_prefix]
-        · simp [hright]
-        · simp [Ref.hgate]
-    · simp only
-      intros
-      rw [denote_blastUdiv (lhs := -lhs) (rhs := - rhs)]
-      · intros
-        simp only [RefVec.get_cast, Ref.cast_eq]
-        rw [AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix,
-          AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix,
-          AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix]
-        rw [denote_blastNeg (value := lhs)]
-        simp [hleft]
-      · intros
-        simp only [RefVec.get_cast, Ref.cast_eq]
-        rw [AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix,
-          AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix,
-          AIG.LawfulVecOperator.denote_mem_prefix]
-        rw [denote_blastNeg (value := rhs)]
-        intros
-        rw [AIG.LawfulVecOperator.denote_mem_prefix]
-        · simp [hright]
-        · simp [Ref.hgate]
-
-
-end bitblast
-end BVExpr
-
-end Std.Tactic.BVDecide

src/Std/Tactic/BVDecide/Normalize/BitVec.lean

@@ -262,7 +262,6 @@ attribute [bv_normalize] BitVec.zero_umod
 attribute [bv_normalize] BitVec.umod_zero
 attribute [bv_normalize] BitVec.umod_one
 attribute [bv_normalize] BitVec.umod_eq_and
-attribute [bv_normalize] BitVec.sdiv_eq_and
 
 end Normalize
 end Std.Tactic.BVDecide

src/Std/Tactic/BVDecide/Reflect.lean

@@ -118,10 +118,6 @@ theorem umod_congr (lhs rhs lhs' rhs' : BitVec w) (h1 : lhs' = lhs) (h2 : rhs' =
     (lhs' % rhs') = (lhs % rhs) := by
   simp[*]
 
-theorem sdiv_congr (lhs rhs lhs' rhs' : BitVec w) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
-    (BitVec.sdiv lhs' rhs') = (BitVec.sdiv lhs rhs) := by
-  simp[*]
-
 end BitVec
 
 namespace Bool

src/cmake/Modules/FindWindowsSDK.cmake

@@ -1,643 +0,0 @@
-# - Find the Windows SDK aka Platform SDK
-#
-# Relevant Wikipedia article: http://en.wikipedia.org/wiki/Microsoft_Windows_SDK
-#
-# Pass "COMPONENTS tools" to ignore Visual Studio version checks: in case
-# you just want the tool binaries to run, rather than the libraries and headers
-# for compiling.
-#
-# Variables:
-#  WINDOWSSDK_FOUND - if any version of the windows or platform SDK was found that is usable with the current version of visual studio
-#  WINDOWSSDK_LATEST_DIR
-#  WINDOWSSDK_LATEST_NAME
-#  WINDOWSSDK_FOUND_PREFERENCE - if we found an entry indicating a "preferred" SDK listed for this visual studio version
-#  WINDOWSSDK_PREFERRED_DIR
-#  WINDOWSSDK_PREFERRED_NAME
-#
-#  WINDOWSSDK_DIRS - contains no duplicates, ordered most recent first.
-#  WINDOWSSDK_PREFERRED_FIRST_DIRS - contains no duplicates, ordered with preferred first, followed by the rest in descending recency
-#
-# Functions:
-#  windowssdk_name_lookup(<directory> <output variable>) - Find the name corresponding with the SDK directory you pass in, or
-#     NOTFOUND if not recognized. Your directory must be one of WINDOWSSDK_DIRS for this to work.
-#
-#  windowssdk_build_lookup(<directory> <output variable>) - Find the build version number corresponding with the SDK directory you pass in, or
-#     NOTFOUND if not recognized. Your directory must be one of WINDOWSSDK_DIRS for this to work.
-#
-#  get_windowssdk_from_component(<file or dir> <output variable>) - Given a library or include dir,
-#     find the Windows SDK root dir corresponding to it, or NOTFOUND if unrecognized.
-#
-#  get_windowssdk_library_dirs(<directory> <output variable>) - Find the architecture-appropriate
-#     library directories corresponding to the SDK directory you pass in (or NOTFOUND if none)
-#
-#  get_windowssdk_library_dirs_multiple(<output variable> <directory> ...) - Find the architecture-appropriate
-#     library directories corresponding to the SDK directories you pass in, in order, skipping those not found. NOTFOUND if none at all.
-#     Good for passing WINDOWSSDK_DIRS or WINDOWSSDK_DIRS to if you really just want a file and don't care where from.
-#
-#  get_windowssdk_include_dirs(<directory> <output variable>) - Find the
-#     include directories corresponding to the SDK directory you pass in (or NOTFOUND if none)
-#
-#  get_windowssdk_include_dirs_multiple(<output variable> <directory> ...) - Find the
-#     include directories corresponding to the SDK directories you pass in, in order, skipping those not found. NOTFOUND if none at all.
-#     Good for passing WINDOWSSDK_DIRS or WINDOWSSDK_DIRS to if you really just want a file and don't care where from.
-#
-# Requires these CMake modules:
-#  FindPackageHandleStandardArgs (known included with CMake >=2.6.2)
-#
-# Original Author:
-# 2012 Rylie Pavlik <rylie@ryliepavlik.com>
-# https://ryliepavlik.com/
-# Iowa State University HCI Graduate Program/VRAC
-#
-# Copyright 2012, Iowa State University
-#
-# Distributed under the Boost Software License, Version 1.0.
-# (See accompanying file LICENSE_1_0.txt or copy at
-# http://www.boost.org/LICENSE_1_0.txt)
-#
-# SPDX-License-Identifier: BSL-1.0
-
-set(_preferred_sdk_dirs) # pre-output
-set(_win_sdk_dirs) # pre-output
-set(_win_sdk_versanddirs) # pre-output
-set(_win_sdk_buildsanddirs) # pre-output
-set(_winsdk_vistaonly) # search parameters
-set(_winsdk_kits) # search parameters
-
-
-set(_WINDOWSSDK_ANNOUNCE OFF)
-if(NOT WINDOWSSDK_FOUND AND (NOT WindowsSDK_FIND_QUIETLY))
-	set(_WINDOWSSDK_ANNOUNCE ON)
-endif()
-macro(_winsdk_announce)
-	if(_WINSDK_ANNOUNCE)
-		message(STATUS ${ARGN})
-	endif()
-endmacro()
-
-# See https://developer.microsoft.com/en-us/windows/downloads/sdk-archive -
-# although version numbers listed on that page don't necessarily match the directory
-# used by the installer.
-set(_winsdk_win10vers
-	10.0.26100.0
-	10.0.22621.0
-	10.0.22000.0
-	10.0.20348.0
-	10.0.19041.0
-	10.0.18362.0 # Win10 1903 "19H1"
-	10.0.17763.0 # Win10 1809 "October 2018 Update"
-	10.0.17134.0 # Redstone 4 aka Win10 1803 "April 2018 Update"
-	10.0.17133.0 # Redstone 4 aka Win10 1803 "April 2018 Update"
-	10.0.16299.0 # Redstone 3 aka Win10 1709 "Fall Creators Update"
-	10.0.15063.0 # Redstone 2 aka Win10 1703 "Creators Update"
-	10.0.14393.0 # Redstone aka Win10 1607 "Anniversary Update"
-	10.0.10586.0 # TH2 aka Win10 1511
-	10.0.10240.0 # Win10 RTM
-	10.0.10150.0 # just ucrt
-	10.0.10056.0
-)
-
-if(WindowsSDK_FIND_COMPONENTS MATCHES "tools")
-	set(_WINDOWSSDK_IGNOREMSVC ON)
-	_winsdk_announce("Checking for tools from Windows/Platform SDKs...")
-else()
-	set(_WINDOWSSDK_IGNOREMSVC OFF)
-	_winsdk_announce("Checking for Windows/Platform SDKs...")
-endif()
-
-# Appends to the three main pre-output lists used only if the path exists
-# and is not already in the list.
-function(_winsdk_conditional_append _vername _build _path)
-	if(("${_path}" MATCHES "registry") OR (NOT EXISTS "${_path}"))
-		# Path invalid - do not add
-		return()
-	endif()
-	list(FIND _win_sdk_dirs "${_path}" _win_sdk_idx)
-	if(_win_sdk_idx GREATER -1)
-		# Path already in list - do not add
-		return()
-	endif()
-	_winsdk_announce( " - ${_vername}, Build ${_build} @ ${_path}")
-	# Not yet in the list, so we'll add it
-	list(APPEND _win_sdk_dirs "${_path}")
-	set(_win_sdk_dirs "${_win_sdk_dirs}" CACHE INTERNAL "" FORCE)
-	list(APPEND
-		_win_sdk_versanddirs
-		"${_vername}"
-		"${_path}")
-	set(_win_sdk_versanddirs "${_win_sdk_versanddirs}" CACHE INTERNAL "" FORCE)
-	list(APPEND
-		_win_sdk_buildsanddirs
-		"${_build}"
-		"${_path}")
-	set(_win_sdk_buildsanddirs "${_win_sdk_buildsanddirs}" CACHE INTERNAL "" FORCE)
-endfunction()
-
-# Appends to the "preferred SDK" lists only if the path exists
-function(_winsdk_conditional_append_preferred _info _path)
-	if(("${_path}" MATCHES "registry") OR (NOT EXISTS "${_path}"))
-		# Path invalid - do not add
-		return()
-	endif()
-
-	get_filename_component(_path "${_path}" ABSOLUTE)
-
-	list(FIND _win_sdk_preferred_sdk_dirs "${_path}" _win_sdk_idx)
-	if(_win_sdk_idx GREATER -1)
-		# Path already in list - do not add
-		return()
-	endif()
-	_winsdk_announce( " - Found \"preferred\" SDK ${_info} @ ${_path}")
-	# Not yet in the list, so we'll add it
-	list(APPEND _win_sdk_preferred_sdk_dirs "${_path}")
-	set(_win_sdk_preferred_sdk_dirs "${_win_sdk_dirs}" CACHE INTERNAL "" FORCE)
-
-	# Just in case we somehow missed it:
-	_winsdk_conditional_append("${_info}" "" "${_path}")
-endfunction()
-
-# Given a version like v7.0A, looks for an SDK in the registry under "Microsoft SDKs".
-# If the given version might be in both HKEY_LOCAL_MACHINE\\SOFTWARE\\Microsoft\\Microsoft SDKs\\Windows
-# and HKEY_LOCAL_MACHINE\\SOFTWARE\\Microsoft\\Windows Kits\\Installed Roots aka "Windows Kits",
-# use this macro first, since these registry keys usually have more information.
-#
-# Pass a "default" build number as an extra argument in case we can't find it.
-function(_winsdk_check_microsoft_sdks_registry _winsdkver)
-	set(SDKKEY "HKEY_LOCAL_MACHINE\\SOFTWARE\\Microsoft\\Microsoft SDKs\\Windows\\${_winsdkver}")
-	get_filename_component(_sdkdir
-		"[${SDKKEY};InstallationFolder]"
-		ABSOLUTE)
-
-	set(_sdkname "Windows SDK ${_winsdkver}")
-
-	# Default build number passed as extra argument
-	set(_build ${ARGN})
-	# See if the registry holds a Microsoft-mutilated, err, designated, product name
-	# (just using get_filename_component to execute the registry lookup)
-	get_filename_component(_sdkproductname
-		"[${SDKKEY};ProductName]"
-		NAME)
-	if(NOT "${_sdkproductname}" MATCHES "registry")
-		# Got a product name
-		set(_sdkname "${_sdkname} (${_sdkproductname})")
-	endif()
-
-	# try for a version to augment our name
-	# (just using get_filename_component to execute the registry lookup)
-	get_filename_component(_sdkver
-		"[${SDKKEY};ProductVersion]"
-		NAME)
-	if(NOT "${_sdkver}" MATCHES "registry" AND NOT MATCHES)
-		# Got a version
-		if(NOT "${_sdkver}" MATCHES "\\.\\.")
-			# and it's not an invalid one with two dots in it:
-			# use to override the default build
-			set(_build ${_sdkver})
-			if(NOT "${_sdkname}" MATCHES "${_sdkver}")
-				# Got a version that's not already in the name, let's use it to improve our name.
-				set(_sdkname "${_sdkname} (${_sdkver})")
-			endif()
-		endif()
-	endif()
-	_winsdk_conditional_append("${_sdkname}" "${_build}" "${_sdkdir}")
-endfunction()
-
-# Given a name for identification purposes, the build number, and a key (technically a "value name")
-# corresponding to a Windows SDK packaged as a "Windows Kit", look for it
-# in HKEY_LOCAL_MACHINE\\SOFTWARE\\Microsoft\\Windows Kits\\Installed Roots
-# Note that the key or "value name" tends to be something weird like KitsRoot81 -
-# no easy way to predict, just have to observe them in the wild.
-# Doesn't hurt to also try _winsdk_check_microsoft_sdks_registry for these:
-# sometimes you get keys in both parts of the registry (in the wow64 portion especially),
-# and the non-"Windows Kits" location is often more descriptive.
-function(_winsdk_check_windows_kits_registry _winkit_name _winkit_build _winkit_key)
-	get_filename_component(_sdkdir
-		"[HKEY_LOCAL_MACHINE\\SOFTWARE\\Microsoft\\Windows Kits\\Installed Roots;${_winkit_key}]"
-		ABSOLUTE)
-	_winsdk_conditional_append("${_winkit_name}" "${_winkit_build}" "${_sdkdir}")
-endfunction()
-
-# Given a name for identification purposes and the build number
-# corresponding to a Windows 10 SDK packaged as a "Windows Kit", look for it
-# in HKEY_LOCAL_MACHINE\\SOFTWARE\\Microsoft\\Windows Kits\\Installed Roots
-# Doesn't hurt to also try _winsdk_check_microsoft_sdks_registry for these:
-# sometimes you get keys in both parts of the registry (in the wow64 portion especially),
-# and the non-"Windows Kits" location is often more descriptive.
-function(_winsdk_check_win10_kits _winkit_build)
-	get_filename_component(_sdkdir
-		"[HKEY_LOCAL_MACHINE\\SOFTWARE\\Microsoft\\Windows Kits\\Installed Roots;KitsRoot10]"
-		ABSOLUTE)
-	if(("${_sdkdir}" MATCHES "registry") OR (NOT EXISTS "${_sdkdir}"))
-		return() # not found
-	endif()
-	if(EXISTS "${_sdkdir}/Include/${_winkit_build}/um")
-		_winsdk_conditional_append("Windows Kits 10 (Build ${_winkit_build})" "${_winkit_build}" "${_sdkdir}")
-	endif()
-endfunction()
-
-# Given a name for indentification purposes, the build number, and the associated package GUID,
-# look in the registry under both HKLM and HKCU in \\SOFTWARE\\Microsoft\\MicrosoftSDK\\InstalledSDKs\\
-# for that guid and the SDK it points to.
-function(_winsdk_check_platformsdk_registry _platformsdkname _build _platformsdkguid)
-	foreach(_winsdk_hive HKEY_LOCAL_MACHINE HKEY_CURRENT_USER)
-		get_filename_component(_sdkdir
-			"[${_winsdk_hive}\\SOFTWARE\\Microsoft\\MicrosoftSDK\\InstalledSDKs\\${_platformsdkguid};Install Dir]"
-			ABSOLUTE)
-		_winsdk_conditional_append("${_platformsdkname} (${_build})" "${_build}" "${_sdkdir}")
-	endforeach()
-endfunction()
-
-###
-# Detect toolchain information: to know whether it's OK to use Vista+ only SDKs
-###
-set(_winsdk_vistaonly_ok OFF)
-if(MSVC AND NOT _WINDOWSSDK_IGNOREMSVC)
-	# VC 10 and older has broad target support
-	if(MSVC_VERSION LESS 1700)
-		# VC 11 by default targets Vista and later only, so we can add a few more SDKs that (might?) only work on vista+
-	elseif("${CMAKE_VS_PLATFORM_TOOLSET}" MATCHES "_xp")
-		# This is the XP-compatible v110+ toolset
-	elseif("${CMAKE_VS_PLATFORM_TOOLSET}" STREQUAL "v100" OR "${CMAKE_VS_PLATFORM_TOOLSET}" STREQUAL "v90")
-		# This is the VS2010/VS2008 toolset
-	else()
-		# OK, we're VC11 or newer and not using a backlevel or XP-compatible toolset.
-		# These versions have no XP (and possibly Vista pre-SP1) support
-		set(_winsdk_vistaonly_ok ON)
-		if(_WINDOWSSDK_ANNOUNCE AND NOT _WINDOWSSDK_VISTAONLY_PESTERED)
-			set(_WINDOWSSDK_VISTAONLY_PESTERED ON CACHE INTERNAL "" FORCE)
-			message(STATUS "FindWindowsSDK: Detected Visual Studio 2012 or newer, not using the _xp toolset variant: including SDK versions that drop XP support in search!")
-		endif()
-	endif()
-endif()
-if(_WINDOWSSDK_IGNOREMSVC)
-	set(_winsdk_vistaonly_ok ON)
-endif()
-
-###
-# MSVC version checks - keeps messy conditionals in one place
-# (messy because of _WINDOWSSDK_IGNOREMSVC)
-###
-set(_winsdk_msvc_greater_1200 OFF)
-if(_WINDOWSSDK_IGNOREMSVC OR (MSVC AND (MSVC_VERSION GREATER 1200)))
-	set(_winsdk_msvc_greater_1200 ON)
-endif()
-# Newer than VS .NET/VS Toolkit 2003
-set(_winsdk_msvc_greater_1310 OFF)
-if(_WINDOWSSDK_IGNOREMSVC OR (MSVC AND (MSVC_VERSION GREATER 1310)))
-	set(_winsdk_msvc_greater_1310 ON)
-endif()
-
-# VS2005/2008
-set(_winsdk_msvc_less_1600 OFF)
-if(_WINDOWSSDK_IGNOREMSVC OR (MSVC AND (MSVC_VERSION LESS 1600)))
-	set(_winsdk_msvc_less_1600 ON)
-endif()
-
-# VS2013+
-set(_winsdk_msvc_not_less_1800 OFF)
-if(_WINDOWSSDK_IGNOREMSVC OR (MSVC AND (NOT MSVC_VERSION LESS 1800)))
-	set(_winsdk_msvc_not_less_1800 ON)
-endif()
-
-###
-# START body of find module
-###
-if(_winsdk_msvc_greater_1310) # Newer than VS .NET/VS Toolkit 2003
-	###
-	# Look for "preferred" SDKs
-	###
-
-	# Environment variable for SDK dir
-	if(EXISTS "$ENV{WindowsSDKDir}" AND (NOT "$ENV{WindowsSDKDir}" STREQUAL ""))
-		_winsdk_conditional_append_preferred("WindowsSDKDir environment variable" "$ENV{WindowsSDKDir}")
-	endif()
-
-	if(_winsdk_msvc_less_1600)
-		# Per-user current Windows SDK for VS2005/2008
-		get_filename_component(_sdkdir
-			"[HKEY_CURRENT_USER\\Software\\Microsoft\\Microsoft SDKs\\Windows;CurrentInstallFolder]"
-			ABSOLUTE)
-		_winsdk_conditional_append_preferred("Per-user current Windows SDK" "${_sdkdir}")
-
-		# System-wide current Windows SDK for VS2005/2008
-		get_filename_component(_sdkdir
-			"[HKEY_LOCAL_MACHINE\\SOFTWARE\\Microsoft\\Microsoft SDKs\\Windows;CurrentInstallFolder]"
-			ABSOLUTE)
-		_winsdk_conditional_append_preferred("System-wide current Windows SDK" "${_sdkdir}")
-	endif()
-
-	###
-	# Begin the massive list of SDK searching!
-	###
-	if(_winsdk_vistaonly_ok AND _winsdk_msvc_not_less_1800)
-		# These require at least Visual Studio 2013 (VC12)
-
-		_winsdk_check_microsoft_sdks_registry(v10.0A)
-
-		# Windows Software Development Kit (SDK) for Windows 10
-		# Several different versions living in the same directory - if nothing else we can assume RTM (10240)
-		_winsdk_check_microsoft_sdks_registry(v10.0 10.0.10240.0)
-		foreach(_win10build ${_winsdk_win10vers})
-			_winsdk_check_win10_kits(${_win10build})
-		endforeach()
-	endif() # vista-only and 2013+
-
-	# Included in Visual Studio 2013
-	# Includes the v120_xp toolset
-	_winsdk_check_microsoft_sdks_registry(v8.1A 8.1.51636)
-
-	if(_winsdk_vistaonly_ok AND _winsdk_msvc_not_less_1800)
-		# Windows Software Development Kit (SDK) for Windows 8.1
-		# http://msdn.microsoft.com/en-gb/windows/desktop/bg162891
-		_winsdk_check_microsoft_sdks_registry(v8.1 8.1.25984.0)
-		_winsdk_check_windows_kits_registry("Windows Kits 8.1" 8.1.25984.0 KitsRoot81)
-	endif() # vista-only and 2013+
-
-	if(_winsdk_vistaonly_ok)
-		# Included in Visual Studio 2012
-		_winsdk_check_microsoft_sdks_registry(v8.0A 8.0.50727)
-
-		# Microsoft Windows SDK for Windows 8 and .NET Framework 4.5
-		# This is the first version to also include the DirectX SDK
-		# http://msdn.microsoft.com/en-US/windows/desktop/hh852363.aspx
-		_winsdk_check_microsoft_sdks_registry(v8.0 6.2.9200.16384)
-		_winsdk_check_windows_kits_registry("Windows Kits 8.0" 6.2.9200.16384 KitsRoot)
-	endif() # vista-only
-
-	# Included with VS 2012 Update 1 or later
-	# Introduces v110_xp toolset
-	_winsdk_check_microsoft_sdks_registry(v7.1A 7.1.51106)
-	if(_winsdk_vistaonly_ok)
-		# Microsoft Windows SDK for Windows 7 and .NET Framework 4
-		# http://www.microsoft.com/downloads/en/details.aspx?FamilyID=6b6c21d2-2006-4afa-9702-529fa782d63b
-		_winsdk_check_microsoft_sdks_registry(v7.1 7.1.7600.0.30514)
-	endif() # vista-only
-
-	# Included with VS 2010
-	_winsdk_check_microsoft_sdks_registry(v7.0A 6.1.7600.16385)
-
-	# Windows SDK for Windows 7 and .NET Framework 3.5 SP1
-	# Works with VC9
-	# http://www.microsoft.com/en-us/download/details.aspx?id=18950
-	_winsdk_check_microsoft_sdks_registry(v7.0 6.1.7600.16385)
-
-	# Two versions call themselves "v6.1":
-	# Older:
-	# Windows Vista Update & .NET 3.0 SDK
-	# http://www.microsoft.com/en-us/download/details.aspx?id=14477
-
-	# Newer:
-	# Windows Server 2008 & .NET 3.5 SDK
-	# may have broken VS9SP1? they recommend v7.0 instead, or a KB...
-	# http://www.microsoft.com/en-us/download/details.aspx?id=24826
-	_winsdk_check_microsoft_sdks_registry(v6.1 6.1.6000.16384.10)
-
-	# Included in VS 2008
-	_winsdk_check_microsoft_sdks_registry(v6.0A 6.1.6723.1)
-
-	# Microsoft Windows Software Development Kit for Windows Vista and .NET Framework 3.0 Runtime Components
-	# http://blogs.msdn.com/b/stanley/archive/2006/11/08/microsoft-windows-software-development-kit-for-windows-vista-and-net-framework-3-0-runtime-components.aspx
-	_winsdk_check_microsoft_sdks_registry(v6.0 6.0.6000.16384)
-endif()
-
-# Let's not forget the Platform SDKs, which sometimes are useful!
-if(_winsdk_msvc_greater_1200)
-	_winsdk_check_platformsdk_registry("Microsoft Platform SDK for Windows Server 2003 R2" "5.2.3790.2075.51" "D2FF9F89-8AA2-4373-8A31-C838BF4DBBE1")
-	_winsdk_check_platformsdk_registry("Microsoft Platform SDK for Windows Server 2003 SP1" "5.2.3790.1830.15" "8F9E5EF3-A9A5-491B-A889-C58EFFECE8B3")
-endif()
-###
-# Finally, look for "preferred" SDKs
-###
-if(_winsdk_msvc_greater_1310) # Newer than VS .NET/VS Toolkit 2003
-
-
-	# Environment variable for SDK dir
-	if(EXISTS "$ENV{WindowsSDKDir}" AND (NOT "$ENV{WindowsSDKDir}" STREQUAL ""))
-		_winsdk_conditional_append_preferred("WindowsSDKDir environment variable" "$ENV{WindowsSDKDir}")
-	endif()
-
-	if(_winsdk_msvc_less_1600)
-		# Per-user current Windows SDK for VS2005/2008
-		get_filename_component(_sdkdir
-			"[HKEY_CURRENT_USER\\Software\\Microsoft\\Microsoft SDKs\\Windows;CurrentInstallFolder]"
-			ABSOLUTE)
-		_winsdk_conditional_append_preferred("Per-user current Windows SDK" "${_sdkdir}")
-
-		# System-wide current Windows SDK for VS2005/2008
-		get_filename_component(_sdkdir
-			"[HKEY_LOCAL_MACHINE\\SOFTWARE\\Microsoft\\Microsoft SDKs\\Windows;CurrentInstallFolder]"
-			ABSOLUTE)
-		_winsdk_conditional_append_preferred("System-wide current Windows SDK" "${_sdkdir}")
-	endif()
-endif()
-
-
-function(windowssdk_name_lookup _dir _outvar)
-	list(FIND _win_sdk_versanddirs "${_dir}" _diridx)
-	math(EXPR _idx "${_diridx} - 1")
-	if(${_idx} GREATER -1)
-		list(GET _win_sdk_versanddirs ${_idx} _ret)
-	else()
-		set(_ret "NOTFOUND")
-	endif()
-	set(${_outvar} "${_ret}" PARENT_SCOPE)
-endfunction()
-
-function(windowssdk_build_lookup _dir _outvar)
-	list(FIND _win_sdk_buildsanddirs "${_dir}" _diridx)
-	math(EXPR _idx "${_diridx} - 1")
-	if(${_idx} GREATER -1)
-		list(GET _win_sdk_buildsanddirs ${_idx} _ret)
-	else()
-		set(_ret "NOTFOUND")
-	endif()
-	set(${_outvar} "${_ret}" PARENT_SCOPE)
-endfunction()
-
-# If we found something...
-if(_win_sdk_dirs)
-	list(GET _win_sdk_dirs 0 WINDOWSSDK_LATEST_DIR)
-	windowssdk_name_lookup("${WINDOWSSDK_LATEST_DIR}"
-		WINDOWSSDK_LATEST_NAME)
-	set(WINDOWSSDK_DIRS ${_win_sdk_dirs})
-
-	# Fallback, in case no preference found.
-	set(WINDOWSSDK_PREFERRED_DIR "${WINDOWSSDK_LATEST_DIR}")
-	set(WINDOWSSDK_PREFERRED_NAME "${WINDOWSSDK_LATEST_NAME}")
-	set(WINDOWSSDK_PREFERRED_FIRST_DIRS ${WINDOWSSDK_DIRS})
-	set(WINDOWSSDK_FOUND_PREFERENCE OFF)
-endif()
-
-# If we found indications of a user preference...
-if(_win_sdk_preferred_sdk_dirs)
-	list(GET _win_sdk_preferred_sdk_dirs 0 WINDOWSSDK_PREFERRED_DIR)
-	windowssdk_name_lookup("${WINDOWSSDK_PREFERRED_DIR}"
-		WINDOWSSDK_PREFERRED_NAME)
-	set(WINDOWSSDK_PREFERRED_FIRST_DIRS
-		${_win_sdk_preferred_sdk_dirs}
-		${_win_sdk_dirs})
-	list(REMOVE_DUPLICATES WINDOWSSDK_PREFERRED_FIRST_DIRS)
-	set(WINDOWSSDK_FOUND_PREFERENCE ON)
-endif()
-
-include(FindPackageHandleStandardArgs)
-find_package_handle_standard_args(WindowsSDK
-	"No compatible version of the Windows SDK or Platform SDK found."
-	WINDOWSSDK_DIRS)
-
-if(WINDOWSSDK_FOUND)
-	# Internal: Architecture-appropriate library directory names.
-	if("${CMAKE_VS_PLATFORM_NAME}" STREQUAL "ARM")
-		if(CMAKE_SIZEOF_VOID_P MATCHES "8")
-			# Only supported in Win10 SDK and up.
-			set(_winsdk_arch8 arm64) # what the WDK for Win8+ calls this architecture
-		else()
-			set(_winsdk_archbare /arm) # what the architecture used to be called in oldest SDKs
-			set(_winsdk_arch arm) # what the architecture used to be called
-			set(_winsdk_arch8 arm) # what the WDK for Win8+ calls this architecture
-		endif()
-	else()
-		if(CMAKE_SIZEOF_VOID_P MATCHES "8")
-			set(_winsdk_archbare /x64) # what the architecture used to be called in oldest SDKs
-			set(_winsdk_arch amd64) # what the architecture used to be called
-			set(_winsdk_arch8 x64) # what the WDK for Win8+ calls this architecture
-		else()
-			set(_winsdk_archbare ) # what the architecture used to be called in oldest SDKs
-			set(_winsdk_arch i386) # what the architecture used to be called
-			set(_winsdk_arch8 x86) # what the WDK for Win8+ calls this architecture
-		endif()
-	endif()
-
-	function(get_windowssdk_from_component _component _var)
-		get_filename_component(_component "${_component}" ABSOLUTE)
-		file(TO_CMAKE_PATH "${_component}" _component)
-		foreach(_sdkdir ${WINDOWSSDK_DIRS})
-			get_filename_component(_sdkdir "${_sdkdir}" ABSOLUTE)
-			string(LENGTH "${_sdkdir}" _sdklen)
-			file(RELATIVE_PATH _rel "${_sdkdir}" "${_component}")
-			# If we don't have any "parent directory" items...
-			if(NOT "${_rel}" MATCHES "[.][.]")
-				set(${_var} "${_sdkdir}" PARENT_SCOPE)
-				return()
-			endif()
-		endforeach()
-		# Fail.
-		set(${_var} "NOTFOUND" PARENT_SCOPE)
-	endfunction()
-	function(get_windowssdk_library_dirs _winsdk_dir _var)
-		set(_dirs)
-		set(_suffixes
-			"lib${_winsdk_archbare}" # SDKs like 7.1A
-			"lib/${_winsdk_arch}" # just because some SDKs have x86 dir and root dir
-			"lib/w2k/${_winsdk_arch}" # Win2k min requirement
-			"lib/wxp/${_winsdk_arch}" # WinXP min requirement
-			"lib/wnet/${_winsdk_arch}" # Win Server 2003 min requirement
-			"lib/wlh/${_winsdk_arch}"
-			"lib/wlh/um/${_winsdk_arch8}" # Win Vista ("Long Horn") min requirement
-			"lib/win7/${_winsdk_arch}"
-			"lib/win7/um/${_winsdk_arch8}" # Win 7 min requirement
-		)
-		foreach(_ver
-			wlh # Win Vista ("Long Horn") min requirement
-			win7 # Win 7 min requirement
-			win8 # Win 8 min requirement
-			winv6.3 # Win 8.1 min requirement
-		)
-
-			list(APPEND _suffixes
-				"lib/${_ver}/${_winsdk_arch}"
-				"lib/${_ver}/um/${_winsdk_arch8}"
-				"lib/${_ver}/km/${_winsdk_arch8}"
-			)
-		endforeach()
-
-		# Look for WDF libraries in Win10+ SDK
-		foreach(_mode umdf kmdf)
-			file(GLOB _wdfdirs RELATIVE "${_winsdk_dir}" "${_winsdk_dir}/lib/wdf/${_mode}/${_winsdk_arch8}/*")
-			if(_wdfdirs)
-				list(APPEND _suffixes ${_wdfdirs})
-			endif()
-		endforeach()
-
-		# Look in each Win10+ SDK version for the components
-		foreach(_win10ver ${_winsdk_win10vers})
-			foreach(_component um km ucrt mmos)
-				list(APPEND _suffixes "lib/${_win10ver}/${_component}/${_winsdk_arch8}")
-			endforeach()
-		endforeach()
-
-		foreach(_suffix ${_suffixes})
-			# Check to see if a library actually exists here.
-			file(GLOB _libs "${_winsdk_dir}/${_suffix}/*.lib")
-			if(_libs)
-				list(APPEND _dirs "${_winsdk_dir}/${_suffix}")
-			endif()
-		endforeach()
-		if("${_dirs}" STREQUAL "")
-			set(_dirs NOTFOUND)
-		else()
-			list(REMOVE_DUPLICATES _dirs)
-		endif()
-		set(${_var} ${_dirs} PARENT_SCOPE)
-	endfunction()
-	function(get_windowssdk_include_dirs _winsdk_dir _var)
-		set(_dirs)
-
-		set(_subdirs shared um winrt km wdf mmos ucrt)
-		set(_suffixes Include)
-
-		foreach(_dir ${_subdirs})
-			list(APPEND _suffixes "Include/${_dir}")
-		endforeach()
-
-		foreach(_ver ${_winsdk_win10vers})
-			foreach(_dir ${_subdirs})
-				list(APPEND _suffixes "Include/${_ver}/${_dir}")
-			endforeach()
-		endforeach()
-
-		foreach(_suffix ${_suffixes})
-			# Check to see if a header file actually exists here.
-			file(GLOB _headers "${_winsdk_dir}/${_suffix}/*.h")
-			if(_headers)
-				list(APPEND _dirs "${_winsdk_dir}/${_suffix}")
-			endif()
-		endforeach()
-		if("${_dirs}" STREQUAL "")
-			set(_dirs NOTFOUND)
-		else()
-			list(REMOVE_DUPLICATES _dirs)
-		endif()
-		set(${_var} ${_dirs} PARENT_SCOPE)
-	endfunction()
-	function(get_windowssdk_library_dirs_multiple _var)
-		set(_dirs)
-		foreach(_sdkdir ${ARGN})
-			get_windowssdk_library_dirs("${_sdkdir}" _current_sdk_libdirs)
-			if(_current_sdk_libdirs)
-				list(APPEND _dirs ${_current_sdk_libdirs})
-			endif()
-		endforeach()
-		if("${_dirs}" STREQUAL "")
-			set(_dirs NOTFOUND)
-		else()
-			list(REMOVE_DUPLICATES _dirs)
-		endif()
-		set(${_var} ${_dirs} PARENT_SCOPE)
-	endfunction()
-	function(get_windowssdk_include_dirs_multiple _var)
-		set(_dirs)
-		foreach(_sdkdir ${ARGN})
-			get_windowssdk_include_dirs("${_sdkdir}" _current_sdk_incdirs)
-			if(_current_sdk_libdirs)
-				list(APPEND _dirs ${_current_sdk_incdirs})
-			endif()
-		endforeach()
-		if("${_dirs}" STREQUAL "")
-			set(_dirs NOTFOUND)
-		else()
-			list(REMOVE_DUPLICATES _dirs)
-		endif()
-		set(${_var} ${_dirs} PARENT_SCOPE)
-	endfunction()
-endif()

src/cmake/Modules/GetGitRevisionDescription.cmake

@@ -3,7 +3,7 @@
 # These functions force a re-configure on each git commit so that you can
 # trust the values of the variables in your build system.
 #
-#  get_git_head_revision(<refspecvar> <hashvar> [ALLOW_LOOKING_ABOVE_CMAKE_SOURCE_DIR])
+#  get_git_head_revision(<refspecvar> <hashvar> [<additional arguments to git describe> ...])
 #
 # Returns the refspec and sha hash of the current head revision
 #
@@ -12,41 +12,26 @@
 # Returns the results of git describe on the source tree, and adjusting
 # the output so that it tests false if an error occurs.
 #
-#  git_describe_working_tree(<var> [<additional arguments to git describe> ...])
-#
-# Returns the results of git describe on the working tree (--dirty option),
-# and adjusting the output so that it tests false if an error occurs.
-#
 #  git_get_exact_tag(<var> [<additional arguments to git describe> ...])
 #
 # Returns the results of git describe --exact-match on the source tree,
 # and adjusting the output so that it tests false if there was no exact
 # matching tag.
 #
-#  git_local_changes(<var>)
-#
-# Returns either "CLEAN" or "DIRTY" with respect to uncommitted changes.
-# Uses the return code of "git diff-index --quiet HEAD --".
-# Does not regard untracked files.
-#
 # Requires CMake 2.6 or newer (uses the 'function' command)
 #
 # Original Author:
-# 2009-2020 Rylie Pavlik <rylie@ryliepavlik.com>
-# https://ryliepavlik.com/
-#
-# Copyright 2009-2013, Iowa State University.
-# Copyright 2013-2020, Rylie Pavlik
-# Copyright 2013-2020, Contributors
-#
-# SPDX-License-Identifier: BSL-1.0
+# 2009-2010 Ryan Pavlik <rpavlik@iastate.edu> <abiryan@ryand.net>
+# http://academic.cleardefinition.com
+# Iowa State University HCI Graduate Program/VRAC
 #
+# Copyright Iowa State University 2009-2010.
 # Distributed under the Boost Software License, Version 1.0.
 # (See accompanying file LICENSE_1_0.txt or copy at
 # http://www.boost.org/LICENSE_1_0.txt)
 
 if(__get_git_revision_description)
-    return()
+	return()
 endif()
 set(__get_git_revision_description YES)
 
@@ -54,234 +39,92 @@ set(__get_git_revision_description YES)
 # to find the path to this module rather than the path to a calling list file
 get_filename_component(_gitdescmoddir ${CMAKE_CURRENT_LIST_FILE} PATH)
 
-# Function _git_find_closest_git_dir finds the next closest .git directory
-# that is part of any directory in the path defined by _start_dir.
-# The result is returned in the parent scope variable whose name is passed
-# as variable _git_dir_var. If no .git directory can be found, the
-# function returns an empty string via _git_dir_var.
-#
-# Example: Given a path C:/bla/foo/bar and assuming C:/bla/.git exists and
-# neither foo nor bar contain a file/directory .git. This wil return
-# C:/bla/.git
-#
-function(_git_find_closest_git_dir _start_dir _git_dir_var)
-    set(cur_dir "${_start_dir}")
-    set(git_dir "${_start_dir}/.git")
-    while(NOT EXISTS "${git_dir}")
-        # .git dir not found, search parent directories
-        set(git_previous_parent "${cur_dir}")
-        get_filename_component(cur_dir "${cur_dir}" DIRECTORY)
-        if(cur_dir STREQUAL git_previous_parent)
-            # We have reached the root directory, we are not in git
-            set(${_git_dir_var}
-                ""
-                PARENT_SCOPE)
-            return()
-        endif()
-        set(git_dir "${cur_dir}/.git")
-    endwhile()
-    set(${_git_dir_var}
-        "${git_dir}"
-        PARENT_SCOPE)
-endfunction()
-
 function(get_git_head_revision _refspecvar _hashvar)
-    _git_find_closest_git_dir("${CMAKE_CURRENT_SOURCE_DIR}" GIT_DIR)
+	set(GIT_PARENT_DIR "${CMAKE_CURRENT_SOURCE_DIR}")
+	set(GIT_DIR "${GIT_PARENT_DIR}/.git")
+	while(NOT EXISTS "${GIT_DIR}")	# .git dir not found, search parent directories
+		set(GIT_PREVIOUS_PARENT "${GIT_PARENT_DIR}")
+		get_filename_component(GIT_PARENT_DIR ${GIT_PARENT_DIR} PATH)
+		if(GIT_PARENT_DIR STREQUAL GIT_PREVIOUS_PARENT)
+			# We have reached the root directory, we are not in git
+			set(${_refspecvar} "GITDIR-NOTFOUND" PARENT_SCOPE)
+			set(${_hashvar} "GITDIR-NOTFOUND" PARENT_SCOPE)
+			return()
+		endif()
+		set(GIT_DIR "${GIT_PARENT_DIR}/.git")
+	endwhile()
+	# check if this is a submodule
+	if(NOT IS_DIRECTORY ${GIT_DIR})
+		file(READ ${GIT_DIR} submodule)
+		string(REGEX REPLACE "gitdir: (.*)\n$" "\\1" GIT_DIR_RELATIVE ${submodule})
+		get_filename_component(SUBMODULE_DIR ${GIT_DIR} PATH)
+		get_filename_component(GIT_DIR ${SUBMODULE_DIR}/${GIT_DIR_RELATIVE} ABSOLUTE)
+	endif()
+	set(GIT_DATA "${CMAKE_CURRENT_BINARY_DIR}/CMakeFiles/git-data")
+	if(NOT EXISTS "${GIT_DATA}")
+		file(MAKE_DIRECTORY "${GIT_DATA}")
+	endif()
 
-    if("${ARGN}" STREQUAL "ALLOW_LOOKING_ABOVE_CMAKE_SOURCE_DIR")
-        set(ALLOW_LOOKING_ABOVE_CMAKE_SOURCE_DIR TRUE)
-    else()
-        set(ALLOW_LOOKING_ABOVE_CMAKE_SOURCE_DIR FALSE)
-    endif()
-    if(NOT "${GIT_DIR}" STREQUAL "")
-        file(RELATIVE_PATH _relative_to_source_dir "${CMAKE_SOURCE_DIR}"
-             "${GIT_DIR}")
-        if("${_relative_to_source_dir}" MATCHES "[.][.]"
-           AND NOT ALLOW_LOOKING_ABOVE_CMAKE_SOURCE_DIR)
-            # We've gone above the CMake root dir.
-            set(GIT_DIR "")
-        endif()
-    endif()
-    if("${GIT_DIR}" STREQUAL "")
-        set(${_refspecvar}
-            "GITDIR-NOTFOUND"
-            PARENT_SCOPE)
-        set(${_hashvar}
-            "GITDIR-NOTFOUND"
-            PARENT_SCOPE)
-        return()
-    endif()
+	if(NOT EXISTS "${GIT_DIR}/HEAD")
+		return()
+	endif()
+	set(HEAD_FILE "${GIT_DATA}/HEAD")
+	configure_file("${GIT_DIR}/HEAD" "${HEAD_FILE}" COPYONLY)
 
-    # Check if the current source dir is a git submodule or a worktree.
-    # In both cases .git is a file instead of a directory.
-    #
-    if(NOT IS_DIRECTORY ${GIT_DIR})
-        # The following git command will return a non empty string that
-        # points to the super project working tree if the current
-        # source dir is inside a git submodule.
-        # Otherwise the command will return an empty string.
-        #
-        execute_process(
-            COMMAND "${GIT_EXECUTABLE}" rev-parse
-                    --show-superproject-working-tree
-            WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
-            OUTPUT_VARIABLE out
-            ERROR_QUIET OUTPUT_STRIP_TRAILING_WHITESPACE)
-        if(NOT "${out}" STREQUAL "")
-            # If out is empty, GIT_DIR/CMAKE_CURRENT_SOURCE_DIR is in a submodule
-            file(READ ${GIT_DIR} submodule)
-            string(REGEX REPLACE "gitdir: (.*)$" "\\1" GIT_DIR_RELATIVE
-                                 ${submodule})
-            string(STRIP ${GIT_DIR_RELATIVE} GIT_DIR_RELATIVE)
-            get_filename_component(SUBMODULE_DIR ${GIT_DIR} PATH)
-            get_filename_component(GIT_DIR ${SUBMODULE_DIR}/${GIT_DIR_RELATIVE}
-                                   ABSOLUTE)
-            set(HEAD_SOURCE_FILE "${GIT_DIR}/HEAD")
-        else()
-            # GIT_DIR/CMAKE_CURRENT_SOURCE_DIR is in a worktree
-            file(READ ${GIT_DIR} worktree_ref)
-            # The .git directory contains a path to the worktree information directory
-            # inside the parent git repo of the worktree.
-            #
-            string(REGEX REPLACE "gitdir: (.*)$" "\\1" git_worktree_dir
-                                 ${worktree_ref})
-            string(STRIP ${git_worktree_dir} git_worktree_dir)
-            _git_find_closest_git_dir("${git_worktree_dir}" GIT_DIR)
-            set(HEAD_SOURCE_FILE "${git_worktree_dir}/HEAD")
-        endif()
-    else()
-        set(HEAD_SOURCE_FILE "${GIT_DIR}/HEAD")
-    endif()
-    set(GIT_DATA "${CMAKE_CURRENT_BINARY_DIR}/CMakeFiles/git-data")
-    if(NOT EXISTS "${GIT_DATA}")
-        file(MAKE_DIRECTORY "${GIT_DATA}")
-    endif()
+	configure_file("${_gitdescmoddir}/GetGitRevisionDescription.cmake.in"
+		"${GIT_DATA}/grabRef.cmake"
+		@ONLY)
+	include("${GIT_DATA}/grabRef.cmake")
 
-    if(NOT EXISTS "${HEAD_SOURCE_FILE}")
-        return()
-    endif()
-    set(HEAD_FILE "${GIT_DATA}/HEAD")
-    configure_file("${HEAD_SOURCE_FILE}" "${HEAD_FILE}" COPYONLY)
-
-    configure_file("${_gitdescmoddir}/GetGitRevisionDescription.cmake.in"
-                   "${GIT_DATA}/grabRef.cmake" @ONLY)
-    include("${GIT_DATA}/grabRef.cmake")
-
-    set(${_refspecvar}
-        "${HEAD_REF}"
-        PARENT_SCOPE)
-    set(${_hashvar}
-        "${HEAD_HASH}"
-        PARENT_SCOPE)
+	set(${_refspecvar} "${HEAD_REF}" PARENT_SCOPE)
+	set(${_hashvar} "${HEAD_HASH}" PARENT_SCOPE)
 endfunction()
 
 function(git_describe _var)
-    if(NOT GIT_FOUND)
-        find_package(Git QUIET)
-    endif()
-    get_git_head_revision(refspec hash)
-    if(NOT GIT_FOUND)
-        set(${_var}
-            "GIT-NOTFOUND"
-            PARENT_SCOPE)
-        return()
-    endif()
-    if(NOT hash)
-        set(${_var}
-            "HEAD-HASH-NOTFOUND"
-            PARENT_SCOPE)
-        return()
-    endif()
+	if(NOT GIT_FOUND)
+		find_package(Git QUIET)
+	endif()
+	get_git_head_revision(refspec hash)
+	if(NOT GIT_FOUND)
+		set(${_var} "GIT-NOTFOUND" PARENT_SCOPE)
+		return()
+	endif()
+	if(NOT hash)
+		set(${_var} "HEAD-HASH-NOTFOUND" PARENT_SCOPE)
+		return()
+	endif()
 
-    # TODO sanitize
-    #if((${ARGN}" MATCHES "&&") OR
-    #	(ARGN MATCHES "||") OR
-    #	(ARGN MATCHES "\\;"))
-    #	message("Please report the following error to the project!")
-    #	message(FATAL_ERROR "Looks like someone's doing something nefarious with git_describe! Passed arguments ${ARGN}")
-    #endif()
+	# TODO sanitize
+	#if((${ARGN}" MATCHES "&&") OR
+	#	(ARGN MATCHES "||") OR
+	#	(ARGN MATCHES "\\;"))
+	#	message("Please report the following error to the project!")
+	#	message(FATAL_ERROR "Looks like someone's doing something nefarious with git_describe! Passed arguments ${ARGN}")
+	#endif()
 
-    #message(STATUS "Arguments to execute_process: ${ARGN}")
+	#message(STATUS "Arguments to execute_process: ${ARGN}")
 
-    execute_process(
-        COMMAND "${GIT_EXECUTABLE}" describe --tags --always ${hash} ${ARGN}
-        WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
-        RESULT_VARIABLE res
-        OUTPUT_VARIABLE out
-        ERROR_QUIET OUTPUT_STRIP_TRAILING_WHITESPACE)
-    if(NOT res EQUAL 0)
-        set(out "${out}-${res}-NOTFOUND")
-    endif()
+	execute_process(COMMAND
+		"${GIT_EXECUTABLE}"
+		describe
+		${hash}
+		${ARGN}
+		WORKING_DIRECTORY
+		"${CMAKE_SOURCE_DIR}"
+		RESULT_VARIABLE
+		res
+		OUTPUT_VARIABLE
+		out
+		ERROR_QUIET
+		OUTPUT_STRIP_TRAILING_WHITESPACE)
+	if(NOT res EQUAL 0)
+		set(out "${out}-${res}-NOTFOUND")
+	endif()
 
-    set(${_var}
-        "${out}"
-        PARENT_SCOPE)
-endfunction()
-
-function(git_describe_working_tree _var)
-    if(NOT GIT_FOUND)
-        find_package(Git QUIET)
-    endif()
-    if(NOT GIT_FOUND)
-        set(${_var}
-            "GIT-NOTFOUND"
-            PARENT_SCOPE)
-        return()
-    endif()
-
-    execute_process(
-        COMMAND "${GIT_EXECUTABLE}" describe --dirty ${ARGN}
-        WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
-        RESULT_VARIABLE res
-        OUTPUT_VARIABLE out
-        ERROR_QUIET OUTPUT_STRIP_TRAILING_WHITESPACE)
-    if(NOT res EQUAL 0)
-        set(out "${out}-${res}-NOTFOUND")
-    endif()
-
-    set(${_var}
-        "${out}"
-        PARENT_SCOPE)
+	set(${_var} "${out}" PARENT_SCOPE)
 endfunction()
 
 function(git_get_exact_tag _var)
-    git_describe(out --exact-match ${ARGN})
-    set(${_var}
-        "${out}"
-        PARENT_SCOPE)
-endfunction()
-
-function(git_local_changes _var)
-    if(NOT GIT_FOUND)
-        find_package(Git QUIET)
-    endif()
-    get_git_head_revision(refspec hash)
-    if(NOT GIT_FOUND)
-        set(${_var}
-            "GIT-NOTFOUND"
-            PARENT_SCOPE)
-        return()
-    endif()
-    if(NOT hash)
-        set(${_var}
-            "HEAD-HASH-NOTFOUND"
-            PARENT_SCOPE)
-        return()
-    endif()
-
-    execute_process(
-        COMMAND "${GIT_EXECUTABLE}" diff-index --quiet HEAD --
-        WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
-        RESULT_VARIABLE res
-        OUTPUT_VARIABLE out
-        ERROR_QUIET OUTPUT_STRIP_TRAILING_WHITESPACE)
-    if(res EQUAL 0)
-        set(${_var}
-            "CLEAN"
-            PARENT_SCOPE)
-    else()
-        set(${_var}
-            "DIRTY"
-            PARENT_SCOPE)
-    endif()
+	git_describe(out --exact-match ${ARGN})
+	set(${_var} "${out}" PARENT_SCOPE)
 endfunction()

src/cmake/Modules/GetGitRevisionDescription.cmake.in

@@ -1,21 +1,17 @@
-#
+# 
 # Internal file for GetGitRevisionDescription.cmake
 #
 # Requires CMake 2.6 or newer (uses the 'function' command)
 #
 # Original Author:
-# 2009-2023 Rylie Pavlik <rylie@ryliepavlik.com>
-# https://ryliepavlik.com/
+# 2009-2010 Ryan Pavlik <rpavlik@iastate.edu> <abiryan@ryand.net>
+# http://academic.cleardefinition.com
 # Iowa State University HCI Graduate Program/VRAC
 #
-# Copyright 2009-2012, Iowa State University
-# Copyright 2011-2023, Contributors
-#
+# Copyright Iowa State University 2009-2010.
 # Distributed under the Boost Software License, Version 1.0.
 # (See accompanying file LICENSE_1_0.txt or copy at
 # http://www.boost.org/LICENSE_1_0.txt)
-#
-# SPDX-License-Identifier: BSL-1.0
 
 set(HEAD_HASH)
 
@@ -23,26 +19,20 @@ file(READ "@HEAD_FILE@" HEAD_CONTENTS LIMIT 1024)
 
 string(STRIP "${HEAD_CONTENTS}" HEAD_CONTENTS)
 if(HEAD_CONTENTS MATCHES "ref")
-    # named branch
-    string(REPLACE "ref: " "" HEAD_REF "${HEAD_CONTENTS}")
-    if(EXISTS "@GIT_DIR@/${HEAD_REF}")
-        configure_file("@GIT_DIR@/${HEAD_REF}" "@GIT_DATA@/head-ref" COPYONLY)
-    else()
-        if(EXISTS "@GIT_DIR@/packed-refs")
-            configure_file("@GIT_DIR@/packed-refs" "@GIT_DATA@/packed-refs"
-                           COPYONLY)
-            file(READ "@GIT_DATA@/packed-refs" PACKED_REFS)
-            if(${PACKED_REFS} MATCHES "([0-9a-z]*) ${HEAD_REF}")
-                set(HEAD_HASH "${CMAKE_MATCH_1}")
-            endif()
-        endif()
-    endif()
+	# named branch
+	string(REPLACE "ref: " "" HEAD_REF "${HEAD_CONTENTS}")
+	if(EXISTS "@GIT_DIR@/${HEAD_REF}")
+		configure_file("@GIT_DIR@/${HEAD_REF}" "@GIT_DATA@/head-ref" COPYONLY)
+	elseif(EXISTS "@GIT_DIR@/logs/${HEAD_REF}")
+		configure_file("@GIT_DIR@/logs/${HEAD_REF}" "@GIT_DATA@/head-ref" COPYONLY)
+		set(HEAD_HASH "${HEAD_REF}")
+	endif()
 else()
-    # detached HEAD
-    configure_file("@GIT_DIR@/HEAD" "@GIT_DATA@/head-ref" COPYONLY)
+	# detached HEAD
+	configure_file("@GIT_DIR@/HEAD" "@GIT_DATA@/head-ref" COPYONLY)
 endif()
 
 if(NOT HEAD_HASH)
-    file(READ "@GIT_DATA@/head-ref" HEAD_HASH LIMIT 1024)
-    string(STRIP "${HEAD_HASH}" HEAD_HASH)
+	file(READ "@GIT_DATA@/head-ref" HEAD_HASH LIMIT 1024)
+	string(STRIP "${HEAD_HASH}" HEAD_HASH)
 endif()

src/cmake/Modules/README.md

@@ -1,14 +0,0 @@
-# CMake modules required for building Lean
-
-The files `GetGitRevisionDescription.cmake`, `GetGitRevisionDescription.cmake.in` and
-`FindWindowsSDK.cmake` are part of the `cmake-modules` project by Rylie Pavlik. They
-are licensed under the Boost Software License, Version 1.0.
-
-The modules should be updated when a new version of the Windows SDK is released. To do
-so, obtain an up-to-date checkout of the `cmake-modules` project from
-https://github.com/rpavlik/cmake-modules and run the following command from the root
-of the `cmake-modules` repository:
-
-```bash
-./update-modules.sh /path-to-lean4-repo/src/cmake/Modules
-```

src/lake/Lake/Util/Log.lean

@@ -292,7 +292,7 @@ instance : Append Log := ⟨Log.append⟩
 
 /-- Removes log entries after `pos` (inclusive). -/
 @[inline] def dropFrom (log : Log) (pos : Log.Pos) : Log :=
-  .mk <| log.entries.take pos.val
+  .mk <| log.entries.shrink pos.val
 
 /-- Takes log entries before `pos` (exclusive). -/
 @[inline] def takeFrom (log : Log) (pos : Log.Pos) : Log :=

tests/bench/big_do.lean

@@ -1,459 +0,0 @@
-/-!
-This benchmark exercises
-* general elaboration, likely from many nested lambdas
-* code generation, ditto
--/
-
-set_option maxRecDepth 10000
-
-def addALot (x: Nat) : StateM Nat Nat := do
-  set x
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  modifyGet (λ y => ((), y + x))
-  let y <- get
-  pure y
-
-#eval StateT.run' (addALot 2) 0

tests/bench/big_omega.lean

@@ -1,40 +0,0 @@
-/-!
-This benchmark exercises `omega` in a way that creates a big proof, exercising `instantiateMVars`
-and `shareCommonPreDefs` as well. In particular, running it with `internal.cmdlineSnapshots=false`,
-like the language server does, uncovered a significant slowdown in `instantiateMVars` (#5614).
--/
-
-set_option maxHeartbeats 0
-theorem memcpy_extracted_2 (six0 s0x0 : BitVec 64)
-(h_six0_nonzero : six0 ≠ 0)
-(h_s0x1 : s0x1 + 16#64 * (s0x0 - six0) + 16#64 = s0x1 + 16#64 * (s0x0 - (six0 - 1#64)))
-(h_s0x2 : s0x2 + 16#64 * (s0x0 - six0) + 16#64 = s0x2 + 16#64 * (s0x0 - (six0 - 1#64)))
-(h_assert_1 : six0 ≤ s0x0)
-(h_assert_3 : six1 = s0x1 + 16#64 * (s0x0 - six0))
-(h_assert_4 : six2 = s0x2 + 16#64 * (s0x0 - six0))
-(n : Nat)
-(addr : BitVec 64)
-(h_le : (s0x0 - (six0 - 1#64)).toNat ≤ s0x0.toNat)
-(h_upper_bound : addr.toNat + n ≤ 2 ^ 64)
-(h_upper_bound₂ : s0x2.toNat + s0x0.toNat * 16 ≤ 2 ^ 64)
-(h_upper_bound₃ : s0x2.toNat + (16#64 * (s0x0 - (six0 - 1#64))).toNat ≤ 2 ^ 64)
-(h_width_lt : (16#64).toNat * (s0x0 - (six0 - 1#64)).toNat < 2 ^ 64)
-(hmemSeparate_omega : s0x1.toNat + s0x0.toNat * 16 ≤ 2 ^ 64 ∧
-  s0x2.toNat + s0x0.toNat * 16 ≤ 2 ^ 64 ∧
-    (s0x1.toNat + s0x0.toNat * 16 ≤ s0x2.toNat ∨ s0x1.toNat ≥ s0x2.toNat + s0x0.toNat * 16))
-(hmemLegal_omega : s0x1.toNat + s0x0.toNat * 16 ≤ 2 ^ 64)
-(hmemLegal_omega : s0x2.toNat + s0x0.toNat * 16 ≤ 2 ^ 64)
-(hmemSeparate_omega : s0x2.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - (2 ^ 64 - 1 % 2 ^ 64 + six0.toNat) % 2 ^ 64 + s0x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤
-    2 ^ 64 ∧
-  addr.toNat + n ≤ 2 ^ 64 ∧
-    (s0x2.toNat +
-          16 % 2 ^ 64 * ((2 ^ 64 - (2 ^ 64 - 1 % 2 ^ 64 + six0.toNat) % 2 ^ 64 + s0x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤
-        addr.toNat ∨
-      s0x2.toNat ≥ addr.toNat + n))
-(hmemLegal_omega : s0x2.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - (2 ^ 64 - 1 % 2 ^ 64 + six0.toNat) % 2 ^ 64 + s0x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤
-  2 ^ 64)
-(hmemLegal_omega : addr.toNat + n ≤ 2 ^ 64) :
- s0x2.toNat + (16#64 * (s0x0 - six0)).toNat ≤ 2 ^ 64 ∧
-  addr.toNat + n ≤ 2 ^ 64 ∧
-    (s0x2.toNat + (16#64 * (s0x0 - six0)).toNat ≤ addr.toNat ∨ s0x2.toNat ≥ addr.toNat + n) := by
-    bv_omega

tests/bench/speedcenter.exec.velcom.yaml

@@ -362,21 +362,3 @@
   run_config:
     <<: *time
     cmd: lean bv_decide_inequality.lean
-- attributes:
-    description: big_do
-    tags: [fast]
-  run_config:
-    <<: *time
-    cmd: lean big_do.lean
-- attributes:
-    description: big_omega.lean
-    tags: [fast]
-  run_config:
-    <<: *time
-    cmd: lean big_omega.lean
-- attributes:
-    description: big_omega.lean MT
-    tags: [fast]
-  run_config:
-    <<: *time
-    cmd: lean big_omega.lean -Dinternal.cmdlineSnapshots=false

tests/lean/delabOverApp.lean.expected.out

@@ -3,4 +3,4 @@ f +' g : Nat → Nat
 f * g : Nat → Nat
 (f * g) 1 : Nat
 mul f g : Nat → Nat
-mul f g (@OfNat.ofNat Nat 1 (instOfNatNat 1)) : Nat
+mul f g 1 : Nat

tests/lean/interactive/completion2.lean.expected.out

@@ -3,7 +3,7 @@
 {"items":
  [{"sortText": "0",
    "label": "ax1",
-   "kind": 23,
+   "kind": 3,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completion2.lean"},
@@ -11,7 +11,7 @@
     "id": {"const": {"declName": "Foo.Bla.ax1"}}}},
   {"sortText": "1",
    "label": "ex1",
-   "kind": 23,
+   "kind": 3,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completion2.lean"},
@@ -19,7 +19,7 @@
     "id": {"const": {"declName": "Foo.Bla.ex1"}}}},
   {"sortText": "2",
    "label": "ex2",
-   "kind": 23,
+   "kind": 3,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completion2.lean"},
@@ -27,7 +27,7 @@
     "id": {"const": {"declName": "Foo.Bla.ex2"}}}},
   {"sortText": "3",
    "label": "ex3",
-   "kind": 23,
+   "kind": 3,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completion2.lean"},
@@ -39,7 +39,7 @@
 {"items":
  [{"sortText": "0",
    "label": "ax1",
-   "kind": 23,
+   "kind": 3,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completion2.lean"},
@@ -47,7 +47,7 @@
     "id": {"const": {"declName": "Foo.Bla.ax1"}}}},
   {"sortText": "1",
    "label": "ex1",
-   "kind": 23,
+   "kind": 3,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completion2.lean"},
@@ -55,7 +55,7 @@
     "id": {"const": {"declName": "Foo.Bla.ex1"}}}},
   {"sortText": "2",
    "label": "ex2",
-   "kind": 23,
+   "kind": 3,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completion2.lean"},
@@ -63,7 +63,7 @@
     "id": {"const": {"declName": "Foo.Bla.ex2"}}}},
   {"sortText": "3",
    "label": "ex3",
-   "kind": 23,
+   "kind": 3,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completion2.lean"},
@@ -75,7 +75,7 @@
 {"items":
  [{"sortText": "0",
    "label": "ax1",
-   "kind": 23,
+   "kind": 3,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completion2.lean"},
@@ -83,7 +83,7 @@
     "id": {"const": {"declName": "Foo.Bla.ax1"}}}},
   {"sortText": "1",
    "label": "ex1",
-   "kind": 23,
+   "kind": 3,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completion2.lean"},
@@ -91,7 +91,7 @@
     "id": {"const": {"declName": "Foo.Bla.ex1"}}}},
   {"sortText": "2",
    "label": "ex2",
-   "kind": 23,
+   "kind": 3,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completion2.lean"},
@@ -99,7 +99,7 @@
     "id": {"const": {"declName": "Foo.Bla.ex2"}}}},
   {"sortText": "3",
    "label": "ex3",
-   "kind": 23,
+   "kind": 3,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completion2.lean"},
@@ -111,7 +111,7 @@
 {"items":
  [{"sortText": "0",
    "label": "ex1",
-   "kind": 23,
+   "kind": 3,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completion2.lean"},
@@ -119,7 +119,7 @@
     "id": {"const": {"declName": "Foo.Bla.ex1"}}}},
   {"sortText": "1",
    "label": "ex2",
-   "kind": 23,
+   "kind": 3,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completion2.lean"},
@@ -127,7 +127,7 @@
     "id": {"const": {"declName": "Foo.Bla.ex2"}}}},
   {"sortText": "2",
    "label": "ex3",
-   "kind": 23,
+   "kind": 3,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completion2.lean"},

tests/lean/interactive/completionFallback.lean.expected.out

@@ -55,7 +55,7 @@
 {"items":
  [{"sortText": "0",
    "label": "ha",
-   "kind": 23,
+   "kind": 5,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionFallback.lean"},
@@ -63,7 +63,7 @@
     "id": {"const": {"declName": "CustomAnd.ha"}}}},
   {"sortText": "1",
    "label": "hb",
-   "kind": 23,
+   "kind": 5,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionFallback.lean"},

tests/lean/interactive/completionPrv.lean.expected.out

@@ -31,7 +31,7 @@
     "id": {"const": {"declName": "instToBoolBool"}}}},
   {"sortText": "2",
    "label": "BitVec.getElem_ofBoolListBE",
-   "kind": 23,
+   "kind": 3,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionPrv.lean"},
@@ -39,7 +39,7 @@
     "id": {"const": {"declName": "BitVec.getElem_ofBoolListBE"}}}},
   {"sortText": "3",
    "label": "BitVec.getLsbD_ofBoolListBE",
-   "kind": 23,
+   "kind": 3,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionPrv.lean"},
@@ -47,7 +47,7 @@
     "id": {"const": {"declName": "BitVec.getLsbD_ofBoolListBE"}}}},
   {"sortText": "4",
    "label": "BitVec.getMsbD_ofBoolListBE",
-   "kind": 23,
+   "kind": 3,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionPrv.lean"},
@@ -55,7 +55,7 @@
     "id": {"const": {"declName": "BitVec.getMsbD_ofBoolListBE"}}}},
   {"sortText": "5",
    "label": "BitVec.ofBool_and_ofBool",
-   "kind": 23,
+   "kind": 3,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionPrv.lean"},
@@ -63,7 +63,7 @@
     "id": {"const": {"declName": "BitVec.ofBool_and_ofBool"}}}},
   {"sortText": "6",
    "label": "BitVec.ofBool_or_ofBool",
-   "kind": 23,
+   "kind": 3,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionPrv.lean"},
@@ -71,7 +71,7 @@
     "id": {"const": {"declName": "BitVec.ofBool_or_ofBool"}}}},
   {"sortText": "7",
    "label": "BitVec.ofBool_xor_ofBool",
-   "kind": 23,
+   "kind": 3,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionPrv.lean"},

tests/lean/interactive/travellingCompletions.lean.expected.out

@@ -39,7 +39,7 @@
 {"items":
  [{"sortText": "0",
    "label": "continuousAdd",
-   "kind": 23,
+   "kind": 3,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///travellingCompletions.lean"},
@@ -47,7 +47,7 @@
     "id": {"const": {"declName": "Prod.continuousAdd"}}}},
   {"sortText": "1",
    "label": "continuousSMul",
-   "kind": 23,
+   "kind": 3,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///travellingCompletions.lean"},

tests/lean/run/3146.lean

@@ -1,13 +0,0 @@
-/-
-  Verifies that `let`-bodies are reduced accordingly when trying to construct default fields.
-  Fixes `#3146`
--/
-
-def Product (m₁ : Type → Type) (m₂ : Type → Type) (α : Type) := m₁ α × m₂ α
-
-instance [Monad m₁] [Monad m₂] : Monad (Product m₁ m₂) where
-  pure x := (pure x, pure x)
-  bind o f :=
-    let y₁ := do f (← o.1) |>.1
-    let y₂ := do f (← o.2) |>.2
-    (y₁, y₂)

tests/lean/run/array_simp.lean

@@ -5,19 +5,3 @@
 #check_simp #[1,2,3,4,5][2]! ~> 3
 #check_simp #[1,2,3,4,5][7]! ~> (default : Nat)
 #check_simp (#[] : Array Nat)[0]! ~> (default : Nat)
-
-attribute [local simp] Id.run in
-#check_simp
-  (Id.run do
-    let mut s := 0
-    for i in [1,2,3,4].toArray do
-      s := s + i
-    pure s) ~> 10
-
-attribute [local simp] Id.run in
-#check_simp
-  (Id.run do
-    let mut s := 0
-    for h : i in [1,2,3,4].toArray do
-      s := s + i
-    pure s) ~> 10

tests/lean/run/bv_arith.lean

@@ -45,9 +45,3 @@ theorem arith_unit_10 (x y : BitVec 8) : x % y ≤ x := by
 
 theorem arith_unit_10' (x y : BitVec 8) : x.umod y ≤ x := by
   bv_decide
-
-theorem arith_unit_11 (x y : BitVec 8) (hx : x.msb = false) (hy : y.msb = false) : x / y = x.sdiv y := by
-  bv_decide
-
-theorem arith_unit_12 (x y : BitVec 8) (hx : x.msb = false) (hy : y.msb = true) : -(x / -y) = x.sdiv y := by
-  bv_decide

tests/lean/run/bv_decide_rewriter.lean

@@ -78,7 +78,9 @@ example {x : BitVec 16} : (10 + x) + 2 = 12 + x := by bv_normalize
 example {x : BitVec 16} : (x + 10) + 2 = 12 + x := by bv_normalize
 example {x : BitVec 16} : 2 + (x + 10) = 12 + x := by bv_normalize
 example {x : BitVec 16} : 2 + (10 + x) = 12 + x := by bv_normalize
-example {x y : BitVec 1} : x.sdiv y = x &&& y := by bv_normalize
+
+
+
 
 section
 

tests/lean/run/delabProjectionApp.lean

@@ -97,9 +97,9 @@ set_option pp.explicit true
 #guard_msgs in #check x.val
 /-- info: y.val : Nat -/
 #guard_msgs in #check y.val
-/-- info: (@Fin''.toFin0 (@OfNat.ofNat Nat 5 (instOfNatNat 5)) z).val : Nat -/
+/-- info: (@Fin''.toFin0 5 z).val : Nat -/
 #guard_msgs in #check z.val
-/-- info: (@D.toA (@OfNat.ofNat Nat 5 (instOfNatNat 5)) d).x : Nat -/
+/-- info: (@D.toA 5 d).x : Nat -/
 #guard_msgs in #check d.x
 
 end

tests/lean/run/inductive_typestar.lean

@@ -1,44 +0,0 @@
-import Lean
-
-/-!
-# `inductive` and the mathlib `Type*` notation
-
-The `inductive` command interacts badly with `Type*`.
-Universe parameters that came from the `variable` command were forgotten,
-leading to parameters coming from the binder list shadowing them.
--/
-
-elab "Type*" : term => do
-  let u ← Lean.Meta.mkFreshLevelMVar
-  Lean.Elab.Term.levelMVarToParam (.sort (.succ u))
-
-section
-variable {F : Type*}
-
-/-!
-There should be three distinct level parameters.
--/
-inductive I1 (A B : Type*) (x : F) : Type
-/-- info: I1.{u_1, u_2, u_3} {F : Type u_1} (A : Type u_2) (B : Type u_3) (x : F) : Type -/
-#guard_msgs in #check I1
-
-/-!
-This was also a problem for `axiom`.
--/
-axiom ax1 (A B : Type*) (x : F) : Type
-/-- info: ax1.{u_1, u_2, u_3} {F : Type u_1} (A : Type u_2) (B : Type u_3) (x : F) : Type -/
-#guard_msgs in #check ax1
-end
-
-/-!
-Regression test: `axiom` shouldn't report "unused univeres levels" from `variable`s.
--/
-section
-variable (X : Type u)
-axiom ax2 : Nat
-end
-section
-variable (X : Type*)
-axiom ax3 : Nat
-axiom ax4 (α : Sort _) : α
-end

tests/lean/run/issue5767.lean

@@ -1,64 +0,0 @@
-axiom Std.HashMap : Type
-axiom Std.HashMap.insert : Std.HashMap → Std.HashMap
-axiom Std.HashMap.get? : Std.HashMap → Int → Option Unit
-
-structure St where
-  m : Unit
-  map : Std.HashMap
-
-opaque P : St → Prop
-
-noncomputable
-def go1 (ss : Int) (st0 : St) : Bool :=
-        let st1 := { st0 with map := st0.map.insert }
-        match st1.map.get? ss with
-        | some _ =>
-          have : P st1 := sorry
-          have : P st1 := sorry
-          go1 ss st1
-        | none => true
-      termination_by st0
-      decreasing_by sorry
-
-/--
-info: go1.induct (ss : Int) (motive : St → Prop)
-  (case1 :
-    ∀ (x : St),
-      let st1 := { m := x.m, map := x.map.insert };
-      ∀ (val : Unit), st1.map.get? ss = some val → P st1 → P st1 → motive st1 → motive x)
-  (case2 :
-    ∀ (x : St),
-      let st1 := { m := x.m, map := x.map.insert };
-      st1.map.get? ss = none → motive x)
-  (st0 : St) : motive st0
--/
-#guard_msgs in
-#check go1.induct
-
-
--- the above was the original bugreport, and a (spurious) mdata around the match
--- triggered a bug and looking through it solved it. But that would just hide it, and it
--- can be triggered like this:
-
-noncomputable
-def go2 (ss : Int) (st0 : St) : Bool :=
-        let st1 := { st0 with map := st0.map.insert }
-        id <| match st1.map.get? ss with -- the ss argument is needed
-          | some _ =>
-            have : P st1 := sorry -- both needed
-            have : P st1 := sorry -- both needed
-            go2 ss st1
-          | none => true
-      termination_by st0
-      decreasing_by sorry
-
-/--
-info: go2.induct : Int →
-  ∀ (motive : St → Prop),
-    (∀ (x : St),
-        let st1 := { m := x.m, map := x.map.insert };
-        motive st1 → motive x) →
-      ∀ (st0 : St), motive st0
--/
-#guard_msgs in
-#check @go2.induct

tests/lean/run/partialDelta.lean

@@ -1,61 +0,0 @@
-/-!
-# `partial` inhabitation with delta derivation
--/
-set_option pp.mvars false
-
-/-!
-In the following, `partial` needs to unfold the return type to find an Inhabited instance.
--/
-def MyGreatType (α : Type) := α × α
-
-partial def myLessGreatFunction (n : Nat) : MyGreatType Nat := myLessGreatFunction n
-
-
-/-!
-In the following, it needs to unfold underneath a forall.
--/
-def MyGreaterType (α : Type) := α → MyGreatType α
-
-partial def myEvenLessGreatFunction (n : Nat) : MyGreaterType Nat := myEvenLessGreatFunction n
-
-
-/-!
-Regression test: can use existing parameter.
--/
-partial def test1 (x : α) : α := test1 x
-
-/-!
-Regression test: can use Inhabited instance in parameter list.
--/
-partial def test2 [Inhabited α] (n : Nat) : α := test2 n
-
-/-!
-Regression test: can use Nonempty instance in parameter list.
--/
-partial def test3 [Nonempty α] (n : Nat) : α := test3 n
-
-/-!
-Error message.
--/
-/--
-error: failed to compile 'partial' definition 'test4', could not prove that the type
-  {α : Sort u_1} → Nat → α
-is nonempty.
-
-This process uses multiple strategies:
-- It looks for a parameter that matches the return type.
-- It tries synthesizing 'Inhabited' and 'Nonempty' instances for the return type, while making every parameter into a local 'Inhabited' instance.
-- It tries unfolding the return type.
-
-If the return type is defined using the 'structure' or 'inductive' command, you can try adding a 'deriving Nonempty' clause to it.
--/
-#guard_msgs in partial def test4 (n : Nat) : α := test4 n
-
-/-!
-Add arguments as inhabited instances.
-Example adapted from https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Why.20return.20type.20of.20partial.20function.20MUST.20.60inhabited.60.3F/near/477905312
--/
-inductive ListNode where
-  | mk : Nat → Option ListNode → ListNode
-
-partial def checkMyList (head : ListNode) : Bool × ListNode := checkMyList head

tests/lean/run/treeNode.lean

@@ -14,7 +14,7 @@ def treeToList (t : TreeNode) : List String :=
    return r
 
 @[simp] theorem treeToList_eq (name : String) (children : List TreeNode) : treeToList (.mkNode name children) =  name :: List.join (children.map treeToList) := by
-  simp only [treeToList, Id.run, Id.pure_eq, Id.bind_eq, List.forIn'_eq_forIn, forIn, List.forIn]
+  simp [treeToList, Id.run, forIn, List.forIn]
   have : ∀ acc, (Id.run do List.forIn.loop (fun a b => ForInStep.yield (b ++ treeToList a)) children acc) = acc ++ List.join (List.map treeToList children) := by
     intro acc
     induction children generalizing acc with simp [List.forIn.loop, List.map, List.join, Id.run]

tests/lean/run/unfoldTactic.lean

@@ -93,15 +93,3 @@ example : let x := 1; let y := 2; x + y = y + x := by
   conv => unfold x
   guard_target =ₛ 1 + y = y + 1
   rfl
-
-/-!
-Error: not a local definition
--/
-
-/-- error: tactic 'unfold' failed, local variable 'x' has no definition -/
-#guard_msgs in example (x : Nat) : x + 1 = 1 := by
-  unfold x
-
-  /-- error: conv tactic 'unfold' failed, local variable 'x' has no definition -/
-#guard_msgs in example (x : Nat) : x + 1 = 1 := by
-  conv => unfold x

tests/lean/rwWithSynthesizeBug.lean.expected.out

@@ -1,4 +1,4 @@
 rwWithSynthesizeBug.lean:36:18-39:15: error: unsolved goals
-inst : Bar Nat := @Bar.mk Nat (@OfNat.ofNat Nat 0 (instOfNatNat 0))
-h : @w Nat (@f Nat inst (@OfNat.ofNat Nat 5 (instOfNatNat 5)))
+inst : Bar Nat := @Bar.mk Nat 0
+h : @w Nat (@f Nat inst 5)
 ⊢ True

tests/lean/sanitychecks.lean.expected.out

@@ -12,15 +12,6 @@ sanitychecks.lean:10:0-10:23: error: failed to synthesize
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 sanitychecks.lean:18:12-18:20: error: invalid use of 'partial', 'Foo.unsound3' is not a function
   False
-sanitychecks.lean:20:0-20:54: error: failed to compile 'partial' definition 'Foo.unsound4', could not prove that the type
-  Unit → False
-is nonempty.
-
-This process uses multiple strategies:
-- It looks for a parameter that matches the return type.
-- It tries synthesizing 'Inhabited' and 'Nonempty' instances for the return type, while making every parameter into a local 'Inhabited' instance.
-- It tries unfolding the return type.
-
-If the return type is defined using the 'structure' or 'inductive' command, you can try adding a 'deriving Nonempty' clause to it.
+sanitychecks.lean:20:0-20:54: error: failed to compile partial definition 'Foo.unsound4', failed to show that type is inhabited and non empty
 sanitychecks.lean:22:12-22:20: error: (kernel) invalid declaration, it uses unsafe declaration 'unsafeCast'
 sanitychecks.lean:25:12-25:20: error: (kernel) invalid declaration, it uses unsafe declaration 'unsafeCast'

tests/lean/unfoldFailure.lean.expected.out

@@ -1,4 +1,4 @@
-unfoldFailure.lean:2:9-2:16: error: tactic 'unfold' failed to unfold 'Nat.add' at
+unfoldFailure.lean:2:2-2:16: error: tactic 'unfold' failed to unfold 'Nat.add' at
   True
-unfoldFailure.lean:5:9-5:16: error: tactic 'unfold' failed to unfold 'Nat.add' at
+unfoldFailure.lean:5:2-5:21: error: tactic 'unfold' failed to unfold 'Nat.add' at
   x = 2 * y

tests/playground/parser/parser.lean

@@ -64,7 +64,7 @@ d.errorMsg != none
 d.stxStack.size
 
 def ParserData.restore (d : ParserData) (iniStackSz : Nat) (iniPos : Nat) : ParserData :=
-{ stxStack := d.stxStack.take iniStackSz, errorMsg := none, pos := iniPos, .. d}
+{ stxStack := d.stxStack.shrink iniStackSz, errorMsg := none, pos := iniPos, .. d}
 
 def ParserData.setPos (d : ParserData) (pos : Nat) : ParserData :=
 { pos := pos, .. d }
@@ -75,8 +75,8 @@ def ParserData.setCache (d : ParserData) (cache : ParserCache) : ParserData :=
 def ParserData.pushSyntax (d : ParserData) (n : Syntax) : ParserData :=
 { stxStack := d.stxStack.push n, .. d }
 
-def ParserData.takeStack (d : ParserData) (iniStackSz : Nat) : ParserData :=
-{ stxStack := d.stxStack.take iniStackSz, .. d }
+def ParserData.shrinkStack (d : ParserData) (iniStackSz : Nat) : ParserData :=
+{ stxStack := d.stxStack.shrink iniStackSz, .. d }
 
 def ParserData.next (d : ParserData) (s : String) (pos : Nat) : ParserData :=
 { pos := s.next pos, .. d }
@@ -114,7 +114,7 @@ match d with
     d
   else
     let newNode := Syntax.node k (stack.extract iniStackSz stack.size) [] in
-    let stack   := stack.take iniStackSz in
+    let stack   := stack.shrink iniStackSz in
     let stack   := stack.push newNode in
     ⟨stack, pos, cache, err⟩
 
@@ -144,7 +144,7 @@ match d with
   let iniSz  := d.stackSize in
   let iniPos := d.pos in
   match p s d with
-  | ⟨stack, _, cache, some msg⟩ := ⟨stack.take iniSz, iniPos, cache, some msg⟩
+  | ⟨stack, _, cache, some msg⟩ := ⟨stack.shrink iniSz, iniPos, cache, some msg⟩
   | other                       := other
 
 @[noinline] def noFirstTokenInfo (info : ParserInfo) : ParserInfo :=
@@ -516,15 +516,15 @@ partial def identFnAux (startPos : Nat) (tk : Option TokenConfig) : Name → Par
 
 def ParserData.keepNewError (d : ParserData) (oldStackSize : Nat) : ParserData :=
 match d with
-| ⟨stack, pos, cache, err⟩ := ⟨stack.take oldStackSize, pos, cache, err⟩
+| ⟨stack, pos, cache, err⟩ := ⟨stack.shrink oldStackSize, pos, cache, err⟩
 
 def ParserData.keepPrevError (d : ParserData) (oldStackSize : Nat) (oldStopPos : String.Pos) (oldError : Option String) : ParserData :=
 match d with
-| ⟨stack, _, cache, _⟩ := ⟨stack.take oldStackSize, oldStopPos, cache, oldError⟩
+| ⟨stack, _, cache, _⟩ := ⟨stack.shrink oldStackSize, oldStopPos, cache, oldError⟩
 
 def ParserData.mergeErrors (d : ParserData) (oldStackSize : Nat) (oldError : String) : ParserData :=
 match d with
-| ⟨stack, pos, cache, some err⟩ := ⟨stack.take oldStackSize, pos, cache, some (err ++ "; " ++ oldError)⟩
+| ⟨stack, pos, cache, some err⟩ := ⟨stack.shrink oldStackSize, pos, cache, some (err ++ "; " ++ oldError)⟩
 | other                         := other
 
 def ParserData.mkLongestNodeAlt (d : ParserData) (startSize : Nat) : ParserData :=
@@ -535,14 +535,14 @@ match d with
   else
     -- parser created more than one node, combine them into a single node
     let node := Syntax.node nullKind (stack.extract startSize stack.size) [] in
-    let stack := stack.take startSize in
+    let stack := stack.shrink startSize in
     ⟨stack.push node, pos, cache, none⟩
 
 def ParserData.keepLatest (d : ParserData) (startStackSize : Nat) : ParserData :=
 match d with
 | ⟨stack, pos, cache, _⟩ :=
   let node  := stack.back in
-  let stack := stack.take startStackSize in
+  let stack := stack.shrink startStackSize in
   let stack := stack.push node in
   ⟨stack, pos, cache, none⟩
 
@@ -591,7 +591,7 @@ def longestMatchFn₂ (p q : ParserFn) : ParserFn :=
 let startSize := d.stackSize in
 let startPos  := d.pos in
 let d         := p s d in
-let d         := if d.hasError then d.takeStack startSize else d.mkLongestNodeAlt startSize in
+let d         := if d.hasError then d.shrinkStack startSize else d.mkLongestNodeAlt startSize in
 let d         := longestMatchStep startSize startPos q s d in
 longestMatchMkResult startSize d
 
@@ -603,7 +603,7 @@ def longestMatchFn : List ParserFn → ParserFn
   let startPos  := d.pos in
   let d         := p s d in
   if d.hasError then
-    let d := d.takeStack startSize in
+    let d := d.shrinkStack startSize in
     longestMatchFnAux startSize startPos ps s d
   else
     let d := d.mkLongestNodeAlt startSize in