fix: move openssl linker flags after libc++ link

.github/workflows/build-template.yml

@@ -59,11 +59,11 @@ jobs:
         with:
           msystem: clang64
           # `:` means do not prefix with msystem
-          pacboy: "make: python: cmake clang ccache gmp libuv git: zip: unzip: diffutils: binutils: tree: zstd tar:"
+          pacboy: "make: python: cmake clang ccache gmp libuv openssl: git: zip: unzip: diffutils: binutils: tree: zstd tar:"
         if: runner.os == 'Windows'
       - name: Install Brew Packages
         run: |
-          brew install ccache tree zstd coreutils gmp libuv
+          brew install ccache tree zstd coreutils gmp libuv openssl
         if: runner.os == 'macOS'
       - name: Checkout
         uses: actions/checkout@v6
@@ -92,7 +92,7 @@ jobs:
         run: |
           sudo dpkg --add-architecture i386
           sudo apt-get update
-          sudo apt-get install -y gcc-multilib g++-multilib ccache libuv1-dev:i386 pkgconf:i386
+          sudo apt-get install -y gcc-multilib g++-multilib ccache libuv1-dev:i386 libssl-dev:i386 pkgconf:i386
         if: matrix.cmultilib
       - name: Restore Cache
         id: restore-cache

doc/make/index.md

