chore: nicer errors for too large reads

This seems to be prone to confusing Claude

.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:
@@ -66,6 +61,8 @@ To rebuild individual stage 2 modules without a full `make stage2`, use Lake dir
 cd build/release/stage2 && lake build Init.Prelude
 ```
 
+To run tests in stage2, replace `-C build/release` from above with `-C build/release/stage2`.
+
 ## New features
 
 When asked to implement new features:

.github/workflows/build-template.yml

@@ -59,11 +59,11 @@ jobs:
         with:
           msystem: clang64
           # `:` means do not prefix with msystem
-          pacboy: "make: python: cmake clang ccache gmp libuv openssl: git: zip: unzip: diffutils: binutils: tree: zstd tar:"
+          pacboy: "make: python: cmake clang ccache gmp libuv git: zip: unzip: diffutils: binutils: tree: zstd tar:"
         if: runner.os == 'Windows'
       - name: Install Brew Packages
         run: |
-          brew install ccache tree zstd coreutils gmp libuv openssl
+          brew install ccache tree zstd coreutils gmp libuv
         if: runner.os == 'macOS'
       - name: Checkout
         uses: actions/checkout@v6
@@ -92,7 +92,7 @@ jobs:
         run: |
           sudo dpkg --add-architecture i386
           sudo apt-get update
-          sudo apt-get install -y gcc-multilib g++-multilib ccache libuv1-dev:i386 libssl-dev:i386 pkgconf:i386
+          sudo apt-get install -y gcc-multilib g++-multilib ccache libuv1-dev:i386 pkgconf:i386
         if: matrix.cmultilib
       - name: Restore Cache
         id: restore-cache
@@ -131,7 +131,7 @@ jobs:
           [ -d build ] || mkdir build
           cd build
           # arguments passed to `cmake`
-          OPTIONS=(-DLEAN_EXTRA_MAKE_OPTS=-DwarningAsError=true)
+          OPTIONS=(-DWFAIL=ON)
           if [[ -n '${{ matrix.release }}' ]]; then
             # this also enables githash embedding into stage 1 library, which prohibits reusing
             # `.olean`s across commits, so we don't do it in the fast non-release CI

.github/workflows/ci.yml

@@ -305,7 +305,8 @@ jobs:
                 "test": true,
                 "CMAKE_PRESET": "reldebug",
                 // * `elab_bench/big_do` crashes with exit code 134
-                "CTEST_OPTIONS": "-E 'elab_bench/big_do'",
+                // * `compile_bench/channel` randomly segfaults
+                "CTEST_OPTIONS": "-E 'elab_bench/big_do|compile_bench/channel'",
               },
               {
                 "name": "Linux fsanitize",

.github/workflows/update-stage0.yml

@@ -77,7 +77,7 @@ jobs:
       # sync options with `Linux Lake` to ensure cache reuse
       run: |
         mkdir -p build
-        cmake --preset release -B build -DLEAN_EXTRA_MAKE_OPTS=-DwarningAsError=true
+        cmake --preset release -B build -DWFAIL=ON
       shell: 'nix develop -c bash -euxo pipefail {0}'
     - if: env.should_update_stage0 == 'yes'
       run: |

.gitignore

@@ -34,3 +34,4 @@ wdErr.txt
 wdIn.txt
 wdOut.txt
 downstream_releases/
+.claude/worktrees/

CMakeLists.txt

@@ -220,7 +220,9 @@ add_custom_target(
   DEPENDS stage2
 )
 
-add_custom_target(clean-stdlib COMMAND $(MAKE) -C stage1 clean-stdlib DEPENDS stage1)
+add_custom_target(clean-stdlib COMMAND $(MAKE) -C stage1 clean-stdlib DEPENDS stage1-configure)
+
+add_custom_target(cache-get COMMAND $(MAKE) -C stage1 cache-get DEPENDS stage1-configure)
 
 install(CODE "execute_process(COMMAND make -C stage1 install)")
 

doc/make/index.md

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

doc/make/msys2.md

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

doc/make/osx-10.9.md

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

doc/make/ubuntu.md

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

flake.nix

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

script/prepare-llvm-linux.sh

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

script/prepare-llvm-macos.sh

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

script/prepare-llvm-mingw.sh

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

script/release_repos.yml

@@ -28,6 +28,14 @@ repositories:
     branch: main
     dependencies: []
 
+  - name: leansqlite
+    url: https://github.com/leanprover/leansqlite
+    toolchain-tag: true
+    stable-branch: false
+    branch: main
+    dependencies:
+      - plausible
+
   - name: verso
     url: https://github.com/leanprover/verso
     toolchain-tag: true
@@ -100,7 +108,7 @@ repositories:
     toolchain-tag: true
     stable-branch: false
     branch: main
-    dependencies: [lean4-cli, BibtexQuery, mathlib4]
+    dependencies: [lean4-cli, BibtexQuery, mathlib4, leansqlite]
 
   - name: cslib
     url: https://github.com/leanprover/cslib

script/release_steps.py

@@ -481,11 +481,9 @@ def execute_release_steps(repo, version, config):
         run_command("lake update", cwd=repo_path, stream_output=True)
     elif repo_name == "verso":
         # verso has nested Lake projects in test-projects/ that each have their own
-        # lake-manifest.json with a subverso pin. After updating the root manifest via
-        # `lake update`, sync the de-modulized subverso rev into all sub-manifests.
-        # The sub-projects use an old toolchain (v4.21.0) that doesn't support module/prelude
-        # syntax, so they need the de-modulized version (tagged no-modules/<root-rev>).
-        # The "SubVerso version consistency" CI check accepts either the root or de-modulized rev.
+        # lake-manifest.json with a subverso pin and their own lean-toolchain.
+        # After updating the root manifest via `lake update`, sync the de-modulized
+        # subverso rev into all sub-manifests, and update their lean-toolchain files.
         run_command("lake update", cwd=repo_path, stream_output=True)
         print(blue("Syncing de-modulized subverso rev to test-project sub-manifests..."))
         sync_script = (
@@ -498,6 +496,15 @@ def execute_release_steps(repo, version, config):
         )
         run_command(sync_script, cwd=repo_path)
         print(green("Synced de-modulized subverso rev to all test-project sub-manifests"))
+        # Update all lean-toolchain files in test-projects/ to match the root
+        print(blue("Updating lean-toolchain files in test-projects/..."))
+        find_result = run_command("find test-projects -name lean-toolchain", cwd=repo_path)
+        for tc_path in find_result.stdout.strip().splitlines():
+            if tc_path:
+                tc_file = repo_path / tc_path
+                with open(tc_file, "w") as f:
+                    f.write(f"leanprover/lean4:{version}\n")
+                print(green(f"  Updated {tc_path}"))
     elif dependencies:
         run_command(f'perl -pi -e \'s/"v4\\.[0-9]+(\\.[0-9]+)?(-rc[0-9]+)?"/"' + version + '"/g\' lakefile.*', cwd=repo_path)
         run_command("lake update", cwd=repo_path, stream_output=True)
@@ -659,56 +666,61 @@ def execute_release_steps(repo, version, config):
         # Fetch latest changes to ensure we have the most up-to-date nightly-testing branch
         print(blue("Fetching latest changes from origin..."))
         run_command("git fetch origin", cwd=repo_path)
-        
-        try:
-            print(blue("Merging origin/nightly-testing..."))
-            run_command("git merge origin/nightly-testing", cwd=repo_path)
-            print(green("Merge completed successfully"))
-        except subprocess.CalledProcessError:
-            # Merge failed due to conflicts - check which files are conflicted
-            print(blue("Merge conflicts detected, checking which files are affected..."))
-            
-            # Get conflicted files using git status
-            status_result = run_command("git status --porcelain", cwd=repo_path)
-            conflicted_files = []
-            
-            for line in status_result.stdout.splitlines():
-                if len(line) >= 2 and line[:2] in ['UU', 'AA', 'DD', 'AU', 'UA', 'DU', 'UD']:
-                    # Extract filename (skip the first 3 characters which are status codes)
-                    conflicted_files.append(line[3:])
-            
-            # Filter out allowed files
-            allowed_patterns = ['lean-toolchain', 'lake-manifest.json']
-            problematic_files = []
-            
-            for file in conflicted_files:
-                is_allowed = any(pattern in file for pattern in allowed_patterns)
-                if not is_allowed:
-                    problematic_files.append(file)
-            
-            if problematic_files:
-                # There are conflicts in non-allowed files - fail
-                print(red("❌ Merge failed!"))
-                print(red(f"Merging nightly-testing resulted in conflicts in:"))
-                for file in problematic_files:
-                    print(red(f"  - {file}"))
-                print(red("Please resolve these conflicts manually."))
-                return
-            else:
-                # Only allowed files are conflicted - resolve them automatically
-                print(green(f"✅ Only allowed files conflicted: {', '.join(conflicted_files)}"))
-                print(blue("Resolving conflicts automatically..."))
-                
-                # For lean-toolchain and lake-manifest.json, keep our versions
+
+        # Check if nightly-testing branch exists on origin (use local ref after fetch for exact match)
+        nightly_check = run_command("git show-ref --verify --quiet refs/remotes/origin/nightly-testing", cwd=repo_path, check=False)
+        if nightly_check.returncode != 0:
+            print(yellow("No nightly-testing branch found on origin, skipping merge"))
+        else:
+            try:
+                print(blue("Merging origin/nightly-testing..."))
+                run_command("git merge origin/nightly-testing", cwd=repo_path)
+                print(green("Merge completed successfully"))
+            except subprocess.CalledProcessError:
+                # Merge failed due to conflicts - check which files are conflicted
+                print(blue("Merge conflicts detected, checking which files are affected..."))
+
+                # Get conflicted files using git status
+                status_result = run_command("git status --porcelain", cwd=repo_path)
+                conflicted_files = []
+
+                for line in status_result.stdout.splitlines():
+                    if len(line) >= 2 and line[:2] in ['UU', 'AA', 'DD', 'AU', 'UA', 'DU', 'UD']:
+                        # Extract filename (skip the first 3 characters which are status codes)
+                        conflicted_files.append(line[3:])
+
+                # Filter out allowed files
+                allowed_patterns = ['lean-toolchain', 'lake-manifest.json']
+                problematic_files = []
+
                 for file in conflicted_files:
-                    print(blue(f"Keeping our version of {file}"))
-                    run_command(f"git checkout --ours {file}", cwd=repo_path)
-                
-                # Complete the merge
-                run_command("git add .", cwd=repo_path)
-                run_command("git commit --no-edit", cwd=repo_path)
-                
-                print(green("✅ Merge completed successfully with automatic conflict resolution"))
+                    is_allowed = any(pattern in file for pattern in allowed_patterns)
+                    if not is_allowed:
+                        problematic_files.append(file)
+
+                if problematic_files:
+                    # There are conflicts in non-allowed files - fail
+                    print(red("❌ Merge failed!"))
+                    print(red(f"Merging nightly-testing resulted in conflicts in:"))
+                    for file in problematic_files:
+                        print(red(f"  - {file}"))
+                    print(red("Please resolve these conflicts manually."))
+                    return
+                else:
+                    # Only allowed files are conflicted - resolve them automatically
+                    print(green(f"✅ Only allowed files conflicted: {', '.join(conflicted_files)}"))
+                    print(blue("Resolving conflicts automatically..."))
+
+                    # For lean-toolchain and lake-manifest.json, keep our versions
+                    for file in conflicted_files:
+                        print(blue(f"Keeping our version of {file}"))
+                        run_command(f"git checkout --ours {file}", cwd=repo_path)
+
+                    # Complete the merge
+                    run_command("git add .", cwd=repo_path)
+                    run_command("git commit --no-edit", cwd=repo_path)
+
+                    print(green("✅ Merge completed successfully with automatic conflict resolution"))
 
     # Build and test (skip for Mathlib)
     if repo_name not in ["mathlib4"]:

src/CMakeLists.txt

@@ -116,11 +116,19 @@ option(CHECK_OLEAN_VERSION "Only load .olean files compiled with the current ver
 option(USE_LAKE "Use Lake instead of lean.mk for building core libs from language server" ON)
 option(USE_LAKE_CACHE "Use the Lake artifact cache for stage 1 builds (requires USE_LAKE)" OFF)
 
-set(LEAN_EXTRA_MAKE_OPTS "" CACHE STRING "extra options to lean --make")
+set(LEAN_EXTRA_OPTS "" CACHE STRING "extra options to lean (via lake or make)")
+set(LEAN_EXTRA_MAKE_OPTS "" CACHE STRING "extra options to leanmake")
 set(LEANC_CC ${CMAKE_C_COMPILER} CACHE STRING "C compiler to use in `leanc`")
 
 # Temporary, core-only flags. Must be synced with stdlib_flags.h.
-string(APPEND LEAN_EXTRA_MAKE_OPTS " -Dbackward.do.legacy=false")
+string(APPEND LEAN_EXTRA_OPTS " -Dbackward.do.legacy=false")
+
+# option used by the CI to fail on warnings
+option(WFAIL "Fail build if warnings are emitted by Lean" ON)
+if(WFAIL MATCHES "ON")
+  string(APPEND LAKE_EXTRA_ARGS " --wfail")
+  string(APPEND LEAN_EXTRA_MAKE_OPTS " -DwarningAsError=true")
+endif()
 
 if(LAZY_RC MATCHES "ON")
   set(LEAN_LAZY_RC "#define LEAN_LAZY_RC")
@@ -198,7 +206,7 @@ set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/lib/lean")
 
 # OSX default thread stack size is very small. Moreover, in Debug mode, each new stack frame consumes a lot of extra memory.
 if((MULTI_THREAD MATCHES "ON") AND (CMAKE_SYSTEM_NAME MATCHES "Darwin"))
-  string(APPEND LEAN_EXTRA_MAKE_OPTS " -s40000")
+  string(APPEND LEAN_EXTRA_OPTS " -s40000")
 endif()
 
 # We want explicit stack probes in huge Lean stack frames for robust stack overflow detection
@@ -357,28 +365,6 @@ if(NOT LEAN_STANDALONE)
   string(APPEND LEAN_EXTRA_LINKER_FLAGS " ${LIBUV_LDFLAGS}")
 endif()
 
-# OpenSSL
-if(NOT "${CMAKE_SYSTEM_NAME}" MATCHES "Emscripten")
-  find_package(OpenSSL 3 REQUIRED)
-  set(OPENSSL_LIBRARIES ${OPENSSL_SSL_LIBRARY} ${OPENSSL_CRYPTO_LIBRARY})
-  include_directories(${OPENSSL_INCLUDE_DIR})
-  string(JOIN " " OPENSSL_LIBRARIES_STR ${OPENSSL_LIBRARIES})
-  if(NOT LEAN_STANDALONE)
-    string(APPEND LEAN_EXTRA_LINKER_FLAGS " ${OPENSSL_LIBRARIES_STR}")
-  endif()
-endif()
-
-if(CMAKE_SYSTEM_NAME MATCHES "Linux")
-  string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,-rpath,\\$$ORIGIN")
-endif()
-
-if(CMAKE_SYSTEM_NAME MATCHES "Windows")
-  string(APPEND LEANSHARED_LINKER_FLAGS " -lcrypt32 -lgdi32")
-  if(NOT LEAN_STANDALONE)
-    string(APPEND LEAN_EXTRA_LINKER_FLAGS " -lcrypt32 -lgdi32")
-  endif()
-endif()
-
 # Windows SDK (for ICU)
 if(CMAKE_SYSTEM_NAME MATCHES "Windows")
   # Pass 'tools' to skip MSVC version check (as MSVC/Visual Studio is not necessarily installed)
@@ -494,17 +480,6 @@ endif()
 string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
 string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
 
-# In standalone (release) builds, OpenSSL must be statically embedded in libleanshared.so.
-# In non-standalone (dev/CI nix) builds, `find_package(OpenSSL)` resolves to shared libs from
-# the nix store. Adding those to libleanshared.so would produce DT_NEEDED entries pointing into
-# the nix store (including transitive libc++.so.1 because nix's libssl is built with libc++).
-# Those paths don't exist in `out/` during `make run-local` tests, breaking them.
-# For non-standalone builds, OpenSSL is instead provided via LEAN_EXTRA_LINKER_FLAGS (leanc.sh)
-# and resolved at runtime from the loading executable.
-if(DEFINED OPENSSL_LIBRARIES_STR AND LEAN_STANDALONE)
-  string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " ${OPENSSL_LIBRARIES_STR}")
-endif()
-
 # in local builds, link executables and not just dynlibs against C++ stdlib as well,
 # which is required for e.g. asan
 if(NOT LEAN_STANDALONE)
@@ -703,6 +678,9 @@ else()
   set(LEAN_PATH_SEPARATOR ":")
 endif()
 
+# inherit genral options for lean.mk.in and stdlib.make.in
+string(APPEND LEAN_EXTRA_MAKE_OPTS " ${LEAN_EXTRA_OPTS}")
+
 # Version
 configure_file("${LEAN_SOURCE_DIR}/version.h.in" "${LEAN_BINARY_DIR}/include/lean/version.h")
 if(STAGE EQUAL 0)
@@ -796,7 +774,7 @@ if(STAGE GREATER 1)
   endif()
 else()
   add_subdirectory(runtime)
-  if("${CMAKE_SYSTEM_NAME}" MATCHES "Emscripten")
+  if(CMAKE_SYSTEM_NAME MATCHES "Emscripten")
     add_dependencies(leanrt libuv)
     add_dependencies(leanrt_initial-exec libuv)
   endif()
@@ -1014,6 +992,13 @@ add_custom_target(
 
 add_custom_target(clean-olean DEPENDS clean-stdlib)
 
+if(USE_LAKE_CACHE)
+  add_custom_target(
+    cache-get
+    COMMAND ${PREV_STAGE}/bin/lake${CMAKE_EXECUTABLE_SUFFIX} cache get --repo=leanprover/lean4
+  )
+endif()
+
 install(
   DIRECTORY "${CMAKE_BINARY_DIR}/lib/"
   DESTINATION lib
@@ -1087,7 +1072,7 @@ string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}" LEANC_CC "${LEANC_CC}")
 string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}" LEANC_INTERNAL_FLAGS "${LEANC_INTERNAL_FLAGS}")
 string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}" LEANC_INTERNAL_LINKER_FLAGS "${LEANC_INTERNAL_LINKER_FLAGS}")
 
-toml_escape("${LEAN_EXTRA_MAKE_OPTS}" LEAN_EXTRA_OPTS_TOML)
+toml_escape("${LEAN_EXTRA_OPTS}" LEAN_EXTRA_OPTS_TOML)
 
 if(CMAKE_BUILD_TYPE MATCHES "Debug|Release|RelWithDebInfo|MinSizeRel")
   set(CMAKE_BUILD_TYPE_TOML "${CMAKE_BUILD_TYPE}")

src/Init/Data/Array/Basic.lean

@@ -802,6 +802,7 @@ Examples:
 def firstM {α : Type u} {m : Type v → Type w} [Alternative m] (f : α → m β) (as : Array α) : m β :=
   go 0
 where
+  @[specialize]
   go (i : Nat) : m β :=
     if hlt : i < as.size then
       f as[i] <|> go (i+1)
@@ -1085,6 +1086,17 @@ Examples:
 def sum {α} [Add α] [Zero α] : Array α → α :=
   foldr (· + ·) 0
 
+/--
+Computes the product of the elements of an array.
+
+Examples:
+ * `#[a, b, c].prod = a * (b * (c * 1))`
+ * `#[1, 2, 5].prod = 10`
+-/
+@[inline, expose]
+def prod {α} [Mul α] [One α] : Array α → α :=
+  foldr (· * ·) 1
+
 /--
 Counts the number of elements in the array `as` that satisfy the Boolean predicate `p`.
 
@@ -1253,7 +1265,7 @@ Examples:
 -/
 @[inline, expose]
 def findIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option Nat :=
-  let rec loop (j : Nat) :=
+  let rec @[specialize] loop (j : Nat) :=
     if h : j < as.size then
       if p as[j] then some j else loop (j + 1)
     else none

src/Init/Data/Array/Int.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.List.Int.Sum
+public import Init.Data.List.Int.Prod
 public import Init.Data.Array.MinMax
 import Init.Data.Int.Lemmas
 
