chore: use SharedExprs

.claude/commands/release.md

@@ -13,54 +13,12 @@ These comments explain the scripts' behavior, which repositories get special han
 ## Arguments
 - `version`: The version to release (e.g., v4.24.0)
 
-## Release Notes (Required for -rc1 releases)
-
-For first release candidates (`-rc1`), you must create release notes BEFORE the reference-manual toolchain bump PR can be merged.
-
-**Steps to create release notes:**
-
-1. Generate the release notes:
-   ```bash
-   cd /path/to/lean4
-   python3 script/release_notes.py --since <previous_version> > /tmp/release-notes-<version>.md
-   ```
-   Replace `<previous_version>` with the last stable release (e.g., `v4.27.0` when releasing `v4.28.0-rc1`).
-
-2. Review `/tmp/release-notes-<version>.md` for common issues:
-   - **Unterminated code blocks**: Look for code fences that aren't closed. Fetch original PR with `gh pr view <number>` to repair.
-   - **Truncated descriptions**: Some may end mid-sentence. Complete them from the original PR.
-   - **Markdown issues**: Other syntax problems that could cause parsing errors.
-
-3. Create the release notes file in the reference-manual repository:
-   - File path: `Manual/Releases/v<version>.lean` (e.g., `v4_28_0.lean`)
-   - Use Verso format with proper imports and `#doc (Manual)` block
-   - **Use `#` for headers, not `##`** (Verso uses level 1 for subsections)
-   - **Use plain ` ``` ` not ` ```lean `** (the latter executes code)
-   - **Wrap underscore identifiers in backticks**: `` `bv_decide` `` not `bv_decide`
-
-4. Update `Manual/Releases.lean`:
-   - Add import: `import Manual.Releases.«v4_28_0»`
-   - Add include: `{include 0 Manual.Releases.«v4_28_0»}`
-
-5. Build to verify: `lake build Manual.Releases.v4_28_0`
-
-6. Create a **separate PR** for release notes (not bundled with toolchain bump):
-   ```bash
-   git checkout -b v<version>-release-notes
-   gh pr create --title "doc: add v<version> release notes"
-   ```
-
-For subsequent RCs (`-rc2`, etc.) and stable releases, just update the version number in the existing release notes file title.
-
-See `doc/dev/release_checklist.md` section "Writing the release notes" for full details.
-
 ## Process
 
 1. Run `script/release_checklist.py {version}` to check the current status
 2. **CRITICAL: If preliminary lean4 checks fail, STOP immediately and alert the user**
-   - Check for: release branch exists, CMake version correct, tag exists, release page exists, release notes file exists
+   - Check for: release branch exists, CMake version correct, tag exists, release page exists, release notes exist
    - **IMPORTANT**: The release page is created AUTOMATICALLY by CI after pushing the tag - DO NOT create it manually
-   - **IMPORTANT**: For -rc1 releases, release notes must be created before proceeding
    - Do NOT create any PRs or proceed with repository updates if these checks fail
 3. Create a todo list tracking all repositories that need updates
 4. **CRITICAL RULE: You can ONLY run `release_steps.py` for a repository if `release_checklist.py` explicitly says to do so**

.github/workflows/build-template.yml

@@ -66,10 +66,16 @@ jobs:
           brew install ccache tree zstd coreutils gmp libuv
         if: runner.os == 'macOS'
       - name: Checkout
+        if: (!endsWith(matrix.os, '-with-cache'))
         uses: actions/checkout@v6
         with:
           # the default is to use a virtual merge commit between the PR and master: just use the PR
           ref: ${{ github.event.pull_request.head.sha }}
+      - name: Namespace Checkout
+        if: endsWith(matrix.os, '-with-cache')
+        uses: namespacelabs/nscloud-checkout-action@v8
+        with:
+          ref: ${{ github.event.pull_request.head.sha }}
       - name: Open Nix shell once
         run: true
         if: runner.os == 'Linux'

doc/dev/release_checklist.md

@@ -218,11 +218,6 @@ Please read https://leanprover-community.github.io/contribute/tags_and_branches.
 
 # Writing the release notes
 
-Release notes are only needed for the first release candidate (`-rc1`). For subsequent RCs and stable releases,
-just update the version number in the title of the existing release notes file.
-
-## Generating the release notes
-
 Release notes are automatically generated from the commit history, using `script/release_notes.py`.
 
 Run this as `script/release_notes.py --since v4.6.0`, where `v4.6.0` is the *previous* release version.
@@ -237,93 +232,4 @@ Some judgement is required here: ignore commits which look minor,
 but manually add items to the release notes for significant PRs that were rebase-merged.
 
 There can also be pre-written entries in `./releases_drafts`, which should be all incorporated in the release notes and then deleted from the branch.
