fix: remove check for openssl < 3

.github/workflows/build-template.yml

@@ -59,11 +59,11 @@ jobs:
         with:
           msystem: clang64
           # `:` means do not prefix with msystem
-          pacboy: "make: python: cmake clang ccache gmp libuv git: zip: unzip: diffutils: binutils: tree: zstd tar:"
+          pacboy: "make: python: cmake clang ccache gmp libuv openssl: git: zip: unzip: diffutils: binutils: tree: zstd tar:"
         if: runner.os == 'Windows'
       - name: Install Brew Packages
         run: |
-          brew install ccache tree zstd coreutils gmp libuv
+          brew install ccache tree zstd coreutils gmp libuv openssl
         if: runner.os == 'macOS'
       - name: Checkout
         uses: actions/checkout@v6
@@ -78,7 +78,7 @@ jobs:
       # (needs to be after "Install *" to use the right shell)
       - name: CI Merge Checkout
         run: |
-          git fetch --depth=${{ matrix.name == 'Linux Lake (Cached)' && '10' || '1' }} origin ${{ github.sha }}
+          git fetch --depth=1 origin ${{ github.sha }}
           git checkout FETCH_HEAD flake.nix flake.lock script/prepare-* tests/elab/importStructure.lean
         if: github.event_name == 'pull_request'
       # (needs to be after "Checkout" so files don't get overridden)
@@ -92,7 +92,7 @@ jobs:
         run: |
           sudo dpkg --add-architecture i386
           sudo apt-get update
-          sudo apt-get install -y gcc-multilib g++-multilib ccache libuv1-dev:i386 pkgconf:i386
+          sudo apt-get install -y gcc-multilib g++-multilib ccache libuv1-dev:i386 libssl-dev:i386 pkgconf:i386
         if: matrix.cmultilib
       - name: Restore Cache
         id: restore-cache
@@ -125,7 +125,7 @@ jobs:
           else
             echo "TARGET_STAGE=stage1" >> $GITHUB_ENV
           fi
-      - name: Configure Build
+      - name: Build
         run: |
           ulimit -c unlimited  # coredumps
           [ -d build ] || mkdir build
@@ -162,21 +162,7 @@ jobs:
           fi
           # contortion to support empty OPTIONS with old macOS bash
           cmake .. --preset ${{ matrix.CMAKE_PRESET || 'release' }} -B . ${{ matrix.CMAKE_OPTIONS }} ${OPTIONS[@]+"${OPTIONS[@]}"} -DLEAN_INSTALL_PREFIX=$PWD/..
-      - name: Build Stage 0 & Configure Stage 1
-        run: |
-          ulimit -c unlimited  # coredumps
-          time make -C build stage1-configure -j$NPROC
-      - name: Download Lake Cache
-        if: matrix.name == 'Linux Lake (Cached)'
-        run: |
-          cd src
-          ../build/stage0/bin/lake cache get --repo=${{ github.repository }}
-        timeout-minutes: 20 # prevent excessive hanging from network issues
-        continue-on-error: true
-      - name: Build Target Stage
-        run: |
-          ulimit -c unlimited  # coredumps
-          time make -C build $TARGET_STAGE -j$NPROC
+          time make $TARGET_STAGE -j$NPROC
       # Should be done as early as possible and in particular *before* "Check rebootstrap" which
       # changes the state of stage1/
       - name: Save Cache
@@ -195,21 +181,6 @@ jobs:
             build/stage1/**/*.c
             build/stage1/**/*.c.o*' || '' }}
           key: ${{ steps.restore-cache.outputs.cache-primary-key }}
-      - name: Upload Lake Cache
-        # Caching on cancellation created some mysterious issues perhaps related to improper build
-        # shutdown. Also, since this needs access to secrets, it cannot be run on forks.
-        if: matrix.name == 'Linux Lake' && !cancelled() && (github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name == github.repository)
-        run: |
-          curl --version
-          cd src
-          time ../build/stage0/bin/lake build -o ../build/lake-mappings.jsonl
-          time ../build/stage0/bin/lake cache put ../build/lake-mappings.jsonl --repo=${{ github.repository }}
-        env:
-          LAKE_CACHE_KEY: ${{ secrets.LAKE_CACHE_KEY }}
-          LAKE_CACHE_ARTIFACT_ENDPOINT: ${{ vars.LAKE_CACHE_ENDPOINT }}/a1
-          LAKE_CACHE_REVISION_ENDPOINT: ${{ vars.LAKE_CACHE_ENDPOINT }}/r1
-        timeout-minutes: 20 # prevent excessive hanging from network issues
-        continue-on-error: true
       - name: Install
         run: |
           make -C build/$TARGET_STAGE install

.github/workflows/ci.yml

@@ -244,7 +244,7 @@ jobs:
                 // portable release build: use channel with older glibc (2.26)
                 "name": "Linux release",
                 // usually not a bottleneck so make exclusive to `fast-ci`
-                "os": large && fast ? "nscloud-ubuntu-24.04-amd64-8x16-with-cache" : "ubuntu-latest",
+                "os": large && fast ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
                 "release": true,
                 // Special handling for release jobs. We want:
                 // 1. To run it in PRs so developers get PR toolchains (so secondary without tests is sufficient)
