fix: issue with session

.claude/CLAUDE.md

@@ -7,11 +7,6 @@ To build Lean you should use `make -j$(nproc) -C build/release`.
 The build uses `ccache`, and in a sandbox `ccache` may complain about read-only file systems.
 Use `CCACHE_READONLY` and `CCACHE_TEMPDIR` instead of disabling ccache completely.
 
-To rebuild individual modules without a full build, use Lake directly:
-```
-cd src && lake build Init.Prelude
-```
-
 ## Running Tests
 
 See `tests/README.md` for full documentation. Quick reference:
@@ -61,11 +56,6 @@ make -C build/release/stage2 clean-stdlib
 ```
 must be run manually before building.
 
-To rebuild individual stage 2 modules without a full `make stage2`, use Lake directly:
-```
-cd build/release/stage2 && lake build Init.Prelude
-```
-
 ## New features
 
 When asked to implement new features:

.claude/commands/release.md

@@ -157,16 +157,6 @@ Note: `gh pr checks --watch` exits as soon as ALL checks complete (pass or fail)
 fail while others are still running, `--watch` will continue until everything settles, then exit
 with a non-zero code. So a background `--watch` finishing = all checks done; check which failed.
 
-## Mathlib Bump Branches
-
-Mathlib `bump/v4.X.0` branches live on the **fork** `leanprover-community/mathlib4-nightly-testing`,
-NOT on `leanprover-community/mathlib4`.
-
-## Never Force-Update Remote Refs Without Confirmation
-
-Never force-update an existing remote branch or tag via `git push --force` or the GitHub API
-without explicit user confirmation.
-
 ## Error Handling
 
 **CRITICAL**: If something goes wrong or a command fails:

.github/workflows/build-template.yml

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

.github/workflows/ci.yml

@@ -143,7 +143,7 @@ jobs:
           CMAKE_MAJOR=$(grep -E "^set\(LEAN_VERSION_MAJOR " src/CMakeLists.txt | grep -oE '[0-9]+')
           CMAKE_MINOR=$(grep -E "^set\(LEAN_VERSION_MINOR " src/CMakeLists.txt | grep -oE '[0-9]+')
           CMAKE_PATCH=$(grep -E "^set\(LEAN_VERSION_PATCH " src/CMakeLists.txt | grep -oE '[0-9]+')
-          CMAKE_IS_RELEASE=$(grep -m 1 -E "^set\(LEAN_VERSION_IS_RELEASE " src/CMakeLists.txt | grep -oE '[0-9]+' | head -1)
+          CMAKE_IS_RELEASE=$(grep -m 1 -E "^set\(LEAN_VERSION_IS_RELEASE " src/CMakeLists.txt | sed -nE 's/^set\(LEAN_VERSION_IS_RELEASE ([0-9]+)\).*/\1/p')
 
           # Expected values from tag parsing
           TAG_MAJOR="${{ steps.set-release.outputs.LEAN_VERSION_MAJOR }}"

.gitpod.yml

@@ -6,6 +6,6 @@ vscode:
     - leanprover.lean4
 
 tasks:
-  - name: Build
-    init: cmake --preset dev
+  - name: Release build
+    init: cmake --preset release
     command: make -C build/release -j$(nproc || sysctl -n hw.logicalcpu)

CMakeLists.txt

@@ -1,6 +1,4 @@
 cmake_minimum_required(VERSION 3.21)
-include(ExternalProject)
-include(FetchContent)
 
 if(NOT CMAKE_GENERATOR MATCHES "Makefiles")
   message(FATAL_ERROR "Only makefile generators are supported")
@@ -36,6 +34,7 @@ foreach(var ${vars})
   endif()
 endforeach()
 
+include(ExternalProject)
 project(LEAN CXX C)
 
 if(NOT (DEFINED STAGE0_CMAKE_EXECUTABLE_SUFFIX))
@@ -120,16 +119,17 @@ if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
 endif()
 
 if(USE_MIMALLOC)
-  FetchContent_Declare(
+  ExternalProject_Add(
     mimalloc
+    PREFIX mimalloc
     GIT_REPOSITORY https://github.com/microsoft/mimalloc
     GIT_TAG v2.2.3
-    # Unnecessarily deep directory structure, but it saves us from a complicated
-    # stage0 update for now. If we ever update the other dependencies like
-    # cadical, it might be worth reorganizing the directory structure.
-    SOURCE_DIR "${CMAKE_BINARY_DIR}/mimalloc/src/mimalloc"
+    # just download, we compile it as part of each stage as it is small
+    CONFIGURE_COMMAND ""
+    BUILD_COMMAND ""
+    INSTALL_COMMAND ""
   )
-  FetchContent_MakeAvailable(mimalloc)
+  list(APPEND EXTRA_DEPENDS mimalloc)
 endif()
 
 if(NOT STAGE1_PREV_STAGE)

CMakePresets.json

@@ -8,26 +8,16 @@
   "configurePresets": [
     {
       "name": "release",
-      "displayName": "Release build config",
+      "displayName": "Default development optimized build config",
       "generator": "Unix Makefiles",
       "binaryDir": "${sourceDir}/build/release"
     },
-    {
-      "name": "dev",
-      "displayName": "Default development optimized build config",
-      "cacheVariables": {
-        "STRIP_BINARIES": "OFF"
-      },
-      "generator": "Unix Makefiles",
-      "binaryDir": "${sourceDir}/build/dev"
-    },
     {
       "name": "debug",
       "displayName": "Debug build config",
       "cacheVariables": {
-        "CMAKE_BUILD_TYPE": "Debug",
         "LEAN_EXTRA_CXX_FLAGS": "-DLEAN_DEFAULT_THREAD_STACK_SIZE=16*1024*1024",
-        "STRIP_BINARIES": "OFF"
+        "CMAKE_BUILD_TYPE": "Debug"
       },
       "generator": "Unix Makefiles",
       "binaryDir": "${sourceDir}/build/debug"
@@ -36,8 +26,7 @@
       "name": "reldebug",
       "displayName": "Release with assertions enabled",
       "cacheVariables": {
-        "CMAKE_BUILD_TYPE": "RelWithAssert",
-        "STRIP_BINARIES": "OFF"
+        "CMAKE_BUILD_TYPE": "RelWithAssert"
       },
       "generator": "Unix Makefiles",
       "binaryDir": "${sourceDir}/build/reldebug"
@@ -49,7 +38,6 @@
         "LEAN_EXTRA_CXX_FLAGS": "-fsanitize=address,undefined -DLEAN_DEFAULT_THREAD_STACK_SIZE=16*1024*1024",
         "LEANC_EXTRA_CC_FLAGS": "-fsanitize=address,undefined",
         "LEAN_EXTRA_LINKER_FLAGS": "-fsanitize=address,undefined -fsanitize-link-c++-runtime",
-        "STRIP_BINARIES": "OFF",
         "SMALL_ALLOCATOR": "OFF",
         "USE_MIMALLOC": "OFF",
         "BSYMBOLIC": "OFF",
@@ -70,10 +58,6 @@
       "name": "release",
       "configurePreset": "release"
     },
-    {
-      "name": "dev",
-      "configurePreset": "dev"
-    },
     {
       "name": "debug",
       "configurePreset": "debug"
@@ -97,11 +81,6 @@
       "configurePreset": "release",
       "output": {"outputOnFailure": true, "shortProgress": true}
     },
-    {
-      "name": "dev",
-      "configurePreset": "dev",
-      "output": {"outputOnFailure": true, "shortProgress": true}
-    },
     {
       "name": "debug",
       "configurePreset": "debug",

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
 -----------------------
@@ -30,9 +31,6 @@ cd lean4
 cmake --preset release
 make -C build/release -j$(nproc || sysctl -n hw.logicalcpu)
 ```
-
-For development, `cmake --preset dev` is recommended instead.
-
 You can replace `$(nproc || sysctl -n hw.logicalcpu)` with the desired parallelism amount.
 
 The above commands will compile the Lean library and binaries into the

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

script/release_checklist.py

@@ -311,16 +311,16 @@ def check_cmake_version(repo_url, branch, version_major, version_minor, github_t
         print(f"  ❌ Could not retrieve {cmake_file_path} from {branch}")
         return False
 
-    expected_patterns = [
-        (f"LEAN_VERSION_MAJOR", rf"^set\(LEAN_VERSION_MAJOR\s+{version_major}[\s)]", f"set(LEAN_VERSION_MAJOR {version_major} ...)"),
-        (f"LEAN_VERSION_MINOR", rf"^set\(LEAN_VERSION_MINOR\s+{version_minor}[\s)]", f"set(LEAN_VERSION_MINOR {version_minor} ...)"),
-        (f"LEAN_VERSION_PATCH", rf"^set\(LEAN_VERSION_PATCH\s+0[\s)]", f"set(LEAN_VERSION_PATCH 0 ...)"),
-        (f"LEAN_VERSION_IS_RELEASE", rf"^set\(LEAN_VERSION_IS_RELEASE\s+1[\s)]", f"set(LEAN_VERSION_IS_RELEASE 1 ...)"),
+    expected_lines = [
+        f"set(LEAN_VERSION_MAJOR {version_major})",
+        f"set(LEAN_VERSION_MINOR {version_minor})",
+        f"set(LEAN_VERSION_PATCH 0)",
+        f"set(LEAN_VERSION_IS_RELEASE 1)"
     ]
 
-    for name, pattern, display in expected_patterns:
-        if not any(re.match(pattern, l.strip()) for l in content.splitlines()):
-            print(f"  ❌ Missing or incorrect line in {cmake_file_path}: {display}")
+    for line in expected_lines:
+        if not any(l.strip().startswith(line) for l in content.splitlines()):
+            print(f"  ❌ Missing or incorrect line in {cmake_file_path}: {line}")
             return False
 
     print(f"  ✅ CMake version settings are correct in {cmake_file_path}")
@@ -343,11 +343,11 @@ def check_stage0_version(repo_url, branch, version_major, version_minor, github_
     for line in content.splitlines():
         stripped = line.strip()
         if stripped.startswith("set(LEAN_VERSION_MAJOR "):
-            actual = stripped.split()[1].rstrip(")")
+            actual = stripped.split()[-1].rstrip(")")
             if actual != str(version_major):
                 errors.append(f"LEAN_VERSION_MAJOR: expected {version_major}, found {actual}")
         elif stripped.startswith("set(LEAN_VERSION_MINOR "):
-            actual = stripped.split()[1].rstrip(")")
+            actual = stripped.split()[-1].rstrip(")")
             if actual != str(version_minor):
                 errors.append(f"LEAN_VERSION_MINOR: expected {version_minor}, found {actual}")
 

src/CMakeLists.txt

@@ -8,7 +8,7 @@ endif()
 include(ExternalProject)
 project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4 CACHE STRING "")
-set(LEAN_VERSION_MINOR 31 CACHE STRING "")
+set(LEAN_VERSION_MINOR 30 CACHE STRING "")
 set(LEAN_VERSION_PATCH 0 CACHE STRING "")
 set(LEAN_VERSION_IS_RELEASE 0 CACHE STRING "") # This number is 1 in the release revision, and 0 otherwise.
 set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")
@@ -80,7 +80,6 @@ option(CCACHE "use ccache" ON)
 option(SPLIT_STACK "SPLIT_STACK" OFF)
 # When OFF we disable LLVM support
 option(LLVM "LLVM" OFF)
-option(STRIP_BINARIES "Strip produced binaries" ON)
 
 # When ON we include githash in the version string
 option(USE_GITHASH "GIT_HASH" ON)
@@ -357,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)
@@ -615,38 +656,6 @@ else()
       OUTPUT_VARIABLE GIT_SHA1
       OUTPUT_STRIP_TRAILING_WHITESPACE
     )
-    # Fallback for jj workspaces where git cannot find .git directly.
-    # Use `jj git root` to find the backing git repo, then `jj log` to
-    # resolve the current workspace's commit (git HEAD points to the root
-    # workspace, not the current one).
-    if("${GIT_SHA1}" STREQUAL "")
-      find_program(JJ_EXECUTABLE jj)
-      if(JJ_EXECUTABLE)
-        execute_process(
-          COMMAND "${JJ_EXECUTABLE}" git root
-          WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
-          OUTPUT_VARIABLE _jj_git_dir
-          OUTPUT_STRIP_TRAILING_WHITESPACE
-          ERROR_QUIET
-          RESULT_VARIABLE _jj_git_root_result
-        )
-        execute_process(
-          COMMAND "${JJ_EXECUTABLE}" log -r @ --no-graph -T "commit_id"
-          WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
-          OUTPUT_VARIABLE _jj_commit
-          OUTPUT_STRIP_TRAILING_WHITESPACE
-          ERROR_QUIET
-          RESULT_VARIABLE _jj_rev_result
-        )
-        if(_jj_git_root_result EQUAL 0 AND _jj_rev_result EQUAL 0)
-          execute_process(
-            COMMAND git --git-dir "${_jj_git_dir}" ls-tree "${_jj_commit}" stage0 --object-only
-            OUTPUT_VARIABLE GIT_SHA1
-            OUTPUT_STRIP_TRAILING_WHITESPACE
-          )
-        endif()
-      endif()
-    endif()
     message(STATUS "stage0 sha1: ${GIT_SHA1}")
     # Now that we've prepared the information for the next stage, we can forget that we will use
     # Lake in the future as we won't use it in this stage
@@ -763,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)
@@ -830,14 +839,7 @@ if(LLVM AND STAGE GREATER 0)
   set(EXTRA_LEANMAKE_OPTS "LLVM=1")
 endif()
 
-set(
-  STDLIBS
-  Init
-  Std
-  Lean
-  Leanc
-  LeanIR
-)
+set(STDLIBS Init Std Lean Leanc LeanIR)
 if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
   list(APPEND STDLIBS Lake LeanChecker)
 endif()
@@ -945,7 +947,10 @@ if(PREV_STAGE)
 endif()
 
 if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
-  add_custom_target(leanir ALL DEPENDS leanshared COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make leanir VERBATIM)
+  add_custom_target(leanir ALL
+    DEPENDS leanshared
+    COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make leanir
+    VERBATIM)
 endif()
 
 # use Bash version for building, use Lean version in bin/ for tests & distribution

src/Init/Data/ByteArray/Basic.lean

@@ -20,20 +20,12 @@ universe u
 
 namespace ByteArray
 
-@[extern "lean_sarray_dec_eq"]
-def beq (lhs rhs : @& ByteArray) : Bool :=
-  lhs.data == rhs.data
-
-instance : BEq ByteArray where
-  beq := beq
+deriving instance BEq for ByteArray
 
 attribute [ext] ByteArray
 
-@[extern "lean_sarray_dec_eq"]
-def decEq (lhs rhs : @& ByteArray) : Decidable (lhs = rhs) :=
-  decidable_of_decidable_of_iff ByteArray.ext_iff.symm
-
-instance : DecidableEq ByteArray := decEq
+instance : DecidableEq ByteArray :=
+  fun _ _ => decidable_of_decidable_of_iff ByteArray.ext_iff.symm
 
 instance : Inhabited ByteArray where
   default := empty

src/Init/Data/Ord/String.lean

@@ -9,7 +9,7 @@ prelude
 public import Init.Data.Order.Ord
 public import Init.Data.String.Basic
 import Init.Data.Char.Lemmas
-import Init.Data.String.Lemmas.StringOrder
+import Init.Data.String.Lemmas
 
 public section
 

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

@@ -17,7 +17,6 @@ namespace Std
 /--
 Appends all the elements in the iterator, in order.
 -/
-@[inline]
 public def Iter.joinString {α β : Type} [Iterator α Id β] [ToString β]
     (it : Std.Iter (α := α) β) : String :=
   (it.map toString).fold (init := "") (· ++ ·)

src/Init/Data/String/Lemmas.lean

@@ -20,4 +20,49 @@ 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
-public import Init.Data.String.Lemmas.StringOrder
+import Init.Data.Order.Lemmas
+public import Init.Data.String.Basic
+import Init.Data.Char.Lemmas
+import Init.Data.Char.Order
+import Init.Data.List.Lex
+
+public section
+
+open Std
+
+namespace String
+
+@[deprecated toList_inj (since := "2025-10-30")]
+protected theorem data_eq_of_eq {a b : String} (h : a = b) : a.toList = b.toList :=
+  h ▸ rfl
+@[deprecated toList_inj (since := "2025-10-30")]
+protected theorem ne_of_data_ne {a b : String} (h : a.toList ≠ b.toList) : a ≠ b := by
+  simpa [← toList_inj]
+
+@[simp] protected theorem not_le {a b : String} : ¬ a ≤ b ↔ b < a := Decidable.not_not
+@[simp] protected theorem not_lt {a b : String} : ¬ a < b ↔ b ≤ a := Iff.rfl
+@[simp] protected theorem le_refl (a : String) : a ≤ a := List.le_refl _
+@[simp] protected theorem lt_irrefl (a : String) : ¬ a < a := List.lt_irrefl _
+
+attribute [local instance] Char.notLTTrans Char.ltTrichotomous Char.ltAsymm
+
+protected theorem le_trans {a b c : String} : a ≤ b → b ≤ c → a ≤ c := List.le_trans
+protected theorem lt_trans {a b c : String} : a < b → b < c → a < c := List.lt_trans
+protected theorem le_total (a b : String) : a ≤ b ∨ b ≤ a := List.le_total _ _
+protected theorem le_antisymm {a b : String} : a ≤ b → b ≤ a → a = b := fun h₁ h₂ => String.ext (List.le_antisymm (as := a.toList) (bs := b.toList) h₁ h₂)
+protected theorem lt_asymm {a b : String} (h : a < b) : ¬ b < a := List.lt_asymm h
+protected theorem ne_of_lt {a b : String} (h : a < b) : a ≠ b := by
+  have := String.lt_irrefl a
+  intro h; subst h; contradiction
+
+instance instIsLinearOrder : IsLinearOrder String := by
+  apply IsLinearOrder.of_le
+  case le_antisymm => constructor; apply String.le_antisymm
+  case le_trans => constructor; apply String.le_trans
+  case le_total => constructor; apply String.le_total
+
+instance : LawfulOrderLT String where
+  lt_iff a b := by
+    simp [← String.not_le, Decidable.imp_iff_not_or, Std.Total.total]
+
+end String

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

@@ -40,7 +40,7 @@ framework.
 /--
 This data-carrying typeclass is used to give semantics to a pattern type that implements
 {name}`ForwardPattern` and/or {name}`ToForwardSearcher` by providing an abstract, not necessarily
-decidable {name}`PatternModel.Matches` predicate that implementations of {name}`ForwardPattern`
+decidable {name}`PatternModel.Matches` predicate that implementates of {name}`ForwardPattern`
 and {name}`ToForwardSearcher` can be validated against.
 
 Correctness results for generic functions relying on the pattern infrastructure, for example the
