feat: adapt non-equality theorems in mkTheoremFromDecl

`mkTheoremFromDecl` and `mkTheoremFromExpr` now handle theorems whose
conclusion is not an equality:
- `¬ p` → adapted to `p = False` via `eq_false`
- `p ↔ q` → adapted to `p = q` via `propext`
- `p` (proposition) → adapted to `p = True` via `eq_true`

This enables `Sym.simp` to use hypotheses like `h : p x` as rewrite
rules that replace `p x` with `True`.

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

.github/workflows/build-template.yml

@@ -33,7 +33,7 @@ jobs:
         include: ${{fromJson(inputs.config)}}
       # complete all jobs
       fail-fast: false
-    runs-on: ${{ endsWith(matrix.os, '-with-cache') && fromJSON(format('["{0}", "nscloud-git-mirror-5gb"]', matrix.os)) || matrix.os }}
+    runs-on: ${{ endsWith(matrix.os, '-with-cache') && fromJSON(format('["{0}", "nscloud-git-mirror-1gb"]', matrix.os)) || matrix.os }}
     defaults:
       run:
         shell: ${{ matrix.shell || 'nix develop -c bash -euxo pipefail {0}' }}
@@ -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

.github/workflows/check-empty-pr.yml

@@ -1,29 +0,0 @@
-name: Check for empty PR
-
-on:
-  merge_group:
-  pull_request:
-
-jobs:
-  check-empty-pr:
-    runs-on: ubuntu-latest
-    steps:
-    - uses: actions/checkout@v6
-      with:
-        ref: ${{ github.event_name == 'pull_request' && github.event.pull_request.head.sha || github.sha }}
-        fetch-depth: 0
-        filter: tree:0
-
-    - name: Check for empty diff
-      run: |
-        if [[ "${{ github.event_name }}" == "pull_request" ]]; then
-          base=$(git merge-base "origin/${{ github.base_ref }}" HEAD)
-        else
-          base=$(git rev-parse HEAD^1)
-        fi
-        if git diff --quiet "$base" HEAD --; then
-          echo "This PR introduces no changes compared to its base branch." | tee "$GITHUB_STEP_SUMMARY"
-          echo "It may be a duplicate of an already-merged PR." | tee -a "$GITHUB_STEP_SUMMARY"
-          exit 1
-        fi
-      shell: bash

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 -Wl,--disable-new-dtags,-rpath,ROOT/lib -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,7 +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/
-  echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp -luv $OPENSSL/lib/libssl.a $OPENSSL/lib/libcrypto.a'"
+  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=''"

script/release_checklist.py

@@ -236,7 +236,7 @@ def parse_version(version_str):
 def is_version_gte(version1, version2):
     """Check if version1 >= version2, including proper handling of release candidates."""
     # Check if version1 is a nightly toolchain
-    if version1.startswith("leanprover/lean4:nightly-") or version1.startswith("leanprover/lean4-nightly:"):
+    if version1.startswith("leanprover/lean4:nightly-"):
         return False
     return parse_version(version1) >= parse_version(version2)
 

src/CMakeLists.txt

@@ -356,48 +356,6 @@ if(NOT LEAN_STANDALONE)
   string(APPEND LEAN_EXTRA_LINKER_FLAGS " ${LIBUV_LDFLAGS}")
 endif()
 
-# OpenSSL
-if("${CMAKE_SYSTEM_NAME}" MATCHES "Emscripten")
-  # Only on WebAssembly we compile OpenSSL ourselves
-  set(OPENSSL_EMSCRIPTEN_FLAGS "${EMSCRIPTEN_SETTINGS}")
-
-  # OpenSSL needs to be configured for Emscripten using their configuration system
-  ExternalProject_add(openssl
-    PREFIX openssl
-    GIT_REPOSITORY https://github.com/openssl/openssl
-    # Sync version with flake.nix if applicable
-    GIT_TAG openssl-3.0.15
-    CONFIGURE_COMMAND <SOURCE_DIR>/Configure linux-generic32 no-shared no-dso no-engine no-tests --prefix=<INSTALL_DIR> CC=${CMAKE_C_COMPILER} CXX=${CMAKE_CXX_COMPILER} AR=${CMAKE_AR} CFLAGS=${OPENSSL_EMSCRIPTEN_FLAGS}
-    BUILD_COMMAND emmake make -j
-    INSTALL_COMMAND emmake make install_sw
-    BUILD_IN_SOURCE ON)
-  set(OPENSSL_INCLUDE_DIR "${CMAKE_BINARY_DIR}/openssl/include")
-  set(OPENSSL_CRYPTO_LIBRARY "${CMAKE_BINARY_DIR}/openssl/lib/libcrypto.a")
-  set(OPENSSL_SSL_LIBRARY "${CMAKE_BINARY_DIR}/openssl/lib/libssl.a")
-  set(OPENSSL_LIBRARIES "${OPENSSL_SSL_LIBRARY} ${OPENSSL_CRYPTO_LIBRARY}")
-else()
-  find_package(OpenSSL 3 REQUIRED)
-  set(OPENSSL_LIBRARIES ${OPENSSL_SSL_LIBRARY} ${OPENSSL_CRYPTO_LIBRARY})
-endif()
-include_directories(${OPENSSL_INCLUDE_DIR})
-string(JOIN " " OPENSSL_LIBRARIES_STR ${OPENSSL_LIBRARIES})
-string(APPEND LEANSHARED_LINKER_FLAGS " ${OPENSSL_LIBRARIES_STR}")
-
-if(NOT LEAN_STANDALONE)
-  string(APPEND LEAN_EXTRA_LINKER_FLAGS " ${OPENSSL_LIBRARIES_STR}")
-endif()
-
-if(CMAKE_SYSTEM_NAME MATCHES "Linux")
-  string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,--disable-new-dtags,-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)
@@ -772,9 +730,9 @@ if(STAGE GREATER 1)
   endif()
 else()
   add_subdirectory(runtime)
-  if("${CMAKE_SYSTEM_NAME}" MATCHES "Emscripten")
-    add_dependencies(leanrt libuv openssl)
-    add_dependencies(leanrt_initial-exec libuv openssl)
+  if(CMAKE_SYSTEM_NAME MATCHES "Emscripten")
+    add_dependencies(leanrt libuv)
+    add_dependencies(leanrt_initial-exec libuv)
   endif()
 
   add_subdirectory(util)

src/Init/Data/BEq.lean

@@ -66,8 +66,3 @@ theorem BEq.neq_of_beq_of_neq [BEq α] [PartialEquivBEq α] {a b c : α} :
 instance (priority := low) [BEq α] [LawfulBEq α] : EquivBEq α where
   symm h := beq_iff_eq.2 <| Eq.symm <| beq_iff_eq.1 h
   trans hab hbc := beq_iff_eq.2 <| (beq_iff_eq.1 hab).trans <| beq_iff_eq.1 hbc
-
-theorem equivBEq_of_iff_apply_eq [BEq α] (f : α → β) (hf : ∀ a b, a == b ↔ f a = f b) : EquivBEq α where
-  rfl := by simp [hf]
-  symm := by simp [hf, eq_comm]
-  trans hab hbc := (hf _ _).2 (Eq.trans ((hf _ _).1 hab) ((hf _ _).1 hbc))

src/Init/Data/String/Basic.lean

@@ -852,10 +852,6 @@ theorem Slice.rawEndPos_copy {s : Slice} : s.copy.rawEndPos = s.rawEndPos := by
 theorem copy_toSlice {s : String} : s.toSlice.copy = s := by
   simp [← toByteArray_inj, Slice.toByteArray_copy, ← size_toByteArray]
 
-@[simp]
-theorem copy_comp_toSlice : String.Slice.copy ∘ String.toSlice = id := by
-  ext; simp
-
 theorem Slice.getUTF8Byte_eq_getUTF8Byte_copy {s : Slice} {p : Pos.Raw} {h : p < s.rawEndPos} :
     s.getUTF8Byte p h = s.copy.getUTF8Byte p (by simpa) := by
   simp [getUTF8Byte, String.getUTF8Byte, toByteArray_copy, ByteArray.getElem_extract]

src/Init/Data/String/Iter.lean

@@ -6,5 +6,29 @@ Authors: Markus Himmel
 module
 
 prelude
-public import Init.Data.String.Iter.Basic
-public import Init.Data.String.Iter.Intercalate
+public import Init.Data.Iterators.Combinators.FilterMap
+public import Init.Data.Iterators.Consumers.Collect
+
+set_option doc.verso true
+
+namespace Std
+
+/--
+Convenience function for turning an iterator into a list of strings, provided the output of the
+iterator implements {name}`ToString`.
+-/
+@[inline]
+public abbrev Iter.toStringList {α β : Type} [Iterator α Id β] [ToString β]
+    (it : Iter (α := α) β) : List String :=
+  it.map toString |>.toList
+
+/--
+Convenience function for turning an iterator into an array of strings, provided the output of the
+iterator implements {name}`ToString`.
+-/
+@[inline]
+public abbrev Iter.toStringArray {α β : Type} [Iterator α Id β] [ToString β]
+    (it : Iter (α := α) β) : Array String :=
+  it.map toString |>.toArray
+
+end Std

src/Init/Data/String/Iter/Basic.lean

@@ -1,34 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-module
-
-prelude
-public import Init.Data.Iterators.Combinators.FilterMap
-public import Init.Data.Iterators.Consumers.Collect
-
-set_option doc.verso true
-
-namespace Std
-
-/--
-Convenience function for turning an iterator into a list of strings, provided the output of the
-iterator implements {name}`ToString`.
--/
-@[inline]
-public abbrev Iter.toStringList {α β : Type} [Iterator α Id β] [ToString β]
-    (it : Iter (α := α) β) : List String :=
-  it.map toString |>.toList
-
-/--
-Convenience function for turning an iterator into an array of strings, provided the output of the
-iterator implements {name}`ToString`.
--/
-@[inline]
-public abbrev Iter.toStringArray {α β : Type} [Iterator α Id β] [ToString β]
-    (it : Iter (α := α) β) : Array String :=
-  it.map toString |>.toArray
-
-end Std

src/Init/Data/String/Iter/Intercalate.lean

@@ -1,36 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Julia Markus Himmel
--/
-module
-
-prelude
-public import Init.Data.Iterators.Combinators.Monadic.FilterMap
-public import Init.Data.String.Basic
-import Init.Data.String.Slice
-
-set_option doc.verso true
-
-namespace Std
-
-/--
-Appends all the elements in the iterator, in order.
--/
-public def Iter.joinString {α β : Type} [Iterator α Id β] [IteratorLoop α Id Id] [ToString β]
-    (it : Std.Iter (α := α) β) : String :=
-  (it.map toString).fold (init := "") (· ++ ·)
-
-/--
-Appends the elements of the iterator into a string, placing the separator {name}`s` between them.
--/
-@[inline]
-public def Iter.intercalateString {α β : Type} [Iterator α Id β] [IteratorLoop α Id Id] [ToString β]
-    (s : String.Slice) (it : Std.Iter (α := α) β) : String :=
-  it.map toString
-    |>.fold (init := none) (fun
-      | none, sl => some sl
-      | some str, sl => some (str ++ s ++ sl))
-    |>.getD ""
-
-end Std

src/Init/Data/String/Lemmas.lean

@@ -17,8 +17,6 @@ public import Init.Data.String.Lemmas.Pattern
 public import Init.Data.String.Lemmas.Slice
 public import Init.Data.String.Lemmas.Iterate
 public import Init.Data.String.Lemmas.Intercalate
-public import Init.Data.String.Lemmas.Iter
-public import Init.Data.String.Lemmas.Hashable
 import Init.Data.Order.Lemmas
 public import Init.Data.String.Basic
 import Init.Data.Char.Lemmas

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

@@ -1,25 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Julia Markus Himmel
--/
-module
-
-prelude
-public import Init.Data.String.Slice
-public import Init.Data.LawfulHashable
-import all Init.Data.String.Slice
-import Init.Data.String.Lemmas.Slice
-
-namespace String
-
-public theorem hash_eq {s : String} : hash s = String.hash s := rfl
-
-namespace Slice
-
-public theorem hash_eq {s : String.Slice} : hash s = String.hash s.copy := (rfl)
-
-public instance : LawfulHashable String.Slice where
-  hash_eq a b hab := by simp [hash_eq, beq_eq_true_iff.1 hab]
-
-end String.Slice

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

@@ -10,7 +10,6 @@ public import Init.Data.String.Defs
 import all Init.Data.String.Defs
 public import Init.Data.String.Slice
 import all Init.Data.String.Slice
-import Init.ByCases
 
 public section
 
