chore: minor fixes in Array lemmas

Closes #3146

Reduction doesn't trigger correctly on the bodies of `let`-expressions
in `StructInst`, leading some meta-variables to linger in the terms of
some fields. Because of this, default fields may try multiple times (and
fail) to be generated, leading to an unexpected error.

The solution implemented here is to modify the values of the introduced
variables in the local context so as to reduce them correctly.

.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-*/source/src/build/ ./push-test; false)
+          nix build --keep-failed $NIX_BUILD_ARGS .#test -o push-test || (ln -s /tmp/nix-build-*/build/source/src/build ./push-test; false)
       - name: Test Summary
         uses: test-summary/action@v2
         with:

doc/make/msys2.md

@@ -15,6 +15,13 @@ 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 10+
+* x86-64 Windows 11 (any version), Windows 10 (version 1903 or higher), Windows Server 2022
 
 ### Tier 2
 

script/prepare-llvm-mingw.sh

@@ -31,14 +31,20 @@ cp /clang64/lib/{crtbegin,crtend,crt2,dllcrt2}.o stage1/lib/
 # runtime
 (cd llvm; cp --parents lib/clang/*/lib/*/libclang_rt.builtins* ../stage1)
 # further dependencies
-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/
+# 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/
 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
+# when not using the above flags, link GMP dynamically/as usual. Always link ICU dynamically.
 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,6 +297,23 @@ 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)
@@ -480,7 +497,7 @@ endif()
 # Git HASH
 if(USE_GITHASH)
   include(GetGitRevisionDescription)
-  get_git_head_revision(GIT_REFSPEC GIT_SHA1)
+  get_git_head_revision(GIT_REFSPEC GIT_SHA1 ALLOW_LOOKING_ABOVE_CMAKE_SOURCE_DIR)
   if(${GIT_SHA1} MATCHES "GITDIR-NOTFOUND")
     message(STATUS "Failed to read git_sha1")
     set(GIT_SHA1 "")

src/Init/Control/StateRef.lean

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

src/Init/Data/Array/Basic.lean

@@ -241,12 +241,15 @@ def swapAt! (a : Array α) (i : Nat) (v : α) : α × Array α :=
     have : Inhabited (α × Array α) := ⟨(v, a)⟩
     panic! ("index " ++ toString i ++ " out of bounds")
 
-def shrink (a : Array α) (n : Nat) : Array α :=
+/-- `take a n` returns the first `n` elements of `a`. -/
+def take (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

src/Init/Data/Array/Lemmas.lean

@@ -9,6 +9,7 @@ import Init.Data.List.Impl
 import Init.Data.List.Monadic
 import Init.Data.List.Range
 import Init.Data.List.Nat.TakeDrop
+import Init.Data.List.Nat.Modify
 import Init.Data.Array.Mem
 import Init.TacticsExtra
 
@@ -101,6 +102,25 @@ 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
+
 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]
@@ -169,6 +189,9 @@ namespace Array
 
 @[simp] theorem size_mk (as : List α) : (Array.mk as).size = as.length := by simp [size]
 
+@[simp] theorem isEmpty_toList {l : Array α} : l.toList.isEmpty = l.isEmpty := by
+  rcases l with ⟨_ | _⟩ <;> simp
+
 theorem foldrM_push [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) :
     (arr.push a).foldrM f init = f a init >>= arr.foldrM f := by
   simp [foldrM_eq_reverse_foldlM_toList, -size_push]
@@ -671,6 +694,40 @@ 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
+
 /-! ### foldl / foldr -/
 
 @[simp] theorem foldlM_loop_empty [Monad m] (f : β → α → m β) (init : β) (i j : Nat) :
@@ -851,6 +908,12 @@ theorem getElem_modify {as : Array α} {x i} (h : i < (as.modify x f).size) :
   · simp only [Id.bind_eq, get_set _ _ _ (by simpa using h)]; split <;> simp [*]
   · rw [if_neg (mt (by rintro rfl; exact h) (by simp_all))]
 
