chore: fix explicitness of Prod.map lemmas

Fixes a bug where Lake incorrectly included the module dynlib in a
platform-independent trace. It was incorrectly excluded only external
native libraries from the trace. Also adds a test.

flake.nix

@@ -35,27 +35,28 @@
       lean-packages = pkgs.callPackage (./nix/packages.nix) { src = ./.; inherit nix lean4-mode; };
 
       devShellWithDist = pkgsDist: pkgs.mkShell.override {
-	  stdenv = pkgs.overrideCC pkgs.stdenv lean-packages.llvmPackages.clang;
-	} ({
-	  buildInputs = with pkgs; [
-	    cmake gmp ccache
-	    lean-packages.llvmPackages.llvm  # llvm-symbolizer for asan/lsan
-	    # TODO: only add when proven to not affect the flakification
-	    #pkgs.python3
-      tree  # for CI
-	  ];
-	  # https://github.com/NixOS/nixpkgs/issues/60919
-	  hardeningDisable = [ "all" ];
-	  # more convenient `ctest` output
-	  CTEST_OUTPUT_ON_FAILURE = 1;
-	} // pkgs.lib.optionalAttrs pkgs.stdenv.isLinux {
-	  GMP = pkgsDist.gmp.override { withStatic = true; };
-	  GLIBC = pkgsDist.glibc;
-	  GLIBC_DEV = pkgsDist.glibc.dev;
-	  GCC_LIB = pkgsDist.gcc.cc.lib;
-	  ZLIB = pkgsDist.zlib;
-	  GDB = pkgsDist.gdb;
-	});
+          stdenv = pkgs.overrideCC pkgs.stdenv lean-packages.llvmPackages.clang;
+        } ({
+          buildInputs = with pkgs; [
+            cmake gmp ccache
+            lean-packages.llvmPackages.llvm  # llvm-symbolizer for asan/lsan
+            gdb
+            # TODO: only add when proven to not affect the flakification
+            #pkgs.python3
+            tree  # for CI
+          ];
+          # https://github.com/NixOS/nixpkgs/issues/60919
+          hardeningDisable = [ "all" ];
+          # more convenient `ctest` output
+          CTEST_OUTPUT_ON_FAILURE = 1;
+        } // pkgs.lib.optionalAttrs pkgs.stdenv.isLinux {
+          GMP = pkgsDist.gmp.override { withStatic = true; };
+          GLIBC = pkgsDist.glibc;
+          GLIBC_DEV = pkgsDist.glibc.dev;
+          GCC_LIB = pkgsDist.gcc.cc.lib;
+          ZLIB = pkgsDist.zlib;
+          GDB = pkgsDist.gdb;
+        });
     in {
       packages = lean-packages // rec {
         debug = lean-packages.override { debug = true; };

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/Control/Except.lean

@@ -131,7 +131,7 @@ protected def adapt {ε' α : Type u} (f : ε → ε') : ExceptT ε m α → Exc
 end ExceptT
 
 @[always_inline]
-instance (m : Type u → Type v) (ε₁ : Type u) (ε₂ : Type u) [Monad m] [MonadExceptOf ε₁ m] : MonadExceptOf ε₁ (ExceptT ε₂ m) where
+instance (m : Type u → Type v) (ε₁ : Type u) (ε₂ : Type u) [MonadExceptOf ε₁ m] : MonadExceptOf ε₁ (ExceptT ε₂ m) where
   throw e := ExceptT.mk <| throwThe ε₁ e
   tryCatch x handle := ExceptT.mk <| tryCatchThe ε₁ x handle
 

src/Init/Control/Lawful/Basic.lean

@@ -9,7 +9,7 @@ import Init.Meta
 
 open Function
 
-@[simp] theorem monadLift_self [Monad m] (x : m α) : monadLift x = x :=
+@[simp] theorem monadLift_self {m : Type u → Type v} (x : m α) : monadLift x = x :=
   rfl
 
 /--

src/Init/Control/Lawful/Instances.lean

@@ -14,7 +14,7 @@ open Function
 
 namespace ExceptT
 
-theorem ext [Monad m] {x y : ExceptT ε m α} (h : x.run = y.run) : x = y := by
+theorem ext {x y : ExceptT ε m α} (h : x.run = y.run) : x = y := by
   simp [run] at h
   assumption
 
@@ -50,7 +50,7 @@ theorem run_bind [Monad m] (x : ExceptT ε m α)
 protected theorem seq_eq {α β ε : Type u} [Monad m] (mf : ExceptT ε m (α → β)) (x : ExceptT ε m α) : mf <*> x = mf >>= fun f => f <$> x :=
   rfl
 
-protected theorem bind_pure_comp [Monad m] [LawfulMonad m] (f : α → β) (x : ExceptT ε m α) : x >>= pure ∘ f = f <$> x := by
+protected theorem bind_pure_comp [Monad m] (f : α → β) (x : ExceptT ε m α) : x >>= pure ∘ f = f <$> x := by
   intros; rfl
 
 protected theorem seqLeft_eq {α β ε : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (x : ExceptT ε m α) (y : ExceptT ε m β) : x <* y = const β <$> x <*> y := by
@@ -200,11 +200,11 @@ theorem ext {x y : StateT σ m α} (h : ∀ s, x.run s = y.run s) : x = y :=
   show (f >>= fun g => g <$> x).run s = _
   simp
 
-@[simp] theorem run_seqRight [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) (s : σ) : (x *> y).run s = (x.run s >>= fun p => y.run p.2) := by
+@[simp] theorem run_seqRight [Monad m] (x : StateT σ m α) (y : StateT σ m β) (s : σ) : (x *> y).run s = (x.run s >>= fun p => y.run p.2) := by
   show (x >>= fun _ => y).run s = _
   simp
 
-@[simp] theorem run_seqLeft {α β σ : Type u} [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) (s : σ) : (x <* y).run s = (x.run s >>= fun p => y.run p.2 >>= fun p' => pure (p.1, p'.2)) := by
+@[simp] theorem run_seqLeft {α β σ : Type u} [Monad m] (x : StateT σ m α) (y : StateT σ m β) (s : σ) : (x <* y).run s = (x.run s >>= fun p => y.run p.2 >>= fun p' => pure (p.1, p'.2)) := by
   show (x >>= fun a => y >>= fun _ => pure a).run s = _
   simp
 

src/Init/Control/Option.lean

@@ -67,7 +67,7 @@ instance : MonadExceptOf Unit (OptionT m) where
   throw    := fun _ => OptionT.fail
   tryCatch := OptionT.tryCatch
 
-instance (ε : Type u) [Monad m] [MonadExceptOf ε m] : MonadExceptOf ε (OptionT m) where
+instance (ε : Type u) [MonadExceptOf ε m] : MonadExceptOf ε (OptionT m) where
   throw e           := OptionT.mk <| throwThe ε e
   tryCatch x handle := OptionT.mk <| tryCatchThe ε x handle
 

src/Init/Control/Reader.lean

@@ -32,7 +32,7 @@ instance : MonadControl m (ReaderT ρ m) where
   restoreM x _ := x
 
 @[always_inline]
-instance ReaderT.tryFinally [MonadFinally m] [Monad m] : MonadFinally (ReaderT ρ m) where
+instance ReaderT.tryFinally [MonadFinally m] : MonadFinally (ReaderT ρ m) where
   tryFinally' x h ctx := tryFinally' (x ctx) (fun a? => h a? ctx)
 
 @[reducible] def ReaderM (ρ : Type u) := ReaderT ρ Id

src/Init/Control/State.lean

@@ -87,7 +87,7 @@ protected def lift {α : Type u} (t : m α) : StateT σ m α :=
 instance : MonadLift m (StateT σ m) := ⟨StateT.lift⟩
 
 @[always_inline]