@@ -151,7 +151,7 @@ theorem IsLongestMatch.le_of_isMatch {pat : ρ} [PatternModel pat] {s : Slice} {
 
 /--
 Predicate stating that the region between the start of the slice {name}`s` and the position
-{name}`pos` matches the pattern {name}`pat`, and that there is no longer match starting at the
+{name}`pos` matches the patten {name}`pat`, and that there is no longer match starting at the
 beginning of the slice. This is what a correct matcher should match.
 
 In some cases, being a match and being a longest match will coincide, see
@@ -228,7 +228,7 @@ theorem isLongestRevMatch_iff_isRevMatch {ρ : Type} (pat : ρ) [PatternModel pa
   exact ht₅ (NoSuffixPatternModel.eq_empty _ _ ht₂ (ht₅'' ▸ ht₂'))
 
 /--
-Predicate stating that the slice formed by {name}`startPos` and {name}`endPos` contains a match
+Predicate stating that the slice formed by {name}`startPos` and {name}`endPos` contains is a match
 of {name}`pat` in {name}`s` and it is longest among matches starting at {name}`startPos`.
 -/
 structure IsLongestMatchAt (pat : ρ) [PatternModel pat] {s : Slice} (startPos endPos : s.Pos) : Prop where
@@ -411,7 +411,7 @@ theorem not_revMatchesAt_startPos {pat : ρ} [PatternModel pat] {s : Slice} :
   intro h
   simpa [← Pos.ofSliceTo_inj] using h.ne_endPos
 
-theorem revMatchesAt_iff_revMatchesAt_ofSliceTo {pat : ρ} [PatternModel pat] {s : Slice} {base : s.Pos}
+theorem revMatchesAt_iff_revMatchesAt_ofSliceto {pat : ρ} [PatternModel pat] {s : Slice} {base : s.Pos}
     {pos : (s.sliceTo base).Pos} : RevMatchesAt pat pos ↔ RevMatchesAt pat (Pos.ofSliceTo pos) := by
   simp only [revMatchesAt_iff_exists_isLongestRevMatchAt]
   constructor
@@ -505,8 +505,8 @@ theorem LawfulForwardPatternModel.skipPrefix?_eq_none_iff {ρ : Type} {pat : ρ}
 /--
 Predicate stating compatibility between {name}`PatternModel` and {name}`BackwardPattern`.
 
-This extends {name}`LawfulBackwardPattern`, but it is much stronger because it forces the
-{name}`BackwardPattern` to match the longest prefix of the given slice that matches the property
+This extends {name}`LawfulForwardPattern`, but it is much stronger because it forces the
+{name}`ForwardPattern` to match the longest prefix of the given slice that matches the property
 supplied by the {name}`PatternModel` instance.
 -/
 class LawfulBackwardPatternModel {ρ : Type} (pat : ρ) [BackwardPattern pat]

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

@@ -65,7 +65,7 @@ theorem startsWith_prop_eq_head? {P : Char → Prop} [DecidablePred P] {s : Slic
     s.startsWith P = s.copy.toList.head?.any (decide <| P ·) := by
   simp [startsWith_prop_eq_startsWith_decide, startsWith_bool_eq_head?]
 
-theorem eq_append_of_dropPrefix?_prop_eq_some {P : Char → Prop} [DecidablePred P] {s res : Slice} (h : s.dropPrefix? P = some res) :
+theorem eq_append_of_dropPrefix_prop_eq_some {P : Char → Prop} [DecidablePred P] {s res : Slice} (h : s.dropPrefix? P = some res) :
     ∃ c, s.copy = singleton c ++ res.copy ∧ P c := by
   rw [dropPrefix?_prop_eq_dropPrefix?_decide] at h
   simpa using eq_append_of_dropPrefix?_bool_eq_some h
@@ -162,7 +162,7 @@ theorem startsWith_prop_eq_head? {P : Char → Prop} [DecidablePred P] {s : Stri
 theorem eq_append_of_dropPrefix?_prop_eq_some {P : Char → Prop} [DecidablePred P] {s : String} {res : Slice}
     (h : s.dropPrefix? P = some res) : ∃ c, s = singleton c ++ res.copy ∧ P c := by
   rw [dropPrefix?_eq_dropPrefix?_toSlice] at h
-  simpa using Slice.eq_append_of_dropPrefix?_prop_eq_some h
+  simpa using Slice.eq_append_of_dropPrefix_prop_eq_some h
 
 theorem skipSuffix?_bool_eq_some_iff {p : Char → Bool} {s : String} {pos : s.Pos} :
     s.skipSuffix? p = some pos ↔ ∃ h, pos = s.endPos.prev h ∧ p ((s.endPos.prev h).get (by simp)) = true := by

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

@@ -1,49 +0,0 @@
-/-
-Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-
-prelude
-public import Init.Data.String.Basic
-public import Init.Data.Order.Classes
-import Init.Data.List.Lex
-import Init.Data.Char.Lemmas
-import Init.Data.Char.Order
-import Init.Data.Order.Factories
-import Init.Data.Order.Lemmas
-
-public section
-
-open Std
-
-namespace String
-
-@[simp] protected theorem not_le {a b : String} : ¬ a ≤ b ↔ b < a := Decidable.not_not
-@[simp] protected theorem not_lt {a b : String} : ¬ a < b ↔ b ≤ a := Iff.rfl
-@[simp] protected theorem le_refl (a : String) : a ≤ a := List.le_refl _
-@[simp] protected theorem lt_irrefl (a : String) : ¬ a < a := List.lt_irrefl _
-
-attribute [local instance] Char.notLTTrans Char.ltTrichotomous Char.ltAsymm
-
-protected theorem le_trans {a b c : String} : a ≤ b → b ≤ c → a ≤ c := List.le_trans
-protected theorem lt_trans {a b c : String} : a < b → b < c → a < c := List.lt_trans
-protected theorem le_total (a b : String) : a ≤ b ∨ b ≤ a := List.le_total _ _
-protected theorem le_antisymm {a b : String} : a ≤ b → b ≤ a → a = b := fun h₁ h₂ => String.ext (List.le_antisymm (as := a.toList) (bs := b.toList) h₁ h₂)
-protected theorem lt_asymm {a b : String} (h : a < b) : ¬ b < a := List.lt_asymm h
-protected theorem ne_of_lt {a b : String} (h : a < b) : a ≠ b := by
-  have := String.lt_irrefl a
-  intro h; subst h; contradiction
-
-instance instIsLinearOrder : IsLinearOrder String := by
-  apply IsLinearOrder.of_le
-  case le_antisymm => constructor; apply String.le_antisymm
-  case le_trans => constructor; apply String.le_trans
-  case le_total => constructor; apply String.le_total
-
-instance : LawfulOrderLT String where
-  lt_iff a b := by
-    simp [← String.not_le, Decidable.imp_iff_not_or, Std.Total.total]
-
-end String

src/Init/Data/String/Slice.lean

@@ -706,14 +706,14 @@ Returns {name}`none` otherwise.
 This function is generic over all currently supported patterns.
 -/
 @[inline]
-def Pos.revSkip? {s : Slice} (pos : s.Pos) (pat : ρ) [BackwardPattern pat] : Option s.Pos :=
-  ((s.sliceFrom pos).skipSuffix? pat).map Pos.ofSliceFrom
+def Pos.revSkip? {s : Slice} (pos : s.Pos) (pat : ρ) [ForwardPattern pat] : Option s.Pos :=
+  ((s.sliceFrom pos).skipPrefix? pat).map Pos.ofSliceFrom
 
 /--
 If {name}`pat` matches a suffix of {name}`s`, returns the remainder. Returns {name}`none` otherwise.
 
 Use {name (scope := "Init.Data.String.Slice")}`String.Slice.dropSuffix` to return the slice
-unchanged when {name}`pat` does not match a suffix.
+unchanged when {name}`pat` does not match a prefix.
 
 This function is generic over all currently supported patterns.
 
@@ -775,7 +775,7 @@ def Pos.revSkipWhile {s : Slice} (pos : s.Pos) (pat : ρ) [BackwardPattern pat]
 termination_by pos.down
 
 /--
-Returns the position at the start of the longest suffix of {name}`s` for which {name}`pat` matches
+Returns the position a the start of the longest suffix of {name}`s` for which {name}`pat` matches
 (potentially repeatedly).
 -/
 @[inline]

src/Init/Data/String/TakeDrop.lean

@@ -314,7 +314,7 @@ Returns {name}`none` otherwise.
 This function is generic over all currently supported patterns.
 -/
 @[inline]
-def Pos.revSkip? {s : String} (pos : s.Pos) (pat : ρ) [BackwardPattern pat] : Option s.Pos :=
+def Pos.revSkip? {s : String} (pos : s.Pos) (pat : ρ) [ForwardPattern pat] : Option s.Pos :=
   (pos.toSlice.revSkip? pat).map Pos.ofToSlice
 
 /--
@@ -461,7 +461,7 @@ def dropPrefix? (s : String) (pat : ρ) [ForwardPattern pat] : Option String.Sli
 If {name}`pat` matches a suffix of {name}`s`, returns the remainder. Returns {name}`none` otherwise.
 
 Use {name (scope := "Init.Data.String.TakeDrop")}`String.dropSuffix` to return the slice
-unchanged when {name}`pat` does not match a suffix.
+unchanged when {name}`pat` does not match a prefix.
 
 This is a cheap operation because it does not allocate a new string to hold the result.
 To convert the result into a string, use {name}`String.Slice.copy`.

src/Init/Grind/Util.lean

@@ -30,13 +30,13 @@ simpMatchDiscrsOnly (match 0 with | 0 => true | _ => false) = true
 ```
 using `eq_self`.
 -/
-@[expose] def simpMatchDiscrsOnly {α : Sort u} (a : α) : α := a
+def simpMatchDiscrsOnly {α : Sort u} (a : α) : α := a
 
 /--
 Gadget for protecting lambda abstractions created by `abstractGroundMismatches?`
 from beta reduction during preprocessing. See `ProveEq.lean` for details.
 -/
-@[expose] def abstractFn {α : Sort u} (a : α) : α := a
+def abstractFn {α : Sort u} (a : α) : α := a
 
 /-- Gadget for representing offsets `t+k` in patterns. -/
 def offset (a b : Nat) : Nat := a + b

src/Init/Notation.lean

@@ -624,23 +624,6 @@ existing code. It may be removed in a future version of the library.
 syntax (name := deprecated) "deprecated" (ppSpace ident)? (ppSpace str)?
     (" (" &"since" " := " str ")")? : attr
 
-/--
-The attribute `@[deprecated_arg old new]` marks a named parameter as deprecated.
-
-When a caller uses the old name with a replacement available, a deprecation warning is emitted
-and the argument is silently forwarded to the new parameter. When no replacement is provided,
-the parameter is treated as removed and using it produces an error.
-
-* `@[deprecated_arg old new (since := "2026-03-18")]` marks `old` as a deprecated alias for `new`.
-* `@[deprecated_arg old new "use foo instead" (since := "2026-03-18")]` adds a custom message.
-* `@[deprecated_arg old (since := "2026-03-18")]` marks `old` as a removed parameter (no replacement).
-* `@[deprecated_arg old "no longer needed" (since := "2026-03-18")]` removed with a custom message.
-
-A warning is emitted if `(since := "...")` is omitted.
--/
-syntax (name := deprecated_arg) "deprecated_arg" ppSpace ident (ppSpace ident)? (ppSpace str)?
-    (" (" &"since" " := " str ")")? : attr
-
 /--
 The attribute `@[suggest_for ..]` on a declaration suggests likely ways in which
 someone might **incorrectly** refer to a definition.

src/Init/Omega/LinearCombo.lean

@@ -36,6 +36,9 @@ private local instance : ToString Int where
 private local instance : Repr Int where
   reprPrec i prec := if i < 0 then Repr.addAppParen (toString i) prec else toString i
 
+private local instance : Append String where
+  append := String.Internal.append
+
 /-- Internal representation of a linear combination of atoms, and a constant term. -/
 structure LinearCombo where
   /-- Constant term. -/

src/Lean/Compiler/LCNF/Check.lean

@@ -232,7 +232,6 @@ partial def checkCases (c : Cases .pure) : CheckM Unit := do
       withParams params do check k
 
 partial def check (code : Code .pure) : CheckM Unit := do
-  checkSystem "LCNF check"
   match code with
   | .let decl k => checkLetDecl decl; withFVarId decl.fvarId do check k
   | .fun decl k =>

src/Lean/Compiler/LCNF/CoalesceRC.lean

@@ -21,7 +21,7 @@ Within a basic block, it is always safe to:
   until the later inc) and thus doing all relevant `inc` in the beginning doesn't change
   semantics.
 - Move all decrements on a variable to the last `dec` location (summing the counts). Because the
-  value is guaranteed to stay alive until at least the last `dec` anyway so a similar argument to
+  value is guaranteed to stay alive until at least the last `dec` anyway so a similiar argument to
   `inc` holds.
 
 Crucially this pass must be placed after `expandResetReuse` as that one relies on `inc`s still being

src/Lean/Compiler/LCNF/ExpandResetReuse.lean

@@ -69,8 +69,8 @@ open ImpureType
 abbrev Mask := Array (Option FVarId)
 
 /--
-Try to erase `inc` instructions on projections of `targetId` occurring in the tail of `ds`.
-Return the updated `ds` and mask containing the `FVarId`s whose `inc` was removed.
+Try to erase `inc` instructions on projections of `targetId` occuring in the tail of `ds`.
+Return the updated `ds` and mask contianing the `FVarId`s whose `inc` was removed.
 -/
 partial def eraseProjIncFor (nFields : Nat) (targetId : FVarId) (ds : Array (CodeDecl .impure)) :
     CompilerM (Array (CodeDecl .impure) × Mask) := do

src/Lean/Compiler/LCNF/Main.lean

@@ -188,7 +188,6 @@ where
     profileitM Exception profilerName (← getOptions) do
       let mut state : (pu : Purity) × Array (Decl pu) := ⟨inPhase, decls⟩
       for pass in passes do
-        checkSystem "LCNF compiler"
         state ← withTraceNode `Compiler (fun _ => return m!"compiler phase: {pass.phase}, pass: {pass.name}") do
           let decls ← withPhase pass.phase do
             state.fst.withAssertPurity pass.phase.toPurity fun h => do

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

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

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

@@ -146,7 +146,7 @@ Similar to the default `Lean.withIncRecDepth`, but include the `inlineStack` in
 @[inline] def withIncRecDepth (x : SimpM α) : SimpM α := do
   let curr ← MonadRecDepth.getRecDepth
   let max  ← MonadRecDepth.getMaxRecDepth
-  if max != 0 && curr == max then
+  if curr == max then
     throwMaxRecDepth
   else
     MonadRecDepth.withRecDepth (curr+1) x

src/Lean/CoreM.lean

@@ -448,25 +448,13 @@ Note that the value of `ctx.initHeartbeats` is ignored and replaced with `IO.get
 protected def withIncRecDepth [Monad m] [MonadControlT CoreM m] (x : m α) : m α :=
   controlAt CoreM fun runInBase => withIncRecDepth (runInBase x)
 
-/--
-Record a check-in for the `LEAN_CHECK_SYSTEM_INTERVAL_MS` monitoring.
-When that env var is set, warns on stderr if too much CPU time has elapsed since
-the last check-in from either the C++ `check_system` or this function.
--/
-@[extern "lean_check_system_interval"]
-opaque checkSystemInterval (componentName : @& String) : BaseIO Unit
-
 /--
 Throws an internal interrupt exception if cancellation has been requested. The exception is not
 caught by `try catch` but is intended to be caught by `Command.withLoggingExceptions` at the top
 level of elaboration. In particular, we want to skip producing further incremental snapshots after
 the exception has been thrown.
-
-Like `checkSystem` but without the global heartbeat check, for callers that have their own
-heartbeat tracking (e.g. `SynthInstance`).
  -/
 @[inline] def checkInterrupted : CoreM Unit := do
-  checkSystemInterval "Lean elaborator"
   if let some tk := (← read).cancelTk? then
     if (← tk.isSet) then
       throwInterruptException

src/Lean/Data/Trie.lean

@@ -60,7 +60,7 @@ instance : EmptyCollection (Trie α) :=
 instance : Inhabited (Trie α) where
   default := empty
 
-/-- Insert or update the value at the given key `s`.  -/
+/-- Insert or update the value at a the given key `s`.  -/
 partial def upsert (t : Trie α) (s : String) (f : Option α → α) : Trie α :=
   let rec insertEmpty (i : Nat) : Trie α :=
     if h : i < s.utf8ByteSize then
@@ -100,7 +100,7 @@ partial def upsert (t : Trie α) (s : String) (f : Option α → α) : Trie α :
         node (f v) cs ts
   loop 0 t
 
-/-- Inserts a value at the given key `s`, overriding an existing value if present. -/
+/-- Inserts a value at a the given key `s`, overriding an existing value if present. -/
 partial def insert (t : Trie α) (s : String) (val : α) : Trie α :=
   upsert t s (fun _ => val)
 

src/Lean/DeprecatedModule.lean

@@ -1,45 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Wojciech Różowski
--/
-module
-
-prelude
-public import Lean.Compiler.ModPkgExt
-
-public section
-
-namespace Lean
-
-structure DeprecatedModuleEntry where
-  message? : Option String := none
-  since? : Option String := none
-  deriving Inhabited
-
-register_builtin_option linter.deprecated.module : Bool := {
-  defValue := true
-  descr := "if true, generate warnings when importing deprecated modules"
-}
-
-builtin_initialize deprecatedModuleExt : ModuleEnvExtension <| Option DeprecatedModuleEntry ←
-  registerModuleEnvExtension <| pure none
-
-def Environment.getDeprecatedModuleByIdx? (env : Environment) (idx : ModuleIdx) : Option DeprecatedModuleEntry :=
-  deprecatedModuleExt.getStateByIdx? env idx |>.join
-
-def Environment.setDeprecatedModule (entry : Option DeprecatedModuleEntry) (env : Environment) : Environment :=
-  deprecatedModuleExt.setState env entry
-
-def formatDeprecatedModuleWarning (env : Environment) (idx : ModuleIdx) (modName : Name)
-    (entry : DeprecatedModuleEntry) : String :=
-  let msg := entry.message?.getD ""
-  let replacements := env.header.moduleData[idx.toNat]!.imports.filter fun imp =>
-    imp.module != `Init
-  let lines := replacements.foldl (init := "") fun acc imp =>
-    acc ++ s!"import {imp.module}\n"
-  s!"{msg}\n\
-    '{modName}' has been deprecated: please replace this import by\n\n\
-    {lines}"
-
-end Lean

src/Lean/Elab.lean

@@ -39,7 +39,6 @@ public import Lean.Elab.Extra
 public import Lean.Elab.GenInjective
 public import Lean.Elab.BuiltinTerm
 public import Lean.Elab.Arg
-public import Lean.Elab.DeprecatedArg
 public import Lean.Elab.PatternVar
 public import Lean.Elab.ElabRules
 public import Lean.Elab.Macro

src/Lean/Elab/App.lean

@@ -11,7 +11,6 @@ public import Lean.Elab.Binders
 public import Lean.Elab.RecAppSyntax
 public import Lean.IdentifierSuggestion
 import all Lean.Elab.ErrorUtils
-import Lean.Elab.DeprecatedArg
 import Init.Omega
 
 public section
@@ -89,38 +88,6 @@ def synthesizeAppInstMVars (instMVars : Array MVarId) (app : Expr) : TermElabM U
 private def findBinderName? (namedArgs : List NamedArg) (binderName : Name) : Option NamedArg :=
   namedArgs.find? fun namedArg => namedArg.name == binderName
 
-/--
-If the function being applied is a constant, search `namedArgs` for an argument whose name is
-a deprecated alias of `binderName`. When `linter.deprecated.arg` is enabled (the default),
-returns `some namedArg` after emitting a deprecation warning with a code action hint. When the
-option is disabled, returns `none` (the old name falls through to the normal "invalid argument"
-error). The returned `namedArg` retains its original (old) name.
--/
-private def findDeprecatedBinderName? (namedArgs : List NamedArg) (f : Expr) (binderName : Name) :
-    TermElabM (Option NamedArg) := do
-  unless linter.deprecated.arg.get <| ← getOptions do return .none
-  unless f.getAppFn.isConst do return none
-  let declName := f.getAppFn.constName!
-  let env ← getEnv
-  for namedArg in namedArgs do
-    if let some entry := findDeprecatedArg? env declName namedArg.name then
-      if entry.newArg? == some binderName then
-        let msg := formatDeprecatedArgMsg entry
-        let span? := namedArg.ref[1]
-        let hint ←
-          if span?.getHeadInfo matches .original .. then
-            MessageData.hint "Rename this argument:" #[{
-              suggestion := .string entry.newArg?.get!.toString
-              span?
-              toCodeActionTitle? := some fun s =>
-                s!"Rename argument `{entry.oldArg}` to `{s}`"
-            }]
-          else
-            pure .nil
-        logWarningAt namedArg.ref <| .tagged ``deprecatedArgExt msg ++ hint
-        return some namedArg
-  return none
-
 /-- Erase entry for `binderName` from `namedArgs`. -/
 def eraseNamedArg (namedArgs : List NamedArg) (binderName : Name) : List NamedArg :=
   namedArgs.filter (·.name != binderName)
@@ -271,23 +238,6 @@ private def synthesizePendingAndNormalizeFunType : M Unit := do
     else
       for namedArg in s.namedArgs do
         let f := s.f.getAppFn
-        if f.isConst then
-          let env ← getEnv
-          if linter.deprecated.arg.get (← getOptions) then
-            if let some entry := findDeprecatedArg? env f.constName! namedArg.name then
-              if entry.newArg?.isNone then
-                let msg := formatDeprecatedArgMsg entry
-                let hint ←
-                  if namedArg.ref.getHeadInfo matches .original .. then
-                    MessageData.hint "Delete this argument:" #[{
-                      suggestion := .string ""
-                      span? := namedArg.ref
-                      toCodeActionTitle? := some fun _ =>
-                        s!"Delete deprecated argument `{entry.oldArg}`"
-                    }]
-                  else
-                    pure .nil
-                throwErrorAt namedArg.ref (msg ++ hint)
         let validNames ← getFoundNamedArgs
         let fnName? := if f.isConst then some f.constName! else none
         throwInvalidNamedArg namedArg fnName? validNames
@@ -806,16 +756,13 @@ mutual
       let binderName := fType.bindingName!
       let binfo := fType.bindingInfo!
       let s ← get
-      let namedArg? ← match findBinderName? s.namedArgs binderName with
-        | some namedArg => pure (some namedArg)
-        | none => findDeprecatedBinderName? s.namedArgs s.f binderName
-      match namedArg? with
+      match findBinderName? s.namedArgs binderName with
       | some namedArg =>
         propagateExpectedType namedArg.val
-        eraseNamedArg namedArg.name
+        eraseNamedArg binderName
         elabAndAddNewArg binderName namedArg.val
         main
-      | none =>
+      | none          =>
         unless binderName.hasMacroScopes do
           pushFoundNamedArg binderName
         match binfo with
@@ -1832,15 +1779,13 @@ To infer a namespace from the expected type, we do the following operations:
 - if the type is of the form `c x₁ ... xₙ` with `c` a constant, then try using `c` as the namespace,
   and if that doesn't work, try unfolding the expression and continuing.
 -/
-private partial def resolveDottedIdentFn (idRef : Syntax) (id : Name) (explicitUnivs : List Level) (expectedType? : Option Expr) : TermElabM (List (Expr × Syntax × List Syntax)) := do
+private partial def resolveDottedIdentFn (idRef : Syntax) (id : Name) (expectedType? : Option Expr) : TermElabM (List (Expr × Syntax × List Syntax)) := do
   unless id.isAtomic do
     throwError "Invalid dotted identifier notation: The name `{id}` must be atomic"
   tryPostponeIfNoneOrMVar expectedType?
   let some expectedType := expectedType?
     | throwNoExpectedType
   addCompletionInfo <| CompletionInfo.dotId idRef id (← getLCtx) expectedType?
-  -- We will check deprecations in `elabAppFnResolutions`.
-  withoutCheckDeprecated do
   withForallBody expectedType fun resultType => do
     go resultType expectedType #[]
 where
@@ -1880,10 +1825,8 @@ where
           |>.filter (fun (_, fieldList) => fieldList.isEmpty)
           |>.map Prod.fst
         if !candidates.isEmpty then
-          candidates.mapM fun resolvedName => return (← mkConst resolvedName explicitUnivs, ← getRef, [])
+          candidates.mapM fun resolvedName => return (← mkConst resolvedName, ← getRef, [])
         else if let some (fvar, []) ← resolveLocalName fullName then
-          unless explicitUnivs.isEmpty do
-            throwInvalidExplicitUniversesForLocal fvar
           return [(fvar, ← getRef, [])]
         else
           throwUnknownIdentifierAt (← getRef) (declHint := fullName) <| m!"Unknown constant `{.ofConstName fullName}`"
@@ -1923,10 +1866,6 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
       let some idx := idxStx.isFieldIdx?
         | throwError "Internal error: Unexpected field index syntax `{idxStx}`"
       elabAppFn e (LVal.fieldIdx idxStx idx :: lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
-    let elabDottedIdent (id : Syntax) (explicitUnivs : List Level) (explicit : Bool) : TermElabM (Array (TermElabResult Expr)) := do
-      let res ← withRef f <| resolveDottedIdentFn id id.getId.eraseMacroScopes explicitUnivs expectedType?
-      -- Use (forceTermInfo := true) because we want to record the result of .ident resolution even in patterns
-      elabAppFnResolutions f res lvals namedArgs args expectedType? explicit ellipsis overloaded acc (forceTermInfo := true)
     match f with
     | `($(e).$idx:fieldIdx) => elabFieldIdx e idx explicit
     | `($e |>.$idx:fieldIdx) => elabFieldIdx e idx explicit
@@ -1942,17 +1881,16 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
     | `($id:ident.{$us,*}) => do
       let us ← elabExplicitUnivs us
       elabAppFnId id us lvals namedArgs args expectedType? explicit ellipsis overloaded acc
-    | `(.$id:ident) => elabDottedIdent id [] explicit
-    | `(.$id:ident.{$us,*}) =>
-      let us ← elabExplicitUnivs us
-      elabDottedIdent id us explicit
-    | `(@$_:ident)
-    | `(@$_:ident.{$_us,*})
-    | `(@.$_:ident)
-    | `(@.$_:ident.{$_us,*}) =>
+    | `(@$id:ident) =>
+      elabAppFn id lvals namedArgs args expectedType? (explicit := true) ellipsis overloaded acc
+    | `(@$_:ident.{$_us,*}) =>
       elabAppFn (f.getArg 1) lvals namedArgs args expectedType? (explicit := true) ellipsis overloaded acc
     | `(@$_)     => throwUnsupportedSyntax -- invalid occurrence of `@`
     | `(_)       => throwError "A placeholder `_` cannot be used where a function is expected"
+    | `(.$id:ident) =>
+        let res ← withRef f <| resolveDottedIdentFn id id.getId.eraseMacroScopes expectedType?
+        -- Use (forceTermInfo := true) because we want to record the result of .ident resolution even in patterns
+        elabAppFnResolutions f res lvals namedArgs args expectedType? explicit ellipsis overloaded acc (forceTermInfo := true)
     | _ => do
       let catchPostpone := !overloaded
       /- If we are processing a choice node, then we should use `catchPostpone == false` when elaborating terms.
@@ -2095,15 +2033,13 @@ private def elabAtom : TermElab := fun stx expectedType? => do
 
 @[builtin_term_elab explicit] def elabExplicit : TermElab := fun stx expectedType? =>
   match stx with
-  | `(@$_:ident)           => elabAtom stx expectedType?  -- Recall that `elabApp` also has support for `@`
-  | `(@$_:ident.{$_us,*})  => elabAtom stx expectedType?
-  | `(@$(_).$_:fieldIdx)   => elabAtom stx expectedType?
-  | `(@$(_).$_:ident)      => elabAtom stx expectedType?
-  | `(@.$_:ident)          => elabAtom stx expectedType?
-  | `(@.$_:ident.{$_us,*}) => elabAtom stx expectedType?
-  | `(@($t))               => elabTerm t expectedType? (implicitLambda := false)   -- `@` is being used just to disable implicit lambdas
-  | `(@$t)                 => elabTerm t expectedType? (implicitLambda := false)   -- `@` is being used just to disable implicit lambdas
-  | _                      => throwUnsupportedSyntax
+  | `(@$_:ident)          => elabAtom stx expectedType?  -- Recall that `elabApp` also has support for `@`
+  | `(@$_:ident.{$_us,*}) => elabAtom stx expectedType?
+  | `(@$(_).$_:fieldIdx)  => elabAtom stx expectedType?
+  | `(@$(_).$_:ident)     => elabAtom stx expectedType?
+  | `(@($t))             => elabTerm t expectedType? (implicitLambda := false)    -- `@` is being used just to disable implicit lambdas
+  | `(@$t)               => elabTerm t expectedType? (implicitLambda := false)   -- `@` is being used just to disable implicit lambdas
+  | _                    => throwUnsupportedSyntax
 
 @[builtin_term_elab choice] def elabChoice : TermElab := elabAtom
 @[builtin_term_elab proj] def elabProj : TermElab := elabAtom

src/Lean/Elab/BuiltinCommand.lean

@@ -9,12 +9,10 @@ prelude
 public import Lean.Meta.Reduce
 public import Lean.Elab.Eval
 public import Lean.Elab.Command
-import Lean.Elab.DeprecatedSyntax
 public import Lean.Elab.Open
 import Init.Data.Nat.Order
 import Init.Data.Order.Lemmas
 import Init.System.Platform
-import Lean.DeprecatedModule
 
 public section
 
@@ -514,15 +512,6 @@ def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do
   modify fun s => { s with maxRecDepth := maxRecDepth.get options }
   modifyScope fun scope => { scope with opts := options }
 
-@[builtin_command_elab «unlock_limits»] def elabUnlockLimits : CommandElab := fun _ => do
-  let opts ← getOptions
-  let opts := maxHeartbeats.set opts 0
-  let opts := maxRecDepth.set opts 0
-  let opts := synthInstance.maxHeartbeats.set opts 0
-  modifyScope ({ · with opts })
-  -- update cached value as well
-  modify ({ · with maxRecDepth := 0 })
-
 open Lean.Parser.Command.InternalSyntax in
 @[builtin_macro Lean.Parser.Command.«in»] def expandInCmd : Macro
   | `($cmd₁ in%$tk $cmd₂) =>
@@ -717,54 +706,4 @@ where
     let env ← getEnv
     IO.eprintln (← env.dbgFormatAsyncState)
 
-/-- Elaborate `deprecated_module`, marking the current module as deprecated. -/
-@[builtin_command_elab Parser.Command.deprecated_module]
-def elabDeprecatedModule : CommandElab
-  | `(Parser.Command.deprecated_module| deprecated_module $[$msg?]? $[(since := $since?)]?) => do
-    let message? := msg?.map TSyntax.getString
-    let since? := since?.map TSyntax.getString
-    if (deprecatedModuleExt.getState (← getEnv)).isSome then
-      logWarning "module is already marked as deprecated"
-    if since?.isNone then
-      logWarning "`deprecated_module` should specify the date or library version \
-        at which the deprecation was introduced, using `(since := \"...\")`"
-    modifyEnv fun env => env.setDeprecatedModule (some { message?, since? })
-  | _ => throwUnsupportedSyntax
-
-/-- Elaborate `#show_deprecated_modules`, displaying all deprecated modules. -/
-@[builtin_command_elab Parser.Command.showDeprecatedModules]
-def elabShowDeprecatedModules : CommandElab := fun _ => do
-  let env ← getEnv
-  let mut parts : Array String := #["Deprecated modules\n"]
-  for h : idx in [:env.header.moduleNames.size] do
-    if let some entry := env.getDeprecatedModuleByIdx? idx then
-      let modName := env.header.moduleNames[idx]
-      let msg := match entry.message? with
-        | some str => s!"message '{str}'"
-        | none => "no message"
-      let replacements := env.header.moduleData[idx]!.imports.filter fun imp =>
-        imp.module != `Init
-      parts := parts.push s!"'{modName}' deprecates to\n{replacements.map (·.module)}\nwith {msg}\n"
-  -- Also show the current module's deprecation if set.
-  if let some entry := deprecatedModuleExt.getState env then
-    let modName := env.mainModule
-    let msg := match entry.message? with
-      | some str => s!"message '{str}'"
-      | none => "no message"
-    let replacements := env.imports.filter fun imp =>
-      imp.module != `Init
-    parts := parts.push s!"'{modName}' deprecates to\n{replacements.map (·.module)}\nwith {msg}\n"
-  logInfo (String.intercalate "\n" parts.toList)
-
-@[builtin_command_elab Parser.Command.deprecatedSyntax] def elabDeprecatedSyntax : CommandElab := fun stx => do
-  let id := stx[1]
-  let kind ← liftCoreM <| checkSyntaxNodeKindAtNamespaces id.getId (← getCurrNamespace)
-  let text? := if stx[2].isNone then none else stx[2][0].isStrLit?
-  let since? := if stx[3].isNone then none else stx[3][3].isStrLit?
-  if since?.isNone then
-    logWarning "`deprecated_syntax` should specify the date or library version at which the \
-      deprecation was introduced, using `(since := \"...\")`"
-  modifyEnv fun env =>
-    deprecatedSyntaxExt.addEntry env { kind, text?, since? }
-
 end Lean.Elab.Command

src/Lean/Elab/BuiltinDo/If.lean

@@ -63,6 +63,6 @@ where
     doElabToSyntax "else branch of if with condition {cond}" (elabDiteBranch false) fun else_ => do
     let mγ ← mkMonadicType (← read).doBlockResultType
     match h with
-    | `(_%$tk) => Term.elabTermEnsuringType (← `(if _%$tk : $cond then $then_ else $else_)) mγ
+    | `(_%$tk) => Term.elabTermEnsuringType (← `(if $(⟨tk⟩):hole : $cond then $then_ else $else_)) mγ
     | `($h:ident) => Term.elabTermEnsuringType (← `(if $h:ident : $cond then $then_ else $else_)) mγ
     | _ => throwUnsupportedSyntax

src/Lean/Elab/Coinductive.lean

@@ -43,7 +43,7 @@ builtin_initialize
 
   Upon such rewrite, the code for adding flat inductives does not diverge much from the usual
   way its done for inductive declarations, but we omit applying attributes/modifiers and
-  we do not set the syntax references to track those declarations (as this is auxiliary piece of
+  we do not set the syntax references to track those declarations (as this is auxillary piece of
   data hidden from the user).
 
   Then, upon adding such flat inductives for each definition in the mutual block to the environment,
@@ -345,7 +345,7 @@ private def mkCasesOnCoinductive (infos : Array InductiveVal) : MetaM Unit := do
         | throwError "expected to be quantifier"
       let motiveMVar ← mkFreshExprMVar type
       /-
-        We intro all the indices and the occurrence of the coinductive predicate
+        We intro all the indices and the occurence of the coinductive predicate
       -/
       let (fvars, subgoal) ← motiveMVar.mvarId!.introN (info.numIndices + 1)
       subgoal.withContext do
@@ -373,7 +373,7 @@ private def mkCasesOnCoinductive (infos : Array InductiveVal) : MetaM Unit := do
           -/
           let originalCasesOn := mkAppN originalCasesOn indices
           /-
-            The next argument is the occurrence of the coinductive predicate.
+            The next argument is the occurence of the coinductive predicate.
             The original `casesOn` of the flat inductive mentions it in
             unrolled form, so we need to rewrite it.
           -/
@@ -447,7 +447,7 @@ public def elabCoinductive (coinductiveElabData : Array CoinductiveElabData) : T
   let consts := namesAndTypes.map fun (name, _) => (mkConst name levelParams)
   /-
     We create values of each of PreDefinitions, by taking existential (see `Meta.SumOfProducts`)
-    form of the associated flat inductives and applying parameters, as well as recursive calls
+    form of the associated flat inductives and applying paramaters, as well as recursive calls
     (with their parameters passed).
   -/
   let preDefVals ← forallBoundedTelescope infos[0]!.type originalNumParams fun params _ => do

src/Lean/Elab/Command.lean

@@ -10,7 +10,6 @@ public import Lean.Meta.Diagnostics
 public import Lean.Elab.Binders
 public import Lean.Elab.Command.Scope
 public import Lean.Elab.SetOption
-import Lean.Elab.DeprecatedSyntax
 public meta import Lean.Parser.Command
 
 public section
@@ -469,7 +468,6 @@ where go := do
       else withTraceNode `Elab.command (fun _ => return stx) (tag :=
         -- special case: show actual declaration kind for `declaration` commands
         (if stx.isOfKind ``Parser.Command.declaration then stx[1] else stx).getKind.toString) do
-        checkDeprecatedSyntax stx (← read).macroStack
         let s ← get
         match (← liftMacroM <| expandMacroImpl? s.env stx) with
         | some (decl, stxNew?) =>

src/Lean/Elab/DeprecatedArg.lean

@@ -1,97 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Wojciech Różowski
--/
-module
-
-prelude
-public import Lean.EnvExtension
-public import Lean.Message
-import Lean.Elab.Term
-
-public section
-
-namespace Lean.Elab
-open Meta
-
-register_builtin_option linter.deprecated.arg : Bool := {
-  defValue := true
-  descr := "if true, generate deprecation warnings and errors for deprecated parameters"
-}
-
-/-- Entry mapping an old parameter name to a new (or no) parameter for a given declaration. -/
-structure DeprecatedArgEntry where
-  declName : Name
-  oldArg : Name
-  newArg? : Option Name := none
-  text? : Option String := none
-  since? : Option String := none
-  deriving Inhabited
-
-/-- State: `declName → (oldArg → entry)` -/
-abbrev DeprecatedArgState := NameMap (NameMap DeprecatedArgEntry)
-
-private def addDeprecatedArgEntry (s : DeprecatedArgState) (e : DeprecatedArgEntry) : DeprecatedArgState :=
-  let inner := (s.find? e.declName).getD {} |>.insert e.oldArg e
-  s.insert e.declName inner
-
-builtin_initialize deprecatedArgExt :
-    SimplePersistentEnvExtension DeprecatedArgEntry DeprecatedArgState ←
-  registerSimplePersistentEnvExtension {
-    addEntryFn := addDeprecatedArgEntry
-    addImportedFn := mkStateFromImportedEntries addDeprecatedArgEntry {}
-  }
-
-/-- Look up a deprecated argument mapping for `(declName, argName)`. -/
-def findDeprecatedArg? (env : Environment) (declName : Name) (argName : Name) :
-    Option DeprecatedArgEntry :=
-  (deprecatedArgExt.getState env |>.find? declName) >>= (·.find? argName)
-
-/-- Format the deprecation warning message for a deprecated argument. -/
-def formatDeprecatedArgMsg (entry : DeprecatedArgEntry) : MessageData :=
-  let base := match entry.newArg? with
-  | some newArg =>
-    m!"parameter `{entry.oldArg}` of `{.ofConstName entry.declName}` has been deprecated, \
-      use `{newArg}` instead"
-  | none =>
-    m!"parameter `{entry.oldArg}` of `{.ofConstName entry.declName}` has been deprecated"
-  match entry.text? with
-  | some text => base ++ m!": {text}"
-  | none => base
-
-builtin_initialize registerBuiltinAttribute {
-  name := `deprecated_arg
-  descr := "mark a parameter as deprecated"
-  add := fun declName stx _kind => do
-    let `(attr| deprecated_arg $oldId $[$newId?]? $[$text?]? $[(since := $since?)]?) := stx
-      | throwError "Invalid `[deprecated_arg]` attribute syntax"
-    let oldArg := oldId.getId
-    let newArg? := newId?.map TSyntax.getId
-    let text? := text?.map TSyntax.getString |>.filter (!·.isEmpty)
-    let since? := since?.map TSyntax.getString
-    let info ← getConstInfo declName
-    let paramNames ← MetaM.run' do
-      forallTelescopeReducing info.type fun xs _ =>
-        xs.mapM fun x => return (← x.fvarId!.getDecl).userName
-    if let some newArg := newArg? then
-      -- We have a replacement provided
-      unless Array.any paramNames (· == newArg) do
-        throwError "`{newArg}` is not a parameter of `{declName}`"
-      if Array.any paramNames (· == oldArg) then
-        throwError "`{oldArg}` is still a parameter of `{declName}`; \
-          rename it to `{newArg}` before adding `@[deprecated_arg]`"
-    else
-      -- We do not have a replacement provided
-      if Array.any paramNames (· == oldArg) then
-        throwError "`{oldArg}` is still a parameter of `{declName}`; \
-          remove it before adding `@[deprecated_arg]`"
-    if since?.isNone then
-      logWarning "`[deprecated_arg]` attribute should specify the date or library version \
-        at which the deprecation was introduced, using `(since := \"...\")`"
-    modifyEnv fun env => deprecatedArgExt.addEntry env {
-      declName, oldArg, newArg?, text?, since?
-    }
-}
-
-end Lean.Elab

src/Lean/Elab/DeprecatedSyntax.lean

@@ -1,71 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Wojciech Różowski
--/
-module
-
-prelude
-public import Lean.MonadEnv
-public import Lean.Linter.Basic
-public import Lean.Elab.Util
-
-public section
-
-namespace Lean.Linter
-
-register_builtin_option linter.deprecated.syntax : Bool := {
-  defValue := true
-  descr := "if true, generate warnings when deprecated syntax is used"
-}
-
-end Lean.Linter
-
-namespace Lean.Elab
-
-/-- Entry recording that a syntax kind has been deprecated. -/
-structure SyntaxDeprecationEntry where
-  /-- The syntax node kind that is deprecated. -/
-  kind : SyntaxNodeKind
-  /-- Optional deprecation message. -/
-  text? : Option String := none
-  /-- Optional version or date at which the syntax was deprecated. -/
-  since? : Option String := none
-
-builtin_initialize deprecatedSyntaxExt :
-    SimplePersistentEnvExtension SyntaxDeprecationEntry (NameMap SyntaxDeprecationEntry) ←
-  registerSimplePersistentEnvExtension {
-    addImportedFn := mkStateFromImportedEntries (fun m e => m.insert e.kind e) {}
-    addEntryFn := fun m e => m.insert e.kind e
-  }
-
-/--
-Check whether `stx` is a deprecated syntax kind, and if so, emit a warning.
-
-If `macroStack` is non-empty, the warning is attributed to the macro call site rather than the
-syntax itself.
--/
-def checkDeprecatedSyntax [Monad m] [MonadEnv m] [MonadLog m] [MonadOptions m]
-    [AddMessageContext m] [MonadRef m] (stx : Syntax) (macroStack : MacroStack) : m Unit := do
-  let env ← getEnv
-  let kind := stx.getKind
-  if let some entry := (deprecatedSyntaxExt.getState env).find? kind then
-    let extraMsg := match entry.text? with
-      | some text => m!": {text}"
-      | none => m!""
-    match macroStack with
-    | { before := macroStx, .. } :: { before := callerStx, .. } :: _ =>
-      let expandedFrom :=
-        if callerStx.getKind != macroStx.getKind then
-          m!" (expanded from '{callerStx.getKind}')"
-        else m!""
-      Linter.logLintIf Linter.linter.deprecated.syntax macroStx
-        m!"macro '{macroStx.getKind}'{expandedFrom} produces deprecated syntax '{kind}'{extraMsg}"
-    | { before := macroStx, .. } :: [] =>
-      Linter.logLintIf Linter.linter.deprecated.syntax macroStx
-        m!"macro '{macroStx.getKind}' produces deprecated syntax '{kind}'{extraMsg}"
-    | [] =>
-      Linter.logLintIf Linter.linter.deprecated.syntax stx
-        m!"syntax '{kind}' has been deprecated{extraMsg}"
-
-end Lean.Elab

src/Lean/Elab/DocString.lean

@@ -85,10 +85,6 @@ structure State where
   -/
   lctx : LocalContext
   /--
-  The local instances.
-
-  The `MonadLift TermElabM DocM` instance runs the lifted action with these instances, so elaboration
-  commands that mutate this state cause it to take effect in subsequent commands.
   -/
   localInstances : LocalInstances
   /--

src/Lean/Elab/Import.lean

@@ -9,7 +9,6 @@ prelude
 public import Lean.Parser.Module
 meta import Lean.Parser.Module
 import Lean.Compiler.ModPkgExt
-public import Lean.DeprecatedModule
 
 public section
 
@@ -43,66 +42,12 @@ def HeaderSyntax.toModuleHeader (stx : HeaderSyntax) : ModuleHeader where
 
 abbrev headerToImports := @HeaderSyntax.imports
 
-/--
-Check imported modules for deprecation and emit warnings.
-
-The `-- deprecated_module: ignore` comment can be placed on the `module` keyword to suppress
-all warnings, or on individual `import` statements to suppress specific ones.
-This follows the same pattern as `-- shake: keep` in Lake shake.
-
-The `headerStx?` parameter carries the header syntax used for checking trailing comments.
-When called from the Language Server, the main header syntax may have its trailing trivia
-stripped by `unsetTrailing` for caching purposes, so `origHeaderStx?` can supply the original
-(untrimmed) syntax to preserve `-- deprecated_module: ignore` annotations on the last import.
--/
-def checkDeprecatedImports
-    (env : Environment) (imports : Array Import) (opts : Options)
-    (inputCtx : Parser.InputContext) (startPos : String.Pos.Raw) (messages : MessageLog)
-    (headerStx? : Option HeaderSyntax := none)
-    (origHeaderStx? : Option HeaderSyntax := none)
-    : MessageLog := Id.run do
-  let mut opts := opts
-  let mut ignoreDeprecatedImports : NameSet := {}
-  if let some headerStx := origHeaderStx? <|> headerStx? then
-    match headerStx with
-    | `(Parser.Module.header| $[module%$moduleTk]? $[prelude%$_]? $importsStx*) =>
-      if moduleTk.any (·.getTrailing?.any (·.toString.contains "deprecated_module: ignore")) then
-        opts := linter.deprecated.module.set opts false
-      for impStx in importsStx do
-        if impStx.raw.getTrailing?.any (·.toString.contains "deprecated_module: ignore") then
-          match impStx with
-          | `(Parser.Module.import| $[public%$_]? $[meta%$_]? import $[all%$_]? $n) =>
-            ignoreDeprecatedImports := ignoreDeprecatedImports.insert n.getId
-          | _ => pure ()
-    | _ => pure ()
-  if !linter.deprecated.module.get opts then
-    return messages
-  imports.foldl (init := messages) fun messages imp =>
-    if ignoreDeprecatedImports.contains imp.module then
-      messages
-    else
-    match env.getModuleIdx? imp.module with
-    | some idx =>
-      match env.getDeprecatedModuleByIdx? idx with
-      | some entry =>
-        let pos := inputCtx.fileMap.toPosition startPos
-        messages.add {
-          fileName := inputCtx.fileName
-          pos := pos
-          severity := .warning
-          data := .tagged ``deprecatedModuleExt <| formatDeprecatedModuleWarning env idx imp.module entry
-        }
-      | none => messages
-    | none => messages
-
 def processHeaderCore
     (startPos : String.Pos.Raw) (imports : Array Import) (isModule : Bool)
     (opts : Options) (messages : MessageLog) (inputCtx : Parser.InputContext)
     (trustLevel : UInt32 := 0) (plugins : Array System.FilePath := #[]) (leakEnv := false)
     (mainModule := Name.anonymous) (package? : Option PkgId := none)
     (arts : NameMap ImportArtifacts := {})
-    (headerStx? : Option HeaderSyntax := none)
-    (origHeaderStx? : Option HeaderSyntax := none)
     : IO (Environment × MessageLog) := do
   let level := if isModule then
     if Elab.inServer.get opts then
@@ -121,7 +66,6 @@ def processHeaderCore
     let pos := inputCtx.fileMap.toPosition startPos
     pure (env, messages.add { fileName := inputCtx.fileName, data := toString e, pos := pos })
   let env := env.setMainModule mainModule |>.setModulePackage package?
-  let messages := checkDeprecatedImports env imports opts inputCtx startPos messages headerStx? origHeaderStx?
   return (env, messages)
 
 /--
@@ -138,7 +82,6 @@ backwards compatibility measure not compatible with the module system.
     : IO (Environment × MessageLog) := do
   processHeaderCore header.startPos header.imports header.isModule
     opts messages inputCtx trustLevel plugins leakEnv mainModule
-    (headerStx? := header)
 
 def parseImports (input : String) (fileName : Option String := none) : IO (Array Import × Position × MessageLog) := do
   let fileName := fileName.getD "<input>"

src/Lean/Elab/PreDefinition/WF/Unfold.lean

@@ -73,9 +73,8 @@ def splitMatchOrCasesOn (mvarId : MVarId) (e : Expr) (matcherInfo : MatcherInfo)
   if (← isMatcherApp e) then
     Split.splitMatch mvarId e
   else
-    -- For casesOn, the last discriminant is the major premise;
-    -- `cases` will handle any index discriminants automatically.
-    let discr := e.getAppArgs[matcherInfo.numParams + matcherInfo.numDiscrs]!
+    assert! matcherInfo.numDiscrs = 1
+    let discr := e.getAppArgs[matcherInfo.numParams + 1]!
     assert! discr.isFVar
     let subgoals ← mvarId.cases discr.fvarId!
     return subgoals.map (·.mvarId) |>.toList

src/Lean/Elab/Quotation/Precheck.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Lean.Elab.Quotation.Util
-import Lean.Elab.DeprecatedSyntax
 
 public section
 
@@ -57,14 +56,6 @@ unsafe builtin_initialize precheckAttribute : KeyedDeclsAttribute Precheck ←
   }
 
 partial def precheck : Precheck := fun stx => do
-  -- Check for deprecated syntax kinds in quotations
-  if let some entry := (deprecatedSyntaxExt.getState (← getEnv)).find? stx.getKind then
-    let extraMsg := match entry.text? with
-      | some text => m!": {text}"
-      | none => m!""
-    withRef stx do
-      Linter.logLintIf Linter.linter.deprecated.syntax stx
-        m!"quotation uses deprecated syntax '{stx.getKind}'{extraMsg}"
   if let p::_ := precheckAttribute.getValues (← getEnv) stx.getKind then
     if ← catchInternalId unsupportedSyntaxExceptionId (do withRef stx <| p stx; pure true) (fun _ => pure false) then
       return

src/Lean/Elab/SyntheticMVars.lean

@@ -582,7 +582,6 @@ mutual
     -- We use `filterRevM` instead of `filterM` to make sure we process the synthetic metavariables using the order they were created.
     -- It would not be incorrect to use `filterM`.
     let remainingPendingMVars ← pendingMVars.filterRevM fun mvarId => do
-       checkSystem "synthesize pending MVars"
        -- We use `traceM` because we want to make sure the metavar local context is used to trace the message
        traceM `Elab.postpone (mvarId.withContext do addMessageContext m!"resuming {mkMVar mvarId}")
        let succeeded ← synthesizeSyntheticMVar mvarId postponeOnError runTactics

src/Lean/Elab/Tactic/Basic.lean

@@ -8,7 +8,6 @@ module
 prelude
 public import Lean.Meta.Tactic.Util
 public import Lean.Elab.Term
-import Lean.Elab.DeprecatedSyntax
 import Init.Omega
 
 public section
@@ -193,7 +192,6 @@ partial def evalTactic (stx : Syntax) : TacticM Unit := do
         Term.withoutTacticIncrementality true <| withTacticInfoContext stx do
           stx.getArgs.forM evalTactic
       else withTraceNode `Elab.step (fun _ => return stx) (tag := stx.getKind.toString) do
-        checkDeprecatedSyntax stx (← readThe Term.Context).macroStack
         let evalFns := tacticElabAttribute.getEntries (← getEnv) stx.getKind
         let macros  := macroAttribute.getEntries (← getEnv) stx.getKind
         if evalFns.isEmpty && macros.isEmpty then

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

@@ -7,8 +7,6 @@ module
 prelude
 public import Lean.Elab.Tactic.Grind.Basic
 import Lean.Elab.Tactic.ConfigSetter
-import Lean.Elab.DeprecatedSyntax  -- shake: skip (workaround for `mkConfigSetter` failing to interpret `deprecatedSyntaxExt`, to be fixed)
-
 public section
 namespace Lean.Elab.Tactic.Grind
 

src/Lean/Elab/Term/TermElabM.lean

@@ -9,7 +9,6 @@ prelude
 public import Lean.Meta.Coe
 public import Lean.Util.CollectLevelMVars
 public import Lean.Linter.Deprecated
-import Lean.Elab.DeprecatedSyntax
 public import Lean.Elab.Attributes
 public import Lean.Elab.Level
 public import Lean.Elab.PreDefinition.TerminationHint
@@ -1795,7 +1794,6 @@ private partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone :
     withTraceNode `Elab.step (fun _ => return m!"expected type: {expectedType?}, term\n{stx}")
       (tag := stx.getKind.toString) do
     checkSystem "elaborator"
-    checkDeprecatedSyntax stx (← read).macroStack
     let env ← getEnv
     let result ← match (← liftMacroM (expandMacroImpl? env stx)) with
     | some (decl, stxNew?) =>
@@ -2124,14 +2122,11 @@ private def mkConsts (candidates : List (Name × List String)) (explicitLevels :
     let const ← withoutCheckDeprecated <| mkConst declName explicitLevels
     return (const, projs) :: result
 
-def throwInvalidExplicitUniversesForLocal {α} (e : Expr) : TermElabM α :=
-  throwError "invalid use of explicit universe parameters, `{e}` is a local variable"
-
 def resolveName (stx : Syntax) (n : Name) (preresolved : List Syntax.Preresolved) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (List (Expr × List String)) := do
   addCompletionInfo <| CompletionInfo.id stx stx.getId (danglingDot := false) (← getLCtx) expectedType?
   if let some (e, projs) ← resolveLocalName n then
     unless explicitLevels.isEmpty do
-      throwInvalidExplicitUniversesForLocal e
+      throwError "invalid use of explicit universe parameters, `{e}` is a local variable"
     return [(e, projs)]
   let preresolved := preresolved.filterMap fun
     | .decl n projs => some (n, projs)

src/Lean/Exception.lean

@@ -245,7 +245,7 @@ We use this combinator to prevent stack overflows.
 @[inline] def withIncRecDepth [Monad m] [MonadError m] [MonadRecDepth m] (x : m α) : m α := do
   let curr ← MonadRecDepth.getRecDepth
   let max  ← MonadRecDepth.getMaxRecDepth
-  if max != 0 && curr == max then
+  if curr == max then
     throwMaxRecDepthAt (← getRef)
   else
     MonadRecDepth.withRecDepth (curr+1) x

src/Lean/Language/Lean.lean

@@ -478,11 +478,11 @@ where
         }
         result? := some {
           parserState
-          processedSnap := (← processHeader ⟨trimmedStx⟩ stx parserState)
+          processedSnap := (← processHeader ⟨trimmedStx⟩ parserState)
         }
       }
 
-  processHeader (stx : HeaderSyntax) (origStx : HeaderSyntax) (parserState : Parser.ModuleParserState) :
+  processHeader (stx : HeaderSyntax) (parserState : Parser.ModuleParserState) :
       LeanProcessingM (SnapshotTask HeaderProcessedSnapshot) := do
     let ctx ← read
     SnapshotTask.ofIO none none (.some ⟨0, ctx.endPos⟩) <|
@@ -498,7 +498,6 @@ where
       let (headerEnv, msgLog) ← Elab.processHeaderCore (leakEnv := true)
         stx.startPos setup.imports setup.isModule setup.opts .empty ctx.toInputContext
         setup.trustLevel setup.plugins setup.mainModuleName setup.package? setup.importArts
-        (headerStx? := stx) (origHeaderStx? := origStx)
       let stopTime := (← IO.monoNanosNow).toFloat / 1000000000
       let diagnostics := (← Snapshot.Diagnostics.ofMessageLog msgLog)
       if msgLog.hasErrors then

src/Lean/Level.lean

@@ -441,27 +441,18 @@ def Result.imax : Result → Result → Result
   | f, Result.imaxNode Fs => Result.imaxNode (f::Fs)
   | f₁, f₂                => Result.imaxNode [f₁, f₂]
 
-structure Context where
-  mvars : Bool
-  lIndex? : LMVarId → Option Nat
-
-abbrev M := ReaderM Context
-
-def toResult (l : Level) : M Result := do
+def toResult (l : Level) (mvars : Bool) : Result :=
   match l with
-  | zero       => return Result.num 0
-  | succ l     => return Result.succ (← toResult l)
-  | max l₁ l₂  => return Result.max (← toResult l₁) (← toResult l₂)
-  | imax l₁ l₂ => return Result.imax (← toResult l₁) (← toResult l₂)
-  | param n    => return Result.leaf n
+  | zero       => Result.num 0
+  | succ l     => Result.succ (toResult l mvars)
+  | max l₁ l₂  => Result.max (toResult l₁ mvars) (toResult l₂ mvars)
+  | imax l₁ l₂ => Result.imax (toResult l₁ mvars) (toResult l₂ mvars)
+  | param n    => Result.leaf n
   | mvar n     =>
-    if !(← read).mvars then
-      return Result.leaf `_
-    else if let some i := (← read).lIndex? n then
-      return Result.leaf <| Name.num (Name.mkSimple "?u") (i + 1)
+    if mvars then
+      Result.leaf <| n.name.replacePrefix `_uniq (Name.mkSimple "?u")
     else
-      -- Undefined mvar, use internal name
-      return Result.leaf <| n.name.replacePrefix `_uniq (Name.mkSimple "?_mvar")
+      Result.leaf `_
 
 private def parenIfFalse : Format → Bool → Format
   | f, true  => f
@@ -478,7 +469,7 @@ mutual
     | Result.offset f 0,     r => format f r
     | Result.offset f (k+1), r =>
       let f' := format f false;
-      parenIfFalse (f' ++ " + " ++ Std.format (k+1)) r
+      parenIfFalse (f' ++ "+" ++ Std.format (k+1)) r
     | Result.maxNode fs,    r => parenIfFalse (Format.group <| "max"  ++ formatLst fs) r
     | Result.imaxNode fs,   r => parenIfFalse (Format.group <| "imax" ++ formatLst fs) r
 end
@@ -496,20 +487,20 @@ protected partial def Result.quote (r : Result) (prec : Nat) : Syntax.Level :=
 
 end PP
 
-protected def format (u : Level) (mvars : Bool) (lIndex? : LMVarId → Option Nat) : Format :=
-  (PP.toResult u) |>.run { mvars, lIndex? } |>.format true
+protected def format (u : Level) (mvars : Bool) : Format :=
+  (PP.toResult u mvars).format true
 
 instance : ToFormat Level where
-  format u := Level.format u (mvars := true) (lIndex? := fun _ => none)
+  format u := Level.format u (mvars := true)
 
 instance : ToString Level where
   toString u := Format.pretty (format u)
 
-protected def quote (u : Level) (prec : Nat := 0) (mvars : Bool := true) (lIndex? : LMVarId → Option Nat) : Syntax.Level :=
-  (PP.toResult u) |>.run { mvars, lIndex? } |>.quote prec
+protected def quote (u : Level) (prec : Nat := 0) (mvars : Bool := true) : Syntax.Level :=
+  (PP.toResult u (mvars := mvars)).quote prec
 
 instance : Quote Level `level where
-  quote := Level.quote (lIndex? := fun _ => none)
+  quote := Level.quote
 
 end Level
 

src/Lean/LibrarySuggestions/Basic.lean

@@ -91,10 +91,10 @@ end FoldRelevantConstantsImpl
 @[implemented_by FoldRelevantConstantsImpl.foldUnsafe]
 public opaque foldRelevantConstants {α : Type} (e : Expr) (init : α) (f : Name → α → MetaM α) : MetaM α := pure init
 
-/-- Collect the constants occurring in `e` (once each), skipping instance arguments and proofs. -/
+/-- Collect the constants occuring in `e` (once each), skipping instance arguments and proofs. -/
 public def relevantConstants (e : Expr) : MetaM (Array Name) := foldRelevantConstants e #[] (fun n ns => return ns.push n)
 
-/-- Collect the constants occurring in `e` (once each), skipping instance arguments and proofs. -/
+/-- Collect the constants occuring in `e` (once each), skipping instance arguments and proofs. -/
 public def relevantConstantsAsSet (e : Expr) : MetaM NameSet := foldRelevantConstants e ∅ (fun n ns => return ns.insert n)
 
 end Lean.Expr

src/Lean/LibrarySuggestions/SymbolFrequency.lean

@@ -66,11 +66,7 @@ Helper function for running `MetaM` code during module export, when there is not
 Panics on errors.
 -/
 unsafe def _root_.Lean.Environment.unsafeRunMetaM [Inhabited α] (env : Environment) (x : MetaM α) : α :=
-   match unsafeEIO ((((withoutExporting x).run' {} {}).run'
-    { fileName := "symbolFrequency", fileMap := default
-      -- avoid triggering since limit cannot be raised here
-      maxHeartbeats := 0 }
-    { env })) with
+   match unsafeEIO ((((withoutExporting x).run' {} {}).run' { fileName := "symbolFrequency", fileMap := default } { env })) with
    | Except.ok a => a
    | Except.error ex => panic! match unsafeIO ex.toMessageData.toString with
      | Except.ok s => s

src/Lean/Linter/MissingDocs.lean

@@ -112,37 +112,15 @@ builtin_initialize
 def lint (stx : Syntax) (msg : String) : CommandElabM Unit :=
   logLint linter.missingDocs stx m!"missing doc string for {msg}"
 
-def lintEmpty (stx : Syntax) (msg : String) : CommandElabM Unit :=
-  logLint linter.missingDocs stx m!"empty doc string for {msg}"
-
 def lintNamed (stx : Syntax) (msg : String) : CommandElabM Unit :=
   lint stx s!"{msg} {stx.getId}"
 
-def lintEmptyNamed (stx : Syntax) (msg : String) : CommandElabM Unit :=
-  lintEmpty stx s!"{msg} {stx.getId}"
-
 def lintField (parent stx : Syntax) (msg : String) : CommandElabM Unit :=
   lint stx s!"{msg} {parent.getId}.{stx.getId}"
 
-def lintEmptyField (parent stx : Syntax) (msg : String) : CommandElabM Unit :=
-  lintEmpty stx s!"{msg} {parent.getId}.{stx.getId}"
-
 def lintStructField (parent stx : Syntax) (msg : String) : CommandElabM Unit :=
   lint stx s!"{msg} {parent.getId}.{stx.getId}"
 
-private def isEmptyDocString (docOpt : Syntax) : CommandElabM Bool := do
-  if docOpt.isNone then return false
-  let docStx : TSyntax `Lean.Parser.Command.docComment := ⟨docOpt[0]⟩
-  -- Verso doc comments with interpolated content cannot be extracted as plain text,
-  -- but they are clearly not empty.
-  if let .node _ `Lean.Parser.Command.versoCommentBody _ := docStx.raw[1] then
-    if !docStx.raw[1][0].isAtom then return false
-  let text ← getDocStringText docStx
-  return text.trimAscii.isEmpty
-
-def isMissingDoc (docOpt : Syntax) : CommandElabM Bool := do
-  return docOpt.isNone || (← isEmptyDocString docOpt)
-
 def hasInheritDoc (attrs : Syntax) : Bool :=
   attrs[0][1].getSepArgs.any fun attr =>
     attr[1].isOfKind ``Parser.Attr.simple &&
@@ -152,68 +130,38 @@ def hasTacticAlt (attrs : Syntax) : Bool :=
   attrs[0][1].getSepArgs.any fun attr =>
     attr[1].isOfKind ``Parser.Attr.tactic_alt
 
-def declModifiersDocStatus (mods : Syntax) : CommandElabM (Option Bool) := do
+def declModifiersPubNoDoc (mods : Syntax) : CommandElabM Bool := do
   let isPublic := if (← getEnv).header.isModule && !(← getScope).isPublic then
     mods[2][0].getKind == ``Command.public else
     mods[2][0].getKind != ``Command.private
-  if !isPublic || hasInheritDoc mods[1] then return none
-  if mods[0].isNone then return some false
-  if (← isEmptyDocString mods[0]) then return some true
-  return none
+  return isPublic && mods[0].isNone && !hasInheritDoc mods[1]
 
-def declModifiersPubNoDoc (mods : Syntax) : CommandElabM Bool := do
-  return (← declModifiersDocStatus mods).isSome
-
-private def lintDocStatus (isEmpty : Bool) (stx : Syntax) (msg : String) : CommandElabM Unit :=
-  if isEmpty then lintEmpty stx msg else lint stx msg
-
-private def lintDocStatusNamed (isEmpty : Bool) (stx : Syntax) (msg : String) : CommandElabM Unit :=
-  if isEmpty then lintEmptyNamed stx msg else lintNamed stx msg
-
-private def lintDocStatusField (isEmpty : Bool) (parent stx : Syntax) (msg : String) :
-    CommandElabM Unit :=
-  if isEmpty then lintEmptyField parent stx msg else lintField parent stx msg
-
-def lintDeclHead (k : SyntaxNodeKind) (id : Syntax) (isEmpty : Bool := false) :
-    CommandElabM Unit := do
-  if k == ``«abbrev» then lintDocStatusNamed isEmpty id "public abbrev"
-  else if k == ``definition then lintDocStatusNamed isEmpty id "public def"
-  else if k == ``«opaque» then lintDocStatusNamed isEmpty id "public opaque"
-  else if k == ``«axiom» then lintDocStatusNamed isEmpty id "public axiom"
-  else if k == ``«inductive» then lintDocStatusNamed isEmpty id "public inductive"
-  else if k == ``classInductive then lintDocStatusNamed isEmpty id "public inductive"
-  else if k == ``«structure» then lintDocStatusNamed isEmpty id "public structure"
-
-private def docOptStatus (docOpt attrs : Syntax) (checkTacticAlt := false) :
-    CommandElabM (Option Bool) := do
-  if hasInheritDoc attrs then return none
-  if checkTacticAlt && hasTacticAlt attrs then return none
-  if docOpt.isNone then return some false
-  if (← isEmptyDocString docOpt) then return some true
-  return none
+def lintDeclHead (k : SyntaxNodeKind) (id : Syntax) : CommandElabM Unit := do
+  if k == ``«abbrev» then lintNamed id "public abbrev"
+  else if k == ``definition then lintNamed id "public def"
+  else if k == ``«opaque» then lintNamed id "public opaque"
+  else if k == ``«axiom» then lintNamed id "public axiom"
+  else if k == ``«inductive» then lintNamed id "public inductive"
+  else if k == ``classInductive then lintNamed id "public inductive"
+  else if k == ``«structure» then lintNamed id "public structure"
 
 @[builtin_missing_docs_handler declaration]
 def checkDecl : SimpleHandler := fun stx => do
   let head := stx[0]; let rest := stx[1]
   if head[2][0].getKind == ``Command.private then return -- not private
   let k := rest.getKind
-  if let some isEmpty ← declModifiersDocStatus head then
-    lintDeclHead k rest[1][0] isEmpty
+  if (← declModifiersPubNoDoc head) then -- no doc string
+    lintDeclHead k rest[1][0]
   if k == ``«inductive» || k == ``classInductive then
     for stx in rest[4].getArgs do
       let head := stx[2]
-      -- Constructor has two doc comment positions: the leading one before `|` (stx[0])
-      -- and the one inside declModifiers (head[0]). If either is non-empty, skip.
-      let leadingEmpty ← isEmptyDocString stx[0]
-      if !stx[0].isNone && !leadingEmpty then
-        pure () -- constructor has a non-empty leading doc comment
-      else if let some modsEmpty ← declModifiersDocStatus head then
-        lintDocStatusField (leadingEmpty || modsEmpty) rest[1][0] stx[3] "public constructor"
+      if stx[0].isNone && (← declModifiersPubNoDoc head) then
+        lintField rest[1][0] stx[3] "public constructor"
     unless rest[5].isNone do
       for stx in rest[5][0][1].getArgs do
         let head := stx[0]
-        if let some isEmpty ← declModifiersDocStatus head then
-          lintDocStatusField isEmpty rest[1][0] stx[1] "computed field"
+        if (← declModifiersPubNoDoc head) then -- no doc string
+          lintField rest[1][0] stx[1] "computed field"
   else if rest.getKind == ``«structure» then
     unless rest[4][2].isNone do
       let redecls : Std.HashSet String.Pos.Raw :=
@@ -225,52 +173,45 @@ def checkDecl : SimpleHandler := fun stx => do
               else s
             else s
       let parent := rest[1][0]
-      let lint1 isEmpty stx := do
+      let lint1 stx := do
         if let some range := stx.getRange? then
           if redecls.contains range.start then return
-        lintDocStatusField isEmpty parent stx "public field"
+        lintField parent stx "public field"
       for stx in rest[4][2][0].getArgs do
         let head := stx[0]
-        if let some isEmpty ← declModifiersDocStatus head then
+        if (← declModifiersPubNoDoc head) then
           if stx.getKind == ``structSimpleBinder then
-            lint1 isEmpty stx[1]
+            lint1 stx[1]
           else
             for stx in stx[2].getArgs do
-              lint1 isEmpty stx
+              lint1 stx
 
 @[builtin_missing_docs_handler «initialize»]
 def checkInit : SimpleHandler := fun stx => do
-  if !stx[2].isNone then
-    if let some isEmpty ← declModifiersDocStatus stx[0] then
-      lintDocStatusNamed isEmpty stx[2][0] "initializer"
+  if !stx[2].isNone && (← declModifiersPubNoDoc stx[0]) then
+    lintNamed stx[2][0] "initializer"
 
 @[builtin_missing_docs_handler «notation»]
 def checkNotation : SimpleHandler := fun stx => do
-  if stx[2][0][0].getKind != ``«local» then
-    if let some isEmpty ← docOptStatus stx[0] stx[1] then
-      if stx[5].isNone then lintDocStatus isEmpty stx[3] "notation"
-      else lintDocStatusNamed isEmpty stx[5][0][3] "notation"
+  if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] then
+    if stx[5].isNone then lint stx[3] "notation"
+    else lintNamed stx[5][0][3] "notation"
 
 @[builtin_missing_docs_handler «mixfix»]
 def checkMixfix : SimpleHandler := fun stx => do
-  if stx[2][0][0].getKind != ``«local» then
-    if let some isEmpty ← docOptStatus stx[0] stx[1] then
-      if stx[5].isNone then lintDocStatus isEmpty stx[3] stx[3][0].getAtomVal
-      else lintDocStatusNamed isEmpty stx[5][0][3] stx[3][0].getAtomVal
+  if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] then
+    if stx[5].isNone then lint stx[3] stx[3][0].getAtomVal
+    else lintNamed stx[5][0][3] stx[3][0].getAtomVal
 
 @[builtin_missing_docs_handler «syntax»]
 def checkSyntax : SimpleHandler := fun stx => do
-  if stx[2][0][0].getKind != ``«local» then
-    if let some isEmpty ← docOptStatus stx[0] stx[1] (checkTacticAlt := true) then
-      if stx[5].isNone then lintDocStatus isEmpty stx[3] "syntax"
-      else lintDocStatusNamed isEmpty stx[5][0][3] "syntax"
+  if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] && !hasTacticAlt stx[1] then
+    if stx[5].isNone then lint stx[3] "syntax"
+    else lintNamed stx[5][0][3] "syntax"
 
 def mkSimpleHandler (name : String) (declNameStxIdx := 2) : SimpleHandler := fun stx => do
-  if (← isMissingDoc stx[0]) then
-    if (← isEmptyDocString stx[0]) then
-      lintEmptyNamed stx[declNameStxIdx] name
-    else
-      lintNamed stx[declNameStxIdx] name
+  if stx[0].isNone then
+    lintNamed stx[declNameStxIdx] name
 
 @[builtin_missing_docs_handler syntaxAbbrev]
 def checkSyntaxAbbrev : SimpleHandler := mkSimpleHandler "syntax"
@@ -280,22 +221,20 @@ def checkSyntaxCat : SimpleHandler := mkSimpleHandler "syntax category"
 
 @[builtin_missing_docs_handler «macro»]
 def checkMacro : SimpleHandler := fun stx => do
-  if stx[2][0][0].getKind != ``«local» then
-    if let some isEmpty ← docOptStatus stx[0] stx[1] (checkTacticAlt := true) then
-      if stx[5].isNone then lintDocStatus isEmpty stx[3] "macro"
-      else lintDocStatusNamed isEmpty stx[5][0][3] "macro"
+  if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] && !hasTacticAlt stx[1] then
+    if stx[5].isNone then lint stx[3] "macro"
+    else lintNamed stx[5][0][3] "macro"
 
 @[builtin_missing_docs_handler «elab»]
 def checkElab : SimpleHandler := fun stx => do
-  if stx[2][0][0].getKind != ``«local» then
-    if let some isEmpty ← docOptStatus stx[0] stx[1] (checkTacticAlt := true) then
-      if stx[5].isNone then lintDocStatus isEmpty stx[3] "elab"
-      else lintDocStatusNamed isEmpty stx[5][0][3] "elab"
+  if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] && !hasTacticAlt stx[1] then
+    if stx[5].isNone then lint stx[3] "elab"
+    else lintNamed stx[5][0][3] "elab"
 
 @[builtin_missing_docs_handler classAbbrev]
 def checkClassAbbrev : SimpleHandler := fun stx => do
-  if let some isEmpty ← declModifiersDocStatus stx[0] then
-    lintDocStatusNamed isEmpty stx[3] "class abbrev"
+  if (← declModifiersPubNoDoc stx[0]) then
+    lintNamed stx[3] "class abbrev"
 
 @[builtin_missing_docs_handler Parser.Tactic.declareSimpLikeTactic]
 def checkSimpLike : SimpleHandler := mkSimpleHandler "simp-like tactic"
@@ -305,8 +244,8 @@ def checkRegisterBuiltinOption : SimpleHandler := mkSimpleHandler (declNameStxId
 
 @[builtin_missing_docs_handler Option.registerOption]
 def checkRegisterOption : SimpleHandler := fun stx => do
-  if let some isEmpty ← declModifiersDocStatus stx[0] then
-    lintDocStatusNamed isEmpty stx[2] "option"
+  if (← declModifiersPubNoDoc stx[0]) then
+    lintNamed stx[2] "option"
 
 @[builtin_missing_docs_handler registerSimpAttr]
 def checkRegisterSimpAttr : SimpleHandler := mkSimpleHandler "simp attr"

src/Lean/Message.lean

@@ -244,7 +244,7 @@ def ofLevel (l : Level) : MessageData :=
   .ofLazy
     (fun ctx? => do
       let msg ← ofFormat <$> match ctx? with
-        | .none => pure (l.format true (fun _ => none))
+        | .none => pure (format l)
         | .some ctx => ppLevel ctx l
       return Dynamic.mk msg)
     (fun _ => false)

src/Lean/Meta.lean

@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Basic
-public import Lean.Meta.HasAssignableMVar
 public import Lean.Meta.LevelDefEq
 public import Lean.Meta.WHNF
 public import Lean.Meta.InferType

src/Lean/Meta/AbstractNestedProofs.lean

@@ -70,7 +70,6 @@ structure Context where
 abbrev M := ReaderT Context $ MonadCacheT ExprStructEq Expr MetaM
 
 partial def visit (e : Expr) : M Expr := do
-  checkSystem "abstract nested proofs"
   if e.isAtomic then
     pure e
   else

src/Lean/Meta/AppBuilder.lean

@@ -8,7 +8,6 @@ prelude
 public import Lean.Meta.SynthInstance
 public import Lean.Meta.DecLevel
 import Lean.Meta.CtorRecognizer
-public import Lean.Meta.HasAssignableMVar
 import Lean.Structure
 import Init.Omega
 public section

src/Lean/Meta/HasAssignableMVar.lean

@@ -1,54 +0,0 @@
-/-
-Copyright (c) 2019 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-
-prelude
-public import Lean.Meta.Basic
-
-public section
-
-open Lean
-
-namespace Lean.Meta
-
-def hasAssignableLevelMVar : Level → MetaM Bool
-  | .succ lvl       => pure lvl.hasMVar <&&> hasAssignableLevelMVar lvl
-  | .max lvl₁ lvl₂  => (pure lvl₁.hasMVar <&&> hasAssignableLevelMVar lvl₁) <||> (pure lvl₂.hasMVar <&&> hasAssignableLevelMVar lvl₂)
-  | .imax lvl₁ lvl₂ => (pure lvl₁.hasMVar <&&> hasAssignableLevelMVar lvl₁) <||> (pure lvl₂.hasMVar <&&> hasAssignableLevelMVar lvl₂)
-  | .mvar mvarId    => isLevelMVarAssignable mvarId
-  | .zero           => return false
-  | .param _        => return false
-
-/-- Return `true` iff expression contains a metavariable that can be assigned. -/
-partial def hasAssignableMVar (e : Expr) : MetaM Bool :=
-  if !e.hasMVar then
-    return false
-  else
-    go e |>.run' {}
-where
-  go (e : Expr) : StateRefT ExprSet MetaM Bool :=
-    match e with
-    | .const _ lvls    => lvls.anyM (liftM <| hasAssignableLevelMVar ·)
-    | .sort lvl        => liftM <| hasAssignableLevelMVar lvl
-    | .app f a         => do checkSystem "hasAssignableMVar"; visit f <||> visit a
-    | .letE _ t v b _  => do checkSystem "hasAssignableMVar"; visit t <||> visit v <||> visit b
-    | .forallE _ d b _ => do checkSystem "hasAssignableMVar"; visit d <||> visit b
-    | .lam _ d b _     => do checkSystem "hasAssignableMVar"; visit d <||> visit b
-    | .fvar _          => return false
-    | .bvar _          => return false
-    | .lit _           => return false
-    | .mdata _ e       => visit e
-    | .proj _ _ e      => visit e
-    | .mvar mvarId     => mvarId.isAssignable
-  visit (e : Expr) : StateRefT ExprSet MetaM Bool := do
-    if !e.hasMVar then return false
-    if (← get).contains e then return false
-    modify fun s => s.insert e
-    go e
-
-end Lean.Meta
-
-end

src/Lean/Meta/LevelDefEq.lean

@@ -8,7 +8,6 @@ module
 prelude
 public import Lean.Util.CollectMVars
 public import Lean.Meta.DecLevel
-public import Lean.Meta.HasAssignableMVar
 
 public section
 

src/Lean/Meta/Sym/Pattern.lean

@@ -18,7 +18,6 @@ import Lean.Meta.Sym.AlphaShareBuilder
 import Lean.Meta.Sym.Offset
 import Lean.Meta.Sym.Eta
 import Lean.Meta.Sym.Util
-import Lean.Meta.HasAssignableMVar
 import Init.Data.List.MapIdx
 import Init.Data.Nat.Linear
 import Std.Do.Triple.Basic

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

@@ -14,7 +14,6 @@ import Lean.Meta.Tactic.Grind.SynthInstance
 import Lean.Meta.Tactic.Grind.Simp
 import Init.Grind.Util
 import Init.Omega
-public import Lean.Meta.HasAssignableMVar
 public section
 namespace Lean.Meta.Grind
 namespace EMatch

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

@@ -714,6 +714,7 @@ where
 set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_simp]
 def simpImpl (e : Expr) : SimpM Result := withIncRecDepth do
+  checkSystem "simp"
   if (← isProof e) then
     return { expr := e }
   trace[Meta.Tactic.simp.heads] "{repr e.toHeadIndex}"

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

@@ -12,7 +12,6 @@ public import Lean.Meta.Tactic.Simp.Arith
 public import Lean.Meta.Tactic.Simp.Attr
 public import Lean.Meta.BinderNameHint
 import Lean.Meta.WHNF
-public import Lean.Meta.HasAssignableMVar
 public section
 namespace Lean.Meta.Simp
 /--
@@ -100,7 +99,7 @@ where
       if (← withReducibleAndInstances <| isDefEq x val) then
         return true
       else
-        trace[Meta.Tactic.simp.discharge] "{← ppOrigin thmId}, failed to assign instance{indentExpr type}\nsynthesized value{indentExpr val}\nis not definitionally equal to{indentExpr x}"
+        trace[Meta.Tactic.simp.discharge] "{← ppOrigin thmId}, failed to assign instance{indentExpr type}\nsythesized value{indentExpr val}\nis not definitionally equal to{indentExpr x}"
         return false
     | _ =>
       trace[Meta.Tactic.simp.discharge] "{← ppOrigin thmId}, failed to synthesize instance{indentExpr type}"
@@ -219,7 +218,6 @@ where
     else
       let candidates := candidates.insertionSort fun e₁ e₂ => e₁.1.priority > e₂.1.priority
       for (thm, numExtraArgs) in candidates do
-        checkSystem "simp"
         if inErasedSet thm then continue
         if rflOnly then
           unless thm.rfl do
@@ -247,7 +245,6 @@ where
     else
       let candidates := candidates.insertionSort fun e₁ e₂ => e₁.priority > e₂.priority
       for thm in candidates do
-        checkSystem "simp"
         unless inErasedSet thm || (rflOnly && !thm.rfl) do
           let result? ← withNewMCtxDepth do
             let val  ← thm.getValue

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

@@ -722,7 +722,6 @@ def simpAppUsingCongr (e : Expr) : SimpM Result := do
     if i == 0 then
       simp f
     else
-      checkSystem "simp"
       let i := i - 1
       let .app f a := e | unreachable!
       let fr ← visit f i

src/Lean/Meta/Transform.lean

@@ -50,7 +50,6 @@ partial def transform {m} [Monad m] [MonadLiftT CoreM m] [MonadControlT CoreM m]
   let _ : MonadLiftT (ST IO.RealWorld) m := { monadLift := fun x => liftM (m := CoreM) (liftM (m := ST IO.RealWorld) x) }
   let rec visit (e : Expr) : MonadCacheT ExprStructEq Expr m Expr :=
     checkCache { val := e : ExprStructEq } fun _ => Core.withIncRecDepth do