@@ -74,4 +75,17 @@ theorem sum_div_length_le_max_of_max?_eq_some_int {xs : Array Int} (h : xs.max?
   simpa [List.max?_toArray, List.sum_toArray] using
     List.sum_div_length_le_max_of_max?_eq_some_int (by simpa using h)
 
+@[simp] theorem prod_replicate_int {n : Nat} {a : Int} : (replicate n a).prod = a ^ n := by
+  rw [← List.toArray_replicate, List.prod_toArray]
+  simp
+
+theorem prod_append_int {as₁ as₂ : Array Int} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
+  simp [prod_append]
+
+theorem prod_reverse_int (xs : Array Int) : xs.reverse.prod = xs.prod := by
+  simp [prod_reverse]
+
+theorem prod_eq_foldl_int {xs : Array Int} : xs.prod = xs.foldl (init := 1) (· * ·) := by
+  simp only [foldl_eq_foldr_reverse, Int.mul_comm, ← prod_eq_foldr, prod_reverse_int]
+
 end Array

src/Init/Data/Array/Lemmas.lean

@@ -3096,13 +3096,13 @@ theorem foldl_eq_foldlM {f : β → α → β} {b} {xs : Array α} {start stop :
 theorem foldr_eq_foldrM {f : α → β → β} {b} {xs : Array α} {start stop : Nat} :
     xs.foldr f b start stop = (xs.foldrM (m := Id) (pure <| f · ·) b start stop).run := rfl
 
-public theorem foldl_eq_foldl_extract {xs : Array α} {f : β → α → β} {init : β} :
+theorem foldl_eq_foldl_extract {xs : Array α} {f : β → α → β} {init : β} :
     xs.foldl (init := init) (start := start) (stop := stop) f =
       (xs.extract start stop).foldl (init := init) f := by
   simp only [foldl_eq_foldlM]
   rw [foldlM_start_stop]
 
-public theorem foldr_eq_foldr_extract {xs : Array α} {f : α → β → β} {init : β} :
+theorem foldr_eq_foldr_extract {xs : Array α} {f : α → β → β} {init : β} :
     xs.foldr (init := init) (start := start) (stop := stop) f =
       (xs.extract stop start).foldr (init := init) f := by
   simp only [foldr_eq_foldrM]
@@ -4380,6 +4380,47 @@ theorem sum_eq_foldl [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
     xs.sum = xs.foldl (init := 0) (· + ·) := by
   simp [← sum_toList, List.sum_eq_foldl]
 
+/-! ### prod -/
+
+@[simp, grind =] theorem prod_empty [Mul α] [One α] : (#[] : Array α).prod = 1 := rfl
+theorem prod_eq_foldr [Mul α] [One α] {xs : Array α} :
+    xs.prod = xs.foldr (init := 1) (· * ·) :=
+  rfl
+
+@[simp, grind =]
+theorem prod_toList [Mul α] [One α] {as : Array α} : as.toList.prod = as.prod := by
+  cases as
+  simp [Array.prod, List.prod]
+
+@[simp, grind =]
+theorem prod_append [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
+    [Std.LawfulLeftIdentity (α := α) (· * ·) 1]
+    {as₁ as₂ : Array α} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
+  simp [← prod_toList, List.prod_append]
+
+@[simp, grind =]
+theorem prod_singleton [Mul α] [One α] [Std.LawfulRightIdentity (· * ·) (1 : α)] {x : α} :
+    #[x].prod = x := by
+  simp [Array.prod_eq_foldr, Std.LawfulRightIdentity.right_id x]
+
+@[simp, grind =]
+theorem prod_push [Mul α] [One α] [Std.Associative (α := α) (· * ·)]
+    [Std.LawfulIdentity (· * ·) (1 : α)] {xs : Array α} {x : α} :
+    (xs.push x).prod = xs.prod * x := by
+  simp [Array.prod_eq_foldr, Std.LawfulRightIdentity.right_id, Std.LawfulLeftIdentity.left_id,
+    ← Array.foldr_assoc]
+
+@[simp, grind =]
+theorem prod_reverse [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
+    [Std.Commutative (α := α) (· * ·)]
+    [Std.LawfulLeftIdentity (α := α) (· * ·) 1] (xs : Array α) : xs.reverse.prod = xs.prod := by
+  simp [← prod_toList, List.prod_reverse]
+
+theorem prod_eq_foldl [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
+    [Std.LawfulIdentity (· * ·) (1 : α)] {xs : Array α} :
+    xs.prod = xs.foldl (init := 1) (· * ·) := by
+  simp [← prod_toList, List.prod_eq_foldl]
+
 theorem foldl_toList_eq_flatMap {l : List α} {acc : Array β}
     {F : Array β → α → Array β} {G : α → List β}
     (H : ∀ acc a, (F acc a).toList = acc.toList ++ G a) :

src/Init/Data/Array/Nat.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Init.Data.Array.MinMax
 import Init.Data.List.Nat.Sum
+import Init.Data.List.Nat.Prod
 import Init.Data.Array.Lemmas
 
 public section
@@ -81,4 +82,24 @@ theorem sum_div_length_le_max_of_max?_eq_some_nat {xs : Array Nat} (h : xs.max?
   simpa [List.max?_toArray, List.sum_toArray] using
     List.sum_div_length_le_max_of_max?_eq_some_nat (by simpa using h)
 
+protected theorem prod_pos_iff_forall_pos_nat {xs : Array Nat} : 0 < xs.prod ↔ ∀ x ∈ xs, 0 < x := by
+  simp [← prod_toList, List.prod_pos_iff_forall_pos_nat]
+
+protected theorem prod_eq_zero_iff_exists_zero_nat {xs : Array Nat} :
+    xs.prod = 0 ↔ ∃ x ∈ xs, x = 0 := by
+  simp [← prod_toList, List.prod_eq_zero_iff_exists_zero_nat]
+
+@[simp] theorem prod_replicate_nat {n : Nat} {a : Nat} : (replicate n a).prod = a ^ n := by
+  rw [← List.toArray_replicate, List.prod_toArray]
+  simp
+
+theorem prod_append_nat {as₁ as₂ : Array Nat} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
+  simp [prod_append]
+
+theorem prod_reverse_nat (xs : Array Nat) : xs.reverse.prod = xs.prod := by
+  simp [prod_reverse]
+
+theorem prod_eq_foldl_nat {xs : Array Nat} : xs.prod = xs.foldl (init := 1) (· * ·) := by
+  simp only [foldl_eq_foldr_reverse, Nat.mul_comm, ← prod_eq_foldr, prod_reverse_nat]
+
 end Array

src/Init/Data/Array/Subarray.lean

@@ -80,7 +80,7 @@ instance : SliceSize (Internal.SubarrayData α) where
   size s := s.internalRepresentation.stop - s.internalRepresentation.start
 
 @[grind =, suggest_for Subarray.size]
-public theorem size_eq {xs : Subarray α} :
+theorem size_eq {xs : Subarray α} :
     xs.size = xs.stop - xs.start := by
   simp [Std.Slice.size, SliceSize.size, start, stop]
 

src/Init/Data/Int/Compare.lean

@@ -74,7 +74,7 @@ protected theorem isGE_compare {a b : Int} :
   rw [← Int.compare_swap, Ordering.isGE_swap]
   exact Int.isLE_compare
 
-public instance : Std.LawfulOrderOrd Int where
+instance : Std.LawfulOrderOrd Int where
   isLE_compare _ _ := Int.isLE_compare
   isGE_compare _ _ := Int.isGE_compare
 

src/Init/Data/Iterators/Basic.lean

@@ -42,29 +42,29 @@ The conversion functions {name (scope := "Init.Data.Iterators.Basic")}`Shrink.de
 {name (scope := "Init.Data.Iterators.Basic")}`Shrink.inflate` form an equivalence between
 {name}`α` and {lean}`Shrink α`, but this equivalence is intentionally not definitional.
 -/
-public def Shrink (α : Type u) : Type u := Internal.idOpaque.1 α
+def Shrink (α : Type u) : Type u := Internal.idOpaque.1 α
 
 /-- Converts elements of {name}`α` into elements of {lean}`Shrink α`. -/
 @[always_inline]
-public def Shrink.deflate {α} (x : α) : Shrink α :=
+def Shrink.deflate {α} (x : α) : Shrink α :=
   cast (by simp [Shrink, Internal.idOpaque.property]) x
 
 /-- Converts elements of {lean}`Shrink α` into elements of {name}`α`. -/
 @[always_inline]
-public def Shrink.inflate {α} (x : Shrink α) : α :=
+def Shrink.inflate {α} (x : Shrink α) : α :=
   cast (by simp [Shrink, Internal.idOpaque.property]) x
 
 @[simp, grind =]
-public theorem Shrink.deflate_inflate {α} {x : Shrink α} :
+theorem Shrink.deflate_inflate {α} {x : Shrink α} :
     Shrink.deflate x.inflate = x := by
   simp [deflate, inflate]
 
 @[simp, grind =]
-public theorem Shrink.inflate_deflate {α} {x : α} :
+theorem Shrink.inflate_deflate {α} {x : α} :
     (Shrink.deflate x).inflate = x := by
   simp [deflate, inflate]
 
-public theorem Shrink.inflate_inj {α} {x y : Shrink α} :
+theorem Shrink.inflate_inj {α} {x y : Shrink α} :
     x.inflate = y.inflate ↔ x = y := by
   apply Iff.intro
   · intro h
@@ -72,7 +72,7 @@ public theorem Shrink.inflate_inj {α} {x y : Shrink α} :
   · rintro rfl
     rfl
 
-public theorem Shrink.deflate_inj {α} {x y : α} :
+theorem Shrink.deflate_inj {α} {x y : α} :
     Shrink.deflate x = Shrink.deflate y ↔ x = y := by
   apply Iff.intro
   · intro h

src/Init/Data/Iterators/Combinators/Monadic/Append.lean

@@ -190,7 +190,7 @@ def Append.instFinitenessRelation [Monad m] [Iterator α₁ m β] [Iterator α
       exact IterM.TerminationMeasures.Finite.rel_of_skip ‹_›
 
 @[no_expose]
-public instance Append.instFinite [Monad m] [Iterator α₁ m β] [Iterator α₂ m β]
+instance Append.instFinite [Monad m] [Iterator α₁ m β] [Iterator α₂ m β]
     [Finite α₁ m] [Finite α₂ m] : Finite (Append α₁ α₂ m β) m :=
   .of_finitenessRelation instFinitenessRelation
 

src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean

@@ -271,7 +271,7 @@ private def optionPelim' {α : Type u_1} (t : Option α) {β :  Sort u_2}
 
 /--
 Inserts an `Option` case distinction after the first computation of a call to `MonadAttach.pbind`.
-This lemma is useful for simplifying the second computation, which often involes `match` expressions
+This lemma is useful for simplifying the second computation, which often involves `match` expressions
 that use `pbind`'s proof term.
 -/
 private theorem pbind_eq_pbind_if_isSome [Monad m] [MonadAttach m] (x : m (Option α)) (f : (_ : _) → _ → m β) :

src/Init/Data/List/Basic.lean

@@ -282,6 +282,7 @@ The lexicographic order with respect to `lt` is:
 * `as.lex [] = false` is `false`
 * `(a :: as).lex (b :: bs)` is true if `lt a b` or `a == b` and `lex lt as bs` is true.
 -/
+@[specialize]
 def lex [BEq α] (l₁ l₂ : List α) (lt : α → α → Bool := by exact (· < ·)) : Bool :=
   match l₁, l₂ with
   | [],      _ :: _  => true
@@ -1004,6 +1005,7 @@ Examples:
  * `[8, 3, 2, 4, 2, 7, 4].dropWhile (· < 4) = [8, 3, 2, 4, 2, 7, 4]`
  * `[8, 3, 2, 4, 2, 7, 4].dropWhile (· < 100) = []`
 -/
+@[specialize]
 def dropWhile (p : α → Bool) : List α → List α
   | []   => []
   | a::l => match p a with
@@ -1460,9 +1462,11 @@ Examples:
 ["circle", "square", "triangle"]
 ```
 -/
+@[inline]
 def modifyTailIdx (l : List α) (i : Nat) (f : List α → List α) : List α :=
   go i l
 where
+  @[specialize]
   go : Nat → List α → List α
   | 0, l => f l
   | _+1, [] => []
@@ -1498,6 +1502,7 @@ Examples:
  * `[1, 2, 3].modify 2 (· * 10) = [1, 2, 30]`
  * `[1, 2, 3].modify 3 (· * 10) = [1, 2, 3]`
 -/
+@[inline]
 def modify (l : List α) (i : Nat) (f : α → α) : List α :=
   l.modifyTailIdx i (modifyHead f)
 
@@ -1604,6 +1609,7 @@ Examples:
 * `[7, 6, 5, 8, 1, 2, 6].find? (· < 5) = some 1`
 * `[7, 6, 5, 8, 1, 2, 6].find? (· < 1) = none`
 -/
+@[specialize]
 def find? (p : α → Bool) : List α → Option α
   | []    => none
   | a::as => match p a with
@@ -1626,6 +1632,7 @@ Examples:
  * `[7, 6, 5, 8, 1, 2, 6].findSome? (fun x => if x < 5 then some (10 * x) else none) = some 10`
  * `[7, 6, 5, 8, 1, 2, 6].findSome? (fun x => if x < 1 then some (10 * x) else none) = none`
 -/
+@[specialize]
 def findSome? (f : α → Option β) : List α → Option β
   | []    => none
   | a::as => match f a with
@@ -1649,6 +1656,7 @@ Examples:
 * `[7, 6, 5, 8, 1, 2, 6].findRev? (· < 5) = some 2`
 * `[7, 6, 5, 8, 1, 2, 6].findRev? (· < 1) = none`
 -/
+@[specialize]
 def findRev? (p : α → Bool) : List α → Option α
   | []    => none
   | a::as => match findRev? p as with
@@ -1667,6 +1675,7 @@ Examples:
  * `[7, 6, 5, 8, 1, 2, 6].findSomeRev? (fun x => if x < 5 then some (10 * x) else none) = some 20`
  * `[7, 6, 5, 8, 1, 2, 6].findSomeRev? (fun x => if x < 1 then some (10 * x) else none) = none`
 -/
+@[specialize]
 def findSomeRev? (f : α → Option β) : List α → Option β
   | []    => none
   | a::as => match findSomeRev? f as with
@@ -1717,9 +1726,11 @@ Examples:
 * `[7, 6, 5, 8, 1, 2, 6].findIdx (· < 5) = some 4`
 * `[7, 6, 5, 8, 1, 2, 6].findIdx (· < 1) = none`
 -/
+@[inline]
 def findIdx? (p : α → Bool) (l : List α) : Option Nat :=
   go l 0
 where
+  @[specialize]
   go : List α → Nat → Option Nat
   | [], _ => none
   | a :: l, i => if p a then some i else go l (i + 1)
@@ -1750,6 +1761,7 @@ Examples:
 @[inline] def findFinIdx? (p : α → Bool) (l : List α) : Option (Fin l.length) :=
   go l 0 (by simp)
 where
+  @[specialize]
   go : (l' : List α) → (i : Nat) → (h : l'.length + i = l.length) → Option (Fin l.length)
   | [], _, _ => none
   | a :: l, i, h =>
@@ -1886,7 +1898,7 @@ Examples:
 * `[2, 4, 5, 6].any (· % 2 = 0) = true`
 * `[2, 4, 5, 6].any (· % 2 = 1) = true`
 -/
-@[suggest_for List.some]
+@[suggest_for List.some, specialize]
 def any : (l : List α) → (p : α → Bool) → Bool
   | [], _ => false
   | h :: t, p => p h || any t p
@@ -1906,7 +1918,7 @@ Examples:
 * `[2, 4, 6].all (· % 2 = 0) = true`
 * `[2, 4, 5, 6].all (· % 2 = 0) = false`
 -/
-@[suggest_for List.every]
+@[suggest_for List.every, specialize]
 def all : List α → (α → Bool) → Bool
   | [], _ => true
   | h :: t, p => p h && all t p
@@ -2007,6 +2019,7 @@ Examples:
 * `[1, 2, 3].zipWithAll Prod.mk [5, 6] = [(some 1, some 5), (some 2, some 6), (some 3, none)]`
 * `[x₁, x₂].zipWithAll f [y] = [f (some x₁) (some y), f (some x₂) none]`
 -/
+@[specialize]
 def zipWithAll (f : Option α → Option β → γ) : List α → List β → List γ
   | [], bs => bs.map fun b => f none (some b)
   | a :: as, [] => (a :: as).map fun a => f (some a) none
@@ -2056,6 +2069,20 @@ def sum {α} [Add α] [Zero α] : List α → α :=
 @[simp, grind =] theorem sum_cons [Add α] [Zero α] {a : α} {l : List α} : (a::l).sum = a + l.sum := rfl
 theorem sum_eq_foldr [Add α] [Zero α] {l : List α} : l.sum = l.foldr (· + ·) 0 := rfl
 
+/--
+Computes the product of the elements of a list.
+
+Examples:
+ * `[a, b, c].prod = a * (b * (c * 1))`
+ * `[1, 2, 5].prod = 10`
+-/
+def prod {α} [Mul α] [One α] : List α → α :=
+  foldr (· * ·) 1
+
+@[simp, grind =] theorem prod_nil [Mul α] [One α] : ([] : List α).prod = 1 := rfl
+@[simp, grind =] theorem prod_cons [Mul α] [One α] {a : α} {l : List α} : (a::l).prod = a * l.prod := rfl
+theorem prod_eq_foldr [Mul α] [One α] {l : List α} : l.prod = l.foldr (· * ·) 1 := rfl
+
 /-! ### range -/
 
 /--

src/Init/Data/List/Control.lean

@@ -444,8 +444,8 @@ theorem findM?_eq_findSomeM? [Monad m] [LawfulMonad m] {p : α → m Bool} {as :
     intro b
     cases b <;> simp
 
-@[inline, expose] protected def forIn' {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : List α) (init : β) (f : (a : α) → a ∈ as → β → m (ForInStep β)) : m β :=
-  let rec @[specialize] loop : (as' : List α) → (b : β) → Exists (fun bs => bs ++ as' = as) → m β
+@[inline, expose] protected def forIn' {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : @& List α) (init : β) (f : (a : α) → a ∈ as → β → m (ForInStep β)) : m β :=
+  let rec @[specialize] loop : (as' : @& List α) → (b : β) → Exists (fun bs => bs ++ as' = as) → m β
     | [], b, _    => pure b
     | a::as', b, h => do
       have : a ∈ as := by

src/Init/Data/List/Int.lean

@@ -7,3 +7,4 @@ module
 
 prelude
 public import Init.Data.List.Int.Sum
+public import Init.Data.List.Int.Prod

src/Init/Data/List/Int/Prod.lean

@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+
+prelude
+import Init.Data.List.Lemmas
+import Init.Data.Int.Lemmas
+public import Init.Data.Int.Pow
+public import Init.Data.List.Basic
+
+public section
+
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
+namespace List
+
+@[simp]
+theorem prod_replicate_int {n : Nat} {a : Int} : (replicate n a).prod = a ^ n := by
+  induction n <;> simp_all [replicate_succ, Int.pow_succ, Int.mul_comm]
+
+theorem prod_append_int {l₁ l₂ : List Int} : (l₁ ++ l₂).prod = l₁.prod * l₂.prod := by
+  simp [prod_append]
+
+theorem prod_reverse_int (xs : List Int) : xs.reverse.prod = xs.prod := by
+  simp [prod_reverse]
+
+end List

src/Init/Data/List/Lemmas.lean

@@ -1878,6 +1878,24 @@ theorem sum_reverse [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
     simp_all [sum_append, Std.Commutative.comm (α := α) _ 0,
       Std.LawfulLeftIdentity.left_id, Std.Commutative.comm]
 
+@[simp, grind =]
+theorem prod_append [Mul α] [One α] [Std.LawfulLeftIdentity (α := α) (· * ·) 1]
+    [Std.Associative (α := α) (· * ·)] {l₁ l₂ : List α} : (l₁ ++ l₂).prod = l₁.prod * l₂.prod := by
+  induction l₁ generalizing l₂ <;> simp_all [Std.Associative.assoc, Std.LawfulLeftIdentity.left_id]
+
+@[simp, grind =]
+theorem prod_singleton [Mul α] [One α] [Std.LawfulRightIdentity (· * ·) (1 : α)] {x : α} :
+    [x].prod = x := by
+  simp [List.prod_eq_foldr, Std.LawfulRightIdentity.right_id x]
+
+@[simp, grind =]
+theorem prod_reverse [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
+    [Std.Commutative (α := α) (· * ·)]
+    [Std.LawfulLeftIdentity (α := α) (· * ·) 1] (xs : List α) : xs.reverse.prod = xs.prod := by
+  induction xs <;>
+    simp_all [prod_append, Std.Commutative.comm (α := α) _ 1,
+      Std.LawfulLeftIdentity.left_id, Std.Commutative.comm]
+
 /-! ### concat
 
 Note that `concat_eq_append` is a `@[simp]` lemma, so `concat` should usually not appear in goals.
@@ -2784,6 +2802,11 @@ theorem sum_eq_foldl [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
     xs.sum = xs.foldl (init := 0) (· + ·) := by
   simp [sum_eq_foldr, foldl_eq_apply_foldr, Std.LawfulLeftIdentity.left_id]
 
+theorem prod_eq_foldl [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
+    [Std.LawfulIdentity (· * ·) (1 : α)] {xs : List α} :
+    xs.prod = xs.foldl (init := 1) (· * ·) := by
+  simp [prod_eq_foldr, foldl_eq_apply_foldr, Std.LawfulLeftIdentity.left_id]
+
 -- The argument `f : α₁ → α₂` is intentionally explicit, as it is sometimes not found by unification.
 theorem foldl_hom (f : α₁ → α₂) {g₁ : α₁ → β → α₁} {g₂ : α₂ → β → α₂} {l : List β} {init : α₁}
     (H : ∀ x y, g₂ (f x) y = f (g₁ x y)) : l.foldl g₂ (f init) = f (l.foldl g₁ init) := by

src/Init/Data/List/MinMax.lean

@@ -37,7 +37,7 @@ open Nat
 @[simp, grind =] theorem min?_nil [Min α] : ([] : List α).min? = none := rfl
 
 @[simp, grind =]
-public theorem min?_singleton [Min α] {x : α} : [x].min? = some x :=
+theorem min?_singleton [Min α] {x : α} : [x].min? = some x :=
   (rfl)
 
 -- We don't put `@[simp]` on `min?_cons'`,
@@ -52,7 +52,7 @@ theorem min?_cons' [Min α] {xs : List α} : (x :: xs).min? = some (foldl min x
   cases xs <;> simp [min?]
 
 @[simp, grind =]
-public theorem isSome_min?_iff [Min α] {xs : List α} : xs.min?.isSome ↔ xs ≠ [] := by
+theorem isSome_min?_iff [Min α] {xs : List α} : xs.min?.isSome ↔ xs ≠ [] := by
   cases xs <;> simp [min?]
 
 @[grind .]
@@ -247,7 +247,7 @@ theorem foldl_min_eq_min [Min α] [Std.IdempotentOp (min : α → α → α)] [S
 @[simp, grind =] theorem max?_nil [Max α] : ([] : List α).max? = none := rfl
 
 @[simp, grind =]
-public theorem max?_singleton [Max α] {x : α} : [x].max? = some x :=
+theorem max?_singleton [Max α] {x : α} : [x].max? = some x :=
   (rfl)
 
 -- We don't put `@[simp]` on `max?_cons'`,
@@ -262,7 +262,7 @@ theorem max?_cons' [Max α] {xs : List α} : (x :: xs).max? = some (foldl max x
   cases xs <;> simp [max?]
 
 @[simp, grind =]
-public theorem isSome_max?_iff [Max α] {xs : List α} : xs.max?.isSome ↔ xs ≠ [] := by
+theorem isSome_max?_iff [Max α] {xs : List α} : xs.max?.isSome ↔ xs ≠ [] := by
   cases xs <;> simp [max?]
 
 @[grind .]

src/Init/Data/List/Nat.lean

@@ -13,6 +13,7 @@ public import Init.Data.List.Nat.Sublist
 public import Init.Data.List.Nat.TakeDrop
 public import Init.Data.List.Nat.Count
 public import Init.Data.List.Nat.Sum
+public import Init.Data.List.Nat.Prod
 public import Init.Data.List.Nat.Erase
 public import Init.Data.List.Nat.Find
 public import Init.Data.List.Nat.BEq

src/Init/Data/List/Nat/Prod.lean

@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+
+prelude
+import Init.Data.List.Lemmas
+public import Init.BinderPredicates
+public import Init.NotationExtra
+import Init.Data.Nat.Lemmas
+
+public section
+
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
+namespace List
+
+protected theorem prod_eq_zero_iff_exists_zero_nat {l : List Nat} : l.prod = 0 ↔ ∃ x ∈ l, x = 0 := by
+  induction l with
+  | nil => simp
+  | cons x xs ih =>
+    simp [Nat.mul_eq_zero, ih, eq_comm (a := (0 : Nat))]
+
+protected theorem prod_pos_iff_forall_pos_nat {l : List Nat} : 0 < l.prod ↔ ∀ x ∈ l, 0 < x := by
+  induction l with
+  | nil => simp
+  | cons x xs ih =>
+    simp only [prod_cons, mem_cons, forall_eq_or_imp, ← ih]
+    constructor
+    · intro h
+      exact ⟨Nat.pos_of_mul_pos_right h, Nat.pos_of_mul_pos_left h⟩
+    · exact fun ⟨hx, hxs⟩ => Nat.mul_pos hx hxs
+
+@[simp]
+theorem prod_replicate_nat {n : Nat} {a : Nat} : (replicate n a).prod = a ^ n := by
+  induction n <;> simp_all [replicate_succ, Nat.pow_succ, Nat.mul_comm]
+
+theorem prod_append_nat {l₁ l₂ : List Nat} : (l₁ ++ l₂).prod = l₁.prod * l₂.prod := by
+  simp [prod_append]
+
+theorem prod_reverse_nat (xs : List Nat) : xs.reverse.prod = xs.prod := by
+  simp [prod_reverse]
+
+theorem prod_eq_foldl_nat {xs : List Nat} : xs.prod = xs.foldl (init := 1) (· * ·) := by
+  simp only [foldl_eq_foldr_reverse, Nat.mul_comm, ← prod_eq_foldr, prod_reverse_nat]
+
+end List

src/Init/Data/List/Perm.lean

@@ -606,6 +606,13 @@ theorem sum_nat {l₁ l₂ : List Nat} (h : l₁ ~ l₂) : l₁.sum = l₂.sum :
   | swap => simpa [List.sum_cons] using Nat.add_left_comm ..
   | trans _ _ ih₁ ih₂ => simp [ih₁, ih₂]
 
+theorem prod_nat {l₁ l₂ : List Nat} (h : l₁ ~ l₂) : l₁.prod = l₂.prod := by
+  induction h with
+  | nil => simp
+  | cons _ _ ih => simp [ih]
+  | swap => simpa [List.prod_cons] using Nat.mul_left_comm ..
+  | trans _ _ ih₁ ih₂ => simp [ih₁, ih₂]
+
 theorem all_eq {l₁ l₂ : List α} {f : α → Bool} (hp : l₁.Perm l₂) : l₁.all f = l₂.all f := by
   rw [Bool.eq_iff_iff]; simp [hp.mem_iff]
 
@@ -615,6 +622,9 @@ theorem any_eq {l₁ l₂ : List α} {f : α → Bool} (hp : l₁.Perm l₂) : l
 grind_pattern Perm.sum_nat => l₁ ~ l₂, l₁.sum
 grind_pattern Perm.sum_nat => l₁ ~ l₂, l₂.sum
 
+grind_pattern Perm.prod_nat => l₁ ~ l₂, l₁.prod
+grind_pattern Perm.prod_nat => l₁ ~ l₂, l₂.prod
+
 end Perm
 
 end List

src/Init/Data/List/ToArray.lean

@@ -213,6 +213,9 @@ theorem forM_toArray [Monad m] (l : List α) (f : α → m PUnit) :
 @[simp, grind =] theorem sum_toArray [Add α] [Zero α] (l : List α) : l.toArray.sum = l.sum := by
   simp [Array.sum, List.sum]
 
+@[simp, grind =] theorem prod_toArray [Mul α] [One α] (l : List α) : l.toArray.prod = l.prod := by
+  simp [Array.prod, List.prod]
+
 @[simp, grind =] theorem append_toArray (l₁ l₂ : List α) :
     l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray := by
   apply ext'

src/Init/Data/Nat/Compare.lean

@@ -70,7 +70,7 @@ protected theorem isGE_compare {a b : Nat} :
   rw [← Nat.compare_swap, Ordering.isGE_swap]
   exact Nat.isLE_compare
 
-public instance : Std.LawfulOrderOrd Nat where
+instance : Std.LawfulOrderOrd Nat where
   isLE_compare _ _ := Nat.isLE_compare
   isGE_compare _ _ := Nat.isGE_compare
 

src/Init/Data/Nat/Gcd.lean

@@ -60,7 +60,7 @@ theorem gcd_def (x y : Nat) : gcd x y = if x = 0 then y else gcd (y % x) x := by
   cases n with
   | zero => simp
   | succ n =>
-    -- `simp [gcd_succ]` produces an invalid term unless `gcd_succ` is proved with `id rfl` instead
+    -- `simp [gcd_succ]` produces an invalid term unless `gcd_succ` is proved with `(rfl)` instead
     rw [gcd_succ]
     exact gcd_zero_left _
 instance : Std.LawfulIdentity gcd 0 where

src/Init/Data/Option/Attach.lean

@@ -444,7 +444,7 @@ instance : MonadAttach Option where
   CanReturn x a := x = some a
   attach x := x.attach
 
-public instance : LawfulMonadAttach Option where
+instance : LawfulMonadAttach Option where
   map_attach {α} x := by simp [MonadAttach.attach]
   canReturn_map_imp {α P x a} := by
     cases x
@@ -455,7 +455,7 @@ end Option
 
 namespace OptionT
 
-public instance [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] :
+instance [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] :
     WeaklyLawfulMonadAttach (OptionT m) where
   map_attach {α} x := by
     apply OptionT.ext
@@ -466,7 +466,7 @@ public instance [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAtta
     | ⟨some a, _⟩ => simp [OptionT.pure, OptionT.mk]
     | ⟨none, _⟩ => simp
 
-public instance [Monad m] [MonadAttach m] [LawfulMonad m] [LawfulMonadAttach m] :
+instance [Monad m] [MonadAttach m] [LawfulMonad m] [LawfulMonadAttach m] :
     LawfulMonadAttach (OptionT m) where
   canReturn_map_imp {α P x a} h := by
     simp only [MonadAttach.CanReturn, OptionT.run_map] at h

src/Init/Data/Order/LemmasExtra.lean

@@ -152,7 +152,7 @@ public theorem max_eq_if_isGE_compare {α : Type u} [Ord α] [LE α] {_ : Max α
     {a b : α} : max a b = if (compare a b).isGE then a else b := by
   open Classical in simp [max_eq_if, isGE_compare]
 
-private theorem min_le_min [LE α] [Min α] [Std.LawfulOrderLeftLeaningMin α] [IsLinearOrder α] (a b : α) : min a b ≤ min b a := by
+theorem min_le_min [LE α] [Min α] [Std.LawfulOrderLeftLeaningMin α] [IsLinearOrder α] (a b : α) : min a b ≤ min b a := by
   apply (LawfulOrderInf.le_min_iff (min a b) b a).2
   rw [And.comm]
   by_cases h : a ≤ b

src/Init/Data/Range/Polymorphic/NatLemmas.lean

@@ -1718,7 +1718,7 @@ theorem toArray_roc_append_toArray_roc {l m n : Nat} (h : l ≤ m) (h' : m ≤ n
 @[simp]
 theorem getElem_toArray_roc {m n i : Nat} (_h : i < (m<...=n).toArray.size) :
     (m<...=n).toArray[i]'_h = m + 1 + i := by
-simp [toArray_roc_eq_toArray_rco]
+  simp [toArray_roc_eq_toArray_rco]
 
 theorem getElem?_toArray_roc {m n i : Nat} :
     (m<...=n).toArray[i]? = if i < n - m then some (m + 1 + i) else none := by

src/Init/Data/Range/Polymorphic/SInt.lean

@@ -248,11 +248,11 @@ instance : HasModel Int8 (BitVec 8) where
   le_iff_encode_le := by simp [LE.le, Int8.le]
   lt_iff_encode_lt := by simp [LT.lt, Int8.lt]
 
-private theorem succ?_eq_minValueSealed {x : Int8} :
+theorem succ?_eq_minValueSealed {x : Int8} :
     UpwardEnumerable.succ? x = if x + 1 = minValueSealed then none else some (x + 1) :=
   (rfl)
 
-private theorem succMany?_eq_maxValueSealed {i : Int8} :
+theorem succMany?_eq_maxValueSealed {i : Int8} :
     UpwardEnumerable.succMany? n i =
       have := i.minValue_le_toInt
       if h : i.toInt + n ≤ maxValueSealed.toInt then some (.ofIntLE _ (by omega) (maxValueSealed_def ▸ h)) else none :=
@@ -605,12 +605,12 @@ theorem minValueSealed_def : minValueSealed = ISize.minValue := (rfl)
 theorem maxValueSealed_def : maxValueSealed = ISize.maxValue := (rfl)
 seal minValueSealed maxValueSealed
 
-private theorem toBitVec_minValueSealed_eq_intMinSealed :
+theorem toBitVec_minValueSealed_eq_intMinSealed :
     minValueSealed.toBitVec = BitVec.Signed.intMinSealed System.Platform.numBits := by
   rw [minValueSealed_def, BitVec.Signed.intMinSealed_def, toBitVec_minValue]
   have := System.Platform.numBits_eq; generalize System.Platform.numBits = a at this ⊢
   rcases this with rfl | rfl <;> rfl
-private theorem toBitVec_maxValueSealed_eq_intMaxSealed :
+theorem toBitVec_maxValueSealed_eq_intMaxSealed :
     maxValueSealed.toBitVec = BitVec.Signed.intMaxSealed System.Platform.numBits := by
   rw [maxValueSealed_def, BitVec.Signed.intMaxSealed_def, toBitVec_maxValue]
   have := System.Platform.numBits_eq; generalize System.Platform.numBits = a at this ⊢

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

@@ -233,7 +233,7 @@ public theorem Subarray.toList_eq {xs : Subarray α} :
   simp [this, ListSlice.toList_eq, lslice]
 
 -- TODO: The current `List.extract_eq_drop_take` should be called `List.extract_eq_take_drop`
-private theorem Std.Internal.List.extract_eq_drop_take' {l : List α} {start stop : Nat} :
+theorem Std.Internal.List.extract_eq_drop_take' {l : List α} {start stop : Nat} :
     l.extract start stop = (l.take stop).drop start := by
   simp [List.take_drop]
   by_cases start ≤ stop

src/Init/Data/String/Decode.lean

@@ -94,7 +94,7 @@ public def String.utf8EncodeCharFast (c : Char) : List UInt8 :=
      (v >>>  6).toUInt8 &&& 0x3f ||| 0x80,
               v.toUInt8 &&& 0x3f ||| 0x80]
 
-private theorem Nat.add_two_pow_eq_or_of_lt {b : Nat} (i : Nat) (b_lt : b < 2 ^ i) (a : Nat) :
+theorem Nat.add_two_pow_eq_or_of_lt {b : Nat} (i : Nat) (b_lt : b < 2 ^ i) (a : Nat) :
     b + 2 ^ i * a = b ||| 2 ^ i * a := by
   rw [Nat.add_comm, Nat.or_comm, Nat.two_pow_add_eq_or_of_lt b_lt]
 
@@ -363,7 +363,7 @@ theorem toBitVec_eq_of_parseFirstByte_eq_threeMore {b : UInt8} (h : parseFirstBy
 public def isInvalidContinuationByte (b : UInt8) : Bool :=
   b &&& 0xc0 != 0x80
 
-theorem isInvalidContinutationByte_eq_false_iff {b : UInt8} :
+theorem isInvalidContinuationByte_eq_false_iff {b : UInt8} :
     isInvalidContinuationByte b = false ↔ b &&& 0xc0 = 0x80 := by
   simp [isInvalidContinuationByte]
 

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

@@ -31,7 +31,7 @@ namespace Slice
 /--
 A list of all positions starting at {name}`p`.
 
-This function is not meant to be used in actual progams. Actual programs should use
+This function is not meant to be used in actual programs. Actual programs should use
 {name}`Slice.positionsFrom` or {name}`Slice.positions`.
 -/
 protected def Model.positionsFrom {s : Slice} (p : s.Pos) : List { p : s.Pos // p ≠ s.endPos } :=
@@ -206,7 +206,7 @@ end Slice
 /--
 A list of all positions starting at {name}`p`.
 
-This function is not meant to be used in actual progams. Actual programs should use
+This function is not meant to be used in actual programs. Actual programs should use
 {name}`Slice.positionsFrom` or {name}`Slice.positions`.
 -/
 protected def Model.positionsFrom {s : String} (p : s.Pos) : List { p : s.Pos // p ≠ s.endPos } :=

src/Init/Data/String/Subslice.lean

@@ -23,7 +23,7 @@ Given a {name}`Slice` {name}`s`, the type {lean}`s.Subslice` is the type of half
 in {name}`s` delineated by a valid position on both sides.
 
 This type is useful to track regions of interest within some larger slice that is also of interest.
-In contrast, {name}`Slice` is used to track regions of interest whithin some larger string that is
+In contrast, {name}`Slice` is used to track regions of interest within some larger string that is
 not or no longer relevant.
 
 Equality on {name}`Subslice` is somewhat better behaved than on {name}`Slice`, but note that there

src/Init/Data/Vector/Basic.lean

@@ -506,6 +506,16 @@ Examples:
 @[inline, expose] def sum [Add α] [Zero α] (xs : Vector α n) : α :=
   xs.toArray.sum
 
+/--
+Computes the product of the elements of a vector.
+
+Examples:
+ * `#v[a, b, c].prod = a * (b * (c * 1))`
+ * `#v[1, 2, 5].prod = 10`
+-/
+@[inline, expose] def prod [Mul α] [One α] (xs : Vector α n) : α :=
+  xs.toArray.prod
+
 /--
 Pad a vector on the left with a given element.
 

src/Init/Data/Vector/Int.lean

@@ -30,4 +30,16 @@ theorem sum_reverse_int (xs : Vector Int n) : xs.reverse.sum = xs.sum := by
 theorem sum_eq_foldl_int {xs : Vector Int n} : xs.sum = xs.foldl (b := 0) (· + ·) := by
   simp only [foldl_eq_foldr_reverse, Int.add_comm, ← sum_eq_foldr, sum_reverse_int]
 
+@[simp] theorem prod_replicate_int {n : Nat} {a : Int} : (replicate n a).prod = a ^ n := by
+  simp [← prod_toArray, Array.prod_replicate_int]
+
+theorem prod_append_int {as₁ as₂ : Vector Int n} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
+  simp [← prod_toArray]
+
+theorem prod_reverse_int (xs : Vector Int n) : xs.reverse.prod = xs.prod := by
+  simp [prod_reverse]
+
+theorem prod_eq_foldl_int {xs : Vector Int n} : xs.prod = xs.foldl (b := 1) (· * ·) := by
+  simp only [foldl_eq_foldr_reverse, Int.mul_comm, ← prod_eq_foldr, prod_reverse_int]
+
 end Vector

src/Init/Data/Vector/Lemmas.lean

@@ -278,6 +278,12 @@ theorem toArray_mk {xs : Array α} (h : xs.size = n) : (Vector.mk xs h).toArray
 @[simp, grind =] theorem sum_toArray [Add α] [Zero α] {xs : Vector α n} :
     xs.toArray.sum = xs.sum := rfl
 
+@[simp] theorem prod_mk [Mul α] [One α] {xs : Array α} (h : xs.size = n) :
+    (Vector.mk xs h).prod = xs.prod := rfl
+
+@[simp, grind =] theorem prod_toArray [Mul α] [One α] {xs : Vector α n} :
+    xs.toArray.prod = xs.prod := rfl
+
 @[simp] theorem eq_mk : xs = Vector.mk as h ↔ xs.toArray = as := by
   cases xs
   simp
@@ -551,6 +557,10 @@ theorem toArray_toList {xs : Vector α n} : xs.toList.toArray = xs.toArray := rf
     xs.toList.sum = xs.sum := by
   rw [← toList_toArray, Array.sum_toList, sum_toArray]
 
+@[simp, grind =] theorem prod_toList [Mul α] [One α] {xs : Vector α n} :
+    xs.toList.prod = xs.prod := by
+  rw [← toList_toArray, Array.prod_toList, prod_toArray]
+
 @[simp] theorem getElem_toList {xs : Vector α n} {i : Nat} (h : i < xs.toList.length) :
     xs.toList[i] = xs[i]'(by simpa using h) := by
   cases xs
@@ -3134,3 +3144,39 @@ theorem sum_eq_foldl [Zero α] [Add α]
     {xs : Vector α n} :
     xs.sum = xs.foldl (b := 0) (· + ·) := by
   simp [← sum_toList, List.sum_eq_foldl]
+
+/-! ### prod -/
+
+@[simp, grind =] theorem prod_empty [Mul α] [One α] : (#v[] : Vector α 0).prod = 1 := rfl
+theorem prod_eq_foldr [Mul α] [One α] {xs : Vector α n} :
+    xs.prod = xs.foldr (b := 1) (· * ·) :=
+  rfl
+
+@[simp, grind =]
+theorem prod_append [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
+    [Std.LeftIdentity (α := α) (· * ·) 1] [Std.LawfulLeftIdentity (α := α) (· * ·) 1]
+    {as₁ as₂ : Vector α n} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
+  simp [← prod_toList, List.prod_append]
+
+@[simp, grind =]
+theorem prod_singleton [Mul α] [One α] [Std.LawfulRightIdentity (· * ·) (1 : α)] {x : α} :
+    #v[x].prod = x := by
+  simp [← prod_toList, Std.LawfulRightIdentity.right_id x]
+
+@[simp, grind =]
+theorem prod_push [Mul α] [One α] [Std.Associative (α := α) (· * ·)]
+    [Std.LawfulIdentity (· * ·) (1 : α)] {xs : Vector α n} {x : α} :
+    (xs.push x).prod = xs.prod * x := by
+  simp [← prod_toArray]
+
+@[simp, grind =]
+theorem prod_reverse [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
+    [Std.Commutative (α := α) (· * ·)]
+    [Std.LawfulLeftIdentity (α := α) (· * ·) 1] (xs : Vector α n) : xs.reverse.prod = xs.prod := by
+  simp [← prod_toList, List.prod_reverse]
+
+theorem prod_eq_foldl [One α] [Mul α]
+    [Std.Associative (α := α) (· * ·)] [Std.LawfulIdentity (· * ·) (1 : α)]
+    {xs : Vector α n} :
+    xs.prod = xs.foldl (b := 1) (· * ·) := by
+  simp [← prod_toList, List.prod_eq_foldl]

src/Init/Data/Vector/Nat.lean

@@ -37,4 +37,23 @@ theorem sum_reverse_nat (xs : Vector Nat n) : xs.reverse.sum = xs.sum := by
 theorem sum_eq_foldl_nat {xs : Vector Nat n} : xs.sum = xs.foldl (b := 0) (· + ·) := by
   simp only [foldl_eq_foldr_reverse, Nat.add_comm, ← sum_eq_foldr, sum_reverse_nat]
 
+protected theorem prod_pos_iff_forall_pos_nat {xs : Vector Nat n} : 0 < xs.prod ↔ ∀ x ∈ xs, 0 < x := by
+  simp [← prod_toArray, Array.prod_pos_iff_forall_pos_nat]
+
+protected theorem prod_eq_zero_iff_exists_zero_nat {xs : Vector Nat n} :
+    xs.prod = 0 ↔ ∃ x ∈ xs, x = 0 := by
+  simp [← prod_toArray, Array.prod_eq_zero_iff_exists_zero_nat]
+
+@[simp] theorem prod_replicate_nat {n : Nat} {a : Nat} : (replicate n a).prod = a ^ n := by
+  simp [← prod_toArray, Array.prod_replicate_nat]
+
+theorem prod_append_nat {as₁ as₂ : Vector Nat n} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
+  simp [← prod_toArray]
+
+theorem prod_reverse_nat (xs : Vector Nat n) : xs.reverse.prod = xs.prod := by
+  simp [prod_reverse]
+
+theorem prod_eq_foldl_nat {xs : Vector Nat n} : xs.prod = xs.foldl (b := 1) (· * ·) := by
+  simp only [foldl_eq_foldr_reverse, Nat.mul_comm, ← prod_eq_foldr, prod_reverse_nat]
+
 end Vector

src/Init/Grind/Ring/Basic.lean

@@ -564,6 +564,28 @@ end Ring
 
 end IsCharP
 
+/--
+`PowIdentity α p` states that `x ^ p = x` holds for all elements of `α`.
+
+The primary source of instances is Fermat's little theorem: for a finite field with `q` elements,
+`x ^ q = x` for every `x`. For `Fin p` or `ZMod p` with prime `p`, this gives `x ^ p = x`.
+
+The `grind` ring solver uses this typeclass to add the relation `x ^ p - x = 0` to the
+Groebner basis, which allows it to reduce high-degree polynomials. Mathlib can provide
+instances for general finite fields via `FiniteField.pow_card`.
+-/
+class PowIdentity (α : Type u) [CommSemiring α] (p : outParam Nat) : Prop where
+  /-- Every element satisfies `x ^ p = x`. -/
+  pow_eq (x : α) : x ^ p = x
+
+namespace PowIdentity
+
+variable [CommSemiring α] [PowIdentity α p]
+
+theorem pow (x : α) : x ^ p = x := pow_eq x
+
+end PowIdentity
+
 open AddCommGroup
 
 theorem no_int_zero_divisors {α : Type u} [IntModule α] [NoNatZeroDivisors α] {k : Int} {a : α}

src/Init/Grind/Ring/Envelope.lean

@@ -193,7 +193,7 @@ theorem mul_assoc (a b c : Q α) : mul (mul a b) c = mul a (mul b c) := by
   simp [Semiring.left_distrib, Semiring.right_distrib]; refine ⟨0, ?_⟩; ac_rfl
 
 theorem mul_one (a : Q α) : mul a (natCast 1) = a := by
-obtain ⟨⟨_, _⟩⟩ := a; simp
+  obtain ⟨⟨_, _⟩⟩ := a; simp
 
 theorem one_mul (a : Q α) : mul (natCast 1) a = a := by
   obtain ⟨⟨_, _⟩⟩ := a; simp

src/Init/GrindInstances/Ring/Fin.lean

@@ -156,6 +156,12 @@ instance [i : NeZero n] : ToInt.Pow (Fin n) (.co 0 n) where
       rw [pow_succ, ToInt.Mul.toInt_mul, ih, ← ToInt.wrap_toInt,
         ← IntInterval.wrap_mul (by simp), Int.pow_succ, ToInt.wrap_toInt]
 
+instance : PowIdentity (Fin 2) 2 where
+  pow_eq x := by
+    match x with
+    | ⟨0, _⟩ => rfl
+    | ⟨1, _⟩ => rfl
+
 end Fin
 
 end Lean.Grind

src/Init/Prelude.lean

@@ -145,7 +145,7 @@ Examples:
 The constant function that ignores its argument.
 
 If `a : α`, then `Function.const β a : β → α` is the “constant function with value `a`”. For all
-arguments `b : β`, `Function.const β a b = a`.
+arguments `b : β`, `Function.const β a b = a`. It is often written directly as `fun _ => a`.
 
 Examples:
  * `Function.const Bool 10 true = 10`
@@ -3754,7 +3754,7 @@ class Functor (f : Type u → Type v) : Type (max (u+1) v) where
   /--
   Mapping a constant function.
 
-  Given `a : α` and `v : f α`, `mapConst a v` is equivalent to `Function.const _ a <$> v`. For some
+  Given `a : α` and `v : f β`, `mapConst a v` is equivalent to `(fun _ => a) <$> v`. For some
   functors, this can be implemented more efficiently; for all other functors, the default
   implementation may be used.
   -/

src/Init/System/IO.lean

@@ -1880,3 +1880,12 @@ lead to undefined behavior.
 -/
 @[extern "lean_runtime_forget"]
 def Runtime.forget (a : α) : BaseIO Unit := return
+
+set_option linter.unusedVariables false in
+/--
+Ensures `a` remains at least alive until the call site by holding a reference to `a`. This can be useful
+for unsafe code (such as an FFI) that relies on a Lean object not being freed until after some point
+in the program. At runtime, this will be a no-op as the C compiler will optimize away this call.
+-/
+@[extern "lean_runtime_hold"]
+def Runtime.hold (a : @& α) : BaseIO Unit := return

src/Lean/AddDecl.lean

@@ -9,6 +9,7 @@ prelude
 public import Lean.Meta.Sorry
 public import Lean.Util.CollectAxioms
 public import Lean.OriginalConstKind
+import Lean.Compiler.MetaAttr
 import all Lean.OriginalConstKind  -- for accessing `privateConstKindsExt`
 
 public section
@@ -208,8 +209,12 @@ where
       catch _ => pure ()
 
 
-def addAndCompile (decl : Declaration) (logCompileErrors : Bool := true) : CoreM Unit := do
+def addAndCompile (decl : Declaration) (logCompileErrors : Bool := true)
+    (markMeta : Bool := false) : CoreM Unit := do
   addDecl decl
+  if markMeta then
+    for n in decl.getNames do
+      modifyEnv (Lean.markMeta · n)
   compileDecl decl (logErrors := logCompileErrors)
 
 end Lean

src/Lean/AuxRecursor.lean

@@ -56,11 +56,11 @@ def markSparseCasesOn (env : Environment) (declName : Name) : Environment :=
   sparseCasesOnExt.tag env declName
 
 /-- Is this a constructor elimination or a sparse casesOn? -/
-public def isSparseCasesOn (env : Environment) (declName : Name) : Bool :=
+def isSparseCasesOn (env : Environment) (declName : Name) : Bool :=
   sparseCasesOnExt.isTagged env declName
 
 /-- Is this a `.casesOn`, a constructor elimination or a sparse casesOn? -/
-public def isCasesOnLike (env : Environment) (declName : Name) : Bool :=
+def isCasesOnLike (env : Environment) (declName : Name) : Bool :=
   isCasesOnRecursor env declName || isSparseCasesOn env declName
 
 /--

src/Lean/Compiler/InitAttr.lean

@@ -54,7 +54,7 @@ unsafe def registerInitAttrUnsafe (attrName : Name) (runAfterImport : Bool) (ref
     descr := "initialization procedure for global references"
     -- We want to run `[init]` in declaration order
     preserveOrder := true
-    getParam := fun declName stx => do
+    getParam := fun declName stx => withoutExporting do
       let decl ← getConstInfo declName
       match (← Attribute.Builtin.getIdent? stx) with
       | some initFnName =>
@@ -149,8 +149,6 @@ def setBuiltinInitAttr (env : Environment) (declName : Name) (initFnName : Name
 def declareBuiltin (forDecl : Name) (value : Expr) : CoreM Unit :=
   -- can always be private, not referenced directly except through emitted C code
   withoutExporting do
-  -- TODO: needs an update-stage0 + prefer_native=true for breaking symbol name
-  withExporting do
     let name ← mkAuxDeclName (kind := `_regBuiltin ++ forDecl)
     let type := mkApp (mkConst `IO) (mkConst `Unit)
     let decl := Declaration.defnDecl { name, levelParams := [], type, value, hints := ReducibilityHints.opaque,

src/Lean/Compiler/LCNF/EmitC.lean

@@ -774,7 +774,7 @@ where
 
 mutual
 
-private partial def emitBasicBlock (code : Code .impure) : EmitM Unit := do
+partial def emitBasicBlock (code : Code .impure) : EmitM Unit := do
   match code with
   | .jp (k := k) .. => emitBasicBlock k
   | .let decl k =>
@@ -896,7 +896,7 @@ where
   emitUnreach : EmitM Unit := do
     emitLn "lean_internal_panic_unreachable();"
 
-private partial def emitJoinPoints (code : Code .impure) : EmitM Unit := do
+partial def emitJoinPoints (code : Code .impure) : EmitM Unit := do
   match code with
   | .jp decl k =>
     emit decl.binderName; emitLn ":"
@@ -906,7 +906,7 @@ private partial def emitJoinPoints (code : Code .impure) : EmitM Unit := do
   | .sset (k := k) .. | .uset (k := k) .. | .oset (k := k) .. => emitJoinPoints k
   | .cases .. | .return .. | .jmp .. | .unreach .. => return ()
 
-private partial def emitCode (code : Code .impure) : EmitM Unit := do
+partial def emitCode (code : Code .impure) : EmitM Unit := do
   withEmitBlock do
     let declared ← declareVars code
     if declared then emitLn ""

src/Lean/Compiler/LCNF/EmitUtil.lean

@@ -12,7 +12,7 @@ import Lean.Compiler.InitAttr
 
 namespace Lean.Compiler.LCNF
 
-private structure CollectUsedDeclsState where
+structure CollectUsedDeclsState where
   visited : NameSet := {}
   localDecls : Array (Decl .impure) := #[]
   extSigs : Array (Signature .impure) := #[]

src/Lean/Compiler/LCNF/InferBorrow.lean

@@ -67,7 +67,7 @@ structure ParamMap where
   The set of fvars that were already annotated as borrowed before arriving at this pass. We try to
   preserve the annotations here if possible.
   -/
-  annoatedBorrows : Std.HashSet FVarId := {}
+  annotatedBorrows : Std.HashSet FVarId := {}
 
 namespace ParamMap
 
@@ -95,7 +95,7 @@ where
         modify fun m =>
           { m with
             map := m.map.insert (.decl decl.name) (initParamsIfNotExported exported decl.params),
-            annoatedBorrows := decl.params.foldl (init := m.annoatedBorrows) fun acc p =>
+            annotatedBorrows := decl.params.foldl (init := m.annotatedBorrows) fun acc p =>
               if p.borrow then acc.insert p.fvarId else acc
           }
         goCode decl.name code
@@ -116,7 +116,7 @@ where
       modify fun m =>
         { m with
           map := m.map.insert (.jp declName decl.fvarId) (initParams decl.params),
-          annoatedBorrows := decl.params.foldl (init := m.annoatedBorrows) fun acc p =>
+          annotatedBorrows := decl.params.foldl (init := m.annotatedBorrows) fun acc p =>
             if p.borrow then acc.insert p.fvarId else acc
         }
       goCode declName decl.value
@@ -286,7 +286,7 @@ where
 
   ownFVar (fvarId : FVarId) (reason : OwnReason) : InferM Unit := do
     unless (← get).owned.contains fvarId do
-      if !reason.isForced && (← get).paramMap.annoatedBorrows.contains fvarId then
+      if !reason.isForced && (← get).paramMap.annotatedBorrows.contains fvarId then
         trace[Compiler.inferBorrow] "user annotation blocked owning {← PP.run <| PP.ppFVar fvarId}: {← reason.toString}"
       else
         trace[Compiler.inferBorrow] "own {← PP.run <| PP.ppFVar fvarId}: {← reason.toString}"

src/Lean/Compiler/LCNF/PassManager.lean

@@ -121,7 +121,7 @@ def mkPerDeclaration (name : Name) (phase : Phase)
   occurrence := occurrence
   phase := phase
   name := name
-  run := fun xs => xs.mapM run
+  run := fun xs => xs.mapM fun decl => do checkSystem "LCNF compiler"; run decl
 
 end Pass
 

src/Lean/Compiler/LCNF/PublicDeclsExt.lean

@@ -29,7 +29,7 @@ public def mkOrderedDeclSetExt : IO (EnvExtension (List Name × NameSet)) :=
 /--
 Set of declarations to be exported to other modules; visibility shared by base/mono/IR phases.
 -/
-private builtin_initialize publicDeclsExt : EnvExtension (List Name × NameSet) ← mkOrderedDeclSetExt
+builtin_initialize publicDeclsExt : EnvExtension (List Name × NameSet) ← mkOrderedDeclSetExt
 
 public def isDeclPublic (env : Environment) (declName : Name) : Bool := Id.run do
   if !env.header.isModule then

src/Lean/Compiler/LCNF/ResetReuse.lean

@@ -28,7 +28,7 @@ inserts addition instructions to attempt to reuse the memory right away instead
 allocator.
 
 For this the paper defines three functions:
-- `R` (called `Decl.insertResetReuse` here) which looks for candidates that might be elligible for
+- `R` (called `Decl.insertResetReuse` here) which looks for candidates that might be eligible for
   reuse. For these variables it invokes `D`.
 - `D` which looks for code regions in which the target variable is dead (i.e. no longer read from),
   it then invokes `S`. If `S` succeeds it inserts a `reset` instruction to match the `reuse`

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

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

src/Lean/Compiler/LCNF/SimpCase.lean

@@ -24,7 +24,7 @@ In particular we perform:
 - folding of the most common cases arm into the default arm if possible
 
 Note: Currently the simplifier still contains almost equivalent simplifications to the ones shown
-here. We know that this causes unforseen behavior and do plan on changing it eventually.
+here. We know that this causes unforeseen behavior and do plan on changing it eventually.
 -/
 
 -- TODO: the following functions are duplicated from simp and should be deleted in simp once we

src/Lean/Compiler/LCNF/ToDecl.lean

@@ -171,7 +171,7 @@ def toDecl (declName : Name) : CompilerM (Decl .pure) := do
     if compiler.ignoreBorrowAnnotation.get (← getOptions) then
       decl := { decl with params := ← decl.params.mapM (·.updateBorrow false) }
     if isExport env decl.name && decl.params.any (·.borrow) then
-      throwError m!" Declaration {decl.name} is marked as `export` but some of its parameters have borrow annotations.\n Consider using `set_option compiler.ignoreBorrowAnnotation true in` to supress the borrow annotations in its type.\n If the declaration is part of an `export`/`extern` pair make sure to also supress the annotations at the `extern` declaration."
+      throwError m!" Declaration {decl.name} is marked as `export` but some of its parameters have borrow annotations.\n Consider using `set_option compiler.ignoreBorrowAnnotation true in` to suppress the borrow annotations in its type.\n If the declaration is part of an `export`/`extern` pair make sure to also suppress the annotations at the `extern` declaration."
     return decl
 
 end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/ToExpr.lean

@@ -142,10 +142,10 @@ partial def Code.toExprM (code : Code pu) : ToExprM Expr := do
     return .letE `dummy (mkConst ``Unit) value body true
 end
 
-public def Code.toExpr (code : Code pu) (xs : Array FVarId := #[]) : Expr :=
+def Code.toExpr (code : Code pu) (xs : Array FVarId := #[]) : Expr :=
   run' code.toExprM xs
 
-public def FunDecl.toExpr (decl : FunDecl pu) (xs : Array FVarId := #[]) : Expr :=
+def FunDecl.toExpr (decl : FunDecl pu) (xs : Array FVarId := #[]) : Expr :=
   run' decl.toExprM xs
 
 end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/ToLCNF.lean

@@ -213,11 +213,22 @@ structure Context where
   -/
   expectedType : Option Expr
 
+/--
+Key for the LCNF translation cache. `ignoreNoncomputable` is part of the key
+because entries cached in irrelevant positions skip the `checkComputable`
+check and must not be reused in relevant positions.
+-/
+structure CacheKey where
+  expr : Expr
+  expectedType? : Option Expr
+  ignoreNoncomputable : Bool
+  deriving BEq, Hashable
+
 structure State where
   /-- Local context containing the original Lean types (not LCNF ones). -/
   lctx : LocalContext := {}
   /-- Cache from Lean regular expression to LCNF argument. -/
-  cache : PHashMap (Expr × Option Expr) (Arg .pure) := {}
+  cache : PHashMap CacheKey (Arg .pure) := {}
   /--
   Determines whether caching has been disabled due to finding a use of
   a constant marked with `never_extract`.
@@ -473,7 +484,9 @@ partial def toLCNF (e : Expr) (eType : Expr) : CompilerM (Code .pure) := do
 where
   visitCore (e : Expr) : M (Arg .pure) := withIncRecDepth do
     let eType? := (← read).expectedType
-    if let some arg := (← get).cache.find? (e, eType?) then
+    let ignoreNoncomputable := (← read).ignoreNoncomputable
+    let key : CacheKey := { expr := e, expectedType? := eType?, ignoreNoncomputable }
+    if let some arg := (← get).cache.find? key then
       return arg
     let r : Arg .pure ← match e with
       | .app ..      => visitApp e
@@ -485,7 +498,7 @@ where
       | .lit lit     => visitLit lit
       | .fvar fvarId => if (← get).toAny.contains fvarId then pure .erased else pure (.fvar fvarId)
       | .forallE .. | .mvar .. | .bvar .. | .sort ..  => unreachable!
-    modify fun s => if s.shouldCache then { s with cache := s.cache.insert (e, eType?) r } else s
+    modify fun s => if s.shouldCache then { s with cache := s.cache.insert key r } else s
     return r
 
   visit (e : Expr) : M (Arg .pure) := withIncRecDepth do

src/Lean/Compiler/ModPkgExt.lean

@@ -37,7 +37,7 @@ public def getStateByIdx? [Inhabited σ] (ext : ModuleEnvExtension σ) (env : En
 
 end ModuleEnvExtension
 
-private initialize modPkgExt : ModuleEnvExtension (Option PkgId) ←
+initialize modPkgExt : ModuleEnvExtension (Option PkgId) ←
   registerModuleEnvExtension (pure none)
 
 /-- Returns the package (if any) of an imported module (by its index). -/

src/Lean/Compiler/NameDemangling.lean

@@ -20,13 +20,13 @@ line parsing. Called from the C runtime via `@[export]` for backtrace display. -
 namespace Lean.Name.Demangle
 
 /-- `String.dropPrefix?` returning a `String` instead of a `Slice`. -/
-private def dropPrefix? (s : String) (pre : String) : Option String :=
+def dropPrefix? (s : String) (pre : String) : Option String :=
   (s.dropPrefix? pre).map (·.toString)
 
-private def isAllDigits (s : String) : Bool :=
+def isAllDigits (s : String) : Bool :=
   !s.isEmpty && s.all (·.isDigit)
 
-private def nameToNameParts (n : Name) : Array NamePart :=
+def nameToNameParts (n : Name) : Array NamePart :=
   go n [] |>.toArray
 where
   go : Name → List NamePart → List NamePart
@@ -34,17 +34,17 @@ where
     | .str pre s, acc => go pre (NamePart.str s :: acc)
     | .num pre n, acc => go pre (NamePart.num n :: acc)
 
-private def namePartsToName (parts : Array NamePart) : Name :=
+def namePartsToName (parts : Array NamePart) : Name :=
   parts.foldl (fun acc p =>
     match p with
     | .str s => acc.mkStr s
     | .num n => acc.mkNum n) .anonymous
 
 /-- Format name parts using `Name.toString` for correct escaping. -/
-private def formatNameParts (comps : Array NamePart) : String :=
+def formatNameParts (comps : Array NamePart) : String :=
   if comps.isEmpty then "" else (namePartsToName comps).toString
 
-private def matchSuffix (c : NamePart) : Option String :=
+def matchSuffix (c : NamePart) : Option String :=
   match c with
   | NamePart.str s =>
     if s == "_redArg" then some "arity↓"
@@ -58,12 +58,12 @@ private def matchSuffix (c : NamePart) : Option String :=
     else none
   | _ => none
 
-private def isSpecIndex (c : NamePart) : Bool :=
+def isSpecIndex (c : NamePart) : Bool :=
   match c with
   | NamePart.str s => (dropPrefix? s "spec_").any isAllDigits
   | _ => false
 
-private def stripPrivate (comps : Array NamePart) (start stop : Nat) :
+def stripPrivate (comps : Array NamePart) (start stop : Nat) :
     Nat × Bool :=
   if stop - start >= 3 && comps[start]? == some (NamePart.str "_private") then
     Id.run do
@@ -75,11 +75,11 @@ private def stripPrivate (comps : Array NamePart) (start stop : Nat) :
   else
     (start, false)
 
-private structure SpecEntry where
+structure SpecEntry where
   name : String
   flags : Array String
 
-private def processSpecContext (comps : Array NamePart) : SpecEntry := Id.run do
+def processSpecContext (comps : Array NamePart) : SpecEntry := Id.run do
   let mut begin_ := 0
   if comps.size >= 3 && comps[0]? == some (NamePart.str "_private") then
     for i in [1:comps.size] do
@@ -99,7 +99,7 @@ private def processSpecContext (comps : Array NamePart) : SpecEntry := Id.run do
       else parts := parts.push c
   { name := formatNameParts parts, flags }
 
-private def postprocessNameParts (components : Array NamePart) : String := Id.run do
+def postprocessNameParts (components : Array NamePart) : String := Id.run do
   if components.isEmpty then return ""
 
   let (privStart, isPrivate) := stripPrivate components 0 components.size
@@ -206,14 +206,14 @@ private def postprocessNameParts (components : Array NamePart) : String := Id.ru
 
   return result
 
-private def demangleBody (body : String) : String :=
+def demangleBody (body : String) : String :=
   let name := Name.demangle body
   postprocessNameParts (nameToNameParts name)
 
 /-- Split a `lp_`-prefixed symbol into (demangled body, package name).
 Tries each underscore as a split point; the first valid split (shortest single-component
 package where the remainder is a valid mangled name) is correct. -/
-private def demangleWithPkg (s : String) : Option (String × String) := do
+def demangleWithPkg (s : String) : Option (String × String) := do
   for ⟨pos, h⟩ in s.positions do
     if pos.get h == '_' && pos ≠ s.startPos then
       let nextPos := pos.next h
@@ -230,12 +230,12 @@ private def demangleWithPkg (s : String) : Option (String × String) := do
         return (demangleBody body, pkgName)
   none
 
-private def stripColdSuffix (s : String) : String × String :=
+def stripColdSuffix (s : String) : String × String :=
   match s.find? ".cold" with
   | some pos => (s.extract s.startPos pos, s.extract pos s.endPos)
   | none => (s, "")
 
-private def demangleCore (s : String) : Option String := do
+def demangleCore (s : String) : Option String := do
   -- _init_l_
   if let some body := dropPrefix? s "_init_l_" then
     if !body.isEmpty then return s!"[init] {demangleBody body}"
@@ -291,17 +291,17 @@ public def demangleSymbol (symbol : String) : Option String := do
   if coldSuffix.isEmpty then return result
   else return s!"{result} {coldSuffix}"
 
-private def skipWhile (s : String) (pos : s.Pos) (pred : Char → Bool) : s.Pos :=
+def skipWhile (s : String) (pos : s.Pos) (pred : Char → Bool) : s.Pos :=
   if h : pos = s.endPos then pos
   else if pred (pos.get h) then skipWhile s (pos.next h) pred
   else pos
 termination_by pos
 
-private def splitAt₂ (s : String) (p₁ p₂ : s.Pos) : String × String × String :=
+def splitAt₂ (s : String) (p₁ p₂ : s.Pos) : String × String × String :=
   (s.extract s.startPos p₁, s.extract p₁ p₂, s.extract p₂ s.endPos)
 
 /-- Extract the symbol from a backtrace line (Linux glibc or macOS format). -/
-private def extractSymbol (line : String) :
+def extractSymbol (line : String) :
     Option (String × String × String) :=
   tryLinux line |>.orElse (fun _ => tryMacOS line)
 where

src/Lean/CoreM.lean

@@ -20,6 +20,8 @@ register_builtin_option diagnostics : Bool := {
   descr    := "collect diagnostic information"
 }
 
+builtin_initialize registerTraceClass `diagnostics
+
 register_builtin_option diagnostics.threshold : Nat := {
   defValue := 20
   descr    := "only diagnostic counters above this threshold are reported by the definitional equality"
@@ -444,10 +446,6 @@ Note that the value of `ctx.initHeartbeats` is ignored and replaced with `IO.get
 @[inline] def CoreM.toIO' (x : CoreM α) (ctx : Context) (s : State) : IO α :=
   (·.1) <$> x.toIO ctx s
 
-/-- withIncRecDepth for a monad `m` such that `[MonadControlT CoreM n]`. -/
-protected def withIncRecDepth [Monad m] [MonadControlT CoreM m] (x : m α) : m α :=
-  controlAt CoreM fun runInBase => withIncRecDepth (runInBase x)
-
 /--
 Throws an internal interrupt exception if cancellation has been requested. The exception is not
 caught by `try catch` but is intended to be caught by `Command.withLoggingExceptions` at the top
@@ -462,6 +460,12 @@ heartbeat tracking (e.g. `SynthInstance`).
     if (← tk.isSet) then
       throwInterruptException
 
+/-- withIncRecDepth for a monad `m` such that `[MonadControlT CoreM n]`.
+Also checks for cancellation, so that recursive elaboration functions
+(inferType, whnf, isDefEq, …) respond promptly to interrupt requests. -/
+protected def withIncRecDepth [Monad m] [MonadControlT CoreM m] (x : m α) : m α :=
+  controlAt CoreM fun runInBase => do checkInterrupted; withIncRecDepth (runInBase x)
+
 register_builtin_option debug.moduleNameAtTimeout : Bool := {
   defValue := true
   descr    := "include module name in deterministic timeout error messages.\nRemark: we set this option to false to increase the stability of our test suite"

src/Lean/Data/JsonRpc.lean

@@ -400,7 +400,7 @@ Namely:
 def parseMessageMetaData (input : String) : Except String MessageMetaData :=
   messageMetaDataParser input |>.run input
 
-public inductive MessageDirection where
+inductive MessageDirection where
   | clientToServer
   | serverToClient
   deriving Inhabited, FromJson, ToJson

src/Lean/Data/PersistentArray.lean

@@ -227,7 +227,7 @@ variable {β : Type v}
 set_option linter.unusedVariables.funArgs false in
 @[specialize]
 partial def forInAux {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] [inh : Inhabited β]
-    (f : α → β → m (ForInStep β)) (n : PersistentArrayNode α) (b : β) : m (ForInStep β) := do
+    (f : α → β → m (ForInStep β)) (n : @&PersistentArrayNode α) (b : β) : m (ForInStep β) := do
   let mut b := b
   match n with
   | leaf vs =>
@@ -243,7 +243,7 @@ partial def forInAux {α : Type u} {β : Type v} {m : Type v → Type w} [Monad
       | ForInStep.yield bNew => b := bNew
     return ForInStep.yield b
 
-@[specialize] protected def forIn (t : PersistentArray α) (init : β) (f : α → β → m (ForInStep β)) : m β := do
+@[specialize] protected def forIn (t : @&PersistentArray α) (init : β) (f : α → β → m (ForInStep β)) : m β := do
   match (← forInAux (inh := ⟨init⟩) f t.root init) with
   | ForInStep.done b  => pure b
   | ForInStep.yield b =>

src/Lean/Data/PersistentHashMap.lean

@@ -153,7 +153,7 @@ partial def findAtAux [BEq α] (keys : Array α) (vals : Array β) (heq : keys.s
     else findAtAux keys vals heq (i+1) k
   else none
 
-partial def findAux [BEq α] : Node α β → USize → α → Option β
+partial def findAux [BEq α] : @&Node α β → USize → α → Option β
   | Node.entries entries, h, k =>
     let j     := (mod2Shift h shift).toNat
     match entries[j]! with
@@ -162,7 +162,7 @@ partial def findAux [BEq α] : Node α β → USize → α → Option β
     | Entry.entry k' v => if k == k' then some v else none
   | Node.collision keys vals heq, _, k => findAtAux keys vals heq 0 k
 
-def find? {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → α → Option β
+def find? {_ : BEq α} {_ : Hashable α} : @&PersistentHashMap α β → α → Option β
   | { root }, k => findAux root (hash k |>.toUSize) k
 
 instance {_ : BEq α} {_ : Hashable α} : GetElem (PersistentHashMap α β) α (Option β) fun _ _ => True where
@@ -184,7 +184,7 @@ partial def findEntryAtAux [BEq α] (keys : Array α) (vals : Array β) (heq : k
     else findEntryAtAux keys vals heq (i+1) k
   else none
 
-partial def findEntryAux [BEq α] : Node α β → USize → α → Option (α × β)
+partial def findEntryAux [BEq α] : @&Node α β → USize → α → Option (α × β)
   | Node.entries entries, h, k =>
     let j     := (mod2Shift h shift).toNat
     match entries[j]! with
@@ -193,7 +193,7 @@ partial def findEntryAux [BEq α] : Node α β → USize → α → Option (α
     | Entry.entry k' v => if k == k' then some (k', v) else none
   | Node.collision keys vals heq, _, k => findEntryAtAux keys vals heq 0 k
 
-def findEntry? {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → α → Option (α × β)
+def findEntry? {_ : BEq α} {_ : Hashable α} : @&PersistentHashMap α β → α → Option (α × β)
   | { root }, k => findEntryAux root (hash k |>.toUSize) k
 
 partial def findKeyDAtAux [BEq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) (i : Nat) (k : α) (k₀ : α) : α :=
@@ -320,7 +320,7 @@ def foldl {_ : BEq α} {_ : Hashable α} (map : PersistentHashMap α β) (f : σ
   Id.run <| map.foldlM (pure <| f · · ·) init
 
 protected def forIn {_ : BEq α} {_ : Hashable α} [Monad m]
-    (map : PersistentHashMap α β) (init : σ) (f : α × β → σ → m (ForInStep σ)) : m σ := do
+    (map : @&PersistentHashMap α β) (init : σ) (f : α × β → σ → m (ForInStep σ)) : m σ := do
   let intoError : ForInStep σ → Except σ σ
   | .done s => .error s
   | .yield s => .ok s

src/Lean/Data/Trie.lean

@@ -131,9 +131,9 @@ partial def find? (t : Trie α) (s : String) : Option α :=
   loop 0 t
 
 /-- Returns an `Array` of all values in the trie, in no particular order. -/
-partial def values (t : Trie α) : Array α := go t |>.run #[] |>.2
+partial def values (t : @&Trie α) : Array α := go t |>.run #[] |>.2
   where
-    go : Trie α → StateM (Array α) Unit
+    go : @&Trie α → StateM (Array α) Unit
       | leaf a? => do
         if let some a := a? then
           modify (·.push a)

src/Lean/DocString/Markdown.lean

@@ -43,14 +43,14 @@ public structure State where
   /-- Footnotes -/
   footnotes : Array (String × String) := #[]
 
-private def combineBlocks (prior current : String) :=
+def combineBlocks (prior current : String) :=
   if prior.isEmpty then current
   else if current.isEmpty then prior
   else if prior.endsWith "\n\n" then prior ++ current
   else if prior.endsWith "\n" then prior ++ "\n" ++ current
   else prior ++ "\n\n" ++ current
 
-private def State.endBlock (state : State) : State :=
+def State.endBlock (state : State) : State :=
   { state with
     priorBlocks :=
       combineBlocks state.priorBlocks state.currentBlock ++
@@ -60,13 +60,13 @@ private def State.endBlock (state : State) : State :=
     footnotes := #[]
   }
 
-private def State.render (state : State) : String :=
+def State.render (state : State) : String :=
   state.endBlock.priorBlocks
 
-private def State.push (state : State) (txt : String) : State :=
+def State.push (state : State) (txt : String) : State :=
   { state with currentBlock := state.currentBlock ++ txt }
 
-private def State.endsWith (state : State) (txt : String) : Bool :=
+def State.endsWith (state : State) (txt : String) : Bool :=
   state.currentBlock.endsWith txt || (state.currentBlock.isEmpty && state.priorBlocks.endsWith txt)
 
 end MarkdownM
@@ -150,7 +150,7 @@ public class MarkdownBlock (i : Type u) (b : Type v) where
 public instance : MarkdownBlock i Empty where
   toMarkdown := nofun
 
-private def escape (s : String) : String := Id.run do
+def escape (s : String) : String := Id.run do
   let mut s' := ""
   let mut iter := s.startPos
   while h : ¬iter.IsAtEnd do
@@ -163,7 +163,7 @@ private def escape (s : String) : String := Id.run do
 where
   isSpecial c := "*_`-+.!<>[]{}()#".any (· == c)
 
-private def quoteCode (str : String) : String := Id.run do
+def quoteCode (str : String) : String := Id.run do
   let mut longest := 0
   let mut current := 0
   let mut iter := str.startPos
@@ -179,7 +179,7 @@ private def quoteCode (str : String) : String := Id.run do
   let str := if str.startsWith "`" || str.endsWith "`" then " " ++ str ++ " " else str
   backticks ++ str ++ backticks
 
-private partial def trimLeft (inline : Inline i) : (String × Inline i) := go [inline]
+partial def trimLeft (inline : Inline i) : (String × Inline i) := go [inline]
 where
   go : List (Inline i) → String × Inline i
     | [] => ("", .empty)
@@ -194,7 +194,7 @@ where
     | .concat xs :: more => go (xs.toList ++ more)
     | here :: more => ("", here ++ .concat more.toArray)
 
-private partial def trimRight (inline : Inline i) : (Inline i × String) := go [inline]
+partial def trimRight (inline : Inline i) : (Inline i × String) := go [inline]
 where
   go : List (Inline i) → Inline i × String
     | [] => (.empty, "")
@@ -209,13 +209,13 @@ where
     | .concat xs :: more => go (xs.reverse.toList ++ more)
     | here :: more => (.concat more.toArray.reverse ++ here, "")
 
-private def trim (inline : Inline i) : (String × Inline i × String) :=
+def trim (inline : Inline i) : (String × Inline i × String) :=
   let (pre, more) := trimLeft inline
   let (mid, post) := trimRight more
   (pre, mid, post)
 
 open MarkdownM in
-private partial def inlineMarkdown [MarkdownInline i] : Inline i → MarkdownM Unit
+partial def inlineMarkdown [MarkdownInline i] : Inline i → MarkdownM Unit
   | .text s =>
     push (escape s)
   | .linebreak s => do
@@ -271,7 +271,7 @@ private partial def inlineMarkdown [MarkdownInline i] : Inline i → MarkdownM U
 public instance [MarkdownInline i] : ToMarkdown (Inline i) where
   toMarkdown inline := private inlineMarkdown inline
 
-private def quoteCodeBlock (indent : Nat) (str : String) : String := Id.run do
+def quoteCodeBlock (indent : Nat) (str : String) : String := Id.run do
   let mut longest := 2
   let mut current := 0
   let mut iter := str.startPos
@@ -292,7 +292,7 @@ private def quoteCodeBlock (indent : Nat) (str : String) : String := Id.run do
   backticks ++ "\n" ++ out ++ backticks ++ "\n"
 
 open MarkdownM in
-private partial def blockMarkdown [MarkdownInline i] [MarkdownBlock i b] : Block i b → MarkdownM Unit
+partial def blockMarkdown [MarkdownInline i] [MarkdownBlock i b] : Block i b → MarkdownM Unit
   | .para xs => do
     for i in xs do
       ToMarkdown.toMarkdown i
@@ -345,7 +345,7 @@ public instance [MarkdownInline i] [MarkdownBlock i b] : ToMarkdown (Block i b)
 
 open MarkdownM in
 open ToMarkdown in
-private partial def partMarkdown [MarkdownInline i] [MarkdownBlock i b] (level : Nat) (part : Part i b p) : MarkdownM Unit := do
+partial def partMarkdown [MarkdownInline i] [MarkdownBlock i b] (level : Nat) (part : Part i b p) : MarkdownM Unit := do
   push ("".pushn '#' (level + 1))
   push " "
   for i in part.title do

src/Lean/DocString/Parser.lean

@@ -18,7 +18,7 @@ open Lean.Doc.Syntax
 local instance : Coe Char ParserFn where
   coe := chFn
 
-private partial def atLeastAux (n : Nat) (p : ParserFn) : ParserFn := fun c s => Id.run do
+partial def atLeastAux (n : Nat) (p : ParserFn) : ParserFn := fun c s => Id.run do
   let iniSz  := s.stackSize
   let iniPos := s.pos
   let mut s  := p c s
@@ -30,7 +30,7 @@ private partial def atLeastAux (n : Nat) (p : ParserFn) : ParserFn := fun c s =>
     s := s.mkNode nullKind iniSz
   atLeastAux (n - 1) p c s
 
-private def atLeastFn (n : Nat) (p : ParserFn) : ParserFn := fun c s =>
+def atLeastFn (n : Nat) (p : ParserFn) : ParserFn := fun c s =>
   let iniSz  := s.stackSize
   let s := atLeastAux n p c s
   s.mkNode nullKind iniSz
@@ -40,9 +40,9 @@ A parser that does nothing.
 -/
 public def skipFn : ParserFn := fun _ s => s
 
-private def eatSpaces := takeWhileFn (· == ' ')
+def eatSpaces := takeWhileFn (· == ' ')
 
-private def repFn : Nat → ParserFn → ParserFn
+def repFn : Nat → ParserFn → ParserFn
   | 0, _ => skipFn
   | n+1, p => p >> repFn n p
 
@@ -55,7 +55,7 @@ partial def satisfyFn' (p : Char → Bool)
   else if p (c.get' i h) then s.next' c i h
   else s.mkUnexpectedError errorMsg
 
-private partial def atMostAux (n : Nat) (p : ParserFn) (msg : String) : ParserFn :=
+partial def atMostAux (n : Nat) (p : ParserFn) (msg : String) : ParserFn :=
   fun c s => Id.run do
     let iniSz  := s.stackSize
     let iniPos := s.pos
@@ -70,13 +70,13 @@ private partial def atMostAux (n : Nat) (p : ParserFn) (msg : String) : ParserFn
       s := s.mkNode nullKind iniSz
     atMostAux (n - 1) p msg c s
 
-private def atMostFn (n : Nat) (p : ParserFn) (msg : String) : ParserFn := fun c s =>
+def atMostFn (n : Nat) (p : ParserFn) (msg : String) : ParserFn := fun c s =>
   let iniSz  := s.stackSize
   let s := atMostAux n p msg c s
   s.mkNode nullKind iniSz
 
 /-- Like `satisfyFn`, but allows any escape sequence through -/
-private partial def satisfyEscFn (p : Char → Bool)
+partial def satisfyEscFn (p : Char → Bool)
     (errorMsg : String := "unexpected character") :
     ParserFn := fun c s =>
   let i := s.pos
@@ -89,7 +89,7 @@ private partial def satisfyEscFn (p : Char → Bool)
   else if p (c.get' i h) then s.next' c i h
   else s.mkUnexpectedError errorMsg
 
-private partial def takeUntilEscFn (p : Char → Bool) : ParserFn := fun c s =>
+partial def takeUntilEscFn (p : Char → Bool) : ParserFn := fun c s =>
   let i := s.pos
   if h : c.atEnd i then s
   else if c.get' i h == '\\' then
@@ -100,7 +100,7 @@ private partial def takeUntilEscFn (p : Char → Bool) : ParserFn := fun c s =>
   else if p (c.get' i h) then s
   else takeUntilEscFn p c (s.next' c i h)
 
-private partial def takeWhileEscFn (p : Char → Bool) : ParserFn := takeUntilEscFn (not ∘ p)
+partial def takeWhileEscFn (p : Char → Bool) : ParserFn := takeUntilEscFn (not ∘ p)
 
 /--
 Parses as `p`, but discards the result.
@@ -111,7 +111,7 @@ public def ignoreFn (p : ParserFn) : ParserFn := fun c s =>
   s'.shrinkStack iniSz
 
 
-private def withInfoSyntaxFn (p : ParserFn) (infoP : SourceInfo → ParserFn) : ParserFn := fun c s =>
+def withInfoSyntaxFn (p : ParserFn) (infoP : SourceInfo → ParserFn) : ParserFn := fun c s =>
   let iniSz := s.stxStack.size
   let startPos := s.pos
   let s := p c s
@@ -121,7 +121,7 @@ private def withInfoSyntaxFn (p : ParserFn) (infoP : SourceInfo → ParserFn) :
   let info     := SourceInfo.original leading startPos trailing stopPos
   infoP info c (s.shrinkStack iniSz)
 
-private def unescapeStr (str : String) : String := Id.run do
+def unescapeStr (str : String) : String := Id.run do
   let mut out := ""
   let mut iter := str.startPos
   while h : ¬iter.IsAtEnd do
@@ -135,7 +135,7 @@ private def unescapeStr (str : String) : String := Id.run do
       out := out.push c
   out
 
-private def asStringAux (quoted : Bool) (startPos : String.Pos.Raw) (transform : String → String) :
+def asStringAux (quoted : Bool) (startPos : String.Pos.Raw) (transform : String → String) :
     ParserFn := fun c s =>
   let stopPos  := s.pos
   let leading  := c.mkEmptySubstringAt startPos
@@ -156,26 +156,26 @@ public def asStringFn (p : ParserFn) (quoted := false) (transform : String → S
   if s.hasError then s
   else asStringAux quoted startPos transform c (s.shrinkStack iniSz)
 
-private def checkCol0Fn (errorMsg : String) : ParserFn := fun c s =>
+def checkCol0Fn (errorMsg : String) : ParserFn := fun c s =>
   let pos      := c.fileMap.toPosition s.pos
   if pos.column = 1 then s
   else s.mkError errorMsg
 
-private def _root_.Lean.Parser.ParserContext.currentColumn
+def _root_.Lean.Parser.ParserContext.currentColumn
     (c : ParserContext) (s : ParserState) : Nat :=
   c.fileMap.toPosition s.pos |>.column
 
-private def pushColumn : ParserFn := fun c s =>
+def pushColumn : ParserFn := fun c s =>
   let col := c.fileMap.toPosition s.pos |>.column
   s.pushSyntax <| Syntax.mkLit `column (toString col) (SourceInfo.synthetic s.pos s.pos)
 
-private def guardColumn (p : Nat → Bool) (message : String) : ParserFn := fun c s =>
+def guardColumn (p : Nat → Bool) (message : String) : ParserFn := fun c s =>
   if p (c.currentColumn s) then s else s.mkErrorAt message s.pos
 
-private def guardMinColumn (min : Nat) (description : String := s!"expected column at least {min}") : ParserFn :=
+def guardMinColumn (min : Nat) (description : String := s!"expected column at least {min}") : ParserFn :=
   guardColumn (· ≥ min) description
 
-private def withCurrentColumn (p : Nat → ParserFn) : ParserFn := fun c s =>
+def withCurrentColumn (p : Nat → ParserFn) : ParserFn := fun c s =>
   p (c.currentColumn s) c s
 
 
@@ -183,7 +183,7 @@ private def withCurrentColumn (p : Nat → ParserFn) : ParserFn := fun c s =>
 We can only start a nestable block if we're immediately after a newline followed by a sequence of
 nestable block openers
 -/
-private def onlyBlockOpeners : ParserFn := fun c s =>
+def onlyBlockOpeners : ParserFn := fun c s =>
   let position := c.fileMap.toPosition s.pos
   let lineStart := c.fileMap.lineStart position.line
   let ok : Bool := Id.run do
@@ -206,7 +206,7 @@ private def onlyBlockOpeners : ParserFn := fun c s =>
   if ok then s
   else s.mkErrorAt "beginning of line or sequence of nestable block openers" s.pos
 
-private def nl := satisfyFn (· == '\n') "newline"
+def nl := satisfyFn (· == '\n') "newline"
 
 /--
 Construct a “fake” atom with the given string content and source information.
@@ -225,13 +225,13 @@ current position.
 Normally, atoms are always substrings of the original input; however, Verso's concrete syntax is
 different enough from Lean's that this isn't always a good match.
 -/
-private def fakeAtomHere (str : String) : ParserFn :=
+def fakeAtomHere (str : String) : ParserFn :=
   withInfoSyntaxFn skip.fn (fun info => fakeAtom str (info := info))
 
-private def pushMissing : ParserFn := fun _c s =>
+def pushMissing : ParserFn := fun _c s =>
   s.pushSyntax .missing
 
-private def strFn (str : String) : ParserFn := asStringFn <| fun c s =>
+def strFn (str : String) : ParserFn := asStringFn <| fun c s =>
   let rec go (iter : str.Pos) (s : ParserState) :=
     if h : iter.IsAtEnd then s
     else
@@ -260,10 +260,10 @@ public instance : Ord OrderedListType where
     | .parenAfter, .numDot => .gt
     | .parenAfter, .parenAfter => .eq
 
-private def OrderedListType.all : List OrderedListType :=
+def OrderedListType.all : List OrderedListType :=
   [.numDot, .parenAfter]
 
-private theorem OrderedListType.all_complete : ∀ x : OrderedListType, x ∈ all := by
+theorem OrderedListType.all_complete : ∀ x : OrderedListType, x ∈ all := by
   unfold all; intro x; cases x <;> repeat constructor
 
 /--
@@ -288,40 +288,40 @@ public instance : Ord UnorderedListType where
     | .plus, .plus => .eq
     | .plus, _ => .gt
 
-private def UnorderedListType.all : List UnorderedListType :=
+def UnorderedListType.all : List UnorderedListType :=
   [.asterisk, .dash, .plus]
 
-private theorem UnorderedListType.all_complete : ∀ x : UnorderedListType, x ∈ all := by
+theorem UnorderedListType.all_complete : ∀ x : UnorderedListType, x ∈ all := by
   unfold all; intro x; cases x <;> repeat constructor
 
-private def unorderedListIndicator (type : UnorderedListType) : ParserFn :=
+def unorderedListIndicator (type : UnorderedListType) : ParserFn :=
   asStringFn <|
     match type with
     | .asterisk => chFn '*'
     | .dash => chFn '-'
     | .plus => chFn '+'
 
-private def orderedListIndicator (type : OrderedListType) : ParserFn :=
+def orderedListIndicator (type : OrderedListType) : ParserFn :=
   asStringFn <|
     takeWhile1Fn (·.isDigit) "digits" >>
     match type with
     | .numDot => chFn '.'
     | .parenAfter => chFn ')'
 
-private def blankLine : ParserFn :=
+def blankLine : ParserFn :=
   nodeFn `blankLine <| atomicFn <| asStringFn <| takeWhileFn (· == ' ') >> nl
 
-private def endLine : ParserFn :=
+def endLine : ParserFn :=
   ignoreFn <| atomicFn <| asStringFn <| takeWhileFn (· == ' ') >> eoiFn
 
-private def bullet := atomicFn (go UnorderedListType.all)
+def bullet := atomicFn (go UnorderedListType.all)
 where
   go
     | [] => fun _ s => s.mkError "no list type"
     | [x] => atomicFn (unorderedListIndicator x)
     | x :: xs => atomicFn (unorderedListIndicator x) <|> go xs
 
-private def numbering := atomicFn (go OrderedListType.all)
+def numbering := atomicFn (go OrderedListType.all)
 where
   go
     | [] => fun _ s => s.mkError "no list type"
@@ -374,7 +374,7 @@ public def inlineTextChar : ParserFn := fun c s =>
 /-- Return some inline text up to the next inline opener or the end of
 the line, whichever is first. Always consumes at least one
 logical character on success, taking escaping into account. -/
-private def inlineText : ParserFn :=
+def inlineText : ParserFn :=
   asStringFn (transform := unescapeStr) <| atomicFn inlineTextChar >> manyFn inlineTextChar
 
 /--
@@ -410,23 +410,23 @@ public def val : ParserFn := fun c s =>
     else
       s.mkError "expected identifier, string, or number"
 
-private def withCurrentStackSize (p : Nat → ParserFn) : ParserFn := fun c s =>
+def withCurrentStackSize (p : Nat → ParserFn) : ParserFn := fun c s =>
   p s.stxStack.size c s
 
 /-- Match the character indicated, pushing nothing to the stack in case of success -/
-private def skipChFn (c : Char) : ParserFn :=
+def skipChFn (c : Char) : ParserFn :=
   satisfyFn (· == c) c.toString
 
-private def skipToNewline : ParserFn :=
+def skipToNewline : ParserFn :=
     takeUntilFn (· == '\n')
 
-private def skipToSpace : ParserFn :=
+def skipToSpace : ParserFn :=
     takeUntilFn (· == ' ')
 
-private def skipRestOfLine : ParserFn :=
+def skipRestOfLine : ParserFn :=
     skipToNewline >> (eoiFn <|> nl)
 
-private def skipBlock : ParserFn :=
+def skipBlock : ParserFn :=
   skipToNewline >> manyFn nonEmptyLine >> takeWhileFn (· == '\n')
 where
   nonEmptyLine : ParserFn :=
@@ -444,7 +444,7 @@ public def recoverBlock (p : ParserFn) (final : ParserFn := skipFn) : ParserFn :
     ignoreFn skipBlock >> final
 
 -- Like `recoverBlock` but stores recovered errors at the original error position.
-private def recoverBlockAtErrPos (p : ParserFn) : ParserFn := fun c s =>
+def recoverBlockAtErrPos (p : ParserFn) : ParserFn := fun c s =>
   let s := p c s
   if let some msg := s.errorMsg then
     let errPos := s.pos
@@ -457,36 +457,36 @@ private def recoverBlockAtErrPos (p : ParserFn) : ParserFn := fun c s =>
       recoveredErrors := s.recoveredErrors.push (errPos, s'.stxStack, msg)}
   else s
 
-private def recoverBlockWith (stxs : Array Syntax) (p : ParserFn) : ParserFn :=
+def recoverBlockWith (stxs : Array Syntax) (p : ParserFn) : ParserFn :=
   recoverFn p fun rctx =>
     ignoreFn skipBlock >>
     show ParserFn from
       fun _ s => stxs.foldl (init := s.shrinkStack rctx.initialSize) (·.pushSyntax ·)
 
-private def recoverLine (p : ParserFn) : ParserFn :=
+def recoverLine (p : ParserFn) : ParserFn :=
   recoverFn p fun _ =>
     ignoreFn skipRestOfLine
 
-private def recoverWs (p : ParserFn) : ParserFn :=
+def recoverWs (p : ParserFn) : ParserFn :=
   recoverFn p fun _ =>
     ignoreFn <| takeUntilFn (fun c =>  c == ' ' || c == '\n')
 
-private def recoverNonSpace (p : ParserFn) : ParserFn :=
+def recoverNonSpace (p : ParserFn) : ParserFn :=
   recoverFn p fun rctx =>
     ignoreFn (takeUntilFn (fun c => c != ' ')) >>
     show ParserFn from
       fun _ s => s.shrinkStack rctx.initialSize
 
-private def recoverWsWith (stxs : Array Syntax) (p : ParserFn) : ParserFn :=
+def recoverWsWith (stxs : Array Syntax) (p : ParserFn) : ParserFn :=
   recoverFn p fun rctx =>
     ignoreFn <| takeUntilFn (fun c =>  c == ' ' || c == '\n') >>
     show ParserFn from
       fun _ s => stxs.foldl (init := s.shrinkStack rctx.initialSize) (·.pushSyntax ·)
 
-private def recoverEol (p : ParserFn) : ParserFn :=
+def recoverEol (p : ParserFn) : ParserFn :=
   recoverFn p fun _ => ignoreFn <| skipToNewline
 
-private def recoverEolWith (stxs : Array Syntax) (p : ParserFn) : ParserFn :=
+def recoverEolWith (stxs : Array Syntax) (p : ParserFn) : ParserFn :=
   recoverFn p fun rctx =>
     ignoreFn skipToNewline >>
     show ParserFn from
@@ -494,7 +494,7 @@ private def recoverEolWith (stxs : Array Syntax) (p : ParserFn) : ParserFn :=
 
 -- Like `recoverEol` but stores recovered errors at the original error position
 -- rather than the post-recovery position.
-private def recoverEolAtErrPos (p : ParserFn) : ParserFn := fun c s =>
+def recoverEolAtErrPos (p : ParserFn) : ParserFn := fun c s =>
   let s := p c s
   if let some msg := s.errorMsg then
     let errPos := s.pos
@@ -509,7 +509,7 @@ private def recoverEolAtErrPos (p : ParserFn) : ParserFn := fun c s =>
 
 -- Like `recoverEolWith` but stores recovered errors at the original error position
 -- rather than the post-recovery position.
-private def recoverEolWithAtErrPos (stxs : Array Syntax) (p : ParserFn) : ParserFn := fun c s =>
+def recoverEolWithAtErrPos (stxs : Array Syntax) (p : ParserFn) : ParserFn := fun c s =>
   let iniSz := s.stxStack.size
   let s := p c s
   if let some msg := s.errorMsg then
@@ -521,10 +521,10 @@ private def recoverEolWithAtErrPos (stxs : Array Syntax) (p : ParserFn) : Parser
       {s' with recoveredErrors := s.recoveredErrors.push (errPos, s'.stxStack, msg)}
   else s
 
-private def recoverSkip (p : ParserFn) : ParserFn :=
+def recoverSkip (p : ParserFn) : ParserFn :=
   recoverFn p fun _ => skipFn
 
-private def recoverSkipWith (stxs : Array Syntax) (p : ParserFn) : ParserFn :=
+def recoverSkipWith (stxs : Array Syntax) (p : ParserFn) : ParserFn :=
   recoverFn p fun rctx =>
     show ParserFn from
       fun _ s => stxs.foldl (init := s.shrinkStack rctx.initialSize) (·.pushSyntax ·)
@@ -535,7 +535,7 @@ def recoverHereWith (stxs : Array Syntax) (p : ParserFn) : ParserFn :=
     show ParserFn from
       fun _ s => stxs.foldl (init := s.restore rctx.initialSize rctx.initialPos) (·.pushSyntax ·)
 
-private def recoverHereWithKeeping (stxs : Array Syntax) (keep : Nat) (p : ParserFn) : ParserFn :=
+def recoverHereWithKeeping (stxs : Array Syntax) (keep : Nat) (p : ParserFn) : ParserFn :=
   recoverFn p fun rctx =>
     show ParserFn from
       fun _ s => stxs.foldl (init := s.restore (rctx.initialSize + keep) rctx.initialPos) (·.pushSyntax ·)
@@ -584,7 +584,7 @@ it's in a single-line context and whitespace may only be the space
 character. If it's `some N`, then newlines are allowed, but `N` is the
 minimum indentation column.
 -/
-private def nameArgWhitespace : (multiline : Option Nat) → ParserFn
+def nameArgWhitespace : (multiline : Option Nat) → ParserFn
   | none => eatSpaces
   | some n => takeWhileFn (fun c => c == ' ' || c == '\n') >> guardMinColumn n
 
@@ -598,7 +598,7 @@ each sub-parser of `delimitedInline` contributes a clear expected-token name, an
 unhelpful generic "unexpected" messages from inner parsers so that the more informative message
 from `inlineTextChar` survives error merging via `<|>`.
 -/
-private def expectedFn (msg : String) (p : ParserFn) : ParserFn := fun c s =>
+def expectedFn (msg : String) (p : ParserFn) : ParserFn := fun c s =>
   let iniPos := s.pos
   let s := p c s
   if s.hasError && s.pos == iniPos then
@@ -649,18 +649,18 @@ def linebreak (ctxt : InlineCtxt) : ParserFn :=
   else
     errorFn "Newlines not allowed here"
 
-private partial def notInLink (ctxt : InlineCtxt) : ParserFn := fun _ s =>
+partial def notInLink (ctxt : InlineCtxt) : ParserFn := fun _ s =>
   if ctxt.inLink then s.mkError "Already in a link" else s
 
 -- Like `satisfyFn (· == '\n')` but with a better error message that mentions what was expected.
-private def newlineOrUnexpected (msg : String) : ParserFn := fun c s =>
+def newlineOrUnexpected (msg : String) : ParserFn := fun c s =>
   let i := s.pos
   if h : c.atEnd i then s.mkEOIError
   else if c.get' i h == '\n' then s.next' c i h
   else s.mkUnexpectedError s!"unexpected '{c.get' i h}'" [msg]
 
 mutual
-  private partial def emphLike
+  partial def emphLike
     (name : SyntaxNodeKind) (char : Char) (what plural : String)
     (getter : InlineCtxt → Option Nat) (setter : InlineCtxt → Option Nat → InlineCtxt)
     (ctxt : InlineCtxt) : ParserFn :=
@@ -799,7 +799,7 @@ mutual
         nodeFn `str (asStringFn (quoted := true) (many1Fn (satisfyEscFn (fun c => c != ']' && c != '\n') "other than ']' or newline"))) >>
         strFn "]")
 
-  private partial def linkTarget : ParserFn := fun c s =>
+  partial def linkTarget : ParserFn := fun c s =>
     let s := (ref <|> url) c s
     if s.hasError then
       match s.errorMsg with
@@ -922,7 +922,7 @@ deriving Inhabited, Repr
 Finds the minimum column of the first non-whitespace character on each non-empty content line
 between `startPos` and `endPos`, returning `init` if no such line exists.
 -/
-private def minContentIndent (text : FileMap) (startPos endPos : String.Pos.Raw)
+def minContentIndent (text : FileMap) (startPos endPos : String.Pos.Raw)
     (init : Nat) : Nat := Id.run do
   let mut result := init
   let mut thisLineCol := 0
@@ -980,13 +980,13 @@ public def BlockCtxt.forDocString (text : FileMap)
       else text.source.rawEndPos
     { docStartPosition := text.toPosition pos, baseColumn }
 
-private def bol (ctxt : BlockCtxt) : ParserFn := fun c s =>
+def bol (ctxt : BlockCtxt) : ParserFn := fun c s =>
   let pos := c.fileMap.toPosition s.pos
   if pos.column ≤ ctxt.baseColumn then s
   else if pos.line == ctxt.docStartPosition.line && pos.column ≤ ctxt.docStartPosition.column then s
   else s.mkErrorAt s!"beginning of line at {pos}" s.pos
 
-private def bolThen (ctxt : BlockCtxt) (p : ParserFn) (description : String) : ParserFn := fun c s =>
+def bolThen (ctxt : BlockCtxt) (p : ParserFn) (description : String) : ParserFn := fun c s =>
   let position := c.fileMap.toPosition s.pos
   let positionOk :=
     position.column ≤ ctxt.baseColumn ||
@@ -1075,16 +1075,16 @@ public def lookaheadUnorderedListIndicator (ctxt : BlockCtxt) (p : UnorderedList
     if s.hasError then s.setPos iniPos
     else p type c (s.shrinkStack iniSz |>.setPos bulletPos)
 
-private def skipUntilDedent (indent : Nat) : ParserFn :=
+def skipUntilDedent (indent : Nat) : ParserFn :=
   skipRestOfLine >>
   manyFn (chFn ' ' >> takeWhileFn (· == ' ') >> guardColumn (· ≥ indent) s!"indentation at {indent}" >> skipRestOfLine)
 
-private def recoverUnindent (indent : Nat) (p : ParserFn) (finish : ParserFn := skipFn) :
+def recoverUnindent (indent : Nat) (p : ParserFn) (finish : ParserFn := skipFn) :
     ParserFn :=
   recoverFn p (fun _ => ignoreFn (skipUntilDedent indent) >> finish)
 
 
-private def blockSep := ignoreFn (manyFn blankLine >> optionalFn endLine)
+def blockSep := ignoreFn (manyFn blankLine >> optionalFn endLine)
 
 mutual
   /-- Parses a list item according to the current nesting context. -/

src/Lean/Elab/App.lean

@@ -13,6 +13,7 @@ public import Lean.IdentifierSuggestion
 import all Lean.Elab.ErrorUtils
 import Lean.Elab.DeprecatedArg
 import Init.Omega
+import Init.Data.List.MapIdx
 
 public section
 
@@ -1299,13 +1300,13 @@ where
 inductive LValResolution where
   /-- When applied to `f`, effectively expands to `BaseStruct.fieldName (self := Struct.toBase f)`.
   This is a special named argument where it suppresses any explicit arguments depending on it so that type parameters don't need to be supplied. -/
-  | projFn   (baseStructName : Name) (structName : Name) (fieldName : Name)
+  | projFn   (baseStructName : Name) (structName : Name) (fieldName : Name) (levels : List Level)
   /-- Similar to `projFn`, but for extracting field indexed by `idx`. Works for one-constructor inductive types in general. -/
   | projIdx  (structName : Name) (idx : Nat)
   /-- When applied to `f`, effectively expands to `constName ... (Struct.toBase f)`, with the argument placed in the correct
   positional argument if possible, or otherwise as a named argument. The `Struct.toBase` is not present if `baseStructName == structName`,
   in which case these do not need to be structures. Supports generalized field notation. -/
-  | const    (baseStructName : Name) (structName : Name) (constName : Name)
+  | const    (baseStructName : Name) (structName : Name) (constName : Name) (levels : List Level)
   /-- Like `const`, but with `fvar` instead of `constName`.
   The `baseName` is the base name of the type to search for in the parameter list. -/
   | localRec (baseName : Name) (fvar : Expr)
@@ -1380,7 +1381,7 @@ private def reverseFieldLookup (env : Environment) (fieldName : String) :=
 
 private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM LValResolution := do
   match eType.getAppFn, lval with
-  | .const structName _, LVal.fieldIdx ref idx =>
+  | .const structName _, LVal.fieldIdx ref idx levels =>
     if idx == 0 then
       throwError "Invalid projection: Index must be greater than 0"
     let env ← getEnv
@@ -1393,10 +1394,14 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
       if idx - 1 < numFields then
         if isStructure env structName then
           let fieldNames := getStructureFields env structName
-          return LValResolution.projFn structName structName fieldNames[idx - 1]!
+          return LValResolution.projFn structName structName fieldNames[idx - 1]! levels
         else
           /- `structName` was declared using `inductive` command.
             So, we don't projection functions for it. Thus, we use `Expr.proj` -/
+          unless levels.isEmpty do
+            throwError "Invalid projection: Explicit universe levels are only supported for inductive types \
+              defined using the `structure` command. \
+              The expression{indentExpr e}\nhas type{inlineExpr eType}which is not a `structure`."
           return LValResolution.projIdx structName (idx - 1)
       else
         if numFields == 0 then
@@ -1409,31 +1414,33 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
           ++ MessageData.note m!"The expression{indentExpr e}\nhas type{inlineExpr eType}which has only \
           {numFields} field{numFields.plural}"
           ++ tupleHint
-  | .const structName _, LVal.fieldName ref fieldName _ _ => withRef ref do
+  | .const structName _, LVal.fieldName ref fieldName levels _ _ => withRef ref do
     let env ← getEnv
     if isStructure env structName then
       if let some baseStructName := findField? env structName (Name.mkSimple fieldName) then
-        return LValResolution.projFn baseStructName structName (Name.mkSimple fieldName)
+        return LValResolution.projFn baseStructName structName (Name.mkSimple fieldName) levels
     -- Search the local context first
     let fullName := Name.mkStr (privateToUserName structName) fieldName
     for localDecl in (← getLCtx) do
       if localDecl.isAuxDecl then
         if let some localDeclFullName := (← getLCtx).auxDeclToFullName.get? localDecl.fvarId then
           if fullName == privateToUserName localDeclFullName then
+            unless levels.isEmpty do
+              throwInvalidExplicitUniversesForLocal localDecl.toExpr
             /- LVal notation is being used to make a "local" recursive call. -/
             return LValResolution.localRec structName localDecl.toExpr
     -- Then search the environment
     if let some (baseStructName, fullName) ← findMethod? structName (.mkSimple fieldName) then
-      return LValResolution.const baseStructName structName fullName
+      return LValResolution.const baseStructName structName fullName levels
     throwInvalidFieldAt ref fieldName fullName
       -- Suggest a potential unreachable private name as hint. This does not cover structure
       -- inheritance, nor `import all`.
       (declHint := (mkPrivateName env structName).mkStr fieldName)
 
-  | .forallE .., LVal.fieldName ref fieldName suffix? fullRef =>
+  | .forallE .., LVal.fieldName ref fieldName levels suffix? fullRef =>
     let fullName := Name.str `Function fieldName
     if (← getEnv).contains fullName then
-      return LValResolution.const `Function `Function fullName
+      return LValResolution.const `Function `Function fullName levels
     match e.getAppFn, suffix? with
     | Expr.const c _, some suffix =>
       throwUnknownNameWithSuggestions (idOrConst := "constant")  (ref? := fullRef) (c ++ suffix)
@@ -1443,7 +1450,7 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
     throwError "Invalid projection: Projections cannot be used on functions, and{indentExpr e}\n\
       has function type{inlineExprTrailing eType}"
 
-  | .mvar .., .fieldName _ fieldName _ _ =>
+  | .mvar .., .fieldName _ fieldName levels _ _ =>
     let hint := match reverseFieldLookup (← getEnv) fieldName with
       | #[] => MessageData.nil
       | #[opt] => .hint' m!"Consider replacing the field projection `.{fieldName}` with a call to the function `{.ofConstName opt}`."
@@ -1451,13 +1458,13 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
           {MessageData.joinSep (opts.toList.map (indentD m!"• `{.ofConstName ·}`")) .nil}"
     throwNamedError lean.invalidField (m!"Invalid field notation: Type of{indentExpr e}\nis not \
       known; cannot resolve field `{fieldName}`" ++ hint)
-  | .mvar .., .fieldIdx _ i  =>
+  | .mvar .., .fieldIdx _ i _ =>
     throwError m!"Invalid projection: Type of{indentExpr e}\nis not known; cannot resolve \
       projection `{i}`"
 
   | _, _ =>
     match e.getAppFn, lval with
-    | Expr.const c _, .fieldName _ref _fieldName (some suffix) fullRef =>
+    | Expr.const c _, .fieldName _ref _fieldName _levels (some suffix) fullRef =>
       throwUnknownNameWithSuggestions (idOrConst := "constant") (ref? := fullRef) (c ++ suffix)
     | _, .fieldName .. =>
       throwNamedError lean.invalidField m!"Invalid field notation: Field projection operates on \
@@ -1706,12 +1713,12 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
       let f ← mkProjAndCheck structName idx f
       let f ← addTermInfo lval.getRef f
       loop f lvals
-    | LValResolution.projFn baseStructName structName fieldName =>
+    | LValResolution.projFn baseStructName structName fieldName levels =>
       let f ← mkBaseProjections baseStructName structName f
       let some info := getFieldInfo? (← getEnv) baseStructName fieldName | unreachable!
       if (← isInaccessiblePrivateName info.projFn) then
         throwError "Field `{fieldName}` from structure `{structName}` is private"
-      let projFn ← withRef lval.getRef <| mkConst info.projFn
+      let projFn ← withRef lval.getRef <| mkConst info.projFn levels
       let projFn ← addProjTermInfo lval.getRef projFn
       if lvals.isEmpty then
         let namedArgs ← addNamedArg namedArgs { name := `self, val := Arg.expr f, suppressDeps := true }
@@ -1719,9 +1726,9 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
       else
         let f ← elabAppArgs projFn #[{ name := `self, val := Arg.expr f, suppressDeps := true }] #[] (expectedType? := none) (explicit := false) (ellipsis := false)
         loop f lvals
-    | LValResolution.const baseStructName structName constName =>
+    | LValResolution.const baseStructName structName constName levels =>
       let f ← if baseStructName != structName then mkBaseProjections baseStructName structName f else pure f
-      let projFn ← withRef lval.getRef <| mkConst constName
+      let projFn ← withRef lval.getRef <| mkConst constName levels
       let projFn ← addProjTermInfo lval.getRef projFn
       if lvals.isEmpty then
         let (args, namedArgs) ← addLValArg baseStructName f args namedArgs projFn explicit
@@ -1772,15 +1779,19 @@ false, no elaboration function executed by `x` will reset it to
 /--
 Elaborates the resolutions of a function. The `fns` array is the output of `resolveName'`.
 -/
-private def elabAppFnResolutions (fRef : Syntax) (fns : List (Expr × Syntax × List Syntax)) (lvals : List LVal)
+private def elabAppFnResolutions (fRef : Syntax) (fns : List (Expr × Syntax × List Syntax × List Level)) (lvals : List LVal)
     (namedArgs : Array NamedArg) (args : Array Arg) (expectedType? : Option Expr) (explicit ellipsis overloaded : Bool)
     (acc : Array (TermElabResult Expr)) (forceTermInfo : Bool := false) :
     TermElabM (Array (TermElabResult Expr)) := do
   let overloaded := overloaded || fns.length > 1
   -- Set `errToSorry` to `false` if `fns` > 1. See comment above about the interaction between `errToSorry` and `observing`.
   withReader (fun ctx => { ctx with errToSorry := fns.length == 1 && ctx.errToSorry }) do
-    fns.foldlM (init := acc) fun acc (f, fIdent, fields) => do
-      let lvals' := toLVals fields (first := true)
+    fns.foldlM (init := acc) fun acc (f, fIdent, fields, projLevels) => do
+      let lastIdx := fields.length - 1
+      let lvals' := fields.mapIdx fun idx field =>
+        let suffix? := if idx == 0       then some <| toName fields else none
+        let levels  := if idx == lastIdx then projLevels            else []
+        LVal.fieldName field field.getId.getString! levels suffix? fRef
       let s ← observing do
         checkDeprecated fIdent f
         let f ← addTermInfo fIdent f expectedType? (force := forceTermInfo)
@@ -1794,11 +1805,6 @@ where
       | field :: fields => .mkStr (go fields) field.getId.toString
     go fields.reverse
 
-  toLVals : List Syntax → (first : Bool) → List LVal
-    | [],            _     => []
-    | field::fields, true  => .fieldName field field.getId.getString! (toName (field::fields)) fRef :: toLVals fields false
-    | field::fields, false => .fieldName field field.getId.getString! none fRef :: toLVals fields false
-
 private def elabAppFnId (fIdent : Syntax) (fExplicitUnivs : List Level) (lvals : List LVal)
     (namedArgs : Array NamedArg) (args : Array Arg) (expectedType? : Option Expr) (explicit ellipsis overloaded : Bool)
     (acc : Array (TermElabResult Expr)) :
@@ -1832,7 +1838,7 @@ 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) (explicitUnivs : List Level) (expectedType? : Option Expr) : TermElabM (List (Expr × Syntax × List Syntax × List Level)) := do
   unless id.isAtomic do
     throwError "Invalid dotted identifier notation: The name `{id}` must be atomic"
   tryPostponeIfNoneOrMVar expectedType?
@@ -1844,7 +1850,7 @@ private partial def resolveDottedIdentFn (idRef : Syntax) (id : Name) (explicitU
   withForallBody expectedType fun resultType => do
     go resultType expectedType #[]
 where
-  throwNoExpectedType := do
+  throwNoExpectedType {α} : TermElabM α := do
     let hint ← match reverseFieldLookup (← getEnv) (id.getString!) with
       | #[] => pure MessageData.nil
       | suggestions =>
@@ -1863,7 +1869,7 @@ where
         withForallBody body k
     else
       k type
-  go (resultType : Expr) (expectedType : Expr) (previousExceptions : Array Exception) : TermElabM (List (Expr × Syntax × List Syntax)) := do
+  go (resultType : Expr) (expectedType : Expr) (previousExceptions : Array Exception) : TermElabM (List (Expr × Syntax × List Syntax × List Level)) := do
     let resultType ← instantiateMVars resultType
     let resultTypeFn := resultType.getAppFn
     try
@@ -1880,11 +1886,11 @@ 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 explicitUnivs, ← getRef, [], [])
         else if let some (fvar, []) ← resolveLocalName fullName then
           unless explicitUnivs.isEmpty do
             throwInvalidExplicitUniversesForLocal fvar
-          return [(fvar, ← getRef, [])]
+          return [(fvar, ← getRef, [], [])]
         else
           throwUnknownIdentifierAt (← getRef) (declHint := fullName) <| m!"Unknown constant `{.ofConstName fullName}`"
             ++ .note m!"Inferred this name from the expected resulting type of `.{id}`:{indentExpr expectedType}"
@@ -1914,26 +1920,37 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
     withReader (fun ctx => { ctx with errToSorry := false }) do
       f.getArgs.foldlM (init := acc) fun acc f => elabAppFn f lvals namedArgs args expectedType? explicit ellipsis true acc
   else
-    let elabFieldName (e field : Syntax) (explicit : Bool) := do
-      let newLVals := field.identComponents.map fun comp =>
-        -- We use `none` in `suffix?` since `field` can't be part of a composite name
-        LVal.fieldName comp comp.getId.getString! none f
+    let elabFieldName (e field : Syntax) (explicitUnivs : List Level) := do
+      let comps := field.identComponents
+      let lastIdx := comps.length - 1
+      let newLVals := comps.mapIdx fun idx comp =>
+        let levels := if idx = lastIdx then explicitUnivs else []
+        let suffix? := none -- We use `none` since the field can't be part of a composite name
+        LVal.fieldName comp comp.getId.getString! levels suffix? f
       elabAppFn e (newLVals ++ lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
-    let elabFieldIdx (e idxStx : Syntax) (explicit : Bool) := do
+    let elabFieldIdx (e idxStx : Syntax) (explicitUnivs : List Level) := do
       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
+      elabAppFn e (LVal.fieldIdx idxStx idx explicitUnivs :: lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
+    let elabDottedIdent (id : Syntax) (explicitUnivs : List Level) : 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
-    | `($(e).$field:ident) => elabFieldName e field explicit
-    | `($e |>.$field:ident) => elabFieldName e field explicit
-    | `(@$(e).$idx:fieldIdx) => elabFieldIdx e idx (explicit := true)
-    | `(@$(e).$field:ident) => elabFieldName e field (explicit := true)
+    | `($(e).$idx:fieldIdx)
+    | `($e |>.$idx:fieldIdx) =>
+      elabFieldIdx e idx []
+    | `($(e).$idx:fieldIdx.{$us,*})
+    | `($e |>.$idx:fieldIdx.{$us,*}) =>
+      let us ← elabExplicitUnivs us
+      elabFieldIdx e idx us
+    | `($(e).$field:ident)
+    | `($e |>.$field:ident) =>
+      elabFieldName e field []
+    | `($(e).$field:ident.{$us,*})
+    | `($e |>.$field:ident.{$us,*}) =>
+      let us ← elabExplicitUnivs us
+      elabFieldName e field us
     | `($_:ident@$_:term) =>
       throwError m!"Expected a function, but found the named pattern{indentD f}"
         ++ .note m!"Named patterns `<identifier>@<term>` can only be used when pattern-matching"
@@ -1942,12 +1959,15 @@ 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) => elabDottedIdent id []
     | `(.$id:ident.{$us,*}) =>
       let us ← elabExplicitUnivs us
-      elabDottedIdent id us explicit
+      elabDottedIdent id us
     | `(@$_:ident)
     | `(@$_:ident.{$_us,*})
+    | `(@$(_).$_:fieldIdx)
+    | `(@$(_).$_:ident)
+    | `(@$(_).$_:ident.{$_us,*})
     | `(@.$_:ident)
     | `(@.$_:ident.{$_us,*}) =>
       elabAppFn (f.getArg 1) lvals namedArgs args expectedType? (explicit := true) ellipsis overloaded acc
@@ -2084,10 +2104,10 @@ private def elabAtom : TermElab := fun stx expectedType? => do
 @[builtin_term_elab dotIdent] def elabDotIdent : TermElab := elabAtom
 @[builtin_term_elab explicitUniv] def elabExplicitUniv : TermElab := elabAtom
 @[builtin_term_elab pipeProj] def elabPipeProj : TermElab
-  | `($e |>.%$tk$f $args*), expectedType? =>
+  | `($e |>.%$tk$f$[.{$us?,*}]? $args*), expectedType? =>
     universeConstraintsCheckpoint do
       let (namedArgs, args, ellipsis) ← expandArgs args
-      let mut stx ← `($e |>.%$tk$f)
+      let mut stx ← `($e |>.%$tk$f$[.{$us?,*}]?)
       if let (some startPos, some stopPos) := (e.raw.getPos?, f.raw.getTailPos?) then
         stx := ⟨stx.raw.setInfo <| .synthetic (canonical := true) startPos stopPos⟩
       elabAppAux stx namedArgs args (ellipsis := ellipsis) expectedType?
@@ -2095,15 +2115,16 @@ 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?
+  | `(@$(_).$_:ident.{$_us,*}) => 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
 
 @[builtin_term_elab choice] def elabChoice : TermElab := elabAtom
 @[builtin_term_elab proj] def elabProj : TermElab := elabAtom

src/Lean/Elab/AutoBound.lean

@@ -74,7 +74,7 @@ def isValidAutoBoundLevelName (n : Name) (relaxed : Bool) : Bool :=
 /--
 Tracks extra context needed within the scope of `Lean.Elab.Term.withAutoBoundImplicit`
 -/
-public structure AutoBoundImplicitContext where
+structure AutoBoundImplicitContext where
   /--
   This always matches the `autoImplicit` option; it is duplicated here in
   order to support the behavior of the deprecated `Lean.Elab.Term.Context.autoImplicit`
@@ -95,7 +95,7 @@ instance : EmptyCollection AutoBoundImplicitContext where
 Pushes a new variable onto the autoImplicit context, indicating that it needs
 to be bound as an implicit parameter.
 -/
-public def AutoBoundImplicitContext.push (ctx : AutoBoundImplicitContext) (x : Expr) :=
+def AutoBoundImplicitContext.push (ctx : AutoBoundImplicitContext) (x : Expr) :=
   { ctx with boundVariables := ctx.boundVariables.push x }
 
 end Lean.Elab

src/Lean/Elab/BuiltinCommand.lean

@@ -116,8 +116,9 @@ private def checkEndHeader : Name → List Scope → Option Name
       addScope (isNewNamespace := false) (isNoncomputable := ncTk.isSome) (isPublic := publicTk.isSome) (isMeta := metaTk.isSome) (attrs := attrs) "" (← getCurrNamespace)
   | _                        => throwUnsupportedSyntax
 
-@[builtin_command_elab InternalSyntax.end_local_scope] def elabEndLocalScope : CommandElab := fun _ => do
-  setDelimitsLocal
+@[builtin_command_elab InternalSyntax.end_local_scope] def elabEndLocalScope : CommandElab := fun stx => do
+  let depth := stx[1].toNat
+  setDelimitsLocal depth
 
 /--
 Produces a `Name` composed of the names of at most the innermost `n` scopes in `ss`, truncating if an
@@ -528,7 +529,7 @@ open Lean.Parser.Command.InternalSyntax in
 @[builtin_macro Lean.Parser.Command.«in»] def expandInCmd : Macro
   | `($cmd₁ in%$tk $cmd₂) =>
     -- Limit ref variability for incrementality; see Note [Incremental Macros]
-    withRef tk `(section $cmd₁:command $endLocalScopeSyntax:command $cmd₂ end)
+    withRef tk `(section $cmd₁:command $(endLocalScopeSyntax 1):command $cmd₂ end)
   | _                 => Macro.throwUnsupported
 
 @[builtin_command_elab Parser.Command.addDocString] def elabAddDeclDoc : CommandElab := fun stx => do

src/Lean/Elab/BuiltinDo/For.lean

@@ -111,8 +111,14 @@ open Lean.Meta
     for x in loopMutVars do
       let defn ← getLocalDeclFromUserName x.getId
       Term.addTermInfo' x defn.toExpr
-      -- ForIn forces all mut vars into the same universe: that of the do block result type.
-      discard <| Term.ensureHasType (mkSort (mi.u.succ)) defn.type
+      -- ForIn forces the mut tuple into the universe mi.u: that of the do block result type.
+      -- If we don't do this, then we are stuck on solving constraints such as
+      --   `max ?u.46 ?u.47 =?= max (max ?u.22 ?u.46) ?u.47`
+      -- It's important we do this as a separate isLevelDefEq check on the decremented level because
+      -- otherwise (`ensureHasType (mkSort mi.u.succ)`) we are stuck on constraints like
+      --   `max (?u+1) (?v+1) =?= ?u+1`
+      let u ← getDecLevel defn.type
+      discard <| isLevelDefEq u mi.u
       defs := defs.push defn.toExpr
     if info.returnsEarly && loopMutVars.isEmpty then
       defs := defs.push (mkConst ``Unit.unit)

src/Lean/Elab/BuiltinTerm.lean

@@ -314,6 +314,23 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
     return val
   | _ => panic! "resolveId? returned an unexpected expression"
 
+/--
+Rebuild a type application with fresh synthetic metavariables for instance-implicit arguments.
+Non-instance-implicit arguments are assigned from the original application's arguments.
+If the function is over-applied, extra arguments are preserved.
+-/
+private def resynthInstImplicitArgs (type : Expr) : TermElabM Expr := do
+  let fn := type.getAppFn
+  let args := type.getAppArgs
+  let (mvars, bis, _) ← forallMetaTelescope (← inferType fn)
+  for i in [:mvars.size] do
+    if bis[i]!.isInstImplicit then
+      mvars[i]!.mvarId!.assign (← mkInstMVar (← inferType mvars[i]!))
+    else
+      mvars[i]!.mvarId!.assign args[i]!
+  let args := mvars ++ args.drop mvars.size
+  instantiateMVars (mkAppN fn args)
+
 @[builtin_term_elab Lean.Parser.Term.inferInstanceAs] def elabInferInstanceAs : TermElab := fun stx expectedType? => do
   -- The type argument is the last child (works for both `inferInstanceAs T` and `inferInstanceAs <| T`)
   let typeStx := stx[stx.getNumArgs - 1]!
@@ -325,19 +342,21 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
       .note "`inferInstanceAs` requires full knowledge of the expected (\"target\") type to do its \
         instance translation. If you do not intend to transport instances between two types, \
         consider using `inferInstance` or `(inferInstance : expectedType)` instead.")
-  let type ← withSynthesize (postpone := .yes) <| elabType typeStx
-  -- Unify with expected type to resolve metavariables (e.g., `_` placeholders)
-  discard <| isDefEq type expectedType
+  let type ← withSynthesize do
+    let type ← elabType typeStx
+    -- Unify with expected type to resolve metavariables (e.g., `_` placeholders)
+    discard <| isDefEq type expectedType
+    return type
+  -- Re-infer instance-implicit args, so that synthesis is not influenced by the expected type's
+  -- instance choices.
+  let type ← withSynthesize <| resynthInstImplicitArgs type
   let type ← instantiateMVars type
-  -- Rebuild type with fresh synthetic mvars for instance-implicit args, so that
-  -- synthesis is not influenced by the expected type's instance choices.
-  let type ← abstractInstImplicitArgs type
   let inst ← synthInstance type
   let inst ← if backward.inferInstanceAs.wrap.get (← getOptions) then
     -- Wrap instance so its type matches the expected type exactly.
     let logCompileErrors := !(← read).isNoncomputableSection && !(← read).declName?.any (Lean.isNoncomputable (← getEnv))
     let isMeta := (← read).declName?.any (isMarkedMeta (← getEnv))
-    withNewMCtxDepth <| wrapInstance inst expectedType (logCompileErrors := logCompileErrors) (isMeta := isMeta)
+    wrapInstance inst expectedType (logCompileErrors := logCompileErrors) (isMeta := isMeta)
   else
     pure inst
   ensureHasType expectedType? inst

src/Lean/Elab/DeclModifiers.lean

@@ -7,11 +7,19 @@ module
 
 prelude
 public import Lean.DocString.Add
+public import Lean.Linter.Basic
 meta import Lean.Parser.Command
 
 public section
 
-namespace Lean.Elab
+namespace Lean
+
+register_builtin_option linter.redundantVisibility : Bool := {
+  defValue := false
+  descr := "warn on redundant `private`/`public` visibility modifiers"
+}
+
+namespace Elab
 
 /--
 Ensure the environment does not contain a declaration with name `declName`.
@@ -65,9 +73,44 @@ def Visibility.isPublic : Visibility → Bool
   | .public    => true
   | _          => false
 
+/--
+Returns whether the given visibility modifier should be interpreted as `public` in the current
+environment.
+
+NOTE: `Environment.isExporting` defaults to `false` when command elaborators are invoked for
+backward compatibility. It needs to be initialized apropriately first before calling this function
+as e.g. done in `elabDeclaration`.
+-/
 def Visibility.isInferredPublic (env : Environment) (v : Visibility) : Bool :=
   if env.isExporting || !env.header.isModule then !v.isPrivate else v.isPublic
 
+/-- Converts optional visibility syntax to a `Visibility` value. -/
+def elabVisibility [Monad m] [MonadError m] [MonadEnv m] [MonadOptions m] [MonadLog m]
+    [AddMessageContext m]
+    (vis? : Option (TSyntax ``Parser.Command.visibility)) :
+    m Visibility := do
+  let env ← getEnv
+  match vis? with
+  | none   => pure .regular
+  | some v =>
+    match v with
+    | `(Parser.Command.visibility| private) =>
+      if v.raw.getHeadInfo matches .original .. then  -- skip macro output
+        if env.header.isModule && !env.isExporting then
+          Linter.logLintIf linter.redundantVisibility v
+            m!"`private` has no effect in a `module` file outside `public section`; \
+            declarations are already `private` by default"
+      pure .private
+    | `(Parser.Command.visibility| public) =>
+      if v.raw.getHeadInfo matches .original .. then  -- skip macro output
+        if env.isExporting || !env.header.isModule then
+          Linter.logLintIf linter.redundantVisibility v
+            m!"`public` is the default visibility{
+              if env.header.isModule then " inside a `public section`" else ""
+            }; the modifier has no effect"
+      pure .public
+    | _ => throwErrorAt v "unexpected visibility modifier"
+
 /-- Whether a declaration is default, partial or nonrec. -/
 inductive RecKind where
   | «partial» | «nonrec» | default
@@ -183,13 +226,7 @@ def elabModifiers (stx : TSyntax ``Parser.Command.declModifiers) : m Modifiers :
     else
       RecKind.nonrec
   let docString? := docCommentStx.getOptional?.map (TSyntax.mk ·, doc.verso.get (← getOptions))
-  let visibility ← match visibilityStx.getOptional? with
-    | none   => pure .regular
-    | some v =>
-      match v with
-      | `(Parser.Command.visibility| private) => pure .private
-      | `(Parser.Command.visibility| public) => pure .public
-      | _ => throwErrorAt v "unexpected visibility modifier"
+  let visibility ← elabVisibility (visibilityStx.getOptional?.map (⟨·⟩))
   let isProtected := !protectedStx.isNone
   let attrs ← match attrsStx.getOptional? with
     | none       => pure #[]

src/Lean/Elab/Declaration.lean

@@ -152,8 +152,9 @@ def expandNamespacedDeclaration : Macro := fun stx => do
   | some (ns, newStx) => do
     -- Limit ref variability for incrementality; see Note [Incremental Macros]
     let declTk := stx[1][0]
+    let depth := ns.getNumParts
     let ns := mkIdentFrom declTk ns
-    withRef declTk `(namespace $ns $endLocalScopeSyntax:command $(⟨newStx⟩) end $ns)
+    withRef declTk `(namespace $ns $(endLocalScopeSyntax depth):command $(⟨newStx⟩) end $ns)
   | none => Macro.throwUnsupported
 
 @[builtin_command_elab declaration, builtin_incremental]
@@ -340,31 +341,29 @@ def elabMutual : CommandElab := fun stx => do
 
 @[builtin_command_elab Lean.Parser.Command.«initialize»] def elabInitialize : CommandElab
   | stx@`($declModifiers:declModifiers $kw:initializeKeyword $[$id? : $type? ←]? $doSeq) => do
+    withExporting (isExporting := (← getScope).isPublic) do
     let attrId := mkIdentFrom stx <| if kw.raw[0].isToken "initialize" then `init else `builtin_init
     if let (some id, some type) := (id?, type?) then
       let `(Parser.Command.declModifiersT| $[$doc?:docComment]? $[@[$attrs?,*]]? $(vis?)? $[meta%$meta?]? $[unsafe%$unsafe?]?) := stx[0]
         | throwErrorAt declModifiers "invalid initialization command, unexpected modifiers"
       let defStx ← `($[$doc?:docComment]? @[$attrId:ident initFn, $(attrs?.getD ∅),*] $(vis?)? $[meta%$meta?]? opaque $id : $type)
       let mut fullId := (← getCurrNamespace) ++ id.getId
-      if vis?.any (·.raw.isOfKind ``Parser.Command.private) then
+      let visibility ← elabVisibility vis?
+      if !visibility.isInferredPublic (← getEnv) then
         fullId := mkPrivateName (← getEnv) fullId
       -- We need to add `id`'s ranges *before* elaborating `initFn` (and then `id` itself) as
       -- otherwise the info context created by `with_decl_name` will be incomplete and break the
       -- call hierarchy
       addDeclarationRangesForBuiltin fullId ⟨defStx.raw[0]⟩ defStx.raw[1]
-      let vis := Parser.Command.visibility.ofBool (!isPrivateName fullId)
       elabCommand (← `(
-        $vis:visibility $[meta%$meta?]? $[unsafe%$unsafe?]? def initFn : IO $type := with_decl_name% $(mkIdent fullId) do $doSeq
+        @[no_expose] private $[meta%$meta?]? $[unsafe%$unsafe?]? def initFn : IO $type := with_decl_name% $(mkIdent fullId) do $doSeq
         $defStx:command))
     else
       let `(Parser.Command.declModifiersT| $[$doc?:docComment]? $[@[$attrs?,*]]? $(_)? $[meta%$meta?]? $[unsafe%$unsafe?]?) := declModifiers
         | throwErrorAt declModifiers "invalid initialization command, unexpected modifiers"
       let attrs := (attrs?.map (·.getElems)).getD #[]
       let attrs := attrs.push (← `(Lean.Parser.Term.attrInstance| $attrId:ident))
-      -- `[builtin_init]` can be private as it is used for local codegen only but `[init]` must be
-      -- available for the interpreter.
-      let vis := Parser.Command.visibility.ofBool (attrId.getId == `init)
-      elabCommand (← `($[$doc?:docComment]? @[$[$attrs],*] $vis:visibility $[meta%$meta?]? $[unsafe%$unsafe?]? def initFn : IO Unit := do $doSeq))
+      elabCommand (← `($[$doc?:docComment]? @[no_expose, $[$attrs],*] private $[meta%$meta?]? $[unsafe%$unsafe?]? def initFn : IO Unit := do $doSeq))
   | _ => throwUnsupportedSyntax
 
 builtin_initialize

src/Lean/Elab/Deriving/Basic.lean

@@ -233,27 +233,41 @@ def processDefDeriving (view : DerivingClassView) (decl : Expr) (isNoncomputable
         finally
           Core.setMessageLog (msgLog ++ (← Core.getMessageLog))
   let env ← getEnv
-  let hints := ReducibilityHints.regular (getMaxHeight env result.value + 1)
-  let decl ← mkDefinitionValInferringUnsafe instName result.levelParams.toList result.type result.value hints
-  -- Pre-check: if the instance value depends on noncomputable definitions and the user didn't write
-  -- `noncomputable`, give an actionable error with a `Try this:` suggestion.
-  unless isNoncomputable || (← read).isNoncomputableSection || (← isProp result.type) do
-    let noncompRef? := preNormValue.foldConsts none fun n acc =>
-      acc <|> if Lean.isNoncomputable (asyncMode := .local) env n then some n else none
-    if let some noncompRef := noncompRef? then
-      if let some cmdRef := cmdRef? then
-        if let some origText := cmdRef.reprint then
-          let newText := (origText.replace "deriving instance " "deriving noncomputable instance ").trimAscii
-          logInfoAt cmdRef m!"Try this: {newText}"
-      throwError "failed to derive instance because it depends on \
-        `{.ofConstName noncompRef}`, which is noncomputable"
-  if isNoncomputable || (← read).isNoncomputableSection then
-    addDecl <| Declaration.defnDecl decl
-    modifyEnv (addNoncomputable · instName)
+  let isPropType ← isProp result.type
+  if isPropType then
+    let decl ← mkThmOrUnsafeDef {
+      name := instName, levelParams := result.levelParams.toList,
+      type := result.type, value := result.value
+    }
+    addDecl decl
   else
-    addAndCompile <| Declaration.defnDecl decl
+    let hints := ReducibilityHints.regular (getMaxHeight env result.value + 1)
+    let decl ← mkDefinitionValInferringUnsafe instName result.levelParams.toList result.type result.value hints
+    -- Pre-check: if the instance value depends on noncomputable definitions and the user didn't write
+    -- `noncomputable`, give an actionable error with a `Try this:` suggestion.
+    unless isNoncomputable || (← read).isNoncomputableSection do
+      let noncompRef? := preNormValue.foldConsts none fun n acc =>
+        acc <|> if Lean.isNoncomputable (asyncMode := .local) env n then some n else none
+      if let some noncompRef := noncompRef? then
+        if let some cmdRef := cmdRef? then
+          if let some origText := cmdRef.reprint then
+            let newText := (origText.replace "deriving instance " "deriving noncomputable instance ").trimAscii
+            logInfoAt cmdRef m!"Try this: {newText}"
+        throwError "failed to derive instance because it depends on \
+          `{.ofConstName noncompRef}`, which is noncomputable"
+    if isNoncomputable || (← read).isNoncomputableSection then
+      addDecl <| Declaration.defnDecl decl
+      modifyEnv (addNoncomputable · instName)
+    else
+      addAndCompile <| Declaration.defnDecl decl
   trace[Elab.Deriving] "Derived instance `{.ofConstName instName}`"
-  registerInstance instName AttributeKind.global (eval_prio default)
+  -- For Prop-typed instances (theorems), skip `implicit_reducible` since reducibility hints are
+  -- irrelevant for theorems. This matches the behavior of the handwritten `instance` command
+  -- (see `MutualDef.lean`).
+  if isPropType then
+    addInstance instName AttributeKind.global (eval_prio default)
+  else
+    registerInstance instName AttributeKind.global (eval_prio default)
   addDeclarationRangesFromSyntax instName (← getRef)
 
 end Term

src/Lean/Elab/Deriving/DecEq.lean

@@ -111,7 +111,7 @@ def mkMatchNew (ctx : Context) (header : Header) (indVal : InductiveVal) : TermE
   let x1 := mkIdent header.targetNames[0]!
   let x2 := mkIdent header.targetNames[1]!
   let ctorIdxName := mkCtorIdxName indVal.name
-  -- NB: the getMatcherInfo? assumes all mathcers are called `match_`
+  -- NB: the getMatcherInfo? assumes all matchers are called `match_`
   let casesOnSameCtorName ← mkFreshUserName (indVal.name ++ `match_on_same_ctor)
   mkCasesOnSameCtor casesOnSameCtorName indVal.name
   let alts ← Array.ofFnM (n := indVal.numCtors) fun ⟨ctorIdx, _⟩ => do

src/Lean/Elab/Deriving/Inhabited.lean

@@ -25,25 +25,23 @@ private def mkInhabitedInstanceUsing (inductiveTypeName : Name) (ctorName : Name
   | none =>
     return false
 where
-  addLocalInstancesForParamsAux {α} (k : LocalInst2Index → TermElabM α) : List Expr → Nat → LocalInst2Index → TermElabM α
-    | [], _, map    => k map
-    | x::xs, i, map =>
+  addLocalInstancesForParamsAux {α} (k : Array Expr → LocalInst2Index → TermElabM α) : List Expr → Nat → Array Expr → LocalInst2Index → TermElabM α
+    | [],    _, insts, map => k insts map
+    | x::xs, i, insts, map =>
       try
         let instType ← mkAppM `Inhabited #[x]
-        if (← isTypeCorrect instType) then
-          withLocalDeclD (← mkFreshUserName `inst) instType fun inst => do
-            trace[Elab.Deriving.inhabited] "adding local instance {instType}"
-            addLocalInstancesForParamsAux k xs (i+1) (map.insert inst.fvarId! i)
-        else
-          addLocalInstancesForParamsAux k xs (i+1) map
+        check instType
+        withLocalDecl (← mkFreshUserName `inst) .instImplicit instType fun inst => do
+          trace[Elab.Deriving.inhabited] "adding local instance {instType}"
+          addLocalInstancesForParamsAux k xs (i+1) (insts.push inst) (map.insert inst.fvarId! i)
       catch _ =>
-        addLocalInstancesForParamsAux k xs (i+1) map
+        addLocalInstancesForParamsAux k xs (i+1) insts map
 
-  addLocalInstancesForParams {α} (xs : Array Expr) (k : LocalInst2Index → TermElabM α) : TermElabM α := do
+  addLocalInstancesForParams {α} (xs : Array Expr) (k : Array Expr → LocalInst2Index → TermElabM α) : TermElabM α := do
     if addHypotheses then
-      addLocalInstancesForParamsAux k xs.toList 0 {}
+      addLocalInstancesForParamsAux k xs.toList 0 #[] {}
     else
-      k {}
+      k #[] {}
 
   collectUsedLocalsInsts (usedInstIdxs : IndexSet) (localInst2Index : LocalInst2Index) (e : Expr) : IndexSet :=
     if localInst2Index.isEmpty then
@@ -58,58 +56,88 @@ where
       runST (fun _ => visit |>.run usedInstIdxs) |>.2
 
   /-- Create an `instance` command using the constructor `ctorName` with a hypothesis `Inhabited α` when `α` is one of the inductive type parameters
-     at position `i` and `i ∈ assumingParamIdxs`. -/
-  mkInstanceCmdWith (assumingParamIdxs : IndexSet) : TermElabM Syntax := do
-    let ctx ← Deriving.mkContext ``Inhabited "inhabited" inductiveTypeName
+     at position `i` and `i ∈ usedInstIdxs`. -/
+  mkInstanceCmdWith (instId : Ident) (usedInstIdxs : IndexSet) (auxFunId : Ident) : TermElabM Syntax := do
     let indVal ← getConstInfoInduct inductiveTypeName
-    let ctorVal ← getConstInfoCtor ctorName
     let mut indArgs := #[]
     let mut binders := #[]
     for i in *...indVal.numParams + indVal.numIndices do
       let arg := mkIdent (← mkFreshUserName `a)
       indArgs := indArgs.push arg
-      let binder ← `(bracketedBinderF| { $arg:ident })
-      binders := binders.push binder
-      if assumingParamIdxs.contains i then
-        let binder ← `(bracketedBinderF| [Inhabited $arg:ident ])
-        binders := binders.push binder
+      binders := binders.push <| ← `(bracketedBinderF| { $arg:ident })
+      if usedInstIdxs.contains i then
+        binders := binders.push <| ← `(bracketedBinderF| [Inhabited $arg:ident ])
     let type ← `(@$(mkCIdent inductiveTypeName):ident $indArgs:ident*)
-    let mut ctorArgs := #[]
-    for _ in *...ctorVal.numParams do
-      ctorArgs := ctorArgs.push (← `(_))
-    for _ in *...ctorVal.numFields do
-      ctorArgs := ctorArgs.push (← ``(Inhabited.default))
-    let val ← `(@$(mkIdent ctorName):ident $ctorArgs*)
-    let ctx ← mkContext ``Inhabited "default" inductiveTypeName
-    let auxFunName := ctx.auxFunNames[0]!
-    `(def $(mkIdent auxFunName):ident $binders:bracketedBinder* : $type := $val
-      instance $(mkIdent ctx.instName):ident $binders:bracketedBinder* : Inhabited $type := ⟨$(mkIdent auxFunName)⟩)
+    `(instance $instId:ident $binders:bracketedBinder* : Inhabited $type := ⟨$auxFunId⟩)
 
+  solveMVarsWithDefault (e : Expr) : TermElabM Unit := do
+    let mvarIds ← getMVarsNoDelayed e
+    mvarIds.forM fun mvarId => mvarId.withContext do
+      unless ← mvarId.isAssigned do
+        let type ← mvarId.getType
+        withTraceNode `Elab.Deriving.inhabited (fun _ => return m!"synthesizing Inhabited instance for{inlineExprTrailing type}") do
+          let val ← mkDefault type
+          mvarId.assign val
+          trace[Elab.Deriving.inhabited] "value:{inlineExprTrailing val}"
 
-  mkInstanceCmd? : TermElabM (Option Syntax) := do
-    let ctorVal ← getConstInfoCtor ctorName
-    forallTelescopeReducing ctorVal.type fun xs _ =>
-      addLocalInstancesForParams xs[*...ctorVal.numParams] fun localInst2Index => do
-        let mut usedInstIdxs := {}
-        let mut ok := true
-        for h : i in ctorVal.numParams...xs.size do
-          let x := xs[i]
-          let instType ← mkAppM `Inhabited #[(← inferType x)]
-          trace[Elab.Deriving.inhabited] "checking {instType} for `{ctorName}`"
-          match (← trySynthInstance instType) with
-          | LOption.some e =>
-            usedInstIdxs := collectUsedLocalsInsts usedInstIdxs localInst2Index e
-          | _ =>
-            trace[Elab.Deriving.inhabited] "failed to generate instance using `{ctorName}` {if addHypotheses then "(assuming parameters are inhabited)" else ""} because of field with type{indentExpr (← inferType x)}"
-            ok := false
-            break
-        if !ok then
-          return none
+  mkDefaultValue (indVal : InductiveVal) : TermElabM (Expr × Expr × IndexSet) := do
+    let us := indVal.levelParams.map Level.param
+    forallTelescopeReducing indVal.type fun xs _ =>
+    withImplicitBinderInfos xs do
+    addLocalInstancesForParams xs[0...indVal.numParams] fun insts localInst2Index => do
+      let type := mkAppN (.const inductiveTypeName us) xs
+      let val ←
+        if isStructure (← getEnv) inductiveTypeName then
+          withTraceNode `Elab.Deriving.inhabited (fun _ => return m!"using structure instance elaborator") do
+            let stx ← `(structInst| {..})
+            withoutErrToSorry <| elabTermAndSynthesize stx type
         else
-          trace[Elab.Deriving.inhabited] "inhabited instance using `{ctorName}` {if addHypotheses then "(assuming parameters are inhabited)" else ""} {usedInstIdxs.toList}"
-          let cmd ← mkInstanceCmdWith usedInstIdxs
-          trace[Elab.Deriving.inhabited] "\n{cmd}"
-          return some cmd
+          withTraceNode `Elab.Deriving.inhabited (fun _ => return m!"using constructor `{.ofConstName ctorName}`") do
+            let val := mkAppN (.const ctorName us) xs[0...indVal.numParams]
+            let (mvars, _, type') ← forallMetaTelescopeReducing (← inferType val)
+            unless ← isDefEq type type' do
+              throwError "cannot unify{indentExpr type}\nand type of constructor{indentExpr type'}"
+            pure <| mkAppN val mvars
+      solveMVarsWithDefault val
+      let val ← instantiateMVars val
+      if val.hasMVar then
+        throwError "default value contains metavariables{inlineExprTrailing val}"
+      let fvars := Lean.collectFVars {} val
+      let insts' := insts.filter fvars.visitedExpr.contains
+      let usedInstIdxs := collectUsedLocalsInsts {} localInst2Index val
+      assert! insts'.size == usedInstIdxs.size
+      trace[Elab.Deriving.inhabited] "inhabited instance using{inlineExpr val}{if insts'.isEmpty then m!"" else m!"(assuming parameters {insts'} are inhabited)"}"
+      let xs' := xs ++ insts'
+      let auxType ← mkForallFVars xs' type
+      let auxVal ← mkLambdaFVars xs' val
+      return (auxType, auxVal, usedInstIdxs)
+
+  mkInstanceCmd? : TermElabM (Option Syntax) :=
+    withExporting (isExporting := !isPrivateName ctorName) do
+      let ctx ← mkContext ``Inhabited "default" inductiveTypeName
+      let auxFunName := (← getCurrNamespace) ++ ctx.auxFunNames[0]!
+      let indVal ← getConstInfoInduct inductiveTypeName
+      let (auxType, auxVal, usedInstIdxs) ←
+        try
+          withDeclName auxFunName do mkDefaultValue indVal
+        catch e =>
+          trace[Elab.Deriving.inhabited] "error: {e.toMessageData}"
+          return none
+      addDecl <| .defnDecl <| ← mkDefinitionValInferringUnsafe
+        (name        := auxFunName)
+        (levelParams := indVal.levelParams)
+        (type        := auxType)
+        (value       := auxVal)
+        (hints       := ReducibilityHints.regular (getMaxHeight (← getEnv) auxVal + 1))
+      if isMarkedMeta (← getEnv) inductiveTypeName then
+        modifyEnv (markMeta · auxFunName)
+      unless (← read).isNoncomputableSection do
+        compileDecls #[auxFunName]
+      enableRealizationsForConst auxFunName
+      trace[Elab.Deriving.inhabited] "defined {.ofConstName auxFunName}"
+      let cmd ← mkInstanceCmdWith (mkIdent ctx.instName) usedInstIdxs (mkCIdent auxFunName)
+      trace[Elab.Deriving.inhabited] "\n{cmd}"
+      return some cmd
 
 private def mkInhabitedInstance (declName : Name) : CommandElabM Unit := do
   withoutExposeFromCtors declName do

src/Lean/Elab/DocString.lean

@@ -1038,19 +1038,19 @@ builtin_initialize registerBuiltinAttribute {
 }
 end
 
-private unsafe def codeSuggestionsUnsafe : TermElabM (Array (StrLit → DocM (Array CodeSuggestion))) := do
+unsafe def codeSuggestionsUnsafe : TermElabM (Array (StrLit → DocM (Array CodeSuggestion))) := do
   let names := (codeSuggestionExt.getState (← getEnv)) |>.toArray
   return (← names.mapM (evalConst _)) ++ (← builtinCodeSuggestions.get).map (·.2)
 
 @[implemented_by codeSuggestionsUnsafe]
-private opaque codeSuggestions : TermElabM (Array (StrLit → DocM (Array CodeSuggestion)))
+opaque codeSuggestions : TermElabM (Array (StrLit → DocM (Array CodeSuggestion)))
 
-private unsafe def codeBlockSuggestionsUnsafe : TermElabM (Array (StrLit → DocM (Array CodeBlockSuggestion))) := do
+unsafe def codeBlockSuggestionsUnsafe : TermElabM (Array (StrLit → DocM (Array CodeBlockSuggestion))) := do
   let names := (codeBlockSuggestionExt.getState (← getEnv)) |>.toArray
   return (← names.mapM (evalConst _)) ++ (← builtinCodeBlockSuggestions.get).map (·.2)
 
 @[implemented_by codeBlockSuggestionsUnsafe]
-private opaque codeBlockSuggestions : TermElabM (Array (StrLit → DocM (Array CodeBlockSuggestion)))
+opaque codeBlockSuggestions : TermElabM (Array (StrLit → DocM (Array CodeBlockSuggestion)))
 
 /--
 Resolves a name against `NameMap` that contains a list of builtin expanders, taking into account
@@ -1060,7 +1060,7 @@ resolution (`realizeGlobalConstNoOverload`) won't find them.
 
 This is called as a fallback when the identifier can't be resolved.
 -/
-private def resolveBuiltinDocName {α : Type} (builtins : NameMap α) (x : Name) : TermElabM (Option α) := do
+def resolveBuiltinDocName {α : Type} (builtins : NameMap α) (x : Name) : TermElabM (Option α) := do
   if let some v := builtins.get? x then return some v
 
   -- Builtins shouldn't require a prefix, as they're part of the language.
@@ -1089,7 +1089,7 @@ private def resolveBuiltinDocName {α : Type} (builtins : NameMap α) (x : Name)
 
   return none
 
-private unsafe def roleExpandersForUnsafe (roleName : Ident) :
+unsafe def roleExpandersForUnsafe (roleName : Ident) :
     TermElabM (Array (Name × (TSyntaxArray `inline → StateT (Array (TSyntax `doc_arg)) DocM (Inline ElabInline)))) := do
   let x? ←
     try some <$> realizeGlobalConstNoOverload roleName
@@ -1105,10 +1105,10 @@ private unsafe def roleExpandersForUnsafe (roleName : Ident) :
 
 
 @[implemented_by roleExpandersForUnsafe]
-private opaque roleExpandersFor (roleName : Ident) :
+opaque roleExpandersFor (roleName : Ident) :
   TermElabM (Array (Name × (TSyntaxArray `inline → StateT (Array (TSyntax `doc_arg)) DocM (Inline ElabInline))))
 
-private unsafe def codeBlockExpandersForUnsafe (codeBlockName : Ident) :
+unsafe def codeBlockExpandersForUnsafe (codeBlockName : Ident) :
     TermElabM (Array (Name × (StrLit → StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock)))) := do
   let x? ←
     try some <$> realizeGlobalConstNoOverload codeBlockName
@@ -1124,10 +1124,10 @@ private unsafe def codeBlockExpandersForUnsafe (codeBlockName : Ident) :
 
 
 @[implemented_by codeBlockExpandersForUnsafe]
-private opaque codeBlockExpandersFor (codeBlockName : Ident) :
+opaque codeBlockExpandersFor (codeBlockName : Ident) :
   TermElabM (Array (Name × (StrLit → StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock))))
 
-private unsafe def directiveExpandersForUnsafe (directiveName : Ident) :
+unsafe def directiveExpandersForUnsafe (directiveName : Ident) :
     TermElabM (Array (Name × (TSyntaxArray `block → StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock)))) := do
   let x? ←
     try some <$> realizeGlobalConstNoOverload directiveName
@@ -1142,10 +1142,10 @@ private unsafe def directiveExpandersForUnsafe (directiveName : Ident) :
     return hasBuiltin.toArray.flatten
 
 @[implemented_by directiveExpandersForUnsafe]
-private opaque directiveExpandersFor (directiveName : Ident) :
+opaque directiveExpandersFor (directiveName : Ident) :
   TermElabM (Array (Name × (TSyntaxArray `block → StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock))))
 
-private unsafe def commandExpandersForUnsafe (commandName : Ident) :
+unsafe def commandExpandersForUnsafe (commandName : Ident) :
     TermElabM (Array (Name × StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock))) := do
   let x? ←
     try some <$> realizeGlobalConstNoOverload commandName
@@ -1161,18 +1161,18 @@ private unsafe def commandExpandersForUnsafe (commandName : Ident) :
     return hasBuiltin.toArray.flatten
 
 @[implemented_by commandExpandersForUnsafe]
-private opaque commandExpandersFor (commandName : Ident) :
+opaque commandExpandersFor (commandName : Ident) :
   TermElabM (Array (Name × StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock)))
 
 
-private def mkArgVal (arg : TSyntax `arg_val) : DocM Term :=
+def mkArgVal (arg : TSyntax `arg_val) : DocM Term :=
   match arg with
   | `(arg_val|$n:ident) => pure n
   | `(arg_val|$n:num) => pure n
   | `(arg_val|$s:str) => pure s
   | _ => throwErrorAt arg "Didn't understand as argument value"
 
-private def mkArg (arg : TSyntax `doc_arg) : DocM (TSyntax ``Parser.Term.argument) := do
+def mkArg (arg : TSyntax `doc_arg) : DocM (TSyntax ``Parser.Term.argument) := do
   match arg with
   | `(doc_arg|$x:arg_val) =>
     let x ← mkArgVal x
@@ -1190,7 +1190,7 @@ private def mkArg (arg : TSyntax `doc_arg) : DocM (TSyntax ``Parser.Term.argumen
     `(Parser.Term.argument| ($x := $v))
   | _ => throwErrorAt arg "Didn't understand as argument"
 
-private def mkAppStx (name : Ident) (args : TSyntaxArray `doc_arg) : DocM Term := do
+def mkAppStx (name : Ident) (args : TSyntaxArray `doc_arg) : DocM Term := do
   return ⟨mkNode ``Parser.Term.app #[name, mkNullNode (← args.mapM mkArg)]⟩
 
 /--
@@ -1204,7 +1204,7 @@ register_builtin_option doc.verso.suggestions : Bool := {
 -- Normally, name suggestions should be provided relative to the current scope. But
 -- during bootstrapping, the names in question may not yet be defined, so builtin
 -- names need special handling.
-private def suggestionName (name : Name) : TermElabM Name := do
+def suggestionName (name : Name) : TermElabM Name := do
   let name' ←
     -- Builtin expander names never need namespacing
     if (← builtinDocRoles.get).contains name then pure (some name)
@@ -1241,7 +1241,7 @@ private def suggestionName (name : Name) : TermElabM Name := do
         -- Fall back to doing nothing
         pure name
 
-private def sortSuggestions (ss : Array Meta.Hint.Suggestion) : Array Meta.Hint.Suggestion :=
+def sortSuggestions (ss : Array Meta.Hint.Suggestion) : Array Meta.Hint.Suggestion :=
   let cmp : (x y : Meta.Tactic.TryThis.SuggestionText) → Bool
     | .string s1, .string s2 => s1 < s2
     | .string _, _ => true
@@ -1250,7 +1250,7 @@ private def sortSuggestions (ss : Array Meta.Hint.Suggestion) : Array Meta.Hint.
   ss.qsort (cmp ·.suggestion ·.suggestion)
 
 open Diff in
-private def mkSuggestion
+def mkSuggestion
     (ref : Syntax) (hintTitle : MessageData)
     (newStrings : Array (String × Option String × Option String)) :
     DocM MessageData := do
@@ -1281,7 +1281,7 @@ def nameOrBuiltinName [Monad m] [MonadEnv m] (x : Name) : m Name := do
 Finds registered expander names that `x` is a suffix of, for use in error message hints when the
 name is shadowed. Returns display names suitable for `mkSuggestion`.
 -/
-private def findShadowedNames {α : Type}
+def findShadowedNames {α : Type}
     (nonBuiltIns : NameMap (Array Name)) (builtins : NameMap α) (x : Name) :
     TermElabM (Array Name) := do
   if x.isAnonymous then return #[]
@@ -1303,7 +1303,7 @@ private def findShadowedNames {α : Type}
 /--
 Builds a hint for an "Unknown role/directive/..." error when the name might be shadowed.
 -/
-private def shadowedHint {α : Type}
+def shadowedHint {α : Type}
     (envEntries : NameMap (Array Name)) (builtins : NameMap α)
     (name : Ident) (kind : String) : DocM MessageData := do
   let candidates ← findShadowedNames envEntries builtins name.getId
@@ -1316,7 +1316,7 @@ Throws an appropriate error for an unknown doc element (role/directive/code bloc
 Distinguishes "name resolves but isn't registered" from "name doesn't resolve at all",
 and includes shadowed-name suggestions when applicable.
 -/
-private def throwUnknownDocElem {α β : Type}
+def throwUnknownDocElem {α β : Type}
     (envEntries : NameMap (Array Name)) (builtins : NameMap α)
     (name : Ident) (kind : String) : DocM β := do
   let hint ← shadowedHint envEntries builtins name kind
@@ -1545,12 +1545,12 @@ where
   withSpace (s : String) : String :=
     if s.endsWith " " then s else s ++ " "
 
-private def takeFirst? (xs : Array α) : Option (α × Array α) :=
+def takeFirst? (xs : Array α) : Option (α × Array α) :=
   if h : xs.size > 0 then
     some (xs[0], xs.extract 1)
   else none
 
-private partial def elabBlocks' (level : Nat) :
+partial def elabBlocks' (level : Nat) :
     StateT (TSyntaxArray `block) DocM (Array (Block ElabInline ElabBlock) × Array (Part ElabInline ElabBlock Empty)) := do
   let mut pre := #[]
   let mut sub := #[]
@@ -1586,7 +1586,7 @@ private partial def elabBlocks' (level : Nat) :
       break
   return (pre, sub)
 
-private def elabModSnippet'
+def elabModSnippet'
     (range : DeclarationRange) (level : Nat) (blocks : TSyntaxArray `block) :
     DocM VersoModuleDocs.Snippet := do
   let mut snippet : VersoModuleDocs.Snippet := {
@@ -1616,7 +1616,7 @@ private def elabModSnippet'
         snippet := snippet.addBlock (← elabBlock b)
   return snippet
 
-private partial def fixupInline (inl : Inline ElabInline) : DocM (Inline ElabInline) := do
+partial def fixupInline (inl : Inline ElabInline) : DocM (Inline ElabInline) := do
   match inl with
   | .concat xs => .concat <$> xs.mapM fixupInline
   | .emph xs => .emph <$> xs.mapM fixupInline
@@ -1663,7 +1663,7 @@ private partial def fixupInline (inl : Inline ElabInline) : DocM (Inline ElabInl
         return .empty
     | _ => .other i <$> xs.mapM fixupInline
 
-private partial def fixupBlock (block : Block ElabInline ElabBlock) : DocM (Block ElabInline ElabBlock) := do
+partial def fixupBlock (block : Block ElabInline ElabBlock) : DocM (Block ElabInline ElabBlock) := do
   match block with
   | .para xs => .para <$> xs.mapM fixupInline
   | .concat xs => .concat <$> xs.mapM fixupBlock
@@ -1677,7 +1677,7 @@ private partial def fixupBlock (block : Block ElabInline ElabBlock) : DocM (Bloc
   | .code s => pure (.code s)
   | .other i xs => .other i <$> xs.mapM fixupBlock
 
-private partial def fixupPart (part : Part ElabInline ElabBlock Empty) : DocM (Part ElabInline ElabBlock Empty) := do
+partial def fixupPart (part : Part ElabInline ElabBlock Empty) : DocM (Part ElabInline ElabBlock Empty) := do
   return { part with
     title := ← part.title.mapM fixupInline
     content := ← part.content.mapM fixupBlock,
@@ -1685,13 +1685,13 @@ private partial def fixupPart (part : Part ElabInline ElabBlock Empty) : DocM (P
   }
 
 
-private partial def fixupBlocks : (Array (Block ElabInline ElabBlock) × Array (Part ElabInline ElabBlock Empty)) → DocM (Array (Block ElabInline ElabBlock) × Array (Part ElabInline ElabBlock Empty))
+partial def fixupBlocks : (Array (Block ElabInline ElabBlock) × Array (Part ElabInline ElabBlock Empty)) → DocM (Array (Block ElabInline ElabBlock) × Array (Part ElabInline ElabBlock Empty))
   | (bs, ps) => do
     let bs ← bs.mapM fixupBlock
     let ps ← ps.mapM fixupPart
     return (bs, ps)
 
-private partial def fixupSnippet (snippet : VersoModuleDocs.Snippet) : DocM VersoModuleDocs.Snippet := do
+partial def fixupSnippet (snippet : VersoModuleDocs.Snippet) : DocM VersoModuleDocs.Snippet := do
   return {snippet with
     text := ← snippet.text.mapM fixupBlock,
     sections := ← snippet.sections.mapM fun (level, range, content) => do
@@ -1700,7 +1700,7 @@ private partial def fixupSnippet (snippet : VersoModuleDocs.Snippet) : DocM Vers
 /--
 After fixing up the references, check to see which were not used and emit a suitable warning.
 -/
-private def warnUnusedRefs : DocM Unit := do
+def warnUnusedRefs : DocM Unit := do
   for (_, {location, seen, ..}) in (← getThe InternalState).urls do
     unless seen do
       logWarningAt location "Unused URL"

src/Lean/Elab/DocString/Builtin/Keywords.lean

@@ -31,7 +31,7 @@ structure Data.Atom where
 deriving TypeName
 
 
-private def onlyCode [Monad m] [MonadError m] (xs : TSyntaxArray `inline) : m StrLit := do
+def onlyCode [Monad m] [MonadError m] (xs : TSyntaxArray `inline) : m StrLit := do
   if h : xs.size = 1 then
     match xs[0] with
     | `(inline|code($s)) => return s
@@ -43,7 +43,7 @@ private def onlyCode [Monad m] [MonadError m] (xs : TSyntaxArray `inline) : m St
 /--
 Checks whether a syntax descriptor's value contains the given atom.
 -/
-private partial def containsAtom (e : Expr) (atom : String) : MetaM Bool := do
+partial def containsAtom (e : Expr) (atom : String) : MetaM Bool := do
   let rec attempt (p : Expr) (tryWhnf : Bool) : MetaM Bool := do
     match p.getAppFnArgs with
     | (``ParserDescr.node, #[_, _, p]) => containsAtom p atom
@@ -67,7 +67,7 @@ private partial def containsAtom (e : Expr) (atom : String) : MetaM Bool := do
 Checks whether a syntax descriptor's value contains the given atom. If so, the residual value after
 the atom is returned.
 -/
-private partial def containsAtom' (e : Expr) (atom : String) : MetaM (Option Expr) := do
+partial def containsAtom' (e : Expr) (atom : String) : MetaM (Option Expr) := do
   let rec attempt (p : Expr) (tryWhnf : Bool) : MetaM (Option Expr) := do
     match p.getAppFnArgs with
     | (``ParserDescr.node, #[_, _, p]) => containsAtom' p atom
@@ -92,7 +92,7 @@ private partial def containsAtom' (e : Expr) (atom : String) : MetaM (Option Exp
     | _ => if tryWhnf then attempt (← Meta.whnf p) false else pure none
   attempt e true
 
-private partial def canEpsilon (e : Expr) : MetaM Bool := do
+partial def canEpsilon (e : Expr) : MetaM Bool := do
   let rec attempt (p : Expr) (tryWhnf : Bool) : MetaM Bool := do
     match p.getAppFnArgs with
     | (``ParserDescr.node, #[_, _, p]) => canEpsilon p
@@ -118,7 +118,7 @@ private partial def canEpsilon (e : Expr) : MetaM Bool := do
 Checks whether a syntax descriptor's value begins with the given atom. If so, the residual value
 after the atom is returned.
 -/
-private partial def startsWithAtom? (e : Expr) (atom : String) : MetaM (Option Expr) := do
+partial def startsWithAtom? (e : Expr) (atom : String) : MetaM (Option Expr) := do
   let rec attempt (p : Expr) (tryWhnf : Bool) : MetaM (Option Expr) := do
     match p.getAppFnArgs with
     | (``ParserDescr.node, #[_, _, p]) => startsWithAtom? p atom
@@ -149,7 +149,7 @@ private partial def startsWithAtom? (e : Expr) (atom : String) : MetaM (Option E
 Checks whether a syntax descriptor's value begins with the given atoms. If so, the residual value
 after the atoms is returned.
 -/
-private partial def startsWithAtoms? (e : Expr) (atoms : List String) : MetaM (Option Expr) := do
+partial def startsWithAtoms? (e : Expr) (atoms : List String) : MetaM (Option Expr) := do
   match atoms with
   | [] => pure e
   | a :: as =>
@@ -157,7 +157,7 @@ private partial def startsWithAtoms? (e : Expr) (atoms : List String) : MetaM (O
       startsWithAtoms? e' as
     else pure none
 
-private partial def exprContainsAtoms (e : Expr) (atoms : List String) : MetaM Bool := do
+partial def exprContainsAtoms (e : Expr) (atoms : List String) : MetaM Bool := do
   match atoms with
   | [] => pure true
   | a :: as =>
@@ -165,7 +165,7 @@ private partial def exprContainsAtoms (e : Expr) (atoms : List String) : MetaM B
       (startsWithAtoms? e' as <&> Option.isSome) <||> exprContainsAtoms e' (a :: as)
     else pure false
 
-private def withAtom (cat : Name) (atom : String) : DocM (Array Name) := do
+def withAtom (cat : Name) (atom : String) : DocM (Array Name) := do
   let env ← getEnv
   let some catContents := (Lean.Parser.parserExtension.getState env).categories.find? cat
     | return #[]
@@ -177,7 +177,7 @@ private def withAtom (cat : Name) (atom : String) : DocM (Array Name) := do
         found := found.push k
   return found
 
-private partial def isAtoms (atoms : List String) (stx : Syntax) : Bool :=
+partial def isAtoms (atoms : List String) (stx : Syntax) : Bool :=
   StateT.run (go [stx]) atoms |>.fst
 where
   go (stxs : List Syntax) : StateM (List String) Bool := do
@@ -196,7 +196,7 @@ where
       | .node _ _ args :: ss =>
         go (args.toList ++ ss)
 
-private def parserHasAtomPrefix (atoms : List String) (p : Parser) : TermElabM Bool := do
+def parserHasAtomPrefix (atoms : List String) (p : Parser) : TermElabM Bool := do
   let str := " ".intercalate atoms
   let env ← getEnv
   let options ← getOptions
@@ -206,16 +206,16 @@ private def parserHasAtomPrefix (atoms : List String) (p : Parser) : TermElabM B
   let s := p.fn.run {inputString := str, fileName := "", fileMap := FileMap.ofString str} {env, options} (getTokenTable env) s
   return isAtoms atoms (mkNullNode (s.stxStack.extract 1 s.stxStack.size))
 
-private unsafe def namedParserHasAtomPrefixUnsafe (atoms : List String) (parserName : Name) : TermElabM Bool := do
+unsafe def namedParserHasAtomPrefixUnsafe (atoms : List String) (parserName : Name) : TermElabM Bool := do
   try
     let p ← evalConstCheck Parser ``Parser parserName
     parserHasAtomPrefix atoms p
   catch | _ => pure false
 
 @[implemented_by namedParserHasAtomPrefixUnsafe]
-private opaque namedParserHasAtomPrefix (atoms : List String) (parserName : Name) : TermElabM Bool
+opaque namedParserHasAtomPrefix (atoms : List String) (parserName : Name) : TermElabM Bool
 
-private def parserDescrCanEps : ParserDescr → Bool
+def parserDescrCanEps : ParserDescr → Bool
   | .node _ _ p | .trailingNode _ _ _ p => parserDescrCanEps p
   | .binary ``Parser.andthen p1 p2 => parserDescrCanEps p1 && parserDescrCanEps p2
   | .binary ``Parser.orelse p1 p2 => parserDescrCanEps p1 || parserDescrCanEps p2
@@ -227,7 +227,7 @@ private def parserDescrCanEps : ParserDescr → Bool
   | .const ``Parser.ppHardSpace => true
   | _ => false
 
-private def parserDescrHasAtom (atom : String) (p : ParserDescr) : TermElabM (Option ParserDescr) := do
+def parserDescrHasAtom (atom : String) (p : ParserDescr) : TermElabM (Option ParserDescr) := do
   match p with
   | .node _ _ p | .trailingNode _ _ _ p | .unary _ p =>
     parserDescrHasAtom atom p
@@ -249,7 +249,7 @@ private def parserDescrHasAtom (atom : String) (p : ParserDescr) : TermElabM (Op
     | none, none => pure none
   | _ => pure none
 
-private def parserDescrStartsWithAtom (atom : String) (p : ParserDescr) : TermElabM (Option ParserDescr) := do
+def parserDescrStartsWithAtom (atom : String) (p : ParserDescr) : TermElabM (Option ParserDescr) := do
   match p with
   | .node _ _ p | .trailingNode _ _ _ p | .unary _ p =>
     parserDescrStartsWithAtom atom p
@@ -272,7 +272,7 @@ private def parserDescrStartsWithAtom (atom : String) (p : ParserDescr) : TermEl
     | none, none => pure none
   | _ => pure none
 
-private def parserDescrStartsWithAtoms (atoms : List String) (p : ParserDescr) : TermElabM Bool := do
+def parserDescrStartsWithAtoms (atoms : List String) (p : ParserDescr) : TermElabM Bool := do
   match atoms with
   | [] => pure true
   | a :: as =>
@@ -280,7 +280,7 @@ private def parserDescrStartsWithAtoms (atoms : List String) (p : ParserDescr) :
       parserDescrStartsWithAtoms as p'
     else pure false
 
-private partial def parserDescrHasAtoms (atoms : List String) (p : ParserDescr) : TermElabM Bool := do
+partial def parserDescrHasAtoms (atoms : List String) (p : ParserDescr) : TermElabM Bool := do
   match atoms with
   | [] => pure true
   | a :: as =>
@@ -289,16 +289,16 @@ private partial def parserDescrHasAtoms (atoms : List String) (p : ParserDescr)
       else parserDescrHasAtoms (a :: as) p'
     else pure false
 
-private unsafe def parserDescrNameHasAtomsUnsafe (atoms : List String) (p : Name) : TermElabM Bool := do
+unsafe def parserDescrNameHasAtomsUnsafe (atoms : List String) (p : Name) : TermElabM Bool := do
   try
     let p ← evalConstCheck ParserDescr ``ParserDescr p
     parserDescrHasAtoms atoms p
   catch | _ => pure false
 
 @[implemented_by parserDescrNameHasAtomsUnsafe]
-private opaque parserDescrNameHasAtoms (atoms : List String) (p : Name) : TermElabM Bool
+opaque parserDescrNameHasAtoms (atoms : List String) (p : Name) : TermElabM Bool
 
-private def kindHasAtoms (k : Name) (atoms : List String) : TermElabM Bool := do
+def kindHasAtoms (k : Name) (atoms : List String) : TermElabM Bool := do
   let env ← getEnv
   if let some ci := env.find? k then
     if let some d := ci.value? then
@@ -312,7 +312,7 @@ private def kindHasAtoms (k : Name) (atoms : List String) : TermElabM Bool := do
         return true
   return false
 
-private def withAtoms (cat : Name) (atoms : List String) : TermElabM (Array Name) := do
+def withAtoms (cat : Name) (atoms : List String) : TermElabM (Array Name) := do
   let env ← getEnv
   let some catContents := (Lean.Parser.parserExtension.getState env).categories.find? cat
     | return #[]
@@ -323,7 +323,7 @@ private def withAtoms (cat : Name) (atoms : List String) : TermElabM (Array Name
       found := found.push k
   return found
 
-private def kwImpl (cat : Ident := mkIdent .anonymous) (of : Ident := mkIdent .anonymous)
+def kwImpl (cat : Ident := mkIdent .anonymous) (of : Ident := mkIdent .anonymous)
     (suggest : Bool)
     (s : StrLit) : TermElabM (Inline ElabInline) := do
   let atoms := s.getString |>.split Char.isWhitespace |>.toStringList

src/Lean/Elab/Import.lean

@@ -10,6 +10,7 @@ public import Lean.Parser.Module
 meta import Lean.Parser.Module
 import Lean.Compiler.ModPkgExt
 public import Lean.DeprecatedModule
+import Init.Data.String.Modify
 
 public section
 
@@ -28,7 +29,9 @@ def HeaderSyntax.isModule (header : HeaderSyntax) : Bool :=
 def HeaderSyntax.imports (stx : HeaderSyntax) (includeInit : Bool := true) : Array Import :=
   match stx with
   | `(Parser.Module.header| $[module%$moduleTk]? $[prelude%$preludeTk]? $importsStx*) =>
-    let imports := if preludeTk.isNone && includeInit then #[{ module := `Init : Import }] else #[]
+    let imports := if preludeTk.isNone && includeInit then
+        #[{ module := `Init : Import }, { module := `Init, isMeta := true : Import }]
+      else #[]
     imports ++ importsStx.map fun
       | `(Parser.Module.import| $[public%$publicTk]? $[meta%$metaTk]? import $[all%$allTk]? $n) =>
         { module := n.getId, importAll := allTk.isSome
@@ -95,6 +98,43 @@ def checkDeprecatedImports
       | none => messages
     | none => messages
 
+private def osForbiddenChars : Array Char :=
+  #['<', '>', '"', '|', '?', '*', '!']
+
+private def osForbiddenNames : Array String :=
+  #["CON", "PRN", "AUX", "NUL",
+    "COM1", "COM2", "COM3", "COM4", "COM5", "COM6", "COM7", "COM8", "COM9",
+    "COM¹", "COM²", "COM³",
+    "LPT1", "LPT2", "LPT3", "LPT4", "LPT5", "LPT6", "LPT7", "LPT8", "LPT9",
+    "LPT¹", "LPT²", "LPT³"]
+
+private def checkComponentPortability (comp : String) : Option String :=
+  if osForbiddenNames.contains comp.toUpper then
+    some s!"'{comp}' is a reserved file name on some operating systems"
+  else if let some c := osForbiddenChars.find? (comp.contains ·) then
+    some s!"contains character '{c}' which is forbidden on some operating systems"
+  else
+    none
+
+def checkModuleNamePortability
+    (mainModule : Name) (inputCtx : Parser.InputContext) (startPos : String.Pos.Raw)
+    (messages : MessageLog) : MessageLog :=
+  go mainModule messages
+where
+  go : Name → MessageLog → MessageLog
+    | .anonymous, messages => messages
+    | .str parent s, messages =>
+      let messages := match checkComponentPortability s with
+        | some reason => messages.add {
+            fileName := inputCtx.fileName
+            pos := inputCtx.fileMap.toPosition startPos
+            severity := .error
+            data := s!"module name '{mainModule}' is not portable: {reason}"
+          }
+        | none => messages
+      go parent messages
+    | .num parent _, messages => go parent messages
+
 def processHeaderCore
     (startPos : String.Pos.Raw) (imports : Array Import) (isModule : Bool)
     (opts : Options) (messages : MessageLog) (inputCtx : Parser.InputContext)
@@ -122,6 +162,7 @@ def processHeaderCore
     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?
+  let messages := checkModuleNamePortability mainModule inputCtx startPos messages
   return (env, messages)
 
 /--

src/Lean/Elab/ParseImportsFast.lean

@@ -233,7 +233,7 @@ def setImportAll : Parser := fun _ s =>
 
 def main : Parser :=
   keywordCore "module" (setIsModule false) (setIsModule true) >>
-  keywordCore "prelude" (fun _ s => s.pushImport `Init) skip >>
+  keywordCore "prelude" (fun _ s => (s.pushImport `Init).pushImport { module := `Init, isMeta := true }) skip >>
   manyImports (atomic (keywordCore "public" skip setExported >>
     keywordCore "meta" skip setMeta >>
     keyword "import") >>

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -55,7 +55,7 @@ def unfoldLHS (declName : Name) (mvarId : MVarId) : MetaM MVarId := mvarId.withC
     -- Else use delta reduction
     deltaLHS mvarId
 
-private partial def mkEqnProof (declName : Name) (type : Expr) : MetaM Expr := do
+partial def mkEqnProof (declName : Name) (type : Expr) : MetaM Expr := do
   withTraceNode `Elab.definition.eqns (fun _ => return m!"proving:{indentExpr type}") do
   withNewMCtxDepth do
     let main ← mkFreshExprSyntheticOpaqueMVar type
@@ -102,7 +102,7 @@ private partial def mkEqnProof (declName : Name) (type : Expr) : MetaM Expr := d
         else
           throwError "failed to generate equational theorem for `{.ofConstName declName}`\n{MessageData.ofGoal mvarId}"
 
-private def lhsDependsOn (type : Expr) (fvarId : FVarId) : MetaM Bool :=
+def lhsDependsOn (type : Expr) (fvarId : FVarId) : MetaM Bool :=
   forallTelescope type fun _ type => do
     if let some (_, lhs, _) ← matchEq? type then
       dependsOn lhs fvarId

src/Lean/Elab/Quotation/Precheck.lean

@@ -113,7 +113,7 @@ private def isSectionVariable (e : Expr) : TermElabM Bool := do
     if (← read).quotLCtx.contains val then
       return
     let rs ← try resolveName stx val [] [] catch _ => pure []
-    for (e, _) in rs do
+    for (e, _, _) in rs do
       match e with
       | Expr.fvar _      .. =>
         if quotPrecheck.allowSectionVars.get (← getOptions) && (← isSectionVariable e) then

src/Lean/Elab/Tactic/BVDecide/Frontend/BVCheck.lean

@@ -36,7 +36,7 @@ def mkContext (lratPath : System.FilePath) (cfg : BVDecideConfig) : TermElabM Ta
   TacticContext.new lratPath cfg
 
 /--
-Prepare an `Expr` that proves `bvExpr.unsat` using native evalution.
+Prepare an `Expr` that proves `bvExpr.unsat` using native evaluation.
 -/
 def lratChecker (ctx : TacticContext) (reflectionResult : ReflectionResult) : MetaM Expr := do
   let cert ← LratCert.ofFile ctx.lratPath ctx.config.trimProofs

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean

@@ -357,6 +357,7 @@ def reflectBV (g : MVarId) : M ReflectionResult := g.withContext do
   let mut sats := #[]
   let mut unusedHypotheses := {}
   for hyp in hyps do
+    checkSystem "bv_decide"
     if let (some reflected, lemmas) ← (SatAtBVLogical.of (mkFVar hyp)).run then
       sats := (sats ++ lemmas).push reflected
     else

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean

@@ -33,6 +33,7 @@ where
   Reify `x`, returns `none` if the reification procedure failed.
   -/
   go (origExpr : Expr) : LemmaM (Option ReifiedBVExpr) := do
+    checkSystem "bv_decide"
     match_expr origExpr with
     | BitVec.ofNat _ _ => goBvLit origExpr
     | HAnd.hAnd _ _ _ _ lhsExpr rhsExpr =>
@@ -340,6 +341,7 @@ where
   Reify `t`, returns `none` if the reification procedure failed.
   -/
   go (origExpr : Expr) : LemmaM (Option ReifiedBVLogical) := do
+    checkSystem "bv_decide"
     match_expr origExpr with
     | Bool.true => ReifiedBVLogical.mkBoolConst true
     | Bool.false => ReifiedBVLogical.mkBoolConst false

src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Basic.lean

@@ -159,6 +159,7 @@ Repeatedly run a list of `Pass` until they either close the goal or an iteration
 the goal anymore.
 -/
 partial def fixpointPipeline (passes : List Pass) (goal : MVarId) : PreProcessM (Option MVarId) := do
+  checkSystem "bv_decide"
   let mut newGoal := goal
   for pass in passes do
     if let some nextGoal ← pass.run newGoal then

src/Lean/Elab/Term/TermElabM.lean

@@ -232,7 +232,10 @@ structure TacticFinishedSnapshot extends Language.Snapshot where
   state? : Option SavedState
   /-- Untyped snapshots from `logSnapshotTask`, saved at this level for cancellation. -/
   moreSnaps : Array (SnapshotTask SnapshotTree)
-deriving Inhabited
+
+instance : Inhabited TacticFinishedSnapshot where
+  default := { toSnapshot := default, state? := default, moreSnaps := default }
+
 instance : ToSnapshotTree TacticFinishedSnapshot where
   toSnapshotTree s := ⟨s.toSnapshot, s.moreSnaps⟩
 
@@ -246,7 +249,10 @@ structure TacticParsedSnapshot extends Language.Snapshot where
   finished : SnapshotTask TacticFinishedSnapshot
   /-- Tasks for subsequent, potentially parallel, tactic steps. -/
   next     : Array (SnapshotTask TacticParsedSnapshot) := #[]
-deriving Inhabited
+
+instance : Inhabited TacticParsedSnapshot where
+  default := { toSnapshot := default, stx := default, finished := default }
+
 partial instance : ToSnapshotTree TacticParsedSnapshot where
   toSnapshotTree := go where
     go := fun s => ⟨s.toSnapshot,
@@ -627,13 +633,13 @@ builtin_initialize termElabAttribute : KeyedDeclsAttribute TermElab ← mkTermEl
   `[LVal.fieldName "foo", LVal.fieldIdx 1]`.
 -/
 inductive LVal where
-  | fieldIdx  (ref : Syntax) (i : Nat)
+  | fieldIdx  (ref : Syntax) (i : Nat) (levels : List Level)
   /-- Field `suffix?` is for producing better error messages because `x.y` may be a field access or a hierarchical/composite name.
   `ref` is the syntax object representing the field. `fullRef` includes the LHS. -/
-  | fieldName (ref : Syntax) (name : String) (suffix? : Option Name) (fullRef : Syntax)
+  | fieldName (ref : Syntax) (name : String) (levels : List Level) (suffix? : Option Name) (fullRef : Syntax)
 
 def LVal.getRef : LVal → Syntax
-  | .fieldIdx ref _    => ref
+  | .fieldIdx ref ..   => ref
   | .fieldName ref ..  => ref
 
 def LVal.isFieldName : LVal → Bool
@@ -642,8 +648,11 @@ def LVal.isFieldName : LVal → Bool
 
 instance : ToString LVal where
   toString
-    | .fieldIdx _ i     => toString i
-    | .fieldName _ n .. => n
+    | .fieldIdx _ i levels ..  => toString i ++ levelsToString levels
+    | .fieldName _ n levels .. => n ++ levelsToString levels
+where
+  levelsToString levels :=
+    if levels.isEmpty then "" else ".{" ++ String.intercalate "," (levels.map toString) ++ "}"
 
 /-- Return the name of the declaration being elaborated if available. -/
 def getDeclName? : TermElabM (Option Name) := return (← read).declName?
@@ -2111,8 +2120,10 @@ def checkDeprecated (ref : Syntax) (e : Expr) : TermElabM Unit := do
 @[inline] def withoutCheckDeprecated [MonadWithReaderOf Context m] : m α → m α :=
   withTheReader Context (fun ctx => { ctx with checkDeprecated := false })
 
-private def mkConsts (candidates : List (Name × List String)) (explicitLevels : List Level) : TermElabM (List (Expr × List String)) := do
+private def mkConsts (candidates : List (Name × List String)) (explicitLevels : List Level) : TermElabM (List (Expr × List String × List Level)) := do
   candidates.foldlM (init := []) fun result (declName, projs) => do
+    -- levels apply to the last projection, not the constant
+    let (constLevels, projLevels) := if projs.isEmpty then (explicitLevels, []) else ([], explicitLevels)
     -- TODO: better support for `mkConst` failure. We may want to cache the failures, and report them if all candidates fail.
     /-
     We disable `checkDeprecated` here because there may be many overloaded symbols.
@@ -2121,25 +2132,38 @@ private def mkConsts (candidates : List (Name × List String)) (explicitLevels :
     At `elabAppFnId`, we perform the check when converting the list returned by `resolveName'` into a list of
     `TermElabResult`s.
     -/
-    let const ← withoutCheckDeprecated <| mkConst declName explicitLevels
-    return (const, projs) :: result
+    let const ← withoutCheckDeprecated <| mkConst declName constLevels
+    return (const, projs, projLevels) :: 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
+/--
+  Gives all resolutions of the name `n`.
+
+- `explicitLevels` provides a prefix of level parameters to the constant. For resolutions with a projection
+  component, the levels are not used, since they must apply to the last projection, not the constant.
+  In that case, the third component of the tuple is `explicitLevels`.
+-/
+def resolveName (stx : Syntax) (n : Name) (preresolved : List Syntax.Preresolved) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (List (Expr × List String × List Level)) := do
   addCompletionInfo <| CompletionInfo.id stx stx.getId (danglingDot := false) (← getLCtx) expectedType?
+  let processLocal (e : Expr) (projs : List String) := do
+    if projs.isEmpty then
+      if explicitLevels.isEmpty then
+        return [(e, [], [])]
+      else
+        throwInvalidExplicitUniversesForLocal e
+    else
+      return [(e, projs, explicitLevels)]
   if let some (e, projs) ← resolveLocalName n then
-    unless explicitLevels.isEmpty do
-      throwInvalidExplicitUniversesForLocal e
-    return [(e, projs)]
+    return ← processLocal e projs
   let preresolved := preresolved.filterMap fun
     | .decl n projs => some (n, projs)
     | _             => none
   -- check for section variable capture by a quotation
   let ctx ← read
   if let some (e, projs) := preresolved.findSome? fun (n, projs) => ctx.sectionFVars.find? n |>.map (·, projs) then
-    return [(e, projs)]  -- section variables should shadow global decls
+    return ← processLocal e projs  -- section variables should shadow global decls
   if preresolved.isEmpty then
     mkConsts (← realizeGlobalName n) explicitLevels
   else
@@ -2148,14 +2172,17 @@ def resolveName (stx : Syntax) (n : Name) (preresolved : List Syntax.Preresolved
 /--
   Similar to `resolveName`, but creates identifiers for the main part and each projection with position information derived from `ident`.
   Example: Assume resolveName `v.head.bla.boo` produces `(v.head, ["bla", "boo"])`, then this method produces
-  `(v.head, id, [f₁, f₂])` where `id` is an identifier for `v.head`, and `f₁` and `f₂` are identifiers for fields `"bla"` and `"boo"`. -/
-def resolveName' (ident : Syntax) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (Name × List (Expr × Syntax × List Syntax)) := do
+  `(v.head, id, [f₁, f₂])` where `id` is an identifier for `v.head`, and `f₁` and `f₂` are identifiers for fields `"bla"` and `"boo"`.
+
+  See the comment there about `explicitLevels` and the meaning of the `List Level` component of the returned tuple.
+-/
+def resolveName' (ident : Syntax) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (Name × List (Expr × Syntax × List Syntax × List Level)) := do
   let .ident _ _ n preresolved := ident
     | throwError "identifier expected"
   let r ← resolveName ident n preresolved explicitLevels expectedType?
-  let rc ← r.mapM fun (c, fields) => do
+  let rc ← r.mapM fun (c, fields, levels) => do
     let ids := ident.identComponents (nFields? := fields.length)
-    return (c, ids.head!, ids.tail!)
+    return (c, ids.head!, ids.tail!, levels)
   return (n, rc)
 
 
@@ -2163,7 +2190,7 @@ def resolveId? (stx : Syntax) (kind := "term") (withInfo := false) : TermElabM (
   match stx with
   | .ident _ _ val preresolved =>
     let rs ← try resolveName stx val preresolved [] catch _ => pure []
-    let rs := rs.filter fun ⟨_, projs⟩ => projs.isEmpty
+    let rs := rs.filter fun ⟨_, projs, _⟩ => projs.isEmpty
     let fs := rs.map fun (f, _) => f
     match fs with
     | []  => return none