-instance (σ m) [Monad m] : MonadFunctor m (StateT σ m) := ⟨fun f x s => f (x s)⟩
+instance (σ m) : MonadFunctor m (StateT σ m) := ⟨fun f x s => f (x s)⟩
 
 @[always_inline]
 instance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (StateT σ m) := {

src/Init/Control/StateCps.lean

@@ -14,16 +14,18 @@ def StateCpsT (σ : Type u) (m : Type u → Type v) (α : Type u) := (δ : Type
 
 namespace StateCpsT
 
+variable {α σ : Type u} {m : Type u → Type v}
+
 @[always_inline, inline]
-def runK {α σ : Type u} {m : Type u → Type v}  (x : StateCpsT σ m α) (s : σ) (k : α → σ → m β) : m β :=
+def runK (x : StateCpsT σ m α) (s : σ) (k : α → σ → m β) : m β :=
   x _ s k
 
 @[always_inline, inline]
-def run {α σ : Type u} {m : Type u → Type v} [Monad m] (x : StateCpsT σ m α) (s : σ) : m (α × σ) :=
+def run [Monad m] (x : StateCpsT σ m α) (s : σ) : m (α × σ) :=
   runK x s (fun a s => pure (a, s))
 
 @[always_inline, inline]
-def run' {α σ : Type u} {m : Type u → Type v}  [Monad m] (x : StateCpsT σ m α) (s : σ) : m α :=
+def run' [Monad m] (x : StateCpsT σ m α) (s : σ) : m α :=
   runK x s (fun a _ => pure a)
 
 @[always_inline]
@@ -48,29 +50,29 @@ protected def lift [Monad m] (x : m α) : StateCpsT σ m α :=
 instance [Monad m] : MonadLift m (StateCpsT σ m) where
   monadLift := StateCpsT.lift
 
-@[simp] theorem runK_pure {m : Type u → Type v} (a : α) (s : σ) (k : α → σ → m β) : (pure a : StateCpsT σ m α).runK s k = k a s := rfl
+@[simp] theorem runK_pure (a : α) (s : σ) (k : α → σ → m β) : (pure a : StateCpsT σ m α).runK s k = k a s := rfl
 
-@[simp] theorem runK_get {m : Type u → Type v} (s : σ) (k : σ → σ → m β) : (get : StateCpsT σ m σ).runK s k = k s s := rfl
+@[simp] theorem runK_get (s : σ) (k : σ → σ → m β) : (get : StateCpsT σ m σ).runK s k = k s s := rfl
 
-@[simp] theorem runK_set {m : Type u → Type v} (s s' : σ) (k : PUnit → σ → m β) : (set s' : StateCpsT σ m PUnit).runK s k = k ⟨⟩ s' := rfl
+@[simp] theorem runK_set (s s' : σ) (k : PUnit → σ → m β) : (set s' : StateCpsT σ m PUnit).runK s k = k ⟨⟩ s' := rfl
 
-@[simp] theorem runK_modify {m : Type u → Type v} (f : σ → σ) (s : σ) (k : PUnit → σ → m β) : (modify f : StateCpsT σ m PUnit).runK s k = k ⟨⟩ (f s) := rfl
+@[simp] theorem runK_modify (f : σ → σ) (s : σ) (k : PUnit → σ → m β) : (modify f : StateCpsT σ m PUnit).runK s k = k ⟨⟩ (f s) := rfl
 
-@[simp] theorem runK_lift {α σ : Type u} [Monad m] (x : m α) (s : σ) (k : α → σ → m β) : (StateCpsT.lift x : StateCpsT σ m α).runK s k = x >>= (k . s) := rfl
+@[simp] theorem runK_lift [Monad m] (x : m α) (s : σ) (k : α → σ → m β) : (StateCpsT.lift x : StateCpsT σ m α).runK s k = x >>= (k . s) := rfl
 
-@[simp] theorem runK_monadLift {σ : Type u} [Monad m] [MonadLiftT n m] (x : n α) (s : σ) (k : α → σ → m β)
+@[simp] theorem runK_monadLift [Monad m] [MonadLiftT n m] (x : n α) (s : σ) (k : α → σ → m β)
     : (monadLift x : StateCpsT σ m α).runK s k = (monadLift x : m α) >>= (k . s) := rfl
 
-@[simp] theorem runK_bind_pure {α σ : Type u} [Monad m] (a : α) (f : α → StateCpsT σ m β) (s : σ) (k : β → σ → m γ) : (pure a >>= f).runK s k = (f a).runK s k := rfl
+@[simp] theorem runK_bind_pure (a : α) (f : α → StateCpsT σ m β) (s : σ) (k : β → σ → m γ) : (pure a >>= f).runK s k = (f a).runK s k := rfl
 
-@[simp] theorem runK_bind_lift {α σ : Type u} [Monad m] (x : m α) (f : α → StateCpsT σ m β) (s : σ) (k : β → σ → m γ)
+@[simp] theorem runK_bind_lift [Monad m] (x : m α) (f : α → StateCpsT σ m β) (s : σ) (k : β → σ → m γ)
     : (StateCpsT.lift x >>= f).runK s k = x >>= fun a => (f a).runK s k := rfl
 
-@[simp] theorem runK_bind_get {σ : Type u} [Monad m] (f : σ → StateCpsT σ m β) (s : σ) (k : β → σ → m γ) : (get >>= f).runK s k = (f s).runK s k := rfl
+@[simp] theorem runK_bind_get (f : σ → StateCpsT σ m β) (s : σ) (k : β → σ → m γ) : (get >>= f).runK s k = (f s).runK s k := rfl
 
-@[simp] theorem runK_bind_set {σ : Type u} [Monad m] (f : PUnit → StateCpsT σ m β) (s s' : σ) (k : β → σ → m γ) : (set s' >>= f).runK s k = (f ⟨⟩).runK s' k := rfl
+@[simp] theorem runK_bind_set (f : PUnit → StateCpsT σ m β) (s s' : σ) (k : β → σ → m γ) : (set s' >>= f).runK s k = (f ⟨⟩).runK s' k := rfl
 
-@[simp] theorem runK_bind_modify {σ : Type u} [Monad m] (f : σ → σ) (g : PUnit → StateCpsT σ m β) (s : σ) (k : β → σ → m γ) : (modify f >>= g).runK s k = (g ⟨⟩).runK (f s) k := rfl
+@[simp] theorem runK_bind_modify (f : σ → σ) (g : PUnit → StateCpsT σ m β) (s : σ) (k : β → σ → m γ) : (modify f >>= g).runK s k = (g ⟨⟩).runK (f s) k := rfl
 
 @[simp] theorem run_eq [Monad m] (x : StateCpsT σ m α) (s : σ) : x.run s = x.runK s (fun a s => pure (a, s)) := rfl
 

src/Init/Control/StateRef.lean

@@ -34,22 +34,22 @@ protected def lift (x : m α) : StateRefT' ω σ m α :=
 
 instance [Monad m] : Monad (StateRefT' ω σ m) := inferInstanceAs (Monad (ReaderT _ _))
 instance : MonadLift m (StateRefT' ω σ m) := ⟨StateRefT'.lift⟩
-instance (σ m) [Monad m] : MonadFunctor m (StateRefT' ω σ m) := inferInstanceAs (MonadFunctor m (ReaderT _ _))
+instance (σ m) : MonadFunctor m (StateRefT' ω σ m) := inferInstanceAs (MonadFunctor m (ReaderT _ _))
 instance [Alternative m] [Monad m] : Alternative (StateRefT' ω σ m) := inferInstanceAs (Alternative (ReaderT _ _))
 
 @[inline]
-protected def get [Monad m] [MonadLiftT (ST ω) m] : StateRefT' ω σ m σ :=
+protected def get [MonadLiftT (ST ω) m] : StateRefT' ω σ m σ :=
   fun ref => ref.get
 
 @[inline]
-protected def set [Monad m] [MonadLiftT (ST ω) m] (s : σ) : StateRefT' ω σ m PUnit :=
+protected def set [MonadLiftT (ST ω) m] (s : σ) : StateRefT' ω σ m PUnit :=
   fun ref => ref.set s
 
 @[inline]
-protected def modifyGet [Monad m] [MonadLiftT (ST ω) m] (f : σ → α × σ) : StateRefT' ω σ m α :=
+protected def modifyGet [MonadLiftT (ST ω) m] (f : σ → α × σ) : StateRefT' ω σ m α :=
   fun ref => ref.modifyGet f
 
-instance [MonadLiftT (ST ω) m] [Monad m] : MonadStateOf σ (StateRefT' ω σ m) where
+instance [MonadLiftT (ST ω) m] : MonadStateOf σ (StateRefT' ω σ m) where
   get       := StateRefT'.get
   set       := StateRefT'.set
   modifyGet := StateRefT'.modifyGet

src/Init/Core.lean

@@ -642,7 +642,7 @@ instance : LawfulBEq String := inferInstance
 
 /-! # Logical connectives and equality -/
 
-@[inherit_doc True.intro] def trivial : True := ⟨⟩
+@[inherit_doc True.intro] theorem trivial : True := ⟨⟩
 
 theorem mt {a b : Prop} (h₁ : a → b) (h₂ : ¬b) : ¬a :=
   fun ha => h₂ (h₁ ha)
@@ -1173,7 +1173,7 @@ def Prod.lexLt [LT α] [LT β] (s : α × β) (t : α × β) : Prop :=
   s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)
 
 instance Prod.lexLtDec
-    [LT α] [LT β] [DecidableEq α] [DecidableEq β]
+    [LT α] [LT β] [DecidableEq α]
     [(a b : α) → Decidable (a < b)] [(a b : β) → Decidable (a < b)]
     : (s t : α × β) → Decidable (Prod.lexLt s t) :=
   fun _ _ => inferInstanceAs (Decidable (_ ∨ _))
@@ -1191,6 +1191,11 @@ def Prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂
     (f : α₁ → α₂) (g : β₁ → β₂) : α₁ × β₁ → α₂ × β₂
   | (a, b) => (f a, g b)
 
+@[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 -/
 
 theorem ex_of_PSigma {α : Type u} {p : α → Prop} : (PSigma (fun x => p x)) → Exists (fun x => p x)

src/Init/Data/Array/Lemmas.lean

@@ -750,7 +750,7 @@ theorem mem_of_mem_filter {a : α} {l} (h : a ∈ filter p l) : a ∈ l :=
   exact this #[]
   induction l
   · simp_all [Id.run]
-  · simp_all [Id.run]
+  · simp_all [Id.run, List.filterMap_cons]
     split <;> simp_all
 
 @[simp] theorem mem_filterMap (f : α → Option β) (l : Array α) {b : β} :

src/Init/Data/BitVec/Lemmas.lean

@@ -184,8 +184,7 @@ theorem msb_eq_getLsb_last (x : BitVec w) :
     · simp only [h]
       rw [Nat.div_eq_sub_div (Nat.two_pow_pos w) h, Nat.div_eq_of_lt]
       · decide
-      · have : BitVec.toNat x < 2^w + 2^w := by simpa [Nat.pow_succ, Nat.mul_two] using x.isLt
-        omega
+      · omega
 
 @[bv_toNat] theorem getLsb_succ_last (x : BitVec (w + 1)) :
     x.getLsb w = decide (2 ^ w ≤ x.toNat) := getLsb_last x
@@ -331,10 +330,7 @@ theorem toNat_eq_nat (x : BitVec w) (y : Nat)
   : (x.toNat = y) ↔ (y < 2^w ∧ (x = BitVec.ofNat w y)) := by
   apply Iff.intro
   · intro eq
-    simp at eq
-    have lt := x.isLt
-    simp [eq] at lt
-    simp [←eq, lt, x.isLt]
+    simp [←eq, x.isLt]
   · intro eq
     simp [Nat.mod_eq_of_lt, eq]
 
@@ -1240,11 +1236,7 @@ x.rotateLeft 2 = (<6 5 | 4 3 2 1 0>).rotateLeft 2 = <3 2 1 0 | 6 5>
 theorem getLsb_rotateLeftAux_of_le {x : BitVec w} {r : Nat} {i : Nat} (hi : i < r) :
     (x.rotateLeftAux r).getLsb i = x.getLsb (w - r + i) := by
   rw [rotateLeftAux, getLsb_or, getLsb_ushiftRight]
-  suffices (x <<< r).getLsb i = false by
-    simp; omega
-  simp only [getLsb_shiftLeft, Bool.and_eq_false_imp, Bool.and_eq_true, decide_eq_true_eq,
-    Bool.not_eq_true', decide_eq_false_iff_not, Nat.not_lt, and_imp]
-  omega
+  simp; omega
 
 /--
 Accessing bits in `x.rotateLeft r` the range `[r, w)` is equal to

src/Init/Data/Fin/Lemmas.lean

@@ -378,7 +378,7 @@ theorem castSucc_lt_succ (i : Fin n) : Fin.castSucc i < i.succ :=
   lt_def.2 <| by simp only [coe_castSucc, val_succ, Nat.lt_succ_self]
 
 theorem le_castSucc_iff {i : Fin (n + 1)} {j : Fin n} : i ≤ Fin.castSucc j ↔ i < j.succ := by
-  simpa [lt_def, le_def] using Nat.succ_le_succ_iff.symm
+  simpa only [lt_def, le_def] using Nat.add_one_le_add_one_iff.symm
 
 theorem castSucc_lt_iff_succ_le {n : Nat} {i : Fin n} {j : Fin (n + 1)} :
     Fin.castSucc i < j ↔ i.succ ≤ j := .rfl

src/Init/Data/Int/DivModLemmas.lean

@@ -636,7 +636,7 @@ theorem sub_ediv_of_dvd (a : Int) {b c : Int}
   have := Int.mul_ediv_cancel 1 H; rwa [Int.one_mul] at this
 
 @[simp]
-theorem Int.emod_sub_cancel (x y : Int): (x - y)%y = x%y := by
+theorem emod_sub_cancel (x y : Int): (x - y)%y = x%y := by
   by_cases h : y = 0
   · simp [h]
   · simp only [Int.emod_def, Int.sub_ediv_of_dvd, Int.dvd_refl, Int.ediv_self h, Int.mul_sub]

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
@@ -398,7 +401,7 @@ filterMap
     | some b => b :: filterMap f as
 
 @[simp] theorem filterMap_nil (f : α → Option β) : filterMap f [] = [] := rfl
-@[simp] theorem filterMap_cons (f : α → Option β) (a : α) (l : List α) :
+theorem filterMap_cons (f : α → Option β) (a : α) (l : List α) :
     filterMap f (a :: l) =
       match f a with
       | none => filterMap f l
@@ -562,12 +565,17 @@ set_option linter.missingDocs false in
 `replicate n a` is `n` copies of `a`:
 * `replicate 5 a = [a, a, a, a, a]`
 -/
-@[simp] def replicate : (n : Nat) → (a : α) → List α
+def replicate : (n : Nat) → (a : α) → List α
   | 0,   _ => []
   | n+1, a => a :: replicate n a
 
+@[simp] theorem replicate_zero : replicate 0 a = [] := rfl
+theorem replicate_succ (a : α) (n) : replicate (n+1) a = a :: replicate n a := rfl
+
 @[simp] theorem length_replicate (n : Nat) (a : α) : (replicate n a).length = n := by
-  induction n <;> simp_all
+  induction n with
+  | zero => simp
+  | succ n ih => simp only [ih, replicate_succ, length_cons, Nat.succ_eq_add_one]
 
 /-! ## List membership
 
@@ -606,13 +614,13 @@ def isEmpty : List α → Bool
 -/
 def elem [BEq α] (a : α) : List α → Bool
   | []    => false
-  | b::bs => match b == a with
+  | b::bs => match a == b with
     | true  => true
     | false => elem a bs
 
 @[simp] theorem elem_nil [BEq α] : ([] : List α).elem a = false := rfl
 theorem elem_cons [BEq α] {a : α} :
-    (a::as).elem b = match a == b with | true => true | false => as.elem b := rfl
+    (b::bs).elem a = match a == b with | true => true | false => bs.elem a := rfl
 
 /-- `notElem a l` is `!(elem a l)`. -/
 @[deprecated (since := "2024-06-15")]
@@ -735,7 +743,7 @@ theorem drop_eq_nil_of_le {as : List α} {i : Nat} (h : as.length ≤ i) : as.dr
   match as, i with
   | [],    i   => simp
   | _::_,  0   => simp at h
-  | _::as, i+1 => simp at h; exact @drop_eq_nil_of_le as i (Nat.le_of_succ_le_succ h)
+  | _::as, i+1 => simp only [length_cons] at h; exact @drop_eq_nil_of_le as i (Nat.le_of_succ_le_succ h)
 
 /-! ### takeWhile -/
 
@@ -847,6 +855,9 @@ That is, there exists a `t` such that `l₂ == t ++ l₁`. -/
 def isSuffixOf [BEq α] (l₁ l₂ : List α) : Bool :=
   isPrefixOf l₁.reverse l₂.reverse
 
+@[simp] theorem isSuffixOf_nil_left [BEq α] : isSuffixOf ([] : List α) l = true := by
+  simp [isSuffixOf]
+
 /-! ### isSuffixOf? -/
 
 /-- `isSuffixOf? l₁ l₂` returns `some t` when `l₂ == t ++ l₁`.-/
@@ -872,6 +883,8 @@ def rotateLeft (xs : List α) (n : Nat := 1) : List α :=
     let e := xs.drop n
     e ++ b
 
+@[simp] theorem rotateLeft_nil : ([] : List α).rotateLeft n = [] := rfl
+
 /-! ### rotateRight -/
 
 /--
@@ -891,6 +904,8 @@ def rotateRight (xs : List α) (n : Nat := 1) : List α :=
     let e := xs.drop n
     e ++ b
 
+@[simp] theorem rotateRight_nil : ([] : List α).rotateRight n = [] := rfl
+
 /-! ## Manipulating elements -/
 
 /-! ### replace -/
@@ -903,13 +918,13 @@ def rotateRight (xs : List α) (n : Nat := 1) : List α :=
 -/
 def replace [BEq α] : List α → α → α → List α
   | [],    _, _ => []
-  | a::as, b, c => match a == b with
+  | a::as, b, c => match b == a with
     | true  => c::as
     | false => a :: replace as b c
 
 @[simp] theorem replace_nil [BEq α] : ([] : List α).replace a b = [] := rfl
 theorem replace_cons [BEq α] {a : α} :
-    (a::as).replace b c = match a == b with | true => c::as | false => a :: replace as b c :=
+    (a::as).replace b c = match b == a with | true => c::as | false => a :: replace as b c :=
   rfl
 
 /-! ### insert -/

src/Init/Data/List/Impl.lean

@@ -258,7 +258,7 @@ theorem replicateTR_loop_eq : ∀ n, replicateTR.loop a n acc = replicate n a ++
   unless `b` is not found in `xs` in which case it returns `l`. -/
   @[specialize] go : List α → Array α → List α
   | [], _ => l
-  | a::as, acc => bif a == b then acc.toListAppend (c::as) else go as (acc.push a)
+  | a::as, acc => bif b == a then acc.toListAppend (c::as) else go as (acc.push a)
 
 @[csimp] theorem replace_eq_replaceTR : @List.replace = @replaceTR := by
   funext α _ l b c; simp [replaceTR]

src/Init/Data/List/TakeDrop.lean

@@ -39,10 +39,15 @@ theorem take_take : ∀ (n m) (l : List α), take n (take m l) = take (min n m)
   | succ n, succ m, a :: l => by
     simp only [take, succ_min_succ, take_take n m l]
 
-theorem take_replicate (a : α) : ∀ n m : Nat, take n (replicate m a) = replicate (min n m) a
+@[simp] theorem take_replicate (a : α) : ∀ n m : Nat, take n (replicate m a) = replicate (min n m) a
   | n, 0 => by simp [Nat.min_zero]
   | 0, m => by simp [Nat.zero_min]
-  | succ n, succ m => by simp [succ_min_succ, take_replicate]
+  | succ n, succ m => by simp [replicate_succ, succ_min_succ, take_replicate]
+
+@[simp] theorem drop_replicate (a : α) : ∀ n m : Nat, drop n (replicate m a) = replicate (m - n) a
+  | n, 0 => by simp
+  | 0, m => by simp
+  | succ n, succ m => by simp [replicate_succ, succ_sub_succ, drop_replicate]
 
 /-- Taking the first `n` elements in `l₁ ++ l₂` is the same as appending the first `n` elements
 of `l₁` to the first `n - l₁.length` elements of `l₂`. -/
@@ -97,7 +102,7 @@ theorem get_take' (L : List α) {j i} :
 
 theorem getElem?_take_eq_none {l : List α} {n m : Nat} (h : n ≤ m) :
     (l.take n)[m]? = none :=
-  getElem?_eq_none.mpr <| Nat.le_trans (length_take_le _ _) h
+  getElem?_eq_none <| Nat.le_trans (length_take_le _ _) h
 
 @[deprecated getElem?_take_eq_none (since := "2024-06-12")]
 theorem get?_take_eq_none {l : List α} {n m : Nat} (h : n ≤ m) :
@@ -298,6 +303,32 @@ theorem take_reverse {α} {xs : List α} (n : Nat) (h : n ≤ xs.length) :
 
 @[deprecated (since := "2024-06-15")] abbrev reverse_take := @take_reverse
 
+/-! ### rotateLeft -/
+
+@[simp] theorem rotateLeft_replicate (n) (a : α) : rotateLeft (replicate m a) n = replicate m a := by
+  cases n with
+  | zero => simp
+  | succ n =>
+    suffices 1 < m → m - (n + 1) % m + min ((n + 1) % m) m = m by
+      simpa [rotateLeft]
+    intro h
+    rw [Nat.min_eq_left (Nat.le_of_lt (Nat.mod_lt _ (by omega)))]
+    have : (n + 1) % m < m := Nat.mod_lt _ (by omega)
+    omega
+
+/-! ### rotateRight -/
+
+@[simp] theorem rotateRight_replicate (n) (a : α) : rotateRight (replicate m a) n = replicate m a := by
+  cases n with
+  | zero => simp
+  | succ n =>
+    suffices 1 < m → m - (m - (n + 1) % m) + min (m - (n + 1) % m) m = m by
+      simpa [rotateRight]
+    intro h
+    have : (n + 1) % m < m := Nat.mod_lt _ (by omega)
+    rw [Nat.min_eq_left (by omega)]
+    omega
+
 /-! ### zipWith -/
 
 @[simp] theorem length_zipWith (f : α → β → γ) (l₁ l₂) :
@@ -305,10 +336,32 @@ theorem take_reverse {α} {xs : List α} (n : Nat) (h : n ≤ xs.length) :
   induction l₁ generalizing l₂ <;> cases l₂ <;>
     simp_all [succ_min_succ, Nat.zero_min, Nat.min_zero]
 
+theorem zipWith_eq_zipWith_take_min : ∀ (l₁ : List α) (l₂ : List β),
+    zipWith f l₁ l₂ = zipWith f (l₁.take (min l₁.length l₂.length)) (l₂.take (min l₁.length l₂.length))
+  | [], _ => by simp
+  | _, [] => by simp
+  | a :: l₁, b :: l₂ => by simp [succ_min_succ, zipWith_eq_zipWith_take_min l₁ l₂]
+
+@[simp] theorem zipWith_replicate {a : α} {b : β} {m n : Nat} :
+    zipWith f (replicate m a) (replicate n b) = replicate (min m n) (f a b) := by
+  rw [zipWith_eq_zipWith_take_min]
+  simp
+
 /-! ### zip -/
 
 @[simp] theorem length_zip (l₁ : List α) (l₂ : List β) :
     length (zip l₁ l₂) = min (length l₁) (length l₂) := by
   simp [zip]
 
+theorem zip_eq_zip_take_min : ∀ (l₁ : List α) (l₂ : List β),
+    zip l₁ l₂ = zip (l₁.take (min l₁.length l₂.length)) (l₂.take (min l₁.length l₂.length))
+  | [], _ => by simp
+  | _, [] => by simp
+  | a :: l₁, b :: l₂ => by simp [succ_min_succ, zip_eq_zip_take_min l₁ l₂]
+
+@[simp] theorem zip_replicate {a : α} {b : β} {m n : Nat} :
+    zip (replicate m a) (replicate n b) = replicate (min m n) (a, b) := by
+  rw [zip_eq_zip_take_min]
+  simp
+
 end List

src/Init/Data/Nat/Basic.lean

@@ -636,6 +636,12 @@ theorem succ_le_succ_iff : succ a ≤ succ b ↔ a ≤ b := ⟨le_of_succ_le_suc
 
 theorem succ_lt_succ_iff : succ a < succ b ↔ a < b := ⟨lt_of_succ_lt_succ, succ_lt_succ⟩
 
+theorem add_one_inj : a + 1 = b + 1 ↔ a = b := succ_inj'
+
+theorem add_one_le_add_one_iff : a + 1 ≤ b + 1 ↔ a ≤ b := succ_le_succ_iff
+
+theorem add_one_lt_add_one_iff : a + 1 < b + 1 ↔ a < b := succ_lt_succ_iff
+
 theorem pred_inj : ∀ {a b}, 0 < a → 0 < b → pred a = pred b → a = b
   | _+1, _+1, _, _ => congrArg _
 

src/Init/Data/Nat/Lemmas.lean

@@ -212,13 +212,19 @@ instance : Std.IdempotentOp (α := Nat) min := ⟨Nat.min_self⟩
 
 @[simp] protected theorem min_zero (a) : min a 0 = 0 := Nat.min_eq_right (Nat.zero_le _)
 
-protected theorem min_assoc : ∀ (a b c : Nat), min (min a b) c = min a (min b c)
+@[simp] protected theorem min_assoc : ∀ (a b c : Nat), min (min a b) c = min a (min b c)
   | 0, _, _ => by rw [Nat.zero_min, Nat.zero_min, Nat.zero_min]
   | _, 0, _ => by rw [Nat.zero_min, Nat.min_zero, Nat.zero_min]
   | _, _, 0 => by rw [Nat.min_zero, Nat.min_zero, Nat.min_zero]
   | _+1, _+1, _+1 => by simp only [Nat.succ_min_succ]; exact congrArg succ <| Nat.min_assoc ..
 instance : Std.Associative (α := Nat) min := ⟨Nat.min_assoc⟩
 
+@[simp] protected theorem min_self_assoc {m n : Nat} : min m (min m n) = min m n := by
+  rw [← Nat.min_assoc, Nat.min_self]
+
+@[simp] protected theorem min_self_assoc' {m n : Nat} : min n (min m n) = min n m := by
+  rw [Nat.min_comm m n, ← Nat.min_assoc, Nat.min_self]
+
 protected theorem sub_sub_eq_min : ∀ (a b : Nat), a - (a - b) = min a b
   | 0, _ => by rw [Nat.zero_sub, Nat.zero_min]
   | _, 0 => by rw [Nat.sub_zero, Nat.sub_self, Nat.min_zero]

src/Init/Data/Nat/Linear.lean

@@ -583,8 +583,6 @@ theorem PolyCnstr.denote_mul (ctx : Context) (k : Nat) (c : PolyCnstr) : (c.mul
   have : k ≠ 0 → k + 1 ≠ 1 := by intro h; match k with | 0 => contradiction | k+1 => simp [Nat.succ.injEq]
   have : ¬ (k == 0) → (k + 1 == 1) = false := fun h => beq_false_of_ne (this (ne_of_beq_false (Bool.of_not_eq_true h)))
   have : ¬ ((k + 1 == 0) = true)  := fun h => absurd (eq_of_beq h) (Nat.succ_ne_zero k)
-  have : (1 == (0 : Nat)) = false := rfl
-  have : (1 == (1 : Nat)) = true  := rfl
   by_cases he : eq = true <;> simp [he, PolyCnstr.mul, PolyCnstr.denote, Poly.denote_le, Poly.denote_eq]
      <;> by_cases hk : k == 0 <;> (try simp [eq_of_beq hk]) <;> simp [*] <;> apply Iff.intro <;> intro h
   · exact Nat.eq_of_mul_eq_mul_left (Nat.zero_lt_succ _) h

src/Init/Data/Option/Instances.lean

@@ -26,7 +26,7 @@ instance : Membership α (Option α) := ⟨fun a b => b = some a⟩
 instance [DecidableEq α] (j : α) (o : Option α) : Decidable (j ∈ o) :=
   inferInstanceAs <| Decidable (o = some j)
 
-theorem isNone_iff_eq_none {o : Option α} : o.isNone ↔ o = none :=
+@[simp] theorem isNone_iff_eq_none {o : Option α} : o.isNone ↔ o = none :=
   ⟨Option.eq_none_of_isNone, fun e => e.symm ▸ rfl⟩
 
 theorem some_inj {a b : α} : some a = some b ↔ a = b := by simp; rfl

src/Init/Data/String/Extra.lean

@@ -69,7 +69,7 @@ where
   decreasing_by exact Nat.sub_lt_sub_left ‹_› (Nat.lt_add_of_pos_right c.utf8Size_pos)
 
 /-- Converts a [UTF-8](https://en.wikipedia.org/wiki/UTF-8) encoded `ByteArray` string to `String`. -/
-@[extern "lean_string_from_utf8"]
+@[extern "lean_string_from_utf8_unchecked"]
 def fromUTF8 (a : @& ByteArray) (h : validateUTF8 a) : String :=
   loop 0 ""
 where

src/Init/Meta.lean

@@ -1278,12 +1278,46 @@ def Occurrences.isAll : Occurrences → Bool
   | all => true
   | _   => false
 
+/--
+Controls which new mvars are turned in to goals by the `apply` tactic.
+- `nonDependentFirst`  mvars that don't depend on other goals appear first in the goal list.
+- `nonDependentOnly` only mvars that don't depend on other goals are added to goal list.
+- `all` all unassigned mvars are added to the goal list.
+-/
+-- TODO: Consider renaming to `Apply.NewGoals`
+inductive ApplyNewGoals where
+  | nonDependentFirst | nonDependentOnly | all
+
+/-- Configures the behaviour of the `apply` tactic. -/
+-- TODO: Consider renaming to `Apply.Config`
+structure ApplyConfig where
+  newGoals := ApplyNewGoals.nonDependentFirst
+  /--
+  If `synthAssignedInstances` is `true`, then `apply` will synthesize instance implicit arguments
+  even if they have assigned by `isDefEq`, and then check whether the synthesized value matches the
+  one inferred. The `congr` tactic sets this flag to false.
+  -/
+  synthAssignedInstances := true
+  /--
+  If `allowSynthFailures` is `true`, then `apply` will return instance implicit arguments
+  for which typeclass search failed as new goals.
+  -/
+  allowSynthFailures := false
+  /--
+  If `approx := true`, then we turn on `isDefEq` approximations. That is, we use
+  the `approxDefEq` combinator.
+  -/
+  approx : Bool := true
+
 namespace Rewrite
 
+abbrev NewGoals := ApplyNewGoals
+
 structure Config where
-  transparency : TransparencyMode := TransparencyMode.reducible
+  transparency : TransparencyMode := .reducible
   offsetCnstrs : Bool := true
-  occs : Occurrences := Occurrences.all
+  occs : Occurrences := .all
+  newGoals : NewGoals := .nonDependentFirst
 
 end Rewrite
 

src/Init/MetaTypes.lean

@@ -42,23 +42,67 @@ inductive EtaStructMode where
 
 namespace DSimp
 
+/--
+The configuration for `dsimp`.
+Passed to `dsimp` using, for example, the `dsimp (config := {zeta := false})` syntax.
+
+Implementation note: this structure is only used for processing the `(config := ...)` syntax, and it is not used internally.
+It is immediately converted to `Lean.Meta.Simp.Config` by `Lean.Elab.Tactic.elabSimpConfig`.
+-/
 structure Config where
-  /-- `let x := v; e[x]` reduces to `e[v]`. -/
+  /--
+  When `true` (default: `true`), performs zeta reduction of let expressions.
+  That is, `let x := v; e[x]` reduces to `e[v]`.
+  See also `zetaDelta`.
+  -/
   zeta              : Bool := true
+  /--
+  When `true` (default: `true`), performs beta reduction of applications of `fun` expressions.
+  That is, `(fun x => e[x]) v` reduces to `e[v]`.
+  -/
   beta              : Bool := true
+  /--
+  TODO (currently unimplemented). When `true` (default: `true`), performs eta reduction for `fun` expressions.
+  That is, `(fun x => f x)` reduces to `f`.
+  -/
   eta               : Bool := true
+  /--
+  Configures how to determine definitional equality between two structure instances.
+  See documentation for `Lean.Meta.EtaStructMode`.
+  -/
   etaStruct         : EtaStructMode := .all
+  /--
+  When `true` (default: `true`), reduces `match` expressions applied to constructors.
+  -/
   iota              : Bool := true
+  /--
+  When `true` (default: `true`), reduces projections of structure constructors.
+  -/
   proj              : Bool := true
+  /--
+  When `true` (default: `false`), rewrites a proposition `p` to `True` or `False` by inferring
+  a `Decidable p` instance and reducing it.
+  -/
   decide            : Bool := false
+  /--
+  When `true` (default: `false`), unfolds definitions.
+  This can be enabled using the `simp!` syntax.
+  -/
   autoUnfold        : Bool := false
-  /-- If `failIfUnchanged := true`, then calls to `simp`, `dsimp`, or `simp_all`
-  will fail if they do not make progress. -/
+  /--
+  If `failIfUnchanged` is `true` (default: `true`), then calls to `simp`, `dsimp`, or `simp_all`
+  will fail if they do not make progress.
+  -/
   failIfUnchanged   : Bool := true
-  /-- If `unfoldPartialApp := true`, then calls to `simp`, `dsimp`, or `simp_all`
-  will unfold even partial applications of `f` when we request `f` to be unfolded. -/
+  /--
+  If `unfoldPartialApp` is `true` (default: `false`), then calls to `simp`, `dsimp`, or `simp_all`
+  will unfold even partial applications of `f` when we request `f` to be unfolded.
+  -/
   unfoldPartialApp  : Bool := false
-  /-- Given a local context containing entry `x : t := e`, free variable `x` reduces to `e`. -/
+  /--
+  When `true` (default: `false`), local definitions are unfolded.
+  That is, given a local context containing entry `x : t := e`, the free variable `x` reduces to `e`.
+  -/
   zetaDelta         : Bool := false
   deriving Inhabited, BEq
 
@@ -72,7 +116,7 @@ def defaultMaxSteps := 100000
 The configuration for `simp`.
 Passed to `simp` using, for example, the `simp (config := {contextual := true})` syntax.
 
-See also `Lean.Meta.Simp.neutralConfig`.
+See also `Lean.Meta.Simp.neutralConfig` and `Lean.Meta.DSimp.Config`.
 -/
 structure Config where
   /--

src/Init/Notation.lean

@@ -558,6 +558,22 @@ syntax (name := runMeta) "run_meta " doSeq : command
 set_option linter.missingDocs false in
 syntax guardMsgsFilterSeverity := &"info" <|> &"warning" <|> &"error" <|> &"all"
 
+/--
+`#reduce <expression>` reduces the expression `<expression>` to its normal form. This
+involves applying reduction rules until no further reduction is possible.
+
+By default, proofs and types within the expression are not reduced. Use modifiers
+`(proofs := true)`  and `(types := true)` to reduce them.
+Recall that propositions are types in Lean.
+
+**Warning:** This can be a computationally expensive operation,
+especially for complex expressions.
+
+Consider using `#eval <expression>` for simple evaluation/execution
+of expressions.
+-/
+syntax (name := reduceCmd) "#reduce " (atomic("(" &"proofs" " := " &"true" ")"))? (atomic("(" &"types" " := " &"true" ")"))? term : command
+
 /--
 A message filter specification for `#guard_msgs`.
 - `info`, `warning`, `error`: capture messages with the given severity level.

src/Init/Omega/IntList.lean

@@ -173,7 +173,7 @@ theorem mul_neg_left (xs ys : IntList) : (-xs) * ys = -(xs * ys) := by
 attribute [local simp] add_def neg_def sub_def in
 theorem sub_eq_add_neg (xs ys : IntList) : xs - ys = xs + (-ys) := by
   induction xs generalizing ys with
-  | nil => simp; rfl
+  | nil => simp
   | cons x xs ih =>
     cases ys with
     | nil => simp

src/Init/Prelude.lean

@@ -740,7 +740,7 @@ prove `p` given any element `x : α`, then `p` holds. Note that it is essential
 that `p` is a `Prop` here; the version with `p` being a `Sort u` is equivalent
 to `Classical.choice`.
 -/
-protected def Nonempty.elim {α : Sort u} {p : Prop} (h₁ : Nonempty α) (h₂ : α → p) : p :=
+protected theorem Nonempty.elim {α : Sort u} {p : Prop} (h₁ : Nonempty α) (h₂ : α → p) : p :=
   match h₁ with
   | intro a => h₂ a
 
@@ -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
@@ -2976,7 +2973,7 @@ def MonadExcept.ofExcept [Monad m] [MonadExcept ε m] : Except ε α → m α
 
 export MonadExcept (throw tryCatch ofExcept)
 
-instance (ε : outParam (Type u)) (m : Type v → Type w) [MonadExceptOf ε m] : MonadExcept ε m where
+instance (ε : Type u) (m : Type v → Type w) [MonadExceptOf ε m] : MonadExcept ε m where
   throw    := throwThe ε
   tryCatch := tryCatchThe ε
 
@@ -3150,7 +3147,7 @@ instance (ρ : Type u) (m : Type u → Type v) [MonadWithReaderOf ρ m] : MonadW
 instance {ρ : Type u} {m : Type u → Type v} {n : Type u → Type v} [MonadFunctor m n] [MonadWithReaderOf ρ m] : MonadWithReaderOf ρ n where
   withReader f := monadMap (m := m) (withTheReader ρ f)
 
-instance {ρ : Type u} {m : Type u → Type v} [Monad m] : MonadWithReaderOf ρ (ReaderT ρ m) where
+instance {ρ : Type u} {m : Type u → Type v} : MonadWithReaderOf ρ (ReaderT ρ m) where
   withReader f x := fun ctx => x (f ctx)
 
 /--
@@ -3233,7 +3230,7 @@ def modify {σ : Type u} {m : Type u → Type v} [MonadState σ m] (f : σ →
 of the state. It is equivalent to `get <* modify f` but may be more efficient.
 -/
 @[always_inline, inline]
-def getModify {σ : Type u} {m : Type u → Type v} [MonadState σ m] [Monad m] (f : σ → σ) : m σ :=
+def getModify {σ : Type u} {m : Type u → Type v} [MonadState σ m] (f : σ → σ) : m σ :=
   modifyGet fun s => (s, f s)
 
 -- NOTE: The Ordering of the following two instances determines that the top-most `StateT` Monad layer

src/Init/Tactics.lean

@@ -267,7 +267,9 @@ syntax (name := case') "case' " sepBy1(caseArg, " | ") " => " tacticSeq : tactic
 `next x₁ ... xₙ => tac` additionally renames the `n` most recent hypotheses with
 inaccessible names to the given names.
 -/
-macro "next " args:binderIdent* " => " tac:tacticSeq : tactic => `(tactic| case _ $args* => $tac)
+macro "next " args:binderIdent* arrowTk:" => " tac:tacticSeq : tactic =>
+  -- Limit ref variability for incrementality; see Note [Incremental Macros]
+  withRef arrowTk `(tactic| case _ $args* =>%$arrowTk $tac)
 
 /-- `all_goals tac` runs `tac` on each goal, concatenating the resulting goals, if any. -/
 syntax (name := allGoals) "all_goals " tacticSeq : tactic
@@ -1459,6 +1461,7 @@ have been simplified by using the modifier `↓`. Here is an example
 ```
 
 When multiple simp theorems are applicable, the simplifier uses the one with highest priority.
+The equational theorems of function are applied at very low priority (100 and below).
 If there are several with the same priority, it is uses the "most recent one". Example:
 ```lean
 @[simp high] theorem cond_true (a b : α) : cond true a b = a := rfl

src/Init/TacticsExtra.lean

@@ -31,15 +31,19 @@ private def expandIfThenElse
       pure (hole, #[case])
   let (posHole, posCase) ← mkCase thenTk pos `(?pos)
   let (negHole, negCase) ← mkCase elseTk neg `(?neg)
-  `(tactic| (open Classical in refine%$ifTk $(← mkIf posHole negHole); $[$(posCase ++ negCase)]*))
+  `(tactic| ((open Classical in refine%$ifTk $(← mkIf posHole negHole)); $[$(posCase ++ negCase)]*))
 
 macro_rules
   | `(tactic| if%$tk $h : $c then%$ttk $pos else%$etk $neg) =>
-    expandIfThenElse tk ttk etk pos neg fun pos neg => `(if $h : $c then $pos else $neg)
+    -- Limit ref variability for incrementality; see Note [Incremental Macros]
+    withRef tk do
+      expandIfThenElse tk ttk etk pos neg fun pos neg => `(if $h : $c then $pos else $neg)
 
 macro_rules
   | `(tactic| if%$tk $c then%$ttk $pos else%$etk $neg) =>
-    expandIfThenElse tk ttk etk pos neg fun pos neg => `(if h : $c then $pos else $neg)
+    -- Limit ref variability for incrementality; see Note [Incremental Macros]
+    withRef tk do
+      expandIfThenElse tk ttk etk pos neg fun pos neg => `(if h : $c then $pos else $neg)
 
 /--
 `iterate n tac` runs `tac` exactly `n` times.

src/Init/WF.lean

@@ -37,7 +37,7 @@ noncomputable abbrev Acc.ndrecOn.{u1, u2} {α : Sort u2} {r : α → α → Prop
 namespace Acc
 variable {α : Sort u} {r : α → α → Prop}
 
-def inv {x y : α} (h₁ : Acc r x) (h₂ : r y x) : Acc r y :=
+theorem inv {x y : α} (h₁ : Acc r x) (h₂ : r y x) : Acc r y :=
   h₁.recOn (fun _ ac₁ _ h₂ => ac₁ y h₂) h₂
 
 end Acc
@@ -58,7 +58,7 @@ class WellFoundedRelation (α : Sort u) where
   wf  : WellFounded rel
 
 namespace WellFounded
-def apply {α : Sort u} {r : α → α → Prop} (wf : WellFounded r) (a : α) : Acc r a :=
+theorem apply {α : Sort u} {r : α → α → Prop} (wf : WellFounded r) (a : α) : Acc r a :=
   wf.rec (fun p => p) a
 
 section
@@ -78,7 +78,7 @@ noncomputable def fixF (x : α) (a : Acc r x) : C x := by
   induction a with
   | intro x₁ _ ih => exact F x₁ ih
 
-def fixFEq (x : α) (acx : Acc r x) : fixF F x acx = F x (fun (y : α) (p : r y x) => fixF F y (Acc.inv acx p)) := by
+theorem fixFEq (x : α) (acx : Acc r x) : fixF F x acx = F x (fun (y : α) (p : r y x) => fixF F y (Acc.inv acx p)) := by
   induction acx with
   | intro x r _ => exact rfl
 
@@ -112,14 +112,14 @@ def emptyWf {α : Sort u} : WellFoundedRelation α where
 namespace Subrelation
 variable {α : Sort u} {r q : α → α → Prop}
 
-def accessible {a : α} (h₁ : Subrelation q r) (ac : Acc r a) : Acc q a := by
+theorem accessible {a : α} (h₁ : Subrelation q r) (ac : Acc r a) : Acc q a := by
   induction ac with
   | intro x _ ih =>
     apply Acc.intro
     intro y h
     exact ih y (h₁ h)
 
-def wf (h₁ : Subrelation q r) (h₂ : WellFounded r) : WellFounded q :=
+theorem wf (h₁ : Subrelation q r) (h₂ : WellFounded r) : WellFounded q :=
   ⟨fun a => accessible @h₁ (apply h₂ a)⟩
 end Subrelation
 
@@ -136,10 +136,10 @@ private def accAux (f : α → β) {b : β} (ac : Acc r b) : (x : α) → f x =
     subst x
     apply ih (f y) lt y rfl
 
-def accessible {a : α} (f : α → β) (ac : Acc r (f a)) : Acc (InvImage r f) a :=
+theorem accessible {a : α} (f : α → β) (ac : Acc r (f a)) : Acc (InvImage r f) a :=
   accAux f ac a rfl
 
-def wf (f : α → β) (h : WellFounded r) : WellFounded (InvImage r f) :=
+theorem wf (f : α → β) (h : WellFounded r) : WellFounded (InvImage r f) :=
   ⟨fun a => accessible f (apply h (f a))⟩
 end InvImage
 
@@ -151,7 +151,7 @@ end InvImage
 namespace TC
 variable {α : Sort u} {r : α → α → Prop}
 
-def accessible {z : α} (ac : Acc r z) : Acc (TC r) z := by
+theorem accessible {z : α} (ac : Acc r z) : Acc (TC r) z := by
   induction ac with
   | intro x acx ih =>
     apply Acc.intro x
@@ -160,7 +160,7 @@ def accessible {z : α} (ac : Acc r z) : Acc (TC r) z := by
     | base a b rab => exact ih a rab
     | trans a b c rab _ _ ih₂ => apply Acc.inv (ih₂ acx ih) rab
 
-def wf (h : WellFounded r) : WellFounded (TC r) :=
+theorem wf (h : WellFounded r) : WellFounded (TC r) :=
   ⟨fun a => accessible (apply h a)⟩
 end TC
 
@@ -251,7 +251,7 @@ instance [αeqDec : DecidableEq α] {r : α → α → Prop} [rDec : DecidableRe
         apply isFalse; intro contra; cases contra <;> contradiction
 
 -- TODO: generalize
-def right' {a₁ : Nat} {b₁ : β} (h₁ : a₁ ≤ a₂) (h₂ : rb b₁ b₂) : Prod.Lex Nat.lt rb (a₁, b₁) (a₂, b₂) :=
+theorem right' {a₁ : Nat} {b₁ : β} (h₁ : a₁ ≤ a₂) (h₂ : rb b₁ b₂) : Prod.Lex Nat.lt rb (a₁, b₁) (a₂, b₂) :=
   match Nat.eq_or_lt_of_le h₁ with
   | Or.inl h => h ▸ Prod.Lex.right a₁ h₂
   | Or.inr h => Prod.Lex.left b₁ _ h
@@ -268,7 +268,7 @@ section
 variable {α : Type u} {β : Type v}
 variable {ra  : α → α → Prop} {rb  : β → β → Prop}
 
-def lexAccessible {a : α} (aca : Acc ra a) (acb : (b : β) → Acc rb b) (b : β) : Acc (Prod.Lex ra rb) (a, b) := by
+theorem lexAccessible {a : α} (aca : Acc ra a) (acb : (b : β) → Acc rb b) (b : β) : Acc (Prod.Lex ra rb) (a, b) := by
   induction aca generalizing b with
   | intro xa _ iha =>
     induction (acb b) with
@@ -347,7 +347,7 @@ variable {α : Sort u} {β : Sort v}
 def lexNdep (r : α → α → Prop) (s : β → β → Prop) :=
   Lex r (fun _ => s)
 
-def lexNdepWf {r  : α → α → Prop} {s : β → β → Prop} (ha : WellFounded r) (hb : WellFounded s) : WellFounded (lexNdep r s) :=
+theorem lexNdepWf {r  : α → α → Prop} {s : β → β → Prop} (ha : WellFounded r) (hb : WellFounded s) : WellFounded (lexNdep r s) :=
   WellFounded.intro fun ⟨a, b⟩ => lexAccessible (WellFounded.apply ha a) (fun _ => hb) b
 end
 
@@ -365,7 +365,7 @@ open WellFounded
 variable {α : Sort u} {β : Sort v}
 variable {r  : α → α → Prop} {s : β → β → Prop}
 
-def revLexAccessible {b} (acb : Acc s b) (aca : (a : α) → Acc r a): (a : α) → Acc (RevLex r s) ⟨a, b⟩ := by
+theorem revLexAccessible {b} (acb : Acc s b) (aca : (a : α) → Acc r a): (a : α) → Acc (RevLex r s) ⟨a, b⟩ := by
   induction acb with
   | intro xb _ ihb =>
     intro a
@@ -377,7 +377,7 @@ def revLexAccessible {b} (acb : Acc s b) (aca : (a : α) → Acc r a): (a : α)
       | left  => apply iha; assumption
       | right => apply ihb; assumption
 
-def revLex (ha : WellFounded r) (hb : WellFounded s) : WellFounded (RevLex r s) :=
+theorem revLex (ha : WellFounded r) (hb : WellFounded s) : WellFounded (RevLex r s) :=
   WellFounded.intro fun ⟨a, b⟩ => revLexAccessible (apply hb b) (WellFounded.apply ha) a
 end
 
@@ -389,7 +389,7 @@ def skipLeft (α : Type u) {β : Type v} (hb : WellFoundedRelation β) : WellFou
   rel := SkipLeft α hb.rel
   wf  := revLex emptyWf.wf hb.wf
 
-def mkSkipLeft {α : Type u} {β : Type v} {b₁ b₂ : β} {s : β → β → Prop} (a₁ a₂ : α) (h : s b₁ b₂) : SkipLeft α s ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ :=
+theorem mkSkipLeft {α : Type u} {β : Type v} {b₁ b₂ : β} {s : β → β → Prop} (a₁ a₂ : α) (h : s b₁ b₂) : SkipLeft α s ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ :=
   RevLex.right _ _ h
 end
 

src/Lean/Attributes.lean

@@ -53,7 +53,7 @@ structure AttributeImpl extends AttributeImplCore where
   erase (decl : Name) : AttrM Unit := throwError "attribute cannot be erased"
   deriving Inhabited
 
-builtin_initialize attributeMapRef : IO.Ref (PersistentHashMap Name AttributeImpl) ← IO.mkRef {}
+builtin_initialize attributeMapRef : IO.Ref (HashMap Name AttributeImpl) ← IO.mkRef {}
 
 /-- Low level attribute registration function. -/
 def registerBuiltinAttribute (attr : AttributeImpl) : IO Unit := do
@@ -185,7 +185,7 @@ structure ParametricAttributeImpl (α : Type) extends AttributeImplCore where
   afterSet : Name → α → AttrM Unit := fun _ _ _ => pure ()
   afterImport : Array (Array (Name × α)) → ImportM Unit := fun _ => pure ()
 
-def registerParametricAttribute [Inhabited α] (impl : ParametricAttributeImpl α) : IO (ParametricAttribute α) := do
+def registerParametricAttribute (impl : ParametricAttributeImpl α) : IO (ParametricAttribute α) := do
   let ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α) ← registerPersistentEnvExtension {
     name            := impl.ref
     mkInitial       := pure {}
@@ -239,7 +239,7 @@ structure EnumAttributes (α : Type) where
   ext   : PersistentEnvExtension (Name × α) (Name × α) (NameMap α)
   deriving Inhabited
 
-def registerEnumAttributes [Inhabited α] (attrDescrs : List (Name × String × α))
+def registerEnumAttributes (attrDescrs : List (Name × String × α))
     (validate : Name → α → AttrM Unit := fun _ _ => pure ())
     (applicationTime := AttributeApplicationTime.afterTypeChecking)
     (ref : Name := by exact decl_name%) : IO (EnumAttributes α) := do
@@ -317,7 +317,7 @@ inductive AttributeExtensionOLeanEntry where
 
 structure AttributeExtensionState where
   newEntries : List AttributeExtensionOLeanEntry := []
-  map        : PersistentHashMap Name AttributeImpl
+  map        : HashMap Name AttributeImpl
   deriving Inhabited
 
 abbrev AttributeExtension := PersistentEnvExtension AttributeExtensionOLeanEntry (AttributeExtensionOLeanEntry × AttributeImpl) AttributeExtensionState
@@ -348,7 +348,7 @@ private def AttributeExtension.addImported (es : Array (Array AttributeExtension
   let map ← es.foldlM
     (fun map entries =>
       entries.foldlM
-        (fun (map : PersistentHashMap Name AttributeImpl) entry => do
+        (fun (map : HashMap Name AttributeImpl) entry => do
           let attrImpl ← mkAttributeImplOfEntry ctx.env ctx.opts entry
           return map.insert attrImpl.name attrImpl)
         map)
@@ -374,7 +374,7 @@ def isBuiltinAttribute (n : Name) : IO Bool := do
 
 /-- Return the name of all registered attributes. -/
 def getBuiltinAttributeNames : IO (List Name) :=
-  return (← attributeMapRef.get).foldl (init := []) fun r n _ => n::r
+  return (← attributeMapRef.get).fold (init := []) fun r n _ => n::r
 
 def getBuiltinAttributeImpl (attrName : Name) : IO AttributeImpl := do
   let m ← attributeMapRef.get
@@ -392,7 +392,7 @@ def isAttribute (env : Environment) (attrName : Name) : Bool :=
 
 def getAttributeNames (env : Environment) : List Name :=
   let m := (attributeExtension.getState env).map
-  m.foldl (fun r n _ => n::r) []
+  m.fold (fun r n _ => n::r) []
 
 def getAttributeImpl (env : Environment) (attrName : Name) : Except String AttributeImpl :=
   let m := (attributeExtension.getState env).map
@@ -427,7 +427,7 @@ def Attribute.erase (declName : Name) (attrName : Name) : AttrM Unit := do
 def updateEnvAttributesImpl (env : Environment) : IO Environment := do
   let map ← attributeMapRef.get
   let s := attributeExtension.getState env
-  let s := map.foldl (init := s) fun s attrName attrImpl =>
+  let s := map.fold (init := s) fun s attrName attrImpl =>
     if s.map.contains attrName then
       s
     else

src/Lean/AuxRecursor.lean

@@ -13,16 +13,17 @@ def recOnSuffix         := "recOn"
 def brecOnSuffix        := "brecOn"
 def binductionOnSuffix  := "binductionOn"
 def belowSuffix         := "below"
+def ibelowSuffix        := "ibelow"
 
 def mkCasesOnName (indDeclName : Name) : Name := Name.mkStr indDeclName casesOnSuffix
 def mkRecOnName (indDeclName : Name) : Name   := Name.mkStr indDeclName recOnSuffix
 def mkBRecOnName (indDeclName : Name) : Name  := Name.mkStr indDeclName brecOnSuffix
 def mkBInductionOnName (indDeclName : Name) : Name  := Name.mkStr indDeclName binductionOnSuffix
 def mkBelowName (indDeclName : Name) : Name := Name.mkStr indDeclName belowSuffix
+def mkIBelowName (indDeclName : Name) : Name := Name.mkStr indDeclName ibelowSuffix
 
 builtin_initialize auxRecExt : TagDeclarationExtension ← mkTagDeclarationExtension
 
-@[export lean_mark_aux_recursor]
 def markAuxRecursor (env : Environment) (declName : Name) : Environment :=
   auxRecExt.tag env declName
 
@@ -50,7 +51,6 @@ def isBRecOnRecursor (env : Environment) (declName : Name) : Bool :=
 
 builtin_initialize noConfusionExt : TagDeclarationExtension ← mkTagDeclarationExtension
 
-@[export lean_mark_no_confusion]
 def markNoConfusion (env : Environment) (n : Name) : Environment :=
   noConfusionExt.tag env n
 

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

@@ -499,7 +499,11 @@ def emitLit (z : VarId) (t : IRType) (v : LitVal) : M Unit := do
   emitLhs z;
   match v with
   | LitVal.num v => emitNumLit t v; emitLn ";"
-  | LitVal.str v => emit "lean_mk_string_from_bytes("; emit (quoteString v); emit ", "; emit v.utf8ByteSize; emitLn ");"
+  | LitVal.str v =>
+    emit "lean_mk_string_unchecked(";
+    emit (quoteString v); emit ", ";
+    emit v.utf8ByteSize; emit ", ";
+    emit v.length; emitLn ");"
 
 def emitVDecl (z : VarId) (t : IRType) (v : Expr) : M Unit :=
   match v with

src/Lean/Compiler/IR/EmitLLVM.lean

@@ -178,14 +178,14 @@ def callLeanUnsignedToNatFn (builder : LLVM.Builder llvmctx)
   let nv ← constIntUnsigned n
   LLVM.buildCall2 builder fnty f #[nv] name
 
-def callLeanMkStringFromBytesFn (builder : LLVM.Builder llvmctx)
-    (strPtr nBytes : LLVM.Value llvmctx) (name : String) : M llvmctx (LLVM.Value llvmctx) := do
-  let fnName :=  "lean_mk_string_from_bytes"
+def callLeanMkStringUncheckedFn (builder : LLVM.Builder llvmctx)
+    (strPtr nBytes nChars : LLVM.Value llvmctx) (name : String) : M llvmctx (LLVM.Value llvmctx) := do
+  let fnName :=  "lean_mk_string_unchecked"
   let retty ← LLVM.voidPtrType llvmctx
-  let argtys :=  #[← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx]
+  let argtys :=  #[← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx, ← LLVM.size_tType llvmctx]
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
   let fnty ← LLVM.functionType retty argtys
-  LLVM.buildCall2 builder fnty fn #[strPtr, nBytes] name
+  LLVM.buildCall2 builder fnty fn #[strPtr, nBytes, nChars] name
 
 def callLeanMkString (builder : LLVM.Builder llvmctx)
     (strPtr : LLVM.Value llvmctx) (name : String) : M llvmctx (LLVM.Value llvmctx) := do
@@ -772,7 +772,8 @@ def emitLit (builder : LLVM.Builder llvmctx)
                                 (← LLVM.opaquePointerTypeInContext llvmctx)
                                 str_global #[zero] ""
                  let nbytes ← constIntSizeT v.utf8ByteSize
-                 callLeanMkStringFromBytesFn builder strPtr nbytes ""
+                 let nchars ← constIntSizeT v.length
+                 callLeanMkStringUncheckedFn builder strPtr nbytes nchars ""
   LLVM.buildStore builder zv zslot
   return zslot
 

src/Lean/Data/PersistentHashMap.lean

@@ -23,6 +23,13 @@ inductive Node (α : Type u) (β : Type v) : Type (max u v) where
   | entries   (es : Array (Entry α β (Node α β))) : Node α β
   | collision (ks : Array α) (vs : Array β) (h : ks.size = vs.size) : Node α β
 
+partial def Node.isEmpty : Node α β → Bool
+  | .collision .. => false
+  | .entries es => es.all fun
+    | .entry .. => false
+    | .ref n    => n.isEmpty
+    | .null     => true
+
 instance {α β} : Inhabited (Node α β) := ⟨Node.entries #[]⟩
 
 abbrev shift         : USize  := 5
@@ -36,8 +43,7 @@ def mkEmptyEntriesArray {α β} : Array (Entry α β (Node α β)) :=
 end PersistentHashMap
 
 structure PersistentHashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] where
-  root    : PersistentHashMap.Node α β := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray
-  size    : Nat                        := 0
+  root : PersistentHashMap.Node α β := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray
 
 abbrev PHashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] := PersistentHashMap α β
 
@@ -45,8 +51,8 @@ namespace PersistentHashMap
 
 def empty [BEq α] [Hashable α] : PersistentHashMap α β := {}
 
-def isEmpty [BEq α] [Hashable α] (m : PersistentHashMap α β) : Bool :=
-  m.size == 0
+def isEmpty {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → Bool
+  | { root } => root.isEmpty
 
 instance [BEq α] [Hashable α] : Inhabited (PersistentHashMap α β) := ⟨{}⟩
 
@@ -130,7 +136,7 @@ partial def insertAux [BEq α] [Hashable α] : Node α β → USize → USize
         else Entry.ref $ mkCollisionNode k' v' k v
 
 def insert {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → α → β → PersistentHashMap α β
-  | { root := n, size := sz }, k, v => { root := insertAux n (hash k |>.toUSize) 1 k v, size := sz + 1 }
+  | { root }, k, v => { root := insertAux root (hash k |>.toUSize) 1 k v }
 
 partial def findAtAux [BEq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) (i : Nat) (k : α) : Option β :=
   if h : i < keys.size then
@@ -150,7 +156,7 @@ partial def findAux [BEq α] : Node α β → USize → α → Option β
   | Node.collision keys vals heq, _, k => findAtAux keys vals heq 0 k
 
 def find? {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → α → Option β
-  | { root := n, .. }, k => findAux n (hash k |>.toUSize) k
+  | { root }, k => findAux root (hash k |>.toUSize) k
 
 instance {_ : BEq α} {_ : Hashable α} : GetElem (PersistentHashMap α β) α (Option β) fun _ _ => True where
   getElem m i _ := m.find? i
@@ -183,7 +189,7 @@ partial def findEntryAux [BEq α] : Node α β → USize → α → Option (α
   | Node.collision keys vals heq, _, k => findEntryAtAux keys vals heq 0 k
 
 def findEntry? {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → α → Option (α × β)
-  | { root := n, .. }, k => findEntryAux n (hash k |>.toUSize) k
+  | { root }, k => findEntryAux root (hash k |>.toUSize) k
 
 partial def containsAtAux [BEq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) (i : Nat) (k : α) : Bool :=
   if h : i < keys.size then
@@ -202,7 +208,7 @@ partial def containsAux [BEq α] : Node α β → USize → α → Bool
   | Node.collision keys vals heq, _, k => containsAtAux keys vals heq 0 k
 
 def contains [BEq α] [Hashable α] : PersistentHashMap α β → α → Bool
-  | { root := n, .. }, k => containsAux n (hash k |>.toUSize) k
+  | { root }, k => containsAux root (hash k |>.toUSize) k
 
 partial def isUnaryEntries (a : Array (Entry α β (Node α β))) (i : Nat) (acc : Option (α × β)) : Option (α × β) :=
   if h : i < a.size then
@@ -225,7 +231,7 @@ def isUnaryNode : Node α β → Option (α × β)
     else
       none
 
-partial def eraseAux [BEq α] : Node α β → USize → α → Node α β × Bool
+partial def eraseAux [BEq α] : Node α β → USize → α → Node α β
   | n@(Node.collision keys vals heq), _, k =>
     match keys.indexOf? k with
     | some idx =>
@@ -234,28 +240,26 @@ partial def eraseAux [BEq α] : Node α β → USize → α → Node α β × Bo
       let vals' := vals.feraseIdx (Eq.ndrec idx heq)
       have veq := vals.size_feraseIdx (Eq.ndrec idx heq)
       have : keys.size - 1 = vals.size - 1 := by rw [heq]
-      (Node.collision keys' vals' (keq.trans (this.trans veq.symm)), true)
-    | none     => (n, false)
+      Node.collision keys' vals' (keq.trans (this.trans veq.symm))
+    | none     => n
   | n@(Node.entries entries), h, k =>
     let j       := (mod2Shift h shift).toNat
     let entry   := entries.get! j
     match entry with
-    | Entry.null       => (n, false)
+    | Entry.null       => n
     | Entry.entry k' _ =>
-      if k == k' then (Node.entries (entries.set! j Entry.null), true) else (n, false)
+      if k == k' then Node.entries (entries.set! j Entry.null) else n
     | Entry.ref node   =>
       let entries := entries.set! j Entry.null
-      let (newNode, deleted) := eraseAux node (div2Shift h shift) k
-      if !deleted then (n, false)
-      else match isUnaryNode newNode with
-        | none        => (Node.entries (entries.set! j (Entry.ref newNode)), true)
-        | some (k, v) => (Node.entries (entries.set! j (Entry.entry k v)), true)
+      let newNode := eraseAux node (div2Shift h shift) k
+      match isUnaryNode newNode with
+      | none        => Node.entries (entries.set! j (Entry.ref newNode))
+      | some (k, v) => Node.entries (entries.set! j (Entry.entry k v))
 
 def erase {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → α → PersistentHashMap α β
-  | { root := n, size := sz }, k =>
+  | { root }, k =>
     let h := hash k |>.toUSize
-    let (n, del) := eraseAux n h k
-    { root := n, size := if del then sz - 1 else sz }
+    { root := eraseAux root h k }
 
 section
 variable {m : Type w → Type w'} [Monad m]
@@ -317,7 +321,7 @@ partial def mapMAux {α : Type u} {β : Type v} {σ : Type u} {m : Type u → Ty
 
 def mapM {α : Type u} {β : Type v} {σ : Type u} {m : Type u → Type w} [Monad m] {_ : BEq α} {_ : Hashable α} (pm : PersistentHashMap α β) (f : β → m σ) : m (PersistentHashMap α σ) := do
   let root ← mapMAux f pm.root
-  return { pm with root }
+  return { root }
 
 def map {α : Type u} {β : Type v} {σ : Type u} {_ : BEq α} {_ : Hashable α} (pm : PersistentHashMap α β) (f : β → σ) : PersistentHashMap α σ :=
   Id.run <| pm.mapM f

src/Lean/Data/PersistentHashSet.lean

@@ -44,9 +44,6 @@ variable {_ : BEq α} {_ : Hashable α}
 @[inline] def contains (s : PersistentHashSet α) (a : α) : Bool :=
   s.set.contains a
 
-@[inline] def size (s : PersistentHashSet α) : Nat :=
-  s.set.size
-
 @[inline] def foldM {β : Type v} {m : Type v → Type v} [Monad m] (f : β → α → m β) (init : β) (s : PersistentHashSet α) : m β :=
   s.set.foldlM (init := init) fun d a _ => f d a
 

src/Lean/Data/SMap.lean

@@ -90,12 +90,6 @@ def switch (m : SMap α β) : SMap α β :=
 def fold {σ : Type w} (f : σ → α → β → σ) (init : σ) (m : SMap α β) : σ :=
   m.map₂.foldl f $ m.map₁.fold f init
 
-def size (m : SMap α β) : Nat :=
-  m.map₁.size + m.map₂.size
-
-def stageSizes (m : SMap α β) : Nat × Nat :=
-  (m.map₁.size, m.map₂.size)
-
 def numBuckets (m : SMap α β) : Nat :=
   m.map₁.numBuckets
 

src/Lean/Data/SSet.lean

@@ -34,9 +34,6 @@ abbrev switch (s : SSet α) : SSet α :=
 abbrev fold (f : σ → α → σ) (init : σ) (s : SSet α) : σ :=
   SMap.fold (fun d a _ => f d a) init s
 
-abbrev size (s : SSet α) : Nat :=
-  SMap.size s
-
 def toList (m : SSet α) : List α :=
   m.fold (init := []) fun es a => a::es
 

src/Lean/Declaration.lean

@@ -35,7 +35,7 @@ inductive ReducibilityHints where
   | opaque  : ReducibilityHints
   | abbrev  : ReducibilityHints
   | regular : UInt32 → ReducibilityHints
-  deriving Inhabited
+  deriving Inhabited, BEq
 
 @[export lean_mk_reducibility_hints_regular]
 def mkReducibilityHintsRegularEx (h : UInt32) : ReducibilityHints :=
@@ -117,7 +117,7 @@ structure DefinitionVal extends ConstantVal where
     are compiled using recursors and `WellFounded.fix`.
   -/
   all : List Name := [name]
-  deriving Inhabited
+  deriving Inhabited, BEq
 
 @[export lean_mk_definition_val]
 def mkDefinitionValEx (name : Name) (levelParams : List Name) (type : Expr) (value : Expr) (hints : ReducibilityHints) (safety : DefinitionSafety) (all : List Name) : DefinitionVal := {
@@ -161,13 +161,13 @@ def mkOpaqueValEx (name : Name) (levelParams : List Name) (type : Expr) (value :
 structure Constructor where
   name : Name
   type : Expr
-  deriving Inhabited
+  deriving Inhabited, BEq
 
 structure InductiveType where
   name : Name
   type : Expr
   ctors : List Constructor
-  deriving Inhabited
+  deriving Inhabited, BEq
 
 /-- Declaration object that can be sent to the kernel. -/
 inductive Declaration where
@@ -178,7 +178,7 @@ inductive Declaration where
   | quotDecl
   | mutualDefnDecl  (defns : List DefinitionVal) -- All definitions must be marked as `unsafe` or `partial`
   | inductDecl      (lparams : List Name) (nparams : Nat) (types : List InductiveType) (isUnsafe : Bool)
-  deriving Inhabited
+  deriving Inhabited, BEq
 
 @[export lean_mk_inductive_decl]
 def mkInductiveDeclEs (lparams : List Name) (nparams : Nat) (types : List InductiveType) (isUnsafe : Bool) : Declaration :=
@@ -189,6 +189,10 @@ def Declaration.isUnsafeInductiveDeclEx : Declaration → Bool
   | Declaration.inductDecl _ _ _ isUnsafe => isUnsafe
   | _ => false
 
+def Declaration.definitionVal! : Declaration → DefinitionVal
+  | .defnDecl val => val
+  | _ => panic! "Expected a `Declaration.defnDecl`."
+
 @[specialize] def Declaration.foldExprM {α} {m : Type → Type} [Monad m] (d : Declaration) (f : α → Expr → m α) (a : α) : m α :=
   match d with
   | Declaration.quotDecl                                        => pure a

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] [MonadRef 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/Attributes.lean

@@ -39,7 +39,7 @@ def toAttributeKind (attrKindStx : Syntax) : MacroM AttributeKind := do
 def mkAttrKindGlobal : Syntax :=
   mkNode ``Lean.Parser.Term.attrKind #[mkNullNode]
 
-def elabAttr [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadInfoTree m] [MonadLiftT IO m] (attrInstance : Syntax) : m Attribute := do
+def elabAttr [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLiftT IO m] (attrInstance : Syntax) : m Attribute := do
   /- attrInstance     := ppGroup $ leading_parser attrKind >> attrParser -/
   let attrKind ← liftMacroM <| toAttributeKind attrInstance[0]
   let attr := attrInstance[1]
@@ -55,7 +55,7 @@ def elabAttr [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMa
      So, we expand them before here before we invoke the attributer handlers implemented using `AttrM`. -/
   return { kind := attrKind, name := attrName, stx := attr }
 
-def elabAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadInfoTree m] [MonadLiftT IO m] (attrInstances : Array Syntax) : m (Array Attribute) := do
+def elabAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadLiftT IO m] (attrInstances : Array Syntax) : m (Array Attribute) := do
   let mut attrs := #[]
   for attr in attrInstances do
     try
@@ -65,7 +65,7 @@ def elabAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadM
   return attrs
 
 -- leading_parser "@[" >> sepBy1 attrInstance ", " >> "]"
-def elabDeclAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadInfoTree m] [MonadLiftT IO m] (stx : Syntax) : m (Array Attribute) :=
+def elabDeclAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadLiftT IO m] (stx : Syntax) : m (Array Attribute) :=
   elabAttrs stx[1].getSepArgs
 
 end Lean.Elab

src/Lean/Elab/BuiltinCommand.lean

@@ -262,16 +262,22 @@ def elabCheckCore (ignoreStuckTC : Bool) : CommandElab
 
 @[builtin_command_elab Lean.Parser.Command.check] def elabCheck : CommandElab := elabCheckCore (ignoreStuckTC := true)
 
-@[builtin_command_elab Lean.Parser.Command.reduce] def elabReduce : CommandElab
-  | `(#reduce%$tk $term) => withoutModifyingEnv <| runTermElabM fun _ => Term.withDeclName `_reduce do
-    let e ← Term.elabTerm term none
-    Term.synthesizeSyntheticMVarsNoPostponing
-    let e ← Term.levelMVarToParam (← instantiateMVars e)
-    -- TODO: add options or notation for setting the following parameters
-    withTheReader Core.Context (fun ctx => { ctx with options := ctx.options.setBool `smartUnfolding false }) do
-      let e ← withTransparency (mode := TransparencyMode.all) <| reduce e (skipProofs := false) (skipTypes := false)
-      logInfoAt tk e
+@[builtin_command_elab Lean.reduceCmd] def elabReduce : CommandElab
+  | `(#reduce%$tk $term) => go tk term
+  | `(#reduce%$tk (proofs := true) $term) => go tk term (skipProofs := false)
+  | `(#reduce%$tk (types := true) $term) => go tk term (skipTypes := false)
+  | `(#reduce%$tk (proofs := true) (types := true) $term) => go tk term (skipProofs := false) (skipTypes := false)
   | _ => throwUnsupportedSyntax
+where
+  go (tk : Syntax) (term : Syntax) (skipProofs := true) (skipTypes := true) : CommandElabM Unit :=
+    withoutModifyingEnv <| runTermElabM fun _ => Term.withDeclName `_reduce do
+      let e ← Term.elabTerm term none
+      Term.synthesizeSyntheticMVarsNoPostponing
+      let e ← Term.levelMVarToParam (← instantiateMVars e)
+      -- TODO: add options or notation for setting the following parameters
+      withTheReader Core.Context (fun ctx => { ctx with options := ctx.options.setBool `smartUnfolding false }) do
+        let e ← withTransparency (mode := TransparencyMode.all) <| reduce e (skipProofs := skipProofs) (skipTypes := skipTypes)
+        logInfoAt tk e
 
 def hasNoErrorMessages : CommandElabM Bool := do
   return !(← get).messages.hasErrors

src/Lean/Elab/CheckTactic.lean

@@ -17,6 +17,7 @@ namespace Lean.Elab.CheckTactic
 
 open Lean.Meta CheckTactic
 open Lean.Elab.Tactic
+open Lean.Elab.Term
 open Lean.Elab.Command
 
 @[builtin_command_elab Lean.Parser.checkTactic]
@@ -24,7 +25,7 @@ def elabCheckTactic : CommandElab := fun stx => do
   let `(#check_tactic $t ~> $result by $tac) := stx | throwUnsupportedSyntax
   withoutModifyingEnv $ do
     runTermElabM $ fun _vars => do
-      let u ← Lean.Elab.Term.elabTerm t none
+      let u ← withSynthesize (postpone := .no) <| Lean.Elab.Term.elabTerm t none
       let type ← inferType u
       let checkGoalType ← mkCheckGoalType u type
       let mvar ← mkFreshExprMVar (.some checkGoalType)

src/Lean/Elab/DeclModifiers.lean

@@ -81,10 +81,14 @@ def Modifiers.isNonrec : Modifiers → Bool
   | { recKind := .nonrec, .. } => true
   | _                          => false
 
-/-- Store `attr` in `modifiers` -/
-def Modifiers.addAttribute (modifiers : Modifiers) (attr : Attribute) : Modifiers :=
+/-- Adds attribute `attr` in `modifiers` -/
+def Modifiers.addAttr (modifiers : Modifiers) (attr : Attribute) : Modifiers :=
   { modifiers with attrs := modifiers.attrs.push attr }
 
+/-- Filters attributes using `p` -/
+def Modifiers.filterAttrs (modifiers : Modifiers) (p : Attribute → Bool) : Modifiers :=
+  { modifiers with attrs := modifiers.attrs.filter p }
+
 instance : ToFormat Modifiers := ⟨fun m =>
   let components : List Format :=
     (match m.docString? with

src/Lean/Elab/Declaration.lean

@@ -184,7 +184,7 @@ def elabInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
   elabInductiveViews #[v]
 
 def elabClassInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
-  let modifiers := modifiers.addAttribute { name := `class }
+  let modifiers := modifiers.addAttr { name := `class }
   let v ← classInductiveSyntaxToView modifiers stx
   elabInductiveViews #[v]
 

src/Lean/Elab/DefView.lean

@@ -135,8 +135,8 @@ open Meta
 def mkDefViewOfAbbrev (modifiers : Modifiers) (stx : Syntax) : DefView :=
   -- leading_parser "abbrev " >> declId >> optDeclSig >> declVal
   let (binders, type) := expandOptDeclSig stx[2]
-  let modifiers       := modifiers.addAttribute { name := `inline }
-  let modifiers       := modifiers.addAttribute { name := `reducible }
+  let modifiers       := modifiers.addAttr { name := `inline }
+  let modifiers       := modifiers.addAttr { name := `reducible }
   { ref := stx, headerRef := mkNullNode stx.getArgs[:3], kind := DefKind.abbrev, modifiers,
     declId := stx[1], binders, type? := type, value := stx[3] }
 
@@ -159,7 +159,7 @@ def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM De
   let prio            ← liftMacroM <| expandOptNamedPrio stx[2]
   let attrStx         ← `(attr| instance $(quote prio):num)
   let (binders, type) := expandDeclSig stx[4]
-  let modifiers       := modifiers.addAttribute { kind := attrKind, name := `instance, stx := attrStx }
+  let modifiers       := modifiers.addAttr { kind := attrKind, name := `instance, stx := attrStx }
   let declId ← match stx[3].getOptional? with
     | some declId =>
       if ← isTracingEnabledFor `Elab.instance.mkInstanceName then

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

@@ -32,6 +32,9 @@ structure PreDefinition where
   termination : WF.TerminationHints
   deriving Inhabited
 
+def PreDefinition.filterAttrs (preDef : PreDefinition) (p : Attribute → Bool) : PreDefinition :=
+  { preDef with modifiers := preDef.modifiers.filterAttrs p }
+
 def instantiateMVarsAtPreDecls (preDefs : Array PreDefinition) : TermElabM (Array PreDefinition) :=
   preDefs.mapM fun preDef => do
     pure { preDef with type := (← instantiateMVars preDef.type), value := (← instantiateMVars preDef.value) }

src/Lean/Elab/PreDefinition/WF/Main.lean

@@ -129,7 +129,15 @@ def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
         eraseRecAppSyntaxExpr value
       /- `mkFix` invokes `decreasing_tactic` which may add auxiliary theorems to the environment. -/
       let value ← unfoldDeclsFrom envNew value
-      return { unaryPreDef with value }
+      let unaryPreDef := { unaryPreDef with value }
+      /-
+      We must remove `implemented_by` attributes from the auxiliary application because
+      this attribute is only relevant for code that is compiled. Moreover, the `[implemented_by <decl>]`
+      attribute would check whether the `unaryPreDef` type matches with `<decl>`'s type, and produce
+      and error. See issue #2899
+      -/
+      let unaryPreDef := unaryPreDef.filterAttrs fun attr => attr.name != `implemented_by
+      return unaryPreDef
   trace[Elab.definition.wf] ">> {preDefNonRec.declName} :=\n{preDefNonRec.value}"
   let preDefs ← preDefs.mapM fun d => eraseRecAppSyntax d
   -- Do not complain if the user sets @[semireducible], which usually is a noop,

src/Lean/Elab/Structure.lean

@@ -878,7 +878,7 @@ def structCtor           := leading_parser try (declModifiers >> ident >> " :: "
 def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
   checkValidInductiveModifier modifiers
   let isClass   := stx[0].getKind == ``Parser.Command.classTk
-  let modifiers := if isClass then modifiers.addAttribute { name := `class } else modifiers
+  let modifiers := if isClass then modifiers.addAttr { name := `class } else modifiers
   let declId    := stx[1]
   let params    := stx[2].getArgs
   let exts      := stx[3]

src/Lean/Elab/SyntheticMVars.lean

@@ -498,7 +498,7 @@ private partial def withSynthesizeImp (k : TermElabM α) (postpone : PostponeBeh
   Execute `k`, and synthesize pending synthetic metavariables created while executing `k` are solved.
   If `mayPostpone == false`, then all of them must be synthesized.
   Remark: even if `mayPostpone == true`, the method still uses `synthesizeUsingDefault` -/
-@[inline] def withSynthesize [MonadFunctorT TermElabM m] [Monad m] (k : m α) (postpone := PostponeBehavior.no) : m α :=
+@[inline] def withSynthesize [MonadFunctorT TermElabM m] (k : m α) (postpone := PostponeBehavior.no) : m α :=
   monadMap (m := TermElabM) (withSynthesizeImp · postpone) k
 
 private partial def withSynthesizeLightImp (k : TermElabM α) : TermElabM α := do
@@ -512,7 +512,7 @@ private partial def withSynthesizeLightImp (k : TermElabM α) : TermElabM α :=
     modify fun s => { s with pendingMVars := s.pendingMVars ++ pendingMVarsSaved }
 
 /-- Similar to `withSynthesize`, but uses `postpone := .true`, does not use use `synthesizeUsingDefault` -/
-@[inline] def withSynthesizeLight [MonadFunctorT TermElabM m] [Monad m] (k : m α) : m α :=
+@[inline] def withSynthesizeLight [MonadFunctorT TermElabM m] (k : m α) : m α :=
   monadMap (m := TermElabM) (withSynthesizeLightImp ·) k
 
 /-- Elaborate `stx`, and make sure all pending synthetic metavariables created while elaborating `stx` are solved. -/

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

@@ -37,7 +37,7 @@ private def dbg_cache (msg : String) : TacticM Unit := do
 private def dbg_cache' (cacheRef : IO.Ref Cache) (pos : String.Pos) (mvarId : MVarId) (msg : String) : TacticM Unit := do
   if tactic.dbg_cache.get (← getOptions) then
     let {line, column} := (← getFileMap).toPosition pos
-    dbg_trace "{msg}, cache size: {(← cacheRef.get).pre.size}, line: {line}, column: {column}, contains entry: {(← cacheRef.get).pre.find? { mvarId, pos } |>.isSome}"
+    dbg_trace "{msg}, line: {line}, column: {column}, contains entry: {(← cacheRef.get).pre.find? { mvarId, pos } |>.isSome}"
 
 private def findCache? (cacheRef : IO.Ref Cache) (mvarId : MVarId) (stx : Syntax) (pos : String.Pos) : TacticM (Option Snapshot) := do
   let some s := (← cacheRef.get).pre.find? { mvarId, pos } | do dbg_cache "cache key not found"; return none

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

@@ -341,7 +341,7 @@ def mkSimpOnly (stx : Syntax) (usedSimps : Simp.UsedSimps) : MetaM Syntax := do
   let mut localsOrStar := some #[]
   let lctx ← getLCtx
   let env ← getEnv
-  for (thm, _) in usedSimps.toArray.qsort (·.2 < ·.2) do
+  for thm in usedSimps.toArray do
     match thm with
     | .decl declName post inv => -- global definitions in the environment
       if env.contains declName

src/Lean/Elab/Term.lean

@@ -353,7 +353,7 @@ part. `act` is then run on the inner part but with reuse information adjusted as
 For any tactic that participates in reuse, `withNarrowedTacticReuse` should be applied to the
 tactic's syntax and `act` should be used to do recursive tactic evaluation of nested parts.
 -/
-def withNarrowedTacticReuse [Monad m] [MonadExceptOf Exception m] [MonadWithReaderOf Context m]
+def withNarrowedTacticReuse [Monad m] [MonadWithReaderOf Context m]
     [MonadOptions m] [MonadRef m] (split : Syntax → Syntax × Syntax) (act : Syntax → m α)
     (stx : Syntax) : m α := do
   let (outer, inner) := split stx
@@ -377,7 +377,7 @@ NOTE: child nodes after `argIdx` are not tested (which would almost always disab
 necessarily shifted by changes at `argIdx`) so it must be ensured that the result of `arg` does not
 depend on them (i.e. they should not be inspected beforehand).
 -/
-def withNarrowedArgTacticReuse [Monad m] [MonadExceptOf Exception m] [MonadWithReaderOf Context m]
+def withNarrowedArgTacticReuse [Monad m] [MonadWithReaderOf Context m]
     [MonadOptions m] [MonadRef m] (argIdx : Nat) (act : Syntax → m α) (stx : Syntax) : m α :=
   withNarrowedTacticReuse (fun stx => (mkNullNode stx.getArgs[:argIdx], stx[argIdx])) act stx
 
@@ -387,7 +387,7 @@ to `none`. This should be done for tactic blocks that are run multiple times as
 reported progress will jump back and forth (and partial reuse for these kinds of tact blocks is
 similarly questionable).
 -/
-def withoutTacticIncrementality [Monad m] [MonadWithReaderOf Context m] [MonadOptions m] [MonadRef m]
+def withoutTacticIncrementality [Monad m] [MonadWithReaderOf Context m] [MonadOptions m]
     (cond : Bool) (act : m α) : m α := do
   let opts ← getOptions
   withTheReader Term.Context (fun ctx => { ctx with tacSnap? := ctx.tacSnap?.filter fun tacSnap => Id.run do
@@ -398,7 +398,7 @@ def withoutTacticIncrementality [Monad m] [MonadWithReaderOf Context m] [MonadOp
   }) act
 
 /-- Disables incremental tactic reuse for `act` if `cond` is true. -/
-def withoutTacticReuse [Monad m] [MonadWithReaderOf Context m] [MonadOptions m] [MonadRef m]
+def withoutTacticReuse [Monad m] [MonadWithReaderOf Context m] [MonadOptions m]
     (cond : Bool) (act : m α) : m α := do
   let opts ← getOptions
   withTheReader Term.Context (fun ctx => { ctx with tacSnap? := ctx.tacSnap?.map fun tacSnap =>
@@ -1398,7 +1398,7 @@ def resolveLocalName (n : Name) : TermElabM (Option (Expr × List String)) := do
   ```
   def foo.aux := 1
   def foo : Nat → Nat
-    | n => foo.aux -- should not be interpreted as `(foo).bar`
+    | n => foo.aux -- should not be interpreted as `(foo).aux`
   ```
   See test `aStructPerfIssue.lean` for another example.
   We skip auxiliary declarations when `projs` is not empty and `globalDeclFound` is true.
@@ -1415,16 +1415,29 @@ def resolveLocalName (n : Name) : TermElabM (Option (Expr × List String)) := do
   -/
   let rec loop (n : Name) (projs : List String) (globalDeclFound : Bool) := do
     let givenNameView := { view with name := n }
-    let mut globalDeclFound := globalDeclFound
+    let mut globalDeclFoundNext := globalDeclFound
     unless globalDeclFound do
       let r ← resolveGlobalName givenNameView.review
       let r := r.filter fun (_, fieldList) => fieldList.isEmpty
       unless r.isEmpty do
-        globalDeclFound := true
+        globalDeclFoundNext := true
+    /-
+    Note that we use `globalDeclFound` instead of `globalDeclFoundNext` in the following test.
+    Reason: a local should shadow a global with the same name.
+    Consider the following example. See issue #3079
+    ```
+    def foo : Nat := 1
+
+    def bar : Nat :=
+      foo.add 1 -- should be 11
+    where
+      foo := 10
+    ```
+    -/
     match findLocalDecl? givenNameView (skipAuxDecl := globalDeclFound && not projs.isEmpty) with
     | some decl => return some (decl.toExpr, projs)
     | none => match n with
-      | .str pre s => loop pre (s::projs) globalDeclFound
+      | .str pre s => loop pre (s::projs) globalDeclFoundNext
       | _ => return none
   loop view.name [] (globalDeclFound := false)
 
@@ -1836,9 +1849,9 @@ def resolveName' (ident : Syntax) (explicitLevels : List Level) (expectedType? :
       return (c, ids.head!, ids.tail!)
   | _ => throwError "identifier expected"
 
-def resolveId? (stx : Syntax) (kind := "term") (withInfo := false) : TermElabM (Option Expr) :=
+def resolveId? (stx : Syntax) (kind := "term") (withInfo := false) : TermElabM (Option Expr) := withRef stx do
   match stx with
-  | .ident _ _ val preresolved => do
+  | .ident _ _ val preresolved =>
     let rs ← try resolveName stx val preresolved [] catch _ => pure []
     let rs := rs.filter fun ⟨_, projs⟩ => projs.isEmpty
     let fs := rs.map fun (f, _) => f

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
@@ -599,7 +628,7 @@ end TagDeclarationExtension
 
 def MapDeclarationExtension (α : Type) := SimplePersistentEnvExtension (Name × α) (NameMap α)
 
-def mkMapDeclarationExtension [Inhabited α] (name : Name := by exact decl_name%) : IO (MapDeclarationExtension α) :=
+def mkMapDeclarationExtension (name : Name := by exact decl_name%) : IO (MapDeclarationExtension α) :=
   registerSimplePersistentEnvExtension {
     name          := name,
     addImportedFn := fun _ => {},
@@ -984,9 +1013,6 @@ def displayStats (env : Environment) : IO Unit := do
   IO.println ("direct imports:                        " ++ toString env.header.imports);
   IO.println ("number of imported modules:            " ++ toString env.header.regions.size);
   IO.println ("number of memory-mapped modules:       " ++ toString (env.header.regions.filter (·.isMemoryMapped) |>.size));
-  IO.println ("number of consts:                      " ++ toString env.constants.size);
-  IO.println ("number of imported consts:             " ++ toString env.constants.stageSizes.1);
-  IO.println ("number of local consts:                " ++ toString env.constants.stageSizes.2);
   IO.println ("number of buckets for imported consts: " ++ toString env.constants.numBuckets);
   IO.println ("trust level:                           " ++ toString env.header.trustLevel);
   IO.println ("number of extensions:                  " ++ toString env.extensions.size);
@@ -1063,4 +1089,11 @@ instance (m n) [MonadLift m n] [MonadEnv m] : MonadEnv n where
   getEnv    := liftM (getEnv : m Environment)
   modifyEnv := fun f => liftM (modifyEnv f : m Unit)
 
+/-- Constructs a DefinitionVal, inferring the `unsafe` field -/
+def mkDefinitionValInferrringUnsafe [Monad m] [MonadEnv m] (name : Name) (levelParams : List Name)
+    (type : Expr) (value : Expr) (hints : ReducibilityHints) : m DefinitionVal := do
+  let env ← getEnv
+  let safety := if env.hasUnsafe type || env.hasUnsafe value then DefinitionSafety.unsafe else DefinitionSafety.safe
+  return { name, levelParams, type, value, hints, safety }
+
 end Lean

src/Lean/HeadIndex.lean

@@ -32,8 +32,6 @@ inductive HeadIndex where
   | forallE
   deriving Inhabited, BEq, Repr
 
-namespace HeadIndex
-
 /-- Hash code for a `HeadIndex` value. -/
 protected def HeadIndex.hash : HeadIndex → UInt64
   | fvar fvarId         => mixHash 11 <| hash fvarId
@@ -47,8 +45,6 @@ protected def HeadIndex.hash : HeadIndex → UInt64
 
 instance : Hashable HeadIndex := ⟨HeadIndex.hash⟩
 
-end HeadIndex
-
 namespace Expr
 
 /-- Return the number of arguments in the given expression with respect to its `HeadIndex` -/

src/Lean/Meta/Basic.lean

@@ -912,8 +912,8 @@ def mkForallFVars (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedL
 /-- Takes an array `xs` of free variables and metavariables and a
 body term `e` and creates `fun ..xs => e`, suitably
 abstracting `e` and the types in `xs`. -/
-def mkLambdaFVars (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) (binderInfoForMVars := BinderInfo.implicit) : MetaM Expr :=
-  if xs.isEmpty then return e else liftMkBindingM <| MetavarContext.mkLambda xs e usedOnly usedLetOnly binderInfoForMVars
+def mkLambdaFVars (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) (etaReduce : Bool := false) (binderInfoForMVars := BinderInfo.implicit) : MetaM Expr :=
+  if xs.isEmpty then return e else liftMkBindingM <| MetavarContext.mkLambda xs e usedOnly usedLetOnly etaReduce binderInfoForMVars
 
 def mkLetFVars (xs : Array Expr) (e : Expr) (usedLetOnly := true) (binderInfoForMVars := BinderInfo.implicit) : MetaM Expr :=
   mkLambdaFVars xs e (usedLetOnly := usedLetOnly) (binderInfoForMVars := binderInfoForMVars)

src/Lean/Meta/Closure.lean

@@ -349,14 +349,9 @@ end Closure
 def mkAuxDefinition (name : Name) (type : Expr) (value : Expr) (zetaDelta : Bool := false) (compile : Bool := true) : MetaM Expr := do
   let result ← Closure.mkValueTypeClosure type value zetaDelta
   let env ← getEnv
-  let decl := Declaration.defnDecl {
-    name        := name
-    levelParams := result.levelParams.toList
-    type        := result.type
-    value       := result.value
-    hints       := ReducibilityHints.regular (getMaxHeight env result.value + 1)
-    safety      := if env.hasUnsafe result.type || env.hasUnsafe result.value then DefinitionSafety.unsafe else DefinitionSafety.safe
-  }
+  let hints := ReducibilityHints.regular (getMaxHeight env result.value + 1)
+  let decl := Declaration.defnDecl (← mkDefinitionValInferrringUnsafe name result.levelParams.toList
+    result.type result.value  hints)
   addDecl decl
   if compile then
     compileDecl decl

src/Lean/Meta/CompletionName.lean

@@ -25,7 +25,6 @@ namespace Lean.Meta
 
 builtin_initialize completionBlackListExt : TagDeclarationExtension ← mkTagDeclarationExtension
 
-@[export lean_completion_add_to_black_list]
 def addToCompletionBlackList (env : Environment) (declName : Name) : Environment :=
   completionBlackListExt.tag env declName
 

src/Lean/Meta/Constructions.lean

@@ -7,33 +7,101 @@ prelude
 import Lean.AuxRecursor
 import Lean.AddDecl
 import Lean.Meta.AppBuilder
+import Lean.Meta.CompletionName
 
 namespace Lean
 
-@[extern "lean_mk_cases_on"] opaque mkCasesOnImp (env : Environment) (declName : @& Name) : Except KernelException Environment
-@[extern "lean_mk_rec_on"] opaque mkRecOnImp (env : Environment) (declName : @& Name) : Except KernelException Environment
-@[extern "lean_mk_no_confusion"] opaque mkNoConfusionCoreImp (env : Environment) (declName : @& Name) : Except KernelException Environment
-@[extern "lean_mk_below"] opaque mkBelowImp (env : Environment) (declName : @& Name) : Except KernelException Environment
-@[extern "lean_mk_ibelow"] opaque mkIBelowImp (env : Environment) (declName : @& Name) : Except KernelException Environment
-@[extern "lean_mk_brec_on"] opaque mkBRecOnImp (env : Environment) (declName : @& Name) : Except KernelException Environment
-@[extern "lean_mk_binduction_on"] opaque mkBInductionOnImp (env : Environment) (declName : @& Name) : Except KernelException Environment
-
-variable [Monad m] [MonadEnv m] [MonadError m] [MonadOptions m]
-
-@[inline] private def adaptFn (f : Environment → Name → Except KernelException Environment) (declName : Name) : m Unit := do
-  let env ← ofExceptKernelException (f (← getEnv) declName)
-  modifyEnv fun _ => env
-
-def mkCasesOn (declName : Name) : m Unit := adaptFn mkCasesOnImp declName
-def mkRecOn (declName : Name) : m Unit := adaptFn mkRecOnImp declName
-def mkNoConfusionCore (declName : Name) : m Unit := adaptFn mkNoConfusionCoreImp declName
-def mkBelow (declName : Name) : m Unit := adaptFn mkBelowImp declName
-def mkIBelow (declName : Name) : m Unit := adaptFn mkIBelowImp declName
-def mkBRecOn (declName : Name) : m Unit := adaptFn mkBRecOnImp declName
-def mkBInductionOn (declName : Name) : m Unit := adaptFn mkBInductionOnImp declName
+@[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
+@[extern "lean_mk_below"] opaque mkBelowImp (env : Environment) (declName : @& Name) (ibelow : Bool) : Except KernelException Declaration
+@[extern "lean_mk_brec_on"] opaque mkBRecOnImp (env : Environment) (declName : @& Name) (ind : Bool) : Except KernelException Declaration
 
 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)
+  addDecl decl
+  setReducibleAttribute name
+  modifyEnv fun env => markAuxRecursor env name
+  modifyEnv fun env => addProtected env name
+
+private def mkBelowOrIBelow (declName : Name) (ibelow : Bool) : MetaM Unit := do
+  let .inductInfo indVal ← getConstInfo declName | return
+  unless indVal.isRec do return
+  if ← isPropFormerType indVal.type then return
+
+  let decl ← ofExceptKernelException (mkBelowImp (← getEnv) declName ibelow)
+  let name := decl.definitionVal!.name
+  addDecl decl
+  setReducibleAttribute name
+  modifyEnv fun env => addToCompletionBlackList env name
+  modifyEnv fun env => addProtected env name
+
+def mkBelow (declName : Name) : MetaM Unit := mkBelowOrIBelow declName true
+def mkIBelow (declName : Name) : MetaM Unit := mkBelowOrIBelow declName false
+
+private def mkBRecOrBInductionOn (declName : Name) (ind : Bool) : MetaM Unit := do
+  let .inductInfo indVal ← getConstInfo declName | return
+  unless indVal.isRec do return
+  if ← isPropFormerType indVal.type then return
+  let .recInfo recInfo ← getConstInfo (mkRecName declName) | return
+  unless recInfo.numMotives = indVal.all.length do
+    /-
+    The mutual declaration containing `declName` contains nested inductive datatypes.
+    We don't support this kind of declaration here yet. We probably never will :)
+    To support it, we will need to generate an auxiliary `below` for each nested inductive
+    type since their default `below` is not good here. For example, at
+    ```
+    inductive Term
+    | var : String -> Term
+    | app : String -> List Term -> Term
+    ```
+    The `List.below` is not useful since it will not allow us to recurse over the nested terms.
+    We need to generate another one using the auxiliary recursor `Term.rec_1` for `List Term`.
+    -/
+    return
+
+  let decl ← ofExceptKernelException (mkBRecOnImp (← getEnv) declName ind)
+  let name := decl.definitionVal!.name
+  addDecl decl
+  setReducibleAttribute name
+  modifyEnv fun env => markAuxRecursor env name
+  modifyEnv fun env => addProtected env name
+
+def mkBRecOn (declName : Name) : MetaM Unit := mkBRecOrBInductionOn declName false
+def mkBInductionOn (declName : Name) : MetaM Unit := mkBRecOrBInductionOn declName true
+
+def mkNoConfusionCore (declName : Name) : MetaM Unit := do
+  -- Do not do anything unless can_elim_to_type. TODO: Extract to util
+  let .inductInfo indVal ← getConstInfo declName | return
+  let recInfo ← getConstInfo (mkRecName declName)
+  unless recInfo.levelParams.length > indVal.levelParams.length do return
+
+  let name := Name.mkStr declName "noConfusionType"
+  let decl ← ofExceptKernelException (mkNoConfusionTypeCoreImp (← getEnv) declName)
+  addDecl decl
+  setReducibleAttribute name
+  modifyEnv fun env => addToCompletionBlackList env name
+  modifyEnv fun env => addProtected env name
+
+  let name := Name.mkStr declName "noConfusion"
+  let decl ← ofExceptKernelException (mkNoConfusionCoreImp (← getEnv) declName)
+  addDecl decl
+  setReducibleAttribute name
+  modifyEnv fun env => markNoConfusion env name
+  modifyEnv fun env => addProtected env name
+
 def mkNoConfusionEnum (enumName : Name) : MetaM Unit := do
   if (← getEnv).contains ``noConfusionEnum then
     mkToCtorIdx

src/Lean/Meta/DiscrTree.lean

@@ -850,7 +850,7 @@ def foldValues (f : σ → α → σ) (init : σ) (t : DiscrTree α) : σ :=
 Check for the presence of a value satisfying a predicate.
 -/
 @[inline]
-def containsValueP [BEq α] (t : DiscrTree α) (f : α → Bool) : Bool :=
+def containsValueP (t : DiscrTree α) (f : α → Bool) : Bool :=
   t.foldValues (init := false) fun r a => r || f a
 
 /--

src/Lean/Meta/ExprDefEq.lean

@@ -419,10 +419,10 @@ where the index is the position in the local context.
 -/
 private partial def mkLambdaFVarsWithLetDeps (xs : Array Expr) (v : Expr) : MetaM (Option Expr) := do
   if not (← hasLetDeclsInBetween) then
-    mkLambdaFVars xs v
+    mkLambdaFVars xs v (etaReduce := true)
   else
     let ys ← addLetDeps
-    mkLambdaFVars ys v
+    mkLambdaFVars ys v (etaReduce := true)
 
 where
   /-- Return true if there are let-declarions between `xs[0]` and `xs[xs.size-1]`.
@@ -1775,15 +1775,12 @@ private partial def isDefEqQuickOther (t s : Expr) : MetaM LBool := do
         | LBool.true => return LBool.true
         | LBool.false => return LBool.false
         | _ =>
-          if tFn.isMVar || sFn.isMVar then
-            let ctx ← read
-            if ctx.config.isDefEqStuckEx then do
-              trace[Meta.isDefEq.stuck] "{t} =?= {s}"
-              Meta.throwIsDefEqStuck
-            else
-              return LBool.false
+          let ctx ← read
+          if ctx.config.isDefEqStuckEx then do
+            trace[Meta.isDefEq.stuck] "{t} =?= {s}"
+            Meta.throwIsDefEqStuck
           else
-            return LBool.undef
+            return LBool.false
       else
         isDefEqQuickMVarMVar t s
 

src/Lean/Meta/InferType.lean

@@ -377,29 +377,41 @@ def isType (e : Expr) : MetaM Bool := do
   withReader (fun ctx => { ctx with lctx := ctx.lctx.mkLocalDecl fvarId name type bi }) do
     x (mkFVar fvarId)
 
-def isTypeFormerTypeQuick : Expr → Bool
-  | .forallE _ _ b _ => isTypeFormerTypeQuick b
-  | .sort _ => true
-  | _ => false
+def typeFormerTypeLevelQuick : Expr → Option Level
+  | .forallE _ _ b _ => typeFormerTypeLevelQuick b
+  | .sort l => some l
+  | _ => none
+
+/--
+Return `u` iff `type` is `Sort u` or `As → Sort u`.
+-/
+partial def typeFormerTypeLevel (type : Expr) : MetaM (Option Level) := do
+  match typeFormerTypeLevelQuick type with
+  | .some l => return .some l
+  | .none => savingCache <| go type #[]
+where
+  go (type : Expr) (xs : Array Expr) : MetaM (Option Level) := do
+    match type with
+    | .sort l => return some l
+    | .forallE n d b c => withLocalDecl' n c (d.instantiateRev xs) fun x => go b (xs.push x)
+    | _ =>
+      let type ← whnfD (type.instantiateRev xs)
+      match type with
+      | .sort l => return some l
+      | .forallE .. => go type #[]
+      | _ => return none
 
 /--
 Return true iff `type` is `Sort _` or `As → Sort _`.
 -/
 partial def isTypeFormerType (type : Expr) : MetaM Bool := do
-  match isTypeFormerTypeQuick type with
-  | true => return true
-  | false => savingCache <| go type #[]
-where
-  go (type : Expr) (xs : Array Expr) : MetaM Bool := do
-    match type with
-    | .sort .. => return true
-    | .forallE n d b c => withLocalDecl' n c (d.instantiateRev xs) fun x => go b (xs.push x)
-    | _ =>
-      let type ← whnfD (type.instantiateRev xs)
-      match type with
-      | .sort .. => return true
-      | .forallE .. => go type #[]
-      | _ => return false
+  return (← typeFormerTypeLevel type).isSome
+
+/--
+Return true iff `type` is `Prop` or `As → Prop`.
+-/
+partial def isPropFormerType (type : Expr) : MetaM Bool := do
+  return (← typeFormerTypeLevel type) == .some .zero
 
 /--
 Return true iff `e : Sort _` or `e : (forall As, Sort _)`.

src/Lean/Meta/Match/Match.lean

@@ -776,14 +776,8 @@ def mkMatcherAuxDefinition (name : Name) (type : Expr) (value : Expr) : MetaM (E
   match (matcherExt.getState env).find? (result.value, compile) with
   | some nameNew => return (mkMatcherConst nameNew, none)
   | none =>
-    let decl := Declaration.defnDecl {
-      name
-      levelParams := result.levelParams.toList
-      type        := result.type
-      value       := result.value
-      hints       := ReducibilityHints.abbrev
-      safety      := if env.hasUnsafe result.type || env.hasUnsafe result.value then DefinitionSafety.unsafe else DefinitionSafety.safe
-    }
+    let decl := Declaration.defnDecl (← mkDefinitionValInferrringUnsafe name result.levelParams.toList
+      result.type result.value .abbrev)
     trace[Meta.Match.debug] "{name} : {result.type} := {result.value}"
     let addMatcher : MatcherInfo → MetaM Unit := fun mi => do
       addDecl decl

src/Lean/Meta/SynthInstance.lean

@@ -194,9 +194,6 @@ def checkSystem : SynthM Unit := do
   Core.checkInterrupted
   Core.checkMaxHeartbeatsCore "typeclass" `synthInstance.maxHeartbeats (← read).maxHeartbeats
 
-@[inline] def mapMetaM (f : forall {α}, MetaM α → MetaM α) {α} : SynthM α → SynthM α :=
-  monadMap @f
-
 instance : Inhabited (SynthM α) where
   default := fun _ _ => default
 
@@ -336,26 +333,6 @@ def getSubgoals (lctx : LocalContext) (localInsts : LocalInstances) (xs : Array
     subgoals := inst.synthOrder.map (mvars[·]!) |>.toList
   }
 
-/--
-Similar to `mkLambdaFVars`, but ensures result is eta-reduced.
-For example, suppose `e` is the local variable `inst x y`, and `xs` is `#[x, y]`, then
-the result is `inst` instead of `fun x y => inst x y`.
-
-We added this auxiliary function because of aliases such as `DecidablePred`. For example,
-consider the following definition.
-```
-def filter (p : α → Prop) [inst : DecidablePred p] (xs : List α) : List α :=
-  match xs with
-  | [] => []
-  | x :: xs' => if p x then x :: filter p xs' else filter p xs'
-```
-Without `mkLambdaFVars'`, the implicit instance at the `filter` applications would be `fun x => inst x` instead of `inst`.
-Moreover, the equation lemmas associated with `filter` would have `fun x => inst x` on their right-hand-side. Then,
-we would start getting terms such as `fun x => (fun x => inst x) x` when using the equational theorem.
--/
-private def mkLambdaFVars' (xs : Array Expr) (e : Expr) : MetaM Expr :=
-  return (← mkLambdaFVars xs e).eta
-
 /--
   Try to synthesize metavariable `mvar` using the instance `inst`.
   Remark: `mctx` is set using `withMCtx`.
@@ -373,7 +350,23 @@ def tryResolve (mvar : Expr) (inst : Instance) : MetaM (Option (MetavarContext
     withTraceNode `Meta.synthInstance.tryResolve (withMCtx (← getMCtx) do
         return m!"{exceptOptionEmoji ·} {← instantiateMVars mvarTypeBody} ≟ {← instantiateMVars instTypeBody}") do
     if (← isDefEq mvarTypeBody instTypeBody) then
-      let instVal ← mkLambdaFVars' xs instVal
+      /-
+      We set `etaReduce := true`.
+      For example, suppose `e` is the local variable `inst x y`, and `xs` is `#[x, y]`, then
+      the result is `inst` instead of `fun x y => inst x y`.
+
+      Consider the following definition.
+      ```
+      def filter (p : α → Prop) [inst : DecidablePred p] (xs : List α) : List α :=
+        match xs with
+        | [] => []
+        | x :: xs' => if p x then x :: filter p xs' else filter p xs'
+      ```
+      Without `etaReduce := true`, the implicit instance at the `filter` applications would be `fun x => inst x` instead of `inst`.
+      Moreover, the equation lemmas associated with `filter` would have `fun x => inst x` on their right-hand-side. Then,
+      we would start getting terms such as `fun x => (fun x => inst x) x` when using the equational theorem.
+      -/
+      let instVal ← mkLambdaFVars xs instVal (etaReduce := true)
       if (← isDefEq mvar instVal) then
         return some ((← getMCtx), subgoals)
     return none
@@ -486,7 +479,7 @@ private def removeUnusedArguments? (mctx : MetavarContext) (mvar : Expr) : MetaM
         let ys := ys.toArray
         let mvarType' ← mkForallFVars ys body
         withLocalDeclD `redf mvarType' fun f => do
-          let transformer ← mkLambdaFVars' #[f] (← mkLambdaFVars' xs (mkAppN f ys))
+          let transformer ← mkLambdaFVars #[f] (← mkLambdaFVars xs (mkAppN f ys) (etaReduce := true)) (etaReduce := true)
           trace[Meta.synthInstance.unusedArgs] "{mvarType}\nhas unused arguments, reduced type{indentExpr mvarType'}\nTransformer{indentExpr transformer}"
           return some (mvarType', transformer)
 

src/Lean/Meta/Tactic/Apply.lean

@@ -11,34 +11,6 @@ import Lean.Meta.Tactic.Util
 import Lean.PrettyPrinter
 
 namespace Lean.Meta
-/-- Controls which new mvars are turned in to goals by the `apply` tactic.
-- `nonDependentFirst`  mvars that don't depend on other goals appear first in the goal list.
-- `nonDependentOnly` only mvars that don't depend on other goals are added to goal list.
-- `all` all unassigned mvars are added to the goal list.
--/
-inductive ApplyNewGoals where
-  | nonDependentFirst | nonDependentOnly | all
-
-/-- Configures the behaviour of the `apply` tactic. -/
-structure ApplyConfig where
-  newGoals := ApplyNewGoals.nonDependentFirst
-  /--
-  If `synthAssignedInstances` is `true`, then `apply` will synthesize instance implicit arguments
-  even if they have assigned by `isDefEq`, and then check whether the synthesized value matches the
-  one inferred. The `congr` tactic sets this flag to false.
-  -/
-  synthAssignedInstances := true
-  /--
-  If `allowSynthFailures` is `true`, then `apply` will return instance implicit arguments
-  for which typeclass search failed as new goals.
-  -/
-  allowSynthFailures := false
-  /--
-  If `approx := true`, then we turn on `isDefEq` approximations. That is, we use
-  the `approxDefEq` combinator.
-  -/
-  approx : Bool := true
-
 /--
   Compute the number of expected arguments and whether the result type is of the form
   (?m ...) where ?m is an unassigned metavariable.

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

@@ -19,6 +19,7 @@ structure Literal where
   n     : Nat
   /-- Actual value. -/
   value : BitVec n
+  deriving DecidableEq, Repr
 
 /--
 Try to convert `OfNat.ofNat`/`BitVec.OfNat` application into a

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

@@ -14,6 +14,7 @@ open Lean Meta Simp
 structure Value where
   n     : Nat
   value : Fin n
+  deriving DecidableEq, Repr
 
 def fromExpr? (e : Expr) : SimpM (Option Value) := do
   let some ⟨n, value⟩ ← getFinValue? e | return none

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -34,7 +34,7 @@ def Config.updateArith (c : Config) : CoreM Config := do
 
 /-- Return true if `e` is of the form `ofNat n` where `n` is a kernel Nat literal -/
 def isOfNatNatLit (e : Expr) : Bool :=
-  e.isAppOfArity ``OfNat.ofNat 3 && e.appFn!.appArg!.isRawNatLit
+  e.isAppOf ``OfNat.ofNat && e.getAppNumArgs >= 3 && (e.getArg! 1).isRawNatLit
 
 /--
 If `e` is a raw Nat literal and `OfNat.ofNat` is not in the list of declarations to unfold,
@@ -430,7 +430,10 @@ private def doNotVisit (pred : Expr → Bool) (declName : Name) : DSimproc := fu
     if (← readThe Simp.Context).isDeclToUnfold declName then
       return .continue e
     else
-      return .done e
+      -- Users may have added a `[simp]` rfl theorem for the literal
+      match (← (← getMethods).dpost e) with
+      | .continue none => return .done e
+      | r => return r
   else
     return .continue e
 

src/Lean/Meta/Tactic/Simp/SimpTheorems.lean

@@ -175,7 +175,7 @@ def ppOrigin [Monad m] [MonadEnv m] [MonadError m] : Origin → m MessageData
   | .stx _ ref => return ref
   | .other n => return n
 
-def ppSimpTheorem [Monad m] [MonadLiftT IO m] [MonadEnv m] [MonadError m] (s : SimpTheorem) : m MessageData := do
+def ppSimpTheorem [Monad m] [MonadEnv m] [MonadError m] (s : SimpTheorem) : m MessageData := do
   let perm := if s.perm then ":perm" else ""
   let name ← ppOrigin s.origin
   let prio := m!":{s.priority}"
@@ -466,8 +466,25 @@ def SimpTheorems.add (s : SimpTheorems) (id : Origin) (levelParams : Array Name)
 def SimpTheorems.addDeclToUnfold (d : SimpTheorems) (declName : Name) : MetaM SimpTheorems := do
   if let some eqns ← getEqnsFor? declName then
     let mut d := d
-    for eqn in eqns do
-      d ← SimpTheorems.addConst d eqn
+    for h : i in [:eqns.size] do
+      let eqn := eqns[i]
+      /-
+      We assign priorities to the equational lemmas so that more specific ones
+      are tried first before a possible catch-all with possible side-conditions.
+
+      We assign very low priorities to match the simplifiers behavior when unfolding
+      a definition, which happens in `simpLoop`’ `visitPreContinue` after applying
+      rewrite rules.
+
+      Definitions with more than 100 equational theorems will use priority 1 for all
+      but the last (a heuristic, not perfect).
+      -/
+      let prio := if eqns.size > 100 then
+        if i + 1 = eqns.size then 0 else 1
+      else
+        100 - i
+      -- We assign very low priority to equational le
+      d ← SimpTheorems.addConst d eqn (prio := prio)
     /-
     Even if a function has equation theorems,
     we also store it in the `toUnfold` set in the following two cases:

src/Lean/Meta/Tactic/Simp/Types.lean

@@ -106,8 +106,21 @@ structure Context where
 def Context.isDeclToUnfold (ctx : Context) (declName : Name) : Bool :=
   ctx.simpTheorems.isDeclToUnfold declName
 
--- We should use `PHashMap` because we backtrack the contents of `UsedSimps`
-abbrev UsedSimps := PHashMap Origin Nat
+structure UsedSimps where
+  -- We should use `PHashMap` because we backtrack the contents of `UsedSimps`
+  -- The natural number tracks the insertion order
+  map  : PHashMap Origin Nat := {}
+  size : Nat := 0
+  deriving Inhabited
+
+def UsedSimps.insert (s : UsedSimps) (thmId : Origin) : UsedSimps :=
+  if s.map.contains thmId then
+    s
+  else match s with
+    | { map, size } => { map := map.insert thmId size, size := size + 1 }
+
+def UsedSimps.toArray (s : UsedSimps) : Array Origin :=
+  s.map.toArray.qsort (·.2 < ·.2) |>.map (·.1)
 
 structure Diagnostics where
   /-- Number of times each simp theorem has been used/applied. -/
@@ -367,9 +380,7 @@ def recordSimpTheorem (thmId : Origin) : SimpM Unit := do
       else
         pure thmId
     | _ => pure thmId
-  modify fun s => if s.usedTheorems.contains thmId then s else
-    let n := s.usedTheorems.size
-    { s with usedTheorems := s.usedTheorems.insert thmId n }
+  modify fun s => { s with usedTheorems := s.usedTheorems.insert thmId }
 
 def recordCongrTheorem (declName : Name) : SimpM Unit := do
   modifyDiag fun s =>

src/Lean/Meta/Transform.lean

@@ -21,7 +21,7 @@ inductive TransformStep where
   For `pre`, this means visiting the children of the expression.
   For `post`, this is equivalent to returning `done`. -/
   | continue (e? : Option Expr := none)
-  deriving Inhabited
+  deriving Inhabited, Repr
 
 namespace Core
 
@@ -81,7 +81,7 @@ namespace Meta
   `.const f` is not visited again. Put differently: every `.const f` is visited once, with its
   arguments if present, on its own otherwise.
  -/
-partial def transform {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m] [MonadTrace m] [MonadRef m] [MonadOptions m] [AddMessageContext m]
+partial def transform {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m]
     (input : Expr)
     (pre   : Expr → m TransformStep := fun _ => return .continue)
     (post  : Expr → m TransformStep := fun e => return .done e)

src/Lean/MetavarContext.lean

@@ -1274,13 +1274,25 @@ partial def revert (xs : Array Expr) (mvarId : MVarId) : M (Expr × Array Expr)
   let e ← elimMVarDeps xs e
   pure (e.abstractRange i xs)
 
+private def mkLambda' (x : Name) (bi : BinderInfo) (t : Expr) (b : Expr) (etaReduce : Bool) : Expr :=
+  if etaReduce then
+    match b with
+    | .app f (.bvar 0) =>
+      if !f.hasLooseBVar 0 then
+        f.lowerLooseBVars 1 1
+      else
+        mkLambda x bi t b
+    | _ => mkLambda x bi t b
+  else
+    mkLambda x bi t b
+
 /--
   Similar to `LocalContext.mkBinding`, but handles metavariables correctly.
   If `usedOnly == true` then `forall` and `lambda` expressions are created only for used variables.
   If `usedLetOnly == true` then `let` expressions are created only for used (let-) variables. -/
-@[specialize] def mkBinding (isLambda : Bool) (lctx : LocalContext) (xs : Array Expr) (e : Expr) (usedOnly : Bool) (usedLetOnly : Bool) : M (Expr × Nat) := do
+@[specialize] def mkBinding (isLambda : Bool) (lctx : LocalContext) (xs : Array Expr) (e : Expr) (usedOnly : Bool) (usedLetOnly : Bool) (etaReduce : Bool) : M Expr := do
   let e ← abstractRange xs xs.size e
-  xs.size.foldRevM (init := (e, 0)) fun i (e, num) => do
+  xs.size.foldRevM (init := e) fun i e => do
       let x := xs[i]!
       if x.isFVar then
         match lctx.getFVar! x with
@@ -1289,27 +1301,27 @@ partial def revert (xs : Array Expr) (mvarId : MVarId) : M (Expr × Array Expr)
             let type := type.headBeta;
             let type ← abstractRange xs i type
             if isLambda then
-              return (Lean.mkLambda n bi type e, num + 1)
+              return mkLambda' n bi type e etaReduce
             else
-              return (Lean.mkForall n bi type e, num + 1)
+              return Lean.mkForall n bi type e
           else
-            return (e.lowerLooseBVars 1 1, num)
+            return e.lowerLooseBVars 1 1
         | LocalDecl.ldecl _ _ n type value nonDep _ =>
           if !usedLetOnly || e.hasLooseBVar 0 then
             let type  ← abstractRange xs i type
             let value ← abstractRange xs i value
-            return (mkLet n type value e nonDep, num + 1)
+            return mkLet n type value e nonDep
           else
-            return (e.lowerLooseBVars 1 1, num)
+            return e.lowerLooseBVars 1 1
       else
         let mvarDecl := (← get).mctx.getDecl x.mvarId!
         let type := mvarDecl.type.headBeta
         let type ← abstractRange xs i type
         let id ← if mvarDecl.userName.isAnonymous then mkFreshBinderName else pure mvarDecl.userName
         if isLambda then
-          return (Lean.mkLambda id (← read).binderInfoForMVars type e, num + 1)
+          return mkLambda' id (← read).binderInfoForMVars type e etaReduce
         else
-          return (Lean.mkForall id (← read).binderInfoForMVars type e, num + 1)
+          return Lean.mkForall id (← read).binderInfoForMVars type e
 
 end MkBinding
 
@@ -1325,15 +1337,15 @@ def elimMVarDeps (xs : Array Expr) (e : Expr) (preserveOrder : Bool) : MkBinding
 def revert (xs : Array Expr) (mvarId : MVarId) (preserveOrder : Bool) : MkBindingM (Expr × Array Expr) := fun ctx =>
   MkBinding.revert xs mvarId { preserveOrder, mainModule := ctx.mainModule }
 
-def mkBinding (isLambda : Bool) (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) (binderInfoForMVars := BinderInfo.implicit) : MkBindingM (Expr × Nat) := fun ctx =>
+def mkBinding (isLambda : Bool) (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) (etaReduce := false) (binderInfoForMVars := BinderInfo.implicit) : MkBindingM Expr := fun ctx =>
   let mvarIdsToAbstract := xs.foldl (init := {}) fun s x => if x.isMVar then s.insert x.mvarId! else s
-  MkBinding.mkBinding isLambda ctx.lctx xs e usedOnly usedLetOnly { preserveOrder := false, binderInfoForMVars, mvarIdsToAbstract, mainModule := ctx.mainModule }
+  MkBinding.mkBinding isLambda ctx.lctx xs e usedOnly usedLetOnly etaReduce { preserveOrder := false, binderInfoForMVars, mvarIdsToAbstract, mainModule := ctx.mainModule }
 
-@[inline] def mkLambda (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) (binderInfoForMVars := BinderInfo.implicit) : MkBindingM Expr :=
-  return (← mkBinding (isLambda := true) xs e usedOnly usedLetOnly binderInfoForMVars).1
+@[inline] def mkLambda (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) (etaReduce := false) (binderInfoForMVars := BinderInfo.implicit) : MkBindingM Expr :=
+  return ← mkBinding (isLambda := true) xs e usedOnly usedLetOnly etaReduce binderInfoForMVars
 
 @[inline] def mkForall (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) (binderInfoForMVars := BinderInfo.implicit) : MkBindingM Expr :=
-  return (← mkBinding (isLambda := false) xs e usedOnly usedLetOnly binderInfoForMVars).1
+  return ← mkBinding (isLambda := false) xs e usedOnly usedLetOnly false binderInfoForMVars
 
 @[inline] def abstractRange (e : Expr) (n : Nat) (xs : Array Expr) : MkBindingM Expr := fun ctx =>
   MkBinding.abstractRange xs n e { preserveOrder := false, mainModule := ctx.mainModule }

src/Lean/Modifiers.lean

@@ -10,11 +10,9 @@ namespace Lean
 
 builtin_initialize protectedExt : TagDeclarationExtension ← mkTagDeclarationExtension
 
-@[export lean_add_protected]
 def addProtected (env : Environment) (n : Name) : Environment :=
   protectedExt.tag env n
 
-@[export lean_is_protected]
 def isProtected (env : Environment) (n : Name) : Bool :=
   protectedExt.isTagged env n
 

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

@@ -435,8 +435,6 @@ structure Pair (α : Type u) (β : Type v) : Type (max u v) where
   "#check " >> termParser
 @[builtin_command_parser] def check_failure  := leading_parser
   "#check_failure " >> termParser -- Like `#check`, but succeeds only if term does not type check
-@[builtin_command_parser] def reduce         := leading_parser
-  "#reduce " >> termParser
 @[builtin_command_parser] def eval           := leading_parser
   "#eval " >> termParser
 @[builtin_command_parser] def synth          := leading_parser
@@ -449,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
@@ -671,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/ReducibilityAttrs.lean

@@ -165,11 +165,11 @@ def getReducibilityStatus [Monad m] [MonadEnv m] (declName : Name) : m Reducibil
   return getReducibilityStatusCore (← getEnv) declName
 
 /-- Set the reducibility attribute for the given declaration. -/
-def setReducibilityStatus [Monad m] [MonadEnv m] (declName : Name) (s : ReducibilityStatus) : m Unit := do
+def setReducibilityStatus [MonadEnv m] (declName : Name) (s : ReducibilityStatus) : m Unit :=
   modifyEnv fun env => setReducibilityStatusCore env declName s .global .anonymous
 
 /-- Set the given declaration as `[reducible]` -/
-def setReducibleAttribute [Monad m] [MonadEnv m] (declName : Name) : m Unit := do
+def setReducibleAttribute [MonadEnv m] (declName : Name) : m Unit :=
   setReducibilityStatus declName ReducibilityStatus.reducible
 
 /-- Return `true` if the given declaration has been marked as `[reducible]`. -/
@@ -185,7 +185,7 @@ def isIrreducible [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
   | _ => return false
 
 /-- Set the given declaration as `[irreducible]` -/
-def setIrreducibleAttribute [Monad m] [MonadEnv m] (declName : Name) : m Unit := do
+def setIrreducibleAttribute [MonadEnv m] (declName : Name) : m Unit :=
   setReducibilityStatus declName ReducibilityStatus.irreducible
 
 

src/Lean/ResolveName.lean

@@ -187,10 +187,17 @@ def resolveGlobalName (env : Environment) (ns : Name) (openDecls : List OpenDecl
 
 /-! # Namespace resolution -/
 
-def resolveNamespaceUsingScope? (env : Environment) (n : Name) : Name → Option Name
-  | .anonymous    => if env.isNamespace n then some n else none
-  | ns@(.str p _) => if env.isNamespace (ns ++ n) then some (ns ++ n) else resolveNamespaceUsingScope? env n p
-  | _             => unreachable!
+def resolveNamespaceUsingScope? (env : Environment) (n : Name) (ns : Name) : Option Name :=
+  match ns with
+  | .str p _ =>
+    if env.isNamespace (ns ++ n) then
+      some (ns ++ n)
+    else
+      resolveNamespaceUsingScope? env n p
+  | .anonymous =>
+    let n := n.replacePrefix rootNamespace .anonymous
+    if env.isNamespace n then some n else none
+  | _ => unreachable!
 
 def resolveNamespaceUsingOpenDecls (env : Environment) (n : Name) : List OpenDecl → List Name
   | [] => []
@@ -307,7 +314,7 @@ def ensureNoOverload [Monad m] [MonadError m] (n : Name) (cs : List Name) : m Na
 def resolveGlobalConstNoOverloadCore [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (n : Name) : m Name := do
   ensureNoOverload n (← resolveGlobalConstCore n)
 
-def preprocessSyntaxAndResolve [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (stx : Syntax) (k : Name → m (List Name)) : m (List Name) := do
+def preprocessSyntaxAndResolve [Monad m] [MonadEnv m] [MonadError m] (stx : Syntax) (k : Name → m (List Name)) : m (List Name) := do
   match stx with
   | .ident _ _ n pre => do
     let pre := pre.filterMap fun

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/Lean/Util/ForEachExprWhere.lean

@@ -16,8 +16,6 @@ if the number of subterms satisfying `p` is a small subset of the set of subterm
 If `p` holds for most subterms, then it is more efficient to use `forEach f e`.
 -/
 
-variable {ω : Type} {m : Type → Type} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m]
-
 namespace ForEachExprWhere
 abbrev cacheSize : USize := 8192 - 1
 
@@ -37,7 +35,9 @@ unsafe def initCache : State := {
   checked := {}
 }
 
-abbrev ForEachM {ω : Type} (m : Type → Type) [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] := StateRefT' ω State m
+abbrev ForEachM {ω : Type} (m : Type → Type) [STWorld ω m] := StateRefT' ω State m
+
+variable {ω : Type} {m : Type → Type} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m]
 
 unsafe def visited (e : Expr) : ForEachM m Bool := do
   let s ← get

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/include/lean/lean.h

@@ -990,7 +990,10 @@ static inline size_t lean_string_capacity(lean_object * o) { return lean_to_stri
 static inline size_t lean_string_byte_size(lean_object * o) { return sizeof(lean_string_object) + lean_string_capacity(o); }
 /* instance : inhabited char := ⟨'A'⟩ */
 static inline uint32_t lean_char_default_value() { return 'A'; }
+LEAN_EXPORT lean_obj_res lean_mk_string_unchecked(char const * s, size_t sz, size_t len);
 LEAN_EXPORT lean_obj_res lean_mk_string_from_bytes(char const * s, size_t sz);
+LEAN_EXPORT lean_obj_res lean_mk_string_from_bytes_unchecked(char const * s, size_t sz);
+LEAN_EXPORT lean_obj_res lean_mk_ascii_string_unchecked(char const * s);
 LEAN_EXPORT lean_obj_res lean_mk_string(char const * s);
 static inline char const * lean_string_cstr(b_lean_obj_arg o) {
     assert(lean_is_string(o));

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: