chore: bump patch version to 1

The namespace cache volumes were running out of space and preventing CI
from running.

.claude/commands/release.md

@@ -13,12 +13,54 @@ 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 exist
+   - Check for: release branch exists, CMake version correct, tag exists, release page exists, release notes file exists
    - **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,16 +66,10 @@ 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,6 +218,11 @@ 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.
@@ -232,4 +237,93 @@ 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,6 +185,30 @@ 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 {}
@@ -714,6 +738,27 @@ 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,13 +14,6 @@ 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
@@ -42,6 +35,14 @@ 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 0)
-set(LEAN_VERSION_IS_RELEASE 0)  # This number is 1 in the release revision, and 0 otherwise.
+set(LEAN_VERSION_PATCH 1)
+set(LEAN_VERSION_IS_RELEASE 1)  # 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,12 +543,10 @@ 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) := (← getNGen).mkChild
-  setNGen parentNGen
-  let (childDeclNGen, parentDeclNGen) := (← getDeclNGen).mkChild
-  setDeclNGen parentDeclNGen
+  let (childNGen, parentNGen) := (← getDeclNGen).mkChild
+  setDeclNGen parentNGen
   let st ← get
-  let st := { st with auxDeclNGen := childDeclNGen, ngen := childNGen }
+  let st := { st with auxDeclNGen := childNGen }
   let ctx ← read
   let ctx := { ctx with cancelTk? }
   let heartbeats := (← IO.getNumHeartbeats) - ctx.initHeartbeats

src/Lean/Elab/Command.lean

@@ -274,12 +274,10 @@ def wrapAsync {α β : Type} (act : α → CommandElabM β) (cancelTk? : Option
     CommandElabM (α → EIO Exception β) := do
   let ctx ← read
   let ctx := { ctx with cancelTk? }
-  let (childNGen, parentNGen) := (← get).ngen.mkChild
-  modify fun s => { s with ngen := parentNGen }
-  let (childDeclNGen, parentDeclNGen) := (← getDeclNGen).mkChild
-  setDeclNGen parentDeclNGen
+  let (childNGen, parentNGen) := (← getDeclNGen).mkChild
+  setDeclNGen parentNGen
   let st ← get
-  let st := { st with auxDeclNGen := childDeclNGen, ngen := childNGen }
+  let st := { st with auxDeclNGen := 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.
 -/
-def simpFixedPrefix (e : Expr) (prefixSize : Nat) (suffixSize : Nat) : SimpM Result := do
+public 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.
 -/
-def simpInterlaced (e : Expr) (rewritable : Array Bool) : SimpM Result := do
+public 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,4 +22,8 @@ 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,6 +324,55 @@ 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);
@@ -609,7 +658,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(sizeof(lean_ctor_object) + sizeof(void*)*num_objs + scalar_sz);
+    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_set_st_header(o, tag, num_objs);
     return o;
 }
@@ -715,7 +764,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(sizeof(lean_closure_object) + sizeof(void*)*num_fixed);
+    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_set_st_header((lean_object*)o, LeanClosure, 0);
     o->m_fun = fun;
     o->m_arity = arity;
