chore: reduce benchmark stack usage

We are running out of stack space in debug mode
chore: recursion => while at instantiate_mvars_fn
2026-03-18 02:44:12 +00:00 · 2024-08-06 10:23:25 -07:00 · 2024-08-06 10:23:25 -07:00 · 2024-08-06 15:27:20 +00:00 · 2024-08-06 15:17:23 +00:00 · 2024-08-06 08:19:33 +00:00
311 changed files with 2149 additions and 1477 deletions
--- a/.github/workflows/nix-ci.yml
+++ b/.github/workflows/nix-ci.yml
@@ -103,7 +103,7 @@ jobs:
        continue-on-error: true
      - name: Build manual
        run: |
-          nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc#{lean-mdbook,leanInk,alectryon,test,inked} -o push-doc
+          nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc#{lean-mdbook,leanInk,alectryon,inked} -o push-doc
          nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc
          # https://github.com/netlify/cli/issues/1809
          cp -r --dereference ./result ./dist
@@ -146,5 +146,3 @@ jobs:
      - name: Fixup CCache Cache
        run: |
          sudo chown -R $USER /nix/var/cache
-      - name: CCache stats
-        run: CCACHE_DIR=/nix/var/cache/ccache nix run .#nixpkgs.ccache -- -s
--- a/doc/dev/release_checklist.md
+++ b/doc/dev/release_checklist.md
@@ -147,16 +147,10 @@ We'll use `v4.7.0-rc1` as the intended release version in this example.
  - You can monitor this at `https://github.com/leanprover/lean4/actions/workflows/ci.yml`, looking for the `v4.7.0-rc1` tag.
  - This step can take up to an hour.
 - (GitHub release notes) Once the release appears at https://github.com/leanprover/lean4/releases/
-  - Edit the release notes on Github to select the "Set as a pre-release box".
-  - If release notes have been written already, copy the section of `RELEASES.md` for this version into the Github release notes
-    and use the title "Changes since v4.6.0 (from RELEASES.md)".
-  - Otherwise, in the "previous tag" dropdown, select `v4.6.0`, and click "Generate release notes".
+  - Verify that the release is marked as a prerelease (this should have been done automatically by the CI release job).
+  - In the "previous tag" dropdown, select `v4.6.0`, and click "Generate release notes".
    This will add a list of all the commits since the last stable version.
-    - Delete anything already mentioned in the hand-written release notes above.
    - Delete "update stage0" commits, and anything with a completely inscrutable commit message.
-    - Briefly rearrange the remaining items by category (e.g. `simp`, `lake`, `bug fixes`),
-      but for minor items don't put any work in expanding on commit messages.
-  - (How we want to release notes to look is evolving: please update this section if it looks wrong!)
 - Next, we will move a curated list of downstream repos to the release candidate.
  - This assumes that there is already a *reviewed* branch `bump/v4.7.0` on each repository
    containing the required adaptations (or no adaptations are required).
--- a/doc/flake.lock
+++ b/doc/flake.lock
@@ -18,12 +18,15 @@
      }
    },
    "flake-utils": {
+      "inputs": {
+        "systems": "systems"
+      },
      "locked": {
-        "lastModified": 1656928814,
-        "narHash": "sha256-RIFfgBuKz6Hp89yRr7+NR5tzIAbn52h8vT6vXkYjZoM=",
+        "lastModified": 1710146030,
+        "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=",
        "owner": "numtide",
        "repo": "flake-utils",
-        "rev": "7e2a3b3dfd9af950a856d66b0a7d01e3c18aa249",
+        "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a",
        "type": "github"
      },
      "original": {
@@ -35,13 +38,12 @@
    "lean": {
      "inputs": {
        "flake-utils": "flake-utils",
-        "lean4-mode": "lean4-mode",
-        "nix": "nix",
-        "nixpkgs": "nixpkgs_2"
+        "nixpkgs": "nixpkgs",
+        "nixpkgs-old": "nixpkgs-old"
      },
      "locked": {
        "lastModified": 0,
-        "narHash": "sha256-YnYbmG0oou1Q/GE4JbMNb8/yqUVXBPIvcdQQJHBqtPk=",
+        "narHash": "sha256-saRAtQ6VautVXKDw1XH35qwP0KEBKTKZbg/TRa4N9Vw=",
        "path": "../.",
        "type": "path"
      },
@@ -50,22 +52,6 @@
        "type": "path"
      }
    },
-    "lean4-mode": {
-      "flake": false,
-      "locked": {
-        "lastModified": 1659020985,
-        "narHash": "sha256-+dRaXB7uvN/weSZiKcfSKWhcdJVNg9Vg8k0pJkDNjpc=",
-        "owner": "leanprover",
-        "repo": "lean4-mode",
-        "rev": "37d5c99b7b29c80ab78321edd6773200deb0bca6",
-        "type": "github"
-      },
-      "original": {
-        "owner": "leanprover",
-        "repo": "lean4-mode",
-        "type": "github"
-      }
-    },
    "leanInk": {
      "flake": false,
      "locked": {
@@ -83,22 +69,6 @@
        "type": "github"
      }
    },
-    "lowdown-src": {
-      "flake": false,
-      "locked": {
-        "lastModified": 1633514407,
-        "narHash": "sha256-Dw32tiMjdK9t3ETl5fzGrutQTzh2rufgZV4A/BbxuD4=",
-        "owner": "kristapsdz",
-        "repo": "lowdown",
-        "rev": "d2c2b44ff6c27b936ec27358a2653caaef8f73b8",
-        "type": "github"
-      },
-      "original": {
-        "owner": "kristapsdz",
-        "repo": "lowdown",
-        "type": "github"
-      }
-    },
    "mdBook": {
      "flake": false,
      "locked": {
@@ -115,65 +85,13 @@
        "type": "github"
      }
    },
-    "nix": {
-      "inputs": {
-        "lowdown-src": "lowdown-src",
-        "nixpkgs": "nixpkgs",
-        "nixpkgs-regression": "nixpkgs-regression"
-      },
-      "locked": {
-        "lastModified": 1657097207,
-        "narHash": "sha256-SmeGmjWM3fEed3kQjqIAO8VpGmkC2sL1aPE7kKpK650=",
-        "owner": "NixOS",
-        "repo": "nix",
-        "rev": "f6316b49a0c37172bca87ede6ea8144d7d89832f",
-        "type": "github"
-      },
-      "original": {
-        "owner": "NixOS",
-        "repo": "nix",
-        "type": "github"
-      }
-    },
    "nixpkgs": {
      "locked": {
-        "lastModified": 1653988320,
-        "narHash": "sha256-ZaqFFsSDipZ6KVqriwM34T739+KLYJvNmCWzErjAg7c=",
+        "lastModified": 1710889954,
+        "narHash": "sha256-Pr6F5Pmd7JnNEMHHmspZ0qVqIBVxyZ13ik1pJtm2QXk=",
        "owner": "NixOS",
        "repo": "nixpkgs",
-        "rev": "2fa57ed190fd6c7c746319444f34b5917666e5c1",
-        "type": "github"
-      },
-      "original": {
-        "owner": "NixOS",
-        "ref": "nixos-22.05-small",
-        "repo": "nixpkgs",
-        "type": "github"
-      }
-    },
-    "nixpkgs-regression": {
-      "locked": {
-        "lastModified": 1643052045,
-        "narHash": "sha256-uGJ0VXIhWKGXxkeNnq4TvV3CIOkUJ3PAoLZ3HMzNVMw=",
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2",
-        "type": "github"
-      },
-      "original": {
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2",
-        "type": "github"
-      }
-    },
-    "nixpkgs_2": {
-      "locked": {
-        "lastModified": 1657208011,
-        "narHash": "sha256-BlIFwopAykvdy1DYayEkj6ZZdkn+cVgPNX98QVLc0jM=",
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "2770cc0b1e8faa0e20eb2c6aea64c256a706d4f2",
+        "rev": "7872526e9c5332274ea5932a0c3270d6e4724f3b",
        "type": "github"
      },
      "original": {
@@ -183,6 +101,23 @@
        "type": "github"
      }
    },
+    "nixpkgs-old": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1581379743,
+        "narHash": "sha256-i1XCn9rKuLjvCdu2UeXKzGLF6IuQePQKFt4hEKRU5oc=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "34c7eb7545d155cc5b6f499b23a7cb1c96ab4d59",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "ref": "nixos-19.03",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
    "root": {
      "inputs": {
        "alectryon": "alectryon",
@@ -194,6 +129,21 @@
        "leanInk": "leanInk",
        "mdBook": "mdBook"
      }
+    },
+    "systems": {
+      "locked": {
+        "lastModified": 1681028828,
+        "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
+        "owner": "nix-systems",
+        "repo": "default",
+        "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-systems",
+        "repo": "default",
+        "type": "github"
+      }
    }
  },
  "root": "root",
--- a/doc/flake.nix
+++ b/doc/flake.nix
@@ -17,7 +17,7 @@
  };

  outputs = inputs@{ self, ... }: inputs.flake-utils.lib.eachDefaultSystem (system:
-    with inputs.lean.packages.${system}; with nixpkgs;
+    with inputs.lean.packages.${system}.deprecated; with nixpkgs;
    let
      doc-src = lib.sourceByRegex ../. ["doc.*" "tests(/lean(/beginEndAsMacro.lean)?)?"];
    in {
@@ -44,21 +44,6 @@
          mdbook build -d $out
        '';
      };
-      # We use a separate derivation instead of `checkPhase` so we can push it but not `doc` to the binary cache
-      test = stdenv.mkDerivation {
-        name ="lean-doc-test";
-        src = doc-src;
-        buildInputs = [ lean-mdbook stage1.Lean.lean-package strace ];
-        patchPhase = ''
-          cd doc
-          patchShebangs test
-        '';
-        buildPhase = ''
-          mdbook test
-          touch $out
-        '';
-        dontInstall = true;
-      };
      leanInk = (buildLeanPackage {
        name = "Main";
        src = inputs.leanInk;
--- a/flake.lock
+++ b/flake.lock
@@ -1,21 +1,5 @@
 {
  "nodes": {
-    "flake-compat": {
-      "flake": false,
-      "locked": {
-        "lastModified": 1673956053,
-        "narHash": "sha256-4gtG9iQuiKITOjNQQeQIpoIB6b16fm+504Ch3sNKLd8=",
-        "owner": "edolstra",
-        "repo": "flake-compat",
-        "rev": "35bb57c0c8d8b62bbfd284272c928ceb64ddbde9",
-        "type": "github"
-      },
-      "original": {
-        "owner": "edolstra",
-        "repo": "flake-compat",
-        "type": "github"
-      }
-    },
    "flake-utils": {
      "inputs": {
        "systems": "systems"
@@ -34,71 +18,18 @@
        "type": "github"
      }
    },
-    "lean4-mode": {
-      "flake": false,
-      "locked": {
-        "lastModified": 1709737301,
-        "narHash": "sha256-uT9JN2kLNKJK9c/S/WxLjiHmwijq49EgLb+gJUSDpz0=",
-        "owner": "leanprover",
-        "repo": "lean4-mode",
-        "rev": "f1f24c15134dee3754b82c9d9924866fe6bc6b9f",
-        "type": "github"
-      },
-      "original": {
-        "owner": "leanprover",
-        "repo": "lean4-mode",
-        "type": "github"
-      }
-    },
-    "libgit2": {
-      "flake": false,
-      "locked": {
-        "lastModified": 1697646580,
-        "narHash": "sha256-oX4Z3S9WtJlwvj0uH9HlYcWv+x1hqp8mhXl7HsLu2f0=",
-        "owner": "libgit2",
-        "repo": "libgit2",
-        "rev": "45fd9ed7ae1a9b74b957ef4f337bc3c8b3df01b5",
-        "type": "github"
-      },
-      "original": {
-        "owner": "libgit2",
-        "repo": "libgit2",
-        "type": "github"
-      }
-    },
-    "nix": {
-      "inputs": {
-        "flake-compat": "flake-compat",
-        "libgit2": "libgit2",
-        "nixpkgs": "nixpkgs",
-        "nixpkgs-regression": "nixpkgs-regression"
-      },
-      "locked": {
-        "lastModified": 1711102798,
-        "narHash": "sha256-CXOIJr8byjolqG7eqCLa+Wfi7rah62VmLoqSXENaZnw=",
-        "owner": "NixOS",
-        "repo": "nix",
-        "rev": "a22328066416650471c3545b0b138669ea212ab4",
-        "type": "github"
-      },
-      "original": {
-        "owner": "NixOS",
-        "repo": "nix",
-        "type": "github"
-      }
-    },
    "nixpkgs": {
      "locked": {
-        "lastModified": 1709083642,
-        "narHash": "sha256-7kkJQd4rZ+vFrzWu8sTRtta5D1kBG0LSRYAfhtmMlSo=",
+        "lastModified": 1710889954,
+        "narHash": "sha256-Pr6F5Pmd7JnNEMHHmspZ0qVqIBVxyZ13ik1pJtm2QXk=",
        "owner": "NixOS",
        "repo": "nixpkgs",
-        "rev": "b550fe4b4776908ac2a861124307045f8e717c8e",
+        "rev": "7872526e9c5332274ea5932a0c3270d6e4724f3b",
        "type": "github"
      },
      "original": {
        "owner": "NixOS",
-        "ref": "release-23.11",
+        "ref": "nixpkgs-unstable",
        "repo": "nixpkgs",
        "type": "github"
      }
@@ -120,44 +51,10 @@
        "type": "github"
      }
    },
-    "nixpkgs-regression": {
-      "locked": {
-        "lastModified": 1643052045,
-        "narHash": "sha256-uGJ0VXIhWKGXxkeNnq4TvV3CIOkUJ3PAoLZ3HMzNVMw=",
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2",
-        "type": "github"
-      },
-      "original": {
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2",
-        "type": "github"
-      }
-    },
-    "nixpkgs_2": {
-      "locked": {
-        "lastModified": 1710889954,
-        "narHash": "sha256-Pr6F5Pmd7JnNEMHHmspZ0qVqIBVxyZ13ik1pJtm2QXk=",
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "7872526e9c5332274ea5932a0c3270d6e4724f3b",
-        "type": "github"
-      },
-      "original": {
-        "owner": "NixOS",
-        "ref": "nixpkgs-unstable",
-        "repo": "nixpkgs",
-        "type": "github"
-      }
-    },
    "root": {
      "inputs": {
        "flake-utils": "flake-utils",
-        "lean4-mode": "lean4-mode",
-        "nix": "nix",
-        "nixpkgs": "nixpkgs_2",
+        "nixpkgs": "nixpkgs",
        "nixpkgs-old": "nixpkgs-old"
      }
    },
--- a/flake.nix
+++ b/flake.nix
@@ -1,38 +1,21 @@
 {
-  description = "Lean interactive theorem prover";
+  description = "Lean development flake. Not intended for end users.";

  inputs.nixpkgs.url = "github:NixOS/nixpkgs/nixpkgs-unstable";
  # old nixpkgs used for portable release with older glibc (2.27)
  inputs.nixpkgs-old.url = "github:NixOS/nixpkgs/nixos-19.03";
  inputs.nixpkgs-old.flake = false;
  inputs.flake-utils.url = "github:numtide/flake-utils";
-  inputs.nix.url = "github:NixOS/nix";
-  inputs.lean4-mode = {
-    url = "github:leanprover/lean4-mode";
-    flake = false;
-  };
-  # used *only* by `stage0-from-input` below
-  #inputs.lean-stage0 = {
-  #  url = github:leanprover/lean4;
-  #  inputs.nixpkgs.follows = "nixpkgs";
-  #  inputs.flake-utils.follows = "flake-utils";
-  #  inputs.nix.follows = "nix";
-  #  inputs.lean4-mode.follows = "lean4-mode";
-  #};

-  outputs = { self, nixpkgs, nixpkgs-old, flake-utils, nix, lean4-mode, ... }@inputs: flake-utils.lib.eachDefaultSystem (system:
+  outputs = { self, nixpkgs, nixpkgs-old, flake-utils, ... }@inputs: flake-utils.lib.eachDefaultSystem (system:
    let
-      pkgs = import nixpkgs {
-        inherit system;
-        # for `vscode-with-extensions`
-        config.allowUnfree = true;
-      };
+      pkgs = import nixpkgs { inherit system; };
      # An old nixpkgs for creating releases with an old glibc
      pkgsDist-old = import nixpkgs-old { inherit system; };
      # An old nixpkgs for creating releases with an old glibc
      pkgsDist-old-aarch = import nixpkgs-old { localSystem.config = "aarch64-unknown-linux-gnu"; };

-      lean-packages = pkgs.callPackage (./nix/packages.nix) { src = ./.; inherit nix lean4-mode; };
+      lean-packages = pkgs.callPackage (./nix/packages.nix) { src = ./.; };

      devShellWithDist = pkgsDist: pkgs.mkShell.override {
          stdenv = pkgs.overrideCC pkgs.stdenv lean-packages.llvmPackages.clang;
@@ -58,41 +41,15 @@
          GDB = pkgsDist.gdb;
        });
    in {
-      packages = lean-packages // rec {
-        debug = lean-packages.override { debug = true; };
-        stage0debug = lean-packages.override { stage0debug = true; };
-        asan = lean-packages.override { extraCMakeFlags = [ "-DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address" "-DLEANC_EXTRA_FLAGS=-fsanitize=address" "-DSMALL_ALLOCATOR=OFF" "-DSYMBOLIC=OFF" ]; };
-        asandebug = asan.override { debug = true; };
-        tsan = lean-packages.override {
-          extraCMakeFlags = [ "-DLEAN_EXTRA_CXX_FLAGS=-fsanitize=thread" "-DLEANC_EXTRA_FLAGS=-fsanitize=thread" "-DCOMPRESSED_OBJECT_HEADER=OFF" ];
-          stage0 = (lean-packages.override {
-            # Compressed headers currently trigger data race reports in tsan.
-            # Turn them off for stage 0 as well so stage 1 can read its own stdlib.
-            extraCMakeFlags = [ "-DCOMPRESSED_OBJECT_HEADER=OFF" ];
-          }).stage1;
-        };
-        tsandebug = tsan.override { debug = true; };
-        stage0-from-input = lean-packages.override {
-          stage0 = pkgs.writeShellScriptBin "lean" ''
-            exec ${inputs.lean-stage0.packages.${system}.lean}/bin/lean -Dinterpreter.prefer_native=false "$@"
-          '';
-        };
-        inherit self;
+      packages = {
+        # to be removed when Nix CI is not needed anymore
+        inherit (lean-packages) cacheRoots test update-stage0-commit ciShell;
+        deprecated = lean-packages;
      };
-      defaultPackage = lean-packages.lean-all;

      # The default development shell for working on lean itself
      devShells.default = devShellWithDist pkgs;
      devShells.oldGlibc = devShellWithDist pkgsDist-old;
      devShells.oldGlibcAArch = devShellWithDist pkgsDist-old-aarch;
-
-      checks.lean = lean-packages.test;
-    }) // rec {
-      templates.pkg = {
-        path = ./nix/templates/pkg;
-        description = "A custom Lean package";
-      };
-
-      defaultTemplate = templates.pkg;
-    };
+    });
 }
--- a/nix/bootstrap.nix
+++ b/nix/bootstrap.nix
@@ -2,7 +2,7 @@
  stdenv, lib, cmake, gmp, git, gnumake, bash, buildLeanPackage, writeShellScriptBin, runCommand, symlinkJoin, lndir, perl, gnused, darwin, llvmPackages, linkFarmFromDrvs,
  ... } @ args:
 with builtins;