@@ -9,6 +9,7 @@ Requirements
 - [CMake](http://www.cmake.org)
 - [GMP (GNU multiprecision library)](http://gmplib.org/)
 - [LibUV](https://libuv.org/)
+- [OpenSSL](https://www.openssl.org/)
 
 Platform-Specific Setup
 -----------------------

doc/make/msys2.md

@@ -32,7 +32,7 @@ MSYS2 has a package management system, [pacman][pacman].
 Here are the commands to install all dependencies needed to compile Lean on your machine.
 
 ```bash
-pacman -S make python mingw-w64-clang-x86_64-cmake mingw-w64-clang-x86_64-clang mingw-w64-clang-x86_64-ccache mingw-w64-clang-x86_64-libuv mingw-w64-clang-x86_64-gmp git unzip diffutils binutils
+pacman -S make python mingw-w64-clang-x86_64-cmake mingw-w64-clang-x86_64-clang mingw-w64-clang-x86_64-ccache mingw-w64-clang-x86_64-libuv mingw-w64-clang-x86_64-gmp mingw-w64-clang-x86_64-openssl git unzip diffutils binutils
 ```
 
 You should now be able to run these commands:

doc/make/osx-10.9.md

@@ -32,12 +32,13 @@ following to use `g++`.
 cmake -DCMAKE_CXX_COMPILER=g++ ...
 ```
 
-## Required Packages: CMake, GMP, libuv, pkgconf
+## Required Packages: CMake, GMP, libuv, OpenSSL, pkgconf
 
 ```bash
 brew install cmake
 brew install gmp
 brew install libuv
+brew install openssl
 brew install pkgconf
 ```
 

doc/make/ubuntu.md

@@ -8,5 +8,5 @@ follow the [generic build instructions](index.md).
 ## Basic packages
 
 ```bash
-sudo apt-get install git libgmp-dev libuv1-dev cmake ccache clang pkgconf
+sudo apt-get install git libgmp-dev libuv1-dev libssl-dev cmake ccache clang pkgconf
 ```

flake.nix

@@ -24,7 +24,7 @@
           stdenv = pkgs.overrideCC pkgs.stdenv llvmPackages.clang;
         } ({
           buildInputs = with pkgs; [
-            cmake gmp libuv ccache pkg-config
+            cmake gmp libuv ccache pkg-config openssl openssl.dev
             llvmPackages.bintools  # wrapped lld
             llvmPackages.llvm  # llvm-symbolizer for asan/lsan
             gdb
@@ -34,7 +34,21 @@
           hardeningDisable = [ "all" ];
           # more convenient `ctest` output
           CTEST_OUTPUT_ON_FAILURE = 1;
-        } // pkgs.lib.optionalAttrs pkgs.stdenv.isLinux {
+        } // pkgs.lib.optionalAttrs pkgs.stdenv.isLinux (let
+          # Build OpenSSL 3 statically using pkgsDist's old-glibc stdenv,
+          # so the resulting static libs don't require newer glibc symbols.
+          opensslForDist = pkgsDist.stdenv.mkDerivation {
+            name = "openssl-static-${pkgs.lib.getVersion pkgs.openssl.name}";
+            inherit (pkgs.openssl) src;
+            nativeBuildInputs = [ pkgsDist.perl ];
+            configurePhase = ''
+            patchShebangs .
+            ./config --prefix=$out no-shared no-tests
+          '';
+            buildPhase = "make -j$NIX_BUILD_CORES";
+            installPhase = "make install_sw";
+          };
+        in {
           GMP = (pkgsDist.gmp.override { withStatic = true; }).overrideAttrs (attrs:
             pkgs.lib.optionalAttrs (pkgs.stdenv.system == "aarch64-linux") {
               # would need additional linking setup on Linux aarch64, we don't use it anywhere else either
@@ -53,13 +67,15 @@
             };
             doCheck = false;
           });
+          OPENSSL = opensslForDist;
+          OPENSSL_DEV = opensslForDist;
           GLIBC = pkgsDist.glibc;
           GLIBC_DEV = pkgsDist.glibc.dev;
           GCC_LIB = pkgsDist.gcc.cc.lib;
           ZLIB = pkgsDist.zlib;
           # for CI coredumps
           GDB = pkgsDist.gdb;
-        });
+        }));
     in {
       devShells.${system} = {
         # The default development shell for working on lean itself

script/prepare-llvm-linux.sh

@@ -1,7 +1,7 @@
 #!/usr/bin/env bash
 set -euxo pipefail
 
-# run from root build directory (from inside nix-shell or otherwise defining GLIBC/ZLIB/GMP) as in
+# run from root build directory (from inside nix-shell or otherwise defining GLIBC/ZLIB/GMP/OPENSSL) as in
 # ```
 # eval cmake ../.. $(../../script/prepare-llvm-linux.sh ~/Downloads/lean-llvm-x86_64-linux-gnu.tar.zst)
 # ```
@@ -42,6 +42,8 @@ $CP $GLIBC/lib/*crt* stage1/lib/
 # runtime
 (cd llvm; $CP --parents lib/clang/*/lib/*/{clang_rt.*.o,libclang_rt.builtins*} ../stage1)
 $CP llvm/lib/*/lib{c++,c++abi,unwind}.* $GMP/lib/libgmp.a $LIBUV/lib/libuv.a stage1/lib/
+# bundle OpenSSL static libs
+cp $OPENSSL/lib/libssl.a $OPENSSL/lib/libcrypto.a stage1/lib/
 # LLVM 19 appears to ship the dependencies in 'llvm/lib/<target-triple>/' and 'llvm/include/<target-triple>/'
 # but clang-19 that we use to compile is linked against 'llvm/lib/' and 'llvm/include'
 # https://github.com/llvm/llvm-project/issues/54955
@@ -57,6 +59,7 @@ for f in $GLIBC/lib/{ld,lib{c,dl,m,rt,pthread}}-*; do b=$(basename $f); cp $f st
 OPTIONS=()
 # We build cadical using the custom toolchain on Linux to avoid glibc versioning issues
 echo -n " -DLEAN_STANDALONE=ON -DCADICAL_USE_CUSTOM_CXX=ON"
+echo -n " -DOPENSSL_INCLUDE_DIR=$OPENSSL_DEV/include -DOPENSSL_SSL_LIBRARY=$OPENSSL/lib/libssl.a -DOPENSSL_CRYPTO_LIBRARY=$OPENSSL/lib/libcrypto.a"
 echo -n " -DCMAKE_CXX_COMPILER=$PWD/llvm-host/bin/clang++ -DLEAN_CXX_STDLIB='-Wl,-Bstatic -lc++ -lc++abi -Wl,-Bdynamic'"
 # these should also be used for cadical, so do not use `LEAN_EXTRA_CXX_FLAGS` here
 echo -n " -DCMAKE_CXX_FLAGS='--sysroot $PWD/llvm -idirafter $GLIBC_DEV/include ${EXTRA_FLAGS:-}'"
@@ -74,8 +77,8 @@ fi
 echo -n " -DLEANC_INTERNAL_FLAGS='--sysroot ROOT -nostdinc -isystem ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang"
 # ld.so is usually included by the libc.so linker script but we discard those. Make sure it is linked to only after `libc.so` like in the original
 # linker script so that no libc symbols are bound to it instead.
-echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='--sysroot ROOT -L ROOT/lib -L ROOT/lib/glibc -lc -lc_nonshared -Wl,--as-needed -l:ld.so -Wl,--no-as-needed -lpthread_nonshared -Wl,--as-needed -Wl,-Bstatic -lgmp -lunwind -luv -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld'"
-# when not using the above flags, link GMP dynamically/as usual
-echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-Wl,--as-needed -lgmp -luv -lpthread -ldl -lrt -Wl,--no-as-needed'"
+echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='--sysroot ROOT -L ROOT/lib -L ROOT/lib/glibc -lc -lc_nonshared -Wl,--as-needed -l:ld.so -Wl,--no-as-needed -lpthread_nonshared -Wl,--as-needed -Wl,-Bstatic -lgmp -lunwind -luv -lssl -lcrypto -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld'"
+# when not using the above flags, link GMP/libuv/OpenSSL dynamically/as usual
+echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-Wl,--as-needed -lgmp -luv -Wl,-Bstatic -lssl -lcrypto -Wl,-Bdynamic -lpthread -ldl -lrt -Wl,--no-as-needed'"
 # do not set `LEAN_CC` for tests
 echo -n " -DLEAN_TEST_VARS=''"

script/prepare-llvm-macos.sh

@@ -10,6 +10,7 @@ set -uxo pipefail
 
 GMP=${GMP:-$(brew --prefix)}
 LIBUV=${LIBUV:-$(brew --prefix)}
+OPENSSL=${OPENSSL:-$(brew --prefix openssl@3)}
 
 [[ -d llvm ]] || (mkdir llvm; gtar xf $1 --strip-components 1 --directory llvm)
 [[ -d llvm-host ]] || if [[ "$#" -gt 1 ]]; then
@@ -41,6 +42,7 @@ gcp llvm/lib/libc++.dylib stage1/lib/libc
 # and apparently since Sonoma does not do so implicitly either
 install_name_tool -id /usr/lib/libc++.dylib stage1/lib/libc/libc++.dylib
 echo -n " -DLEAN_STANDALONE=ON"
+echo -n " -DOPENSSL_INCLUDE_DIR=$OPENSSL/include -DOPENSSL_SSL_LIBRARY=$OPENSSL/lib/libssl.a -DOPENSSL_CRYPTO_LIBRARY=$OPENSSL/lib/libcrypto.a"
 # do not change C++ compiler; libc++ etc. being system libraries means there's no danger of conflicts,
 # and the custom clang++ outputs a myriad of warnings when consuming the SDK
 echo -n " -DLEAN_EXTRA_CXX_FLAGS='${EXTRA_FLAGS:-}'"
@@ -48,7 +50,8 @@ if [[ -L llvm-host ]]; then
   echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang"
   gcp $GMP/lib/libgmp.a stage1/lib/
   gcp $LIBUV/lib/libuv.a stage1/lib/
-  echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp -luv'"
+  gcp $OPENSSL/lib/libssl.a $OPENSSL/lib/libcrypto.a stage1/lib/
+  echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp -luv -lssl -lcrypto'"
 else
   echo -n " -DCMAKE_C_COMPILER=$PWD/llvm-host/bin/clang -DLEANC_OPTS='--sysroot $PWD/stage1 -resource-dir $PWD/stage1/lib/clang/15.0.1 ${EXTRA_FLAGS:-}'"
 fi

script/prepare-llvm-mingw.sh

@@ -40,14 +40,14 @@ cp /clang64/lib/{crtbegin,crtend,crt2,dllcrt2}.o stage1/lib/
 # tells the compiler how to dynamically link against `bcrypt.dll` (which is located in the System32 folder).
 # This distinction is relevant specifically for `libicu.a`/`icu.dll` because there we want updates to the time zone database to
 # be delivered to users via Windows Update without having to recompile Lean or Lean programs.
-cp /clang64/lib/lib{m,bcrypt,mingw32,moldname,mingwex,msvcrt,pthread,advapi32,shell32,user32,kernel32,ucrtbase,psapi,iphlpapi,userenv,ws2_32,dbghelp,ole32,icu}.* /clang64/lib/libgmp.a /clang64/lib/libuv.a llvm/lib/lib{c++,c++abi,unwind}.a stage1/lib/
+cp /clang64/lib/lib{m,bcrypt,mingw32,moldname,mingwex,msvcrt,pthread,advapi32,shell32,user32,kernel32,ucrtbase,psapi,iphlpapi,userenv,ws2_32,dbghelp,ole32,icu,crypt32,gdi32}.* /clang64/lib/libgmp.a /clang64/lib/libuv.a /clang64/lib/libssl.a /clang64/lib/libcrypto.a llvm/lib/lib{c++,c++abi,unwind}.a stage1/lib/
 echo -n " -DLEAN_STANDALONE=ON"
 echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang.exe -DCMAKE_C_COMPILER_WORKS=1 -DCMAKE_CXX_COMPILER=$PWD/llvm/bin/clang++.exe -DCMAKE_CXX_COMPILER_WORKS=1 -DLEAN_CXX_STDLIB='-lc++ -lc++abi'"
 echo -n " -DSTAGE0_CMAKE_C_COMPILER=clang -DSTAGE0_CMAKE_CXX_COMPILER=clang++"
 echo -n " -DLEAN_EXTRA_CXX_FLAGS='--sysroot $PWD/llvm -idirafter /clang64/include/'"
 echo -n " -DLEANC_INTERNAL_FLAGS='--sysroot ROOT -nostdinc -isystem ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang.exe"
-echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='--sysroot ROOT -L ROOT/lib -Wl,-Bstatic -lgmp $(pkg-config --static --libs libuv) -lunwind -Wl,-Bdynamic -fuse-ld=lld'"
-# when not using the above flags, link GMP dynamically/as usual. Always link ICU dynamically.
-echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp $(pkg-config --libs libuv) -lucrtbase'"
+echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='--sysroot ROOT -L ROOT/lib -Wl,-Bstatic -lgmp $(pkg-config --static --libs libuv) -lssl -lcrypto -lunwind -Wl,-Bdynamic -lcrypt32 -lgdi32 -fuse-ld=lld'"
+# when not using the above flags, link GMP/libuv/OpenSSL dynamically/as usual. Always link ICU dynamically.
+echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp $(pkg-config --libs libuv) -lssl -lcrypto -lcrypt32 -lgdi32 -lucrtbase'"
 # do not set `LEAN_CC` for tests
 echo -n " -DLEAN_TEST_VARS=''"

script/release_repos.yml

@@ -28,14 +28,6 @@ repositories:
     branch: main
     dependencies: []
 
-  - name: leansqlite
-    url: https://github.com/leanprover/leansqlite
-    toolchain-tag: true
-    stable-branch: false
-    branch: main
-    dependencies:
-      - plausible
-
   - name: verso
     url: https://github.com/leanprover/verso
     toolchain-tag: true
@@ -108,7 +100,7 @@ repositories:
     toolchain-tag: true
     stable-branch: false
     branch: main
-    dependencies: [lean4-cli, BibtexQuery, mathlib4, leansqlite]
+    dependencies: [lean4-cli, BibtexQuery, mathlib4]
 
   - name: cslib
     url: https://github.com/leanprover/cslib

src/CMakeLists.txt

@@ -357,6 +357,28 @@ if(NOT LEAN_STANDALONE)
   string(APPEND LEAN_EXTRA_LINKER_FLAGS " ${LIBUV_LDFLAGS}")
 endif()
 
+# OpenSSL
+if(NOT "${CMAKE_SYSTEM_NAME}" MATCHES "Emscripten")
+  find_package(OpenSSL 3 REQUIRED)
+  set(OPENSSL_LIBRARIES ${OPENSSL_SSL_LIBRARY} ${OPENSSL_CRYPTO_LIBRARY})
+  include_directories(${OPENSSL_INCLUDE_DIR})
+  string(JOIN " " OPENSSL_LIBRARIES_STR ${OPENSSL_LIBRARIES})
+  if(NOT LEAN_STANDALONE)
+    string(APPEND LEAN_EXTRA_LINKER_FLAGS " ${OPENSSL_LIBRARIES_STR}")
+  endif()
+endif()
+
+if(CMAKE_SYSTEM_NAME MATCHES "Linux")
+  string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,-rpath,\\$$ORIGIN")
+endif()
+
+if(CMAKE_SYSTEM_NAME MATCHES "Windows")
+  string(APPEND LEANSHARED_LINKER_FLAGS " -lcrypt32 -lgdi32")
+  if(NOT LEAN_STANDALONE)
+    string(APPEND LEAN_EXTRA_LINKER_FLAGS " -lcrypt32 -lgdi32")
+  endif()
+endif()
+
 # Windows SDK (for ICU)
 if(CMAKE_SYSTEM_NAME MATCHES "Windows")
   # Pass 'tools' to skip MSVC version check (as MSVC/Visual Studio is not necessarily installed)
@@ -472,6 +494,17 @@ endif()
 string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
 string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
 
+# In standalone (release) builds, OpenSSL must be statically embedded in libleanshared.so.
+# In non-standalone (dev/CI nix) builds, `find_package(OpenSSL)` resolves to shared libs from
+# the nix store. Adding those to libleanshared.so would produce DT_NEEDED entries pointing into
+# the nix store (including transitive libc++.so.1 because nix's libssl is built with libc++).
+# Those paths don't exist in `out/` during `make run-local` tests, breaking them.
+# For non-standalone builds, OpenSSL is instead provided via LEAN_EXTRA_LINKER_FLAGS (leanc.sh)
+# and resolved at runtime from the loading executable.
+if(DEFINED OPENSSL_LIBRARIES_STR AND LEAN_STANDALONE)
+  string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " ${OPENSSL_LIBRARIES_STR}")
+endif()
+
 # in local builds, link executables and not just dynlibs against C++ stdlib as well,
 # which is required for e.g. asan
 if(NOT LEAN_STANDALONE)
@@ -763,7 +796,7 @@ if(STAGE GREATER 1)
   endif()
 else()
   add_subdirectory(runtime)
-  if(CMAKE_SYSTEM_NAME MATCHES "Emscripten")
+  if("${CMAKE_SYSTEM_NAME}" MATCHES "Emscripten")
     add_dependencies(leanrt libuv)
     add_dependencies(leanrt_initial-exec libuv)
   endif()

src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean

@@ -271,7 +271,7 @@ private def optionPelim' {α : Type u_1} (t : Option α) {β :  Sort u_2}
 
 /--
 Inserts an `Option` case distinction after the first computation of a call to `MonadAttach.pbind`.
-This lemma is useful for simplifying the second computation, which often involves `match` expressions
+This lemma is useful for simplifying the second computation, which often involes `match` expressions
 that use `pbind`'s proof term.
 -/
 private theorem pbind_eq_pbind_if_isSome [Monad m] [MonadAttach m] (x : m (Option α)) (f : (_ : _) → _ → m β) :

src/Init/Data/String/Decode.lean

@@ -363,7 +363,7 @@ theorem toBitVec_eq_of_parseFirstByte_eq_threeMore {b : UInt8} (h : parseFirstBy
 public def isInvalidContinuationByte (b : UInt8) : Bool :=
   b &&& 0xc0 != 0x80
 
-theorem isInvalidContinuationByte_eq_false_iff {b : UInt8} :
+theorem isInvalidContinutationByte_eq_false_iff {b : UInt8} :
     isInvalidContinuationByte b = false ↔ b &&& 0xc0 = 0x80 := by
   simp [isInvalidContinuationByte]
 

src/Init/Data/String/Lemmas/Iterate.lean

@@ -31,7 +31,7 @@ namespace Slice
 /--
 A list of all positions starting at {name}`p`.
 
-This function is not meant to be used in actual programs. Actual programs should use
+This function is not meant to be used in actual progams. Actual programs should use
 {name}`Slice.positionsFrom` or {name}`Slice.positions`.
 -/
 protected def Model.positionsFrom {s : Slice} (p : s.Pos) : List { p : s.Pos // p ≠ s.endPos } :=
@@ -206,7 +206,7 @@ end Slice
 /--
 A list of all positions starting at {name}`p`.
 
-This function is not meant to be used in actual programs. Actual programs should use
+This function is not meant to be used in actual progams. Actual programs should use
 {name}`Slice.positionsFrom` or {name}`Slice.positions`.
 -/
 protected def Model.positionsFrom {s : String} (p : s.Pos) : List { p : s.Pos // p ≠ s.endPos } :=

src/Init/Data/String/Subslice.lean

@@ -23,7 +23,7 @@ Given a {name}`Slice` {name}`s`, the type {lean}`s.Subslice` is the type of half
 in {name}`s` delineated by a valid position on both sides.
 
 This type is useful to track regions of interest within some larger slice that is also of interest.
-In contrast, {name}`Slice` is used to track regions of interest within some larger string that is
+In contrast, {name}`Slice` is used to track regions of interest whithin some larger string that is
 not or no longer relevant.
 
 Equality on {name}`Subslice` is somewhat better behaved than on {name}`Slice`, but note that there

src/Init/Prelude.lean

@@ -145,7 +145,7 @@ Examples:
 The constant function that ignores its argument.
 
 If `a : α`, then `Function.const β a : β → α` is the “constant function with value `a`”. For all
-arguments `b : β`, `Function.const β a b = a`. It is often written directly as `fun _ => a`.
+arguments `b : β`, `Function.const β a b = a`.
 
 Examples:
  * `Function.const Bool 10 true = 10`
@@ -3754,7 +3754,7 @@ class Functor (f : Type u → Type v) : Type (max (u+1) v) where
   /--
   Mapping a constant function.
 
-  Given `a : α` and `v : f β`, `mapConst a v` is equivalent to `(fun _ => a) <$> v`. For some
+  Given `a : α` and `v : f α`, `mapConst a v` is equivalent to `Function.const _ a <$> v`. For some
   functors, this can be implemented more efficiently; for all other functors, the default
   implementation may be used.
   -/

src/Init/System/IO.lean

@@ -1880,12 +1880,3 @@ lead to undefined behavior.
 -/
 @[extern "lean_runtime_forget"]
 def Runtime.forget (a : α) : BaseIO Unit := return
-
-set_option linter.unusedVariables false in
-/--
-Ensures `a` remains at least alive until the call site by holding a reference to `a`. This can be useful
-for unsafe code (such as an FFI) that relies on a Lean object not being freed until after some point
-in the program. At runtime, this will be a no-op as the C compiler will optimize away this call.
--/
-@[extern "lean_runtime_hold"]
-def Runtime.hold (a : @& α) : BaseIO Unit := return

src/Lean/Compiler/LCNF/PassManager.lean

@@ -121,7 +121,7 @@ def mkPerDeclaration (name : Name) (phase : Phase)
   occurrence := occurrence
   phase := phase
   name := name
-  run := fun xs => xs.mapM fun decl => do checkSystem "LCNF compiler"; run decl
+  run := fun xs => xs.mapM run
 
 end Pass
 

src/Lean/Compiler/LCNF/ResetReuse.lean

@@ -28,7 +28,7 @@ inserts addition instructions to attempt to reuse the memory right away instead
 allocator.
 
 For this the paper defines three functions:
-- `R` (called `Decl.insertResetReuse` here) which looks for candidates that might be eligible for
+- `R` (called `Decl.insertResetReuse` here) which looks for candidates that might be elligible for
   reuse. For these variables it invokes `D`.
 - `D` which looks for code regions in which the target variable is dead (i.e. no longer read from),
   it then invokes `S`. If `S` succeeds it inserts a `reset` instruction to match the `reuse`

src/Lean/Compiler/LCNF/Simp/Main.lean

@@ -217,8 +217,6 @@ Simplify `code`
 -/
 partial def simp (code : Code .pure) : SimpM (Code .pure) := withIncRecDepth do
   incVisited
-  if (← get).visited % 128 == 0 then
-    checkSystem "LCNF simp"
   match code with
   | .let decl k =>
     let baseDecl := decl

src/Lean/Compiler/LCNF/SimpCase.lean

@@ -24,7 +24,7 @@ In particular we perform:
 - folding of the most common cases arm into the default arm if possible
 
 Note: Currently the simplifier still contains almost equivalent simplifications to the ones shown
-here. We know that this causes unforeseen behavior and do plan on changing it eventually.
+here. We know that this causes unforseen behavior and do plan on changing it eventually.
 -/
 
 -- TODO: the following functions are duplicated from simp and should be deleted in simp once we

src/Lean/Compiler/LCNF/ToDecl.lean

@@ -171,7 +171,7 @@ def toDecl (declName : Name) : CompilerM (Decl .pure) := do
     if compiler.ignoreBorrowAnnotation.get (← getOptions) then
       decl := { decl with params := ← decl.params.mapM (·.updateBorrow false) }
     if isExport env decl.name && decl.params.any (·.borrow) then
-      throwError m!" Declaration {decl.name} is marked as `export` but some of its parameters have borrow annotations.\n Consider using `set_option compiler.ignoreBorrowAnnotation true in` to suppress the borrow annotations in its type.\n If the declaration is part of an `export`/`extern` pair make sure to also suppress the annotations at the `extern` declaration."
+      throwError m!" Declaration {decl.name} is marked as `export` but some of its parameters have borrow annotations.\n Consider using `set_option compiler.ignoreBorrowAnnotation true in` to supress the borrow annotations in its type.\n If the declaration is part of an `export`/`extern` pair make sure to also supress the annotations at the `extern` declaration."
     return decl
 
 end Lean.Compiler.LCNF

src/Lean/CoreM.lean

@@ -20,8 +20,6 @@ register_builtin_option diagnostics : Bool := {
   descr    := "collect diagnostic information"
 }
 
-builtin_initialize registerTraceClass `diagnostics
-
 register_builtin_option diagnostics.threshold : Nat := {
   defValue := 20
   descr    := "only diagnostic counters above this threshold are reported by the definitional equality"
@@ -446,6 +444,10 @@ Note that the value of `ctx.initHeartbeats` is ignored and replaced with `IO.get
 @[inline] def CoreM.toIO' (x : CoreM α) (ctx : Context) (s : State) : IO α :=
   (·.1) <$> x.toIO ctx s
 
+/-- withIncRecDepth for a monad `m` such that `[MonadControlT CoreM n]`. -/
+protected def withIncRecDepth [Monad m] [MonadControlT CoreM m] (x : m α) : m α :=
+  controlAt CoreM fun runInBase => withIncRecDepth (runInBase x)
+
 /--
 Throws an internal interrupt exception if cancellation has been requested. The exception is not
 caught by `try catch` but is intended to be caught by `Command.withLoggingExceptions` at the top
@@ -460,12 +462,6 @@ heartbeat tracking (e.g. `SynthInstance`).
     if (← tk.isSet) then
       throwInterruptException
 
-/-- withIncRecDepth for a monad `m` such that `[MonadControlT CoreM n]`.
-Also checks for cancellation, so that recursive elaboration functions
-(inferType, whnf, isDefEq, …) respond promptly to interrupt requests. -/
-protected def withIncRecDepth [Monad m] [MonadControlT CoreM m] (x : m α) : m α :=
-  controlAt CoreM fun runInBase => do checkInterrupted; withIncRecDepth (runInBase x)
-
 register_builtin_option debug.moduleNameAtTimeout : Bool := {
   defValue := true
   descr    := "include module name in deterministic timeout error messages.\nRemark: we set this option to false to increase the stability of our test suite"

src/Lean/Elab/Deriving/DecEq.lean

@@ -111,7 +111,7 @@ def mkMatchNew (ctx : Context) (header : Header) (indVal : InductiveVal) : TermE
   let x1 := mkIdent header.targetNames[0]!
   let x2 := mkIdent header.targetNames[1]!
   let ctorIdxName := mkCtorIdxName indVal.name
-  -- NB: the getMatcherInfo? assumes all matchers are called `match_`
+  -- NB: the getMatcherInfo? assumes all mathcers are called `match_`
   let casesOnSameCtorName ← mkFreshUserName (indVal.name ++ `match_on_same_ctor)
   mkCasesOnSameCtor casesOnSameCtorName indVal.name
   let alts ← Array.ofFnM (n := indVal.numCtors) fun ⟨ctorIdx, _⟩ => do

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

@@ -36,7 +36,7 @@ def mkContext (lratPath : System.FilePath) (cfg : BVDecideConfig) : TermElabM Ta
   TacticContext.new lratPath cfg
 
 /--
-Prepare an `Expr` that proves `bvExpr.unsat` using native evaluation.
+Prepare an `Expr` that proves `bvExpr.unsat` using native evalution.
 -/
 def lratChecker (ctx : TacticContext) (reflectionResult : ReflectionResult) : MetaM Expr := do
   let cert ← LratCert.ofFile ctx.lratPath ctx.config.trimProofs

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

@@ -357,7 +357,6 @@ def reflectBV (g : MVarId) : M ReflectionResult := g.withContext do
   let mut sats := #[]
   let mut unusedHypotheses := {}
   for hyp in hyps do
-    checkSystem "bv_decide"
     if let (some reflected, lemmas) ← (SatAtBVLogical.of (mkFVar hyp)).run then
       sats := (sats ++ lemmas).push reflected
     else

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

@@ -33,7 +33,6 @@ where
   Reify `x`, returns `none` if the reification procedure failed.
   -/
   go (origExpr : Expr) : LemmaM (Option ReifiedBVExpr) := do
-    checkSystem "bv_decide"
     match_expr origExpr with
     | BitVec.ofNat _ _ => goBvLit origExpr
     | HAnd.hAnd _ _ _ _ lhsExpr rhsExpr =>
@@ -341,7 +340,6 @@ where
   Reify `t`, returns `none` if the reification procedure failed.
   -/
   go (origExpr : Expr) : LemmaM (Option ReifiedBVLogical) := do
-    checkSystem "bv_decide"
     match_expr origExpr with
     | Bool.true => ReifiedBVLogical.mkBoolConst true
     | Bool.false => ReifiedBVLogical.mkBoolConst false

src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Basic.lean

@@ -159,7 +159,6 @@ Repeatedly run a list of `Pass` until they either close the goal or an iteration
 the goal anymore.
 -/
 partial def fixpointPipeline (passes : List Pass) (goal : MVarId) : PreProcessM (Option MVarId) := do
-  checkSystem "bv_decide"
   let mut newGoal := goal
   for pass in passes do
     if let some nextGoal ← pass.run newGoal then

src/Lean/Meta/ExprDefEq.lean

@@ -48,16 +48,6 @@ register_builtin_option backward.isDefEq.respectTransparency : Bool := {
   when checking whether implicit arguments are definitionally equal"
 }
 
-/--
-Controls the transparency used to check whether the type of metavariable matches the type of the
-term being assigned to it.
--/
-register_builtin_option backward.isDefEq.respectTransparency.types : Bool := {
-  defValue := false -- TODO: replace with `true` after we fix stage0
-  descr    := "if true, do not bump transparency to `.default` \
-  when checking whether the type of a metavariable matches the type of the term being assigned to it."
-}
-
 /--
 Controls whether *all* implicit arguments (not just instance-implicit `[..]`) get their
 transparency bumped to `TransparencyMode.instances` during `isDefEq`.
@@ -345,10 +335,10 @@ private def isDefEqArgsFirstPass
 
 /--
 Ensure `MetaM` configuration is strong enough for checking definitional equality of
-implicit arguments (e.g., instances) and types.
-For example, we must be able to unfold instances, `beta := true`, `proj := .yesWithDelta` are essential.
+instances. For example, we must be able to unfold instances, `beta := true`, `proj := .yesWithDelta`
+are essential.
 -/
-@[inline] def withImplicitConfig (x : MetaM α) : MetaM α :=
+@[inline] def withInstanceConfig (x : MetaM α) : MetaM α :=
   withAtLeastTransparency .instances do
     let cfg ← getConfig
     if cfg.beta && cfg.iota && cfg.zeta && cfg.zetaHave && cfg.zetaDelta && cfg.proj == .yesWithDelta then
@@ -392,7 +382,7 @@ private partial def isDefEqArgs (f : Expr) (args₁ args₂ : Array Expr) : Meta
       -- Bump to `.instances` so that `[implicit_reducible]` definitions (instances, `Nat.add`,
       -- `Array.size`, etc.) are unfolded. The user doesn't choose implicit arguments directly,
       -- so Lean should try harder than the caller's transparency to make them match.
-      unless (← withImplicitConfig <| Meta.isExprDefEqAux a₁ a₂) do return false
+      unless (← withInstanceConfig <| Meta.isExprDefEqAux a₁ a₂) do return false
     else if respectTransparency then
       unless (← Meta.isExprDefEqAux a₁ a₂) do return false
     else
@@ -402,7 +392,7 @@ private partial def isDefEqArgs (f : Expr) (args₁ args₂ : Array Expr) : Meta
     let a₁   := args₁[i]!
     let a₂   := args₂[i]!
     if respectTransparency && (implicitBump || finfo.paramInfo[i]!.isInstance) then
-      unless (← withImplicitConfig <| Meta.isExprDefEqAux a₁ a₂) do return false
+      unless (← withInstanceConfig <| Meta.isExprDefEqAux a₁ a₂) do return false
     else if !respectTransparency && finfo.paramInfo[i]!.isInstance then
       -- Old behavior
       unless (← withInferTypeConfig <| Meta.isExprDefEqAux a₁ a₂) do return false
@@ -464,19 +454,6 @@ private partial def isDefEqBindingAux (lctx : LocalContext) (fvars : Array Expr)
   let lctx ← getLCtx
   isDefEqBindingAux lctx #[] a b #[]
 
-/--
-Returns `true` if both `backward.isDefEq.respectTransparency` and `backward.isDefEq.respectTransparency.types` is true.
-
-The option `backward.isDefEq.respectTransparency.types` is newer than ``backward.isDefEq.respectTransparency`,
-and is used to enable the transparency bump when checking metavariable assignments.
-
-If `backward.isDefEq.respectTransparency` is `false`, then we automatically disable
-`backward.isDefEq.respectTransparency.types` too.
--/
-abbrev respectTransparencyAtTypes : CoreM Bool := do
-  let opts ← getOptions
-  return backward.isDefEq.respectTransparency.types.get opts && backward.isDefEq.respectTransparency.get opts
-
 private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool :=
   withTraceNodeBefore `Meta.isDefEq.assign.checkTypes (fun _ => return m!"({mvar} : {← inferType mvar}) := ({v} : {← inferType v})") do
     if !mvar.isMVar then
@@ -485,24 +462,14 @@ private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool :=
     else
       -- must check whether types are definitionally equal or not, before assigning and returning true
       let mvarType ← inferType mvar
-      let vType ← inferType v
-      if (← respectTransparencyAtTypes) then
-        withImplicitConfig do
-          if (← Meta.isExprDefEqAux mvarType vType) then
-            mvar.mvarId!.assign v
-            return true
-          else
-            if (← isDiagnosticsEnabled) then withInferTypeConfig do
-              if (← Meta.isExprDefEqAux mvarType vType) then
-                trace[diagnostics] "failure when assigning metavariable with type{indentExpr mvarType}\nwhich is not definitionally equal to{indentExpr vType}\nwhen using `.instances` transparency, but it is with `.default`.\nWorkaround: `set_option backward.isDefEq.respectTransparency.types false`"
-            return false
-      else
-        withInferTypeConfig do
-          if (← Meta.isExprDefEqAux mvarType vType) then
-            mvar.mvarId!.assign v
-            return true
-          else
-            return false
+      -- **TODO**: avoid transparency bump. Let's fix other issues first
+      withInferTypeConfig do
+        let vType ← inferType v
+        if (← Meta.isExprDefEqAux mvarType vType) then
+          mvar.mvarId!.assign v
+          pure true
+        else
+          pure false
 
 /--
 Auxiliary method for solving constraints of the form `?m xs := v`.
@@ -2095,7 +2062,7 @@ private def isDefEqProj : Expr → Expr → MetaM Bool
        for instance-implicit parameters. -/
     let fromClass := isClass (← getEnv) m
     let isDefEqStructArgs (x : MetaM Bool) : MetaM Bool :=
-      if fromClass then withImplicitConfig x else x
+      if fromClass then withInstanceConfig x else x
     if (← read).inTypeClassResolution then
       -- See comment at `inTypeClassResolution`
       pure (i == j && m == n) <&&> isDefEqStructArgs (Meta.isExprDefEqAux t s)

src/Lean/Meta/Match/Match.lean

@@ -33,12 +33,12 @@ The high-level overview of moves are
   * If there is an alternative, solve its constraints
   * Else use `contradiction` to prove completeness of the match
 * Process “independent prefixes” of patterns. These are patterns that can be processed without
-  affecting the other alternatives, and without side effects in the sense of updating the `mvarId`.
+  affecting the aother alternatives, and without side effects in the sense of updating the `mvarId`.
   These are
   - variable patterns; substitute
   - inaccessible patterns; add equality constraints
   - as-patterns: substitute value and equality
-  After these have been processed, we use `.inaccessible x` where `x` is the variable being matched
+  After thes have been processed, we use `.inaccessible x` where `x` is the variable being matched
   to mark them as “done”.
 * If all patterns start with “done”, drop the first variable
 * The first alt has only “done” patterns, drop remaining alts (they're overlapped)
@@ -1108,9 +1108,6 @@ def mkMatcherAuxDefinition (name : Name) (type : Expr) (value : Expr) (isSplitte
       -- matcher bodies should always be exported, if not private anyway
       withExporting do
         addDecl decl
-      -- if `matcher` is not private, we mark it as `implicit_reducible` too
-      unless isPrivateName name do
-        setReducibilityStatus name .implicitReducible
       unless isSplitter do
         modifyEnv fun env => matcherExt.modifyState env fun s => s.insert key name
         addMatcherInfo name mi

src/Lean/Meta/Match/Rewrite.lean

@@ -17,7 +17,7 @@ namespace Lean.Meta
 
 /--
 Tries to rewrite the `ite`, `dite` or `cond` expression `e` with the hypothesis `hc`.
-If it fails, it returns a rewrite with `proof? := none` and unchanged expression.
+If it fails, it returns a rewrite with `proof? := none` and unchaged expression.
 -/
 def rwIfWith (hc : Expr) (e : Expr) : MetaM Simp.Result := do
   match_expr e with

src/Lean/Meta/Native.lean

@@ -22,9 +22,9 @@ of that computation as an axiom towards the logic.
 -/
 
 public inductive NativeEqTrueResult where
-  /-- The given expression `e` evaluates to true. `prf` is a proof of `e = true`. -/
+  /-- The given expression `e` evalutes to true. `prf` is a proof of `e = true`. -/
   | success (prf : Expr)
-  /-- The given expression `e` evaluates to false. -/
+  /-- The given expression `e` evalutes to false. -/
   | notTrue
 
 /--

src/Lean/Meta/SameCtorUtils.lean

@@ -14,7 +14,7 @@ This module contains utilities for dealing with equalities between constructor a
 in particular about which fields must be the same a-priori for the equality to type check.
 
 Users include (or will include) the injectivity theorems, the per-constructor no-confusion
-construction and deriving type classes like `BEq`, `DecidableEq` or `Ord`.
+construction and deriving type classes lik `BEq`, `DecidableEq` or `Ord`.
 -/
 
 namespace Lean.Meta

src/Lean/Meta/Sym.lean

@@ -25,7 +25,6 @@ public import Lean.Meta.Sym.Simp
 public import Lean.Meta.Sym.Util
 public import Lean.Meta.Sym.Eta
 public import Lean.Meta.Sym.Canon
-public import Lean.Meta.Sym.Arith
 public import Lean.Meta.Sym.Grind
 public import Lean.Meta.Sym.SynthInstance
 

src/Lean/Meta/Sym/AbstractS.lean

@@ -97,16 +97,4 @@ public def mkLambdaFVarsS (xs : Array Expr) (e : Expr) : SymM Expr := do
     let type ← abstractFVarsRange decl.type i xs
     mkLambdaS decl.userName decl.binderInfo type b
 
-/--
-Similar to `mkForallFVars`, but uses the more efficient `abstractFVars` and `abstractFVarsRange`,
-and makes the same assumption made by these functions.
--/
-public def mkForallFVarsS (xs : Array Expr) (e : Expr) : SymM Expr := do
-  let b ← abstractFVars e xs
-  xs.size.foldRevM (init := b) fun i _ b => do
-    let x := xs[i]
-    let decl ← x.fvarId!.getDecl
-    let type ← abstractFVarsRange decl.type i xs
-    mkForallS decl.userName decl.binderInfo type b
-
 end Lean.Meta.Sym

src/Lean/Meta/Sym/AlphaShareBuilder.lean

@@ -189,48 +189,4 @@ def mkAppS₄ (f a₁ a₂ a₃ a₄ : Expr) : m Expr := do
 def mkAppS₅ (f a₁ a₂ a₃ a₄ a₅ : Expr) : m Expr := do
   mkAppS (← mkAppS₄ f a₁ a₂ a₃ a₄) a₅
 
-def mkAppS₆ (f a₁ a₂ a₃ a₄ a₅ a₆ : Expr) : m Expr := do
-  mkAppS (← mkAppS₅ f a₁ a₂ a₃ a₄ a₅) a₆
-
-def mkAppS₇ (f a₁ a₂ a₃ a₄ a₅ a₆ a₇ : Expr) : m Expr := do
-  mkAppS (← mkAppS₆ f a₁ a₂ a₃ a₄ a₅ a₆) a₇
-
-def mkAppS₈ (f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ : Expr) : m Expr := do
-  mkAppS (← mkAppS₇ f a₁ a₂ a₃ a₄ a₅ a₆ a₇) a₈
-
-def mkAppS₉ (f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ : Expr) : m Expr := do
-  mkAppS (← mkAppS₈ f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈) a₉
-
-def mkAppS₁₀ (f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ a₁₀ : Expr) : m Expr := do
-  mkAppS (← mkAppS₉ f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉) a₁₀
-
-def mkAppS₁₁ (f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ a₁₀ a₁₁ : Expr) : m Expr := do
-  mkAppS (← mkAppS₁₀ f a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ a₁₀) a₁₁
-
-/-- `mkAppRangeS f i j #[a₀, ..., aᵢ, ..., aⱼ, ...]` ==> `f aᵢ ... aⱼ₋₁` with max sharing. -/
-partial def mkAppRangeS (f : Expr) (beginIdx endIdx : Nat) (args : Array Expr) : m Expr :=
-  go endIdx f beginIdx
-where
-  go (endIdx : Nat) (b : Expr) (i : Nat) : m Expr := do
-    if endIdx ≤ i then return b
-    else go endIdx (← mkAppS b args[i]!) (i + 1)
-
-/-- `mkAppNS f #[a₀, ..., aₙ]` constructs `f a₀ ... aₙ` with max sharing. -/
-def mkAppNS (f : Expr) (args : Array Expr) : m Expr :=
-  mkAppRangeS f 0 args.size args
-
-/-- `mkAppRevRangeS f b e revArgs` ==> `mkAppRev f (revArgs.extract b e)` with max sharing. -/
-partial def mkAppRevRangeS (f : Expr) (beginIdx endIdx : Nat) (revArgs : Array Expr) : m Expr :=
-  go revArgs beginIdx f endIdx
-where
-  go (revArgs : Array Expr) (start : Nat) (b : Expr) (i : Nat) : m Expr := do
-    if i ≤ start then return b
-    else
-      let i := i - 1
-      go revArgs start (← mkAppS b revArgs[i]!) i
-
-/-- Same as `mkAppS f args` but reversing `args`, with max sharing. -/
-def mkAppRevS (f : Expr) (revArgs : Array Expr) : m Expr :=
-  mkAppRevRangeS f 0 revArgs.size revArgs
-
 end Lean.Meta.Sym.Internal

src/Lean/Meta/Sym/Arith.lean

@@ -1,20 +0,0 @@
-/-
-Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-prelude
-public import Lean.Meta.Sym.Arith.Types
-public import Lean.Meta.Sym.Arith.EvalNum
-public import Lean.Meta.Sym.Arith.Classify
-public import Lean.Meta.Sym.Arith.MonadCanon
-public import Lean.Meta.Sym.Arith.MonadRing
-public import Lean.Meta.Sym.Arith.MonadSemiring
-public import Lean.Meta.Sym.Arith.MonadVar
-public import Lean.Meta.Sym.Arith.Functions
-public import Lean.Meta.Sym.Arith.Reify
-public import Lean.Meta.Sym.Arith.DenoteExpr
-public import Lean.Meta.Sym.Arith.ToExpr
-public import Lean.Meta.Sym.Arith.VarRename
-public import Lean.Meta.Sym.Arith.Poly

src/Lean/Meta/Sym/Arith/Classify.lean

@@ -1,143 +0,0 @@
-/-
-Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-prelude
-public import Lean.Meta.Sym.Arith.EvalNum
-import Lean.Meta.Sym.SynthInstance
-import Lean.Meta.Sym.Canon
-import Lean.Meta.DecLevel
-import Init.Grind.Ring
-public section
-
-namespace Lean.Meta.Sym.Arith
-
-/-!
-# Algebraic structure classification
-
-Detects the strongest algebraic structure available for a type and caches
-the classification in `Arith.State.typeClassify`. The detection order is:
-
-1. `Grind.CommRing` (includes `Field` check)
-2. `Grind.Ring` (non-commutative)
-3. `Grind.CommSemiring` (via `OfSemiring.Q` envelope)
-4. `Grind.Semiring` (non-commutative)
-
-Results (including failures) are cached in a single `PHashMap ExprPtr ClassifyResult`
-to avoid repeated synthesis attempts.
--/
-
-private def getIsCharInst? (u : Level) (type : Expr) (semiringInst : Expr) : SymM (Option (Expr × Nat)) := do
-  withNewMCtxDepth do
-    let n ← mkFreshExprMVar (mkConst ``Nat)
-    let charType := mkApp3 (mkConst ``Grind.IsCharP [u]) type semiringInst n
-    let some charInst ← Sym.synthInstance? charType | return none
-    let n ← instantiateMVars n
-    let some n ← evalNat? n | return none
-    return some (charInst, n)
-
-private def getNoZeroDivInst? (u : Level) (type : Expr) : SymM (Option Expr) := do
-  let natModuleType := mkApp (mkConst ``Grind.NatModule [u]) type
-  let some natModuleInst ← Sym.synthInstance? natModuleType | return none
-  let noZeroDivType := mkApp2 (mkConst ``Grind.NoNatZeroDivisors [u]) type natModuleInst
-  Sym.synthInstance? noZeroDivType
-
-/-- Try to classify `type` as a `CommRing`. Returns the ring id on success. -/
-private def tryCommRing? (type : Expr) : SymM (Option Nat) := do
-  let u ← getDecLevel type
-  let commRing := mkApp (mkConst ``Grind.CommRing [u]) type
-  let some commRingInst ← Sym.synthInstance? commRing | return none
-  let ringInst := mkApp2 (mkConst ``Grind.CommRing.toRing [u]) type commRingInst
-  let semiringInst := mkApp2 (mkConst ``Grind.Ring.toSemiring [u]) type ringInst
-  let commSemiringInst := mkApp2 (mkConst ``Grind.CommRing.toCommSemiring [u]) type semiringInst
-  let charInst? ← getIsCharInst? u type semiringInst
-  let noZeroDivInst? ← getNoZeroDivInst? u type
-  let fieldInst? ← Sym.synthInstance? <| mkApp (mkConst ``Grind.Field [u]) type
-  let semiringId? := none
-  let id := (← getArithState).rings.size
-  let ring : CommRing := {
-    id, semiringId?, type, u, semiringInst, ringInst, commSemiringInst,
-    commRingInst, charInst?, noZeroDivInst?, fieldInst?,
-  }
-  modifyArithState fun s => { s with rings := s.rings.push ring }
-  return some id
-
-/-- Try to classify `type` as a non-commutative `Ring`. -/
-private def tryNonCommRing? (type : Expr) : SymM (Option Nat) := do
-  let u ← getDecLevel type
-  let ring := mkApp (mkConst ``Grind.Ring [u]) type
-  let some ringInst ← Sym.synthInstance? ring | return none
-  let semiringInst := mkApp2 (mkConst ``Grind.Ring.toSemiring [u]) type ringInst
-  let charInst? ← getIsCharInst? u type semiringInst
-  let id := (← getArithState).ncRings.size
-  let ring : Ring := {
-    id, type, u, semiringInst, ringInst, charInst?
-  }
-  modifyArithState fun s => { s with ncRings := s.ncRings.push ring }
-  return some id
-
-/-- Helper function for `tryCommSemiring? -/
-private def tryCacheAndCommRing? (type : Expr) : SymM (Option Nat) := do
-  if let some result := (← getArithState).typeClassify.find? { expr := type } then
-    let .commRing id := result | return none
-    return id
-  let id? ← tryCommRing? type
-  let result := match id? with
-    | none => .none
-    | some id => .commRing id
-  modifyArithState fun s => { s with typeClassify := s.typeClassify.insert { expr := type } result }
-  return id?
-
-/-- Try to classify `type` as a `CommSemiring`. Creates the `OfSemiring.Q` envelope ring. -/
-private def tryCommSemiring? (type : Expr) : SymM (Option Nat) := do
-  let u ← getDecLevel type
-  let commSemiring := mkApp (mkConst ``Grind.CommSemiring [u]) type
-  let some commSemiringInst ← Sym.synthInstance? commSemiring | return none
-  let semiringInst := mkApp2 (mkConst ``Grind.CommSemiring.toSemiring [u]) type commSemiringInst
-  let q ← shareCommon (← Sym.canon (mkApp2 (mkConst ``Grind.Ring.OfSemiring.Q [u]) type semiringInst))
-  -- The envelope `Q` type must be classifiable as a CommRing.
-  let some ringId ← tryCacheAndCommRing? q
-    | reportIssue! "unexpected failure initializing ring{indentExpr q}"; return none
-  let id := (← getArithState).semirings.size
-  let semiring : CommSemiring := {
-    id, type, ringId, u, semiringInst, commSemiringInst
-  }
-  modifyArithState fun s => { s with semirings := s.semirings.push semiring }
-  -- Link the envelope ring back to this semiring
-  modifyArithState fun s =>
-    let rings := s.rings.modify ringId fun r => { r with semiringId? := some id }
-    { s with rings }
-  return some id
-
-/-- Try to classify `type` as a non-commutative `Semiring`. -/
-private def tryNonCommSemiring? (type : Expr) : SymM (Option Nat) := do
-  let u ← getDecLevel type
-  let semiring := mkApp (mkConst ``Grind.Semiring [u]) type
-  let some semiringInst ← Sym.synthInstance? semiring | return none
-  let id := (← getArithState).ncSemirings.size
-  let semiring : Semiring := { id, type, u, semiringInst }
-  modifyArithState fun s => { s with ncSemirings := s.ncSemirings.push semiring }
-  return some id
-
-/--
-Classify the algebraic structure of `type`, trying the strongest first:
-CommRing > Ring > CommSemiring > Semiring.
-Results are cached in `Arith.State.typeClassify`.
--/
-def classify? (type : Expr) : SymM ClassifyResult := do
-  if let some result := (← getArithState).typeClassify.find? { expr := type } then
-    return result
-  let result ← go
-  modifyArithState fun s => { s with typeClassify := s.typeClassify.insert { expr := type } result }
-  return result
-where
-  go : SymM ClassifyResult := do
-    if let some id ← tryCommRing? type then return .commRing id
-    if let some id ← tryNonCommRing? type then return .nonCommRing id
-    if let some id ← tryCommSemiring? type then return .commSemiring id
-    if let some id ← tryNonCommSemiring? type then return .nonCommSemiring id
-    return .none
-
-end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Arith/DenoteExpr.lean

@@ -1,93 +0,0 @@
-/-
-Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-prelude
-public import Lean.Meta.Sym.Arith.Functions
-public import Lean.Meta.Sym.Arith.MonadVar
-public section
-namespace Lean.Meta.Sym.Arith
-
-/-!
-# Denotation of reified expressions
-
-Converts reified `RingExpr`, `Poly`, `Mon`, `Power` back into Lean `Expr`s using
-the ring's cached operator functions and variable array.
--/
-
-variable [Monad m] [MonadError m] [MonadLiftT MetaM m] [MonadCanon m] [MonadRing m]
-
-/-- Convert an integer to a numeral expression in the ring. Negative values use `getNegFn`. -/
-def denoteNum (k : Int) : m Expr := do
-  let ring ← getRing
-  let n := mkRawNatLit k.natAbs
-  let ofNatInst ← if let some inst ← MonadCanon.synthInstance? (mkApp2 (mkConst ``OfNat [ring.u]) ring.type n) then
-    pure inst
-  else
-    pure <| mkApp3 (mkConst ``Grind.Semiring.ofNat [ring.u]) ring.type ring.semiringInst n
-  let e := mkApp3 (mkConst ``OfNat.ofNat [ring.u]) ring.type n ofNatInst
-  if k < 0 then
-    return mkApp (← getNegFn) e
-  else
-    return e
-
-/-- Denote a `Power` (variable raised to a power). -/
-def denotePower [MonadGetVar m] (pw : Power) : m Expr := do
-  let x ← getVar pw.x
-  if pw.k == 1 then
-    return x
-  else
-    return mkApp2 (← getPowFn) x (toExpr pw.k)
-
-/-- Denote a `Mon` (product of powers). -/
-def denoteMon [MonadGetVar m] (mn : Mon) : m Expr := do
-  match mn with
-  | .unit => denoteNum 1
-  | .mult pw mn => go mn (← denotePower pw)
-where
-  go (mn : Mon) (acc : Expr) : m Expr := do
-    match mn with
-    | .unit => return acc
-    | .mult pw mn => go mn (mkApp2 (← getMulFn) acc (← denotePower pw))
-
-/-- Denote a `Poly` (sum of coefficient × monomial terms). -/
-def denotePoly [MonadGetVar m] (p : Poly) : m Expr := do
-  match p with
-  | .num k => denoteNum k
-  | .add k mn p => go p (← denoteTerm k mn)
-where
-  denoteTerm (k : Int) (mn : Mon) : m Expr := do
-    if k == 1 then
-      denoteMon mn
-    else
-      return mkApp2 (← getMulFn) (← denoteNum k) (← denoteMon mn)
-
-  go (p : Poly) (acc : Expr) : m Expr := do
-    match p with
-    | .num 0 => return acc
-    | .num k => return mkApp2 (← getAddFn) acc (← denoteNum k)
-    | .add k mn p => go p (mkApp2 (← getAddFn) acc (← denoteTerm k mn))
-
-/-- Denote a `RingExpr` using a variable lookup function. -/
-@[specialize]
-private def denoteRingExprCore (getVarExpr : Nat → Expr) (e : RingExpr) : m Expr := do
-  go e
-where
-  go : RingExpr → m Expr
-  | .num k => denoteNum k
-  | .natCast k => return mkApp (← getNatCastFn) (mkNatLit k)
-  | .intCast k => return mkApp (← getIntCastFn) (mkIntLit k)
-  | .var x => return getVarExpr x
-  | .add a b => return mkApp2 (← getAddFn) (← go a) (← go b)
-  | .sub a b => return mkApp2 (← getSubFn) (← go a) (← go b)
-  | .mul a b => return mkApp2 (← getMulFn) (← go a) (← go b)
-  | .pow a k => return mkApp2 (← getPowFn) (← go a) (toExpr k)
-  | .neg a => return mkApp (← getNegFn) (← go a)
-
-/-- Denote a `RingExpr` using an explicit variable array. -/
-def denoteRingExpr (vars : Array Expr) (e : RingExpr) : m Expr := do
-  denoteRingExprCore (fun x => vars[x]!) e
-
-end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Arith/EvalNum.lean

@@ -1,90 +0,0 @@
-/-
-Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-prelude
-public import Lean.Meta.Sym.Arith.Types
-import Lean.Meta.Sym.LitValues
-import Lean.Meta.IntInstTesters
-import Lean.Meta.NatInstTesters
-public section
-
-namespace Lean.Meta.Sym.Arith
-
-/-!
-Functions for evaluating simple `Nat` and `Int` expressions that appear in type classes
-(e.g., `ToInt` and `IsCharP`). Using `whnf` for this purpose is too expensive and can
-exhaust the stack. We considered `evalExpr` as an alternative, but it introduces
-considerable overhead. We may use `evalExpr` as a fallback in the future.
--/
-
-def checkExp (k : Nat) : OptionT SymM Unit := do
-  let exp ← getExpThreshold
-  if k > exp then
-    reportIssue! "exponent {k} exceeds threshold for exponentiation `(exp := {exp})`"
-    failure
-
-/-
-**Note**: It is safe to use (the more efficient) structural instance tests here because
-`Sym.Canon` has already run.
--/
-open Structural in
-mutual
-private partial def evalNatCore (e : Expr) : OptionT SymM Nat := do
-  match_expr e with
-  | Nat.zero => return 0
-  | Nat.succ a => return (← evalNatCore a) + 1
-  | Int.toNat a => return (← evalIntCore a).toNat
-  | Int.natAbs a => return (← evalIntCore a).natAbs
-  | HAdd.hAdd _ _ _ inst a b => guard (← isInstHAddNat inst); return (← evalNatCore a) + (← evalNatCore b)
-  | HMul.hMul _ _ _ inst a b => guard (← isInstHMulNat inst); return (← evalNatCore a) * (← evalNatCore b)
-  | HSub.hSub _ _ _ inst a b => guard (← isInstHSubNat inst); return (← evalNatCore a) - (← evalNatCore b)
-  | HDiv.hDiv _ _ _ inst a b => guard (← isInstHDivNat inst); return (← evalNatCore a) / (← evalNatCore b)
-  | HMod.hMod _ _ _ inst a b => guard (← isInstHModNat inst); return (← evalNatCore a) % (← evalNatCore b)
-  | OfNat.ofNat _ _ _ =>
-    let some n := Sym.getNatValue? e |>.run | failure
-    return n
-  | HPow.hPow _ _ _ inst a k =>
-    guard (← isInstHPowNat inst)
-    let k ← evalNatCore k
-    checkExp k
-    let a ← evalNatCore a
-    return a ^ k
-  | _ => failure
-
-private partial def evalIntCore (e : Expr) : OptionT SymM Int := do
-  match_expr e with
-  | Neg.neg _ i a => guard (← isInstNegInt i); return - (← evalIntCore a)
-  | HAdd.hAdd _ _ _ i a b => guard (← isInstHAddInt i); return (← evalIntCore a) + (← evalIntCore b)
-  | HSub.hSub _ _ _ i a b => guard (← isInstHSubInt i); return (← evalIntCore a) - (← evalIntCore b)
-  | HMul.hMul _ _ _ i a b => guard (← isInstHMulInt i); return (← evalIntCore a) * (← evalIntCore b)
-  | HDiv.hDiv _ _ _ i a b => guard (← isInstHDivInt i); return (← evalIntCore a) / (← evalIntCore b)
-  | HMod.hMod _ _ _ i a b => guard (← isInstHModInt i); return (← evalIntCore a) % (← evalIntCore b)
-  | HPow.hPow _ _ _ i a k =>
-    guard (← isInstHPowInt i)
-    let a ← evalIntCore a
-    let k ← evalNatCore k
-    checkExp k
-    return a ^ k
-  | OfNat.ofNat _ _ _ =>
-    let some n := Sym.getIntValue? e |>.run | failure
-    return n
-  | NatCast.natCast _ i a =>
-    let_expr instNatCastInt ← i | failure
-    return (← evalNatCore a)
-  | Nat.cast _ i a =>
-    let_expr instNatCastInt ← i | failure
-    return (← evalNatCore a)
-  | _ => failure
-
-end
-
-def evalNat? (e : Expr) : SymM (Option Nat) :=
-  evalNatCore e |>.run
-
-def evalInt? (e : Expr) : SymM (Option Int) :=
-  evalIntCore e |>.run
-
-end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Arith/Functions.lean

@@ -1,171 +0,0 @@
-/-
-Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-prelude
-public import Lean.Meta.Sym.Arith.MonadRing
-public import Lean.Meta.Sym.Arith.MonadSemiring
-public section
-namespace Lean.Meta.Sym.Arith
-
-/-!
-# Cached function expressions for arithmetic operators
-
-Synthesizes and caches the canonical Lean expressions for arithmetic operators
-(`+`, `*`, `-`, `^`, `intCast`, `natCast`, etc.). These cached expressions are used
-during reification to validate instances via pointer equality (`isSameExpr`).
-
-Each getter checks the cache field first. On a miss, it synthesizes the instance,
-verifies it against the expected instance from the ring structure using `isDefEqI`,
-canonicalizes the result via `canonExpr`, and stores it.
--/
-
-variable [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m]
-
-private def checkInst (declName : Name) (inst inst' : Expr) : MetaM Unit := do
-  unless (← withReducibleAndInstances <| isDefEq inst inst') do
-    throwError "error while initializing arithmetic operators:\ninstance for `{declName}` {indentExpr inst}\nis not definitionally equal to the expected one {indentExpr inst'}\nwhen only reducible definitions and instances are reduced"
-
-private def mkUnaryFn (type : Expr) (u : Level) (instDeclName : Name) (declName : Name) (expectedInst : Expr) : m Expr := do
-  let inst ← MonadCanon.synthInstance <| mkApp (mkConst instDeclName [u]) type
-  checkInst declName inst expectedInst
-  canonExpr <| mkApp2 (mkConst declName [u]) type inst
-
-private def mkBinHomoFn (type : Expr) (u : Level) (instDeclName : Name) (declName : Name) (expectedInst : Expr) : m Expr := do
-  let inst ← MonadCanon.synthInstance <| mkApp3 (mkConst instDeclName [u, u, u]) type type type
-  checkInst declName inst expectedInst
-  canonExpr <| mkApp4 (mkConst declName [u, u, u]) type type type inst
-
-private def mkPowFn (u : Level) (type : Expr) (semiringInst : Expr) : m Expr := do
-  let inst ← MonadCanon.synthInstance <| mkApp3 (mkConst ``HPow [u, 0, u]) type Nat.mkType type
-  let inst' := mkApp2 (mkConst ``Grind.Semiring.npow [u]) type semiringInst
-  checkInst ``HPow.hPow inst inst'
-  canonExpr <| mkApp4 (mkConst ``HPow.hPow [u, 0, u]) type Nat.mkType type inst
-
-private def mkNatCastFn (u : Level) (type : Expr) (semiringInst : Expr) : m Expr := do
-  let inst' := mkApp2 (mkConst ``Grind.Semiring.natCast [u]) type semiringInst
-  let instType := mkApp (mkConst ``NatCast [u]) type
-  -- Note: `Semiring.natCast` is not a global instance, so `NatCast α` may not be available.
-  -- When present, verify defeq; otherwise fall back to the semiring field.
-  let inst ← match (← MonadCanon.synthInstance? instType) with
-  | none => pure inst'
-  | some inst => checkInst ``NatCast.natCast inst inst'; pure inst
-  canonExpr <| mkApp2 (mkConst ``NatCast.natCast [u]) type inst
-
-section RingFns
-variable [MonadRing m]
-
-def getAddFn : m Expr := do
-  let ring ← getRing
-  if let some addFn := ring.addFn? then return addFn
-  let expectedInst := mkApp2 (mkConst ``instHAdd [ring.u]) ring.type <| mkApp2 (mkConst ``Grind.Semiring.toAdd [ring.u]) ring.type ring.semiringInst
-  let addFn ← mkBinHomoFn ring.type ring.u ``HAdd ``HAdd.hAdd expectedInst
-  modifyRing fun s => { s with addFn? := some addFn }
-  return addFn
-
-def getMulFn : m Expr := do
-  let ring ← getRing
-  if let some mulFn := ring.mulFn? then return mulFn
-  let expectedInst := mkApp2 (mkConst ``instHMul [ring.u]) ring.type <| mkApp2 (mkConst ``Grind.Semiring.toMul [ring.u]) ring.type ring.semiringInst
-  let mulFn ← mkBinHomoFn ring.type ring.u ``HMul ``HMul.hMul expectedInst
-  modifyRing fun s => { s with mulFn? := some mulFn }
-  return mulFn
-
-def getSubFn : m Expr := do
-  let ring ← getRing
-  if let some subFn := ring.subFn? then return subFn
-  let expectedInst := mkApp2 (mkConst ``instHSub [ring.u]) ring.type <| mkApp2 (mkConst ``Grind.Ring.toSub [ring.u]) ring.type ring.ringInst
-  let subFn ← mkBinHomoFn ring.type ring.u ``HSub ``HSub.hSub expectedInst
-  modifyRing fun s => { s with subFn? := some subFn }
-  return subFn
-
-def getNegFn : m Expr := do
-  let ring ← getRing
-  if let some negFn := ring.negFn? then return negFn
-  let expectedInst := mkApp2 (mkConst ``Grind.Ring.toNeg [ring.u]) ring.type ring.ringInst
-  let negFn ← mkUnaryFn ring.type ring.u ``Neg ``Neg.neg expectedInst
-  modifyRing fun s => { s with negFn? := some negFn }
-  return negFn
-
-def getPowFn : m Expr := do
-  let ring ← getRing
-  if let some powFn := ring.powFn? then return powFn
-  let powFn ← mkPowFn ring.u ring.type ring.semiringInst
-  modifyRing fun s => { s with powFn? := some powFn }
-  return powFn
-
-def getIntCastFn : m Expr := do
-  let ring ← getRing
-  if let some intCastFn := ring.intCastFn? then return intCastFn
-  let inst' := mkApp2 (mkConst ``Grind.Ring.intCast [ring.u]) ring.type ring.ringInst
-  let instType := mkApp (mkConst ``IntCast [ring.u]) ring.type
-  -- Note: `Ring.intCast` is not a global instance. Same pattern as `mkNatCastFn`.
-  let inst ← match (← MonadCanon.synthInstance? instType) with
-    | none => pure inst'
-    | some inst => checkInst ``Int.cast inst inst'; pure inst
-  let intCastFn ← canonExpr <| mkApp2 (mkConst ``IntCast.intCast [ring.u]) ring.type inst
-  modifyRing fun s => { s with intCastFn? := some intCastFn }
-  return intCastFn
-
-def getNatCastFn : m Expr := do
-  let ring ← getRing
-  if let some natCastFn := ring.natCastFn? then return natCastFn
-  let natCastFn ← mkNatCastFn ring.u ring.type ring.semiringInst
-  modifyRing fun s => { s with natCastFn? := some natCastFn }
-  return natCastFn
-
-end RingFns
-
-section CommRingFns
-variable [MonadCommRing m]
-
-def getInvFn : m Expr := do
-  let ring ← getCommRing
-  let some fieldInst := ring.fieldInst?
-    | throwError "internal error: type is not a field{indentExpr ring.type}"
-  if let some invFn := ring.invFn? then return invFn
-  let expectedInst := mkApp2 (mkConst ``Grind.Field.toInv [ring.u]) ring.type fieldInst
-  let invFn ← mkUnaryFn ring.type ring.u ``Inv ``Inv.inv expectedInst
-  modifyCommRing fun s => { s with invFn? := some invFn }
-  return invFn
-
-end CommRingFns
-
-section SemiringFns
-variable [MonadSemiring m]
-
-def getAddFn' : m Expr := do
-  let sr ← getSemiring
-  if let some addFn := sr.addFn? then return addFn
-  let expectedInst := mkApp2 (mkConst ``instHAdd [sr.u]) sr.type <| mkApp2 (mkConst ``Grind.Semiring.toAdd [sr.u]) sr.type sr.semiringInst
-  let addFn ← mkBinHomoFn sr.type sr.u ``HAdd ``HAdd.hAdd expectedInst
-  modifySemiring fun s => { s with addFn? := some addFn }
-  return addFn
-
-def getMulFn' : m Expr := do
-  let sr ← getSemiring
-  if let some mulFn := sr.mulFn? then return mulFn
-  let expectedInst := mkApp2 (mkConst ``instHMul [sr.u]) sr.type <| mkApp2 (mkConst ``Grind.Semiring.toMul [sr.u]) sr.type sr.semiringInst
-  let mulFn ← mkBinHomoFn sr.type sr.u ``HMul ``HMul.hMul expectedInst
-  modifySemiring fun s => { s with mulFn? := some mulFn }
-  return mulFn
-
-def getPowFn' : m Expr := do
-  let sr ← getSemiring
-  if let some powFn := sr.powFn? then return powFn
-  let powFn ← mkPowFn sr.u sr.type sr.semiringInst
-  modifySemiring fun s => { s with powFn? := some powFn }
-  return powFn
-
-def getNatCastFn' : m Expr := do
-  let sr ← getSemiring
-  if let some natCastFn := sr.natCastFn? then return natCastFn
-  let natCastFn ← mkNatCastFn sr.u sr.type sr.semiringInst
-  modifySemiring fun s => { s with natCastFn? := some natCastFn }
-  return natCastFn
-
-end SemiringFns
-
-end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Arith/MonadRing.lean

@@ -1,39 +0,0 @@
-/-
-Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-prelude
-public import Lean.Meta.Sym.Arith.MonadCanon
-public section
-namespace Lean.Meta.Sym.Arith
-
-class MonadRing (m : Type → Type) where
-  getRing : m Ring
-  modifyRing : (Ring → Ring) → m Unit
-
-export MonadRing (getRing modifyRing)
-
-@[always_inline]
-instance (m n) [MonadLift m n] [MonadRing m] : MonadRing n where
-  getRing    := liftM (getRing : m Ring)
-  modifyRing f := liftM (modifyRing f : m Unit)
-
-class MonadCommRing (m : Type → Type) where
-  getCommRing : m CommRing
-  modifyCommRing : (CommRing → CommRing) → m Unit
-
-export MonadCommRing (getCommRing modifyCommRing)
-
-@[always_inline]
-instance (m n) [MonadLift m n] [MonadCommRing m] : MonadCommRing n where
-  getCommRing      := liftM (getCommRing : m CommRing)
-  modifyCommRing f := liftM (modifyCommRing f : m Unit)
-
-@[always_inline]
-instance (m) [Monad m] [MonadCommRing m] : MonadRing m where
-  getRing := return (← getCommRing).toRing
-  modifyRing f := modifyCommRing fun s => { s with toRing := f s.toRing }
-
-end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Arith/MonadSemiring.lean

@@ -1,39 +0,0 @@
-/-
-Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-prelude
-public import Lean.Meta.Sym.Arith.MonadCanon
-public section
-namespace Lean.Meta.Sym.Arith
-
-class MonadSemiring (m : Type → Type) where
-  getSemiring : m Semiring
-  modifySemiring : (Semiring → Semiring) → m Unit
-
-export MonadSemiring (getSemiring modifySemiring)
-
-@[always_inline]
-instance (m n) [MonadLift m n] [MonadSemiring m] : MonadSemiring n where
-  getSemiring    := liftM (getSemiring : m Semiring)
-  modifySemiring f := liftM (modifySemiring f : m Unit)
-
-class MonadCommSemiring (m : Type → Type) where
-  getCommSemiring : m CommSemiring
-  modifyCommSemiring : (CommSemiring → CommSemiring) → m Unit
-
-export MonadCommSemiring (getCommSemiring modifyCommSemiring)
-
-@[always_inline]
-instance (m n) [MonadLift m n] [MonadCommSemiring m] : MonadCommSemiring n where
-  getCommSemiring      := liftM (getCommSemiring : m CommSemiring)
-  modifyCommSemiring f := liftM (modifyCommSemiring f : m Unit)
-
-@[always_inline]
-instance (m) [Monad m] [MonadCommSemiring m] : MonadSemiring m where
-  getSemiring := return (← getCommSemiring).toSemiring
-  modifySemiring f := modifyCommSemiring fun s => { s with toSemiring := f s.toSemiring }
-
-end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Arith/MonadVar.lean

@@ -1,32 +0,0 @@
-/-
-Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-prelude
-public import Lean.Meta.Sym.Arith.Types
-public section
-namespace Lean.Meta.Sym.Arith
-
-/-- Read a variable's Lean expression by index. Used by `DenoteExpr` and diagnostics (PP). -/
-class MonadGetVar (m : Type → Type) where
-  getVar : Var → m Expr
-
-export MonadGetVar (getVar)
-
-@[always_inline]
-instance (m n) [MonadLift m n] [MonadGetVar m] : MonadGetVar n where
-  getVar x := liftM (getVar x : m Expr)
-
-/-- Create or lookup a variable for a Lean expression. Used by reification. -/
-class MonadMkVar (m : Type → Type) where
-  mkVar : Expr → m Var
-
-export MonadMkVar (mkVar)
-
-@[always_inline]
-instance (m n) [MonadLift m n] [MonadMkVar m] : MonadMkVar n where
-  mkVar e := liftM (mkVar e : m Var)
-
-end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Arith/Reify.lean

@@ -1,205 +0,0 @@
-/-
-Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-prelude
-public import Lean.Meta.Sym.Arith.Functions
-public import Lean.Meta.Sym.Arith.MonadVar
-public import Lean.Meta.Sym.LitValues
-public section
-namespace Lean.Meta.Sym.Arith
-open Sym.Arith (MonadCanon)
-
-/-!
-# Reification of arithmetic expressions
-
-Converts Lean expressions into `CommRing.Expr` (ring) or `CommSemiring.Expr`
-(semiring) for reflection-based normalization.
-
-Instance validation uses pointer equality (`isSameExpr`) against cached function
-expressions from `Functions.lean`.
-
-## Differences from grind's `Reify.lean`
-
-- Uses `MonadMkVar` for variable creation instead of grind's `internalize` + `mkVarCore`
-- Uses `Sym.getNatValue?`/`Sym.getIntValue?` (pure) instead of `MetaM` versions
-- No `MonadSetTermId` — term-to-ring-id tracking is grind-specific
--/
-
-section RingReify
-
-variable [MonadLiftT SymM m] [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] [MonadMkVar m]
-
-def isAddInst (inst : Expr) : m Bool :=
-  return isSameExpr (← getAddFn).appArg! inst
-def isMulInst (inst : Expr) : m Bool :=
-  return isSameExpr (← getMulFn).appArg! inst
-def isSubInst (inst : Expr) : m Bool :=
-  return isSameExpr (← getSubFn).appArg! inst
-def isNegInst (inst : Expr) : m Bool :=
-  return isSameExpr (← getNegFn).appArg! inst
-def isPowInst (inst : Expr) : m Bool :=
-  return isSameExpr (← getPowFn).appArg! inst
-def isIntCastInst (inst : Expr) : m Bool :=
-  return isSameExpr (← getIntCastFn).appArg! inst
-def isNatCastInst (inst : Expr) : m Bool :=
-  return isSameExpr (← getNatCastFn).appArg! inst
-
-private def reportRingAppIssue [MonadLiftT SymM m] (e : Expr) : m Unit := do
-  reportIssue! "ring term with unexpected instance{indentExpr e}"
-
-/--
-Converts a Lean expression `e` into a `RingExpr`.
-
-If `skipVar` is `true`, returns `none` if `e` is not an interpreted ring term
-(used for equalities/disequalities). If `false`, treats non-interpreted terms
-as variables (used for inequalities).
--/
-partial def reifyRing? (e : Expr) (skipVar : Bool := true) : m (Option RingExpr) := do
-  let toVar (e : Expr) : m RingExpr := do
-    return .var (← mkVar e)
-  let asVar (e : Expr) : m RingExpr := do
-    reportRingAppIssue e
-    return .var (← mkVar e)
-  let rec go (e : Expr) : m RingExpr := do
-    match_expr e with
-    | HAdd.hAdd _ _ _ i a b =>
-      if (← isAddInst i) then return .add (← go a) (← go b) else asVar e
-    | HMul.hMul _ _ _ i a b =>
-      if (← isMulInst i) then return .mul (← go a) (← go b) else asVar e
-    | HSub.hSub _ _ _ i a b =>
-      if (← isSubInst i) then return .sub (← go a) (← go b) else asVar e
-    | HPow.hPow _ _ _ i a b =>
-      let some k := Sym.getNatValue? b |>.run | toVar e
-      if (← isPowInst i) then return .pow (← go a) k else asVar e
-    | Neg.neg _ i a =>
-      if (← isNegInst i) then return .neg (← go a) else asVar e
-    | IntCast.intCast _ i a =>
-      if (← isIntCastInst i) then
-        let some k := Sym.getIntValue? a |>.run | toVar e
-        return .intCast k
-      else
-        asVar e
-    | NatCast.natCast _ i a =>
-      if (← isNatCastInst i) then
-        let some k := Sym.getNatValue? a |>.run | toVar e
-        return .natCast k
-      else
-        asVar e
-    | OfNat.ofNat _ n _ =>
-      /-
-      **Note**: We extract `n` directly as a raw nat literal. The grind version uses `MetaM`'s
-      `getNatValue?` which handles multiple encodings (raw literals, nested `OfNat`, etc.).
-      In `SymM`, we assume terms have been canonicalized by `Sym.canon` before reification,
-      so `OfNat.ofNat _ n _` always has a raw nat literal at position 1.
-      -/
-      let .lit (.natVal k) := n | toVar e
-      return .num k
-    | BitVec.ofNat _ n =>
-      let .lit (.natVal k) := n | toVar e
-      return .num k
-    | _ => toVar e
-  let toTopVar (e : Expr) : m (Option RingExpr) := do
-    if skipVar then
-      return none
-    else
-      return some (← toVar e)
-  let asTopVar (e : Expr) : m (Option RingExpr) := do
-    reportRingAppIssue e
-    toTopVar e
-  match_expr e with
-  | HAdd.hAdd _ _ _ i a b =>
-    if (← isAddInst i) then return some (.add (← go a) (← go b)) else asTopVar e
-  | HMul.hMul _ _ _ i a b =>
-    if (← isMulInst i) then return some (.mul (← go a) (← go b)) else asTopVar e
-  | HSub.hSub _ _ _ i a b =>
-    if (← isSubInst i) then return some (.sub (← go a) (← go b)) else asTopVar e
-  | HPow.hPow _ _ _ i a b =>
-    let some k := Sym.getNatValue? b |>.run | asTopVar e
-    if (← isPowInst i) then return some (.pow (← go a) k) else asTopVar e
-  | Neg.neg _ i a =>
-    if (← isNegInst i) then return some (.neg (← go a)) else asTopVar e
-  | IntCast.intCast _ i a =>
-    if (← isIntCastInst i) then
-      let some k := Sym.getIntValue? a |>.run | toTopVar e
-      return some (.intCast k)
-    else
-      asTopVar e
-  | NatCast.natCast _ i a =>
-    if (← isNatCastInst i) then
-      let some k := Sym.getNatValue? a |>.run | toTopVar e
-      return some (.natCast k)
-    else
-      asTopVar e
-  | OfNat.ofNat _ n _ =>
-    let .lit (.natVal k) := n | asTopVar e
-    return some (.num k)
-  | _ => toTopVar e
-
-end RingReify
-
-section SemiringReify
-
-variable [MonadLiftT SymM m] [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadSemiring m] [MonadMkVar m]
-
-private def reportSemiringAppIssue [MonadLiftT SymM m] (e : Expr) : m Unit := do
-  reportIssue! "semiring term with unexpected instance{indentExpr e}"
-
-/--
-Converts a Lean expression `e` into a `SemiringExpr`.
-Only recognizes `add`, `mul`, `pow`, `natCast`, and numerals (no `sub`, `neg`, `intCast`).
--/
-partial def reifySemiring? (e : Expr) : m (Option SemiringExpr) := do
-  let toVar (e : Expr) : m SemiringExpr := do
-    return .var (← mkVar e)
-  let asVar (e : Expr) : m SemiringExpr := do
-    reportSemiringAppIssue e
-    return .var (← mkVar e)
-  let rec go (e : Expr) : m SemiringExpr := do
-    match_expr e with
-    | HAdd.hAdd _ _ _ i a b =>
-      if isSameExpr (← getAddFn').appArg! i then return .add (← go a) (← go b) else asVar e
-    | HMul.hMul _ _ _ i a b =>
-      if isSameExpr (← getMulFn').appArg! i then return .mul (← go a) (← go b) else asVar e
-    | HPow.hPow _ _ _ i a b =>
-      let some k := Sym.getNatValue? b |>.run | toVar e
-      if isSameExpr (← getPowFn').appArg! i then return .pow (← go a) k else asVar e
-    | NatCast.natCast _ i a =>
-      if isSameExpr (← getNatCastFn').appArg! i then
-        let some k := Sym.getNatValue? a |>.run | toVar e
-        return .num k
-      else
-        asVar e
-    | OfNat.ofNat _ n _ =>
-      let .lit (.natVal k) := n | toVar e
-      return .num k
-    | _ => toVar e
-  let toTopVar (e : Expr) : m (Option SemiringExpr) := do
-    return some (← toVar e)
-  let asTopVar (e : Expr) : m (Option SemiringExpr) := do
-    reportSemiringAppIssue e
-    toTopVar e
-  match_expr e with
-  | HAdd.hAdd _ _ _ i a b =>
-    if isSameExpr (← getAddFn').appArg! i then return some (.add (← go a) (← go b)) else asTopVar e
-  | HMul.hMul _ _ _ i a b =>
-    if isSameExpr (← getMulFn').appArg! i then return some (.mul (← go a) (← go b)) else asTopVar e
-  | HPow.hPow _ _ _ i a b =>
-    let some k := Sym.getNatValue? b |>.run | return none
-    if isSameExpr (← getPowFn').appArg! i then return some (.pow (← go a) k) else asTopVar e
-  | NatCast.natCast _ i a =>
-    if isSameExpr (← getNatCastFn').appArg! i then
-      let some k := Sym.getNatValue? a |>.run | toTopVar e
-      return some (.num k)
-    else
-      asTopVar e
-  | OfNat.ofNat _ n _ =>
-    let .lit (.natVal k) := n | asTopVar e
-    return some (.num k)
-  | _ => toTopVar e
-
-end SemiringReify
-
-end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Arith/Types.lean

@@ -1,137 +0,0 @@
-/-
-Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-prelude
-public import Init.Grind.Ring.CommSemiringAdapter
-public import Lean.Meta.Sym.SymM
-public section
-
-namespace Lean.Meta.Sym.Arith
-export Lean.Grind.CommRing (Var Power Mon Poly)
-abbrev RingExpr := Grind.CommRing.Expr
-/-
-**Note**: recall that we use ring expressions to represent semiring expressions,
-and ignore non-applicable constructors.
--/
-abbrev SemiringExpr := Grind.CommRing.Expr
-
-/-- Classification state for a type with a `Semiring` instance. -/
-structure Semiring where
-  id             : Nat
-  type           : Expr
-  /-- Cached `getDecLevel type` -/
-  u              : Level
-  /-- `Semiring` instance for `type` -/
-  semiringInst   : Expr
-  addFn?         : Option Expr := none
-  mulFn?         : Option Expr := none
-  powFn?         : Option Expr := none
-  natCastFn?     : Option Expr := none
-  deriving Inhabited
-
-/-- Classification state for a type with a `Ring` instance. -/
-structure Ring where
-  id             : Nat
-  type           : Expr
-  /-- Cached `getDecLevel type` -/
-  u              : Level
-  /-- `Ring` instance for `type` -/
-  ringInst       : Expr
-  /-- `Semiring` instance for `type` -/
-  semiringInst   : Expr
-  /-- `IsCharP` instance for `type` if available. -/
-  charInst?      : Option (Expr × Nat)
-  addFn?         : Option Expr := none
-  mulFn?         : Option Expr := none
-  subFn?         : Option Expr := none
-  negFn?         : Option Expr := none
-  powFn?         : Option Expr := none
-  intCastFn?     : Option Expr := none
-  natCastFn?     : Option Expr := none
-  one?           : Option Expr := none
-  deriving Inhabited
-
-/-- Classification state for a type with a `CommRing` instance. -/
-structure CommRing extends Ring where
-  /-- Inverse function if `fieldInst?` is `some inst` -/
-  invFn?             : Option Expr := none
-  /--
-  If this is a `OfSemiring.Q α` ring, this field contains the
-  `semiringId` for `α`.
-  -/
-  semiringId?        : Option Nat
-  /-- `CommSemiring` instance for `type` -/
-  commSemiringInst   : Expr
-  /-- `CommRing` instance for `type` -/
-  commRingInst       : Expr
-  /-- `NoNatZeroDivisors` instance for `type` if available. -/
-  noZeroDivInst?     : Option Expr
-  /-- `Field` instance for `type` if available. -/
-  fieldInst?         : Option Expr
-  deriving Inhabited
-
-/--
-Classification state for a type with a `CommSemiring` instance.
-Recall that `CommSemiring` types are normalized using the `OfSemiring.Q` envelope.
--/
-structure CommSemiring extends Semiring where
-  /-- Id of the envelope ring `OfSemiring.Q type` -/
-  ringId             : Nat
-  /-- `CommSemiring` instance for `type` -/
-  commSemiringInst   : Expr
-  /-- `AddRightCancel` instance for `type` if available. -/
-  addRightCancelInst? : Option (Option Expr) := none
-  toQFn?             : Option Expr := none
-  deriving Inhabited
-
-/-- Result of classifying a type's algebraic structure. -/
-inductive ClassifyResult where
-  | commRing (id : Nat)
-  | nonCommRing (id : Nat)
-  | commSemiring (id : Nat)
-  | nonCommSemiring (id : Nat)
-  | /-- No algebraic structure found. -/ none
-  deriving Inhabited
-
-/-- Arith type classification state, stored as a `SymExtension`. -/
-structure State where
-  /-- Exponent threshold for `HPow` evaluation. -/
-  exp            : Nat := 8
-  /-- Commutative rings. -/
-  rings          : Array CommRing := {}
-  /-- Commutative semirings. -/
-  semirings      : Array CommSemiring := {}
-  /-- Non-commutative rings. -/
-  ncRings        : Array Ring := {}
-  /-- Non-commutative semirings. -/
-  ncSemirings    : Array Semiring := {}
-  /-- Mapping from types to their classification result. Caches failures as `.none`. -/
-  typeClassify   : PHashMap ExprPtr ClassifyResult := {}
-  deriving Inhabited
-
-builtin_initialize arithExt : SymExtension State ← registerSymExtension (return {})
-
-def getArithState : SymM State :=
-  arithExt.getState
-
-@[inline] def modifyArithState (f : State → State) : SymM Unit :=
-  arithExt.modifyState f
-
-/-- Get the exponent threshold. -/
-def getExpThreshold : SymM Nat :=
-  return (← getArithState).exp
-
-/-- Set the exponent threshold. -/
-def setExpThreshold (exp : Nat) : SymM Unit :=
-  modifyArithState fun s => { s with exp }
-
-/-- Run `k` with a temporary exponent threshold. -/
-def withExpThreshold (exp : Nat) (k : SymM α) : SymM α := do
-  let oldExp := (← getArithState).exp
-  setExpThreshold exp
-  try k finally setExpThreshold oldExp
-
-end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Canon.lean

@@ -24,19 +24,10 @@ builtin_initialize registerTraceClass `sym.debug.canon
 
 Canonicalizes expressions by normalizing types and instances. At the top level, it traverses
 applications, foralls, lambdas, and let-bindings, classifying each argument as a type, instance,
-implicit, or value using `shouldCanon`. Targeted reductions (projection, match/ite/cond, Nat
-arithmetic) are applied to all positions; instances are re-synthesized.
+implicit, or value using `shouldCanon`. Values are recursively visited but not normalized.
+Types and instances receive targeted reductions.
 
-**Note about types:** `grind` is not built for reasoning about types that are not propositions.
-We assume that definitionally equal types will be structurally identical after we apply the
-canonicalizer. We also erase most of the subsingleton markers occurring inside types.
-
-## Reductions
-
-It also normalizes expressions using the following reductions. We can view it as a cheap/custom `dsimp`.
-We used to reduce only terms inside types, but it restricted important normalizations that were important
-when, for example, a term had a forward dependency. That is, the term is not directly in a type, but
-there is a type that depends on it.
+## Reductions (applied only in type positions)
 
 - **Eta**: `fun x => f x` → `f`
 - **Projection**: `⟨a, b⟩.1` → `a` (structure projections, not class projections)
@@ -44,30 +35,11 @@ there is a type that depends on it.
 - **Nat arithmetic**: ground evaluation (`2 + 1` → `3`) and offset normalization
   (`n.succ + 1` → `n + 2`)
 
-**Note**: Eta is applied only if the lambda is occurring inside of a type. For lambdas occurring
-in non type positions, we want to leverage the support in `grind` for lambda-expressions.
-
 ## Instance canonicalization
 
 Instances are re-synthesized via `synthInstance`. The instance type is first normalized
 using the type-level reductions above, so that `OfNat (Fin (2+1)) 0` and `OfNat (Fin 3) 0`
-produce the same canonical instance. Two special cases:
-
-- **`Decidable` instances** (`Grind.nestedDecidable`): the proposition is recursively
-  canonicalized, then the `Decidable` instance is re-synthesized. If resynthesis fails,
-  the original instance is kept (users often provide these via `haveI`).
-  A `checkDefEqInst` guard is required because structurally different `Decidable` instances
-  are not necessarily definitionally equal.
-
-- **Propositional instances** (`Grind.nestedProof`): the proposition is recursively
-  canonicalized, then the proof is re-synthesized. If resynthesis fails, the original
-  proof is kept. No definitional-equality check is needed thanks to proof irrelevance.
-
-In both cases, resynthesis failure is silent — the original instance or proof is kept.
-Ideally we would report an issue when resynthesis fails inside a type (where structural
-agreement matters most), but in practice users provide non-synthesizable instances via `haveI`,
-and these instances propagate into types through forward dependencies. Reporting failures
-for such instances produces noise that obscures real issues.
+produce the same canonical instance.
 
 ## Two caches
 
@@ -241,7 +213,7 @@ def checkDefEqInst (e : Expr) (inst : Expr) : SymM Expr := do
     return e
   return inst
 
-/-- Canonicalize `e`. Applies targeted reductions and re-synthesizes instances. -/
+/-- Canonicalize `e`. Applies targeted reductions in type positions; recursively visits value positions. -/
 partial def canon (e : Expr) : CanonM Expr := do
   match e with
   | .forallE ..    => withCaching e <| canonForall #[] e
@@ -274,91 +246,23 @@ where
     else
       withReader (fun ctx => { ctx with insideType := true }) <| canon e
 
-  /--
-  Canonicalize `e : type` where `e` is an instance by trying to resynthesize `type`.
-  If `report` is `true`, we report an issue when the instance cannot be resynthesized.
-  -/
-  canonInstCore (e : Expr) (type : Expr) (report := true) : CanonM Expr := do
-    let some inst ← Sym.synthInstance? type |
-      if report then
-        reportIssue! "failed to canonicalize instance{indentExpr e}\nfailed to synthesize{indentExpr type}"
-      return e
-    checkDefEqInst e inst
-
-  /--
-  Canonicalize an instance by trying to resynthesize it without caching.
-  Recall that we have special support for `Decidable` and propositional instances.
-  -/
-  canonInst' (e : Expr) (report := true) : CanonM Expr := do
-    /-
-    We normalize the type to make sure `OfNat (Fin (2+1)) 1` and `OfNat (Fin 3) 1` will produce
-    the same instances.
-    -/
-    let type ← inferType e
-    let type' ← canonInsideType' type
-    canonInstCore e type' report
-
-  /-- `withCaching` + `canonInst'` -/
-  canonInst (e : Expr) (report := true) : CanonM Expr := withCaching e do
-    canonInst' e report
-
-  /--
-  Canonicalize a proposition that is also a term instance.
-  Given a term `e` of the form `@Grind.nestedProof prop h`, where `g` is the constant `Grind.nestedProof`,
-  we canonicalize it as follows:
-  1- We recursively canonicalize the proposition `prop`.
-  2- Try to resynthesize the instance, but keep the original one in case of failure since users often
-  provide them using `haveI`.
-  -/
-  canonInstProp (g : Expr) (prop : Expr) (h : Expr) (e : Expr) : CanonM Expr := withCaching e do
-    let prop' ← canon prop
-    if (← read).insideType then
-      /- We suppress reporting here because `haveI`-provided instances propagate into types
-         through forward dependencies, and reporting them produces noise. See module doc. -/
-      canonInstCore h prop' (report := false)
+  canonInst (e : Expr) : CanonM Expr := do
+    if let some inst := (← get).canon.cacheInsts.get? e then
+      checkDefEqInst e inst
     else
       /-
-      **Note**: We try to resynthesize the proposition, but if it fails we keep the current one.
-      This may happen because propositional instances are often provided manually using `haveI`.
+      We normalize the type to make sure `OfNat (Fin (2+1)) 1` and `OfNat (Fin 3) 1` will produce
+      the same instances.
       -/
-      let h' := (← Sym.synthInstance? prop').getD h
-      /- **Note**: We don't need to check whether `h` and `h'` are definitionally equal because of proof irrelevance. -/
-      return if isSameExpr prop prop' && isSameExpr h h' then e else mkApp2 g prop' h'
-
-  /--
-  Canonicalize a decidable instance without checking the cache.
-  Given a term `e` of the form `@Grind.nestedDecidable prop inst`, where `g` is the constant `Grind.nestedDecidable`,
-  we canonicalize it as follows:
-  1- We recursively canonicalize the proposition `prop`.
-  2- Try to resynthesize the instance, but keep the original one in case of failure since users often
-  provide them using `haveI`.
-  -/
-  canonInstDec' (g : Expr) (prop : Expr) (inst : Expr) (e : Expr) : CanonM Expr := do
-    let prop' ← canon prop
-    let type := mkApp (mkConst ``Decidable) prop'
-    if (← read).insideType then
-      /- See comment in `canonInstProp` for why we suppress reporting here. -/
-      canonInstCore inst type (report := false)
-    else
-      /-
-      **Note**: We try to resynthesize the instance, but if it fails we keep the current one.
-      We use `checkDefEqInst` here because two structurally different decidable instances are not necessarily
-      definitionally equal.
-      This may happen because propositional instances are often provided manually using `haveI`.
-      -/
-      let inst' := (← Sym.synthInstance? type).getD inst
-      let inst' ← checkDefEqInst inst inst'
-      return if isSameExpr prop prop' && isSameExpr inst inst' then e else mkApp2 g prop' inst'
-
-  /-- `withCaching` + `canonInstDec'` -/
-  canonInstDec (g : Expr) (prop : Expr) (h : Expr) (e : Expr) : CanonM Expr := withCaching e do
-    canonInstDec' g prop h e
-
-  /-- `canonInstDec` variant for normalizing `if-then-else` expressions. -/
-  canonInstDecCore (e : Expr) : CanonM Expr := do
-    match_expr e with
-    | g@Grind.nestedDecidable prop inst => canonInstDec g prop inst e
-    | _  => canonInst e (report := false)
+      let type ← inferType e
+      let type' ← canonInsideType' type
+      let some inst ← Sym.synthInstance? type' |
+        reportIssue! "failed to canonicalize instance{indentExpr e}\nfailed to synthesize{indentExpr type'}"
+        return e
+      let inst ← checkDefEqInst e inst
+      -- Remark: we cache result using the type **before** canonicalization.
+      modify fun s => { s with canon.cacheInsts := s.canon.cacheInsts.insert e inst }
+      return inst
 
   canonLambda (e : Expr) : CanonM Expr := do
     if (← read).insideType then
@@ -391,56 +295,60 @@ where
       mkLetFVars (generalizeNondepLet := false) fvars (← canon (e.instantiateRev fvars))
 
   canonAppDefault (e : Expr) : CanonM Expr := e.withApp fun f args => do
-    if args.size == 2 then
-      if f.isConstOf ``Grind.nestedProof then
-        /- **Note**: We don't have special treatment if `e` inside a type. -/
-        let prop := args[0]!
-        let prop' ← canon prop
-        let e' := if isSameExpr prop prop' then e else mkApp2 f prop' args[1]!
-        return e'
-      else if f.isConstOf ``Grind.nestedDecidable then
-        return (← canonInstDec' f args[0]! args[1]! e)
-    let mut modified := false
-    let args ← if f.isConstOf ``OfNat.ofNat then
-      let some args ← normOfNatArgs? args | pure args
-      modified := true
-      pure args
+    if f.isConstOf ``Grind.nestedProof && args.size == 2 then
+      let prop := args[0]!
+      let prop' ← canon prop
+      let e' := if isSameExpr prop prop' then e else mkAppN f (args.set! 0 prop')
+      return e'
+    else if f.isConstOf ``Grind.nestedDecidable && args.size == 2 then
+      let prop := args[0]!
+      let prop' ← canon prop
+      let e' := if isSameExpr prop prop' then e else mkAppN f (args.set! 0 prop')
+      return e'
     else
-      pure args
-    let mut f := f
-    let f' ← canon f
-    unless isSameExpr f f' do
-      f := f'
-      modified := true
-    let pinfos := (← getFunInfo f).paramInfo
-    let mut args := args.toVector
-    for h : i in *...args.size do
-      let arg := args[i]
-      trace[sym.debug.canon] "[{repr (← shouldCanon pinfos i arg)}]: {arg} : {← inferType arg}"
-      let arg' ← match (← shouldCanon pinfos i arg) with
-        | .canonType =>
-          /-
-          The type may have nested propositions and terms that may need to be canonicalized too.
-          So, we must recurse over it. See issue #10232
-          -/
-          canonInsideType' arg
-        | .canonImplicit => canon arg
-        | .visit => canon arg
-        | .canonInst =>
-          match_expr arg with
-          | g@Grind.nestedDecidable prop h => canonInstDec g prop h arg
-          | g@Grind.nestedProof prop h => canonInstProp g prop h arg
-          | _ => canonInst arg
-      unless isSameExpr arg arg' do
-        args := args.set i arg'
+      let mut modified := false
+      let args ← if f.isConstOf ``OfNat.ofNat then
+        let some args ← normOfNatArgs? args | pure args
         modified := true
-    return if modified then mkAppN f args.toArray else e
+        pure args
+      else
+        pure args
+      let mut f := f
+      let f' ← canon f
+      unless isSameExpr f f' do
+        f := f'
+        modified := true
+      let pinfos := (← getFunInfo f).paramInfo
+      let mut args := args.toVector
+      for h : i in *...args.size do
+        let arg := args[i]
+        trace[sym.debug.canon] "[{repr (← shouldCanon pinfos i arg)}]: {arg} : {← inferType arg}"
+        let arg' ← match (← shouldCanon pinfos i arg) with
+          | .canonType =>
+            /-
+            The type may have nested propositions and terms that may need to be canonicalized too.
+            So, we must recurse over it. See issue #10232
+            -/
+            canonInsideType' arg
+          | .canonImplicit => canon arg
+          | .visit => canon arg
+          | .canonInst =>
+            if arg.isAppOfArity ``Grind.nestedDecidable 2 then
+              let prop := arg.appFn!.appArg!
+              let prop' ← canon prop
+              if isSameExpr prop prop' then pure arg else pure (mkApp2 arg.appFn!.appFn! prop' arg.appArg!)
+            else
+              canonInst arg
+        unless isSameExpr arg arg' do
+          args := args.set i arg'
+          modified := true
+      return if modified then mkAppN f args.toArray else e
 
   canonIte (f : Expr) (α c inst a b : Expr) : CanonM Expr := do
     let c ← canon c
     if isTrueCond c then canon a
     else if isFalseCond c then canon b
-    else return mkApp5 f (← canonInsideType α) c (← canonInstDecCore inst) (← canon a) (← canon b)
+    else return mkApp5 f (← canonInsideType α) c (← canonInst inst) (← canon a) (← canon b)
 
   canonCond (f : Expr) (α c a b : Expr) : CanonM Expr := do
     let c ← canon c
@@ -481,24 +389,30 @@ where
         return e
 
   canonApp (e : Expr) : CanonM Expr := do
-    match_expr e with
-    | f@ite α c i a b => canonIte f α c i a b
-    | f@cond α c a b => canonCond f α c a b
-    -- Remark: We currently don't normalize dependent-if-then-else occurring in types.
-    | _ =>
-      let f := e.getAppFn
-      let .const declName _ := f | canonAppAndPost e
-      if (← isMatcher declName) then
-        canonMatch e
-      else
-        canonAppAndPost e
+    if (← read).insideType then
+      match_expr e with
+      | f@ite α c i a b => canonIte f α c i a b
+      | f@cond α c a b => canonCond f α c a b
+      -- Remark: We currently don't normalize dependent-if-then-else occurring in types.
+      | _ =>
+        let f := e.getAppFn
+        let .const declName _ := f | canonAppAndPost e
+        if (← isMatcher declName) then
+          canonMatch e
+        else
+          canonAppAndPost e
+    else
+      canonAppDefault e
 
   canonProj (e : Expr) : CanonM Expr := do
     let e := e.updateProj! (← canon e.projExpr!)
-    return (← reduceProj? e).getD e
+    if (← read).insideType then
+      return (← reduceProj? e).getD e
+    else
+      return e
 
 /--
-Returns `true` if `shouldCanon pinfos i arg` is not `.visit`.
+Returns `true` if `shouldCannon pinfos i arg` is not `.visit`.
 This is a helper function used to implement mbtc.
 -/
 public def isSupport (pinfos : Array ParamInfo) (i : Nat) (arg : Expr) : MetaM Bool := do
@@ -509,8 +423,8 @@ end Canon
 
 /--
 Canonicalize `e` by normalizing types, instances, and support arguments.
-Applies targeted reductions (projection, match/ite/cond, Nat arithmetic) in all positions;
-eta reduction is applied only inside types. Instances are re-synthesized.
+Types receive targeted reductions (eta, projection, match/ite, Nat arithmetic).
+Instances are re-synthesized. Values are traversed but not reduced.
 Runs at reducible transparency.
 -/
 public def canon (e : Expr) : SymM Expr := do profileitM Exception "sym canon" (← getOptions) do

src/Lean/Meta/Sym/InstantiateS.lean

@@ -86,8 +86,22 @@ It assumes the input is maximally shared, and ensures the output is too.
 public def instantiateS  (e : Expr) (subst : Array Expr) : SymM Expr :=
   liftBuilderM <| instantiateS' e subst
 
-/-- Internal variant of `betaRevS` that runs in `AlphaShareBuilderM`. -/
-private partial def betaRevS' (f : Expr) (revArgs : Array Expr) : AlphaShareBuilderM Expr :=
+/-- `mkAppRevRangeS f b e args == mkAppRev f (revArgs.extract b e)` -/
+def mkAppRevRangeS (f : Expr) (beginIdx endIdx : Nat) (revArgs : Array Expr) : AlphaShareBuilderM Expr :=
+  loop revArgs beginIdx f endIdx
+where
+  loop (revArgs : Array Expr) (start : Nat) (b : Expr) (i : Nat) : AlphaShareBuilderM Expr := do
+  if i ≤ start then
+    return b
+  else
+    let i := i - 1
+    loop revArgs start (← mkAppS b revArgs[i]!) i
+
+/--
+Beta-reduces `f` applied to reversed arguments `revArgs`, ensuring maximally shared terms.
+`betaRevS f #[a₃, a₂, a₁]` computes the beta-normal form of `f a₁ a₂ a₃`.
+-/
+partial def betaRevS (f : Expr) (revArgs : Array Expr) : AlphaShareBuilderM Expr :=
   if revArgs.size == 0 then
     return f
   else
@@ -159,7 +173,7 @@ where
     | .bvar bidx =>
       let f' ← visitBVar f bidx offset
       if modified || !isSameExpr f f' then
-        betaRevS' f' argsRev
+        betaRevS f' argsRev
       else
         return e
     | _ => unreachable!
@@ -201,18 +215,4 @@ public def instantiateRevBetaS (e : Expr) (subst : Array Expr) : SymM Expr := do
   if !e.hasLooseBVars || subst.isEmpty then return e
   else liftBuilderM <| instantiateRevBetaS' e subst
 
-/--
-Beta-reduces `f` applied to reversed arguments `revArgs`, ensuring maximally shared terms.
-`betaRevS f #[a₃, a₂, a₁]` computes the beta-normal form of `f a₁ a₂ a₃`.
--/
-public def betaRevS (f : Expr) (revArgs : Array Expr) : SymM Expr :=
-  liftBuilderM <| betaRevS' f revArgs
-
-/--
-Apply the given arguments to `f`, beta-reducing if `f` is a lambda expression,
-ensuring maximally shared terms. See `betaRevS` for details.
--/
-public def betaS (f : Expr) (args : Array Expr) : SymM Expr :=
-  betaRevS f args.reverse
-
 end Lean.Meta.Sym

src/Lean/Meta/Sym/SymM.lean

@@ -152,6 +152,8 @@ structure Canon.State where
   cache       : Std.HashMap Expr Expr := {}
   /-- Cache for type-level canonicalization (reductions applied). -/
   cacheInType : Std.HashMap Expr Expr := {}
+  /-- Cache mapping instances to their canonical synthesized instances. -/
+  cacheInsts  : Std.HashMap Expr Expr := {}
 
 /-- Mutable state for the symbolic computation framework. -/
 structure State where

src/Lean/Meta/Tactic/Cbv/ControlFlow.lean

@@ -44,7 +44,7 @@ def isCbvNoncomputable (p : Name) : CoreM Bool := do
   return evalLemmas.isNone && Lean.isNoncomputable (← getEnv) p
 
 /--
-Attempts to synthesize `Decidable p` instance and guards against picking up a `noncomputable` instance
+Attemps to synthesize `Decidable p` instance and guards against picking up a `noncomputable` instance
 -/
 def trySynthComputableInstance (p : Expr) : SymM <| Option Expr := do
   let .some inst' ← trySynthInstance (mkApp (mkConst ``Decidable) p) | return .none
@@ -112,7 +112,7 @@ builtin_cbv_simproc ↓ simpIteCbv (@ite _ _ _ _ _) := fun e => do
       else if (← isFalseExpr c') then
         return .step b (mkApp (e.replaceFn ``ite_cond_eq_false) h) (contextDependent := cd)
       else
-        -- If we got stuck with simplifying `p` then let's try evaluating the original instance
+        -- If we got stuck with simplifying `p` then let's try evaluating the original isntance
         simpAndMatchIteDecidable f α c inst a b do
           -- If we get stuck here, maybe the problem is that we need to look at `Decidable c'`
           let inst' := mkApp4 (mkConst ``decidable_of_decidable_of_eq) c c' inst h
@@ -317,7 +317,7 @@ public def reduceRecMatcher : Simproc := fun e => do
   else
     return .rfl
 
-builtin_cbv_simproc ↓ simpDecidableRec (@Decidable.rec _ _ _ _ _) :=
+builtin_cbv_simproc ↓ simpDecidableRec (@Decidable.rec _ _ _ _ _) := 
   (simpInterlaced · #[false,false,false,false,true]) >> reduceRecMatcher
 
 def tryMatchEquations (appFn : Name) : Simproc := fun e => do

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

@@ -272,7 +272,7 @@ def handleProj : Simproc := fun e => do
         let reduced ← Sym.share reduced
         return .step reduced (← Sym.mkEqRefl reduced)
       | .none =>
-       -- If we failed to reduce it, we turn to a last resort; we try use heterogeneous congruence lemma that we then try to turn into an equality.
+       -- If we failed to reduce it, we turn to a last resort; we try use heterogenous congruence lemma that we then try to turn into an equality.
         unless (← isDefEq struct e') do
           -- If we rewrote the projection body using something that holds up to propositional equality, then there is nothing we can do.
           -- TODO: Check if there is a need to report this to a user, or shall we fail silently.
@@ -283,7 +283,6 @@ def handleProj : Simproc := fun e => do
         let newProof ← mkEqOfHEq newProof (check := false)
         return .step (← Lean.Expr.updateProjS! e e') newProof
 
-open Sym.Internal in
 /--
 For an application whose head is neither a constant nor a lambda (e.g. a projection
 like `p.1 x`), simplify the function head and lift the proof via `congrArg`.

src/Lean/Meta/Tactic/Cbv/Util.lean

@@ -24,6 +24,9 @@ namespace Lean.Meta.Tactic.Cbv
 
 open Lean.Meta.Sym.Simp
 
+public def mkAppNS (f : Expr) (args : Array Expr) : Sym.SymM Expr := do
+  args.foldlM Sym.Internal.mkAppS f
+
 abbrev isNatValue (e : Expr) : Bool := (Sym.getNatValue? e).isSome
 abbrev isStringValue (e : Expr) : Bool := (Sym.getStringValue? e).isSome
 abbrev isIntValue (e : Expr) : Bool := (Sym.getIntValue? e).isSome

src/Lean/Meta/Tactic/Grind/Arith/CommRing.lean

@@ -5,9 +5,11 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Internalize
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.ToExpr
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.SemiringM
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommRingM
@@ -19,6 +21,8 @@ public import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Inv
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.PP
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.VarRename
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadCanon
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadSemiring
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Action

src/Lean/Meta/Tactic/Grind/Arith/CommRing/DenoteExpr.lean

@@ -8,7 +8,6 @@ prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-open Sym.Arith
 /-!
 Helper functions for converting reified terms back into their denotations.
 -/

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Functions.lean

@@ -8,7 +8,6 @@ prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-open Sym.Arith
 variable [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m]
 
 section

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Inv.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
-import Lean.Meta.Sym.Arith.Poly
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
 

src/Lean/Meta/Tactic/Grind/Arith/CommRing/MonadCanon.lean

@@ -1,23 +1,24 @@
 /-
-Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Sym.Arith.Types
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
 public section
-namespace Lean.Meta.Sym.Arith
+namespace Lean.Meta.Grind.Arith.CommRing
 
 class MonadCanon (m : Type → Type) where
   /--
-  Canonicalize an expression (types, instances, support arguments).
-  In `SymM`, this is `Sym.canon`. In `PP.M` (diagnostics), this is the identity.
+  Helper function for removing dependency on `GoalM`.
+  In `RingM` and `SemiringM`, this is just `sharedCommon (← canon e)`
+  When printing counterexamples, we are at `MetaM`, and this is just the identity function.
   -/
   canonExpr : Expr → m Expr
   /--
-  Synthesize an instance, returning `none` on failure.
-  In `SymM`, this is `Sym.synthInstance?`. In `PP.M`, this is `Meta.synthInstance?`.
+  Helper function for removing dependency on `GoalM`. During search we
+  want to track the instances synthesized by `grind`, and this is `Grind.synthInstance`.
   -/
   synthInstance? : Expr → m (Option Expr)
 
@@ -30,7 +31,7 @@ instance (m n) [MonadLift m n] [MonadCanon m] : MonadCanon n where
 
 def MonadCanon.synthInstance [Monad m] [MonadError m] [MonadCanon m] (type : Expr) : m Expr := do
   let some inst ← synthInstance? type
-    | throwError "failed to find instance{indentExpr type}"
+    | throwError "`grind` failed to find instance{indentExpr type}"
   return inst
 
-end Lean.Meta.Sym.Arith
+end Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing/MonadRing.lean

@@ -5,8 +5,7 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Sym.Arith.MonadCanon
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadCanon
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
 

src/Lean/Meta/Tactic/Grind/Arith/CommRing/MonadSemiring.lean

@@ -5,8 +5,7 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Sym.Arith.MonadCanon
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadCanon
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
 

src/Lean/Meta/Tactic/Grind/Arith/CommRing/NonCommRingM.lean

@@ -8,7 +8,7 @@ prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-open Sym.Arith
+
 structure NonCommRingM.Context where
   ringId : Nat
 

src/Lean/Meta/Tactic/Grind/Arith/CommRing/NonCommSemiringM.lean

@@ -8,7 +8,6 @@ prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.SemiringM
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-open Sym.Arith (MonadCanon)
 
 structure NonCommSemiringM.Context where
   semiringId : Nat

src/Lean/Meta/Tactic/Grind/Arith/CommRing/PP.lean

@@ -10,7 +10,6 @@ import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 import Init.Omega
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-open Sym.Arith
 
 private abbrev M := StateT CommRing MetaM
 

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean

@@ -12,14 +12,12 @@ import Lean.Data.RArray
 import Lean.Meta.Tactic.Grind.Diseq
 import Lean.Meta.Tactic.Grind.ProofUtil
 import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
-import Lean.Meta.Sym.Arith.ToExpr
-import Lean.Meta.Sym.Arith.VarRename
+import Lean.Meta.Tactic.Grind.Arith.CommRing.ToExpr
+import Lean.Meta.Tactic.Grind.Arith.CommRing.VarRename
 import Init.Data.Nat.Order
 import Init.Data.Order.Lemmas
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-open Sym.Arith (MonadCanon)
-
 /--
 Returns a context of type `RArray α` containing the variables `vars` where
 `α` is the type of the ring.

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Reify.lean

@@ -9,7 +9,6 @@ public import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommRingM
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommSemiringM
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-open Sym.Arith (MonadCanon)
 
 variable [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m]
 

src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingM.lean

@@ -9,7 +9,6 @@ public import Lean.Meta.Tactic.Grind.SynthInstance
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-open Sym.Arith
 
 def checkMaxSteps : GoalM Bool := do
   return (← get').steps >= (← getConfig).ringSteps

src/Lean/Meta/Tactic/Grind/Arith/CommRing/SafePoly.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
-public import Lean.Meta.Sym.Arith.Poly
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
 import Lean.Meta.Tactic.Grind.Arith.EvalNum
 import Init.Data.Nat.Linear
 public section

src/Lean/Meta/Tactic/Grind/Arith/CommRing/SemiringM.lean

@@ -11,7 +11,6 @@ import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-open Sym.Arith
 
 structure SemiringM.Context where
   semiringId : Nat

src/Lean/Meta/Tactic/Grind/Arith/CommRing/ToExpr.lean

@@ -8,7 +8,7 @@ prelude
 public import Init.Grind.Ring.CommSemiringAdapter
 public import Lean.ToExpr
 public section
-namespace Lean.Meta.Sym.Arith
+namespace Lean.Meta.Grind.Arith.CommRing
 open Grind.CommRing
 /-!
 `ToExpr` instances for `CommRing.Poly` types.
@@ -57,4 +57,4 @@ instance : ToExpr CommRing.Expr where
   toExpr := ofRingExpr
   toTypeExpr := mkConst ``CommRing.Expr
 
-end Lean.Meta.Sym.Arith
+end Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean

@@ -7,7 +7,7 @@ module
 prelude
 public import Init.Grind.Ring.CommSemiringAdapter
 public import Lean.Meta.Tactic.Grind.Types
-import Lean.Meta.Sym.Arith.Poly
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
 public section
 
 namespace Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean

@@ -14,8 +14,8 @@ import Lean.Meta.Tactic.Grind.Arith.Cutsat.CommRing
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.VarRename
-import Lean.Meta.Sym.Arith.VarRename
-import Lean.Meta.Sym.Arith.ToExpr
+import Lean.Meta.Tactic.Grind.Arith.CommRing.VarRename
+import Lean.Meta.Tactic.Grind.Arith.CommRing.ToExpr
 import Init.Data.Nat.Order
 import Init.Data.Order.Lemmas
 public section

src/Lean/Meta/Tactic/Grind/Arith/Linear/LinearM.lean

@@ -9,7 +9,6 @@ public import Lean.Meta.Tactic.Grind.Arith.Linear.Types
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
 public section
 namespace Lean.Meta.Grind.Arith.Linear
-open Sym.Arith (MonadCanon)
 
 def get' : GoalM State := do
   linearExt.getState

src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean

@@ -11,8 +11,8 @@ import Lean.Data.RArray
 import Lean.Meta.Tactic.Grind.Arith.Linear.ToExpr
 import Lean.Meta.Tactic.Grind.Diseq
 import Lean.Meta.Tactic.Grind.ProofUtil
-import Lean.Meta.Sym.Arith.VarRename
-import Lean.Meta.Sym.Arith.ToExpr
+import Lean.Meta.Tactic.Grind.Arith.CommRing.VarRename
+import Lean.Meta.Tactic.Grind.Arith.CommRing.ToExpr
 import Lean.Meta.Tactic.Grind.Arith.Linear.VarRename
 public import Lean.Meta.Tactic.Grind.Arith.Linear.DenoteExpr
 public import Lean.Meta.Tactic.Grind.Arith.Linear.OfNatModule

src/Lean/Meta/Tactic/Grind/Core.lean

@@ -172,7 +172,7 @@ private partial def addEqStep (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit
       trueEqFalse := true
     else
       let hasHEq := isHEq || lhsRoot.heqProofs || rhsRoot.heqProofs
-      -- **Note**: We only have to check the types if there are heterogeneous equalities.
+      -- **Note**: We only have to check the types if there are heterogenous equalities.
       if (← pure !hasHEq <||> hasSameType lhsRoot.self rhsRoot.self) then
         valueInconsistency := true
   if    (lhsRoot.interpreted && !rhsRoot.interpreted)

src/Lean/Meta/Tactic/Grind/Order/Internalize.lean

@@ -97,8 +97,6 @@ def mkCnstrNorm0 (s : Struct) (ringInst : Expr) (kind : CnstrKind) (lhs rhs : Ex
   | .le => mkLeNorm0 s ringInst lhs rhs
   | .lt => mkLtNorm0 s ringInst lhs rhs
 
-open Sym.Arith (MonadCanon)
-
 /--
 Returns `rel lhs (rhs + 0)`
 -/

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

@@ -1973,7 +1973,7 @@ def SolverExtension.markTerm (ext : SolverExtension σ) (e : Expr) : GoalM Unit
     | .next id' e' sTerms' =>
       if id == id' then
         -- Skip if `e` and `e'` have different types (e.g., they were merged via `HEq` from `cast`).
-        -- This can happen when we have heterogeneous equalities in an equivalence class containing types such as `Fin n` and `Fin m`
+        -- This can happen when we have heterogenous equalities in an equivalence class containing types such as `Fin n` and `Fin m`
         if (← pure !root.heqProofs <||> hasSameType e e') then
           (← solverExtensionsRef.get)[id]!.newEq e e'
         return sTerms
@@ -2056,7 +2056,7 @@ where
     | .nil => return ()
     | .eq solverId lhs rhs rest =>
       -- Skip if `lhs` and `rhs` have different types (e.g., they were merged via `HEq` from `cast`).
-      -- This can happen when we have heterogeneous equalities in an equivalence class containing types such as `Fin n` and `Fin m`
+      -- This can happen when we have heterogenous equalities in an equivalence class containing types such as `Fin n` and `Fin m`
       let root ← getRootENode lhs
       if (← pure !root.heqProofs <||> hasSameType lhs rhs) then
         (← solverExtensionsRef.get)[solverId]!.newEq lhs rhs

src/Lean/Runtime.lean

@@ -21,6 +21,9 @@ opaque maxSmallNatFn : Unit → Nat
 @[extern "lean_libuv_version"]
 opaque libUVVersionFn : Unit → Nat
 
+@[extern "lean_openssl_version"]
+opaque openSSLVersionFn : Unit → Nat
+
 def closureMaxArgs : Nat :=
   closureMaxArgsFn ()
 
@@ -30,4 +33,7 @@ def maxSmallNat : Nat :=
 def libUVVersion : Nat :=
   libUVVersionFn ()
 
+def openSSLVersion : Nat :=
+  openSSLVersionFn ()
+
 end Lean

src/Lean/Server/FileWorker/WidgetRequests.lean

@@ -192,7 +192,7 @@ private def matchEndPos (query : String) (startPos : String.Pos.Raw) : String.Po
   startPos + query
 
 @[specialize]
-private def highlightStringMatches? (query text : String) (matchPositions : Array String.Pos.Raw)
+private def hightlightStringMatches? (query text : String) (matchPositions : Array String.Pos.Raw)
     (highlight : α) (offset : String.Pos.Raw := ⟨0⟩) (mapIdx : Nat → Nat := id) :
     Option (TaggedText α) := Id.run do
   if query.isEmpty || text.isEmpty || matchPositions.isEmpty then
@@ -245,7 +245,7 @@ private def advanceTaggedTextHighlightState (text : String) (highlighted : α) :
   let query := (← get).query
   let p := (← get).p
   let ms := (← get).ms
-  let highlighted? := highlightStringMatches? query text ms highlighted (offset := p)
+  let highlighted? := hightlightStringMatches? query text ms highlighted (offset := p)
     (mapIdx := fun i => ms.size - i - 1)
   updateState text highlighted?.isSome
   return highlighted?.getD (.text text)

src/Std/Tactic/BVDecide/Syntax.lean

@@ -53,7 +53,7 @@ structure BVDecideConfig where
   /--
   Split hypotheses of the form `h : (x && y) = true` into `h1 : x = true` and `h2 : y = true`.
   This has synergy potential with embedded constraint substitution. Because embedded constraint
-  substitution is the only use case for this feature it is automatically disabled whenever embedded
+  subsitution is the only use case for this feature it is automatically disabled whenever embedded
   constraint substitution is disabled.
   -/
   andFlattening : Bool := true

src/include/lean/lean.h

@@ -3168,10 +3168,6 @@ static inline lean_obj_res lean_manual_get_root(lean_obj_arg _unit) {
     return lean_mk_string(LEAN_MANUAL_ROOT);
 }
 
-static inline lean_obj_res lean_runtime_hold(b_lean_obj_arg a) {
-    return lean_box(0);
-}
-
 #ifdef LEAN_EMSCRIPTEN
 #define LEAN_SCALAR_PTR_LITERAL(b1, b2, b3, b4, b5, b6, b7, b8) (lean_object*)((uint32_t)b1 | ((uint32_t)b2 << 8) | ((uint32_t)b3 << 16) | ((uint32_t)b4 << 24)), (lean_object*)((uint32_t)b5 | ((uint32_t)b6 << 8) | ((uint32_t)b7 << 16) | ((uint32_t)b8 << 24))
 #else

src/kernel/declaration.h

@@ -226,7 +226,7 @@ public:
     bool is_unsafe() const;
     /** \brief Only definitions have values for the purpose of reduction and
         type checking. Theorems used to be like that; now they are treated like
-        opaque declarations. */
+        opaque declations. */
     bool has_value() const { return is_definition(); }
 
     axiom_val const & to_axiom_val() const { lean_assert(is_axiom()); return static_cast<axiom_val const &>(cnstr_get_ref(raw(), 0)); }

src/lake/Lake/Build/Common.lean

@@ -271,7 +271,7 @@ Returns `true` if the saved trace exists and its hash matches `inputHash`.
 
 If up-to-date, replays the saved log from the trace and sets the current
 build action to `replay`. Otherwise, if the log is empty and trace is synthetic,
-or if the trace is not up-to-date, the build action will be set to `fetch`.
+or if the trace is not up-to-date, the build action will be set ot `fetch`.
 -/
 public def SavedTrace.replayOrFetchIfUpToDate (inputHash : Hash) (self : SavedTrace) : JobM Bool := do
   if let .ok data := self then

src/lake/Lake/Build/InitFacets.lean

@@ -19,7 +19,7 @@ import Lake.Build.InputFile
 namespace Lake
 
 /-- The initial set of Lake facets. -/
-public def initFacetConfigs : FacetConfigMap :=
+public def initFacetConfigs : DNameMap FacetConfig :=
   DNameMap.empty
   |> insert Module.initFacetConfigs
   |> insert Package.initFacetConfigs
@@ -30,4 +30,4 @@ public def initFacetConfigs : FacetConfigMap :=
   |> insert InputDir.initFacetConfigs
 where
   insert {k} (group : DNameMap (KFacetConfig k)) map :=
-    group.foldl (init := map) fun m _ v => m.insert v.toFacetConfig
+    group.foldl (init := map) fun m k v => m.insert k v.toFacetConfig

src/lake/Lake/Build/Module.lean

@@ -705,7 +705,7 @@ private def Module.restoreAllArtifacts (mod : Module) (cached : ModuleOutputArti
 where
   @[inline] restoreSome file art? := art?.mapM (restoreArtifact file ·)
 
-public def Module.checkArtifactsExist (self : Module) (isModule : Bool) : BaseIO Bool := do
+public def Module.checkArtifactsExsist (self : Module) (isModule : Bool) : BaseIO Bool := do
   unless (← self.oleanFile.pathExists) do return false
   unless (← self.ileanFile.pathExists) do return false
   unless (← self.cFile.pathExists) do return false
@@ -718,7 +718,7 @@ public def Module.checkArtifactsExist (self : Module) (isModule : Bool) : BaseIO
   return true
 
 public protected def Module.checkExists (self : Module) (isModule : Bool) : BaseIO Bool := do
-  self.ltarFile.pathExists <||> self.checkArtifactsExist isModule
+  self.ltarFile.pathExists <||> self.checkArtifactsExsist isModule
 
 @[deprecated Module.checkExists (since := "2025-03-04")]
 public instance : CheckExists Module := ⟨Module.checkExists (isModule := false)⟩
@@ -788,7 +788,7 @@ instance : ToOutputJson ModuleOutputArtifacts := ⟨(toJson ·.descrs)⟩
 
 def Module.packLtar (self : Module) (arts : ModuleOutputArtifacts) : JobM Artifact := do
   let arts ← id do
-    if (← self.checkArtifactsExist arts.isModule) then
+    if (← self.checkArtifactsExsist arts.isModule) then
       return arts
     else self.restoreAllArtifacts arts
   let args ← id do
@@ -941,7 +941,7 @@ where
       | .inr savedTrace =>
         let status ← savedTrace.replayIfUpToDate' (oldTrace := srcTrace.mtime) mod depTrace
         if status.isUpToDate then
-          unless (← mod.checkArtifactsExist setup.isModule) do
+          unless (← mod.checkArtifactsExsist setup.isModule) do
             mod.unpackLtar mod.ltarFile
         else
           discard <| mod.buildLean depTrace srcFile setup
@@ -953,7 +953,7 @@ where
           mod.computeArtifacts setup.isModule
     else
       if (← savedTrace.replayIfUpToDate (oldTrace := srcTrace.mtime) mod depTrace) then
-        unless (← mod.checkArtifactsExist setup.isModule) do
+        unless (← mod.checkArtifactsExsist setup.isModule) do
           mod.unpackLtar mod.ltarFile
         mod.computeArtifacts setup.isModule
       else

src/lake/Lake/Build/Trace.lean

@@ -151,7 +151,7 @@ public def ofDecimal? (s : String) : Option Hash :=
 @[inline] public def ofString? (s : String) : Option Hash :=
   ofHex? s
 
-/-- Load a hash from a `.hash` file. -/
+/-- Laod a hash from a `.hash` file. -/
 public def load? (hashFile : FilePath) : BaseIO (Option Hash) :=
   ofString? <$> IO.FS.readFile hashFile |>.catchExceptions fun _ => pure none
 

src/lake/Lake/CLI/Help.lean

@@ -356,9 +356,9 @@ USAGE:
 
 COMMANDS:
   get [<mappings>]      download build outputs into the local Lake cache
-  put <mappings>        upload build outputs to a remote cache
+  put <mappings>        upload build ouptuts to a remote cache
   add <mappings>        add input-to-output mappings to the Lake cache
-  clean                 removes ALL from the local Lake cache
+  clean                 removes ALL froms the local Lake cache
   services              print configured remote cache services
 
 STAGING COMMANDS:
@@ -415,7 +415,7 @@ will search the repository's entire history (or as far as Git will allow).
 
 By default, Lake will download both the input-to-output mappings and the
 output artifacts for a package. By using `--mappings-onlys`, Lake will only
-download the mappings and delay downloading artifacts until they are needed.
+download the mappings abd delay downloading artifacts until they are needed.
 
 If a download for an artifact fails or the download process for a whole
 package fails, Lake will report this and continue on to the next. Once done,
@@ -469,7 +469,7 @@ OPTIONS:
   --scope=<remote-scope>          the prefix of artifacts within the service
   --repo=<github-repo>            for Reservoir, a GitHub repository scope
 
-Reads a list of input-to-output mappings from the provided file and adds
+Reads a list of input-to-output mapppings from the provided file and adds
 them to the local Lake cache. If `--service` is provided, the output artifacts
 can then be fetched lazily from that service during a Lake build. The service
 must either be `reservoir` or  be configured through the Lake system

src/lake/Lake/Config/Env.lean

@@ -58,7 +58,7 @@ public structure Env where
   If `none`, no suitable system directory for the cache exists.
   -/
   lakeSystemCache? : Option Cache := none
-  /-- The path to the system Lake configuration (i.e., `LAKE_CONFIG`). -/
+  /-- The path to the sytem Lake configuration (i.e., `LAKE_CONFIG`). -/
   lakeConfig? : Option FilePath
   /-- The authentication key for cache uploads (i.e., `LAKE_CACHE_KEY`). -/
   cacheKey? : Option String

src/lake/Lake/Config/FacetConfig.lean

@@ -27,20 +27,6 @@ public structure FacetConfig (name : Name) : Type where
   memoize : Bool := true
   deriving Inhabited
 
-/-- A mapping of facet names to the configuration for that name. -/
-public abbrev FacetConfigMap := DNameMap FacetConfig
-
-/--
-Tries to retrieve the facet configuration for the given {lean}`name`,
-returning {lean}`none` if no such mapping is present.
--/
-public nonrec def FacetConfigMap.get? (name : Name) (self : FacetConfigMap) : Option (FacetConfig name) :=
-  self.get? name -- specializes `get?`
-
-/-- Inserts the facet configuration {lean}`cfg` into the map (overwriting any existing configuration). -/
-public nonrec def FacetConfigMap.insert {name} (cfg : FacetConfig name) (self : FacetConfigMap) : FacetConfigMap :=
-  self.insert name cfg -- specializes `insert`
-
 public protected abbrev FacetConfig.name (_ : FacetConfig name) := name
 
 public structure KFacetConfig (k : Name) (name : Name) extends FacetConfig name where
@@ -84,9 +70,6 @@ public structure NamedConfigDecl (β : Name → Type u) where
   name : Name
   config : β name
 
-/-- A facet declaration from a configuration file. -/
-public abbrev FacetDecl := NamedConfigDecl FacetConfig
-
 /-- A module facet's declarative configuration. -/
 public abbrev ModuleFacetConfig := KFacetConfig Module.facetKind
 

src/lake/Lake/Config/LakefileConfig.lean

@@ -1,53 +0,0 @@
-/-
-Copyright (c) 2025 Mac Malone. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mac Malone
--/
-module
-
-prelude
-public import Lake.Config.Script
-public import Lake.Config.Dependency
-public import Lake.Config.PackageConfig
-public import Lake.Config.FacetConfig
-public import Lake.Config.TargetConfig
-
-set_option doc.verso true
-
-open Lean
-
-namespace Lake
-
-/-- The configuration defined by a Lake configuration file (e.g., {lit}`lakefile.(lean|toml)`). -/
-public structure LakefileConfig where
-  /-- The package deceleration of the configuration file. -/
-  pkgDecl : PackageDecl
-  /-- Depdency configurations in the order declared by the configuration file.  -/
-  depConfigs : Array Dependency := #[]
-  /-- Facet configurations in the order declared by the configuration file. -/
-  facetDecls : Array FacetDecl := {}
-  /-- Target configurations in the order declared by the configuration file. -/
-  targetDecls : Array (PConfigDecl pkgDecl.keyName) := #[]
-  /-- Name-declaration map of target configurations declared in the configuration file. -/
-  targetDeclMap : DNameMap (NConfigDecl pkgDecl.keyName) :=
-    targetDecls.foldl (fun m d => m.insert d.name (.mk d rfl)) {}
-  /-- The names of targets declared via {lit}`@[default_target]`. -/
-  defaultTargets : Array Name := #[]
-  /-- Scripts declared in the configuration file. -/
-  scripts : NameMap Script := {}
-  /-- The names of the scripts declared via {lit}`@[default_script]`. -/
-  defaultScripts : Array Script := #[]
-  /-- {lit}`post_update` hooks in the order declared by the configuration file.. -/
-  postUpdateHooks : Array (OpaquePostUpdateHook pkgDecl.keyName) := #[]
-  /--
-  The name of the configuration file's test driver.
-
-  It is either  declared via {lit}`@[test_driver]` or derived from {lean}`PackageConfig.testDriver`.
-  -/
-  testDriver : String := pkgDecl.config.testDriver
-  /--
-  The name of the configuration file's test driver.
-
-  It is either declared via {lit}`@[lint_driver]` or derived from {lean}`PackageConfig.lintDriver`.
-  -/
-  lintDriver : String := pkgDecl.config.lintDriver

src/lake/Lake/Config/Package.lean

@@ -45,7 +45,7 @@ public structure Package where
   /-- The path to the package's configuration file (relative to `dir`). -/
   relConfigFile : FilePath
   /-- The path to the package's JSON manifest of remote dependencies (relative to `dir`). -/
-  relManifestFile : FilePath
+  relManifestFile : FilePath := defaultManifestFile
   /-- The package's scope (e.g., in Reservoir). -/
   scope : String
   /-- The URL to this package's Git remote. -/

src/lake/Lake/Config/PackageConfig.lean

@@ -336,16 +336,11 @@ public configuration PackageConfig (p : Name) (n : Name) extends WorkspaceConfig
 deriving Inhabited
 
 /-- The package's name as specified by the author. -/
-@[deprecated "Deprecated without replacement" (since := "2025-12-10")]
 public abbrev PackageConfig.origName (_ : PackageConfig p n) := n
 
 /-- A package declaration from a configuration written in Lean. -/
 public structure PackageDecl where
-  baseName : Name
-  keyName : Name
+  name : Name
   origName : Name
-  config : PackageConfig keyName origName
+  config : PackageConfig name origName
   deriving TypeName
-
-@[deprecated PackageDecl.keyName (since := "2025-12-10")]
-public abbrev PackageDecl.name := @keyName

src/lake/Lake/Config/Workspace.lean

@@ -22,17 +22,15 @@ open Lean (Name LeanOptions)
 
 namespace Lake
 
-/--
-**For internal use only.**
-Computes the cache to use for the package based on the environment.
--/
+/-- **For internal use only.** Computes the cache to use for the package based on the environment. -/
 public def computeLakeCache (pkg : Package) (lakeEnv : Lake.Env) : Cache :=
   if pkg.bootstrap then
     lakeEnv.lakeSystemCache?.getD ⟨pkg.lakeDir / "cache"⟩
   else
     lakeEnv.lakeCache?.getD ⟨pkg.lakeDir / "cache"⟩
 
-public structure Workspace.Raw : Type where
+/-- A Lake workspace -- the top-level package directory. -/
+public structure Workspace : Type where
   /-- The root package of the workspace. -/
   root : Package
   /-- The detected {lean}`Lake.Env` of the workspace. -/
@@ -51,25 +49,14 @@ public structure Workspace.Raw : Type where
   The packages within the workspace
   (in {lit}`require` declaration order with the root coming first).
   -/
-  packages : Array Package := #[]
+  packages : Array Package := {}
   /-- Name-package map of packages within the workspace. -/
   packageMap : DNameMap NPackage := {}
   /-- Configuration map of facets defined in the workspace. -/
-  facetConfigs : FacetConfigMap := {}
-  deriving Nonempty
+  facetConfigs : DNameMap FacetConfig := {}
 
-public structure Workspace.Raw.WF (ws : Workspace.Raw) : Prop where
-  packages_wsIdx : ∀ (h : i < ws.packages.size), (ws.packages[i]'h).wsIdx = i
-
-/-- A Lake workspace -- the top-level package directory. -/
-public structure Workspace extends raw : Workspace.Raw, wf : raw.WF
-
-public instance : Nonempty Workspace := .intro {
-  lakeEnv := default
-  lakeConfig := Classical.ofNonempty
-  root := Classical.ofNonempty
-  packages_wsIdx h := by simp at h
-}
+public instance : Nonempty Workspace :=
+  ⟨by constructor <;> exact Classical.ofNonempty⟩
 
 public hydrate_opaque_type OpaqueWorkspace Workspace
 
@@ -188,20 +175,9 @@ This is configured through {lit}`cache.service` entries in the system Lake confi
 @[inline] public def packageOverridesFile (self : Workspace) : FilePath :=
   self.lakeDir / "package-overrides.json"
 
-/-- **For internal use only.** Add a well-formed package to the workspace. -/
-@[inline] public def addPackage' (pkg : Package) (self : Workspace) (h : pkg.wsIdx = self.packages.size) : Workspace :=
-  {self with
-    packages := self.packages.push pkg
-    packageMap := self.packageMap.insert pkg.keyName pkg
-    packages_wsIdx {i} i_lt := by
-      cases Nat.lt_add_one_iff_lt_or_eq.mp <| Array.size_push .. ▸ i_lt with
-      | inl i_lt => simpa [Array.getElem_push_lt i_lt] using self.packages_wsIdx i_lt
-      | inr i_eq => simpa [i_eq] using h
-  }
-
 /-- Add a package to the workspace. -/
-@[inline] public def addPackage (pkg : Package) (self : Workspace) : Workspace :=
-  self.addPackage' {pkg with wsIdx := self.packages.size} rfl
+public def addPackage (pkg : Package) (self : Workspace) : Workspace :=
+  {self with packages := self.packages.push pkg, packageMap := self.packageMap.insert pkg.keyName pkg}
 
 /-- Returns the unique package in the workspace (if any) that is identified by  {lean}`keyName`. -/
 @[inline] public protected def findPackageByKey? (keyName : Name) (self : Workspace) : Option (NPackage keyName) :=
@@ -275,15 +251,15 @@ public def findTargetDecl? (name : Name) (self : Workspace) : Option ((pkg : Pac
   self.packages.findSome? fun pkg => pkg.findTargetDecl? name <&> (⟨pkg, ·⟩)
 
 /-- Add a facet to the workspace. -/
-@[inline] public def addFacetConfig {name} (cfg : FacetConfig name) (self : Workspace) : Workspace :=
-  {self with facetConfigs := self.facetConfigs.insert cfg}
+public def addFacetConfig {name} (cfg : FacetConfig name) (self : Workspace) : Workspace :=
+  {self with facetConfigs := self.facetConfigs.insert name cfg}
 
 /-- Try to find a facet configuration in the workspace with the given name. -/
-@[inline] public def findFacetConfig? (name : Name) (self : Workspace) : Option (FacetConfig name) :=
+public def findFacetConfig? (name : Name) (self : Workspace) : Option (FacetConfig name) :=
   self.facetConfigs.get? name
 
 /-- Add a module facet to the workspace. -/
-@[inline] public def addModuleFacetConfig (cfg : ModuleFacetConfig name) (self : Workspace) : Workspace :=
+public def addModuleFacetConfig (cfg : ModuleFacetConfig name) (self : Workspace) : Workspace :=
   self.addFacetConfig cfg.toFacetConfig
 
 /-- Try to find a module facet configuration in the workspace with the given name. -/
@@ -291,7 +267,7 @@ public def findModuleFacetConfig? (name : Name) (self : Workspace) : Option (Mod
   self.findFacetConfig? name |>.bind (·.toKind? Module.facetKind)
 
 /-- Add a package facet to the workspace. -/
-@[inline] public def addPackageFacetConfig (cfg : PackageFacetConfig name) (self : Workspace) : Workspace :=
+public def addPackageFacetConfig (cfg : PackageFacetConfig name) (self : Workspace) : Workspace :=
   self.addFacetConfig cfg.toFacetConfig
 
 /-- Try to find a package facet configuration in the workspace with the given name. -/
@@ -299,7 +275,7 @@ public def findPackageFacetConfig? (name : Name) (self : Workspace) : Option (Pa
   self.findFacetConfig? name |>.bind (·.toKind? Package.facetKind)
 
 /-- Add a library facet to the workspace. -/
-@[inline] public def addLibraryFacetConfig (cfg : LibraryFacetConfig name) (self : Workspace) : Workspace :=
+public def addLibraryFacetConfig (cfg : LibraryFacetConfig name) (self : Workspace) : Workspace :=
   self.addFacetConfig cfg.toFacetConfig
 
 /-- Try to find a library facet configuration in the workspace with the given name. -/

src/lake/Lake/DSL/Package.lean

@@ -26,18 +26,17 @@ def elabPackageCommand : CommandElab := fun stx => do
   let configId : Ident ← `(pkgConfig)
   let id ← mkConfigDeclIdent nameStx?
   let origName := Name.quoteFrom id id.getId
-  let ⟨wsIdx, name⟩ := nameExt.getState (← getEnv)
-  let baseName := match name with
+  let ⟨idx, name⟩ := nameExt.getState (← getEnv)
+  let name := match name with
     | .anonymous => origName
     | name => Name.quoteFrom id name
-  let wsIdx := quote wsIdx
-  let keyName := Syntax.mkCApp ``Name.num #[baseName, wsIdx]
-  let ty := Syntax.mkCApp ``PackageConfig #[keyName, origName]
+  let name := Syntax.mkCApp ``Name.num #[name, quote idx]
+  let ty := Syntax.mkCApp ``PackageConfig #[name, origName]
   elabConfig ``PackageConfig configId ty cfg
   let attr ← `(Term.attrInstance| «package»)
   let attrs := #[attr] ++ expandAttrs attrs?
   let id := mkIdentFrom id packageDeclName
-  let decl ← `({baseName := $baseName, origName := $origName, keyName := $keyName, config := $configId})
+  let decl ← `({name := $name, origName := $origName, config := $configId})
   let cmd ← `($[$doc?]? @[$attrs,*] abbrev $id : PackageDecl := $decl)
   withMacroExpansion stx cmd <| elabCommand cmd
   let nameId := mkIdentFrom id <| packageDeclName.str "name"

src/lake/Lake/Load/Config.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Lake.Config.Env
-public import Lake.Config.Lang
 public import Lake.Config.LakeConfig
 public import Lake.Load.Manifest
 
@@ -42,16 +41,8 @@ public structure LoadConfig where
   pkgDir : FilePath := wsDir / relPkgDir
   /-- The package's Lake configuration file (relative to its directory). -/
   relConfigFile : FilePath := defaultConfigFile
-  /-- The full path to the loaded package's Lake configuration file. -/
+    /-- The full path to the loaded package's Lake configuration file. -/
   configFile : FilePath := pkgDir / relConfigFile
-  /-
-  The format of the package's configuration file.
-
-  If {lean}`none`, the format will be determined by the file's extension.
-  -/
-  configLang? : Option ConfigLang := none
-  /-- The package's Lake manifest file (relative to its directory). -/
-  relManifestFile : FilePath := defaultManifestFile
   /-- Additional package overrides for this workspace load. -/
   packageOverrides : Array PackageEntry := #[]
   /-- A set of key-value Lake configuration options (i.e., {lit}`-K` settings). -/
@@ -64,7 +55,6 @@ public structure LoadConfig where
   updateDeps : Bool := false
   /--
   Whether to update the workspace's {lit}`lean-toolchain` when dependencies are updated.
-
   If {lean}`true` and a toolchain update occurs, Lake will need to be restarted.
   -/
   updateToolchain : Bool := true

src/lake/Lake/Load/Lean.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Lake.Config.Package
-public import Lake.Config.LakefileConfig
 public import Lake.Load.Config
 import Lake.Load.Lean.Elab
 import Lake.Load.Lean.Eval
@@ -22,7 +21,22 @@ open Lean
 
 namespace Lake
 
-/-- Elaborate a Lake configuration file written in Lean and extract the Lake configuration.  -/
-public def loadLeanConfig  (cfg : LoadConfig) : LogIO LakefileConfig := do
+/--
+Elaborate a Lean configuration file into a `Package`.
+The resulting package does not yet include any dependencies.
+-/
+public def loadLeanConfig (cfg : LoadConfig) : LogIO (Package × Environment) := do
   let configEnv ← importConfigFile cfg
-  LakefileConfig.loadFromEnv configEnv cfg.leanOpts
+  let ⟨keyName, origName, config⟩ ← IO.ofExcept <| PackageDecl.loadFromEnv configEnv cfg.leanOpts
+  let baseName := if cfg.pkgName.isAnonymous then origName else cfg.pkgName
+  let pkg : Package := {
+    wsIdx := cfg.pkgIdx
+    baseName, keyName, origName, config
+    dir := cfg.pkgDir
+    relDir := cfg.relPkgDir
+    configFile := cfg.configFile
+    relConfigFile := cfg.relConfigFile
+    scope := cfg.scope
+    remoteUrl := cfg.remoteUrl
+  }
+  return (← pkg.loadFromEnv configEnv cfg.leanOpts, configEnv)

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

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Lake.Config.Workspace
-public import Lake.Config.LakefileConfig
 import Lean.DocString
 import Lake.DSL.AttributesCore
 
@@ -76,38 +75,39 @@ private def mkOrdTagMap
     return map.insert declName <| ← f declName
 
 /-- Load a `PackageDecl` from a configuration environment. -/
-private def PackageDecl.loadFromEnv
+public def PackageDecl.loadFromEnv
   (env : Environment) (opts := Options.empty)
 : Except String PackageDecl := do
   let declName ←
     match packageAttr.getAllEntries env |>.toList with
     | [] => error s!"configuration file is missing a `package` declaration"
-    | [keyName] => pure keyName
+    | [name] => pure name
     | _ => error s!"configuration file has multiple `package` declarations"
   evalConstCheck env opts _ declName
 
-/-- Load a Lake configuration from a configuration file's environment. -/
-public def LakefileConfig.loadFromEnv
-  (env : Environment) (opts : Options)
-: LogIO LakefileConfig := do
-
-  -- load package declaration
-  let pkgDecl ← IO.ofExcept <| PackageDecl.loadFromEnv env opts
-  let prettyName := pkgDecl.baseName.toString (escape := false)
-  let keyName := pkgDecl.keyName
+/--
+Load the optional elements of a `Package` from the Lean environment.
+This is done after loading its core configuration but before resolving
+its dependencies.
+-/
+public def Package.loadFromEnv
+  (self : Package) (env : Environment) (opts : Options)
+: LogIO Package := do
 
   -- load target, script, hook, and driver configurations
   let constTargetMap ← IO.ofExcept <| mkOrdTagMap env targetAttr fun name => do
     evalConstCheck env opts ConfigDecl name
   let targetDecls ← constTargetMap.toArray.mapM fun decl => do
-    if h : decl.pkg = keyName then
+    if h : decl.pkg = self.keyName then
       return .mk decl h
     else
-      error s!"target '{decl.name}' was defined in package '{decl.pkg}', \
-        but registered under '{keyName}'"
+      error s!"\
+        target '{decl.name}' was defined in package '{decl.pkg}', \
+        but registered under '{self.keyName}'"
   let targetDeclMap ← targetDecls.foldlM (init := {}) fun m decl => do
     if let some orig := m.get? decl.name then
-      error s!"{prettyName}: target '{decl.name}' was already defined as a '{orig.kind}', \
+      error s!"\
+        {self.prettyName}: target '{decl.name}' was already defined as a '{orig.kind}', \
         but then redefined as a '{decl.kind}'"
     else
       return m.insert decl.name (.mk decl rfl)
@@ -116,7 +116,8 @@ public def LakefileConfig.loadFromEnv
     if let some exeConfig := decl.config? LeanExe.configKind then
       let root := exeConfig.root
       if let some origExe := exeRoots.get? root then
-        error s!"{prettyName}: executable '{decl.name}' has the same root module '{root}' \
+        error s!"\
+          {self.prettyName}: executable '{decl.name}' has the same root module '{root}' \
           as executable '{origExe}'"
       else
         return exeRoots.insert root decl.name
@@ -124,78 +125,80 @@ public def LakefileConfig.loadFromEnv
       return exeRoots
   let defaultTargets ← defaultTargetAttr.getAllEntries env |>.mapM fun name =>
     if let some decl := constTargetMap.find? name then pure decl.name else
-      error s!"{prettyName}: package is missing target '{name}' marked as a default"
+      error s!"{self.prettyName}: package is missing target '{name}' marked as a default"
   let scripts ← mkTagMap env scriptAttr fun scriptName => do
-    let name := prettyName ++ "/" ++ scriptName.toString (escape := false)
+    let name := self.prettyName ++ "/" ++ scriptName.toString (escape := false)
     let fn ← IO.ofExcept <| evalConstCheck env opts ScriptFn scriptName
     return {name, fn, doc? := ← findDocString? env scriptName : Script}
   let defaultScripts ← defaultScriptAttr.getAllEntries env |>.mapM fun name =>
     if let some script := scripts.get? name then pure script else
-      error s!"{prettyName}: package is missing script '{name}' marked as a default"
+      error s!"{self.prettyName}: package is missing script '{name}' marked as a default"
   let postUpdateHooks ← postUpdateAttr.getAllEntries env |>.mapM fun name =>
     match evalConstCheck env opts PostUpdateHookDecl name with
     | .ok decl =>
-      if h : decl.pkg = keyName then
-        return OpaquePostUpdateHook.mk ⟨cast (by rw [h]) decl.fn⟩
+      if h : decl.pkg = self.keyName then
+        return OpaquePostUpdateHook.mk ⟨cast (by rw [h, keyName]) decl.fn⟩
       else
-        error s!"post-update hook was defined in '{decl.pkg}', but was registered in '{keyName}'"
+        error s!"post-update hook was defined in '{decl.pkg}', but was registered in '{self.keyName}'"
     | .error e => error e
   let depConfigs ← IO.ofExcept <| packageDepAttr.getAllEntries env |>.mapM fun name =>
     evalConstCheck env opts Dependency name
   let testDrivers ← testDriverAttr.getAllEntries env |>.mapM fun name =>
     if let some decl := constTargetMap.find? name then
-      return decl.name
+      pure decl.name
     else if scripts.contains name then
-      return name
+      pure name
     else
-      error s!"{prettyName}: package is missing script or target '{name}' marked as a test driver"
-  let testDriver ← id do
+      error s!"{self.prettyName}: package is missing script or target '{name}' marked as a test driver"
+  let testDriver ←
     if testDrivers.size > 1 then
-      error s!"{prettyName}: only one script, executable, or library can be tagged @[test_driver]"
+      error s!"{self.prettyName}: only one script, executable, or library can be tagged @[test_driver]"
     else if h : testDrivers.size > 0 then
-      if pkgDecl.config.testDriver.isEmpty then
-        return (testDrivers[0]'h |>.toString)
+      if self.config.testDriver.isEmpty then
+        pure (testDrivers[0]'h |>.toString)
       else
-        error s!"{prettyName}: cannot both set testDriver and use @[test_driver]"
+        error s!"{self.prettyName}: cannot both set testDriver and use @[test_driver]"
     else
-      return pkgDecl.config.testDriver
+      pure self.config.testDriver
   let lintDrivers ← lintDriverAttr.getAllEntries env |>.mapM fun name =>
     if let some decl := constTargetMap.find? name then
-      return decl.name
+      pure decl.name
     else if scripts.contains name then
-      return name
+      pure name
     else
-      error s!"{prettyName}: package is missing script or target '{name}' marked as a lint driver"
-  let lintDriver ← id do
+      error s!"{self.prettyName}: package is missing script or target '{name}' marked as a lint driver"
+  let lintDriver ←
     if lintDrivers.size > 1 then
-      error s!"{prettyName}: only one script or executable can be tagged @[lint_driver]"
+      error s!"{self.prettyName}: only one script or executable can be tagged @[lint_driver]"
     else if h : lintDrivers.size > 0 then
-      if pkgDecl.config.lintDriver.isEmpty then
-        return (lintDrivers[0]'h |>.toString)
+      if self.config.lintDriver.isEmpty then
+        pure (lintDrivers[0]'h |>.toString)
       else
-        error s!"{prettyName}: cannot both set lintDriver and use @[lint_driver]"
+        error s!"{self.prettyName}: cannot both set lintDriver and use @[lint_driver]"
     else
-      return pkgDecl.config.lintDriver
-
-  -- load facets
-  let facetDecls ← IO.ofExcept do
-    let mut decls : Array FacetDecl := #[]
-    for name in moduleFacetAttr.getAllEntries env do
-      let decl ← evalConstCheck env opts ModuleFacetDecl name
-      decls :=  decls.push {decl with config := decl.config.toFacetConfig}
-    for name in packageFacetAttr.getAllEntries env do
-      let decl ← evalConstCheck env opts PackageFacetDecl name
-      decls := decls.push  {decl with config := decl.config.toFacetConfig}
-    for name in libraryFacetAttr.getAllEntries env do
-      let decl ← evalConstCheck env opts LibraryFacetDecl name
-      decls := decls.push  {decl with config := decl.config.toFacetConfig}
-    return decls
+      pure self.config.lintDriver
 
   -- Fill in the Package
-  return {
-    pkgDecl, depConfigs, facetDecls,
-    targetDecls, targetDeclMap, defaultTargets,
-    scripts, defaultScripts,
-    testDriver, lintDriver,
-    postUpdateHooks,
+  return {self with
+    depConfigs, targetDecls, targetDeclMap
+    defaultTargets, scripts, defaultScripts
+    testDriver, lintDriver,  postUpdateHooks
   }
+
+/--
+Load module/package facets into a `Workspace` from a configuration environment.
+-/
+public def Workspace.addFacetsFromEnv
+  (env : Environment) (opts : Options) (self : Workspace)
+: Except String Workspace := do
+  let mut ws := self
+  for name in moduleFacetAttr.getAllEntries env do
+    let decl ← evalConstCheck env opts ModuleFacetDecl name
+    ws := ws.addModuleFacetConfig decl.config
+  for name in packageFacetAttr.getAllEntries env do
+    let decl ← evalConstCheck env opts PackageFacetDecl name
+    ws := ws.addPackageFacetConfig decl.config
+  for name in libraryFacetAttr.getAllEntries env do
+    let decl ← evalConstCheck env opts LibraryFacetDecl name
+    ws := ws.addLibraryFacetConfig decl.config
+  return ws

src/lake/Lake/Load/Manifest.lean

@@ -94,9 +94,6 @@ public structure PackageEntry where
 
 namespace PackageEntry
 
-@[inline] public def prettyName (entry : PackageEntry) : String :=
-  entry.name.toString (escape := false)
-
 public protected def toJson (entry : PackageEntry) : Json :=
   let fields := [
     ("name", toJson entry.name),

src/lake/Lake/Load/Materialize.lean

@@ -10,7 +10,6 @@ public import Lake.Config.Env
 public import Lake.Load.Manifest
 public import Lake.Config.Package
 import Lake.Util.Git
-import Lake.Util.IO
 import Lake.Reservoir
 
 open System Lean
@@ -88,8 +87,6 @@ def materializeGitRepo
     cloneGitPkg name repo url rev?
 
 public structure MaterializedDep where
-  /-- Absolute path to the materialized package. -/
-  pkgDir : FilePath
   /-- Path to the materialized package relative to the workspace's root directory. -/
   relPkgDir : FilePath
   /--
@@ -108,31 +105,16 @@ namespace MaterializedDep
 @[inline] public def name (self : MaterializedDep) : Name :=
   self.manifestEntry.name
 
-@[inline] public def prettyName (self : MaterializedDep) : String :=
-  self.manifestEntry.name.toString (escape := false)
-
 @[inline] public def scope (self : MaterializedDep) : String :=
   self.manifestEntry.scope
 
-/-- Path to the dependency's manfiest file (relative to `relPkgDir`). -/
-@[inline] public def relManifestFile? (self : MaterializedDep) : Option FilePath :=
+/-- Path to the dependency's configuration file (relative to `relPkgDir`). -/
+@[inline] public def manifestFile? (self : MaterializedDep) : Option FilePath :=
   self.manifestEntry.manifestFile?
 
-/-- Path to the dependency's manfiest file (relative to `relPkgDir`). -/
-@[inline] public def relManifestFile (self : MaterializedDep) : FilePath :=
-  self.relManifestFile?.getD defaultManifestFile
-
-/-- Absolute path to the dependency's manfiest file. -/
-@[inline] public def manifestFile (self : MaterializedDep) : FilePath :=
-  self.pkgDir / self.relManifestFile
-
 /-- Path to the dependency's configuration file (relative to `relPkgDir`). -/
-@[inline] public def relConfigFile (self : MaterializedDep) : FilePath :=
-  self.manifestEntry.configFile
-
-/-- Absolute path to the dependency's configuration file. -/
 @[inline] public def configFile (self : MaterializedDep) : FilePath :=
-  self.pkgDir / self.relConfigFile
+  self.manifestEntry.configFile
 
 public def fixedToolchain (self : MaterializedDep) : Bool :=
   match self.manifest? with
@@ -175,11 +157,10 @@ public def Dependency.materialize
   (lakeEnv : Env) (wsDir relPkgsDir relParentDir : FilePath)
 : LoggerIO MaterializedDep := do
   if let some src := dep.src? then
-    let sname := dep.name.toString (escape := false)
     match src with
     | .path dir =>
       let relPkgDir := relParentDir / dir
-      mkDep sname relPkgDir "" (.path relPkgDir)
+      mkDep (wsDir / relPkgDir) relPkgDir "" (.path relPkgDir)
     | .git url inputRev? subDir? => do
       let sname := dep.name.toString (escape := false)
       let repoUrl := Git.filterUrl? url |>.getD ""
@@ -227,19 +208,16 @@ public def Dependency.materialize
     | _ => error s!"{pkg.fullName}: Git source not found on Reservoir"
 where
   materializeGit name relPkgDir gitUrl remoteUrl inputRev? subDir? : LoggerIO MaterializedDep := do
-    let gitDir := wsDir / relPkgDir
-    let repo := GitRepo.mk gitDir
+    let pkgDir := wsDir / relPkgDir
+    let repo := GitRepo.mk pkgDir
     let gitUrl := lakeEnv.pkgUrlMap.find? dep.name |>.getD gitUrl
     materializeGitRepo name repo gitUrl inputRev?
     let rev ← repo.getHeadRevision
     let relPkgDir := if let some subDir := subDir? then relPkgDir / subDir else relPkgDir
-    mkDep name relPkgDir remoteUrl <| .git gitUrl rev inputRev? subDir?
-  @[inline] mkDep name relPkgDir remoteUrl src : LoggerIO MaterializedDep := do
-    let pkgDir := wsDir / relPkgDir
-    let some pkgDir ← resolvePath? pkgDir
-      | error s!"{name}: package directory not found: {pkgDir}"
+    mkDep pkgDir relPkgDir remoteUrl <| .git gitUrl rev inputRev? subDir?
+  @[inline] mkDep pkgDir relPkgDir remoteUrl src : LoggerIO MaterializedDep := do
     return {
-      pkgDir, relPkgDir, remoteUrl,
+      relPkgDir, remoteUrl
       manifest? :=  ← Manifest.load (pkgDir / defaultManifestFile) |>.toBaseIO
       manifestEntry := {name := dep.name, scope := dep.scope, inherited, src}
     }
@@ -253,9 +231,9 @@ public def PackageEntry.materialize
 : LoggerIO MaterializedDep :=
   match manifestEntry.src with
   | .path (dir := relPkgDir) .. =>
-    mkDep relPkgDir ""
+    mkDep (wsDir / relPkgDir) relPkgDir ""
   | .git (url := url) (rev := rev) (subDir? := subDir?) .. => do
-    let sname := manifestEntry.prettyName
+    let sname := manifestEntry.name.toString (escape := false)
     let relGitDir := relPkgsDir / sname
     let gitDir := wsDir / relGitDir
     let repo := GitRepo.mk gitDir
@@ -276,15 +254,12 @@ public def PackageEntry.materialize
       let url := lakeEnv.pkgUrlMap.find? manifestEntry.name |>.getD url
       cloneGitPkg sname repo url rev
     let relPkgDir := match subDir? with | .some subDir => relGitDir / subDir | .none => relGitDir
-    mkDep relPkgDir (Git.filterUrl? url |>.getD "")
+    mkDep gitDir relPkgDir (Git.filterUrl? url |>.getD "")
 where
-  @[inline] mkDep relPkgDir remoteUrl : LoggerIO MaterializedDep := do
-    let pkgDir := wsDir / relPkgDir
-    let some pkgDir ← resolvePath? pkgDir
-      | error s!"{manifestEntry.prettyName}: package directory not found: {pkgDir}"
+  @[inline] mkDep pkgDir relPkgDir remoteUrl : LoggerIO MaterializedDep := do
     let manifest? ← id do
       if let some manifestFile := manifestEntry.manifestFile? then
         Manifest.load (pkgDir / manifestFile) |>.toBaseIO
       else
         return .error (.noFileOrDirectory "" 0 "")
-    return {pkgDir, relPkgDir, remoteUrl, manifest?, manifestEntry}
+    return {relPkgDir, remoteUrl, manifest?, manifestEntry}

src/lake/Lake/Load/Package.lean

@@ -8,13 +8,10 @@ module
 prelude
 public import Lake.Load.Config
 public import Lake.Config.Package
-public import Lake.Config.LakefileConfig
 import Lake.Util.IO
 import Lake.Load.Lean
 import Lake.Load.Toml
 
-set_option doc.verso true
-
 /-! # Package Loader
 
 This module contains the main definitions to load a package
@@ -26,38 +23,6 @@ open System (FilePath)
 
 namespace Lake
 
-/--
-**For interal use only.**
-
-Constructs a package from the configuration defined in its Lake configuration file
-and the load configuaration.
--/
-public def mkPackage
-  (loadCfg : LoadConfig) (fileCfg : LakefileConfig) (wsIdx := loadCfg.pkgIdx)
-: Package :=
-  let {
-    pkgDir := dir, relPkgDir := relDir,
-    configFile, relConfigFile, relManifestFile,
-    scope, remoteUrl, ..} := loadCfg
-  let {
-    depConfigs, defaultTargets, scripts, defaultScripts, testDriver, lintDriver
-    -- destructing needed for type-correctness
-    pkgDecl, targetDecls, targetDeclMap, postUpdateHooks,
-    ..} := fileCfg
-  let {baseName, keyName, origName, config} := pkgDecl
-  {
-    wsIdx, baseName, keyName, origName, config
-    dir, relDir, configFile, relConfigFile, relManifestFile
-    scope, remoteUrl
-    depConfigs
-    targetDecls, targetDeclMap, defaultTargets
-    scripts, defaultScripts
-    testDriver, lintDriver
-    postUpdateHooks
-  }
-
-public theorem wsIdx_mkPackage : (mkPackage l f i).wsIdx = i := by rfl
-
 /--
 Return whether a configuration file with the given name
 and/or a supported extension exists.
@@ -84,25 +49,21 @@ public def realConfigFile (cfgFile : FilePath) : BaseIO FilePath := do
       resolvePath (cfgFile.addExtension "toml")
 
 /--
-**For internal use only.**
-
-Resolves a relative configuration file path in {lean}`cfg` and
-detects its configuration language (if necessary).
+Loads a Lake package configuration (either Lean or TOML).
+The resulting package does not yet include any dependencies.
 -/
-public def resolveConfigFile
+public def loadPackageCore
   (name : String) (cfg : LoadConfig)
-: LogIO {cfg : LoadConfig // cfg.configLang?.isSome} := do
-  if h : cfg.configLang?.isSome then
-    let some configFile ← resolvePath? cfg.configFile
-      | error s!"{name}: configuration file not found: {cfg.configFile}"
-    return ⟨{cfg with configFile}, h⟩
-  else if let some ext := cfg.relConfigFile.extension then
-    let some configFile ← resolvePath? cfg.configFile
-      | error s!"{name}: configuration file not found: {cfg.configFile}"
+: LogIO (Package × Option Environment) := do
+  if let some ext := cfg.relConfigFile.extension then
+    let cfg ←
+      if let some configFile ← resolvePath? cfg.configFile then
+        pure {cfg with configFile}
+      else error s!"{name}: configuration file not found: {cfg.configFile}"
     match ext with
-    | "lean" => return ⟨{cfg with configFile, configLang? := some .lean}, rfl⟩
-    | "toml" => return ⟨{cfg with configFile, configLang? := some .toml}, rfl⟩
-    | _ => error s!"{name}: configuration has unsupported file extension: {configFile}"
+    | "lean" => (·.map id some) <$> loadLeanConfig cfg
+    | "toml" => ((·,none)) <$> loadTomlConfig cfg
+    | _ => error s!"{name}: configuration has unsupported file extension: {cfg.configFile}"
   else
     let relLeanFile := cfg.relConfigFile.addExtension "lean"
     let relTomlFile := cfg.relConfigFile.addExtension "toml"
@@ -111,28 +72,18 @@ public def resolveConfigFile
     if let some configFile ← resolvePath? leanFile then
       if (← tomlFile.pathExists) then
         logInfo s!"{name}: {relLeanFile} and {relTomlFile} are both present; using {relLeanFile}"
-      return ⟨{cfg with configFile, relConfigFile := relLeanFile, configLang? := some .lean}, rfl⟩
-    else if let some configFile ← resolvePath? tomlFile then
-      return ⟨{cfg with configFile, relConfigFile := relTomlFile, configLang? := some .toml}, rfl⟩
+       let cfg := {cfg with configFile, relConfigFile := relLeanFile}
+      let (pkg, env) ← loadLeanConfig cfg
+      return (pkg, some env)
     else
-      error s!"{name}: no configuration file with a supported extension:\n{leanFile}\n{tomlFile}"
-
-/--
-**For internal use only.**
-Reads the configuration of a Lake configuration file.
-
-The load configuration {lean}`cfg` is assumed to already have an absolute path in
-{lean}`cfg.configFile` and that the proper configuratin langauge for it is in
-{lean}`cfg.configLang?`. This can be ensured through {lean}`resolveConfigFile`.
--/
-public def loadConfigFile (cfg : LoadConfig) (h : cfg.configLang?.isSome) : LogIO LakefileConfig := do
-  match cfg.configLang?.get h with
-  | .lean => loadLeanConfig cfg
-  | .toml => loadTomlConfig cfg
+      if let some configFile ← resolvePath? tomlFile then
+        let cfg := {cfg with configFile, relConfigFile := relTomlFile}
+        let pkg ← loadTomlConfig cfg
+        return (pkg, none)
+      else
+        error s!"{name}: no configuration file with a supported extension:\n{leanFile}\n{tomlFile}"
 
 /-- Loads a Lake package as a single independent object (without dependencies). -/
-public def loadPackage (cfg : LoadConfig) : LogIO Package := do
-  Lean.searchPathRef.set cfg.lakeEnv.leanSearchPath
-  let ⟨cfg, h⟩ ← resolveConfigFile "[root]" cfg
-  let fileCfg ← loadConfigFile cfg h
-  return mkPackage cfg fileCfg
+public def loadPackage (config : LoadConfig) : LogIO Package := do
+  Lean.searchPathRef.set config.lakeEnv.leanSearchPath
+  (·.1) <$> loadPackageCore "[root]" config