+@[simp] theorem toList_modify (as : Array α) (f : α → α) :
+    (as.modify x f).toList = as.toList.modify f x := by
+  apply List.ext_getElem
+  · simp
+  · simp [getElem_modify, List.getElem_modify]
+
 theorem getElem_modify_self {as : Array α} {i : Nat} (f : α → α) (h : i < (as.modify i f).size) :
     (as.modify i f)[i] = f (as[i]'(by simpa using h)) := by
   simp [getElem_modify h]
@@ -958,18 +1021,38 @@ theorem getElem_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle :
   conv => rhs; rw [← List.getElem_append_right (h₁ := hle) (h₂ := h')]
   apply List.get_of_eq; rw [toList_append]
 
+theorem getElem?_append_left {as bs : Array α} {n : Nat} (hn : n < as.size) :
+    (as ++ bs)[n]? = as[n]? := by
+  have hn' : n < (as ++ bs).size := Nat.lt_of_lt_of_le hn <|
+    size_append .. ▸ Nat.le_add_right ..
+  simp_all [getElem?_eq_getElem, getElem_append]
+
+theorem getElem?_append_right {as bs : Array α} {n : Nat} (h : as.size ≤ n) :
+    (as ++ bs)[n]? = bs[n - as.size]? := by
+  cases as
+  cases bs
+  simp at h
+  simp [List.getElem?_append_right, h]
+
+theorem getElem?_append {as bs : Array α} {n : Nat} :
+    (as ++ bs)[n]? = if n < as.size then as[n]? else bs[n - as.size]? := by
+  split <;> rename_i h
+  · exact getElem?_append_left h
+  · exact getElem?_append_right (by simpa using h)
+
 @[simp] theorem append_nil (as : Array α) : as ++ #[] = as := by
   apply ext'; simp only [toList_append, toList_empty, List.append_nil]
 
 @[simp] theorem nil_append (as : Array α) : #[] ++ as = as := by
   apply ext'; simp only [toList_append, toList_empty, List.nil_append]
 
-theorem append_assoc (as bs cs : Array α) : as ++ bs ++ cs = as ++ (bs ++ cs) := by
+@[simp] theorem append_assoc (as bs cs : Array α) : as ++ bs ++ cs = as ++ (bs ++ cs) := by
   apply ext'; simp only [toList_append, List.append_assoc]
 
 /-! ### flatten -/
 
-@[simp] theorem toList_flatten {l : Array (Array α)} : l.flatten.toList = (l.toList.map toList).flatten := by
+@[simp] theorem toList_flatten {l : Array (Array α)} :
+    l.flatten.toList = (l.toList.map toList).flatten := by
   dsimp [flatten]
   simp only [foldl_eq_foldl_toList]
   generalize l.toList = l
@@ -1339,6 +1422,10 @@ 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]
@@ -1433,6 +1520,11 @@ theorem all_toArray (p : α → Bool) (l : List α) : l.toArray.all p = l.all p
   apply ext'
   simp
 
+@[simp] theorem modify_toArray (f : α → α) (l : List α) :
+    l.toArray.modify i f = (l.modify f i).toArray := by
+  apply ext'
+  simp
+
 @[simp] theorem filter_toArray' (p : α → Bool) (l : List α) (h : stop = l.toArray.size) :
     l.toArray.filter p 0 stop = (l.filter p).toArray := by
   subst h

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`, `bind`, `replicate`, and
+  `map`, `filter`, `filterMap`, `foldr`, `append`, `flatten`, `pure`, `flatMap`, `replicate`, and
   `reverse`.
 * Additional functions defined in terms of these: `leftpad`, `rightPad`, and `reduceOption`.
 * Operations using indexes: `mapIdx`.
@@ -38,7 +38,7 @@ The operations are organized as follow:
 * Sublists: `take`, `drop`, `takeWhile`, `dropWhile`, `partition`, `dropLast`,
   `isPrefixOf`, `isPrefixOf?`, `isSuffixOf`, `isSuffixOf?`, `Subset`, `Sublist`,
   `rotateLeft` and `rotateRight`.
-* Manipulating elements: `replace`, `insert`, `erase`, `eraseP`, `eraseIdx`.
+* Manipulating elements: `replace`, `insert`, `modify`, `erase`, `eraseP`, `eraseIdx`.
 * Finding elements: `find?`, `findSome?`, `findIdx`, `indexOf`, `findIdx?`, `indexOf?`,
  `countP`, `count`, and `lookup`.
 * Logic: `any`, `all`, `or`, and `and`.
@@ -1119,6 +1119,35 @@ theorem replace_cons [BEq α] {a : α} :
 @[inline] protected def insert [BEq α] (a : α) (l : List α) : List α :=
   if l.elem a then l else a :: l
 
+/-! ### modify -/
+
+/--
+Apply a function to the nth tail of `l`. Returns the input without
+using `f` if the index is larger than the length of the List.
+```
+modifyTailIdx f 2 [a, b, c] = [a, b] ++ f [c]
+```
+-/
+@[simp] def modifyTailIdx (f : List α → List α) : Nat → List α → List α
+  | 0, l => f l
+  | _+1, [] => []
+  | n+1, a :: l => a :: modifyTailIdx f n l
+
+/-- Apply `f` to the head of the list, if it exists. -/
+@[inline] def modifyHead (f : α → α) : List α → List α
+  | [] => []
+  | a :: l => f a :: l
+
+@[simp] theorem modifyHead_nil (f : α → α) : [].modifyHead f = [] := by rw [modifyHead]
+@[simp] theorem modifyHead_cons (a : α) (l : List α) (f : α → α) :
+    (a :: l).modifyHead f = f a :: l := by rw [modifyHead]
+
+/--
+Apply `f` to the nth element of the list, if it exists, replacing that element with the result.
+-/
+def modify (f : α → α) : Nat → List α → List α :=
+  modifyTailIdx (modifyHead f)
+
 /-! ### erase -/
 
 /--

src/Init/Data/List/Find.lean

@@ -595,15 +595,14 @@ 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 ∃ x, x ∈ l₁ ∧ p x = true then l₁.findIdx p else l₂.findIdx p + l₁.length := by
+      if l₁.findIdx p < l₁.length 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, mem_cons, exists_eq_or_imp,
-        false_or]
+    · simp only [h, ih, cond_eq_if, Bool.false_eq_true, ↓reduceIte, add_one_lt_add_one_iff]
       split <;> simp [Nat.add_assoc]
 
 theorem IsPrefix.findIdx_le {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <+: l₂) :

src/Init/Data/List/Impl.lean

@@ -38,7 +38,7 @@ The following operations were already given `@[csimp]` replacements in `Init/Dat
 
 The following operations are given `@[csimp]` replacements below:
 `set`, `filterMap`, `foldr`, `append`, `bind`, `join`,
-`take`, `takeWhile`, `dropLast`, `replace`, `erase`, `eraseIdx`, `zipWith`,
+`take`, `takeWhile`, `dropLast`, `replace`, `modify`, `erase`, `eraseIdx`, `zipWith`,
 `enumFrom`, and `intercalate`.
 
 -/
@@ -197,6 +197,24 @@ The following operations are given `@[csimp]` replacements below:
     · simp [*]
     · intro h; rw [IH] <;> simp_all
 
+/-! ### modify -/
+
+/-- Tail-recursive version of `modify`. -/
+def modifyTR (f : α → α) (n : Nat) (l : List α) : List α := go l n #[] where
+  /-- Auxiliary for `modifyTR`: `modifyTR.go f l n acc = acc.toList ++ modify f n l`. -/
+  go : List α → Nat → Array α → List α
+  | [], _, acc => acc.toList
+  | a :: l, 0, acc => acc.toListAppend (f a :: l)
+  | a :: l, n+1, acc => go l n (acc.push a)
+
+theorem modifyTR_go_eq : ∀ l n, modifyTR.go f l n acc = acc.toList ++ modify f n l
+  | [], n => by cases n <;> simp [modifyTR.go, modify]
+  | a :: l, 0 => by simp [modifyTR.go, modify]
+  | a :: l, n+1 => by simp [modifyTR.go, modify, modifyTR_go_eq l]
+
+@[csimp] theorem modify_eq_modifyTR : @modify = @modifyTR := by
+  funext α f n l; simp [modifyTR, modifyTR_go_eq]
+
 /-! ### erase -/
 
 /-- Tail recursive version of `List.erase`. -/

src/Init/Data/List/Nat.lean

@@ -13,3 +13,4 @@ import Init.Data.List.Nat.Count
 import Init.Data.List.Nat.Erase
 import Init.Data.List.Nat.Find
 import Init.Data.List.Nat.BEq
+import Init.Data.List.Nat.Modify

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

@@ -0,0 +1,295 @@
+/-
+Copyright (c) 2014 Parikshit Khanna. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
+-/
+
+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 : α → α} :
+    (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
+
+@[simp] theorem modify_zero_cons (f : α → α) (a : α) (l : List α) :
+    (a :: l).modify f 0 = f a :: l := rfl
+
+@[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
+
+@[simp] theorem modify_eq_nil_iff (f : α → α) (n) (l : List α) :
+    l.modify f n = [] ↔ l = [] := by cases l <;> cases n <;> simp
+
+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]?
+  | n, l, 0 => by cases l <;> cases n <;> simp
+  | n, [], _+1 => by cases n <;> rfl
+  | 0, _ :: l, m+1 => by cases h : l[m]? <;> simp [h, modify, m.succ_ne_zero.symm]
+  | n+1, a :: l, m+1 => by
+    simp only [modify_succ_cons, getElem?_cons_succ, Nat.reduceEqDiff, Option.map_eq_map]
+    refine (getElem?_modify f n l m).trans ?_
+    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_modify (f : α → α) : ∀ n l, length (modify f n l) = length l :=
+  length_modifyTailIdx _ fun l => by cases l <;> rfl
+
+@[simp] theorem getElem?_modify_eq (f : α → α) (n) (l : List α) :
+    (modify f n l)[n]? = f <$> l[n]? := by
+  simp only [getElem?_modify, if_pos]
+
+@[simp] theorem getElem?_modify_ne (f : α → α) {m n} (l : List α) (h : m ≠ n) :
+    (modify f m l)[n]? = l[n]? := by
+  simp only [getElem?_modify, if_neg h, id_map']
+
+theorem getElem_modify (f : α → α) (n) (l : List α) (m) (h : m < (modify f n l).length) :
+    (modify f n l)[m] =
+      if n = m then f (l[m]'(by simp at h; omega)) else l[m]'(by simp at h; omega) := by
+  rw [getElem_eq_iff, getElem?_modify]
+  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 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) :
+    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_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,6 +187,9 @@ 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]
@@ -282,14 +285,14 @@ theorem mem_drop_iff_getElem {l : List α} {a : α} :
   · rintro ⟨i, hm, rfl⟩
     refine ⟨i, by simp; omega, by rw [getElem_drop]⟩
 
-theorem head?_drop (l : List α) (n : Nat) :
+@[simp] theorem head?_drop (l : List α) (n : Nat) :
     (l.drop n).head? = l[n]? := by
   rw [head?_eq_getElem?, getElem?_drop, Nat.add_zero]
 
-theorem head_drop {l : List α} {n : Nat} (h : l.drop n ≠ []) :
+@[simp] 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
-  simpa [getElem?_eq_getElem, h, w, head_eq_iff_head?_eq_some] using head?_drop l n
+  simp [getElem?_eq_getElem, h, w, head_eq_iff_head?_eq_some]
 
 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]
@@ -300,7 +303,7 @@ theorem getLast?_drop {l : List α} : (l.drop n).getLast? = if l.length ≤ n th
     congr
     omega
 
-theorem getLast_drop {l : List α} (h : l.drop n ≠ []) :
+@[simp] 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
@@ -449,6 +452,26 @@ 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,9 +4,7 @@ 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/Repr.lean

@@ -5,10 +5,6 @@ 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,7 +6,6 @@ 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,14 +4,9 @@ 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.Int.Basic
-import Init.Data.Format.Basic
-import Init.Control.Id
-import Init.Control.Option
+import Init.Data.Option.Basic
+
 open Sum Subtype Nat
 
 open Std

src/Init/GetElem.lean

@@ -144,22 +144,26 @@ 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) [Decidable (dom c i)] : c[i]? = some (c[i]'h) := by
+    (c : cont) (i : idx) (h : dom c i) : c[i]? = some (c[i]'h) := by
+  have : Decidable (dom c i) := .isTrue h
   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) [Decidable (dom c i)] : c[i]? = none := by
+    (c : cont) (i : idx) (h : ¬dom c i) : c[i]? = none := by
+  have : Decidable (dom c i) := .isFalse h
   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) [Decidable (dom c i)] :