-rec {
+lib.warn "The Nix-based build is deprecated" rec {
  inherit stdenv;
  sourceByRegex = p: rs: lib.sourceByRegex p (map (r: "(/src/)?${r}") rs);
  buildCMake = args: stdenv.mkDerivation ({
--- a/nix/buildLeanPackage.nix
+++ b/nix/buildLeanPackage.nix
@@ -1,5 +1,5 @@
 { lean, lean-leanDeps ? lean, lean-final ? lean, leanc,
-  stdenv, lib, coreutils, gnused, writeShellScriptBin, bash, lean-emacs, lean-vscode, nix, substituteAll, symlinkJoin, linkFarmFromDrvs,
+  stdenv, lib, coreutils, gnused, writeShellScriptBin, bash, substituteAll, symlinkJoin, linkFarmFromDrvs,
  runCommand, darwin, mkShell, ... }:
 let lean-final' = lean-final; in
 lib.makeOverridable (
@@ -197,19 +197,6 @@ with builtins; let
             then map (m: m.module) header.imports
             else abort "errors while parsing imports of ${mod}:\n${lib.concatStringsSep "\n" header.errors}";
    in mkMod mod (map (dep: if modDepsMap ? ${dep} then modCandidates.${dep} else externalModMap.${dep}) deps)) modDepsMap;
-  makeEmacsWrapper = name: emacs: lean: writeShellScriptBin name ''
-    ${emacs} --eval "(progn (setq lean4-rootdir \"${lean}\"))" "$@"
-  '';
-  makeVSCodeWrapper = name: lean: writeShellScriptBin name ''
-    PATH=${lean}/bin:$PATH ${lean-vscode}/bin/code "$@"
-  '';
-  printPaths = deps: writeShellScriptBin "print-paths" ''
-    echo '${toJSON {
-      oleanPath = [(depRoot "print-paths" deps)];
-      srcPath = ["."] ++ map (dep: dep.src) allExternalDeps;
-      loadDynlibPaths = map pathOfSharedLib (loadDynlibsOfDeps deps);
-    }}'
-  '';
  expandGlob = g:
    if typeOf g == "string" then [g]
    else if g.glob == "one" then [g.mod]
@@ -257,48 +244,4 @@ in rec {
        -o $out/bin/${executableName} \
        ${lib.concatStringsSep " " allLinkFlags}
    '') {};
-
-  lean-package = writeShellScriptBin "lean" ''
-    LEAN_PATH=${modRoot}:$LEAN_PATH LEAN_SRC_PATH=$LEAN_SRC_PATH:${src} exec ${lean-final}/bin/lean "$@"
-  '';
-  emacs-package = makeEmacsWrapper "emacs-package" lean-package;
-  vscode-package = makeVSCodeWrapper "vscode-package" lean-package;
-
-  link-ilean = writeShellScriptBin "link-ilean" ''
-    dest=''${1:-.}
-    mkdir -p $dest/build/lib
-    ln -sf ${iTree}/* $dest/build/lib
-  '';
-
-  makePrintPathsFor = deps: mods: printPaths deps // mapAttrs (_: mod: makePrintPathsFor (deps ++ [mod]) mods) mods;
-  print-paths = makePrintPathsFor [] (mods' // externalModMap);
-  # `lean` wrapper that dynamically runs Nix for the actual `lean` executable so the same editor can be
-  # used for multiple projects/after upgrading the `lean` input/for editing both stage 1 and the tests
-  lean-bin-dev = substituteAll {
-    name = "lean";
-    dir = "bin";
-    src = ./lean-dev.in;
-    isExecutable = true;
-    srcRoot = fullSrc;  # use root flake.nix in case of Lean repo
-    inherit bash nix srcTarget srcArgs;
-  };
-  lake-dev = substituteAll {
-    name = "lake";
-    dir = "bin";
-    src = ./lake-dev.in;
-    isExecutable = true;
-    srcRoot = fullSrc;  # use root flake.nix in case of Lean repo
-    inherit bash nix srcTarget srcArgs;
-  };
-  lean-dev = symlinkJoin { name = "lean-dev"; paths = [ lean-bin-dev lake-dev ]; };
-  emacs-dev = makeEmacsWrapper "emacs-dev" "${lean-emacs}/bin/emacs" lean-dev;
-  emacs-path-dev = makeEmacsWrapper "emacs-path-dev" "emacs" lean-dev;
-  vscode-dev = makeVSCodeWrapper "vscode-dev" lean-dev;
-
-  devShell = mkShell {
-    buildInputs = [ nix ];
-    shellHook = ''
-      export LEAN_SRC_PATH="${srcPath}"
-    '';
-  };
 })
--- a/nix/packages.nix
+++ b/nix/packages.nix
@@ -1,9 +1,6 @@
-{ src, pkgs, nix, ... } @ args:
+{ src, pkgs, ... } @ args:
 with pkgs;
 let
-  nix-pinned = writeShellScriptBin "nix" ''
-    ${nix.packages.${system}.default}/bin/nix --experimental-features 'nix-command flakes' --extra-substituters https://lean4.cachix.org/ --option warn-dirty false "$@"
-  '';
  # https://github.com/NixOS/nixpkgs/issues/130963
  llvmPackages = if stdenv.isDarwin then llvmPackages_11 else llvmPackages_15;
  cc = (ccacheWrapper.override rec {
@@ -42,40 +39,9 @@ let
    inherit (lean) stdenv;
    lean = lean.stage1;
    inherit (lean.stage1) leanc;
-    inherit lean-emacs lean-vscode;
-    nix = nix-pinned;
  }));
-  lean4-mode = emacsPackages.melpaBuild {
-    pname = "lean4-mode";
-    version = "1";
-    commit = "1";
-    src = args.lean4-mode;
-    packageRequires = with pkgs.emacsPackages.melpaPackages; [ dash f flycheck magit-section lsp-mode s ];
-    recipe = pkgs.writeText "recipe" ''
-      (lean4-mode
-       :repo "leanprover/lean4-mode"
-       :fetcher github
-       :files ("*.el" "data"))
-    '';
-  };
-  lean-emacs = emacsWithPackages [ lean4-mode ];
-  # updating might be nicer by building from source from a flake input, but this is good enough for now
-  vscode-lean4 = vscode-utils.extensionFromVscodeMarketplace {
-      name = "lean4";
-      publisher = "leanprover";
-      version = "0.0.63";
-      sha256 = "sha256-kjEex7L0F2P4pMdXi4NIZ1y59ywJVubqDqsoYagZNkI=";
-  };
-  lean-vscode = vscode-with-extensions.override {
-    vscodeExtensions = [ vscode-lean4 ];
-  };
 in {
-  inherit cc lean4-mode buildLeanPackage llvmPackages vscode-lean4;
-  lean = lean.stage1;
-  stage0print-paths = lean.stage1.Lean.print-paths;
-  HEAD-as-stage0 = (lean.stage1.Lean.overrideArgs { srcTarget = "..#stage0-from-input.stage0"; srcArgs = "(--override-input lean-stage0 ..\?rev=$(git rev-parse HEAD) -- -Dinterpreter.prefer_native=false \"$@\")"; });
-  HEAD-as-stage1 = (lean.stage1.Lean.overrideArgs { srcTarget = "..\?rev=$(git rev-parse HEAD)#stage0"; });
-  nix = nix-pinned;
+  inherit cc buildLeanPackage llvmPackages;
  nixpkgs = pkgs;
  ciShell = writeShellScriptBin "ciShell" ''
    set -o pipefail
@@ -83,5 +49,4 @@ in {
    # prefix lines with cumulative and individual execution time
    "$@" |& ts -i "(%.S)]" | ts -s "[%M:%S"
  '';
-  vscode = lean-vscode;
-} // lean.stage1.Lean // lean.stage1 // lean
+} // lean.stage1
--- a/src/Init/Data/BitVec/Basic.lean
+++ b/src/Init/Data/BitVec/Basic.lean
@@ -20,6 +20,8 @@ We define many of the bitvector operations from the
 of SMT-LIBv2.
 -/

+set_option linter.missingDocs true
+
 /--
 A bitvector of the specified width.

@@ -34,9 +36,9 @@ structure BitVec (w : Nat) where
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  toFin : Fin (2^w)

-@[deprecated (since := "2024-04-12")]
-protected abbrev Std.BitVec := _root_.BitVec
-
+/--
+Bitvectors have decidable equality. This should be used via the instance `DecidableEq (BitVec n)`.
+-/
 -- We manually derive the `DecidableEq` instances for `BitVec` because
 -- we want to have builtin support for bit-vector literals, and we
 -- need a name for this function to implement `canUnfoldAtMatcher` at `WHNF.lean`.
@@ -583,11 +585,9 @@ instance : HAppend (BitVec w) (BitVec v) (BitVec (w + v)) := ⟨.append⟩
 -- TODO: write this using multiplication
 /-- `replicate i x` concatenates `i` copies of `x` into a new vector of length `w*i`. -/
 def replicate : (i : Nat) → BitVec w → BitVec (w*i)
-  | 0,   _ => 0
+  | 0,   _ => 0#0
  | n+1, x =>
-    have hEq : w + w*n = w*(n + 1) := by
-      rw [Nat.mul_add, Nat.add_comm, Nat.mul_one]
-    hEq ▸ (x ++ replicate n x)
+    (x ++ replicate n x).cast (by rw [Nat.mul_succ]; omega)

 /-!
 ### Cons and Concat
--- a/src/Init/Data/BitVec/Bitblast.lean
+++ b/src/Init/Data/BitVec/Bitblast.lean
@@ -28,6 +28,8 @@ https://github.com/mhk119/lean-smt/blob/bitvec/Smt/Data/Bitwise.lean.

 -/

+set_option linter.missingDocs true
+
 open Nat Bool

 namespace Bool
@@ -403,12 +405,8 @@ theorem shiftLeftRec_eq {x : BitVec w₁} {y : BitVec w₂} {n : Nat} :
  induction n generalizing x y
  case zero =>
    ext i
-    simp only [shiftLeftRec_zero, twoPow_zero, Nat.reduceAdd, truncate_one]
-    suffices (y &&& 1#w₂) = zeroExtend w₂ (ofBool (y.getLsb 0)) by simp [this]
-    ext i
-    by_cases h : (↑i : Nat) = 0
-    · simp [h, Bool.and_comm]
-    · simp [h]; omega
+    simp only [shiftLeftRec_zero, twoPow_zero, Nat.reduceAdd, truncate_one,
+      and_one_eq_zeroExtend_ofBool_getLsb]
  case succ n ih =>
    simp only [shiftLeftRec_succ, and_twoPow]
    rw [ih]
@@ -431,4 +429,67 @@ theorem shiftLeft_eq_shiftLeftRec (x : BitVec w₁) (y : BitVec w₂) :
  · simp [of_length_zero]
  · simp [shiftLeftRec_eq]

+/- ### Logical shift right (ushiftRight) recurrence for bitblasting -/
+
+/--
+`ushiftRightRec x y n` shifts `x` logically to the right by the first `n` bits of `y`.
+
+The theorem `shiftRight_eq_ushiftRightRec` proves the equivalence
+of `(x >>> y)` and `ushiftRightRec`.
+
+Together with equations `ushiftRightRec_zero`, `ushiftRightRec_succ`,
+this allows us to unfold `ushiftRight` into a circuit for bitblasting.
+-/
+def ushiftRightRec (x : BitVec w₁) (y : BitVec w₂) (n : Nat) : BitVec w₁ :=
+  let shiftAmt := (y &&& (twoPow w₂ n))
+  match n with
+  | 0 => x >>> shiftAmt
+  | n + 1 => (ushiftRightRec x y n) >>> shiftAmt
+
+@[simp]
+theorem ushiftRightRec_zero (x : BitVec w₁) (y : BitVec w₂) :
+    ushiftRightRec x y 0 = x >>> (y &&& twoPow w₂ 0) := by
+  simp [ushiftRightRec]
+
+@[simp]
+theorem ushiftRightRec_succ (x : BitVec w₁) (y : BitVec w₂) :
+    ushiftRightRec x y (n + 1) = (ushiftRightRec x y n) >>> (y &&& twoPow w₂ (n + 1)) := by
+  simp [ushiftRightRec]
+
+/--
+If `y &&& z = 0`, `x >>> (y ||| z) = x >>> y >>> z`.
+This follows as `y &&& z = 0` implies `y ||| z = y + z`,
+and thus `x >>> (y ||| z) = x >>> (y + z) = x >>> y >>> z`.
+-/
+theorem ushiftRight'_or_of_and_eq_zero {x : BitVec w₁} {y z : BitVec w₂}
+    (h : y &&& z = 0#w₂) :
+    x >>> (y ||| z) = x >>> y >>> z := by
+  simp [← add_eq_or_of_and_eq_zero _ _ h, toNat_add_of_and_eq_zero h, shiftRight_add]
+
+theorem ushiftRightRec_eq (x : BitVec w₁) (y : BitVec w₂) (n : Nat) :
+    ushiftRightRec x y n = x >>> (y.truncate (n + 1)).zeroExtend w₂ := by
+  induction n generalizing x y
+  case zero =>
+    ext i
+    simp only [ushiftRightRec_zero, twoPow_zero, Nat.reduceAdd,
+      and_one_eq_zeroExtend_ofBool_getLsb, truncate_one]
+  case succ n ih =>
+    simp only [ushiftRightRec_succ, and_twoPow]
+    rw [ih]
+    by_cases h : y.getLsb (n + 1) <;> simp only [h, ↓reduceIte]
+    · rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsb_true h,
+        ushiftRight'_or_of_and_eq_zero]
+      simp
+    · simp [zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsb_false, h]
+
+/--
+Show that `x >>> y` can be written in terms of `ushiftRightRec`.
+This can be unfolded in terms of `ushiftRightRec_zero`, `ushiftRightRec_succ` for bitblasting.
+-/
+theorem shiftRight_eq_ushiftRightRec (x : BitVec w₁) (y : BitVec w₂) :
+    x >>> y = ushiftRightRec x y (w₂ - 1) := by
+  rcases w₂ with rfl | w₂
+  · simp [of_length_zero]
+  · simp [ushiftRightRec_eq]
+
 end BitVec
--- a/src/Init/Data/BitVec/Folds.lean
+++ b/src/Init/Data/BitVec/Folds.lean
@@ -8,6 +8,8 @@ import Init.Data.BitVec.Lemmas
 import Init.Data.Nat.Lemmas
 import Init.Data.Fin.Iterate

+set_option linter.missingDocs true
+
 namespace BitVec

 /--
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -12,6 +12,8 @@ import Init.Data.Nat.Lemmas
 import Init.Data.Nat.Mod
 import Init.Data.Int.Bitwise.Lemmas

+set_option linter.missingDocs true
+
 namespace BitVec

 /--
@@ -731,6 +733,16 @@ theorem getLsb_shiftLeft' {x : BitVec w₁} {y : BitVec w₂} {i : Nat} :
    getLsb (x >>> i) j = getLsb x (i+j) := by
  unfold getLsb ; simp

+@[simp]
+theorem ushiftRight_zero_eq (x : BitVec w) : x >>> 0 = x := by
+  simp [bv_toNat]
+
+/-! ### ushiftRight reductions from BitVec to Nat -/
+
+@[simp]
+theorem ushiftRight_eq' (x : BitVec w₁) (y : BitVec w₂) :
+    x >>> y = x >>> y.toNat := by rfl
+
 /-! ### sshiftRight -/

 theorem sshiftRight_eq {x : BitVec n} {i : Nat} :
@@ -1549,4 +1561,54 @@ theorem zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsb_true
    simp [hx]
  · by_cases hik' : k < i + 1 <;> simp [hik, hik'] <;> omega

+/-- Bitwise and of `(x : BitVec w)` with `1#w` equals zero extending `x.lsb` to `w`. -/
+theorem and_one_eq_zeroExtend_ofBool_getLsb {x : BitVec w} :
+    (x &&& 1#w) = zeroExtend w (ofBool (x.getLsb 0)) := by
+  ext i
+  simp only [getLsb_and, getLsb_one, getLsb_zeroExtend, Fin.is_lt, decide_True, getLsb_ofBool,
+    Bool.true_and]
+  by_cases h : (0 = (i : Nat)) <;> simp [h] <;> omega
+
+@[simp]
+theorem replicate_zero_eq {x : BitVec w} : x.replicate 0 = 0#0 := by
+  simp [replicate]
+
+@[simp]
+theorem replicate_succ_eq {x : BitVec w} :
+    x.replicate (n + 1) =
+    (x ++ replicate n x).cast (by rw [Nat.mul_succ]; omega) := by
+  simp [replicate]
+
+/--
+If a number `w * n ≤ i < w * (n + 1)`, then `i - w * n` equals `i % w`.
+This is true by subtracting `w * n` from the inequality, giving
+`0 ≤ i - w * n < w`, which uniquely identifies `i % w`.
+-/
+private theorem Nat.sub_mul_eq_mod_of_lt_of_le (hlo : w * n ≤ i) (hhi : i < w * (n + 1)) :
+    i - w * n = i % w := by
+  rw [Nat.mod_def]
+  congr
+  symm
+  apply Nat.div_eq_of_lt_le
+    (by rw [Nat.mul_comm]; omega)
+    (by rw [Nat.mul_comm]; omega)
+
+@[simp]
+theorem getLsb_replicate {n w : Nat} (x : BitVec w) :
+    (x.replicate n).getLsb i =
+    (decide (i < w * n) && x.getLsb (i % w)) := by
+  induction n generalizing x
+  case zero => simp
+  case succ n ih =>
+    simp only [replicate_succ_eq, getLsb_cast, getLsb_append]
+    by_cases hi : i < w * (n + 1)
+    · simp only [hi, decide_True, Bool.true_and]
+      by_cases hi' : i < w * n
+      · simp [hi', ih]
+      · simp only [hi', decide_False, cond_false]
+        rw [Nat.sub_mul_eq_mod_of_lt_of_le] <;> omega
+    · rw [Nat.mul_succ] at hi ⊢
+      simp only [show ¬i < w * n by omega, decide_False, cond_false, hi, Bool.false_and]
+      apply BitVec.getLsb_ge (x := x) (i := i - w * n) (ge := by omega)
+
 end BitVec
--- a/src/Init/Data/ByteArray/Basic.lean
+++ b/src/Init/Data/ByteArray/Basic.lean
@@ -191,6 +191,121 @@ def foldlM {β : Type v} {m : Type v → Type w} [Monad m] (f : β → UInt8 →
 def foldl {β : Type v} (f : β → UInt8 → β) (init : β) (as : ByteArray) (start := 0) (stop := as.size) : β :=
  Id.run <| as.foldlM f init start stop

+/-- Iterator over the bytes (`UInt8`) of a `ByteArray`.
+
+Typically created by `arr.iter`, where `arr` is a `ByteArray`.
+
+An iterator is *valid* if the position `i` is *valid* for the array `arr`, meaning `0 ≤ i ≤ arr.size`
+
+Most operations on iterators return arbitrary values if the iterator is not valid. The functions in
+the `ByteArray.Iterator` API should rule out the creation of invalid iterators, with two exceptions:
+
+- `Iterator.next iter` is invalid if `iter` is already at the end of the array (`iter.atEnd` is
+  `true`)
+- `Iterator.forward iter n`/`Iterator.nextn iter n` is invalid if `n` is strictly greater than the
+  number of remaining bytes.
+-/
+structure Iterator where
+  /-- The array the iterator is for. -/
+  array : ByteArray
+  /-- The current position.
+
+  This position is not necessarily valid for the array, for instance if one keeps calling
+  `Iterator.next` when `Iterator.atEnd` is true. If the position is not valid, then the
+  current byte is `(default : UInt8)`. -/
+  idx : Nat
+  deriving Inhabited
+
+/-- Creates an iterator at the beginning of an array. -/
+def mkIterator (arr : ByteArray) : Iterator :=
+  ⟨arr, 0⟩
+
+@[inherit_doc mkIterator]
+abbrev iter := mkIterator
+
+/-- The size of an array iterator is the number of bytes remaining. -/
+instance : SizeOf Iterator where
+  sizeOf i := i.array.size - i.idx
+
+theorem Iterator.sizeOf_eq (i : Iterator) : sizeOf i = i.array.size - i.idx :=
+  rfl
+
+namespace Iterator
+
+/-- Number of bytes remaining in the iterator. -/
+def remainingBytes : Iterator → Nat
+  | ⟨arr, i⟩ => arr.size - i
+
+@[inherit_doc Iterator.idx]
+def pos := Iterator.idx
+
+/-- The byte at the current position.
+
+On an invalid position, returns `(default : UInt8)`. -/
+@[inline]
+def curr : Iterator → UInt8
+  | ⟨arr, i⟩ =>
+    if h:i < arr.size then
+      arr[i]'h
+    else
+      default
+
+/-- Moves the iterator's position forward by one byte, unconditionally.
+
+It is only valid to call this function if the iterator is not at the end of the array, *i.e.*
+`Iterator.atEnd` is `false`; otherwise, the resulting iterator will be invalid. -/
+@[inline]
+def next : Iterator → Iterator
+  | ⟨arr, i⟩ => ⟨arr, i + 1⟩
+
+/-- Decreases the iterator's position.
+
+If the position is zero, this function is the identity. -/
+@[inline]
+def prev : Iterator → Iterator
+  | ⟨arr, i⟩ => ⟨arr, i - 1⟩
+
+/-- True if the iterator is past the array's last byte. -/
+@[inline]
+def atEnd : Iterator → Bool
+  | ⟨arr, i⟩ => i ≥ arr.size
+
+/-- True if the iterator is not past the array's last byte. -/
+@[inline]
+def hasNext : Iterator → Bool
+  | ⟨arr, i⟩ => i < arr.size
+
+/-- True if the position is not zero. -/
+@[inline]
+def hasPrev : Iterator → Bool
+  | ⟨_, i⟩ => i > 0
+
+/-- Moves the iterator's position to the end of the array.
+
+Note that `i.toEnd.atEnd` is always `true`. -/
+@[inline]
+def toEnd : Iterator → Iterator
+  | ⟨arr, _⟩ => ⟨arr, arr.size⟩
+
+/-- Moves the iterator's position several bytes forward.
+
+The resulting iterator is only valid if the number of bytes to skip is less than or equal to
+the number of bytes left in the iterator. -/
+@[inline]
+def forward : Iterator → Nat → Iterator
+  | ⟨arr, i⟩, f => ⟨arr, i + f⟩
+
+@[inherit_doc forward, inline]
+def nextn : Iterator → Nat → Iterator := forward
+
+/-- Moves the iterator's position several bytes back.
+
+If asked to go back more bytes than available, stops at the beginning of the array. -/
+@[inline]
+def prevn : Iterator → Nat → Iterator
+  | ⟨arr, i⟩, f => ⟨arr, i - f⟩
+
+end Iterator
 end ByteArray

 def List.toByteArray (bs : List UInt8) : ByteArray :=
--- a/src/Init/Data/Int/Basic.lean
+++ b/src/Init/Data/Int/Basic.lean
@@ -322,8 +322,8 @@ protected def pow (m : Int) : Nat → Int
  | 0      => 1
  | succ n => Int.pow m n * m

-instance : HPow Int Nat Int where
-  hPow := Int.pow
+instance : NatPow Int where
+  pow := Int.pow

 instance : LawfulBEq Int where
  eq_of_beq h := by simp [BEq.beq] at h; assumption
--- a/src/Init/Data/Nat/Div.lean
+++ b/src/Init/Data/Nat/Div.lean
@@ -203,6 +203,10 @@ theorem mod_add_div (m k : Nat) : m % k + k * (m / k) = m := by
  | base x y h => simp [h]
  | ind x y h IH => simp [h]; rw [Nat.mul_succ, ← Nat.add_assoc, IH, Nat.sub_add_cancel h.2]

+theorem mod_def (m k : Nat) : m % k = m - k * (m / k) := by
+  rw [Nat.sub_eq_of_eq_add]
+  apply (Nat.mod_add_div _ _).symm
+
@[simp] protected theorem div_one (n : Nat) : n / 1 = n := by
  have := mod_add_div n 1
  rwa [mod_one, Nat.zero_add, Nat.one_mul] at this
--- a/src/Init/ShareCommon.lean
+++ b/src/Init/ShareCommon.lean
@@ -109,4 +109,4 @@ A more restrictive but efficient max sharing primitive.
 Remark: it optimizes the number of RC operations, and the strategy for caching results.
 -/
@[extern "lean_sharecommon_quick"]
-def ShareCommon.shareCommon' (a : α) : α := a
+def ShareCommon.shareCommon' (a : @& α) : α := a
--- a/src/Init/System/IO.lean
+++ b/src/Init/System/IO.lean
@@ -435,6 +435,12 @@ Note that EOF does not actually close a handle, so further reads may block and r

 end Handle

+/--
+Resolves a pathname to an absolute pathname with no '.', '..', or symbolic links.
+
+This function coincides with the [POSIX `realpath` function](https://pubs.opengroup.org/onlinepubs/9699919799/functions/realpath.html),
+see there for more information.
+-/
@[extern "lean_io_realpath"] opaque realPath (fname : FilePath) : IO FilePath
@[extern "lean_io_remove_file"] opaque removeFile (fname : @& FilePath) : IO Unit
 /-- Remove given directory. Fails if not empty; see also `IO.FS.removeDirAll`. -/
--- a/src/Lean/Compiler/IR/EmitC.lean
+++ b/src/Lean/Compiler/IR/EmitC.lean
@@ -94,7 +94,10 @@ def emitCInitName (n : Name) : M Unit :=
 def shouldExport (n : Name) : Bool :=
  -- HACK: exclude symbols very unlikely to be used by the interpreter or other consumers of
  -- libleanshared to avoid Windows symbol limit
-  !(`Lean.Compiler.LCNF).isPrefixOf n && !(`Lean.IR).isPrefixOf n && !(`Lean.Server).isPrefixOf n
+  !(`Lean.Compiler.LCNF).isPrefixOf n &&
+  !(`Lean.IR).isPrefixOf n &&
+  -- Lean.Server.findModuleRefs is used in Verso
+  (!(`Lean.Server).isPrefixOf n || n == `Lean.Server.findModuleRefs)

 def emitFnDeclAux (decl : Decl) (cppBaseName : String) (isExternal : Bool) : M Unit := do
  let ps := decl.params
--- a/src/Lean/CoreM.lean
+++ b/src/Lean/CoreM.lean
@@ -40,7 +40,7 @@ def useDiagnosticMsg : MessageData :=
    if diagnostics.get ctx.opts then
      pure ""
    else
-      pure s!"\nAdditional diagnostic information may be available by using the `set_option {diagnostics.name} true` command."
+      pure s!"\nAdditional diagnostic information may be available using the `set_option {diagnostics.name} true` command."

 namespace Core

--- a/src/Lean/Data/Json/Parser.lean
+++ b/src/Lean/Data/Json/Parser.lean
@@ -12,10 +12,11 @@ import Lean.Data.RBMap
 namespace Lean.Json.Parser

 open Lean.Parsec
+open Lean.Parsec.String

@[inline]
-def hexChar : Parsec Nat := do
-  let c ← anyChar
+def hexChar : Parser Nat := do
+  let c ← any
  if '0' ≤ c ∧ c ≤ '9' then
    pure $ c.val.toNat - '0'.val.toNat
  else if 'a' ≤ c ∧ c ≤ 'f' then
@@ -25,8 +26,8 @@ def hexChar : Parsec Nat := do
  else
    fail "invalid hex character"

-def escapedChar : Parsec Char := do
-  let c ← anyChar
+def escapedChar : Parser Char := do
+  let c ← any
  match c with
  | '\\' => return '\\'
  | '"'  => return '"'
@@ -41,13 +42,13 @@ def escapedChar : Parsec Char := do
    return Char.ofNat $ 4096*u1 + 256*u2 + 16*u3 + u4
  | _ => fail "illegal \\u escape"

-partial def strCore (acc : String) : Parsec String := do
+partial def strCore (acc : String) : Parser String := do
  let c ← peek!
  if c = '"' then -- "
    skip
    return acc
  else
-    let c ← anyChar
+    let c ← any
    if c = '\\' then
      strCore (acc.push (← escapedChar))
    -- as to whether c.val > 0xffff should be split up and encoded with multiple \u,
@@ -58,9 +59,9 @@ partial def strCore (acc : String) : Parsec String := do
    else
      fail "unexpected character in string"

-def str : Parsec String := strCore ""
+def str : Parser String := strCore ""

-partial def natCore (acc digits : Nat) : Parsec (Nat × Nat) := do
+partial def natCore (acc digits : Nat) : Parser (Nat × Nat) := do
  let some c ← peek? | return (acc, digits)
  if '0' ≤ c ∧ c ≤ '9' then
    skip
@@ -70,7 +71,7 @@ partial def natCore (acc digits : Nat) : Parsec (Nat × Nat) := do
    return (acc, digits)

@[inline]
-def lookahead (p : Char → Prop) (desc : String) [DecidablePred p] : Parsec Unit := do
+def lookahead (p : Char → Prop) (desc : String) [DecidablePred p] : Parser Unit := do
  let c ← peek!
  if p c then
    return ()
@@ -78,22 +79,22 @@ def lookahead (p : Char → Prop) (desc : String) [DecidablePred p] : Parsec Uni
    fail <| "expected " ++ desc

@[inline]
-def natNonZero : Parsec Nat := do
+def natNonZero : Parser Nat := do
  lookahead (fun c => '1' ≤ c ∧ c ≤ '9') "1-9"
  let (n, _) ← natCore 0 0
  return n

@[inline]
-def natNumDigits : Parsec (Nat × Nat) := do
+def natNumDigits : Parser (Nat × Nat) := do
  lookahead (fun c => '0' ≤ c ∧ c ≤ '9') "digit"
  natCore 0 0

@[inline]
-def natMaybeZero : Parsec Nat := do
+def natMaybeZero : Parser Nat := do
  let (n, _) ← natNumDigits
  return n

-def num : Parsec JsonNumber := do
+def num : Parser JsonNumber := do
  let c ← peek!
  let sign ← if c = '-' then
    skip
@@ -132,10 +133,10 @@ def num : Parsec JsonNumber := do
  else
    return res

-partial def arrayCore (anyCore : Parsec Json) (acc : Array Json) : Parsec (Array Json) := do
+partial def arrayCore (anyCore : Parser Json) (acc : Array Json) : Parser (Array Json) := do
  let hd ← anyCore
  let acc' := acc.push hd
-  let c ← anyChar
+  let c ← any
  if c = ']' then
    ws
    return acc'
@@ -145,12 +146,12 @@ partial def arrayCore (anyCore : Parsec Json) (acc : Array Json) : Parsec (Array
  else
    fail "unexpected character in array"

-partial def objectCore (anyCore : Parsec Json) : Parsec (RBNode String (fun _ => Json)) := do
+partial def objectCore (anyCore : Parser Json) : Parser (RBNode String (fun _ => Json)) := do
  lookahead (fun c => c = '"') "\""; skip; -- "
  let k ← strCore ""; ws
  lookahead (fun c => c = ':') ":"; skip; ws
  let v ← anyCore
-  let c ← anyChar
+  let c ← any
  if c = '}' then
    ws
    return RBNode.singleton k v
@@ -161,7 +162,7 @@ partial def objectCore (anyCore : Parsec Json) : Parsec (RBNode String (fun _ =>
  else
    fail "unexpected character in object"

-partial def anyCore : Parsec Json := do
+partial def anyCore : Parser Json := do
  let c ← peek!
  if c = '[' then
    skip; ws
@@ -203,7 +204,7 @@ partial def anyCore : Parsec Json := do
    fail "unexpected input"


-def any : Parsec Json := do
+def any : Parser Json := do
  ws
  let res ← anyCore
  eof
--- a/src/Lean/Data/Parsec.lean
+++ b/src/Lean/Data/Parsec.lean
@@ -4,181 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Dany Fabian
 -/
 prelude
-import Init.NotationExtra
-import Init.Data.ToString.Macro
-
-namespace Lean
-
-namespace Parsec
-inductive ParseResult (α : Type) where
-  | success (pos : String.Iterator) (res : α)
-  | error (pos : String.Iterator) (err : String)
-  deriving Repr
-end Parsec
-
-def Parsec (α : Type) : Type := String.Iterator → Lean.Parsec.ParseResult α
-
-namespace Parsec
-
-open ParseResult
-
-instance (α : Type) : Inhabited (Parsec α) :=
-  ⟨λ it => error it ""⟩
-
-@[inline]
-protected def pure (a : α) : Parsec α := λ it =>
- success it a
-
-@[inline]
-def bind {α β : Type} (f : Parsec α) (g : α → Parsec β) : Parsec β := λ it =>
-  match f it with
-  | success rem a => g a rem
-  | error pos msg => error pos msg
-
-instance : Monad Parsec :=
-  { pure := Parsec.pure, bind }
-
-@[inline]
-def fail (msg : String) : Parsec α := fun it =>
-  error it msg
-
-@[inline]
-def tryCatch (p : Parsec α)
-    (csuccess : α → Parsec β)
-    (cerror : Unit → Parsec β)
-    : Parsec β := fun it =>
-  match p it with
-  | .success rem a => csuccess a rem
-  | .error rem err =>
-    -- We assume that it.s never changes as the `Parsec` monad only modifies `it.pos`.
-    if it.pos = rem.pos then cerror () rem else .error rem err
-
-@[inline]
-def orElse (p : Parsec α) (q : Unit → Parsec α) : Parsec α :=
-  tryCatch p pure q
-
-@[inline]
-def attempt (p : Parsec α) : Parsec α := λ it =>
-  match p it with
-  | success rem res => success rem res
-  | error _ err => error it err
-
-instance : Alternative Parsec :=
-{ failure := fail "", orElse }
-
-protected def run (p : Parsec α) (s : String) : Except String α :=
-  match p s.mkIterator with
-  | Parsec.ParseResult.success _ res => Except.ok res
-  | Parsec.ParseResult.error it err  => Except.error s!"offset {repr it.i.byteIdx}: {err}"
-
-def expectedEndOfInput := "expected end of input"
-
-@[inline]
-def eof : Parsec Unit := fun it =>
-  if it.hasNext then
-    error it expectedEndOfInput
-  else
-    success it ()
-
-@[specialize]
-partial def manyCore (p : Parsec α) (acc : Array α) : Parsec $ Array α :=
-  tryCatch p (manyCore p <| acc.push ·) (fun _ => pure acc)
-
-@[inline]
-def many (p : Parsec α) : Parsec $ Array α := manyCore p #[]
-
-@[inline]
-def many1 (p : Parsec α) : Parsec $ Array α := do manyCore p #[←p]
-
-@[specialize]
-partial def manyCharsCore (p : Parsec Char) (acc : String) : Parsec String :=
-  tryCatch p (manyCharsCore p <| acc.push ·) (fun _ => pure acc)
-
-@[inline]
-def manyChars (p : Parsec Char) : Parsec String := manyCharsCore p ""
-
-@[inline]
-def many1Chars (p : Parsec Char) : Parsec String := do manyCharsCore p (←p).toString
-
-/-- Parses the given string. -/
-def pstring (s : String) : Parsec String := λ it =>
-  let substr := it.extract (it.forward s.length)
-  if substr = s then
-    success (it.forward s.length) substr
-  else
-    error it s!"expected: {s}"
-
-@[inline]
-def skipString (s : String) : Parsec Unit := pstring s *> pure ()
-
-def unexpectedEndOfInput := "unexpected end of input"
-
-@[inline]
-def anyChar : Parsec Char := λ it =>
-  if it.hasNext then success it.next it.curr else error it unexpectedEndOfInput
-
-@[inline]
-def pchar (c : Char) : Parsec Char := attempt do
-  if (←anyChar) = c then pure c else fail s!"expected: '{c}'"
-
-@[inline]
-def skipChar (c : Char) : Parsec Unit := pchar c *> pure ()
-
-@[inline]
-def digit : Parsec Char := attempt do
-  let c ← anyChar
-  if '0' ≤ c ∧ c ≤ '9' then return c else fail s!"digit expected"
-
-@[inline]
-def hexDigit : Parsec Char := attempt do
-  let c ← anyChar
-  if ('0' ≤ c ∧ c ≤ '9')
-   ∨ ('a' ≤ c ∧ c ≤ 'f')
-   ∨ ('A' ≤ c ∧ c ≤ 'F') then return c else fail s!"hex digit expected"
-
-@[inline]
-def asciiLetter : Parsec Char := attempt do
-  let c ← anyChar
-  if ('A' ≤ c ∧ c ≤ 'Z') ∨ ('a' ≤ c ∧ c ≤ 'z') then return c else fail s!"ASCII letter expected"
-
-@[inline]
-def satisfy (p : Char → Bool) : Parsec Char := attempt do
-  let c ← anyChar
-  if p c then return c else fail "condition not satisfied"
-
-@[inline]
-def notFollowedBy (p : Parsec α) : Parsec Unit := λ it =>
-  match p it with
-  | success _ _ => error it ""
-  | error _ _ => success it ()
-
-partial def skipWs (it : String.Iterator) : String.Iterator :=
-  if it.hasNext then
-    let c := it.curr
-    if c = '\u0009' ∨ c = '\u000a' ∨ c = '\u000d' ∨ c = '\u0020' then
-      skipWs it.next
-    else
-      it
-  else
-   it
-
-@[inline]
-def peek? : Parsec (Option Char) := fun it =>
-  if it.hasNext then
-    success it it.curr
-  else
-    success it none
-
-@[inline]
-def peek! : Parsec Char := do
-  let some c ← peek? | fail unexpectedEndOfInput
-  return c
-
-@[inline]
-def skip : Parsec Unit := fun it =>
-  success it.next ()
-
-@[inline]
-def ws : Parsec Unit := fun it =>
-  success (skipWs it) ()
-end Parsec
+import Lean.Data.Parsec.Basic
+import Lean.Data.Parsec.String
+import Lean.Data.Parsec.ByteArray
--- a/src/Lean/Data/Parsec/Basic.lean
+++ b/src/Lean/Data/Parsec/Basic.lean
@@ -0,0 +1,144 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Dany Fabian, Henrik Böving
+-/
+prelude
+import Init.NotationExtra
+import Init.Data.ToString.Macro
+
+namespace Lean
+
+namespace Parsec
+
+inductive ParseResult (α : Type) (ι : Type) where
+  | success (pos : ι) (res : α)
+  | error (pos : ι) (err : String)
+  deriving Repr
+
+end Parsec
+
+def Parsec (ι : Type) (α : Type) : Type := ι → Lean.Parsec.ParseResult α ι
+
+namespace Parsec
+
+class Input (ι : Type) (elem : outParam Type) (idx : outParam Type) [DecidableEq idx] [DecidableEq elem] where
+  pos : ι → idx
+  next : ι → ι
+  curr : ι → elem
+  hasNext : ι → Bool
+
+variable {α : Type} {ι : Type} {elem : Type} {idx : Type}
+variable [DecidableEq idx] [DecidableEq elem] [Input ι elem idx]
+
+instance : Inhabited (Parsec ι α) where
+  default := fun it => .error it ""
+
+@[inline]
+protected def pure (a : α) : Parsec ι α := fun it =>
+  .success it a
+
+@[inline]
+def bind {α β : Type} (f : Parsec ι α) (g : α → Parsec ι β) : Parsec ι β := fun it =>
+  match f it with
+  | .success rem a => g a rem
+  | .error pos msg => .error pos msg
+
+instance : Monad (Parsec ι) where
+  pure := Parsec.pure
+  bind := Parsec.bind
+
+@[inline]
+def fail (msg : String) : Parsec ι α := fun it =>
+  .error it msg
+
+@[inline]
+def tryCatch (p : Parsec ι α) (csuccess : α → Parsec ι β) (cerror : Unit → Parsec ι β)
+    : Parsec ι β := fun it =>
+  match p it with
+  | .success rem a => csuccess a rem
+  | .error rem err =>
+    -- We assume that it.s never changes as the `Parsec` monad only modifies `it.pos`.
+    if Input.pos it = Input.pos rem then cerror () rem else .error rem err
+
+@[inline]
+def orElse (p : Parsec ι α) (q : Unit → Parsec ι α) : Parsec ι α :=
+  tryCatch p pure q
+
+@[inline]
+def attempt (p : Parsec ι α) : Parsec ι α := fun it =>
+  match p it with
+  | .success rem res => .success rem res
+  | .error _ err => .error it err
+
+instance : Alternative (Parsec ι) where
+  failure := fail ""
+  orElse := orElse
+
+def expectedEndOfInput := "expected end of input"
+
+@[inline]
+def eof : Parsec ι Unit := fun it =>
+  if Input.hasNext it then
+    .error it expectedEndOfInput
+  else
+    .success it ()
+
+@[specialize]
+partial def manyCore (p : Parsec ι α) (acc : Array α) : Parsec ι <| Array α :=
+  tryCatch p (manyCore p <| acc.push ·) (fun _ => pure acc)
+
+@[inline]
+def many (p : Parsec ι α) : Parsec ι <| Array α := manyCore p #[]
+
+@[inline]
+def many1 (p : Parsec ι α) : Parsec ι <| Array α := do manyCore p #[← p]
+
+def unexpectedEndOfInput := "unexpected end of input"
+
+@[inline]
+def any : Parsec ι elem := fun it =>
+  if Input.hasNext it then
+    .success (Input.next it) (Input.curr it)
+  else
+    .error it unexpectedEndOfInput
+
+@[inline]
+def satisfy (p : elem → Bool) : Parsec ι elem := attempt do
+  let c ← any
+  if p c then return c else fail "condition not satisfied"
+
+@[inline]
+def notFollowedBy (p : Parsec ι α) : Parsec ι Unit := fun it =>
+  match p it with
+  | .success _ _ => .error it ""
+  | .error _ _ => .success it ()
+
+@[inline]
+def peek? : Parsec ι (Option elem) := fun it =>
+  if Input.hasNext it then
+    .success it (Input.curr it)
+  else
+    .success it none
+
+@[inline]
+def peek! : Parsec ι elem := do
+  let some c ← peek? | fail unexpectedEndOfInput
+  return c
+
+@[inline]
+def skip : Parsec ι Unit := fun it =>
+  .success (Input.next it) ()
+
+@[specialize]
+partial def manyCharsCore (p : Parsec ι Char) (acc : String) : Parsec ι String :=
+  tryCatch p (manyCharsCore p <| acc.push ·) (fun _ => pure acc)
+
+@[inline]
+def manyChars (p : Parsec ι Char) : Parsec ι String := manyCharsCore p ""
+
+@[inline]
+def many1Chars (p : Parsec ι Char) : Parsec ι String := do manyCharsCore p (← p).toString
+
+
+end Parsec
--- a/src/Lean/Data/Parsec/ByteArray.lean
+++ b/src/Lean/Data/Parsec/ByteArray.lean
@@ -0,0 +1,103 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+prelude
+import Lean.Data.Parsec.Basic
+import Init.Data.ByteArray.Basic
+import Init.Data.String.Extra
+
+namespace Lean
+namespace Parsec
+namespace ByteArray
+
+instance : Input ByteArray.Iterator UInt8 Nat where
+  pos it := it.pos
+  next it := it.next
+  curr it := it.curr
+  hasNext it := it.hasNext
+
+abbrev Parser (α : Type) : Type := Parsec ByteArray.Iterator α
+
+protected def Parser.run (p : Parser α) (arr : ByteArray) : Except String α :=
+  match p arr.iter with
+  | .success _ res => Except.ok res
+  | .error it err  => Except.error s!"offset {repr it.pos}: {err}"
+
+@[inline]
+def pbyte (b : UInt8) : Parser UInt8 := attempt do
+  if (← any) = b then pure b else fail s!"expected: '{b}'"
+
+@[inline]
+def skipByte (b : UInt8) : Parser Unit := pbyte b *> pure ()
+
+def skipBytes (arr : ByteArray) : Parser Unit := do
+  for b in arr do
+    skipByte b
+
+@[inline]
+def pstring (s : String) : Parser String := do
+  skipBytes s.toUTF8
+  return s
+
+@[inline]
+def skipString (s : String) : Parser Unit := pstring s *> pure ()
+
+/--
+Parse a `Char` that can be represented in 1 byte. If `c` uses more than 1 byte it is truncated.
+-/
+@[inline]
+def pByteChar (c : Char) : Parser Char := attempt do
+  if (← any) = c.toUInt8 then pure c else fail s!"expected: '{c}'"
+
+/--
+Skip a `Char` that can be represented in 1 byte. If `c` uses more than 1 byte it is truncated.
+-/
+@[inline]
+def skipByteChar (c : Char) : Parser Unit := skipByte c.toUInt8
+
+@[inline]
+def digit : Parser Char := attempt do
+  let b ← any
+  if '0'.toUInt8 ≤ b ∧ b ≤ '9'.toUInt8 then return Char.ofUInt8 b else fail s!"digit expected"
+
+@[inline]
+def hexDigit : Parser Char := attempt do
+  let b ← any
+  if ('0'.toUInt8 ≤ b ∧ b ≤ '9'.toUInt8)
+   ∨ ('a'.toUInt8 ≤ b ∧ b ≤ 'f'.toUInt8)
+   ∨ ('A'.toUInt8 ≤ b ∧ b ≤ 'F'.toUInt8) then return Char.ofUInt8 b else fail s!"hex digit expected"
+
+@[inline]
+def asciiLetter : Parser Char := attempt do
+  let b ← any
+  if ('A'.toUInt8 ≤ b ∧ b ≤ 'Z'.toUInt8) ∨ ('a'.toUInt8 ≤ b ∧ b ≤ 'z'.toUInt8) then
+    return Char.ofUInt8 b
+  else
+    fail s!"ASCII letter expected"
+
+private partial def skipWs (it : ByteArray.Iterator) : ByteArray.Iterator :=
+  if it.hasNext then
+    let b := it.curr
+    if b = '\u0009'.toUInt8 ∨ b = '\u000a'.toUInt8 ∨ b = '\u000d'.toUInt8 ∨ b = '\u0020'.toUInt8 then
+      skipWs it.next
+    else
+      it
+  else
+   it
+
+@[inline]
+def ws : Parser Unit := fun it =>
+  .success (skipWs it) ()
+
+def take (n : Nat) : Parser ByteArray := fun it =>
+  let subarr := it.array.extract it.idx (it.idx + n)
+  if subarr.size != n then
+    .error it s!"expected: {n} bytes"
+  else
+    .success (it.forward n) subarr
+
+end ByteArray
+end Parsec
+end Lean
--- a/src/Lean/Data/Parsec/String.lean
+++ b/src/Lean/Data/Parsec/String.lean
@@ -0,0 +1,84 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Dany Fabian, Henrik Böving
+-/
+prelude
+import Lean.Data.Parsec.Basic
+
+namespace Lean
+namespace Parsec
+namespace String
+
+instance : Input String.Iterator Char String.Pos where
+  pos it := it.pos
+  next it := it.next
+  curr it := it.curr
+  hasNext it := it.hasNext
+
+abbrev Parser (α : Type) : Type := Parsec String.Iterator α
+
+protected def Parser.run (p : Parser α) (s : String) : Except String α :=
+  match p s.mkIterator with
+  | .success _ res => Except.ok res
+  | .error it err  => Except.error s!"offset {repr it.i.byteIdx}: {err}"
+
+/-- Parses the given string. -/
+def pstring (s : String) : Parser String := fun it =>
+  let substr := it.extract (it.forward s.length)
+  if substr = s then
+    .success (it.forward s.length) substr
+  else
+    .error it s!"expected: {s}"
+
+@[inline]
+def skipString (s : String) : Parser Unit := pstring s *> pure ()
+
+@[inline]
+def pchar (c : Char) : Parser Char := attempt do
+  if (← any) = c then pure c else fail s!"expected: '{c}'"
+
+@[inline]
+def skipChar (c : Char) : Parser Unit := pchar c *> pure ()
+
+@[inline]
+def digit : Parser Char := attempt do
+  let c ← any
+  if '0' ≤ c ∧ c ≤ '9' then return c else fail s!"digit expected"
+
+@[inline]
+def hexDigit : Parser Char := attempt do
+  let c ← any
+  if ('0' ≤ c ∧ c ≤ '9')
+   ∨ ('a' ≤ c ∧ c ≤ 'f')
+   ∨ ('A' ≤ c ∧ c ≤ 'F') then return c else fail s!"hex digit expected"
+
+@[inline]
+def asciiLetter : Parser Char := attempt do
+  let c ← any
+  if ('A' ≤ c ∧ c ≤ 'Z') ∨ ('a' ≤ c ∧ c ≤ 'z') then return c else fail s!"ASCII letter expected"
+
+private partial def skipWs (it : String.Iterator) : String.Iterator :=
+  if it.hasNext then
+    let c := it.curr
+    if c = '\u0009' ∨ c = '\u000a' ∨ c = '\u000d' ∨ c = '\u0020' then
+      skipWs it.next
+    else
+      it
+  else
+   it
+
+@[inline]
+def ws : Parser Unit := fun it =>
+  .success (skipWs it) ()
+
+def take (n : Nat) : Parser String := fun it =>
+  let substr := it.extract (it.forward n)
+  if substr.length != n then
+    .error it s!"expected: {n} codepoints"
+  else
+    .success (it.forward n) substr
+
+end String
+end Parsec
+end Lean
--- a/src/Lean/Data/Xml/Parser.lean
+++ b/src/Lean/Data/Xml/Parser.lean
@@ -13,23 +13,24 @@ namespace Lean
 namespace Xml

 namespace Parser
+
 open Lean.Parsec
-open Parsec.ParseResult
+open Lean.Parsec.String

 abbrev LeanChar := Char

 /-- consume a newline character sequence pretending, that we read '\n'. As per spec:
  https://www.w3.org/TR/xml/#sec-line-ends -/
-def endl : Parsec LeanChar := (skipString "\r\n" <|> skipChar '\r' <|> skipChar '\n') *> pure '\n'
+def endl : Parser LeanChar := (skipString "\r\n" <|> skipChar '\r' <|> skipChar '\n') *> pure '\n'

-def quote (p : Parsec α) : Parsec α :=
+def quote (p : Parser α) : Parser α :=
  skipChar '\'' *> p <* skipChar '\''
  <|> skipChar '"' *> p <* skipChar '"'

 /-- https://www.w3.org/TR/xml/#NT-Char -/
-def Char : Parsec LeanChar :=
+def Char : Parser LeanChar :=
  (attempt do
-  let c ← anyChar
+  let c ← any
  let cNat := c.toNat
  if (0x20 ≤ cNat ∧ cNat ≤ 0xD7FF)
   ∨ (0xE000 ≤ cNat ∧ cNat ≤ 0xFFFD)
@@ -37,11 +38,11 @@ def Char : Parsec LeanChar :=
  <|> pchar '\t' <|> endl

 /-- https://www.w3.org/TR/xml/#NT-S -/
-def S : Parsec String :=
+def S : Parser String :=
  many1Chars (pchar ' ' <|> endl <|> pchar '\t')

 /-- https://www.w3.org/TR/xml/#NT-Eq -/
-def Eq : Parsec Unit :=
+def Eq : Parser Unit :=
  optional S *> skipChar '=' <* optional S

 private def nameStartCharRanges : Array (Nat × Nat) :=
@@ -59,8 +60,8 @@ private def nameStartCharRanges : Array (Nat × Nat) :=
    (0x10000, 0xEFFFF)]

 /-- https://www.w3.org/TR/xml/#NT-NameStartChar -/
-def NameStartChar : Parsec LeanChar := attempt do
-  let c ← anyChar
+def NameStartChar : Parser LeanChar := attempt do
+  let c ← any
  if ('A' ≤ c ∧ c ≤ 'Z') ∨ ('a' ≤ c ∧ c ≤ 'z') then pure c
  else if c = ':' ∨ c = '_' then pure c
  else
@@ -69,44 +70,44 @@ def NameStartChar : Parsec LeanChar := attempt do
    else fail "expected a name character"

 /-- https://www.w3.org/TR/xml/#NT-NameChar -/
-def NameChar : Parsec LeanChar :=
+def NameChar : Parser LeanChar :=
  NameStartChar <|> digit <|> pchar '-' <|> pchar '.' <|> pchar '\xB7'
  <|> satisfy (λ c => ('\u0300' ≤ c ∧ c ≤ '\u036F') ∨ ('\u203F' ≤ c ∧ c ≤ '\u2040'))

 /-- https://www.w3.org/TR/xml/#NT-Name -/
-def Name : Parsec String := do
+def Name : Parser String := do
  let x ← NameStartChar
  manyCharsCore NameChar x.toString

 /-- https://www.w3.org/TR/xml/#NT-VersionNum -/
-def VersionNum : Parsec Unit :=
+def VersionNum : Parser Unit :=
  skipString "1." <* (many1 digit)

 /-- https://www.w3.org/TR/xml/#NT-VersionInfo -/
-def VersionInfo : Parsec Unit := do
+def VersionInfo : Parser Unit := do
  S *>
  skipString "version"
  Eq
  quote VersionNum

 /-- https://www.w3.org/TR/xml/#NT-EncName -/
-def EncName : Parsec String := do
+def EncName : Parser String := do
  let x ← asciiLetter
  manyCharsCore (asciiLetter <|> digit <|> pchar '-' <|> pchar '_' <|> pchar '.') x.toString

 /-- https://www.w3.org/TR/xml/#NT-EncodingDecl -/
-def EncodingDecl : Parsec String := do
+def EncodingDecl : Parser String := do
  S *>
  skipString "encoding"
  Eq
  quote EncName

 /-- https://www.w3.org/TR/xml/#NT-SDDecl -/
-def SDDecl : Parsec String := do
+def SDDecl : Parser String := do
  S *> skipString "standalone" *> Eq *> quote (pstring "yes" <|> pstring "no")

 /-- https://www.w3.org/TR/xml/#NT-XMLDecl -/
-def XMLdecl : Parsec Unit := do
+def XMLdecl : Parser Unit := do
  skipString "<?xml"
  VersionInfo
  optional EncodingDecl *>
@@ -115,7 +116,7 @@ def XMLdecl : Parsec Unit := do
  skipString "?>"

 /-- https://www.w3.org/TR/xml/#NT-Comment -/
-def Comment : Parsec String :=
+def Comment : Parser String :=
  let notDash := Char.toString <$> satisfy (λ c => c ≠ '-')
  skipString "<!--" *>
  Array.foldl String.append "" <$> many (attempt <| notDash <|> (do
@@ -125,45 +126,45 @@ def Comment : Parsec String :=
  <* skipString "-->"

 /-- https://www.w3.org/TR/xml/#NT-PITarget -/
-def PITarget : Parsec String :=
+def PITarget : Parser String :=
  Name <* (skipChar 'X' <|> skipChar 'x') <* (skipChar 'M' <|> skipChar 'm') <* (skipChar 'L' <|> skipChar 'l')

 /-- https://www.w3.org/TR/xml/#NT-PI -/
-def PI : Parsec Unit := do
+def PI : Parser Unit := do
  skipString "<?"
  <* PITarget <*
  optional (S *> manyChars (notFollowedBy (skipString "?>") *> Char))
  skipString "?>"

 /-- https://www.w3.org/TR/xml/#NT-Misc -/
-def Misc : Parsec Unit :=
+def Misc : Parser Unit :=
  Comment *> pure () <|> PI <|> S *> pure ()

 /-- https://www.w3.org/TR/xml/#NT-SystemLiteral -/
-def SystemLiteral : Parsec String :=
+def SystemLiteral : Parser String :=
  pchar '"' *> manyChars (satisfy λ c => c ≠ '"') <* pchar '"'
  <|> pchar '\'' *> manyChars (satisfy λ c => c ≠ '\'') <* pure '\''

 /-- https://www.w3.org/TR/xml/#NT-PubidChar -/
-def PubidChar : Parsec LeanChar :=
+def PubidChar : Parser LeanChar :=
  asciiLetter <|> digit <|> endl <|> attempt do
-  let c ← anyChar
+  let c ← any
  if "-'()+,./:=?;!*#@$_%".contains c then pure c else fail "PublidChar expected"

 /-- https://www.w3.org/TR/xml/#NT-PubidLiteral -/
-def PubidLiteral : Parsec String :=
+def PubidLiteral : Parser String :=
  pchar '"' *> manyChars PubidChar <* pchar '"'
  <|> pchar '\'' *> manyChars (attempt do
    let c ← PubidChar
    if c = '\'' then fail "'\\'' not expected" else pure c) <* pchar '\''

 /-- https://www.w3.org/TR/xml/#NT-ExternalID -/
-def ExternalID : Parsec Unit :=
+def ExternalID : Parser Unit :=
  skipString "SYSTEM" *> S *> SystemLiteral *> pure ()
  <|> skipString "PUBLIC" *> S *> PubidLiteral *> S *> SystemLiteral *> pure ()

 /-- https://www.w3.org/TR/xml/#NT-Mixed -/
-def Mixed : Parsec Unit :=
+def Mixed : Parser Unit :=
  (do
    skipChar '('
    optional S *>
@@ -175,11 +176,11 @@ def Mixed : Parsec Unit :=

 mutual
  /-- https://www.w3.org/TR/xml/#NT-cp -/
-  partial def cp : Parsec Unit :=
+  partial def cp : Parser Unit :=
    (Name *> pure () <|> choice <|> seq) <* optional (skipChar '?' <|> skipChar '*' <|> skipChar '+')

  /-- https://www.w3.org/TR/xml/#NT-choice -/
-  partial def choice : Parsec Unit := do
+  partial def choice : Parser Unit := do
    skipChar '('
    optional S *>
    cp
@@ -188,7 +189,7 @@ mutual
    skipChar ')'

  /-- https://www.w3.org/TR/xml/#NT-seq -/
-  partial def seq : Parsec Unit := do
+  partial def seq : Parser Unit := do
    skipChar '('
    optional S *>
    cp
@@ -198,15 +199,15 @@ mutual
 end

 /-- https://www.w3.org/TR/xml/#NT-children -/
-def children : Parsec Unit :=
+def children : Parser Unit :=
  (choice <|> seq) <* optional (skipChar '?' <|> skipChar '*' <|> skipChar '+')

 /-- https://www.w3.org/TR/xml/#NT-contentspec -/
-def contentspec : Parsec Unit := do
+def contentspec : Parser Unit := do
  skipString "EMPTY" <|> skipString "ANY" <|> Mixed <|> children

 /-- https://www.w3.org/TR/xml/#NT-elementdecl -/
-def elementDecl : Parsec Unit := do
+def elementDecl : Parser Unit := do
  skipString "<!ELEMENT"
  S *>
  Name *>
@@ -215,11 +216,11 @@ def elementDecl : Parsec Unit := do
  skipChar '>'

 /-- https://www.w3.org/TR/xml/#NT-StringType -/
-def StringType : Parsec Unit :=
+def StringType : Parser Unit :=
  skipString "CDATA"

 /-- https://www.w3.org/TR/xml/#NT-TokenizedType -/
-def TokenizedType : Parsec Unit :=
+def TokenizedType : Parser Unit :=
  skipString "ID"
  <|> skipString "IDREF"
  <|> skipString "IDREFS"
@@ -229,7 +230,7 @@ def TokenizedType : Parsec Unit :=
  <|> skipString "NMTOKENS"

 /-- https://www.w3.org/TR/xml/#NT-NotationType -/
-def NotationType : Parsec Unit := do
+def NotationType : Parser Unit := do
  skipString "NOTATION"
  S *>
  skipChar '(' <*
@@ -239,11 +240,11 @@ def NotationType : Parsec Unit := do
  skipChar ')'

 /-- https://www.w3.org/TR/xml/#NT-Nmtoken -/
-def Nmtoken : Parsec String := do
+def Nmtoken : Parser String := do
  many1Chars NameChar

 /-- https://www.w3.org/TR/xml/#NT-Enumeration -/
-def Enumeration : Parsec Unit := do
+def Enumeration : Parser Unit := do
  skipChar '('
  optional S *>
  Nmtoken *> many (optional S *> skipChar '|' *> optional S *> Nmtoken) *>
@@ -251,11 +252,11 @@ def Enumeration : Parsec Unit := do
  skipChar ')'

 /-- https://www.w3.org/TR/xml/#NT-EnumeratedType -/
-def EnumeratedType : Parsec Unit :=
+def EnumeratedType : Parser Unit :=
  NotationType <|> Enumeration

 /-- https://www.w3.org/TR/xml/#NT-AttType -/
-def AttType : Parsec Unit :=
+def AttType : Parser Unit :=
  StringType <|> TokenizedType <|> EnumeratedType

 def predefinedEntityToChar : String → Option LeanChar
@@ -267,7 +268,7 @@ def predefinedEntityToChar : String → Option LeanChar
 | _ => none

 /-- https://www.w3.org/TR/xml/#NT-EntityRef -/
-def EntityRef : Parsec $ Option LeanChar := attempt $
+def EntityRef : Parser $ Option LeanChar := attempt $
  skipChar '&' *> predefinedEntityToChar <$> Name <* skipChar ';'

@[inline]
@@ -280,7 +281,7 @@ def digitsToNat (base : Nat) (digits : Array Nat) : Nat :=
  digits.foldl (λ r d => r * base + d) 0

 /-- https://www.w3.org/TR/xml/#NT-CharRef -/
-def CharRef : Parsec LeanChar := do
+def CharRef : Parser LeanChar := do
  skipString "&#"
  let charCode ←
    digitsToNat 10 <$> many1 (hexDigitToNat <$> digit)
@@ -289,11 +290,11 @@ def CharRef : Parsec LeanChar := do
  return Char.ofNat charCode

 /-- https://www.w3.org/TR/xml/#NT-Reference -/
-def Reference : Parsec $ Option LeanChar :=
+def Reference : Parser $ Option LeanChar :=
  EntityRef <|> some <$> CharRef

 /-- https://www.w3.org/TR/xml/#NT-AttValue -/
-def AttValue : Parsec String := do
+def AttValue : Parser String := do
  let chars ←
  (do
    skipChar '"'
@@ -306,25 +307,25 @@ def AttValue : Parsec String := do
  return chars.foldl (λ s c => if let some c := c then s.push c else s) ""

 /-- https://www.w3.org/TR/xml/#NT-DefaultDecl -/
-def DefaultDecl : Parsec Unit :=
+def DefaultDecl : Parser Unit :=
  skipString "#REQUIRED"
  <|> skipString "#IMPLIED"
  <|> optional (skipString "#FIXED" <* S) *> AttValue *> pure ()

 /-- https://www.w3.org/TR/xml/#NT-AttDef -/
-def AttDef : Parsec Unit :=
+def AttDef : Parser Unit :=
  S *> Name *> S *> AttType *> S *> DefaultDecl

 /-- https://www.w3.org/TR/xml/#NT-AttlistDecl -/
-def AttlistDecl : Parsec Unit :=
+def AttlistDecl : Parser Unit :=
  skipString "<!ATTLIST" *> S *> Name *> many AttDef *> optional S *> skipChar '>'

 /-- https://www.w3.org/TR/xml/#NT-PEReference -/
-def PEReference : Parsec Unit :=
+def PEReference : Parser Unit :=
  skipChar '%' *> Name *> skipChar ';'

 /-- https://www.w3.org/TR/xml/#NT-EntityValue -/
-def EntityValue : Parsec String := do
+def EntityValue : Parser String := do
  let chars ←
  (do
    skipChar '"'
@@ -338,51 +339,51 @@ def EntityValue : Parsec String := do


 /-- https://www.w3.org/TR/xml/#NT-NDataDecl -/
-def NDataDecl : Parsec Unit :=
+def NDataDecl : Parser Unit :=
  S *> skipString "NDATA" <* S <* Name

 /-- https://www.w3.org/TR/xml/#NT-EntityDef -/
-def EntityDef : Parsec Unit :=
+def EntityDef : Parser Unit :=
  EntityValue *> pure () <|> (ExternalID <* optional NDataDecl)

 /-- https://www.w3.org/TR/xml/#NT-GEDecl -/
-def GEDecl : Parsec Unit :=
+def GEDecl : Parser Unit :=
  skipString "<!ENTITY" *> S *> Name *> S *> EntityDef *> optional S *> skipChar '>'

 /-- https://www.w3.org/TR/xml/#NT-PEDef -/
-def PEDef : Parsec Unit :=
+def PEDef : Parser Unit :=
  EntityValue *> pure () <|> ExternalID

 /-- https://www.w3.org/TR/xml/#NT-PEDecl -/
-def PEDecl : Parsec Unit :=
+def PEDecl : Parser Unit :=
  skipString "<!ENTITY" *> S *> skipChar '%' *> S *> Name *> PEDef *> optional S *> skipChar '>'

 /-- https://www.w3.org/TR/xml/#NT-EntityDecl -/
-def EntityDecl : Parsec Unit :=
+def EntityDecl : Parser Unit :=
  GEDecl <|> PEDecl

 /-- https://www.w3.org/TR/xml/#NT-PublicID -/
-def PublicID : Parsec Unit :=
+def PublicID : Parser Unit :=
  skipString "PUBLIC" <* S <* PubidLiteral

 /-- https://www.w3.org/TR/xml/#NT-NotationDecl -/
-def NotationDecl : Parsec Unit :=
+def NotationDecl : Parser Unit :=
  skipString "<!NOTATION" *> S *> Name *> (ExternalID <|> PublicID) *> optional S *> skipChar '>'

 /-- https://www.w3.org/TR/xml/#NT-markupdecl -/
-def markupDecl : Parsec Unit :=
+def markupDecl : Parser Unit :=
  elementDecl <|> AttlistDecl <|> EntityDecl <|> NotationDecl <|> PI <|> (Comment *> pure ())

 /-- https://www.w3.org/TR/xml/#NT-DeclSep -/
-def DeclSep : Parsec Unit :=
+def DeclSep : Parser Unit :=
  PEReference <|> S *> pure ()

 /-- https://www.w3.org/TR/xml/#NT-intSubset -/
-def intSubset : Parsec Unit :=
+def intSubset : Parser Unit :=
  many (markupDecl <|> DeclSep) *> pure ()

 /-- https://www.w3.org/TR/xml/#NT-doctypedecl -/
-def doctypedecl : Parsec Unit := do
+def doctypedecl : Parser Unit := do
  skipString "<!DOCTYPE"
  S *>
  Name *>
@@ -392,19 +393,19 @@ def doctypedecl : Parsec Unit := do
  skipChar '>'

 /-- https://www.w3.org/TR/xml/#NT-prolog -/
-def prolog : Parsec Unit :=
+def prolog : Parser Unit :=
  optional XMLdecl *>
  many Misc *>
  optional (doctypedecl <* many Misc) *> pure ()

 /-- https://www.w3.org/TR/xml/#NT-Attribute -/
-def Attribute : Parsec (String × String) := do
+def Attribute : Parser (String × String) := do
  let name ← Name
  Eq
  let value ← AttValue
  return (name, value)

-protected def elementPrefix : Parsec (Array Content → Element) := do
+protected def elementPrefix : Parser (Array Content → Element) := do
  skipChar '<'
  let name ← Name
  let attributes ← many (attempt <| S *> Attribute)
@@ -412,40 +413,40 @@ protected def elementPrefix : Parsec (Array Content → Element) := do
  return Element.Element name (RBMap.fromList attributes.toList compare)

 /-- https://www.w3.org/TR/xml/#NT-EmptyElemTag -/
-def EmptyElemTag (elem : Array Content → Element) : Parsec Element := do
+def EmptyElemTag (elem : Array Content → Element) : Parser Element := do
  skipString "/>" *> pure (elem #[])

 /-- https://www.w3.org/TR/xml/#NT-STag -/
-def STag (elem : Array Content → Element) : Parsec (Array Content → Element) := do
+def STag (elem : Array Content → Element) : Parser (Array Content → Element) := do
  skipChar '>' *> pure elem

 /-- https://www.w3.org/TR/xml/#NT-ETag -/
-def ETag : Parsec Unit :=
+def ETag : Parser Unit :=
  skipString "</" *> Name *> optional S *> skipChar '>'

 /-- https://www.w3.org/TR/xml/#NT-CDStart -/
-def CDStart : Parsec Unit :=
+def CDStart : Parser Unit :=
  skipString "<![CDATA["

 /-- https://www.w3.org/TR/xml/#NT-CDEnd -/
-def CDEnd : Parsec Unit :=
+def CDEnd : Parser Unit :=
  skipString "]]>"

 /-- https://www.w3.org/TR/xml/#NT-CData -/
-def CData : Parsec String :=
-  manyChars (notFollowedBy (skipString "]]>") *> anyChar)
+def CData : Parser String :=
+  manyChars (notFollowedBy (skipString "]]>") *> any)

 /-- https://www.w3.org/TR/xml/#NT-CDSect -/
-def CDSect : Parsec String :=
+def CDSect : Parser String :=
  CDStart *> CData <* CDEnd

 /-- https://www.w3.org/TR/xml/#NT-CharData -/
-def CharData : Parsec String :=
+def CharData : Parser String :=
  notFollowedBy (skipString "]]>") *> manyChars (satisfy λ c => c ≠ '<' ∧ c ≠ '&')

 mutual
  /-- https://www.w3.org/TR/xml/#NT-content -/
-  partial def content : Parsec (Array Content) := do
+  partial def content : Parser (Array Content) := do
    let x ← optional (Content.Character <$> CharData)
    let xs ← many do
      let y ←
@@ -468,20 +469,20 @@ mutual
    return res

  /-- https://www.w3.org/TR/xml/#NT-element -/
-  partial def element : Parsec Element := do
+  partial def element : Parser Element := do
    let elem ← Parser.elementPrefix
    EmptyElemTag elem <|> STag elem <*> content <* ETag

 end

 /-- https://www.w3.org/TR/xml/#NT-document -/
-def document : Parsec Element := prolog *> element <* many Misc <* eof
+def document : Parser Element := prolog *> element <* many Misc <* eof

 end Parser

 def parse (s : String) : Except String Element :=
  match Xml.Parser.document s.mkIterator with
-  | Parsec.ParseResult.success _ res => Except.ok res
-  | Parsec.ParseResult.error it err  => Except.error s!"offset {it.i.byteIdx.repr}: {err}\n{(it.prevn 10).extract it}"
+  | .success _ res => Except.ok res
+  | .error it err  => Except.error s!"offset {it.i.byteIdx.repr}: {err}\n{(it.prevn 10).extract it}"

 end Xml
--- a/src/Lean/Elab/Frontend.lean
+++ b/src/Lean/Elab/Frontend.lean
@@ -81,10 +81,6 @@ end Frontend

 open Frontend

-def IO.processCommands (inputCtx : Parser.InputContext) (parserState : Parser.ModuleParserState) (commandState : Command.State) : IO State := do
-  let (_, s) ← (Frontend.processCommands.run { inputCtx := inputCtx }).run { commandState := commandState, parserState := parserState, cmdPos := parserState.pos }
-  pure s
-
 structure IncrementalState extends State where
  inputCtx    : Parser.InputContext
  initialSnap : Language.Lean.CommandParsedSnapshot
@@ -92,12 +88,10 @@ deriving Nonempty

 open Language in
 /--
-Variant of `IO.processCommands` that uses the new Lean language processor implementation for
-potential incremental reuse. Pass in result of a previous invocation done with the same state
-(but usually different input context) to allow for reuse.
+Variant of `IO.processCommands` that allows for potential incremental reuse. Pass in the result of a
+previous invocation done with the same state (but usually different input context) to allow for
+reuse.
 -/
-- `IO.processCommands` can be reimplemented on top of this as soon as the additional tasks speed up
-- things instead of slowing them down
 partial def IO.processCommandsIncrementally (inputCtx : Parser.InputContext)
    (parserState : Parser.ModuleParserState) (commandState : Command.State)
    (old? : Option IncrementalState) :
@@ -110,7 +104,7 @@ where
    let snap := t.get
    let commands := commands.push snap.data.stx
    if let some next := snap.nextCmdSnap? then
-      go initialSnap next commands
+      go initialSnap next.task commands
    else
      -- Opting into reuse also enables incremental reporting, so make sure to collect messages from
      -- all snapshots
@@ -126,6 +120,11 @@ where
        inputCtx, initialSnap, commands
      }

+def IO.processCommands (inputCtx : Parser.InputContext) (parserState : Parser.ModuleParserState)
+    (commandState : Command.State) : IO State := do
+  let st ← IO.processCommandsIncrementally inputCtx parserState commandState none
+  return st.toState
+
 def process (input : String) (env : Environment) (opts : Options) (fileName : Option String := none) : IO (Environment × MessageLog) := do
  let fileName   := fileName.getD "<input>"
  let inputCtx   := Parser.mkInputContext input fileName
@@ -144,62 +143,31 @@ def runFrontend
    : IO (Environment × Bool) := do
  let startTime := (← IO.monoNanosNow).toFloat / 1000000000
  let inputCtx := Parser.mkInputContext input fileName
-  if true then
-    -- Temporarily keep alive old cmdline driver for the Lean language so that we don't pay the
-    -- overhead of passing the environment between snapshots until we actually make good use of it
-    -- outside the server
-    let (header, parserState, messages) ← Parser.parseHeader inputCtx
-    -- allow `env` to be leaked, which would live until the end of the process anyway
-    let (env, messages) ← processHeader (leakEnv := true) header opts messages inputCtx trustLevel
-    let env := env.setMainModule mainModuleName
-    let mut commandState := Command.mkState env messages opts
-    let elabStartTime := (← IO.monoNanosNow).toFloat / 1000000000
-
-    if ileanFileName?.isSome then
-      -- Collect InfoTrees so we can later extract and export their info to the ilean file
-      commandState := { commandState with infoState.enabled := true }
-
-    let s ← IO.processCommands inputCtx parserState commandState
-    Language.reportMessages s.commandState.messages opts jsonOutput
-
-    if let some ileanFileName := ileanFileName? then
-      let trees := s.commandState.infoState.trees.toArray
-      let references ←
-        Lean.Server.findModuleRefs inputCtx.fileMap trees (localVars := false) |>.toLspModuleRefs
-      let ilean := { module := mainModuleName, references : Lean.Server.Ilean }
-      IO.FS.writeFile ileanFileName $ Json.compress $ toJson ilean
-
-    if let some out := trace.profiler.output.get? opts then
-      let traceState := s.commandState.traceState
-      -- importing does not happen in an elaboration monad, add now
-      let traceState := { traceState with
-        traces := #[{
-          ref := .missing,
-          msg := .trace { cls := `Import, startTime, stopTime := elabStartTime }
-            (.ofFormat "importing") #[]
-        }].toPArray' ++ traceState.traces
-      }
-      let profile ← Firefox.Profile.export mainModuleName.toString startTime traceState opts
-      IO.FS.writeFile ⟨out⟩ <| Json.compress <| toJson profile
-
-    return (s.commandState.env, !s.commandState.messages.hasErrors)
-
+  let opts := Language.Lean.internal.minimalSnapshots.set opts true
  let ctx := { inputCtx with }
  let processor := Language.Lean.process
  let snap ← processor (fun _ => pure <| .ok { mainModuleName, opts, trustLevel }) none ctx
  let snaps := Language.toSnapshotTree snap
  snaps.runAndReport opts jsonOutput
+
  if let some ileanFileName := ileanFileName? then
    let trees := snaps.getAll.concatMap (match ·.infoTree? with | some t => #[t] | _ => #[])
    let references := Lean.Server.findModuleRefs inputCtx.fileMap trees (localVars := false)
    let ilean := { module := mainModuleName, references := ← references.toLspModuleRefs : Lean.Server.Ilean }
    IO.FS.writeFile ileanFileName $ Json.compress $ toJson ilean

-  let hasErrors := snaps.getAll.any (·.diagnostics.msgLog.hasErrors)
  -- TODO: remove default when reworking cmdline interface in Lean; currently the only case
  -- where we use the environment despite errors in the file is `--stats`
-  let env := Language.Lean.waitForFinalEnv? snap |>.getD (← mkEmptyEnvironment)
-  pure (env, !hasErrors)
+  let some cmdState := Language.Lean.waitForFinalCmdState? snap
+    | return (← mkEmptyEnvironment, false)
+
+  if let some out := trace.profiler.output.get? opts then
+    let traceState := cmdState.traceState
+    let profile ← Firefox.Profile.export mainModuleName.toString startTime traceState opts
+    IO.FS.writeFile ⟨out⟩ <| Json.compress <| toJson profile
+
+  let hasErrors := snaps.getAll.any (·.diagnostics.msgLog.hasErrors)
+  pure (cmdState.env, !hasErrors)


 end Lean.Elab
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -323,6 +323,10 @@ private def declValToTerminationHint (declVal : Syntax) : TermElabM TerminationH
  else
    return .none

+def instantiateMVarsProfiling (e : Expr) : MetaM Expr := do
+  profileitM Exception s!"instantiate metavars" (← getOptions) do
+    instantiateMVars e
+
 private def elabFunValues (headers : Array DefViewElabHeader) : TermElabM (Array Expr) :=
  headers.mapM fun header => do
    let mut reusableResult? := none
@@ -348,7 +352,7 @@ private def elabFunValues (headers : Array DefViewElabHeader) : TermElabM (Array
          elabTermEnsuringType valStx type <* synthesizeSyntheticMVarsNoPostponing
        -- NOTE: without this `instantiatedMVars`, `mkLambdaFVars` may leave around a redex that
        -- leads to more section variables being included than necessary
-        let val ← instantiateMVars val
+        let val ← instantiateMVarsProfiling val
        mkLambdaFVars xs val
    if let some snap := header.bodySnap? then
      snap.new.resolve <| some {
@@ -389,7 +393,7 @@ private def instantiateMVarsAtHeader (header : DefViewElabHeader) : TermElabM De

 private def instantiateMVarsAtLetRecToLift (toLift : LetRecToLift) : TermElabM LetRecToLift := do
  let type ← instantiateMVars toLift.type
-  let val ← instantiateMVars toLift.val
+  let val ← instantiateMVarsProfiling toLift.val
  pure { toLift with type, val }

 private def typeHasRecFun (type : Expr) (funFVars : Array Expr) (letRecsToLift : List LetRecToLift) : Option FVarId :=
@@ -597,7 +601,7 @@ private def pickMaxFVar? (lctx : LocalContext) (fvarIds : Array FVarId) : Option
  fvarIds.getMax? fun fvarId₁ fvarId₂ => (lctx.get! fvarId₁).index < (lctx.get! fvarId₂).index

 private def preprocess (e : Expr) : TermElabM Expr := do
-  let e ← instantiateMVars e
+  let e ← instantiateMVarsProfiling e
  -- which let-decls are dependent. We say a let-decl is dependent if its lambda abstraction is type incorrect.
  Meta.check e
  pure e
@@ -708,7 +712,7 @@ private def mkLetRecClosures (sectionVars : Array Expr) (mainFVarIds : Array FVa
      -- This can happen when this particular let-rec has nested let-rec that have been resolved in previous iterations.
      -- This code relies on the fact that nested let-recs occur before the outer most let-recs at `letRecsToLift`.
      -- Unresolved nested let-recs appear as metavariables before they are resolved. See `assignExprMVar` at `mkLetRecClosureFor`
-      let valNew ← instantiateMVars letRecsToLift[i]!.val
+      let valNew ← instantiateMVarsProfiling letRecsToLift[i]!.val
      letRecsToLift := letRecsToLift.modify i fun t => { t with val := valNew }
      -- We have to recompute the `freeVarMap` in this case. This overhead should not be an issue in practice.
      freeVarMap ← mkFreeVarMap sectionVars mainFVarIds recFVarIds letRecsToLift
@@ -821,10 +825,10 @@ def main (sectionVars : Array Expr) (mainHeaders : Array DefViewElabHeader) (mai
    let letRecsToLift ← letRecsToLift.mapM fun toLift => withLCtx toLift.lctx toLift.localInstances do
      Meta.check toLift.type
      Meta.check toLift.val
-      return { toLift with val := (← instantiateMVars toLift.val), type := (← instantiateMVars toLift.type) }
+      return { toLift with val := (← instantiateMVarsProfiling toLift.val), type := (← instantiateMVars toLift.type) }
    let letRecClosures ← mkLetRecClosures sectionVars mainFVarIds recFVarIds letRecsToLift
    -- mkLetRecClosures assign metavariables that were placeholders for the lifted declarations.
-    let mainVals    ← mainVals.mapM (instantiateMVars ·)
+    let mainVals    ← mainVals.mapM (instantiateMVarsProfiling ·)
    let mainHeaders ← mainHeaders.mapM instantiateMVarsAtHeader
    let letRecClosures ← letRecClosures.mapM fun closure => do pure { closure with toLift := (← instantiateMVarsAtLetRecToLift closure.toLift) }
    -- Replace fvarIds for functions being defined with closed terms
@@ -923,7 +927,7 @@ where
          try
            let values ← elabFunValues headers
            Term.synthesizeSyntheticMVarsNoPostponing
-            values.mapM (instantiateMVars ·)
+            values.mapM (instantiateMVarsProfiling ·)
          catch ex =>
            logException ex
            headers.mapM fun header => mkSorry header.type (synthetic := true)
--- a/src/Lean/Elab/PreDefinition/Basic.lean
+++ b/src/Lean/Elab/PreDefinition/Basic.lean
@@ -7,6 +7,9 @@ prelude
 import Init.ShareCommon
 import Lean.Compiler.NoncomputableAttr
 import Lean.Util.CollectLevelParams
+import Lean.Util.NumObjs
+import Lean.Util.NumApps
+import Lean.PrettyPrinter
 import Lean.Meta.AbstractNestedProofs
 import Lean.Meta.ForEachExpr
 import Lean.Elab.RecAppSyntax
@@ -17,7 +20,6 @@ namespace Lean.Elab
 open Meta
 open Term

-
 /--
  A (potentially recursive) definition.
  The elaborator converts it into Kernel definitions using many different strategies.
@@ -98,15 +100,33 @@ private def compileDecl (decl : Declaration) : TermElabM Bool := do
      throw ex
  return true

+register_builtin_option diagnostics.threshold.proofSize : Nat := {
+  defValue := 16384
+  group    := "diagnostics"
+  descr    := "only display proof statistics when proof has at least this number of terms"
+}
+
+private def reportTheoremDiag (d : TheoremVal) : TermElabM Unit := do
+  if (← isDiagnosticsEnabled) then
+    let proofSize ← d.value.numObjs
+    if proofSize > diagnostics.threshold.proofSize.get (← getOptions) then
+      let sizeMsg := MessageData.trace { cls := `size } m!"{proofSize}" #[]
+      let constOccs ← d.value.numApps (threshold := diagnostics.threshold.get (← getOptions))
+      let constOccsMsg ← constOccs.mapM fun (declName, numOccs) => return MessageData.trace { cls := `occs } m!"{MessageData.ofConst (← mkConstWithLevelParams declName)} ↦ {numOccs}" #[]
+      -- let info
+      logInfo <| MessageData.trace { cls := `theorem } m!"{d.name}" (#[sizeMsg] ++ constOccsMsg)
+
 private def addNonRecAux (preDef : PreDefinition) (compile : Bool) (all : List Name) (applyAttrAfterCompilation := true) : TermElabM Unit :=
  withRef preDef.ref do
    let preDef ← abstractNestedProofs preDef
    let decl ←
      match preDef.kind with
      | DefKind.«theorem» =>
-        pure <| Declaration.thmDecl {
+        let d := {
          name := preDef.declName, levelParams := preDef.levelParams, type := preDef.type, value := preDef.value, all
        }
+        reportTheoremDiag d
+        pure <| Declaration.thmDecl d
      | DefKind.«opaque»  =>
        pure <| Declaration.opaqueDecl {
          name := preDef.declName, levelParams := preDef.levelParams, type := preDef.type, value := preDef.value
--- a/src/Lean/Expr.lean
+++ b/src/Lean/Expr.lean
@@ -1452,28 +1452,26 @@ partial def betaRev (f : Expr) (revArgs : Array Expr) (useZeta := false) (preser
  else
    let sz := revArgs.size
    let rec go (e : Expr) (i : Nat) : Expr :=
+      let done (_ : Unit) : Expr :=
+        let n := sz - i
+        mkAppRevRange (e.instantiateRange n sz revArgs) 0 n revArgs
      match e with
-      | Expr.lam _ _ b _ =>
+      | .lam _ _ b _ =>
        if i + 1 < sz then
          go b (i+1)
        else
-          let n := sz - (i + 1)
-          mkAppRevRange (b.instantiateRange n sz revArgs) 0 n revArgs
-      | Expr.letE _ _ v b _ =>
+          b.instantiate revArgs
+      | .letE _ _ v b _ =>
        if useZeta && i < sz then
          go (b.instantiate1 v) i
        else
-          let n := sz - i
-          mkAppRevRange (e.instantiateRange n sz revArgs) 0 n revArgs
-      | Expr.mdata k b =>
+          done ()
+      | .mdata _ b =>
        if preserveMData then
-          let n := sz - i
-          mkMData k (mkAppRevRange (b.instantiateRange n sz revArgs) 0 n revArgs)
+          done ()
        else
          go b i
-      | b =>
-        let n := sz - i
-        mkAppRevRange (b.instantiateRange n sz revArgs) 0 n revArgs
+      | _ => done ()
    go f 0

 /--
--- a/src/Lean/Language/Lean.lean
+++ b/src/Lean/Language/Lean.lean
@@ -234,6 +234,54 @@ structure SetupImportsResult where
  /-- Kernel trust level. -/
  trustLevel : UInt32 := 0

+/-- Performance option used by cmdline driver. -/
+register_builtin_option internal.minimalSnapshots : Bool := {
+  defValue := false
+  descr    := "reduce information stored in snapshots to the minimum necessary for the cmdline \
+driver: diagnostics per command and final full snapshot"
+}
+
+/--
+Parses values of options registered during import and left by the C++ frontend as strings, fails if
+any option names remain unknown.
+-/
+def reparseOptions (opts : Options) : IO Options := do
+  let mut opts := opts
+  let decls ← getOptionDecls
+  for (name, val) in opts do
+    let .ofString val := val
+      | continue  -- Already parsed by C++
+    -- Options can be prefixed with `weak` in order to turn off the error when the option is not
+    -- defined
+    let weak := name.getRoot == `weak
+    if weak then
+      opts := opts.erase name
+    let name := name.replacePrefix `weak Name.anonymous
+    let some decl := decls.find? name
+      | unless weak do
+          throw <| .userError s!"invalid -D parameter, unknown configuration option '{name}'
+
+If the option is defined in this library, use '-D{`weak ++ name}' to set it conditionally"
+
+    match decl.defValue with
+    | .ofBool _ =>
+      match val with
+      | "true"  => opts := opts.insert name true
+      | "false" => opts := opts.insert name false
+      | _ =>
+        throw <| .userError s!"invalid -D parameter, invalid configuration option '{val}' value, \
+          it must be true/false"
+    | .ofNat _ =>
+      let some val := val.toNat?
+        | throw <| .userError s!"invalid -D parameter, invalid configuration option '{val}' value, \
+            it must be a natural number"
+      opts := opts.insert name val
+    | .ofString _ => opts := opts.insert name val
+    | _ => throw <| .userError s!"invalid -D parameter, configuration option '{name}' \
+              cannot be set in the command line, use set_option command"
+
+  return opts
+
 /--
 Entry point of the Lean language processor.

@@ -279,9 +327,11 @@ where
              if let some oldProcSuccess := oldProcessed.result? then
                -- also wait on old command parse snapshot as parsing is cheap and may allow for
                -- elaboration reuse
-                oldProcSuccess.firstCmdSnap.bindIO (sync := true) fun oldCmd =>
+                oldProcSuccess.firstCmdSnap.bindIO (sync := true) fun oldCmd => do
+                  let prom ← IO.Promise.new
+                  let _ ← IO.asTask (parseCmd oldCmd newParserState oldProcSuccess.cmdState oldProcSuccess.cmdState.env prom ctx)
                  return .pure { oldProcessed with result? := some { oldProcSuccess with
-                    firstCmdSnap := (← parseCmd oldCmd newParserState oldProcSuccess.cmdState ctx) } }
+                    firstCmdSnap := { range? := none, task := prom.result } } }
              else
                return .pure oldProcessed) } }
      else return old
@@ -343,42 +393,68 @@ where
      let setup ← match (← setupImports stx) with
        | .ok setup => pure setup
        | .error snap => return snap
+
+      let startTime := (← IO.monoNanosNow).toFloat / 1000000000
      -- allows `headerEnv` to be leaked, which would live until the end of the process anyway
      let (headerEnv, msgLog) ← Elab.processHeader (leakEnv := true) stx setup.opts .empty
        ctx.toInputContext setup.trustLevel
+      let stopTime := (← IO.monoNanosNow).toFloat / 1000000000
      let diagnostics := (← Snapshot.Diagnostics.ofMessageLog msgLog)
      if msgLog.hasErrors then
        return { diagnostics, result? := none }

      let headerEnv := headerEnv.setMainModule setup.mainModuleName
-      let cmdState := Elab.Command.mkState headerEnv msgLog setup.opts
-      let cmdState := { cmdState with infoState := {
-        enabled := true
-        trees := #[Elab.InfoTree.context (.commandCtx {
-          env     := headerEnv
-          fileMap := ctx.fileMap
-          ngen    := { namePrefix := `_import }
-        }) (Elab.InfoTree.node
-            (Elab.Info.ofCommandInfo { elaborator := `header, stx })
-            (stx[1].getArgs.toList.map (fun importStx =>
-              Elab.InfoTree.node (Elab.Info.ofCommandInfo {
-                elaborator := `import
-                stx := importStx
-              }) #[].toPArray'
-            )).toPArray'
-        )].toPArray'
-      }}
+      let mut traceState := default
+      if trace.profiler.output.get? setup.opts |>.isSome then
+        traceState := {
+          traces := #[{
+            ref := .missing,
+            msg := .trace { cls := `Import, startTime, stopTime }
+              (.ofFormat "importing") #[]
+            : TraceElem
+          }].toPArray'
+        }
+      -- now that imports have been loaded, check options again
+      let opts ← reparseOptions setup.opts
+      let cmdState := Elab.Command.mkState headerEnv msgLog opts
+      let cmdState := { cmdState with
+        infoState := {
+          enabled := true
+          trees := #[Elab.InfoTree.context (.commandCtx {
+            env     := headerEnv
+            fileMap := ctx.fileMap
+            ngen    := { namePrefix := `_import }
+          }) (Elab.InfoTree.node
+              (Elab.Info.ofCommandInfo { elaborator := `header, stx })
+              (stx[1].getArgs.toList.map (fun importStx =>
+                Elab.InfoTree.node (Elab.Info.ofCommandInfo {
+                  elaborator := `import
+                  stx := importStx
+                }) #[].toPArray'
+              )).toPArray'
+          )].toPArray'
+        }
+        traceState
+      }
+      let prom ← IO.Promise.new
+      -- The speedup of these `markPersistent`s is negligible but they help in making unexpected
+      -- `inc_ref_cold`s more visible
+      let parserState := Runtime.markPersistent parserState
+      let cmdState := Runtime.markPersistent cmdState
+      let ctx := Runtime.markPersistent ctx
+      let _ ← IO.asTask (parseCmd none parserState cmdState cmdState.env prom ctx)
      return {
        diagnostics
        infoTree? := cmdState.infoState.trees[0]!
        result? := some {
          cmdState
-          firstCmdSnap := (← parseCmd none parserState cmdState)
+          firstCmdSnap := { range? := none, task := prom.result }
        }
      }

  parseCmd (old? : Option CommandParsedSnapshot) (parserState : Parser.ModuleParserState)
-      (cmdState : Command.State) : LeanProcessingM (SnapshotTask CommandParsedSnapshot) := do
+      (cmdState : Command.State) (initEnv : Environment) (prom : IO.Promise CommandParsedSnapshot) :
+      LeanProcessingM Unit := do
    let ctx ← read

    -- check for cancellation, most likely during elaboration of previous command, before starting
@@ -387,82 +463,100 @@ where
      -- this is a bit ugly as we don't want to adjust our API with `Option`s just for cancellation
      -- (as no-one should look at this result in that case) but anything containing `Environment`
      -- is not `Inhabited`
-      return .pure <| .mk (nextCmdSnap? := none) {
+      prom.resolve <| .mk (nextCmdSnap? := none) {
        diagnostics := .empty, stx := .missing, parserState
        elabSnap := .pure <| .ofTyped { diagnostics := .empty : SnapshotLeaf }
        finishedSnap := .pure { diagnostics := .empty, cmdState }
        tacticCache := (← IO.mkRef {})
      }
+      return

-    let unchanged old newParserState : BaseIO CommandParsedSnapshot :=
+    let unchanged old newParserState : BaseIO Unit :=
      -- when syntax is unchanged, reuse command processing task as is
      -- NOTE: even if the syntax tree is functionally unchanged, the new parser state may still
      -- have changed because of trailing whitespace and comments etc., so it is passed separately
      -- from `old`
-      if let some oldNext := old.nextCmdSnap? then
-        return .mk (data := old.data)
-          (nextCmdSnap? := (← old.data.finishedSnap.bindIO (sync := true) fun oldFinished =>
-            -- also wait on old command parse snapshot as parsing is cheap and may allow for
-            -- elaboration reuse
-            oldNext.bindIO (sync := true) fun oldNext => do
-              parseCmd oldNext newParserState oldFinished.cmdState ctx))
-      else return old  -- terminal command, we're done!
+      if let some oldNext := old.nextCmdSnap? then do
+        let newProm ← IO.Promise.new
+        let _ ← old.data.finishedSnap.bindIO fun oldFinished =>
+          -- also wait on old command parse snapshot as parsing is cheap and may allow for
+          -- elaboration reuse
+          oldNext.bindIO (sync := true) fun oldNext => do
+            parseCmd oldNext newParserState oldFinished.cmdState initEnv newProm ctx
+            return .pure ()
+        prom.resolve <| .mk (data := old.data) (nextCmdSnap? := some { range? := none, task := newProm.result })
+      else prom.resolve old  -- terminal command, we're done!

    -- fast path, do not even start new task for this snapshot
    if let some old := old? then
      if let some nextCom ← old.nextCmdSnap?.bindM (·.get?) then
        if (← isBeforeEditPos nextCom.data.parserState.pos) then
-          return .pure (← unchanged old old.data.parserState)
+          return (← unchanged old old.data.parserState)

-    SnapshotTask.ofIO (some ⟨parserState.pos, ctx.input.endPos⟩) do
-      let beginPos := parserState.pos
-      let scope := cmdState.scopes.head!
-      let pmctx := {
-        env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace
-        openDecls := scope.openDecls
-      }
-      let (stx, parserState, msgLog) := Parser.parseCommand ctx.toInputContext pmctx parserState
-        .empty
+    let beginPos := parserState.pos
+    let scope := cmdState.scopes.head!
+    let pmctx := {
+      env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace
+      openDecls := scope.openDecls
+    }
+    let (stx, parserState, msgLog) :=
+      profileit "parsing" scope.opts fun _ =>
+        Parser.parseCommand ctx.toInputContext pmctx parserState .empty

-      -- semi-fast path
-      if let some old := old? then
-        -- NOTE: as `parserState.pos` includes trailing whitespace, this forces reprocessing even if
-        -- only that whitespace changes, which is wasteful but still necessary because it may
-        -- influence the range of error messages such as from a trailing `exact`
-        if stx.eqWithInfo old.data.stx then
-          -- Here we must make sure to pass the *new* parser state; see NOTE in `unchanged`
-          return (← unchanged old parserState)
-        -- on first change, make sure to cancel old invocation
-        -- TODO: pass token into incrementality-aware elaborators to improve reuse of still-valid,
-        -- still-running elaboration steps?
-        if let some tk := ctx.oldCancelTk? then
-          tk.set
+    -- semi-fast path
+    if let some old := old? then
+      -- NOTE: as `parserState.pos` includes trailing whitespace, this forces reprocessing even if
+      -- only that whitespace changes, which is wasteful but still necessary because it may
+      -- influence the range of error messages such as from a trailing `exact`
+      if stx.eqWithInfo old.data.stx then
+        -- Here we must make sure to pass the *new* parser state; see NOTE in `unchanged`
+        return (← unchanged old parserState)
+      -- on first change, make sure to cancel old invocation
+      -- TODO: pass token into incrementality-aware elaborators to improve reuse of still-valid,
+      -- still-running elaboration steps?
+      if let some tk := ctx.oldCancelTk? then
+        tk.set

-      -- definitely resolved in `doElab` task
-      let elabPromise ← IO.Promise.new
-      let tacticCache ← old?.map (·.data.tacticCache) |>.getDM (IO.mkRef {})
-      let finishedSnap ←
-        doElab stx cmdState beginPos
-          { old? := old?.map fun old => ⟨old.data.stx, old.data.elabSnap⟩, new := elabPromise }
-          tacticCache
-          ctx
-
-      let next? ← if Parser.isTerminalCommand stx then pure none
-        -- for now, wait on "command finished" snapshot before parsing next command
-        else some <$> finishedSnap.bindIO fun finished =>
-          parseCmd none parserState finished.cmdState ctx
-      return .mk (nextCmdSnap? := next?) {
-        diagnostics := (← Snapshot.Diagnostics.ofMessageLog msgLog)
-        stx
-        parserState
-        elabSnap := { range? := stx.getRange?, task := elabPromise.result }
-        finishedSnap
+    -- definitely resolved in `doElab` task
+    let elabPromise ← IO.Promise.new
+    let tacticCache ← old?.map (·.data.tacticCache) |>.getDM (IO.mkRef {})
+    let finishedSnap ←
+      doElab stx cmdState beginPos
+        { old? := old?.map fun old => ⟨old.data.stx, old.data.elabSnap⟩, new := elabPromise }
        tacticCache
+        ctx
+
+    let minimalSnapshots := internal.minimalSnapshots.get cmdState.scopes.head!.opts
+    let next? ← if Parser.isTerminalCommand stx then pure none
+      -- for now, wait on "command finished" snapshot before parsing next command
+      else some <$> IO.Promise.new
+    let diagnostics ← Snapshot.Diagnostics.ofMessageLog msgLog
+    let data := if minimalSnapshots && !Parser.isTerminalCommand stx then {
+      diagnostics
+      stx := .missing
+      parserState := {}
+      elabSnap := { range? := stx.getRange?, task := elabPromise.result }
+      finishedSnap := .pure {
+        diagnostics := finishedSnap.diagnostics
+        infoTree? := none
+        cmdState := {
+          env := initEnv
+          maxRecDepth := 0
+        }
      }
+      tacticCache
+    } else {
+      diagnostics, stx, parserState, tacticCache
+      elabSnap := { range? := stx.getRange?, task := elabPromise.result }
+      finishedSnap := .pure finishedSnap
+    }
+    prom.resolve <| .mk (nextCmdSnap? := next?.map ({ range? := some ⟨parserState.pos, ctx.input.endPos⟩, task := ·.result })) data
+    if let some next := next? then
+      parseCmd none parserState finishedSnap.cmdState initEnv next ctx

  doElab (stx : Syntax) (cmdState : Command.State) (beginPos : String.Pos)
      (snap : SnapshotBundle DynamicSnapshot) (tacticCache : IO.Ref Tactic.Cache) :
-      LeanProcessingM (SnapshotTask CommandFinishedSnapshot) := do
+      LeanProcessingM CommandFinishedSnapshot := do
    let ctx ← read
    -- (Try to) use last line of command as range for final snapshot task. This ensures we do not
    -- retract the progress bar to a previous position in case the command support incremental
@@ -471,48 +565,46 @@ where
    -- `parseCmd` and containing the entire range of the command will determine the reported
    -- progress and be resolved effectively at the same time as this snapshot task, so `tailPos` is
    -- irrelevant in this case.
-    let tailPos := stx.getTailPos? |>.getD beginPos
-    SnapshotTask.ofIO (some ⟨tailPos, tailPos⟩) do
-      let scope := cmdState.scopes.head!
-      let cmdStateRef ← IO.mkRef { cmdState with messages := .empty }
-      /-
-      The same snapshot may be executed by different tasks. So, to make sure `elabCommandTopLevel`
-      has exclusive access to the cache, we create a fresh reference here. Before this change, the
-      following `tacticCache.modify` would reset the tactic post cache while another snapshot was
-      still using it.
-      -/
-      let tacticCacheNew ← IO.mkRef (← tacticCache.get)
-      let cmdCtx : Elab.Command.Context := { ctx with
-        cmdPos       := beginPos
-        tacticCache? := some tacticCacheNew
-        snap?        := some snap
-        cancelTk?    := some ctx.newCancelTk
-      }
-      let (output, _) ←
-        IO.FS.withIsolatedStreams (isolateStderr := stderrAsMessages.get scope.opts) do
-          liftM (m := BaseIO) do
-            withLoggingExceptions
-              (getResetInfoTrees *> Elab.Command.elabCommandTopLevel stx)
-              cmdCtx cmdStateRef
-      let postNew := (← tacticCacheNew.get).post
-      tacticCache.modify fun _ => { pre := postNew, post := {} }
-      let cmdState ← cmdStateRef.get
-      let mut messages := cmdState.messages
-      if !output.isEmpty then
-        messages := messages.add {
-          fileName := ctx.fileName
-          severity := MessageSeverity.information
-          pos      := ctx.fileMap.toPosition beginPos
-          data     := output
-        }
-      let cmdState := { cmdState with messages }
-      -- definitely resolve eventually
-      snap.new.resolve <| .ofTyped { diagnostics := .empty : SnapshotLeaf }
-      return {
-        diagnostics := (← Snapshot.Diagnostics.ofMessageLog cmdState.messages)
-        infoTree? := some cmdState.infoState.trees[0]!
-        cmdState
+    let scope := cmdState.scopes.head!
+    let cmdStateRef ← IO.mkRef { cmdState with messages := .empty }
+    /-
+    The same snapshot may be executed by different tasks. So, to make sure `elabCommandTopLevel`
+    has exclusive access to the cache, we create a fresh reference here. Before this change, the
+    following `tacticCache.modify` would reset the tactic post cache while another snapshot was
+    still using it.
+    -/
+    let tacticCacheNew ← IO.mkRef (← tacticCache.get)
+    let cmdCtx : Elab.Command.Context := { ctx with
+      cmdPos       := beginPos
+      tacticCache? := some tacticCacheNew
+      snap?        := if internal.minimalSnapshots.get scope.opts then none else snap
+      cancelTk?    := some ctx.newCancelTk
+    }
+    let (output, _) ←
+      IO.FS.withIsolatedStreams (isolateStderr := stderrAsMessages.get scope.opts) do
+        liftM (m := BaseIO) do
+          withLoggingExceptions
+            (getResetInfoTrees *> Elab.Command.elabCommandTopLevel stx)
+            cmdCtx cmdStateRef
+    let postNew := (← tacticCacheNew.get).post
+    tacticCache.modify fun _ => { pre := postNew, post := {} }
+    let cmdState ← cmdStateRef.get
+    let mut messages := cmdState.messages
+    if !output.isEmpty then
+      messages := messages.add {
+        fileName := ctx.fileName
+        severity := MessageSeverity.information
+        pos      := ctx.fileMap.toPosition beginPos
+        data     := output
      }
+    let cmdState := { cmdState with messages }
+    -- definitely resolve eventually
+    snap.new.resolve <| .ofTyped { diagnostics := .empty : SnapshotLeaf }
+    return {
+      diagnostics := (← Snapshot.Diagnostics.ofMessageLog cmdState.messages)
+      infoTree? := some cmdState.infoState.trees[0]!
+      cmdState
+    }

 /--
 Convenience function for tool uses of the language processor that skips header handling.
@@ -520,14 +612,15 @@ Convenience function for tool uses of the language processor that skips header h
 def processCommands (inputCtx : Parser.InputContext) (parserState : Parser.ModuleParserState)
    (commandState : Command.State)
    (old? : Option (Parser.InputContext × CommandParsedSnapshot) := none) :
-    BaseIO (SnapshotTask CommandParsedSnapshot) := do
-  process.parseCmd (old?.map (·.2)) parserState commandState
+    BaseIO (Task CommandParsedSnapshot) := do
+  let prom ← IO.Promise.new
+  process.parseCmd (old?.map (·.2)) parserState commandState commandState.env prom
    |>.run (old?.map (·.1))
    |>.run { inputCtx with }
+  return prom.result

-
-/-- Waits for and returns final environment, if importing was successful. -/
-partial def waitForFinalEnv? (snap : InitialSnapshot) : Option Environment := do
+/-- Waits for and returns final command state, if importing was successful. -/
+partial def waitForFinalCmdState? (snap : InitialSnapshot) : Option Command.State := do
  let snap ← snap.result?
  let snap ← snap.processedSnap.get.result?
  goCmd snap.firstCmdSnap.get
@@ -535,6 +628,6 @@ where goCmd snap :=
  if let some next := snap.nextCmdSnap? then
    goCmd next.get
  else
-    snap.data.finishedSnap.get.cmdState.env
+    snap.data.finishedSnap.get.cmdState

 end Lean
--- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean
+++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean
@@ -60,6 +60,16 @@ builtin_dsimproc [simp, seval] reducePow ((_ ^ _ : Nat)) := fun e => do
  unless (← checkExponent m) do return .continue
  return .done <| toExpr (n ^ m)

+builtin_dsimproc [simp, seval] reduceAnd ((_ &&& _ : Nat)) := reduceBin ``HOr.hOr 6 (· &&& ·)
+builtin_dsimproc [simp, seval] reduceXor ((_ ^^^ _ : Nat)) := reduceBin ``HXor.hXor 6 (· ^^^ ·)
+builtin_dsimproc [simp, seval] reduceOr ((_ ||| _ : Nat)) := reduceBin ``HOr.hOr 6 (· ||| ·)
+
+builtin_dsimproc [simp, seval] reduceShiftLeft ((_ <<< _ : Nat)) :=
+  reduceBin ``HShiftLeft.hShiftLeft 6 (· <<< ·)
+
+builtin_dsimproc [simp, seval] reduceShiftRight ((_ >>> _ : Nat)) :=
+  reduceBin ``HShiftRight.hShiftRight 6 (· >>> ·)
+
 builtin_dsimproc [simp, seval] reduceGcd (gcd _ _)       := reduceBin ``gcd 2 gcd

 builtin_simproc [simp, seval] reduceLT  (( _ : Nat) < _)  := reduceBinPred ``LT.lt 4 (. < .)
--- a/src/Lean/MetavarContext.lean
+++ b/src/Lean/MetavarContext.lean
@@ -336,6 +336,8 @@ structure MetavarContext where
  For more information about delayed abstraction, see the docstring for `DelayedMetavarAssignment`. -/
  dAssignment    : PersistentHashMap MVarId DelayedMetavarAssignment := {}

+instance : Inhabited MetavarContext := ⟨{}⟩
+
 /-- A monad with a stateful metavariable context, defining `getMCtx` and `modifyMCtx`. -/
 class MonadMCtx (m : Type → Type) where
  getMCtx    : m MetavarContext
@@ -358,15 +360,27 @@ abbrev setMCtx [MonadMCtx m] (mctx : MetavarContext) : m Unit :=
 abbrev getLevelMVarAssignment? [Monad m] [MonadMCtx m] (mvarId : LMVarId) : m (Option Level) :=
  return (← getMCtx).lAssignment.find? mvarId

+@[export lean_get_lmvar_assignment]
+def getLevelMVarAssignmentExp (m : MetavarContext) (mvarId : LMVarId) : Option Level :=
+  m.lAssignment.find? mvarId
+
 def MetavarContext.getExprAssignmentCore? (m : MetavarContext) (mvarId : MVarId) : Option Expr :=
  m.eAssignment.find? mvarId

+@[export lean_get_mvar_assignment]
+def MetavarContext.getExprAssignmentExp (m : MetavarContext) (mvarId : MVarId) : Option Expr :=
+  m.eAssignment.find? mvarId
+
 def getExprMVarAssignment? [Monad m] [MonadMCtx m] (mvarId : MVarId) : m (Option Expr) :=
  return (← getMCtx).getExprAssignmentCore? mvarId

 def MetavarContext.getDelayedMVarAssignmentCore? (mctx : MetavarContext) (mvarId : MVarId) : Option DelayedMetavarAssignment :=
  mctx.dAssignment.find? mvarId

+@[export lean_get_delayed_mvar_assignment]
+def MetavarContext.getDelayedMVarAssignmentExp (mctx : MetavarContext) (mvarId : MVarId) : Option DelayedMetavarAssignment :=
+  mctx.dAssignment.find? mvarId
+
 def getDelayedMVarAssignment? [Monad m] [MonadMCtx m] (mvarId : MVarId) : m (Option DelayedMetavarAssignment) :=
  return (← getMCtx).getDelayedMVarAssignmentCore? mvarId

@@ -478,6 +492,10 @@ def hasAssignableMVar [Monad m] [MonadMCtx m] : Expr → m Bool
 def assignLevelMVar [MonadMCtx m] (mvarId : LMVarId) (val : Level) : m Unit :=
  modifyMCtx fun m => { m with lAssignment := m.lAssignment.insert mvarId val }

+@[export lean_assign_lmvar]
+def assignLevelMVarExp (m : MetavarContext) (mvarId : LMVarId) (val : Level) : MetavarContext :=
+  { m with lAssignment := m.lAssignment.insert mvarId val }
+
 /--
 Add `mvarId := x` to the metavariable assignment.
 This method does not check whether `mvarId` is already assigned, nor it checks whether
@@ -487,6 +505,10 @@ This is a low-level API, and it is safer to use `isDefEq (mkMVar mvarId) x`.
 def _root_.Lean.MVarId.assign [MonadMCtx m] (mvarId : MVarId) (val : Expr) : m Unit :=
  modifyMCtx fun m => { m with eAssignment := m.eAssignment.insert mvarId val }

+@[export lean_assign_mvar]
+def assignExp (m : MetavarContext) (mvarId : MVarId) (val : Expr) : MetavarContext :=
+  { m with eAssignment := m.eAssignment.insert mvarId val }
+
 /--
 Add a delayed assignment for the given metavariable. You must make sure that
 the metavariable is not already assigned or delayed-assigned.
@@ -516,95 +538,22 @@ To avoid this term eta-expanded term, we apply beta-reduction when instantiating
 This operation is performed at `instantiateExprMVars`, `elimMVarDeps`, and `levelMVarToParam`.
 -/

-partial def instantiateLevelMVars [Monad m] [MonadMCtx m] : Level → m Level
-  | lvl@(Level.succ lvl₁)      => return Level.updateSucc! lvl (← instantiateLevelMVars lvl₁)
-  | lvl@(Level.max lvl₁ lvl₂)  => return Level.updateMax! lvl (← instantiateLevelMVars lvl₁) (← instantiateLevelMVars lvl₂)
-  | lvl@(Level.imax lvl₁ lvl₂) => return Level.updateIMax! lvl (← instantiateLevelMVars lvl₁) (← instantiateLevelMVars lvl₂)
-  | lvl@(Level.mvar mvarId)    => do
-    match (← getLevelMVarAssignment? mvarId) with
-    | some newLvl =>
-      if !newLvl.hasMVar then pure newLvl
-      else do
-        let newLvl' ← instantiateLevelMVars newLvl
-        assignLevelMVar mvarId newLvl'
-        pure newLvl'
-    | none        => pure lvl
-  | lvl => pure lvl
+@[extern "lean_instantiate_level_mvars"]
+opaque instantiateLevelMVarsImp (mctx : MetavarContext) (l : Level) : MetavarContext × Level
+
+partial def instantiateLevelMVars [Monad m] [MonadMCtx m] (l : Level) : m Level := do
+  let (mctx, lNew) := instantiateLevelMVarsImp (← getMCtx) l
+  setMCtx mctx
+  return lNew
+
+@[extern "lean_instantiate_expr_mvars"]
+opaque instantiateExprMVarsImp (mctx : MetavarContext) (e : Expr) : MetavarContext × Expr

 /-- instantiateExprMVars main function -/
-partial def instantiateExprMVars [Monad m] [MonadMCtx m] [STWorld ω m] [MonadLiftT (ST ω) m] (e : Expr) : MonadCacheT ExprStructEq Expr m Expr :=
-  if !e.hasMVar then
-    pure e
-  else checkCache { val := e : ExprStructEq } fun _ => do match e with
-    | .proj _ _ s      => return e.updateProj! (← instantiateExprMVars s)
-    | .forallE _ d b _ => return e.updateForallE! (← instantiateExprMVars d) (← instantiateExprMVars b)
-    | .lam _ d b _     => return e.updateLambdaE! (← instantiateExprMVars d) (← instantiateExprMVars b)
-    | .letE _ t v b _  => return e.updateLet! (← instantiateExprMVars t) (← instantiateExprMVars v) (← instantiateExprMVars b)
-    | .const _ lvls    => return e.updateConst! (← lvls.mapM instantiateLevelMVars)
-    | .sort lvl        => return e.updateSort! (← instantiateLevelMVars lvl)
-    | .mdata _ b       => return e.updateMData! (← instantiateExprMVars b)
-    | .app ..          => e.withApp fun f args => do
-      let instArgs (f : Expr) : MonadCacheT ExprStructEq Expr m Expr := do
-        let args ← args.mapM instantiateExprMVars
-        pure (mkAppN f args)
-      let instApp : MonadCacheT ExprStructEq Expr m Expr := do
-        let wasMVar := f.isMVar
-        let f ← instantiateExprMVars f
-        if wasMVar && f.isLambda then
-          /- Some of the arguments in `args` are irrelevant after we beta
-             reduce. Also, it may be a bug to not instantiate them, since they
-             may depend on free variables that are not in the context (see
-             issue #4375). So we pass `useZeta := true` to ensure that they are
-             instantiated. -/
-          instantiateExprMVars (f.betaRev args.reverse (useZeta := true))
-        else
-          instArgs f
-      match f with
-      | .mvar mvarId =>
-        match (← getDelayedMVarAssignment? mvarId) with
-        | none => instApp
-        | some { fvars, mvarIdPending } =>
-          /-
-             Apply "delayed substitution" (i.e., delayed assignment + application).
-             That is, `f` is some metavariable `?m`, that is delayed assigned to `val`.
-             If after instantiating `val`, we obtain `newVal`, and `newVal` does not contain
-             metavariables, we replace the free variables `fvars` in `newVal` with the first
-             `fvars.size` elements of `args`. -/
-          if fvars.size > args.size then
-            /- We don't have sufficient arguments for instantiating the free variables `fvars`.
-               This can only happen if a tactic or elaboration function is not implemented correctly.
-               We decided to not use `panic!` here and report it as an error in the frontend
-               when we are checking for unassigned metavariables in an elaborated term. -/
-            instArgs f
-          else
-            let newVal ← instantiateExprMVars (mkMVar mvarIdPending)
-            if newVal.hasExprMVar then
-              instArgs f
-            else do
-              let args ← args.mapM instantiateExprMVars
-              /-
-                 Example: suppose we have
-                   `?m t1 t2 t3`
-                 That is, `f := ?m` and `args := #[t1, t2, t3]`
-                 Moreover, `?m` is delayed assigned
-                   `?m #[x, y] := f x y`
-                 where, `fvars := #[x, y]` and `newVal := f x y`.
-                 After abstracting `newVal`, we have `f (Expr.bvar 0) (Expr.bvar 1)`.
-                 After `instantiaterRevRange 0 2 args`, we have `f t1 t2`.
-                 After `mkAppRange 2 3`, we have `f t1 t2 t3` -/
-              let newVal := newVal.abstract fvars
-              let result := newVal.instantiateRevRange 0 fvars.size args
-              let result := mkAppRange result fvars.size args.size args
-              pure result
-      | _ => instApp
-    | e@(.mvar mvarId) => checkCache { val := e : ExprStructEq } fun _ => do
-      match (← getExprMVarAssignment? mvarId) with
-      | some newE => do
-        let newE' ← instantiateExprMVars newE
-        mvarId.assign newE'
-        pure newE'
-      | none => pure e
-    | e => pure e
+def instantiateExprMVars [Monad m] [MonadMCtx m] (e : Expr) : m Expr := do
+  let (mctx, eNew) := instantiateExprMVarsImp (← getMCtx) e
+  setMCtx mctx
+  return eNew

 instance : MonadMCtx (StateRefT MetavarContext (ST ω)) where
  getMCtx    := get
@@ -792,8 +741,6 @@ def localDeclDependsOnPred [Monad m] [MonadMCtx m] (localDecl : LocalDecl) (pf :

 namespace MetavarContext

-instance : Inhabited MetavarContext := ⟨{}⟩
-
@[export lean_mk_metavar_ctx]
 def mkMetavarContext : Unit → MetavarContext := fun _ => {}

--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -703,6 +703,9 @@ list, so it should be brief.
@[builtin_command_parser] def genInjectiveTheorems := leading_parser
  "gen_injective_theorems% " >> ident

+/-- To be implemented. -/
+@[builtin_command_parser] def «include» := leading_parser "include " >> many1 (checkColGt >> ident)
+
 /-- No-op parser used as syntax kind for attaching remaining whitespace at the end of the input. -/
@[run_builtin_parser_attribute_hooks] def eoi : Parser := leading_parser ""

--- a/src/Lean/Util.lean
+++ b/src/Lean/Util.lean
@@ -32,3 +32,4 @@ import Lean.Util.Heartbeats
 import Lean.Util.SearchPath
 import Lean.Util.SafeExponentiation
 import Lean.Util.NumObjs
+import Lean.Util.NumApps
--- a/src/Lean/Util/NumApps.lean
+++ b/src/Lean/Util/NumApps.lean
@@ -0,0 +1,57 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Expr
+import Lean.Util.PtrSet
+
+namespace Lean.Expr
+namespace NumApps
+
+unsafe structure State where
+ visited  : PtrSet Expr := mkPtrSet
+ counters : NameMap Nat := {}
+
+unsafe abbrev M := StateM State
+
+unsafe def visit (e : Expr) : M Unit :=
+  unless (← get).visited.contains e do
+    modify fun s => { s with visited := s.visited.insert e }
+    match e with
+      | .forallE _ d b _ => visit d; visit b
+      | .lam _ d b _     => visit d; visit b
+      | .mdata _ b       => visit b
+      | .letE _ t v b _  => visit t; visit v; visit b
+      | .app ..          => e.withApp fun f args => do
+        if let .const declName _ := f then
+          let c := (← get).counters.find? declName |>.getD 0
+          modify fun s => { s with counters := s.counters.insert declName (c+1) }
+        visit f
+        args.forM visit
+      | .proj _ _ b      => visit b
+      | _                => return ()
+
+unsafe def main (e : Expr) : NameMap Nat :=
+  let (_, s) := NumApps.visit e |>.run {}
+  s.counters
+
+end NumApps
+
+/--
+Returns the number of applications for each declaration used in `e`.
+
+This operation is performed in `IO` because the result depends on the memory representation of the object.
+
+Note: Use this function primarily for diagnosing performance issues.
+-/
+def numApps (e : Expr) (threshold : Nat := 0) : IO (Array (Name × Nat)) := do
+  let counters := unsafe NumApps.main e
+  let mut result := #[]
+  for (declName, num) in counters do
+    if num > threshold then
+      result := result.push (declName, num)
+  return result.qsort fun a b => a.2 > b.2
+
+end Lean.Expr
--- a/src/kernel/CMakeLists.txt
+++ b/src/kernel/CMakeLists.txt
@@ -2,4 +2,4 @@ add_library(kernel OBJECT level.cpp expr.cpp expr_eq_fn.cpp
 for_each_fn.cpp replace_fn.cpp abstract.cpp instantiate.cpp
 local_ctx.cpp declaration.cpp environment.cpp type_checker.cpp
 init_module.cpp expr_cache.cpp equiv_manager.cpp quot.cpp
-inductive.cpp trace.cpp)
+inductive.cpp trace.cpp instantiate_mvars.cpp)
--- a/src/kernel/declaration.h
+++ b/src/kernel/declaration.h
@@ -63,9 +63,9 @@ class constant_val : public object_ref {
 public:
    constant_val(name const & n, names const & lparams, expr const & type);
    constant_val(constant_val const & other):object_ref(other) {}
-    constant_val(constant_val && other):object_ref(other) {}
+    constant_val(constant_val && other):object_ref(std::move(other)) {}
    constant_val & operator=(constant_val const & other) { object_ref::operator=(other); return *this; }
-    constant_val & operator=(constant_val && other) { object_ref::operator=(other); return *this; }
+    constant_val & operator=(constant_val && other) { object_ref::operator=(std::move(other)); return *this; }
    name const & get_name() const { return static_cast<name const &>(cnstr_get_ref(*this, 0)); }
    names const & get_lparams() const { return static_cast<names const &>(cnstr_get_ref(*this, 1)); }
    expr const & get_type() const { return static_cast<expr const &>(cnstr_get_ref(*this, 2)); }
@@ -79,9 +79,9 @@ class axiom_val : public object_ref {
 public:
    axiom_val(name const & n, names const & lparams, expr const & type, bool is_unsafe);
    axiom_val(axiom_val const & other):object_ref(other) {}
-    axiom_val(axiom_val && other):object_ref(other) {}
+    axiom_val(axiom_val && other):object_ref(std::move(other)) {}
    axiom_val & operator=(axiom_val const & other) { object_ref::operator=(other); return *this; }
-    axiom_val & operator=(axiom_val && other) { object_ref::operator=(other); return *this; }
+    axiom_val & operator=(axiom_val && other) { object_ref::operator=(std::move(other)); return *this; }
    constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_get_ref(*this, 0)); }
    name const & get_name() const { return to_constant_val().get_name(); }
    names const & get_lparams() const { return to_constant_val().get_lparams(); }
@@ -105,9 +105,9 @@ class definition_val : public object_ref {
 public:
    definition_val(name const & n, names const & lparams, expr const & type, expr const & val, reducibility_hints const & hints, definition_safety safety, names const & all);
    definition_val(definition_val const & other):object_ref(other) {}
-    definition_val(definition_val && other):object_ref(other) {}
+    definition_val(definition_val && other):object_ref(std::move(other)) {}
    definition_val & operator=(definition_val const & other) { object_ref::operator=(other); return *this; }
-    definition_val & operator=(definition_val && other) { object_ref::operator=(other); return *this; }
+    definition_val & operator=(definition_val && other) { object_ref::operator=(std::move(other)); return *this; }
    constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_get_ref(*this, 0)); }
    name const & get_name() const { return to_constant_val().get_name(); }
    names const & get_lparams() const { return to_constant_val().get_lparams(); }
@@ -128,9 +128,9 @@ class theorem_val : public object_ref {
 public:
    theorem_val(name const & n, names const & lparams, expr const & type, expr const & val, names const & all);
    theorem_val(theorem_val const & other):object_ref(other) {}
-    theorem_val(theorem_val && other):object_ref(other) {}
+    theorem_val(theorem_val && other):object_ref(std::move(other)) {}
    theorem_val & operator=(theorem_val const & other) { object_ref::operator=(other); return *this; }
-    theorem_val & operator=(theorem_val && other) { object_ref::operator=(other); return *this; }
+    theorem_val & operator=(theorem_val && other) { object_ref::operator=(std::move(other)); return *this; }
    constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_get_ref(*this, 0)); }
    name const & get_name() const { return to_constant_val().get_name(); }
    names const & get_lparams() const { return to_constant_val().get_lparams(); }
@@ -148,9 +148,9 @@ class opaque_val : public object_ref {
 public:
    opaque_val(name const & n, names const & lparams, expr const & type, expr const & val, bool is_unsafe, names const & all);
    opaque_val(opaque_val const & other):object_ref(other) {}
-    opaque_val(opaque_val && other):object_ref(other) {}
+    opaque_val(opaque_val && other):object_ref(std::move(other)) {}
    opaque_val & operator=(opaque_val const & other) { object_ref::operator=(other); return *this; }
-    opaque_val & operator=(opaque_val && other) { object_ref::operator=(other); return *this; }
+    opaque_val & operator=(opaque_val && other) { object_ref::operator=(std::move(other)); return *this; }
    constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_get_ref(*this, 0)); }
    name const & get_name() const { return to_constant_val().get_name(); }
    names const & get_lparams() const { return to_constant_val().get_lparams(); }
@@ -179,9 +179,9 @@ class inductive_type : public object_ref {
 public:
    inductive_type(name const & id, expr const & type, constructors const & cnstrs);
    inductive_type(inductive_type const & other):object_ref(other) {}
-    inductive_type(inductive_type && other):object_ref(other) {}
+    inductive_type(inductive_type && other):object_ref(std::move(other)) {}
    inductive_type & operator=(inductive_type const & other) { object_ref::operator=(other); return *this; }
-    inductive_type & operator=(inductive_type && other) { object_ref::operator=(other); return *this; }
+    inductive_type & operator=(inductive_type && other) { object_ref::operator=(std::move(other)); return *this; }
    name const & get_name() const { return static_cast<name const &>(cnstr_get_ref(*this, 0)); }
    expr const & get_type() const { return static_cast<expr const &>(cnstr_get_ref(*this, 1)); }
    constructors const & get_cnstrs() const { return static_cast<constructors const &>(cnstr_get_ref(*this, 2)); }
@@ -205,7 +205,7 @@ class declaration : public object_ref {
 public:
    declaration();
    declaration(declaration const & other):object_ref(other) {}
-    declaration(declaration && other):object_ref(other) {}
+    declaration(declaration && other):object_ref(std::move(other)) {}
    /* low-level constructors */
    explicit declaration(object * o):object_ref(o) {}
    explicit declaration(b_obj_arg o, bool b):object_ref(o, b) {}
@@ -213,7 +213,7 @@ public:
    declaration_kind kind() const { return static_cast<declaration_kind>(obj_tag(raw())); }

    declaration & operator=(declaration const & other) { object_ref::operator=(other); return *this; }
-    declaration & operator=(declaration && other) { object_ref::operator=(other); return *this; }
+    declaration & operator=(declaration && other) { object_ref::operator=(std::move(other)); return *this; }

    friend bool is_eqp(declaration const & d1, declaration const & d2) { return d1.raw() == d2.raw(); }

@@ -263,10 +263,10 @@ declaration mk_axiom_inferring_unsafe(environment const & env, name const & n,
 class inductive_decl : public object_ref {
 public:
    inductive_decl(inductive_decl const & other):object_ref(other) {}
-    inductive_decl(inductive_decl && other):object_ref(other) {}
+    inductive_decl(inductive_decl && other):object_ref(std::move(other)) {}
    inductive_decl(declaration const & d):object_ref(d) { lean_assert(d.is_inductive()); }
    inductive_decl & operator=(inductive_decl const & other) { object_ref::operator=(other); return *this; }
-    inductive_decl & operator=(inductive_decl && other) { object_ref::operator=(other); return *this; }
+    inductive_decl & operator=(inductive_decl && other) { object_ref::operator=(std::move(other)); return *this; }
    names const & get_lparams() const { return static_cast<names const &>(cnstr_get_ref(raw(), 0)); }
    nat const & get_nparams() const { return static_cast<nat const &>(cnstr_get_ref(raw(), 1)); }
    inductive_types const & get_types() const { return static_cast<inductive_types const &>(cnstr_get_ref(raw(), 2)); }
@@ -290,9 +290,9 @@ public:
    inductive_val(name const & n, names const & lparams, expr const & type, unsigned nparams,
                  unsigned nindices, names const & all, names const & cnstrs, unsigned nnested, bool is_rec, bool is_unsafe, bool is_reflexive);
    inductive_val(inductive_val const & other):object_ref(other) {}
-    inductive_val(inductive_val && other):object_ref(other) {}
+    inductive_val(inductive_val && other):object_ref(std::move(other)) {}
    inductive_val & operator=(inductive_val const & other) { object_ref::operator=(other); return *this; }
-    inductive_val & operator=(inductive_val && other) { object_ref::operator=(other); return *this; }
+    inductive_val & operator=(inductive_val && other) { object_ref::operator=(std::move(other)); return *this; }
    constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_get_ref(*this, 0)); }
    unsigned get_nparams() const { return static_cast<nat const &>(cnstr_get_ref(*this, 1)).get_small_value(); }
    unsigned get_nindices() const { return static_cast<nat const &>(cnstr_get_ref(*this, 2)).get_small_value(); }
@@ -317,9 +317,9 @@ class constructor_val : public object_ref {
 public:
    constructor_val(name const & n, names const & lparams, expr const & type, name const & induct, unsigned cidx, unsigned nparams, unsigned nfields, bool is_unsafe);
    constructor_val(constructor_val const & other):object_ref(other) {}
-    constructor_val(constructor_val && other):object_ref(other) {}
+    constructor_val(constructor_val && other):object_ref(std::move(other)) {}
    constructor_val & operator=(constructor_val const & other) { object_ref::operator=(other); return *this; }
-    constructor_val & operator=(constructor_val && other) { object_ref::operator=(other); return *this; }
+    constructor_val & operator=(constructor_val && other) { object_ref::operator=(std::move(other)); return *this; }
    constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_get_ref(*this, 0)); }
    name const & get_induct() const { return static_cast<name const &>(cnstr_get_ref(*this, 1)); }
    unsigned get_cidx() const { return static_cast<nat const &>(cnstr_get_ref(*this, 2)).get_small_value(); }
@@ -338,9 +338,9 @@ class recursor_rule : public object_ref {
 public:
    recursor_rule(name const & cnstr, unsigned nfields, expr const & rhs);
    recursor_rule(recursor_rule const & other):object_ref(other) {}
-    recursor_rule(recursor_rule && other):object_ref(other) {}
+    recursor_rule(recursor_rule && other):object_ref(std::move(other)) {}
    recursor_rule & operator=(recursor_rule const & other) { object_ref::operator=(other); return *this; }
-    recursor_rule & operator=(recursor_rule && other) { object_ref::operator=(other); return *this; }
+    recursor_rule & operator=(recursor_rule && other) { object_ref::operator=(std::move(other)); return *this; }
    name const & get_cnstr() const { return static_cast<name const &>(cnstr_get_ref(*this, 0)); }
    unsigned get_nfields() const { return static_cast<nat const &>(cnstr_get_ref(*this, 1)).get_small_value(); }
    expr const & get_rhs() const { return static_cast<expr const &>(cnstr_get_ref(*this, 2)); }
@@ -365,9 +365,9 @@ public:
                 names const & all, unsigned nparams, unsigned nindices, unsigned nmotives,
                 unsigned nminors, recursor_rules const & rules, bool k, bool is_unsafe);
    recursor_val(recursor_val const & other):object_ref(other) {}
-    recursor_val(recursor_val && other):object_ref(other) {}
+    recursor_val(recursor_val && other):object_ref(std::move(other)) {}
    recursor_val & operator=(recursor_val const & other) { object_ref::operator=(other); return *this; }
-    recursor_val & operator=(recursor_val && other) { object_ref::operator=(other); return *this; }
+    recursor_val & operator=(recursor_val && other) { object_ref::operator=(std::move(other)); return *this; }
    constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_get_ref(*this, 0)); }
    name const & get_name() const { return to_constant_val().get_name(); }
    name const & get_induct() const { return get_name().get_prefix(); }
