fix: IndPredBelow should not add auxiliary declarations containing sorry

Issue #4535 is being affected by a bug in the structural inductive
predicate termination checker (`IndPred.lean`). This module did not
exist in Lean 3, and it is buggy in Lean 4. In the given example,
it introduces an auxiliary declaration containing a `sorry`, and the
fails. This PR ensures this kind of declaration is not added to the
environment.

Closes #4535

TODO: we need a new maintainer for the `IndPred.lean`.

.github/workflows/ci.yml

@@ -467,6 +467,7 @@ jobs:
         with:
           files: artifacts/*/*
           fail_on_unmatched_files: true
+          prerelease: ${{ !startsWith(github.ref, 'refs/tags/v') || contains(github.ref, '-rc') }}
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
 

nix/bootstrap.nix

@@ -87,7 +87,8 @@ rec {
         leanFlags = [ "-DwarningAsError=true" ];
       } // args);
       Init' = build { name = "Init"; deps = []; };
-      Lean' = build { name = "Lean"; deps = [ Init' ]; };
+      Std' = build { name = "Std"; deps = [ Init' ]; };
+      Lean' = build { name = "Lean"; deps = [ Std' ]; };
       attachSharedLib = sharedLib: pkg: pkg // {
         inherit sharedLib;
         mods = mapAttrs (_: m: m // { inherit sharedLib; propagatedLoadDynlibs = []; }) pkg.mods;
@@ -95,7 +96,8 @@ rec {
     in (all: all // all.lean) rec {
       inherit (Lean) emacs-dev emacs-package vscode-dev vscode-package;
       Init = attachSharedLib leanshared Init';
-      Lean = attachSharedLib leanshared Lean' // { allExternalDeps = [ Init ]; };
+      Std = attachSharedLib leanshared Std' // { allExternalDeps = [ Init ]; };
+      Lean = attachSharedLib leanshared Lean' // { allExternalDeps = [ Std ]; };
       Lake = build {
         name = "Lake";
         src = src + "/src/lake";
@@ -109,23 +111,22 @@ rec {
         linkFlags = lib.optional stdenv.isLinux "-rdynamic";
         src = src + "/src/lake";
       };
-      stdlib = [ Init Lean Lake ];
+      stdlib = [ Init Std Lean Lake ];
       modDepsFiles = symlinkJoin { name = "modDepsFiles"; paths = map (l: l.modDepsFile) (stdlib ++ [ Leanc ]); };
       depRoots = symlinkJoin { name = "depRoots"; paths = map (l: l.depRoots) stdlib; };
       iTree = symlinkJoin { name = "ileans"; paths = map (l: l.iTree) stdlib; };
       Leanc = build { name = "Leanc"; src = lean-bin-tools-unwrapped.leanc_src; deps = stdlib; roots = [ "Leanc" ]; };
-      stdlibLinkFlags = "-L${Init.staticLib} -L${Lean.staticLib} -L${Lake.staticLib} -L${leancpp}/lib/lean";
+      stdlibLinkFlags = "${lib.concatMapStringsSep " " (l: "-L${l.staticLib}") stdlib} -L${leancpp}/lib/lean";
       libInit_shared = runCommand "libInit_shared" { buildInputs = [ stdenv.cc ]; libName = "libInit_shared${stdenv.hostPlatform.extensions.sharedLibrary}"; } ''
         mkdir $out
-        LEAN_CC=${stdenv.cc}/bin/cc ${lean-bin-tools-unwrapped}/bin/leanc -shared -Wl,-Bsymbolic \
-          -Wl,--whole-archive -lInit ${leancpp}/lib/libleanrt_initial-exec.a -Wl,--no-whole-archive -lstdc++ -lm ${stdlibLinkFlags} \
-          $(${llvmPackages.libllvm.dev}/bin/llvm-config --ldflags --libs) \
-          -o $out/$libName
+        touch empty.c
+        ${stdenv.cc}/bin/cc -shared -o $out/$libName empty.c
       '';
       leanshared = runCommand "leanshared" { buildInputs = [ stdenv.cc ]; libName = "libleanshared${stdenv.hostPlatform.extensions.sharedLibrary}"; } ''
         mkdir $out
-        LEAN_CC=${stdenv.cc}/bin/cc ${lean-bin-tools-unwrapped}/bin/leanc -shared -Wl,-Bsymbolic \
-          ${libInit_shared}/* -Wl,--whole-archive -lLean -lleancpp -Wl,--no-whole-archive -lstdc++ -lm ${stdlibLinkFlags} \
+        LEAN_CC=${stdenv.cc}/bin/cc ${lean-bin-tools-unwrapped}/bin/leanc -shared ${lib.optionalString stdenv.isLinux "-Wl,-Bsymbolic"} \
+          ${if stdenv.isDarwin then "-Wl,-force_load,${Init.staticLib}/libInit.a -Wl,-force_load,${Lean.staticLib}/libStd.a -Wl,-force_load,${Lean.staticLib}/libLean.a -Wl,-force_load,${leancpp}/lib/lean/libleancpp.a ${leancpp}/lib/libleanrt_initial-exec.a -lc++"
+            else "-Wl,--whole-archive -lInit -lStd -lLean -lleancpp ${leancpp}/lib/libleanrt_initial-exec.a -Wl,--no-whole-archive -lstdc++"} -lm ${stdlibLinkFlags} \
           $(${llvmPackages.libllvm.dev}/bin/llvm-config --ldflags --libs) \
           -o $out/$libName
       '';
@@ -151,11 +152,9 @@ rec {
         '';
         meta.mainProgram = "lean";
       };
-      cacheRoots = linkFarmFromDrvs "cacheRoots" [
+      cacheRoots = linkFarmFromDrvs "cacheRoots" ([
         stage0 lean leanc lean-all iTree modDepsFiles depRoots Leanc.src
-        # .o files are not a runtime dependency on macOS because of lack of thin archives
-        Lean.oTree Lake.oTree
-      ];
+      ] ++ map (lib: lib.oTree) stdlib);
       test = buildCMake {
         name = "lean-test-${desc}";
         realSrc = lib.sourceByRegex src [ "src.*" "tests.*" ];
@@ -178,7 +177,7 @@ rec {
         '';
       };
       update-stage0 =
-        let cTree = symlinkJoin { name = "cs"; paths = [ Init.cTree Lean.cTree Lake.cTree ]; }; in
+        let cTree = symlinkJoin { name = "cs"; paths = map (lib: lib.cTree) stdlib; }; in
         writeShellScriptBin "update-stage0" ''
           CSRCS=${cTree} CP_C_PARAMS="--dereference --no-preserve=all" ${src + "/script/lib/update-stage0"}
         '';

nix/buildLeanPackage.nix

@@ -5,7 +5,7 @@ let lean-final' = lean-final; in
 lib.makeOverridable (
 { name, src, fullSrc ? src, srcPrefix ? "", srcPath ? "$PWD/${srcPrefix}",
   # Lean dependencies. Each entry should be an output of buildLeanPackage.
-  deps ? [ lean.Lean ],
+  deps ? [ lean.Init lean.Std lean.Lean ],
   # Static library dependencies. Each derivation `static` should contain a static library in the directory `${static}`.
   staticLibDeps ? [],
   # Whether to wrap static library inputs in a -Wl,--start-group [...] -Wl,--end-group to ensure dependencies are resolved.
@@ -249,7 +249,7 @@ in rec {
     ${if stdenv.isDarwin then "-Wl,-force_load,${staticLib}/lib${libName}.a" else "-Wl,--whole-archive ${staticLib}/lib${libName}.a -Wl,--no-whole-archive"} \
     ${lib.concatStringsSep " " (map (d: "${d.sharedLib}/*") deps)}'';
   executable = lib.makeOverridable ({ withSharedStdlib ? true }: let
-      objPaths = map (drv: "${drv}/${drv.oPath}") (attrValues objects) ++ lib.optional withSharedStdlib "${lean-final.libInit_shared}/* ${lean-final.leanshared}/*";
+      objPaths = map (drv: "${drv}/${drv.oPath}") (attrValues objects) ++ lib.optional withSharedStdlib "${lean-final.leanshared}/*";
     in runCommand executableName { buildInputs = [ stdenv.cc leanc ]; } ''
       mkdir -p $out/bin
       leanc ${staticLibLinkWrapper (lib.concatStringsSep " " (objPaths ++ map (d: "${d}/*.a") allStaticLibDeps))} \

src/CMakeLists.txt

@@ -313,7 +313,7 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
   set(LEAN_CXX_STDLIB "-lc++")
 endif()
 
-string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
+string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " ${LEAN_CXX_STDLIB} -lStd")
 string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
 
 # in local builds, link executables and not just dynlibs against C++ stdlib as well,
@@ -514,11 +514,11 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
 endif()
 
 if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
-  set(LEANSHARED_LINKER_FLAGS "-Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libInit.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLean.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
+  set(LEANSHARED_LINKER_FLAGS "-Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libInit.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libStd.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLean.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
 elseif(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
-  set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/temp/libLean.a.export -lleancpp -Wl,--no-whole-archive -lInit_shared -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libleanshared.dll.a")
+  set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/temp/libStd.a.export ${CMAKE_BINARY_DIR}/lib/temp/libLean.a.export -lleancpp -Wl,--no-whole-archive -lInit_shared -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libleanshared.dll.a")
 else()
-  set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive -lInit -lLean -lleancpp -Wl,--no-whole-archive ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
+  set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive -lInit -lStd -lLean -lleancpp -Wl,--no-whole-archive ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
 endif()
 
 if (${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
@@ -540,7 +540,7 @@ add_custom_target(make_stdlib ALL
   # The actual rule is in a separate makefile because we want to prefix it with '+' to use the Make job server
   # for a parallelized nested build, but CMake doesn't let us do that.
   # We use `lean` from the previous stage, but `leanc`, headers, etc. from the current stage
-  COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Init Lean
+  COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Init Std Lean
   VERBATIM)
 
 # if we have LLVM enabled, then build `lean.h.bc` which has the LLVM bitcode

src/Init/Core.lean

@@ -1191,7 +1191,10 @@ def Prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂
     (f : α₁ → α₂) (g : β₁ → β₂) : α₁ × β₁ → α₂ × β₂
   | (a, b) => (f a, g b)
 
-@[simp] theorem Prod.map_apply : Prod.map f g (x, y) = (f x, g y) := rfl
+@[simp] theorem Prod.map_apply (f : α → β) (g : γ → δ) (x) (y) :
+    Prod.map f g (x, y) = (f x, g y) := rfl
+@[simp] theorem Prod.map_fst (f : α → β) (g : γ → δ) (x) : (Prod.map f g x).1 = f x.1 := rfl
+@[simp] theorem Prod.map_snd (f : α → β) (g : γ → δ) (x) : (Prod.map f g x).2 = g x.2 := rfl
 
 /-! # Dependent products -/
 

src/Init/Data/BitVec/Basic.lean

@@ -614,6 +614,13 @@ theorem ofBool_append (msb : Bool) (lsbs : BitVec w) :
     ofBool msb ++ lsbs = (cons msb lsbs).cast (Nat.add_comm ..) :=
   rfl
 
+/--
+`twoPow w i` is the bitvector `2^i` if `i < w`, and `0` otherwise.
+That is, 2 to the power `i`.
+For the bitwise point of view, it has the `i`th bit as `1` and all other bits as `0`.
+-/
+def twoPow (w : Nat) (i : Nat) : BitVec w := 1#w <<< i
+
 end bitwise
 
 section normalization_eqs

src/Init/Data/BitVec/Lemmas.lean

@@ -1367,4 +1367,51 @@ theorem getLsb_rotateRight {x : BitVec w} {r i : Nat} :
   · simp
   · rw [← rotateRight_mod_eq_rotateRight, getLsb_rotateRight_of_le (Nat.mod_lt _ (by omega))]
 
+/- ## twoPow -/
+
+@[simp, bv_toNat]
+theorem toNat_twoPow (w : Nat) (i : Nat) : (twoPow w i).toNat = 2^i % 2^w := by
+  rcases w with rfl | w
+  · simp [Nat.mod_one]
+  · simp only [twoPow, toNat_shiftLeft, toNat_ofNat]
+    have h1 : 1 < 2 ^ (w + 1) := Nat.one_lt_two_pow (by omega)
+    rw [Nat.mod_eq_of_lt h1, Nat.shiftLeft_eq, Nat.one_mul]
+
+@[simp]
+theorem getLsb_twoPow (i j : Nat) : (twoPow w i).getLsb j = ((i < w) && (i = j)) := by
+  rcases w with rfl | w
+  · simp; omega
+  · simp only [twoPow, getLsb_shiftLeft, getLsb_ofNat]
+    by_cases hj : j < i
+    · simp only [hj, decide_True, Bool.not_true, Bool.and_false, Bool.false_and, Bool.false_eq,
+      Bool.and_eq_false_imp, decide_eq_true_eq, decide_eq_false_iff_not]
+      omega
+    · by_cases hi : Nat.testBit 1 (j - i)
+      · obtain hi' := Nat.testBit_one_eq_true_iff_self_eq_zero.mp hi
+        have hij : j = i := by omega
+        simp_all
+      · have hij : i ≠ j := by
+          intro h; subst h
+          simp at hi
+        simp_all
+
+theorem and_twoPow_eq (x : BitVec w) (i : Nat) :
+    x &&& (twoPow w i) = if x.getLsb i then twoPow w i else 0#w := by
+  ext j
+  simp only [getLsb_and, getLsb_twoPow]
+  by_cases hj : i = j <;> by_cases hx : x.getLsb i <;> simp_all
+
+@[simp]
+theorem mul_twoPow_eq_shiftLeft (x : BitVec w) (i : Nat) :
+    x * (twoPow w i) = x <<< i := by
+  apply eq_of_toNat_eq
+  simp only [toNat_mul, toNat_twoPow, toNat_shiftLeft, Nat.shiftLeft_eq]
+  by_cases hi : i < w
+  · have hpow : 2^i < 2^w := Nat.pow_lt_pow_of_lt (by omega) (by omega)
+    rw [Nat.mod_eq_of_lt hpow]
+  · have hpow : 2 ^ i % 2 ^ w = 0 := by
+      rw [Nat.mod_eq_zero_of_dvd]
+      apply Nat.pow_dvd_pow 2 (by omega)
+    simp [Nat.mul_mod, hpow]
+
 end BitVec

src/Init/Data/Int/Order.lean

@@ -127,9 +127,14 @@ protected theorem lt_iff_le_not_le {a b : Int} : a < b ↔ a ≤ b ∧ ¬b ≤ a
   · exact Int.le_antisymm h h'
   · subst h'; apply Int.le_refl
 
+protected theorem lt_of_not_ge {a b : Int} (h : ¬a ≤ b) : b < a :=
+  Int.lt_iff_le_not_le.mpr ⟨(Int.le_total ..).resolve_right h, h⟩
+
+protected theorem not_le_of_gt {a b : Int} (h : b < a) : ¬a ≤ b :=
+  (Int.lt_iff_le_not_le.mp h).right
+
 protected theorem not_le {a b : Int} : ¬a ≤ b ↔ b < a :=
-  ⟨fun h => Int.lt_iff_le_not_le.2 ⟨(Int.le_total ..).resolve_right h, h⟩,
-   fun h => (Int.lt_iff_le_not_le.1 h).2⟩
+  Iff.intro Int.lt_of_not_ge Int.not_le_of_gt
 
 protected theorem not_lt {a b : Int} : ¬a < b ↔ b ≤ a :=
   by rw [← Int.not_le, Decidable.not_not]
@@ -509,9 +514,6 @@ theorem mem_toNat' : ∀ (a : Int) (n : Nat), toNat' a = some n ↔ a = n
 
 /-! ## Order properties of the integers -/
 
-protected theorem lt_of_not_ge {a b : Int} : ¬a ≤ b → b < a := Int.not_le.mp
-protected theorem not_le_of_gt {a b : Int} : b < a → ¬a ≤ b := Int.not_le.mpr
-
 protected theorem le_of_not_le {a b : Int} : ¬ a ≤ b → b ≤ a := (Int.le_total a b).resolve_left
 
 @[simp] theorem negSucc_not_pos (n : Nat) : 0 < -[n+1] ↔ False := by
@@ -586,7 +588,10 @@ theorem add_one_le_iff {a b : Int} : a + 1 ≤ b ↔ a < b := .rfl
 theorem lt_add_one_iff {a b : Int} : a < b + 1 ↔ a ≤ b := Int.add_le_add_iff_right _
 
 @[simp] theorem succ_ofNat_pos (n : Nat) : 0 < (n : Int) + 1 :=
-  lt_add_one_iff.2 (ofNat_zero_le _)
+  lt_add_one_iff.mpr (ofNat_zero_le _)
+
+theorem not_ofNat_neg (n : Nat) : ¬((n : Int) < 0) :=
+  Int.not_lt.mpr (ofNat_zero_le ..)
 
 theorem le_add_one {a b : Int} (h : a ≤ b) : a ≤ b + 1 :=
   Int.le_of_lt (Int.lt_add_one_iff.2 h)
@@ -801,6 +806,12 @@ protected theorem lt_add_of_neg_lt_sub_right {a b c : Int} (h : -b < a - c) : c
 protected theorem neg_lt_sub_right_of_lt_add {a b c : Int} (h : c < a + b) : -b < a - c :=
   Int.lt_sub_left_of_add_lt (Int.sub_right_lt_of_lt_add h)
 
+protected theorem add_lt_iff (a b c : Int) : a + b < c ↔ a < -b + c := by
+  rw [← Int.add_lt_add_iff_left (-b), Int.add_comm (-b), Int.add_neg_cancel_right]
+
+protected theorem sub_lt_iff (a b c : Int) : a - b < c ↔ a < c + b :=
+  Iff.intro Int.lt_add_of_sub_right_lt Int.sub_right_lt_of_lt_add
+
 protected theorem sub_lt_of_sub_lt {a b c : Int} (h : a - b < c) : a - c < b :=
   Int.sub_left_lt_of_lt_add (Int.lt_add_of_sub_right_lt h)
 

src/Init/Data/List/Basic.lean

@@ -67,6 +67,9 @@ namespace List
 
 @[simp 1100] theorem length_singleton (a : α) : length [a] = 1 := rfl
 
+@[simp] theorem length_cons {α} (a : α) (as : List α) : (cons a as).length = as.length + 1 :=
+  rfl
+
 /-! ### set -/
 
 @[simp] theorem length_set (as : List α) (i : Nat) (a : α) : (as.set i a).length = as.length := by

src/Init/Data/List/Lemmas.lean

@@ -923,12 +923,12 @@ theorem map_filter_eq_foldr (f : α → β) (p : α → Bool) (as : List α) :
   | a :: l₁, l₂ => by simp [filter]; split <;> simp [filter_append l₁]
 
 theorem filter_congr {p q : α → Bool} :
-    ∀ {l : List α}, (∀ x ∈ l, p x ↔ q x) → filter p l = filter q l
+    ∀ {l : List α}, (∀ x ∈ l, p x = q x) → filter p l = filter q l
   | [], _ => rfl
   | a :: l, h => by
     rw [forall_mem_cons] at h; by_cases pa : p a
-    · simp [pa, h.1.1 pa, filter_congr h.2]
-    · simp [pa, mt h.1.2 pa, filter_congr h.2]
+    · simp [pa, h.1 ▸ pa, filter_congr h.2]
+    · simp [pa, h.1 ▸ pa, filter_congr h.2]
 
 @[deprecated filter_congr (since := "2024-06-20")] abbrev filter_congr' := @filter_congr
 
@@ -1275,7 +1275,7 @@ theorem map_bind (f : β → γ) (g : α → List β) :
   | [] => rfl
   | a::l => by simp only [bind_cons, map_append, map_bind _ _ l]
 
-theorem bind_map {f : α → β} {g : β → List γ} (l : List α) : (map f l).bind g = l.bind (fun a => g (f a)) := by
+theorem bind_map (f : α → β) (g : β → List γ) (l : List α) : (map f l).bind g = l.bind (fun a => g (f a)) := by
   induction l <;> simp [bind_cons, append_bind, *]
 
 theorem map_eq_bind {α β} (f : α → β) (l : List α) : map f l = l.bind fun x => [f x] := by

src/Init/Data/List/TakeDrop.lean

@@ -364,4 +364,24 @@ theorem zip_eq_zip_take_min : ∀ (l₁ : List α) (l₂ : List β),
   rw [zip_eq_zip_take_min]
   simp
 
+/-! ### minimum? -/
+
+-- A specialization of `minimum?_eq_some_iff` to Nat.
+theorem minimum?_eq_some_iff' {xs : List Nat} :
+    xs.minimum? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, a ≤ b) :=
+  minimum?_eq_some_iff
+    (le_refl := Nat.le_refl)
+    (min_eq_or := fun _ _ => by omega)
+    (le_min_iff := fun _ _ _ => by omega)
+
+/-! ### maximum? -/
+
+-- A specialization of `maximum?_eq_some_iff` to Nat.
+theorem maximum?_eq_some_iff' {xs : List Nat} :
+    xs.maximum? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, b ≤ a) :=
+  maximum?_eq_some_iff
+    (le_refl := Nat.le_refl)
+    (max_eq_or := fun _ _ => by omega)
+    (max_le_iff := fun _ _ _ => by omega)
+
 end List

src/Init/Data/Nat/Basic.lean

@@ -278,7 +278,7 @@ theorem succ_sub_succ_eq_sub (n m : Nat) : succ n - succ m = n - m := by
   | zero      => exact rfl
   | succ m ih => apply congrArg pred ih
 
-@[simp] theorem pred_le : ∀ (n : Nat), pred n ≤ n
+theorem pred_le : ∀ (n : Nat), pred n ≤ n
   | zero   => Nat.le.refl
   | succ _ => le_succ _
 
@@ -288,7 +288,7 @@ theorem pred_lt : ∀ {n : Nat}, n ≠ 0 → pred n < n
 
 theorem sub_one_lt : ∀ {n : Nat}, n ≠ 0 → n - 1 < n := pred_lt
 
-theorem sub_le (n m : Nat) : n - m ≤ n := by
+@[simp] theorem sub_le (n m : Nat) : n - m ≤ n := by
   induction m with
   | zero      => exact Nat.le_refl (n - 0)
   | succ m ih => apply Nat.le_trans (pred_le (n - m)) ih

src/Init/Data/Nat/Bitwise/Lemmas.lean

@@ -310,6 +310,11 @@ theorem testBit_bool_to_nat (b : Bool) (i : Nat) :
         ←Nat.div_div_eq_div_mul _ 2, one_div_two,
         Nat.mod_eq_of_lt]
 
+/-- `testBit 1 i` is true iff the index `i` equals 0. -/
+theorem testBit_one_eq_true_iff_self_eq_zero {i : Nat} :
+    Nat.testBit 1 i = true ↔ i = 0 := by
+  cases i <;> simp
+
 /-! ### bitwise -/
 
 theorem testBit_bitwise

src/Init/Data/Nat/Div.lean

@@ -251,10 +251,10 @@ theorem div_mul_le_self : ∀ (m n : Nat), m / n * n ≤ m
 theorem div_lt_iff_lt_mul (Hk : 0 < k) : x / k < y ↔ x < y * k := by
   rw [← Nat.not_le, ← Nat.not_le]; exact not_congr (le_div_iff_mul_le Hk)
 
-@[simp] theorem add_div_right (x : Nat) {z : Nat} (H : 0 < z) : (x + z) / z = succ (x / z) := by
+@[simp] theorem add_div_right (x : Nat) {z : Nat} (H : 0 < z) : (x + z) / z = (x / z) + 1 := by
   rw [div_eq_sub_div H (Nat.le_add_left _ _), Nat.add_sub_cancel]
 
-@[simp] theorem add_div_left (x : Nat) {z : Nat} (H : 0 < z) : (z + x) / z = succ (x / z) := by
+@[simp] theorem add_div_left (x : Nat) {z : Nat} (H : 0 < z) : (z + x) / z = (x / z) + 1 := by
   rw [Nat.add_comm, add_div_right x H]
 
 theorem add_mul_div_left (x z : Nat) {y : Nat} (H : 0 < y) : (x + y * z) / y = x / y + z := by
@@ -285,7 +285,7 @@ theorem add_mul_div_right (x y : Nat) {z : Nat} (H : 0 < z) : (x + y * z) / z =
 @[simp] theorem mul_mod_left (m n : Nat) : (m * n) % n = 0 := by
   rw [Nat.mul_comm, mul_mod_right]
 
-protected theorem div_eq_of_lt_le (lo : k * n ≤ m) (hi : m < succ k * n) : m / n = k :=
+protected theorem div_eq_of_lt_le (lo : k * n ≤ m) (hi : m < (k + 1) * n) : m / n = k :=
 have npos : 0 < n := (eq_zero_or_pos _).resolve_left fun hn => by
   rw [hn, Nat.mul_zero] at hi lo; exact absurd lo (Nat.not_le_of_gt hi)
 Nat.le_antisymm
@@ -307,7 +307,7 @@ theorem sub_mul_div (x n p : Nat) (h₁ : n*p ≤ x) : (x - n*p) / n = x / n - p
       rw [sub_succ, ← IH h₂, div_eq_sub_div h₀ h₃]
       simp [Nat.pred_succ, mul_succ, Nat.sub_sub]
 
-theorem mul_sub_div (x n p : Nat) (h₁ : x < n*p) : (n * p - succ x) / n = p - succ (x / n) := by
+theorem mul_sub_div (x n p : Nat) (h₁ : x < n*p) : (n * p - (x + 1)) / n = p - ((x / n) + 1) := by
   have npos : 0 < n := (eq_zero_or_pos _).resolve_left fun n0 => by
     rw [n0, Nat.zero_mul] at h₁; exact not_lt_zero _ h₁
   apply Nat.div_eq_of_lt_le

src/Init/Data/Option/Basic.lean

@@ -119,7 +119,7 @@ def merge (fn : α → α → α) : Option α → Option α → Option α
 
 
 /-- An elimination principle for `Option`. It is a nondependent version of `Option.recOn`. -/
-@[simp, inline] protected def elim : Option α → β → (α → β) → β
+@[inline] protected def elim : Option α → β → (α → β) → β
   | some x, _, f => f x
   | none, y, _ => y
 

src/Init/Data/Option/Lemmas.lean

@@ -208,9 +208,9 @@ theorem liftOrGet_eq_or_eq {f : α → α → α} (h : ∀ a b, f a b = a ∨ f
 @[simp] theorem liftOrGet_some_some {f} {a b : α} :
   liftOrGet f (some a) (some b) = f a b := rfl
 
-theorem elim_none (x : β) (f : α → β) : none.elim x f = x := rfl
+@[simp] theorem elim_none (x : β) (f : α → β) : none.elim x f = x := rfl
 
-theorem elim_some (x : β) (f : α → β) (a : α) : (some a).elim x f = f a := rfl
+@[simp] theorem elim_some (x : β) (f : α → β) (a : α) : (some a).elim x f = f a := rfl
 
 @[simp] theorem getD_map (f : α → β) (x : α) (o : Option α) :
   (o.map f).getD (f x) = f (getD o x) := by cases o <;> rfl

src/Init/Prelude.lean

@@ -2329,9 +2329,6 @@ without running out of stack space.
 def List.lengthTR (as : List α) : Nat :=
   lengthTRAux as 0
 
-@[simp] theorem List.length_cons {α} (a : α) (as : List α) : Eq (cons a as).length as.length.succ :=
-  rfl
-
 /--
 `as.get i` returns the `i`'th element of the list `as`.
 This version of the function uses `i : Fin as.length` to ensure that it will

src/Init/Tactics.lean

@@ -373,7 +373,8 @@ reflexivity theorems (e.g., `Iff.rfl`).
 macro "rfl" : tactic => `(tactic| case' _ => fail "The rfl tactic failed. Possible reasons:
 - The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
 - The arguments of the relation are not equal.
-Try using the reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`.")
+Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
+`exact HEq.rfl` etc.")
 
 macro_rules | `(tactic| rfl) => `(tactic| eq_refl)
 macro_rules | `(tactic| rfl) => `(tactic| exact HEq.rfl)

src/Lean/BuiltinDocAttr.lean

@@ -5,12 +5,12 @@ Authors: Mario Carneiro
 -/
 prelude
 import Lean.Compiler.InitAttr
-import Lean.DocString
+import Lean.DocString.Extension
 
 namespace Lean
 
 def declareBuiltinDocStringAndRanges (declName : Name) : AttrM Unit := do
-  if let some doc ← findDocString? (← getEnv) declName (includeBuiltin := false) then
+  if let some doc ← findSimpleDocString? (← getEnv) declName (includeBuiltin := false) then
     declareBuiltin (declName ++ `docString) (mkAppN (mkConst ``addBuiltinDocString) #[toExpr declName, toExpr doc])
   if let some declRanges ← findDeclarationRanges? declName then
     declareBuiltin (declName ++ `declRange) (mkAppN (mkConst ``addBuiltinDeclarationRanges) #[toExpr declName, toExpr declRanges])

src/Lean/Compiler/FFI.lean

@@ -18,6 +18,13 @@ private opaque getLeancExtraFlags : Unit → String
 def getCFlags (leanSysroot : FilePath) : Array String :=
   #["-I", (leanSysroot / "include").toString] ++ (getLeancExtraFlags ()).trim.splitOn
 
+@[extern "lean_get_leanc_internal_flags"]
+private opaque getLeancInternalFlags : Unit → String
+
+/-- Return C compiler flags needed to use the C compiler bundled with the Lean toolchain. -/
+def getInternalCFlags (leanSysroot : FilePath) : Array String :=
+  (getLeancInternalFlags ()).trim.splitOn.toArray.map (·.replace "ROOT" leanSysroot.toString)
+
 @[extern "lean_get_linker_flags"]
 private opaque getBuiltinLinkerFlags (linkStatic : Bool) : String
 
@@ -25,4 +32,11 @@ private opaque getBuiltinLinkerFlags (linkStatic : Bool) : String
 def getLinkerFlags (leanSysroot : FilePath) (linkStatic := true) : Array String :=
   #["-L", (leanSysroot / "lib" / "lean").toString] ++ (getBuiltinLinkerFlags linkStatic).trim.splitOn
 
+@[extern "lean_get_internal_linker_flags"]
+private opaque getBuiltinInternalLinkerFlags : Unit → String
+
+/-- Return linker flags needed to use the linker bundled with the Lean toolchain. -/
+def getInternalLinkerFlags (leanSysroot : FilePath) : Array String :=
+  (getBuiltinInternalLinkerFlags ()).trim.splitOn.toArray.map (·.replace "ROOT" leanSysroot.toString)
+
 end Lean.Compiler.FFI

src/Lean/DocString.lean

@@ -4,58 +4,26 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.DeclarationRange
-import Lean.MonadEnv
-import Init.Data.String.Extra
+import Lean.DocString.Extension
+import Lean.Parser.Tactic.Doc
+
+set_option linter.missingDocs true
+
+-- This module contains the main query interface for docstrings, which assembles user-visible
+-- docstrings.
+-- The module `Lean.DocString.Extension` contains the underlying data.
 
 namespace Lean
+open Lean.Parser.Tactic.Doc
 
-private builtin_initialize builtinDocStrings : IO.Ref (NameMap String) ← IO.mkRef {}
-private builtin_initialize docStringExt : MapDeclarationExtension String ← mkMapDeclarationExtension
+/--
+Finds the docstring for a name, taking tactic alternate forms and documentation extensions into
+account.
 
-def addBuiltinDocString (declName : Name) (docString : String) : IO Unit :=
-  builtinDocStrings.modify (·.insert declName docString.removeLeadingSpaces)
-
-def addDocString [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString : String) : m Unit := do
-  unless (← getEnv).getModuleIdxFor? declName |>.isNone do
-    throwError s!"invalid doc string, declaration '{declName}' is in an imported module"
-  modifyEnv fun env => docStringExt.insert env declName docString.removeLeadingSpaces
-
-def addDocString' [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString? : Option String) : m Unit :=
-  match docString? with
-  | some docString => addDocString declName docString
-  | none => return ()
-
-def findDocString? (env : Environment) (declName : Name) (includeBuiltin := true) : IO (Option String) :=
-  if let some docStr := docStringExt.find? env declName then
-    return some docStr
-  else if includeBuiltin then
-    return (← builtinDocStrings.get).find? declName
-  else
-    return none
-
-structure ModuleDoc where
-  doc : String
-  declarationRange : DeclarationRange
-
-private builtin_initialize moduleDocExt : SimplePersistentEnvExtension ModuleDoc (PersistentArray ModuleDoc) ← registerSimplePersistentEnvExtension {
-  addImportedFn := fun _ => {}
-  addEntryFn    := fun s e => s.push e
-  toArrayFn     := fun es => es.toArray
-}
-
-def addMainModuleDoc (env : Environment) (doc : ModuleDoc) : Environment :=
-  moduleDocExt.addEntry env doc
-
-def getMainModuleDoc (env : Environment) : PersistentArray ModuleDoc :=
-  moduleDocExt.getState env
-
-def getModuleDoc? (env : Environment) (moduleName : Name) : Option (Array ModuleDoc) :=
-  env.getModuleIdx? moduleName |>.map fun modIdx => moduleDocExt.getModuleEntries env modIdx
-
-def getDocStringText [Monad m] [MonadError m] (stx : TSyntax `Lean.Parser.Command.docComment) : m String :=
-  match stx.raw[1] with
-  | Syntax.atom _ val => return val.extract 0 (val.endPos - ⟨2⟩)
-  | _                 => throwErrorAt stx "unexpected doc string{indentD stx.raw[1]}"
-
-end Lean
+Use `Lean.findSimpleDocString?` to look up the raw docstring without resolving alternate forms or
+including extensions.
+-/
+def findDocString? (env : Environment) (declName : Name) (includeBuiltin := true) : IO (Option String) := do
+  let declName := alternativeOfTactic env declName |>.getD declName
+  let exts := getTacticExtensionString env declName
+  return (← findSimpleDocString? env declName (includeBuiltin := includeBuiltin)).map (· ++ exts)

src/Lean/DocString/Extension.lean

@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.DeclarationRange
+import Lean.MonadEnv
+import Init.Data.String.Extra
+
+-- This module contains the underlying data for docstrings, with as few imports as possible, so that
+-- docstrings can be saved in as much of the compiler as possible.
+-- The module `Lean.DocString` contains the query interface, which needs to look at additional data
+-- to construct user-visible docstrings.
+
+namespace Lean
+
+private builtin_initialize builtinDocStrings : IO.Ref (NameMap String) ← IO.mkRef {}
+private builtin_initialize docStringExt : MapDeclarationExtension String ← mkMapDeclarationExtension
+
+def addBuiltinDocString (declName : Name) (docString : String) : IO Unit :=
+  builtinDocStrings.modify (·.insert declName docString.removeLeadingSpaces)
+
+def addDocString [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString : String) : m Unit := do
+  unless (← getEnv).getModuleIdxFor? declName |>.isNone do
+    throwError s!"invalid doc string, declaration '{declName}' is in an imported module"
+  modifyEnv fun env => docStringExt.insert env declName docString.removeLeadingSpaces
+
+def addDocString' [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString? : Option String) : m Unit :=
+  match docString? with
+  | some docString => addDocString declName docString
+  | none => return ()
+
+/--
+Finds a docstring without performing any alias resolution or enrichment with extra metadata.
+
+Docstrings to be shown to a user should be looked up with `Lean.findDocString?` instead.
+-/
+def findSimpleDocString? (env : Environment) (declName : Name) (includeBuiltin := true) : IO (Option String) :=
+  if let some docStr := docStringExt.find? env declName then
+    return some docStr
+  else if includeBuiltin then
+    return (← builtinDocStrings.get).find? declName
+  else
+    return none
+
+structure ModuleDoc where
+  doc : String
+  declarationRange : DeclarationRange
+
+private builtin_initialize moduleDocExt : SimplePersistentEnvExtension ModuleDoc (PersistentArray ModuleDoc) ← registerSimplePersistentEnvExtension {
+  addImportedFn := fun _ => {}
+  addEntryFn    := fun s e => s.push e
+  toArrayFn     := fun es => es.toArray
+}
+
+def addMainModuleDoc (env : Environment) (doc : ModuleDoc) : Environment :=
+  moduleDocExt.addEntry env doc
+
+def getMainModuleDoc (env : Environment) : PersistentArray ModuleDoc :=
+  moduleDocExt.getState env
+
+def getModuleDoc? (env : Environment) (moduleName : Name) : Option (Array ModuleDoc) :=
+  env.getModuleIdx? moduleName |>.map fun modIdx => moduleDocExt.getModuleEntries env modIdx
+
+def getDocStringText [Monad m] [MonadError m] (stx : TSyntax `Lean.Parser.Command.docComment) : m String :=
+  match stx.raw[1] with
+  | Syntax.atom _ val => return val.extract 0 (val.endPos - ⟨2⟩)
+  | _                 => throwErrorAt stx "unexpected doc string{indentD stx.raw[1]}"

src/Lean/Elab.lean

@@ -50,3 +50,4 @@ import Lean.Elab.ParseImportsFast
 import Lean.Elab.GuardMsgs
 import Lean.Elab.CheckTactic
 import Lean.Elab.MatchExpr
+import Lean.Elab.Tactic.Doc

src/Lean/Elab/InheritDoc.lean

@@ -5,7 +5,7 @@ Authors: Mario Carneiro
 -/
 prelude
 import Lean.Elab.InfoTree.Main
-import Lean.DocString
+import Lean.DocString.Extension
 
 namespace Lean
 
@@ -21,9 +21,9 @@ builtin_initialize
         let some id := id?
           | throwError "invalid `[inherit_doc]` attribute, could not infer doc source"
         let declName ← Elab.realizeGlobalConstNoOverloadWithInfo id
-        if (← findDocString? (← getEnv) decl).isSome then
+        if (← findSimpleDocString? (← getEnv) decl).isSome then
           logWarning m!"{← mkConstWithLevelParams decl} already has a doc string"
-        let some doc ← findDocString? (← getEnv) declName
+        let some doc ← findSimpleDocString? (← getEnv) declName
           | logWarningAt id m!"{← mkConstWithLevelParams declName} does not have a doc string"
         addDocString decl doc
       | _  => throwError "invalid `[inherit_doc]` attribute"

src/Lean/Elab/MutualDef.lean

@@ -846,7 +846,10 @@ private def levelMVarToParamHeaders (views : Array DefView) (headers : Array Def
   let rec process : StateRefT Nat TermElabM (Array DefViewElabHeader) := do
     let mut newHeaders := #[]
     for view in views, header in headers do
-      if view.kind.isTheorem then
+      -- Remark: we should consider using `pure view.kind.isTheorem <||> isProp header.type`, and
+      -- also handle definitions. We used the following approach because it is less disruptive to Mathlib.
+      -- Moreover, the type of most definitions are not propositions anyway.
+      if ← pure view.kind.isTheorem <||> (pure view.kind.isExample <&&> isProp header.type) then
         newHeaders ←
           withLevelNames header.levelNames do
             return newHeaders.push { header with type := (← levelMVarToParam header.type), levelNames := (← getLevelNames) }

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -199,7 +199,7 @@ def evalTacticCDot : Tactic := fun stx => do
   -- but the token antiquotation does not copy trailing whitespace, leading to
   -- differences in the goal display (#2153)
   let initInfo ← mkInitialTacticInfo stx[0]
-  withRef stx[0] <| closeUsingOrAdmit do
+  withCaseRef stx[0] stx[1] <| closeUsingOrAdmit do
     -- save state before/after entering focus on `·`
     withInfoContext (pure ()) initInfo
     Term.withNarrowedArgTacticReuse (argIdx := 1) evalTactic stx

src/Lean/Elab/Tactic/Doc.lean

@@ -0,0 +1,178 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Thrane Christiansen
+-/
+prelude
+import Lean.DocString
+import Lean.Elab.Command
+import Lean.Parser.Tactic.Doc
+import Lean.Parser.Command
+
+namespace Lean.Elab.Tactic.Doc
+open Lean.Parser.Tactic.Doc
+open Lean.Elab.Command
+open Lean.Parser.Command
+
+@[builtin_command_elab «tactic_extension»] def elabTacticExtension : CommandElab
+  | `(«tactic_extension»|tactic_extension%$cmd $_) => do
+    throwErrorAt cmd "Missing documentation comment"
+  | `(«tactic_extension»|$docs:docComment tactic_extension $tac:ident) => do
+    let tacName ← liftTermElabM <| realizeGlobalConstNoOverloadWithInfo tac
+
+    if let some tgt' := alternativeOfTactic (← getEnv) tacName then
+        throwErrorAt tac "'{tacName}' is an alternative form of '{tgt'}'"
+    if !(isTactic (← getEnv) tacName) then
+      throwErrorAt tac "'{tacName}' is not a tactic"
+
+    modifyEnv (tacticDocExtExt.addEntry · (tacName, docs.getDocString))
+    pure ()
+  | _ => throwError "Malformed tactic extension command"
+
+@[builtin_command_elab «register_tactic_tag»] def elabRegisterTacticTag : CommandElab
+  | `(«register_tactic_tag»|$[$doc:docComment]? register_tactic_tag $tag:ident $user:str) => do
+    let docstring ← doc.mapM getDocStringText
+    modifyEnv (knownTacticTagExt.addEntry · (tag.getId, user.getString, docstring))
+  | _ => throwError "Malformed 'register_tactic_tag' command"
+
+/--
+Gets the first string token in a parser description. For example, for a declaration like
+`syntax "squish " term " with " term : tactic`, it returns `some "squish "`, and for a declaration
+like `syntax tactic " <;;;> " tactic : tactic`, it returns `some " <;;;> "`.
+
+Returns `none` for syntax declarations that don't contain a string constant.
+-/
+private partial def getFirstTk (e : Expr) : MetaM (Option String) := do
+  match (← Meta.whnf e).getAppFnArgs with
+  | (``ParserDescr.node, #[_, _, p]) => getFirstTk p
+  | (``ParserDescr.trailingNode, #[_, _, _, p]) => getFirstTk p
+  | (``ParserDescr.unary, #[.app _ (.lit (.strVal "withPosition")), p]) => getFirstTk p
+  | (``ParserDescr.unary, #[.app _ (.lit (.strVal "atomic")), p]) => getFirstTk p
+  | (``ParserDescr.binary, #[.app _ (.lit (.strVal "andthen")), p, _]) => getFirstTk p
+  | (``ParserDescr.nonReservedSymbol, #[.lit (.strVal tk), _]) => pure (some tk)
+  | (``ParserDescr.symbol, #[.lit (.strVal tk)]) => pure (some tk)
+  | (``Parser.withAntiquot, #[_, p]) => getFirstTk p
+  | (``Parser.leadingNode, #[_, _, p]) => getFirstTk p
+  | (``HAndThen.hAndThen, #[_, _, _, _, p1, p2]) =>
+    if let some tk ← getFirstTk p1 then pure (some tk)
+    else getFirstTk (.app p2 (.const ``Unit.unit []))
+  | (``Parser.nonReservedSymbol, #[.lit (.strVal tk), _]) => pure (some tk)
+  | (``Parser.symbol, #[.lit (.strVal tk)]) => pure (some tk)
+  | _ => pure none
+
+
+/--
+Creates some `MessageData` for a parser name.
+
+If the parser name maps to a description with an
+identifiable leading token, then that token is shown. Otherwise, the underlying name is shown
+without an `@`. The name includes metadata that makes infoview hovers and the like work. This
+only works for global constants, as the local context is not included.
+-/
+private def showParserName (n : Name) : MetaM MessageData := do
+  let env ← getEnv
+  let params :=
+    env.constants.find?' n |>.map (·.levelParams.map Level.param) |>.getD []
+  let tok ←
+    if let some descr := env.find? n |>.bind (·.value?) then
+      if let some tk ← getFirstTk descr then
+        pure <| Std.Format.text tk.trim
+      else pure <| format n
+    else pure <| format n
+  pure <| .ofFormatWithInfos {
+    fmt := "'" ++ .tag 0 tok ++ "'",
+    infos :=
+      .fromList [(0, .ofTermInfo {
+        lctx := .empty,
+        expr := .const n params,
+        stx := .ident .none (toString n).toSubstring n [.decl n []],
+        elaborator := `Delab,
+        expectedType? := none
+      })] _
+  }
+
+
+/--
+Displays all available tactic tags, with documentation.
+-/
+@[builtin_command_elab printTacTags] def elabPrintTacTags : CommandElab := fun _stx => do
+  let all :=
+    tacticTagExt.toEnvExtension.getState (← getEnv)
+      |>.importedEntries |>.push (tacticTagExt.exportEntriesFn (tacticTagExt.getState (← getEnv)))
+  let mut mapping : NameMap NameSet := {}
+  for arr in all do
+    for (tac, tag) in arr do
+      mapping := mapping.insert tag (mapping.findD tag {} |>.insert tac)
+
+  let showDocs : Option String → MessageData
+    | none => .nil
+    | some d => Format.line ++ MessageData.joinSep ((d.splitOn "\n").map toMessageData) Format.line
+
+  let showTactics (tag : Name) : MetaM MessageData := do
+    match mapping.find? tag with
+    | none => pure .nil
+    | some tacs =>
+      if tacs.isEmpty then pure .nil
+      else
+        let tacs := tacs.toArray.qsort (·.toString < ·.toString) |>.toList
+        pure (Format.line ++ MessageData.joinSep (← tacs.mapM showParserName) ", ")
+
+  let tagDescrs ← liftTermElabM <| (← allTagsWithInfo).mapM fun (name, userName, docs) => do
+    pure <| m!"• " ++
+      MessageData.nestD (m!"'{name}'" ++
+        (if name.toString != userName then m!" — \"{userName}\"" else MessageData.nil) ++
+        showDocs docs ++
+        (← showTactics name))
+
+  let tagList : MessageData :=
+    m!"Available tags: {MessageData.nestD (Format.line ++ .joinSep tagDescrs Format.line)}"
+
+  logInfo tagList
+
+/--
+The information needed to display all documentation for a tactic.
+-/
+structure TacticDoc where
+  /-- The name of the canonical parser for the tactic -/
+  internalName : Name
+  /-- The user-facing name to display (typically the first keyword token) -/
+  userName : String
+  /-- The tags that have been applied to the tactic -/
+  tags : NameSet
+  /-- The docstring for the tactic -/
+  docString : Option String
+  /-- Any docstring extensions that have been specified -/
+  extensionDocs : Array String
+
+def allTacticDocs : MetaM (Array TacticDoc) := do
+  let env ← getEnv
+  let all :=
+    tacticTagExt.toEnvExtension.getState (← getEnv)
+      |>.importedEntries |>.push (tacticTagExt.exportEntriesFn (tacticTagExt.getState (← getEnv)))
+  let mut tacTags : NameMap NameSet := {}
+  for arr in all do
+    for (tac, tag) in arr do
+      tacTags := tacTags.insert tac (tacTags.findD tac {} |>.insert tag)
+
+  let mut docs := #[]
+
+  let some tactics := (Lean.Parser.parserExtension.getState env).categories.find? `tactic
+    | return #[]
+  for (tac, _) in tactics.kinds do
+    -- Skip noncanonical tactics
+    if let some _ := alternativeOfTactic env tac then continue
+    let userName : String ←
+      if let some descr := env.find? tac |>.bind (·.value?) then
+        if let some tk ← getFirstTk descr then
+          pure tk.trim
+        else pure tac.toString
+      else pure tac.toString
+
+    docs := docs.push {
+      internalName := tac,
+      userName := userName,
+      tags := tacTags.findD tac {},
+      docString := ← findDocString? env tac,
+      extensionDocs := getTacticExtensions env tac
+    }
+  return docs

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -22,12 +22,15 @@ Runs a term elaborator inside a tactic.
 This function ensures that term elaboration fails when backtracking,
 i.e., in `first| tac term | other`.
 -/
-def runTermElab (k : TermElabM α) (mayPostpone := false) : TacticM α := do
-  /- If error recovery is disabled, we disable `Term.withoutErrToSorry` -/
-  if (← read).recover then
-    go
-  else
-    Term.withoutErrToSorry go
+def runTermElab (k : TermElabM α) (mayPostpone := false) : TacticM α :=
+  -- We disable incrementality here so that nested tactics do not unexpectedly use and affect the
+  -- incrementality state of a calling incrementality-enabled tactic.
+  Term.withoutTacticIncrementality true do
+    /- If error recovery is disabled, we disable `Term.withoutErrToSorry` -/
+    if (← read).recover then
+      go
+    else
+      Term.withoutErrToSorry go
 where
   go := k <* Term.synthesizeSyntheticMVars (postpone := .ofBool mayPostpone)
 

src/Lean/Elab/Term.lean

@@ -1259,8 +1259,8 @@ private def isNoImplicitLambda (stx : Syntax) : Bool :=
 
 private def isTypeAscription (stx : Syntax) : Bool :=
   match stx with
-  | `(($_ : $_)) => true
-  | _            => false
+  | `(($_ : $[$_]?)) => true
+  | _                => false
 
 def hasNoImplicitLambdaAnnotation (type : Expr) : Bool :=
   annotation? `noImplicitLambda type |>.isSome

src/Lean/Environment.lean

@@ -423,22 +423,51 @@ structure ImportM.Context where
 
 abbrev ImportM := ReaderT Lean.ImportM.Context IO
 
-/-- An environment extension with support for storing/retrieving entries from a .olean file.
-   - α is the type of the entries that are stored in .olean files.
-   - β is the type of values used to update the state.
-   - σ is the actual state.
+/--
+An environment extension with support for storing/retrieving entries from a .olean file.
+ - α is the type of the entries that are stored in .olean files.
+ - β is the type of values used to update the state.
+ - σ is the actual state.
 
-   Remark: for most extensions α and β coincide.
+For most extensions, α and β coincide. `α` and ‵β` do not coincide for extensions where the data
+used to update the state contains elements which cannot be stored in files (for example, closures).
 
-   Note that `addEntryFn` is not in `IO`. This is intentional, and allows us to write simple functions such as
-   ```
-   def addAlias (env : Environment) (a : Name) (e : Name) : Environment :=
-   aliasExtension.addEntry env (a, e)
-   ```
-   without using `IO`. We have many functions like `addAlias`.
+During elaboration of a module, state of type `σ` can be both read and written. When elaboration is
+complete, the state of type `σ` is converted to serialized state of type `Array α` by
+`exportEntriesFn`. To read the current module's state, use `PersistentEnvExtension.getState`. To
+modify it, use `PersistentEnvExtension.addEntry`, with an `addEntryFn` that performs the appropriate
+modification.
 
-   `α` and ‵β` do not coincide for extensions where the data used to update the state contains, for example,
-   closures which we currently cannot store in files. -/
+When a module is loaded, the values saved by all of its dependencies for this
+`PersistentEnvExtension` are are available as an `Array (Array α)` via the environment extension,
+with one array per transitively imported module. The state of type `σ` used in the current module
+can be initialized from these imports by specifying a suitable `addImportedFn`. The `addImportedFn`
+runs at the beginning of elaboration for every module, so it's usually better for performance to
+query the array of imported modules directly, because only a fraction of imported entries is usually
+queried during elaboration of a module.
+
+The most typical pattern for using `PersistentEnvExtension` is to set `σ` to a datatype such as
+`NameMap` that efficiently tracks data for the current module. Then, in `exportEntriesFn`, this type
+is converted to an array of pairs, sorted by the key. Given `ext : PersistentEnvExtension α β σ` and
+`env : Environment`, the complete array of imported entries sorted by module index can be obtained
+using `(ext.toEnvExtension.getState env).importedEntries`. To query the extension for some constant
+name `n`, first use `env.getModuleIdxFor? n`. If it returns `none`, look up `n` in the current
+module's state (the `NameMap`). If it returns `some idx`, use `ext.getModuleEntries env idx` to get
+the array of entries for `n`'s defining module, and query it using `Array.binSearch`. This pattern
+imposes a constraint that the extension can only track metadata that is declared in the same module
+as the definition to which it applies; relaxing this restriction can make queries slower due to
+needing to search _all_ modules. If it is necessary to search all modules, it is usually better to
+initialize the state of type `σ` once from all imported entries and choose a more efficient search
+datastructure for it.
+
+Note that `addEntryFn` is not in `IO`. This is intentional, and allows us to write simple functions
+such as
+```
+def addAlias (env : Environment) (a : Name) (e : Name) : Environment :=
+aliasExtension.addEntry env (a, e)
+```
+without using `IO`. We have many functions like `addAlias`.
+-/
 structure PersistentEnvExtension (α : Type) (β : Type) (σ : Type) where
   toEnvExtension  : EnvExtension (PersistentEnvExtensionState α σ)
   name            : Name

src/Lean/Meta/AbstractMVars.lean

@@ -7,13 +7,6 @@ prelude
 import Lean.Meta.Basic
 
 namespace Lean.Meta
-
-structure AbstractMVarsResult where
-  paramNames : Array Name
-  numMVars   : Nat
-  expr       : Expr
-  deriving Inhabited, BEq
-
 namespace AbstractMVars
 
 structure State where

src/Lean/Meta/Basic.lean

@@ -222,7 +222,14 @@ structure SynthInstanceCacheKey where
   synthPendingDepth : Nat
   deriving Hashable, BEq
 
-abbrev SynthInstanceCache := PersistentHashMap SynthInstanceCacheKey (Option Expr)
+/-- Resulting type for `abstractMVars` -/
+structure AbstractMVarsResult where
+  paramNames : Array Name
+  numMVars   : Nat
+  expr       : Expr
+  deriving Inhabited, BEq
+
+abbrev SynthInstanceCache := PersistentHashMap SynthInstanceCacheKey (Option AbstractMVarsResult)
 
 abbrev InferTypeCache := PersistentExprStructMap Expr
 abbrev FunInfoCache   := PersistentHashMap InfoCacheKey FunInfo

src/Lean/Meta/Constructions.lean

@@ -8,10 +8,10 @@ import Lean.AuxRecursor
 import Lean.AddDecl
 import Lean.Meta.AppBuilder
 import Lean.Meta.CompletionName
+import Lean.Meta.Constructions.RecOn
 
 namespace Lean
 
-@[extern "lean_mk_rec_on"] opaque mkRecOnImp (env : Environment) (declName : @& Name) : Except KernelException Declaration
 @[extern "lean_mk_cases_on"] opaque mkCasesOnImp (env : Environment) (declName : @& Name) : Except KernelException Declaration
 @[extern "lean_mk_no_confusion_type"] opaque mkNoConfusionTypeCoreImp (env : Environment) (declName : @& Name) : Except KernelException Declaration
 @[extern "lean_mk_no_confusion"] opaque mkNoConfusionCoreImp (env : Environment) (declName : @& Name) : Except KernelException Declaration
@@ -20,14 +20,6 @@ namespace Lean
 
 open Meta
 
-def mkRecOn (declName : Name) : MetaM Unit := do
-  let name := mkRecOnName declName
-  let decl ← ofExceptKernelException (mkRecOnImp (← getEnv) declName)
-  addDecl decl
-  setReducibleAttribute name
-  modifyEnv fun env => markAuxRecursor env name
-  modifyEnv fun env => addProtected env name
-
 def mkCasesOn (declName : Name) : MetaM Unit := do
   let name := mkCasesOnName declName
   let decl ← ofExceptKernelException (mkCasesOnImp (← getEnv) declName)

src/Lean/Meta/Constructions/RecOn.lean

@@ -0,0 +1,35 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Joachim Breitner
+-/
+prelude
+import Lean.Meta.InferType
+import Lean.AuxRecursor
+import Lean.AddDecl
+import Lean.Meta.CompletionName
+
+open Lean Meta
+
+def mkRecOn (n : Name) : MetaM Unit := do
+  let .recInfo recInfo ← getConstInfo (mkRecName n)
+    | throwError "{mkRecName n} not a recinfo"
+  let decl ← forallTelescope recInfo.type fun xs t => do
+    let e := .const recInfo.name (recInfo.levelParams.map (.param ·))
+    let e := mkAppN e xs
+    -- We reorder the parameters
+    -- before: As Cs minor_premises indices major-premise
+    -- fow:    As Cs indices major-premise minor-premises
+    let AC_size := xs.size - recInfo.numMinors - recInfo.numIndices - 1
+    let vs :=
+      xs[:AC_size] ++
+      xs[AC_size + recInfo.numMinors:AC_size + recInfo.numMinors + 1 + recInfo.numIndices] ++
+      xs[AC_size:AC_size + recInfo.numMinors]
+    let type ← mkForallFVars vs t
+    let value ← mkLambdaFVars vs e
+    mkDefinitionValInferrringUnsafe (mkRecOnName n) recInfo.levelParams type value .abbrev
+
+  addDecl (.defnDecl decl)
+  setReducibleAttribute decl.name
+  modifyEnv fun env => markAuxRecursor env decl.name
+  modifyEnv fun env => addProtected env decl.name

src/Lean/Meta/IndPredBelow.lean

@@ -434,7 +434,7 @@ partial def mkBelowMatcher
   withExistingLocalDecls (lhss.foldl (init := []) fun s v => s ++ v.fvarDecls) do
     for lhs in lhss do
       trace[Meta.IndPredBelow.match] "{lhs.patterns.map (·.toMessageData)}"
-  let res ← Match.mkMatcher { matcherName, matchType, discrInfos := mkArray (mkMatcherInput.numDiscrs + 1) {}, lhss }
+  let res ← Match.mkMatcher (exceptionIfContainsSorry := true) { matcherName, matchType, discrInfos := mkArray (mkMatcherInput.numDiscrs + 1) {}, lhss }
   res.addMatcher
   -- if a wrong index is picked, the resulting matcher can be type-incorrect.
   -- we check here, so that errors can propagate higher up the call stack.

src/Lean/Meta/Match/Match.lean

@@ -830,8 +830,12 @@ Each `AltLHS` has a list of local declarations and a list of patterns.
 The number of patterns must be the same in each `AltLHS`.
 The generated matcher has the structure described at `MatcherInfo`. The motive argument is of the form
 `(motive : (a_1 : A_1) -> (a_2 : A_2[a_1]) -> ... -> (a_n : A_n[a_1, a_2, ... a_{n-1}]) -> Sort v)`
-where `v` is a universe parameter or 0 if `B[a_1, ..., a_n]` is a proposition. -/
-def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult := withCleanLCtxFor input do
+where `v` is a universe parameter or 0 if `B[a_1, ..., a_n]` is a proposition.
+
+If `exceptionIfContainsSorry := true`, then `mkMatcher` throws an exception if the auxiliary
+declarations contains a `sorry`. We use this argument to workaround a bug at `IndPredBelow.mkBelowMatcher`.
+-/
+def mkMatcher (input : MkMatcherInput) (exceptionIfContainsSorry := false) : MetaM MatcherResult := withCleanLCtxFor input do
   let ⟨matcherName, matchType, discrInfos, lhss⟩ := input
   let numDiscrs := discrInfos.size
   let numEqs := getNumEqsFromDiscrInfos discrInfos
@@ -844,6 +848,11 @@ def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult := withCleanLCtxFor
   let uElim ← getLevel matchTypeBody
   let uElimGen ← if uElim == levelZero then pure levelZero else mkFreshLevelMVar
   let mkMatcher (type val : Expr) (minors : Array (Expr × Nat)) (s : State) : MetaM MatcherResult := do
+    let val ← instantiateMVars val
+    let type ← instantiateMVars type
+    if exceptionIfContainsSorry then
+      if type.hasSorry || val.hasSorry then
+        throwError "failed to create auxiliary match declaration `{matcherName}`, it contains `sorry`"
     trace[Meta.Match.debug] "matcher value: {val}\ntype: {type}"
     trace[Meta.Match.debug] "minors num params: {minors.map (·.2)}"
     /- The option `bootstrap.gen_matcher_code` is a helper hack. It is useful, for example,
@@ -857,7 +866,6 @@ def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult := withCleanLCtxFor
        | negSucc n => succ n
        ```
        which is defined **before** `Int.decLt` -/
-
     let (matcher, addMatcher) ← mkMatcherAuxDefinition matcherName type val
     trace[Meta.Match.debug] "matcher levels: {matcher.getAppFn.constLevels!}, uElim: {uElimGen}"
     let uElimPos? ← getUElimPos? matcher.getAppFn.constLevels! uElimGen

src/Lean/Meta/SynthInstance.lean

@@ -698,6 +698,83 @@ private def preprocessOutParam (type : Expr) : MetaM Expr :=
   Remark: we use a different option for controlling the maximum result size for coercions.
 -/
 
+private def assignOutParams (type : Expr) (result : Expr) : MetaM Bool := do
+  let resultType ← inferType result
+  /- Output parameters of local instances may be marked as `syntheticOpaque` by the application-elaborator.
+      We use `withAssignableSyntheticOpaque` to make sure this kind of parameter can be assigned by the following `isDefEq`.
+      TODO: rewrite this check to avoid `withAssignableSyntheticOpaque`. -/
+  let defEq ← withDefault <| withAssignableSyntheticOpaque <| isDefEq type resultType
+  unless defEq do
+    trace[Meta.synthInstance] "{crossEmoji} result type{indentExpr resultType}\nis not definitionally equal to{indentExpr type}"
+  return defEq
+
+/--
+Auxiliary function for converting the `AbstractMVarsResult` returned by `SynthIntance.main` into an `Expr`.
+-/
+private def applyAbstractResult? (type : Expr) (abstResult? : Option AbstractMVarsResult) : MetaM (Option Expr) := do
+  let some abstResult := abstResult? | return none
+  let (_, _, result) ← openAbstractMVarsResult abstResult
+  unless (← assignOutParams type result) do return none
+  let result ← instantiateMVars result
+  /- We use `check` to propagate universe constraints implied by the `result`.
+      Recall that we use `allowLevelAssignments := true` which allows universe metavariables in the current depth to be assigned,
+      but these assignments are discarded by `withNewMCtxDepth`.
+
+      TODO: If this `check` is a performance bottleneck, we can improve performance by tracking whether
+            a universe metavariable from previous universe levels have been assigned or not during TC resolution.
+            We only need to perform the `check` if this kind of assignment have been performed.
+
+      The example in the issue #796 exposed this issue.
+      ```
+      structure A
+      class B (a : outParam A) (α : Sort u)
+      class C {a : A} (α : Sort u) [B a α]
+      class D {a : A} (α : Sort u) [B a α] [c : C α]
+      class E (a : A) where [c (α : Sort u) [B a α] : C α]
+      instance c {a : A} [e : E a] (α : Sort u) [B a α] : C α := e.c α
+
+      def d {a : A} [e : E a] (α : Sort u) [b : B a α] : D α := ⟨⟩
+      ```
+      The term `D α` has two instance implicit arguments. The second one has type `C α`, and TC
+      resolution produces the result `@c.{u} a e α b`.
+      Note that the `e` has type `E.{?v} a`, and `E` is universe polymorphic,
+      but the universe does not occur in the parameter `a`. We have that `?v := u` is implied by `@c.{u} a e α b`,
+      but this assignment is lost.
+  -/
+  check result
+  return some result
+
+/--
+Auxiliary function for converting a cached `AbstractMVarsResult` returned by `SynthIntance.main` into an `Expr`.
+This function tries to avoid the potentially expensive `check` at `applyCachedAbstractResult?`.
+-/
+private def applyCachedAbstractResult? (type : Expr) (abstResult? : Option AbstractMVarsResult) : MetaM (Option Expr) := do
+  let some abstResult := abstResult? | return none
+  if abstResult.numMVars == 0 && abstResult.paramNames.isEmpty then
+    /-
+    Result does not instroduce new metavariables, thus we don't need to perform (again)
+    the `check` at `applyAbstractResult?`.
+    This is an optimization.
+    -/
+    unless (← assignOutParams type abstResult.expr) do
+      return none
+    return some abstResult.expr
+  else
+    applyAbstractResult? type abstResult?
+
+/-- Helper function for caching synthesized type class instances. -/
+private def cacheResult (cacheKey : SynthInstanceCacheKey) (abstResult? : Option AbstractMVarsResult) (result? : Option Expr) : MetaM Unit := do
+  match result? with
+  | none => modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert cacheKey none }
+  | some result =>
+    let some abstResult := abstResult? | return ()
+    if abstResult.numMVars == 0 && abstResult.paramNames.isEmpty then
+      -- See `applyCachedAbstractResult?` If new metavariables have **not** been introduced,
+      -- we don't need to perform extra checks again when reusing result.
+      modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert cacheKey (some { expr := result, paramNames := #[], numMVars := 0 }) }
+    else
+      modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert cacheKey (some abstResult) }
+
 def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (Option Expr) := do profileitM Exception "typeclass inference" (← getOptions) (decl := type.getAppFn.constName?.getD .anonymous) do
   let opts ← getOptions
   let maxResultSize := maxResultSize?.getD (synthInstance.maxSize.get opts)
@@ -709,66 +786,20 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
     let localInsts ← getLocalInstances
     let type ← instantiateMVars type
     let type ← preprocess type
-    let s ← get
-    let rec assignOutParams (result : Expr) : MetaM Bool := do
-      let resultType ← inferType result
-      /- Output parameters of local instances may be marked as `syntheticOpaque` by the application-elaborator.
-         We use `withAssignableSyntheticOpaque` to make sure this kind of parameter can be assigned by the following `isDefEq`.
-         TODO: rewrite this check to avoid `withAssignableSyntheticOpaque`. -/
-      let defEq ← withDefault <| withAssignableSyntheticOpaque <| isDefEq type resultType
-      unless defEq do
-        trace[Meta.synthInstance] "{crossEmoji} result type{indentExpr resultType}\nis not definitionally equal to{indentExpr type}"
-      return defEq
     let cacheKey := { localInsts, type, synthPendingDepth := (← read).synthPendingDepth }
-    match s.cache.synthInstance.find? cacheKey with
-    | some result =>
-      trace[Meta.synthInstance] "result {result} (cached)"
-      if let some inst := result then
-        unless (← assignOutParams inst) do
-          return none
-      pure result
-    | none        =>
-      let result? ← withNewMCtxDepth (allowLevelAssignments := true) do
+    match (← get).cache.synthInstance.find? cacheKey with
+    | some abstResult? =>
+      let result? ← applyCachedAbstractResult? type abstResult?
+      trace[Meta.synthInstance] "result {result?} (cached)"
+      return result?
+    | none =>
+      let abstResult? ← withNewMCtxDepth (allowLevelAssignments := true) do
         let normType ← preprocessOutParam type
         SynthInstance.main normType maxResultSize
-      let result? ← match result? with
-        | none        => pure none
-        | some result => do
-          let (_, _, result) ← openAbstractMVarsResult result
-          trace[Meta.synthInstance] "result {result}"
-          if (← assignOutParams result) then
-            let result ← instantiateMVars result
-            /- We use `check` to propagate universe constraints implied by the `result`.
-               Recall that we use `allowLevelAssignments := true` which allows universe metavariables in the current depth to be assigned,
-               but these assignments are discarded by `withNewMCtxDepth`.
-
-               TODO: If this `check` is a performance bottleneck, we can improve performance by tracking whether
-                     a universe metavariable from previous universe levels have been assigned or not during TC resolution.
-                     We only need to perform the `check` if this kind of assignment have been performed.
-
-               The example in the issue #796 exposed this issue.
-               ```
-                structure A
-                class B (a : outParam A) (α : Sort u)
-                class C {a : A} (α : Sort u) [B a α]
-                class D {a : A} (α : Sort u) [B a α] [c : C α]
-                class E (a : A) where [c (α : Sort u) [B a α] : C α]
-                instance c {a : A} [e : E a] (α : Sort u) [B a α] : C α := e.c α
-
-                def d {a : A} [e : E a] (α : Sort u) [b : B a α] : D α := ⟨⟩
-               ```
-               The term `D α` has two instance implicit arguments. The second one has type `C α`, and TC
-               resolution produces the result `@c.{u} a e α b`.
-               Note that the `e` has type `E.{?v} a`, and `E` is universe polymorphic,
-               but the universe does not occur in the parameter `a`. We have that `?v := u` is implied by `@c.{u} a e α b`,
-               but this assignment is lost.
-            -/
-            check result
-            pure (some result)
-          else
-            pure none
-      modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert cacheKey result? }
-      pure result?
+      let result? ← applyAbstractResult? type abstResult?
+      trace[Meta.synthInstance] "result {result?}"
+      cacheResult cacheKey abstResult? result?
+      return result?
 
 /--
   Return `LOption.some r` if succeeded, `LOption.none` if it failed, and `LOption.undef` if

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean

@@ -25,6 +25,12 @@ def fromExpr? (e : Expr) : SimpM (Option Int) :=
   let some v₂ ← fromExpr? e.appArg! | return .continue
   return .done <| toExpr (op v₁ v₂)
 
+def reduceBinIntNatOp (name : Name) (op : Int → Nat → Int) (e : Expr) : SimpM DStep := do
+  unless e.isAppOfArity name 2 do return .continue
+  let some v₁ ← getIntValue? e.appFn!.appArg! | return .continue
+  let some v₂ ← getNatValue? e.appArg! | return .continue
+  return .done <| toExpr (op v₁ v₂)
+
 @[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : Int → Int → Bool) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue
@@ -65,6 +71,12 @@ builtin_dsimproc [simp, seval] reduceMul ((_ * _ : Int)) := reduceBin ``HMul.hMu
 builtin_dsimproc [simp, seval] reduceSub ((_ - _ : Int)) := reduceBin ``HSub.hSub 6 (· - ·)
 builtin_dsimproc [simp, seval] reduceDiv ((_ / _ : Int)) := reduceBin ``HDiv.hDiv 6 (· / ·)
 builtin_dsimproc [simp, seval] reduceMod ((_ % _ : Int)) := reduceBin ``HMod.hMod 6 (· % ·)
+builtin_dsimproc [simp, seval] reduceTDiv (div  _ _) := reduceBin ``Int.div 2 Int.div
+builtin_dsimproc [simp, seval] reduceTMod (mod  _ _) := reduceBin ``Int.mod 2 Int.mod
+builtin_dsimproc [simp, seval] reduceFDiv (fdiv _ _) := reduceBin ``Int.fdiv 2 Int.fdiv
+builtin_dsimproc [simp, seval] reduceFMod (fmod _ _) := reduceBin ``Int.fmod 2 Int.fmod
+builtin_dsimproc [simp, seval] reduceBdiv (bdiv _ _) := reduceBinIntNatOp ``bdiv bdiv
+builtin_dsimproc [simp, seval] reduceBmod (bmod _ _) := reduceBinIntNatOp ``bmod bmod
 
 builtin_dsimproc [simp, seval] reducePow ((_ : Int) ^ (_ : Nat)) := fun e => do
   let_expr HPow.hPow _ _ _ _ a b ← e | return .continue

src/Lean/Parser.lean

@@ -12,6 +12,7 @@ import Lean.Parser.Command
 import Lean.Parser.Module
 import Lean.Parser.Syntax
 import Lean.Parser.Do
+import Lean.Parser.Tactic.Doc
 
 namespace Lean
 namespace Parser

src/Lean/Parser/Attr.lean

@@ -50,6 +50,24 @@ def externEntry := leading_parser
 @[builtin_attr_parser] def extern     := leading_parser
   nonReservedSymbol "extern" >> optional (ppSpace >> numLit) >> many (ppSpace >> externEntry)
 
+/--
+Declare this tactic to be an alias or alternative form of an existing tactic.
+
+This has the following effects:
+ * The alias relationship is saved
+ * The docstring is taken from the original tactic, if present
+-/
+@[builtin_attr_parser] def «tactic_alt» := leading_parser
+  "tactic_alt" >> ppSpace >> ident
+
+/--
+Add one or more tags to a tactic.
+
+Tags should be applied to the canonical names for tactics.
+-/
+@[builtin_attr_parser] def «tactic_tag» := leading_parser
+  "tactic_tag" >> many1 (ppSpace >> ident)
+
 end Attr
 
 end Lean.Parser

src/Lean/Parser/Command.lean

@@ -447,6 +447,11 @@ structure Pair (α : Type u) (β : Type v) : Type (max u v) where
   "#print " >> nonReservedSymbol "axioms " >> ident
 @[builtin_command_parser] def printEqns      := leading_parser
   "#print " >> (nonReservedSymbol "equations " <|> nonReservedSymbol "eqns ") >> ident
+/--
+Displays all available tactic tags, with documentation.
+-/
+@[builtin_command_parser] def printTacTags   := leading_parser
+  "#print " >> nonReservedSymbol "tactic " >> nonReservedSymbol "tags"
 @[builtin_command_parser] def «init_quot»    := leading_parser
   "init_quot"
 def optionValue := nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> strLit <|> numLit
@@ -669,6 +674,26 @@ Documentation can only be added to declarations in the same module.
 @[builtin_command_parser] def addDocString := leading_parser
   docComment >> "add_decl_doc " >> ident
 
+/--
+Register a tactic tag, saving its user-facing name and docstring.
+
+Tactic tags can be used by documentation generation tools to classify related tactics.
+-/
+@[builtin_command_parser] def «register_tactic_tag» := leading_parser
+  optional (docComment >> ppLine) >>
+  "register_tactic_tag " >> ident >> strLit
+
+/--
+Add more documentation as an extension of the documentation for a given tactic.
+
+The extended documentation is placed in the command's docstring. It is shown as part of a bulleted
+list, so it should be brief.
+-/
+@[builtin_command_parser] def «tactic_extension» := leading_parser
+  optional (docComment >> ppLine) >>
+  "tactic_extension " >> ident
+
+
 /--
   This is an auxiliary command for generation constructor injectivity theorems for
   inductive types defined at `Prelude.lean`.

src/Lean/Parser/Tactic.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
 import Lean.Parser.Term
+import Lean.Parser.Tactic.Doc
 
 namespace Lean
 namespace Parser

src/Lean/Parser/Tactic/Doc.lean

@@ -0,0 +1,290 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Thrane Christiansen
+-/
+prelude
+import Lean.Attributes
+import Lean.DocString.Extension
+import Lean.Elab.InfoTree.Main
+import Lean.Parser.Attr
+import Lean.Parser.Extension
+
+set_option linter.missingDocs true
+
+namespace Lean.Parser.Tactic.Doc
+
+open Lean.Parser (registerParserAttributeHook)
+open Lean.Parser.Attr
+
+/-- Check whether a name is a tactic syntax kind -/
+def isTactic (env : Environment) (kind : Name) : Bool := Id.run do
+  let some tactics := (Lean.Parser.parserExtension.getState env).categories.find? `tactic
+    | return false
+  for (tac, _) in tactics.kinds do
+    if kind == tac then return true
+  return false
+
+/--
+Stores a collection of *tactic alternatives*, to track which new syntax rules represent new forms of
+existing tactics.
+-/
+builtin_initialize tacticAlternativeExt
+    : PersistentEnvExtension (Name × Name) (Name × Name) (NameMap Name) ←
+  registerPersistentEnvExtension {
+    mkInitial := pure {},
+    addImportedFn := fun _ => pure {},
+    addEntryFn := fun as (src, tgt) => as.insert src tgt,
+    exportEntriesFn := fun es =>
+      es.fold (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1)
+  }
+
+/--
+If `tac` is registered as the alternative form of another tactic, then return the canonical name for
+it.
+-/
+def alternativeOfTactic (env : Environment) (tac : Name) : Option Name :=
+  match env.getModuleIdxFor? tac with
+  | some modIdx =>
+    match (tacticAlternativeExt.getModuleEntries env modIdx).binSearch (tac, .anonymous) (Name.quickLt ·.1 ·.1) with
+    | some (_, val) => some val
+    | none => none
+  | none => tacticAlternativeExt.getState env |>.find? tac
+
+/--
+Find all alternatives for a given canonical tactic name.
+-/
+def aliases [Monad m] [MonadEnv m] (tac : Name) : m NameSet := do
+  let env ← getEnv
+  let mut found := {}
+  for (src, tgt) in tacticAlternativeExt.getState env do
+    if tgt == tac then found := found.insert src
+  for arr in tacticAlternativeExt.toEnvExtension.getState env |>.importedEntries do
+    for (src, tgt) in arr do
+      if tgt == tac then found := found.insert src
+  pure found
+
+builtin_initialize
+  let name := `tactic_alt
+  registerBuiltinAttribute {
+    name := name,
+    ref := by exact decl_name%,
+    add := fun decl stx kind => do
+      unless kind == AttributeKind.global do throwError "invalid attribute '{name}', must be global"
+      unless ((← getEnv).getModuleIdxFor? decl).isNone do
+        throwError "invalid attribute '{name}', declaration is in an imported module"
+      let `(«tactic_alt»|tactic_alt $tgt) := stx
+        | throwError "invalid syntax for '{name}' attribute"
+
+      let tgtName ← Lean.Elab.realizeGlobalConstNoOverloadWithInfo tgt
+
+      if !(isTactic (← getEnv) tgtName) then throwErrorAt tgt "'{tgtName}' is not a tactic"
+      -- If this condition is true, then we're in an `attribute` command and can validate here.
+      if (← getEnv).find? decl |>.isSome then
+        if !(isTactic (← getEnv) decl) then throwError "'{decl}' is not a tactic"
+
+      if let some tgt' := alternativeOfTactic (← getEnv) tgtName then
+        throwError "'{tgtName}' is itself an alternative for '{tgt'}'"
+      modifyEnv fun env => tacticAlternativeExt.addEntry env (decl, tgtName)
+      if (← findSimpleDocString? (← getEnv) decl).isSome then
+        logWarningAt stx m!"Docstring for '{decl}' will be ignored because it is an alternative"
+
+    descr :=
+      "Register a tactic parser as an alternative form of an existing tactic, so they " ++
+      "can be grouped together in documentation.",
+    -- This runs prior to elaboration because it allows a check for whether the decl is present
+    -- in the environment to determine whether we can see if it's a tactic name. This is useful
+    -- when the attribute is applied after definition, using an `attribute` command (error checking
+    -- for the `@[tactic_alt TAC]` syntax is performed by the parser attribute hook). If this
+    -- attribute ran later, then the decl would already be present.
+    applicationTime := .beforeElaboration
+  }
+
+
+/--
+The known tactic tags that allow tactics to be grouped by purpose.
+-/
+builtin_initialize knownTacticTagExt
+    : PersistentEnvExtension
+        (Name × String × Option String)
+        (Name × String × Option String)
+        (NameMap (String × Option String)) ←
+  registerPersistentEnvExtension {
+    mkInitial := pure {},
+    addImportedFn := fun _ => pure {},
+    addEntryFn := fun as (src, tgt) => as.insert src tgt,
+    exportEntriesFn := fun es =>
+      es.fold (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1)
+  }
+
+/--
+Get the user-facing name and docstring for a tactic tag.
+-/
+def tagInfo [Monad m] [MonadEnv m] (tag : Name) : m (Option (String × Option String)) := do
+  let env ← getEnv
+  match env.getModuleIdxFor? tag with
+  | some modIdx =>
+    match (knownTacticTagExt.getModuleEntries env modIdx).binSearch (tag, default) (Name.quickLt ·.1 ·.1) with
+    | some (_, val) => pure (some val)
+    | none => pure none
+  | none => pure (knownTacticTagExt.getState env |>.find? tag)
+
+/-- Enumerate the tactic tags that are available -/
+def allTags [Monad m] [MonadEnv m] : m (List Name) := do
+  let env ← getEnv
+  let mut found : NameSet := {}
+  for (tag, _) in knownTacticTagExt.getState env do
+    found := found.insert tag
+  for arr in knownTacticTagExt.toEnvExtension.getState env |>.importedEntries do
+    for (tag, _) in arr do
+      found := found.insert tag
+  pure (found.toArray.qsort (·.toString < ·.toString) |>.toList)
+
+/-- Enumerate the tactic tags that are available, with their user-facing name and docstring -/
+def allTagsWithInfo [Monad m] [MonadEnv m] : m (List (Name × String × Option String)) := do
+  let env ← getEnv
+  let mut found : NameMap (String × Option String) := {}
+  for (tag, info) in knownTacticTagExt.getState env do
+    found := found.insert tag info
+  for arr in knownTacticTagExt.toEnvExtension.getState env |>.importedEntries do
+    for (tag, info) in arr do
+      found := found.insert tag info
+  let arr := found.fold (init := #[]) (fun arr k v => arr.push (k, v))
+  pure (arr.qsort (·.1.toString < ·.1.toString) |>.toList)
+
+/--
+The mapping between tags and tactics. Tags may be applied in any module, not just the defining
+module for the tactic.
+
+Because this is expected to be augmented regularly, but queried rarely (only when generating
+documentation indices), it is just stored as flat unsorted arrays of pairs. Before it is used for
+some other purpose, consider a new representation.
+
+The first projection in each pair is the tactic name, and the second is the tag name.
+-/
+builtin_initialize tacticTagExt
+    : PersistentEnvExtension (Name × Name) (Name × Name) (NameMap NameSet) ←
+  registerPersistentEnvExtension {
+    mkInitial := pure {},
+    addImportedFn := fun _ => pure {},
+    addEntryFn := fun tags (decl, newTag) => tags.insert decl (tags.findD decl {} |>.insert newTag)
+    exportEntriesFn := fun tags => Id.run do
+      let mut exported := #[]
+      for (decl, dTags) in tags do
+        for t in dTags do
+          exported := exported.push (decl, t)
+      exported
+  }
+
+builtin_initialize
+  let name := `tactic_tag
+  registerBuiltinAttribute {
+    name := name,
+    ref := by exact decl_name%,
+    add := fun decl stx kind => do
+      unless kind == AttributeKind.global do throwError "invalid attribute '{name}', must be global"
+      let `(«tactic_tag»|tactic_tag $tags*) := stx
+        | throwError "invalid '{name}' attribute"
+      if (← getEnv).find? decl |>.isSome then
+        if !(isTactic (← getEnv) decl) then
+          throwErrorAt stx "'{decl}' is not a tactic"
+
+      if let some tgt' := alternativeOfTactic (← getEnv) decl then
+        throwErrorAt stx "'{decl}' is an alternative form of '{tgt'}'"
+
+      for t in tags do
+        let tagName := t.getId
+        if let some _ ← tagInfo tagName then
+          modifyEnv (tacticTagExt.addEntry · (decl, tagName))
+        else
+          let all ← allTags
+          let extra : MessageData :=
+              let count := all.length
+              let name := (m!"'{·}'")
+              let suggestions :=
+                if count == 0 then m!"(no tags defined)"
+                else if count == 1 then
+                  MessageData.joinSep (all.map name) ", "
+                else if count < 10 then
+                  m!"one of " ++ MessageData.joinSep (all.map name) ", "
+                else
+                  m!"one of " ++
+                  MessageData.joinSep (all.take 10 |>.map name) ", " ++ ", ..."
+              m!"(expected {suggestions})"
+
+          throwErrorAt t (m!"unknown tag '{tagName}' " ++ extra)
+    descr := "Register a tactic parser as an alternative of an existing tactic, so they can be " ++
+      "grouped together in documentation.",
+    -- This runs prior to elaboration because it allows a check for whether the decl is present
+    -- in the environment to determine whether we can see if it's a tactic name. This is useful
+    -- when the attribute is applied after definition, using an `attribute` command (error checking
+    -- for the `@[tactic_tag ...]` syntax is performed by the parser attribute hook). If this
+    -- attribute ran later, then the decl would already be present.
+    applicationTime := .beforeElaboration
+  }
+
+/--
+Extensions to tactic documentation.
+
+This provides a structured way to indicate that an extensible tactic has been extended (for
+instance, new cases tried by `trivial`).
+-/
+builtin_initialize tacticDocExtExt
+    : PersistentEnvExtension (Name × Array String) (Name × String) (NameMap (Array String)) ←
+  registerPersistentEnvExtension {
+    mkInitial := pure {},
+    addImportedFn := fun _ => pure {},
+    addEntryFn := fun es (x, ext) => es.insert x (es.findD x #[] |>.push ext),
+    exportEntriesFn := fun es =>
+      es.fold (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1)
+  }
+
+/-- Gets the extensions declared for the documentation for the given canonical tactic name -/
+def getTacticExtensions (env : Environment) (tactic : Name) : Array String := Id.run do
+  let mut extensions := #[]
+  -- Extensions may be declared in any module, so they must all be searched
+  for modArr in tacticDocExtExt.toEnvExtension.getState env |>.importedEntries do
+    if let some (_, strs) := modArr.binSearch (tactic, #[]) (Name.quickLt ·.1 ·.1) then
+      extensions := extensions ++ strs
+  if let some strs := tacticDocExtExt.getState env |>.find? tactic then
+    extensions := extensions ++ strs
+  pure extensions
+
+/-- Gets the rendered extensions for the given canonical tactic name -/
+def getTacticExtensionString (env : Environment) (tactic : Name) : String := Id.run do
+  let exts := getTacticExtensions env tactic
+  if exts.size == 0 then ""
+  else "\n\nExtensions:\n\n" ++ String.join (exts.toList.map bullet) |>.trimRight
+where
+  indentLine (str: String) : String :=
+    (if str.all (·.isWhitespace) then str else "   " ++ str) ++ "\n"
+  bullet (str : String) : String :=
+    let lines := str.splitOn "\n"
+    match lines with
+    | [] => ""
+    | [l] => " * " ++ l ++ "\n\n"
+    | l::ls => " * " ++ l ++ "\n" ++ String.join (ls.map indentLine) ++ "\n\n"
+
+
+-- Note: this error handler doesn't prevent all cases of non-tactics being added to the data
+-- structure. But the module will throw errors during elaboration, and there doesn't seem to be
+-- another way to implement this, because the category parser extension attribute runs *after* the
+-- attributes specified before a `syntax` command.
+/--
+Validates that a tactic alternative is actually a tactic and that syntax tagged as tactics are
+tactics.
+-/
+def tacticDocsOnTactics : ParserAttributeHook where
+  postAdd (catName declName : Name) (_builtIn : Bool) := do
+    if catName == `tactic then
+      return
+    if alternativeOfTactic (← getEnv) declName |>.isSome then
+      throwError m!"'{declName}' is not a tactic"
+    -- It's sufficient to look in the state (and not the imported entries) because this validation
+    -- only needs to check tags added in the current module
+    if let some tags := tacticTagExt.getState (← getEnv) |>.find? declName then
+      if !tags.isEmpty then
+        throwError m!"'{declName}' is not a tactic"
+
+builtin_initialize
+  registerParserAttributeHook tacticDocsOnTactics

src/Lean/PrettyPrinter/Delaborator/Basic.lean

@@ -45,6 +45,8 @@ structure Context where
   depth          : Nat := 0
 
 structure State where
+  /-- The number of `delab` steps so far. Used by `pp.maxSteps` to stop delaboration. -/
+  steps : Nat := 0
   /-- We attach `Elab.Info` at various locations in the `Syntax` output in order to convey
   its semantics. While the elaborator emits `InfoTree`s, here we have no real text location tree
   to traverse, so we use a flattened map. -/
@@ -262,10 +264,12 @@ def withBindingBodyUnusedName {α} (d : Syntax → DelabM α) : DelabM α := do
 inductive OmissionReason
   | deep
   | proof
+  | maxSteps
 
 def OmissionReason.toString : OmissionReason → String
   | deep => "Term omitted due to its depth (see option `pp.deepTerms`)."
   | proof => "Proof omitted (see option `pp.proofs`)."
+  | maxSteps => "Term omitted due to reaching the maximum number of steps allowed for pretty printing this expression (see option `pp.maxSteps`)."
 
 def addOmissionInfo (pos : Pos) (stx : Syntax) (e : Expr) (reason : OmissionReason) : DelabM Unit := do
   let info := Info.ofOmissionInfo <| ← mkOmissionInfo stx e
@@ -361,6 +365,11 @@ partial def delabFor : Name → Delab
 
 partial def delab : Delab := do
   checkSystem "delab"
+
+  if (← get).steps ≥ (← getPPOption getPPMaxSteps) then
+    return ← omission .maxSteps
+  modify fun s => {s with steps := s.steps + 1}
+
   let e ← getExpr
 
   if ← shouldOmitExpr e then

src/Lean/PrettyPrinter/Delaborator/Options.lean

@@ -8,6 +8,11 @@ import Lean.Data.Options
 
 namespace Lean
 
+register_builtin_option pp.maxSteps : Nat := {
+  defValue := 5000
+  group    := "pp"
+  descr    := "(pretty printer) maximum number of expressions to visit, after which terms will pretty print as `⋯`"
+}
 register_builtin_option pp.all : Bool := {
   defValue := false
   group    := "pp"
@@ -162,12 +167,12 @@ register_builtin_option pp.instanceTypes : Bool := {
   descr    := "(pretty printer) when printing explicit applications, show the types of inst-implicit arguments"
 }
 register_builtin_option pp.deepTerms : Bool := {
-  defValue := true
+  defValue := false
   group    := "pp"
   descr    := "(pretty printer) display deeply nested terms, replacing them with `⋯` if set to false"
 }
 register_builtin_option pp.deepTerms.threshold : Nat := {
-  defValue := 20
+  defValue := 50
   group    := "pp"
   descr    := "(pretty printer) when `pp.deepTerms` is false, the depth at which terms start being replaced with `⋯`"
 }
@@ -188,16 +193,6 @@ register_builtin_option pp.motives.all : Bool := {
 }
 -- TODO:
 /-
-register_builtin_option g_pp_max_depth : Nat := {
-  defValue := false
-  group    := "pp"
-  descr    := "(pretty printer) maximum expression depth, after that it will use ellipsis"
-}
-register_builtin_option g_pp_max_steps : Nat := {
-  defValue := false
-  group    := "pp"
-  descr    := "(pretty printer) maximum number of visited expressions, after that it will use ellipsis"
-}
 register_builtin_option g_pp_locals_full_names : Bool := {
   defValue := false
   group    := "pp"
@@ -225,6 +220,7 @@ register_builtin_option g_pp_compact_let : Bool := {
 }
 -/
 
+def getPPMaxSteps (o : Options) : Nat := o.get pp.maxSteps.name pp.maxSteps.defValue
 def getPPAll (o : Options) : Bool := o.get pp.all.name false
 def getPPFunBinderTypes (o : Options) : Bool := o.get pp.funBinderTypes.name (getPPAll o)
 def getPPPiBinderTypes (o : Options) : Bool := o.get pp.piBinderTypes.name pp.piBinderTypes.defValue

src/Lean/Server/FileWorker/RequestHandling.lean

@@ -10,6 +10,8 @@ import Lean.DeclarationRange
 import Lean.Data.Json
 import Lean.Data.Lsp
 
+import Lean.Parser.Tactic.Doc
+
 import Lean.Server.FileWorker.Utils
 import Lean.Server.Requests
 import Lean.Server.Completion
@@ -24,6 +26,8 @@ open Lsp
 open RequestM
 open Snapshots
 
+open Lean.Parser.Tactic.Doc (alternativeOfTactic getTacticExtensionString)
+
 def handleCompletion (p : CompletionParams)
     : RequestM (RequestTask CompletionList) := do
   let doc ← readDoc
@@ -85,7 +89,8 @@ def handleHover (p : HoverParams)
       let stxDoc? ← match stack? with
         | some stack => stack.findSomeM? fun (stx, _) => do
           let .node _ kind _ := stx | pure none
-          return (← findDocString? snap.env kind).map (·, stx.getRange?.get!)
+          let docStr ← findDocString? snap.env kind
+          return docStr.map (·, stx.getRange?.get!)
         | none => pure none
 
       -- now try info tree

src/Lean/Server/InfoUtils.lean

@@ -5,10 +5,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Wojciech Nawrocki
 -/
 prelude
+import Lean.DocString
 import Lean.PrettyPrinter
+import Lean.Parser.Tactic.Doc
 
 namespace Lean.Elab
 
+open Lean.Parser.Tactic.Doc (alternativeOfTactic getTacticExtensionString)
+
 /-- Elaborator information with elaborator context.
 
 It can be thought of as a "thunked" elaboration computation that allows us
@@ -244,7 +248,7 @@ def Info.docString? (i : Info) : MetaM (Option String) := do
   match i with
   | .ofTermInfo ti =>
     if let some n := ti.expr.constName? then
-      return ← findDocString? env n
+      return (← findDocString? env n)
   | .ofFieldInfo fi => return ← findDocString? env fi.projName
   | .ofOptionInfo oi =>
     if let some doc ← findDocString? env oi.declName then
@@ -258,6 +262,7 @@ def Info.docString? (i : Info) : MetaM (Option String) := do
     return ← findDocString? env ei.stx.getKind <||> findDocString? env ei.elaborator
   return none
 
+
 /-- Construct a hover popup, if any, from an info node in a context.-/
 def Info.fmtHover? (ci : ContextInfo) (i : Info) : IO (Option FormatWithInfos) := do
   ci.runMetaM i.lctx do

src/Leanc.lean

@@ -8,10 +8,15 @@ import Lean.Compiler.FFI
 open Lean.Compiler.FFI
 
 def main (args : List String) : IO UInt32 := do
-  if args.isEmpty then
-    IO.println "Lean C compiler
+  let root ← match (← IO.getEnv "LEAN_SYSROOT") with
+    | some root => pure <| System.FilePath.mk root
+    | none      => pure <| (← IO.appDir).parent.get!
+  let mut cc := "@LEANC_CC@".replace "ROOT" root.toString
 
-A simple wrapper around a C compiler. Defaults to `@LEANC_CC@`,
+  if args.isEmpty then
+    IO.println s!"Lean C compiler
+
+A simple wrapper around a C compiler. Defaults to `{cc}`,
 which can be overridden with the environment variable `LEAN_CC`. All parameters are passed
 as-is to the wrapped compiler.
 
@@ -20,11 +25,6 @@ Interesting options:
 * `--print-ldflags`: print C compiler flags necessary for statically linking against the Lean library and exit"
     return 1
 
-  let root ← match (← IO.getEnv "LEAN_SYSROOT") with
-    | some root => pure <| System.FilePath.mk root
-    | none      => pure <| (← IO.appDir).parent.get!
-  let rootify s := s.replace "ROOT" root.toString
-
   -- It is difficult to identify the correct minor version here, leading to linking warnings like:
   -- `ld64.lld: warning: /usr/lib/system/libsystem_kernel.dylib has version 13.5.0, which is newer than target minimum of 13.0.0`
   -- In order to suppress these we set the MACOSX_DEPLOYMENT_TARGET variable into the far future.
@@ -38,29 +38,27 @@ Interesting options:
 
   -- We assume that the CMake variables do not contain escaped spaces
   let cflags := getCFlags root
-  let mut cflagsInternal := "@LEANC_INTERNAL_FLAGS@".trim.splitOn
-  let mut ldflagsInternal := "@LEANC_INTERNAL_LINKER_FLAGS@".trim.splitOn
+  let mut cflagsInternal := getInternalCFlags root
+  let mut ldflagsInternal := getInternalLinkerFlags root
   let ldflags := getLinkerFlags root linkStatic
 
   for arg in args do
     match arg with
     | "--print-cflags" =>
-      IO.println <| " ".intercalate (cflags.map rootify |>.toList)
+      IO.println <| " ".intercalate cflags.toList
       return 0
     | "--print-ldflags" =>
-      IO.println <| " ".intercalate ((cflags ++ ldflags).map rootify |>.toList)
+      IO.println <| " ".intercalate (cflags ++ ldflags).toList
       return 0
     | _ => pure ()
 
-  let mut cc := "@LEANC_CC@"
   if let some cc' ← IO.getEnv "LEAN_CC" then
     cc := cc'
     -- these are intended for the bundled compiler only
-    cflagsInternal := []
-    ldflagsInternal := []
-  cc := rootify cc
+    cflagsInternal := #[]
+    ldflagsInternal := #[]
   let args := cflags ++ cflagsInternal ++ args ++ ldflagsInternal ++ ldflags ++ ["-Wno-unused-command-line-argument"]
-  let args := args.filter (!·.isEmpty) |>.map rootify
+  let args := args.filter (!·.isEmpty)
   if args.contains "-v" then
     IO.eprintln s!"{cc} {" ".intercalate args.toList}"
   let child ← IO.Process.spawn { cmd := cc, args, env }

src/Std.lean

@@ -0,0 +1,5 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Ullrich
+-/

src/lake/Lake/Build/Common.lean

@@ -5,6 +5,7 @@ Authors: Mac Malone
 -/
 import Lake.Config.Monad
 import Lake.Build.Actions
+import Lake.Util.JsonObject
 
 /-! # Common Build Tools
 This file defines general utilities that abstract common
@@ -31,15 +32,29 @@ which stores information about a (successful) build.
 structure BuildMetadata where
   depHash : Hash
   log : Log
-  deriving ToJson, FromJson
+  deriving ToJson
+
+def BuildMetadata.ofHash (h : Hash) : BuildMetadata :=
+  {depHash := h, log := {}}
+
+def BuildMetadata.fromJson? (json : Json) : Except String BuildMetadata := do
+  let obj ← JsonObject.fromJson? json
+  let depHash ← obj.get "depHash"
+  let log ← obj.getD "log" {}
+  return {depHash, log}
+
+instance : FromJson BuildMetadata := ⟨BuildMetadata.fromJson?⟩
 
 /-- Read persistent trace data from a file. -/
 def readTraceFile? (path : FilePath) : LogIO (Option BuildMetadata) := OptionT.run do
   match (← IO.FS.readFile path |>.toBaseIO) with
   | .ok contents =>
-    match Json.parse contents >>= fromJson? with
-    | .ok contents => return contents
-    | .error e => logVerbose s!"{path}: invalid trace file: {e}"; failure
+    if let some hash := Hash.ofString? contents.trim then
+      return .ofHash hash
+    else
+      match Json.parse contents >>= fromJson? with
+      | .ok contents => return contents
+      | .error e => logVerbose s!"{path}: invalid trace file: {e}"; failure
   | .error (.noFileOrDirectory ..) => failure
   | .error e => logWarning s!"{path}: read failed: {e}"; failure
 
@@ -86,25 +101,34 @@ then `depTrace` / `oldTrace`. No log will be replayed.
   (depTrace : BuildTrace) (traceFile : FilePath) (build : JobM PUnit)
   (action : JobAction := .build) (oldTrace := depTrace.mtime)
 : JobM Bool := do
-  if let some data ← readTraceFile? traceFile then
-    if (← checkHashUpToDate info depTrace data.depHash oldTrace) then
-      updateAction .replay
-      data.log.replay
+  if (← traceFile.pathExists) then
+    if let some data ← readTraceFile? traceFile then
+      if (← checkHashUpToDate info depTrace data.depHash oldTrace) then
+        updateAction .replay
+        data.log.replay
+        return true
+      else
+        go
+    else if (← getIsOldMode) && (← oldTrace.checkUpToDate info) then
       return true
-  else if (← getIsOldMode) then
-    if (← oldTrace.checkUpToDate info) then
-      return true
-  else if (← depTrace.checkAgainstTime info) then
-    return true
-  if (← getNoBuild) then
-    IO.Process.exit noBuildCode.toUInt8
+    else
+      go
   else
-    updateAction action
-    let iniPos ← getLogPos
-    build -- fatal errors will not produce a trace (or cache their log)
-    let log := (← getLog).takeFrom iniPos
-    writeTraceFile traceFile depTrace log
-    return false
+    if (← depTrace.checkAgainstTime info) then
+      return true
+    else
+      go
+where
+  go := do
+    if (← getNoBuild) then
+      IO.Process.exit noBuildCode.toUInt8
+    else
+      updateAction action
+      let iniPos ← getLogPos
+      build -- fatal errors will not produce a trace (or cache their log)
+      let log := (← getLog).takeFrom iniPos
+      writeTraceFile traceFile depTrace log
+      return false
 
 /--
 Checks whether `info` is up-to-date, and runs `build` to recreate it if not.

src/lake/Lake/Build/Module.lean

@@ -110,22 +110,22 @@ def Module.recBuildDeps (mod : Module) : FetchM (BuildJob (SearchPath × Array F
     imp.olean.fetch
   let precompileImports ← try mod.precompileImports.fetch
     catch errPos => return Job.error (← takeLogFrom errPos)
-  let modJobs ← precompileImports.mapM (·.dynlib.fetch)
+  let modLibJobs ← precompileImports.mapM (·.dynlib.fetch)
   let pkgs := precompileImports.foldl (·.insert ·.pkg)
     OrdPackageSet.empty |>.insert mod.pkg |>.toArray
   let (externJobs, libDirs) ← recBuildExternDynlibs pkgs
   let externDynlibsJob ← BuildJob.collectArray externJobs
-  let modDynlibsJob ← BuildJob.collectArray modJobs
+  let modDynlibsJob ← BuildJob.collectArray modLibJobs
 
   extraDepJob.bindAsync fun _ extraDepTrace => do
   importJob.bindAsync fun _ importTrace => do
-  modDynlibsJob.bindAsync fun modDynlibs modTrace => do
+  modDynlibsJob.bindAsync fun modDynlibs modLibTrace => do
   return externDynlibsJob.mapWithTrace fun externDynlibs externTrace =>
-    let depTrace := extraDepTrace.mix <| importTrace.mix <| modTrace
+    let depTrace := extraDepTrace.mix <| importTrace
     let depTrace :=
       match mod.platformIndependent with
-      | none => depTrace.mix <| externTrace
-      | some false => depTrace.mix <| externTrace.mix <| platformTrace
+      | none => depTrace.mix <| modLibTrace.mix <| externTrace
+      | some false => depTrace.mix <| modLibTrace.mix <| externTrace.mix <| platformTrace
       | some true => depTrace
     /-
     Requirements:

src/lake/Lake/Build/Trace.lean

@@ -87,8 +87,11 @@ namespace Hash
 @[inline] def ofNat (n : Nat) :=
   mk n.toUInt64
 
+def ofString? (s : String) : Option Hash :=
+  (inline s.toNat?).map ofNat
+
 def load? (hashFile : FilePath) : BaseIO (Option Hash) :=
-  (·.toNat?.map ofNat) <$> IO.FS.readFile hashFile |>.catchExceptions fun _ => pure none
+  ofString? <$> IO.FS.readFile hashFile |>.catchExceptions fun _ => pure none
 
 def nil : Hash :=
   mk <| 1723 -- same as Name.anonymous

src/lake/Lake/Load/Lean/Eval.lean

@@ -5,6 +5,7 @@ Authors: Mac Malone
 -/
 import Lake.DSL.Attributes
 import Lake.Config.Workspace
+import Lean.DocString
 
 /-! # Lean Configuration Evaluator
 

src/lake/Lake/Util/JsonObject.lean

@@ -20,6 +20,9 @@ abbrev JsonObject :=
 
 namespace JsonObject
 
+@[inline] def mk (val : RBNode String (fun _ => Json)) : JsonObject :=
+  val
+
 @[inline] protected def toJson (obj : JsonObject) : Json :=
   .obj obj
 

src/lake/examples/precompile/test.sh

@@ -4,7 +4,9 @@ LAKE=${LAKE:-../../.lake/build/bin/lake}
 
 ./clean.sh
 $LAKE -d bar update
-$LAKE -d bar build # tests lake#83
+# test that build a module w/o precompile modules still precompiles deps
+# https://github.com/leanprover/lake/issues/83
+$LAKE -d bar build
 $LAKE -d foo build
 
 ./clean.sh

src/lake/tests/precompileArgs/lakefile.lean

@@ -6,4 +6,5 @@ package precompileArgs
 @[default_target]
 lean_lib Foo where
   precompileModules := true
-  moreLinkArgs := #["-lBaz"]
+  platformIndependent := if get_config? platformIndependent |>.isSome then true else none
+  moreLinkArgs := if let some cfg := get_config? linkArgs then cfg.splitOn " " |>.toArray else #[]

src/lake/tests/precompileArgs/test.sh

@@ -3,7 +3,27 @@ set -exo pipefail
 
 LAKE=${LAKE:-../../.lake/build/bin/lake}
 
+if [ "$OS" = Windows_NT ]; then
+LIB_PREFIX=
+SHARED_LIB_EXT=dll
+elif [ "`uname`" = Darwin ]; then
+LIB_PREFIX=lib
+SHARED_LIB_EXT=dylib
+else
+LIB_PREFIX=lib
+SHARED_LIB_EXT=so
+fi
+
 ./clean.sh
 
 # Test that `moreLinkArgs` are included when linking precompiled modules
-($LAKE build +Foo:dynlib 2>&1 || true) | grep --color -- "-lBaz"
+($LAKE build -KlinkArgs=-lBaz 2>&1 || true) | grep --color -- "-lBaz"
+
+# Test that dynlibs are part of the module trace unless `platformIndependent` is set
+$LAKE build -R
+echo foo > .lake/build/lib/${LIB_PREFIX}Foo-Bar-1.$SHARED_LIB_EXT
+($LAKE build 2>&1 --rehash && exit 1 || true) | grep --color "Building Foo"
+rm .lake/build/lib/${LIB_PREFIX}Foo-Bar-1.$SHARED_LIB_EXT
+$LAKE build -R -KplatformIndependent=true
+echo foo > .lake/build/lib/${LIB_PREFIX}Foo-Bar-1.$SHARED_LIB_EXT
+$LAKE build --rehash --no-build

src/lake/tests/trace/clean.sh

@@ -0,0 +1 @@
+rm -rf .lake lake-manifest.json

src/lake/tests/trace/lakefile.toml

@@ -0,0 +1,5 @@
+name = "test"
+defaultTargets = ["Foo"]
+
+[[lean_lib]]
+name = "Foo"

src/lake/tests/trace/test.sh

@@ -0,0 +1,35 @@
+#!/usr/bin/env bash
+set -euxo pipefail
+
+LAKE=${LAKE:-../../.lake/build/bin/lake}
+
+./clean.sh
+
+# ---
+# Tests aspects of Lake tracing
+# ---
+
+# Tests that a build produces a trace
+test ! -f .lake/build/lib/Foo.trace
+$LAKE build | grep --color "Built Foo"
+test -f .lake/build/lib/Foo.trace
+
+# Tests that a proper trace prevents a rebuild
+$LAKE build --no-build
+
+# Tests that Lake accepts pure numerical traces
+if command -v jq > /dev/null; then # skip if no jq found
+  jq -r '.depHash' .lake/build/lib/Foo.trace > .lake/build/lib/Foo.trace.hash
+  mv .lake/build/lib/Foo.trace.hash .lake/build/lib/Foo.trace
+  $LAKE build --no-build
+fi
+
+# Tests that removal of the trace does not cause a rebuild
+# (if the modification time of the artifact is still newer than the inputs)
+rm .lake/build/lib/Foo.trace
+$LAKE build --no-build
+
+# Tests that an invalid trace does cause a rebuild
+touch .lake/build/lib/Foo.trace
+$LAKE build | grep --color "Built Foo"
+$LAKE build --no-build

src/lakefile.toml.in

@@ -27,6 +27,9 @@ nativeLibDir = "lib/lean"
 [[lean_lib]]
 name = "Init"
 
+[[lean_lib]]
+name = "Std"
+
 [[lean_lib]]
 name = "Lean"
 globs = [

src/library/compiler/ir_interpreter.cpp

@@ -796,7 +796,7 @@ private:
         }
         if (object * const * o = g_init_globals->find(fn)) {
             // persistent, so no `inc` needed
-            return *o;
+            return type_is_scalar(t) ? unbox_t(*o, t) : *o;
         }
 
         symbol_cache_entry e = lookup_symbol(fn);
@@ -867,7 +867,7 @@ private:
                 string_ref boxed_mangled(string_append(mangled.to_obj_arg(), g_boxed_mangled_suffix->raw()));
                 throw exception(sstream() << "Could not find native implementation of external declaration '" << fn
                                           << "' (symbols '" << boxed_mangled.data() << "' or '" << mangled.data() << "').\n"
-                                          << "For declarations from `Init` or `Lean`, you need to set `supportInterpreter := true` "
+                                          << "For declarations from `Init`, `Std`, or `Lean`, you need to set `supportInterpreter := true` "
                                           << "in the relevant `lean_exe` statement in your `lakefile.lean`.");
             }
             // evaluate args in old stack frame

src/library/constructions/CMakeLists.txt

@@ -1,3 +1,3 @@
-add_library(constructions OBJECT rec_on.cpp cases_on.cpp
+add_library(constructions OBJECT cases_on.cpp
   no_confusion.cpp projection.cpp brec_on.cpp init_module.cpp
   util.cpp)

src/library/constructions/rec_on.cpp

@@ -1,64 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "runtime/sstream.h"
-#include "kernel/kernel_exception.h"
-#include "kernel/environment.h"
-#include "kernel/instantiate.h"
-#include "kernel/abstract.h"
-#include "kernel/inductive.h"
-#include "library/reducible.h"
-#include "library/suffixes.h"
-#include "library/aux_recursors.h"
-#include "library/constructions/util.h"
-
-namespace lean {
-declaration mk_rec_on(environment const & env, name const & n) {
-    constant_info ind_info = env.get(n);
-    if (!ind_info.is_inductive())
-        throw exception(sstream() << "error in '" << g_rec_on << "' generation, '" << n << "' is not an inductive datatype");
-    name_generator ngen = mk_constructions_name_generator();
-    local_ctx lctx;
-    name rec_on_name(n, g_rec_on);
-    constant_info rec_info = env.get(mk_rec_name(n));
-    recursor_val  rec_val  = rec_info.to_recursor_val();
-    buffer<expr> locals;
-    expr rec_type = rec_info.get_type();
-    while (is_pi(rec_type)) {
-        expr local = lctx.mk_local_decl(ngen, binding_name(rec_type), binding_domain(rec_type), binding_info(rec_type));
-        rec_type   = instantiate(binding_body(rec_type), local);
-        locals.push_back(local);
-    }
-
-    // locals order
-    //   As Cs minor_premises indices major-premise
-
-    // new_locals order
-    //   As Cs indices major-premise minor-premises
-    buffer<expr> new_locals;
-    unsigned num_indices  = rec_val.get_nindices();
-    unsigned num_minors   = rec_val.get_nminors();
-    unsigned AC_sz        = locals.size() - num_minors - num_indices - 1;
-    for (unsigned i = 0; i < AC_sz; i++)
-        new_locals.push_back(locals[i]);
-    for (unsigned i = 0; i < num_indices + 1; i++)
-        new_locals.push_back(locals[AC_sz + num_minors + i]);
-    for (unsigned i = 0; i < num_minors; i++)
-        new_locals.push_back(locals[AC_sz + i]);
-    expr rec_on_type = lctx.mk_pi(new_locals, rec_type);
-
-    levels ls = lparams_to_levels(rec_info.get_lparams());
-    expr rec  = mk_constant(rec_info.get_name(), ls);
-    expr rec_on_val = lctx.mk_lambda(new_locals, mk_app(rec, locals));
-
-    return mk_definition_inferring_unsafe(env, rec_on_name, rec_info.get_lparams(),
-                                          rec_on_type, rec_on_val, reducibility_hints::mk_abbreviation());
-}
-
-extern "C" LEAN_EXPORT object * lean_mk_rec_on(object * env, object * n) {
-    return catch_kernel_exceptions<declaration>([&]() { return mk_rec_on(environment(env), name(n, true)); });
-}
-}

src/library/constructions/rec_on.h

@@ -1,19 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "kernel/environment.h"
-
-namespace lean {
-/** \brief Given an inductive datatype \c n in \c env, returns
-    the declaration for <tt>n.rec_on</tt>.
-
-    \remark <tt>rec_on</tt> is based on <tt>n.rec</tt>
-
-    \remark Throws an exception if \c n is not an inductive datatype.
-*/
-declaration mk_rec_on(environment const & env, name const & n);
-}

src/library/suffixes.h

@@ -8,7 +8,6 @@ Author: Leonardo de Moura
 
 namespace lean {
 constexpr char const * g_rec               = "rec";
-constexpr char const * g_rec_on            = "recOn";
 constexpr char const * g_brec_on           = "brecOn";
 constexpr char const * g_binduction_on     = "binductionOn";
 constexpr char const * g_cases_on          = "casesOn";

src/stdlib.make.in

@@ -29,7 +29,7 @@ ifeq "${STAGE}" "0"
   LEANMAKE_OPTS+=C_ONLY=1 C_OUT=${LEAN_SOURCE_DIR}/../stdlib/
 endif
 
-.PHONY: Init Lean leanshared Lake lean
+.PHONY: Init Std Lean leanshared Lake lean
 
 # These can be phony since the inner Makefile will have the correct dependencies and avoid rebuilds
 Init:
@@ -37,9 +37,12 @@ Init:
 # Use `+` to use the Make jobserver with `leanmake` for parallelized builds
 # Build `.olean/.o`s of downstream libraries as well for better parallelism
 	+"${LEAN_BIN}/leanmake" objs lib lib.export PKG=Init $(LEANMAKE_OPTS) \
-	  EXTRA_SRC_ROOTS="Lean Lean.lean"
+	  EXTRA_SRC_ROOTS="Std Std.lean Lean Lean.lean"
 
-Lean: Init
+Std: Init
+	+"${LEAN_BIN}/leanmake" lib lib.export PKG=Std $(LEANMAKE_OPTS)
+
+Lean: Std
 	+"${LEAN_BIN}/leanmake" lib lib.export PKG=Lean $(LEANMAKE_OPTS)
 
 ${LIB}/temp/empty.c:
@@ -61,7 +64,7 @@ endif
 
 Init_shared: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX}
 
-${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX} ${LIB}/temp/libLean.a.export ${LIB}/lean/libleancpp.a
+${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX} ${LIB}/temp/libStd.a.export ${LIB}/temp/libLean.a.export ${LIB}/lean/libleancpp.a
 	@echo "[    ] Building $@"
 # on Windows, must remove file before writing a new one (since the old one may be in use)
 	@rm -f $@

src/util/ffi.cpp

@@ -13,7 +13,15 @@ extern "C" object * lean_get_leanc_extra_flags(object *) {
     return lean_mk_string("@LEANC_EXTRA_FLAGS@");
 }
 
+extern "C" object * lean_get_leanc_internal_flags(object *) {
+    return lean_mk_string("@LEANC_INTERNAL_FLAGS@");
+}
+
 extern "C" object * lean_get_linker_flags(uint8 link_static) {
     return lean_mk_string(link_static ? "@LEANC_STATIC_LINKER_FLAGS@ @LEAN_EXTRA_LINKER_FLAGS@" : "@LEANC_SHARED_LINKER_FLAGS@ @LEAN_EXTRA_LINKER_FLAGS@");
 }
+
+extern "C" object * lean_get_internal_linker_flags(object *) {
+    return lean_mk_string("@LEANC_INTERNAL_LINKER_FLAGS@");
+}
 }