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=''"

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/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/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,7 +217,6 @@ Simplify `code`
 -/
 partial def simp (code : Code .pure) : SimpM (Code .pure) := withIncRecDepth do
   incVisited
-  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,13 +444,9 @@ 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
 
-/--
-Record a check-in for the `LEAN_CHECK_SYSTEM_INTERVAL_MS` monitoring.
-When that env var is set, warns on stderr if too much CPU time has elapsed since
-the last check-in from either the C++ `check_system` or this function.
--/
-@[extern "lean_check_system_interval"]
-opaque checkSystemInterval (componentName : @& String) : BaseIO Unit
+/-- 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
@@ -464,17 +458,10 @@ Like `checkSystem` but without the global heartbeat check, for callers that have
 heartbeat tracking (e.g. `SynthInstance`).
  -/
 @[inline] def checkInterrupted : CoreM Unit := do
-  checkSystemInterval "Lean elaborator"
   if let some tk := (← read).cancelTk? then
     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/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)

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/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/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/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/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/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/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/Load/Resolve.lean

@@ -220,7 +220,7 @@ private structure ToolchainCandidate where
   fixed : Bool := false
 
 private structure ToolchainState where
-  /-- The name of dependency which provided the current candidate toolchain. -/
+  /-- The name of depedency which provided the current candidate toolchain. -/
   src : Name
   /-- The current candidate toolchain version (if any). -/
   tc? : Option ToolchainVer

src/runtime/CMakeLists.txt

@@ -33,6 +33,7 @@ set(
   uv/dns.cpp
   uv/system.cpp
   uv/signal.cpp
+  openssl.cpp
 )
 if(USE_MIMALLOC)
   list(APPEND RUNTIME_OBJS ${LEAN_BINARY_DIR}/../mimalloc/src/mimalloc/src/static.c)

src/runtime/interrupt.cpp

@@ -5,15 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <limits>
-#include <cstdlib>
-#include <ctime>
-#include <execinfo.h>
-#ifdef __linux__
-#include <unistd.h>
-#include <sys/ioctl.h>
-#include <linux/perf_event.h>
-#include <sys/syscall.h>
-#endif
 #include "runtime/thread.h"
 #include "runtime/interrupt.h"
 #include "runtime/exception.h"