@@ -398,9 +398,9 @@ class quot_val : public object_ref {
 public:
    quot_val(name const & n, names const & lparams, expr const & type, quot_kind k);
    quot_val(quot_val const & other):object_ref(other) {}
-    quot_val(quot_val && other):object_ref(other) {}
+    quot_val(quot_val && other):object_ref(std::move(other)) {}
    quot_val & operator=(quot_val const & other) { object_ref::operator=(other); return *this; }
-    quot_val & operator=(quot_val && other) { object_ref::operator=(other); return *this; }
+    quot_val & operator=(quot_val && other) { object_ref::operator=(std::move(other)); return *this; }
    constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_get_ref(*this, 0)); }
    name const & get_name() const { return to_constant_val().get_name(); }
    names const & get_lparams() const { return to_constant_val().get_lparams(); }
@@ -434,14 +434,14 @@ public:
    constant_info(constructor_val const & v);
    constant_info(recursor_val const & v);
    constant_info(constant_info const & other):object_ref(other) {}
-    constant_info(constant_info && other):object_ref(other) {}
+    constant_info(constant_info && other):object_ref(std::move(other)) {}
    explicit constant_info(b_obj_arg o, bool b):object_ref(o, b) {}
    explicit constant_info(obj_arg o):object_ref(o) {}

    constant_info_kind kind() const { return static_cast<constant_info_kind>(cnstr_tag(raw())); }

    constant_info & operator=(constant_info const & other) { object_ref::operator=(other); return *this; }
-    constant_info & operator=(constant_info && other) { object_ref::operator=(other); return *this; }
+    constant_info & operator=(constant_info && other) { object_ref::operator=(std::move(other)); return *this; }

    friend bool is_eqp(constant_info const & d1, constant_info const & d2) { return d1.raw() == d2.raw(); }

--- a/src/kernel/environment.cpp
+++ b/src/kernel/environment.cpp
@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include <limits>
 #include "runtime/sstream.h"
 #include "runtime/thread.h"
+#include "runtime/sharecommon.h"
 #include "util/map_foreach.h"
 #include "util/io.h"
 #include "kernel/environment.h"
@@ -220,12 +221,15 @@ environment environment::add_theorem(declaration const & d, bool check) const {
    theorem_val const & v = d.to_theorem_val();
    if (check) {
        type_checker checker(*this, diag.get());
-        if (!checker.is_prop(v.get_type()))
-            throw theorem_type_is_not_prop(*this, v.get_name(), v.get_type());
+        sharecommon_persistent_fn share;
+        expr val(share(v.get_value().raw()));
+        expr type(share(v.get_type().raw()));
+        if (!checker.is_prop(type))
+            throw theorem_type_is_not_prop(*this, v.get_name(), type);
        check_constant_val(*this, v.to_constant_val(), checker);
-        check_no_metavar_no_fvar(*this, v.get_name(), v.get_value());
-        expr val_type = checker.check(v.get_value(), v.get_lparams());
-        if (!checker.is_def_eq(val_type, v.get_type()))
+        check_no_metavar_no_fvar(*this, v.get_name(), val);
+        expr val_type = checker.check(val, v.get_lparams());
+        if (!checker.is_def_eq(val_type, type))
            throw definition_type_mismatch_exception(*this, d, val_type);
    }
    return diag.update(add(constant_info(d)));
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -50,9 +50,9 @@ public:
    explicit literal(nat const & v);
    literal():literal(0u) {}
    literal(literal const & other):object_ref(other) {}
-    literal(literal && other):object_ref(other) {}
+    literal(literal && other):object_ref(std::move(other)) {}
    literal & operator=(literal const & other) { object_ref::operator=(other); return *this; }
-    literal & operator=(literal && other) { object_ref::operator=(other); return *this; }
+    literal & operator=(literal && other) { object_ref::operator=(std::move(other)); return *this; }

    static literal_kind kind(object * o) { return static_cast<literal_kind>(cnstr_tag(o)); }
    literal_kind kind() const { return kind(raw()); }
@@ -100,14 +100,14 @@ class expr : public object_ref {
 public:
    expr();
    expr(expr const & other):object_ref(other) {}
-    expr(expr && other):object_ref(other) {}
+    expr(expr && other):object_ref(std::move(other)) {}
    explicit expr(b_obj_arg o, bool b):object_ref(o, b) {}
    explicit expr(obj_arg o):object_ref(o) {}
    static expr_kind kind(object * o) { return static_cast<expr_kind>(cnstr_tag(o)); }
    expr_kind kind() const { return kind(raw()); }

    expr & operator=(expr const & other) { object_ref::operator=(other); return *this; }
-    expr & operator=(expr && other) { object_ref::operator=(other); return *this; }
+    expr & operator=(expr && other) { object_ref::operator=(std::move(other)); return *this; }

    friend bool is_eqp(expr const & e1, expr const & e2) { return e1.raw() == e2.raw(); }
 };
--- a/src/kernel/expr_eq_fn.cpp
+++ b/src/kernel/expr_eq_fn.cpp
@@ -11,65 +11,49 @@ Author: Leonardo de Moura
 #include "kernel/expr.h"
 #include "kernel/expr_sets.h"

-#ifndef LEAN_EQ_CACHE_CAPACITY
-#define LEAN_EQ_CACHE_CAPACITY 1024*8
-#endif
-
 namespace lean {
-struct eq_cache {
-    struct entry {
-        object * m_a;
-        object * m_b;
-        entry():m_a(nullptr), m_b(nullptr) {}
-    };
-    unsigned              m_capacity;
-    std::vector<entry>    m_cache;
-    std::vector<unsigned> m_used;
-    eq_cache():m_capacity(LEAN_EQ_CACHE_CAPACITY), m_cache(LEAN_EQ_CACHE_CAPACITY) {}
+/**
+\brief Functional object for comparing expressions.

-    bool check(expr const & a, expr const & b) {
-        if (!is_shared(a) || !is_shared(b))
-            return false;
-        unsigned i = hash(hash(a), hash(b)) % m_capacity;
-        if (m_cache[i].m_a == a.raw() && m_cache[i].m_b == b.raw()) {
-            return true;
-        } else {
-            if (m_cache[i].m_a == nullptr)
-                m_used.push_back(i);
-            m_cache[i].m_a = a.raw();
-            m_cache[i].m_b = b.raw();
-            return false;
-        }
-    }
-
-    void clear() {
-        for (unsigned i : m_used)
-            m_cache[i].m_a = nullptr;
-        m_used.clear();
-    }
-};
-
-/* CACHE_RESET: No */
-MK_THREAD_LOCAL_GET_DEF(eq_cache, get_eq_cache);
-
-/** \brief Functional object for comparing expressions.
-
-    Remark if CompareBinderInfo is true, then functional object will also compare
-    binder information attached to lambda and Pi expressions */
+Remark if CompareBinderInfo is true, then functional object will also compare
+binder information attached to lambda and Pi expressions
+*/
 template<bool CompareBinderInfo>
 class expr_eq_fn {
-    eq_cache & m_cache;
-
+    struct key_hasher {
+        std::size_t operator()(std::pair<lean_object *, lean_object *> const & p) const {
+            return hash((size_t)p.first >> 3, (size_t)p.first >> 3);
+        }
+    };
+    typedef std::unordered_set<std::pair<lean_object *, lean_object *>, key_hasher> cache;
+    cache * m_cache = nullptr;
+    bool check_cache(expr const & a, expr const & b) {
+        if (!is_shared(a) || !is_shared(b))
+            return false;
+        if (!m_cache)
+            m_cache = new cache();
+        std::pair<lean_object *, lean_object *> key(a.raw(), b.raw());
+        if (m_cache->find(key) != m_cache->end())
+            return true;
+        m_cache->insert(key);
+        return false;
+    }
    static void check_system() {
        ::lean::check_system("expression equality test");
    }
-
-    bool apply(expr const & a, expr const & b) {
+    bool apply(expr const & a, expr const & b, bool root = false) {
        if (is_eqp(a, b))          return true;
        if (hash(a) != hash(b))    return false;
        if (a.kind() != b.kind())  return false;
-        if (is_bvar(a))            return bvar_idx(a) == bvar_idx(b);
-        if (m_cache.check(a, b))
+        switch (a.kind()) {
+        case expr_kind::BVar: return bvar_idx(a) == bvar_idx(b);
+        case expr_kind::Lit:  return lit_value(a) == lit_value(b);
+        case expr_kind::MVar: return mvar_name(a) == mvar_name(b);
+        case expr_kind::FVar: return fvar_name(a) == fvar_name(b);
+        case expr_kind::Sort: return sort_level(a) == sort_level(b);
+        default: break;
+        }
+        if (!root && check_cache(a, b))
            return true;
        /*
           We increase the number of heartbeats here because some code (e.g., `simp`) may spend a lot of time comparing
@@ -78,6 +62,10 @@ class expr_eq_fn {
        lean_inc_heartbeat();
        switch (a.kind()) {
        case expr_kind::BVar:
+        case expr_kind::Lit:
+        case expr_kind::MVar:
+        case expr_kind::FVar:
+        case expr_kind::Sort:
            lean_unreachable(); // LCOV_EXCL_LINE
        case expr_kind::MData:
            return
@@ -88,16 +76,10 @@ class expr_eq_fn {
                apply(proj_expr(a), proj_expr(b)) &&
                proj_sname(a) == proj_sname(b) &&
                proj_idx(a) == proj_idx(b);
-        case expr_kind::Lit:
-            return lit_value(a) == lit_value(b);
        case expr_kind::Const:
            return
                const_name(a) == const_name(b) &&
                compare(const_levels(a), const_levels(b), [](level const & l1, level const & l2) { return l1 == l2; });
-        case expr_kind::MVar:
-            return mvar_name(a) == mvar_name(b);
-        case expr_kind::FVar:
-            return fvar_name(a) == fvar_name(b);
        case expr_kind::App:
            check_system();
            return
@@ -117,15 +99,13 @@ class expr_eq_fn {
                apply(let_value(a), let_value(b)) &&
                apply(let_body(a), let_body(b)) &&
                (!CompareBinderInfo || let_name(a) == let_name(b));
-        case expr_kind::Sort:
-            return sort_level(a) == sort_level(b);
        }
        lean_unreachable(); // LCOV_EXCL_LINE
    }
 public:
-    expr_eq_fn():m_cache(get_eq_cache()) {}
-    ~expr_eq_fn() { m_cache.clear(); }
-    bool operator()(expr const & a, expr const & b) { return apply(a, b); }
+    expr_eq_fn() {}
+    ~expr_eq_fn() { if (m_cache) delete m_cache; }
+    bool operator()(expr const & a, expr const & b) { return apply(a, b, true); }
 };

 bool is_equal(expr const & a, expr const & b) {
--- a/src/kernel/instantiate.cpp
+++ b/src/kernel/instantiate.cpp
@@ -165,22 +165,38 @@ bool is_head_beta(expr const & t) {
    return is_app(t) && is_lambda(get_app_fn(t));
 }

-expr apply_beta(expr f, unsigned num_args, expr const * args) {
-    if (num_args == 0) {
-        return f;
-    } else if (!is_lambda(f)) {
-        return mk_rev_app(f, num_args, args);
-    } else {
-        unsigned m = 1;
-        while (is_lambda(binding_body(f)) && m < num_args) {
-            f = binding_body(f);
-            m++;
+static expr apply_beta_rec(expr e, unsigned i, unsigned num_rev_args, expr const * rev_args, bool preserve_data, bool zeta) {
+    if (is_lambda(e)) {
+        if (i + 1 < num_rev_args) {
+            return apply_beta_rec(binding_body(e), i+1, num_rev_args, rev_args, preserve_data, zeta);
+        } else {
+            return instantiate(binding_body(e), num_rev_args, rev_args);
        }
-        lean_assert(m <= num_args);
-        return mk_rev_app(instantiate(binding_body(f), m, args + (num_args - m)), num_args - m, args);
+    } else if (is_let(e)) {
+        if (zeta && i < num_rev_args) {
+            return apply_beta_rec(instantiate(let_body(e), let_value(e)), i, num_rev_args, rev_args, preserve_data, zeta);
+        } else {
+            unsigned n = num_rev_args - i;
+            return mk_rev_app(instantiate(e, i, rev_args + n), n, rev_args);
+        }
+    } else if (is_mdata(e)) {
+        if (preserve_data) {
+            unsigned n = num_rev_args - i;
+            return mk_rev_app(instantiate(e, i, rev_args + n), n, rev_args);
+        } else {
+            return apply_beta_rec(mdata_expr(e), i, num_rev_args, rev_args, preserve_data, zeta);
+        }
+    } else {
+        unsigned n = num_rev_args - i;
+        return mk_rev_app(instantiate(e, i, rev_args + n), n, rev_args);
    }
 }

+expr apply_beta(expr f, unsigned num_rev_args, expr const * rev_args, bool preserve_data, bool zeta) {
+    if (num_rev_args == 0) return f;
+    return apply_beta_rec(f, 0, num_rev_args, rev_args, preserve_data, zeta);
+}
+
 expr head_beta_reduce(expr const & t) {
    if (!is_head_beta(t)) {
        return t;
--- a/src/kernel/instantiate.h
+++ b/src/kernel/instantiate.h
@@ -24,7 +24,7 @@ inline expr instantiate_rev(expr const & e, buffer<expr> const & s) {
    return instantiate_rev(e, s.size(), s.data());
 }

-expr apply_beta(expr f, unsigned num_rev_args, expr const * rev_args);
+expr apply_beta(expr f, unsigned num_rev_args, expr const * rev_args, bool preserve_data = true, bool zeta = false);
 bool is_head_beta(expr const & t);
 expr head_beta_reduce(expr const & t);
 /* If `e` is of the form `(fun x, t) a` return `head_beta_const_fn(t)` if `t` does not depend on `x`,
--- a/src/kernel/instantiate_mvars.cpp
+++ b/src/kernel/instantiate_mvars.cpp
@@ -0,0 +1,369 @@
+/*
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Leonardo de Moura
+*/
+#include <vector>
+#include <unordered_map>
+#include "util/name_set.h"
+#include "runtime/option_ref.h"
+#include "runtime/array_ref.h"
+#include "kernel/instantiate.h"
+#include "kernel/replace_fn.h"
+
+/*
+This module is not used by the kernel. It just provides an efficient implementation of
+`instantiateExprMVars`
+*/
+
+namespace lean {
+extern "C" object * lean_get_lmvar_assignment(obj_arg mctx, obj_arg mid);
+extern "C" object * lean_assign_lmvar(obj_arg mctx, obj_arg mid, obj_arg val);
+
+typedef object_ref metavar_ctx;
+void assign_lmvar(metavar_ctx & mctx, name const & mid, level const & l) {
+    object * r = lean_assign_lmvar(mctx.steal(), mid.to_obj_arg(), l.to_obj_arg());
+    mctx.set_box(r);
+}
+
+option_ref<level> get_lmvar_assignment(metavar_ctx & mctx, name const & mid) {
+    return option_ref<level>(lean_get_lmvar_assignment(mctx.to_obj_arg(), mid.to_obj_arg()));
+}
+
+class instantiate_lmvars_fn {
+    metavar_ctx & m_mctx;
+    std::unordered_map<lean_object *, level> m_cache;
+    std::vector<level> m_saved; // Helper vector to prevent values from being garbagge collected
+
+    inline level cache(level const & l, level r, bool shared) {
+        if (shared) {
+            m_cache.insert(mk_pair(l.raw(), r));
+        }
+        return r;
+    }
+public:
+    instantiate_lmvars_fn(metavar_ctx & mctx):m_mctx(mctx) {}
+    level visit(level const & l) {
+        if (!has_mvar(l))
+            return l;
+        bool shared = false;
+        if (is_shared(l)) {
+            auto it = m_cache.find(l.raw());
+            if (it != m_cache.end()) {
+                return it->second;
+            }
+            shared = true;
+        }
+        switch (l.kind()) {
+        case level_kind::Succ:
+            return cache(l, update_succ(l, visit(succ_of(l))), shared);
+        case level_kind::Max: case level_kind::IMax:
+            return cache(l, update_max(l, visit(level_lhs(l)), visit(level_rhs(l))), shared);
+        case level_kind::Zero: case level_kind::Param:
+            lean_unreachable();
+        case level_kind::MVar: {
+            option_ref<level> r = get_lmvar_assignment(m_mctx, mvar_id(l));
+            if (!r) {
+                return l;
+            } else {
+                level a(r.get_val());
+                if (!has_mvar(a)) {
+                    return a;
+                } else {
+                    level a_new = visit(a);
+                    if (!is_eqp(a, a_new)) {
+                        /*
+                        We save `a` to ensure it will not be garbage collected
+                        after we update `mctx`. This is necessary because `m_cache`
+                        may contain references to its subterms.
+                        */
+                        m_saved.push_back(a);
+                        assign_lmvar(m_mctx, mvar_id(l), a_new);
+                    }
+                    return a_new;
+                }
+            }
+        }}
+    }
+    level operator()(level const & l) { return visit(l); }
+};
+
+extern "C" LEAN_EXPORT object * lean_instantiate_level_mvars(object * m, object * l) {
+    metavar_ctx mctx(m);
+    level l_new = instantiate_lmvars_fn(mctx)(level(l));
+    object * r = alloc_cnstr(0, 2, 0);
+    cnstr_set(r, 0, mctx.steal());
+    cnstr_set(r, 1, l_new.steal());
+    return r;
+}
+
+extern "C" object * lean_get_mvar_assignment(obj_arg mctx, obj_arg mid);
+extern "C" object * lean_get_delayed_mvar_assignment(obj_arg mctx, obj_arg mid);
+extern "C" object * lean_assign_mvar(obj_arg mctx, obj_arg mid, obj_arg val);
+typedef object_ref delayed_assignment;
+
+void assign_mvar(metavar_ctx & mctx, name const & mid, expr const & e) {
+    object * r = lean_assign_mvar(mctx.steal(), mid.to_obj_arg(), e.to_obj_arg());
+    mctx.set_box(r);
+}
+
+option_ref<expr> get_mvar_assignment(metavar_ctx & mctx, name const & mid) {
+    return option_ref<expr>(lean_get_mvar_assignment(mctx.to_obj_arg(), mid.to_obj_arg()));
+}
+
+option_ref<delayed_assignment> get_delayed_mvar_assignment(metavar_ctx & mctx, name const & mid) {
+    return option_ref<delayed_assignment>(lean_get_delayed_mvar_assignment(mctx.to_obj_arg(), mid.to_obj_arg()));
+}
+
+expr replace_fvars(expr const & e, array_ref<expr> const & fvars, expr const * rev_args) {
+    size_t sz = fvars.size();
+    if (sz == 0)
+        return e;
+    return replace(e, [=](expr const & m, unsigned offset) -> optional<expr> {
+            if (!has_fvar(m))
+                return some_expr(m); // expression m does not contain free variables
+            if (is_fvar(m)) {
+                size_t i = sz;
+                name const & fid = fvar_name(m);
+                while (i > 0) {
+                    --i;
+                    if (fvar_name(fvars[i]) == fid) {
+                        return some_expr(lift_loose_bvars(rev_args[sz - i - 1], offset));
+                    }
+                }
+            }
+            return none_expr();
+        });
+}
+
+class instantiate_mvars_fn {
+    metavar_ctx & m_mctx;
+    instantiate_lmvars_fn m_level_fn;
+    name_set m_already_normalized; // Store metavariables whose assignment has already been normalized.
+    std::unordered_map<lean_object *, expr> m_cache;
+    std::vector<expr> m_saved; // Helper vector to prevent values from being garbagge collected
+
+    level visit_level(level const & l) {
+        return m_level_fn(l);
+    }
+
+    levels visit_levels(levels const & ls) {
+        buffer<level> lsNew;
+        for (auto const & l : ls)
+            lsNew.push_back(visit_level(l));
+        return levels(lsNew);
+    }
+
+    inline expr cache(expr const & e, expr r, bool shared) {
+        if (shared) {
+            m_cache.insert(mk_pair(e.raw(), r));
+        }
+        return r;
+    }
+
+    optional<expr> get_assignment(name const & mid) {
+        option_ref<expr> r = get_mvar_assignment(m_mctx, mid);
+        if (!r) {
+            return optional<expr>();
+        } else {
+            expr a(r.get_val());
+            if (!has_mvar(a) || m_already_normalized.contains(mid)) {
+                return optional<expr>(a);
+            } else {
+                m_already_normalized.insert(mid);
+                expr a_new = visit(a);
+                if (!is_eqp(a, a_new)) {
+                    /*
+                    We save `a` to ensure it will not be garbage collected
+                    after we update `mctx`. This is necessary because `m_cache`
+                    may contain references to its subterms.
+                    */
+                    m_saved.push_back(a);
+                    assign_mvar(m_mctx, mid, a_new);
+                }
+                return optional<expr>(a_new);
+            }
+        }
+    }
+
+    /*
+    Given `e` of the form `f a_1 ... a_n` where `f` is not a metavariable,
+    instantiate metavariables.
+    */
+    expr visit_app_default(expr const & e) {
+        buffer<expr> args;
+        expr const * curr = &e;
+        while (is_app(*curr)) {
+            args.push_back(visit(app_arg(*curr)));
+            curr = &app_fn(*curr);
+        }
+        lean_assert(!is_mvar(*curr));
+        expr f = visit(*curr);
+        return mk_rev_app(f, args.size(), args.data());
+    }
+
+    /*
+    Given `e` of the form `?m a_1 ... a_n`, return new application where
+    the metavariables in the arguments `a_i` have been instantiated.
+    */
+    expr visit_mvar_app_args(expr const & e) {
+        buffer<expr> args;
+        expr const * curr = &e;
+        while (is_app(*curr)) {
+            args.push_back(visit(app_arg(*curr)));
+            curr = &app_fn(*curr);
+        }
+        lean_assert(is_mvar(*curr));
+        return mk_rev_app(*curr, args.size(), args.data());
+    }
+
+    /*
+    Given `e` of the form `f a_1 ... a_n`, return new application `f_new a_1' ... a_n'`
+    where `a_i'` is `visit(a_i)`. `args` is an accumulator for the new arguments.
+    */
+    expr visit_args_and_beta(expr const & f_new, expr const & e, buffer<expr> & args) {
+        expr const * curr = &e;
+        while (is_app(*curr)) {
+            args.push_back(visit(app_arg(*curr)));
+            curr = &app_fn(*curr);
+        }
+        /*
+          Some of the arguments in `args` are irrelevant after we beta
+          reduce. Also, it may be a bug to not instantiate them, since they
+          may depend on free variables that are not in the context (see
+          issue #4375). So we pass `useZeta := true` to ensure that they are
+          instantiated.
+        */
+        bool preserve_data = false;
+        bool zeta = true;
+        return apply_beta(f_new, args.size(), args.data(), preserve_data, zeta);
+    }
+
+    /*
+    Helper function for delayed assignment case at `visit_app`.
+    `e` is a term of the form `?m t1 t2 t3`
+    Moreover, `?m` is delayed assigned
+      `?m #[x, y] := g x y`
+    where, `fvars := #[x, y]` and `val := g x y`.
+    `args` is an accumulator for `e`'s arguments.
+
+    We want to return `g t1' t2' t3'` where
+    `ti'`s are `visit(ti)`.
+    */
+    expr visit_delayed(array_ref<expr> const & fvars, expr const & val, expr const & e, buffer<expr> & args) {
+        expr const * curr = &e;
+        while (is_app(*curr)) {
+            args.push_back(visit(app_arg(*curr)));
+            curr = &app_fn(*curr);
+        }
+        expr val_new = replace_fvars(val, fvars, args.data() + (args.size() - fvars.size()));
+        return mk_rev_app(val_new, args.size() - fvars.size(), args.data());
+    }
+
+    expr visit_app(expr const & e) {
+        expr const & f = get_app_fn(e);
+        if (!is_mvar(f)) {
+            return visit_app_default(e);
+        } else {
+            name const & mid = mvar_name(f);
+            option_ref<delayed_assignment> d = get_delayed_mvar_assignment(m_mctx, mid);
+            if (!d) {
+                // mvar is not delayed assigned
+                expr f_new = visit(f);
+                if (is_eqp(f, f_new)) {
+                    return visit_mvar_app_args(e);
+                } else {
+                    buffer<expr> args;
+                    return visit_args_and_beta(f_new, e, args);
+                }
+            } else {
+                /*
+                Apply "delayed substitution" (i.e., delayed assignment + application).
+                That is, `f` is some metavariable `?m`, that is delayed assigned to `val`.
+                If after instantiating `val`, we obtain `newVal`, and `newVal` does not contain
+                metavariables, we replace the free variables `fvars` in `newVal` with the first
+                `fvars.size` elements of `args`.
+                */
+                array_ref<expr> fvars(cnstr_get(d.get_val().raw(), 0), true);
+                name mid_pending(cnstr_get(d.get_val().raw(), 1), true);
+                if (fvars.size() > get_app_num_args(e)) {
+                    /*
+                    We don't have sufficient arguments for instantiating the free variables `fvars`.
+                    This can only happen if a tactic or elaboration function is not implemented correctly.
+                    We decided to not use `panic!` here and report it as an error in the frontend
+                    when we are checking for unassigned metavariables in an elaborated term. */
+                    return visit_mvar_app_args(e);
+                }
+                optional<expr> val = get_assignment(mid_pending);
+                if (!val)
+                    // mid_pending has not been assigned yet.
+                    return visit_mvar_app_args(e);
+                if (has_expr_mvar(*val))
+                    // mid_pending has been assigned, but assignment contains mvars.
+                    return visit_mvar_app_args(e);
+                buffer<expr> args;
+                return visit_delayed(fvars, *val, e, args);
+            }
+        }
+    }
+
+    expr visit_mvar(expr const & e) {
+        name const & mid = mvar_name(e);
+        if (auto r = get_assignment(mid)) {
+            return *r;
+        } else {
+            return e;
+        }
+    }
+
+public:
+    instantiate_mvars_fn(metavar_ctx & mctx):m_mctx(mctx), m_level_fn(mctx) {}
+
+    expr visit(expr const & e) {
+        if (!has_mvar(e))
+            return e;
+        bool shared = false;
+        if (is_shared(e)) {
+            auto it = m_cache.find(e.raw());
+            if (it != m_cache.end()) {
+                return it->second;
+            }
+            shared = true;
+        }
+
+        switch (e.kind()) {
+        case expr_kind::BVar:
+        case expr_kind::Lit:  case expr_kind::FVar:
+            lean_unreachable();
+        case expr_kind::Sort:
+            return cache(e, update_sort(e, visit_level(sort_level(e))), shared);
+        case expr_kind::Const:
+            return cache(e, update_const(e, visit_levels(const_levels(e))), shared);
+        case expr_kind::MVar:
+            return visit_mvar(e);
+        case expr_kind::MData:
+            return cache(e, update_mdata(e, visit(mdata_expr(e))), shared);
+        case expr_kind::Proj:
+            return cache(e, update_proj(e, visit(proj_expr(e))), shared);
+        case expr_kind::App:
+            return cache(e, visit_app(e), shared);
+        case expr_kind::Pi: case expr_kind::Lambda:
+            return cache(e, update_binding(e, visit(binding_domain(e)), visit(binding_body(e))), shared);
+        case expr_kind::Let:
+            return cache(e, update_let(e, visit(let_type(e)), visit(let_value(e)), visit(let_body(e))), shared);
+        }
+    }
+
+    expr operator()(expr const & e) { return visit(e); }
+};
+
+extern "C" LEAN_EXPORT object * lean_instantiate_expr_mvars(object * m, object * e) {
+    metavar_ctx mctx(m);
+    expr e_new = instantiate_mvars_fn(mctx)(expr(e));
+    object * r = alloc_cnstr(0, 2, 0);
+    cnstr_set(r, 0, mctx.steal());
+    cnstr_set(r, 1, e_new.steal());
+    return r;
+}
+}
--- a/src/kernel/level.h
+++ b/src/kernel/level.h
@@ -43,14 +43,14 @@ public:
    explicit level(obj_arg o):object_ref(o) {}
    explicit level(b_obj_arg o, bool b):object_ref(o, b) {}
    level(level const & other):object_ref(other) {}
-    level(level && other):object_ref(other) {}
+    level(level && other):object_ref(std::move(other)) {}
    level_kind kind() const {
      return lean_is_scalar(raw()) ? level_kind::Zero : static_cast<level_kind>(lean_ptr_tag(raw()));
    }
    unsigned hash() const;

    level & operator=(level const & other) { object_ref::operator=(other); return *this; }
-    level & operator=(level && other) { object_ref::operator=(other); return *this; }
+    level & operator=(level && other) { object_ref::operator=(std::move(other)); return *this; }

    friend bool is_eqp(level const & l1, level const & l2) { return l1.raw() == l2.raw(); }

@@ -82,6 +82,8 @@ inline bool operator!=(level const & l1, level const & l2) { return !operator==(
 struct level_hash { unsigned operator()(level const & n) const { return n.hash(); } };
 struct level_eq { bool operator()(level const & n1, level const & n2) const { return n1 == n2; } };

+inline bool is_shared(level const & l) { return !is_exclusive(l.raw()); }
+
 inline optional<level> none_level() { return optional<level>(); }
 inline optional<level> some_level(level const & e) { return optional<level>(e); }
 inline optional<level> some_level(level && e) { return optional<level>(std::forward<level>(e)); }
--- a/src/kernel/local_ctx.h
+++ b/src/kernel/local_ctx.h
@@ -27,11 +27,11 @@ class local_decl : public object_ref {
 public:
    local_decl();
    local_decl(local_decl const & other):object_ref(other) {}
-    local_decl(local_decl && other):object_ref(other) {}
+    local_decl(local_decl && other):object_ref(std::move(other)) {}
    local_decl(obj_arg o):object_ref(o) {}
    local_decl(b_obj_arg o, bool):object_ref(o, true) {}
    local_decl & operator=(local_decl const & other) { object_ref::operator=(other); return *this; }
-    local_decl & operator=(local_decl && other) { object_ref::operator=(other); return *this; }
+    local_decl & operator=(local_decl && other) { object_ref::operator=(std::move(other)); return *this; }
    friend bool is_eqp(local_decl const & d1, local_decl const & d2) { return d1.raw() == d2.raw(); }
    unsigned get_idx() const { return static_cast<nat const &>(cnstr_get_ref(raw(), 0)).get_small_value(); }
    name const & get_name() const { return static_cast<name const &>(cnstr_get_ref(raw(), 1)); }
@@ -54,9 +54,9 @@ public:
    explicit local_ctx(obj_arg o):object_ref(o) {}
    local_ctx(b_obj_arg o, bool):object_ref(o, true) {}
    local_ctx(local_ctx const & other):object_ref(other) {}
-    local_ctx(local_ctx && other):object_ref(other) {}
+    local_ctx(local_ctx && other):object_ref(std::move(other)) {}
    local_ctx & operator=(local_ctx const & other) { object_ref::operator=(other); return *this; }
-    local_ctx & operator=(local_ctx && other) { object_ref::operator=(other); return *this; }
+    local_ctx & operator=(local_ctx && other) { object_ref::operator=(std::move(other)); return *this; }

    bool empty() const;

--- a/src/kernel/replace_fn.cpp
+++ b/src/kernel/replace_fn.cpp
@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include <vector>
 #include <memory>
+#include <utility>
 #include <unordered_map>
 #include "kernel/replace_fn.h"

@@ -14,14 +15,14 @@ namespace lean {
 class replace_rec_fn {
    struct key_hasher {
        std::size_t operator()(std::pair<lean_object *, unsigned> const & p) const {
-            return hash((size_t)p.first, p.second);
+            return hash((size_t)p.first >> 3, p.second);
        }
    };
    std::unordered_map<std::pair<lean_object *, unsigned>, expr, key_hasher> m_cache;
    std::function<optional<expr>(expr const &, unsigned)> m_f;
    bool                                                  m_use_cache;

-    expr save_result(expr const & e, unsigned offset, expr const & r, bool shared) {
+    expr save_result(expr const & e, unsigned offset, expr r, bool shared) {
        if (shared)
            m_cache.insert(mk_pair(mk_pair(e.raw(), offset), r));
        return r;
@@ -36,7 +37,7 @@ class replace_rec_fn {
            shared = true;
        }
        if (optional<expr> r = m_f(e, offset)) {
-            return save_result(e, offset, *r, shared);
+            return save_result(e, offset, std::move(*r), shared);
        } else {
            switch (e.kind()) {
            case expr_kind::Const: case expr_kind::Sort:
--- a/src/library/compiler/specialize.cpp
+++ b/src/library/compiler/specialize.cpp
@@ -92,10 +92,10 @@ public:
        object_ref(mk_cnstr(0, ns, ks)) {}
    spec_info():spec_info(names(), spec_arg_kinds()) {}
    spec_info(spec_info const & other):object_ref(other) {}
-    spec_info(spec_info && other):object_ref(other) {}
+    spec_info(spec_info && other):object_ref(std::move(other)) {}
    spec_info(b_obj_arg o, bool b):object_ref(o, b) {}
    spec_info & operator=(spec_info const & other) { object_ref::operator=(other); return *this; }
-    spec_info & operator=(spec_info && other) { object_ref::operator=(other); return *this; }
+    spec_info & operator=(spec_info && other) { object_ref::operator=(std::move(other)); return *this; }
    names const & get_mutual_decls() const { return static_cast<names const &>(cnstr_get_ref(*this, 0)); }
    spec_arg_kinds const & get_arg_kinds() const { return static_cast<spec_arg_kinds const &>(cnstr_get_ref(*this, 1)); }
 };
--- a/src/library/projection.h
+++ b/src/library/projection.h
@@ -24,13 +24,13 @@ public:
    projection_info(name const & c, unsigned nparams, unsigned i, bool inst_implicit);
    projection_info():projection_info(name(), 0, 0, false) {}
    projection_info(projection_info const & other):object_ref(other) {}
-    projection_info(projection_info && other):object_ref(other) {}
+    projection_info(projection_info && other):object_ref(std::move(other)) {}
    /* low-level constructors */
    explicit projection_info(object * o):object_ref(o) {}
    explicit projection_info(b_obj_arg o, bool b):object_ref(o, b) {}
    explicit projection_info(object_ref const & o):object_ref(o) {}
    projection_info & operator=(projection_info const & other) { object_ref::operator=(other); return *this; }
-    projection_info & operator=(projection_info && other) { object_ref::operator=(other); return *this; }
+    projection_info & operator=(projection_info && other) { object_ref::operator=(std::move(other)); return *this; }
    name const & get_constructor() const { return static_cast<name const &>(cnstr_get_ref(*this, 0)); }
    unsigned get_nparams() const { return static_cast<nat const &>(cnstr_get_ref(*this, 1)).get_small_value(); }
    unsigned get_i() const { return static_cast<nat const &>(cnstr_get_ref(*this, 2)).get_small_value(); }
--- a/src/runtime/array_ref.h
+++ b/src/runtime/array_ref.h
@@ -28,12 +28,12 @@ public:
    array_ref(b_obj_arg o, bool b):object_ref(o, b) {}
    array_ref():object_ref(array_mk_empty()) {}
    array_ref(array_ref const & other):object_ref(other) {}
-    array_ref(array_ref && other):object_ref(other) {}
+    array_ref(array_ref && other):object_ref(std::move(other)) {}
    array_ref(std::initializer_list<T> const & elems):object_ref(to_array(elems)) {}
    array_ref(buffer<T> const & elems):object_ref(to_array(elems)) {}

    array_ref & operator=(array_ref const & other) { object_ref::operator=(other); return *this; }
-    array_ref & operator=(array_ref && other) { object_ref::operator=(other); return *this; }
+    array_ref & operator=(array_ref && other) { object_ref::operator=(std::move(other)); return *this; }

    size_t size() const { return array_size(raw()); }

--- a/src/runtime/list_ref.h
+++ b/src/runtime/list_ref.h
@@ -23,7 +23,7 @@ public:
    explicit list_ref(list_ref<T> const * l) { if (l) *this = *l; }
    list_ref(T const & h, list_ref<T> const & t):object_ref(mk_cnstr(1, h.raw(), t.raw())) { inc(h.raw()); inc(t.raw()); }
    list_ref(list_ref const & other):object_ref(other) {}
-    list_ref(list_ref && other):object_ref(other) {}
+    list_ref(list_ref && other):object_ref(std::move(other)) {}
    template<typename It> list_ref(It const & begin, It const & end):list_ref() {
        auto it = end;
        while (it != begin) {
@@ -35,7 +35,7 @@ public:
    list_ref(buffer<T> const & b):list_ref(b.begin(), b.end()) {}

    list_ref & operator=(list_ref const & other) { object_ref::operator=(other); return *this; }
-    list_ref & operator=(list_ref && other) { object_ref::operator=(other); return *this; }
+    list_ref & operator=(list_ref && other) { object_ref::operator=(std::move(other)); return *this; }

    explicit operator bool() const { return !is_scalar(raw()); }
    friend bool is_nil(list_ref const & l) { return is_scalar(l.raw()); }
--- a/src/runtime/object_ref.h
+++ b/src/runtime/object_ref.h
@@ -35,6 +35,10 @@ public:
        s.m_obj = box(0);
        return *this;
    }
+    void set_box(object * o) {
+        lean_assert(is_scalar(m_obj));
+        m_obj = o;
+    }
    object * raw() const { return m_obj; }
    object * steal() { object * r = m_obj; m_obj = box(0); return r; }
    object * to_obj_arg() const { inc(m_obj); return m_obj; }
--- a/src/runtime/option_ref.h
+++ b/src/runtime/option_ref.h
@@ -16,18 +16,20 @@ public:
    option_ref(b_obj_arg o, bool b):object_ref(o, b) {}
    option_ref():object_ref(box(0)) {}
    option_ref(option_ref const & other):object_ref(other) {}
-    option_ref(option_ref && other):object_ref(other) {}
+    option_ref(option_ref && other):object_ref(std::move(other)) {}
    explicit option_ref(T const & a):object_ref(mk_cnstr(1, a.raw())) { inc(a.raw()); }
    explicit option_ref(T const * a) { if (a) *this = option_ref(*a); }
    explicit option_ref(option_ref<T> const * o) { if (o) *this = *o; }
    explicit option_ref(optional<T> const & o):option_ref(o ? &*o : nullptr) {}

    option_ref & operator=(option_ref const & other) { object_ref::operator=(other); return *this; }
-    option_ref & operator=(option_ref && other) { object_ref::operator=(other); return *this; }
+    option_ref & operator=(option_ref && other) { object_ref::operator=(std::move(other)); return *this; }

    explicit operator bool() const { return !is_scalar(raw()); }
    optional<T> get() const { return *this ? some(static_cast<T const &>(cnstr_get_ref(*this, 0))) : optional<T>(); }

+    T get_val() const { lean_assert(*this); return static_cast<T const &>(cnstr_get_ref(*this, 0)); }
+
    /** \brief Structural equality. */
    friend bool operator==(option_ref const & o1, option_ref const & o2) {
        return o1.get() == o2.get();
--- a/src/runtime/optional.h
+++ b/src/runtime/optional.h
@@ -31,13 +31,13 @@ public:
    }
    optional(optional && other):m_some(other.m_some) {
        if (other.m_some)
-            new (&m_value) T(std::forward<T>(other.m_value));
+            new (&m_value) T(std::move(other.m_value));
    }
    explicit optional(T const & v):m_some(true) {
        new (&m_value) T(v);
    }
    explicit optional(T && v):m_some(true) {
-        new (&m_value) T(std::forward<T>(v));
+        new (&m_value) T(std::move(v));
    }
    template<typename... Args>
    explicit optional(Args&&... args):m_some(true) {
@@ -84,7 +84,7 @@ public:
            m_value.~T();
        m_some = other.m_some;
        if (m_some)
-            new (&m_value) T(std::forward<T>(other.m_value));
+            new (&m_value) T(std::move(other.m_value));
        return *this;
    }
    optional& operator=(T const & other) {
@@ -98,7 +98,7 @@ public:
        if (m_some)
            m_value.~T();
        m_some = true;
-        new (&m_value) T(std::forward<T>(other));
+        new (&m_value) T(std::move(other));
        return *this;
    }

@@ -130,9 +130,9 @@ template<> class optional<P> {                                          \
 public:                                                                 \
    optional():m_value(nullptr) {}                                      \
    optional(optional const & other):m_value(other.m_value) {}          \
-    optional(optional && other):m_value(std::forward<P>(other.m_value)) {} \
+    optional(optional && other):m_value(std::move(other.m_value)) {} \
    explicit optional(P const & v):m_value(v) {}                        \
-    explicit optional(P && v):m_value(std::forward<P>(v)) {}            \
+    explicit optional(P && v):m_value(std::move(v)) {}            \
                                                                        \
    explicit operator bool() const { return m_value.m_ptr != nullptr; } \
    P const * operator->() const { lean_assert(m_value.m_ptr); return &m_value; } \
@@ -142,9 +142,9 @@ public:                                                                 \
    P const & value() const { lean_assert(m_value.m_ptr); return m_value; } \
    P & value() { lean_assert(m_value.m_ptr); return m_value; }         \
    optional & operator=(optional const & other) { m_value = other.m_value; return *this; } \
-    optional& operator=(optional && other) { m_value = std::forward<P>(other.m_value); return *this; } \
+    optional& operator=(optional && other) { m_value = std::move(other.m_value); return *this; } \
    optional& operator=(P const & other) { m_value = other; return *this; } \
-    optional& operator=(P && other) { m_value = std::forward<P>(other); return *this; } \
+    optional& operator=(P && other) { m_value = std::move(other); return *this; } \
    friend bool operator==(optional const & o1, optional const & o2) {  \
        return static_cast<bool>(o1) == static_cast<bool>(o2) && (!o1 || o1.m_value == o2.m_value); \
    }                                                                   \
--- a/src/runtime/sharecommon.cpp
+++ b/src/runtime/sharecommon.cpp
@@ -4,11 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.

 Author: Leonardo de Moura
 */
-#include <vector>
 #include <cstring>
-#include <unordered_map>
-#include <unordered_set>
-#include "runtime/object.h"
+#include "runtime/sharecommon.h"
 #include "runtime/hash.h"

 namespace lean {
@@ -271,176 +268,168 @@ extern "C" LEAN_EXPORT obj_res lean_state_sharecommon(b_obj_arg tc, obj_arg s, o
    return sharecommon_fn(tc, s)(a);
 }

+
 /*
-A faster version of `sharecommon_fn` which only uses a local state.
-It optimizes the number of RC operations, the strategy for caching results,
-and uses C++ hashmap.
+  We do not increment reference counters when inserting Lean objects at `m_cache` and `m_set`.
+  This is correct because
+  - The domain of `m_cache` contains only sub-objects of `lean_sharecommon_quick` parameter,
+    and we know the object referenced by this parameter will remain alive.
+  - The range of `m_cache` contains only new objects that have been maxed shared, and these
+    objects will be are sub-objects of the object returned by `lean_sharecommon_quick`.
+  - `m_set` is like the range of `m_cache`.
 */
-class sharecommon_quick_fn {
-    struct set_hash {
-        std::size_t operator()(lean_object * o) const { return lean_sharecommon_hash(o); }
-    };
-    struct set_eq {
-        std::size_t operator()(lean_object * o1, lean_object * o2) const { return lean_sharecommon_eq(o1, o2); }
-    };

-    /*
-    We use `m_cache` to ensure we do **not** traverse a DAG as a tree.
-    We use pointer equality for this collection.
-    */
-    std::unordered_map<lean_object *, lean_object *> m_cache;
-    /* Set of maximally shared terms. AKA hash-consing table. */
-    std::unordered_set<lean_object *, set_hash, set_eq> m_set;
-
-    /*
-      We do not increment reference counters when inserting Lean objects at `m_cache` and `m_set`.
-      This is correct because
-      - The domain of `m_cache` contains only sub-objects of `lean_sharecommon_quick` parameter,
-        and we know the object referenced by this parameter will remain alive.
-      - The range of `m_cache` contains only new objects that have been maxed shared, and these
-        objects will be are sub-objects of the object returned by `lean_sharecommon_quick`.
-      - `m_set` is like the range of `m_cache`.
-    */
-
-    lean_object * check_cache(lean_object * a) {
-        if (!lean_is_exclusive(a)) {
-            // We only check the cache if `a` is a shared object
-            auto it = m_cache.find(a);
-            if (it != m_cache.end()) {
-                // All objects stored in the range of `m_cache` are single threaded.
-                lean_assert(lean_is_st(it->second));
-                // We increment the reference counter because this object
-                // will be returned by `lean_sharecommon_quick` or stored into a new object.
-                it->second->m_rc++;
-                return it->second;
+lean_object * sharecommon_quick_fn::check_cache(lean_object * a) {
+    if (!lean_is_exclusive(a)) {
+        // We only check the cache if `a` is a shared object
+        auto it = m_cache.find(a);
+        if (it != m_cache.end()) {
+            // All objects stored in the range of `m_cache` are single threaded.
+            lean_assert(lean_is_st(it->second));
+            // We increment the reference counter because this object
+            // will be returned by `lean_sharecommon_quick` or stored into a new object.
+            it->second->m_rc++;
+            return it->second;
+        }
+        if (m_check_set) {
+            auto it = m_set.find(a);
+            if (it != m_set.end()) {
+                lean_object * result = *it;
+                lean_assert(lean_is_st(result));
+                result->m_rc++;
+                return result;
            }
        }
-        return nullptr;
    }
+    return nullptr;
+}

-    /*
-    `new_a` is a new object that is equal to `a`, but its subobjects are maximally shared.
-    */
-    lean_object * save(lean_object * a, lean_object * new_a) {
-        lean_assert(lean_is_st(new_a));
-        lean_assert(new_a->m_rc == 1);
-        auto it = m_set.find(new_a);
-        lean_object * result;
-        if (it == m_set.end()) {
-            // `new_a` is a new object
-            m_set.insert(new_a);
-            result = new_a;
-        } else {
-            // We already have a maximally shared object that is equal to `new_a`
-            result = *it;
-            DEBUG_CODE({
-                    if (lean_is_ctor(new_a)) {
-                        lean_assert(lean_is_ctor(result));
-                        unsigned num_objs = lean_ctor_num_objs(new_a);
-                        lean_assert(lean_ctor_num_objs(result) == num_objs);
-                        for (unsigned i = 0; i < num_objs; i++) {
-                            lean_assert(lean_ctor_get(result, i) == lean_ctor_get(new_a, i));
-                        }
+/*
+  `new_a` is a new object that is equal to `a`, but its subobjects are maximally shared.
+*/
+lean_object * sharecommon_quick_fn::save(lean_object * a, lean_object * new_a) {
+    lean_assert(lean_is_st(new_a));
+    lean_assert(new_a->m_rc == 1);
+    auto it = m_set.find(new_a);
+    lean_object * result;
+    if (it == m_set.end()) {
+        // `new_a` is a new object
+        m_set.insert(new_a);
+        result = new_a;
+    } else {
+        // We already have a maximally shared object that is equal to `new_a`
+        result = *it;
+        DEBUG_CODE({
+                if (lean_is_ctor(new_a)) {
+                    lean_assert(lean_is_ctor(result));
+                    unsigned num_objs = lean_ctor_num_objs(new_a);
+                    lean_assert(lean_ctor_num_objs(result) == num_objs);
+                    for (unsigned i = 0; i < num_objs; i++) {
+                        lean_assert(lean_ctor_get(result, i) == lean_ctor_get(new_a, i));
                    }
-                });
-            lean_dec_ref(new_a); // delete `new_a`
-            // All objects in `m_set` are single threaded.
-            lean_assert(lean_is_st(result));
-            result->m_rc++;
-            lean_assert(result->m_rc > 1);
-        }
-        if (!lean_is_exclusive(a)) {
-            // We only cache the result if `a` is a shared object.
-            m_cache.insert(std::make_pair(a, result));
-        }
-        lean_assert(result == new_a || result->m_rc > 1);
-        lean_assert(result != new_a || result->m_rc == 1);
-        return result;
+                }
+            });
+        lean_dec_ref(new_a); // delete `new_a`
+        // All objects in `m_set` are single threaded.
+        lean_assert(lean_is_st(result));
+        result->m_rc++;
+        lean_assert(result->m_rc > 1);
    }
+    if (!lean_is_exclusive(a)) {
+        // We only cache the result if `a` is a shared object.
+        m_cache.insert(std::make_pair(a, result));
+    }
+    lean_assert(result == new_a || result->m_rc > 1);
+    lean_assert(result != new_a || result->m_rc == 1);
+    return result;
+}

-    // `sarray` and `string`
-    lean_object * visit_terminal(lean_object * a) {
-        auto it = m_set.find(a);
-        if (it == m_set.end()) {
-            m_set.insert(a);
-        } else {
-            a = *it;
-        }
-        lean_inc_ref(a);
+// `sarray` and `string`
+lean_object * sharecommon_quick_fn::visit_terminal(lean_object * a) {
+    auto it = m_set.find(a);
+    if (it == m_set.end()) {
+        m_set.insert(a);
+    } else {
+        a = *it;
+    }
+    lean_inc_ref(a);
+    return a;
+}
+
+lean_object * sharecommon_quick_fn::visit_array(lean_object * a) {
+    lean_object * r = check_cache(a);
+    if (r != nullptr) { lean_assert(r->m_rc > 1); return r; }
+
+    size_t sz = array_size(a);
+    lean_array_object * new_a = (lean_array_object*)lean_alloc_array(sz, sz);
+    for (size_t i = 0; i < sz; i++) {
+        lean_array_set_core((lean_object*)new_a, i, visit(lean_array_get_core(a, i)));
+    }
+    return save(a, (lean_object*)new_a);
+}
+
+lean_object * sharecommon_quick_fn::visit_ctor(lean_object * a) {
+    lean_object * r = check_cache(a);
+    if (r != nullptr) { lean_assert(r->m_rc > 1); return r; }
+    unsigned num_objs      = lean_ctor_num_objs(a);
+    unsigned tag           = lean_ptr_tag(a);
+    unsigned sz            = lean_object_byte_size(a);
+    unsigned scalar_offset = sizeof(lean_object) + num_objs*sizeof(void*);
+    unsigned scalar_sz     = sz - scalar_offset;
+    lean_object * new_a    = lean_alloc_ctor(tag, num_objs, scalar_sz);
+    for (unsigned i = 0; i < num_objs; i++) {
+        lean_ctor_set(new_a, i, visit(lean_ctor_get(a, i)));
+    }
+    if (scalar_sz > 0) {
+        memcpy(reinterpret_cast<char*>(new_a) + scalar_offset, reinterpret_cast<char*>(a) + scalar_offset, scalar_sz);
+    }
+    return save(a, new_a);
+}
+
+/*
+**TODO:** We did not implement stack overflow detection.
+We claim it is not needed in the current uses of `shareCommon'`.
+If this becomes an issue, we can use the following approach to address the issue without
+affecting the performance.
+- Add an extra `depth` parameter.
+- In `operator()`, estimate the maximum depth based on the remaining stack space. See `check_stack`.
+- If the limit is reached, simply return `a`.
+*/
+lean_object * sharecommon_quick_fn::visit(lean_object * a) {
+    if (lean_is_scalar(a)) {
        return a;
    }
-
-    lean_object * visit_array(lean_object * a) {
-        lean_object * r = check_cache(a);
-        if (r != nullptr) { lean_assert(r->m_rc > 1); return r; }
-
-        size_t sz = array_size(a);
-        lean_array_object * new_a = (lean_array_object*)lean_alloc_array(sz, sz);
-        for (size_t i = 0; i < sz; i++) {
-            lean_array_set_core((lean_object*)new_a, i, visit(lean_array_get_core(a, i)));
-        }
-        return save(a, (lean_object*)new_a);
-    }
-
-    lean_object * visit_ctor(lean_object * a) {
-        lean_object * r = check_cache(a);
-        if (r != nullptr) { lean_assert(r->m_rc > 1); return r; }
-        unsigned num_objs      = lean_ctor_num_objs(a);
-        unsigned tag           = lean_ptr_tag(a);
-        unsigned sz            = lean_object_byte_size(a);
-        unsigned scalar_offset = sizeof(lean_object) + num_objs*sizeof(void*);
-        unsigned scalar_sz     = sz - scalar_offset;
-        lean_object * new_a    = lean_alloc_ctor(tag, num_objs, scalar_sz);
-        for (unsigned i = 0; i < num_objs; i++) {
-            lean_ctor_set(new_a, i, visit(lean_ctor_get(a, i)));
-        }
-        if (scalar_sz > 0) {
-            memcpy(reinterpret_cast<char*>(new_a) + scalar_offset, reinterpret_cast<char*>(a) + scalar_offset, scalar_sz);
-        }
-        return save(a, new_a);
-    }
-
-public:
-
+    switch (lean_ptr_tag(a)) {
    /*
-    **TODO:** We did not implement stack overflow detection.
-    We claim it is not needed in the current uses of `shareCommon'`.
-    If this becomes an issue, we can use the following approach to address the issue without
-    affecting the performance.
-    - Add an extra `depth` parameter.
-    - In `operator()`, estimate the maximum depth based on the remaining stack space. See `check_stack`.
-    - If the limit is reached, simply return `a`.
+      Similarly to `sharecommon_fn`, we only maximally share arrays, scalar arrays, strings, and
+      constructor objects.
    */
-    lean_object * visit(lean_object * a) {
-        if (lean_is_scalar(a)) {
-            return a;
-        }
-        switch (lean_ptr_tag(a)) {
-        /*
-        Similarly to `sharecommon_fn`, we only maximally share arrays, scalar arrays, strings, and
-        constructor objects.
-        */
-        case LeanMPZ:             lean_inc_ref(a); return a;
-        case LeanClosure:         lean_inc_ref(a); return a;
-        case LeanThunk:           lean_inc_ref(a); return a;
-        case LeanTask:            lean_inc_ref(a); return a;
-        case LeanRef:             lean_inc_ref(a); return a;
-        case LeanExternal:        lean_inc_ref(a); return a;
-        case LeanReserved:        lean_inc_ref(a); return a;
-        case LeanScalarArray:     return visit_terminal(a);
-        case LeanString:          return visit_terminal(a);
-        case LeanArray:           return visit_array(a);
-        default:                  return visit_ctor(a);
-        }
+    case LeanMPZ:             lean_inc_ref(a); return a;
+    case LeanClosure:         lean_inc_ref(a); return a;
+    case LeanThunk:           lean_inc_ref(a); return a;
+    case LeanTask:            lean_inc_ref(a); return a;
+    case LeanRef:             lean_inc_ref(a); return a;
+    case LeanExternal:        lean_inc_ref(a); return a;
+    case LeanReserved:        lean_inc_ref(a); return a;
+    case LeanScalarArray:     return visit_terminal(a);
+    case LeanString:          return visit_terminal(a);
+    case LeanArray:           return visit_array(a);
+    default:                  return visit_ctor(a);
    }
-
-    lean_object * operator()(lean_object * a) {
-        return visit(a);
-    }
-};
+}

 // def ShareCommon.shareCommon' (a : A) : A := a
 extern "C" LEAN_EXPORT obj_res lean_sharecommon_quick(obj_arg a) {
    return sharecommon_quick_fn()(a);
 }
+
+lean_object * sharecommon_persistent_fn::operator()(lean_object * e) {
+    lean_object * r = check_cache(e);
+    if (r != nullptr)
+        return r;
+    m_saved.push_back(object_ref(e, true));
+    r = visit(e);
+    m_saved.push_back(object_ref(r, true));
+    return r;
+}
 };
--- a/src/runtime/sharecommon.h
+++ b/src/runtime/sharecommon.h
@@ -0,0 +1,71 @@
+/*
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include <vector>
+#include <unordered_map>
+#include <unordered_set>
+#include "runtime/object_ref.h"
+
+namespace lean {
+extern "C" LEAN_EXPORT uint8 lean_sharecommon_eq(b_obj_arg o1, b_obj_arg o2);
+extern "C" LEAN_EXPORT uint64_t lean_sharecommon_hash(b_obj_arg o);
+
+/*
+A faster version of `sharecommon_fn` which only uses a local state.
+It optimizes the number of RC operations, the strategy for caching results,
+and uses C++ hashmap.
+*/
+class LEAN_EXPORT sharecommon_quick_fn {
+protected:
+    struct set_hash {
+        std::size_t operator()(lean_object * o) const { return lean_sharecommon_hash(o); }
+    };
+    struct set_eq {
+        std::size_t operator()(lean_object * o1, lean_object * o2) const { return lean_sharecommon_eq(o1, o2); }
+    };
+
+    /*
+    We use `m_cache` to ensure we do **not** traverse a DAG as a tree.
+    We use pointer equality for this collection.
+    */
+    std::unordered_map<lean_object *, lean_object *> m_cache;
+    /* Set of maximally shared terms. AKA hash-consing table. */
+    std::unordered_set<lean_object *, set_hash, set_eq> m_set;
+    /*
+    If `true`, `check_cache` will also check `m_set`.
+    This is useful when the input term may contain terms that have already
+    been hashconsed.
+    */
+    bool m_check_set;
+
+    lean_object * check_cache(lean_object * a);
+    lean_object * save(lean_object * a, lean_object * new_a);
+    lean_object * visit_terminal(lean_object * a);
+    lean_object * visit_array(lean_object * a);
+    lean_object * visit_ctor(lean_object * a);
+    lean_object * visit(lean_object * a);
+public:
+    sharecommon_quick_fn(bool s = false):m_check_set(s) {}
+    void set_check_set(bool f) { m_check_set = f; }
+    lean_object * operator()(lean_object * a) {
+        return visit(a);
+    }
+};
+
+/*
+Similar to `sharecommon_quick_fn`, but we save the entry points and result values to ensure
+they are not deleted.
+*/
+class LEAN_EXPORT sharecommon_persistent_fn : private sharecommon_quick_fn {
+    std::vector<object_ref> m_saved;
+public:
+    sharecommon_persistent_fn(bool s = false):sharecommon_quick_fn(s) {}
+    void set_check_set(bool f) { m_check_set = f; }
+    lean_object * operator()(lean_object * e);
+};
+
+};
--- a/src/runtime/string_ref.h
+++ b/src/runtime/string_ref.h
@@ -17,11 +17,11 @@ public:
    explicit string_ref(std::string const & s):object_ref(mk_string(s)) {}
    explicit string_ref(sstream const & strm):string_ref(strm.str()) {}
    string_ref(string_ref const & other):object_ref(other) {}
-    string_ref(string_ref && other):object_ref(other) {}
+    string_ref(string_ref && other):object_ref(std::move(other)) {}
    explicit string_ref(obj_arg o):object_ref(o) {}
    string_ref(b_obj_arg o, bool b):object_ref(o, b) {}
    string_ref & operator=(string_ref const & other) { object_ref::operator=(other); return *this; }
-    string_ref & operator=(string_ref && other) { object_ref::operator=(other); return *this; }
+    string_ref & operator=(string_ref && other) { object_ref::operator=(std::move(other)); return *this; }
    /* Number of bytes used to store the string in UTF8.
       Remark: it does not include the null character added in the end to make it efficient to
       convert to C string. */
--- a/src/runtime/thread.cpp
+++ b/src/runtime/thread.cpp
@@ -9,6 +9,9 @@ Author: Leonardo de Moura
 #include <iostream>
 #ifdef LEAN_WINDOWS
 #include <windows.h>
+# ifdef LEAN_AUTO_THREAD_FINALIZATION
+#include <pthread.h>
+# endif
 #else
 #include <pthread.h>
 #endif
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@@ -144,7 +144,7 @@ ENDFOREACH(T)
 # LEAN PACKAGE TESTS
 file(GLOB LEANPKGTESTS "${LEAN_SOURCE_DIR}/../tests/pkg/*")
 FOREACH(T ${LEANPKGTESTS})
-  if(IS_DIRECTORY ${T})
+  if(EXISTS ${T}/test.sh)
    GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
    add_test(NAME "leanpkgtest_${T_NAME}"
            WORKING_DIRECTORY "${T}"
--- a/src/util/kvmap.h
+++ b/src/util/kvmap.h
@@ -30,9 +30,9 @@ public:
    explicit data_value(name const & v):object_ref(mk_cnstr(static_cast<unsigned>(data_value_kind::Name), v.raw())) { inc(v.raw()); }
    data_value():data_value(false) {}
    data_value(data_value const & other):object_ref(other) {}
-    data_value(data_value && other):object_ref(other) {}
+    data_value(data_value && other):object_ref(std::move(other)) {}
    data_value & operator=(data_value const & other) { object_ref::operator=(other); return *this; }
-    data_value & operator=(data_value && other) { object_ref::operator=(other); return *this; }
+    data_value & operator=(data_value && other) { object_ref::operator=(std::move(other)); return *this; }

    data_value_kind kind() const { return static_cast<data_value_kind>(cnstr_tag(raw())); }
    string_ref const & get_string() const { lean_assert(kind() == data_value_kind::String); return static_cast<string_ref const &>(cnstr_get_ref(*this, 0)); }
--- a/src/util/name.h
+++ b/src/util/name.h
@@ -74,7 +74,7 @@ public:
    name(std::string const & s):name(name(), string_ref(s)) {}
    name(string_ref const & s):name(name(), s) {}
    name(name const & other):object_ref(other) {}
-    name(name && other):object_ref(other) {}
+    name(name && other):object_ref(std::move(other)) {}
    /**
       \brief Create a hierarchical name using the given strings.
       Example: <code>name{"foo", "bla", "tst"}</code> creates the hierarchical
@@ -97,7 +97,7 @@ public:
    */
    static name mk_internal_unique_name();
    name & operator=(name const & other) { object_ref::operator=(other); return *this; }
-    name & operator=(name && other) { object_ref::operator=(other); return *this; }
+    name & operator=(name && other) { object_ref::operator=(std::move(other)); return *this; }
    static uint64_t hash(b_obj_arg n) {
       lean_assert(lean_name_hash(n) == lean_name_hash_exported_b(n));
       return lean_name_hash(n);
--- a/src/util/nat.h
+++ b/src/util/nat.h
@@ -27,10 +27,10 @@ public:
    static nat of_size_t(size_t v) { return nat(lean_usize_to_nat(v)); }

    nat(nat const & other):object_ref(other) {}
-    nat(nat && other):object_ref(other) {}
+    nat(nat && other):object_ref(std::move(other)) {}

    nat & operator=(nat const & other) { object_ref::operator=(other); return *this; }
-    nat & operator=(nat && other) { object_ref::operator=(other); return *this; }
+    nat & operator=(nat && other) { object_ref::operator=(std::move(other)); return *this; }
    bool is_small() const { return is_scalar(raw()); }
    size_t get_small_value() const { lean_assert(is_small()); return unbox(raw()); }
    bool is_zero() const { return is_small() && get_small_value() == 0; }
--- a/src/util/shell.cpp
+++ b/src/util/shell.cpp
@@ -191,43 +191,44 @@ static void display_features(std::ostream & out) {
 static void display_help(std::ostream & out) {
    display_header(out);
    std::cout << "Miscellaneous:\n";
-    std::cout << "  --help -h          display this message\n";
-    std::cout << "  --features -f      display features compiler provides (eg. LLVM support)\n";
-    std::cout << "  --version -v       display version number\n";
-    std::cout << "  --githash          display the git commit hash number used to build this binary\n";
-    std::cout << "  --run              call the 'main' definition in a file with the remaining arguments\n";
-    std::cout << "  --o=oname -o       create olean file\n";
-    std::cout << "  --i=iname -i       create ilean file\n";
-    std::cout << "  --c=fname -c       name of the C output file\n";
-    std::cout << "  --bc=fname -b      name of the LLVM bitcode file\n";
-    std::cout << "  --stdin            take input from stdin\n";
-    std::cout << "  --root=dir         set package root directory from which the module name of the input file is calculated\n"
-              << "                     (default: current working directory)\n";
-    std::cout << "  --trust=num -t     trust level (default: max) 0 means do not trust any macro,\n"
-              << "                     and type check all imported modules\n";
-    std::cout << "  --quiet -q         do not print verbose messages\n";
-    std::cout << "  --memory=num -M    maximum amount of memory that should be used by Lean\n";
-    std::cout << "                     (in megabytes)\n";
-    std::cout << "  --timeout=num -T   maximum number of memory allocations per task\n";
-    std::cout << "                     this is a deterministic way of interrupting long running tasks\n";
+    std::cout << "  -h, --help             display this message\n";
+    std::cout << "  -f, --features         display features compiler provides (eg. LLVM support)\n";
+    std::cout << "  -v, --version          display version number\n";
+    std::cout << "      --githash          display the git commit hash number used to build this binary\n";
+    std::cout << "      --run              call the 'main' definition in a file with the remaining arguments\n";
+    std::cout << "  -o, --o=oname          create olean file\n";
+    std::cout << "  -i, --i=iname          create ilean file\n";
+    std::cout << "  -c, --c=fname          name of the C output file\n";
+    std::cout << "  -b, --bc=fname         name of the LLVM bitcode file\n";
+    std::cout << "      --stdin            take input from stdin\n";
+    std::cout << "      --root=dir         set package root directory from which the module name\n"
+              << "                         of the input file is calculated\n"
+              << "                         (default: current working directory)\n";
+    std::cout << "  -t, --trust=num        trust level (default: max) 0 means do not trust any macro,\n"
+              << "                         and type check all imported modules\n";
+    std::cout << "  -q, --quiet            do not print verbose messages\n";
+    std::cout << "  -M, --memory=num       maximum amount of memory that should be used by Lean\n";
+    std::cout << "                         (in megabytes)\n";
+    std::cout << "  -T, --timeout=num      maximum number of memory allocations per task\n";
+    std::cout << "                         this is a deterministic way of interrupting long running tasks\n";
 #if defined(LEAN_MULTI_THREAD)
-    std::cout << "  --threads=num -j   number of threads used to process lean files\n";
-    std::cout << "  --tstack=num -s    thread stack size in Kb\n";
-    std::cout << "  --server           start lean in server mode\n";
-    std::cout << "  --worker           start lean in server-worker mode\n";
+    std::cout << "  -j, --threads=num      number of threads used to process lean files\n";
+    std::cout << "  -s, --tstack=num       thread stack size in Kb\n";
+    std::cout << "      --server           start lean in server mode\n";
+    std::cout << "      --worker           start lean in server-worker mode\n";
 #endif
-    std::cout << "  --plugin=file      load and initialize Lean shared library for registering linters etc.\n";
-    std::cout << "  --load-dynlib=file load shared library to make its symbols available to the interpreter\n";
-    std::cout << "  --json             report Lean output (e.g., messages) as JSON (one per line)\n";
-    std::cout << "  --deps             just print dependencies of a Lean input\n";
-    std::cout << "  --print-prefix     print the installation prefix for Lean and exit\n";
-    std::cout << "  --print-libdir     print the installation directory for Lean's built-in libraries and exit\n";
-    std::cout << "  --profile          display elaboration/type checking time for each definition/theorem\n";
-    std::cout << "  --stats            display environment statistics\n";
+    std::cout << "      --plugin=file      load and initialize Lean shared library for registering linters etc.\n";
+    std::cout << "      --load-dynlib=file load shared library to make its symbols available to the interpreter\n";
+    std::cout << "      --json             report Lean output (e.g., messages) as JSON (one per line)\n";
+    std::cout << "      --deps             just print dependencies of a Lean input\n";
+    std::cout << "      --print-prefix     print the installation prefix for Lean and exit\n";
+    std::cout << "      --print-libdir     print the installation directory for Lean's built-in libraries and exit\n";
+    std::cout << "      --profile          display elaboration/type checking time for each definition/theorem\n";
+    std::cout << "      --stats            display environment statistics\n";
    DEBUG_CODE(
-    std::cout << "  --debug=tag        enable assertions with the given tag\n";
+    std::cout << "      --debug=tag        enable assertions with the given tag\n";
        )
-    std::cout << "  -D name=value      set a configuration option (see set_option command)\n";
+    std::cout << "      -D name=value      set a configuration option (see set_option command)\n";
 }

 static int print_prefix = 0;
@@ -310,7 +311,9 @@ options set_config_option(options const & opts, char const * in) {
                                  << "' cannot be set in the command line, use set_option command");
        }
    } else {
-        throw lean::exception(lean::sstream() << "invalid -D parameter, unknown configuration option '" << opt << "'");
+        // More options may be registered by imports, so we leave validating them to the Lean side.
+        // This (minor) duplication will be resolved when this file is rewritten in Lean.
+        return opts.update(opt, val.c_str());
    }
 }

--- a/stage0/src/kernel/CMakeLists.txt
+++ b/stage0/src/kernel/CMakeLists.txt
--- a/stage0/src/kernel/declaration.h
+++ b/stage0/src/kernel/declaration.h
--- a/stage0/src/kernel/environment.cpp
+++ b/stage0/src/kernel/environment.cpp
--- a/stage0/src/kernel/expr.h
+++ b/stage0/src/kernel/expr.h
--- a/stage0/src/kernel/expr_eq_fn.cpp
+++ b/stage0/src/kernel/expr_eq_fn.cpp
--- a/stage0/src/kernel/instantiate.cpp
+++ b/stage0/src/kernel/instantiate.cpp
--- a/stage0/src/kernel/instantiate.h
+++ b/stage0/src/kernel/instantiate.h
--- a/stage0/src/kernel/instantiate_mvars.cpp
+++ b/stage0/src/kernel/instantiate_mvars.cpp
--- a/stage0/src/kernel/level.h
+++ b/stage0/src/kernel/level.h
--- a/stage0/src/kernel/local_ctx.h
+++ b/stage0/src/kernel/local_ctx.h
--- a/stage0/src/kernel/replace_fn.cpp
+++ b/stage0/src/kernel/replace_fn.cpp
--- a/stage0/src/library/compiler/specialize.cpp
+++ b/stage0/src/library/compiler/specialize.cpp
--- a/stage0/src/library/projection.h
+++ b/stage0/src/library/projection.h
--- a/stage0/src/runtime/array_ref.h
+++ b/stage0/src/runtime/array_ref.h
--- a/stage0/src/runtime/list_ref.h
+++ b/stage0/src/runtime/list_ref.h
--- a/stage0/src/runtime/object_ref.h
+++ b/stage0/src/runtime/object_ref.h
--- a/stage0/src/runtime/option_ref.h
+++ b/stage0/src/runtime/option_ref.h
--- a/stage0/src/runtime/optional.h
+++ b/stage0/src/runtime/optional.h
--- a/stage0/src/runtime/sharecommon.cpp
+++ b/stage0/src/runtime/sharecommon.cpp
--- a/stage0/src/runtime/sharecommon.h
+++ b/stage0/src/runtime/sharecommon.h
--- a/stage0/src/runtime/string_ref.h
+++ b/stage0/src/runtime/string_ref.h
--- a/stage0/src/runtime/thread.cpp
+++ b/stage0/src/runtime/thread.cpp
--- a/stage0/src/util/kvmap.h
+++ b/stage0/src/util/kvmap.h
--- a/stage0/src/util/name.h
+++ b/stage0/src/util/name.h
--- a/stage0/src/util/nat.h
+++ b/stage0/src/util/nat.h
--- a/stage0/src/util/shell.cpp
+++ b/stage0/src/util/shell.cpp
--- a/stage0/stdlib/Init/Data.c
+++ b/stage0/stdlib/Init/Data.c
--- a/stage0/stdlib/Init/Data/Array/Lemmas.c
+++ b/stage0/stdlib/Init/Data/Array/Lemmas.c
--- a/stage0/stdlib/Init/Data/Array/TakeDrop.c
+++ b/stage0/stdlib/Init/Data/Array/TakeDrop.c
--- a/stage0/stdlib/Init/Data/BitVec/Basic.c
+++ b/stage0/stdlib/Init/Data/BitVec/Basic.c
--- a/stage0/stdlib/Init/Data/BitVec/Bitblast.c
+++ b/stage0/stdlib/Init/Data/BitVec/Bitblast.c
--- a/stage0/stdlib/Init/Data/BitVec/Lemmas.c
+++ b/stage0/stdlib/Init/Data/BitVec/Lemmas.c
--- a/stage0/stdlib/Init/Data/Int/Basic.c
+++ b/stage0/stdlib/Init/Data/Int/Basic.c
--- a/stage0/stdlib/Init/Data/List.c
+++ b/stage0/stdlib/Init/Data/List.c
--- a/stage0/stdlib/Init/Data/List/Attach.c
+++ b/stage0/stdlib/Init/Data/List/Attach.c
--- a/stage0/stdlib/Init/Data/List/Count.c
+++ b/stage0/stdlib/Init/Data/List/Count.c
--- a/stage0/stdlib/Init/Data/List/Erase.c
+++ b/stage0/stdlib/Init/Data/List/Erase.c
--- a/Show More
+++ b/Show More
Author	SHA1	Message	Date
Leonardo de Moura	89e1b4d304	chore: reduce benchmark stack usage We are running out of stack space in debug mode	2024-08-06 10:23:25 -07:00
Leonardo de Moura	f8816b8c15	chore: `recursion` => `while` at `instantiate_mvars_fn`	2024-08-06 10:23:25 -07:00
Leonardo de Moura	4a2fb6e922	chore: fix typo (#4929 )	2024-08-06 15:27:20 +00:00
Henrik Böving	b7db82894b	feat: generalized `Parsec` (#4774 ) For experimentation by @the-sofi-uwu. I also have an efficient number parser in LeanSAT that I am planning to upstream after we have sufficiently bikeshed this change.	2024-08-06 15:17:23 +00:00
Sebastian Ullrich	35e1554ef7	chore: ignore stale leanpkg tests (#4925 )	2024-08-06 08:19:33 +00:00
Leonardo de Moura	14d59b3599	feat: theorem diagnostics (#4924 ) When `set_option diagnostics true`, for each theorem with size > `diagnostics.threshold.proofSize`, display proof size, and the number of applications for each constant symbol.	2024-08-06 01:01:28 +00:00
Leonardo de Moura	a8e480cd52	chore: profile `instantiateMVars` at `MutualDef.lean` (#4923 ) `instantiateMVars` can be a performance bottleneck when assembling the final proof term. For example, it takes approx. 1 second at https://github.com/leanprover/LNSym/blob/proof_size_expt/Proofs/SHA512/Experiments/Sym30.lean	2024-08-05 19:15:56 +00:00
Leonardo de Moura	d07239d1bd	perf: use `lean_instantiate_expr_mvars` at `instantiateExprMVars` (#4922 ) This PR completes #4915	2024-08-05 19:02:54 +00:00
Leonardo de Moura	590de785cc	chore: cleanup `betaRev` (#4921 )	2024-08-05 18:02:20 +00:00
Lean stage0 autoupdater	d671d0d61a	chore: update stage0	2024-08-05 17:53:40 +00:00
Leonardo de Moura	8e476e9d22	perf: `instantiateExprMVars` (#4915 ) TODO: - Support for `zeta := true` at `apply_beta`. - Investigate test failure. - Break PR in pieces because of bootstrapping issues. The current PR updates a stage0 file to workaround the issue. Motivation: significant performance improvement at https://github.com/leanprover/LNSym/blob/proof_size_expt/Proofs/SHA512/Experiments/Sym30.lean With M1 Pro: - Before: 4.56 secs - After: 3.16 secs Successfully built stage2 using this PR	2024-08-05 17:15:22 +00:00
Sebastian Ullrich	a3d144a362	feat: new snapshot architecture on the cmdline (#3106 ) This is #3014 with cad5cce reverted for testing.	2024-08-05 15:57:42 +00:00
Sebastian Ullrich	87d41e6326	chore: missing include on Windows (#4919 )	2024-08-05 15:50:43 +00:00
Kim Morrison	d6cb2432c6	chore: remove unnecessary steps from release checklist (#4914 )	2024-08-05 01:57:30 +00:00
Kim Morrison	c0ffc85d75	chore: require docs in BitVec (#4913 )	2024-08-05 01:12:04 +00:00
Leonardo de Moura	f62359acc7	perf: use `lean_instantiate_level_mvars` (#4912 ) implemented in C/C++. Next step: same for `instantiateExprMVars`	2024-08-04 23:21:57 +00:00
Shuhao Song	2d09c96caf	chore: cli help text: comma-separate alternative option forms (#4911 ) The help message of Lean command line contains ``` --o=oname -o create olean file ``` This may lead to misunderstanding that the command needs both argument `--o=oname` and `-o`, i. e. `lean --o=test.o -o test.lean`. In the help message of GNU coreutils, such as `ls`, it is `-a, --all ...`, which might be better. Some discussion is on Zulip thread [https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/The.20help.20message.20of.20Lean.20command.20line](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/The.20help.20message.20of.20Lean.20command.20line).	2024-08-04 22:54:34 +00:00
Lean stage0 autoupdater	21b4377d36	chore: update stage0	2024-08-04 19:11:50 +00:00
Leonardo de Moura	1e9d96be22	perf: add `lean_instantiate_level_mvars` (#4910 ) The new code is not active yet because of bootstrapping issues. It requires an `update_stage0`.	2024-08-04 18:31:44 +00:00
Leonardo de Moura	647a5e9492	perf: use `NatPow Int` instead of `HPow Int Nat Int` (#4903 ) This modification improves the performance of the example in issue #4861. It no longer times out but is still expensive. Here is the analysis of the performance issue: Given `(x : Int)`, to elaborate `x ^ 1`, a few default instances have to be tried. First, the homogeneous instance is tried and fails since `Int` does not implement `Pow Int`. Then, the `NatPow` instance is tried, and it also fails. The same process is performed for each term of the form `p ^ 1`. There are seveal of them at #4861. After all of these fail, the lower priority default instance for numerals is tried, and `x ^ 1` becomes `x ^ (1 : Nat)`. Then, `HPow Int Nat Int` can be applied, and the elaboration succeeds. However, this process has to be repeated for every single term of the form `p ^ 1`. The elaborator tries all homogeneous `HPow` and `NatPow` instances for all `p ^ 1` terms before trying the lower priority default instance `OfNat`. This commit ensures `Int` has a `NatPow` instance instead of `HPow Int Nat Int`. This change shortcuts the process, but it still first tries the homogeneous `HPow` instance, fails, and then tries `NatPow`. The elaboration can be made much more efficient by writing `p ^ (1 : Nat)`.	2024-08-03 00:35:04 +00:00
Clement Courbet	9c4028aab4	perf: avoid expr copies in replace_rec_fn::apply (#4702 ) Those represent ~13% of the time spent in `save_result`, even though `r` is a temporary in all cases but one. See #4698 for details. --------- Co-authored-by: Leonardo de Moura <leomoura@amazon.com>	2024-08-02 18:32:36 +00:00
Clement Courbet	2c002718e0	perf: fix implementation of move constructors and move assignment ope… (#4700 ) …rators Right now those constructors result in a copy instead of the desired move. We've measured that expr copying and assignment by itself uses around 10% of total runtime on our workloads. See #4698 for details.	2024-08-02 17:55:03 +00:00
Sebastian Ullrich	b07384acbb	feat: accept user-defined options on the cmdline (#4741 ) Initial options are now re-parsed and validated after importing. Cmdline option assignments prefixed with `weak.` are silently discarded if the option name without the prefix does not exist. Fixes #3403	2024-08-02 12:24:56 +00:00
Sebastian Ullrich	efc99b982e	chore: deprecate Nix-based build, remove interactive components (#4895 ) Users who prefer the flake build should maintain it externally	2024-08-02 09:57:34 +00:00
Siddharth	ee430b6c80	feat: getLsb_replicate (#4873 ) This allows bitblasting `BitVec.replicate`. I changed the definition of `BitVec.replicate` to use `BitVec.cast` in order to make the proof smoother, since it's an easier time simplifying away terms with `BitVec.cast`. --------- Co-authored-by: Tobias Grosser <tobias@grosser.es>	2024-08-01 23:07:19 +00:00
Alok Singh	a8740f5ed9	doc: add docstring to `IO.FS.realpath` (#4648 ) Based on `IO.FS.rename` template.	2024-08-01 14:00:54 +00:00
Sebastian Ullrich	5e6a3cf5f9	chore: revert "fix: make import resolution case-sensitive on all platforms" (#4896 ) Reverts leanprover/lean4#4538 because of unexpected overhead	2024-08-01 13:55:37 +00:00
Sebastian Ullrich	0ed1cf7244	fix: `LEAN_EXPORT` in sharecommon (#4893 )	2024-08-01 13:03:25 +02:00
Lean stage0 autoupdater	e83f78d5af	chore: update stage0	2024-08-01 06:54:29 +00:00
David Thrane Christiansen	32b9de8c77	fix: export symbols needed by Verso (#4884 ) Verso needed a symbol that was unexported - this exposes it again.	2024-08-01 04:56:27 +00:00
Leonardo de Moura	a856016b9d	perf: precise cache for `expr_eq_fn` (#4890 ) This performance issue was exposed by the benchmarks at https://github.com/leanprover/LNSym/tree/proof_size_expt/Proofs/SHA512/Experiments	2024-08-01 02:56:41 +00:00
Siddharth	c517688f1d	feat: ushiftRight bitblasting (#4872 ) This adds theorems `ushiftRight_rec_zero`, `ushiftRight_rec_succ`, `ushiftRight_rec_eq`, and `shiftRight_eq_shiftRight_rec`. --------- Co-authored-by: Tobias Grosser <github@grosser.es>	2024-07-31 21:44:06 +00:00
Leonardo de Moura	db594425bf	refactor: `sharecommon` (#4887 ) This PR also fixes a missing borrow annotation.	2024-07-31 19:13:12 +00:00
Kim Morrison	dcea47db02	chore: shorten suggestion about diagnostics (#4882 ) This message is often incorporated into source files via `#guard_msgs`. This change ensures it won't go over the 100 character ruler, and I think is equally grammatical. :-)	2024-07-31 17:56:43 +00:00
Siddharth	f869902a4b	feat: Nat simprocs for simplifying bit expressions (#4874 ) This came up in the context of simplifying proof states for https://github.com/leanprover/LNSym.	2024-07-31 17:26:05 +00:00
Sebastian Ullrich	d5a8c9647f	fix: make import resolution case-sensitive on all platforms (#4538 ) Co-authored-by: Mac Malone <tydeu@hatpress.net>	2024-07-31 16:48:14 +00:00
Sebastian Ullrich	d19bab0c27	feat: `include` command (#4883 ) To be implemented in #4814	2024-07-31 13:25:54 +00:00