+    [Inhabited elem] (c : cont) (i : idx) (h : 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) [Decidable (dom c i)] : c[i]! = default := by
+    [Inhabited elem] (c : cont) (i : idx) (h : ¬dom c i) : c[i]! = default := by
+  have : Decidable (dom c i) := .isFalse h
   simp [getElem!_def, getElem?_def, h]
 
 namespace Fin

src/Init/System/FilePath.lean

@@ -5,8 +5,6 @@ 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,13 +4,9 @@ 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,10 +5,7 @@ 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` calls `rw`, then closes any remaining goals using `assumption`. -/
+/-- `rwa` is short-hand for `rw; 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.shrink toPullSizeSaved ++ keep }
+  modify fun s => { s with toPull := s.toPull.take toPullSizeSaved ++ keep }
   return c
 
 def attachToPull (c : Code) : PullM Code := do

src/Lean/Declaration.lean

@@ -472,6 +472,10 @@ 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`
-      addAuxDeclarationRanges declName stx id
+      addDeclarationRangesFromSyntax 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, stx := ⟨.missing⟩ }
+  let defView := mkDefViewOfDef { isUnsafe := true }
     (← `(Parser.Command.definition|
           def $(mkIdent <| `_root_ ++ declName) := $(← Term.exprToSyntax value)))
   Term.elabMutualDef #[] { header := "" } #[defView]

src/Lean/Elab/Command.lean

@@ -711,21 +711,54 @@ 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 traces and the environment.
+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.
 
 Commands that modify the processing of subsequent commands,
 such as `open` and `namespace` commands,
@@ -738,27 +771,9 @@ 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 α) : 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
+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)
 
 /--
 Given a command elaborator `cmd`, returns a new command elaborator that

src/Lean/Elab/DeclModifiers.lean

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

src/Lean/Elab/Declaration.lean

@@ -102,14 +102,16 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
   -- leading_parser "axiom " >> declId >> declSig
   let declId             := stx[1]
   let (binders, typeStx) := expandDeclSig stx[2]
-  let scopeLevelNames ← getLevelNames
-  let ⟨_, declName, allUserLevelNames⟩ ← expandDeclId declId modifiers
-  addDeclarationRanges declName modifiers.stx stx
-  runTermElabM fun vars =>
+  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
     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)
@@ -135,63 +137,6 @@ 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`.
@@ -230,19 +175,6 @@ 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 =>
@@ -400,7 +332,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
-      addDeclarationRanges fullId ⟨defStx.raw[0]⟩ defStx.raw[1]
+      addDeclarationRangesForBuiltin 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,29 +49,31 @@ 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.addDeclarationRanges` to store this information for their commands.
+`Lean.Elab.addDeclarationRangesFromSyntax` or `Lean.addDeclarationRanges` to store this information
+for their commands.
 -/
-def addDeclarationRanges [Monad m] [MonadEnv m] [MonadFileMap m] (declName : Name)
+def addDeclarationRangesForBuiltin [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]
-  -- 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 }
+  addDeclarationRangesFromSyntax declName stx (getDeclarationSelectionRef declStx)
 
 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.set opts true
+  let opts := Language.Lean.internal.cmdlineSnapshots.setIfNotSet 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,6 +18,7 @@ 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
@@ -79,10 +80,56 @@ 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
@@ -94,7 +141,8 @@ private partial def elabHeaderAux (views : Array InductiveView) (i : Nat) (acc :
           let type := mkSort u
           Term.synthesizeSyntheticMVarsNoPostponing
           Term.addAutoBoundImplicits' params type fun params type => do
-            return acc.push { lctx := (← getLCtx), localInsts := (← getLocalInstances), params, type, view }
+            let levelNames ← Term.getLevelNames
+            return acc.push { lctx := (← getLCtx), localInsts := (← getLocalInstances), levelNames, params, type, view }
         | some typeStx =>
           let (type, _) ← Term.withAutoBoundImplicit do
             let type ← Term.elabType typeStx
@@ -105,7 +153,8 @@ 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}"
-            return acc.push { lctx := (← getLCtx), localInsts := (← getLocalInstances), params, type, view }
+            let levelNames ← Term.getLevelNames
+            return acc.push { lctx := (← getLCtx), localInsts := (← getLocalInstances), levelNames, params, type, view }
       elabHeaderAux views (i+1) acc
     else
       return acc
@@ -123,13 +172,20 @@ 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 checkLevelNames (views : Array InductiveView) : TermElabM Unit := do
+private def InductiveView.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
@@ -791,12 +847,15 @@ 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
-  checkLevelNames views
+  InductiveView.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 := #[]
@@ -888,19 +947,55 @@ private def applyComputedFields (indViews : Array InductiveView) : CommandElabM
   liftTermElabM do Term.withDeclName indViews[0]!.declName do
     ComputedFields.setComputedFields computedFields
 
-def elabInductiveViews (views : Array InductiveView) : CommandElabM Unit := do
+def elabInductiveViews (vars : Array Expr) (views : Array InductiveView) : TermElabM Unit := do
   let view0 := views[0]!
   let ref := view0.ref
-  runTermElabM fun vars => Term.withDeclName view0.declName do withRef ref do
+  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?
-      addAuxDeclarationRanges declName decl declId
+      addDeclarationRangesFromSyntax 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,7 +887,6 @@ 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
@@ -998,7 +997,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
-        addDeclarationRanges header.declName view.modifiers.stx view.ref
+        addDeclarationRangesForBuiltin 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.shrink size }
+  | some _ => { pos, error? := none, imports := s.imports.take 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,9 +5,24 @@ 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
@@ -17,36 +32,41 @@ private def mkInhabitant? (type : Expr) (useOfNonempty : Bool) : MetaM (Option E
   catch _ =>
     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
+/--
+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
 
 /- TODO: add a global IO.Ref to let users customize/extend this procedure -/
-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"
+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."
 
 end Lean.Elab

src/Lean/Elab/StructInst.lean

@@ -826,9 +826,22 @@ 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)
-  | .letE ..      => lambdaLetTelescope e fun xs b => do mkLetFVars 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))
   | .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
-    addAuxDeclarationRanges declName ref ref
+    addDeclarationRangesFromSyntax declName 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?
-      addAuxDeclarationRanges declName ctor[1] ctor[1]
+      addDeclarationRangesFromSyntax declName 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"
-    addAuxDeclarationRanges field.declName field.ref field.ref
+    addDeclarationRangesFromSyntax field.declName 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
-        addDeclarationRanges declName modifiers.stx stx
+        addDeclarationRangesForBuiltin 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,6 +29,7 @@ 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,6 +102,8 @@ 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,13 +12,16 @@ open Meta
 
 @[builtin_tactic Lean.Parser.Tactic.Conv.unfold] def evalUnfold : Tactic := fun stx => withMainContext do
   for declNameId in stx[1].getArgs do
-    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"
+    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"
 
 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
-        addAuxDeclarationRanges extName (← getRef) (← getRef)
+        addDeclarationRangesFromSyntax extName (← 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
-        addAuxDeclarationRanges extName (← getRef) (← getRef)
+        addDeclarationRangesFromSyntax extName (← 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,13 +29,15 @@ 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 do
+  go (declNameId : Syntax) (loc : Location) : TacticM Unit := withMainContext <| withRef declNameId 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}'")
-    | _ => withRef declNameId <| throwTacticEx `unfold (← getMainGoal) m!"expression {e} is not a global or local constant"
+    | _ => throwTacticEx `unfold (← getMainGoal) m!"expression {e} is not a global or local constant"
 
 end Lean.Elab.Tactic

src/Lean/Language/Lean.lean

@@ -300,7 +300,9 @@ 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.
+  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.
 -/
 partial def process
     (setupImports : Syntax → ProcessingT IO (Except HeaderProcessedSnapshot SetupImportsResult))
@@ -330,7 +332,7 @@ where
                 -- elaboration reuse
                 oldProcSuccess.firstCmdSnap.bindIO (sync := true) fun oldCmd => do
                   let prom ← IO.Promise.new
-                  let _ ← IO.asTask (parseCmd oldCmd newParserState oldProcSuccess.cmdState prom ctx)
+                  parseCmd oldCmd newParserState oldProcSuccess.cmdState prom (sync := true) ctx
                   return .pure {
                     diagnostics := oldProcessed.diagnostics
                     result? := some {
@@ -446,7 +448,7 @@ where
       let parserState := Runtime.markPersistent parserState
       let cmdState := Runtime.markPersistent cmdState
       let ctx := Runtime.markPersistent ctx
-      let _ ← IO.asTask (parseCmd none parserState cmdState prom ctx)
+      parseCmd none parserState cmdState prom (sync := true) ctx
       return {
         diagnostics
         infoTree? := cmdState.infoState.trees[0]!
@@ -457,24 +459,10 @@ where
       }
 
   parseCmd (old? : Option CommandParsedSnapshot) (parserState : Parser.ModuleParserState)
-      (cmdState : Command.State) (prom : IO.Promise CommandParsedSnapshot) :
+      (cmdState : Command.State) (prom : IO.Promise CommandParsedSnapshot) (sync : Bool) :
       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
@@ -482,11 +470,11 @@ where
       -- from `old`
       if let some oldNext := old.nextCmdSnap? then do
         let newProm ← IO.Promise.new
-        let _ ← old.data.finishedSnap.bindIO fun oldFinished =>
+        let _ ← old.data.finishedSnap.bindIO (sync := true) 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 ctx
+            parseCmd oldNext newParserState oldFinished.cmdState newProm sync 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!
@@ -521,44 +509,61 @@ where
       if let some tk := ctx.oldCancelTk? then
         tk.set
 
-    -- 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 {})
+    -- 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 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
+    -- 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
 
   doElab (stx : Syntax) (cmdState : Command.State) (beginPos : String.Pos)
       (snap : SnapshotBundle DynamicSnapshot) (finishedPromise : IO.Promise CommandFinishedSnapshot)
@@ -625,7 +630,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
+  process.parseCmd (old?.map (·.2)) parserState commandState prom (sync := true)
     |>.run (old?.map (·.1))
     |>.run { inputCtx with }
   return prom.result

src/Lean/Meta/AppBuilder.lean

@@ -28,6 +28,7 @@ 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,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Meta.Basic
+import Init.Control.Option
 
 namespace Lean.Meta
 

src/Lean/Meta/Offset.lean

@@ -4,6 +4,7 @@ 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 ← withLetDecl n t' v' fun x => do
-        M.localMapM (mkLetFVars (usedLetOnly := true) #[x] ·) do
+      return ← withLocalDeclD n t' fun x => do
+        M.localMapM (mkLetFun x v' ·) do
           let b' ← foldAndCollect oldIH newIH isRecCall (b.instantiate1 x)
           mkLetFun x v' b'
 
@@ -598,6 +598,11 @@ 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
@@ -608,7 +613,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 ← withLocalDecl n .default t' fun x => M2.branch do
+    return ← withLocalDeclD n 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.shrink (a : Assignment) (newSize : Nat) : Assignment :=
-  { a with val := a.val.shrink newSize }
+abbrev Assignment.take (a : Assignment) (newSize : Nat) : Assignment :=
+  { a with val := a.val.take 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.shrink maxVarIdx
+      let assignment := assignment.take 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.shrink nparams)
+  return mkAppN (mkConst ctor lvls) (type.getAppArgs.take 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.shrink ctorInfo.numParams
+        let params := majorType.getAppArgs.take 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.shrink startStackSize |>.push node
+  s.take 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.shrink oldStackSize, oldLhsPrec, oldStopPos, cache, oldError, errs⟩
+    ⟨stack.take 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.shrink oldStackSize, lhsPrec, pos, cache, some newError, errs⟩
+    ⟨stack.take 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.shrinkStack startSize |>.pushSyntax Syntax.missing
+    s.takeStack startSize |>.pushSyntax Syntax.missing
   else
     -- parser succeeded with incorrect number of nodes
     invalidLongestMatchParser s

src/Lean/Parser/Term.lean

@@ -819,6 +819,7 @@ 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,8 +158,10 @@ def size (stack : SyntaxStack) : Nat :=
 def isEmpty (stack : SyntaxStack) : Bool :=
   stack.size == 0
 
-def shrink (stack : SyntaxStack) (n : Nat) : SyntaxStack :=
-  { stack with raw := stack.raw.shrink (stack.drop + n) }
+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 push (stack : SyntaxStack) (a : Syntax) : SyntaxStack :=
   { stack with raw := stack.raw.push a }
@@ -212,7 +214,7 @@ def stackSize (s : ParserState) : Nat :=
   s.stxStack.size
 
 def restore (s : ParserState) (iniStackSz : Nat) (iniPos : String.Pos) : ParserState :=
-  { s with stxStack := s.stxStack.shrink iniStackSz, errorMsg := none, pos := iniPos }
+  { s with stxStack := s.stxStack.take iniStackSz, errorMsg := none, pos := iniPos }
 
 def setPos (s : ParserState) (pos : String.Pos) : ParserState :=
   { s with pos := pos }
@@ -226,8 +228,10 @@ def pushSyntax (s : ParserState) (n : Syntax) : ParserState :=
 def popSyntax (s : ParserState) : ParserState :=
   { s with stxStack := s.stxStack.pop }
 
-def shrinkStack (s : ParserState) (iniStackSz : Nat) : ParserState :=
-  { s with stxStack := s.stxStack.shrink iniStackSz }
+def takeStack (s : ParserState) (iniStackSz : Nat) : ParserState :=
+  { s with stxStack := s.stxStack.take iniStackSz }
+
+@[deprecated takeStack (since := "2024-10-22")] abbrev shrinkStack := @takeStack
 
 def next (s : ParserState) (input : String) (pos : String.Pos) : ParserState :=
   { s with pos := input.next pos }
@@ -250,7 +254,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.shrink iniStackSz
+      let stack   := stack.take iniStackSz
       let stack   := stack.push newNode
       ⟨stack, lhsPrec, pos, cache, err, recovered⟩
 
@@ -258,7 +262,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.shrink (iniStackSz - 1)
+    let stack   := stack.take (iniStackSz - 1)
     let stack   := stack.push newNode
     ⟨stack, lhsPrec, pos, cache, err, errs⟩
 
@@ -283,7 +287,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.shrinkStack sz
+    s := s.takeStack 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 := whenPPOption getPPCoercions <| withOverApp 3 do
+def delabOfNat : Delab := whenNotPPOption getPPExplicit <| 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 := whenPPOption getPPCoercions do
+def delabNeg : Delab := whenNotPPOption getPPExplicit <| 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 := whenPPOption getPPCoercions do
+def delabHDiv : Delab := whenNotPPOption getPPExplicit <| 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 := whenPPOption getPPCoercions <| withOverApp 5 do
+def delabOfScientific : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPCoercions <| withOverApp 5 do
   let expr ← getExpr
   guard <| expr.getAppNumArgs == 5
   let .lit (.natVal m) ← pure (expr.getArg! 2) | failure
@@ -1080,6 +1080,9 @@ 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
@@ -1092,7 +1095,7 @@ def coeDelaborator : Delab := whenPPOption getPPCoercions do
     | .coeSort => `(↥$(← withNaryArg info.coercee delab))
 
 @[builtin_delab app.dite]
-def delabDIte : Delab := whenPPOption getPPNotation <| withOverApp 5 do
+def delabDIte : Delab := whenNotPPOption getPPExplicit <| 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
@@ -1109,7 +1112,7 @@ where
         return (← delab, h.getId)
 
 @[builtin_delab app.cond]
-def delabCond : Delab := whenPPOption getPPNotation <| withOverApp 4 do
+def delabCond : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPNotation <| withOverApp 4 do
   guard $ (← getExpr).getAppNumArgs == 4
   let c ← withAppFn $ withAppFn $ withAppArg delab
   let t ← withAppFn $ withAppArg delab
@@ -1129,7 +1132,7 @@ def delabNamedPattern : Delab := do
   `($x:ident@$h:ident:$p:term)
 
 -- Sigma and PSigma delaborators
-def delabSigmaCore (sigma : Bool) : Delab := whenPPOption getPPNotation do
+def delabSigmaCore (sigma : Bool) : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPNotation do
   guard $ (← getExpr).getAppNumArgs == 2
   guard $ (← getExpr).appArg!.isLambda
   withAppArg do
@@ -1209,7 +1212,7 @@ partial def delabDoElems : DelabM (List Syntax) := do
     prependAndRec x : DelabM _ := List.cons <$> x <*> delabDoElems
 
 @[builtin_delab app.Bind.bind]
-def delabDo : Delab := whenPPOption getPPNotation do
+def delabDo : Delab := whenNotPPOption getPPExplicit <| 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.shrink mvars.size
+      let args := args.take 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.shrink sp).push f
+  setStack $ (stack.take sp).push f
 
 /-- Execute `x` and concatenate generated Format objects. -/
 def concat (x : FormatterM Unit) : FormatterM Unit := do

src/Lean/Server/Completion.lean

@@ -207,6 +207,8 @@ 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,6 +7,7 @@ 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,6 +73,10 @@ inductive BVBinOp where
   Unsigned modulo.
   -/
   | umod
+  /--
+  Signed division.
+  -/
+  | sdiv
 
 namespace BVBinOp
 
@@ -84,6 +88,7 @@ def toString : BVBinOp → String
   | mul => "*"
   | udiv => "/ᵤ"
   | umod => "%ᵤ"
+  | sdiv => "/ₛ"
 
 instance : ToString BVBinOp := ⟨toString⟩
 
@@ -98,6 +103,7 @@ 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
@@ -106,6 +112,7 @@ 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,6 +21,7 @@ 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`).
@@ -117,6 +118,13 @@ 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
@@ -227,7 +235,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 =>
+    | .and | .or | .xor | .add | .mul | .udiv | .umod | .sdiv =>
       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

@@ -0,0 +1,230 @@
+/-
+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,6 +21,7 @@ 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
 
 /-!
@@ -218,6 +219,18 @@ 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

@@ -0,0 +1,201 @@
+/-
+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,6 +262,7 @@ 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,6 +118,10 @@ 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

@@ -0,0 +1,643 @@
+# - 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> [<additional arguments to git describe> ...])
+#  get_git_head_revision(<refspecvar> <hashvar> [ALLOW_LOOKING_ABOVE_CMAKE_SOURCE_DIR])
 #
 # Returns the refspec and sha hash of the current head revision
 #
@@ -12,26 +12,41 @@
 # 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-2010 Ryan Pavlik <rpavlik@iastate.edu> <abiryan@ryand.net>
-# http://academic.cleardefinition.com
-# Iowa State University HCI Graduate Program/VRAC
+# 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
 #
-# 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)
 
@@ -39,92 +54,234 @@ 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)
-	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()
+    _git_find_closest_git_dir("${CMAKE_CURRENT_SOURCE_DIR}" GIT_DIR)
 