@@ -25,124 +16,6 @@ namespace lean {
 LEAN_THREAD_VALUE(size_t, g_max_heartbeat, 0);
 LEAN_THREAD_VALUE(size_t, g_heartbeat, 0);
 
-// --- check_system interval monitoring ---
-//
-// Two modes (mutually exclusive, instruction count takes priority):
-//
-// 1. LEAN_CHECK_SYSTEM_INTERVAL_INSN=N — warn if more than N million retired
-//    instructions elapse between consecutive check_system calls. Uses
-//    perf_event_open (Linux only). Deterministic and load-independent.
-//
-// 2. LEAN_CHECK_SYSTEM_INTERVAL_MS=N — warn if more than N milliseconds of
-//    CPU time elapse. Uses CLOCK_THREAD_CPUTIME_ID. Subject to CPU frequency
-//    scaling and machine load.
-
-// 0 = disabled
-static uint64_t g_check_system_interval_threshold = 0;
-static bool g_check_system_interval_initialized = false;
-// false = CPU time (ns), true = instructions
-static bool g_check_system_use_insn = false;
-
-#ifdef __linux__
-LEAN_THREAD_VALUE(int, g_perf_fd, -1);
-
-static int perf_open_insn_counter() {
-    struct perf_event_attr pe = {};
-    pe.type = PERF_TYPE_HARDWARE;
-    pe.size = sizeof(pe);
-    pe.config = PERF_COUNT_HW_INSTRUCTIONS;
-    pe.disabled = 0;
-    pe.exclude_kernel = 1;
-    pe.exclude_hv = 1;
-    // pid=0, cpu=-1: count calling thread on any CPU
-    return syscall(SYS_perf_event_open, &pe, 0, -1, -1, 0);
-}
-
-static uint64_t read_insn_counter() {
-    int fd = g_perf_fd;
-    if (fd < 0) {
-        fd = perf_open_insn_counter();
-        g_perf_fd = fd;
-        if (fd < 0) return 0; // perf not available
-    }
-    uint64_t count = 0;
-    if (read(fd, &count, sizeof(count)) != sizeof(count))
-        return 0;
-    return count;
-}
-#else
-static uint64_t read_insn_counter() { return 0; }
-#endif
-
-static void init_check_system_interval() {
-    if (g_check_system_interval_initialized) return;
-    g_check_system_interval_initialized = true;
-    if (const char * env = std::getenv("LEAN_CHECK_SYSTEM_INTERVAL_INSN")) {
-        uint64_t millions = std::atoll(env);
-        if (millions > 0) {
-            g_check_system_interval_threshold = millions * 1000000ULL;
-            g_check_system_use_insn = true;
-            return;
-        }
-    }
-    if (const char * env = std::getenv("LEAN_CHECK_SYSTEM_INTERVAL_MS")) {
-        unsigned ms = std::atoi(env);
-        if (ms > 0) {
-            g_check_system_interval_threshold = static_cast<uint64_t>(ms) * 1000000ULL; // ms -> ns
-            g_check_system_use_insn = false;
-        }
-    }
-}
-
-static uint64_t thread_cpu_time_ns() {
-    struct timespec ts;
-    clock_gettime(CLOCK_THREAD_CPUTIME_ID, &ts);
-    return static_cast<uint64_t>(ts.tv_sec) * 1000000000ULL + static_cast<uint64_t>(ts.tv_nsec);
-}
-
-static uint64_t current_counter() {
-    return g_check_system_use_insn ? read_insn_counter() : thread_cpu_time_ns();
-}
-
-// Thread-local: last counter value when check_system was called on this thread.
-LEAN_THREAD_VALUE(uint64_t, g_last_check_system_counter, 0);
-
-static void check_system_interval(char const * component_name) {
-    init_check_system_interval();
-    uint64_t threshold = g_check_system_interval_threshold;
-    if (threshold > 0) {
-        uint64_t now = current_counter();
-        uint64_t last = g_last_check_system_counter;
-        g_last_check_system_counter = now;
-        if (last != 0 && now > last) {
-            uint64_t elapsed = now - last;
-            if (elapsed > threshold) {
-                if (g_check_system_use_insn) {
-                    fprintf(stderr,
-                        "[check_system] WARNING: %llu M instructions since last check_system call "
-                        "(component: %s)\n",
-                        (unsigned long long)(elapsed / 1000000), component_name);
-                } else {
-                    fprintf(stderr,
-                        "[check_system] WARNING: %llu ms CPU time since last check_system call "
-                        "(component: %s)\n",
-                        (unsigned long long)(elapsed / 1000000), component_name);
-                }
-                void * bt_buf[64];
-                int nptrs = backtrace(bt_buf, 64);
-                backtrace_symbols_fd(bt_buf, nptrs, 2); // fd 2 = stderr
-                // Reset counter after printing to avoid backtrace overhead cascading
-                g_last_check_system_counter = current_counter();
-            }
-        }
-    }
-}
-
-extern "C" LEAN_EXPORT obj_res lean_check_system_interval(b_lean_obj_arg component_name) {
-    check_system_interval(lean_string_cstr(component_name));
-    return lean_io_result_mk_ok(lean_box(0));
-}
-
 extern "C" LEAN_EXPORT obj_res lean_internal_get_default_max_heartbeat() {
 #ifdef LEAN_DEFAULT_MAX_HEARTBEAT
     return lean_box(LEAN_DEFAULT_MAX_HEARTBEAT);
@@ -198,7 +71,6 @@ void check_interrupted() {
 }
 
 void check_system(char const * component_name, bool do_check_interrupted) {
-    check_system_interval(component_name);
     check_stack(component_name);
     check_memory(component_name);
     if (do_check_interrupted) {

src/runtime/openssl.cpp

@@ -0,0 +1,42 @@
+/*
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Sofia Rodrigues
+*/
+#include "runtime/openssl.h"
+
+#ifndef LEAN_EMSCRIPTEN
+#include <openssl/opensslv.h>
+#include <openssl/err.h>
+#include <openssl/ssl.h>
+
+namespace lean {
+
+void initialize_openssl() {
+    if (OPENSSL_init_ssl(0, nullptr) != 1) {
+        lean_internal_panic("failed to initialize OpenSSL");
+    }
+}
+
+void finalize_openssl() {}
+
+}
+
+extern "C" LEAN_EXPORT lean_obj_res lean_openssl_version(lean_obj_arg o) {
+    return lean_unsigned_to_nat(OPENSSL_VERSION_NUMBER);
+}
+
+#else
+
+namespace lean {
+
+void initialize_openssl() {}
+void finalize_openssl() {}
+
+}
+
+extern "C" LEAN_EXPORT lean_obj_res lean_openssl_version(lean_obj_arg o) {
+    return lean_box(0);
+}
+
+#endif

src/runtime/openssl.h

@@ -0,0 +1,9 @@
+/*
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Sofia Rodrigues
+*/
+#pragma once
+#include <lean/lean.h>
+
+extern "C" LEAN_EXPORT lean_obj_res lean_openssl_version(lean_obj_arg);