@@ -265,7 +265,7 @@ jobs:
               },
               {
                 "name": "Linux Lake",
-                "os": large ? "nscloud-ubuntu-24.04-amd64-8x16-with-cache" : "ubuntu-latest",
+                "os": large ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
                 "enabled": true,
                 "check-rebootstrap": level >= 1,
                 "check-stage3": level >= 2,
@@ -273,19 +273,7 @@ jobs:
                 // NOTE: `test-bench` currently seems to be broken on `ubuntu-latest`
                 "test-bench": large && level >= 2,
                 // We are not warning-free yet on all platforms, start here
-                "CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-Werror -DUSE_LAKE_CACHE=ON",
-              },
-              {
-                "name": "Linux Lake (Cached)",
-                "os": large ? "nscloud-ubuntu-24.04-amd64-8x16-with-cache" : "ubuntu-latest",
-                "enabled": true,
-                "check-rebootstrap": level >= 1,
-                "check-stage3": level >= 2,
-                "test": true,
-                "secondary": true,
-                // NOTE: `test-bench` currently seems to be broken on `ubuntu-latest`
-                "test-bench": large && level >= 2,
-                "CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-Werror -DUSE_LAKE_CACHE=ON",
+                "CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-Werror",
               },
               {
                 "name": "Linux Reldebug",
@@ -299,7 +287,7 @@ jobs:
               {
                 "name": "Linux fsanitize",
                 // Always run on large if available, more reliable regarding timeouts
-                "os": large ? "nscloud-ubuntu-24.04-amd64-16x32-with-cache" : "ubuntu-latest",
+                "os": large ? "nscloud-ubuntu-22.04-amd64-16x32-with-cache" : "ubuntu-latest",
                 "enabled": level >= 2,
                 // do not fail nightlies on this for now
                 "secondary": level <= 2,

doc/make/index.md

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

doc/make/msys2.md

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

doc/make/osx-10.9.md

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

doc/make/ubuntu.md

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

flake.nix

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

script/prepare-llvm-linux.sh

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

script/prepare-llvm-macos.sh

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

script/prepare-llvm-mingw.sh

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

src/CMakeLists.txt

@@ -356,6 +356,48 @@ 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)
@@ -730,9 +772,9 @@ if(STAGE GREATER 1)
   endif()
 else()
   add_subdirectory(runtime)
-  if(CMAKE_SYSTEM_NAME MATCHES "Emscripten")
-    add_dependencies(leanrt libuv)
-    add_dependencies(leanrt_initial-exec libuv)
+  if("${CMAKE_SYSTEM_NAME}" MATCHES "Emscripten")
+    add_dependencies(leanrt libuv openssl)
+    add_dependencies(leanrt_initial-exec libuv openssl)
   endif()
 
   add_subdirectory(util)

src/Init/Data/Char/Lemmas.lean

@@ -98,8 +98,4 @@ theorem toNat_inj {c d : Char} : c.toNat = d.toNat ↔ c = d := by
 theorem isDigit_iff_toNat {c : Char} : c.isDigit ↔ '0'.toNat ≤ c.toNat ∧ c.toNat ≤ '9'.toNat := by
   simp [isDigit, UInt32.le_iff_toNat_le]
 
-@[simp]
-theorem toNat_mk {val : UInt32} {h} : (Char.mk val h).toNat = val.toNat := by
-  simp [← toNat_val]
-
 end Char

src/Init/Data/Nat/ToString.lean

@@ -298,7 +298,7 @@ theorem ofDigitChars_cons {c : Char} {cs : List Char} {init : Nat} :
   simp [ofDigitChars]
 
 theorem ofDigitChars_cons_digitChar_of_lt_ten {n : Nat} (hn : n < 10) {cs : List Char} {init : Nat} :
-    ofDigitChars b (n.digitChar :: cs) init = ofDigitChars b cs (b * init + n) := by
+    ofDigitChars 10 (n.digitChar :: cs) init = ofDigitChars 10 cs (10 * init + n) := by
   simp [ofDigitChars_cons, Nat.toNat_digitChar_sub_48_of_lt_ten hn]
 
 theorem ofDigitChars_eq_ofDigitChars_zero {l : List Char} {init : Nat} :
@@ -320,17 +320,15 @@ theorem ofDigitChars_replicate_zero {n : Nat} : ofDigitChars b (List.replicate n
   | zero => simp
   | succ n ih => simp [List.replicate_succ, ofDigitChars_cons, ih, Nat.pow_succ, Nat.mul_assoc]
 
-theorem ofDigitChars_toDigits {b n : Nat} (hb' : 1 < b) (hb : b ≤ 10) : ofDigitChars b (toDigits b n) 0 = n := by
-  induction n using base_induction b hb' with
-  | single m hm =>
-    simp [Nat.toDigits_of_lt_base hm, ofDigitChars_cons_digitChar_of_lt_ten (by omega : m < 10)]
-  | digit m k hk hm ih =>
-    rw [← Nat.toDigits_append_toDigits hb' hm hk,
-      ofDigitChars_append, ih, Nat.toDigits_of_lt_base hk,
-      ofDigitChars_cons_digitChar_of_lt_ten (Nat.lt_of_lt_of_le hk hb), ofDigitChars_nil]
-
 @[simp]
-theorem ofDigitChars_ten_toDigits {n : Nat} : ofDigitChars 10 (toDigits 10 n) 0 = n :=
-  ofDigitChars_toDigits (by decide) (by decide)
+theorem ofDigitChars_toDigits {n : Nat} : ofDigitChars 10 (toDigits 10 n) 0 = n := by
+  have : 1 < 10 := by decide
+  induction n using base_induction 10 this with
+  | single m hm =>
+    simp [Nat.toDigits_of_lt_base hm, ofDigitChars_cons_digitChar_of_lt_ten hm]
+  | digit m k hk hm ih =>
+    rw [← Nat.toDigits_append_toDigits this hm hk,
+      ofDigitChars_append, ih, Nat.toDigits_of_lt_base hk,
+      ofDigitChars_cons_digitChar_of_lt_ten hk, ofDigitChars_nil]
 
 end Nat

src/Init/Data/String/Defs.lean

@@ -187,9 +187,6 @@ theorem append_right_inj (s : String) {t₁ t₂ : String} :
 theorem append_assoc {s₁ s₂ s₃ : String} : s₁ ++ s₂ ++ s₃ = s₁ ++ (s₂ ++ s₃) := by
   simp [← toByteArray_inj, ByteArray.append_assoc]
 
-instance : Std.Associative (α := String) (· ++ ·) where
-  assoc _ _ _ := append_assoc
-
 @[simp]
 theorem utf8ByteSize_eq_zero_iff {s : String} : s.utf8ByteSize = 0 ↔ s = "" := by
   refine ⟨fun h => ?_, fun h => h ▸ utf8ByteSize_empty⟩

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

@@ -17,7 +17,7 @@ namespace Std
 /--
 Appends all the elements in the iterator, in order.
 -/
-public def Iter.joinString {α β : Type} [Iterator α Id β] [ToString β]
+public def Iter.joinString {α β : Type} [Iterator α Id β] [IteratorLoop α Id Id] [ToString β]
     (it : Std.Iter (α := α) β) : String :=
   (it.map toString).fold (init := "") (· ++ ·)
 
@@ -25,7 +25,7 @@ public def Iter.joinString {α β : Type} [Iterator α Id β] [ToString β]
 Appends the elements of the iterator into a string, placing the separator {name}`s` between them.
 -/
 @[inline]
-public def Iter.intercalateString {α β : Type} [Iterator α Id β] [ToString β]
+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

src/Init/Data/String/Lemmas.lean

@@ -19,7 +19,6 @@ 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
-public import Init.Data.String.Lemmas.TakeDrop
 import Init.Data.Order.Lemmas
 public import Init.Data.String.Basic
 import Init.Data.Char.Lemmas

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

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Init.Data.String.Basic
-import all Init.Data.String.Basic
 import Init.Data.ByteArray.Lemmas
 import Init.Data.Nat.MinMax
 
@@ -57,11 +56,6 @@ theorem singleton_ne_empty {c : Char} : singleton c ≠ "" := by
 theorem empty_ne_singleton {c : Char} : "" ≠ singleton c := by
   simp
 
-@[simp]
-theorem ofList_cons {c : Char} {l : List Char} :
-    String.ofList (c :: l) = String.singleton c ++ String.ofList l := by
-  simp [← toList_inj]
-
 @[simp]
 theorem Slice.Pos.copy_inj {s : Slice} {p₁ p₂ : s.Pos} : p₁.copy = p₂.copy ↔ p₁ = p₂ := by
   simp [String.Pos.ext_iff, Pos.ext_iff]
@@ -250,46 +244,4 @@ theorem Pos.get_ofToSlice {s : String} {p : (s.toSlice).Pos} {h} :
 @[simp]
 theorem push_empty {c : Char} : "".push c = singleton c := rfl
 
-namespace Slice.Pos
-
-@[simp]
-theorem nextn_zero {s : Slice} {p : s.Pos} : p.nextn 0 = p := by
-  simp [nextn]
-
-theorem nextn_add_one {s : Slice} {p : s.Pos} :
-    p.nextn (n + 1) = if h : p = s.endPos then p else (p.next h).nextn n := by
-  simp [nextn]
-
-@[simp]
-theorem nextn_endPos {s : Slice} : s.endPos.nextn n = s.endPos := by
-  cases n <;> simp [nextn_add_one]
-
-end Slice.Pos
-
-namespace Pos
-
-theorem nextn_eq_nextn_toSlice {s : String} {p : s.Pos} : p.nextn n = Pos.ofToSlice (p.toSlice.nextn n) :=
-  (rfl)
-
-@[simp]
-theorem nextn_zero {s : String} {p : s.Pos} : p.nextn 0 = p := by
-  simp [nextn_eq_nextn_toSlice]
-
-theorem nextn_add_one {s : String} {p : s.Pos} :
-    p.nextn (n + 1) = if h : p = s.endPos then p else (p.next h).nextn n := by
-  simp only [nextn_eq_nextn_toSlice, Slice.Pos.nextn_add_one, endPos_toSlice, toSlice_inj]
-  split <;> simp [Pos.next_toSlice]
-
-theorem nextn_toSlice {s : String} {p : s.Pos} : p.toSlice.nextn n = (p.nextn n).toSlice := by
-  induction n generalizing p with simp_all [nextn_add_one, Slice.Pos.nextn_add_one, apply_dite Pos.toSlice, next_toSlice]
-
-theorem toSlice_nextn {s : String} {p : s.Pos} : (p.nextn n).toSlice = p.toSlice.nextn n :=
-  nextn_toSlice.symm
-
-@[simp]
-theorem nextn_endPos {s : String} : s.endPos.nextn n = s.endPos := by
-  cases n <;> simp [nextn_add_one]
-
-end Pos
-
 end String

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

@@ -11,8 +11,6 @@ import all Init.Data.String.FindPos
 import Init.Data.String.OrderInstances
 import Init.Data.String.Lemmas.Order
 import Init.Data.Order.Lemmas
-import Init.Data.Option.Lemmas
-import Init.ByCases
 
 public section
 
@@ -219,23 +217,6 @@ theorem Pos.prev_next {s : Slice} {p : s.Pos} {h} : (p.next h).prev (by simp) =
 theorem Pos.next_prev {s : Slice} {p : s.Pos} {h} : (p.prev h).next (by simp) = p :=
   next_eq_iff.2 (by simp)
 
-theorem Pos.prev?_eq_dif {s : Slice} {p : s.Pos} : p.prev? = if h : p = s.startPos then none else some (p.prev h) :=
-  (rfl)
-
-theorem Pos.prev?_eq_some_prev {s : Slice} {p : s.Pos} (h : p ≠ s.startPos) : p.prev? = some (p.prev h) := by
-  simp [Pos.prev?, h]
-
-@[simp]
-theorem Pos.prev?_eq_none_iff {s : Slice} {p : s.Pos} : p.prev? = none ↔ p = s.startPos := by
-  simp [Pos.prev?]
-
-theorem Pos.prev?_eq_none {s : Slice} {p : s.Pos} (h : p = s.startPos) : p.prev? = none :=
-  prev?_eq_none_iff.2 h
-
-@[simp]
-theorem Pos.prev?_startPos {s : Slice} : s.startPos.prev? = none := by
-  simp
-
 end Slice
 
 @[simp]
@@ -447,18 +428,10 @@ theorem Pos.toSlice_prev {s : String} {p : s.Pos} {h} :
     (p.prev h).toSlice = p.toSlice.prev (by simpa [toSlice_inj]) := by
   simp [prev]
 
-theorem Pos.ofToSlice_prev {s : String} {p : s.toSlice.Pos} {h} :
-    Pos.ofToSlice (p.prev h) = (Pos.ofToSlice p).prev (by simpa [← toSlice_inj]) := by
-  simp [prev]
-
 theorem Pos.prev_toSlice {s : String} {p : s.Pos} {h} :
     p.toSlice.prev h = (p.prev (by simpa [← toSlice_inj])).toSlice := by
   simp [prev]
 
-theorem Pos.prev_ofToSlice {s : String} {p : s.toSlice.Pos} {h} :
-    (Pos.ofToSlice p).prev h = Pos.ofToSlice (p.prev (by simpa [← ofToSlice_inj])) := by
-  simp [prev]
-
 theorem Pos.prevn_le {s : String} {p : s.Pos} {n : Nat} :
     p.prevn n ≤ p := by
   simpa [Pos.le_iff, ← offset_toSlice] using Slice.Pos.prevn_le
@@ -471,71 +444,4 @@ theorem Pos.prev_next {s : String} {p : s.Pos} {h} : (p.next h).prev (by simp) =
 theorem Pos.next_prev {s : String} {p : s.Pos} {h} : (p.prev h).next (by simp) = p :=
   next_eq_iff.2 (by simp)
 
-theorem Pos.prev?_eq_prev?_toSlice {s : String} {p : s.Pos} : p.prev? = p.toSlice.prev?.map Pos.ofToSlice :=
-  (rfl)
-
-theorem Pos.prev?_toSlice {s : String} {p : s.Pos} : p.toSlice.prev? = p.prev?.map Pos.toSlice := by
-  simp [prev?_eq_prev?_toSlice]
-
-theorem Pos.prev?_eq_dif {s : String} {p : s.Pos} : p.prev? = if h : p = s.startPos then none else some (p.prev h) := by
-  simp [prev?_eq_prev?_toSlice, Slice.Pos.prev?_eq_dif, apply_dite (Option.map Pos.ofToSlice),
-    ofToSlice_prev]
-
-theorem Pos.prev?_eq_some_prev {s : String} {p : s.Pos} (h : p ≠ s.startPos) : p.prev? = some (p.prev h) := by
-  simp [prev?_eq_prev?_toSlice, Slice.Pos.prev?_eq_some_prev (by simpa : p.toSlice ≠ s.toSlice.startPos),
-    ofToSlice_prev]
-
-@[simp]
-theorem Pos.prev?_eq_none_iff {s : String} {p : s.Pos} : p.prev? = none ↔ p = s.startPos := by
-  simp [prev?_eq_prev?_toSlice]
-
-theorem Pos.prev?_eq_none {s : String} {p : s.Pos} (h : p = s.startPos) : p.prev? = none :=
-  prev?_eq_none_iff.2 h
-
-@[simp]
-theorem Pos.prev?_startPos {s : String} : s.startPos.prev? = none := by
-  simp
-
-namespace Slice.Pos
-
-@[simp]
-theorem prevn_zero {s : Slice} {p : s.Pos} : p.prevn 0 = p := by
-  simp [prevn]
-
-theorem prevn_add_one {s : Slice} {p : s.Pos} :
-    p.prevn (n + 1) = if h : p = s.startPos then p else (p.prev h).prevn n := by
-  simp [prevn]
-
-@[simp]
-theorem prevn_startPos {s : Slice} : s.startPos.prevn n = s.startPos := by
-  cases n <;> simp [prevn_add_one]
-
-end Slice.Pos
-
-namespace Pos
-
-theorem prevn_eq_prevn_toSlice {s : String} {p : s.Pos} : p.prevn n = Pos.ofToSlice (p.toSlice.prevn n) :=
-  (rfl)
-
-@[simp]
-theorem prevn_zero {s : String} {p : s.Pos} : p.prevn 0 = p := by
-  simp [prevn_eq_prevn_toSlice]
-
-theorem prevn_add_one {s : String} {p : s.Pos} :
-    p.prevn (n + 1) = if h : p = s.startPos then p else (p.prev h).prevn n := by
-  simp only [prevn_eq_prevn_toSlice, Slice.Pos.prevn_add_one, startPos_toSlice, toSlice_inj]
-  split <;> simp [Pos.prev_toSlice]
-
-theorem prevn_toSlice {s : String} {p : s.Pos} : p.toSlice.prevn n = (p.prevn n).toSlice := by
-  induction n generalizing p with simp_all [prevn_add_one, Slice.Pos.prevn_add_one, apply_dite Pos.toSlice, prev_toSlice]
-
-theorem toSlice_prevn {s : String} {p : s.Pos} : (p.prevn n).toSlice = p.toSlice.prevn n :=
-  prevn_toSlice.symm
-
-@[simp]
-theorem prevn_startPos {s : String} : s.startPos.prevn n = s.startPos := by
-  cases n <;> simp [prevn_add_one]
-
-end Pos
-
 end String

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

@@ -60,23 +60,6 @@ theorem toList_intercalate {s : String} {l : List String} :
   | nil => simp
   | cons hd tl ih => cases tl <;> simp_all
 
-theorem join_eq_foldl : join l = l.foldl (fun r s => r ++ s) "" :=
-  (rfl)
-
-@[simp]
-theorem join_nil : join [] = "" := by
-  simp [join]
-
-@[simp]
-theorem join_cons : join (s :: l) = s ++ join l := by
-  simp only [join, List.foldl_cons, empty_append]
-  conv => lhs; rw [← String.append_empty (s := s)]
-  rw [List.foldl_assoc]
-
-@[simp]
-theorem toList_join {l : List String} : (String.join l).toList = l.flatMap String.toList := by
-  induction l <;> simp_all
-
 namespace Slice
 
 @[simp]
@@ -93,10 +76,6 @@ theorem intercalate_eq {s : Slice} {l : List Slice} :
   | nil => simp [intercalate]
   | cons hd tl ih => cases tl <;> simp_all [intercalate, intercalate.go, intercalateGo_append]
 
-@[simp]
-theorem join_eq {l : List Slice} : join l = String.join (l.map copy) := by
-  simp [join, String.join, List.foldl_map]
-
 end Slice
 
 end String

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

@@ -18,13 +18,14 @@ namespace Std.Iter
 
 @[simp]
 public theorem joinString_eq {α β : Type} [Std.Iterator α Id β] [Std.Iterators.Finite α Id]
-    [ToString β] {it : Std.Iter (α := α) β} :
-    it.joinString = String.join (it.toList.map toString) := by
+    [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]
-    [ToString β] {s : String.Slice} {it : Std.Iter (α := α) β} :
+    [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

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

@@ -8,8 +8,6 @@ module
 prelude
 public import Init.Data.String.Search
 import all Init.Data.String.Search
-import Init.Data.String.Lemmas.Slice
-import Init.Data.String.Lemmas.FindPos
 
 public section
 
@@ -30,42 +28,4 @@ theorem Pos.le_find {s : String} (pos : s.Pos) (pattern : ρ) [ToForwardSearcher
     pos ≤ pos.find pattern := by
   simp [Pos.find, ← toSlice_le]
 
-@[simp]
-theorem front?_toSlice {s : String} : s.toSlice.front? = s.front? :=
-  (rfl)
-
-theorem front?_eq_get? {s : String} : s.front? = s.startPos.get? := by
-  simp [← front?_toSlice, ← Pos.get?_toSlice, Slice.front?_eq_get?]
-
-theorem front?_eq {s : String} : s.front? = s.toList.head? := by
-  simp [← front?_toSlice, Slice.front?_eq]
-
-@[simp]
-theorem front_toSlice {s : String} : s.toSlice.front = s.front :=
-  (rfl)
-
-@[simp]
-theorem front_eq {s : String} : s.front = s.front?.getD default := by
-  simp [← front_toSlice, Slice.front_eq]
-
-@[simp]
-theorem back?_toSlice {s : String} : s.toSlice.back? = s.back? :=
-  (rfl)
-
-theorem back?_eq_get? {s : String} : s.back? = s.endPos.prev?.bind Pos.get? := by
-  simp only [← back?_toSlice, Slice.back?_eq_get?, endPos_toSlice, Slice.Pos.prev?_eq_dif,
-    startPos_toSlice, Pos.toSlice_inj, Pos.prev?_eq_dif]
-  split <;> simp [← Pos.get?_toSlice, Pos.toSlice_prev]
-
-theorem back?_eq {s : String} : s.back? = s.toList.getLast? := by
-  simp [← back?_toSlice, Slice.back?_eq]
-
-@[simp]
-theorem back_toSlice {s : String} : s.toSlice.back = s.back :=
-  (rfl)
-
-@[simp]
-theorem back_eq {s : String} : s.back = s.back?.getD default := by
-  simp [← back_toSlice, Slice.back_eq]
-
 end String

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

@@ -11,8 +11,6 @@ import all Init.Data.String.Slice
 import Init.Data.String.Lemmas.Pattern.Memcmp
 import Init.Data.String.Lemmas.Basic
 import Init.Data.ByteArray.Lemmas
-import Init.Data.String.Lemmas.IsEmpty
-import Init.Data.String.Lemmas.FindPos
 
 public section
 
@@ -54,85 +52,4 @@ theorem beq_list_eq_decide {l l' : List String.Slice} :
 
 end BEq
 
-namespace Pos
-
-theorem get?_eq_dif {s : Slice} {p : s.Pos} : p.get? = if h : p = s.endPos then none else some (p.get h) :=
-  (rfl)
-
-theorem get?_eq_some_get {s : Slice} {p : s.Pos} (h : p ≠ s.endPos) : p.get? = some (p.get h) := by
-  simp [Pos.get?, h]
-
-@[simp]
-theorem get?_eq_none_iff {s : Slice} {p : s.Pos} : p.get? = none ↔ p = s.endPos := by
-  simp [Pos.get?]
-
-theorem get?_eq_none {s : Slice} {p : s.Pos} (h : p = s.endPos) : p.get? = none :=
-  get?_eq_none_iff.2 h
-
-@[simp]
-theorem get?_endPos {s : Slice} : s.endPos.get? = none := by
-  simp
-
-end Pos
-
-end Slice
-
-namespace Pos
-
-theorem get?_toSlice {s : String} {p : s.Pos} : p.toSlice.get? = p.get? :=
-  (rfl)
-
-theorem get?_eq_dif {s : String} {p : s.Pos} : p.get? = if h : p = s.endPos then none else some (p.get h) := by
-  simp [← get?_toSlice, Slice.Pos.get?_eq_dif]
-
-theorem get?_eq_some_get {s : String} {p : s.Pos} (h : p ≠ s.endPos) : p.get? = some (p.get h) := by
-  simpa [← get?_toSlice] using Slice.Pos.get?_eq_some_get (by simpa)
-
-@[simp]
-theorem get?_eq_none_iff {s : String} {p : s.Pos} : p.get? = none ↔ p = s.endPos := by
-  simp [← get?_toSlice]
-
-theorem get?_eq_none {s : String} {p : s.Pos} (h : p = s.endPos) : p.get? = none :=
-  get?_eq_none_iff.2 h
-
-@[simp]
-theorem get?_endPos {s : String} : s.endPos.get? = none := by
-  simp
-
-end Pos
-
-namespace Slice
-
-theorem front?_eq_get? {s : Slice} : s.front? = s.startPos.get? :=
-  (rfl)
-
-theorem front?_eq {s : Slice} : s.front? = s.copy.toList.head? := by
-  simp only [front?_eq_get?, Pos.get?_eq_dif]
-  split
-  · simp_all [startPos_eq_endPos_iff, eq_comm (a := none)]
-  · rename_i h
-    obtain ⟨t, ht⟩ := s.splits_startPos.exists_eq_singleton_append h
-    simp [ht]
-
-@[simp]
-theorem front_eq {s : Slice} : s.front = s.front?.getD default := by
-  simp [front]
-
-theorem back?_eq_get? {s : Slice} : s.back? = s.endPos.prev?.bind Pos.get? :=
-  (rfl)
-
-theorem back?_eq {s : Slice} : s.back? = s.copy.toList.getLast? := by
-  simp [back?_eq_get?, Pos.prev?_eq_dif]
-  split
-  · simp_all [startPos_eq_endPos_iff, eq_comm (a := s.endPos), eq_comm (a := none)]
-  · rename_i h
-    obtain ⟨t, ht⟩ := s.splits_endPos.exists_eq_append_singleton_of_ne_startPos h
-    simp [ht, Pos.get?_eq_some_get]
-
-@[simp]
-theorem back_eq {s : Slice} : s.back = s.back?.getD default := by
-  simp [back]
-
-end Slice
-
-end String
+end String.Slice

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

@@ -17,8 +17,6 @@ import Init.Data.String.OrderInstances
 import Init.Data.Nat.Order
 import Init.Omega
 import Init.Data.String.Lemmas.FindPos
-import Init.Data.List.TakeDrop
-import Init.Data.List.Nat.TakeDrop
 
 /-!
 # `Splits` predicates on `String.Pos` and `String.Slice.Pos`.
@@ -651,51 +649,4 @@ theorem Slice.splits_slice {s : Slice} {p₀ p₁ : s.Pos} (h) (p : (s.slice p
     p.Splits (s.slice p₀ (Pos.ofSlice p) Pos.le_ofSlice).copy (s.slice (Pos.ofSlice p) p₁ Pos.ofSlice_le).copy := by
   simpa using p.splits
 
-theorem Slice.Pos.Splits.nextn {s : Slice} {t₁ t₂ : String} {p : s.Pos} (h : p.Splits t₁ t₂) (n : Nat) :
-    (p.nextn n).Splits (t₁ ++ String.ofList (t₂.toList.take n)) (String.ofList (t₂.toList.drop n)) := by
-  induction n generalizing p t₁ t₂ with
-  | zero => simpa
-  | succ n ih =>
-    rw [Pos.nextn_add_one]
-    split
-    · simp_all
-    · obtain ⟨t₂, rfl⟩ := h.exists_eq_singleton_append ‹_›
-      simpa [← append_assoc] using ih h.next
-
-theorem Slice.splits_nextn_startPos (s : Slice) (n : Nat) :
-    (s.startPos.nextn n).Splits (String.ofList (s.copy.toList.take n)) (String.ofList (s.copy.toList.drop n)) := by
-  simpa using s.splits_startPos.nextn n
-
-theorem Pos.Splits.nextn {s t₁ t₂ : String} {p : s.Pos} (h : p.Splits t₁ t₂) (i : Nat) :
-    (p.nextn i).Splits (t₁ ++ String.ofList (t₂.toList.take i)) (String.ofList (t₂.toList.drop i)) := by
-  simpa [← splits_toSlice_iff, toSlice_nextn] using h.toSlice.nextn i
-
-theorem splits_nextn_startPos (s : String) (n : Nat) :
-    (s.startPos.nextn n).Splits (String.ofList (s.toList.take n)) (String.ofList (s.toList.drop n)) := by
-  simpa using s.splits_startPos.nextn n
-
-theorem Slice.Pos.Splits.prevn {s : Slice} {t₁ t₂ : String} {p : s.Pos} (h : p.Splits t₁ t₂) (n : Nat) :
-    (p.prevn n).Splits (String.ofList (t₁.toList.take (t₁.length - n))) (String.ofList (t₁.toList.drop (t₁.length - n)) ++ t₂) := by
-  induction n generalizing p t₁ t₂ with
-  | zero => simpa [← String.length_toList]
-  | succ n ih =>
-    rw [Pos.prevn_add_one]
-    split
-    · simp_all
-    · obtain ⟨t₂, rfl⟩ := h.exists_eq_append_singleton_of_ne_startPos ‹_›
-      simpa [Nat.add_sub_add_right, List.take_append, List.drop_append, ← append_assoc] using ih h.prev
-
-theorem Slice.splits_prevn_endPos (s : Slice) (n : Nat) :
-    (s.endPos.prevn n).Splits (String.ofList (s.copy.toList.take (s.copy.length - n)))
-      (String.ofList (s.copy.toList.drop (s.copy.length - n))) := by
-  simpa using s.splits_endPos.prevn n
-
-theorem Pos.Splits.prevn {s t₁ t₂ : String} {p : s.Pos} (h : p.Splits t₁ t₂) (n : Nat) :
-    (p.prevn n).Splits (String.ofList (t₁.toList.take (t₁.length - n))) (String.ofList (t₁.toList.drop (t₁.length - n)) ++ t₂) := by
-  simpa [← splits_toSlice_iff, toSlice_prevn] using h.toSlice.prevn n
-
-theorem splits_prevn_endPos (s : String) (n : Nat) :
-    (s.endPos.prevn n).Splits (String.ofList (s.toList.take (s.length - n))) (String.ofList (s.toList.drop (s.length - n))) := by
-  simpa using s.splits_endPos.prevn n
-
 end String

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

@@ -1,86 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: Julia Markus Himmel
--/
-module
-
-prelude
-public import Init.Data.String.TakeDrop
-import all Init.Data.String.Slice
-import all Init.Data.String.TakeDrop
-import Init.Data.String.Lemmas.Splits
-
-public section
-
-namespace String
-
-namespace Slice
-
-theorem drop_eq_sliceFrom {s : Slice} {n : Nat} : s.drop n = s.sliceFrom (s.startPos.nextn n) :=
-  (rfl)
-
-@[simp]
-theorem toList_copy_drop {s : Slice} {n : Nat} : (s.drop n).copy.toList = s.copy.toList.drop n := by
-  simp [drop_eq_sliceFrom, (s.splits_nextn_startPos n).copy_sliceFrom_eq]
-
-theorem dropEnd_eq_sliceTo {s : Slice} {n : Nat} : s.dropEnd n = s.sliceTo (s.endPos.prevn n) :=
-  (rfl)
-
-@[simp]
-theorem toList_copy_dropEnd {s : Slice} {n : Nat} :
-    (s.dropEnd n).copy.toList = s.copy.toList.take (s.copy.length - n) := by
-  simp [dropEnd_eq_sliceTo, (s.splits_prevn_endPos n).copy_sliceTo_eq]
-
-theorem take_eq_sliceTo {s : Slice} {n : Nat} : s.take n = s.sliceTo (s.startPos.nextn n) :=
-  (rfl)
-
-@[simp]
-theorem toList_copy_take {s : Slice} {n : Nat} : (s.take n).copy.toList = s.copy.toList.take n := by
-  simp [take_eq_sliceTo, (s.splits_nextn_startPos n).copy_sliceTo_eq]
-
-theorem takeEnd_eq_sliceFrom {s : Slice} {n : Nat} : s.takeEnd n = s.sliceFrom (s.endPos.prevn n) :=
-  (rfl)
-
-@[simp]
-theorem toList_copy_takeEnd {s : Slice} {n : Nat} :
-    (s.takeEnd n).copy.toList = s.copy.toList.drop (s.copy.length - n) := by
-  simp [takeEnd_eq_sliceFrom, (s.splits_prevn_endPos n).copy_sliceFrom_eq]
-
-end Slice
-
-@[simp]
-theorem drop_toSlice {s : String} {n : Nat} : s.toSlice.drop n = s.drop n :=
-  (rfl)
-
-@[simp]
-theorem toList_copy_drop {s : String} {n : Nat} : (s.drop n).copy.toList = s.toList.drop n := by
-  simp [← drop_toSlice]
-
-@[simp]
-theorem dropEnd_toSlice {s : String} {n : Nat} : s.toSlice.dropEnd n = s.dropEnd n :=
-  (rfl)
-
-@[simp]
-theorem toList_copy_dropEnd {s : String} {n : Nat} :
-    (s.dropEnd n).copy.toList = s.toList.take (s.length - n) := by
-  simp [← dropEnd_toSlice]
-
-@[simp]
-theorem take_toSlice {s : String} {n : Nat} : s.toSlice.take n = s.take n :=
-  (rfl)
-
-@[simp]
-theorem toList_copy_take {s : String} {n : Nat} : (s.take n).copy.toList = s.toList.take n := by
-  simp [← take_toSlice]
-
-@[simp]
-theorem takeEnd_toSlice {s : String} {n : Nat} : s.toSlice.takeEnd n = s.takeEnd n :=
-  (rfl)
-
-@[simp]
-theorem toList_copy_takeEnd {s : String} {n : Nat} :
-    (s.takeEnd n).copy.toList = s.toList.drop (s.length - n) := by
-  simp [← takeEnd_toSlice]
-
-end String

src/Init/Data/String/Slice.lean

@@ -1152,19 +1152,6 @@ where go (acc : String) (s : Slice) : List Slice → String
   | a :: as => go (acc ++ s ++ a) s as
   | []      => acc
 
-/--
-Appends all the slices in a list of slices, in order.
-
-Use {name}`String.Slice.intercalate` to place a separator string between the strings in a list.
-
-Examples:
- * {lean}`String.Slice.join ["gr", "ee", "n"] = "green"`
- * {lean}`String.Slice.join ["b", "", "l", "", "ue"] = "blue"`
- * {lean}`String.Slice.join [] = ""`
--/
-def join (l : List String.Slice) : String :=
-  l.foldl (fun (r : String) (s : String.Slice) => r ++ s) ""
-
 /--
 Converts a string to the Lean compiler's representation of names. The resulting name is
 hierarchical, and the string is split at the dots ({lean}`'.'`).

src/Init/Prelude.lean

@@ -185,21 +185,15 @@ example : foo.default = (default, default) :=
 abbrev inferInstance {α : Sort u} [i : α] : α := i
 
 set_option checkBinderAnnotations false in
-/-- `inferInstanceAs α` synthesizes an instance of type `α`, transporting it from a
-definitionally equal type if necessary. This is useful when `α` is definitionally equal to
-some `α'` for which instances are registered, as it prevents leaking the definition's RHS
-at lower transparencies.
-
-`inferInstanceAs` requires an expected type from context. If you just need to synthesize an
-instance without transporting between types, use `inferInstance` instead.
-
-Example:
+/-- `inferInstanceAs α` synthesizes an instance of type `α` and normalizes it to
+"instance normal form": the result is a constructor application whose sub-instance fields
+are canonical instances and whose types match `α` exactly. This is useful when `α` is
+definitionally equal to some `α'` for which instances are registered, as it prevents
+leaking the definition's RHS at lower transparencies. See `Lean.Meta.InstanceNormalForm`
+for details. Example:
 ```
-def D := Nat
-instance : Inhabited D := inferInstanceAs (Inhabited Nat)
+#check inferInstanceAs (Inhabited Nat) -- Inhabited Nat
 ```
-
-See `Lean.Meta.WrapInstance` for details.
 -/
 abbrev «inferInstanceAs» (α : Sort u) [i : α] : α := i
 
@@ -3267,7 +3261,7 @@ Version of `Array.get!Internal` that does not increment the reference count of i
 This is only intended for direct use by the compiler.
 -/
 @[extern "lean_array_get_borrowed"]
-unsafe opaque Array.get!InternalBorrowed {α : Type u} [@&Inhabited α] (a : @& Array α) (i : @& Nat) : α
+unsafe opaque Array.get!InternalBorrowed {α : Type u} [Inhabited α] (a : @& Array α) (i : @& Nat) : α
 
 /--
 Use the indexing notation `a[i]!` instead.
@@ -3275,7 +3269,7 @@ Use the indexing notation `a[i]!` instead.
 Access an element from an array, or panic if the index is out of bounds.
 -/
 @[extern "lean_array_get"]
-def Array.get!Internal {α : Type u} [@&Inhabited α] (a : @& Array α) (i : @& Nat) : α :=
+def Array.get!Internal {α : Type u} [Inhabited α] (a : @& Array α) (i : @& Nat) : α :=
   Array.getD a i default
 
 /--
@@ -3654,8 +3648,8 @@ will prevent the actual monad from being "copied" to the code being specialized.
 When we reimplement the specializer, we may consider copying `inst` if it also
 occurs outside binders or if it is an instance.
 -/
-@[never_extract, extern "lean_panic_fn_borrowed"]
-def panicCore {α : Sort u} [@&Inhabited α] (msg : String) : α := default
+@[never_extract, extern "lean_panic_fn"]
+def panicCore {α : Sort u} [Inhabited α] (msg : String) : α := default
 
 /--
 `(panic "msg" : α)` has a built-in implementation which prints `msg` to

src/Lean/Compiler/LCNF/InferBorrow.lean

@@ -243,19 +243,13 @@ def OwnReason.isForced (reason : OwnReason) : Bool :=
   -- All of these reasons propagate through ABI decisions and can thus safely be ignored as they
   -- will be accounted for by the reference counting pass.
   | .constructorArg .. | .functionCallArg .. | .fvarCall .. | .partialApplication ..
-  | .jpArgPropagation ..
-  -- forward propagation can never affect a user-annotated parameter
-  | .forwardProjectionProp ..
-  -- backward propagation on a user-annotated parameter is only necessary if the projected value
-  -- directly flows into a reset-reuse. However, the borrow annotation propagator ensures this
-  -- situation never arises
-  | .backwardProjectionProp .. => false
+  | .jpArgPropagation .. => false
   -- Results of functions and constructors are naturally owned.
   | .constructorResult .. | .functionCallResult ..
   -- We cannot pass borrowed values to reset or have borrow annotations destroy tail calls for
   -- correctness reasons.
-  | .resetReuse .. | .tailCallPreservation .. | .jpTailCallPreservation ..
-  | .ownedAnnotation => true
+  | .resetReuse .. | .tailCallPreservation .. | .jpTailCallPreservation .. | .ownedAnnotation
+  | .forwardProjectionProp .. | .backwardProjectionProp .. => true
 
 /--
 Infer the borrowing annotations in a SCC through dataflow analysis.

src/Lean/Compiler/LCNF/OtherDecl.lean

@@ -21,6 +21,6 @@ def getOtherDeclType (declName : Name) (us : List Level := []) : CompilerM Expr
   match (← getPhase) with
   | .base => getOtherDeclBaseType declName us
   | .mono => getOtherDeclMonoType declName
-  | .impure => throwError "getOtherDeclType unsupported for impure"
+  | .impure => getOtherDeclImpureType declName
 
 end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/PrettyPrinter.lean

@@ -154,18 +154,16 @@ mutual
       return f!"oset {← ppFVar fvarId} [{i}] := {← ppArg y};" ++ .line ++ (← ppCode k)
     | .setTag fvarId cidx k _ =>
       return f!"setTag {← ppFVar fvarId} := {cidx};" ++ .line ++ (← ppCode k)
-    | .inc fvarId n check persistent k _ =>
-      let ann := (if persistent then "[persistent]" else "") ++ (if !check then "[ref]" else "")
+    | .inc fvarId n _ _ k _ =>
       if n != 1 then
-        return f!"inc[{n}]{ann} {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
+        return f!"inc[{n}] {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
       else
-        return f!"inc{ann} {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
-    | .dec fvarId n check persistent k _ =>
-      let ann := (if persistent then "[persistent]" else "") ++ (if !check then "[ref]" else "")
+        return f!"inc {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
+    | .dec fvarId n _ _ k _ =>
       if n != 1 then
-        return f!"dec[{n}]{ann} {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
+        return f!"dec[{n}] {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
       else
-        return f!"dec{ann} {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
+        return f!"dec {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
     | .del fvarId k _ =>
       return f!"del {← ppFVar fvarId};" ++ .line ++ (← ppCode k)
 

src/Lean/Compiler/LCNF/ToImpureType.lean

@@ -240,4 +240,12 @@ where fillCache := do
       fieldInfo := fields
     }
 
+public def getOtherDeclImpureType (declName : Name) : CoreM Expr := do
+  match (← impureTypeExt.find? declName) with
+  | some type => return type
+  | none =>
+    let type ← toImpureType (← getOtherDeclMonoType declName)
+    monoTypeExt.insert declName type
+    return type
+
 end Lean.Compiler.LCNF

src/Lean/Elab/BuiltinTerm.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Lean.Meta.Diagnostics
-public import Lean.Meta.WrapInstance
+public import Lean.Meta.InstanceNormalForm
 public import Lean.Elab.Open
 public import Lean.Elab.SetOption
 public import Lean.Elab.Eval
@@ -315,16 +315,9 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
   | _ => panic! "resolveId? returned an unexpected expression"
 
 @[builtin_term_elab Lean.Parser.Term.inferInstanceAs] def elabInferInstanceAs : TermElab := fun stx expectedType? => do
+  let expectedType ← tryPostponeIfHasMVars expectedType? "`inferInstanceAs` failed"
   -- The type argument is the last child (works for both `inferInstanceAs T` and `inferInstanceAs <| T`)
   let typeStx := stx[stx.getNumArgs - 1]!
-  if !backward.inferInstanceAs.wrap.get (← getOptions) then
-    return (← elabTerm (← `(_root_.inferInstanceAs $(⟨typeStx⟩))) expectedType?)
-
-  let some expectedType ← tryPostponeIfHasMVars? expectedType? |
-    throwError (m!"`inferInstanceAs` failed, expected type contains metavariables{indentD expectedType?}" ++
-      .note "`inferInstanceAs` requires full knowledge of the expected (\"target\") type to do its \
-        instance translation. If you do not intend to transport instances between two types, \
-        consider using `inferInstance` or `(inferInstance : expectedType)` instead.")
   let type ← withSynthesize (postpone := .yes) <| elabType typeStx
   -- Unify with expected type to resolve metavariables (e.g., `_` placeholders)
   discard <| isDefEq type expectedType
@@ -334,10 +327,10 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
   let type ← abstractInstImplicitArgs type
   let inst ← synthInstance type
   let inst ← if backward.inferInstanceAs.wrap.get (← getOptions) then
-    -- Wrap instance so its type matches the expected type exactly.
+    -- Normalize to instance normal form.
     let logCompileErrors := !(← read).isNoncomputableSection && !(← read).declName?.any (Lean.isNoncomputable (← getEnv))
-    let isMeta := (← read).declName?.any (isMarkedMeta (← getEnv))
-    withNewMCtxDepth <| wrapInstance inst expectedType (logCompileErrors := logCompileErrors) (isMeta := isMeta)
+    let isMeta := (← read).isMetaSection
+    withNewMCtxDepth <| normalizeInstance inst expectedType (logCompileErrors := logCompileErrors) (isMeta := isMeta)
   else
     pure inst
   ensureHasType expectedType? inst

src/Lean/Elab/Deriving/Basic.lean

@@ -9,7 +9,7 @@ prelude
 public import Lean.Elab.App
 public import Lean.Elab.DeclNameGen
 import Lean.Compiler.NoncomputableAttr
-import Lean.Meta.WrapInstance
+import Lean.Meta.InstanceNormalForm
 
 public section
 
@@ -211,19 +211,19 @@ def processDefDeriving (view : DerivingClassView) (decl : Expr) (isNoncomputable
           -- We don't reduce because of abbreviations such as `DecidableEq`
           forallTelescope classExpr fun _ classExpr => do
             let result ← mkInst classExpr declName decl value
-            -- Save the pre-wrapping value for the noncomputable check below,
-            -- since `wrapInstance` may inline noncomputable constants.
+            -- Save the pre-normalization value for the noncomputable check below,
+            -- since `normalizeInstance` may inline noncomputable constants.
             let preNormClosure ← Closure.mkValueTypeClosure result.instType result.instVal (zetaDelta := true)
-            -- Compute instance name early so `wrapInstance` can use it for aux def naming.
+            -- Compute instance name early so `normalizeInstance` can use it for aux def naming.
             let env ← getEnv
             let mut instName := (← getCurrNamespace) ++ (← NameGen.mkBaseNameWithSuffix "inst" preNormClosure.type)
             instName ← liftMacroM <| mkUnusedBaseName instName
             if isPrivateName declName then
               instName := mkPrivateName env instName
-            let isMeta := (← read).declName?.any (isMarkedMeta (← getEnv))
+            let isMeta := (← read).isMetaSection
             let inst ← if backward.inferInstanceAs.wrap.get (← getOptions) then
               withDeclNameForAuxNaming instName <| withNewMCtxDepth <|
-                wrapInstance result.instVal result.instType
+                normalizeInstance result.instVal result.instType
                   (logCompileErrors := false)  -- covered by noncomputable check below
                   (isMeta := isMeta)
             else

src/Lean/Elab/PreDefinition/Basic.lean

@@ -10,7 +10,7 @@ public import Lean.Compiler.NoncomputableAttr
 public import Lean.Util.NumApps
 public import Lean.Meta.Eqns
 public import Lean.Elab.RecAppSyntax
-public import Lean.Meta.WrapInstance
+public import Lean.Meta.InstanceNormalForm
 public import Lean.Elab.DefView
 public section
 

src/Lean/Expr.lean

@@ -73,7 +73,7 @@ inductive BinderInfo where
   | default
   /-- Implicit binder annotation, e.g., `{x : α}` -/
   | implicit
-  /-- Strict implicit binder annotation, e.g., `⦃x : α⦄` -/
+  /-- Strict implicit binder annotation, e.g., `{{ x : α }}` -/
   | strictImplicit
   /-- Local instance binder annotation, e.g., `[Decidable α]` -/
   | instImplicit
@@ -107,7 +107,7 @@ def BinderInfo.isImplicit : BinderInfo → Bool
   | BinderInfo.implicit => true
   | _                   => false
 
-/-- Return `true` if the given `BinderInfo` is a strict implicit annotation (e.g., `⦃α : Type u⦄`) -/
+/-- Return `true` if the given `BinderInfo` is a strict implicit annotation (e.g., `{{α : Type u}}`) -/
 def BinderInfo.isStrictImplicit : BinderInfo → Bool
   | BinderInfo.strictImplicit => true
   | _                         => false

src/Lean/Meta.lean

@@ -27,7 +27,7 @@ public import Lean.Meta.Match
 public import Lean.Meta.ReduceEval
 public import Lean.Meta.Closure
 public import Lean.Meta.AbstractNestedProofs
-public import Lean.Meta.WrapInstance
+public import Lean.Meta.InstanceNormalForm
 public import Lean.Meta.LetToHave
 public import Lean.Meta.ForEachExpr
 public import Lean.Meta.Transform

src/Lean/Meta/InstanceNormalForm.lean

@@ -13,16 +13,17 @@ public import Lean.Meta.CtorRecognizer
 public section
 
 /-!
-# Instance Wrapping
+# Instance Normal Form
 
-Both `inferInstanceAs` and the default `deriving` handler wrap instance bodies to ensure
-that when deriving or inferring an instance for a semireducible type definition, the
-definition's RHS is not leaked when reduced at lower than semireducible transparency.
+Both `inferInstanceAs` and the default `deriving` handler normalize instance bodies to
+"instance normal form". This ensures that when deriving or inferring an instance for a
+semireducible type definition, the definition's RHS is not leaked when reduced at lower
+than semireducible transparency.
 
 ## Algorithm
 
 Given an instance `i : I` and expected type `I'` (where `I'` must be mvar-free),
-`wrapInstance` constructs a result instance as follows, executing all steps at
+`normalizeInstance` constructs a result instance as follows, executing all steps at
 `instances` transparency:
 
 1. If `I'` is not a class, return `i` unchanged.
@@ -45,7 +46,7 @@ Given an instance `i : I` and expected type `I'` (where `I'` must be mvar-free),
 
 ## Options
 
-- `backward.inferInstanceAs.wrap`: master switch for wrapping in both `inferInstanceAs`
+- `backward.inferInstanceAs.wrap`: master switch for normalization in both `inferInstanceAs`
   and the default `deriving` handler
 - `backward.inferInstanceAs.wrap.reuseSubInstances`: reuse existing instances for sub-instance
   fields to avoid non-defeq instance diamonds
@@ -58,7 +59,7 @@ namespace Lean.Meta
 
 register_builtin_option backward.inferInstanceAs.wrap : Bool := {
   defValue := true
-  descr := "wrap instance bodies in `inferInstanceAs` and the default `deriving` handler"
+  descr := "normalize instance bodies to constructor-based normal form in `inferInstanceAs` and the default `deriving` handler"
 }
 
 register_builtin_option backward.inferInstanceAs.wrap.reuseSubInstances : Bool := {
@@ -76,7 +77,7 @@ register_builtin_option backward.inferInstanceAs.wrap.data : Bool := {
   descr := "wrap data fields in auxiliary definitions to fix their types"
 }
 
-builtin_initialize registerTraceClass `Meta.wrapInstance
+builtin_initialize registerTraceClass `Meta.instanceNormalForm
 
 /--
 Rebuild a type application with fresh synthetic metavariables for instance-implicit arguments.
@@ -94,16 +95,16 @@ def abstractInstImplicitArgs (type : Expr) : MetaM Expr := do
   instantiateMVars (mkAppN fn args)
 
 /--
-Wrap an instance value so its type matches the expected type exactly.
+Normalize an instance value to "instance normal form".
 See the module docstring for the full algorithm specification.
 -/
-partial def wrapInstance (inst expectedType : Expr) (compile : Bool := true)
+partial def normalizeInstance (inst expectedType : Expr) (compile : Bool := true)
     (logCompileErrors : Bool := true) (isMeta : Bool := false) : MetaM Expr := withTransparency .instances do
-  withTraceNode `Meta.wrapInstance
+  withTraceNode `Meta.instanceNormalForm
       (fun _ => return m!"type: {expectedType}") do
   let some className ← isClass? expectedType
     | return inst
-  trace[Meta.wrapInstance] "class is {className}"
+  trace[Meta.instanceNormalForm] "class is {className}"
 
   if ← isProp expectedType then
     if backward.inferInstanceAs.wrap.instances.get (← getOptions) then
@@ -116,7 +117,7 @@ partial def wrapInstance (inst expectedType : Expr) (compile : Bool := true)
   inst.withApp fun f args => do
     let some (.ctorInfo ci) ← f.constName?.mapM getConstInfo
       | do
-        trace[Meta.wrapInstance] "did not reduce to constructor application, returning/wrapping as is: {inst}"
+        trace[Meta.instanceNormalForm] "did not reduce to constructor application, returning/wrapping as is: {inst}"
         if backward.inferInstanceAs.wrap.instances.get (← getOptions) then
           let instType ← inferType inst
           if ← isDefEq expectedType instType then
@@ -134,11 +135,11 @@ partial def wrapInstance (inst expectedType : Expr) (compile : Bool := true)
           return inst
     let (mvars, _, cls) ← forallMetaTelescope (← inferType f)
     if h₁ : args.size ≠ mvars.size then
-      throwError "wrapInstance: incorrect number of arguments for \
+      throwError "instance normal form: incorrect number of arguments for \
         constructor application `{f}`: {args}"
     else
       unless ← isDefEq expectedType cls do
-        throwError "wrapInstance: `{expectedType}` does not unify with the conclusion of \
+        throwError "instance normal form: `{expectedType}` does not unify with the conclusion of \
           `{.ofConstName ci.name}`"
       for h₂ : i in ci.numParams...args.size do
         have : i < mvars.size := by
@@ -154,7 +155,7 @@ partial def wrapInstance (inst expectedType : Expr) (compile : Bool := true)
           if ← isDefEq argExpectedType argType then
             mvarId.assign arg
           else
-            trace[Meta.wrapInstance] "proof field {i} does not have expected type {argExpectedType} but {argType}, wrapping in auxiliary theorem: {arg}"
+            trace[Meta.instanceNormalForm] "proof field {i} does not have expected type {argExpectedType} but {argType}, wrapping in auxiliary theorem: {arg}"
             mvarId.assign (← mkAuxTheorem argExpectedType arg (zetaDelta := true))
         -- Recurse into instance arguments of the constructor
         else if (← isClass? argExpectedType).isSome then
@@ -164,12 +165,12 @@ partial def wrapInstance (inst expectedType : Expr) (compile : Bool := true)
             -- semireducible transparency.
             try
               if let .some new ← trySynthInstance argExpectedType then
-                trace[Meta.wrapInstance] "using existing instance {new}"
+                trace[Meta.instanceNormalForm] "using existing instance {new}"
                 mvarId.assign new
                 continue
             catch _ => pure ()
 
-          mvarId.assign (← wrapInstance arg argExpectedType (compile := compile)
+          mvarId.assign (← normalizeInstance arg argExpectedType (compile := compile)
             (logCompileErrors := logCompileErrors) (isMeta := isMeta))
         else
           -- For data fields, assign directly or wrap in aux def to fix types.

src/Lean/Meta/Sym/SymM.lean

@@ -15,48 +15,6 @@ register_builtin_option sym.debug : Bool := {
   descr    := "check invariants"
 }
 
-/-!
-## Sym Extensions
-
-Extensible state mechanism for `SymM`, allowing modules to register persistent state
-that lives across `simp` invocations within a `sym =>` block. Follows the same pattern
-as `Grind.SolverExtension` in `Lean/Meta/Tactic/Grind/Types.lean`.
--/
-
-/-- Opaque extension state type used to store type-erased extension values. -/
-opaque SymExtensionStateSpec : (α : Type) × Inhabited α := ⟨Unit, ⟨()⟩⟩
-@[expose] def SymExtensionState : Type := SymExtensionStateSpec.fst
-instance : Inhabited SymExtensionState := SymExtensionStateSpec.snd
-
-/--
-A registered extension for `SymM`. Each extension gets a unique index into the
-extensions array in `Sym.State`. Can only be created via `registerSymExtension`.
--/
-structure SymExtension (σ : Type) where private mk ::
-  id        : Nat
-  mkInitial : IO σ
-  deriving Inhabited
-
-private builtin_initialize symExtensionsRef : IO.Ref (Array (SymExtension SymExtensionState)) ← IO.mkRef #[]
-
-/--
-Registers a new `SymM` state extension. Extensions can only be registered during initialization.
-Returns a handle for typed access to the extension's state.
--/
-def registerSymExtension {σ : Type} (mkInitial : IO σ) : IO (SymExtension σ) := do
-  unless (← initializing) do
-    throw (IO.userError "failed to register `Sym` extension, extensions can only be registered during initialization")
-  let exts ← symExtensionsRef.get
-  let id := exts.size
-  let ext : SymExtension σ := { id, mkInitial }
-  symExtensionsRef.modify fun exts => exts.push (unsafe unsafeCast ext)
-  return ext
-
-/-- Returns initial state for all registered extensions. -/
-def SymExtensions.mkInitialStates : IO (Array SymExtensionState) := do
-  let exts ← symExtensionsRef.get
-  exts.mapM fun ext => ext.mkInitial
-
 /--
 Information about a single argument position in a function's type signature.
 
@@ -175,8 +133,6 @@ structure State where
   congrInfo : PHashMap ExprPtr CongrInfo := {}
   /-- Cache for `isDefEqI` results -/
   defEqI : PHashMap (ExprPtr × ExprPtr) Bool := {}
-  /-- State for registered `SymExtension`s, indexed by extension id. -/
-  extensions : Array SymExtensionState := #[]
   debug : Bool := false
 
 abbrev SymM := ReaderT Context <| StateRefT State MetaM
@@ -194,8 +150,7 @@ private def mkSharedExprs : AlphaShareCommonM SharedExprs := do
 def SymM.run (x : SymM α) : MetaM α := do
   let (sharedExprs, share) := mkSharedExprs |>.run {}
   let debug := sym.debug.get (← getOptions)
-  let extensions ← SymExtensions.mkInitialStates
-  x { sharedExprs } |>.run' { debug, share, extensions }
+  x { sharedExprs } |>.run' { debug, share }
 
 /-- Returns maximally shared commonly used terms -/
 def getSharedExprs : SymM SharedExprs :=
@@ -275,26 +230,4 @@ def isDefEqI (s t : Expr) : SymM Bool := do
   modify fun s => { s with defEqI := s.defEqI.insert key result }
   return result
 
-instance : Inhabited (SymM α) where
-  default := throwError "<SymM default value>"
-
-/-! ### SymExtension accessors -/
-
-private unsafe def SymExtension.getStateCoreImpl (ext : SymExtension σ) (extensions : Array SymExtensionState) : IO σ :=
-  return unsafeCast extensions[ext.id]!
-
-@[implemented_by SymExtension.getStateCoreImpl]
-opaque SymExtension.getStateCore (ext : SymExtension σ) (extensions : Array SymExtensionState) : IO σ
-
-def SymExtension.getState (ext : SymExtension σ) : SymM σ := do
-  ext.getStateCore (← get).extensions
-
-private unsafe def SymExtension.modifyStateImpl (ext : SymExtension σ) (f : σ → σ) : SymM Unit := do
-  modify fun s => { s with
-    extensions := s.extensions.modify ext.id fun state => unsafeCast (f (unsafeCast state))
-  }
-
-@[implemented_by SymExtension.modifyStateImpl]
-opaque SymExtension.modifyState (ext : SymExtension σ) (f : σ → σ) : SymM Unit
-
 end Lean.Meta.Sym

src/Lean/Parser/Term.lean

@@ -774,15 +774,10 @@ In particular, it is like a unary operation with a fixed parameter `b`, where on
 @[builtin_term_parser] def noImplicitLambda := leading_parser
   "no_implicit_lambda% " >> termParser maxPrec
 /--
-`inferInstanceAs α` synthesizes an instance of type `α`, transporting it from a
-definitionally equal type if necessary. This is useful when `α` is definitionally equal to
-some `α'` for which instances are registered, as it prevents leaking the definition's RHS
-at lower transparencies.
-
-`inferInstanceAs` requires an expected type from context. If you just need to synthesize an
-instance without transporting between types, use `inferInstance` instead.
-
-See `Lean.Meta.WrapInstance` for details.
+`inferInstanceAs α` synthesizes an instance of type `α` and normalizes it to
+"instance normal form": the result is a constructor application whose sub-instance
+fields are canonical instances and whose types match `α` exactly. See
+`Lean.Meta.InstanceNormalForm` for details.
 -/
 @[builtin_term_parser] def «inferInstanceAs» := leading_parser
   "inferInstanceAs" >> (((" $ " <|> " <| ") >> termParser minPrec) <|> (ppSpace >> termParser argPrec))

src/Lean/Runtime.lean

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

src/Std/Do/Triple/SpecLemmas.lean

@@ -136,15 +136,6 @@ theorem Cursor.pos_at {l : List α} {n : Nat} (h : n < l.length) :
 theorem Cursor.pos_mk {l pre suff : List α} (h : pre ++ suff = l) :
     (Cursor.mk pre suff h).pos = pre.length := rfl
 
-theorem Cursor.pos_le_length {c : Cursor l} : c.pos ≤ l.length := by
-  simp [← congrArg List.length c.property]
-
-theorem Cursor.length_prefix_le_length {c : Cursor l} : c.prefix.length ≤ l.length :=
-  pos_le_length
-
-theorem Cursor.length_suffix_le_length {c : Cursor l} : c.suffix.length ≤ l.length := by
-  simp [← congrArg List.length c.property]
-
 @[grind →]
 theorem eq_of_range'_eq_append_cons (h : range' s n step = xs ++ cur :: ys) :
     cur = s + step * xs.length := by

src/include/lean/lean.h

@@ -319,7 +319,6 @@ LEAN_EXPORT void lean_set_panic_messages(bool flag);
 
 LEAN_EXPORT void lean_panic(char const * msg, bool force_stderr);
 LEAN_EXPORT lean_object * lean_panic_fn(lean_object * default_val, lean_object * msg);
-LEAN_EXPORT lean_object * lean_panic_fn_borrowed(b_lean_obj_arg default_val, lean_object * msg);
 
 LEAN_EXPORT LEAN_NORETURN void lean_internal_panic(char const * msg);
 LEAN_EXPORT LEAN_NORETURN void lean_internal_panic_out_of_memory(void);
@@ -848,10 +847,11 @@ static inline lean_obj_res lean_array_fget_borrowed(b_lean_obj_arg a, b_lean_obj
 
 LEAN_EXPORT lean_obj_res lean_array_get_panic(lean_obj_arg def_val);
 
-static inline lean_object * lean_array_get(b_lean_obj_arg def_val, b_lean_obj_arg a, b_lean_obj_arg i) {
+static inline lean_object * lean_array_get(lean_obj_arg def_val, b_lean_obj_arg a, b_lean_obj_arg i) {
     if (lean_is_scalar(i)) {
         size_t idx = lean_unbox(i);
         if (idx < lean_array_size(a)) {
+            lean_dec(def_val);
             return lean_array_uget(a, idx);
         }
     }
@@ -859,14 +859,14 @@ static inline lean_object * lean_array_get(b_lean_obj_arg def_val, b_lean_obj_ar
        i > LEAN_MAX_SMALL_NAT == MAX_UNSIGNED >> 1
        but each array entry is 8 bytes in 64-bit machines and 4 in 32-bit ones.
        In both cases, we would be out-of-memory. */
-    lean_inc(def_val);
     return lean_array_get_panic(def_val);
 }
 
-static inline lean_object * lean_array_get_borrowed(b_lean_obj_arg def_val, b_lean_obj_arg a, b_lean_obj_arg i) {
+static inline lean_object * lean_array_get_borrowed(lean_obj_arg def_val, b_lean_obj_arg a, b_lean_obj_arg i) {
     if (lean_is_scalar(i)) {
         size_t idx = lean_unbox(i);
         if (idx < lean_array_size(a)) {
+            lean_dec(def_val);
             return lean_array_get_core(a, idx);
         }
     }
@@ -874,7 +874,6 @@ static inline lean_object * lean_array_get_borrowed(b_lean_obj_arg def_val, b_le
        i > LEAN_MAX_SMALL_NAT == MAX_UNSIGNED >> 1
        but each array entry is 8 bytes in 64-bit machines and 4 in 32-bit ones.
        In both cases, we would be out-of-memory. */
-    lean_inc(def_val);
     return lean_array_get_panic(def_val);
 }
 

src/lake/Lake/Build/Common.lean

@@ -463,12 +463,10 @@ public def Cache.saveArtifact
       IO.setAccessRights file ⟨r, r, r⟩
       unless (← cacheFile.pathExists) do
         createParentDirs cacheFile
-        -- other functions can race to create the file
-        -- use `writeFileIfNew` to prevent errors on races
-        writeFileIfNew cacheFile normalized
-      IO.setAccessRights cacheFile ⟨r, r, r⟩
+        IO.FS.writeFile cacheFile normalized
+        IO.setAccessRights cacheFile ⟨r, r, r⟩
       writeFileHash file hash
-      let mtime ← getMTime cacheFile
+      let mtime := (← getMTime cacheFile |>.toBaseIO).toOption.getD 0
       let path := if useLocalFile then file else cacheFile
       return {descr, name := file.toString, path, mtime}
     else
@@ -482,14 +480,11 @@ public def Cache.saveArtifact
       IO.setAccessRights file ⟨r, r, r⟩
       unless (← cacheFile.pathExists) do
         createParentDirs cacheFile
-        if let .error e ← (IO.FS.hardLink file cacheFile).toBaseIO then
-          -- other functions can race to create the file
-          unless e matches .alreadyExists .. do
-            -- use `writeBinFileIfNew` to prevent errors on races
-            writeBinFileIfNew cacheFile contents
-      IO.setAccessRights cacheFile ⟨r, r, r⟩
+        if let .error _ ← (IO.FS.hardLink file cacheFile).toBaseIO then
+          IO.FS.writeBinFile cacheFile contents
+          IO.setAccessRights cacheFile ⟨r, r, r⟩
       writeFileHash file hash
-      let mtime ← getMTime cacheFile
+      let mtime := (← getMTime cacheFile |>.toBaseIO).toOption.getD 0
       let path := if useLocalFile then file else cacheFile
       return {descr, name := file.toString, path, mtime}
   catch e =>

src/lake/Lake/Util/IO.lean

@@ -24,26 +24,6 @@ public def removeFileIfExists (path : FilePath) : IO Unit := do
     | .noFileOrDirectory .. => pure ()
     | e => throw e
 
-/--
-Write the UTF-8 encoded string {lean}`content` to {lean}`path`.
-If the file already exists, does nothing.
--/
-public def writeFileIfNew (path : FilePath) (content : String) : IO Unit := do
-  let h ← try IO.FS.Handle.mk path IO.FS.Mode.writeNew catch
-    | .alreadyExists .. => return
-    | e => throw e
-  h.putStr content
-
-/--
-Write the bytes of {lean}`content` to {lean}`path`.
-If the file already exists, does nothing.
--/
-public def writeBinFileIfNew (path : FilePath) (content : ByteArray) : IO Unit := do
-  let h ← try IO.FS.Handle.mk path IO.FS.Mode.writeNew catch
-    | .alreadyExists .. => return
-    | e => throw e
-  h.write content
-
 /--
 Remove a directory and all its contents.
 Like {lean}`IO.FS.removeDirAll`, but does not fail if {lean}`path` does not exist

src/runtime/CMakeLists.txt

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

src/runtime/object.cpp

@@ -196,11 +196,6 @@ extern "C" LEAN_EXPORT object * lean_panic_fn(object * default_val, object * msg
     return default_val;
 }
 
-extern "C" LEAN_EXPORT object * lean_panic_fn_borrowed(b_obj_arg default_val, object * msg) {
-    lean_inc(default_val);
-    return lean_panic_fn(default_val, msg);
-}
-
 extern "C" LEAN_EXPORT object * lean_sorry(uint8) {
     lean_internal_panic("executed 'sorry'");
     lean_unreachable();

src/runtime/object.h

@@ -194,7 +194,7 @@ inline object * mk_empty_array() { return lean_mk_empty_array(); }
 inline object * mk_empty_array(b_obj_arg capacity) { return lean_mk_empty_array_with_capacity(capacity); }
 inline object * array_uget(b_obj_arg a, usize i) { return lean_array_uget(a, i); }
 inline obj_res array_fget(b_obj_arg a, b_obj_arg i) { return lean_array_fget(a, i); }
-inline object * array_get(b_obj_arg def_val, b_obj_arg a, b_obj_arg i) { return lean_array_get(def_val, a, i); }
+inline object * array_get(obj_arg def_val, b_obj_arg a, b_obj_arg i) { return lean_array_get(def_val, a, i); }
 inline obj_res copy_array(obj_arg a, bool expand = false) { return lean_copy_expand_array(a, expand); }
 inline object * array_uset(obj_arg a, usize i, obj_arg v) { return lean_array_uset(a, i, v); }
 inline object * array_fset(obj_arg a, b_obj_arg i, obj_arg v) { return lean_array_fset(a, i, v); }

src/runtime/openssl.cpp

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

src/runtime/openssl.h

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