-      Core.checkSystem "transform"
       let rec visitPost (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := do
         match (← post e) with
         | .done e      => pure e
@@ -108,7 +107,6 @@ partial def transformWithCache {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT
   let _ : MonadLiftT (ST IO.RealWorld) m := { monadLift := fun x => liftM (m := MetaM) (liftM (m := ST IO.RealWorld) x) }
   let rec visit (e : Expr) : MonadCacheT ExprStructEq Expr m Expr :=
     checkCache { val := e : ExprStructEq } fun _ => Meta.withIncRecDepth do
-      (Core.checkSystem "transform" : MetaM Unit)
       let rec visitPost (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := do
         match (← post e) with
         | .done e      => pure e

src/Lean/Meta/WHNF.lean

@@ -650,7 +650,7 @@ expand let-expressions, expand assigned meta-variables, unfold aux declarations.
 partial def whnfCore (e : Expr) : MetaM Expr :=
   go e
 where
-  go (e : Expr) : MetaM Expr := do
+  go (e : Expr) : MetaM Expr :=
     whnfEasyCases e fun e => do
       trace[Meta.whnf] e
       match e with

src/Lean/MetavarContext.lean

@@ -247,18 +247,6 @@ very simple unification and/or non-nested TC. So, if the "app builder" becomes a
 we may solve the issue by implementing `isDefEqCheap` that never invokes TC and uses tmp metavars.
 -/
 
-structure LevelMetavarDecl where
-  /-- The nesting depth of this metavariable. We do not want
-  unification subproblems to influence the results of parent
-  problems. The depth keeps track of this information and ensures
-  that unification subproblems cannot leak information out, by unifying
-  based on depth. -/
-  depth : Nat
-  /-- This field tracks how old a metavariable is. It is set using a counter at `MetavarContext`.
-  We primarily use the index of a level metavariable for pretty printing. -/
-  index : Nat
-  deriving Inhabited
-
 /--
 `LocalInstance` represents a local typeclass instance registered by and for
 the elaborator. It stores the name of the typeclass in `className`, and the
@@ -321,8 +309,7 @@ structure MetavarDecl where
   kind           : MetavarKind
   /-- See comment at `CheckAssignment` `Meta/ExprDefEq.lean` -/
   numScopeArgs   : Nat := 0
-  /-- We use this field to track how old a metavariable is. It is set using a counter at `MetavarContext`.
-  We also use it for pretty printing anonymous metavariables. -/
+  /-- We use this field to track how old a metavariable is. It is set using a counter at `MetavarContext` -/
   index          : Nat
   deriving Inhabited
 
@@ -353,12 +340,9 @@ structure MetavarContext where
   depth          : Nat := 0
   /-- At what depth level mvars can be assigned. -/
   levelAssignDepth : Nat := 0
-  /-- Counter for setting the field `index` at `LevelMetavarDecl`. -/
-  lmvarCounter   : Nat := 0
   /-- Counter for setting the field `index` at `MetavarDecl` -/
   mvarCounter    : Nat := 0
-  /-- Level metavariable declarations. -/
-  lDecls         : PersistentHashMap LMVarId LevelMetavarDecl := {}
+  lDepth         : PersistentHashMap LMVarId Nat := {}
   /-- Metavariable declarations. -/
   decls          : PersistentHashMap MVarId MetavarDecl := {}
   /-- Index mapping user-friendly names to ids. -/
@@ -460,21 +444,11 @@ def _root_.Lean.MVarId.isAssignedOrDelayedAssigned [Monad m] [MonadMCtx m] (mvar
   let mctx ← getMCtx
   return mctx.eAssignment.contains mvarId || mctx.dAssignment.contains mvarId
 
-def MetavarContext.findLevelDecl? (mctx : MetavarContext) (mvarId : LMVarId) : Option LevelMetavarDecl :=
-  mctx.lDecls.find? mvarId
-
-def MetavarContext.getLevelDecl (mctx : MetavarContext) (mvarId : LMVarId) : LevelMetavarDecl :=
-  match mctx.lDecls.find? mvarId with
-  | some decl => decl
-  | none      => panic! s!"unknown universe metavariable {mvarId.name}"
-
 def isLevelMVarAssignable [Monad m] [MonadMCtx m] (mvarId : LMVarId) : m Bool := do
   let mctx ← getMCtx
-  let decl := mctx.getLevelDecl mvarId
-  return decl.depth >= mctx.levelAssignDepth
-
-def MetavarContext.findDecl? (mctx : MetavarContext) (mvarId : MVarId) : Option MetavarDecl :=
-  mctx.decls.find? mvarId
+  match mctx.lDepth.find? mvarId with
+  | some d => return d >= mctx.levelAssignDepth
+  | _      => panic! s!"unknown universe metavariable {mvarId.name}"
 
 def MetavarContext.getDecl (mctx : MetavarContext) (mvarId : MVarId) : MetavarDecl :=
   match mctx.decls.find? mvarId with
@@ -510,6 +484,30 @@ def hasAssignedMVar [Monad m] [MonadMCtx m] : Expr → m Bool
   | .proj _ _ e      => pure e.hasMVar <&&> hasAssignedMVar e
   | .mvar mvarId     => mvarId.isAssigned <||> mvarId.isDelayedAssigned
 
+/-- Return true iff the given level contains a metavariable that can be assigned. -/
+def hasAssignableLevelMVar [Monad m] [MonadMCtx m] : Level → m Bool
+  | .succ lvl       => pure lvl.hasMVar <&&> hasAssignableLevelMVar lvl
+  | .max lvl₁ lvl₂  => (pure lvl₁.hasMVar <&&> hasAssignableLevelMVar lvl₁) <||> (pure lvl₂.hasMVar <&&> hasAssignableLevelMVar lvl₂)
+  | .imax lvl₁ lvl₂ => (pure lvl₁.hasMVar <&&> hasAssignableLevelMVar lvl₁) <||> (pure lvl₂.hasMVar <&&> hasAssignableLevelMVar lvl₂)
+  | .mvar mvarId    => isLevelMVarAssignable mvarId
+  | .zero           => return false
+  | .param _        => return false
+
+/-- Return `true` iff expression contains a metavariable that can be assigned. -/
+def hasAssignableMVar [Monad m] [MonadMCtx m] : Expr → m Bool
+  | .const _ lvls    => lvls.anyM hasAssignableLevelMVar
+  | .sort lvl        => hasAssignableLevelMVar lvl
+  | .app f a         => (pure f.hasMVar <&&> hasAssignableMVar f) <||> (pure a.hasMVar <&&> hasAssignableMVar a)
+  | .letE _ t v b _  => (pure t.hasMVar <&&> hasAssignableMVar t) <||> (pure v.hasMVar <&&> hasAssignableMVar v) <||> (pure b.hasMVar <&&> hasAssignableMVar b)
+  | .forallE _ d b _ => (pure d.hasMVar <&&> hasAssignableMVar d) <||> (pure b.hasMVar <&&> hasAssignableMVar b)
+  | .lam _ d b _     => (pure d.hasMVar <&&> hasAssignableMVar d) <||> (pure b.hasMVar <&&> hasAssignableMVar b)
+  | .fvar _          => return false
+  | .bvar _          => return false
+  | .lit _           => return false
+  | .mdata _ e       => pure e.hasMVar <&&> hasAssignableMVar e
+  | .proj _ _ e      => pure e.hasMVar <&&> hasAssignableMVar e
+  | .mvar mvarId     => mvarId.isAssignable
+
 /--
   Add `mvarId := u` to the universe metavariable assignment.
   This method does not check whether `mvarId` is already assigned, nor does it check whether
@@ -828,11 +826,10 @@ def addExprMVarDeclExp (mctx : MetavarContext) (mvarId : MVarId) (userName : Nam
    It is used to implement actions in the monads `MetaM`, `ElabM` and `TacticM`.
    It should not be used directly since the argument `(mvarId : MVarId)` is assumed to be "unique". -/
 def addLevelMVarDecl (mctx : MetavarContext) (mvarId : LMVarId) : MetavarContext :=
-  { mctx with
-    lmvarCounter := mctx.lmvarCounter + 1
-    lDecls := mctx.lDecls.insert mvarId {
-      depth := mctx.depth
-      index := mctx.lmvarCounter } }
+  { mctx with lDepth := mctx.lDepth.insert mvarId mctx.depth }
+
+def findDecl? (mctx : MetavarContext) (mvarId : MVarId) : Option MetavarDecl :=
+  mctx.decls.find? mvarId
 
 def findUserName? (mctx : MetavarContext) (userName : Name) : Option MVarId :=
   mctx.userNames.find? userName
@@ -912,13 +909,12 @@ def setFVarBinderInfo (mctx : MetavarContext) (mvarId : MVarId)
   mctx.modifyExprMVarLCtx mvarId (·.setBinderInfo fvarId bi)
 
 def findLevelDepth? (mctx : MetavarContext) (mvarId : LMVarId) : Option Nat :=
-  (mctx.findLevelDecl? mvarId).map LevelMetavarDecl.depth
+  mctx.lDepth.find? mvarId
 
 def getLevelDepth (mctx : MetavarContext) (mvarId : LMVarId) : Nat :=
-  (mctx.getLevelDecl mvarId).depth
-
-def findLevelIndex? (mctx : MetavarContext) (mvarId : LMVarId) : Option Nat :=
-  (mctx.findLevelDecl? mvarId).map LevelMetavarDecl.index
+  match mctx.findLevelDepth? mvarId with
+  | some d => d
+  | none   => panic! "unknown metavariable"
 
 def isAnonymousMVar (mctx : MetavarContext) (mvarId : MVarId) : Bool :=
   match mctx.findDecl? mvarId with

src/Lean/Parser/Command.lean

@@ -622,15 +622,6 @@ declaration signatures.
 /-- Debugging command: Prints the result of `Environment.dumpAsyncEnvState`. -/
 @[builtin_command_parser] def dumpAsyncEnvState := leading_parser
   "#dump_async_env_state"
-/--
-Mark a syntax kind as deprecated. When this syntax is elaborated, a warning will be emitted.
-
-```
-deprecated_syntax Lean.Parser.Term.let_fun "use `have` instead" (since := "2026-03-18")
-```
--/
-@[builtin_command_parser] def deprecatedSyntax := leading_parser
-  "deprecated_syntax " >> ident >> optional (ppSpace >> strLit) >> optional (" (" >> nonReservedSymbol "since" >> " := " >> strLit >> ")")
 @[builtin_command_parser] def «init_quot»    := leading_parser
   "init_quot"
 /--
@@ -638,27 +629,6 @@ An internal bootstrapping command that reinterprets a Markdown docstring as Vers
 -/
 @[builtin_command_parser] def «docs_to_verso»    := leading_parser
   "docs_to_verso " >> sepBy1 ident ", "
-/--
-`deprecated_module` marks the current module as deprecated.
-When another module imports a deprecated module, a warning is emitted during elaboration.
-
-```
-deprecated_module "use NewModule instead" (since := "2026-03-19")
-```
-
-The warning message is optional but recommended.
-The warning can be disabled with `set_option linter.deprecated.module false` or
-`-Dlinter.deprecated.module=false`.
--/
-@[builtin_command_parser] def «deprecated_module» := leading_parser
-  "deprecated_module" >> optional (ppSpace >> strLit) >> optional (" (" >> nonReservedSymbol "since" >> " := " >> strLit >> ")")
-
-/--
-`#show_deprecated_modules` displays all modules in the current environment that have been
-marked with `deprecated_module`.
--/
-@[builtin_command_parser] def showDeprecatedModules := leading_parser
-  "#show_deprecated_modules"
 
 def optionValue := nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> strLit <|> numLit
 /--
@@ -678,12 +648,6 @@ only in a single term or tactic.
 -/
 @[builtin_command_parser] def «set_option»   := leading_parser
   "set_option " >> identWithPartialTrailingDot >> ppSpace >> optionValue
-/--
-`unlock_limits` disables all built-in resource limit options (currently `maxRecDepth`,
-`maxHeartbeats`, and `synthInstance.maxHeartbeats`) in the current scope by setting them to 0.
--/
-@[builtin_command_parser] def «unlock_limits» := leading_parser
-  "unlock_limits"
 def eraseAttr := leading_parser
   "-" >> rawIdent
 @[builtin_command_parser] def «attribute»    := leading_parser

src/Lean/Parser/Term.lean

@@ -882,19 +882,13 @@ the available context).
 -/
 def identProjKind := `Lean.Parser.Term.identProj
 
-@[builtin_term_parser] def dotIdent := leading_parser
-  "." >> checkNoWsBefore >> rawIdent
-
 def isIdent (stx : Syntax) : Bool :=
   -- antiquotations should also be allowed where an identifier is expected
   stx.isAntiquot || stx.isIdent
 
-def isIdentOrDotIdent (stx : Syntax) : Bool :=
-  isIdent stx || stx.isOfKind ``dotIdent
-
 /-- `x.{u, ...}` explicitly specifies the universes `u, ...` of the constant `x`. -/
 @[builtin_term_parser] def explicitUniv : TrailingParser := trailing_parser
-  checkStackTop isIdentOrDotIdent "expected preceding identifier" >>
+  checkStackTop isIdent "expected preceding identifier" >>
   checkNoWsBefore "no space before '.{'" >> ".{" >>
   sepBy1 levelParser ", " >> "}"
 /-- `x@e` or `x@h:e` matches the pattern `e` and binds its value to the identifier `x`.
@@ -982,6 +976,9 @@ appropriate parameter for the underlying monad's `ST` effects, then passes it to
 @[builtin_term_parser] def dynamicQuot := withoutPosition <| leading_parser
   "`(" >> ident >> "| " >> incQuotDepth (parserOfStack 1) >> ")"
 
+@[builtin_term_parser] def dotIdent := leading_parser
+  "." >> checkNoWsBefore >> rawIdent
+
 /--
 Implementation of the `show_term` term elaborator.
 -/

src/Lean/Parser/Types.lean

@@ -469,7 +469,6 @@ def seq : FirstTokens → FirstTokens → FirstTokens
   | epsilon,      tks          => tks
   | optTokens s₁, optTokens s₂ => optTokens (s₁ ++ s₂)
   | optTokens s₁, tokens s₂    => tokens (s₁ ++ s₂)
-  | optTokens _,  unknown      => unknown
   | tks,          _            => tks
 
 def toOptional : FirstTokens → FirstTokens

src/Lean/PrettyPrinter.lean

@@ -70,9 +70,6 @@ def ppExprLegacy (env : Environment) (mctx : MetavarContext) (lctx : LocalContex
     { fileName := "<PrettyPrinter>", fileMap := default }
     { env := env }
 
-def ppLevel (l : Level) : MetaM Format := do
-  ppCategory `level (← delabLevel l (prec := 0))
-
 def ppTactic (stx : TSyntax `tactic) : CoreM Format := ppCategory `tactic stx
 
 def ppCommand (stx : Syntax.Command) : CoreM Format := ppCategory `command stx
@@ -113,7 +110,7 @@ builtin_initialize
     ppExprWithInfos := fun ctx e => ctx.runMetaM <| withoutContext <| ppExprWithInfos e
     ppConstNameWithInfos := fun ctx n => ctx.runMetaM <| withoutContext <| ppConstNameWithInfos n
     ppTerm := fun ctx stx => ctx.runCoreM <| withoutContext <| ppTerm stx
-    ppLevel := fun ctx l => ctx.runMetaM <| withoutContext <| ppLevel l
+    ppLevel := fun ctx l => return l.format (mvars := getPPMVarsLevels ctx.opts)
     ppGoal := fun ctx mvarId => ctx.runMetaM <| withoutContext <| Meta.ppGoal mvarId
   }
 

src/Lean/PrettyPrinter/Delaborator/Basic.lean

@@ -450,10 +450,6 @@ partial def delab : Delab := do
   else
     return stx
 
-def delabLevel (l : Level) (prec : Nat) : DelabM Syntax.Level := do
-  let mvars ← getPPOption getPPMVarsLevels
-  return Level.quote l prec (mvars := mvars) (lIndex? := (← getMCtx).findLevelIndex?)
-
 /--
 Registers an unexpander for applications of a given constant.
 
@@ -481,11 +477,7 @@ unsafe builtin_initialize appUnexpanderAttribute : KeyedDeclsAttribute Unexpande
 end Delaborator
 
 open SubExpr (Pos PosMap)
-open Delaborator (OptionsPerPos topDownAnalyze DelabM getPPOption)
-
-def delabLevel (l : Level) (prec : Nat) : MetaM Syntax.Level := do
-  let mvars := getPPMVarsLevels (← getOptions)
-  return Level.quote l prec (mvars := mvars) (lIndex? := (← getMCtx).findLevelIndex?)
+open Delaborator (OptionsPerPos topDownAnalyze DelabM)
 
 def delabCore (e : Expr) (optionsPerPos : OptionsPerPos := {}) (delab : DelabM α) :
     MetaM (α × PosMap Elab.Info) := do

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -91,9 +91,10 @@ def delabSort : Delab := do
   | Level.zero => `(Prop)
   | Level.succ .zero => `(Type)
   | _ =>
+    let mvars ← getPPOption getPPMVarsLevels
     match l.dec with
-    | some l' => `(Type $(← delabLevel l' (prec := max_prec)))
-    | none    => `(Sort $(← delabLevel l (prec := max_prec)))
+    | some l' => `(Type $(Level.quote l' (prec := max_prec) (mvars := mvars)))
+    | none    => `(Sort $(Level.quote l (prec := max_prec) (mvars := mvars)))
 
 /--
 Delaborator for `const` expressions.
@@ -130,8 +131,8 @@ def delabConst : Delab := do
 
   let stx ←
     if !ls.isEmpty && (← getPPOption getPPUniverses) then
-      let ls' ← ls.toArray.mapM fun l => delabLevel l (prec := 0)
-      `($(mkIdent c).{$ls',*})
+      let mvars ← getPPOption getPPMVarsLevels
+      `($(mkIdent c).{$[$(ls.toArray.map (Level.quote · (prec := 0) (mvars := mvars)))],*})
     else
       pure <| mkIdent c
 

src/Lean/Runtime.lean

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

src/Lean/Server/FileWorker/SemanticHighlighting.lean

@@ -46,7 +46,7 @@ structure LeanSemanticToken where
   stx  : Syntax
   /-- Type of the semantic token. -/
   type : SemanticTokenType
-  /-- In case of overlap, higher-priority tokens will take precedence -/
+  /-- In case of overlap, higher-priority tokens will take precendence -/
   priority : Nat := 5
 
 /-- Semantic token information with absolute LSP positions. -/
@@ -57,7 +57,7 @@ structure AbsoluteLspSemanticToken where
   tailPos : Lsp.Position
   /-- Start position of the semantic token. -/
   type    : SemanticTokenType
-  /-- In case of overlap, higher-priority tokens will take precedence -/
+  /-- In case of overlap, higher-priority tokens will take precendence -/
   priority : Nat := 5
   deriving BEq, Hashable, FromJson, ToJson
 

src/Lean/Util/PPExt.lean

@@ -52,7 +52,7 @@ structure PPFns where
   ppExprWithInfos : PPContext → Expr → IO FormatWithInfos
   ppConstNameWithInfos : PPContext → Name → IO FormatWithInfos
   ppTerm : PPContext → Term → IO Format
-  ppLevel : PPContext → Level → IO Format
+  ppLevel : PPContext → Level → BaseIO Format
   ppGoal : PPContext → MVarId → IO Format
   deriving Inhabited
 
@@ -67,7 +67,7 @@ builtin_initialize ppFnsRef : IO.Ref PPFns ←
     ppExprWithInfos := fun _ e => return format (toString e)
     ppConstNameWithInfos := fun _ n => return format n
     ppTerm := fun ctx stx => return formatRawTerm ctx stx
-    ppLevel := fun ctx l => return l.format true ctx.mctx.findLevelIndex?
+    ppLevel := fun _ l => return format l
     ppGoal := fun _ mvarId => return formatRawGoal mvarId
   }
 
@@ -108,14 +108,8 @@ def ppTerm (ctx : PPContext) (stx : Term) : BaseIO Format := do
       else
         pure f!"failed to pretty print term (use 'set_option pp.rawOnError true' for raw representation)"
 
-def ppLevel (ctx : PPContext) (l : Level) : BaseIO Format := do
-  match (← ppExt.getState ctx.env |>.ppLevel ctx l |>.toBaseIO) with
-  | .ok fmt => return fmt
-  | .error ex =>
-    if pp.rawOnError.get ctx.opts then
-      pure f!"[Error pretty printing level: {ex}. Falling back to raw printer.]{Format.line}{l.format true ctx.mctx.findLevelIndex?}"
-    else
-      pure f!"failed to pretty print level (use 'set_option pp.rawOnError true' for raw representation)"
+def ppLevel (ctx : PPContext) (l : Level) : BaseIO Format :=
+  ppExt.getState ctx.env |>.ppLevel ctx l
 
 def ppGoal (ctx : PPContext) (mvarId : MVarId) : BaseIO Format := do
   match (← ppExt.getState ctx.env |>.ppGoal ctx mvarId |>.toBaseIO) with

src/Lean/Util/RecDepth.lean

@@ -14,7 +14,7 @@ namespace Lean
 
 register_builtin_option maxRecDepth : Nat := {
   defValue := defaultMaxRecDepth
-  descr    := "maximum recursion depth for many Lean procedures, 0 means no limit"
+  descr    := "maximum recursion depth for many Lean procedures"
 }
 
 end Lean

src/Std/Data/String/ToInt.lean

@@ -183,8 +183,7 @@ public theorem toInt?_repr (a : Int) : a.repr.toInt? = some a := by
   rw [repr_eq_if]
   split <;> (simp; omega)
 
-@[simp]
-public theorem isInt_repr (a : Int) : a.repr.isInt = true := by
+public theorem isInt?_repr (a : Int) : a.repr.isInt = true := by
   simp [← String.isSome_toInt?]
 
 public theorem repr_injective {a b : Int} (h : Int.repr a = Int.repr b) : a = b := by

src/Std/Internal.lean

@@ -10,6 +10,7 @@ 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,6 +10,7 @@ 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
@@ -17,3 +18,4 @@ 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.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Std.Time
 public import Std.Internal.UV.TCP
+public import Std.Internal.Async.IO
 public import Std.Internal.Async.Select
 
 public section

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

@@ -0,0 +1,442 @@
+/-
+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
+  let want ← ssl.handshake
+  flushEncrypted native ssl
+  match want with
+  | none =>
+    return ()
+  | some .write =>
+    doHandshake native ssl chunkSize
+  | some .read =>
+    let encrypted? ← Async.ofPromise <| native.recv? chunkSize
+    match encrypted? with
+    | none =>
+      throw <| IO.userError "connection closed during TLS handshake"
+    | some encrypted =>
+      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
+
+/--
+Creates a `Selector` that resolves once `s` has a connection available and the TLS handshake
+has completed.
+-/
+def acceptSelector (s : Server) : Selector ServerConn :=
+  {
+    tryFn := do
+      let res ← s.native.tryAccept
+      match ← IO.ofExcept res with
+      | none => return none
+      | some native =>
+        let conn ← mkServerConn native s.serverCtx
+        doHandshake conn.native conn.ssl ioChunkSize
+        return some conn
+
+    registerFn waiter := do
+      let connTask ← (do
+        let native ← Async.ofPromise <| s.native.accept
+        let ssl ← Session.Server.mk s.serverCtx
+        let conn : ServerConn := ⟨native, ssl⟩
+        doHandshake conn.native conn.ssl ioChunkSize
+        return conn
+      ).asTask
+
+      -- If we get cancelled the promise will be dropped so prepare for that
+      discard <| IO.mapTask (t := connTask) fun res => do
+        let lose := return ()
+        let win promise := do
+          try
+            let conn ← IO.ofExcept res
+            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
+
+/--
+Disables 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
+
+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
+  match ← s.ssl.write data with
+  | none =>
+    flushEncrypted s.native s.ssl
+    return true
+  | some _ =>
+    -- Data was queued internally; flush whatever the SSL engine produced.
+    flushEncrypted s.native s.ssl
+    return false
+
+/--
+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 performs the required socket I/O
+(flush or receive) and retries until data arrives or the connection is closed.
+-/
+partial def recv? {r : Role} (s : Connection r) (size : UInt64) (chunkSize : UInt64 := ioChunkSize) : Async (Option ByteArray) := do
+  match ← s.ssl.read? size with
+  | .data plain =>
+    flushEncrypted s.native s.ssl
+    return some plain
+  | .closed =>
+    return none
+  | .wantIO _ =>
+    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) : Async Unit := do
+  flushEncrypted s.native s.ssl
+
+  let pending ← s.ssl.pendingPlaintext
+  if pending > 0 then
+    return ()
+
+  if (← s.ssl.pendingPlaintext) > 0 then
+    return ()
+
+  match ← s.ssl.read? 0 with
+  | .data _ =>
+    flushEncrypted s.native s.ssl
+    return ()
+  | .closed =>
+    return ()
+  | .wantIO _ =>
+    flushEncrypted s.native s.ssl
+    let encrypted? ← Async.ofPromise <| s.native.recv? ioChunkSize
+    match encrypted? with
+    | none => return ()
+    | some encrypted =>
+      feedEncryptedChunk s.ssl encrypted
+      waitReadable s
+
+/--
+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
+
+/--
+Disables 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/Http/Data.lean

@@ -14,7 +14,6 @@ public import Std.Internal.Http.Data.Status
 public import Std.Internal.Http.Data.Chunk
 public import Std.Internal.Http.Data.Headers
 public import Std.Internal.Http.Data.URI
-public import Std.Internal.Http.Data.Body
 
 /-!
 # HTTP Data Types

src/Std/Internal/Http/Data/Body.lean

@@ -1,24 +0,0 @@
-/-
-Copyright (c) 2025 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.Internal.Http.Data.Body.Basic
-public import Std.Internal.Http.Data.Body.Length
-public import Std.Internal.Http.Data.Body.Any
-public import Std.Internal.Http.Data.Body.Stream
-public import Std.Internal.Http.Data.Body.Empty
-public import Std.Internal.Http.Data.Body.Full
-
-public section
-
-/-!
-# Body
-
-This module re-exports all HTTP body types: `Body.Empty`, `Body.Full`, `Body.Stream`,
-`Body.Any`, and `Body.Length`, along with the `Http.Body` typeclass and conversion
-utilities (`ToByteArray`, `FromByteArray`).
--/

src/Std/Internal/Http/Data/Body/Any.lean

@@ -1,83 +0,0 @@
-/-
-Copyright (c) 2025 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.Internal.Http.Data.Body.Basic
-
-public section
-
-/-!
-# Body.Any
-
-A type-erased body backed by closures. Implements `Http.Body` and can be constructed from any
-type that also implements `Http.Body`. Used as the default handler response body type.
--/
-
-namespace Std.Http.Body
-open Std Internal IO Async
-
-set_option linter.all true
-
-/--
-A type-erased body handle. Operations are stored as closures, making it open to any body type
-that implements `Http.Body`.
--/
-structure Any where
-
-  /--
-  Receives the next body chunk. Returns `none` at end-of-stream.
-  -/
-  recv : Async (Option Chunk)
-
-  /--
-  Closes the body stream.
-  -/
-  close : Async Unit
-
-  /--
-  Returns `true` when the body stream is closed.
-  -/
-  isClosed : Async Bool
-
-  /--
-  Selector that resolves when a chunk is available or EOF is reached.
-  -/
-  recvSelector : Selector (Option Chunk)
-
-  /--
-  Returns the declared size.
-  -/
-  getKnownSize : Async (Option Body.Length)
-
-  /--
-  Sets the size of the body.
-  -/
-  setKnownSize : Option Body.Length → Async Unit
-namespace Any
-
-/--
-Erases a body of any `Http.Body` instance into a `Body.Any`.
--/
-def ofBody [Http.Body α] (body : α) : Any where
-  recv := Http.Body.recv body
-  close := Http.Body.close body
-  isClosed := Http.Body.isClosed body
-  recvSelector := Http.Body.recvSelector body
-  getKnownSize := Http.Body.getKnownSize body
-  setKnownSize := Http.Body.setKnownSize body
-
-end Any
-
-instance : Http.Body Any where
-  recv := Any.recv
-  close := Any.close
-  isClosed := Any.isClosed
-  recvSelector := Any.recvSelector
-  getKnownSize := Any.getKnownSize
-  setKnownSize := Any.setKnownSize
-
-end Std.Http.Body

src/Std/Internal/Http/Data/Body/Basic.lean

@@ -1,102 +0,0 @@
-/-
-Copyright (c) 2025 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.Internal.Async
-public import Std.Internal.Async.ContextAsync
-public import Std.Internal.Http.Data.Chunk
-public import Std.Internal.Http.Data.Headers
-public import Std.Internal.Http.Data.Body.Length
-
-public section
-
-/-!
-# Body.Basic
-
-This module defines the `Body` typeclass for HTTP body streams, and shared conversion types
-`ToByteArray` and `FromByteArray` used for encoding and decoding body content.
--/
-
-namespace Std.Http
-open Std Internal IO Async
-
-set_option linter.all true
-
-/--
-Typeclass for values that can be read as HTTP body streams.
--/
-class Body (α : Type) where
-  /--
-  Receives the next body chunk. Returns `none` at end-of-stream.
-  -/
-  recv : α → Async (Option Chunk)
-
-  /--
-  Closes the body stream.
-  -/
-  close : α → Async Unit
-
-  /--
-  Returns `true` when the body stream is closed.
-  -/
-  isClosed : α → Async Bool
-
-  /--
-  Selector that resolves when a chunk is available or EOF is reached.
-  -/
-  recvSelector : α → Selector (Option Chunk)
-
-  /--
-  Gets the declared size of the body.
-  -/
-  getKnownSize : α → Async (Option Body.Length)
-
-  /--
-  Sets the declared size of a body.
-  -/
-  setKnownSize : α → Option Body.Length → Async Unit
-end Std.Http
-
-namespace Std.Http.Body
-
-/--
-Typeclass for types that can be converted to a `ByteArray`.
--/
-class ToByteArray (α : Type) where
-
-  /--
-  Transforms into a `ByteArray`.
-  -/
-  toByteArray : α → ByteArray
-
-instance : ToByteArray ByteArray where
-  toByteArray := id
-
-instance : ToByteArray String where
-  toByteArray := String.toUTF8
-
-/--
-Typeclass for types that can be decoded from a `ByteArray`. The conversion may fail with an error
-message if the bytes are not valid for the target type.
--/
-class FromByteArray (α : Type) where
-
-  /--
-  Attempts to decode a `ByteArray` into the target type, returning an error message on failure.
-  -/
-  fromByteArray : ByteArray → Except String α
-
-instance : FromByteArray ByteArray where
-  fromByteArray := .ok
-
-instance : FromByteArray String where
-  fromByteArray bs :=
-    match String.fromUTF8? bs with
-    | some s => .ok s
-    | none => .error "invalid UTF-8 encoding"
-
-end Std.Http.Body

src/Std/Internal/Http/Data/Body/Empty.lean

@@ -1,116 +0,0 @@
-/-
-Copyright (c) 2025 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.Internal.Http.Data.Request
-public import Std.Internal.Http.Data.Response
-public import Std.Internal.Http.Data.Body.Any
-
-public section
-
-/-!
-# Body.Empty
-
-Represents an always-empty, already-closed body handle.
--/
-
-namespace Std.Http.Body
-open Std Internal IO Async
-
-set_option linter.all true
-
-/--
-An empty body handle.
--/
-structure Empty where
-deriving Inhabited, BEq
-
-namespace Empty
-
-/--
-Receives from an empty body, always returning end-of-stream.
--/
-@[inline]
-def recv (_ : Empty) : Async (Option Chunk) :=
-  pure none
-
-/--
-Closes an empty body (no-op).
--/
-@[inline]
-def close (_ : Empty) : Async Unit :=
-  pure ()
-
-/--
-Empty bodies are always closed for reading.
--/
-@[inline]
-def isClosed (_ : Empty) : Async Bool :=
-  pure true
-
-/--
-Selector that immediately resolves with end-of-stream for an empty body.
--/
-@[inline]
-def recvSelector (_ : Empty) : Selector (Option Chunk) where
-  tryFn := pure (some none)
-  registerFn waiter := do
-    let lose := pure ()
-    let win promise := do
-      promise.resolve (.ok none)
-    waiter.race lose win
-  unregisterFn := pure ()
-
-end Empty
-
-instance : Http.Body Empty where
-  recv := Empty.recv
-  close := Empty.close
-  isClosed := Empty.isClosed
-  recvSelector := Empty.recvSelector
-  getKnownSize _ := pure (some <| .fixed 0)
-  setKnownSize _ _ := pure ()
-
-
-instance : Coe Empty Any := ⟨Any.ofBody⟩
-
-instance : Coe (Response Empty) (Response Any) where
-  coe f := { f with }
-
-instance : Coe (ContextAsync (Response Empty)) (ContextAsync (Response Any)) where
-  coe action := do
-    let response ← action
-    pure (response : Response Any)
-
-instance : Coe (Async (Response Empty)) (ContextAsync (Response Any)) where
-  coe action := do
-    let response ← action
-    pure (response : Response Any)
-
-end Body
-
-namespace Request.Builder
-open Internal.IO.Async
-
-/--
-Builds a request with no body.
--/
-def empty (builder : Builder) : Async (Request Body.Empty) :=
-  pure <| builder.body {}
-
-end Request.Builder
-
-namespace Response.Builder
-open Internal.IO.Async
-
-/--
-Builds a response with no body.
--/
-def empty (builder : Builder) : Async (Response Body.Empty) :=
-  pure <| builder.body {}
-
-end Response.Builder

src/Std/Internal/Http/Data/Body/Full.lean

@@ -1,232 +0,0 @@
-/-
-Copyright (c) 2025 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.Sync
-public import Std.Internal.Http.Data.Request
-public import Std.Internal.Http.Data.Response
-public import Std.Internal.Http.Data.Body.Any
-public import Init.Data.ByteArray
-
-public section
-
-/-!
-# Body.Full
-
-A body backed by a fixed `ByteArray` held in a `Mutex`.
-
-The byte array is consumed at most once: the first call to `recv` atomically takes the data
-and returns it as a single chunk; subsequent calls return `none` (end-of-stream).
-Closing the body discards any unconsumed data.
--/
-
-namespace Std.Http.Body
-open Std Internal IO Async
-
-set_option linter.all true
-
-/--
-A body backed by a fixed, mutex-protected `ByteArray`.
-
-The data is consumed on the first read. Once consumed (or explicitly closed), the body
-behaves as a closed, empty channel.
--/
-structure Full where
-  private mk ::
-  private state : Mutex (Option ByteArray)
-deriving Nonempty
-
-namespace Full
-
-private def takeChunk : AtomicT (Option ByteArray) Async (Option Chunk) := do
-  match ← get with
-  | none =>
-    pure none
-  | some data =>
-    set (none : Option ByteArray)
-    if data.isEmpty then
-      pure none
-    else
-      pure (some (Chunk.ofByteArray data))
-
-/--
-Creates a `Full` body from a `ByteArray`.
--/
-def ofByteArray (data : ByteArray) : Async Full := do
-  let state ← Mutex.new (some data)
-  return { state }
-
-/--
-Creates a `Full` body from a `String`.
--/
-def ofString (data : String) : Async Full := do
-  let state ← Mutex.new (some data.toUTF8)
-  return { state }
-
-/--
-Receives the body data. Returns the full byte array on the first call as a single chunk,
-then `none` on all subsequent calls.
--/
-def recv (full : Full) : Async (Option Chunk) :=
-  full.state.atomically do
-    takeChunk
-
-/--
-Closes the body, discarding any unconsumed data.
--/
-def close (full : Full) : Async Unit :=
-  full.state.atomically do
-    set (none : Option ByteArray)
-
-/--
-Returns `true` when the data has been consumed or the body has been closed.
--/
-def isClosed (full : Full) : Async Bool :=
-  full.state.atomically do
-    return (← get).isNone
-
-/--
-Returns the known size of the remaining data.
-Returns `some (.fixed n)` with the current byte count, or `some (.fixed 0)` if the body has
-already been consumed or closed.
--/
-def getKnownSize (full : Full) : Async (Option Body.Length) :=
-  full.state.atomically do
-    match ← get with
-    | none => pure (some (.fixed 0))
-    | some data => pure (some (.fixed data.size))
-
-/--
-Selector that immediately resolves to the remaining chunk (or EOF).
--/
-def recvSelector (full : Full) : Selector (Option Chunk) where
-  tryFn := do
-    let chunk ← full.state.atomically do
-      takeChunk
-    pure (some chunk)
-
-  registerFn waiter := do
-    full.state.atomically do
-      let lose := pure ()
-
-      let win promise := do
-        let chunk ← takeChunk
-        promise.resolve (.ok chunk)
-
-      waiter.race lose win
-
-  unregisterFn := pure ()
-
-end Full
-
-instance : Http.Body Full where
-  recv := Full.recv
-  close := Full.close
-  isClosed := Full.isClosed
-  recvSelector := Full.recvSelector
-  getKnownSize := Full.getKnownSize
-  setKnownSize _ _ := pure ()
-
-instance : Coe Full Any := ⟨Any.ofBody⟩
-
-instance : Coe (Response Full) (Response Any) where
-  coe f := { f with }
-
-instance : Coe (ContextAsync (Response Full)) (ContextAsync (Response Any)) where
-  coe action := do
-    let response ← action
-    pure (response : Response Any)
-
-instance : Coe (Async (Response Full)) (ContextAsync (Response Any)) where
-  coe action := do
-    let response ← action
-    pure (response : Response Any)
-
-end Body
-
-namespace Request.Builder
-
-open Internal.IO.Async
-
-/--
-Builds a request body from raw bytes without setting any headers.
-Use `bytes` instead if you want `Content-Type: application/octet-stream` set automatically.
--/
-def fromBytes (builder : Builder) (content : ByteArray) : Async (Request Body.Full) := do
-  return builder.body (← Body.Full.ofByteArray content)
-
-/--
-Builds a request with a binary body.
-Sets `Content-Type: application/octet-stream`.
-Use `fromBytes` instead if you need to set a different `Content-Type` or none at all.
--/
-def bytes (builder : Builder) (content : ByteArray) : Async (Request Body.Full) :=
-  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "application/octet-stream")) content
-
-/--
-Builds a request with a text body.
-Sets `Content-Type: text/plain; charset=utf-8`.
--/
-def text (builder : Builder) (content : String) : Async (Request Body.Full) :=
-  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "text/plain; charset=utf-8")) content.toUTF8
-
-/--
-Builds a request with a JSON body.
-Sets `Content-Type: application/json`.
--/
-def json (builder : Builder) (content : String) : Async (Request Body.Full) :=
-  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "application/json")) content.toUTF8
-
-/--
-Builds a request with an HTML body.
-Sets `Content-Type: text/html; charset=utf-8`.
--/
-def html (builder : Builder) (content : String) : Async (Request Body.Full) :=
-  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "text/html; charset=utf-8")) content.toUTF8
-
-end Request.Builder
-
-namespace Response.Builder
-open Internal.IO.Async
-
-/--
-Builds a response body from raw bytes without setting any headers.
-Use `bytes` instead if you want `Content-Type: application/octet-stream` set automatically.
--/
-def fromBytes (builder : Builder) (content : ByteArray) : Async (Response Body.Full) := do
-  return builder.body (← Body.Full.ofByteArray content)
-
-/--
-Builds a response with a binary body.
-Sets `Content-Type: application/octet-stream`.
-Use `fromBytes` instead if you need to set a different `Content-Type` or none at all.
--/
-def bytes (builder : Builder) (content : ByteArray) : Async (Response Body.Full) :=
-  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "application/octet-stream")) content
-
-/--
-Builds a response with a text body.
-Sets `Content-Type: text/plain; charset=utf-8`.
--/
-def text (builder : Builder) (content : String) : Async (Response Body.Full) :=
-  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "text/plain; charset=utf-8")) content.toUTF8
-
-/--
-Builds a response with a JSON body.
-Sets `Content-Type: application/json`.
--/
-def json (builder : Builder) (content : String) : Async (Response Body.Full) :=
-  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "application/json")) content.toUTF8
-
-/--
-Builds a response with an HTML body.
-Sets `Content-Type: text/html; charset=utf-8`.
--/
-def html (builder : Builder) (content : String) : Async (Response Body.Full) :=
-  fromBytes (builder.header Header.Name.contentType (Header.Value.ofString! "text/html; charset=utf-8")) content.toUTF8
-
-end Response.Builder

src/Std/Internal/Http/Data/Body/Length.lean

@@ -1,60 +0,0 @@
-/-
-Copyright (c) 2025 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.Data.Repr
-
-public section
-
-/-!
-# Body.Length
-
-This module defines the `Length` type, that represents the Content-Length or Transfer-Encoding
-of an HTTP request or response.
--/
-
-namespace Std.Http.Body
-
-set_option linter.all true
-
-/--
-Size of the body of a response or request.
--/
-inductive Length
-  /--
-  Indicates that the HTTP message body uses **chunked transfer encoding**.
-  -/
-  | chunked
-
-  /--
-  Indicates that the HTTP message body has a **fixed, known length**, as specified by the
-  `Content-Length` header.
-  -/
-  | fixed (n : Nat)
-deriving Repr, BEq
-
-namespace Length
-
-/--
-Checks if the `Length` is chunked.
--/
-@[inline]
-def isChunked : Length → Bool
-  | .chunked => true
-  | _ => false
-
-/--
-Checks if the `Length` is a fixed size.
--/
-@[inline]
-def isFixed : Length → Bool
-  | .fixed _ => true
-  | _ => false
-
-end Length
-
-end Std.Http.Body

src/Std/Internal/Http/Data/Body/Stream.lean

@@ -1,650 +0,0 @@
-/-
-Copyright (c) 2025 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.Sync
-public import Std.Internal.Async
-public import Std.Internal.Http.Data.Request
-public import Std.Internal.Http.Data.Response
-public import Std.Internal.Http.Data.Chunk
-public import Std.Internal.Http.Data.Body.Basic
-public import Std.Internal.Http.Data.Body.Any
-public import Init.Data.ByteArray
-
-public section
-
-/-!
-# Body.Stream
-
-This module defines a zero-buffer rendezvous body channel (`Body.Stream`) that supports
-both sending and receiving chunks.
-
-There is no queue and no capacity. A send waits for a receiver and a receive waits for a sender.
-At most one blocked producer and one blocked consumer are supported.
--/
-
-namespace Std.Http
-
-namespace Body
-
-open Std Internal IO Async
-
-set_option linter.all true
-
-namespace Channel
-
-open Internal.IO.Async in
-private inductive Consumer where
-  | normal (promise : IO.Promise (Option Chunk))
-  | select (finished : Waiter (Option Chunk))
-
-private def Consumer.resolve (c : Consumer) (x : Option Chunk) : BaseIO Bool := do
-  match c with
-  | .normal promise =>
-    promise.resolve x
-    return true
-  | .select waiter =>
-    let lose := return false
-    let win promise := do
-      promise.resolve (.ok x)
-      return true
-    waiter.race lose win
-
-private structure Producer where
-  chunk : Chunk
-
-  /--
-  Resolved with `true` when consumed by a receiver, `false` when the channel closes.
-  -/
-  done : IO.Promise Bool
-
-open Internal.IO.Async in
-private def resolveInterestWaiter (waiter : Waiter Bool) (x : Bool) : BaseIO Bool := do
-  let lose := return false
-  let win promise := do
-    promise.resolve (.ok x)
-    return true
-  waiter.race lose win
-
-private structure State where
-  /--
-  A single blocked producer waiting for a receiver.
-  -/
-  pendingProducer : Option Producer
-
-  /--
-  A single blocked consumer waiting for a producer.
-  -/
-  pendingConsumer : Option Consumer
-
-  /--
-  A waiter for `Stream.interestSelector`.
-  -/
-  interestWaiter : Option (Internal.IO.Async.Waiter Bool)
-
-  /--
-  Whether the channel is closed.
-  -/
-  closed : Bool
-
-  /--
-  Known size of the stream if available.
-  -/
-  knownSize : Option Body.Length
-
-  /--
-  Buffered partial chunk data accumulated from `Stream.send ... (incomplete := true)`.
-  These partial pieces are collapsed and emitted as a single chunk on the next complete send.
-  -/
-  pendingIncompleteChunk : Option Chunk := none
-deriving Nonempty
-
-end Channel
-
-/--
-A zero-buffer rendezvous body channel that supports both sending and receiving chunks.
--/
-structure Stream where
-  private mk ::
-  private state : Mutex Channel.State
-deriving Nonempty, TypeName
-
-/--
-Creates a rendezvous body stream.
--/
-def mkStream : Async Stream := do
-  let state ← Mutex.new {
-    pendingProducer := none
-    pendingConsumer := none
-    interestWaiter := none
-    closed := false
-    knownSize := none
-  }
-  return { state }
-
-namespace Channel
-
-private def decreaseKnownSize (knownSize : Option Body.Length) (chunk : Chunk) : Option Body.Length :=
-  match knownSize with
-  | some (.fixed res) => some (Body.Length.fixed (res - chunk.data.size))
-  | _ => knownSize
-
-private def pruneFinishedWaiters [Monad m] [MonadLiftT (ST IO.RealWorld) m] :
-    AtomicT State m Unit := do
-  let st ← get
-
-  let pendingConsumer ←
-    match st.pendingConsumer with
-    | some (.select waiter) =>
-      if ← waiter.checkFinished then
-        pure none
-      else
-        pure st.pendingConsumer
-    | _ =>
-      pure st.pendingConsumer
-
-  let interestWaiter ←
-    match st.interestWaiter with
-    | some waiter =>
-      if ← waiter.checkFinished then
-        pure none
-      else
-        pure st.interestWaiter
-    | none =>
-      pure none
-
-  set { st with pendingConsumer, interestWaiter }
-
-private def signalInterest [Monad m] [MonadLiftT (ST IO.RealWorld) m] [MonadLiftT BaseIO m] :
-    AtomicT State m Unit := do
-  let st ← get
-  if let some waiter := st.interestWaiter then
-    discard <| resolveInterestWaiter waiter true
-    set { st with interestWaiter := none }
-
-private def recvReady' [Monad m] [MonadLiftT (ST IO.RealWorld) m] :
-    AtomicT State m Bool := do
-  let st ← get
-  return st.pendingProducer.isSome || st.closed
-
-private def hasInterest' [Monad m] [MonadLiftT (ST IO.RealWorld) m] :
-    AtomicT State m Bool := do
-  let st ← get
-  return st.pendingConsumer.isSome
-
-private def tryRecv' [Monad m] [MonadLiftT (ST IO.RealWorld) m] [MonadLiftT BaseIO m] :
-    AtomicT State m (Option Chunk) := do
-  let st ← get
-  if let some producer := st.pendingProducer then
-    set {
-      st with
-      pendingProducer := none
-      knownSize := decreaseKnownSize st.knownSize producer.chunk
-    }
-    discard <| producer.done.resolve true
-    return some producer.chunk
-  else
-    return none
-
-private def close' [Monad m] [MonadLiftT (ST IO.RealWorld) m] [MonadLiftT BaseIO m] :
-    AtomicT State m Unit := do
-  let st ← get
-  if st.closed then
-    return ()
-
-  if let some consumer := st.pendingConsumer then
-    discard <| consumer.resolve none
-
-  if let some waiter := st.interestWaiter then
-    discard <| resolveInterestWaiter waiter false
-
-  if let some producer := st.pendingProducer then
-    discard <| producer.done.resolve false
-
-  set {
-    st with
-    pendingProducer := none
-    pendingConsumer := none
-    interestWaiter := none
-    pendingIncompleteChunk := none
-    closed := true
-  }
-
-end Channel
-
-namespace Stream
-
-/--
-Attempts to receive a chunk from the channel without blocking.
-Returns `some chunk` only when a producer is already waiting.
--/
-def tryRecv (stream : Stream) : Async (Option Chunk) :=
-  stream.state.atomically do
-    Channel.pruneFinishedWaiters
-    Channel.tryRecv'
-
-private def recv' (stream : Stream) : BaseIO (AsyncTask (Option Chunk)) := do
-  stream.state.atomically do
-    Channel.pruneFinishedWaiters
-
-    if let some chunk ← Channel.tryRecv' then
-      return AsyncTask.pure (some chunk)
-
-    let st ← get
-    if st.closed then
-      return AsyncTask.pure none
-
-    if st.pendingConsumer.isSome then
-      return Task.pure (.error (IO.Error.userError "only one blocked consumer is allowed"))
-
-    let promise ← IO.Promise.new
-    set { st with pendingConsumer := some (.normal promise) }
-    Channel.signalInterest
-    return promise.result?.map (sync := true) fun
-      | none => .error (IO.Error.userError "the promise linked to the consumer was dropped")
-      | some res => .ok res
-
-/--
-Receives a chunk from the channel. Blocks until a producer sends one.
-Returns `none` if the channel is closed and no producer is waiting.
--/
-def recv (stream : Stream) : Async (Option Chunk) := do
-  Async.ofAsyncTask (← recv' stream)
-
-/--
-Closes the channel.
--/
-def close (stream : Stream) : Async Unit :=
-  stream.state.atomically do
-    Channel.close'
-
-/--
-Checks whether the channel is closed.
--/
-@[always_inline, inline]
-def isClosed (stream : Stream) : Async Bool :=
-  stream.state.atomically do
-    return (← get).closed
-
-/--
-Gets the known size if available.
--/
-@[always_inline, inline]
-def getKnownSize (stream : Stream) : Async (Option Body.Length) :=
-  stream.state.atomically do
-    return (← get).knownSize
-
-/--
-Sets known size metadata.
--/
-@[always_inline, inline]
-def setKnownSize (stream : Stream) (size : Option Body.Length) : Async Unit :=
-  stream.state.atomically do
-    modify fun st => { st with knownSize := size }
-
-open Internal.IO.Async in
-
-/--
-Creates a selector that resolves when a producer is waiting (or the channel closes).
--/
-def recvSelector (stream : Stream) : Selector (Option Chunk) where
-  tryFn := do
-    stream.state.atomically do
-      Channel.pruneFinishedWaiters
-      if ← Channel.recvReady' then
-        return some (← Channel.tryRecv')
-      else
-        return none
-
-  registerFn waiter := do
-    stream.state.atomically do
-      Channel.pruneFinishedWaiters
-      if ← Channel.recvReady' then
-        let lose := return ()
-        let win promise := do
-          promise.resolve (.ok (← Channel.tryRecv'))
-        waiter.race lose win
-      else
-        let st ← get
-        if st.pendingConsumer.isSome then
-          throw (.userError "only one blocked consumer is allowed")
-
-        set { st with pendingConsumer := some (.select waiter) }
-        Channel.signalInterest
-
-  unregisterFn := do
-    stream.state.atomically do
-      Channel.pruneFinishedWaiters
-
-/--
-Iterates over chunks until the channel closes.
--/
-@[inline]
-protected partial def forIn
-    {β : Type} (stream : Stream) (acc : β)
-    (step : Chunk → β → Async (ForInStep β)) : Async β := do
-
-  let rec @[specialize] loop (stream : Stream) (acc : β) : Async β := do
-    if let some chunk ← stream.recv then
-      match ← step chunk acc with
-      | .done res => return res
-      | .yield res => loop stream res
-    else
-      return acc
-
-  loop stream acc
-
-/--
-Context-aware iteration over chunks until the channel closes.
--/
-@[inline]
-protected partial def forIn'
-    {β : Type} (stream : Stream) (acc : β)
-    (step : Chunk → β → ContextAsync (ForInStep β)) : ContextAsync β := do
-
-  let rec @[specialize] loop (stream : Stream) (acc : β) : ContextAsync β := do
-    let data ← Selectable.one #[
-      .case stream.recvSelector pure,
-      .case (← ContextAsync.doneSelector) (fun _ => pure none),
-    ]
-
-    if let some chunk := data then
-      match ← step chunk acc with
-      | .done res => return res
-      | .yield res => loop stream res
-    else
-      return acc
-
-  loop stream acc
-
-/--
-Abstracts over how the next chunk is received, allowing `readAll` to work in both `Async`
-(no cancellation) and `ContextAsync` (races with cancellation via `doneSelector`).
--/
-class NextChunk (m : Type → Type) where
-  /--
-  Receives the next chunk, stopping at EOF or (in `ContextAsync`) when the context is cancelled.
-  -/
-  nextChunk : Stream → m (Option Chunk)
-
-instance : NextChunk Async where
-  nextChunk := Stream.recv
-
-instance : NextChunk ContextAsync where
-  nextChunk stream := do
-    Selectable.one #[
-      .case stream.recvSelector pure,
-      .case (← ContextAsync.doneSelector) (fun _ => pure none),
-    ]
-
-/--
-Reads all remaining chunks and decodes them into `α`.
-
-Works in both `Async` (reads until EOF, no cancellation) and `ContextAsync` (also stops if the
-context is cancelled).
--/
-partial def readAll
-    [FromByteArray α]
-    [Monad m] [MonadExceptOf IO.Error m] [NextChunk m]
-    (stream : Stream)
-    (maximumSize : Option UInt64 := none) :
-    m α := do
-
-  let rec loop (result : ByteArray) : m ByteArray := do
-    match ← NextChunk.nextChunk stream with
-    | none => return result
-    | some chunk =>
-      let result := result ++ chunk.data
-      if let some max := maximumSize then
-        if result.size.toUInt64 > max then
-          throw (.userError s!"body exceeded maximum size of {max} bytes")
-      loop result
-
-  let result ← loop ByteArray.empty
-
-  match FromByteArray.fromByteArray result with
-  | .ok a => return a
-  | .error msg => throw (.userError msg)
-
-private def collapseForSend
-    (stream : Stream)
-    (chunk : Chunk)
-    (incomplete : Bool) : BaseIO (Except IO.Error (Option Chunk)) := do
-
-  stream.state.atomically do
-    Channel.pruneFinishedWaiters
-    let st ← get
-
-    if st.closed then
-      return .error (.userError "channel closed")
-
-    let merged := match st.pendingIncompleteChunk with
-      | some pending =>
-        {
-          data := pending.data ++ chunk.data
-          extensions := if pending.extensions.isEmpty then chunk.extensions else pending.extensions
-        }
-      | none => chunk
-
-    if incomplete then
-      set { st with pendingIncompleteChunk := some merged }
-      return .ok none
-    else
-      set { st with pendingIncompleteChunk := none }
-      return .ok (some merged)
-
-/--
-Sends a chunk, retrying if a select-mode consumer races and loses. If no consumer is ready,
-installs the chunk as a pending producer and awaits acknowledgement from the receiver.
--/
-private partial def send' (stream : Stream) (chunk : Chunk) : Async Unit := do
-  let done ← IO.Promise.new
-  let result : Except IO.Error (Option Bool) ← stream.state.atomically do
-    Channel.pruneFinishedWaiters
-    let st ← get
-
-    if st.closed then
-      return .error (IO.Error.userError "channel closed")
-
-    if let some consumer := st.pendingConsumer then
-      let success ← consumer.resolve (some chunk)
-
-      if success then
-        set {
-          st with
-          pendingConsumer := none
-          knownSize := Channel.decreaseKnownSize st.knownSize chunk
-        }
-        return .ok (some true)
-      else
-        set { st with pendingConsumer := none }
-        return .ok (some false)
-    else if st.pendingProducer.isSome then
-      return .error (IO.Error.userError "only one blocked producer is allowed")
-    else
-      set { st with pendingProducer := some { chunk, done } }
-      return .ok none
-
-  match result with
-  | .error err =>
-    throw err
-  | .ok (some true) =>
-    return ()
-  | .ok (some false) =>
-    -- The select-mode consumer raced and lost; recurse to allocate a fresh `done` promise.
-    send' stream chunk
-  | .ok none =>
-    match ← await done.result? with
-    | some true => return ()
-    | _ => throw (IO.Error.userError "channel closed")
-
-/--
-Sends a chunk.
-
-If `incomplete := true`, the chunk is buffered and collapsed with subsequent chunks, and is not
-delivered to the receiver yet.
-If `incomplete := false`, any buffered incomplete pieces are collapsed with this chunk and the
-single merged chunk is sent.
--/
-def send (stream : Stream) (chunk : Chunk) (incomplete : Bool := false) : Async Unit := do
-  match (← collapseForSend stream chunk incomplete) with
-  | .error err => throw err
-  | .ok none => pure ()
-  | .ok (some toSend) =>
-    if toSend.data.isEmpty ∧ toSend.extensions.isEmpty then
-      return ()
-
-    send' stream toSend
-
-/--
-Returns `true` when a consumer is currently blocked waiting for data.
--/
-def hasInterest (stream : Stream) : Async Bool :=
-  stream.state.atomically do
-    Channel.pruneFinishedWaiters
-    Channel.hasInterest'
-
-open Internal.IO.Async in
-/--
-Creates a selector that resolves when consumer interest is present.
-Returns `true` when a consumer is waiting, `false` when the channel closes first.
--/
-def interestSelector (stream : Stream) : Selector Bool where
-  tryFn := do
-    stream.state.atomically do
-      Channel.pruneFinishedWaiters
-      let st ← get
-      if st.pendingConsumer.isSome then
-        return some true
-      else if st.closed then
-        return some false
-      else
-        return none
-
-  registerFn waiter := do
-    stream.state.atomically do
-      Channel.pruneFinishedWaiters
-      let st ← get
-
-      if st.pendingConsumer.isSome then
-        let lose := return ()
-        let win promise := do
-          promise.resolve (.ok true)
-        waiter.race lose win
-      else if st.closed then
-        let lose := return ()
-        let win promise := do
-          promise.resolve (.ok false)
-        waiter.race lose win
-      else if st.interestWaiter.isSome then
-        throw (.userError "only one blocked interest selector is allowed")
-      else
-        set { st with interestWaiter := some waiter }
-
-  unregisterFn := do
-    stream.state.atomically do
-      Channel.pruneFinishedWaiters
-
-end Stream
-
-/--
-Creates a body from a producer function.
-Returns the stream immediately and runs `gen` in a detached task.
-The channel is always closed when `gen` returns or throws.
-Errors from `gen` are not rethrown here; consumers observe end-of-stream via `recv = none`.
--/
-def stream (gen : Stream → Async Unit) : Async Stream := do
-  let s ← mkStream
-  background <| do
-    try
-      gen s
-    finally
-      s.close
-  return s
-
-/--
-Creates a body from a fixed byte array.
--/
-def fromBytes (content : ByteArray) : Async Stream := do
-  stream fun s => do
-    s.setKnownSize (some (.fixed content.size))
-    if content.size > 0 then
-      s.send (Chunk.ofByteArray content)
-
-/--
-Creates an empty `Stream` body channel (already closed, no data).
-
-Prefer `Body.Empty` when you need a concrete zero-cost type. Use this when the calling
-context requires a `Stream` specifically.
--/
-def empty : Async Stream := do
-  let s ← mkStream
-  s.setKnownSize (some (.fixed 0))
-  s.close
-  return s
-
-instance : ForIn Async Stream Chunk where
-  forIn := Stream.forIn
-
-instance : ForIn ContextAsync Stream Chunk where
-  forIn := Stream.forIn'
-
-instance : Http.Body Stream where
-  recv := Stream.recv
-  close := Stream.close
-  isClosed := Stream.isClosed
-  recvSelector := Stream.recvSelector
-  getKnownSize := Stream.getKnownSize
-  setKnownSize := Stream.setKnownSize
-
-instance : Coe Stream Any := ⟨Any.ofBody⟩
-
-instance : Coe (Response Stream) (Response Any) where
-  coe f := { f with }
-
-instance : Coe (ContextAsync (Response Stream)) (ContextAsync (Response Any)) where
-  coe action := do
-    let response ← action
-    pure (response : Response Any)
-
-instance : Coe (Async (Response Stream)) (ContextAsync (Response Any)) where
-  coe action := do
-    let response ← action
-    pure (response : Response Any)
-
-end Body
-
-namespace Request.Builder
-
-open Internal.IO.Async
-
-/--
-Builds a request with a streaming body generator.
--/
-def stream
-    (builder : Builder)
-    (gen : Body.Stream → Async Unit) :
-    Async (Request Body.Stream) := do
-  let s ← Body.stream gen
-  return Request.Builder.body builder s
-
-end Request.Builder
-
-namespace Response.Builder
-open Internal.IO.Async
-
-/--
-Builds a response with a streaming body generator.
--/
-def stream
-    (builder : Builder)
-    (gen : Body.Stream → Async Unit) :
-    Async (Response Body.Stream) := do
-  let s ← Body.stream gen
-  return Response.Builder.body builder s
-
-end Response.Builder

src/Std/Internal/Http/Data/Request.lean

@@ -124,6 +124,12 @@ def new : Builder := { }
 
 namespace Builder
 
+/--
+Creates a new HTTP request builder with the default head
+(method: GET, version: HTTP/1.1, target: `*`).
+-/
+def empty : Builder := { }
+
 /--
 Sets the HTTP method for the request being built.
 -/

src/Std/Internal/Http/Data/Response.lean

@@ -111,7 +111,7 @@ namespace Builder
 /--
 Creates a new HTTP Response builder with default head (status: 200 OK, version: HTTP/1.1).
 -/
-def new : Builder := { }
+def empty : Builder := { }
 
 /--
 Sets the HTTP status code for the response being built.
@@ -173,66 +173,66 @@ end Builder
 Creates a new HTTP Response builder with the 200 status code.
 -/
 def ok : Builder :=
-  .new |>.status .ok
+  .empty |>.status .ok
 
 /--
 Creates a new HTTP Response builder with the provided status.
 -/
 def withStatus (status : Status) : Builder :=
-  .new |>.status status
+  .empty |>.status status
 
 /--
 Creates a new HTTP Response builder with the 404 status code.
 -/
 def notFound : Builder :=
-  .new |>.status .notFound
+  .empty |>.status .notFound
 
 /--
 Creates a new HTTP Response builder with the 500 status code.
 -/
 def internalServerError : Builder :=
-  .new |>.status .internalServerError
+  .empty |>.status .internalServerError
 
 /--
 Creates a new HTTP Response builder with the 400 status code.
 -/
 def badRequest : Builder :=
-  .new |>.status .badRequest
+  .empty |>.status .badRequest
 
 /--
 Creates a new HTTP Response builder with the 201 status code.
 -/
 def created : Builder :=
-  .new |>.status .created
+  .empty |>.status .created
 
 /--
 Creates a new HTTP Response builder with the 202 status code.
 -/
 def accepted : Builder :=
-  .new |>.status .accepted
+  .empty |>.status .accepted
 
 /--
 Creates a new HTTP Response builder with the 401 status code.
 -/
 def unauthorized : Builder :=
-  .new |>.status .unauthorized
+  .empty |>.status .unauthorized
 
 /--
 Creates a new HTTP Response builder with the 403 status code.
 -/
 def forbidden : Builder :=
-  .new |>.status .forbidden
+  .empty |>.status .forbidden
 
 /--
 Creates a new HTTP Response builder with the 409 status code.
 -/
 def conflict : Builder :=
-  .new |>.status .conflict
+  .empty |>.status .conflict
 
 /--
 Creates a new HTTP Response builder with the 503 status code.
 -/
 def serviceUnavailable : Builder :=
-  .new |>.status .serviceUnavailable
+  .empty |>.status .serviceUnavailable
 
 end Response

src/Std/Internal/Http/Data/URI.lean

@@ -94,3 +94,4 @@ def parseOrRoot (s : String) : Std.Http.URI.Path :=
   parse? s |>.getD { segments := #[], absolute := true }
 
 end Std.Http.URI.Path
+