-	if(NOT EXISTS "${GIT_DIR}/HEAD")
-		return()
-	endif()
-	set(HEAD_FILE "${GIT_DATA}/HEAD")
-	configure_file("${GIT_DIR}/HEAD" "${HEAD_FILE}" COPYONLY)
+    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()
 
-	configure_file("${_gitdescmoddir}/GetGitRevisionDescription.cmake.in"
-		"${GIT_DATA}/grabRef.cmake"
-		@ONLY)
-	include("${GIT_DATA}/grabRef.cmake")
+    # 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()
 
-	set(${_refspecvar} "${HEAD_REF}" PARENT_SCOPE)
-	set(${_hashvar} "${HEAD_HASH}" PARENT_SCOPE)
+    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)
 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
-		${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()
+    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()
 
-	set(${_var} "${out}" PARENT_SCOPE)
+    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)
 endfunction()
 
 function(git_get_exact_tag _var)
-	git_describe(out --exact-match ${ARGN})
-	set(${_var} "${out}" PARENT_SCOPE)
+    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()
 endfunction()

src/cmake/Modules/GetGitRevisionDescription.cmake.in

@@ -1,17 +1,21 @@
-# 
+#
 # Internal file for GetGitRevisionDescription.cmake
 #
 # Requires CMake 2.6 or newer (uses the 'function' command)
 #
 # Original Author:
-# 2009-2010 Ryan Pavlik <rpavlik@iastate.edu> <abiryan@ryand.net>
-# http://academic.cleardefinition.com
+# 2009-2023 Rylie Pavlik <rylie@ryliepavlik.com>
+# https://ryliepavlik.com/
 # Iowa State University HCI Graduate Program/VRAC
 #
-# Copyright Iowa State University 2009-2010.
+# Copyright 2009-2012, Iowa State University
+# Copyright 2011-2023, Contributors
+#
 # 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)
 
@@ -19,20 +23,26 @@ 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)
-	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()
+    # 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()
 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

@@ -0,0 +1,14 @@
+# 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.shrink pos.val
+  .mk <| log.entries.take pos.val
 
 /-- Takes log entries before `pos` (exclusive). -/
 @[inline] def takeFrom (log : Log) (pos : Log.Pos) : Log :=

tests/bench/big_do.lean

@@ -0,0 +1,459 @@
+/-!
+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

@@ -0,0 +1,40 @@
+/-!
+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,3 +362,21 @@
   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 1 : Nat
+mul f g (@OfNat.ofNat Nat 1 (instOfNatNat 1)) : Nat

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

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

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

@@ -55,7 +55,7 @@
 {"items":
  [{"sortText": "0",
    "label": "ha",
-   "kind": 5,
+   "kind": 23,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionFallback.lean"},
@@ -63,7 +63,7 @@
     "id": {"const": {"declName": "CustomAnd.ha"}}}},
   {"sortText": "1",
    "label": "hb",
-   "kind": 5,
+   "kind": 23,
    "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": 3,
+   "kind": 23,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionPrv.lean"},
@@ -39,7 +39,7 @@
     "id": {"const": {"declName": "BitVec.getElem_ofBoolListBE"}}}},
   {"sortText": "3",
    "label": "BitVec.getLsbD_ofBoolListBE",
-   "kind": 3,
+   "kind": 23,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionPrv.lean"},
@@ -47,7 +47,7 @@
     "id": {"const": {"declName": "BitVec.getLsbD_ofBoolListBE"}}}},
   {"sortText": "4",
    "label": "BitVec.getMsbD_ofBoolListBE",
-   "kind": 3,
+   "kind": 23,
    "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": 3,
+   "kind": 23,
    "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": 3,
+   "kind": 23,
    "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": 3,
+   "kind": 23,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionPrv.lean"},

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

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

tests/lean/run/3146.lean

@@ -0,0 +1,13 @@
+/-
+  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,3 +5,11 @@
 #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

tests/lean/run/bv_arith.lean

@@ -45,3 +45,9 @@ 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,9 +78,7 @@ 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 5 z).val : Nat -/
+/-- info: (@Fin''.toFin0 (@OfNat.ofNat Nat 5 (instOfNatNat 5)) z).val : Nat -/
 #guard_msgs in #check z.val
