refactor: remove Cbv.mkAppNS alias, use Sym.Internal.mkAppNS directly

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

.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 openssl: git: zip: unzip: diffutils: binutils: tree: zstd tar:"
+          pacboy: "make: python: cmake clang ccache gmp libuv 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 openssl
+          brew install ccache tree zstd coreutils gmp libuv
         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 libssl-dev:i386 pkgconf:i386
+          sudo apt-get install -y gcc-multilib g++-multilib ccache libuv1-dev:i386 pkgconf:i386
         if: matrix.cmultilib
       - name: Restore Cache
         id: restore-cache

doc/make/index.md

@@ -9,7 +9,6 @@ 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 mingw-w64-clang-x86_64-openssl 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 git unzip diffutils binutils
 ```
 
 You should now be able to run these commands:

doc/make/osx-10.9.md

@@ -32,13 +32,12 @@ following to use `g++`.
 cmake -DCMAKE_CXX_COMPILER=g++ ...
 ```
 
-## Required Packages: CMake, GMP, libuv, OpenSSL, pkgconf
+## Required Packages: CMake, GMP, libuv, 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 libssl-dev cmake ccache clang pkgconf
+sudo apt-get install git libgmp-dev libuv1-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 openssl openssl.dev
+            cmake gmp libuv ccache pkg-config
             llvmPackages.bintools  # wrapped lld
             llvmPackages.llvm  # llvm-symbolizer for asan/lsan
             gdb
@@ -34,21 +34,7 @@
           hardeningDisable = [ "all" ];
           # more convenient `ctest` output
           CTEST_OUTPUT_ON_FAILURE = 1;
-        } // 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 {
+        } // pkgs.lib.optionalAttrs pkgs.stdenv.isLinux {
           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
@@ -67,15 +53,13 @@
             };
             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/OPENSSL) as in
+# run from root build directory (from inside nix-shell or otherwise defining GLIBC/ZLIB/GMP) as in
 # ```
 # eval cmake ../.. $(../../script/prepare-llvm-linux.sh ~/Downloads/lean-llvm-x86_64-linux-gnu.tar.zst)
 # ```
@@ -42,8 +42,6 @@ $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
@@ -59,7 +57,6 @@ 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:-}'"
@@ -77,8 +74,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 -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'"
+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'"
 # do not set `LEAN_CC` for tests
 echo -n " -DLEAN_TEST_VARS=''"

script/prepare-llvm-macos.sh

@@ -10,7 +10,6 @@ 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
@@ -42,7 +41,6 @@ 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:-}'"
@@ -50,8 +48,7 @@ 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/
-  gcp $OPENSSL/lib/libssl.a $OPENSSL/lib/libcrypto.a stage1/lib/
-  echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp -luv -lssl -lcrypto'"
+  echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp -luv'"
 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,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/
+cp /clang64/lib/lib{m,bcrypt,mingw32,moldname,mingwex,msvcrt,pthread,advapi32,shell32,user32,kernel32,ucrtbase,psapi,iphlpapi,userenv,ws2_32,dbghelp,ole32,icu}.* /clang64/lib/libgmp.a /clang64/lib/libuv.a llvm/lib/lib{c++,c++abi,unwind}.a stage1/lib/
 echo -n " -DLEAN_STANDALONE=ON"
 echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang.exe -DCMAKE_C_COMPILER_WORKS=1 -DCMAKE_CXX_COMPILER=$PWD/llvm/bin/clang++.exe -DCMAKE_CXX_COMPILER_WORKS=1 -DLEAN_CXX_STDLIB='-lc++ -lc++abi'"
 echo -n " -DSTAGE0_CMAKE_C_COMPILER=clang -DSTAGE0_CMAKE_CXX_COMPILER=clang++"
 echo -n " -DLEAN_EXTRA_CXX_FLAGS='--sysroot $PWD/llvm -idirafter /clang64/include/'"
 echo -n " -DLEANC_INTERNAL_FLAGS='--sysroot ROOT -nostdinc -isystem ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang.exe"
-echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='--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'"
+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'"
 # do not set `LEAN_CC` for tests
 echo -n " -DLEAN_TEST_VARS=''"

src/CMakeLists.txt

@@ -357,28 +357,6 @@ 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)
@@ -494,17 +472,6 @@ 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)
@@ -796,7 +763,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/Lean/Meta/Sym/AbstractS.lean

@@ -97,4 +97,16 @@ 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,4 +189,48 @@ 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

@@ -27,6 +27,10 @@ applications, foralls, lambdas, and let-bindings, classifying each argument as a
 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 (applied only in type positions)
 
 - **Eta**: `fun x => f x` → `f`
@@ -39,7 +43,19 @@ Types and instances receive targeted reductions.
 
 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.
+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.
+
+Inside types, both cases are strict: resynthesis failure is reported as an issue.
 
 ## Two caches
 
@@ -246,23 +262,81 @@ where
     else
       withReader (fun ctx => { ctx with insideType := true }) <| canon e
 
-  canonInst (e : Expr) : CanonM Expr := do
-    if let some inst := (← get).canon.cacheInsts.get? e then
-      checkDefEqInst e inst
+  /--
+  Canonicalize `e : type` where `e` is an instance by trying to resynthesize `type`.
+  We report an issue if the instance cannot be resynthesized.
+  -/
+  canonInstCore (e : Expr) (type : Expr) : CanonM Expr := do
+    let some inst ← Sym.synthInstance? type |
+      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) : 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'
+
+  /-- `withCaching` + `canonInst'` -/
+  canonInst (e : Expr) : CanonM Expr := withCaching e do
+    canonInst' e
+
+  /--
+  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
+      canonInstCore h prop'
     else
       /-
-      We normalize the type to make sure `OfNat (Fin (2+1)) 1` and `OfNat (Fin 3) 1` will produce
-      the same instances.
+      **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`.
       -/
-      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
+      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
+      canonInstCore inst type
+    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
 
   canonLambda (e : Expr) : CanonM Expr := do
     if (← read).insideType then
@@ -295,54 +369,50 @@ where
       mkLetFVars (generalizeNondepLet := false) fvars (← canon (e.instantiateRev fvars))
 
   canonAppDefault (e : Expr) : CanonM Expr := e.withApp fun f args => do
-    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'
+    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
     else
-      let mut modified := false
-      let args ← if f.isConstOf ``OfNat.ofNat then
-        let some args ← normOfNatArgs? args | pure args
+      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'
         modified := true
-        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
+    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
@@ -412,7 +482,7 @@ where
       return e
 
 /--
-Returns `true` if `shouldCannon pinfos i arg` is not `.visit`.
+Returns `true` if `shouldCanon 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

src/Lean/Meta/Sym/InstantiateS.lean

@@ -86,22 +86,8 @@ 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
 