@@ -43,16 +42,6 @@ theorem intercalate_cons_of_ne_nil {s t : String} {l : List String} (h : l ≠ [
   match l, h with
   | u::l, _ => by simp
 
-theorem intercalate_append_of_ne_nil {l m : List String} {s : String} (hl : l ≠ []) (hm : m ≠ []) :
-    s.intercalate (l ++ m) = s.intercalate l ++ s ++ s.intercalate m := by
-  induction l with
-  | nil => simp_all
-  | cons hd tl ih =>
-    rw [List.cons_append, intercalate_cons_of_ne_nil (by simp_all)]
-    by_cases ht : tl = []
-    · simp_all
-    · simp [ih ht, intercalate_cons_of_ne_nil ht, String.append_assoc]
-
 @[simp]
 theorem toList_intercalate {s : String} {l : List String} :
     (s.intercalate l).toList = s.toList.intercalate (l.map String.toList) := by

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

@@ -1,51 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Julia Markus Himmel
--/
-module
-
-prelude
-public import Init.Data.String.Iter.Intercalate
-public import Init.Data.String.Slice
-import all Init.Data.String.Iter.Intercalate
-import all Init.Data.String.Defs
-import Init.Data.String.Lemmas.Intercalate
-import Init.Data.Iterators.Lemmas.Consumers.Loop
-import Init.Data.Iterators.Lemmas.Combinators.FilterMap
-
-namespace Std.Iter
-
-@[simp]
-public theorem joinString_eq {α β : Type} [Std.Iterator α Id β] [Std.Iterators.Finite α Id]
-    [Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id Id] [ToString β]
-    {it : Std.Iter (α := α) β} : it.joinString = String.join (it.toList.map toString) := by
-  rw [joinString, String.join, ← foldl_toList, toList_map]
-
-@[simp]
-public theorem intercalateString_eq {α β : Type} [Std.Iterator α Id β] [Std.Iterators.Finite α Id]
-    [Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id Id] [ToString β] {s : String.Slice}
-    {it : Std.Iter (α := α) β} :
-    it.intercalateString s = s.copy.intercalate (it.toList.map toString) := by
-  simp only [intercalateString, String.appendSlice_eq, ← foldl_toList, toList_map]
-  generalize s.copy = s
-  suffices ∀ (l m : List String),
-      (l.foldl (init := if m = [] then none else some (s.intercalate m))
-        (fun | none, sl => some sl | some str, sl => some (str ++ s ++ sl))).getD ""
-        = s.intercalate (m ++ l) by
-    simpa [-foldl_toList] using this (it.toList.map toString) []
-  intro l m
-  induction l generalizing m with
-  | nil => cases m <;> simp
-  | cons hd tl ih =>
-    rw [List.append_cons, ← ih, List.foldl_cons]
-    congr
-    simp only [List.append_eq_nil_iff, List.cons_ne_self, and_false, ↓reduceIte]
-    match m with
-    | [] => simp
-    | x::xs =>
-      simp only [reduceCtorEq, ↓reduceIte, List.cons_append, Option.some.injEq]
-      rw [← List.cons_append, String.intercalate_append_of_ne_nil (by simp) (by simp),
-        String.intercalate_singleton]
-
-end Std.Iter

src/Init/Data/String/Lemmas/Pattern/Split/Char.lean

@@ -23,7 +23,6 @@ import Init.Data.String.OrderInstances
 import Init.Data.String.Lemmas.Order
 import Init.Data.String.Lemmas.Intercalate
 import Init.Data.List.SplitOn.Lemmas
-import Init.Data.String.Lemmas.Slice
 
 public section
 
@@ -71,11 +70,6 @@ theorem Slice.toList_split_intercalate {c : Char} {l : List Slice} (hl : ∀ s
   · simp_all
   · rw [List.splitOn_intercalate] <;> simp_all
 
-theorem Slice.toList_split_intercalate_beq {c : Char} {l : List Slice} (hl : ∀ s ∈ l, c ∉ s.copy.toList) :
-    ((Slice.intercalate (String.singleton c) l).split c).toList ==
-      if l = [] then ["".toSlice] else l := by
-  split <;> simp_all [toList_split_intercalate hl, beq_list_iff]
-
 theorem toList_split_intercalate {c : Char} {l : List String} (hl : ∀ s ∈ l, c ∉ s.toList) :
     ((String.intercalate (String.singleton c) l).split c).toList.map (·.copy) =
       if l = [] then [""] else l := by
@@ -84,9 +78,4 @@ theorem toList_split_intercalate {c : Char} {l : List String} (hl : ∀ s ∈ l,
   · simp_all
   · rw [List.splitOn_intercalate] <;> simp_all
 
-theorem toList_split_intercalate_beq {c : Char} {l : List String} (hl : ∀ s ∈ l, c ∉ s.toList) :
-    ((String.intercalate (String.singleton c) l).split c).toList ==
-      if l = [] then ["".toSlice] else l.map String.toSlice := by
-  split <;> simp_all [toList_split_intercalate hl, Slice.beq_list_iff]
-
 end String

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

@@ -33,22 +33,8 @@ theorem beq_eq_true_iff {s t : Slice} : s == t ↔ s.copy = t.copy := by
 theorem beq_eq_false_iff {s t : Slice} : (s == t) = false ↔ s.copy ≠ t.copy := by
   simp [← Bool.not_eq_true]
 
-theorem beq_eq_decide {s t : Slice} : (s == t) = decide (s.copy = t.copy) :=
-  Bool.eq_iff_iff.2 (by simp)
-
-instance : EquivBEq String.Slice :=
-  equivBEq_of_iff_apply_eq copy (by simp)
-
-theorem beq_list_iff {l l' : List String.Slice} : l == l' ↔ l.map copy = l'.map copy := by
-  induction l generalizing l' <;> cases l' <;> simp_all
-
-theorem beq_list_eq_false_iff {l l' : List String.Slice} :
-    (l == l') = false ↔ l.map copy ≠ l'.map copy := by
-  simp [← Bool.not_eq_true, beq_list_iff]
-
-theorem beq_list_eq_decide {l l' : List String.Slice} :
-    (l == l') = decide (l.map copy = l'.map copy) :=
-  Bool.eq_iff_iff.2 (by simp [beq_list_iff])
+theorem beq_eq_decide {s t : Slice} : (s == t) = decide (s.copy = t.copy) := by
+  cases h : s == t <;> simp_all
 
 end BEq
 

src/Init/Data/String/Slice.lean

@@ -11,7 +11,7 @@ public import Init.Data.Ord.Basic
 public import Init.Data.Iterators.Combinators.FilterMap
 public import Init.Data.String.ToSlice
 public import Init.Data.String.Subslice
-public import Init.Data.String.Iter.Basic
+public import Init.Data.String.Iter
 public import Init.Data.String.Iterate
 import Init.Data.Iterators.Consumers.Collect
 import Init.Data.Iterators.Consumers.Loop
@@ -84,11 +84,10 @@ instance : ToString String.Slice where
 theorem toStringToString_eq : ToString.toString = String.Slice.copy := (rfl)
 
 @[extern "lean_slice_hash"]
-protected def hash (s : @& Slice) : UInt64 :=
-  String.hash s.copy
+opaque hash (s : @& Slice) : UInt64
 
 instance : Hashable Slice where
-  hash := Slice.hash
+  hash := hash
 
 instance : LT Slice where
   lt x y := x.copy < y.copy

src/Init/Grind/Interactive.lean

@@ -107,9 +107,6 @@ syntax (name := showLocalThms) "show_local_thms" : grind
 -/
 syntax (name := showTerm) "show_term " grindSeq : grind
 
-/-- Shows the pending goals. -/
-syntax (name := showGoals) "show_goals" : grind
-
 declare_syntax_cat grind_ref (behavior := both)
 
 syntax:max anchor : grind_ref
@@ -318,8 +315,5 @@ Only available in `sym =>` mode.
 -/
 syntax (name := symSimp) "simp" (ppSpace colGt ident)? (" [" ident,* "]")? : grind
 
-/-- `exact e` closes the main goal if its target type matches that of `e`. -/
-macro "exact " e:term : grind => `(grind| tactic => exact $e:term)
-
 end Grind
 end Lean.Parser.Tactic

src/Init/Prelude.lean

@@ -4082,7 +4082,7 @@ Actions in the resulting monad are functions that take the local value as a para
 ordinary actions in `m`.
 -/
 def ReaderT (ρ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
-  (a : @&ρ) → m α
+  ρ → m α
 
 /--
 Interpret `ρ → m α` as an element of `ReaderT ρ m α`.

src/Init/Sym/Simp/SimprocDSL.lean

@@ -49,14 +49,6 @@ syntax (name := ground) "ground" : sym_simproc
 /-- Simplify telescope binders but not the final body. -/
 syntax (name := telescope) "telescope" : sym_simproc
 
-/-- Simplify control-flow expressions (`if-then-else`, `match`, `cond`, `dite`).
-Visits only conditions and discriminants. Intended as a `pre` simproc. -/
-syntax (name := control) "control" : sym_simproc
-
-/-- Simplify arrow telescopes (`p₁ → p₂ → ... → q`) without entering binders.
-Simplifies each `pᵢ` and `q` individually. Intended as a `pre` simproc. -/
-syntax (name := arrowTelescope) "arrow_telescope" : sym_simproc
-
 /-- Rewrite using a named theorem set. Optionally specify a discharger for conditional rewrites. -/
 syntax (name := rewriteSet) "rewrite" ident (" with " sym_discharger)? : sym_simproc
 

src/Lean/Compiler/IR/AddExtern.lean

@@ -21,7 +21,6 @@ public section
 
 namespace Lean.IR
 
-set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_add_extern]
 def addExtern (declName : Name) (externAttrData : ExternAttrData) : CoreM Unit := do
   if !isPrivateName declName then

src/Lean/Compiler/LCNF/ExplicitRC.lean

@@ -97,7 +97,6 @@ partial def collectCode (code : Code .impure) : M Unit := do
     match decl.value with
     | .oproj _ parent =>
       addDerivedValue parent decl.fvarId
-    -- Keep in sync with PropagateBorrow, InferBorrow
     | .fap ``Array.getInternal args =>
       if let .fvar parent := args[1]! then
         addDerivedValue parent decl.fvarId

src/Lean/Compiler/LCNF/InferBorrow.lean

@@ -213,8 +213,6 @@ inductive OwnReason where
   | jpArgPropagation (jpFVar : FVarId)
   /-- Tail call preservation at a join point jump. -/
   | jpTailCallPreservation (jpFVar : FVarId)
-  /-- Annotated as an owned parameter (currently only triggerable through `@[export]`)-/
-  | ownedAnnotation
 
 def OwnReason.toString (reason : OwnReason) : CompilerM String := do
   PP.run do
@@ -231,7 +229,6 @@ def OwnReason.toString (reason : OwnReason) : CompilerM String := do
     | .tailCallPreservation funcName => return s!"tail call preservation of {funcName}"
     | .jpArgPropagation jpFVar => return s!"backward propagation from JP {← PP.ppFVar jpFVar}"
     | .jpTailCallPreservation jpFVar => return s!"JP tail call preservation {← PP.ppFVar jpFVar}"
-    | .ownedAnnotation => return s!"Annotated as owned"
 
 /--
 Determine whether an `OwnReason` is necessary for correctness (forced) or just an optimization
@@ -248,7 +245,7 @@ def OwnReason.isForced (reason : OwnReason) : Bool :=
   | .constructorResult .. | .functionCallResult ..
   -- We cannot pass borrowed values to reset or have borrow annotations destroy tail calls for
   -- correctness reasons.
-  | .resetReuse .. | .tailCallPreservation .. | .jpTailCallPreservation .. | .ownedAnnotation
+  | .resetReuse .. | .tailCallPreservation .. | .jpTailCallPreservation ..
   | .forwardProjectionProp .. | .backwardProjectionProp .. => true
 
 /--
@@ -259,19 +256,10 @@ partial def infer (decls : Array (Decl .impure)) : CompilerM ParamMap := do
   return map.paramMap
 where
   go : InferM Unit := do
-    for (_, params) in (← get).paramMap.map do
-      for param in params do
-        if !param.borrow && param.type.isPossibleRef then
-          -- if the param already disqualifies as borrow now this is because of an annotation
-          ownFVar param.fvarId .ownedAnnotation
-    modify fun s => { s with modified := false }
-    loop
-
-  loop : InferM Unit := do
     step
     if (← get).modified then
       modify fun s => { s with modified := false }
-      loop
+      go
     else
       return ()
 
@@ -373,16 +361,6 @@ where
     | .oproj _ x _ =>
       if ← isOwned x then ownFVar z (.forwardProjectionProp z)
       if ← isOwned z then ownFVar x (.backwardProjectionProp z)
-    -- Keep in sync with ExplicitRC, PropagateBorrow
-    | .fap ``Array.getInternal args =>
-      if let .fvar parent := args[1]! then
-        if ← isOwned parent then ownFVar z (.forwardProjectionProp z)
-    | .fap ``Array.get!Internal args =>
-      if let .fvar parent := args[2]! then
-        if ← isOwned parent then ownFVar z (.forwardProjectionProp z)
-    | .fap ``Array.uget args =>
-      if let .fvar parent := args[1]! then
-        if ← isOwned parent then ownFVar z (.forwardProjectionProp z)
     | .fap f args =>
       let ps ← getParamInfo (.decl f)
       ownFVar z (.functionCallResult z)

src/Lean/Compiler/LCNF/PropagateBorrow.lean

@@ -105,22 +105,9 @@ where
 
   collectLetValue (z : FVarId) (v : LetValue .impure) : InferM Unit := do
     match v with
-    | .oproj _ parent _ =>
-      let parentVal ← getOwnedness parent
-      join z parentVal
-    -- Keep in sync with ExplicitRC, InferBorrow
-    | .fap ``Array.getInternal args =>
-      if let .fvar parent := args[1]! then
-        let parentVal ← getOwnedness parent
-        join z parentVal
-    | .fap ``Array.get!Internal args =>
-      if let .fvar parent := args[2]! then
-        let parentVal ← getOwnedness parent
-        join z parentVal
-    | .fap ``Array.uget args =>
-      if let .fvar parent := args[1]! then
-        let parentVal ← getOwnedness parent
-        join z parentVal
+    | .oproj _ x _ =>
+      let xVal ← getOwnedness x
+      join z xVal
     | .ctor .. | .fap .. | .fvar .. | .pap .. | .sproj .. | .uproj .. | .erased .. | .lit .. =>
       join z .own
     | _ => unreachable!

src/Lean/CoreM.lean

@@ -343,13 +343,13 @@ def instantiateTypeLevelParams (c : ConstantVal) (us : List Level) : CoreM Expr
   modifyInstLevelTypeCache fun s => s.insert c.name (us, r)
   return r
 
-def instantiateValueLevelParams (c : ConstantInfo) (us : List Level) (allowOpaque := false) : CoreM Expr := do
+def instantiateValueLevelParams (c : ConstantInfo) (us : List Level) : CoreM Expr := do
   if let some (us', r) := (← get).cache.instLevelValue.find? c.name then
     if us == us' then
       return r
-  unless c.hasValue (allowOpaque := allowOpaque) do
+  unless c.hasValue do
     throwError "Not a definition or theorem: {.ofConstName c.name}"
-  let r := c.instantiateValueLevelParams! us (allowOpaque := allowOpaque)
+  let r := c.instantiateValueLevelParams! us
   modifyInstLevelValueCache fun s => s.insert c.name (us, r)
   return r
 

src/Lean/Declaration.lean

@@ -14,35 +14,29 @@ public section
 
 namespace Lean
 /--
-Reducibility hints guide the kernel's *lazy delta reduction* strategy. When the kernel encounters a
-definitional equality constraint
+Reducibility hints are used in the convertibility checker.
+When trying to solve a constraint such a
 
            (f ...) =?= (g ...)
 
-where `f` and `g` are definitions, it must decide which side to unfold. The rules (implemented in
-`lazy_delta_reduction_step` in `src/kernel/type_checker.cpp`) are:
+where f and g are definitions, the checker has to decide which one will be unfolded.
+  If      f (g) is opaque,     then g (f) is unfolded if it is also not marked as opaque,
+  Else if f (g) is abbrev,     then f (g) is unfolded if g (f) is also not marked as abbrev,
+  Else if f and g are regular, then we unfold the one with the biggest definitional height.
+  Otherwise both are unfolded.
 
-* If `f` and `g` have the **same hint kind**:
-  - Both `.opaque` or both `.abbrev`: unfold both.
-  - Both `.regular`: unfold the one with the **greater** height first. If their heights are equal
-    (in particular, if `f` and `g` are the same definition), first try to compare their arguments
-    for definitional equality (short-circuiting the unfolding if they match), then unfold both.
-* If `f` and `g` have **different hint kinds**: unfold the one that is *not* `.opaque`, preferring to
-  unfold `.abbrev` over `.regular`.
+The arguments of the `regular` Constructor are: the definitional height and the flag `selfOpt`.
 
-The `.regular` constructor carries a `UInt32` *definitional height*, which is computed by the
-elaborator as one plus the maximum height of all `.regular` constants appearing in the definition's
-body (see `getMaxHeight`). This means `.abbrev` and `.opaque` constants do not contribute to the
-height. When creating declarations via meta-programming, the height can be specified manually.
+The definitional height is by default computed by the kernel. It only takes into account
+other regular definitions used in a definition. When creating declarations using meta-programming,
+we can specify the definitional depth manually.
 
-The hints only affect performance — they control the order in which definitions are unfolded, but
-never prevent the kernel from unfolding a definition during type checking.
+Remark: the hint only affects performance. None of the hints prevent the kernel from unfolding a
+declaration during Type checking.
 
-The `ReducibilityHints` are not related to the `@[reducible]`/`@[irreducible]`/`@[semireducible]`
-attributes. Those attributes are used by the elaborator to control which definitions tactics like
-`simp`, `rfl`, and `dsimp` will unfold; they do not affect the kernel. Conversely,
-`ReducibilityHints` are set when a declaration is added to the kernel and cannot be changed
-afterwards. -/
+Remark: the ReducibilityHints are not related to the attributes: reducible/irrelevance/semireducible.
+These attributes are used by the Elaborator. The ReducibilityHints are used by the kernel (and Elaborator).
+Moreover, the ReducibilityHints cannot be changed after a declaration is added to the kernel. -/
 inductive ReducibilityHints where
   | opaque  : ReducibilityHints
   | abbrev  : ReducibilityHints
@@ -475,37 +469,24 @@ def numLevelParams (d : ConstantInfo) : Nat :=
 def type (d : ConstantInfo) : Expr :=
   d.toConstantVal.type
 
-/--
-Returns the value of a definition. With `allowOpaque := true`, values
-of theorems and opaque declarations are also returned.
--/
 def value? (info : ConstantInfo) (allowOpaque := false) : Option Expr :=
   match info with
   | .defnInfo {value, ..}   => some value
-  | .thmInfo  {value, ..}   => if allowOpaque then some value else none
+  | .thmInfo  {value, ..}   => some value
   | .opaqueInfo {value, ..} => if allowOpaque then some value else none
   | _                       => none
 
-/--
-Returns `true` if this declaration as a value for the purpose of reduction
-and type-checking, i.e. is a definition.
-With `allowOpaque := true`, theorems and opaque declarations are also considered to have values.
--/
 def hasValue (info : ConstantInfo) (allowOpaque := false) : Bool :=
   match info with
   | .defnInfo _   => true
-  | .thmInfo  _   => allowOpaque
+  | .thmInfo  _   => true
   | .opaqueInfo _ => allowOpaque
   | _             => false
 
-/--
-Returns the value of a definition. With `allowOpaque := true`, values
-of theorems and opaque declarations are also returned.
--/
 def value! (info : ConstantInfo) (allowOpaque := false) : Expr :=
   match info with
   | .defnInfo {value, ..}   => value
-  | .thmInfo  {value, ..}   => if allowOpaque then value else panic! "declaration with value expected"
+  | .thmInfo  {value, ..}   => value
   | .opaqueInfo {value, ..} => if allowOpaque then value else panic! "declaration with value expected"
   | _                       => panic! s!"declaration with value expected, but {info.name} has none"
 
@@ -529,10 +510,6 @@ def isDefinition : ConstantInfo → Bool
   | .defnInfo _ => true
   | _           => false
 
-def isTheorem : ConstantInfo → Bool
-  | .thmInfo _ => true
-  | _          => false
-
 def inductiveVal! : ConstantInfo → InductiveVal
   | .inductInfo val => val
   | _ => panic! "Expected a `ConstantInfo.inductInfo`."

src/Lean/DefEqAttrib.lean

@@ -101,7 +101,7 @@ def inferDefEqAttr (declName : Name) : MetaM Unit := do
   withoutExporting do
     let info ← getConstInfo declName
     let isRfl ←
-      if let some value := info.value? (allowOpaque := true) then
+      if let some value := info.value? then
         isRflProofCore info.type value
       else
         pure false

src/Lean/Elab/BuiltinTerm.lean

@@ -329,8 +329,7 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
   let inst ← if backward.inferInstanceAs.wrap.get (← getOptions) then
     -- Normalize to instance normal form.
     let logCompileErrors := !(← read).isNoncomputableSection && !(← read).declName?.any (Lean.isNoncomputable (← getEnv))
-    let isMeta := (← read).isMetaSection
-    withNewMCtxDepth <| normalizeInstance inst expectedType (logCompileErrors := logCompileErrors) (isMeta := isMeta)
+    withNewMCtxDepth <| normalizeInstance inst expectedType (logCompileErrors := logCompileErrors)
   else
     pure inst
   ensureHasType expectedType? inst

src/Lean/Elab/Command.lean

@@ -666,8 +666,7 @@ private def mkTermContext (ctx : Context) (s : State) : CommandElabM Term.Contex
   return {
     macroStack             := ctx.macroStack
     sectionVars            := sectionVars
-    isNoncomputableSection := scope.isNoncomputable
-    isMetaSection          := scope.isMeta }
+    isNoncomputableSection := scope.isNoncomputable }
 
 /--
 Lift the `TermElabM` monadic action `x` into a `CommandElabM` monadic action.

src/Lean/Elab/Deriving/Basic.lean

@@ -220,12 +220,10 @@ def processDefDeriving (view : DerivingClassView) (decl : Expr) (isNoncomputable
             instName ← liftMacroM <| mkUnusedBaseName instName
             if isPrivateName declName then
               instName := mkPrivateName env instName
-            let isMeta := (← read).isMetaSection
             let inst ← if backward.inferInstanceAs.wrap.get (← getOptions) then
               withDeclNameForAuxNaming instName <| withNewMCtxDepth <|
                 normalizeInstance result.instVal result.instType
                   (logCompileErrors := false)  -- covered by noncomputable check below
-                  (isMeta := isMeta)
             else
               pure result.instVal
             let closure ← Closure.mkValueTypeClosure result.instType inst (zetaDelta := true)

src/Lean/Elab/PreDefinition/Mutual.lean

@@ -63,11 +63,10 @@ def addPreDefAttributes (preDefs : Array PreDefinition) : TermElabM Unit := do
   a wrong setting and creates bad `defEq` equations.
   -/
   for preDef in preDefs do
-    unless preDef.kind.isTheorem do
-      unless preDef.modifiers.attrs.any fun a =>
-          a.name = `reducible || a.name = `semireducible ||
-          a.name = `instance_reducible || a.name = `implicit_reducible do
-        setIrreducibleAttribute preDef.declName
+    unless preDef.modifiers.attrs.any fun a =>
+        a.name = `reducible || a.name = `semireducible ||
+        a.name = `instance_reducible || a.name = `implicit_reducible do
+      setIrreducibleAttribute preDef.declName
 
   /-
   `enableRealizationsForConst` must happen before `generateEagerEqns`

src/Lean/Elab/PreDefinition/Structural/Eqns.lean

@@ -184,7 +184,6 @@ def getUnfoldFor? (declName : Name) : MetaM (Option Name) := do
   else
     return none
 
-set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_get_structural_rec_arg_pos]
 def getStructuralRecArgPosImp? (declName : Name) : CoreM (Option Nat) := do
   let some info := eqnInfoExt.find? (← getEnv) declName | return none

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

@@ -80,32 +80,6 @@ private def elimMutualRecursion (preDefs : Array PreDefinition) (fixedParamPerms
       withRecFunsAsAxioms preDefs do
         mkBRecOnF recArgInfos positions r values[idx]! FTypes[idx]!
   trace[Elab.definition.structural] "FArgs: {FArgs}"
-
-  -- Extract the functionals into named `_f` helper definitions (e.g. `foo._f`) so they show up
-  -- with a helpful name in kernel diagnostics. The `_f` definitions are `.abbrev` so the kernel
-  -- unfolds them eagerly; their body heights are registered via `setDefHeightOverride` so that
-  -- `getMaxHeight` computes the correct height for parent definitions.
-  -- For inductive predicates, the previous inline behavior is kept.
-  let FArgs ←
-    if isIndPred then
-      pure FArgs
-    else
-      let us := preDefs[0]!.levelParams.map mkLevelParam
-      FArgs.mapIdxM fun idx fArg => do
-        let fName := preDefs[idx]!.declName ++ `_f
-        let fValue ← eraseRecAppSyntaxExpr (← mkLambdaFVars xs fArg)
-        let fType ← Meta.letToHave (← inferType fValue)
-        let fHeight := getMaxHeight (← getEnv) fValue
-        addDecl (.defnDecl {
-          name := fName, levelParams := preDefs[idx]!.levelParams,
-          type := fType, value := fValue,
-          hints := .abbrev,
-          safety := if preDefs[idx]!.modifiers.isUnsafe then .unsafe else .safe,
-          all := [fName] })
-        modifyEnv (setDefHeightOverride · fName fHeight)
-        setReducibleAttribute fName
-        return mkAppN (mkConst fName us) xs
-
   let brecOn := brecOnConst 0
   -- the indices and the major premise are not mentioned in the minor premises
   -- so using `default` is fine here

src/Lean/Elab/Tactic/Grind/Basic.lean

@@ -25,16 +25,10 @@ structure Context extends Tactic.Context where
 
 open Meta.Grind (Goal)
 
-/-- An extra theorem passed to `simp` in `sym =>` mode. -/
-inductive ExtraTheorem where
-  | const (declName : Name)
-  | fvar  (fvarId : FVarId)
-  deriving BEq, Hashable
-
-/-- Cache key for `Sym.simp` variant invocations. -/
+/-- Cache key for `Sym.simp` variant invocations: variant name + ordered extra theorem names. -/
 structure SimpCacheKey where
   variant : Name
-  extras  : Array ExtraTheorem
+  extras  : List Name
   deriving BEq, Hashable
 
 structure Cache where

src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean

@@ -76,10 +76,6 @@ def evalGrindSeq : GrindTactic := fun stx =>
 @[builtin_grind_tactic skip] def evalSkip : GrindTactic := fun _ =>
   return ()
 
-@[builtin_grind_tactic showGoals] def evalShowGoals : GrindTactic := fun _ => do
-  let goals ← getUnsolvedGoalMVarIds
-  addRawTrace (goalsToMessageData goals)
-
 @[builtin_grind_tactic paren] def evalParen : GrindTactic := fun stx =>
   evalGrindTactic stx[1]
 

src/Lean/Elab/Tactic/Grind/SimprocDSLBuiltin.lean

@@ -9,8 +9,6 @@ import Lean.Elab.Tactic.Grind.SimprocDSL
 import Init.Sym.Simp.SimprocDSL
 import Lean.Meta.Sym.Simp.EvalGround
 import Lean.Meta.Sym.Simp.Telescope
-import Lean.Meta.Sym.Simp.ControlFlow
-import Lean.Meta.Sym.Simp.Forall
 import Lean.Meta.Sym.Simp.Rewrite
 namespace Lean.Elab.Tactic.Grind
 open Meta Sym.Simp
@@ -25,14 +23,6 @@ def elabSimprocGround : SymSimprocElab := fun _ =>
 def elabSimprocTelescope : SymSimprocElab := fun _ =>
   return simpTelescope
 
-@[builtin_sym_simproc Lean.Parser.Sym.Simp.control]
-def elabSimprocControl : SymSimprocElab := fun _ =>
-  return simpControl
-
-@[builtin_sym_simproc Lean.Parser.Sym.Simp.arrowTelescope]
-def elabSimprocArrowTelescope : SymSimprocElab := fun _ =>
-  return simpArrowTelescope
-
 @[builtin_sym_simproc self]
 def elabSimprocSelf : SymSimprocElab := fun _ =>
   return simp

src/Lean/Elab/Tactic/Grind/Sym.lean

@@ -153,54 +153,39 @@ def elabOptSimproc (stx? : Option Syntax) : GrindTacticM Simproc := do
   let some stx := stx? | return trivialSimproc
   elabSymSimproc stx
 
-def resolveExtraTheorems (ids? :  Option (Array (TSyntax `ident))) : GrindTacticM (Array ExtraTheorem × Array Theorem) := do
-  let some ids := ids? | return (#[], #[])
-  let mut extras := #[]
-  let mut thms := #[]
-  let lctx ← getLCtx
-  for id in ids do
-    if let some decl := lctx.findFromUserName? id.getId then
-      extras := extras.push <| .fvar decl.fvarId
-      thms := thms.push (← mkTheoremFromExpr decl.toExpr)
-    else
-      let declName ← realizeGlobalConstNoOverload id
-      extras := extras.push <| .const declName
-      thms := thms.push (← mkTheoremFromDecl declName)
-  return (extras, thms)
-
-def addExtraTheorems (post : Simproc) (extraThms : Array Theorem) : GrindTacticM Simproc := do
-  if extraThms.isEmpty then return post
+def addExtraTheorems (post : Simproc) (extraNames : Array Name) : GrindTacticM Simproc := do
+  if extraNames.isEmpty then return post
   let mut thms : Theorems := {}
-  for thm in extraThms do
-    thms := thms.insert thm
+  for name in extraNames do
+    thms := thms.insert (← mkTheoremFromDecl name)
   return post >> thms.rewrite
 
-def mkDefaultMethods (extraThms : Array Theorem) : GrindTacticM Sym.Simp.Methods := do
+def mkDefaultMethods (extraNames : Array Name) : GrindTacticM Sym.Simp.Methods := do
   let thms ← getSymSimpTheorems
   let pre := simpControl >> simpArrowTelescope
-  let post ← addExtraTheorems (evalGround >> thms.rewrite) extraThms
+  let post ← addExtraTheorems (evalGround >> thms.rewrite) extraNames
   return { pre, post }
 
-def elabVariant (variantName : Name) (extraThms : Array Theorem) : GrindTacticM (Sym.Simp.Methods × Sym.Simp.Config) := do
+def elabVariant (variantName : Name) (extraNames : Array Name) : GrindTacticM (Sym.Simp.Methods × Sym.Simp.Config) := do
   if variantName.isAnonymous then
-    return (← mkDefaultMethods extraThms, {})
+    return (← mkDefaultMethods extraNames, {})
   let some v := getSymSimpVariant? (← getEnv) variantName
     | throwError "unknown Sym.simp variant `{variantName}`"
   let pre ← elabOptSimproc v.pre?
-  let post ← addExtraTheorems (← elabOptSimproc v.post?) extraThms
+  let post ← addExtraTheorems (← elabOptSimproc v.post?) extraNames
   return ({ pre, post}, v.config)
 
-@[builtin_grind_tactic Parser.Tactic.Grind.symSimp] def evalSymSimp : GrindTactic := fun stx => withMainContext do
+@[builtin_grind_tactic Parser.Tactic.Grind.symSimp] def evalSymSimp : GrindTactic := fun stx => do
   ensureSym
   let `(grind| simp $[$variantId?]? $[[ $[$extraIds],* ]]?) := stx | throwUnsupportedSyntax
   -- Resolve variant
   let variantName := variantId?.map (·.getId) |>.getD .anonymous
-  -- Resolve extra theorems (local hypotheses first, then global constants)
-  let (extras, thms) ← resolveExtraTheorems extraIds
+  -- Compose extra theorems into post
+  let extraNames ← (extraIds.getD #[]).mapM fun id => realizeGlobalConstNoOverload id
   -- Cache lookup/creation
-  let cacheKey : SimpCacheKey := { variant := variantName, extras }
+  let cacheKey : SimpCacheKey := { variant := variantName, extras := extraNames.toList }
   let simpState := (← get).cache.simpState[cacheKey]?.getD {}
-  let (methods, config) ← elabVariant variantName thms
+  let (methods, config) ← elabVariant variantName extraNames
   let goal ← getMainGoal
   let (simpResult, simpState) ← liftGrindM <| goal.withContext do
     Sym.Simp.SimpM.run (Sym.Simp.simp (← goal.mvarId.getType)) methods config simpState

src/Lean/Elab/Tactic/Try.lean

@@ -787,7 +787,6 @@ where
           throw ex
 
 -- `evalSuggest` implementation
-set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_eval_suggest_tactic]
 private partial def evalSuggestImpl : TryTactic := fun tac => do
   trace[try.debug] "{tac}"

src/Lean/Elab/Term/TermElabM.lean

@@ -309,8 +309,6 @@ structure Context where
   heedElabAsElim     : Bool            := true
   /-- Noncomputable sections automatically add the `noncomputable` modifier to any declaration we cannot generate code for. -/
   isNoncomputableSection : Bool        := false
-  /-- `true` when inside a `meta section`. -/
-  isMetaSection : Bool                 := false
   /-- When `true` we skip TC failures. We use this option when processing patterns. -/
   ignoreTCFailures : Bool := false
   /-- `true` when elaborating patterns. It affects how we elaborate named holes. -/

src/Lean/Environment.lean

@@ -1193,8 +1193,8 @@ namespace ConstantInfo
 def instantiateTypeLevelParams (c : ConstantInfo) (ls : List Level) : Expr :=
   c.toConstantVal.instantiateTypeLevelParams ls
 
-def instantiateValueLevelParams! (c : ConstantInfo) (ls : List Level) (allowOpaque := false) : Expr :=
-  (c.value! (allowOpaque := allowOpaque)).instantiateLevelParams c.levelParams ls
+def instantiateValueLevelParams! (c : ConstantInfo) (ls : List Level) : Expr :=
+  c.value!.instantiateLevelParams c.levelParams ls
 
 end ConstantInfo
 
@@ -2755,28 +2755,13 @@ def mkThmOrUnsafeDef [Monad m] [MonadEnv m] (thm : TheoremVal) : m Declaration :
   else
     return .thmDecl thm
 
-/-- Environment extension for overriding the height that `getMaxHeight` assigns to a definition.
-This is consulted for all definitions regardless of their reducibility hints. Currently used by
-structural recursion to ensure that parent definitions get the correct height even though the
-`_f` helper definitions are marked as `.abbrev` (which `getMaxHeight` would otherwise ignore). -/
-builtin_initialize defHeightOverrideExt : EnvExtension (NameMap UInt32) ←
-  registerEnvExtension (pure {}) (asyncMode := .local)
-
-/-- Register a height override for a definition so that `getMaxHeight` uses it. -/
-def setDefHeightOverride (env : Environment) (declName : Name) (height : UInt32) : Environment :=
-  defHeightOverrideExt.modifyState env fun m => m.insert declName height
-
 def getMaxHeight (env : Environment) (e : Expr) : UInt32 :=
-  let overrides := defHeightOverrideExt.getState env
   e.foldConsts 0 fun constName max =>
-    match overrides.find? constName with
-    | some h => if h > max then h else max
-    | none =>
-      match env.findAsync? constName with
-      | some { kind := .defn, constInfo := info, .. } =>
-        match info.get.hints with
-        | ReducibilityHints.regular h => if h > max then h else max
-        | _                           => max
-      | _ => max
+    match env.findAsync? constName with
+    | some { kind := .defn, constInfo := info, .. } =>
+      match info.get.hints with
+      | ReducibilityHints.regular h => if h > max then h else max
+      | _                           => max
+    | _ => max
 
 end Lean

src/Lean/Meta/Basic.lean

@@ -1321,7 +1321,7 @@ private def getDefInfoTemp (info : ConstantInfo) : MetaM (Option ConstantInfo) :
    `constName` is an instance. This difference should be irrelevant for `isClassQuickConst?`. -/
 private def getConstTemp? (constName : Name) : MetaM (Option ConstantInfo) := do
   match (← getEnv).find? constName with
-  | some (ConstantInfo.thmInfo _)          => return none
+  | some (info@(ConstantInfo.thmInfo _))  => getTheoremInfo info
   | some (info@(ConstantInfo.defnInfo _)) => getDefInfoTemp info
   | some info                             => pure (some info)
   | none                                  => throwUnknownConstantAt (← getRef) constName

src/Lean/Meta/ExprDefEq.lean

@@ -1126,7 +1126,6 @@ def checkAssignment (mvarId : MVarId) (fvars : Array Expr) (v : Expr) : MetaM (O
       return none
     return some v
 
-set_option compiler.ignoreBorrowAnnotation true in
 -- Implementation for `_root_.Lean.MVarId.checkedAssign`
 @[export lean_checked_assign]
 def checkedAssignImpl (mvarId : MVarId) (val : Expr) : MetaM Bool := do
@@ -2234,7 +2233,6 @@ private def whnfCoreAtDefEq (e : Expr) : MetaM Expr := do
   else
     whnfCore e
 
-set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_is_expr_def_eq]
 partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecDepth do
   withTraceNodeBefore `Meta.isDefEq (fun _ => return m!"{t} =?= {s}") do

src/Lean/Meta/GetUnfoldableConst.lean

@@ -46,7 +46,11 @@ External users wanting to look up names should be using `Lean.getConstInfo`.
 def getUnfoldableConst? (constName : Name) : MetaM (Option ConstantInfo) := do
   let some ainfo := (← getEnv).findAsync? constName | throwUnknownConstantAt (← getRef) constName
   match ainfo.kind with
-  | .thm => return none
+  | .thm =>
+    if (← shouldReduceAll) then
+      return some ainfo.toConstantInfo
+    else
+      return none
   | .defn => if (← canUnfold ainfo.toConstantInfo) then return ainfo.toConstantInfo else return none
   | _ => return none
 
@@ -55,7 +59,7 @@ As with `getUnfoldableConst?` but return `none` instead of failing if the consta
 -/
 def getUnfoldableConstNoEx? (constName : Name) : MetaM (Option ConstantInfo) := do
   match (← getEnv).find? constName with
-  | some (.thmInfo _)          => return none
+  | some (info@(.thmInfo _))  => getTheoremInfo info
   | some (info@(.defnInfo _)) => if (← canUnfold info) then return info else return none
   | some (.axiomInfo _)       => recordUnfoldAxiom constName; return none
   | _                         => return none

src/Lean/Meta/InferType.lean

@@ -206,7 +206,6 @@ because it overrides unrelated configurations.
     else
       withConfig (fun cfg => { cfg with beta := true, iota := true, zeta := true, zetaHave := true, zetaDelta := true, proj := .yesWithDelta, etaStruct := .all }) x
 
-set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_infer_type]
 def inferTypeImp (e : Expr) : MetaM Expr :=
   let rec infer (e : Expr) :  MetaM Expr := do

src/Lean/Meta/InstanceNormalForm.lean

@@ -99,7 +99,7 @@ Normalize an instance value to "instance normal form".
 See the module docstring for the full algorithm specification.
 -/
 partial def normalizeInstance (inst expectedType : Expr) (compile : Bool := true)
-    (logCompileErrors : Bool := true) (isMeta : Bool := false) : MetaM Expr := withTransparency .instances do
+    (logCompileErrors : Bool := true) : MetaM Expr := withTransparency .instances do
   withTraceNode `Meta.instanceNormalForm
       (fun _ => return m!"type: {expectedType}") do
   let some className ← isClass? expectedType
@@ -124,11 +124,9 @@ partial def normalizeInstance (inst expectedType : Expr) (compile : Bool := true
             return inst
           else
             let name ← mkAuxDeclName
-            let wrapped ← mkAuxDefinition name expectedType inst (compile := false)
+            let wrapped ← mkAuxDefinition name expectedType inst (compile := compile)
+              (logCompileErrors := logCompileErrors)
             setReducibilityStatus name .implicitReducible
-            if isMeta then modifyEnv (markMeta · name)
-            if compile then
-              compileDecls (logErrors := logCompileErrors) #[name]
             enableRealizationsForConst name
             return wrapped
         else
@@ -171,7 +169,7 @@ partial def normalizeInstance (inst expectedType : Expr) (compile : Bool := true
             catch _ => pure ()
 
           mvarId.assign (← normalizeInstance arg argExpectedType (compile := compile)
-            (logCompileErrors := logCompileErrors) (isMeta := isMeta))
+            (logCompileErrors := logCompileErrors))
         else
           -- For data fields, assign directly or wrap in aux def to fix types.
           if backward.inferInstanceAs.wrap.data.get (← getOptions) then
@@ -182,7 +180,6 @@ partial def normalizeInstance (inst expectedType : Expr) (compile : Bool := true
               let name ← mkAuxDeclName
               mvarId.assign (← mkAuxDefinition name argExpectedType arg (compile := false))
               setInlineAttribute name
-              if isMeta then modifyEnv (markMeta · name)
               if compile then
                 compileDecls (logErrors := logCompileErrors) #[name]
               enableRealizationsForConst name

src/Lean/Meta/LevelDefEq.lean

@@ -85,7 +85,6 @@ private def isMVarWithGreaterDepth (v : Level) (mvarId : LMVarId) : MetaM Bool :
   | Level.mvar mvarId' => return (← mvarId'.getLevel) > (← mvarId.getLevel)
   | _ => return false
 
-set_option compiler.ignoreBorrowAnnotation true in
 mutual
 
   private partial def solve (u v : Level) : MetaM LBool := do

src/Lean/Meta/Match/MatchEqs.lean

@@ -138,7 +138,6 @@ Creates conditional equations and splitter for the given match auxiliary declara
 
 See also `getEquationsFor`.
 -/
-set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_get_match_equations_for]
 def getEquationsForImpl (matchDeclName : Name) : MetaM MatchEqns := do
   /-
@@ -247,7 +246,6 @@ where go baseName splitterName := withConfig (fun c => { c with etaStruct := .no
     let result := { eqnNames, splitterName, splitterMatchInfo }
     registerMatchEqns matchDeclName result
 
-set_option compiler.ignoreBorrowAnnotation true in
 /--
 Generate the congruence equations for the given match auxiliary declaration.
 The congruence equations have a completely unrestricted left-hand side (arbitrary discriminants),

src/Lean/Meta/Sym/Pattern.lean

@@ -785,7 +785,6 @@ def isDefEqApp (tFn : Expr) (t : Expr) (s : Expr) (_ : tFn = t.getAppFn) : DefEq
   let numArgs := t.getAppNumArgs
   isDefEqAppWithInfo t s (numArgs - 1) info
 
-set_option compiler.ignoreBorrowAnnotation true in
 /--
 `isDefEqMain` implementation.
 -/

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

@@ -40,7 +40,6 @@ abbrev cacheResult (e : Expr) (r : Result) : SimpM Result := do
     modify fun s => { s with persistentCache := s.persistentCache.insert { expr := e } r }
   return r
 
-set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_sym_simp]
 def simpImpl (e₁ : Expr) : SimpM Result := withIncRecDepth do
   let numSteps := (← get).numSteps

src/Lean/Meta/Sym/Simp/Rewrite.lean

@@ -9,7 +9,6 @@ public import Lean.Meta.Sym.Simp.Simproc
 public import Lean.Meta.Sym.Simp.Theorems
 public import Lean.Meta.Sym.Simp.App
 public import Lean.Meta.Sym.Simp.Discharger
-import Lean.Meta.ACLt
 import Lean.Meta.Sym.InstantiateS
 import Lean.Meta.Sym.InstantiateMVarsS
 import Init.Data.Range.Polymorphic.Iterators
@@ -72,16 +71,10 @@ public def Theorem.rewrite (thm : Theorem) (e : Expr) (d : Discharger := dischar
     let expr  ← instantiateRevBetaS rhs args.toArray
     if isSameExpr e expr then
       return mkRflResultCD isCD
-    else if !(← checkPerm thm.perm e expr) then
-      return mkRflResultCD isCD
     else
       return .step expr proof (contextDependent := isCD)
   else
     return .rfl
-where
-  checkPerm (perm : Bool) (e result : Expr) : MetaM Bool := do
-    if !perm then return true
-    acLt result e
 
 public def Theorems.rewrite (thms : Theorems) (d : Discharger := dischargeNone) : Simproc := fun e => do
   -- Track `cd` across all attempted theorems. If theorem A fails with cd=true

src/Lean/Meta/Sym/Simp/Theorems.lean

@@ -10,7 +10,6 @@ public import Lean.Meta.DiscrTree
 import Lean.Meta.Sym.Simp.DiscrTree
 import Lean.Meta.AppBuilder
 import Lean.ExtraModUses
-import Init.Omega
 public section
 namespace Lean.Meta.Sym.Simp
 
@@ -27,10 +26,6 @@ structure Theorem where
   pattern : Pattern
   /-- Right-hand side of the equation. -/
   rhs     : Expr
-  /-- If `true`, the theorem is a permutation rule (e.g., `x + y = y + x`).
-  Rewriting is only applied when the result is strictly less than the input
-  (using `acLt`), preventing infinite loops. -/
-  perm    : Bool := false
   deriving Inhabited
 
 instance : BEq Theorem where
@@ -50,49 +45,6 @@ def Theorems.getMatch (thms : Theorems) (e : Expr) : Array Theorem :=
 def Theorems.getMatchWithExtra (thms : Theorems) (e : Expr) : Array (Theorem × Nat) :=
   Sym.getMatchWithExtra thms.thms e
 
-/--
-Check whether `lhs` and `rhs` (with `numVars` pattern variables represented as `.bvar` indices
-`≥ 0` before any binder entry) are permutations of each other — same structure with only
-pattern variable indices rearranged via a consistent bijection.
-
-Bvars with index `< offset` are "local" (introduced by binders inside the pattern) and must
-match exactly. Bvars with index `≥ offset` are pattern variables and may be permuted,
-but the mapping must be a bijection.
-
-Simplified compared to `Meta.simp`'s `isPerm`:
-- Uses de Bruijn indices instead of metavariables
-- No `.proj` (folded into applications) or `.letE` (zeta-expanded) cases
--/
-private abbrev IsPermM := ReaderT Nat $ StateT (Array (Option Nat)) $ Except Unit
-
-private partial def isPermAux (a b : Expr) : IsPermM Unit := do
-  match a, b with
-  | .bvar i, .bvar j =>
-    let offset ← read
-    if i < offset && j < offset then
-      unless i == j do throw ()
-    else if i >= offset && j >= offset then
-      let pi := i - offset
-      let pj := j - offset
-      let fwd ← get
-      if h : pi >= fwd.size then throw () else
-      match fwd[pi] with
-      | none =>
-        -- Check injectivity: pj must not already be a target of another mapping
-        if fwd.contains (some pj) then throw ()
-        set (fwd.set pi (some pj))
-      | some pj' => unless pj == pj' do throw ()
-    else throw ()
-  | .app f₁ a₁, .app f₂ a₂ => isPermAux f₁ f₂; isPermAux a₁ a₂
-  | .mdata _ s, t => isPermAux s t
-  | s, .mdata _ t => isPermAux s t
-  | .forallE _ d₁ b₁ _, .forallE _ d₂ b₂ _ => isPermAux d₁ d₂; withReader (· + 1) (isPermAux b₁ b₂)
-  | .lam _ d₁ b₁ _, .lam _ d₂ b₂ _ => isPermAux d₁ d₂; withReader (· + 1) (isPermAux b₁ b₂)
-  | s, t => unless s == t do throw ()
-
-def isPerm (numVars : Nat) (lhs rhs : Expr) : Bool :=
-  ((isPermAux lhs rhs).run 0 |>.run (Array.replicate numVars none)) matches .ok _
-
 /-- Describes how a theorem's conclusion was adapted to an equality for use in `Sym.simp`. -/
 private inductive EqAdaptation where
   /-- Already an equality `lhs = rhs`. Proof is used as-is. -/
@@ -147,15 +99,13 @@ where
 def mkTheoremFromDecl (declName : Name) : MetaM Theorem := do
   let (pattern, (rhs, adaptation)) ← mkPatternFromDeclWithKey declName selectEqKey
   let expr ← wrapProof pattern.varTypes.size (mkConst declName) adaptation
-  let perm := isPerm pattern.varTypes.size pattern.pattern rhs
-  return { expr, pattern, rhs, perm }
+  return { expr, pattern, rhs }
 
 /-- Create a `Theorem` from a proof expression. Handles equalities, `¬`, `↔`, and propositions. -/
 def mkTheoremFromExpr (e : Expr) : MetaM Theorem := do
   let (pattern, (rhs, adaptation)) ← mkPatternFromExprWithKey e [] selectEqKey
   let expr ← wrapProof pattern.varTypes.size e adaptation
-  let perm := isPerm pattern.varTypes.size pattern.pattern rhs
-  return { expr, pattern, rhs, perm }
+  return { expr, pattern, rhs }
 
 /--
 Environment extension storing a set of `Sym.Simp` theorems.

src/Lean/Meta/SynthInstance.lean

@@ -944,7 +944,6 @@ def synthInstance (type : Expr) (maxResultSize? : Option Nat := none) : MetaM Ex
       | none        => throwFailedToSynthesize type)
     (fun _ => throwFailedToSynthesize type)
 
-set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_synth_pending]
 private def synthPendingImp (mvarId : MVarId) : MetaM Bool := withIncRecDepth <| mvarId.withContext do
   let mvarDecl ← mvarId.getDecl

src/Lean/Meta/Tactic/Delta.lean

@@ -10,18 +10,18 @@ import Lean.Meta.Transform
 public section
 namespace Lean.Meta
 
-def delta? (e : Expr) (p : Name → Bool := fun _ => true) (allowOpaque := false) : CoreM (Option Expr) :=
+def delta? (e : Expr) (p : Name → Bool := fun _ => true) : CoreM (Option Expr) :=
   matchConst e.getAppFn (fun _ => return none) fun fInfo fLvls => do
-    if p fInfo.name && fInfo.hasValue (allowOpaque := allowOpaque) && fInfo.levelParams.length == fLvls.length then
-      let f ← instantiateValueLevelParams fInfo fLvls (allowOpaque := allowOpaque)
+    if p fInfo.name && fInfo.hasValue && fInfo.levelParams.length == fLvls.length then
+      let f ← instantiateValueLevelParams fInfo fLvls
       return some (f.betaRev e.getAppRevArgs (useZeta := true))
     else
       return none
 
 /-- Low-level delta expansion. It is used to implement equation lemmas and elimination principles for recursive definitions. -/
-def deltaExpand (e : Expr) (p : Name → Bool) (allowOpaque := false) : CoreM Expr :=
+def deltaExpand (e : Expr) (p : Name → Bool) : CoreM Expr :=
   Core.transform e fun e => do
-    match (← delta? e p (allowOpaque := allowOpaque)) with
+    match (← delta? e p) with
     | some e' => return .visit e'
     | none    => return .continue
 

src/Lean/Meta/Tactic/FunInd.lean

@@ -347,13 +347,11 @@ partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option E
 
     if e.getAppArgs.any (·.isFVarOf oldIH) then
       -- Sometimes Fix.lean abstracts over oldIH in a proof definition.
-      -- So delta-beta-reduce that definition. We need to look through theorems here!
-      if let .const declName lvls := e.getAppFn then
-        if let some cinfo := (← getEnv).find? declName then
-          if let some val := cinfo.value? (allowOpaque := true) then
-            let e' := (val.instantiateLevelParams cinfo.levelParams lvls).betaRev e.getAppRevArgs
-            return ← foldAndCollect oldIH newIH isRecCall e'
-      throwError "Internal error in `foldAndCollect`: Cannot reduce application of `{e.getAppFn}` in:{indentExpr e}"
+      -- So beta-reduce that definition. We need to look through theorems here!
+      if let some e' ← withTransparency .all do unfoldDefinition? e then
+        return ← foldAndCollect oldIH newIH isRecCall e'
+      else
+        throwError "Internal error in `foldAndCollect`: Cannot reduce application of `{e.getAppFn}` in:{indentExpr e}"
 
     match e with
     | .app e1 e2 =>
@@ -744,13 +742,6 @@ partial def buildInductionBody (toErase toClear : Array FVarId) (goal : Expr)
         let b' ← buildInductionBody toErase toClear goal' oldIH newIH isRecCall (b.instantiate1 x)
         mkLambdaFVars #[x] b'
 
-  -- Unfold constant applications that take `oldIH` as an argument (e.g. `_f` auxiliary
-  -- definitions from structural recursion), so that we can see their body structure.
-  -- Similar to the case in `foldAndCollect`.
-  if e.getAppFn.isConst && e.getAppArgs.any (·.isFVarOf oldIH) then
-    if let some e' ← withTransparency .all (unfoldDefinition? e) then
-      return ← buildInductionBody toErase toClear goal oldIH newIH isRecCall e'
-
   liftM <| buildInductionCase oldIH newIH isRecCall toErase toClear goal e
 
 /--

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

@@ -276,7 +276,6 @@ private def propagateNonlinearPow (x : Var) : GoalM Bool := do
   c'.assert
   return true
 
-set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_cutsat_propagate_nonlinear]
 def propagateNonlinearTermImpl (y : Var) (x : Var) : GoalM Bool := do
   unless (← isVarEqConst? y).isSome do return false
@@ -339,7 +338,6 @@ partial def _root_.Int.Linear.Poly.updateOccsForElimEq (p : Poly) (x : Var) : Go
     go p
   go p
 
-set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_grind_cutsat_assert_eq]
 def EqCnstr.assertImpl (c : EqCnstr) : GoalM Unit := do
   if (← inconsistent) then return ()

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

@@ -99,7 +99,6 @@ where
         return some { p := c.p.addConst 1, h := .ofLeDiseq c c' }
     return none
 
-set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_grind_cutsat_assert_le]
 def LeCnstr.assertImpl (c : LeCnstr) : GoalM Unit := do
   if (← inconsistent) then return ()

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

@@ -325,9 +325,7 @@ private def mkPowEqProof (ka : Int) (ca? : Option EqCnstr) (kb : Nat) (cb? : Opt
   let h := mkApp8 (mkConst ``Int.Linear.pow_eq) a b (toExpr ka) (toExpr kbInt) (toExpr k) h₁ h₂ eagerReflBoolTrue
   return mkApp6 (mkConst ``Int.Linear.of_var_eq) (← getContext) (← mkVarDecl x) (toExpr k) (← mkPolyDecl c'.p) eagerReflBoolTrue h
 
-set_option compiler.ignoreBorrowAnnotation true in
 mutual
-
 @[export lean_cutsat_eq_cnstr_to_proof]
 private partial def EqCnstr.toExprProofImpl (c' : EqCnstr) : ProofM Expr := caching c' do
   trace[grind.debug.lia.proof] "{← c'.pp}"

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

@@ -64,7 +64,6 @@ where
         registerNonlinearOcc e x
     | _ => registerNonlinearOcc e x
 
-set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_grind_cutsat_mk_var]
 def mkVarImpl (expr : Expr) : GoalM Var := do
   if let some var := (← get').varMap.find? { expr } then

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

@@ -239,7 +239,6 @@ private def normOfNatArgs? (args : Array Expr) : MetaM (Option (Array Expr)) :=
       return some args.toArray
   return none
 
-set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_grind_canon]
 partial def canonImpl (e : Expr) : GoalM Expr := do profileitM Exception "grind canon" (← getOptions) do
   trace_goal[grind.debug.canon] "{e}"

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

@@ -348,7 +348,6 @@ where
       internalize rhs generation p
       addEqCore lhs rhs proof isHEq
 
-set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_grind_process_new_facts]
 private def processNewFactsImpl : GoalM Unit := do
   repeat

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

@@ -535,7 +535,6 @@ private def internalizeOfNatFinBitVecLiteral (e : Expr) (generation : Nat) (pare
   updateIndicesFound (.const ``OfNat.ofNat)
   activateTheorems ``OfNat.ofNat generation
 
-set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_grind_internalize]
 private partial def internalizeImpl (e : Expr) (generation : Nat) (parent? : Option Expr := none) : GoalM Unit := withIncRecDepth do
   if (← alreadyInternalized e) then

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

@@ -328,7 +328,6 @@ mutual
 
 end
 
-set_option compiler.ignoreBorrowAnnotation true in
 /--
 Returns a proof that `a = b`.
 It assumes `a` and `b` are in the same equivalence class.
@@ -339,7 +338,6 @@ def mkEqProofImpl (a b : Expr) : GoalM Expr := do
     throwError "internal `grind` error, `mkEqProof` invoked with terms of different types{indentExpr a}\nhas type{indentExpr (← inferType a)}\nbut{indentExpr b}\nhas type{indentExpr (← inferType b)}"
   mkEqProofCore a b (heq := false)
 
-set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_grind_mk_heq_proof]
 def mkHEqProofImpl (a b : Expr) : GoalM Expr :=
   mkEqProofCore a b (heq := true)

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

@@ -42,7 +42,6 @@ def dsimpCore (e : Expr) : GrindM Expr := do profileitM Exception "grind dsimp"
   modify fun s => { s with simp }
   return r
 
-set_option compiler.ignoreBorrowAnnotation true in
 /--
 Preprocesses `e` using `grind` normalization theorems and simprocs,
 and then applies several other preprocessing steps.

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

@@ -202,7 +202,6 @@ protected def getSimpContext (config : Grind.Config) : MetaM Simp.Context := do
     (simpTheorems := #[thms])
     (congrTheorems := (← getSimpCongrTheorems))
 
-set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_grind_normalize]
 def normalizeImp (e : Expr) (config : Grind.Config) : MetaM Expr := do
   let (r, _) ← Meta.simp e (← Grind.getSimpContext config) (← Grind.getSimprocs)

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

@@ -52,12 +52,6 @@ builtin_dsimproc [simp, seval] reduceSingleton (String.singleton _) := fun e =>
   let some c ← Char.fromExpr? e.appArg! | return .continue
   return .done <| toExpr (String.singleton c)
 
-builtin_dsimproc_decl reduceToSingleton ((_ : String)) := fun e => do
-  let some s ← fromExpr? e | return .continue
-  let l := s.toList
-  let [c] := l | return .continue
-  return .done <| mkApp (mkConst ``String.singleton) (toExpr c)
-
 @[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : String → String → Bool) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← fromExpr? e.appFn!.appArg! | return .continue

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

@@ -512,7 +512,6 @@ Auxiliary `dsimproc` for not visiting `Char` literal subterms.
 -/
 private def doNotVisitCharLit : DSimproc := doNotVisit isCharLit ``Char.ofNat
 
-set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_dsimp]
 private partial def dsimpImpl (e : Expr) : SimpM Expr := do
   let cfg ← getConfig
@@ -711,7 +710,6 @@ where
       r ← r.mkEqTrans (← simpLoop r.expr)
     cacheResult e cfg r
 
-set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_simp]
 def simpImpl (e : Expr) : SimpM Result := withIncRecDepth do
   checkSystem "simp"

src/Lean/Meta/Transform.lean

@@ -240,8 +240,8 @@ def unfoldDeclsFrom (biggerEnv : Environment) (e : Expr) : CoreM Expr := do
       if env.contains declName then
         return .done e
       let some info := biggerEnv.find? declName | return .done e
-      if info.hasValue (allowOpaque := true) then
-        return .visit (← instantiateValueLevelParams info us (allowOpaque := true))
+      if info.hasValue then
+        return .visit (← instantiateValueLevelParams info us)
       else
         return .done e
     Core.transform e (pre := pre)
@@ -282,7 +282,7 @@ def unfoldIfArgIsAppOf (fnNames : Array Name) (numSectionVars : Nat) (e : Expr)
         -/
         if revArgs.any isInterestingArg then
           if let some info@(.thmInfo _) := env.find? f.constName! then
-            return .visit <| (← instantiateValueLevelParams info f.constLevels! (allowOpaque := true)).betaRev revArgs
+            return .visit <| (← instantiateValueLevelParams info f.constLevels!).betaRev revArgs
       return .continue)
   where
     isInterestingArg (a : Expr) : Bool := a.withApp fun af axs =>

src/Lean/Meta/WHNF.lean

@@ -1100,7 +1100,6 @@ private def cache (useCache : Bool) (e r : Expr) : MetaM Expr := do
     modify fun s => { s with cache.whnf := s.cache.whnf.insert key r }
   return r
 
-set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_whnf]
 partial def whnfImp (e : Expr) : MetaM Expr :=
   withIncRecDepth <| whnfEasyCases e fun e => do

src/Lean/Parser.lean

@@ -65,7 +65,6 @@ end Parser
 namespace PrettyPrinter
 namespace Parenthesizer
 
-set_option compiler.ignoreBorrowAnnotation true in
 -- Close the mutual recursion loop; see corresponding `[extern]` in the parenthesizer.
 @[export lean_mk_antiquot_parenthesizer]
 def mkAntiquot.parenthesizer (name : String) (kind : SyntaxNodeKind) (anonymous := true) (isPseudoKind := true) : Parenthesizer :=
@@ -81,7 +80,6 @@ def mkAntiquot.parenthesizer (name : String) (kind : SyntaxNodeKind) (anonymous
 
 open Lean.Parser
 
-set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_pretty_printer_parenthesizer_interpret_parser_descr]
 unsafe def interpretParserDescr : ParserDescr → CoreM Parenthesizer
   | ParserDescr.const n                             => getConstAlias parenthesizerAliasesRef n
@@ -103,7 +101,6 @@ end Parenthesizer
 
 namespace Formatter
 
-set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_mk_antiquot_formatter]
 def mkAntiquot.formatter (name : String) (kind : SyntaxNodeKind) (anonymous := true) (isPseudoKind := true) : Formatter :=
   Parser.mkAntiquot.formatter name kind anonymous isPseudoKind
@@ -116,7 +113,6 @@ def mkAntiquot.formatter (name : String) (kind : SyntaxNodeKind) (anonymous := t
 
 open Lean.Parser
 
-set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_pretty_printer_formatter_interpret_parser_descr]
 unsafe def interpretParserDescr : ParserDescr → CoreM Formatter
   | ParserDescr.const n                             => getConstAlias formatterAliasesRef n

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

@@ -64,10 +64,11 @@ namespace ConstantInfo
 
 /-- Return all names appearing in the type or value of a `ConstantInfo`. -/
 def getUsedConstantsAsSet (c : ConstantInfo) : NameSet :=
-  c.type.getUsedConstantsAsSet ++ match c.value? (allowOpaque := true) with
+  c.type.getUsedConstantsAsSet ++ match c.value? with
   | some v => v.getUsedConstantsAsSet
   | none => match c with
     | .inductInfo val => .ofList val.ctors
+    | .opaqueInfo val => val.value.getUsedConstantsAsSet
     | .ctorInfo val => ({} : NameSet).insert val.name
     | .recInfo val => .ofList val.all
     | _ => {}

src/Std/Data/String/ToInt.lean

@@ -98,34 +98,18 @@ end Slice
 public theorem isInt_toSlice {s : String} : s.toSlice.isInt = s.isInt :=
   (rfl)
 
-@[simp]
-public theorem isInt_comp_toSlice : String.Slice.isInt ∘ String.toSlice = String.isInt := by
-  ext; simp
-
 @[simp]
 public theorem toInt?_toSlice {s : String} : s.toSlice.toInt? = s.toInt? :=
   (rfl)
 
-@[simp]
-public theorem toInt?_comp_toSlice : String.Slice.toInt? ∘ String.toSlice = String.toInt? := by
-  ext; simp
-
 @[simp]
 public theorem Slice.isInt_copy {s : Slice} : s.copy.isInt = s.isInt := by
   simpa [← isInt_toSlice] using Slice.isInt_congr (by simp)
 
-@[simp]
-public theorem Slice.isInt_comp_copy : String.isInt ∘ String.Slice.copy = String.Slice.isInt := by
-  ext; simp
-
 @[simp]
 public theorem Slice.toInt?_copy {s : Slice} : s.copy.toInt? = s.toInt? := by
   simpa [← isInt_toSlice] using Slice.toInt?_congr (by simp)
 
-@[simp]
-public theorem Slice.toInt?_comp_copy : String.toInt? ∘ String.Slice.copy = String.Slice.toInt? := by
-  ext; simp
-
 public theorem toInt?_eq_some_iff {s : String} {a : Int} :
     s.toInt? = some a ↔ (∃ b, s.toNat? = some b ∧ a = (b : Int)) ∨ ∃ t, s = "-" ++ t ∧ ∃ b, t.toNat? = some b ∧ a = -(b : Int) := by
   simp [← toInt?_toSlice, Slice.toInt?_eq_some_iff]

src/Std/Data/String/ToNat.lean

@@ -221,34 +221,18 @@ namespace String
 public theorem isNat_toSlice {s : String} : s.toSlice.isNat = s.isNat :=
   (rfl)
 
-@[simp]
-public theorem isNat_comp_toSlice : String.Slice.isNat ∘ String.toSlice = String.isNat := by
-  ext; simp
-
 @[simp]
 public theorem toNat?_toSlice {s : String} : s.toSlice.toNat? = s.toNat? :=
   (rfl)
 
-@[simp]
-public theorem toNat?_comp_toSlice : String.Slice.toNat? ∘ String.toSlice = String.toNat? := by
-  ext; simp
-
 @[simp]
 public theorem Slice.isNat_copy {s : Slice} : s.copy.isNat = s.isNat := by
   simpa [← isNat_toSlice] using Slice.isNat_congr (by simp)
 
-@[simp]
-public theorem Slice.isNat_comp_copy : String.isNat ∘ String.Slice.copy = String.Slice.isNat := by
-  ext; simp
-
 @[simp]
 public theorem Slice.toNat?_copy {s : Slice} : s.copy.toNat? = s.toNat? := by
   simpa [← isNat_toSlice] using Slice.toNat?_congr (by simp)
 
-@[simp]
-public theorem Slice.toNat?_comp_copy : String.toNat? ∘ String.Slice.copy = String.Slice.toNat? := by
-  ext; simp
-
 public theorem isNat_iff {s : String} :
     s.isNat = true ↔
       s ≠ "" ∧

src/Std/Internal.lean

@@ -10,7 +10,6 @@ public import Std.Internal.Async
 public import Std.Internal.Http
 public import Std.Internal.Parsec
 public import Std.Internal.UV
-public import Std.Internal.SSL
 
 @[expose] public section
 

src/Std/Internal/Async.lean

@@ -10,7 +10,6 @@ public import Std.Internal.Async.Basic
 public import Std.Internal.Async.ContextAsync
 public import Std.Internal.Async.Timer
 public import Std.Internal.Async.TCP
-public import Std.Internal.Async.TCP.SSL
 public import Std.Internal.Async.UDP
 public import Std.Internal.Async.DNS
 public import Std.Internal.Async.Select
@@ -18,4 +17,3 @@ public import Std.Internal.Async.Process
 public import Std.Internal.Async.System
 public import Std.Internal.Async.Signal
 public import Std.Internal.Async.IO
-public import Std.Internal.SSL

src/Std/Internal/Async/TCP/SSL.lean

@@ -1,445 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sofia Rodrigues
--/
-module
-
-prelude
-public import Std.Time
-public import Std.Internal.UV.TCP
-public import Std.Internal.Async.Timer
-public import Std.Internal.Async.Select
-public import Std.Internal.SSL
-
-public section
-
-namespace Std.Internal.IO.Async.TCP.SSL
-
-open Std.Internal.SSL
-open Std.Internal.UV.TCP
-open Std.Net
-
-/--
-Default chunk size used by TLS I/O loops.
--/
-def ioChunkSize : UInt64 := 16 * 1024
-
--- ## Private helpers: SSL ↔ TCP I/O bridge
-
-/--
-Feeds an encrypted chunk into the SSL input BIO.
-Raises an error if OpenSSL consumed fewer bytes than supplied.
--/
-@[inline]
-private def feedEncryptedChunk (ssl : Session r) (encrypted : ByteArray) : IO Unit := do
-  if encrypted.size == 0 then return ()
-  let consumed ← ssl.feedEncrypted encrypted
-  if consumed.toNat != encrypted.size then
-    throw <| IO.userError s!"TLS input short write: consumed {consumed} / {encrypted.size} bytes"
-
-/--
-Drains all pending encrypted bytes from the SSL output BIO and sends them over TCP.
--/
-private partial def flushEncrypted (native : Socket) (ssl : Session r) : Async Unit := do
-  let out ← ssl.drainEncrypted
-  if out.size == 0 then return ()
-  Async.ofPromise <| native.send #[out]
-  flushEncrypted native ssl
-
-/--
-Runs the TLS handshake loop to completion, interleaving SSL state machine steps
-with TCP I/O.
--/
-private partial def doHandshake (native : Socket) (ssl : Session r) (chunkSize : UInt64) : Async Unit := do
-  dbg_trace "start handshake"
-
-  dbg_trace "checking :D"
-  if ← ssl.handshake then
-    flushEncrypted native ssl
-    dbg_trace "handshaked :D"
-    return ()
-
-  dbg_trace "flush :D"
-  flushEncrypted native ssl
-
-  dbg_trace "receiving more data"
-  let encrypted? ← Async.ofPromise <| native.recv? chunkSize
-  match encrypted? with
-  | none =>
-    throw <| IO.userError "connection closed during TLS handshake"
-  | some encrypted =>
-    dbg_trace "feeding more data"
-    feedEncryptedChunk ssl encrypted
-    doHandshake native ssl chunkSize
-
--- ## Types
-
-/--
-Represents a TLS-enabled TCP server socket. Carries its own server context so
-that each accepted connection gets a session configured from the same context.
--/
-structure Server where
-  private ofNative ::
-    native : Socket
-    serverCtx : Context.Server
-
-/--
-Represents a TLS-enabled TCP connection, parameterized by TLS role.
-Use `Client` for outgoing connections and `ServerConn` for server-accepted connections.
--/
-structure Connection (r : Role) where
-  private ofNative ::
-    native : Socket
-    ssl : Session r
-
-/--
-An outgoing TLS client connection.
--/
-abbrev Client := Connection .client
-
-/--
-An incoming TLS connection accepted by a `Server`.
--/
-abbrev ServerConn := Connection .server
-
-namespace Server
-
-/--
-Creates a new TLS-enabled TCP server socket using the given context.
--/
-@[inline]
-def mk (serverCtx : Context.Server) : IO Server := do
-  let native ← Socket.new
-  return Server.ofNative native serverCtx
-
-/--
-Configures the server context with a PEM certificate and private key.
--/
-@[inline]
-def configureServer (s : Server) (certFile keyFile : String) : IO Unit :=
-  s.serverCtx.configure certFile keyFile
-
-/--
-Binds the server socket to the specified address.
--/
-@[inline]
-def bind (s : Server) (addr : SocketAddress) : IO Unit :=
-  s.native.bind addr
-
-/--
-Listens for incoming connections with the given backlog.
--/
-@[inline]
-def listen (s : Server) (backlog : UInt32) : IO Unit :=
-  s.native.listen backlog
-
-@[inline] private def mkServerConn (native : Socket) (ctx : Context.Server) : IO ServerConn := do
-  let ssl ← Session.Server.mk ctx
-  return ⟨native, ssl⟩
-
-/--
-Accepts an incoming TLS connection and performs the TLS handshake.
--/
-@[inline]
-def accept (s : Server) (chunkSize : UInt64 := ioChunkSize) : Async ServerConn := do
-  let native ← Async.ofPromise <| s.native.accept
-  let conn ← mkServerConn native s.serverCtx
-  doHandshake conn.native conn.ssl chunkSize
-  return conn
-
-/--
-Tries to accept an incoming TLS connection without blocking.
--/
-@[inline]
-def tryAccept (s : Server) : IO (Option ServerConn) := do
-  let res ← s.native.tryAccept
-  let socket ← IO.ofExcept res
-  match socket with
-  | none => return none
-  | some native => return some (← mkServerConn native s.serverCtx)
-
-/--
-Creates a `Selector` that resolves once `s` has a connection available.
--/
-def acceptSelector (s : Server) : Selector ServerConn :=
-  {
-    tryFn :=
-      s.tryAccept
-
-    registerFn waiter := do
-      let task ← s.native.accept
-
-      -- If we get cancelled the promise will be dropped so prepare for that
-      IO.chainTask (t := task.result?) fun res => do
-        match res with
-        | none => return ()
-        | some res =>
-          let lose := return ()
-          let win promise := do
-            try
-              let native ← IO.ofExcept res
-              let ssl ← Session.Server.mk s.serverCtx
-              let conn : ServerConn := ⟨native, ssl⟩
-              promise.resolve (.ok conn)
-            catch e =>
-              promise.resolve (.error e)
-          waiter.race lose win
-
-    unregisterFn := s.native.cancelAccept
-  }
-
-/--
-Gets the local address of the server socket.
--/
-@[inline]
-def getSockName (s : Server) : IO SocketAddress :=
-  s.native.getSockName
-
-/--
-Enables the Nagle algorithm for all client sockets accepted by this server socket.
--/
-@[inline]
-def noDelay (s : Server) : IO Unit :=
-  s.native.noDelay
-
-/--
-Enables TCP keep-alive for all client sockets accepted by this server socket.
--/
-@[inline]
-def keepAlive (s : Server) (enable : Bool) (delay : Std.Time.Second.Offset) (_ : delay.val ≥ 1 := by decide) : IO Unit :=
-  s.native.keepAlive enable.toInt8 delay.val.toNat.toUInt32
-
-end Server
-
--- ## Connection (shared read/write operations for both roles)
-
-namespace Connection
-
-/--
-Attempts to write plaintext data into TLS. Returns true when accepted.
-Any encrypted TLS output generated is flushed to the socket.
--/
-@[inline]
-def write {r : Role} (s : Connection r) (data : ByteArray) : Async Bool := do
-  let accepted ← s.ssl.write data
-  flushEncrypted s.native s.ssl
-  return accepted
-
-/--
-Sends data through a TLS-enabled socket.
-Fails if OpenSSL reports the write as pending additional I/O.
--/
-@[inline]
-def send {r : Role} (s : Connection r) (data : ByteArray) : Async Unit := do
-  if ← s.write data then
-    return ()
-  else
-    throw <| IO.userError "TLS write is pending additional I/O; call `recv?` or retry later"
-
-/--
-Sends multiple data buffers through the TLS-enabled socket.
--/
-@[inline]
-def sendAll {r : Role} (s : Connection r) (data : Array ByteArray) : Async Unit :=
-  data.forM (s.send ·)
-
-/--
-Receives decrypted plaintext data from TLS.
-If no plaintext is immediately available, this function pulls encrypted data from TCP first.
--/
-partial def recv? {r : Role} (s : Connection r) (size : UInt64) (chunkSize : UInt64 := ioChunkSize) : Async (Option ByteArray) := do
-  match ← s.ssl.read? size with
-  | some plain =>
-    flushEncrypted s.native s.ssl
-    return some plain
-  | none =>
-    flushEncrypted s.native s.ssl
-    let encrypted? ← Async.ofPromise <| s.native.recv? chunkSize
-    match encrypted? with
-    | none =>
-      return none
-    | some encrypted =>
-      feedEncryptedChunk s.ssl encrypted
-      recv? s size chunkSize
-
-/--
-Tries to receive decrypted plaintext data without blocking.
-Returns `some (some data)` if plaintext is available, `some none` if the peer closed,
-or `none` if no data is ready yet.
--/
-partial def tryRecv {r : Role} (s : Connection r) (size : UInt64) (chunkSize : UInt64 := ioChunkSize) : Async (Option (Option ByteArray)) := do
-  let pending ← s.ssl.pendingPlaintext
-
-  if pending > 0 then
-    return some (← s.recv? size)
-  else
-    let readableWaiter ← s.native.waitReadable
-
-    flushEncrypted s.native s.ssl
-
-    if ← readableWaiter.isResolved then
-      let encrypted? ← Async.ofPromise <| s.native.recv? ioChunkSize
-      match encrypted? with
-      | none =>
-        return none
-      | some encrypted =>
-        feedEncryptedChunk s.ssl encrypted
-        tryRecv s size chunkSize
-    else
-      s.native.cancelRecv
-      return none
-
-/--
-Feeds encrypted socket data into SSL until plaintext is pending.
-Resolves the returned promise once plaintext is available.
--/
-partial def waitReadable {r : Role} (s : Connection r) (chunkSize : UInt64 := ioChunkSize) : Async Unit := do
-  if (← s.ssl.pendingPlaintext) > 0 then
-    return ()
-
-  let rec go : Async Unit := do
-    let readable ← Async.ofPromise <| s.native.waitReadable
-
-    if !readable then
-      return ()
-
-    let encrypted? ← Async.ofPromise <| s.native.recv? chunkSize
-
-    match encrypted? with
-    | none =>
-      return ()
-    | some encrypted =>
-      feedEncryptedChunk s.ssl encrypted
-      flushEncrypted s.native s.ssl
-
-      if (← s.ssl.pendingPlaintext) > 0 then
-        return ()
-      else
-        go
-
-  go
-
-/--
-Creates a `Selector` that resolves once `s` has plaintext data available.
--/
-def recvSelector {r : Role} (s : Connection r) (size : UInt64) : Selector (Option ByteArray) :=
-  {
-    tryFn := s.tryRecv size
-
-    registerFn waiter := do
-      let readableWaiter ← s.waitReadable.asTask
-
-      -- If we get cancelled the promise will be dropped so prepare for that
-      discard <| IO.mapTask (t := readableWaiter) fun res => do
-        match res with
-        | .error _ => return ()
-        | .ok _ =>
-          let lose := return ()
-          let win promise := do
-            try
-              -- We know that this read should not block.
-              let result ← (s.recv? size).block
-              promise.resolve (.ok result)
-            catch e =>
-              promise.resolve (.error e)
-          waiter.race lose win
-
-    unregisterFn := s.native.cancelRecv
-  }
-
-/--
-Shuts down the write side of the socket.
--/
-@[inline]
-def shutdown {r : Role} (s : Connection r) : Async Unit :=
-  Async.ofPromise <| s.native.shutdown
-
-/--
-Gets the remote address of the socket.
--/
-@[inline]
-def getPeerName {r : Role} (s : Connection r) : IO SocketAddress :=
-  s.native.getPeerName
-
-/--
-Gets the local address of the socket.
--/
-@[inline]
-def getSockName {r : Role} (s : Connection r) : IO SocketAddress :=
-  s.native.getSockName
-
-/--
-Returns the X.509 verification result code for this TLS session.
--/
-@[inline]
-def verifyResult {r : Role} (s : Connection r) : IO UInt64 :=
-  s.ssl.verifyResult
-
-/--
-Enables the Nagle algorithm for the socket.
--/
-@[inline]
-def noDelay {r : Role} (s : Connection r) : IO Unit :=
-  s.native.noDelay
-
-/--
-Enables TCP keep-alive with a specified delay for the socket.
--/
-@[inline]
-def keepAlive {r : Role} (s : Connection r) (enable : Bool) (delay : Std.Time.Second.Offset) (_ : delay.val ≥ 0 := by decide) : IO Unit :=
-  s.native.keepAlive enable.toInt8 delay.val.toNat.toUInt32
-
-end Connection
-
--- ## Client (outgoing connection setup)
-
-namespace Client
-
-/--
-Creates a new outgoing TLS client connection using the given client context.
--/
-@[inline]
-def mk (ctx : Context.Client) : IO Client := do
-  let native ← Socket.new
-  let ssl ← Session.Client.mk ctx
-  return ⟨native, ssl⟩
-
-/--
-Configures the given client context.
-`caFile` may be empty to use default trust settings.
--/
-@[inline]
-def configureContext (ctx : Context.Client) (caFile := "") (verifyPeer := true) : IO Unit :=
-  ctx.configure caFile verifyPeer
-
-/--
-Binds the client socket to the specified address.
--/
-@[inline]
-def bind (s : Client) (addr : SocketAddress) : IO Unit :=
-  s.native.bind addr
-
-/--
-Sets SNI server name used during the TLS handshake.
--/
-@[inline]
-def setServerName (s : Client) (host : String) : IO Unit :=
-  Session.Client.setServerName s.ssl host
-
-/--
-Performs the TLS handshake on an established TCP connection.
--/
-@[inline]
-def handshake (s : Client) (chunkSize : UInt64 := ioChunkSize) : Async Unit :=
-  doHandshake (Connection.native s) (Connection.ssl s) chunkSize
-
-/--
-Connects the client socket to the given address and performs the TLS handshake.
--/
-@[inline]
-def connect (s : Client) (addr : SocketAddress) (chunkSize : UInt64 := ioChunkSize) : Async Unit := do
-  Async.ofPromise <| (Connection.native s).connect addr
-  s.handshake chunkSize
-
-end Std.Internal.IO.Async.TCP.SSL.Client

src/Std/Internal/SSL.lean

@@ -1,178 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sofia Rodrigues
--/
-module
-
-prelude
-public import Init.System.Promise
-
-public section
-
-namespace Std.Internal.SSL
-
-/--
-Distinguishes server-side from client-side TLS contexts and sessions at the type level.
--/
-inductive Role where
-  | server
-  | client
-
-private opaque ContextImpl : Role → NonemptyType.{0}
-
-/--
-Represents an OpenSSL context (`SSL_CTX`) parameterized by role.
-Use `Context.Server` or `Context.Client` for the concrete aliases.
--/
-def Context (r : Role) : Type := (ContextImpl r).type
-
-/--
-Server-side TLS context (`SSL_CTX` configured with `TLS_server_method`).
--/
-abbrev Context.Server := Context .server
-
-/--
-Client-side TLS context (`SSL_CTX` configured with `TLS_client_method`).
--/
-abbrev Context.Client := Context .client
-
-instance (r : Role) : Nonempty (Context r) := (ContextImpl r).property
-
-namespace Context
-
-namespace Server
-
-/--
-Creates a new server-side TLS context using `TLS_server_method`.
--/
-@[extern "lean_uv_ssl_ctx_mk_server"]
-opaque mk : IO Context.Server
-
-/--
-Loads a PEM certificate and private key into a server context.
--/
-@[extern "lean_uv_ssl_ctx_configure_server"]
-opaque configure (ctx : @& Context.Server) (certFile : @& String) (keyFile : @& String) : IO Unit
-
-end Server
-
-namespace Client
-
-/--
-reates a new client-side TLS context using `TLS_client_method`.
--/
-@[extern "lean_uv_ssl_ctx_mk_client"]
-opaque mk : IO Context.Client
-
-/--
-Configures CA trust anchors and peer verification for a client context.
-`caFile` may be empty to use platform default trust anchors.
--/
-@[extern "lean_uv_ssl_ctx_configure_client"]
-opaque configure (ctx : @& Context.Client) (caFile : @& String) (verifyPeer : Bool) : IO Unit
-
-end Client
-
-end Context
-
-private opaque SessionImpl : Role → NonemptyType.{0}
-
-/--
-Represents an OpenSSL SSL session parameterized by role.
-Use `Session.Server` or `Session.Client` for the concrete aliases.
--/
-def Session (r : Role) : Type := (SessionImpl r).type
-
-/--
-Server-side TLS session.
--/
-abbrev Session.Server := Session .server
-
-/--
-Client-side TLS session.
--/
-abbrev Session.Client := Session .client
-
-instance (r : Role) : Nonempty (Session r) := (SessionImpl r).property
-
-namespace Session
-
-namespace Server
-
-/--
-Creates a new server-side SSL session from the given context.
--/
-@[extern "lean_uv_ssl_mk_server"]
-opaque mk (ctx : @& Context.Server) : IO Session.Server
-
-end Server
-
-namespace Client
-
-/--
-Creates a new client-side SSL session from the given context.
--/
-@[extern "lean_uv_ssl_mk_client"]
-opaque mk (ctx : @& Context.Client) : IO Session.Client
-
-/--
-Sets the SNI host name for client-side handshakes.
--/
-@[extern "lean_uv_ssl_set_server_name"]
-opaque setServerName (ssl : @& Session.Client) (host : @& String) : IO Unit
-
-end Client
-
-/--
-Gets the X.509 verify result code after handshake.
--/
-@[extern "lean_uv_ssl_verify_result"]
-opaque verifyResult {r : Role} (ssl : @& Session r) : IO UInt64
-
-/--
-Runs one handshake step. Returns `true` when the handshake is complete.
--/
-@[extern "lean_uv_ssl_handshake"]
-opaque handshake {r : Role} (ssl : @& Session r) : IO Bool
-
-/--
-Attempts to write plaintext application data into SSL.
-Returns `true` when accepted, `false` when OpenSSL needs more I/O first.
--/
-@[extern "lean_uv_ssl_write"]
-opaque write {r : Role} (ssl : @& Session r) (data : @& ByteArray) : IO Bool
-
-/--
-Attempts to read decrypted plaintext data. Returns `none` when OpenSSL needs more I/O.
--/
-@[extern "lean_uv_ssl_read"]
-opaque read? {r : Role} (ssl : @& Session r) (maxBytes : UInt64) : IO (Option ByteArray)
-
-/--
-Feeds encrypted TLS bytes into the SSL input BIO.
--/
-@[extern "lean_uv_ssl_feed_encrypted"]
-opaque feedEncrypted {r : Role} (ssl : @& Session r) (data : @& ByteArray) : IO UInt64
-
-/--
-Drains encrypted TLS bytes from the SSL output BIO.
--/
-@[extern "lean_uv_ssl_drain_encrypted"]
-opaque drainEncrypted {r : Role} (ssl : @& Session r) : IO ByteArray
-
-/--
-Returns the amount of encrypted TLS bytes currently pending in the output BIO.
--/
-@[extern "lean_uv_ssl_pending_encrypted"]
-opaque pendingEncrypted {r : Role} (ssl : @& Session r) : IO UInt64
-
-/--
-Returns the amount of decrypted plaintext bytes currently buffered inside the SSL object.
--/
-@[extern "lean_uv_ssl_pending_plaintext"]
-opaque pendingPlaintext {r : Role} (ssl : @& Session r) : IO UInt64
-
-end Session
-
-end Std.Internal.SSL

src/kernel/declaration.h

@@ -224,10 +224,7 @@ public:
     bool is_mutual() const { return kind() == declaration_kind::MutualDefinition; }
     bool is_inductive() const { return kind() == declaration_kind::Inductive; }
     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 declations. */
-    bool has_value() const { return is_definition(); }
+    bool has_value() const { return is_theorem() || is_definition(); }
 
     axiom_val const & to_axiom_val() const { lean_assert(is_axiom()); return static_cast<axiom_val const &>(cnstr_get_ref(raw(), 0)); }
     definition_val const & to_definition_val() const { lean_assert(is_definition()); return static_cast<definition_val const &>(cnstr_get_ref(raw(), 0)); }

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

@@ -111,18 +111,6 @@ public def Package.loadFromEnv
         but then redefined as a '{decl.kind}'"
     else
       return m.insert decl.name (.mk decl rfl)
-  -- Check that executables have distinct root module names
-  let _ ← targetDecls.foldlM (init := ({} : Lean.NameMap Name)) fun exeRoots decl => do
-    if let some exeConfig := decl.config? LeanExe.configKind then
-      let root := exeConfig.root
-      if let some origExe := exeRoots.get? root then
-        error s!"\
-          {self.prettyName}: executable '{decl.name}' has the same root module '{root}' \
-          as executable '{origExe}'"
-      else
-        return exeRoots.insert root decl.name
-    else
-      return exeRoots
   let defaultTargets ← defaultTargetAttr.getAllEntries env |>.mapM fun name =>
     if let some decl := constTargetMap.find? name then pure decl.name else
       error s!"{self.prettyName}: package is missing target '{name}' marked as a default"

src/lake/Lake/Load/Toml.lean

@@ -415,57 +415,35 @@ local macro "gen_toml_decoders%" : command => do
 
 gen_toml_decoders%
 
-private structure DecodeTargetState (pkg : Name) where
-  decls : Array (PConfigDecl pkg) := #[]
-  map : DNameMap (NConfigDecl pkg) := {}
-  exeRoots : Lean.NameMap Name := {}
-
 private def decodeTargetDecls
-  (pkg : Name) (prettyName : String) (t : Table)
+  (pkg : Name) (t : Table)
 : DecodeM (Array (PConfigDecl pkg) × DNameMap (NConfigDecl pkg)) := do
-  let r : DecodeTargetState pkg := {}
+  let r := (#[], {})
   let r ← go r LeanLib.keyword LeanLib.configKind LeanLibConfig.decodeToml
   let r ← go r LeanExe.keyword LeanExe.configKind LeanExeConfig.decodeToml
   let r ← go r InputFile.keyword InputFile.configKind InputFileConfig.decodeToml
   let r ← go r InputDir.keyword InputDir.configKind InputDirConfig.decodeToml
-  return (r.decls, r.map)
+  return r
 where
-  go (r : DecodeTargetState pkg) kw kind
-      (decode : {n : Name} → Table → DecodeM (ConfigType kind pkg n)) := do
+  go r kw kind (decode : {n : Name} → Table → DecodeM (ConfigType kind pkg n)) := do
     let some tableArrayVal := t.find? kw | return r
     let some vals ← tryDecode? tableArrayVal.decodeValueArray | return r
     vals.foldlM (init := r) fun r val => do
       let some t ← tryDecode? val.decodeTable | return r
       let some name ← tryDecode? <| stringToLegalOrSimpleName <$> t.decode `name
         | return r
-      if let some orig := r.map.get? name then
-        logDecodeErrorAt val.ref s!"{prettyName}: \
-          target '{name}' was already defined as a '{orig.kind}', \
+      let (decls, map) := r
+      if let some orig := map.get? name then
+        modify fun es => es.push <| .mk val.ref s!"\
+          {pkg}: target '{name}' was already defined as a '{orig.kind}', \
           but then redefined as a '{kind}'"
-        return r
+        return (decls, map)
       else
         let config ← @decode name t
         let decl : NConfigDecl pkg name :=
           -- Safety: By definition, config kind = facet kind for declarative configurations.
           unsafe {pkg, name, kind, config, wf_data := lcProof}
-        -- Check that executables have distinct root module names
-        let exeRoots ← id do
-          if h : kind = LeanExe.configKind then
-            let exeConfig : LeanExeConfig name := cast (by rw [h]; rfl) config
-            if let some origExe := r.exeRoots.get? exeConfig.root then
-              logDecodeErrorAt val.ref s!"{prettyName}: \
-                executable '{name}' has the same root module '{exeConfig.root}' as \
-                executable '{origExe}'"
-              return r.exeRoots
-            else
-              return r.exeRoots.insert exeConfig.root name
-          else
-            return r.exeRoots
-        return {
-          decls := r.decls.push decl.toPConfigDecl
-          map := r.map.insert name decl
-          exeRoots
-        }
+        return (decls.push decl.toPConfigDecl, map.insert name decl)
 
 /-! ## Root Loader -/
 
@@ -480,9 +458,8 @@ public def loadTomlConfig (cfg: LoadConfig) : LogIO Package := do
       let wsIdx := cfg.pkgIdx
       let baseName := if cfg.pkgName.isAnonymous then origName else cfg.pkgName
       let keyName := baseName.num wsIdx
-      let prettyName := baseName.toString (escape := false)
       let config ← @PackageConfig.decodeToml keyName origName table
-      let (targetDecls, targetDeclMap) ← decodeTargetDecls keyName prettyName table
+      let (targetDecls, targetDeclMap) ← decodeTargetDecls keyName table
       let defaultTargets ← table.tryDecodeD `defaultTargets #[]
       let defaultTargets := defaultTargets.map stringToLegalOrSimpleName
       let depConfigs ← table.tryDecodeD `require #[]

src/lake/Lake/Toml/Decode.lean

@@ -96,9 +96,6 @@ public def mergeErrors (x₁ : EDecodeM α) (x₂ : EDecodeM β) (f : α → β
     | .error _ es => .error () es
   | .error _ es => .error () es
 
-@[inline] public def logDecodeErrorAt (ref : Syntax) (msg : String) : DecodeM Unit :=
-  fun es => .ok () (es.push {ref, msg})
-
 @[inline] public def throwDecodeErrorAt (ref : Syntax) (msg : String) : EDecodeM α :=
   fun es => .error () (es.push {ref, msg})
 

src/runtime/CMakeLists.txt

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

src/runtime/init_module.cpp

@@ -14,9 +14,6 @@ Author: Leonardo de Moura
 #include "runtime/mutex.h"
 #include "runtime/init_module.h"
 #include "runtime/libuv.h"
-#include "runtime/openssl.h"
-#include "runtime/openssl/context.h"
-#include "runtime/openssl/session.h"
 
 namespace lean {
 extern "C" LEAN_EXPORT void lean_initialize_runtime_module() {
@@ -28,9 +25,6 @@ extern "C" LEAN_EXPORT void lean_initialize_runtime_module() {
     initialize_mutex();
     initialize_process();
     initialize_stack_overflow();
-    initialize_openssl();
-    initialize_openssl_context();
-    initialize_openssl_session();
     initialize_libuv();
 }
 void initialize_runtime_module() {
@@ -38,7 +32,6 @@ void initialize_runtime_module() {
 }
 void finalize_runtime_module() {
     finalize_stack_overflow();
-    finalize_openssl();
     finalize_process();
     finalize_mutex();
     finalize_thread();

src/runtime/openssl.cpp

@@ -1,43 +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"
-#include "runtime/io.h"
-
-#ifndef LEAN_EMSCRIPTEN
-#include <openssl/opensslv.h>
-#include <openssl/ssl.h>
-#include <openssl/err.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,16 +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>
-
-namespace lean {
-
-void initialize_openssl();
-void finalize_openssl();
-
-}
-
-extern "C" LEAN_EXPORT lean_obj_res lean_openssl_version(lean_obj_arg);

src/runtime/openssl/context.cpp

@@ -1,155 +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/context.h"
-
-#ifndef LEAN_EMSCRIPTEN
-#include <openssl/err.h>
-#endif
-
-namespace lean {
-
-#ifndef LEAN_EMSCRIPTEN
-
-static inline lean_obj_res mk_ssl_ctx_io_error(char const * where) {
-    unsigned long err = ERR_get_error();
-    char err_buf[256];
-    err_buf[0] = '\0';
-
-    if (err != 0) {
-        ERR_error_string_n(err, err_buf, sizeof(err_buf));
-    }
-
-    ERR_clear_error();
-
-    std::string msg(where);
-    if (err_buf[0] != '\0') {
-        msg += ": ";
-        msg += err_buf;
-    }
-
-    return lean_io_result_mk_error(lean_mk_io_user_error(mk_string(msg.c_str())));
-}
-
-static void configure_ctx_options(SSL_CTX * ctx) {
-    SSL_CTX_set_mode(ctx, SSL_MODE_AUTO_RETRY);
-
-    #ifdef SSL_OP_NO_RENEGOTIATION
-    SSL_CTX_clear_options(ctx, SSL_OP_NO_RENEGOTIATION);
-    #endif
-    #ifdef SSL_OP_ALLOW_CLIENT_RENEGOTIATION
-    SSL_CTX_set_options(ctx, SSL_OP_ALLOW_CLIENT_RENEGOTIATION);
-    #endif
-}
-
-static void lean_ssl_context_finalizer(void * ptr) {
-    lean_ssl_context_object * obj = (lean_ssl_context_object*)ptr;
-    if (obj->ctx != nullptr) {
-        SSL_CTX_free(obj->ctx);
-    }
-    free(obj);
-}
-
-void initialize_openssl_context() {
-    g_ssl_context_external_class = lean_register_external_class(lean_ssl_context_finalizer, [](void * obj, lean_object * f) {
-        (void)obj;
-        (void)f;
-    });
-}
-
-static lean_obj_res mk_ssl_context(const SSL_METHOD * method) {
-    SSL_CTX * ctx = SSL_CTX_new(method);
-    if (ctx == nullptr) {
-        return mk_ssl_ctx_io_error("SSL_CTX_new failed");
-    }
-
-    configure_ctx_options(ctx);
-
-    lean_ssl_context_object * obj = (lean_ssl_context_object*)malloc(sizeof(lean_ssl_context_object));
-    if (obj == nullptr) {
-        SSL_CTX_free(ctx);
-        return mk_ssl_ctx_io_error("failed to allocate SSL context object");
-    }
-
-    obj->ctx = ctx;
-    lean_object * lean_obj = lean_ssl_context_object_new(obj);
-    lean_mark_mt(lean_obj);
-    return lean_io_result_mk_ok(lean_obj);
-}
-
-/* Std.Internal.SSL.Context.mkServer : IO Context */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_ctx_mk_server() {
-    return mk_ssl_context(TLS_server_method());
-}
-
-/* Std.Internal.SSL.Context.mkClient : IO Context */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_ctx_mk_client() {
-    return mk_ssl_context(TLS_client_method());
-}
-
-/* Std.Internal.SSL.Context.configureServer (ctx : @& Context) (certFile keyFile : @& String) : IO Unit */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_ctx_configure_server(b_obj_arg ctx_obj, b_obj_arg cert_file, b_obj_arg key_file) {
-    lean_ssl_context_object * obj = lean_to_ssl_context_object(ctx_obj);
-    const char * cert = lean_string_cstr(cert_file);
-    const char * key = lean_string_cstr(key_file);
-
-    if (SSL_CTX_use_certificate_file(obj->ctx, cert, SSL_FILETYPE_PEM) <= 0) {
-        return mk_ssl_ctx_io_error("SSL_CTX_use_certificate_file failed");
-    }
-    if (SSL_CTX_use_PrivateKey_file(obj->ctx, key, SSL_FILETYPE_PEM) <= 0) {
-        return mk_ssl_ctx_io_error("SSL_CTX_use_PrivateKey_file failed");
-    }
-    if (SSL_CTX_check_private_key(obj->ctx) != 1) {
-        return mk_ssl_ctx_io_error("SSL_CTX_check_private_key failed");
-    }
-
-    return lean_io_result_mk_ok(lean_box(0));
-}
-
-/* Std.Internal.SSL.Context.configureClient (ctx : @& Context) (caFile : @& String) (verifyPeer : Bool) : IO Unit */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_ctx_configure_client(b_obj_arg ctx_obj, b_obj_arg ca_file, uint8_t verify_peer) {
-    lean_ssl_context_object * obj = lean_to_ssl_context_object(ctx_obj);
-    const char * ca = lean_string_cstr(ca_file);
-
-    if (ca != nullptr && ca[0] != '\0') {
-        if (SSL_CTX_load_verify_locations(obj->ctx, ca, nullptr) != 1) {
-            return mk_ssl_ctx_io_error("SSL_CTX_load_verify_locations failed");
-        }
-    } else if (verify_peer) {
-        if (SSL_CTX_set_default_verify_paths(obj->ctx) != 1) {
-            return mk_ssl_ctx_io_error("SSL_CTX_set_default_verify_paths failed");
-        }
-    }
-
-    SSL_CTX_set_verify(obj->ctx, verify_peer ? SSL_VERIFY_PEER : SSL_VERIFY_NONE, nullptr);
-    return lean_io_result_mk_ok(lean_box(0));
-}
-
-#else
-
-void initialize_openssl_context() {}
-
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_ctx_mk_server() {
-    return io_result_mk_error("lean_uv_ssl_ctx_mk_server is not supported");
-}
-
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_ctx_mk_client() {
-    return io_result_mk_error("lean_uv_ssl_ctx_mk_client is not supported");
-}
-
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_ctx_configure_server(b_obj_arg ctx_obj, b_obj_arg cert_file, b_obj_arg key_file) {
-    (void)ctx_obj; (void)cert_file; (void)key_file;
-    return io_result_mk_error("lean_uv_ssl_ctx_configure_server is not supported");
-}
-
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_ctx_configure_client(b_obj_arg ctx_obj, b_obj_arg ca_file, uint8_t verify_peer) {
-    (void)ctx_obj; (void)ca_file; (void)verify_peer;
-    return io_result_mk_error("lean_uv_ssl_ctx_configure_client is not supported");
-}
-
-#endif
-
-}

src/runtime/openssl/context.h

@@ -1,40 +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>
-#include "runtime/io.h"
-#include "runtime/object.h"
-#include "runtime/openssl.h"
-
-#ifndef LEAN_EMSCRIPTEN
-#include <openssl/ssl.h>
-#endif
-
-namespace lean {
-
-static lean_external_class * g_ssl_context_external_class = nullptr;
-void initialize_openssl_context();
-
-#ifndef LEAN_EMSCRIPTEN
-typedef struct {
-    SSL_CTX * ctx;
-} lean_ssl_context_object;
-
-static inline lean_object * lean_ssl_context_object_new(lean_ssl_context_object * c) {
-    return lean_alloc_external(g_ssl_context_external_class, c);
-}
-static inline lean_ssl_context_object * lean_to_ssl_context_object(lean_object * o) {
-    return (lean_ssl_context_object*)(lean_get_external_data(o));
-}
-#endif
-
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_ctx_mk_server();
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_ctx_mk_client();
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_ctx_configure_server(b_obj_arg ctx, b_obj_arg cert_file, b_obj_arg key_file);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_ctx_configure_client(b_obj_arg ctx, b_obj_arg ca_file, uint8_t verify_peer);
-
-}

src/runtime/openssl/session.cpp

@@ -1,490 +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/session.h"
-
-#include <climits>
-#include <cstdlib>
-#include <cstring>
-#include <string>
-
-#ifndef LEAN_EMSCRIPTEN
-#include <openssl/err.h>
-#endif
-
-namespace lean {
-
-#ifndef LEAN_EMSCRIPTEN
-
-static inline lean_object * mk_ssl_error(char const * where, int ssl_err = 0) {
-    unsigned long err = ERR_get_error();
-    char err_buf[256];
-    err_buf[0] = '\0';
-
-    if (err != 0) {
-        ERR_error_string_n(err, err_buf, sizeof(err_buf));
-    }
-
-    // Drain remaining errors so they don't pollute future calls.
-    ERR_clear_error();
-
-    std::string msg(where);
-
-    if (ssl_err != 0) {
-        msg += " (ssl_error=" + std::to_string(ssl_err) + ")";
-    }
-    if (err_buf[0] != '\0') {
-        msg += ": ";
-        msg += err_buf;
-    }
-
-    return lean_mk_io_user_error(mk_string(msg.c_str()));
-}
-
-static inline lean_obj_res mk_ssl_io_error(char const * where, int ssl_err = 0) {
-    return lean_io_result_mk_error(mk_ssl_error(where, ssl_err));
-}
-
-static inline lean_object * mk_empty_byte_array() {
-    lean_object * arr = lean_alloc_sarray(1, 0, 0);
-    lean_sarray_set_size(arr, 0);
-    return arr;
-}
-
-static void free_pending_writes(lean_ssl_session_object * obj) {
-    if (obj->pending_writes != nullptr) {
-        for (size_t i = 0; i < obj->pending_writes_count; i++) {
-            free(obj->pending_writes[i].data);
-        }
-        free(obj->pending_writes);
-        obj->pending_writes = nullptr;
-    }
-    obj->pending_writes_count = 0;
-}
-
-static bool append_pending_write(lean_ssl_session_object * obj, char const * data, size_t size) {
-    char * copy = (char*)malloc(size);
-    if (copy == nullptr) return false;
-
-    std::memcpy(copy, data, size);
-
-    size_t new_count = obj->pending_writes_count + 1;
-    lean_ssl_pending_write * new_arr = (lean_ssl_pending_write*)realloc(
-        obj->pending_writes, sizeof(lean_ssl_pending_write) * new_count
-    );
-
-    if (new_arr == nullptr) {
-        free(copy);
-        return false;
-    }
-
-    obj->pending_writes = new_arr;
-    obj->pending_writes[obj->pending_writes_count].data = copy;
-    obj->pending_writes[obj->pending_writes_count].size = size;
-    obj->pending_writes_count = new_count;
-    return true;
-}
-
-/*
-Return values:
-  1 -> write completed
-  0 -> write blocked (WANT_READ / WANT_WRITE / ZERO_RETURN)
- -1 -> fatal error
-*/
-static int ssl_write_step(lean_ssl_session_object * obj, char const * data, size_t size, int * out_err) {
-    if (size > INT_MAX) {
-        *out_err = SSL_ERROR_SSL;
-        return -1;
-    }
-
-    int rc = SSL_write(obj->ssl, data, (int)size);
-    if (rc > 0) {
-        return 1;
-    }
-
-    int err = SSL_get_error(obj->ssl, rc);
-    *out_err = err;
-    if (err == SSL_ERROR_WANT_READ || err == SSL_ERROR_WANT_WRITE || err == SSL_ERROR_ZERO_RETURN) {
-        return 0;
-    }
-    return -1;
-}
-
-/*
-Return values:
-  1 -> all pending writes flushed
-  0 -> still blocked by renegotiation
- -1 -> fatal error, *out_err filled
-*/
-static int try_flush_pending_writes(lean_ssl_session_object * obj, int * out_err) {
-    if (obj->pending_writes_count == 0) return 1;
-
-    size_t completed = 0;
-
-    for (size_t i = 0; i < obj->pending_writes_count; i++) {
-        lean_ssl_pending_write * pw = &obj->pending_writes[i];
-
-        while (pw->size > 0) {
-            int err = 0;
-            int step = ssl_write_step(obj, pw->data, pw->size, &err);
-
-            if (step == 1) {
-                // We do not enable partial writes, so a successful SSL_write consumes the full buffer.
-                pw->size = 0;
-                continue;
-            }
-
-            if (step == 0) {
-                goto done;
-            }
-
-            *out_err = err;
-            return -1;
-        }
-
-        free(pw->data);
-        pw->data = nullptr;
-        completed++;
-    }
-
-done:
-    if (completed > 0) {
-        obj->pending_writes_count -= completed;
-        if (obj->pending_writes_count == 0) {
-            free(obj->pending_writes);
-            obj->pending_writes = nullptr;
-        } else {
-            std::memmove(
-                obj->pending_writes,
-                obj->pending_writes + completed,
-                sizeof(lean_ssl_pending_write) * obj->pending_writes_count
-            );
-            // Keep memory usage proportional to currently queued writes.
-            lean_ssl_pending_write * shrunk = (lean_ssl_pending_write*)realloc(
-                obj->pending_writes,
-                sizeof(lean_ssl_pending_write) * obj->pending_writes_count
-            );
-            if (shrunk != nullptr) {
-                obj->pending_writes = shrunk;
-            }
-        }
-    }
-
-    return obj->pending_writes_count == 0 ? 1 : 0;
-}
-
-void lean_ssl_session_finalizer(void * ptr) {
-    lean_ssl_session_object * obj = (lean_ssl_session_object*)ptr;
-
-    if (obj->ssl != nullptr) {
-        SSL_free(obj->ssl);
-    }
-
-    free_pending_writes(obj);
-    free(obj);
-}
-
-void initialize_openssl_session() {
-    g_ssl_session_external_class = lean_register_external_class(lean_ssl_session_finalizer, [](void * obj, lean_object * f) {
-        (void)obj;
-        (void)f;
-    });
-}
-
-static lean_obj_res mk_ssl_session(SSL_CTX * ctx, uint8_t is_server) {
-    SSL * ssl = SSL_new(ctx);
-    if (ssl == nullptr) {
-        return mk_ssl_io_error("SSL_new failed");
-    }
-
-    BIO * read_bio = BIO_new(BIO_s_mem());
-    BIO * write_bio = BIO_new(BIO_s_mem());
-
-    if (read_bio == nullptr || write_bio == nullptr) {
-        if (read_bio != nullptr) BIO_free(read_bio);
-        if (write_bio != nullptr) BIO_free(write_bio);
-        SSL_free(ssl);
-        return mk_ssl_io_error("BIO_new failed");
-    }
-
-    BIO_set_nbio(read_bio, 1);
-    BIO_set_nbio(write_bio, 1);
-
-    SSL_set_bio(ssl, read_bio, write_bio);
-    SSL_set_mode(ssl, SSL_MODE_AUTO_RETRY);
-
-    if (is_server) {
-        SSL_set_accept_state(ssl);
-    } else {
-        SSL_set_connect_state(ssl);
-    }
-
-    lean_ssl_session_object * ssl_obj = (lean_ssl_session_object*)malloc(sizeof(lean_ssl_session_object));
-    if (ssl_obj == nullptr) {
-        SSL_free(ssl);
-        return mk_ssl_io_error("failed to allocate SSL session object");
-    }
-
-    ssl_obj->ssl = ssl;
-    ssl_obj->read_bio = read_bio;
-    ssl_obj->write_bio = write_bio;
-    ssl_obj->pending_writes_count = 0;
-    ssl_obj->pending_writes = nullptr;
-
-    lean_object * obj = lean_ssl_session_object_new(ssl_obj);
-    lean_mark_mt(obj);
-    return lean_io_result_mk_ok(obj);
-}
-
-/* Std.Internal.SSL.Session.Server.mk (ctx : @& Context.Server) : IO Session.Server */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_mk_server(b_obj_arg ctx_obj) {
-    lean_ssl_context_object * ctx = lean_to_ssl_context_object(ctx_obj);
-    return mk_ssl_session(ctx->ctx, 1);
-}
-
-/* Std.Internal.SSL.Session.Client.mk (ctx : @& Context.Client) : IO Session.Client */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_mk_client(b_obj_arg ctx_obj) {
-    lean_ssl_context_object * ctx = lean_to_ssl_context_object(ctx_obj);
-    return mk_ssl_session(ctx->ctx, 0);
-}
-
-/* Std.Internal.SSL.Session.setServerName (ssl : @& Session) (host : @& String) : IO Unit */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_set_server_name(b_obj_arg _role, b_obj_arg ssl, b_obj_arg host) {
-    lean_ssl_session_object * ssl_obj = lean_to_ssl_session_object(ssl);
-    const char * server_name = lean_string_cstr(host);
-    if (SSL_set_tlsext_host_name(ssl_obj->ssl, server_name) != 1) {
-        return mk_ssl_io_error("SSL_set_tlsext_host_name failed");
-    }
-    return lean_io_result_mk_ok(lean_box(0));
-}
-
-/* Std.Internal.SSL.Session.verifyResult (ssl : @& Session) : IO UInt64 */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_verify_result(b_obj_arg _role, b_obj_arg ssl) {
-    lean_ssl_session_object * ssl_obj = lean_to_ssl_session_object(ssl);
-    long result = SSL_get_verify_result(ssl_obj->ssl);
-    return lean_io_result_mk_ok(lean_box_uint64((uint64_t)result));
-}
-
-/* Std.Internal.SSL.Session.handshake (ssl : @& Session) : IO Bool */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_handshake(b_obj_arg _role, b_obj_arg ssl) {
-    lean_ssl_session_object * ssl_obj = lean_to_ssl_session_object(ssl);
-    int rc = SSL_do_handshake(ssl_obj->ssl);
-
-    if (rc == 1) {
-        return lean_io_result_mk_ok(lean_box(1));
-    }
-
-    int err = SSL_get_error(ssl_obj->ssl, rc);
-    if (err == SSL_ERROR_WANT_READ || err == SSL_ERROR_WANT_WRITE || err == SSL_ERROR_ZERO_RETURN) {
-        return lean_io_result_mk_ok(lean_box(0));
-    }
-
-    return mk_ssl_io_error("SSL_do_handshake failed", err);
-}
-
-/* Std.Internal.SSL.Session.write (ssl : @& Session) (data : @& ByteArray) : IO Bool */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_write(b_obj_arg _role, b_obj_arg ssl, b_obj_arg data) {
-    lean_ssl_session_object * ssl_obj = lean_to_ssl_session_object(ssl);
-    size_t data_len = lean_sarray_size(data);
-    char const * payload = (char const*)lean_sarray_cptr(data);
-
-    if (data_len == 0) {
-        return lean_io_result_mk_ok(lean_box(1));
-    }
-
-    int err = 0;
-    int step = ssl_write_step(ssl_obj, payload, data_len, &err);
-    if (step == 1) {
-        return lean_io_result_mk_ok(lean_box(1));
-    }
-
-    // If renegotiation blocks writes, queue plaintext and retry after subsequent reads.
-    if (step == 0 && err == SSL_ERROR_WANT_READ) {
-        if (!append_pending_write(ssl_obj, payload, data_len)) {
-            return mk_ssl_io_error("failed to append pending SSL write");
-        }
-        return lean_io_result_mk_ok(lean_box(0));
-    }
-
-    if (step == 0 && (err == SSL_ERROR_WANT_WRITE || err == SSL_ERROR_ZERO_RETURN)) {
-        return lean_io_result_mk_ok(lean_box(0));
-    }
-
-    return mk_ssl_io_error("SSL_write failed", err);
-}
-
-/* Std.Internal.SSL.Session.read? (ssl : @& Session) (maxBytes : UInt64) : IO (Option ByteArray) */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_read(b_obj_arg _role, b_obj_arg ssl, uint64_t max_bytes) {
-    lean_ssl_session_object * ssl_obj = lean_to_ssl_session_object(ssl);
-
-    if (max_bytes == 0) {
-        return lean_io_result_mk_ok(mk_option_some(mk_empty_byte_array()));
-    }
-
-    if (max_bytes > INT_MAX) {
-        max_bytes = INT_MAX;
-    }
-
-    lean_object * out = lean_alloc_sarray(1, 0, max_bytes);
-    int rc = SSL_read(ssl_obj->ssl, (void*)lean_sarray_cptr(out), (int)max_bytes);
-
-    if (rc > 0) {
-        int flush_err = 0;
-        if (try_flush_pending_writes(ssl_obj, &flush_err) < 0) {
-            lean_dec(out);
-            return mk_ssl_io_error("pending SSL write flush failed", flush_err);
-        }
-        lean_sarray_set_size(out, (size_t)rc);
-        return lean_io_result_mk_ok(mk_option_some(out));
-    }
-
-    lean_dec(out);
-
-    int err = SSL_get_error(ssl_obj->ssl, rc);
-    if (err == SSL_ERROR_WANT_READ || err == SSL_ERROR_WANT_WRITE || err == SSL_ERROR_ZERO_RETURN) {
-        int flush_err = 0;
-        if (try_flush_pending_writes(ssl_obj, &flush_err) < 0) {
-            return mk_ssl_io_error("pending SSL write flush failed", flush_err);
-        }
-        return lean_io_result_mk_ok(mk_option_none());
-    }
-
-    return mk_ssl_io_error("SSL_read failed", err);
-}
-
-/* Std.Internal.SSL.Session.feedEncrypted (ssl : @& Session) (data : @& ByteArray) : IO UInt64 */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_feed_encrypted(b_obj_arg _role, b_obj_arg ssl, b_obj_arg data) {
-    lean_ssl_session_object * ssl_obj = lean_to_ssl_session_object(ssl);
-    size_t data_len = lean_sarray_size(data);
-
-    if (data_len == 0) {
-        return lean_io_result_mk_ok(lean_box_uint64(0));
-    }
-
-    if (data_len > INT_MAX) {
-        return mk_ssl_io_error("BIO_write input too large");
-    }
-
-    int rc = BIO_write(ssl_obj->read_bio, lean_sarray_cptr(data), (int)data_len);
-    if (rc >= 0) {
-        return lean_io_result_mk_ok(lean_box_uint64((uint64_t)rc));
-    }
-
-    if (BIO_should_retry(ssl_obj->read_bio)) {
-        return lean_io_result_mk_ok(lean_box_uint64(0));
-    }
-
-    return mk_ssl_io_error("BIO_write failed");
-}
-
-/* Std.Internal.SSL.Session.drainEncrypted (ssl : @& Session) : IO ByteArray */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_drain_encrypted(b_obj_arg _role, b_obj_arg ssl) {
-    lean_ssl_session_object * ssl_obj = lean_to_ssl_session_object(ssl);
-    size_t pending = BIO_ctrl_pending(ssl_obj->write_bio);
-
-    if (pending == 0) {
-        return lean_io_result_mk_ok(mk_empty_byte_array());
-    }
-
-    if (pending > INT_MAX) {
-        return mk_ssl_io_error("BIO_pending output too large");
-    }
-
-    lean_object * out = lean_alloc_sarray(1, 0, pending);
-    int rc = BIO_read(ssl_obj->write_bio, (void*)lean_sarray_cptr(out), (int)pending);
-
-    if (rc >= 0) {
-        lean_sarray_set_size(out, (size_t)rc);
-        return lean_io_result_mk_ok(out);
-    }
-
-    lean_dec(out);
-
-    if (BIO_should_retry(ssl_obj->write_bio)) {
-        return lean_io_result_mk_ok(mk_empty_byte_array());
-    }
-
-    return mk_ssl_io_error("BIO_read failed");
-}
-
-/* Std.Internal.SSL.Session.pendingEncrypted (ssl : @& Session) : IO UInt64 */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_pending_encrypted(b_obj_arg _role, b_obj_arg ssl) {
-    lean_ssl_session_object * ssl_obj = lean_to_ssl_session_object(ssl);
-    return lean_io_result_mk_ok(lean_box_uint64((uint64_t)BIO_ctrl_pending(ssl_obj->write_bio)));
-}
-
-/* Std.Internal.SSL.Session.pendingPlaintext (ssl : @& Session) : IO UInt64 */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_pending_plaintext(b_obj_arg _role, b_obj_arg ssl) {
-    lean_ssl_session_object * ssl_obj = lean_to_ssl_session_object(ssl);
-    return lean_io_result_mk_ok(lean_box_uint64((uint64_t)SSL_pending(ssl_obj->ssl)));
-}
-
-#else
-
-void initialize_openssl_session() {}
-
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_mk_server(b_obj_arg ctx_obj) {
-    (void)ctx_obj;
-    return io_result_mk_error("lean_uv_ssl_mk_server is not supported");
-}
-
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_mk_client(b_obj_arg ctx_obj) {
-    (void)ctx_obj;
-    return io_result_mk_error("lean_uv_ssl_mk_client is not supported");
-}
-
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_set_server_name(b_obj_arg _role, b_obj_arg ssl, b_obj_arg host) {
-    (void)ssl;
-    (void)host;
-    return io_result_mk_error("lean_uv_ssl_set_server_name is not supported");
-}
-
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_verify_result(b_obj_arg _role, b_obj_arg ssl) {
-    (void)ssl;
-    return io_result_mk_error("lean_uv_ssl_verify_result is not supported");
-}
-
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_handshake(b_obj_arg _role, b_obj_arg ssl) {
-    (void)ssl;
-    return io_result_mk_error("lean_uv_ssl_handshake is not supported");
-}
-
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_write(b_obj_arg _role, b_obj_arg ssl, b_obj_arg data) {
-    (void)ssl;
-    (void)data;
-    return io_result_mk_error("lean_uv_ssl_write is not supported");
-}
-
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_read(b_obj_arg _role, b_obj_arg ssl, uint64_t max_bytes) {
-    (void)ssl;
-    (void)max_bytes;
-    return io_result_mk_error("lean_uv_ssl_read is not supported");
-}
-
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_feed_encrypted(b_obj_arg _role, b_obj_arg ssl, b_obj_arg data) {
-    (void)ssl;
-    (void)data;
-    return io_result_mk_error("lean_uv_ssl_feed_encrypted is not supported");
-}
-
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_drain_encrypted(b_obj_arg _role, b_obj_arg ssl) {
-    (void)ssl;
-    return io_result_mk_error("lean_uv_ssl_drain_encrypted is not supported");
-}
-
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_pending_encrypted(b_obj_arg _role, b_obj_arg ssl) {
-    (void)ssl;
-    return io_result_mk_error("lean_uv_ssl_pending_encrypted is not supported");
-}
-
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_pending_plaintext(b_obj_arg _role, b_obj_arg ssl) {
-    (void)ssl;
-    return io_result_mk_error("lean_uv_ssl_pending_plaintext is not supported");
-}
-
-#endif
-
-}

src/runtime/openssl/session.h

@@ -1,53 +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>
-#include "runtime/io.h"
-#include "runtime/object.h"
-#include "runtime/openssl/context.h"
-
-#ifndef LEAN_EMSCRIPTEN
-#include <openssl/ssl.h>
-#include <openssl/bio.h>
-#endif
-
-namespace lean {
-
-static lean_external_class * g_ssl_session_external_class = nullptr;
-void initialize_openssl_session();
-
-#ifndef LEAN_EMSCRIPTEN
-typedef struct {
-    char * data;
-    size_t size;
-} lean_ssl_pending_write;
-
-typedef struct {
-    SSL * ssl;
-    BIO * read_bio;
-    BIO * write_bio;
-    size_t pending_writes_count;
-    lean_ssl_pending_write * pending_writes;
-} lean_ssl_session_object;
-
-static inline lean_object * lean_ssl_session_object_new(lean_ssl_session_object * s) { return lean_alloc_external(g_ssl_session_external_class, s); }
-static inline lean_ssl_session_object * lean_to_ssl_session_object(lean_object * o) { return (lean_ssl_session_object*)(lean_get_external_data(o)); }
-#endif
-
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_mk_server(b_obj_arg ctx);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_mk_client(b_obj_arg ctx);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_set_server_name(b_obj_arg _role, b_obj_arg ssl, b_obj_arg host);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_verify_result(b_obj_arg _role, b_obj_arg ssl);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_handshake(b_obj_arg _role, b_obj_arg ssl);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_write(b_obj_arg _role, b_obj_arg ssl, b_obj_arg data);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_read(b_obj_arg _role, b_obj_arg ssl, uint64_t max_bytes);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_feed_encrypted(b_obj_arg _role, b_obj_arg ssl, b_obj_arg data);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_drain_encrypted(b_obj_arg _role, b_obj_arg ssl);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_pending_encrypted(b_obj_arg _role, b_obj_arg ssl);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_ssl_pending_plaintext(b_obj_arg _role, b_obj_arg ssl);
-
-}