-/-- info: (@D.toA 5 d).x : Nat -/
+/-- info: (@D.toA (@OfNat.ofNat Nat 5 (instOfNatNat 5)) d).x : Nat -/
 #guard_msgs in #check d.x
 
 end

tests/lean/run/inductive_typestar.lean

@@ -0,0 +1,44 @@
+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

@@ -0,0 +1,64 @@
+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

@@ -0,0 +1,61 @@
+/-!
+# `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/unfoldTactic.lean

@@ -93,3 +93,15 @@ 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 0
-h : @w Nat (@f Nat inst 5)
+inst : Bar Nat := @Bar.mk Nat (@OfNat.ofNat Nat 0 (instOfNatNat 0))
+h : @w Nat (@f Nat inst (@OfNat.ofNat Nat 5 (instOfNatNat 5)))
 ⊢ True

tests/lean/sanitychecks.lean.expected.out

@@ -12,6 +12,15 @@ 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', failed to show that type is inhabited and non empty
+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: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:2-2:16: error: tactic 'unfold' failed to unfold 'Nat.add' at
+unfoldFailure.lean:2:9-2:16: error: tactic 'unfold' failed to unfold 'Nat.add' at
   True
-unfoldFailure.lean:5:2-5:21: error: tactic 'unfold' failed to unfold 'Nat.add' at
+unfoldFailure.lean:5:9-5:16: 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.shrink iniStackSz, errorMsg := none, pos := iniPos, .. d}
+{ stxStack := d.stxStack.take 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.shrinkStack (d : ParserData) (iniStackSz : Nat) : ParserData :=
-{ stxStack := d.stxStack.shrink iniStackSz, .. d }
+def ParserData.takeStack (d : ParserData) (iniStackSz : Nat) : ParserData :=
+{ stxStack := d.stxStack.take 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.shrink iniStackSz in
+    let stack   := stack.take 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.shrink iniSz, iniPos, cache, some msg⟩
+  | ⟨stack, _, cache, some msg⟩ := ⟨stack.take 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.shrink oldStackSize, pos, cache, err⟩
+| ⟨stack, pos, cache, err⟩ := ⟨stack.take oldStackSize, pos, cache, err⟩
 
 def ParserData.keepPrevError (d : ParserData) (oldStackSize : Nat) (oldStopPos : String.Pos) (oldError : Option String) : ParserData :=
 match d with
-| ⟨stack, _, cache, _⟩ := ⟨stack.shrink oldStackSize, oldStopPos, cache, oldError⟩
+| ⟨stack, _, cache, _⟩ := ⟨stack.take oldStackSize, oldStopPos, cache, oldError⟩
 
 def ParserData.mergeErrors (d : ParserData) (oldStackSize : Nat) (oldError : String) : ParserData :=
 match d with
-| ⟨stack, pos, cache, some err⟩ := ⟨stack.shrink oldStackSize, pos, cache, some (err ++ "; " ++ oldError)⟩
+| ⟨stack, pos, cache, some err⟩ := ⟨stack.take 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.shrink startSize in
+    let stack := stack.take 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.shrink startStackSize in
+  let stack := stack.take 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.shrinkStack startSize else d.mkLongestNodeAlt startSize in
+let d         := if d.hasError then d.takeStack 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.shrinkStack startSize in
+    let d := d.takeStack startSize in
     longestMatchFnAux startSize startPos ps s d
   else
     let d := d.mkLongestNodeAlt startSize in