-/-- `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 :=
+/-- Internal variant of `betaRevS` that runs in `AlphaShareBuilderM`. -/
+private partial def betaRevS' (f : Expr) (revArgs : Array Expr) : AlphaShareBuilderM Expr :=
   if revArgs.size == 0 then
     return f
   else
@@ -173,7 +159,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!
@@ -215,4 +201,18 @@ 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,8 +152,6 @@ 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/Main.lean

@@ -283,6 +283,7 @@ 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,9 +24,6 @@ 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/Runtime.lean

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

src/runtime/CMakeLists.txt

@@ -33,7 +33,6 @@ 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/openssl.cpp

@@ -1,42 +0,0 @@
-/*
-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

@@ -1,9 +0,0 @@
-/*
-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);

tests/elab/grind_indexmap_trace.lean

@@ -149,7 +149,7 @@ info: Try these:
   [apply] ⏎
     instantiate only [= mem_indices_of_mem, insert]
     instantiate only [=_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos]
-    cases #bcd5
+    cases #bd4f
     · cases #54dd
       · instantiate only
       · instantiate only
@@ -164,7 +164,7 @@ info: Try these:
         · instantiate only
           instantiate only [= HashMap.contains_insert]
   [apply] finish only [= mem_indices_of_mem, insert, =_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos,
-    = HashMap.contains_insert, #bcd5, #54dd, #2eb4, #cc2e]
+    = HashMap.contains_insert, #bd4f, #54dd, #2eb4, #cc2e]
 -/
 #guard_msgs in
 example (m : IndexMap α β) (a a' : α) (b : β) :
@@ -176,7 +176,7 @@ info: Try these:
   [apply] ⏎
     instantiate only [= mem_indices_of_mem, insert]
     instantiate only [=_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos]
-    cases #bcd5
+    cases #bd4f
     · cases #54dd
       · instantiate only
       · instantiate only
@@ -191,7 +191,7 @@ info: Try these:
         · instantiate only
           instantiate only [= HashMap.contains_insert]
   [apply] finish only [= mem_indices_of_mem, insert, =_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos,
-    = HashMap.contains_insert, #bcd5, #54dd, #2eb4, #cc2e]
+    = HashMap.contains_insert, #bd4f, #54dd, #2eb4, #cc2e]
 -/
 #guard_msgs in
 example (m : IndexMap α β) (a a' : α) (b : β) :
@@ -203,7 +203,7 @@ example (m : IndexMap α β) (a a' : α) (b : β) :
   grind =>
     instantiate only [= mem_indices_of_mem, insert]
     instantiate only [=_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos]
-    cases #bcd5
+    cases #bd4f
     · cases #54dd
       · instantiate only
       · instantiate only
@@ -223,7 +223,7 @@ example (m : IndexMap α β) (a a' : α) (b : β) :
   grind =>
     instantiate only [= mem_indices_of_mem, insert]
     instantiate only [=_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos]
-    cases #bcd5
+    cases #bd4f
     · cases #54dd
       · instantiate only
       · instantiate only

tests/elab/grind_prop_inst.lean

@@ -0,0 +1,55 @@
+
+opaque f [Nonempty α] (a : α) : α := a
+
+-- Note: The following test should not generate any issues.
+/--
+error: `grind` failed
+case grind
+α : Sort u_1
+a b : α
+h : ¬f a = b
+⊢ False
+[grind] Goal diagnostics
+  [facts] Asserted facts
+    [prop] ¬f a = b
+  [eqc] True propositions
+    [prop] Nonempty α
+  [eqc] False propositions
+    [prop] f a = b
+-/
+#guard_msgs in
+example (a b : α) :
+    (haveI : Nonempty α := ⟨a⟩
+     f a)
+    = b := by
+  grind
+
+/--
+trace: [grind.assert] @Eq α c (@f α (@Lean.Grind.nestedProof (Nonempty α) (@Nonempty.intro α a)) a)
+[grind.assert] Not (@Eq α c (@f α (@Lean.Grind.nestedProof (Nonempty α) (@Nonempty.intro α b)) a))
+-/
+#guard_msgs in
+set_option trace.grind.assert true in
+set_option pp.proofs true in
+set_option pp.explicit true in
+example (a b c : α) :
+    c = (haveI : Nonempty α := ⟨a⟩; f a)
+    →
+    c = (haveI : Nonempty α := ⟨b⟩; f a) := by
+  grind
+
+-- Must preserve `Grind.nestedProof`
+/--
+trace: [grind.assert] Nonempty α
+[grind.assert] @Eq α c (@f α (@Lean.Grind.nestedProof (Nonempty α) inst) a)
+[grind.assert] Not (@Eq α c (@f α (@Lean.Grind.nestedProof (Nonempty α) inst) a))
+-/
+#guard_msgs in
+set_option trace.grind.assert true in
+set_option pp.proofs true in
+set_option pp.explicit true in
+example [Nonempty α] (a b c : α) :
+    c = (haveI : Nonempty α := ⟨a⟩; f a)
+    →
+    c = (haveI : Nonempty α := ⟨b⟩; f a) := by
+  grind

tests/elab/openssl.lean

@@ -1,6 +0,0 @@
-import Lean.Runtime
-
--- Non-emscripten build: expect the major version of OpenSSL (3)
-/-- info: 3 -/
-#guard_msgs in
-#eval if !System.Platform.isEmscripten then Lean.openSSLVersion >>> 28 else 3