@@ -761,7 +810,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(sizeof(lean_array_object) + sizeof(void*)*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_set_st_header((lean_object*)o, LeanArray, 0);
     o->m_size = size;
     o->m_capacity = capacity;
@@ -934,8 +983,18 @@ 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(sizeof(lean_sarray_object) + elem_size*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_set_st_header((lean_object*)o, LeanScalarArray, elem_size);
     o->m_size = size;
     o->m_capacity = capacity;
@@ -1090,7 +1149,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(sizeof(lean_string_object) + capacity);
+    lean_string_object * o = (lean_string_object*)lean_alloc_object(lean_usize_add_checked(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 = sizeof(lean_sarray_object) + elem_sz*sz;
+    size_t obj_sz = lean_usize_add_checked(sizeof(lean_sarray_object), lean_usize_mul_checked(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 = sizeof(lean_string_object) + sz;
+    size_t obj_sz = lean_usize_add_checked(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 = sizeof(lean_array_object) + sizeof(void*)*sz;
+    size_t obj_sz = lean_usize_add_checked(sizeof(lean_array_object), lean_usize_mul_checked(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 = sizeof(mp_limb_t) * nlimbs;
-    size_t sz = sizeof(mpz_object) + data_sz;
+    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);
     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 = sizeof(mpn_digit) * to_mpz(o)->m_value.m_size;
-    size_t sz      = sizeof(mpz_object) + data_sz;
+    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);
     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,6 +583,9 @@ 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) {
@@ -861,6 +864,9 @@ 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(s * sizeof(mpn_digit)));
+    m_digits = static_cast<mpn_digit*>(mpz_alloc(lean_usize_mul_checked(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(m_size * sizeof(mpn_digit)));
-    memcpy(m_digits, v.m_digits, m_size * sizeof(mpn_digit));
+    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)));
 }
 
 mpz::mpz() {

src/runtime/object.cpp

@@ -99,6 +99,10 @@ 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,6 +182,9 @@ 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,6 +140,9 @@ 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,6 +104,29 @@ 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`.
@@ -120,6 +143,7 @@ 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
@@ -127,9 +151,10 @@ 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
-    -- logInfo goal₀.mvarId
-    let .goals [goal] ← goal₀.apply execBindRule | return goal₀
+  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 .goals [goal] ← goal.apply execGetRule | failure
     let .goals [goal] ← goal.apply execBindRule | failure
     let .goals [goal] ← goal.apply execSetRule | failure
@@ -155,5 +180,10 @@ def solveUsingGrind (n : Nat) (check := true) : MetaM Unit := do
   driver n check fun mvarId => SymM.run <| GrindM.run (params := params) do
     solve mvarId
 
--- **TODO**: the proof term grows quadratically because we are not simplifying the state
-#eval solveUsingGrind 50
+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

tests/compiler/file_read_overflow.lean

@@ -0,0 +1,14 @@
+/-!
+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.4"]},
+   "data": ["«external:file:///533.lean»", 4, 10, 0, "f_uniq.3"]},
   {"label": "F",
    "kind": 6,
-   "data": ["«external:file:///533.lean»", 4, 10, 0, "f_uniq.8"]}],
+   "data": ["«external:file:///533.lean»", 4, 10, 0, "f_uniq.7"]}],
  "isIncomplete": false}
 Resolution of Foo:
 {"label": "Foo",
  "kind": 6,
  "detail": "Sort ?u",
- "data": ["«external:file:///533.lean»", 4, 10, 0, "f_uniq.4"]}
+ "data": ["«external:file:///533.lean»", 4, 10, 0, "f_uniq.3"]}
 Resolution of F:
 {"label": "F",
  "kind": 6,
  "detail": "Sort ?u",
- "data": ["«external:file:///533.lean»", 4, 10, 0, "f_uniq.8"]}
+ "data": ["«external:file:///533.lean»", 4, 10, 0, "f_uniq.7"]}

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.11"]},
+   "data": ["«external:file:///compHeader.lean»", 2, 22, 0, "f_uniq.7"]},
   {"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.11"]}
+ "data": ["«external:file:///compHeader.lean»", 2, 22, 0, "f_uniq.7"]}
 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.39"]},
+   ["«external:file:///completionPrefixIssue.lean»", 1, 64, 0, "f_uniq.35"]},
   {"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.39"]}
+ ["«external:file:///completionPrefixIssue.lean»", 1, 64, 0, "f_uniq.35"]}
 Resolution of veryLongDefinitionNameVeryLongDefinitionName:
 {"label": "veryLongDefinitionNameVeryLongDefinitionName",
  "kind": 21,

tests/lean/interactive/fvarIdCollision.lean

@@ -1,14 +0,0 @@
---^ 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

@@ -1,10 +0,0 @@
-{"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.35.3 @ ⟨1, 0⟩†-⟨1, 0⟩†
+                    • [Completion-Id] Nat.zero_le : some LE.le.{0} Nat instLENat (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) _uniq.37 @ ⟨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.4
+?_uniq.3
 -/
 #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.121} {a : α}, a = a
+  ∀ {α : Sort ?u.115} {a : α}, a = a
 
 Note: The following definitions were not unfolded because their definition is not exposed:
   f ↦ 1