-
-## Reviewing and fixing the generated markdown
-
-Before adding the release notes to the reference manual, carefully review the generated markdown for these common issues:
-
-1. **Unterminated code blocks**: PR descriptions sometimes have unclosed code fences. Look for code blocks
-   that don't have a closing ` ``` `. If found, fetch the original PR description with `gh pr view <number>`
-   and repair the code block with the complete content.
-
-2. **Truncated descriptions**: Some PR descriptions may end abruptly mid-sentence. Review these and complete
-   the descriptions based on the original PR.
-
-3. **Markdown syntax issues**: Check for other markdown problems that could cause parsing errors.
-
-## Creating the release notes file
-
-The release notes go in `Manual/Releases/v4_7_0.lean` in the reference-manual repository.
-
-The file structure must follow the Verso format:
-
-```lean
-/-
-Copyright (c) 2025 Lean FRO LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: <Your Name>
--/
-
-import VersoManual
-import Manual.Meta
-import Manual.Meta.Markdown
-
-open Manual
-open Verso.Genre
-open Verso.Genre.Manual
-open Verso.Genre.Manual.InlineLean
-
-#doc (Manual) "Lean 4.7.0-rc1 (YYYY-MM-DD)" =>
-%%%
-tag := "release-v4.7.0"
-file := "v4.7.0"
-%%%
-
-<release notes content here>
-```
-
-**Important formatting rules for Verso:**
-- Use `#` for section headers inside the document, not `##` (Verso uses header level 1 for subsections)
-- Use plain ` ``` ` for code blocks, not ` ```lean ` (the latter will cause Lean to execute the code)
-- Identifiers with underscores like `bv_decide` should be wrapped in backticks: `` `bv_decide` ``
-  (otherwise the underscore may be interpreted as markdown emphasis)
-
-## Updating Manual/Releases.lean
-
-After creating the release notes file, update `Manual/Releases.lean` to include it:
-
-1. Add the import near the top with other version imports:
-   ```lean
-   import Manual.Releases.«v4_7_0»
-   ```
-
-2. Add the include statement after the other includes:
-   ```lean
-   {include 0 Manual.Releases.«v4_7_0»}
-   ```
-
-## Building and verifying
-
-Build the release notes to check for errors:
-```bash
-lake build Manual.Releases.v4_7_0
-```
-
-Common errors and fixes:
-- "Wrong header nesting - got ## but expected at most #": Change `##` to `#`
-- "Tactic 'X' failed" or similar: Code is being executed; change ` ```lean ` to ` ``` `
-- "'_'" errors: Underscore in identifier being parsed as emphasis; wrap in backticks
-
-## Creating the PR
-
-Create a separate PR for the release notes (don't bundle with the toolchain bump PR):
-```bash
-git checkout -b v4.7.0-release-notes
-git add Manual/Releases/v4_7_0.lean Manual/Releases.lean
-git commit -m "doc: add v4.7.0 release notes"
-git push -u origin v4.7.0-release-notes
-gh pr create --title "doc: add v4.7.0 release notes" --body "This PR adds the release notes for Lean v4.7.0."
-```
-
-See `./releases_drafts/README.md` for more information about pre-written release note entries.
 See `./releases_drafts/README.md` for more information.

script/release_checklist.py

@@ -185,30 +185,6 @@ def get_release_notes(tag_name):
     except Exception:
         return None
 
-def check_release_notes_file_exists(toolchain, github_token):
-    """Check if the release notes file exists in the reference-manual repository.
-
-    For -rc1 releases, this checks that the release notes have been created.
-    For subsequent RCs and stable releases, release notes should already exist.
-
-    Returns tuple (exists: bool, is_rc1: bool) where is_rc1 indicates if this is
-    the first release candidate (when release notes need to be written).
-    """
-    # Determine the release notes file path
-    # e.g., v4.28.0-rc1 -> Manual/Releases/v4_28_0.lean
-    base_version = strip_rc_suffix(toolchain.lstrip('v'))  # "4.28.0"
-    file_name = f"v{base_version.replace('.', '_')}.lean"  # "v4_28_0.lean"
-    file_path = f"Manual/Releases/{file_name}"
-
-    is_rc1 = toolchain.endswith("-rc1")
-
-    repo_url = "https://github.com/leanprover/reference-manual"
-
-    # Check if the file exists on main branch
-    content = get_branch_content(repo_url, "main", file_path, github_token)
-
-    return (content is not None, is_rc1)
-
 def get_branch_content(repo_url, branch, file_path, github_token):
     api_url = repo_url.replace("https://github.com/", "https://api.github.com/repos/") + f"/contents/{file_path}?ref={branch}"
     headers = {'Authorization': f'token {github_token}'} if github_token else {}
@@ -738,27 +714,6 @@ def main():
     else:
         print(f"  ✅ Release notes page title looks good ('{actual_title}').")
 
-    # Check if release notes file exists in reference-manual repository
-    # For -rc1 releases, this is when release notes need to be written
-    # For subsequent RCs and stable releases, they should already exist
-    release_notes_exists, is_rc1 = check_release_notes_file_exists(toolchain, github_token)
-    base_version = strip_rc_suffix(toolchain.lstrip('v'))
-    release_notes_file = f"Manual/Releases/v{base_version.replace('.', '_')}.lean"
-
-    if not release_notes_exists:
-        if is_rc1:
-            print(f"  ❌ Release notes file not found: {release_notes_file}")
-            print(f"     This is an -rc1 release, so release notes need to be written.")
-            print(f"     Run `script/release_notes.py --since <previous_version>` to generate them.")
-            print(f"     See doc/dev/release_checklist.md section 'Writing the release notes' for details.")
-            lean4_success = False
-        else:
-            print(f"  ❌ Release notes file not found: {release_notes_file}")
-            print(f"     Release notes should have been created for -rc1. Check the reference-manual repository.")
-            lean4_success = False
-    else:
-        print(f"  ✅ Release notes file exists: {release_notes_file}")
-
     repo_status["lean4"] = lean4_success
 
     # If the release page doesn't exist, skip repository checks and master branch checks

script/release_repos.yml

@@ -14,6 +14,13 @@ repositories:
     bump-branch: true
     dependencies: []
 
+  - name: verso
+    url: https://github.com/leanprover/verso
+    toolchain-tag: true
+    stable-branch: false
+    branch: main
+    dependencies: []
+
   - name: lean4checker
     url: https://github.com/leanprover/lean4checker
     toolchain-tag: true
@@ -35,14 +42,6 @@ repositories:
     branch: main
     dependencies: []
 
-  - name: verso
-    url: https://github.com/leanprover/verso
-    toolchain-tag: true
-    stable-branch: false
-    branch: main
-    dependencies:
-      - plausible
-
   - name: import-graph
     url: https://github.com/leanprover-community/import-graph
     toolchain-tag: true

src/CMakeLists.txt

@@ -11,8 +11,8 @@ include(ExternalProject)
 project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
 set(LEAN_VERSION_MINOR 28)
-set(LEAN_VERSION_PATCH 1)
-set(LEAN_VERSION_IS_RELEASE 1)  # This number is 1 in the release revision, and 0 otherwise.
+set(LEAN_VERSION_PATCH 0)
+set(LEAN_VERSION_IS_RELEASE 0)  # This number is 1 in the release revision, and 0 otherwise.
 set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")
 set(LEAN_VERSION_STRING "${LEAN_VERSION_MAJOR}.${LEAN_VERSION_MINOR}.${LEAN_VERSION_PATCH}")
 if (LEAN_SPECIAL_VERSION_DESC)

src/Lean/CoreM.lean

@@ -543,10 +543,12 @@ def logSnapshotTask (task : Language.SnapshotTask Language.SnapshotTree) : CoreM
 /-- Wraps the given action for use in `EIO.asTask` etc., discarding its final monadic state. -/
 def wrapAsync {α : Type} (act : α → CoreM β) (cancelTk? : Option IO.CancelToken) :
     CoreM (α → EIO Exception β) := do
-  let (childNGen, parentNGen) := (← getDeclNGen).mkChild
-  setDeclNGen parentNGen
+  let (childNGen, parentNGen) := (← getNGen).mkChild
+  setNGen parentNGen
+  let (childDeclNGen, parentDeclNGen) := (← getDeclNGen).mkChild
+  setDeclNGen parentDeclNGen
   let st ← get
-  let st := { st with auxDeclNGen := childNGen }
+  let st := { st with auxDeclNGen := childDeclNGen, ngen := childNGen }
   let ctx ← read
   let ctx := { ctx with cancelTk? }
   let heartbeats := (← IO.getNumHeartbeats) - ctx.initHeartbeats

src/Lean/Elab/Command.lean

@@ -274,10 +274,12 @@ def wrapAsync {α β : Type} (act : α → CommandElabM β) (cancelTk? : Option
     CommandElabM (α → EIO Exception β) := do
   let ctx ← read
   let ctx := { ctx with cancelTk? }
-  let (childNGen, parentNGen) := (← getDeclNGen).mkChild
-  setDeclNGen parentNGen
+  let (childNGen, parentNGen) := (← get).ngen.mkChild
+  modify fun s => { s with ngen := parentNGen }
+  let (childDeclNGen, parentDeclNGen) := (← getDeclNGen).mkChild
+  setDeclNGen parentDeclNGen
   let st ← get
-  let st := { st with auxDeclNGen := childNGen }
+  let st := { st with auxDeclNGen := childDeclNGen, ngen := childNGen }
   return (act · |>.run ctx |>.run' st)
 
 open Language in

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

@@ -224,7 +224,7 @@ position. However, the type is only meaningful (non-`default`) when `Result` is
 `.step`, since we only need types for constructing congruence proofs. This avoids
 unnecessary type inference when no rewriting occurs.
 -/
-public def simpFixedPrefix (e : Expr) (prefixSize : Nat) (suffixSize : Nat) : SimpM Result := do
+def simpFixedPrefix (e : Expr) (prefixSize : Nat) (suffixSize : Nat) : SimpM Result := do
   let numArgs := e.getAppNumArgs
   if numArgs ≤ prefixSize then
     -- Nothing to be done
@@ -274,7 +274,7 @@ Uses `rewritable[i]` to determine whether argument `i` should be simplified.
 For rewritable arguments, calls `simp` and uses `congrFun'`, `congrArg`, and `congr`; for fixed arguments,
 uses `congrFun` to propagate changes from earlier arguments.
 -/
-public def simpInterlaced (e : Expr) (rewritable : Array Bool) : SimpM Result := do
+def simpInterlaced (e : Expr) (rewritable : Array Bool) : SimpM Result := do
   let numArgs := e.getAppNumArgs
   if h : numArgs = 0 then
     -- Nothing to be done

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

@@ -22,8 +22,4 @@ public abbrev mkEqTransResult (e₁ : Expr) (e₂ : Expr) (h₁ : Expr) (r₂ :
   | .rfl done => return .step e₂ h₁ done
   | .step e₃ h₂ done => return .step e₃ (← mkEqTrans e₁ e₂ h₁ e₃ h₂) done
 
-public def Result.markAsDone : Result → Result
-  | .rfl _ => .rfl true
-  | .step e h _ => .step e h true
-
 end Lean.Meta.Sym.Simp

src/include/lean/lean.h

@@ -324,55 +324,6 @@ LEAN_EXPORT LEAN_NORETURN void lean_internal_panic(char const * msg);
 LEAN_EXPORT LEAN_NORETURN void lean_internal_panic_out_of_memory(void);
 LEAN_EXPORT LEAN_NORETURN void lean_internal_panic_unreachable(void);
 LEAN_EXPORT LEAN_NORETURN void lean_internal_panic_rc_overflow(void);
-LEAN_EXPORT LEAN_NORETURN void lean_internal_panic_overflow(void);
-
-static inline bool lean_usize_mul_would_overflow(size_t a, size_t b) {
-#if defined(__GNUC__) || defined(__clang__)
-    size_t r;
-    return __builtin_mul_overflow(a, b, &r);
-#else
-    return a != 0 && b > SIZE_MAX / a;
-#endif
-}
-
-static inline bool lean_usize_add_would_overflow(size_t a, size_t b) {
-#if defined(__GNUC__) || defined(__clang__)
-    size_t r;
-    return __builtin_add_overflow(a, b, &r);
-#else
-    return a > SIZE_MAX - b;
-#endif
-}
-
-static inline size_t lean_usize_mul_checked(size_t a, size_t b) {
-#if defined(__GNUC__) || defined(__clang__)
-    size_t r;
-    if (LEAN_UNLIKELY(__builtin_mul_overflow(a, b, &r))) {
-        lean_internal_panic_overflow();
-    }
-    return r;
-#else
-    if (a != 0 && b > SIZE_MAX / a) {
-        lean_internal_panic_overflow();
-    }
-    return a * b;
-#endif
-}
-
-static inline size_t lean_usize_add_checked(size_t a, size_t b) {
-#if defined(__GNUC__) || defined(__clang__)
-    size_t r;
-    if (LEAN_UNLIKELY(__builtin_add_overflow(a, b, &r))) {
-        lean_internal_panic_overflow();
-    }
-    return r;
-#else
-    if (a > SIZE_MAX - b) {
-        lean_internal_panic_overflow();
-    }
-    return a + b;
-#endif
-}
 
 static inline size_t lean_align(size_t v, size_t a) {
     return (v / a)*a + a * (v % a != 0);
@@ -658,7 +609,7 @@ static inline uint8_t * lean_ctor_scalar_cptr(lean_object * o) {
 
 static inline lean_object * lean_alloc_ctor(unsigned tag, unsigned num_objs, unsigned scalar_sz) {
     assert(tag <= LeanMaxCtorTag && num_objs < LEAN_MAX_CTOR_FIELDS && scalar_sz < LEAN_MAX_CTOR_SCALARS_SIZE);
-    lean_object * o = lean_alloc_ctor_memory(lean_usize_add_checked(lean_usize_add_checked(sizeof(lean_ctor_object), lean_usize_mul_checked(sizeof(void*), num_objs)), scalar_sz));
+    lean_object * o = lean_alloc_ctor_memory(sizeof(lean_ctor_object) + sizeof(void*)*num_objs + scalar_sz);
     lean_set_st_header(o, tag, num_objs);
     return o;
 }
@@ -764,7 +715,7 @@ static inline lean_object ** lean_closure_arg_cptr(lean_object * o) { return lea
 static inline lean_obj_res lean_alloc_closure(void * fun, unsigned arity, unsigned num_fixed) {
     assert(arity > 0);
     assert(num_fixed < arity);
-    lean_closure_object * o = (lean_closure_object*)lean_alloc_object(lean_usize_add_checked(sizeof(lean_closure_object), lean_usize_mul_checked(sizeof(void*), num_fixed)));
+    lean_closure_object * o = (lean_closure_object*)lean_alloc_object(sizeof(lean_closure_object) + sizeof(void*)*num_fixed);
     lean_set_st_header((lean_object*)o, LeanClosure, 0);
     o->m_fun = fun;
     o->m_arity = arity;
@@ -810,7 +761,7 @@ LEAN_EXPORT lean_object* lean_apply_m(lean_object* f, unsigned n, lean_object**
 
 /* Arrays of objects (low level API) */
 static inline lean_obj_res lean_alloc_array(size_t size, size_t capacity) {
-    lean_array_object * o = (lean_array_object*)lean_alloc_object(lean_usize_add_checked(sizeof(lean_array_object), lean_usize_mul_checked(sizeof(void*), capacity)));
+    lean_array_object * o = (lean_array_object*)lean_alloc_object(sizeof(lean_array_object) + sizeof(void*)*capacity);
     lean_set_st_header((lean_object*)o, LeanArray, 0);
     o->m_size = size;
     o->m_capacity = capacity;
@@ -983,18 +934,8 @@ LEAN_EXPORT lean_object * lean_mk_array(lean_obj_arg n, lean_obj_arg v);
 
 /* Array of scalars */
 
-static inline bool lean_alloc_sarray_would_overflow(unsigned elem_size, size_t capacity) {
-    if (lean_usize_mul_would_overflow(elem_size, capacity)) {
-        return true;
-    }
-    if (lean_usize_add_would_overflow(sizeof(lean_sarray_object), elem_size * capacity)) {
-        return true;
-    }
-    return false;
-}
-
 static inline lean_obj_res lean_alloc_sarray(unsigned elem_size, size_t size, size_t capacity) {
-    lean_sarray_object * o = (lean_sarray_object*)lean_alloc_object(lean_usize_add_checked(sizeof(lean_sarray_object), lean_usize_mul_checked(elem_size, capacity)));
+    lean_sarray_object * o = (lean_sarray_object*)lean_alloc_object(sizeof(lean_sarray_object) + elem_size*capacity);
     lean_set_st_header((lean_object*)o, LeanScalarArray, elem_size);
     o->m_size = size;
     o->m_capacity = capacity;
@@ -1149,7 +1090,7 @@ static inline lean_obj_res lean_float_array_set(lean_obj_arg a, b_lean_obj_arg i
 /* Strings */
 
 static inline lean_obj_res lean_alloc_string(size_t size, size_t capacity, size_t len) {
-    lean_string_object * o = (lean_string_object*)lean_alloc_object(lean_usize_add_checked(sizeof(lean_string_object), capacity));
+    lean_string_object * o = (lean_string_object*)lean_alloc_object(sizeof(lean_string_object) + capacity);
     lean_set_st_header((lean_object*)o, LeanString, 0);
     o->m_size = size;
     o->m_capacity = capacity;

src/runtime/compact.cpp

@@ -143,7 +143,7 @@ object * object_compactor::copy_object(object * o) {
 void object_compactor::insert_sarray(object * o) {
     size_t sz        = lean_sarray_size(o);
     unsigned elem_sz = lean_sarray_elem_size(o);
-    size_t obj_sz = lean_usize_add_checked(sizeof(lean_sarray_object), lean_usize_mul_checked(elem_sz, sz));
+    size_t obj_sz = sizeof(lean_sarray_object) + elem_sz*sz;
     lean_sarray_object * new_o = (lean_sarray_object*)alloc(obj_sz);
     lean_set_non_heap_header_for_big((lean_object*)new_o, LeanScalarArray, elem_sz);
     new_o->m_size     = sz;
@@ -155,7 +155,7 @@ void object_compactor::insert_sarray(object * o) {
 void object_compactor::insert_string(object * o) {
     size_t sz        = lean_string_size(o);
     size_t len       = lean_string_len(o);
-    size_t obj_sz = lean_usize_add_checked(sizeof(lean_string_object), sz);
+    size_t obj_sz = sizeof(lean_string_object) + sz;
     lean_string_object * new_o = (lean_string_object*)alloc(obj_sz);
     lean_set_non_heap_header_for_big((lean_object*)new_o, LeanString, 0);
     new_o->m_size     = sz;
@@ -214,7 +214,7 @@ bool object_compactor::insert_array(object * o) {
     }
     if (missing_children)
         return false;
-    size_t obj_sz = lean_usize_add_checked(sizeof(lean_array_object), lean_usize_mul_checked(sizeof(void*), sz));
+    size_t obj_sz = sizeof(lean_array_object) + sizeof(void*)*sz;
     lean_array_object * new_o = (lean_array_object*)alloc(obj_sz);
     lean_set_non_heap_header_for_big((lean_object*)new_o, LeanArray, 0);
     new_o->m_size     = sz;
@@ -274,8 +274,8 @@ bool object_compactor::insert_promise(object * o) {
 void object_compactor::insert_mpz(object * o) {
 #ifdef LEAN_USE_GMP
     size_t nlimbs = mpz_size(to_mpz(o)->m_value.m_val);
-    size_t data_sz = lean_usize_mul_checked(sizeof(mp_limb_t), nlimbs);
-    size_t sz = lean_usize_add_checked(sizeof(mpz_object), data_sz);
+    size_t data_sz = sizeof(mp_limb_t) * nlimbs;
+    size_t sz = sizeof(mpz_object) + data_sz;
     mpz_object * new_o = (mpz_object *)alloc(sz);
     memcpy(new_o, to_mpz(o), sizeof(mpz_object));
     lean_set_non_heap_header((lean_object*)new_o, sz, LeanMPZ, 0);
@@ -287,8 +287,8 @@ void object_compactor::insert_mpz(object * o) {
     m._mp_alloc = nlimbs;
     save(o, (lean_object*)new_o);
 #else
-    size_t data_sz = lean_usize_mul_checked(sizeof(mpn_digit), to_mpz(o)->m_value.m_size);
-    size_t sz      = lean_usize_add_checked(sizeof(mpz_object), data_sz);
+    size_t data_sz = sizeof(mpn_digit) * to_mpz(o)->m_value.m_size;
+    size_t sz      = sizeof(mpz_object) + data_sz;
     mpz_object * new_o = (mpz_object *)alloc(sz);
     // Manually copy the `mpz_object` to ensure `mpz` struct padding is left as
     // zero as prepared by `object_compactor::alloc`. `memcpy` would copy the

src/runtime/io.cpp

@@ -583,9 +583,6 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_truncate(b_obj_arg h) {
 /* Handle.read : (@& Handle) → USize → IO ByteArray */
 extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_read(b_obj_arg h, usize nbytes) {
     FILE * fp = io_get_handle(h);
-    if (lean_alloc_sarray_would_overflow(1, nbytes)) {
-        return io_result_mk_error(decode_io_error(ENOMEM, NULL));
-    }
     obj_res res = lean_alloc_sarray(1, 0, nbytes);
     usize n = std::fread(lean_sarray_cptr(res), 1, nbytes, fp);
     if (n > 0) {
@@ -864,9 +861,6 @@ extern "C" LEAN_EXPORT obj_res lean_io_get_random_bytes (size_t nbytes) {
     }
 #endif
 
-    if (lean_alloc_sarray_would_overflow(1, nbytes)) {
-        return io_result_mk_error(decode_io_error(ENOMEM, NULL));
-    }
     obj_res res = lean_alloc_sarray(1, 0, nbytes);
     size_t remain = nbytes;
     uint8_t *dst = lean_sarray_cptr(res);

src/runtime/mpz.cpp

@@ -340,7 +340,7 @@ static void mpz_dealloc(void *ptr, size_t size) {
 
 void mpz::allocate(size_t s) {
     m_size   = s;
-    m_digits = static_cast<mpn_digit*>(mpz_alloc(lean_usize_mul_checked(s, sizeof(mpn_digit))));
+    m_digits = static_cast<mpn_digit*>(mpz_alloc(s * sizeof(mpn_digit)));
 }
 
 void mpz::init() {
@@ -409,8 +409,8 @@ void mpz::init_int64(int64 v) {
 void mpz::init_mpz(mpz const & v) {
     m_sign   = v.m_sign;
     m_size   = v.m_size;
-    m_digits = static_cast<mpn_digit*>(mpz_alloc(lean_usize_mul_checked(m_size, sizeof(mpn_digit))));
-    memcpy(m_digits, v.m_digits, lean_usize_mul_checked(m_size, sizeof(mpn_digit)));
+    m_digits = static_cast<mpn_digit*>(mpz_alloc(m_size * sizeof(mpn_digit)));
+    memcpy(m_digits, v.m_digits, m_size * sizeof(mpn_digit));
 }
 
 mpz::mpz() {

src/runtime/object.cpp

@@ -99,10 +99,6 @@ extern "C" LEAN_EXPORT void lean_internal_panic_rc_overflow() {
     lean_internal_panic("reference counter overflowed");
 }
 
-extern "C" LEAN_EXPORT void lean_internal_panic_overflow() {
-    lean_internal_panic("integer overflow in runtime computation");
-}
-
 bool g_exit_on_panic = false;
 bool g_panic_messages = true;
 

src/runtime/uv/tcp.cpp

@@ -182,9 +182,6 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_send(b_obj_arg socket, obj_arg d
     }
 
     // Allocate buffer array for uv_write
-    if (lean_usize_mul_would_overflow(array_len, sizeof(uv_buf_t))) {
-        return lean_io_result_mk_error(decode_io_error(ENOMEM, nullptr));
-    }
     uv_buf_t* bufs = (uv_buf_t*)malloc(array_len * sizeof(uv_buf_t));
 
     for (size_t i = 0; i < array_len; i++) {

src/runtime/uv/udp.cpp

@@ -140,9 +140,6 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_send(b_obj_arg socket, obj_arg d
         return lean_io_result_mk_ok(promise);
     }
 
-    if (lean_usize_mul_would_overflow(array_len, sizeof(uv_buf_t))) {
-        return lean_io_result_mk_error(decode_io_error(ENOMEM, nullptr));
-    }
     uv_buf_t* bufs = (uv_buf_t*)malloc(array_len * sizeof(uv_buf_t));
 
     for (size_t i = 0; i < array_len; i++) {

tests/bench/sym/shallow_add_sub_cancel_grind.lean

@@ -104,29 +104,6 @@ def isBind (goal : Goal) : MetaM Bool := do
   let_expr Exec _ _ _ k _ := target | return false
   return k.isAppOf ``Bind.bind
 
-def simpExecState : Sym.Simp.Simproc := fun e =>
-  /-
-  **Remark**: This simproc demonstrates how to perform targeted simplification steps using `Sym.simp`.
-  We only want to simplify the third argument of an `Exec`-application. We accomplished that
-  by using this simproc as a pre-method, using `simpInterlaced` where the `rewritable` mask
-  instructs the function to rewrite only the third argument, and then mark the resulting term
-  as simplified.
-  -/
-  let_expr Exec _ _ _ _ _ := e | return .rfl
-  -- Simplifies only the state (the third argument)
-  return (← Simp.simpInterlaced e #[false, false, true, false, false]).markAsDone
-
-theorem add_assoc_rev (a b c : Nat) : a + (b + c) = (a + b) + c := by simp +arith
-
-def mkSimpExecStateMethods : MetaM Sym.Simp.Methods := do
-  -- **Note**: we don't have `simp +arith` in `Sym.simp` yet. This is just a cheap hack
-  -- allow `Sym.simp` to simplify terms such as `2 + (1 + s)`.
-  let thm ← Sym.Simp.mkTheoremFromDecl ``add_assoc_rev
-  return {
-    pre  := simpExecState
-    post := Sym.Simp.evalGround.andThen thm.rewrite
-  }
-
 partial def solve (mvarId : MVarId) : GrindM Unit := do
   /-
   Creates an `BackwardRule` for each theorem `T` we want to use `apply T`.
@@ -143,7 +120,6 @@ partial def solve (mvarId : MVarId) : GrindM Unit := do
   -/
   let preMethods ← mkSimpMethods #[``step.eq_1, ``loop.eq_1, ``loop.eq_2,
     ``Nat.add_zero, ``Nat.sub_zero, ``bind_pure_comp, ``map_bind, ``id_map', ``unit_map, ``bind_assoc]
-  let execStateMethods ← mkSimpExecStateMethods
   -- ## Initialize
   let goal ← mkGoal mvarId
   let .goal _ goal ← goal.introN 1 | failure
@@ -151,10 +127,9 @@ partial def solve (mvarId : MVarId) : GrindM Unit := do
   let goal ← goal.internalizeAll -- Internalize all hypotheses
   -- ## Loop
   -- We simulate the `repeat` block using a tail-recursive function `loop`
-  let rec loop (goal : Goal) : GrindM Goal := do
-    let .goal goal ← goal.simpIgnoringNoProgress execStateMethods | failure
-    -- logInfo goal.mvarId
-    let .goals [goal] ← goal.apply execBindRule | return goal
+  let rec loop (goal₀ : Goal) : GrindM Goal := do
+    -- logInfo goal₀.mvarId
+    let .goals [goal] ← goal₀.apply execBindRule | return goal₀
     let .goals [goal] ← goal.apply execGetRule | failure
     let .goals [goal] ← goal.apply execBindRule | failure
     let .goals [goal] ← goal.apply execSetRule | failure
@@ -180,10 +155,5 @@ def solveUsingGrind (n : Nat) (check := true) : MetaM Unit := do
   driver n check fun mvarId => SymM.run <| GrindM.run (params := params) do
     solve mvarId
 
-def runBenchUsingGrind : MetaM Unit := do
-  IO.println "=== Symbolic Simulation Tests ==="
-  IO.println ""
-  for n in [10, 20, 30, 40, 50, 60, 70, 80, 90, 100, 110, 120, 130, 140, 150] do
-    solveUsingGrind n
-
-#eval runBenchUsingGrind
+-- **TODO**: the proof term grows quadratically because we are not simplifying the state
+#eval solveUsingGrind 50

tests/compiler/file_read_overflow.lean

@@ -1,14 +0,0 @@
-/-!
-This issue is a minimal reproducer for #13388 which now throws an out of memory error.
--/
-
-def main : IO UInt32 := do
-  let (h, _) ← IO.FS.createTempFile
-  let n : USize := (0 : USize) - (1 : USize)
-  try
-    discard <| h.read n
-    return 1
-  catch e =>
-    match e with
-    | .resourceExhausted .. => return 0
-    | _ => return 1

tests/lean/interactive/533.lean.expected.out

@@ -3,18 +3,18 @@
 {"items":
  [{"label": "Foo",
    "kind": 6,
-   "data": ["«external:file:///533.lean»", 4, 10, 0, "f_uniq.3"]},
+   "data": ["«external:file:///533.lean»", 4, 10, 0, "f_uniq.4"]},
   {"label": "F",
    "kind": 6,
-   "data": ["«external:file:///533.lean»", 4, 10, 0, "f_uniq.7"]}],
+   "data": ["«external:file:///533.lean»", 4, 10, 0, "f_uniq.8"]}],
  "isIncomplete": false}
 Resolution of Foo:
 {"label": "Foo",
  "kind": 6,
  "detail": "Sort ?u",
- "data": ["«external:file:///533.lean»", 4, 10, 0, "f_uniq.3"]}
+ "data": ["«external:file:///533.lean»", 4, 10, 0, "f_uniq.4"]}
 Resolution of F:
 {"label": "F",
  "kind": 6,
  "detail": "Sort ?u",
- "data": ["«external:file:///533.lean»", 4, 10, 0, "f_uniq.7"]}
+ "data": ["«external:file:///533.lean»", 4, 10, 0, "f_uniq.8"]}

tests/lean/interactive/compHeader.lean.expected.out

@@ -3,7 +3,7 @@
 {"items":
  [{"label": "veryLongNam",
    "kind": 6,
-   "data": ["«external:file:///compHeader.lean»", 2, 22, 0, "f_uniq.7"]},
+   "data": ["«external:file:///compHeader.lean»", 2, 22, 0, "f_uniq.11"]},
   {"label": "veryLongNameForCompletion",
    "kind": 21,
    "data":
@@ -17,7 +17,7 @@ Resolution of veryLongNam:
 {"label": "veryLongNam",
  "kind": 6,
  "detail": "Sort u_1",
- "data": ["«external:file:///compHeader.lean»", 2, 22, 0, "f_uniq.7"]}
+ "data": ["«external:file:///compHeader.lean»", 2, 22, 0, "f_uniq.11"]}
 Resolution of veryLongNameForCompletion:
 {"label": "veryLongNameForCompletion",
  "kind": 21,

tests/lean/interactive/completionPrefixIssue.lean.expected.out

@@ -4,7 +4,7 @@
  [{"label": "veryLongDefinitionName",
    "kind": 6,
    "data":
-   ["«external:file:///completionPrefixIssue.lean»", 1, 64, 0, "f_uniq.35"]},
+   ["«external:file:///completionPrefixIssue.lean»", 1, 64, 0, "f_uniq.39"]},
   {"label": "veryLongDefinitionNameVeryLongDefinitionName",
    "kind": 21,
    "data":
@@ -19,7 +19,7 @@ Resolution of veryLongDefinitionName:
  "kind": 6,
  "detail": "Nat",
  "data":
- ["«external:file:///completionPrefixIssue.lean»", 1, 64, 0, "f_uniq.35"]}
+ ["«external:file:///completionPrefixIssue.lean»", 1, 64, 0, "f_uniq.39"]}
 Resolution of veryLongDefinitionNameVeryLongDefinitionName:
 {"label": "veryLongDefinitionNameVeryLongDefinitionName",
  "kind": 21,

tests/lean/interactive/fvarIdCollision.lean

@@ -0,0 +1,14 @@
+--^ waitForILeans
+
+-- Regression test for a bug where (due to parallelism) the fvar ids weren't unique for the whole
+-- module, leading to a conflict between `i` of `lt_next'` and the fvar id for `prev'`, thus
+-- making go to definition jump to the wrong location.
+
+theorem lt_next' (s : Substring.Raw) (i : String.Pos.Raw) (h : i.1 < s.bsize) :
+    i.1 < (s.next i).1 := by
+  sorry
+
+def prev' : Substring.Raw → String.Pos.Raw → String.Pos.Raw := sorry
+
+#check prev'
+       --^ textDocument/definition

tests/lean/interactive/fvarIdCollision.lean.expected.out

@@ -0,0 +1,10 @@
+{"textDocument": {"uri": "file:///fvarIdCollision.lean"},
+ "position": {"line": 12, "character": 9}}
+[{"targetUri": "file:///fvarIdCollision.lean",
+  "targetSelectionRange":
+  {"start": {"line": 10, "character": 4}, "end": {"line": 10, "character": 9}},
+  "targetRange":
+  {"start": {"line": 10, "character": 4}, "end": {"line": 10, "character": 9}},
+  "originSelectionRange":
+  {"start": {"line": 12, "character": 7},
+   "end": {"line": 12, "character": 12}}}]

tests/lean/run/info_trees.lean

@@ -62,7 +62,7 @@ info: • [Command] @ ⟨79, 0⟩-⟨79, 40⟩ @ Lean.Elab.Command.elabDeclarati
                   ⊢ 0 ≤ n
                   after no goals
                   • [Term] Nat.zero_le n : 0 ≤ n @ ⟨1, 1⟩†-⟨1, 1⟩† @ Lean.Elab.Term.elabApp
-                    • [Completion-Id] Nat.zero_le : some LE.le.{0} Nat instLENat (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) _uniq.37 @ ⟨1, 0⟩†-⟨1, 0⟩†
+                    • [Completion-Id] Nat.zero_le : some LE.le.{0} Nat instLENat (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) _uniq.35.3 @ ⟨1, 0⟩†-⟨1, 0⟩†
                     • [Term] Nat.zero_le : ∀ (n : Nat), 0 ≤ n @ ⟨1, 0⟩†-⟨1, 0⟩†
                     • [Term] n : Nat @ ⟨1, 5⟩†-⟨1, 5⟩† @ Lean.Elab.Term.elabIdent
                       • [Completion-Id] n : some Nat @ ⟨1, 5⟩†-⟨1, 5⟩†

tests/lean/run/kernelErrorFollowup.lean

@@ -13,7 +13,7 @@ theorem zero_eq_one : 0 = 1 := bad.elim
 
 /--
 info: def bad : Empty :=
-?_uniq.3
+?_uniq.4
 -/
 #guard_msgs in
 set_option pp.raw true in

tests/pkg/module/Module/Imported.lean

@@ -35,7 +35,7 @@ with the goal
   f = 1
 
 Note: The full type of `@rfl` is
-  ∀ {α : Sort ?u.115} {a : α}, a = a
+  ∀ {α : Sort ?u.121} {a : α}, a = a
 
 Note: The following definitions were not unfolded because their definition is not exposed:
   f ↦ 1