test: and fix

.claude/CLAUDE.md

@@ -1,47 +1,6 @@
-(In the following, use `sysctl -n hw.logicalcpu` instead of `nproc` on macOS)
+To build Lean you should use `make -j -C build/release`.
 
-## Building
-
-To build Lean you should use `make -j$(nproc) -C build/release`.
-
-The build uses `ccache`, and in a sandbox `ccache` may complain about read-only file systems.
-Use `CCACHE_READONLY` and `CCACHE_TEMPDIR` instead of disabling ccache completely.
-
-## Running Tests
-
-See `tests/README.md` for full documentation. Quick reference:
-
-```bash
-# Full test suite (use after builds to verify correctness)
-CTEST_PARALLEL_LEVEL="$(nproc)" CTEST_OUTPUT_ON_FAILURE=1 \
-make -C build/release -j "$(nproc)" test
-
-# Specific test by name (supports regex via ctest -R)
-CTEST_PARALLEL_LEVEL="$(nproc)" CTEST_OUTPUT_ON_FAILURE=1 \
-make -C build/release -j "$(nproc)" test ARGS='-R grind_ematch'
-
-# Rerun only previously failed tests
-CTEST_PARALLEL_LEVEL="$(nproc)" CTEST_OUTPUT_ON_FAILURE=1 \
-make -C build/release -j "$(nproc)" test ARGS='--rerun-failed'
-
-# Single test from tests/foo/bar/ (quick check during development)
-CTEST_PARALLEL_LEVEL="$(nproc)" CTEST_OUTPUT_ON_FAILURE=1 \
-make -C build/release -j "$(nproc)" test ARGS=-R testname'
-```
-
-## Testing stage 2
-
-When requested to test stage 2, build it as follows:
-```
-make -C build/release stage2 -j$(nproc)
-```
-Stage 2 is *not* automatically invalidated by changes to `src/` which allows for faster iteration
-when fixing a specific file in the stage 2 build but for invalidating any files that already passed
-the stage 2 build as well as for final validation,
-```
-make -C build/release/stage2 clean-stdlib
-```
-must be run manually before building.
+To run a test you should use `cd tests/lean/run && ./test_single.sh example_test.lean`.
 
 ## New features
 
@@ -50,6 +9,8 @@ When asked to implement new features:
 * write comprehensive tests first (expecting that these will initially fail)
 * and then iterate on the implementation until the tests pass.
 
+All new tests should go in `tests/lean/run/`. These tests don't have expected output; we just check there are no errors. You should use `#guard_msgs` to check for specific messages.
+
 ## Success Criteria
 
 *Never* report success on a task unless you have verified both a clean build without errors, and that the relevant tests pass.
@@ -57,13 +18,9 @@ When asked to implement new features:
 ## Build System Safety
 
 **NEVER manually delete build directories** (build/, stage0/, stage1/, etc.) even when builds fail.
-- ONLY use the project's documented build command: `make -j$(nproc) -C build/release`
+- ONLY use the project's documented build command: `make -j -C build/release`
 - If a build is broken, ask the user before attempting any manual cleanup
 
-## stage0 Is a Copy of src
-
-**Never manually edit files under `stage0/`.** The `stage0/` directory is a snapshot of `src/` produced by `make update-stage0`. To change anything in stage0 (CMakeLists.txt, C++ source, etc.), edit the corresponding file in `src/` and let `update-stage0` propagate it.
-
 ## LSP and IDE Diagnostics
 
 After rebuilding, LSP diagnostics may be stale until the user interacts with files. Trust command-line test results over IDE diagnostics.
@@ -72,59 +29,6 @@ After rebuilding, LSP diagnostics may be stale until the user interacts with fil
 
 If the user expresses frustration with you, stop and ask them to help update this `.claude/CLAUDE.md` file with missing guidance.
 
-## Creating pull requests
+## Creating pull requests.
 
-Follow the commit convention in `doc/dev/commit_convention.md`.
-
-**Title format:** `<type>: <subject>` where type is one of: `feat`, `fix`, `doc`, `style`, `refactor`, `test`, `chore`, `perf`.
-Subject should use imperative present tense ("add" not "added"), no capitalization, no trailing period.
-
-**Body format:** The first paragraph must start with "This PR". This paragraph is automatically incorporated into release notes. Use imperative present tense. Include motivation and contrast with previous behavior when relevant. Do NOT use markdown headings (`## Summary`, `## Test plan`, etc.) in PR bodies.
-
-Example:
-```
-feat: add optional binder limit to `mkPatternFromTheorem`
-
-This PR adds a `num?` parameter to `mkPatternFromTheorem` to control how many
-leading quantifiers are stripped when creating a pattern.
-```
-
-**Changelog labels:** Add one `changelog-*` label to categorize the PR for release notes:
-- `changelog-language` - Language features and metaprograms
-- `changelog-tactics` - User facing tactics
-- `changelog-server` - Language server, widgets, and IDE extensions
-- `changelog-pp` - Pretty printing
-- `changelog-library` - Library
-- `changelog-compiler` - Compiler, runtime, and FFI
-- `changelog-lake` - Lake
-- `changelog-doc` - Documentation
-- `changelog-ffi` - FFI changes
-- `changelog-other` - Other changes
-- `changelog-no` - Do not include this PR in the release changelog
-
-If you're unsure which label applies, it's fine to omit the label and let reviewers add it.
-
-## Module System for `src/` Files
-
-Files in `src/Lean/`, `src/Std/`, and `src/lake/Lake/` must have both `module` and `prelude` (CI enforces `^prelude$` on its own line). With `prelude`, nothing is auto-imported — you must explicitly import `Init.*` modules for standard library features. Check existing files in the same directory for the pattern, e.g.:
-
-```lean
-module
-
-prelude
-import Init.While  -- needed for while/repeat
-import Init.Data.String.TakeDrop  -- needed for String.startsWith
-public import Lean.Compiler.NameMangling  -- public if types are used in public signatures
-```
-
-Files outside these directories (e.g. `tests/`, `script/`) use just `module`.
-
-## CI Log Retrieval
-
-When CI jobs fail, investigate immediately - don't wait for other jobs to complete. Individual job logs are often available even while other jobs are still running. Try `gh run view <run-id> --log` or `gh run view <run-id> --log-failed`, or use `gh run view <run-id> --job=<job-id>` to target the specific failed job. Sleeping is fine when asked to monitor CI and no failures exist yet, but once any job fails, investigate that failure immediately.
-
-## Copyright Headers
-
-New files require a copyright header. To get the year right, always run `date +%Y` rather than relying on memory. The copyright holder should be the author or their current employer — check other recent files by the same author in the repository to determine the correct entity (e.g., "Lean FRO, LLC", "Amazon.com, Inc. or its affiliates").
-
-Test files (in `tests/`) do not need copyright headers.
+All PRs must have a first paragraph starting with "This PR". This paragraph is automatically incorporated into release notes. Read `lean4/doc/dev/commit_convention.md` when making PRs.

.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**
@@ -103,60 +61,6 @@ Every time you run `release_checklist.py`, you MUST:
 This summary should be provided EVERY time you run the checklist, not just after creating new PRs.
 The user needs to see the complete picture of what's waiting for review.
 
-## Checking PR Status When Asked
-
-When the user asks for "status" or you need to report on PRs between checklist runs:
-- **ALWAYS check actual PR state** using `gh pr view <number> --repo <repo> --json state,mergedAt`
-- Do NOT rely on cached CI results or previous checklist output
-- The user may have merged PRs since your last check
-- Report which PRs are MERGED, which are OPEN with CI status, and which are still pending
-- After discovering merged PRs, rerun `release_checklist.py` to advance the release process
-
-## Nightly Infrastructure
-
-The nightly build system uses branches and tags across two repositories:
-
-- `leanprover/lean4` has **branches** `nightly` and `nightly-with-mathlib` tracking the latest nightly builds
-- `leanprover/lean4-nightly` has **dated tags** like `nightly-2026-01-23`
-
-When a nightly succeeds with mathlib, all three should point to the same commit. Don't confuse these: branches are in the main lean4 repo, dated tags are in lean4-nightly.
-
-## CI Failures: Investigate Immediately
-
-**CRITICAL: If the checklist reports `❌ CI: X check(s) failing` for any PR, investigate immediately.**
-
-Do NOT:
-- Report it as "CI in progress" or "some checks pending"
-- Wait for the remaining checks to finish before investigating
-- Assume it's a transient failure without checking
-
-DO:
-1. Run `gh pr checks <number> --repo <owner>/<repo>` to see which specific check failed
-2. Run `gh run view <run-id> --repo <owner>/<repo> --log-failed` to see the failure output
-3. Diagnose the failure and report clearly to the user: what failed and why
-4. Propose a fix if one is obvious (e.g., subverso version mismatch, transient elan install error)
-
-The checklist now distinguishes `❌ X check(s) failing, Y still in progress` from `🔄 Y check(s) in progress`.
-Any `❌` in CI status requires immediate investigation — do not move on.
-
-## Waiting for CI or Merges
-
-Use `gh pr checks --watch` to block until a PR's CI checks complete (no polling needed).
-Run these as background bash commands so you get notified when they finish:
-
-```bash
-# Watch CI, then check merge state
-gh pr checks <number> --repo <owner>/<repo> --watch && gh pr view <number> --repo <owner>/<repo> --json state --jq '.state'
-```
-
-For multiple PRs, launch one background command per PR in parallel. When each completes,
-you'll be notified automatically via a task-notification. Do NOT use sleep-based polling
-loops — `--watch` is event-driven and exits as soon as checks finish.
-
-Note: `gh pr checks --watch` exits as soon as ALL checks complete (pass or fail). If some checks
-fail while others are still running, `--watch` will continue until everything settles, then exit
-with a non-zero code. So a background `--watch` finishing = all checks done; check which failed.
-
 ## Error Handling
 
 **CRITICAL**: If something goes wrong or a command fails:

.claude/settings.json

@@ -1,13 +0,0 @@
-{
-  "extraKnownMarketplaces": {
-    "leanprover": {
-      "source": {
-        "source": "github",
-        "repo": "leanprover/skills"
-      }
-    }
-  },
-  "enabledPlugins": {
-    "lean@leanprover": true
-  }
-}

.claude/skills/profiling/SKILL.md

@@ -1,26 +0,0 @@
----
-name: profiling
-description: Profile Lean programs with demangled names using samply and Firefox Profiler. Use when the user asks to profile a Lean binary or investigate performance.
-allowed-tools: Bash, Read, Glob, Grep
----
-
-# Profiling Lean Programs
-
-Full documentation: `script/PROFILER_README.md`.
-
-## Quick Start
-
-```bash
-script/lean_profile.sh ./build/release/stage1/bin/lean some_file.lean
-```
-
-Requires `samply` (`cargo install samply`) and `python3`.
-
-## Agent Notes
-
-- The pipeline is interactive (serves to browser at the end). When running non-interactively, run the steps manually instead of using the wrapper script.
-- The three steps are: `samply record --save-only`, `symbolicate_profile.py`, then `serve_profile.py`.
-- `lean_demangle.py` works standalone as a stdin filter (like `c++filt`) for quick name lookups.
-- The `--raw` flag on `lean_demangle.py` gives exact demangled names without postprocessing (keeps `._redArg`, `._lam_0` suffixes as-is).
-- Use `PROFILE_KEEP=1` to keep the temp directory for later inspection.
-- The demangled profile is a standard Firefox Profiler JSON. Function names live in `threads[i].stringArray`, indexed by `threads[i].funcTable.name`.

.claude/skills/zulip-extract/SKILL.md

@@ -1,17 +0,0 @@
----
-name: zulip-extract
-description: Extract Zulip thread HTML dumps into readable plain text. Use when the user provides a Zulip HTML file or asks to parse/read/convert/summarize a Zulip thread.
----
-
-# Zulip Thread Extractor
-
-Run the bundled script to convert a Zulip HTML page dump into plain text.
-
-## Usage
-```bash
-python3 .claude/skills/zulip-extract/zulip_thread_extract.py input.html output.txt
-```
-
-The script has zero dependencies beyond Python 3 stdlib.
-It extracts sender, timestamp, message content (with code blocks,
-links, quotes, mentions), and reactions.

.claude/skills/zulip-extract/zulip_thread_extract.py

@@ -1,313 +0,0 @@
-#!/usr/bin/env python3
-"""
-Convert a Zulip HTML page dump to plain text (the visible message thread).
-
-Zero external dependencies — uses only the Python standard library.
-
-Usage:
-    python3 zulip_thread_extract.py input.html [output.txt]
-"""
-
-import sys
-import re
-from html.parser import HTMLParser
-from html import unescape
-
-
-# ---------------------------------------------------------------------------
-# Minimal DOM built from stdlib HTMLParser
-# ---------------------------------------------------------------------------
-
-class Node:
-    """A lightweight DOM node."""
-    __slots__ = ('tag', 'attrs', 'children', 'parent', 'text')
-
-    def __init__(self, tag='', attrs=None):
-        self.tag = tag
-        self.attrs = dict(attrs) if attrs else {}
-        self.children = []
-        self.parent = None
-        self.text = ''  # for text nodes only (tag == '')
-
-    @property
-    def cls(self):
-        return self.attrs.get('class', '')
-
-    def has_class(self, c):
-        return c in self.cls.split()
-
-    def find_all(self, tag=None, class_=None):
-        """Depth-first search for matching descendants."""
-        for child in self.children:
-            if child.tag == '':
-                continue
-            match = True
-            if tag and child.tag != tag:
-                match = False
-            if class_ and not child.has_class(class_):
-                match = False
-            if match:
-                yield child
-            yield from child.find_all(tag, class_)
-
-    def find(self, tag=None, class_=None):
-        return next(self.find_all(tag, class_), None)
-
-    def get_text(self):
-        if self.tag == '':
-            return self.text
-        return ''.join(c.get_text() for c in self.children)
-
-
-class DOMBuilder(HTMLParser):
-    """Build a minimal DOM tree from HTML."""
-
-    VOID_ELEMENTS = frozenset([
-        'area', 'base', 'br', 'col', 'embed', 'hr', 'img', 'input',
-        'link', 'meta', 'param', 'source', 'track', 'wbr',
-    ])
-
-    def __init__(self):
-        super().__init__()
-        self.root = Node('root')
-        self._cur = self.root
-
-    def handle_starttag(self, tag, attrs):
-        node = Node(tag, attrs)
-        node.parent = self._cur
-        self._cur.children.append(node)
-        if tag not in self.VOID_ELEMENTS:
-            self._cur = node
-
-    def handle_endtag(self, tag):
-        # Walk up to find the matching open tag (tolerates misnesting)
-        n = self._cur
-        while n and n.tag != tag and n.parent:
-            n = n.parent
-        if n and n.parent:
-            self._cur = n.parent
-
-    def handle_data(self, data):
-        t = Node()
-        t.text = data
-        t.parent = self._cur
-        self._cur.children.append(t)
-
-    def handle_entityref(self, name):
-        self.handle_data(unescape(f'&{name};'))
-
-    def handle_charref(self, name):
-        self.handle_data(unescape(f'&#{name};'))
-
-
-def parse_html(path):
-    with open(path, 'r', encoding='utf-8') as f:
-        html = f.read()
-    builder = DOMBuilder()
-    builder.feed(html)
-    return builder.root
-
-
-# ---------------------------------------------------------------------------
-# Content extraction
-# ---------------------------------------------------------------------------
-
-SKIP_CLASSES = {
-    'message_controls', 'message_length_controller',
-    'code-buttons-container', 'copy_codeblock', 'code_external_link',
-    'message_edit_notice', 'edit-notifications',
-}
-
-def should_skip(node):
-    return bool(SKIP_CLASSES & set(node.cls.split()))
-
-
-def extract_content(node):
-    """Recursively convert a message_content node into readable text."""
-    parts = []
-    for child in node.children:
-        # Text node
-        if child.tag == '':
-            parts.append(child.text)
-            continue
-
-        if should_skip(child):
-            continue
-
-        cls_set = set(child.cls.split())
-
-        # Code block wrappers  (div.codehilite / div.zulip-code-block)
-        if child.tag == 'div' and ({'codehilite', 'zulip-code-block'} & cls_set):
-            code = child.find('code')
-            lang = child.attrs.get('data-code-language', '')
-            text = code.get_text() if code else child.get_text()
-            parts.append(f'\n```{lang}\n{text}```\n')
-            continue
-
-        # <pre> (bare code blocks without wrapper div)
-        if child.tag == 'pre':
-            code = child.find('code')
-            text = code.get_text() if code else child.get_text()
-            parts.append(f'\n```\n{text}```\n')
-            continue
-
-        # Inline <code>
-        if child.tag == 'code':
-            parts.append(f'`{child.get_text()}`')
-            continue
-
-        # Paragraph
-        if child.tag == 'p':
-            inner = extract_content(child)
-            parts.append(f'\n{inner}\n')
-            continue
-
-        # Line break
-        if child.tag == 'br':
-            parts.append('\n')
-            continue
-
-        # Links
-        if child.tag == 'a':
-            href = child.attrs.get('href', '')
-            text = child.get_text().strip()
-            if href and not href.startswith('#') and text:
-                parts.append(f'[{text}]({href})')
-            else:
-                parts.append(text)
-            continue
-
-        # Block quotes
-        if child.tag == 'blockquote':
-            bq = extract_content(child).strip()
-            parts.append('\n' + '\n'.join(f'> {l}' for l in bq.split('\n')) + '\n')
-            continue
-
-        # Lists
-        if child.tag in ('ul', 'ol'):
-            for i, li in enumerate(c for c in child.children if c.tag == 'li'):
-                pfx = f'{i+1}.' if child.tag == 'ol' else '-'
-                parts.append(f'\n{pfx} {extract_content(li).strip()}')
-            parts.append('\n')
-            continue
-
-        # User mentions
-        if 'user-mention' in cls_set:
-            parts.append(f'@{child.get_text().strip().lstrip("@")}')
-            continue
-
-        # Emoji
-        if 'emoji' in cls_set:
-            alt = child.attrs.get('alt', '') or child.attrs.get('title', '')
-            if alt:
-                parts.append(alt)
-            continue
-
-        # Recurse into everything else
-        parts.append(extract_content(child))
-
-    return ''.join(parts)
-
-
-# ---------------------------------------------------------------------------
-# Thread extraction
-# ---------------------------------------------------------------------------
-
-def extract_thread(html_path, output_path=None):
-    root = parse_html(html_path)
-
-    # Find the message list
-    msg_list = root.find('div', class_='message-list')
-    if not msg_list:
-        print("ERROR: Could not find message list.", file=sys.stderr)
-        sys.exit(1)
-
-    # Topic header
-    header = msg_list.find('div', class_='message_header')
-    stream_name = topic_name = date_str = ''
-    if header:
-        el = header.find('span', class_='message-header-stream-name')
-        if el: stream_name = el.get_text().strip()
-        el = header.find('span', class_='stream-topic-inner')
-        if el: topic_name = el.get_text().strip()
-        el = header.find('span', class_='recipient_row_date')
-        if el:
-            tr = el.find('span', class_='timerender-content')
-            if tr:
-                date_str = tr.attrs.get('data-tippy-content', '') or tr.get_text().strip()
-
-    # Messages
-    messages = []
-    for row in msg_list.find_all('div', class_='message_row'):
-        if not row.has_class('messagebox-includes-sender'):
-            continue
-
-        msg = {}
-
-        sn = row.find('span', class_='sender_name_text')
-        if sn:
-            un = sn.find('span', class_='user-name')
-            msg['sender'] = (un or sn).get_text().strip()
-
-        tm = row.find('a', class_='message-time')
-        if tm:
-            msg['time'] = tm.get_text().strip()
-
-        cd = row.find('div', class_='message_content')
-        if cd:
-            text = extract_content(cd)
-            text = re.sub(r'\n{3,}', '\n\n', text).strip()
-            msg['content'] = text
-
-        # Reactions
-        reactions = []
-        for rx in row.find_all('div', class_='message_reaction'):
-            em = rx.find('div', class_='emoji_alt_code')
-            if em:
-                reactions.append(em.get_text().strip())
-            else:
-                img = rx.find(tag='img')
-                if img:
-                    reactions.append(img.attrs.get('alt', ''))
-            cnt = rx.find('span', class_='message_reaction_count')
-            if cnt and reactions:
-                c = cnt.get_text().strip()
-                if c and c != '1':
-                    reactions[-1] += f' x{c}'
-        if reactions:
-            msg['reactions'] = reactions
-
-        if msg.get('content') or msg.get('sender'):
-            messages.append(msg)
-
-    # Format
-    lines = [
-        '=' * 70,
-        f'# {stream_name} > {topic_name}',
-    ]
-    if date_str:
-        lines.append(f'# Started: {date_str}')
-    lines += [f'# Messages: {len(messages)}', '=' * 70, '']
-
-    for msg in messages:
-        lines.append(f'--- {msg.get("sender","?")}  [{msg.get("time","")}] ---')
-        lines.append(msg.get('content', ''))
-        if msg.get('reactions'):
-            lines.append(f'  Reactions: {", ".join(msg["reactions"])}')
-        lines.append('')
-
-    result = '\n'.join(lines)
-    if output_path:
-        with open(output_path, 'w', encoding='utf-8') as f:
-            f.write(result)
-        print(f"Written {len(messages)} messages to {output_path}")
-    else:
-        print(result)
-
-
-if __name__ == '__main__':
-    if len(sys.argv) < 2:
-        print(f"Usage: {sys.argv[0]} input.html [output.txt]")
-        sys.exit(1)
-    extract_thread(sys.argv[1], sys.argv[2] if len(sys.argv) > 2 else None)
-

.gitattributes

@@ -5,3 +5,9 @@ stage0/** binary linguist-generated
 # The following file is often manually edited, so do show it in diffs
 stage0/src/stdlib_flags.h -binary -linguist-generated
 doc/std/grove/GroveStdlib/Generated/** linguist-generated
+# These files should not have line endings translated on Windows, because
+# it throws off parser tests. Later lines override earlier ones, so the
+# runner code is still treated as ordinary text.
+tests/lean/docparse/* eol=lf
+tests/lean/docparse/*.lean eol=auto
+tests/lean/docparse/*.sh eol=auto

.github/workflows/actionlint.yml

@@ -15,7 +15,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
     - name: Checkout
-      uses: actions/checkout@v6
+      uses: actions/checkout@v5
     - name: actionlint
       uses: raven-actions/actionlint@v2
       with:

.github/workflows/awaiting-manual.yml

@@ -2,19 +2,16 @@ name: Check awaiting-manual label
 
 on:
   merge_group:
-  pull_request_target:
+  pull_request:
     types: [opened, synchronize, reopened, labeled, unlabeled]
 
-permissions:
-  pull-requests: read
-
 jobs:
   check-awaiting-manual:
     runs-on: ubuntu-latest
     steps:
       - name: Check awaiting-manual label
         id: check-awaiting-manual-label
-        if: github.event_name == 'pull_request_target'
+        if: github.event_name == 'pull_request'
         uses: actions/github-script@v8
         with:
           script: |
@@ -31,7 +28,7 @@ jobs:
             }
       
       - name: Wait for manual compatibility
-        if: github.event_name == 'pull_request_target' && steps.check-awaiting-manual-label.outputs.awaiting == 'true'
+        if: github.event_name == 'pull_request' && steps.check-awaiting-manual-label.outputs.awaiting == 'true'
         run: |
           echo "::notice title=Awaiting manual::PR is marked 'awaiting-manual' but neither 'breaks-manual' nor 'builds-manual' labels are present."
           echo "This check will remain in progress until the PR is updated with appropriate manual compatibility labels."

.github/workflows/awaiting-mathlib.yml

@@ -2,19 +2,16 @@ name: Check awaiting-mathlib label
 
 on:
   merge_group:
-  pull_request_target:
+  pull_request:
     types: [opened, synchronize, reopened, labeled, unlabeled]
 
-permissions:
-  pull-requests: read
-
 jobs:
   check-awaiting-mathlib:
     runs-on: ubuntu-latest
     steps:
       - name: Check awaiting-mathlib label
         id: check-awaiting-mathlib-label
-        if: github.event_name == 'pull_request_target'
+        if: github.event_name == 'pull_request'
         uses: actions/github-script@v8
         with:
           script: |
@@ -31,7 +28,7 @@ jobs:
             }
       
       - name: Wait for mathlib compatibility
-        if: github.event_name == 'pull_request_target' && steps.check-awaiting-mathlib-label.outputs.awaiting == 'true'
+        if: github.event_name == 'pull_request' && steps.check-awaiting-mathlib-label.outputs.awaiting == 'true'
         run: |
           echo "::notice title=Awaiting mathlib::PR is marked 'awaiting-mathlib' but neither 'breaks-mathlib' nor 'builds-mathlib' labels are present."
           echo "This check will remain in progress until the PR is updated with appropriate mathlib compatibility labels."

.github/workflows/build-template.yml

@@ -49,7 +49,7 @@ jobs:
       LSAN_OPTIONS: max_leaks=10
       # somehow MinGW clang64 (or cmake?) defaults to `g++` even though it doesn't exist
       CXX: c++
-      MACOSX_DEPLOYMENT_TARGET: 11.0
+      MACOSX_DEPLOYMENT_TARGET: 10.15
     steps:
       - name: Install Nix
         uses: DeterminateSystems/nix-installer-action@main
@@ -66,10 +66,16 @@ jobs:
           brew install ccache tree zstd coreutils gmp libuv
         if: runner.os == 'macOS'
       - name: Checkout
-        uses: actions/checkout@v6
+        if: (!endsWith(matrix.os, '-with-cache'))
+        uses: actions/checkout@v5
         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@v7
+        with:
+          ref: ${{ github.event.pull_request.head.sha }}
       - name: Open Nix shell once
         run: true
         if: runner.os == 'Linux'
@@ -79,7 +85,7 @@ jobs:
       - name: CI Merge Checkout
         run: |
           git fetch --depth=1 origin ${{ github.sha }}
-          git checkout FETCH_HEAD flake.nix flake.lock script/prepare-* tests/elab/importStructure.lean
+          git checkout FETCH_HEAD flake.nix flake.lock script/prepare-* tests/lean/run/importStructure.lean
         if: github.event_name == 'pull_request'
       # (needs to be after "Checkout" so files don't get overridden)
       - name: Setup emsdk
@@ -96,7 +102,7 @@ jobs:
         if: matrix.cmultilib
       - name: Restore Cache
         id: restore-cache
-        uses: actions/cache/restore@v5
+        uses: actions/cache/restore@v4
         with:
           # NOTE: must be in sync with `save` below and with `restore-cache` in `update-stage0.yml`
           path: |
@@ -169,7 +175,7 @@ jobs:
         # Caching on cancellation created some mysterious issues perhaps related to improper build
         # shutdown
         if: steps.restore-cache.outputs.cache-hit != 'true' && !cancelled()
-        uses: actions/cache/save@v5
+        uses: actions/cache/save@v4
         with:
           # NOTE: must be in sync with `restore` above
           path: |
@@ -229,21 +235,25 @@ jobs:
         # prefix `if` above with `always` so it's run even if tests failed
         if: always() && steps.test.conclusion != 'skipped'
       - name: Check Test Binary
-        run: ${{ matrix.binary-check }} tests/compile/534.lean.out
+        run: ${{ matrix.binary-check }} tests/compiler/534.lean.out
         if: (!matrix.cross) && steps.test.conclusion != 'skipped'
       - name: Build Stage 2
         run: |
           make -C build -j$NPROC stage2
-        if: matrix.test-bench
+        if: matrix.test-speedcenter
       - name: Check Stage 3
         run: |
           make -C build -j$NPROC check-stage3
         if: matrix.check-stage3
-      - name: Test Benchmarks
+      - name: Test Speedcenter Benchmarks
         run: |
-          cd tests
-          nix develop -c make -C ../build -j$NPROC bench
-        if: matrix.test-bench
+          # Necessary for some timing metrics but does not work on Namespace runners
+          # and we just want to test that the benchmarks run at all here
+          #echo -1 | sudo tee /proc/sys/kernel/perf_event_paranoid
+          export BUILD=$PWD/build PATH=$PWD/build/stage1/bin:$PATH
+          cd tests/bench
+          nix shell .#temci -c temci exec --config speedcenter.yaml --included_blocks fast --runs 1
+        if: matrix.test-speedcenter
       - name: Check rebootstrap
         run: |
           set -e

.github/workflows/check-prelude.yml

@@ -7,7 +7,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout
-        uses: actions/checkout@v6
+        uses: actions/checkout@v5
         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 }}

.github/workflows/check-stage0.yml

@@ -8,7 +8,7 @@ jobs:
   check-stage0-on-queue:
     runs-on: ubuntu-latest
     steps:
-    - uses: actions/checkout@v6
+    - uses: actions/checkout@v5
       with:
         ref: ${{ github.event.pull_request.head.sha }}
         fetch-depth: 0

.github/workflows/check-stdlib-flags.yml

@@ -1,12 +1,9 @@
 name: Check stdlib_flags.h modifications
 
 on:
-  pull_request_target:
+  pull_request:
     types: [opened, synchronize, reopened, labeled, unlabeled]
 
-permissions:
-  pull-requests: read
-
 jobs:
   check-stdlib-flags:
     runs-on: ubuntu-latest

.github/workflows/ci.yml

@@ -50,7 +50,7 @@ jobs:
 
     steps:
       - name: Checkout
-        uses: actions/checkout@v6
+        uses: actions/checkout@v5
         # don't schedule nightlies on forks
         if: github.event_name == 'schedule' && github.repository == 'leanprover/lean4' || inputs.action == 'release nightly' || (startsWith(github.ref, 'refs/tags/') && github.repository == 'leanprover/lean4')
       - name: Set Nightly
@@ -60,23 +60,10 @@ jobs:
           if [[ -n '${{ secrets.PUSH_NIGHTLY_TOKEN }}' ]]; then
             git remote add nightly https://foo:'${{ secrets.PUSH_NIGHTLY_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-nightly.git
             git fetch nightly --tags
-            if [[ '${{ github.event_name }}' == 'workflow_dispatch' ]]; then
-              # Manual re-release: create a revision of the most recent nightly
-              BASE_NIGHTLY=$(git tag -l 'nightly-*' | sort -rV | head -1)
-              # Strip any existing -revK suffix to get the base date tag
-              BASE_NIGHTLY="${BASE_NIGHTLY%%-rev*}"
-              REV=1
-              while git rev-parse "refs/tags/${BASE_NIGHTLY}-rev${REV}" >/dev/null 2>&1; do
-                REV=$((REV + 1))
-              done
-              LEAN_VERSION_STRING="${BASE_NIGHTLY}-rev${REV}"
+            LEAN_VERSION_STRING="nightly-$(date -u +%F)"
+            # do nothing if commit already has a different tag
+            if [[ "$(git name-rev --name-only --tags --no-undefined HEAD 2> /dev/null || echo "$LEAN_VERSION_STRING")" == "$LEAN_VERSION_STRING" ]]; then
               echo "nightly=$LEAN_VERSION_STRING" >> "$GITHUB_OUTPUT"
-            else
-              # Scheduled: do nothing if commit already has a different tag
-              LEAN_VERSION_STRING="nightly-$(date -u +%F)"
-              if [[ "$(git name-rev --name-only --tags --no-undefined HEAD 2> /dev/null || echo "$LEAN_VERSION_STRING")" == "$LEAN_VERSION_STRING" ]]; then
-                echo "nightly=$LEAN_VERSION_STRING" >> "$GITHUB_OUTPUT"
-              fi
             fi
           fi
 
@@ -128,7 +115,7 @@ jobs:
           CMAKE_MAJOR=$(grep -E "^set\(LEAN_VERSION_MAJOR " src/CMakeLists.txt | grep -oE '[0-9]+')
           CMAKE_MINOR=$(grep -E "^set\(LEAN_VERSION_MINOR " src/CMakeLists.txt | grep -oE '[0-9]+')
           CMAKE_PATCH=$(grep -E "^set\(LEAN_VERSION_PATCH " src/CMakeLists.txt | grep -oE '[0-9]+')
-          CMAKE_IS_RELEASE=$(grep -m 1 -E "^set\(LEAN_VERSION_IS_RELEASE " src/CMakeLists.txt | sed -nE 's/^set\(LEAN_VERSION_IS_RELEASE ([0-9]+)\).*/\1/p')
+          CMAKE_IS_RELEASE=$(grep -m 1 -E "^set\(LEAN_VERSION_IS_RELEASE " src/CMakeLists.txt | grep -oE '[0-9]+')
 
           # Expected values from tag parsing
           TAG_MAJOR="${{ steps.set-release.outputs.LEAN_VERSION_MAJOR }}"
@@ -166,7 +153,7 @@ jobs:
       # 0: PRs without special label
       # 1: PRs with `merge-ci` label, merge queue checks, master commits
       # 2: nightlies
-      # 3: PRs with `release-ci` or `lake-ci` label, full releases
+      # 3: PRs with `release-ci` label, full releases
       - name: Set check level
         id: set-level
         # We do not use github.event.pull_request.labels.*.name here because
@@ -175,7 +162,6 @@ jobs:
         run: |
           check_level=0
           fast=false
-          lake_ci=false
 
           if [[ -n "${{ steps.set-release.outputs.RELEASE_TAG }}" || -n "${{ steps.set-release-custom.outputs.RELEASE_TAG }}" ]]; then
             check_level=3
@@ -190,19 +176,13 @@ jobs:
             elif echo "$labels" | grep -q "merge-ci"; then
               check_level=1
             fi
-            if echo "$labels" | grep -q "lake-ci"; then
-              lake_ci=true
-            fi
             if echo "$labels" | grep -q "fast-ci"; then
               fast=true
             fi
           fi
 
-          {
-            echo "check-level=$check_level"
-            echo "fast=$fast"
-            echo "lake-ci=$lake_ci"
-          } >> "$GITHUB_OUTPUT"
+          echo "check-level=$check_level" >> "$GITHUB_OUTPUT"
+          echo "fast=$fast" >> "$GITHUB_OUTPUT"
         env:
           GH_TOKEN: ${{ github.token }}
 
@@ -213,7 +193,6 @@ jobs:
           script: |
             const level = ${{ steps.set-level.outputs.check-level }};
             const fast = ${{ steps.set-level.outputs.fast }};
-            const lakeCi = "${{ steps.set-level.outputs.lake-ci }}" == "true";
             console.log(`level: ${level}, fast: ${fast}`);
             // use large runners where available (original repo)
             let large = ${{ github.repository == 'leanprover/lean4' }};
@@ -266,8 +245,8 @@ jobs:
                 "check-rebootstrap": level >= 1,
                 "check-stage3": level >= 2,
                 "test": true,
-                // NOTE: `test-bench` currently seems to be broken on `ubuntu-latest`
-                "test-bench": large && level >= 2,
+                // NOTE: `test-speedcenter` currently seems to be broken on `ubuntu-latest`
+                "test-speedcenter": large && level >= 2,
                 // We are not warning-free yet on all platforms, start here
                 "CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-Werror",
               },
@@ -277,30 +256,25 @@ jobs:
                 "enabled": level >= 2,
                 "test": true,
                 "CMAKE_PRESET": "reldebug",
-                // * `elab_bench/big_do` crashes with exit code 134
-                "CTEST_OPTIONS": "-E 'elab_bench/big_do'",
               },
               {
                 "name": "Linux fsanitize",
                 // Always run on large if available, more reliable regarding timeouts
-                "os": large ? "nscloud-ubuntu-22.04-amd64-16x32-with-cache" : "ubuntu-latest",
+                "os": large ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
                 "enabled": level >= 2,
                 // do not fail nightlies on this for now
                 "secondary": level <= 2,
                 "test": true,
                 // turn off custom allocator & symbolic functions to make LSAN do its magic
                 "CMAKE_PRESET": "sanitize",
-                // * `StackOverflow*` correctly triggers ubsan.
-                // * `reverse-ffi` fails to link in sanitizers.
-                // * `interactive` and `async_select_channel` fail nondeterministically, would need
-                //   to be investigated..
-                // * 9366 is too close to timeout.
-                // * `bv_` sometimes times out calling into cadical even though we should be using
-                //   the standard compile flags for it.
-                // * `grind_guide` always times out.
-                // * `pkg/|lake/` tests sometimes time out (likely even hang), related to Lake CI
-                //   failures?
-                "CTEST_OPTIONS": "-E 'StackOverflow|reverse-ffi|interactive|async_select_channel|9366|run/bv_|grind_guide|grind_bitvec2|grind_constProp|grind_indexmap|grind_list|grind_lint|grind_array_attach|grind_ite_trace|pkg/|lake/'"
+                // `StackOverflow*` correctly triggers ubsan.
+                // `reverse-ffi` fails to link in sanitizers.
+                // `interactive` and `async_select_channel` fail nondeterministically, would need to
+                // be investigated..
+                // 9366 is too close to timeout.
+                // `bv_` sometimes times out calling into cadical even though we should be using the
+                // standard compile flags for it.
+                "CTEST_OPTIONS": "-E 'StackOverflow|reverse-ffi|interactive|async_select_channel|9366|run/bv_'"
               },
               {
                 "name": "macOS",
@@ -387,11 +361,6 @@ jobs:
                 job["CMAKE_OPTIONS"] = (job["CMAKE_OPTIONS"] ? job["CMAKE_OPTIONS"] + " " : "") + "-DUSE_LAKE=OFF";
               }
             }
-            if (lakeCi) {
-              for (const job of matrix) {
-                job["CMAKE_OPTIONS"] = (job["CMAKE_OPTIONS"] ? job["CMAKE_OPTIONS"] + " " : "") + "-DLAKE_CI=ON";
-              }
-            }
             console.log(`matrix:\n${JSON.stringify(matrix, null, 2)}`);
             matrix = matrix.filter((job) => job["enabled"]);
             core.setOutput('matrix', matrix.filter((job) => !job["secondary"]));
@@ -461,11 +430,11 @@ jobs:
     runs-on: ubuntu-latest
     needs: build
     steps:
-      - uses: actions/download-artifact@v7
+      - uses: actions/download-artifact@v6
         with:
           path: artifacts
       - name: Release
-        uses: softprops/action-gh-release@a06a81a03ee405af7f2048a818ed3f03bbf83c7b
+        uses: softprops/action-gh-release@6da8fa9354ddfdc4aeace5fc48d7f679b5214090
         with:
           files: artifacts/*/*
           fail_on_unmatched_files: true
@@ -486,14 +455,14 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout
-        uses: actions/checkout@v6
+        uses: actions/checkout@v5
         with:
           # needed for tagging
           fetch-depth: 0
           # Doesn't seem to be working when additionally fetching from lean4-nightly
           #filter: tree:0
           token: ${{ secrets.PUSH_NIGHTLY_TOKEN }}
-      - uses: actions/download-artifact@v7
+      - uses: actions/download-artifact@v6
         with:
           path: artifacts
       - name: Prepare Nightly Release
@@ -503,7 +472,7 @@ jobs:
           git tag "${{ needs.configure.outputs.nightly }}"
           git push nightly "${{ needs.configure.outputs.nightly }}"
           git push -f origin refs/tags/${{ needs.configure.outputs.nightly }}:refs/heads/nightly
-          last_tag="$(git log HEAD^ --simplify-by-decoration --pretty="format:%d" | grep -o "nightly-[^ ,)]*" | head -n 1)"
+          last_tag="$(git log HEAD^ --simplify-by-decoration --pretty="format:%d" | grep -o "nightly-[-0-9]*" | head -n 1)"
           echo -e "*Changes since ${last_tag}:*\n\n" > diff.md
           git show "$last_tag":RELEASES.md > old.md
           #./script/diff_changelogs.py old.md doc/changes.md >> diff.md
@@ -511,7 +480,7 @@ jobs:
           echo -e "\n*Full commit log*\n" >> diff.md
           git log --oneline "$last_tag"..HEAD | sed 's/^/* /' >> diff.md
       - name: Release Nightly
-        uses: softprops/action-gh-release@a06a81a03ee405af7f2048a818ed3f03bbf83c7b
+        uses: softprops/action-gh-release@6da8fa9354ddfdc4aeace5fc48d7f679b5214090
         with:
           body_path: diff.md
           prerelease: true
@@ -526,18 +495,8 @@ jobs:
           gh workflow -R leanprover/release-index run update-index.yml
         env:
           GITHUB_TOKEN: ${{ secrets.RELEASE_INDEX_TOKEN }}
-      - name: Generate mathlib nightly-testing app token
-        id: mathlib-app-token
-        uses: actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1
-        continue-on-error: true
-        with:
-          app-id: ${{ secrets.MATHLIB_NIGHTLY_TESTING_APP_ID }}
-          private-key: ${{ secrets.MATHLIB_NIGHTLY_TESTING_PRIVATE_KEY }}
-          owner: leanprover-community
-          repositories: mathlib4-nightly-testing
       - name: Update toolchain on mathlib4's nightly-testing branch
-        if: steps.mathlib-app-token.outcome == 'success'
         run: |
-          gh workflow -R leanprover-community/mathlib4-nightly-testing run nightly_bump_and_merge.yml
+          gh workflow -R leanprover-community/mathlib4-nightly-testing run nightly_bump_toolchain.yml
         env:
-          GITHUB_TOKEN: ${{ steps.mathlib-app-token.outputs.token }}
+          GITHUB_TOKEN: ${{ secrets.MATHLIB4_BOT }}

.github/workflows/copyright-header.yml

@@ -6,7 +6,7 @@ jobs:
   check-lean-files:
     runs-on: ubuntu-latest
     steps:
-    - uses: actions/checkout@v6
+    - uses: actions/checkout@v5
 
     - name: Verify .lean files start with a copyright header.
       run: |

.github/workflows/labels-from-comments.yml

@@ -1,5 +1,5 @@
 # This workflow allows any user to add one of the `awaiting-review`, `awaiting-author`, `WIP`,
-# `release-ci`, `lake-ci`, or a `changelog-XXX` label by commenting on the PR or issue.
+# `release-ci`, or a `changelog-XXX` label by commenting on the PR or issue.
 # If any labels from the set {`awaiting-review`, `awaiting-author`, `WIP`} are added, other labels
 # from that set are removed automatically at the same time.
 # Similarly, if any `changelog-XXX` label is added, other `changelog-YYY` labels are removed.
@@ -12,7 +12,7 @@ on:
 
 jobs:
   update-label:
-    if: github.event.issue.pull_request != null && (contains(github.event.comment.body, 'awaiting-review') || contains(github.event.comment.body, 'awaiting-author') || contains(github.event.comment.body, 'WIP') || contains(github.event.comment.body, 'release-ci') || contains(github.event.comment.body, 'lake-ci') || contains(github.event.comment.body, 'changelog-'))
+    if: github.event.issue.pull_request != null && (contains(github.event.comment.body, 'awaiting-review') || contains(github.event.comment.body, 'awaiting-author') || contains(github.event.comment.body, 'WIP') || contains(github.event.comment.body, 'release-ci') || contains(github.event.comment.body, 'changelog-'))
     runs-on: ubuntu-latest
 
     steps:
@@ -28,7 +28,6 @@ jobs:
           const awaitingAuthor = commentLines.includes('awaiting-author');
           const wip = commentLines.includes('WIP');
           const releaseCI = commentLines.includes('release-ci');
-          const lakeCI = commentLines.includes('lake-ci');
           const changelogMatch = commentLines.find(line => line.startsWith('changelog-'));
 
           if (awaitingReview || awaitingAuthor || wip) {
@@ -50,9 +49,6 @@ jobs:
           if (releaseCI) {
             await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['release-ci'] });
           }
-          if (lakeCI) {
-            await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['lake-ci'] });
-          }
 
           if (changelogMatch) {
             const changelogLabel = changelogMatch.trim();

.github/workflows/pr-body.yml

@@ -2,23 +2,17 @@ name: Check PR body for changelog convention
 
 on:
   merge_group:
-  pull_request_target:
+  pull_request:
     types: [opened, synchronize, reopened, edited, labeled, converted_to_draft, ready_for_review]
 
-permissions:
-  pull-requests: read
-
 jobs:
   check-pr-body:
     runs-on: ubuntu-latest
     steps:
       - name: Check PR body
-        if: github.event_name == 'pull_request_target'
+        if: github.event_name == 'pull_request'
         uses: actions/github-script@v8
         with:
-          # Safety note: this uses pull_request_target, so the workflow has elevated privileges.
-          # The PR title and body are only used in regex tests (read-only string matching),
-          # never interpolated into shell commands, eval'd, or written to GITHUB_ENV/GITHUB_OUTPUT.
           script: |
             const { title, body, labels, draft } = context.payload.pull_request;
             if (!draft && /^(feat|fix):/.test(title) && !labels.some(label => label.name == "changelog-no")) {

.github/workflows/pr-release.yml

@@ -20,9 +20,7 @@ on:
 jobs:
   on-success:
     runs-on: ubuntu-latest
-    # Run even if CI fails, as long as build artifacts are available
-    # The "Verify release artifacts exist" step will fail if necessary artifacts are missing
-    if: github.event.workflow_run.event == 'pull_request' && github.repository == 'leanprover/lean4'
+    if: github.event.workflow_run.conclusion == 'success' && github.event.workflow_run.event == 'pull_request' && github.repository == 'leanprover/lean4'
     steps:
       - name: Retrieve information about the original workflow
         uses: potiuk/get-workflow-origin@v1_1 # https://github.com/marketplace/actions/get-workflow-origin
@@ -43,19 +41,6 @@ jobs:
           name: build-.*
           name_is_regexp: true
 
-      # Verify artifacts were downloaded before any side effects (tag creation, release deletion).
-      - name: Verify release artifacts exist
-        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        run: |
-          shopt -s nullglob
-          files=(artifacts/*/*)
-          if [ ${#files[@]} -eq 0 ]; then
-            echo "::error::No artifacts found matching artifacts/*/*"
-            exit 1
-          fi
-          echo "Found ${#files[@]} artifacts to upload:"
-          printf '%s\n' "${files[@]}"
-
       - name: Push tag
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         run: |
@@ -77,44 +62,42 @@ jobs:
           git -C lean4.git remote add pr-releases https://foo:'${{ secrets.PR_RELEASES_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-pr-releases.git
           git -C lean4.git push -f pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}
           git -C lean4.git push -f pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-"${SHORT_SHA}"
-      - name: Delete existing releases if present
+      - name: Delete existing release if present
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         run: |
-          # Delete any existing releases for this PR.
-          # The short format release is always recreated with the latest commit.
-          # The SHA-suffixed release should be unique per commit, but delete just in case.
+          # Try to delete any existing release for the current PR (just the version without the SHA suffix).
           gh release delete --repo ${{ github.repository_owner }}/lean4-pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} -y || true
-          gh release delete --repo ${{ github.repository_owner }}/lean4-pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }} -y || true
         env:
           GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
-      # We use `gh release create` instead of `softprops/action-gh-release` because
-      # the latter enumerates all releases to check for existing ones, which fails
-      # when the repository has more than 10000 releases (GitHub API pagination limit).
-      # Upstream fix: https://github.com/softprops/action-gh-release/pull/725
       - name: Release (short format)
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        run: |
-          # There are coredump files in deeper subdirectories; artifacts/*/* gets the release archives.
-          gh release create \
-            --repo ${{ github.repository_owner }}/lean4-pr-releases \
-            --title "Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }}" \
-            --notes "" \
-            pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} \
-            artifacts/*/*
+        uses: softprops/action-gh-release@6da8fa9354ddfdc4aeace5fc48d7f679b5214090
+        with:
+          name: Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }}
+          # There are coredumps files here as well, but all in deeper subdirectories.
+          files: artifacts/*/*
+          fail_on_unmatched_files: true
+          draft: false
+          tag_name: pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}
+          repository: ${{ github.repository_owner }}/lean4-pr-releases
         env:
-          GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
+          # The token used here must have `workflow` privileges.
+          GITHUB_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
 
       - name: Release (SHA-suffixed format)
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        run: |
-          gh release create \
-            --repo ${{ github.repository_owner }}/lean4-pr-releases \
-            --title "Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }} (${{ steps.workflow-info.outputs.sourceHeadSha }})" \
-            --notes "" \
-            pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }} \
-            artifacts/*/*
+        uses: softprops/action-gh-release@6da8fa9354ddfdc4aeace5fc48d7f679b5214090
+        with:
+          name: Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }} (${{ steps.workflow-info.outputs.sourceHeadSha }})
+          # There are coredumps files here as well, but all in deeper subdirectories.
+          files: artifacts/*/*
+          fail_on_unmatched_files: true
+          draft: false
+          tag_name: pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}
+          repository: ${{ github.repository_owner }}/lean4-pr-releases
         env:
-          GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
+          # The token used here must have `workflow` privileges.
+          GITHUB_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
 
       - name: Report release status (short format)
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
@@ -170,18 +153,6 @@ jobs:
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         uses: dcarbone/install-jq-action@v3.2.0
 
-      # Generate a token for posting comments to Lean PRs about mathlib compatibility.
-      # This app is in the leanprover org and installed on leanprover/lean4.
-      - name: Generate GitHub App token for Lean PR comments
-        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        id: mathlib-comment-token
-        uses: actions/create-github-app-token@3ff1caaa28b64c9cc276ce0a02e2ff584f3900c5 # v2.0.2
-        with:
-          app-id: ${{ secrets.MATHLIB_LEAN_PR_TESTING_APP_ID }}
-          private-key: ${{ secrets.MATHLIB_LEAN_PR_TESTING_PRIVATE_KEY }}
-          owner: leanprover
-          repositories: lean4
-
       # Check that the most recently nightly coincides with 'git merge-base HEAD master'
       - name: Check merge-base and nightly-testing-YYYY-MM-DD for Mathlib/Batteries
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
@@ -216,9 +187,8 @@ jobs:
 
           if [[ -n "$MESSAGE" ]]; then
             # Check if force-mathlib-ci label is present
-            # Use GITHUB_TOKEN for read-only label fetch (MATHLIB4_COMMENT_BOT is only for posting comments)
             LABELS="$(curl --retry 3 --location --silent \
-                          -H "Authorization: token ${{ secrets.GITHUB_TOKEN }}" \
+                          -H "Authorization: token ${{ secrets.MATHLIB4_COMMENT_BOT }}" \
                           -H "Accept: application/vnd.github.v3+json" \
                           "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/labels" \
                           | jq -r '.[].name')"
@@ -239,10 +209,10 @@ jobs:
 
             # Use GitHub API to check if a comment already exists
             existing_comment="$(curl --retry 3 --location --silent \
-                                    -H "Authorization: token ${{ steps.mathlib-comment-token.outputs.token }}" \
+                                    -H "Authorization: token ${{ secrets.MATHLIB4_COMMENT_BOT }}" \
                                     -H "Accept: application/vnd.github.v3+json" \
                                     "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments" \
-                                    | jq 'first(.[] | select(.body | test("^- . Mathlib") or startswith("Mathlib CI status")) | select(.user.login == "mathlib-lean-pr-testing[bot]"))')"
+                                    | jq 'first(.[] | select(.body | test("^- . Mathlib") or startswith("Mathlib CI status")) | select(.user.login == "leanprover-community-bot"))')"
             existing_comment_id="$(echo "$existing_comment" | jq -r .id)"
             existing_comment_body="$(echo "$existing_comment" | jq -r .body)"
 
@@ -252,14 +222,14 @@ jobs:
               echo "Posting message to the comments: $MESSAGE"
 
               # Append new result to the existing comment or post a new comment
-              # Use the mathlib-lean-pr-testing app token so Mathlib CI can subsequently edit the comment.
+              # It's essential we use the MATHLIB4_COMMENT_BOT token here, so that Mathlib CI can subsequently edit the comment.
               if [ -z "$existing_comment_id" ]; then
                 INTRO="Mathlib CI status ([docs](https://leanprover-community.github.io/contribute/tags_and_branches.html)):"
                 # Post new comment with a bullet point
                 echo "Posting as new comment at leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments"
                 curl -L -s \
                   -X POST \
-                  -H "Authorization: token ${{ steps.mathlib-comment-token.outputs.token }}" \
+                  -H "Authorization: token ${{ secrets.MATHLIB4_COMMENT_BOT }}" \
                   -H "Accept: application/vnd.github.v3+json" \
                   -d "$(jq --null-input --arg intro "$INTRO" --arg val "$MESSAGE" '{"body":($intro + "\n" + $val)}')" \
                   "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments"
@@ -268,7 +238,7 @@ jobs:
                 echo "Appending to existing comment at leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments"
                 curl -L -s \
                   -X PATCH \
-                  -H "Authorization: token ${{ steps.mathlib-comment-token.outputs.token }}" \
+                  -H "Authorization: token ${{ secrets.MATHLIB4_COMMENT_BOT }}" \
                   -H "Accept: application/vnd.github.v3+json" \
                   -d "$(jq --null-input --arg existing "$existing_comment_body" --arg message "$MESSAGE" '{"body":($existing + "\n" + $message)}')" \
                   "https://api.github.com/repos/leanprover/lean4/issues/comments/$existing_comment_id"
@@ -409,18 +379,6 @@ jobs:
       # We next automatically create a Batteries branch using this toolchain.
       # Batteries doesn't itself have a mechanism to report results of CI from this branch back to Lean
       # Instead this is taken care of by Mathlib CI, which will fail if Batteries fails.
-
-      # Generate a token from the mathlib-nightly-testing GitHub App for cross-org access
-      - name: Generate GitHub App token for leanprover-community repos
-        if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
-        id: mathlib-app-token
-        uses: actions/create-github-app-token@3ff1caaa28b64c9cc276ce0a02e2ff584f3900c5 # v2.0.2
-        with:
-          app-id: ${{ secrets.MATHLIB_NIGHTLY_TESTING_APP_ID }}
-          private-key: ${{ secrets.MATHLIB_NIGHTLY_TESTING_PRIVATE_KEY }}
-          owner: leanprover-community
-          repositories: batteries,mathlib4-nightly-testing
-
       - name: Cleanup workspace
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
         run: |
@@ -429,10 +387,10 @@ jobs:
       # Checkout the Batteries repository with all branches
       - name: Checkout Batteries repository
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
-        uses: actions/checkout@v6
+        uses: actions/checkout@v5
         with:
           repository: leanprover-community/batteries
-          token: ${{ steps.mathlib-app-token.outputs.token }}
+          token: ${{ secrets.MATHLIB4_BOT }}
           ref: nightly-testing
           fetch-depth: 0 # This ensures we check out all tags and branches.
           filter: tree:0
@@ -489,10 +447,10 @@ jobs:
       # Checkout the mathlib4 repository with all branches
       - name: Checkout mathlib4 repository
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
-        uses: actions/checkout@v6
+        uses: actions/checkout@v5
         with:
           repository: leanprover-community/mathlib4-nightly-testing
-          token: ${{ steps.mathlib-app-token.outputs.token }}
+          token: ${{ secrets.MATHLIB4_BOT }}
           ref: nightly-testing
           fetch-depth: 0 # This ensures we check out all tags and branches.
           filter: tree:0
@@ -572,7 +530,7 @@ jobs:
       # Checkout the reference manual repository with all branches
       - name: Checkout mathlib4 repository
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.reference-manual-ready.outputs.manual_ready == 'true'
-        uses: actions/checkout@v6
+        uses: actions/checkout@v5
         with:
           repository: leanprover/reference-manual
           token: ${{ secrets.MANUAL_PR_BOT }}

.github/workflows/restart-on-label.yml

@@ -7,7 +7,7 @@ on:
 jobs:
   restart-on-label:
     runs-on: ubuntu-latest
-    if: contains(github.event.label.name, 'merge-ci') || contains(github.event.label.name, 'release-ci') || contains(github.event.label.name, 'lake-ci')
+    if: contains(github.event.label.name, 'merge-ci') || contains(github.event.label.name, 'release-ci')
     steps:
     - run: |
         # Finding latest CI workflow run on current pull request

.github/workflows/update-stage0.yml

@@ -27,7 +27,7 @@ jobs:
     # This action should push to an otherwise protected branch, so it
     # uses a deploy key with write permissions, as suggested at
     # https://stackoverflow.com/a/76135647/946226
-    - uses: actions/checkout@v6
+    - uses: actions/checkout@v5
       with:
         ssh-key: ${{secrets.STAGE0_SSH_KEY}}
     - run: echo "should_update_stage0=yes" >> "$GITHUB_ENV"
@@ -58,7 +58,7 @@ jobs:
       shell: 'nix develop -c bash -euxo pipefail {0}'
     - name: Restore Cache
       if: env.should_update_stage0 == 'yes'
-      uses: actions/cache/restore@v5
+      uses: actions/cache/restore@v4
       with:
         # NOTE: must be in sync with `restore-cache` in `build-template.yml`
         path: |

.gitignore

@@ -1,6 +1,7 @@
 *~
 \#*
 .#*
+*.lock
 .lake
 lake-manifest.json
 /build
@@ -17,12 +18,8 @@ compile_commands.json
 *.idea
 tasks.json
 settings.json
-!.claude/settings.json
 .gdb_history
 .vscode/*
-!.vscode/settings.json
-!.vscode/tasks.json
-!.vscode/extensions.json
 script/__pycache__
 *.produced.out
 CMakeSettings.json

.vscode/extensions.json

@@ -1,5 +0,0 @@
-{
-	"recommendations": [
-		"leanprover.lean4"
-	]
-}

.vscode/settings.json

@@ -1,12 +0,0 @@
-{
-	"files.insertFinalNewline": true,
-	"files.trimTrailingWhitespace": true,
-	// These require the CMake Tools extension (ms-vscode.cmake-tools).
-	"cmake.buildDirectory": "${workspaceFolder}/build/release",
-	"cmake.generator": "Unix Makefiles",
-	"[lean4]": {
-		"editor.rulers": [
-			100
-		]
-	}
-}

.vscode/tasks.json

@@ -1,34 +0,0 @@
-{
-	"version": "2.0.0",
-	"tasks": [
-		{
-			"label": "build",
-			"type": "shell",
-			"command": "make -C build/release -j$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4)",
-			"problemMatcher": [],
-			"group": {
-				"kind": "build",
-				"isDefault": true
-			}
-		},
-		{
-			"label": "build-old",
-			"type": "shell",
-			"command": "make -C build/release -j$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4) LAKE_EXTRA_ARGS=--old",
-			"problemMatcher": [],
-			"group": {
-				"kind": "build"
-			}
-		},
-		{
-			"label": "test",
-			"type": "shell",
-			"command": "NPROC=$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4); CTEST_OUTPUT_ON_FAILURE=1 make -C build/release test -j$NPROC ARGS=\"-j$NPROC\"",
-			"problemMatcher": [],
-			"group": {
-				"kind": "test",
-				"isDefault": true
-			}
-		}
-	]
-}

CMakeLists.txt

@@ -1,8 +1,4 @@
-cmake_minimum_required(VERSION 3.21)
-
-if(NOT CMAKE_GENERATOR MATCHES "Makefiles")
-  message(FATAL_ERROR "Only makefile generators are supported")
-endif()
+cmake_minimum_required(VERSION 3.11)
 
 option(USE_MIMALLOC "use mimalloc" ON)
 
@@ -14,22 +10,22 @@ option(USE_MIMALLOC "use mimalloc" ON)
 get_cmake_property(vars CACHE_VARIABLES)
 foreach(var ${vars})
   get_property(currentHelpString CACHE "${var}" PROPERTY HELPSTRING)
-  if(var MATCHES "STAGE0_(.*)")
+  if("${var}" MATCHES "STAGE0_(.*)")
     list(APPEND STAGE0_ARGS "-D${CMAKE_MATCH_1}=${${var}}")
-  elseif(var MATCHES "STAGE1_(.*)")
+  elseif("${var}" MATCHES "STAGE1_(.*)")
     list(APPEND STAGE1_ARGS "-D${CMAKE_MATCH_1}=${${var}}")
-  elseif(currentHelpString MATCHES "No help, variable specified on the command line." OR currentHelpString STREQUAL "")
+  elseif("${currentHelpString}" MATCHES "No help, variable specified on the command line." OR "${currentHelpString}" STREQUAL "")
     list(APPEND CL_ARGS "-D${var}=${${var}}")
-    if(var MATCHES "USE_GMP|CHECK_OLEAN_VERSION|LEAN_VERSION_.*|LEAN_SPECIAL_VERSION_DESC")
+    if("${var}" MATCHES "USE_GMP|CHECK_OLEAN_VERSION|LEAN_VERSION_.*|LEAN_SPECIAL_VERSION_DESC")
       # must forward options that generate incompatible .olean format
       list(APPEND STAGE0_ARGS "-D${var}=${${var}}")
-    elseif(var MATCHES "LLVM*|PKG_CONFIG|USE_LAKE|USE_MIMALLOC")
+    elseif("${var}" MATCHES "LLVM*|PKG_CONFIG|USE_LAKE|USE_MIMALLOC")
       list(APPEND STAGE0_ARGS "-D${var}=${${var}}")
     endif()
-  elseif(var MATCHES "USE_MIMALLOC")
+  elseif("${var}" MATCHES "USE_MIMALLOC")
     list(APPEND CL_ARGS "-D${var}=${${var}}")
     list(APPEND STAGE0_ARGS "-D${var}=${${var}}")
-  elseif((var MATCHES "CMAKE_.*") AND NOT (var MATCHES "CMAKE_BUILD_TYPE") AND NOT (var MATCHES "CMAKE_HOME_DIRECTORY"))
+  elseif(("${var}" MATCHES "CMAKE_.*") AND NOT ("${var}" MATCHES "CMAKE_BUILD_TYPE") AND NOT ("${var}" MATCHES "CMAKE_HOME_DIRECTORY"))
     list(APPEND PLATFORM_ARGS "-D${var}=${${var}}")
   endif()
 endforeach()
@@ -38,15 +34,15 @@ include(ExternalProject)
 project(LEAN CXX C)
 
 if(NOT (DEFINED STAGE0_CMAKE_EXECUTABLE_SUFFIX))
-  set(STAGE0_CMAKE_EXECUTABLE_SUFFIX "${CMAKE_EXECUTABLE_SUFFIX}")
+    set(STAGE0_CMAKE_EXECUTABLE_SUFFIX "${CMAKE_EXECUTABLE_SUFFIX}")
 endif()
 
-# Don't do anything with cadical/leantar on wasm
-if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
+# Don't do anything with cadical on wasm
+if (NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
   find_program(CADICAL cadical)
   if(NOT CADICAL)
     set(CADICAL_CXX c++)
-    if(CADICAL_USE_CUSTOM_CXX)
+    if (CADICAL_USE_CUSTOM_CXX)
       set(CADICAL_CXX ${CMAKE_CXX_COMPILER})
       # Use same platform flags as for Lean executables, in particular from `prepare-llvm-linux.sh`,
       # but not Lean-specific `LEAN_EXTRA_CXX_FLAGS` such as fsanitize.
@@ -58,82 +54,42 @@ if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
       set(CADICAL_CXX "${CCACHE} ${CADICAL_CXX}")
     endif()
     # missing stdio locking API on Windows
-    if(CMAKE_SYSTEM_NAME MATCHES "Windows")
+    if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
       string(APPEND CADICAL_CXXFLAGS " -DNUNLOCKED")
     endif()
     string(APPEND CADICAL_CXXFLAGS " -DNCLOSEFROM")
-    ExternalProject_Add(
-      cadical
+    ExternalProject_add(cadical
       PREFIX cadical
       GIT_REPOSITORY https://github.com/arminbiere/cadical
       GIT_TAG rel-2.1.2
       CONFIGURE_COMMAND ""
-      BUILD_COMMAND
-        $(MAKE) -f ${CMAKE_SOURCE_DIR}/src/cadical.mk CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX}
-        CXX=${CADICAL_CXX} CXXFLAGS=${CADICAL_CXXFLAGS} LDFLAGS=${CADICAL_LDFLAGS}
+      BUILD_COMMAND $(MAKE) -f ${CMAKE_SOURCE_DIR}/src/cadical.mk
+        CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX}
+        CXX=${CADICAL_CXX}
+        CXXFLAGS=${CADICAL_CXXFLAGS}
+        LDFLAGS=${CADICAL_LDFLAGS}
       BUILD_IN_SOURCE ON
-      INSTALL_COMMAND ""
-    )
-    set(CADICAL ${CMAKE_BINARY_DIR}/cadical/cadical${CMAKE_EXECUTABLE_SUFFIX})
+      INSTALL_COMMAND "")
+    set(CADICAL ${CMAKE_BINARY_DIR}/cadical/cadical${CMAKE_EXECUTABLE_SUFFIX} CACHE FILEPATH "path to cadical binary" FORCE)
     list(APPEND EXTRA_DEPENDS cadical)
   endif()
-  find_program(LEANTAR leantar)
-  if(NOT LEANTAR)
-    set(LEANTAR_VERSION v0.1.19)
-    if(CMAKE_SYSTEM_NAME MATCHES "Windows")
-      set(LEANTAR_ARCHIVE_SUFFIX .zip)
-      set(LEANTAR_TARGET x86_64-pc-windows-msvc)
-    else()
-      set(LEANTAR_ARCHIVE_SUFFIX .tar.gz)
-      if(CMAKE_SYSTEM_PROCESSOR MATCHES "arm64")
-        set(LEANTAR_TARGET_ARCH aarch64)
-      else()
-        set(LEANTAR_TARGET_ARCH x86_64)
-      endif()
-      if(CMAKE_SYSTEM_NAME MATCHES "Darwin")
-        set(LEANTAR_TARGET_OS apple-darwin)
-      else()
-        set(LEANTAR_TARGET_OS unknown-linux-musl)
-      endif()
-      set(LEANTAR_TARGET ${LEANTAR_TARGET_ARCH}-${LEANTAR_TARGET_OS})
-    endif()
-    set(
-      LEANTAR
-      ${CMAKE_BINARY_DIR}/leantar/leantar-${LEANTAR_VERSION}-${LEANTAR_TARGET}/leantar${CMAKE_EXECUTABLE_SUFFIX}
-    )
-    if(NOT EXISTS "${LEANTAR}")
-      file(
-        DOWNLOAD
-          https://github.com/digama0/leangz/releases/download/${LEANTAR_VERSION}/leantar-${LEANTAR_VERSION}-${LEANTAR_TARGET}${LEANTAR_ARCHIVE_SUFFIX}
-        ${CMAKE_BINARY_DIR}/leantar${LEANTAR_ARCHIVE_SUFFIX}
-      )
-      file(
-        ARCHIVE_EXTRACT
-        INPUT ${CMAKE_BINARY_DIR}/leantar${LEANTAR_ARCHIVE_SUFFIX}
-        DESTINATION ${CMAKE_BINARY_DIR}/leantar
-      )
-    endif()
-  endif()
-  list(APPEND CL_ARGS -DCADICAL=${CADICAL} -DLEANTAR=${LEANTAR})
+  list(APPEND CL_ARGS -DCADICAL=${CADICAL})
 endif()
 
-if(USE_MIMALLOC)
-  ExternalProject_Add(
-    mimalloc
+if (USE_MIMALLOC)
+  ExternalProject_add(mimalloc
     PREFIX mimalloc
     GIT_REPOSITORY https://github.com/microsoft/mimalloc
     GIT_TAG v2.2.3
     # just download, we compile it as part of each stage as it is small
     CONFIGURE_COMMAND ""
     BUILD_COMMAND ""
-    INSTALL_COMMAND ""
-  )
+    INSTALL_COMMAND "")
   list(APPEND EXTRA_DEPENDS mimalloc)
 endif()
 
-if(NOT STAGE1_PREV_STAGE)
-  ExternalProject_Add(
-    stage0
+if (NOT STAGE1_PREV_STAGE)
+  ExternalProject_add(stage0
     SOURCE_DIR "${LEAN_SOURCE_DIR}/stage0"
     SOURCE_SUBDIR src
     BINARY_DIR stage0
@@ -141,85 +97,64 @@ if(NOT STAGE1_PREV_STAGE)
     # (however, CI will override this as we need to embed the githash into the stage 1 library built
     # by stage 0)
     CMAKE_ARGS -DSTAGE=0 -DUSE_GITHASH=OFF ${PLATFORM_ARGS} ${STAGE0_ARGS}
-    BUILD_ALWAYS
-      ON # cmake doesn't auto-detect changes without a download method
-    INSTALL_COMMAND
-      "" # skip install
+    BUILD_ALWAYS ON  # cmake doesn't auto-detect changes without a download method
+    INSTALL_COMMAND ""  # skip install
     DEPENDS ${EXTRA_DEPENDS}
   )
   list(APPEND EXTRA_DEPENDS stage0)
 endif()
-ExternalProject_Add(
-  stage1
+ExternalProject_add(stage1
   SOURCE_DIR "${LEAN_SOURCE_DIR}"
   SOURCE_SUBDIR src
   BINARY_DIR stage1
-  CMAKE_ARGS
-    -DSTAGE=1 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage0
-    -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${STAGE0_CMAKE_EXECUTABLE_SUFFIX} ${CL_ARGS} ${STAGE1_ARGS}
+  CMAKE_ARGS -DSTAGE=1 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage0 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${STAGE0_CMAKE_EXECUTABLE_SUFFIX} ${CL_ARGS} ${STAGE1_ARGS}
   BUILD_ALWAYS ON
   INSTALL_COMMAND ""
   DEPENDS ${EXTRA_DEPENDS}
   STEP_TARGETS configure
 )
-ExternalProject_Add(
-  stage2
+ExternalProject_add(stage2
   SOURCE_DIR "${LEAN_SOURCE_DIR}"
   SOURCE_SUBDIR src
   BINARY_DIR stage2
-  CMAKE_ARGS
-    -DSTAGE=2 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage1 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX}
-    ${CL_ARGS}
+  CMAKE_ARGS -DSTAGE=2 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage1 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX} ${CL_ARGS}
   BUILD_ALWAYS ON
   INSTALL_COMMAND ""
   DEPENDS stage1
   EXCLUDE_FROM_ALL ON
   STEP_TARGETS configure
 )
-ExternalProject_Add(
-  stage3
+ExternalProject_add(stage3
   SOURCE_DIR "${LEAN_SOURCE_DIR}"
   SOURCE_SUBDIR src
   BINARY_DIR stage3
-  CMAKE_ARGS
-    -DSTAGE=3 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage2 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX}
-    ${CL_ARGS}
+  CMAKE_ARGS -DSTAGE=3 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage2 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX} ${CL_ARGS}
   BUILD_ALWAYS ON
   INSTALL_COMMAND ""
   DEPENDS stage2
   EXCLUDE_FROM_ALL ON
-  STEP_TARGETS configure
 )
 
 # targets forwarded to appropriate stages
 
-add_custom_target(update-stage0 COMMAND $(MAKE) -C stage1 update-stage0 DEPENDS stage1)
+add_custom_target(update-stage0
+  COMMAND $(MAKE) -C stage1 update-stage0
+  DEPENDS stage1)
 
-add_custom_target(update-stage0-commit COMMAND $(MAKE) -C stage1 update-stage0-commit DEPENDS stage1)
+add_custom_target(update-stage0-commit
+  COMMAND $(MAKE) -C stage1 update-stage0-commit
+  DEPENDS stage1)
 
-add_custom_target(test COMMAND $(MAKE) -C stage1 test DEPENDS stage1)
+add_custom_target(test
+  COMMAND $(MAKE) -C stage1 test
+  DEPENDS stage1)
 
-add_custom_target(
-  bench
-  COMMAND $(MAKE) -C stage2
-  COMMAND $(MAKE) -C stage2 -j1 bench
-  DEPENDS stage2
-)
-add_custom_target(
-  bench-part1
-  COMMAND $(MAKE) -C stage2
-  COMMAND $(MAKE) -C stage2 -j1 bench-part1
-  DEPENDS stage2
-)
-add_custom_target(
-  bench-part2
-  COMMAND $(MAKE) -C stage2
-  COMMAND $(MAKE) -C stage2 -j1 bench-part2
-  DEPENDS stage2
-)
-
-add_custom_target(clean-stdlib COMMAND $(MAKE) -C stage1 clean-stdlib DEPENDS stage1)
+add_custom_target(clean-stdlib
+  COMMAND $(MAKE) -C stage1 clean-stdlib
+  DEPENDS stage1)
 
 install(CODE "execute_process(COMMAND make -C stage1 install)")
 
-add_custom_target(check-stage3 COMMAND diff "stage2/bin/lean" "stage3/bin/lean" DEPENDS stage3)
+add_custom_target(check-stage3
+  COMMAND diff "stage2/bin/lean" "stage3/bin/lean"
+  DEPENDS stage3)

CMakePresets.json

@@ -41,7 +41,7 @@
         "SMALL_ALLOCATOR": "OFF",
         "USE_MIMALLOC": "OFF",
         "BSYMBOLIC": "OFF",
-        "LEAN_TEST_VARS": "MAIN_STACK_SIZE=16000 TEST_STACK_SIZE=16000 LSAN_OPTIONS=max_leaks=10"
+        "LEAN_TEST_VARS": "MAIN_STACK_SIZE=16000 LSAN_OPTIONS=max_leaks=10"
       },
       "generator": "Unix Makefiles",
       "binaryDir": "${sourceDir}/build/sanitize"

CONTRIBUTING.md

@@ -7,7 +7,7 @@ Helpful links
 -------
 
 * [Development Setup](./doc/dev/index.md)
-* [Testing](./tests/README.md)
+* [Testing](./doc/dev/testing.md)
 * [Commit convention](./doc/dev/commit_convention.md)
 
 Before You Submit a Pull Request (PR):

LICENSES

@@ -1370,208 +1370,4 @@ FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
-SOFTWARE.
-==============================================================================
-leantar is by Mario Carneiro and distributed under the Apache 2.0 License:
-==============================================================================
-                                 Apache License
-                           Version 2.0, January 2004
-                        http://www.apache.org/licenses/
-
-   TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
-
-   1. Definitions.
-
-      "License" shall mean the terms and conditions for use, reproduction,
-      and distribution as defined by Sections 1 through 9 of this document.
-
-      "Licensor" shall mean the copyright owner or entity authorized by
-      the copyright owner that is granting the License.
-
-      "Legal Entity" shall mean the union of the acting entity and all
-      other entities that control, are controlled by, or are under common
-      control with that entity. For the purposes of this definition,
-      "control" means (i) the power, direct or indirect, to cause the
-      direction or management of such entity, whether by contract or
-      otherwise, or (ii) ownership of fifty percent (50%) or more of the
-      outstanding shares, or (iii) beneficial ownership of such entity.
-
-      "You" (or "Your") shall mean an individual or Legal Entity
-      exercising permissions granted by this License.
-
-      "Source" form shall mean the preferred form for making modifications,
-      including but not limited to software source code, documentation
-      source, and configuration files.
-
-      "Object" form shall mean any form resulting from mechanical
-      transformation or translation of a Source form, including but
-      not limited to compiled object code, generated documentation,
-      and conversions to other media types.
-
-      "Work" shall mean the work of authorship, whether in Source or
-      Object form, made available under the License, as indicated by a
-      copyright notice that is included in or attached to the work
-      (an example is provided in the Appendix below).
-
-      "Derivative Works" shall mean any work, whether in Source or Object
-      form, that is based on (or derived from) the Work and for which the
-      editorial revisions, annotations, elaborations, or other modifications
-      represent, as a whole, an original work of authorship. For the purposes
-      of this License, Derivative Works shall not include works that remain
-      separable from, or merely link (or bind by name) to the interfaces of,
-      the Work and Derivative Works thereof.
-
-      "Contribution" shall mean any work of authorship, including
-      the original version of the Work and any modifications or additions
-      to that Work or Derivative Works thereof, that is intentionally
-      submitted to Licensor for inclusion in the Work by the copyright owner
-      or by an individual or Legal Entity authorized to submit on behalf of
-      the copyright owner. For the purposes of this definition, "submitted"
-      means any form of electronic, verbal, or written communication sent
-      to the Licensor or its representatives, including but not limited to
-      communication on electronic mailing lists, source code control systems,
-      and issue tracking systems that are managed by, or on behalf of, the
-      Licensor for the purpose of discussing and improving the Work, but
-      excluding communication that is conspicuously marked or otherwise
-      designated in writing by the copyright owner as "Not a Contribution."
-
-      "Contributor" shall mean Licensor and any individual or Legal Entity
-      on behalf of whom a Contribution has been received by Licensor and
-      subsequently incorporated within the Work.
-
-   2. Grant of Copyright License. Subject to the terms and conditions of
-      this License, each Contributor hereby grants to You a perpetual,
-      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
-      copyright license to reproduce, prepare Derivative Works of,
-      publicly display, publicly perform, sublicense, and distribute the
-      Work and such Derivative Works in Source or Object form.
-
-   3. Grant of Patent License. Subject to the terms and conditions of
-      this License, each Contributor hereby grants to You a perpetual,
-      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
-      (except as stated in this section) patent license to make, have made,
-      use, offer to sell, sell, import, and otherwise transfer the Work,
-      where such license applies only to those patent claims licensable
-      by such Contributor that are necessarily infringed by their
-      Contribution(s) alone or by combination of their Contribution(s)
-      with the Work to which such Contribution(s) was submitted. If You
-      institute patent litigation against any entity (including a
-      cross-claim or counterclaim in a lawsuit) alleging that the Work
-      or a Contribution incorporated within the Work constitutes direct
-      or contributory patent infringement, then any patent licenses
-      granted to You under this License for that Work shall terminate
-      as of the date such litigation is filed.
-
-   4. Redistribution. You may reproduce and distribute copies of the
-      Work or Derivative Works thereof in any medium, with or without
-      modifications, and in Source or Object form, provided that You
-      meet the following conditions:
-
-      (a) You must give any other recipients of the Work or
-          Derivative Works a copy of this License; and
-
-      (b) You must cause any modified files to carry prominent notices
-          stating that You changed the files; and
-
-      (c) You must retain, in the Source form of any Derivative Works
-          that You distribute, all copyright, patent, trademark, and
-          attribution notices from the Source form of the Work,
-          excluding those notices that do not pertain to any part of
-          the Derivative Works; and
-
-      (d) If the Work includes a "NOTICE" text file as part of its
-          distribution, then any Derivative Works that You distribute must
-          include a readable copy of the attribution notices contained
-          within such NOTICE file, excluding those notices that do not
-          pertain to any part of the Derivative Works, in at least one
-          of the following places: within a NOTICE text file distributed
-          as part of the Derivative Works; within the Source form or
-          documentation, if provided along with the Derivative Works; or,
-          within a display generated by the Derivative Works, if and
-          wherever such third-party notices normally appear. The contents
-          of the NOTICE file are for informational purposes only and
-          do not modify the License. You may add Your own attribution
-          notices within Derivative Works that You distribute, alongside
-          or as an addendum to the NOTICE text from the Work, provided
-          that such additional attribution notices cannot be construed
-          as modifying the License.
-
-      You may add Your own copyright statement to Your modifications and
-      may provide additional or different license terms and conditions
-      for use, reproduction, or distribution of Your modifications, or
-      for any such Derivative Works as a whole, provided Your use,
-      reproduction, and distribution of the Work otherwise complies with
-      the conditions stated in this License.
-
-   5. Submission of Contributions. Unless You explicitly state otherwise,
-      any Contribution intentionally submitted for inclusion in the Work
-      by You to the Licensor shall be under the terms and conditions of
-      this License, without any additional terms or conditions.
-      Notwithstanding the above, nothing herein shall supersede or modify
-      the terms of any separate license agreement you may have executed
-      with Licensor regarding such Contributions.
-
-   6. Trademarks. This License does not grant permission to use the trade
-      names, trademarks, service marks, or product names of the Licensor,
-      except as required for reasonable and customary use in describing the
-      origin of the Work and reproducing the content of the NOTICE file.
-
-   7. Disclaimer of Warranty. Unless required by applicable law or
-      agreed to in writing, Licensor provides the Work (and each
-      Contributor provides its Contributions) on an "AS IS" BASIS,
-      WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
-      implied, including, without limitation, any warranties or conditions
-      of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A
-      PARTICULAR PURPOSE. You are solely responsible for determining the
-      appropriateness of using or redistributing the Work and assume any
-      risks associated with Your exercise of permissions under this License.
-
-   8. Limitation of Liability. In no event and under no legal theory,
-      whether in tort (including negligence), contract, or otherwise,
-      unless required by applicable law (such as deliberate and grossly
-      negligent acts) or agreed to in writing, shall any Contributor be
-      liable to You for damages, including any direct, indirect, special,
-      incidental, or consequential damages of any character arising as a
-      result of this License or out of the use or inability to use the
-      Work (including but not limited to damages for loss of goodwill,
-      work stoppage, computer failure or malfunction, or any and all
-      other commercial damages or losses), even if such Contributor
-      has been advised of the possibility of such damages.
-
-   9. Accepting Warranty or Additional Liability. While redistributing
-      the Work or Derivative Works thereof, You may choose to offer,
-      and charge a fee for, acceptance of support, warranty, indemnity,
-      or other liability obligations and/or rights consistent with this
-      License. However, in accepting such obligations, You may act only
-      on Your own behalf and on Your sole responsibility, not on behalf
-      of any other Contributor, and only if You agree to indemnify,
-      defend, and hold each Contributor harmless for any liability
-      incurred by, or claims asserted against, such Contributor by reason
-      of your accepting any such warranty or additional liability.
-
-   END OF TERMS AND CONDITIONS
-
-   APPENDIX: How to apply the Apache License to your work.
-
-      To apply the Apache License to your work, attach the following
-      boilerplate notice, with the fields enclosed by brackets "[]"
-      replaced with your own identifying information. (Don't include
-      the brackets!)  The text should be enclosed in the appropriate
-      comment syntax for the file format. We also recommend that a
-      file or class name and description of purpose be included on the
-      same "printed page" as the copyright notice for easier
-      identification within third-party archives.
-
-   Copyright [yyyy] [name of copyright owner]
-
-   Licensed under the Apache License, Version 2.0 (the "License");
-   you may not use this file except in compliance with the License.
-   You may obtain a copy of the License at
-
-       http://www.apache.org/licenses/LICENSE-2.0
-
-   Unless required by applicable law or agreed to in writing, software
-   distributed under the License is distributed on an "AS IS" BASIS,
-   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
-   See the License for the specific language governing permissions and
-   limitations under the License.
+SOFTWARE.

doc/.gitignore

@@ -0,0 +1 @@
+out

doc/dev/bootstrap.md

@@ -6,7 +6,7 @@ building Lean itself - which is needed to again build those parts. This cycle is
 broken by using pre-built C files checked into the repository (which ultimately
 go back to a point where the Lean compiler was not written in Lean) in place of
 these Lean inputs and then compiling everything in multiple stages up to a fixed
-point. The build directory is organized into these stages:
+point. The build directory is organized in these stages:
 
 ```bash
 stage0/
@@ -79,7 +79,7 @@ with the contents of `src/stdlib_flags.h`, bringing them back in sync.
 NOTE: A full rebuild of stage 1 will only be triggered when the *committed* contents of `stage0/` are changed.
 Thus if you change files in it manually instead of through `update-stage0-commit` (see below) or fetching updates from git, you either need to commit those changes first or run `make -C build/release clean-stdlib`.
 The same is true for further stages except that a rebuild of them is retriggered on any committed change, not just to a specific directory.
-Thus when debugging e.g. stage 2 failures, you can resume the build from these failures on but you may want to explicitly call `clean-stdlib` to either observe changes from `.olean` files of modules that built successfully or to check that you did not break modules that built successfully at some prior point.
+Thus when debugging e.g. stage 2 failures, you can resume the build from these failures on but may want to explicitly call `clean-stdlib` to either observe changes from `.olean` files of modules that built successfully or to check that you did not break modules that built successfully at some prior point.
 
 If you have write access to the lean4 repository, you can also manually
 trigger that process, for example to be able to use new features in the compiler itself.
@@ -101,7 +101,7 @@ The script `script/rebase-stage0.sh` can be used for that.
 
 The CI should prevent PRs with changes to stage0 (besides `stdlib_flags.h`)
 from entering `master` through the (squashing!) merge queue, and label such PRs
-with the `changes-stage0` label. Such PRs should have a cleaned-up history,
+with the `changes-stage0` label. Such PRs should have a cleaned up history,
 with separate stage0 update commits; then coordinate with the admins to merge
 your PR using rebase merge, bypassing the merge queue.
 

doc/dev/index.md

@@ -1,9 +1,7 @@
 # Development Workflow
 
 If you want to make changes to Lean itself, start by [building Lean](../make/index.md) from a clean checkout to make sure that everything is set up correctly.
-After that, read on below to find out how to set up your editor for changing the Lean source code,
-followed by further sections of the development manual where applicable
-such as on the [test suite](../../tests/README.md) and [commit convention](commit_convention.md).
+After that, read on below to find out how to set up your editor for changing the Lean source code, followed by further sections of the development manual where applicable such as on the [test suite](testing.md) and [commit convention](commit_convention.md).
 
 If you are planning to make any changes that may affect the compilation of Lean itself, e.g. changes to the parser, elaborator, or compiler, you should first read about the [bootstrapping pipeline](bootstrap.md).
 You should not edit the `stage0` directory except using the commands described in that section when necessary.
@@ -63,10 +61,10 @@ you can then put `my_name/lean4:my-tag` in your `lean-toolchain` file in a proje
 
 ### VS Code
 
-There is a `.vscode/` directory that correctly sets up VS Code with settings, tasks, and recommended extensions.
-Simply open the repository folder in VS Code, such as by invoking
+There is a `lean.code-workspace` file that correctly sets up VS Code with workspace roots for the stage0/stage1 setup described above as well as with other settings.
+You should always load it when working on Lean, such as by invoking
 ```
-code .
+code lean.code-workspace
 ```
 on the command line.
 

doc/dev/release_checklist.md

@@ -30,7 +30,7 @@ We'll use `v4.6.0` as the intended release version as a running example.
     run `script/release_notes.py --since v4.5.0` on the `releases/v4.6.0` branch,
     and see the section "Writing the release notes" below for more information.
   - Release notes live in https://github.com/leanprover/reference-manual, in e.g. `Manual/Releases/v4.6.0.lean`.
-    It's best if you update these at the same time as you update the `lean-toolchain` for the `reference-manual` repository, see below.
+    It's best if you update these at the same time as a you update the `lean-toolchain` for the `reference-manual` repository, see below.
 - Go to https://github.com/leanprover/lean4/releases and verify that the `v4.6.0` release appears.
   - Verify on Github that "Set as the latest release" is checked.
 - Next, we will move a curated list of downstream repos to the latest stable release.
@@ -54,7 +54,7 @@ We'll use `v4.6.0` as the intended release version as a running example.
     - `verso`:
       - The `subverso` dependency is unusual in that it needs to be compatible with _every_ Lean release simultaneously.
         Usually you don't need to do anything.
-        If you think something is wrong here, please contact David Thrane Christiansen (@david-christiansen)
+        If you think something is wrong here please contact David Thrane Christiansen (@david-christiansen)
       - Warnings during `lake update` and `lake build` are expected.
     - `reference-manual`: the release notes generated by `script/release_notes.py` as described above must be included in
       `Manual/Releases/v4.6.0.lean`, and `import` and `include` statements adding in `Manual/Releases.lean`. 
@@ -65,14 +65,7 @@ We'll use `v4.6.0` as the intended release version as a running example.
       - The `lakefile.toml` should always refer to dependencies via their `main` or `master` branch,
         not a toolchain tag
         (with the exception of `ProofWidgets4`, which *must* use a sequential version tag).
-      - **Important:** After creating and pushing the ProofWidgets4 tag (see above),
-        the mathlib4 lakefile must be updated to reference the new tag (e.g. `v0.0.87`).
-        The `release_steps.py` script handles this automatically by looking up the latest
-        ProofWidgets4 tag compatible with the target toolchain.
       - Push the PR branch to the main Mathlib repository rather than a fork, or CI may not work reliably
-      - The "Verify Transient and Automated Commits" CI check on toolchain bump PRs can be ignored —
-        it often fails on automated commits (`x:` prefixed) from the nightly-testing history that can't be
-        reproduced in CI. This does not block merging.
     - `repl`:
       There are two copies of `lean-toolchain`/`lakefile.lean`:
       in the root, and in `test/Mathlib/`. Edit both, and run `lake update` in both directories.
@@ -153,9 +146,6 @@ We'll use `v4.7.0-rc1` as the intended release version in this example.
     * The repository does not need any changes to move to the new version.
     * Note that sometimes there are *unreviewed* but necessary changes on the `nightly-testing` branch of the repository.
       If so, you will need to merge these into the `bump_to_v4.7.0-rc1` branch manually.
-    * The `nightly-testing` branch may also contain temporary fix scripts (e.g. `fix_backward_defeq.py`,
-      `fix_deprecations.py`) that were used to adapt to breaking changes during the nightly cycle.
-      These should be reviewed and removed if no longer needed, as they can interfere with CI checks.
   - For each of the repositories listed in `script/release_repos.yml`,
     - Run `script/release_steps.py v4.7.0-rc1 <repo>` (e.g. replacing `<repo>` with `batteries`), which will walk you through the following steps:
       - Create a new branch off `master`/`main` (as specified in the `branch` field), called `bump_to_v4.7.0-rc1`.
@@ -228,21 +218,6 @@ Please read https://leanprover-community.github.io/contribute/tags_and_branches.
 
 # Writing the release notes
 
-Release notes content is only written for the first release candidate (`-rc1`). For subsequent RCs and stable releases,
-just update the title in the existing release notes file (see "Release notes title format" below).
-
-## Release notes title format
-
-The title in the `#doc (Manual)` line must follow these formats:
-
-- **For -rc1**: `"Lean 4.7.0-rc1 (2024-03-15)"` — Include the RC suffix and the release date
-- **For -rc2, -rc3, etc.**: `"Lean 4.7.0-rc2 (2024-03-20)"` — Update the RC number and date
-- **For stable release**: `"Lean 4.7.0 (2024-04-01)"` — Remove the RC suffix but keep the date
-
-The date should be the actual date when the tag was pushed (or when CI completed and created the release page).
-
-## 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.
@@ -257,113 +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 (2024-03-15)" =>
-%%%
-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
-
-**Important: Timing with the reference-manual tag**
-
-The reference-manual repository deploys documentation when a version tag is pushed. If you merge
-release notes AFTER the tag is created, the deployed documentation won't include them.
-
-You have two options:
-
-1. **Preferred**: Include the release notes in the same PR as the toolchain bump (or merge the
-   release notes PR before creating the tag). This ensures the tag includes the release notes.
-
-2. **If release notes are merged after the tag**: You must regenerate the tag to trigger a new deployment:
-   ```bash
-   cd /path/to/reference-manual
-   git fetch origin
-   git tag -d v4.7.0-rc1  # Delete local tag
-   git tag v4.7.0-rc1 origin/main  # Create tag at current main (which has release notes)
-   git push origin :refs/tags/v4.7.0-rc1  # Delete remote tag
-   git push origin v4.7.0-rc1  # Push new tag (triggers Deploy workflow)
-   ```
-
-If creating a separate PR for release notes:
-```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.

doc/dev/testing.md

@@ -0,0 +1,138 @@
+# Test Suite
+
+After [building Lean](../make/index.md) you can run all the tests using
+```
+cd build/release
+make test ARGS=-j4
+```
+Change the 4 to the maximum number of parallel tests you want to
+allow. The best choice is the number of CPU cores on your machine as
+the tests are mostly CPU bound.  You can find the number of processors
+on linux using `nproc` and on Windows it is the `NUMBER_OF_PROCESSORS`
+environment variable.
+
+You can run tests after [building a specific stage](bootstrap.md) by
+adding the `-C stageN` argument. The default when run as above is stage 1.  The
+Lean tests will automatically use that stage's corresponding Lean
+executables
+
+Running `make test` will not pick up new test files; run
+```bash
+cmake build/release/stage1
+```
+to update the list of tests.
+
+You can also use `ctest` directly if you are in the right folder.  So
+to run stage1 tests with a 300 second timeout run this:
+
+```bash
+cd build/release/stage1
+ctest -j 4 --output-on-failure --timeout 300
+```
+Useful `ctest` flags are `-R <name of test>` to run a single test, and
+`--rerun-failed` to run all tests that failed during the last run.
+You can also pass `ctest` flags via `make test ARGS="--rerun-failed"`.
+
+To get verbose output from ctest pass the `--verbose` command line
+option. Test output is normally suppressed and only summary
+information is displayed. This option will show all test output.
+
+## Test Suite Organization
+
+All these tests are included by [src/shell/CMakeLists.txt](https://github.com/leanprover/lean4/blob/master/src/shell/CMakeLists.txt):
+
+- [`tests/lean`](https://github.com/leanprover/lean4/tree/master/tests/lean/): contains tests that come equipped with a
+  .lean.expected.out file. The driver script [`test_single.sh`](https://github.com/leanprover/lean4/tree/master/tests/lean/test_single.sh) runs
+  each test and checks the actual output (*.produced.out) with the
+  checked in expected output.
+
+- [`tests/lean/run`](https://github.com/leanprover/lean4/tree/master/tests/lean/run/): contains tests that are run through the lean
+  command line one file at a time. These tests only look for error
+  codes and do not check the expected output even though output is
+  produced, it is ignored.
+
+  **Note:** Tests in this directory run with `-Dlinter.all=false` to reduce noise.
+  If your test needs to verify linter behavior (e.g., deprecation warnings),
+  explicitly enable the relevant linter with `set_option linter.<name> true`.
+
+- [`tests/lean/interactive`](https://github.com/leanprover/lean4/tree/master/tests/lean/interactive/): are designed to test server requests at a
+  given position in the input file. Each .lean file contains comments
+  that indicate how to simulate a client request at that position.
+  using a `--^` point to the line position. Example:
+    ```lean,ignore
+    open Foo in
+    theorem tst2 (h : a ≤ b) : a + 2 ≤ b + 2 :=
+    Bla.
+      --^ completion
+    ```
+    In this example, the test driver [`test_single.sh`](https://github.com/leanprover/lean4/tree/master/tests/lean/interactive/test_single.sh) will simulate an
+    auto-completion request at `Bla.`. The expected output is stored in
+    a .lean.expected.out in the json format that is part of the
+    [Language Server
+    Protocol](https://microsoft.github.io/language-server-protocol/).
+
+    This can also be used to test the following additional requests:
+    ```
+    --^ textDocument/hover
+    --^ textDocument/typeDefinition
+    --^ textDocument/definition
+    --^ $/lean/plainGoal
+    --^ $/lean/plainTermGoal
+    --^ insert: ...
+    --^ collectDiagnostics
+    ```
+
+- [`tests/lean/server`](https://github.com/leanprover/lean4/tree/master/tests/lean/server/): Tests more of the Lean `--server` protocol.
+  There are just a few of them, and it uses .log files containing
+  JSON.
+
+- [`tests/compiler`](https://github.com/leanprover/lean4/tree/master/tests/compiler/): contains tests that will run the Lean compiler and
+  build an executable that is executed and the output is compared to
+  the .lean.expected.out file. This test also contains a subfolder
+  [`foreign`](https://github.com/leanprover/lean4/tree/master/tests/compiler/foreign/) which shows how to extend Lean using C++.
+
+- [`tests/lean/trust0`](https://github.com/leanprover/lean4/tree/master/tests/lean/trust0): tests that run Lean in a mode that Lean doesn't
+  even trust the .olean files (i.e., trust 0).
+
+- [`tests/bench`](https://github.com/leanprover/lean4/tree/master/tests/bench/): contains performance tests.
+
+- [`tests/plugin`](https://github.com/leanprover/lean4/tree/master/tests/plugin/): tests that compiled Lean code can be loaded into
+  `lean` via the `--plugin` command line option.
+
+## Writing Good Tests
+
+Every test file should contain:
+* an initial `/-! -/` module docstring summarizing the test's purpose
+* a module docstring for each test section that describes what is tested
+  and, if not 100% clear, why that is the desirable behavior
+
+At the time of writing, most tests do not follow these new guidelines yet.
+For an example of a conforming test, see [`tests/lean/1971.lean`](https://github.com/leanprover/lean4/tree/master/tests/lean/1971.lean).
+
+## Fixing Tests
+
+When the Lean source code or the standard library are modified, some of the
+tests break because the produced output is slightly different, and we have
+to reflect the changes in the `.lean.expected.out` files.
+We should not blindly copy the new produced output since we may accidentally
+miss a bug introduced by recent changes.
+The test suite contains commands that allow us to see what changed in a convenient way.
+First, we must install [meld](http://meldmerge.org/). On Ubuntu, we can do it by simply executing
+
+```
+sudo apt-get install meld
+```
+
+Now, suppose `bad_class.lean` test is broken. We can see the problem by going to [`tests/lean`](https://github.com/leanprover/lean4/tree/master/tests/lean) directory and
+executing
+
+```
+./test_single.sh -i bad_class.lean
+```
+
+When the `-i` option is provided, `meld` is automatically invoked
+whenever there is discrepancy between the produced and expected
+outputs. `meld` can also be used to repair the problems.
+
+In Emacs, we can also execute `M-x lean4-diff-test-file` to check/diff the file of the current buffer.
+To mass-copy all `.produced.out` files to the respective `.expected.out` file, use `tests/lean/copy-produced`.

doc/examples/.gitignore

@@ -1,2 +0,0 @@
-*.out.produced
-*.exit.produced

doc/examples/IJCAR2026/README.md

@@ -1,6 +0,0 @@
-# IJCAR 2026: `grind`, An SMT-Inspired Tactic for Lean 4
-
-Ancillary materials for the paper.
-
-- `examples.lean`: interactive examples from the paper
-- `analyze_grind_loc.py`: script used for the evaluation section, analyzing `grind` adoption and lines-of-code changes in Mathlib

doc/examples/IJCAR2026/analyze_grind_loc.py

@@ -1,401 +0,0 @@
-#!/usr/bin/env python3
-"""
-Analyze grind adoption LoC changes in mathlib.
-
-For each theorem/lemma in master that uses grind, find the most recent
-commit where it didn't use grind, and measure the LoC change.
-
-This script was used in preparing the "Evaluation" section of the grind paper.
-"""
-
-import subprocess
-import re
-import csv
-import sys
-from pathlib import Path
-from dataclasses import dataclass
-from concurrent.futures import ThreadPoolExecutor, as_completed
-from typing import Iterator
-from functools import lru_cache
-
-
-@dataclass
-class GrindUsage:
-    file: str
-    line_no: int
-    decl_name: str
-    decl_type: str  # theorem, lemma, def, example, etc.
-
-
-@dataclass
-class LocChange:
-    file: str
-    decl_name: str
-    decl_type: str
-    old_loc: int
-    new_loc: int
-    loc_saved: int
-    commit_sha: str
-    commit_date: str
-
-
-def run_git(args: list[str], repo: str = ".") -> str:
-    """Run a git command and return stdout."""
-    result = subprocess.run(
-        ["git", "-C", repo] + args,
-        capture_output=True, text=True, check=True
-    )
-    return result.stdout
-
-
-def run_git_safe(args: list[str], repo: str = ".") -> str | None:
-    """Run a git command, return None on failure."""
-    result = subprocess.run(
-        ["git", "-C", repo] + args,
-        capture_output=True, text=True
-    )
-    if result.returncode != 0:
-        return None
-    return result.stdout
-
-
-@lru_cache(maxsize=4096)
-def get_file_at_commit(repo: str, commit: str, file_path: str) -> str | None:
-    """Get file contents at a specific commit (cached)."""
-    return run_git_safe(["show", f"{commit}:{file_path}"], repo)
-
-
-def find_grind_usages(repo: str = ".") -> tuple[list[GrindUsage], int, int]:
-    """Find all declarations using grind in current master.
-    Returns (usages, total_grind_calls, grind_in_decls) where:
-    - total_grind_calls is the count of grind tactic calls (after filtering comments/attrs)
-    - grind_in_decls is the count of those that are inside named declarations
-    """
-    # Use git grep to find lines containing 'grind' (excludes lake packages)
-    result = run_git(["grep", "-n", "grind", "master", "--", "Mathlib/"], repo)
-
-    usages = []
-    seen = set()  # (file, decl_name) to dedupe
-    total_grind_calls = 0
-    grind_in_decls = 0
-
-    for line in result.strip().split('\n'):
-        if not line:
-            continue
-        # Format: master:path/to/file.lean:123:line content
-        match = re.match(r'^master:(.+\.lean):(\d+):(.*)$', line)
-        if not match:
-            continue
-
-        file_path, line_no_str, content = match.groups()
-        line_no = int(line_no_str)
-
-        # Skip comments and attributes (not tactic calls)
-        content_stripped = content.strip()
-        if content_stripped.startswith('--') or content_stripped.startswith('/-'):
-            continue
-        if content_stripped.startswith('attribute'):
-            continue
-        if '@[' in content and 'grind' in content:
-            # Could be an attribute like @[grind =], skip
-            if 'by' not in content and ':=' not in content:
-                continue
-
-        total_grind_calls += 1
-
-        # Find the declaration this grind belongs to
-        decl_name, decl_type = find_decl_at_line(repo, file_path, line_no)
-        if decl_name is None:
-            continue
-
-        grind_in_decls += 1
-
-        key = (file_path, decl_name)
-        if key in seen:
-            continue
-        seen.add(key)
-
-        usages.append(GrindUsage(
-            file=file_path,
-            line_no=line_no,
-            decl_name=decl_name,
-            decl_type=decl_type
-        ))
-
-    return usages, total_grind_calls, grind_in_decls
-
-
-def find_decl_at_line(repo: str, file_path: str, grind_line: int) -> tuple[str | None, str | None]:
-    """
-    Find the declaration name and type that contains the grind at the given line.
-    Search backwards from grind_line to find the most recent declaration.
-    """
-    # Get file content at master
-    content = get_file_at_commit(repo, "master", file_path)
-    if content is None:
-        return None, None
-
-    lines = content.split('\n')
-
-    # Search backwards from grind_line for a declaration
-    # Match declarations with optional leading modifiers and attributes
-    decl_pattern = re.compile(r'^(?:@\[.*?\]\s*)*(?:private\s+|protected\s+|noncomputable\s+|scoped\s+)*(theorem|lemma|def|example|instance|abbrev|structure|class)\s+(\w+)')
-
-    for i in range(grind_line - 1, -1, -1):
-        if i >= len(lines):
-            continue
-        line = lines[i]
-        match = decl_pattern.match(line)
-        if match:
-            return match.group(2), match.group(1)
-
-    return None, None
-
-
-def find_grind_introduction_commit(repo: str, file_path: str, decl_name: str) -> str | None:
-    """
-    Find the commit that introduced grind to this declaration.
-    Returns None if the declaration was born with grind.
-    """
-    # First, find the line range of the declaration in master
-    content = get_file_at_commit(repo, "master", file_path)
-    if content is None:
-        return None
-
-    lines = content.split('\n')
-    decl_start = None
-    decl_end = None
-
-    # Find declaration start
-    decl_pattern = re.compile(rf'^(?:@\[.*?\]\s*)*(?:private\s+|protected\s+|noncomputable\s+|scoped\s+)*(theorem|lemma|def|example|instance|abbrev|structure|class)\s+{re.escape(decl_name)}\b')
-    for i, line in enumerate(lines):
-        if decl_pattern.match(line):
-            decl_start = i
-            break
-
-    if decl_start is None:
-        return None
-
-    # Find declaration end (next top-level declaration or EOF)
-    end_patterns = re.compile(r'^(?:private\s+|protected\s+|noncomputable\s+|scoped\s+)*(theorem|lemma|def|example|instance|abbrev|structure|class|namespace|section|end\s|@\[|#|/-)')
-    for i in range(decl_start + 1, len(lines)):
-        line = lines[i]
-        if line and not line[0].isspace() and end_patterns.match(line):
-            decl_end = i
-            break
-    if decl_end is None:
-        decl_end = len(lines)
-
-    # Find grind line within declaration
-    grind_line = None
-    for i in range(decl_start, decl_end):
-        if 'grind' in lines[i]:
-            grind_line = i + 1  # 1-indexed
-            break
-
-    if grind_line is None:
-        return None
-
-    # Use git blame to find when that grind line was added
-    blame_result = run_git_safe(["blame", "-L", f"{grind_line},{grind_line}", "--porcelain", "master", "--", file_path], repo)
-    if blame_result is None:
-        return None
-
-    # First line of porcelain output is the commit SHA
-    first_line = blame_result.split('\n')[0]
-    commit_sha = first_line.split()[0]
-
-    # Check if this declaration existed before this commit (without grind)
-    parent_sha = run_git_safe(["rev-parse", f"{commit_sha}^"], repo)
-    if parent_sha is None:
-        return None  # Initial commit, born with grind
-    parent_sha = parent_sha.strip()
-
-    # Check if declaration existed in parent
-    parent_content = get_file_at_commit(repo, parent_sha, file_path)
-    if parent_content is None:
-        # File didn't exist in parent - might be new file or renamed
-        return None
-
-    # Check if declaration existed and didn't have grind
-    if decl_name not in parent_content:
-        return None  # Declaration didn't exist - born with grind
-
-    # Check if it already had grind in parent
-    parent_lines = parent_content.split('\n')
-    in_decl = False
-    for line in parent_lines:
-        if decl_pattern.match(line):
-            in_decl = True
-        elif in_decl:
-            if line and not line[0].isspace() and end_patterns.match(line):
-                break
-            if 'grind' in line:
-                # Already had grind in parent — not the introduction commit
-                return None
-
-    return commit_sha
-
-
-def extract_proof_loc(repo: str, file_path: str, decl_name: str, commit: str) -> int | None:
-    """
-    Extract the number of lines in a declaration's proof at a given commit.
-    Returns None if the declaration doesn't exist at that commit.
-    """
-    content = get_file_at_commit(repo, commit, file_path)
-    if content is None:
-        return None
-
-    lines = content.split('\n')
-
-    # Find declaration start
-    decl_pattern = re.compile(rf'^(?:@\[.*?\]\s*)*(?:private\s+|protected\s+|noncomputable\s+|scoped\s+)*(theorem|lemma|def|example|instance|abbrev|structure|class)\s+{re.escape(decl_name)}\b')
-    decl_start = None
-    for i, line in enumerate(lines):
-        if decl_pattern.match(line):
-            decl_start = i
-            break
-
-    if decl_start is None:
-        return None
-
-    # Find declaration end
-    end_patterns = re.compile(r'^(?:private\s+|protected\s+|noncomputable\s+|scoped\s+)*(theorem|lemma|def|example|instance|abbrev|structure|class|namespace|section|end\s|@\[|#|/-)')
-    decl_end = None
-    for i in range(decl_start + 1, len(lines)):
-        line = lines[i]
-        if line and not line[0].isspace() and end_patterns.match(line):
-            decl_end = i
-            break
-    if decl_end is None:
-        decl_end = len(lines)
-
-    # Count non-empty lines in declaration
-    loc = sum(1 for i in range(decl_start, decl_end) if lines[i].strip())
-    return loc
-
-
-def get_commit_date(repo: str, sha: str) -> str:
-    """Get the date of a commit."""
-    result = run_git(["log", "-1", "--format=%ci", sha], repo)
-    return result.strip().split()[0]  # Just the date part
-
-
-def analyze_usage_detailed(repo: str, usage: GrindUsage) -> tuple[LocChange | None, str]:
-    """Analyze a single grind usage, returning (result, skip_reason)."""
-    commit = find_grind_introduction_commit(repo, usage.file, usage.decl_name)
-    if commit is None:
-        return None, "born_with_grind"
-
-    parent = run_git_safe(["rev-parse", f"{commit}^"], repo)
-    if parent is None:
-        return None, "no_parent"
-    parent = parent.strip()
-
-    old_loc = extract_proof_loc(repo, usage.file, usage.decl_name, parent)
-    new_loc = extract_proof_loc(repo, usage.file, usage.decl_name, "master")
-
-    if old_loc is None:
-        return None, "old_loc_failed"
-    if new_loc is None:
-        return None, "new_loc_failed"
-
-    commit_date = get_commit_date(repo, commit)
-
-    return LocChange(
-        file=usage.file,
-        decl_name=usage.decl_name,
-        decl_type=usage.decl_type,
-        old_loc=old_loc,
-        new_loc=new_loc,
-        loc_saved=old_loc - new_loc,
-        commit_sha=commit[:12],
-        commit_date=commit_date
-    ), "success"
-
-
-def main(repo: str = "."):
-    print("Finding grind usages in master...", file=sys.stderr)
-    usages, total_grind_calls, grind_in_decls = find_grind_usages(repo)
-    print(f"Found {len(usages)} declarations using grind ({grind_in_decls}/{total_grind_calls} grind calls)", file=sys.stderr)
-
-    print("Analyzing git history (this may take a while)...", file=sys.stderr)
-    results: list[LocChange] = []
-    skip_reasons: dict[str, int] = {}
-
-    with ThreadPoolExecutor(max_workers=64) as executor:
-        futures = {executor.submit(analyze_usage_detailed, repo, usage): usage for usage in usages}
-
-        for i, future in enumerate(as_completed(futures)):
-            if (i + 1) % 50 == 0:
-                print(f"  Progress: {i + 1}/{len(usages)}", file=sys.stderr, flush=True)
-
-            result, reason = future.result()
-            if result:
-                results.append(result)
-            else:
-                skip_reasons[reason] = skip_reasons.get(reason, 0) + 1
-
-    total_skipped = sum(skip_reasons.values())
-    print(f"\nAnalyzed {len(results)} declarations, skipped {total_skipped}:", file=sys.stderr)
-    for reason, count in sorted(skip_reasons.items(), key=lambda x: -x[1]):
-        print(f"  - {reason}: {count}", file=sys.stderr)
-
-    # Sort by LoC saved (descending)
-    results.sort(key=lambda r: r.loc_saved, reverse=True)
-
-    # Output CSV
-    writer = csv.writer(sys.stdout)
-    writer.writerow(["file", "declaration", "type", "old_loc", "new_loc", "loc_saved", "commit", "date"])
-    for r in results:
-        writer.writerow([r.file, r.decl_name, r.decl_type, r.old_loc, r.new_loc, r.loc_saved, r.commit_sha, r.commit_date])
-
-    # Summary stats to stderr
-    total_old = sum(r.old_loc for r in results) if results else 0
-    total_new = sum(r.new_loc for r in results) if results else 0
-    total_saved = sum(r.loc_saved for r in results) if results else 0
-    avg_saved = total_saved / len(results) if results else 0
-
-    print("\n" + "=" * 60, file=sys.stderr)
-    print("GRIND ADOPTION LOC ANALYSIS", file=sys.stderr)
-    print("=" * 60, file=sys.stderr)
-
-    print("\n## Declaration Counts\n", file=sys.stderr)
-    print(f"  Total grind tactic calls:         {total_grind_calls}", file=sys.stderr)
-    print(f"  In named declarations:            {grind_in_decls} ({total_grind_calls - grind_in_decls} in anonymous/other)", file=sys.stderr)
-    print(f"  Unique declarations:              {len(usages)}", file=sys.stderr)
-    print(f"  Converted to grind:               {len(results)}", file=sys.stderr)
-    print(f"  Born with grind:                  {skip_reasons.get('born_with_grind', 0)}", file=sys.stderr)
-    if skip_reasons.get('old_loc_failed', 0) > 0:
-        print(f"  Could not trace history:          {skip_reasons.get('old_loc_failed', 0)}", file=sys.stderr)
-
-    print("\n## Lines of Code Impact\n", file=sys.stderr)
-    print(f"  Total LoC before grind:           {total_old}", file=sys.stderr)
-    print(f"  Total LoC after grind:            {total_new}", file=sys.stderr)
-    print(f"  Total LoC saved:                  {total_saved}", file=sys.stderr)
-    print(f"  Average LoC saved per theorem:    {avg_saved:.1f}", file=sys.stderr)
-    big_savings = sum(1 for r in results if r.loc_saved >= 10)
-    print(f"  Declarations shrunk by 10+ lines: {big_savings}", file=sys.stderr)
-
-    if results:
-        print("\n## Top 10 Biggest LoC Savings\n", file=sys.stderr)
-        for r in results[:10]:
-            print(f"  {r.loc_saved:+4d} lines: {r.decl_name} ({r.file})", file=sys.stderr)
-
-        # Show any that got bigger (negative savings)
-        got_bigger = [r for r in results if r.loc_saved < 0]
-        if got_bigger:
-            print(f"\n## Declarations That Got Bigger ({len(got_bigger)} total)\n", file=sys.stderr)
-            print("  (showing 5 worst):", file=sys.stderr)
-            for r in got_bigger[-5:]:  # Show worst 5
-                print(f"  {r.loc_saved:+4d} lines: {r.decl_name} ({r.file})", file=sys.stderr)
-
-    print("\n" + "=" * 60, file=sys.stderr)
-
-
-if __name__ == "__main__":
-    import argparse
-    parser = argparse.ArgumentParser(description="Analyze grind LoC savings")
-    parser.add_argument("--repo", "-r", default=".", help="Repository path")
-    args = parser.parse_args()
-    main(args.repo)

doc/examples/IJCAR2026/examples.lean

@@ -1,127 +0,0 @@
-/- Examples from the paper "grind: An SMT-Inspired Tactic for Lean 4" -/
-open Lean Grind
-
-/- Congruence closure. -/
-
-example (f : Nat → Nat) (h : a = b) : f (f b) = f (f a) := by grind
-
-/-
-E-matching.
-
-Any `f` that is the left inverse of `g` would work on this example.
--/
-def f (x : Nat) := x - 1
-def g (x : Nat) := x + 1
-
-@[grind =] theorem fg : f (g x) = x := by simp [f, g]
-example : f a = b → a = g c → b = c := by grind
-
-/-
-Any `R` that is transitive and symmetric would work on this example.
--/
-def R : Nat → Nat → Prop := (· % 7 = · % 7)
-@[grind →] theorem Rtrans : R x y → R y z → R x z := by grind [R]
-@[grind →] theorem Rsymm  : R x y → R y x := by grind [R]
-example : R a b → R c b → R d c → R a d := by grind
-
-/- Big step operational semantics example. -/
-
-abbrev Variable := String
-def State := Variable → Nat
-inductive Stmt : Type where
-  | skip : Stmt
-  | assign : Variable → (State → Nat) → Stmt
-  | seq : Stmt → Stmt → Stmt
-  | ifThenElse : (State → Prop) → Stmt → Stmt → Stmt
-  | whileDo : (State → Prop) → Stmt → Stmt
-infix:60 ";; " => Stmt.seq
-export Stmt (skip assign seq ifThenElse whileDo)
-set_option quotPrecheck false in
-notation s:70 "[" x:70 "↦" n:70 "]" => (fun v ↦ if v = x then n else s v)
-inductive BigStep : Stmt → State → State → Prop where
-  | skip (s : State) : BigStep skip s s
-  | assign (x : Variable) (a : State → Nat) (s : State) : BigStep (assign x a) s (s[x ↦ a s])
-  | seq {S T : Stmt} {s t u : State} (hS : BigStep S s t) (hT : BigStep T t u) :
-    BigStep (S;; T) s u
-  | if_true {B : State → Prop} {s t : State} (hcond : B s) (S T : Stmt) (hbody : BigStep S s t) :
-    BigStep (ifThenElse B S T) s t
-  | if_false {B : State → Prop} {s t : State} (hcond : ¬ B s) (S T : Stmt) (hbody : BigStep T s t) :
-    BigStep (ifThenElse B S T) s t
-  | while_true {B S s t u} (hcond : B s) (hbody : BigStep S s t) (hrest : BigStep (whileDo B S) t u) :
-    BigStep (whileDo B S) s u
-  | while_false {B S s} (hcond : ¬ B s) : BigStep (whileDo B S) s s
-notation:55 "(" S:55 "," s:55 ")" " ==> " t:55 => BigStep S s t
-
-example {B S T s t} (hcond : B s) : (ifThenElse B S T, s) ==> t → (S, s) ==> t := by
-  grind [cases BigStep]
-
-theorem cases_if_of_true {B S T s t} (hcond : B s) : (ifThenElse B S T, s) ==> t → (S, s) ==> t := by
-  grind [cases BigStep]
-
-theorem cases_if_of_false {B S T s t} (hcond : ¬ B s) : (ifThenElse B S T, s) ==> t → (T, s) ==> t := by
-  grind [cases BigStep]
-
-example {B S T s t} : (ifThenElse B S T, s) ==> t ↔ (B s ∧ (S, s) ==> t) ∨ (¬ B s ∧ (T, s) ==> t) := by
-  grind [BigStep] -- shortcut for `cases BigStep` and `intro BigStep`
-
-attribute [grind] BigStep
-theorem if_iff {B S T s t} : (ifThenElse B S T, s) ==>
-    t ↔ (B s ∧ (S, s) ==> t) ∨ (¬ B s ∧ (T, s) ==> t) := by grind
-
-/- Dependent pattern matching. -/
-
-inductive Vec (α : Type u) : Nat → Type u
-  | nil : Vec α 0
-  | cons : α → Vec α n → Vec α (n+1)
-@[grind =] def Vec.head : Vec α (n+1) → α
-  | .cons a _ => a
-example (as bs : Vec Int (n+1)) : as.head = bs.head
-    → (match as, bs with
-       | .cons a _, .cons b _ => a + b) = 2 * as.head := by grind
-
-/- Theory solvers. -/
-
-example [CommRing α] (a b c : α) :
-    a + b + c = 3 →
-    a^2 + b^2 + c^2 = 5 →
-    a^3 + b^3 + c^3 = 7 →
-    a^4 + b^4 + c^4 = 9 := by grind
-
-example (x : BitVec 8) : (x - 16) * (x + 16) = x^2 := by grind
-
-example [CommSemiring α] [AddRightCancel α] (x y : α) :
-    x^2*y = 1 → x*y^2 = y → y*x = 1 := by grind
-
-example (a b : UInt32) : a ≤ 2 → b ≤ 3 → a + b ≤ 5 := by grind
-
-example [LE α] [Std.IsLinearPreorder α] (a b c d : α) :
-    a ≤ b → ¬ (c ≤ b) → ¬ (d ≤ c) → a ≤ d := by grind
-
-/- Theory combination. -/
-
-example [CommRing α] [NoNatZeroDivisors α]
-    (a b c : α) (f : α → Nat) :
-    a + b + c = 3 → a^2 + b^2 + c^2 = 5 → a^3 + b^3 + c^3 = 7 →
-    f (a^4 + b^4) + f (9 - c^4) ≠ 1 := by grind
-
-/- Interactive mode. -/
-
--- Remark: Mathlib contains the definition of `Real`, `sin`, and `cos`.
-axiom Real : Type
-instance : Lean.Grind.CommRing Real := sorry
-
-axiom cos : Real → Real
-axiom sin : Real → Real
-axiom trig_identity : ∀ x, (cos x)^2 + (sin x)^2 = 1
-
--- Manually specify the patterns for `trig_identity`
-grind_pattern trig_identity => cos x
-grind_pattern trig_identity => sin x
-
-example : (cos x + sin x)^2 = 2 * cos x * sin x + 1 := by
-  grind? -- Provides code action
-
-example : (cos x + sin x)^2 = 2 * cos x * sin x + 1 := by
-  grind =>
-    instantiate only [trig_identity]
-    ring

doc/examples/bintree.lean.out.expected

@@ -1,2 +0,0 @@
-Tree.node (Tree.node (Tree.leaf) 1 "one" (Tree.leaf)) 2 "two" (Tree.node (Tree.leaf) 3 "three" (Tree.leaf))
-[(1, "one"), (2, "two"), (3, "three")]

doc/examples/compiler/run_test.sh

@@ -1,4 +0,0 @@
-leanmake --always-make bin
-
-capture ./build/bin/test hello world
-check_out_contains "[hello, world]"

doc/examples/compiler/test.lean.out.expected

@@ -1 +0,0 @@
-[hello, world]

doc/examples/interp.lean.out.expected

@@ -1,3 +0,0 @@
-30
-interp.lean:146:4: warning: declaration uses `sorry`
-3628800

doc/examples/palindromes.lean.out.expected

@@ -1,2 +0,0 @@
-true
-false

doc/examples/phoas.lean.out.expected

@@ -1,2 +0,0 @@
-"(((fun x_1 => (fun x_2 => (x_1 + x_2))) 1) 2)"
-"((((fun x_1 => (fun x_2 => (x_1 + x_2))) 1) 2) + 5)"

doc/examples/run_test.sh

@@ -1,4 +0,0 @@
-capture_only "$1" \
-  lean -Dlinter.all=false "$1"
-check_out_file
-check_exit_is_success

doc/examples/test_single.sh

@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+source ../../tests/common.sh
+
+exec_check_raw lean -Dlinter.all=false "$f"

doc/std/grove/lean-toolchain

@@ -1 +1 @@
-../../../build/release/stage1
+lean4

doc/style.md

@@ -810,7 +810,7 @@ Docstrings for constants should have the following structure:
 
 The **short summary** should be 1–3 sentences (ideally 1) and provide
 enough information for most readers to quickly decide whether the
-constant is relevant to their task. The first (or only) sentence of
+docstring is relevant to their task. The first (or only) sentence of
 the short summary should be a *sentence fragment* in which the subject
 is implied to be the documented item, written in present tense
 indicative, or a *noun phrase* that characterizes the documented
@@ -1123,110 +1123,6 @@ infix:50 " ⇔ " => Bijection
 recommended_spelling "bij" for "⇔" in [Bijection, «term_⇔_»]
 ```
 
-#### Tactics
-
-Docstrings for tactics should have the following structure:
-
-* Short summary
-* Details
-* Variants
-* Examples
-
-Sometimes more than one declaration is needed to implement what the user
-sees as a single tactic. In that case, only one declaration should have
-the associated docstring, and the others should have the `tactic_alt`
-attribute to mark them as an implementation detail.
-
-The **short summary** should be 1–3 sentences (ideally 1) and provide
-enough information for most readers to quickly decide whether the
-tactic is relevant to their task. The first (or only) sentence of
-the short summary should be a full sentence in which the subject
-is an example invocation of the tactic, written in present tense
-indicative. If the example tactic invocation names parameters, then the
-short summary may refer to them. For the example invocation, prefer the
-simplest or most typical example. Explain more complicated forms in the
-variants section. If needed, abbreviate the invocation by naming part of
-the syntax and expanding it in the next sentence. The summary should be
-written as a single paragraph.
-
-**Details**, if needed, may be 1-3 paragraphs that describe further
-relevant information. They may insert links as needed. This section
-should fully explain the scope of the tactic: its syntax format,
-on which goals it works and what the resulting goal(s) look like. It
-should be clear whether the tactic fails if it does not close the main
-goal and whether it creates any side goals. The details may include
-explanatory examples that can’t necessarily be machine checked and
-don’t fit the format.
-
-If the tactic is extensible using `macro_rules`, mention this in the
-details, with a link to `lean-manual://section/tactic-macro-extension`
-and give a one-line example. If the tactic provides an attribute or a
-command that allows the user to extend its behavior, the documentation
-on how to extend the tactic belongs to that attribute or command. In the
-tactic docstring, use a single sentence to refer the reader to this
-further documentation.
-
-**Variants**, if needed, should be a bulleted list describing different
-options and forms of the same tactic. The reader should be able to parse
-and understand the parts of a tactic invocation they are hovering over,
-using this list. Each list item should describe an individual variant
-and take one of two formats: the **short summary** as above, or a
-**named list item**. A named list item consists of a title in bold
-followed by an indented short paragraph.
-
-Variants should be explained from the perspective of the tactic's users, not
-their implementers. A tactic that is implemented as a single Lean parser may
-have multiple variants from the perspective of users, while a tactic that is
-implemented as multiple parsers may have no variants, but merely an optional
-part of the syntax.
-
-**Examples** should start with the line `Examples:` (or `Example:` if
-there’s exactly one). The section should consist of a sequence of code
-blocks, each showing a Lean declaration (usually with the `example`
-keyword) that invokes the tactic. When the effect of the tactic is not
-clear from the code, you can use code comments to describe this. Do
-not include text between examples, because it can be unclear whether
-the text refers to the code before or after the example.
-
-##### Example
-
-````
-`rw [e]` uses the expression `e` as a rewrite rule on the main goal,
-then tries to close the goal by "cheap" (reducible) `rfl`.
-
-If `e` is a defined constant, then the equational theorems associated with `e`
-are used. This provides a convenient way to unfold `e`. If `e` has parameters,
-the tactic will try to fill these in by unification with the matching part of
-the target. Parameters are only filled in once per rule, restricting which
-later rewrites can be found. Parameters that are not filled in after
-unification will create side goals. If the `rfl` fails to close the main goal,
-no error is raised.
-
-`rw` may fail to rewrite terms "under binders", such as `∀ x, ...` or `∃ x,
-...`. `rw` can also fail with a "motive is type incorrect" error in the context
-of dependent types. In these cases, consider using `simp only`.
-
-* `rw [e₁, ... eₙ]` applies the given rules sequentially.
-* `rw [← e]` or `rw [<- e]` applies the rewrite in the reverse direction.
-* `rw [e] at l` rewrites with `e` at location(s) `l`.
-* `rw (occs := .pos L) [e]`, where `L` is a literal list of natural numbers,
-  only rewrites the given occurrences in the target. Occurrences count from 1.
-* `rw (occs := .neg L) [e]`, where `L` is a literal list of natural numbers,
-  skips rewriting the given occurrences in the target. Occurrences count from 1.
-
-Examples:
-
-```lean
-example {a b : Nat} (h : a + a = b) : (a + a) + (a + a) = b + b := by rw [h]
-```
-
-```lean
-example {f : Nat -> Nat} (h : ∀ x, f x = 1) (a b : Nat) : f a = f b := by
-  rw [h] -- `rw` instantiates `h` only once, so this is equivalent to: `rw [h a]`
-  -- goal: ⊢ 1 = f b
-  rw [h] -- equivalent to: `rw [h b]`
-```
-````
 
 
 ## Dictionary

flake.lock

@@ -2,11 +2,11 @@
   "nodes": {
     "nixpkgs": {
       "locked": {
-        "lastModified": 1769018530,
-        "narHash": "sha256-S/5RU76BdQ32bbE99a+G9gMuatpVWEvIfeSjEqyoFS4=",
-        "rev": "88d3861acdd3d2f0e361767018218e51810df8a1",
+        "lastModified": 1745636243,
+        "narHash": "sha256-kbNvlQZf8wwok3d2X1kM/TlXH/MZ+03ZNv+IPPBx+DM=",
+        "rev": "f771eb401a46846c1aebd20552521b233dd7e18b",
         "type": "tarball",
-        "url": "https://releases.nixos.org/nixos/unstable/nixos-26.05pre931542.88d3861acdd3/nixexprs.tar.xz"
+        "url": "https://releases.nixos.org/nixos/unstable/nixos-25.05pre789333.f771eb401a46/nixexprs.tar.xz"
       },
       "original": {
         "type": "tarball",

flake.nix

@@ -18,7 +18,7 @@
       # An old nixpkgs for creating releases with an old glibc
       pkgsDist-old-aarch = import inputs.nixpkgs-old { localSystem.config = "aarch64-unknown-linux-gnu"; };
 
-      llvmPackages = pkgs.llvmPackages_19;
+      llvmPackages = pkgs.llvmPackages_15;
 
       devShellWithDist = pkgsDist: pkgs.mkShell.override {
           stdenv = pkgs.overrideCC pkgs.stdenv llvmPackages.clang;
@@ -67,5 +67,5 @@
         oldGlibc = devShellWithDist pkgsDist-old;
         oldGlibcAArch = devShellWithDist pkgsDist-old-aarch;
       };
-    }) ["x86_64-linux" "aarch64-linux" "aarch64-darwin"]);
+    }) ["x86_64-linux" "aarch64-linux"]);
 }

lean-toolchain

@@ -1 +1 @@
-build/release/stage1
+lean4

lean.code-workspace

@@ -0,0 +1,72 @@
+{
+	"folders": [
+		{
+			"path": "."
+		},
+		{
+			"path": "src"
+		},
+		{
+			"path": "tests"
+		},
+		{
+			"path": "script"
+		}
+	],
+	"settings": {
+		// Open terminal at root, not current workspace folder
+		// (there is not way to directly refer to the root folder included as `.` above)
+		"terminal.integrated.cwd": "${workspaceFolder:src}/..",
+		"files.insertFinalNewline": true,
+		"files.trimTrailingWhitespace": true,
+		"cmake.buildDirectory": "${workspaceFolder}/build/release",
+		"cmake.generator": "Unix Makefiles",
+		"[markdown]": {
+			"rewrap.wrappingColumn": 70
+		},
+		"[lean4]": {
+			"editor.rulers": [
+				100
+			]
+		}
+	},
+	"tasks": {
+		"version": "2.0.0",
+		"tasks": [
+			{
+				"label": "build",
+				"type": "shell",
+				"command": "make -C build/release -j$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4)",
+				"problemMatcher": [],
+				"group": {
+					"kind": "build",
+					"isDefault": true
+				}
+			},
+			{
+				"label": "build-old",
+				"type": "shell",
+				"command": "make -C build/release -j$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4) LAKE_EXTRA_ARGS=--old",
+				"problemMatcher": [],
+				"group": {
+					"kind": "build"
+				}
+			},
+			{
+				"label": "test",
+				"type": "shell",
+				"command": "NPROC=$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4); CTEST_OUTPUT_ON_FAILURE=1 make -C build/release test -j$NPROC ARGS=\"-j$NPROC\"",
+				"problemMatcher": [],
+				"group": {
+					"kind": "test",
+					"isDefault": true
+				}
+			}
+		]
+	},
+	"extensions": {
+		"recommendations": [
+			"leanprover.lean4"
+		]
+	}
+}

releases_drafts/environment.md

@@ -0,0 +1,6 @@
+**Breaking Changes**
+
+* The functions `Lean.Environment.importModules` and `Lean.Environment.finalizeImport` have been extended with a new parameter `loadExts : Bool := false` that enables environment extension state loading.
+  Their previous behavior corresponds to setting the flag to `true` but is only safe to do in combination with `enableInitializersExecution`; see also the `importModules` docstring.
+  The new default value `false` ensures the functions can be used correctly multiple times within the same process when environment extension access is not needed.
+  The wrapper function `Lean.Environment.withImportModules` now always calls `importModules` with `loadExts := false` as it is incompatible with extension loading.

releases_drafts/module-system.md

@@ -0,0 +1,54 @@
+This release introduces the Lean module system, which allows files to
+control the visibility of their contents for other files. In previous
+releases, this feature was available as a preview when the option
+`experimental.module` was set to `true`; it is now a fully supported
+feature of Lean.
+
+# Benefits
+
+Because modules reduce the amount of information exposed to other
+code, they speed up rebuilds because irrelevant changes can be
+ignored, they make it possible to be deliberate about API evolution by
+hiding details that may change from clients, they help proofs be
+checked faster by avoiding accidentally unfolding definitions, and
+they lead to smaller executable files through improved dead code
+elimination.
+
+# Visibility
+
+A source file is a module if it begins with the `module` keyword.  By
+default, declarations in a module are private; the `public` modifier
+exports them. Proofs of theorems and bodies of definitions are private
+by default even when their signatures are public; the bodies of
+definitions can be made public by adding the `@[expose]`
+attribute. Theorems and opaque constants never expose their bodies.
+
+`public section` and `@[expose] section` change the default visibility
+of declarations in the section.
+
+# Imports
+
+Modules may only import other modules. By default, `import` adds the
+public information of the imported module to the private scope of the
+current module. Adding the `public` modifier to an import places the
+imported modules's public information in the public scope of the
+current module, exposing it in turn to the current module's clients.
+
+Within a package, `import all` can be used to import another module's
+private scope into the current module; this can be used to separate
+lemmas or tests from definition modules without exposing details to
+downstream clients.
+
+# Meta Code
+
+Code used in metaprograms must be marked `meta`. This ensures that the
+code is compiled and available for execution when it is needed during
+elaboration. Meta code may only reference other meta code. A whole
+module can be made available in the meta phase using `meta import`;
+this allows code to be shared across phases by importing the module in
+each phase. Code that is reachable from public metaprograms must be
+imported via `public meta import`, while local metaprograms can use
+plain `meta import` for their dependencies.
+
+
+The module system is described in detail in [the Lean language reference](https://lean-reference-manual-review.netlify.app/find/?domain=Verso.Genre.Manual.section&name=files).

script/Modulize.lean

@@ -29,7 +29,7 @@ def main (args : List String) : IO Unit := do
     if !msgs.toList.isEmpty then -- skip this file if there are parse errors
       msgs.forM fun msg => msg.toString >>= IO.println
       throw <| .userError "parse errors in file"
-    let `(header| $[module%$moduleTk?]? $[prelude%$preludeTk?]? $imps:import*) := header
+    let `(header| $[module%$moduleTk?]? $imps:import*) := header
       | throw <| .userError s!"unexpected header syntax of {path}"
     if moduleTk?.isSome then
       continue
@@ -38,11 +38,11 @@ def main (args : List String) : IO Unit := do
     let startPos := header.raw.getPos? |>.getD parserState.pos
 
     let dummyEnv ← mkEmptyEnvironment
-    let (initCmd, parserState', msgs') :=
+    let (initCmd, parserState', _) :=
       Parser.parseCommand inputCtx { env := dummyEnv, options := {} } parserState msgs
 
-    -- insert section if any trailing command (or error, which could be from an unknown command)
-    if !initCmd.isOfKind ``Parser.Command.eoi || msgs'.hasErrors then
+    -- insert section if any trailing command
+    if !initCmd.isOfKind ``Parser.Command.eoi then
       let insertPos? :=
           -- put below initial module docstring if any
           guard (initCmd.isOfKind ``Parser.Command.moduleDoc) *> initCmd.getTailPos? <|>
@@ -57,21 +57,19 @@ def main (args : List String) : IO Unit := do
         sec := "\n\n" ++ sec
       if insertPos?.isNone then
         sec := sec ++ "\n\n"
-      let insertPos := text.pos! insertPos
-      text := text.extract text.startPos insertPos ++ sec ++ text.extract insertPos text.endPos
+      text := text.extract 0 insertPos ++ sec ++ text.extract insertPos text.rawEndPos
 
     -- prepend each import with `public `
     for imp in imps.reverse do
       let insertPos := imp.raw.getPos?.get!
       let prfx := if doMeta then "public meta " else "public "
-      let insertPos := text.pos! insertPos
-      text := text.extract text.startPos insertPos ++ prfx ++ text.extract insertPos text.endPos
+      text := text.extract 0 insertPos ++ prfx ++ text.extract insertPos text.rawEndPos
 
     -- insert `module` header
-    let mut initText := text.extract text.startPos (text.pos! startPos)
-    if !initText.trimAscii.isEmpty then
+    let mut initText := text.extract 0 startPos
+    if !initText.trim.isEmpty then
       -- If there is a header comment, preserve it and put `module` in the line after
-      initText := initText.trimAsciiEnd.toString ++ "\n"
-    text := initText ++ "module\n\n" ++ text.extract (text.pos! startPos) text.endPos
+      initText := initText.trimRight ++ "\n"
+    text := initText ++ "module\n\n" ++ text.extract startPos text.rawEndPos
 
     IO.FS.writeFile path text

script/PROFILER_README.md

@@ -1,178 +0,0 @@
-# Lean Profiler
-
-Profile Lean programs with demangled names using
-[samply](https://github.com/mstange/samply) and
-[Firefox Profiler](https://profiler.firefox.com).
-
-Python 3, no external dependencies.
-
-## Quick start
-
-```bash
-# One command: record, symbolicate, demangle, and open in Firefox Profiler
-script/lean_profile.sh ./my_lean_binary [args...]
-
-# See all options
-script/lean_profile.sh --help
-```
-
-Requirements: `samply` (`cargo install samply`), `python3`.
-
-## Reading demangled names
-
-The demangler transforms low-level C symbol names into readable Lean names
-and annotates them with compact modifiers.
-
-### Basic names
-
-| Raw symbol | Demangled |
-|---|---|
-| `l_Lean_Meta_Sym_main` | `Lean.Meta.Sym.main` |
-| `lp_std_List_map` | `List.map (std)` |
-| `_init_l_Foo_bar` | `[init] Foo.bar` |
-| `initialize_Init_Data` | `[module_init] Init.Data` |
-| `_lean_main` | `[lean] main` |
-
-### Modifier flags `[...]`
-
-Compiler-generated suffixes are folded into a bracket annotation after the
-name. These indicate *how* the function was derived from the original source
-definition.
-
-| Flag | Meaning | Compiler suffix |
-|---|---|---|
-| `arity`↓ | Reduced-arity specialization | `_redArg` |
-| `boxed` | Boxed calling-convention wrapper | `_boxed` |
-| `impl` | Implementation detail | `_impl` |
-| λ | Lambda-lifted closure | `_lam_N`, `_lambda_N`, `_elam_N` |
-| `jp` | Join point | `_jp_N` |
-| `closed` | Extracted closed subterm | `_closed_N` |
-| `private` | Private (module-scoped) definition | `_private.Module.0.` prefix |
-
-Examples:
-
-```
-Lean.Meta.Simp.simpLambda [boxed, λ]     -- boxed wrapper of a lambda-lifted closure
-Lean.Meta.foo [arity↓, private]           -- reduced-arity version of a private def
-```
-
-Multiple flags are comma-separated. Order reflects how they were collected
-(innermost suffix first).
-
-### Specializations `spec at ...`
-
-When the compiler specializes a function at a particular call site, the
-demangled name shows `spec at <context>` after the base name and its flags.
-The context names the function whose body triggered the specialization, and
-may carry its own modifier flags:
-
-```
-<base-name> [<base-flags>] spec at <context>[<context-flags>]
-```
-
-Examples:
-
-```
--- foo specialized at call site in bar
-Lean.Meta.foo spec at Lean.Meta.bar
-
--- foo (with a lambda closure) specialized at bar (with reduced arity and a lambda)
-Lean.Meta.foo [λ] spec at Lean.Meta.bar[λ, arity↓]
-
--- chained specialization: foo specialized at bar, then at baz
-Lean.Meta.foo spec at Lean.Meta.bar spec at Lean.Meta.baz[arity↓]
-```
-
-Context flags use the same symbols as base flags. When a context has no
-flags, the brackets are omitted.
-
-### Other annotations
-
-| Pattern | Meaning |
-|---|---|
-| `<apply/N>` | Lean runtime apply function (N arguments) |
-| `.cold.N` suffix | LLVM cold-path clone (infrequently executed) |
-| `(pkg)` suffix | Function from package `pkg` |
-
-## Tools
-
-### `script/lean_profile.sh` -- Full profiling pipeline
-
-Records a profile, symbolicates it via samply's API, demangles Lean names,
-and opens the result in Firefox Profiler. This is the recommended workflow.
-
-```bash
-script/lean_profile.sh ./build/release/stage1/bin/lean src/Lean/Elab/Term.lean
-```
-
-Environment variables:
-
-| Variable | Default | Description |
-|---|---|---|
-| `SAMPLY_RATE` | 1000 | Sampling rate in Hz |
-| `SAMPLY_PORT` | 3756 | Port for samply symbolication server |
-| `SERVE_PORT` | 3757 | Port for serving the demangled profile |
-| `PROFILE_KEEP` | 0 | Set to 1 to keep the temp directory |
-
-### `script/profiler/lean_demangle.py` -- Name demangler
-
-Demangles individual symbol names. Works as a stdin filter (like `c++filt`)
-or with arguments.
-
-```bash
-echo "l_Lean_Meta_Sym_main" | python3 script/profiler/lean_demangle.py
-# Lean.Meta.Sym.main
-
-python3 script/profiler/lean_demangle.py --raw l_foo___redArg
-# foo._redArg  (exact name, no postprocessing)
-```
-
-As a Python module:
-
-```python
-from lean_demangle import demangle_lean_name, demangle_lean_name_raw
-
-demangle_lean_name("l_foo___redArg")       # "foo [arity↓]"
-demangle_lean_name_raw("l_foo___redArg")   # "foo._redArg"
-```
-
-### `script/profiler/symbolicate_profile.py` -- Profile symbolicator
-
-Calls samply's symbolication API to resolve raw addresses into symbol names,
-then demangles them. Used internally by `lean_profile.sh`.
-
-### `script/profiler/serve_profile.py` -- Profile server
-
-Serves a profile JSON file to Firefox Profiler without re-symbolication
-(which would overwrite demangled names). Used internally by `lean_profile.sh`.
-
-### `script/profiler/lean_demangle_profile.py` -- Standalone profile rewriter
-
-Demangles names in an already-symbolicated profile file (if you have one
-from another source).
-
-```bash
-python3 script/profiler/lean_demangle_profile.py profile.json.gz -o demangled.json.gz
-```
-
-## Tests
-
-```bash
-cd script/profiler && python3 -m unittest test_demangle -v
-```
-
-## How it works
-
-The demangler is a faithful port of Lean 4's `Name.demangleAux` from
-`src/Lean/Compiler/NameMangling.lean`. It reverses the encoding used by
-`Name.mangle` / `Name.mangleAux` which turns hierarchical Lean names into
-valid C identifiers:
-
-- `_` separates name components (`Lean.Meta` -> `Lean_Meta`)
-- `__` encodes a literal underscore in a component name
-- `_xHH`, `_uHHHH`, `_UHHHHHHHH` encode special characters
-- `_N_` encodes numeric name components
-- `_00` is a disambiguation prefix for ambiguous patterns
-
-After demangling, a postprocessing pass folds compiler-generated suffixes
-into human-readable annotations (see [Reading demangled names](#reading-demangled-names)).

script/Shake.lean

@@ -5,12 +5,12 @@ Authors: Mario Carneiro, Sebastian Ullrich
 -/
 module
 
-prelude
-public import Lean.Util.Path
+import Lean.Environment
 import Lean.ExtraModUses
+
+import Lake.CLI.Main
 import Lean.Parser.Module
-import Init.Data.Range.Polymorphic.Iterators
-meta import Lean.Parser.Module
+import Lake.Load.Workspace
 
 /-! # Shake: A Lean import minimizer
 
@@ -20,12 +20,84 @@ ensuring that every import is used to contribute some constant or other elaborat
 recorded by `recordExtraModUse` and friends.
 -/
 
+/-- help string for the command line interface -/
+def help : String := "Lean project tree shaking tool
+Usage: lake exe shake [OPTIONS] <MODULE>..
+
+Arguments:
+  <MODULE>
+    A module path like `Mathlib`. All files transitively reachable from the
+    provided module(s) will be checked.
+
+Options:
+  --force
+    Skips the `lake build --no-build` sanity check
+
+  --keep-implied
+    Preserves existing imports that are implied by other imports and thus not technically needed
+    anymore
+
+  --keep-prefix
+    If an import `X` would be replaced in favor of a more specific import `X.Y...` it implies,
+    preserves the original import instead. More generally, prefers inserting `import X` even if it
+    was not part of the original imports as long as it was in the original transitive import closure
+    of the current module.
+
+  --keep-public
+    Preserves all `public` imports to avoid breaking changes for external downstream modules
+
+  --add-public
+    Adds new imports as `public` if they have been in the original public closure of that module.
+    In other words, public imports will not be removed from a module unless they are unused even
+    in the private scope, and those that are removed will be re-added as `public` in downstream
+    modules even if only needed in the private scope there. Unlike `--keep-public`, this may
+    introduce breaking changes but will still limit the number of inserted imports.
+
+  --explain
+    Gives constants explaining why each module is needed
+
+  --fix
+    Apply the suggested fixes directly. Make sure you have a clean checkout
+    before running this, so you can review the changes.
+
+  --gh-style
+    Outputs messages that can be parsed by `gh-problem-matcher-wrap`
+
+Annotations:
+  The following annotations can be added to Lean files in order to configure the behavior of
+  `shake`. Only the substring `shake: ` directly followed by a directive is checked for, so multiple
+  directives can be mixed in one line such as `-- shake: keep-downstream, shake: keep-all`, and they
+  can be surrounded by arbitrary comments such as `-- shake: keep (metaprogram output dependency)`.
+
+  * `module -- shake: keep-downstream`:
+    Preserves this module in all (current) downstream modules, adding new imports of it if needed.
+
+  * `module -- shake: keep-all`:
+    Preserves all existing imports in this module as is. New imports now needed because of upstream
+    changes may still be added.
+
+  * `import X -- shake: keep`:
+    Preserves this specific import in the current module. The most common use case is to preserve a
+    public import that will be needed in downstream modules to make sense of the output of a
+    metaprogram defined in this module. For example, if a tactic is defined that may synthesize a
+    reference to a theorem when run, there is no way for `shake` to detect this by itself and the
+    module of that theorem should be publicly imported and annotated with `keep` in the tactic's
+    module.
+    ```
+    public import X  -- shake: keep (metaprogram output dependency)
+
+    ...
+
+    elab \"my_tactic\" : tactic => do
+      ... mkConst ``f -- `f`, defined in `X`, may appear in the output of this tactic
+    ```
+"
+
 open Lean
 
-namespace Lake.Shake
-
-/-- The parsed CLI arguments for shake. -/
-public structure Args where
+/-- The parsed CLI arguments. See `help` for more information -/
+structure Args where
+  help : Bool := false
   keepImplied : Bool := false
   keepPrefix : Bool := false
   keepPublic : Bool := false
@@ -37,8 +109,6 @@ public structure Args where
   fix : Bool := false
   /-- `<MODULE>..`: the list of root modules to check -/
   mods : Array Name := #[]
-  /-- The list of modules to minimize exclusively, otherwise all reachable ones. -/
-  onlyMods : Array Name := #[]
 
 /-- We use `Nat` as a bitset for doing efficient set operations.
 The bit indexes will usually be a module index. -/
@@ -66,7 +136,7 @@ instance : Union Bitset where
 instance : XorOp Bitset where
   xor a b := { toNat := a.toNat ^^^ b.toNat }
 
-def has (s : Bitset) (i : Nat) : Bool := s.toNat.testBit i
+def has (s : Bitset) (i : Nat) : Bool := s ∩ {i} ≠ ∅
 
 end Bitset
 
@@ -167,19 +237,8 @@ structure State where
   /-- Edits to be applied to the module imports. -/
   edits : Edits := {}
 
-  -- Memoizations
-  reservedNames : Std.HashSet Name := Id.run do
-    let mut m := {}
-    for (c, _) in env.constants do
-      if isReservedName env c then
-        m := m.insert c
-    return m
-  indirectModUses : Std.HashMap Name (Array ModuleIdx) :=
-    indirectModUseExt.getState env
-  modNames : Array Name :=
-    env.header.moduleNames
-
 def State.mods (s : State) := s.env.header.moduleData
+def State.modNames (s : State) := s.env.header.moduleNames
 
 /--
 Given module `j`'s transitive dependencies, computes the union of `transImps` and the transitive
@@ -234,9 +293,9 @@ def isDeclMeta' (env : Environment) (declName : Name) : Bool :=
 Given an `Expr` reference, returns the declaration name that should be considered the reference, if
 any.
 -/
-def getDepConstName? (s : State) (ref : Name) : Option Name := do
+def getDepConstName? (env : Environment) (ref : Name) : Option Name := do
   -- Ignore references to reserved names, they can be re-generated in-place
-  guard <| !s.reservedNames.contains ref
+  guard <| !isReservedName env ref
   -- `_simp_...` constants are similar, use base decl instead
   return if ref.isStr && ref.getString!.startsWith "_simp_" then
     ref.getPrefix
@@ -259,7 +318,7 @@ def calcNeeds (s : State) (i : ModuleIdx) : Needs := Id.run do
       needs := visitExpr k e needs
 
   for use in getExtraModUses env i do
-    let j : Nat := env.getModuleIdx? use.module |>.get!
+    let j := env.getModuleIdx? use.module |>.get!
     needs := needs.union { use with } {j}
 
   return needs
@@ -269,24 +328,22 @@ where
     let env := s.env
     Lean.Expr.foldConsts e deps fun c deps => Id.run do
       let mut deps := deps
-      if let some c := getDepConstName? s c then
-        if let some (j : Nat) := env.getModuleIdxFor? c then
+      if let some c := getDepConstName? env c then
+        if let some j := env.getModuleIdxFor? c then
           let k := { k with isMeta := k.isMeta && !isDeclMeta' env c }
           if j != i then
             deps := deps.union k {j}
-            for (indMod : Nat) in s.indirectModUses[c]?.getD #[] do
+            for indMod in (indirectModUseExt.getState env)[c]?.getD #[] do
               if s.transDeps[i]!.has k indMod then
                 deps := deps.union k {indMod}
       return deps
 
-abbrev Explanations := Std.HashMap (ModuleIdx × NeedsKind) (Option (Name × Name))
-
 /--
 Calculates the same as `calcNeeds` but tracing each module to a use-def declaration pair or
 `none` if merely a recorded extra use.
 -/
-def getExplanations (s : State) (i : ModuleIdx) : Explanations := Id.run do
-  let env := s.env
+def getExplanations (env : Environment) (i : ModuleIdx) :
+    Std.HashMap (ModuleIdx × NeedsKind) (Option (Name × Name)) := Id.run do
   let mut deps := default
   for ci in env.header.moduleData[i]!.constants do
     -- Added guard for cases like `structure` that are still exported even if private
@@ -307,25 +364,18 @@ def getExplanations (s : State) (i : ModuleIdx) : Explanations := Id.run do
 where
   /-- Accumulate the results from expression `e` into `deps`. -/
   visitExpr (k : NeedsKind) name e deps :=
-    let env := s.env
     Lean.Expr.foldConsts e deps fun c deps => Id.run do
       let mut deps := deps
-      if let some c := getDepConstName? s c then
+      if let some c := getDepConstName? env c then
         if let some j := env.getModuleIdxFor? c then
           let k := { k with isMeta := k.isMeta && !isDeclMeta' env c }
-          deps := addExplanation j k name c deps
-        for indMod in s.indirectModUses[c]?.getD #[] do
-          if s.transDeps[i]!.has k indMod then
-            deps := addExplanation indMod k name (`_indirect ++ c) deps
+          if
+            if let some (some (name', _)) := deps[(j, k)]? then
+              decide (name.toString.length < name'.toString.length)
+            else true
+          then
+            deps := deps.insert (j, k) (name, c)
       return deps
-  addExplanation (j : ModuleIdx) (k : NeedsKind) (use def_ : Name) (deps : Explanations) : Explanations :=
-    if
-      if let some (some (name', _)) := deps[(j, k)]? then
-        decide (use.toString.length < name'.toString.length)
-      else true
-    then
-      deps.insert (j, k) (use, def_)
-    else deps
 
 partial def initStateFromEnv (env : Environment) : State := Id.run do
   let mut s := { env }
@@ -368,8 +418,7 @@ def parseHeaderFromString (text path : String) :
     throw <| .userError "parse errors in file"
   -- the insertion point for `add` is the first newline after the imports
   let insertion := header.raw.getTailPos?.getD parserState.pos
-  let insertion := inputCtx.fileMap.source.pos! insertion |>.find (· == '\n')
-  let insertion := insertion.next?.getD insertion
+  let insertion := inputCtx.fileMap.source.pos! insertion |>.find (· == '\n') |>.next!
   pure ⟨path, inputCtx, header, insertion⟩
 
 /-- Parse a source file to extract the location of the import lines, for edits and error messages.
@@ -398,24 +447,23 @@ def decodeImport : TSyntax ``Parser.Module.import → Import
 
 /-- Analyze and report issues from module `i`. Arguments:
 
-* `pkgs`: the first components of the input modules
+* `pkg`: the first component of the module name
 * `srcSearchPath`: Used to find the path for error reporting purposes
 * `i`: the module index
 * `needs`: the module's calculated needs
 * `addOnly`: if true, only add missing imports, do not remove unused ones
 -/
-def visitModule (pkgs : Array Name) (srcSearchPath : SearchPath)
+def visitModule (pkg : Name) (srcSearchPath : SearchPath)
     (i : Nat) (needs : Needs) (headerStx : TSyntax ``Parser.Module.header) (args : Args)
     (addOnly := false) : StateT State IO Unit := do
-  let modName := (← get).modNames[i]!
   if isExtraRevModUse (← get).env i then
     modify fun s => { s with preserve := s.preserve.union (if args.addPublic then .pub else .priv) {i} }
     if args.trace then
-      IO.eprintln s!"Preserving `{modName}` because of recorded extra rev use"
+      IO.eprintln s!"Preserving `{(← get).modNames[i]!}` because of recorded extra rev use"
 
-  -- only process modules in the selected packages
+  -- only process modules in the selected package
   -- TODO: should be after `keep-downstream` but core headers are not found yet?
-  if !pkgs.any (·.isPrefixOf modName) then
+  if !pkg.isPrefixOf (← get).modNames[i]! then
     return
 
   let (module?, prelude?, imports) := decodeHeader headerStx
@@ -424,19 +472,16 @@ def visitModule (pkgs : Array Name) (srcSearchPath : SearchPath)
 
   let s ← get
 
-  let addOnly := addOnly ||
-    (!args.onlyMods.isEmpty && !args.onlyMods.contains modName) ||
-    module?.any (·.raw.getTrailing?.any (·.toString.contains "shake: keep-all"))
+  let addOnly := addOnly || module?.any (·.raw.getTrailing?.any (·.toString.contains "shake: keep-all"))
   let mut deps := needs
 
   -- Add additional preserved imports
   for impStx in imports do
     let imp := decodeImport impStx
-    let j : Nat := s.env.getModuleIdx? imp.module |>.get!
+    let j := s.env.getModuleIdx? imp.module |>.get!
     let k := NeedsKind.ofImport imp
     if addOnly ||
-        -- TODO: allow per-library configuration instead of hardcoding `Init`
-        args.keepPublic && imp.isExported && !(`Init).isPrefixOf modName ||
+        args.keepPublic && imp.isExported ||
         impStx.raw.getTrailing?.any (·.toString.contains "shake: keep") then
       deps := deps.union k {j}
       if args.trace then
@@ -461,20 +506,19 @@ def visitModule (pkgs : Array Name) (srcSearchPath : SearchPath)
             deps := deps.sub k' (transDeps.sub k' {j} |>.get k')
 
   if prelude?.isNone then
-    let j : Nat := s.env.getModuleIdx? `Init |>.get!
-    deps := deps.union .pub {j}
+    deps := deps.union .pub {s.env.getModuleIdx? `Init |>.get!}
 
   -- Accumulate `transDeps` which is the non-reflexive transitive closure of the still-live imports
   let mut transDeps := Needs.empty
   let mut alwaysAdd : Array Import := #[]  -- to be added even if implied by other imports
   for imp in s.mods[i]!.imports do
-    let j : Nat := s.env.getModuleIdx? imp.module |>.get!
+    let j := s.env.getModuleIdx? imp.module |>.get!
     let k := NeedsKind.ofImport imp
     if deps.has k j || imp.importAll then
       transDeps := addTransitiveImps transDeps imp j s.transDeps[j]!
       deps := deps.union k {j}
     -- skip folder-nested `public (meta)? import`s but remove `meta`
-    else if modName.isPrefixOf imp.module then
+    else if s.modNames[i]!.isPrefixOf imp.module then
       let imp := { imp with isMeta := false }
       let k := { k with isMeta := false }
       if args.trace then
@@ -498,7 +542,7 @@ def visitModule (pkgs : Array Name) (srcSearchPath : SearchPath)
         let mut imp : Import := { k with module := s.modNames[j]! }
         let mut j := j
         if args.trace then
-          IO.eprintln s!"`{imp}` is needed{if needs.has k j then " (calculated)" else ""}"
+          IO.eprintln s!"`{imp}` is needed"
         if args.addPublic && !k.isExported &&
             -- also add as public if previously `public meta`, which could be from automatic porting
             (s.transDepsOrig[i]!.has { k with isExported := true } j || s.transDepsOrig[i]!.has { k with isExported := true, isMeta := true } j) then
@@ -513,8 +557,8 @@ def visitModule (pkgs : Array Name) (srcSearchPath : SearchPath)
               -- `j'` must be reachable from `i` (allow downgrading from `meta`)
               guard <| s.transDepsOrig[i]!.has k j' || s.transDepsOrig[i]!.has { k with isMeta := true } j'
               let j'transDeps := addTransitiveImps .empty p j' s.transDeps[j']!
-              -- `j` must be publicly reachable from `j'` (now downgrading must be done in the other direction)
-              guard <| j'transDeps.has { k with isExported := true } j || j'transDeps.has { k with isExported := true, isMeta := false } j
+              -- `j` must be reachable from `j'` (now downgrading must be done in the other direction)
+              guard <| j'transDeps.has k j || j'transDeps.has { k with isMeta := false } j
               return j')
             | _ => none
           if let some j' := tryPrefix imp.module then
@@ -568,7 +612,7 @@ def visitModule (pkgs : Array Name) (srcSearchPath : SearchPath)
   -- mark and report the removals
   modify fun s => { s with
     edits := toRemove.foldl (init := s.edits) fun edits imp =>
-      edits.remove modName imp }
+      edits.remove s.modNames[i]! imp }
 
   if !toAdd.isEmpty || !toRemove.isEmpty || args.explain then
     if let some path ← srcSearchPath.findModuleWithExt "lean" s.modNames[i]! then
@@ -587,7 +631,7 @@ def visitModule (pkgs : Array Name) (srcSearchPath : SearchPath)
         if toRemove.any fun imp => imp == decodeImport stx then
           let pos := inputCtx.fileMap.toPosition stx.raw.getPos?.get!
           println! "{path}:{pos.line}:{pos.column+1}: warning: unused import \
-            (use `lake shake --fix` to fix this, or `lake shake --update` to ignore)"
+            (use `lake exe shake --fix` to fix this, or `lake exe shake --update` to ignore)"
       if !toAdd.isEmpty then
         -- we put the insert message on the beginning of the last import line
         let pos := inputCtx.fileMap.toPosition endHeader.offset
@@ -616,7 +660,7 @@ def visitModule (pkgs : Array Name) (srcSearchPath : SearchPath)
   modify fun s => { s with transDeps := s.transDeps.set! i newTransDepsI }
 
   if args.explain then
-    let explanation := getExplanations s i
+    let explanation := getExplanations s.env i
     let sanitize n := if n.hasMacroScopes then (sanitizeName n).run' { options := {} } else n
     let run (imp : Import) := do
       let j := s.env.getModuleIdx? imp.module |>.get!
@@ -632,30 +676,76 @@ def visitModule (pkgs : Array Name) (srcSearchPath : SearchPath)
         run j
     for i in toAdd do run i
 
+/-- Convert a list of module names to a bitset of module indexes -/
+def toBitset (s : State) (ns : List Name) : Bitset :=
+  ns.foldl (init := ∅) fun c name =>
+    match s.env.getModuleIdxFor? name with
+    | some i => c ∪ {i}
+    | none => c
+
 local instance : Ord Import where
   compare :=
     let _ := @lexOrd
     compareOn fun imp => (!imp.isExported, imp.module.toString)
 
-/--
-Run the shake analysis with the given arguments.
+/-- The main entry point. See `help` for more information on arguments. -/
+public def main (args : List String) : IO UInt32 := do
+  initSearchPath (← findSysroot)
+  -- Parse the arguments
+  let rec parseArgs (args : Args) : List String → Args
+    | [] => args
+    | "--help" :: rest => parseArgs { args with help := true } rest
+    | "--keep-implied" :: rest => parseArgs { args with keepImplied := true } rest
+    | "--keep-prefix" :: rest => parseArgs { args with keepPrefix := true } rest
+    | "--keep-public" :: rest => parseArgs { args with keepPublic := true } rest
+    | "--add-public" :: rest => parseArgs { args with addPublic := true } rest
+    | "--force" :: rest => parseArgs { args with force := true } rest
+    | "--fix" :: rest => parseArgs { args with fix := true } rest
+    | "--explain" :: rest => parseArgs { args with explain := true } rest
+    | "--trace" :: rest => parseArgs { args with trace := true } rest
+    | "--gh-style" :: rest => parseArgs { args with githubStyle := true } rest
+    | "--" :: rest => { args with mods := args.mods ++ rest.map (·.toName) }
+    | other :: rest => parseArgs { args with mods := args.mods.push other.toName } rest
+  let args := parseArgs {} args
 
-Assumes Lean's search path has already been properly configured.
--/
-public def run (args : Args) (srcSearchPath : SearchPath := {}) : IO UInt32 := do
+  -- Bail if `--help` is passed
+  if args.help then
+    IO.println help
+    IO.Process.exit 0
 
+  if !args.force then
+    if (← IO.Process.output { cmd := "lake", args := #["build", "--no-build"] }).exitCode != 0 then
+      IO.println "There are out of date oleans. Run `lake build` or `lake exe cache get` first"
+      IO.Process.exit 1
+
+  -- Determine default module(s) to run shake on
+  let defaultTargetModules : Array Name ← try
+    let (elanInstall?, leanInstall?, lakeInstall?) ← Lake.findInstall?
+    let config ← Lake.MonadError.runEIO <| Lake.mkLoadConfig { elanInstall?, leanInstall?, lakeInstall? }
+    let some workspace ← Lake.loadWorkspace config |>.toBaseIO
+      | throw <| IO.userError "failed to load Lake workspace"
+    let defaultTargetModules := workspace.root.defaultTargets.flatMap fun target =>
+      if let some lib := workspace.root.findLeanLib? target then
+        lib.roots
+      else if let some exe := workspace.root.findLeanExe? target then
+        #[exe.config.root]
+      else
+        #[]
+    pure defaultTargetModules
+  catch _ =>
+    pure #[]
+
+  let srcSearchPath ← getSrcSearchPath
   -- the list of root modules
-  let mods := args.mods
-  -- Only submodules of `pkgs` will be edited or have info reported on them
-  let pkgs := mods.map (·.getRoot)
+  let mods := if args.mods.isEmpty then defaultTargetModules else args.mods
+  -- Only submodules of `pkg` will be edited or have info reported on them
+  let pkg := mods[0]!.components.head!
 
   -- Load all the modules
   let imps := mods.map ({ module := · })
   let (_, s) ← importModulesCore imps (isExported := true) |>.run
   let s := s.markAllExported
-  let mut env ← finalizeImport s (isModule := true) imps {} (leakEnv := true) (loadExts := false)
-  if env.header.moduleData.any (!·.isModule) then
-    throw <| .userError "`lake shake` only works with `module`s currently"
+  let mut env ← finalizeImport s (isModule := true) imps {} (leakEnv := false) (loadExts := false)
   -- the one env ext we want to initialize
   let is := indirectModUseExt.toEnvExtension.getState env
   let newState ← indirectModUseExt.addImportedFn is.importedEntries { env := env, opts := {} }
@@ -670,7 +760,7 @@ public def run (args : Args) (srcSearchPath : SearchPath := {}) : IO UInt32 := d
 
   -- Parse headers in parallel
   let headers ← s.mods.mapIdxM fun i _ =>
-    if !pkgs.any (·.isPrefixOf s.modNames[i]!) then
+    if !pkg.isPrefixOf s.modNames[i]! then
       pure <| Task.pure <| .ok ⟨default, default, default, default⟩
     else
       BaseIO.asTask (parseHeader srcSearchPath s.modNames[i]! |>.toBaseIO)
@@ -682,7 +772,7 @@ public def run (args : Args) (srcSearchPath : SearchPath := {}) : IO UInt32 := d
   for i in [0:s.mods.size], t in needs, header in headers do
     match header.get with
     | .ok ⟨_, _, stx, _⟩ =>
-      visitModule pkgs srcSearchPath i t.get stx args
+      visitModule pkg srcSearchPath i t.get stx args
     | .error e =>
       println! e.toString
 
@@ -710,8 +800,7 @@ public def run (args : Args) (srcSearchPath : SearchPath := {}) : IO UInt32 := d
       if remove.contains mod || seen.contains mod then
         out := out ++ text.extract pos (text.pos! stx.raw.getPos?.get!)
         -- We use the end position of the syntax, but include whitespace up to the first newline
-        pos := text.pos! stx.raw.getTailPos?.get! |>.find '\n'
-        pos := pos.next?.getD pos
+        pos := text.pos! stx.raw.getTailPos?.get! |>.find '\n' |>.next!
       seen := seen.insert mod
     out := out ++ text.extract pos insertion
     for mod in add do

script/benchReelabRss.lean

@@ -83,7 +83,7 @@ def main (args : List String) : IO Unit := do
       lastRSS? := some rss
 
     let avgRSSDelta := totalRSSDelta / (n - 2)
-    IO.println s!"measurement: avg-reelab-rss-delta {avgRSSDelta*1024} b"
+    IO.println s!"avg-reelab-rss-delta: {avgRSSDelta}"
 
     let _ ← Ipc.collectDiagnostics requestNo uri versionNo
     (← Ipc.stdin).writeLspMessage (Message.notification "exit" none)

script/benchReelabWatchdogRss.lean

@@ -82,7 +82,7 @@ def main (args : List String) : IO Unit := do
       lastRSS? := some rss
 
     let avgRSSDelta := totalRSSDelta / (n - 2)
-    IO.println s!"measurement: avg-reelab-rss-delta {avgRSSDelta*1024} b"
+    IO.println s!"avg-reelab-rss-delta: {avgRSSDelta}"
 
     let _ ← Ipc.collectDiagnostics requestNo uri versionNo
     Ipc.shutdown requestNo

script/fmt

@@ -1,13 +0,0 @@
-#!/usr/bin/env bash
-set -euo pipefail
-
-# This script expects to be run from the repo root.
-
-# Format cmake files
-find -regex '.*/CMakeLists\.txt\(\.in\)?\|.*\.cmake\(\.in\)?' \
-  ! -path './build/*' \
-  ! -path "./stage0/*" \
-  -exec \
-    uvx gersemi --in-place --line-length 120 --indent 2 \
-    --definitions src/cmake/Modules/ src/CMakeLists.txt tests/CMakeLists.txt \
-    -- {} +

script/gen_constants_cpp.py

@@ -1,4 +1,4 @@
-#!/usr/bin/env python3
+#!/usr/bin/env python
 # -*- coding: utf-8 -*-
 #
 # Copyright (c) 2015 Microsoft Corporation. All rights reserved.

script/gen_tokens_cpp.py

@@ -1,4 +1,4 @@
-#!/usr/bin/env python3
+#!/usr/bin/env python
 # -*- coding: utf-8 -*-
 #
 # Copyright (c) 2015 Microsoft Corporation. All rights reserved.

script/lakefile.toml

@@ -3,3 +3,9 @@ name = "scripts"
 [[lean_exe]]
 name = "modulize"
 root = "Modulize"
+
+[[lean_exe]]
+name = "shake"
+root = "Shake"
+# needed by `Lake.loadWorkspace`
+supportInterpreter = true

script/lean-bisect

@@ -36,7 +36,7 @@ sys.path.insert(0, str(Path(__file__).parent))
 import build_artifact
 
 # Constants
-NIGHTLY_PATTERN = re.compile(r'^nightly-(\d{4})-(\d{2})-(\d{2})(-rev(\d+))?$')
+NIGHTLY_PATTERN = re.compile(r'^nightly-(\d{4})-(\d{2})-(\d{2})$')
 VERSION_PATTERN = re.compile(r'^v4\.(\d+)\.(\d+)(-rc\d+)?$')
 # Accept short SHAs (7+ chars) - we'll resolve to full SHA later
 SHA_PATTERN = re.compile(r'^[0-9a-f]{7,40}$')
@@ -158,7 +158,7 @@ def parse_identifier(s: str) -> Tuple[str, str]:
         return ('sha', full_sha)
     error(f"Invalid identifier format: '{s}'\n"
           f"Expected one of:\n"
-          f"  - nightly-YYYY-MM-DD or nightly-YYYY-MM-DD-revK (e.g., nightly-2024-06-15, nightly-2024-06-15-rev1)\n"
+          f"  - nightly-YYYY-MM-DD (e.g., nightly-2024-06-15)\n"
           f"  - v4.X.Y or v4.X.Y-rcK (e.g., v4.8.0, v4.9.0-rc1)\n"
           f"  - commit SHA (short or full)")
 
@@ -244,13 +244,8 @@ def fetch_nightly_tags() -> List[str]:
         if len(data) < 100:
             break
 
-    # Sort by date and revision (nightly-YYYY-MM-DD-revK needs numeric comparison on rev)
-    def nightly_sort_key(tag):
-        m = NIGHTLY_PATTERN.match(tag)
-        if m:
-            return (int(m.group(1)), int(m.group(2)), int(m.group(3)), int(m.group(5) or 0))
-        return (0, 0, 0, 0)
-    tags.sort(key=nightly_sort_key)
+    # Sort by date (nightly-YYYY-MM-DD format sorts lexicographically)
+    tags.sort()
     return tags
 
 def get_commit_for_nightly(nightly: str) -> str:
@@ -1029,7 +1024,6 @@ Range Syntax:
 Identifier Formats:
 
   nightly-YYYY-MM-DD    Nightly build date (e.g., nightly-2024-06-15)
-  nightly-YYYY-MM-DD-revK  Revised nightly (e.g., nightly-2024-06-15-rev1)
                         Uses pre-built toolchains from leanprover/lean4-nightly.
                         Fast: downloads via elan (~30s each).
 
@@ -1157,9 +1151,9 @@ Examples:
     # Validate --nightly-only
     if args.nightly_only:
         if from_val is not None and from_type != 'nightly':
-            error("--nightly-only requires FROM to be a nightly identifier (nightly-YYYY-MM-DD or nightly-YYYY-MM-DD-revK)")
+            error("--nightly-only requires FROM to be a nightly identifier (nightly-YYYY-MM-DD)")
         if to_type != 'nightly':
-            error("--nightly-only requires TO to be a nightly identifier (nightly-YYYY-MM-DD or nightly-YYYY-MM-DD-revK)")
+            error("--nightly-only requires TO to be a nightly identifier (nightly-YYYY-MM-DD)")
 
     if from_val:
         info(f"From: {from_val} ({from_type})")

script/lean-toolchain

@@ -1 +1 @@
-../build/release/stage1
+lean4

script/lean_profile.sh

@@ -1,133 +0,0 @@
-#!/usr/bin/env bash
-# Profile a Lean binary with demangled names.
-#
-# Usage:
-#   script/lean_profile.sh ./my_lean_binary [args...]
-#
-# Records a profile with samply, symbolicates via samply's API,
-# demangles Lean symbol names, and opens the result in Firefox Profiler.
-#
-# Requirements: samply (cargo install samply), python3
-#
-# Options (via environment variables):
-#   SAMPLY_RATE    — sampling rate in Hz (default: 1000)
-#   SAMPLY_PORT    — port for samply symbolication server (default: 3756)
-#   SERVE_PORT     — port for serving the demangled profile (default: 3757)
-#   PROFILE_KEEP   — set to 1 to keep the raw profile after demangling
-
-set -euo pipefail
-
-SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)"
-PROFILER_DIR="$SCRIPT_DIR/profiler"
-SYMBOLICATE="$PROFILER_DIR/symbolicate_profile.py"
-SERVE_PROFILE="$PROFILER_DIR/serve_profile.py"
-
-usage() {
-    cat >&2 <<EOF
-Usage: $0 [options] <lean-binary> [args...]
-
-Profile a Lean binary and view the results in Firefox Profiler
-with demangled Lean names.
-
-Requirements:
-  samply    cargo install samply
-  python3   (included with macOS / most Linux distros)
-
-Environment variables:
-  SAMPLY_RATE    sampling rate in Hz (default: 1000)
-  SAMPLY_PORT    port for samply symbolication server (default: 3756)
-  SERVE_PORT     port for serving the demangled profile (default: 3757)
-  PROFILE_KEEP   set to 1 to keep the temp directory after profiling
-
-Reading demangled names:
-  Compiler suffixes are shown as modifier flags after the name:
-    [arity↓]   reduced-arity specialization     (_redArg)
-    [boxed]    boxed calling-convention wrapper  (_boxed)
-    [λ]        lambda-lifted closure             (_lam_N, _lambda_N, _elam_N)
-    [jp]       join point                        (_jp_N)
-    [closed]   extracted closed subterm          (_closed_N)
-    [private]  private (module-scoped) def       (_private.Module.0. prefix)
-    [impl]     implementation detail             (_impl)
-
-  Specializations appear after the flags:
-    Lean.Meta.foo [λ] spec at Lean.Meta.bar[λ, arity↓]
-      = foo (with lambda closure), specialized at bar (lambda, reduced arity)
-
-  Multiple "spec at" entries indicate chained specializations.
-  See script/PROFILER_README.md for full documentation.
-EOF
-    exit "${1:-0}"
-}
-
-if [ $# -eq 0 ]; then
-    usage 1
-fi
-
-case "${1:-}" in
-    -h|--help) usage 0 ;;
-esac
-
-if ! command -v samply &>/dev/null; then
-    echo "error: samply not found. Install with: cargo install samply" >&2
-    exit 1
-fi
-
-RATE="${SAMPLY_RATE:-1000}"
-PORT="${SAMPLY_PORT:-3756}"
-SERVE="${SERVE_PORT:-3757}"
-TMPDIR=$(mktemp -d /tmp/lean-profile-XXXXXX)
-TMPFILE="$TMPDIR/profile.json.gz"
-DEMANGLED="$TMPDIR/profile-demangled.json.gz"
-SAMPLY_LOG="$TMPDIR/samply.log"
-SAMPLY_PID=""
-
-cleanup() {
-    if [ -n "$SAMPLY_PID" ]; then
-        kill "$SAMPLY_PID" 2>/dev/null || true
-        wait "$SAMPLY_PID" 2>/dev/null || true
-    fi
-    # Safety net: kill anything still on the symbolication port
-    lsof -ti :"$PORT" 2>/dev/null | xargs kill 2>/dev/null || true
-    [ "${PROFILE_KEEP:-0}" = "1" ] || rm -rf "$TMPDIR"
-}
-trap cleanup EXIT
-
-# Step 1: Record
-echo "Recording profile (rate=${RATE} Hz)..." >&2
-samply record --save-only -o "$TMPFILE" -r "$RATE" "$@"
-
-# Step 2: Start samply server for symbolication
-echo "Starting symbolication server..." >&2
-samply load --no-open -P "$PORT" "$TMPFILE" > "$SAMPLY_LOG" 2>&1 &
-SAMPLY_PID=$!
-
-# Wait for server to be ready
-for i in $(seq 1 30); do
-    if grep -q "Local server listening" "$SAMPLY_LOG" 2>/dev/null; then
-        break
-    fi
-    sleep 0.2
-done
-
-# Extract the token from samply's output
-TOKEN=$(grep -oE '[a-z0-9]{30,}' "$SAMPLY_LOG" | head -1)
-
-if [ -z "$TOKEN" ]; then
-    echo "error: could not get samply server token" >&2
-    exit 1
-fi
-
-SERVER_URL="http://127.0.0.1:${PORT}/${TOKEN}"
-
-# Step 3: Symbolicate + demangle
-echo "Symbolicating and demangling..." >&2
-python3 "$SYMBOLICATE" --server "$SERVER_URL" "$TMPFILE" -o "$DEMANGLED"
-
-# Step 4: Kill symbolication server
-kill "$SAMPLY_PID" 2>/dev/null || true
-wait "$SAMPLY_PID" 2>/dev/null || true
-SAMPLY_PID=""
-
-# Step 5: Serve the demangled profile directly (without samply's re-symbolication)
-echo "Opening in Firefox Profiler..." >&2
-python3 "$SERVE_PROFILE" "$DEMANGLED" -P "$SERVE"

script/lib/update-stage0

@@ -1,7 +1,7 @@
 #!/usr/bin/env bash
 set -euo pipefail
 
-rm -rf stage0 || true
+rm -r stage0 || true
 # don't copy untracked files
 # `:!` is git glob flavor for exclude patterns
 for f in $(git ls-files src ':!:src/lake/*' ':!:src/Leanc.lean'); do

script/profiler/lean_demangle.py

@@ -1,82 +0,0 @@
-#!/usr/bin/env python3
-"""
-Lean name demangler — thin wrapper around the Lean CLI tool.
-
-Spawns ``lean --run lean_demangle_cli.lean`` as a persistent subprocess
-and communicates via stdin/stdout pipes. This ensures a single source
-of truth for demangling logic (the Lean implementation in
-``Lean.Compiler.NameDemangling``).
-
-Usage as a filter (like c++filt):
-    echo "l_Lean_Meta_Sym_main" | python lean_demangle.py
-
-Usage as a module:
-    from lean_demangle import demangle_lean_name
-    print(demangle_lean_name("l_Lean_Meta_Sym_main"))
-"""
-
-import atexit
-import os
-import subprocess
-import sys
-
-_process = None
-_script_dir = os.path.dirname(os.path.abspath(__file__))
-_cli_script = os.path.join(_script_dir, "lean_demangle_cli.lean")
-
-
-def _get_process():
-    """Get or create the persistent Lean demangler subprocess."""
-    global _process
-    if _process is not None and _process.poll() is None:
-        return _process
-
-    lean = os.environ.get("LEAN", "lean")
-    _process = subprocess.Popen(
-        [lean, "--run", _cli_script],
-        stdin=subprocess.PIPE,
-        stdout=subprocess.PIPE,
-        stderr=subprocess.DEVNULL,
-        text=True,
-        bufsize=1,  # line buffered
-    )
-    atexit.register(_cleanup)
-    return _process
-
-
-def _cleanup():
-    global _process
-    if _process is not None:
-        try:
-            _process.stdin.close()
-            _process.wait(timeout=5)
-        except Exception:
-            _process.kill()
-        _process = None
-
-
-def demangle_lean_name(mangled):
-    """
-    Demangle a C symbol name produced by the Lean 4 compiler.
-
-    Returns a human-friendly demangled name, or the original string
-    if it is not a Lean symbol.
-    """
-    try:
-        proc = _get_process()
-        proc.stdin.write(mangled + "\n")
-        proc.stdin.flush()
-        result = proc.stdout.readline().rstrip("\n")
-        return result if result else mangled
-    except Exception:
-        return mangled
-
-
-def main():
-    """Filter stdin, demangling Lean names."""
-    for line in sys.stdin:
-        print(demangle_lean_name(line.rstrip("\n")))
-
-
-if __name__ == "__main__":
-    main()

script/profiler/lean_demangle_cli.lean

@@ -1,32 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison
--/
-module
-
-import Lean.Compiler.NameDemangling
-
-/-!
-Lean name demangler CLI tool. Reads mangled symbol names from stdin (one per
-line) and writes demangled names to stdout. Non-Lean symbols pass through
-unchanged. Like `c++filt` but for Lean names.
-
-Usage:
-    echo "l_Lean_Meta_foo" | lean --run lean_demangle_cli.lean
-    cat symbols.txt | lean --run lean_demangle_cli.lean
--/
-
-open Lean.Name.Demangle
-
-def main : IO Unit := do
-  let stdin ← IO.getStdin
-  let stdout ← IO.getStdout
-  repeat do
-    let line ← stdin.getLine
-    if line.isEmpty then break
-    let sym := line.trimRight
-    match demangleSymbol sym with
-    | some s => stdout.putStrLn s
-    | none => stdout.putStrLn sym
-    stdout.flush

script/profiler/lean_demangle_profile.py

@@ -1,117 +0,0 @@
-#!/usr/bin/env python3
-"""
-Lean name demangler for samply / Firefox Profiler profiles.
-
-Reads a profile JSON (plain or gzipped), demangles Lean function names
-in the string table, and writes the result back.
-
-Usage:
-    python lean_demangle_profile.py profile.json -o profile-demangled.json
-    python lean_demangle_profile.py profile.json.gz -o profile-demangled.json.gz
-"""
-
-import argparse
-import gzip
-import json
-import sys
-
-from lean_demangle import demangle_lean_name
-
-
-def _demangle_string_array(string_array):
-    """Demangle Lean names in a string array in-place. Returns count."""
-    count = 0
-    for i, s in enumerate(string_array):
-        if not isinstance(s, str):
-            continue
-        demangled = demangle_lean_name(s)
-        if demangled != s:
-            string_array[i] = demangled
-            count += 1
-    return count
-
-
-def rewrite_profile(profile):
-    """
-    Demangle Lean names in a Firefox Profiler profile dict (in-place).
-
-    Handles two profile formats:
-    - Newer: shared.stringArray (single shared string table)
-    - Older/samply: per-thread stringArray (each thread has its own)
-    """
-    count = 0
-
-    # Shared string table (newer Firefox Profiler format)
-    shared = profile.get("shared")
-    if shared is not None:
-        sa = shared.get("stringArray")
-        if sa is not None:
-            count += _demangle_string_array(sa)
-
-    # Per-thread string tables (samply format)
-    for thread in profile.get("threads", []):
-        sa = thread.get("stringArray")
-        if sa is not None:
-            count += _demangle_string_array(sa)
-
-    return count
-
-
-def process_profile_file(input_path, output_path):
-    """Read a profile, demangle names, write it back."""
-    is_gzip = input_path.endswith('.gz')
-
-    if is_gzip:
-        with gzip.open(input_path, 'rt', encoding='utf-8') as f:
-            profile = json.load(f)
-    else:
-        with open(input_path, 'r', encoding='utf-8') as f:
-            profile = json.load(f)
-
-    count = rewrite_profile(profile)
-
-    out_gzip = output_path.endswith('.gz') if output_path else is_gzip
-
-    if output_path:
-        if out_gzip:
-            with gzip.open(output_path, 'wt', encoding='utf-8') as f:
-                json.dump(profile, f, ensure_ascii=False)
-        else:
-            with open(output_path, 'w', encoding='utf-8') as f:
-                json.dump(profile, f, ensure_ascii=False)
-    else:
-        json.dump(profile, sys.stdout, ensure_ascii=False)
-        sys.stdout.write('\n')
-
-    return count
-
-
-def main():
-    parser = argparse.ArgumentParser(
-        description="Demangle Lean names in samply/Firefox Profiler profiles")
-    parser.add_argument('input', help='Input profile (JSON or .json.gz)')
-    parser.add_argument('-o', '--output',
-                        help='Output path (default: stdout for JSON, '
-                             'or input with -demangled suffix)')
-    args = parser.parse_args()
-
-    output = args.output
-    if output is None and not sys.stdout.isatty():
-        output = None  # write to stdout
-    elif output is None:
-        # Generate output filename
-        inp = args.input
-        if inp.endswith('.json.gz'):
-            output = inp[:-8] + '-demangled.json.gz'
-        elif inp.endswith('.json'):
-            output = inp[:-5] + '-demangled.json'
-        else:
-            output = inp + '-demangled'
-
-    count = process_profile_file(args.input, output)
-    if output:
-        print(f"Demangled {count} names, wrote {output}", file=sys.stderr)
-
-
-if __name__ == '__main__':
-    main()

script/profiler/serve_profile.py

@@ -1,94 +0,0 @@
-#!/usr/bin/env python3
-"""
-Serve a Firefox Profiler JSON file and open it in the browser.
-
-Unlike `samply load`, this does NOT provide a symbolication API,
-so Firefox Profiler will use the names already in the profile as-is.
-"""
-
-import argparse
-import gzip
-import http.server
-import io
-import sys
-import threading
-import webbrowser
-import urllib.parse
-
-
-class ProfileHandler(http.server.BaseHTTPRequestHandler):
-    """Serve the profile JSON and handle CORS for Firefox Profiler."""
-
-    profile_data = None  # set by main()
-
-    def do_GET(self):
-        if self.path == "/profile.json":
-            self.send_response(200)
-            self.send_header("Content-Type", "application/json")
-            self.send_header("Content-Encoding", "gzip")
-            self.send_header("Access-Control-Allow-Origin", "*")
-            self.end_headers()
-            self.wfile.write(self.profile_data)
-        else:
-            self.send_response(404)
-            self.end_headers()
-
-    def do_OPTIONS(self):
-        # CORS preflight
-        self.send_response(200)
-        self.send_header("Access-Control-Allow-Origin", "*")
-        self.send_header("Access-Control-Allow-Methods", "GET")
-        self.send_header("Access-Control-Allow-Headers", "Content-Type")
-        self.end_headers()
-
-    def log_message(self, format, *args):
-        pass  # suppress request logs
-
-
-def main():
-    parser = argparse.ArgumentParser(
-        description="Serve a profile JSON for Firefox Profiler")
-    parser.add_argument("profile", help="Profile file (.json or .json.gz)")
-    parser.add_argument("-P", "--port", type=int, default=3457,
-                        help="Port to serve on (default: 3457)")
-    parser.add_argument("-n", "--no-open", action="store_true",
-                        help="Do not open the browser")
-    args = parser.parse_args()
-
-    # Read the profile data (keep it gzipped for efficient serving)
-    if args.profile.endswith(".gz"):
-        with open(args.profile, "rb") as f:
-            ProfileHandler.profile_data = f.read()
-    else:
-        with open(args.profile, "rb") as f:
-            raw = f.read()
-        buf = io.BytesIO()
-        with gzip.GzipFile(fileobj=buf, mode="wb") as gz:
-            gz.write(raw)
-        ProfileHandler.profile_data = buf.getvalue()
-
-    http.server.HTTPServer.allow_reuse_address = True
-    server = http.server.HTTPServer(("127.0.0.1", args.port), ProfileHandler)
-    profile_url = f"http://127.0.0.1:{args.port}/profile.json"
-    encoded = urllib.parse.quote(profile_url, safe="")
-    viewer_url = f"https://profiler.firefox.com/from-url/{encoded}"
-
-    if not args.no_open:
-        # Open browser after a short delay to let server start
-        def open_browser():
-            webbrowser.open(viewer_url)
-        threading.Timer(0.5, open_browser).start()
-
-    print(f"Serving profile at {profile_url}", file=sys.stderr)
-    print(f"Firefox Profiler: {viewer_url}", file=sys.stderr)
-    print("Press Ctrl+C to stop.", file=sys.stderr)
-
-    try:
-        server.serve_forever()
-    except KeyboardInterrupt:
-        print("\nStopped.", file=sys.stderr)
-        server.server_close()
-
-
-if __name__ == "__main__":
-    main()

script/profiler/symbolicate_profile.py

@@ -1,198 +0,0 @@
-#!/usr/bin/env python3
-"""
-Symbolicate a raw samply profile using samply's symbolication API,
-then demangle Lean names.
-
-Usage:
-    python symbolicate_profile.py --server http://127.0.0.1:3000/TOKEN \
-        raw-profile.json.gz -o symbolicated-demangled.json.gz
-"""
-
-import argparse
-import gzip
-import json
-import sys
-import urllib.request
-
-from lean_demangle import demangle_lean_name
-
-
-def symbolicate_and_demangle(profile, server_url):
-    """
-    Symbolicate a raw samply profile via the symbolication API,
-    then demangle Lean names. Modifies the profile in-place.
-    Returns the number of names resolved.
-    """
-    libs = profile.get("libs", [])
-    memory_map = [[lib["debugName"], lib["breakpadId"]] for lib in libs]
-
-    count = 0
-    for thread in profile.get("threads", []):
-        count += _process_thread(thread, libs, memory_map, server_url)
-
-    return count
-
-
-def _process_thread(thread, libs, memory_map, server_url):
-    """Symbolicate and demangle one thread. Returns count of resolved names."""
-    sa = thread.get("stringArray")
-    ft = thread.get("frameTable")
-    func_t = thread.get("funcTable")
-    rt = thread.get("resourceTable")
-
-    if not all([sa, ft, func_t, rt]):
-        return 0
-
-    # Build mapping: func_index -> (lib_index, address)
-    # A function may be referenced by multiple frames; pick any address.
-    func_info = {}  # func_idx -> (lib_idx, address)
-    for i in range(ft.get("length", 0)):
-        addr = ft["address"][i]
-        func_idx = ft["func"][i]
-        if func_idx in func_info:
-            continue
-        res_idx = func_t["resource"][func_idx]
-        if res_idx < 0 or res_idx >= rt.get("length", 0):
-            continue
-        lib_idx = rt["lib"][res_idx]
-        if lib_idx < 0 or lib_idx >= len(libs):
-            continue
-        func_info[func_idx] = (lib_idx, addr)
-
-    if not func_info:
-        return 0
-
-    # Batch symbolication: group by lib, send all addresses at once
-    frames_to_symbolicate = []
-    func_order = []  # track which func each frame corresponds to
-    for func_idx, (lib_idx, addr) in func_info.items():
-        frames_to_symbolicate.append([lib_idx, addr])
-        func_order.append(func_idx)
-
-    # Call the symbolication API
-    symbols = _call_symbolication_api(
-        server_url, memory_map, frames_to_symbolicate)
-
-    if not symbols:
-        return 0
-
-    # Update stringArray with demangled names
-    count = 0
-    for func_idx, symbol_name in zip(func_order, symbols):
-        if symbol_name is None:
-            continue
-        demangled = demangle_lean_name(symbol_name)
-        name_idx = func_t["name"][func_idx]
-        if name_idx < len(sa):
-            sa[name_idx] = demangled
-            count += 1
-
-    return count
-
-
-def _call_symbolication_api(server_url, memory_map, frames):
-    """
-    Call the Firefox Profiler symbolication API v5.
-    frames: list of [lib_index, address]
-    Returns: list of symbol names (or None for unresolved frames).
-    """
-    url = server_url.rstrip("/") + "/symbolicate/v5"
-
-    # Send all frames as one "stack" in one job
-    req_body = json.dumps({
-        "memoryMap": memory_map,
-        "stacks": [frames],
-    }).encode()
-
-    req = urllib.request.Request(
-        url,
-        data=req_body,
-        headers={"Content-Type": "application/json"},
-    )
-
-    try:
-        with urllib.request.urlopen(req, timeout=60) as resp:
-            result = json.loads(resp.read())
-    except Exception as e:
-        print(f"Symbolication API error: {e}", file=sys.stderr)
-        return None
-
-    if "error" in result:
-        print(f"Symbolication API error: {result['error']}", file=sys.stderr)
-        return None
-
-    # Extract symbol names from result
-    results = result.get("results", [])
-    if not results:
-        return None
-
-    stacks = results[0].get("stacks", [[]])
-    if not stacks:
-        return None
-
-    symbols = []
-    for frame_result in stacks[0]:
-        if isinstance(frame_result, dict):
-            symbols.append(frame_result.get("function"))
-        elif isinstance(frame_result, str):
-            symbols.append(frame_result)
-        else:
-            symbols.append(None)
-
-    return symbols
-
-
-def process_file(input_path, output_path, server_url):
-    """Read a raw profile, symbolicate + demangle, write it back."""
-    is_gzip = input_path.endswith('.gz')
-
-    if is_gzip:
-        with gzip.open(input_path, 'rt', encoding='utf-8') as f:
-            profile = json.load(f)
-    else:
-        with open(input_path, 'r', encoding='utf-8') as f:
-            profile = json.load(f)
-
-    count = symbolicate_and_demangle(profile, server_url)
-
-    out_gzip = output_path.endswith('.gz') if output_path else is_gzip
-    if output_path:
-        if out_gzip:
-            with gzip.open(output_path, 'wt', encoding='utf-8') as f:
-                json.dump(profile, f, ensure_ascii=False)
-        else:
-            with open(output_path, 'w', encoding='utf-8') as f:
-                json.dump(profile, f, ensure_ascii=False)
-    else:
-        json.dump(profile, sys.stdout, ensure_ascii=False)
-        sys.stdout.write('\n')
-
-    return count
-
-
-def main():
-    parser = argparse.ArgumentParser(
-        description="Symbolicate a raw samply profile and demangle Lean names")
-    parser.add_argument('input', help='Raw profile (JSON or .json.gz)')
-    parser.add_argument('-o', '--output', help='Output path')
-    parser.add_argument('--server', required=True,
-                        help='Samply server URL (e.g., http://127.0.0.1:3000/TOKEN)')
-    args = parser.parse_args()
-
-    output = args.output
-    if output is None:
-        inp = args.input
-        if inp.endswith('.json.gz'):
-            output = inp[:-8] + '-demangled.json.gz'
-        elif inp.endswith('.json'):
-            output = inp[:-5] + '-demangled.json'
-        else:
-            output = inp + '-demangled'
-
-    count = process_file(args.input, output, args.server)
-    print(f"Symbolicated and demangled {count} names, wrote {output}",
-          file=sys.stderr)
-
-
-if __name__ == '__main__':
-    main()

script/release_checklist.py

@@ -11,7 +11,7 @@ IMPORTANT: Keep this documentation up-to-date when modifying the script's behavi
 What this script does:
 1. Validates preliminary Lean4 release infrastructure:
    - Checks that the release branch (releases/vX.Y.0) exists
-   - Verifies CMake version settings are correct (both src/ and stage0/)
+   - Verifies CMake version settings are correct
    - Confirms the release tag exists
    - Validates the release page exists on GitHub (created automatically by CI after tag push)
    - Checks the release notes page on lean-lang.org (updated while bumping the `reference-manual` repository)
@@ -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 {}
@@ -326,42 +302,6 @@ def check_cmake_version(repo_url, branch, version_major, version_minor, github_t
     print(f"  ✅ CMake version settings are correct in {cmake_file_path}")
     return True
 
-def check_stage0_version(repo_url, branch, version_major, version_minor, github_token):
-    """Verify that stage0/src/CMakeLists.txt has the same version as src/CMakeLists.txt.
-
-    The stage0 pre-built binaries stamp .olean headers with their baked-in version.
-    If stage0 has a different version (e.g. from a 'begin development cycle' bump),
-    the release tarball will contain .olean files with the wrong version.
-    """
-    stage0_cmake = "stage0/src/CMakeLists.txt"
-    content = get_branch_content(repo_url, branch, stage0_cmake, github_token)
-    if content is None:
-        print(f"  ❌ Could not retrieve {stage0_cmake} from {branch}")
-        return False
-
-    errors = []
-    for line in content.splitlines():
-        stripped = line.strip()
-        if stripped.startswith("set(LEAN_VERSION_MAJOR "):
-            actual = stripped.split()[-1].rstrip(")")
-            if actual != str(version_major):
-                errors.append(f"LEAN_VERSION_MAJOR: expected {version_major}, found {actual}")
-        elif stripped.startswith("set(LEAN_VERSION_MINOR "):
-            actual = stripped.split()[-1].rstrip(")")
-            if actual != str(version_minor):
-                errors.append(f"LEAN_VERSION_MINOR: expected {version_minor}, found {actual}")
-
-    if errors:
-        print(f"  ❌ stage0 version mismatch in {stage0_cmake}:")
-        for error in errors:
-            print(f"     {error}")
-        print(f"     The stage0 compiler stamps .olean headers with its baked-in version.")
-        print(f"     Run `make update-stage0` to rebuild stage0 with the correct version.")
-        return False
-
-    print(f"  ✅ stage0 version matches in {stage0_cmake}")
-    return True
-
 def extract_org_repo_from_url(repo_url):
     """Extract the 'org/repo' part from a GitHub URL."""
     if repo_url.startswith("https://github.com/"):
@@ -477,10 +417,7 @@ def get_pr_ci_status(repo_url, pr_number, github_token):
     conclusions = [run['conclusion'] for run in check_runs if run.get('status') == 'completed']
     in_progress = [run for run in check_runs if run.get('status') in ['queued', 'in_progress']]
 
-    failed = sum(1 for c in conclusions if c in ['failure', 'timed_out', 'action_required'])
     if in_progress:
-        if failed > 0:
-            return "failure", f"{failed} check(s) failing, {len(in_progress)} still in progress"
         return "pending", f"{len(in_progress)} check(s) in progress"
 
     if not conclusions:
@@ -489,6 +426,7 @@ def get_pr_ci_status(repo_url, pr_number, github_token):
     if all(c == 'success' for c in conclusions):
         return "success", f"All {len(conclusions)} checks passed"
 
+    failed = sum(1 for c in conclusions if c in ['failure', 'timed_out', 'action_required'])
     if failed > 0:
         return "failure", f"{failed} check(s) failed"
 
@@ -563,76 +501,6 @@ def check_proofwidgets4_release(repo_url, target_toolchain, github_token):
     print(f"     You will need to create and push a tag v0.0.{next_version}")
     return False
 
-def check_reference_manual_release_title(repo_url, toolchain, pr_branch, github_token):
-    """Check if the reference-manual release notes title matches the release type.
-
-    For RC releases (e.g., v4.27.0-rc1), the title should contain the exact RC suffix.
-    For final releases (e.g., v4.27.0), the title should NOT contain any "-rc".
-
-    Returns True if check passes or is not applicable, False if title needs updating.
-    """
-    is_rc = is_release_candidate(toolchain)
-
-    # For RC releases, get the base version and RC suffix
-    # e.g., "v4.27.0-rc1" -> version="4.27.0", rc_suffix="-rc1"
-    if is_rc:
-        parts = toolchain.lstrip('v').split('-', 1)
-        version = parts[0]
-        rc_suffix = '-' + parts[1] if len(parts) > 1 else ''
-    else:
-        version = toolchain.lstrip('v')
-        rc_suffix = ''
-
-    # Construct the release notes file path (e.g., Manual/Releases/v4_27_0.lean for v4.27.0)
-    file_name = f"v{version.replace('.', '_')}.lean"  # "v4_27_0.lean"
-    file_path = f"Manual/Releases/{file_name}"
-
-    # Try to get the file from the PR branch first, then fall back to main branch
-    content = get_branch_content(repo_url, pr_branch, file_path, github_token)
-    if content is None:
-        # Try the default branch
-        content = get_branch_content(repo_url, "main", file_path, github_token)
-
-    if content is None:
-        print(f"  ⚠️  Could not check release notes file: {file_path}")
-        return True  # Don't block on this
-
-    # Look for the #doc line with the title
-    for line in content.splitlines():
-        if line.strip().startswith('#doc') and 'Manual' in line:
-            has_rc_in_title = '-rc' in line.lower()
-
-            if is_rc:
-                # For RC releases, title should contain the exact RC suffix (e.g., "-rc1")
-                # Use regex to match exact suffix followed by non-digit (to avoid -rc1 matching -rc10)
-                # Pattern matches the RC suffix followed by a non-digit or end-of-string context
-                # e.g., "-rc1" followed by space, quote, paren, or similar
-                exact_match = re.search(rf'{re.escape(rc_suffix)}(?![0-9])', line, re.IGNORECASE)
-                if exact_match:
-                    print(f"  ✅ Release notes title correctly shows {rc_suffix}")
-                    return True
-                elif has_rc_in_title:
-                    print(f"  ❌ Release notes title shows wrong RC version (expected {rc_suffix})")
-                    print(f"     Update {file_path} to use '{rc_suffix}' in the title")
-                    return False
-                else:
-                    print(f"  ❌ Release notes title missing RC suffix")
-                    print(f"     Update {file_path} to include '{rc_suffix}' in the title")
-                    return False
-            else:
-                # For final releases, title should NOT contain -rc
-                if has_rc_in_title:
-                    print(f"  ❌ Release notes title still shows RC version")
-                    print(f"     Update {file_path} to remove '-rcN' from the title")
-                    return False
-                else:
-                    print(f"  ✅ Release notes title is updated for final release")
-                    return True
-
-    # If we didn't find the #doc line, don't block
-    print(f"  ⚠️  Could not find release notes title in {file_path}")
-    return True
-
 def run_mathlib_verify_version_tags(toolchain, verbose=False):
     """Run mathlib4's verify_version_tags.py script to validate the release tag.
 
@@ -718,9 +586,6 @@ def main():
         # Check CMake version settings
         if not check_cmake_version(lean_repo_url, branch_name, version_major, version_minor, github_token):
             lean4_success = False
-        # Check that stage0 version matches (stage0 stamps .olean headers with its version)
-        if not check_stage0_version(lean_repo_url, branch_name, version_major, version_minor, github_token):
-            lean4_success = False
 
     # Check for tag and release page
     if not tag_exists(lean_repo_url, toolchain, github_token):
@@ -779,27 +644,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
@@ -865,11 +709,6 @@ def main():
                     print(f"     ⚠️  CI: {ci_message}")
                 else:
                     print(f"     ❓ CI: {ci_message}")
-
-                # For reference-manual, check that the release notes title has been updated
-                if name == "reference-manual":
-                    pr_branch = f"bump_to_{toolchain}"
-                    check_reference_manual_release_title(url, toolchain, pr_branch, github_token)
             else:
                 print(f"  ❌ PR with title '{pr_title}' does not exist")
                 print(f"     Run `script/release_steps.py {toolchain} {name}` to create it")
@@ -877,14 +716,6 @@ def main():
             continue
         print(f"  ✅ On compatible toolchain (>= {toolchain})")
 
-        # For reference-manual, check that the release notes title is correct BEFORE tagging.
-        # This catches the case where the toolchain bump PR was merged without updating
-        # the release notes title (e.g., still showing "-rc1" for a stable release).
-        if name == "reference-manual":
-            if not check_reference_manual_release_title(url, toolchain, branch, github_token):
-                repo_status[name] = False
-                continue
-
         # Special handling for ProofWidgets4
         if name == "ProofWidgets4":
             if not check_proofwidgets4_release(url, toolchain, github_token):
@@ -965,8 +796,8 @@ def main():
             
             print(f"  ✅ Bump branch {bump_branch} exists")
             
-            # Update the lean-toolchain to the latest nightly for newly created bump branches
-            if branch_created:
+            # For batteries and mathlib4, update the lean-toolchain to the latest nightly
+            if branch_created and name in ["batteries", "mathlib4"]:
                 latest_nightly = get_latest_nightly_tag(github_token)
                 if latest_nightly:
                     nightly_toolchain = f"leanprover/lean4:{latest_nightly}"
@@ -1006,15 +837,14 @@ def main():
         # Find the actual minor version in CMakeLists.txt
         for line in cmake_lines:
             if line.strip().startswith("set(LEAN_VERSION_MINOR "):
-                m = re.search(r'set\(LEAN_VERSION_MINOR\s+(\d+)', line)
-                actual_minor = int(m.group(1)) if m else 0
+                actual_minor = int(line.split()[-1].rstrip(")"))
                 version_minor_correct = actual_minor >= next_minor
                 break
         else:
             version_minor_correct = False
             
         is_release_correct = any(
-            re.match(r'set\(LEAN_VERSION_IS_RELEASE\s+0[\s)]', l.strip())
+            l.strip().startswith("set(LEAN_VERSION_IS_RELEASE 0)") 
             for l in cmake_lines
         )
         

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
@@ -65,6 +64,13 @@ repositories:
     branch: master
     dependencies: [lean4-unicode-basic]
 
+  - name: doc-gen4
+    url: https://github.com/leanprover/doc-gen4
+    toolchain-tag: true
+    stable-branch: false
+    branch: main
+    dependencies: [lean4-cli, BibtexQuery]
+
   - name: reference-manual
     url: https://github.com/leanprover/reference-manual
     toolchain-tag: true
@@ -77,7 +83,8 @@ repositories:
     toolchain-tag: false
     stable-branch: false
     branch: main
-    dependencies: []
+    dependencies:
+      - batteries
 
   - name: aesop
     url: https://github.com/leanprover-community/aesop
@@ -99,16 +106,10 @@ repositories:
       - lean4checker
       - batteries
       - lean4-cli
+      - doc-gen4
       - import-graph
       - plausible
 
-  - name: doc-gen4
-    url: https://github.com/leanprover/doc-gen4
-    toolchain-tag: true
-    stable-branch: false
-    branch: main
-    dependencies: [lean4-cli, BibtexQuery, mathlib4]
-
   - name: cslib
     url: https://github.com/leanprover/cslib
     toolchain-tag: true
@@ -141,15 +142,3 @@ repositories:
     branch: master
     dependencies:
       - verso-web-components
-
-  - name: comparator
-    url: https://github.com/leanprover/comparator
-    toolchain-tag: true
-    stable-branch: false
-    branch: master
-
-  - name: lean4export
-    url: https://github.com/leanprover/lean4export
-    toolchain-tag: true
-    stable-branch: false
-    branch: master

script/release_steps.py

@@ -24,7 +24,6 @@ What this script does:
    - Safety checks for repositories using bump branches
    - Custom build and test procedures
    - lean-fro.org: runs scripts/update.sh to regenerate site content
-   - mathlib4: updates ProofWidgets4 pin (v0.0.X sequential tags, not v4.X.Y)
 
 6. Commits the changes with message "chore: bump toolchain to {version}"
 
@@ -60,8 +59,6 @@ import re
 import subprocess
 import shutil
 import json
-import requests
-import base64
 from pathlib import Path
 
 # Color functions for terminal output
@@ -118,60 +115,6 @@ def find_repo(repo_name, config):
         sys.exit(1)
     return matching_repos[0]
 
-def get_github_token():
-    try:
-        result = subprocess.run(['gh', 'auth', 'token'], capture_output=True, text=True)
-        if result.returncode == 0:
-            return result.stdout.strip()
-    except FileNotFoundError:
-        pass
-    return None
-
-def find_proofwidgets_tag(version):
-    """Find the latest ProofWidgets4 tag that uses the given toolchain version.
-
-    ProofWidgets4 uses sequential version tags (v0.0.X) rather than toolchain-based tags.
-    This function finds the most recent tag whose lean-toolchain matches the target version
-    exactly, checking the 20 most recent tags.
-    """
-    github_token = get_github_token()
-    api_base = "https://api.github.com/repos/leanprover-community/ProofWidgets4"
-    headers = {'Authorization': f'token {github_token}'} if github_token else {}
-
-    response = requests.get(f"{api_base}/git/matching-refs/tags/v0.0.", headers=headers, timeout=30)
-    if response.status_code != 200:
-        return None
-
-    tags = response.json()
-    tag_names = []
-    for tag in tags:
-        ref = tag['ref']
-        if ref.startswith('refs/tags/v0.0.'):
-            tag_name = ref.replace('refs/tags/', '')
-            try:
-                version_num = int(tag_name.split('.')[-1])
-                tag_names.append((version_num, tag_name))
-            except (ValueError, IndexError):
-                continue
-
-    if not tag_names:
-        return None
-
-    # Sort by version number (descending) and check recent tags
-    tag_names.sort(reverse=True)
-    target = f"leanprover/lean4:{version}"
-    for _, tag_name in tag_names[:20]:
-        # Fetch lean-toolchain for this tag
-        api_url = f"{api_base}/contents/lean-toolchain?ref={tag_name}"
-        resp = requests.get(api_url, headers=headers, timeout=30)
-        if resp.status_code != 200:
-            continue
-        content = base64.b64decode(resp.json().get("content", "").replace("\n", "")).decode('utf-8').strip()
-        if content == target:
-            return tag_name
-
-    return None
-
 def setup_downstream_releases_dir():
     """Create the downstream_releases directory if it doesn't exist."""
     downstream_dir = Path("downstream_releases")
@@ -479,85 +422,10 @@ def execute_release_steps(repo, version, config):
         print(blue("Updating lakefile.toml..."))
         run_command(f'perl -pi -e \'s/"v4\\.[0-9]+(\\.[0-9]+)?(-rc[0-9]+)?"/"' + version + '"/g\' lakefile.*', cwd=repo_path)
         run_command("lake update", cwd=repo_path, stream_output=True)
-    elif repo_name == "verso":
-        # verso has nested Lake projects in test-projects/ that each have their own
-        # lake-manifest.json with a subverso pin. After updating the root manifest via
-        # `lake update`, sync the de-modulized subverso rev into all sub-manifests.
-        # The sub-projects use an old toolchain (v4.21.0) that doesn't support module/prelude
-        # syntax, so they need the de-modulized version (tagged no-modules/<root-rev>).
-        # The "SubVerso version consistency" CI check accepts either the root or de-modulized rev.
-        run_command("lake update", cwd=repo_path, stream_output=True)
-        print(blue("Syncing de-modulized subverso rev to test-project sub-manifests..."))
-        sync_script = (
-            'ROOT_REV=$(jq -r \'.packages[] | select(.name == "subverso") | .rev\' lake-manifest.json); '
-            'SUBVERSO_URL=$(jq -r \'.packages[] | select(.name == "subverso") | .url\' lake-manifest.json); '
-            'DEMOD_REV=$(git ls-remote "$SUBVERSO_URL" "refs/tags/no-modules/$ROOT_REV" | awk \'{print $1}\'); '
-            'find test-projects -name lake-manifest.json -print0 | while IFS= read -r -d \'\' f; do '
-            'jq --arg rev "$DEMOD_REV" \'.packages |= map(if .name == "subverso" then .rev = $rev else . end)\' "$f" > /tmp/lm_tmp.json && mv /tmp/lm_tmp.json "$f"; '
-            'done'
-        )
-        run_command(sync_script, cwd=repo_path)
-        print(green("Synced de-modulized subverso rev to all test-project sub-manifests"))
     elif dependencies:
         run_command(f'perl -pi -e \'s/"v4\\.[0-9]+(\\.[0-9]+)?(-rc[0-9]+)?"/"' + version + '"/g\' lakefile.*', cwd=repo_path)
         run_command("lake update", cwd=repo_path, stream_output=True)
 
-    # For reference-manual, update the release notes title to match the target version.
-    # e.g., for a stable release, change "Lean 4.28.0-rc1 (date)" to "Lean 4.28.0 (date)"
-    # e.g., for rc2, change "Lean 4.28.0-rc1 (date)" to "Lean 4.28.0-rc2 (date)"
-    if repo_name == "reference-manual":
-        base_version = version.lstrip('v').split('-')[0]  # "4.28.0"
-        file_name = f"v{base_version.replace('.', '_')}.lean"
-        release_notes_file = repo_path / "Manual" / "Releases" / file_name
-
-        if release_notes_file.exists():
-            is_rc = "-rc" in version
-            if is_rc:
-                # For RC releases, update to the exact RC version
-                display_version = version.lstrip('v')  # "4.28.0-rc2"
-            else:
-                # For stable releases, strip any RC suffix
-                display_version = base_version  # "4.28.0"
-
-            print(blue(f"Updating release notes title in {file_name}..."))
-            content = release_notes_file.read_text()
-            # Match the #doc line title: "Lean X.Y.Z-rcN (date)" or "Lean X.Y.Z (date)"
-            new_content = re.sub(
-                r'(#doc\s+\(Manual\)\s+"Lean\s+)\d+\.\d+\.\d+(-rc\d+)?(\s+\([^)]*\)"\s*=>)',
-                rf'\g<1>{display_version}\3',
-                content
-            )
-            if new_content != content:
-                release_notes_file.write_text(new_content)
-                print(green(f"Updated release notes title to Lean {display_version}"))
-            else:
-                print(green("Release notes title already correct"))
-        else:
-            print(yellow(f"Release notes file {file_name} not found, skipping title update"))
-
-    # For mathlib4, update ProofWidgets4 pin (it uses sequential v0.0.X tags, not v4.X.Y)
-    if repo_name == "mathlib4":
-        print(blue("Checking ProofWidgets4 version pin..."))
-        pw_tag = find_proofwidgets_tag(version)
-        if pw_tag:
-            print(blue(f"Updating ProofWidgets4 pin to {pw_tag}..."))
-            for lakefile in repo_path.glob("lakefile.*"):
-                content = lakefile.read_text()
-                # Only update the ProofWidgets4 dependency line, not other v0.0.X pins
-                new_content = re.sub(
-                    r'(require\s+"leanprover-community"\s*/\s*"proofwidgets"\s*@\s*git\s+"v)0\.0\.\d+(")',
-                    rf'\g<1>{pw_tag.removeprefix("v")}\2',
-                    content
-                )
-                if new_content != content:
-                    lakefile.write_text(new_content)
-                    print(green(f"Updated ProofWidgets4 pin in {lakefile.name}"))
-            run_command("lake update proofwidgets", cwd=repo_path, stream_output=True)
-            print(green(f"Updated ProofWidgets4 to {pw_tag}"))
-        else:
-            print(yellow(f"Could not find a ProofWidgets4 tag for toolchain {version}"))
-            print(yellow("You may need to update the ProofWidgets4 pin manually"))
-
     # Commit changes (only if there are changes)
     print(blue("Checking for changes to commit..."))
     try:

src/Init.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
+
 prelude
 public import Init.Prelude
 public import Init.Notation
@@ -30,7 +31,6 @@ public import Init.Hints
 public import Init.Conv
 public import Init.Guard
 public import Init.Simproc
-public import Init.CbvSimproc
 public import Init.SizeOfLemmas
 public import Init.BinderPredicates
 public import Init.Ext
@@ -38,12 +38,11 @@ public import Init.Omega
 public import Init.MacroTrace
 public import Init.Grind
 public import Init.GrindInstances
-public import Init.Sym
 public import Init.While
 public import Init.Syntax
 public import Init.Internal
 public import Init.Try
-public meta import Init.Try  -- shake: keep (make sure `Try.Config` can be evaluated anywhere)
+public meta import Init.Try  -- make sure `Try.Config` can be evaluated anywhere
 public import Init.BinderNameHint
 public import Init.Task
 public import Init.MethodSpecsSimp

src/Init/BinderNameHint.lean

@@ -7,8 +7,7 @@ Authors: Joachim Breitner
 module
 
 prelude
-public import Init.Prelude
-import Init.Tactics
+public import Init.Tactics
 
 public section
 

src/Init/BinderPredicates.lean

@@ -6,10 +6,7 @@ Authors: Gabriel Ebner
 module
 
 prelude
-public meta import Init.Grind.Tactics
-public import Init.Notation
-import Init.Meta.Defs
-import Init.NotationExtra
+public import Init.NotationExtra
 
 public section
 

src/Init/ByCases.lean

@@ -6,9 +6,7 @@ Authors: Leonardo de Moura, Mario Carneiro
 module
 
 prelude
-public meta import Init.Grind.Tactics
-public import Init.Grind.Tactics
-import Init.SimpLemmas
+public import Init.Classical
 
 public section
 

src/Init/CbvSimproc.lean

@@ -1,71 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Wojciech Różowski
--/
-module
-
-prelude
-public meta import Init.Data.ToString.Name  -- shake: keep (transitive public meta dep, fix)
-public import Init.Tactics
-import Init.Meta.Defs
-
-public section
-
-namespace Lean.Parser
-
-syntax cbvSimprocEval := "cbv_eval"
-
-/--
-A user-defined simplification procedure used by the `cbv` tactic.
-The body must have type `Lean.Meta.Sym.Simp.Simproc` (`Expr → SimpM Result`).
-Procedures are indexed by a discrimination tree pattern and fire at one of three phases:
-`↓` (pre), `cbv_eval` (eval), or `↑` (post, default).
--/
-syntax (docComment)? attrKind "cbv_simproc " (Tactic.simpPre <|> Tactic.simpPost <|> cbvSimprocEval)? ident " (" term ")" " := " term : command
-
-/--
-A `cbv_simproc` declaration without automatically adding it to the cbv simproc set.
-To activate, use `attribute [cbv_simproc]`.
--/
-syntax (docComment)? "cbv_simproc_decl " ident " (" term ")" " := " term : command
-
-syntax (docComment)? attrKind "builtin_cbv_simproc " (Tactic.simpPre <|> Tactic.simpPost <|> cbvSimprocEval)? ident " (" term ")" " := " term : command
-
-syntax (docComment)? "builtin_cbv_simproc_decl " ident " (" term ")" " := " term : command
-
-syntax (name := cbvSimprocPattern) "cbv_simproc_pattern% " term " => " ident : command
-
-syntax (name := cbvSimprocPatternBuiltin) "builtin_cbv_simproc_pattern% " term " => " ident : command
-
-namespace Attr
-
-syntax (name := cbvSimprocAttr) "cbv_simproc" (Tactic.simpPre <|> Tactic.simpPost <|> cbvSimprocEval)? : attr
-
-syntax (name := cbvSimprocBuiltinAttr) "builtin_cbv_simproc" (Tactic.simpPre <|> Tactic.simpPost <|> cbvSimprocEval)? : attr
-
-end Attr
-
-macro_rules
-  | `($[$doc?:docComment]? cbv_simproc_decl $n:ident ($pattern:term) := $body) => do
-    let simprocType := `Lean.Meta.Sym.Simp.Simproc
-    `($[$doc?:docComment]? meta def $n:ident : $(mkIdent simprocType) := $body
-      cbv_simproc_pattern% $pattern => $n)
-
-macro_rules
-  | `($[$doc?:docComment]? builtin_cbv_simproc_decl $n:ident ($pattern:term) := $body) => do
-    let simprocType := `Lean.Meta.Sym.Simp.Simproc
-    `($[$doc?:docComment]? def $n:ident : $(mkIdent simprocType) := $body
-      builtin_cbv_simproc_pattern% $pattern => $n)
-
-macro_rules
-  | `($[$doc?:docComment]? $kind:attrKind cbv_simproc $[$phase?]? $n:ident ($pattern:term) := $body) => do
-    `($[$doc?:docComment]? cbv_simproc_decl $n ($pattern) := $body
-      attribute [$kind cbv_simproc $[$phase?]?] $n)
-
-macro_rules
-  | `($[$doc?:docComment]? $kind:attrKind builtin_cbv_simproc $[$phase?]? $n:ident ($pattern:term) := $body) => do
-    `($[$doc?:docComment]? builtin_cbv_simproc_decl $n ($pattern) := $body
-      attribute [$kind builtin_cbv_simproc $[$phase?]?] $n)
-
-end Lean.Parser

src/Init/Classical.lean

@@ -69,11 +69,9 @@ theorem em (p : Prop) : p ∨ ¬p :=
 theorem exists_true_of_nonempty {α : Sort u} : Nonempty α → ∃ _ : α, True
   | ⟨x⟩ => ⟨x, trivial⟩
 
-@[implicit_reducible]
 noncomputable def inhabited_of_nonempty {α : Sort u} (h : Nonempty α) : Inhabited α :=
   ⟨choice h⟩
 
-@[implicit_reducible]
 noncomputable def inhabited_of_exists {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : Inhabited α :=
   inhabited_of_nonempty (Exists.elim h (fun w _ => ⟨w⟩))
 
@@ -83,7 +81,6 @@ noncomputable scoped instance (priority := low) propDecidable (a : Prop) : Decid
     | Or.inl h => ⟨isTrue h⟩
     | Or.inr h => ⟨isFalse h⟩
 
-@[implicit_reducible]
 noncomputable def decidableInhabited (a : Prop) : Inhabited (Decidable a) where
   default := inferInstance
 
@@ -105,7 +102,7 @@ noncomputable def strongIndefiniteDescription {α : Sort u} (p : α → Prop) (h
       ⟨xp.val, fun _ => xp.property⟩)
     (fun hp => ⟨choice h, fun h => absurd h hp⟩)
 
-/-- The Hilbert epsilon function. -/
+/-- the Hilbert epsilon Function -/
 noncomputable def epsilon {α : Sort u} [h : Nonempty α] (p : α → Prop) : α :=
   (strongIndefiniteDescription p h).val
 
@@ -145,7 +142,6 @@ is classically true but not constructively. -/
 
 /-- Transfer decidability of `¬ p` to decidability of `p`. -/
 -- This can not be an instance as it would be tried everywhere.
-@[implicit_reducible]
 def decidable_of_decidable_not (p : Prop) [h : Decidable (¬ p)] : Decidable p :=
   match h with
   | isFalse h => isTrue (Classical.not_not.mp h)

src/Init/Control.lean

@@ -17,5 +17,3 @@ public import Init.Control.Lawful
 public import Init.Control.StateCps
 public import Init.Control.ExceptCps
 public import Init.Control.MonadAttach
-public import Init.Control.EState
-public import Init.Control.Do

src/Init/Control/Basic.lean

@@ -29,7 +29,7 @@ instance (priority := 500) instForInOfForIn' [ForIn' m ρ α d] : ForIn m ρ α
     (f : (a : α) → a ∈ x → β → m (ForInStep β)) (g : (a : α) → β → m (ForInStep β))
     (h : ∀ a m b, f a m b = g a b) :
     forIn' x b f = forIn x b g := by
-  simp [forIn]
+  simp [instForInOfForIn']
   congr
   apply funext
   intro a
@@ -144,7 +144,7 @@ instance : ToBool Bool where
 Converts the result of the monadic action `x` to a `Bool`. If it is `true`, returns it and ignores
 `y`; otherwise, runs `y` and returns its result.
 
-This is a monadic counterpart to the short-circuiting `||` operator, usually accessed via the `<||>`
+This a monadic counterpart to the short-circuiting `||` operator, usually accessed via the `<||>`
 operator.
 -/
 @[macro_inline] def orM {m : Type u → Type v} {β : Type u} [Monad m] [ToBool β] (x y : m β) : m β := do
@@ -161,7 +161,7 @@ recommended_spelling "orM" for "<||>" in [orM, «term_<||>_»]
 Converts the result of the monadic action `x` to a `Bool`. If it is `true`, returns `y`; otherwise,
 returns the original result of `x`.
 
-This is a monadic counterpart to the short-circuiting `&&` operator, usually accessed via the `<&&>`
+This a monadic counterpart to the short-circuiting `&&` operator, usually accessed via the `<&&>`
 operator.
 -/
 @[macro_inline] def andM {m : Type u → Type v} {β : Type u} [Monad m] [ToBool β] (x y : m β) : m β := do
@@ -322,8 +322,6 @@ class MonadControl (m : semiOutParam (Type u → Type v)) (n : Type u → Type w
   -/
   restoreM : {α : Type u} → m (stM α) → n α
 
-attribute [reducible] MonadControl.stM
-
 /--
 A way to lift a computation from one monad to another while providing the lifted computation with a
 means of interpreting computations from the outer monad. This provides a means of lifting
@@ -351,8 +349,6 @@ class MonadControlT (m : Type u → Type v) (n : Type u → Type w) where
   -/
   restoreM {α : Type u} : stM α → n α
 
-attribute [reducible] MonadControlT.stM
-
 export MonadControlT (stM liftWith restoreM)
 
 @[always_inline]

src/Init/Control/Do.lean

@@ -1,63 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Graf
--/
-module
-
-prelude
-public import Init.Control.Except
-public import Init.Control.Option
-
-public section
-
-/-!
-This module provides specialized wrappers around `ExceptT` to support the `do` elaborator.
-
-Specifically, the types here are used to tunnel early `return`, `break` and `continue` through
-non-algebraic higher-order effect combinators such as `tryCatch`.
--/
-
-/-- A wrapper around `ExceptT` signifying early return. -/
-@[expose]
-abbrev EarlyReturnT (ρ m α) := ExceptT ρ m α
-
-/-- Exit a computation by returning a value `r : ρ` early. -/
-@[always_inline, inline, expose]
-abbrev EarlyReturnT.return {ρ m α} [Monad m] (r : ρ) : EarlyReturnT ρ m α :=
-  throw r
-
-/-- A specialization of `Except.casesOn`. -/
-@[always_inline, inline, expose]
-abbrev EarlyReturn.runK {ρ α : Type u} {β : Type v} (x : Except ρ α) (ret : ρ → β) (pure : α → β) : β :=
-  x.casesOn ret pure
-
-/-- A wrapper around `OptionT` signifying `break` in a loop. -/
-@[expose]
-abbrev BreakT := OptionT
-
-/-- Exit a loop body via `break`. -/
-@[always_inline, inline, expose]
-abbrev BreakT.break {m : Type w → Type x} [Monad m] : BreakT m α := failure
-
-/-- A specialization of `Option.casesOn`. -/
-@[always_inline, inline, expose]
-abbrev Break.runK {α : Type u} {β : Type v} (x : Option α) (breakK : Unit → β) (successK : α → β) : β :=
-  -- Note: The matcher below is used in the elaborator targeting `forIn` loops.
-  -- If you change the order of match arms here, you may need to adjust the elaborator.
-  match x with
-  | some a => successK a
-  | none => breakK ()
-
-/-- A wrapper around `OptionT` signifying `continue` in a loop. -/
-@[expose]
-abbrev ContinueT := OptionT
-
-/-- Exit a loop body via `continue`. -/
-@[always_inline, inline, expose]
-abbrev ContinueT.continue {m : Type w → Type x} [Monad m] : ContinueT m α := failure
-
-/-- A specialization of `Option.casesOn`. -/
-@[always_inline, inline, expose]
-abbrev Continue.runK {α : Type u} {β : Type v} (x : Option α) (continueK : Unit → β) (successK : α → β) : β :=
-  x.casesOn continueK (fun a _ => successK a) ()

src/Init/Control/EState.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Init.Data.ToString.Basic
-public import Init.Control.State
 
 public section
 universe u v

src/Init/Control/ExceptCps.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Init.Control.Lawful.Basic
-import Init.SimpLemmas
 
 public section
 

src/Init/Control/Id.lean

@@ -8,6 +8,7 @@ The identity Monad.
 module
 
 prelude
+public import Init.Core
 public import Init.Control.MonadAttach
 
 public section
@@ -49,7 +50,6 @@ instance : Monad Id where
 /--
 The identity monad has a `bind` operator.
 -/
-@[implicit_reducible]
 def hasBind : Bind Id :=
   inferInstance
 
@@ -59,7 +59,7 @@ Runs a computation in the identity monad.
 This function is the identity function. Because its parameter has type `Id α`, it causes
 `do`-notation in its arguments to use the `Monad Id` instance.
 -/
-@[always_inline, inline, expose, implicit_reducible]
+@[always_inline, inline, expose]
 protected def run (x : Id α) : α := x
 
 instance [OfNat α n] : OfNat (Id α) n :=
@@ -80,11 +80,3 @@ instance : LawfulMonadAttach Id where
     exact x.run.2
 
 end Id
-
-/-- Turn a collection with a pure `ForIn` instance into an array. -/
-def ForIn.toArray {α : Type u} [inst : ForIn Id ρ α] (xs : ρ) : Array α :=
-  ForIn.forIn xs Array.empty (fun a acc => pure (.yield (acc.push a))) |> Id.run
-
-/-- Turn a collection with a pure `ForIn` instance into a list. -/
-def ForIn.toList {α : Type u} [ForIn Id ρ α] (xs : ρ) : List α :=
-  ForIn.toArray xs |>.toList

src/Init/Control/Lawful/Basic.lean

@@ -6,9 +6,7 @@ Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro
 module
 
 prelude
-public import Init.Control.Id
-public import Init.Grind.Tactics
-import Init.Ext
+public import Init.Ext
 
 public section
 
@@ -254,8 +252,8 @@ instance : LawfulMonad Id := by
 @[simp, grind =] theorem run_bind (x : Id α) (f : α → Id β) : (x >>= f).run = (f x.run).run := rfl
 @[simp, grind =] theorem run_pure (a : α) : (pure a : Id α).run = a := rfl
 @[simp, grind =] theorem pure_run (a : Id α) : pure a.run = a := rfl
-@[simp] theorem run_seqRight (x : Id α) (y : Id β) : (x *> y).run = y.run := rfl
-@[simp] theorem run_seqLeft (x : Id α) (y : Id β) : (x <* y).run = x.run := rfl
+@[simp] theorem run_seqRight (x y : Id α) : (x *> y).run = y.run := rfl
+@[simp] theorem run_seqLeft (x y : Id α) : (x <* y).run = x.run := rfl
 @[simp] theorem run_seq (f : Id (α → β)) (x : Id α) : (f <*> x).run = f.run x.run := rfl
 
 end Id

src/Init/Control/Lawful/Instances.lean

@@ -12,8 +12,6 @@ public import Init.Control.Option
 import all Init.Control.Option
 import all Init.Control.State
 public import Init.Control.StateRef
-public import Init.Control.State
-public import Init.Ext
 
 public section
 
@@ -30,8 +28,6 @@ namespace ExceptT
   simp [run] at h
   assumption
 
-@[simp] theorem stM_eq [Monad m] : stM m (ExceptT ε m) α = Except ε α := rfl
-
 @[simp, grind =] theorem run_mk (x : m (Except ε α)) : run (mk x : ExceptT ε m α) = x := rfl
 
 @[simp, grind =] theorem run_pure [Monad m] (x : α) : run (pure x : ExceptT ε m α) = pure (Except.ok x) := rfl
@@ -106,7 +102,7 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (ExceptT ε m) where
 
 @[simp] theorem map_throw [Monad m] [LawfulMonad m] {α β : Type _} (f : α → β) (e : ε) :
     f <$> (throw e : ExceptT ε m α) = (throw e : ExceptT ε m β) := by
-  simp only [Functor.map, ExceptT.map, ExceptT.mk, throw, throwThe, MonadExceptOf.throw,
+  simp only [ExceptT.instMonad, ExceptT.map, ExceptT.mk, throw, throwThe, MonadExceptOf.throw,
     pure_bind]
 
 /-! Note that the `MonadControl` instance for `ExceptT` is not monad-generic. -/
@@ -120,16 +116,11 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (ExceptT ε m) where
 
 @[simp] theorem run_controlAt [Monad m] [LawfulMonad m] (f : ({β : Type u} → ExceptT ε m β → m (stM m (ExceptT ε m) β)) → m (stM m (ExceptT ε m) α)) :
     ExceptT.run (controlAt m f) = f fun x => x.run := by
-  simp [controlAt, run_bind]
+  simp [controlAt, run_bind, bind_map_left]
 
 @[simp] theorem run_control [Monad m] [LawfulMonad m] (f : ({β : Type u} → ExceptT ε m β → m (stM m (ExceptT ε m) β)) → m (stM m (ExceptT ε m) α)) :
     ExceptT.run (control f) = f fun x => x.run := run_controlAt f
 
-@[simp, grind =]
-theorem run_adapt [Monad m] (f : ε → ε') (x : ExceptT ε m α)
-    : run (ExceptT.adapt f x : ExceptT ε' m α) = Except.mapError f <$> run x :=
-  rfl
-
 end ExceptT
 
 /-! # Except -/
@@ -439,6 +430,7 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (StateT σ m) where
 @[simp] theorem run_restoreM [Monad m] [LawfulMonad m] (x : stM m (StateT σ m) α) (s : σ) :
     StateT.run (restoreM x) s = pure x := by
   simp [restoreM, MonadControl.restoreM]
+  rfl
 
 @[simp] theorem run_liftWith [Monad m] [LawfulMonad m] (f : ({β : Type u} → StateT σ m β → m (stM m (StateT σ m) β)) → m α) (s : σ) :
     StateT.run (liftWith f) s = ((·, s) <$> f fun x => x.run s) := by
@@ -475,33 +467,15 @@ namespace EStateM
 @[simp, grind =] theorem run_throw (e : ε) (s : σ):
     EStateM.run (throw e : EStateM ε σ PUnit) s = .error e s := rfl
 
-@[simp, grind =] theorem run_bind (x : EStateM ε σ α) (f : α → EStateM ε σ β)
-    : EStateM.run (x >>= f : EStateM ε σ β) s
-      =
-      match EStateM.run x s with
-      | .ok x s => EStateM.run (f x) s
-      | .error e s => .error e s :=
-  rfl
-
-@[simp, grind =]
-theorem run_adaptExcept (f : ε → ε') (x : EStateM ε σ α) (s : σ)
-    : EStateM.run (EStateM.adaptExcept f x : EStateM ε' σ α) s
-     =
-     match EStateM.run x s with
-     | .ok x s => .ok x s
-     | .error e s => .error (f e) s := by
-  simp only [EStateM.run, EStateM.adaptExcept]
-  cases (x s) <;> rfl
-
 instance : LawfulMonad (EStateM ε σ) := .mk'
   (id_map := fun x => funext <| fun s => by
-    simp only [Functor.map, EStateM.map]
+    dsimp only [EStateM.instMonad, EStateM.map]
     match x s with
     | .ok _ _ => rfl
     | .error _ _ => rfl)
   (pure_bind := fun _ _ => by rfl)
   (bind_assoc := fun x _ _ => funext <| fun s => by
-    simp only [bind, EStateM.bind]
+    dsimp only [EStateM.instMonad, EStateM.bind]
     match x s with
     | .ok _ _ => rfl
     | .error _ _ => rfl)

src/Init/Control/Lawful/Lemmas.lean

@@ -7,9 +7,7 @@ module
 
 prelude
 public import Init.Control.Lawful.Basic
-public import Init.Classical
-public import Init.Ext
-import Init.ByCases
+public import Init.ByCases
 
 public section
 

src/Init/Control/Lawful/MonadAttach/Instances.lean

@@ -6,17 +6,14 @@ Authors: Paul Reichert
 module
 
 prelude
+public import Init.Control.Reader
+public import Init.Control.Lawful.Instances
 import Init.Control.Lawful.MonadAttach.Lemmas
-public import Init.Control.Lawful.Basic
-public import Init.Control.State
-public import Init.Control.StateRef
-public import Init.Ext
 
 public instance [Monad m] [LawfulMonad m] [MonadAttach m] [WeaklyLawfulMonadAttach m] :
     WeaklyLawfulMonadAttach (ReaderT ρ m) where
   map_attach := by
-    simp only [Functor.map, MonadAttach.attach, Functor.map_map, WeaklyLawfulMonadAttach.map_attach,
-      MonadAttach.CanReturn]
+    simp only [Functor.map, MonadAttach.attach, Functor.map_map, WeaklyLawfulMonadAttach.map_attach]
     intros; rfl
 
 public instance [Monad m] [LawfulMonad m] [MonadAttach m] [LawfulMonadAttach m] :
@@ -31,7 +28,7 @@ public instance [Monad m] [LawfulMonad m] [MonadAttach m] [WeaklyLawfulMonadAtta
   map_attach := by
     intro α x
     simp only [Functor.map, StateT, funext_iff, StateT.map, bind_pure_comp, MonadAttach.attach,
-      Functor.map_map, MonadAttach.CanReturn]
+      Functor.map_map]
     exact fun s => WeaklyLawfulMonadAttach.map_attach
 
 public instance [Monad m] [LawfulMonad m] [MonadAttach m] [LawfulMonadAttach m] :
@@ -46,7 +43,7 @@ public instance [Monad m] [LawfulMonad m] [MonadAttach m] [LawfulMonadAttach m]
 public instance [Monad m] [LawfulMonad m] [MonadAttach m] [WeaklyLawfulMonadAttach m] :
     WeaklyLawfulMonadAttach (ExceptT ε m) where
   map_attach {α} x := by
-    simp only [Functor.map, MonadAttach.attach, ExceptT.map, MonadAttach.CanReturn]
+    simp only [Functor.map, MonadAttach.attach, ExceptT.map]
     simp
     conv => rhs; rw [← WeaklyLawfulMonadAttach.map_attach (m := m) (x := x)]
     simp only [map_eq_pure_bind]
@@ -84,6 +81,6 @@ attribute [local instance] MonadAttach.trivial
 
 public instance [Monad m] [LawfulMonad m] :
     WeaklyLawfulMonadAttach m where
-  map_attach := by simp [MonadAttach.attach, MonadAttach.CanReturn]
+  map_attach := by simp [MonadAttach.attach]
 
 end

src/Init/Control/Lawful/MonadAttach/Lemmas.lean

@@ -6,12 +6,10 @@ Authors: Paul Reichert
 module
 
 prelude
+public import Init.Control.MonadAttach
 import all Init.Control.MonadAttach
-public import Init.Classical
-public import Init.Control.Lawful.Basic
-public import Init.Control.Lawful.MonadLift.Basic
-import Init.Control.Lawful.MonadLift.Lemmas
-import Init.RCases
+public import Init.Control.Lawful.Lemmas
+public import Init.Control.Lawful.MonadLift.Lemmas
 
 public theorem LawfulMonadAttach.canReturn_bind_imp' [Monad m] [LawfulMonad m]
     [MonadAttach m] [LawfulMonadAttach m]

src/Init/Control/Lawful/MonadLift/Basic.lean

@@ -6,7 +6,7 @@ Authors: Quang Dao
 module
 
 prelude
-public import Init.Notation
+public import Init.Control.Basic
 
 public section
 

src/Init/Control/Lawful/MonadLift/Instances.lean

@@ -14,12 +14,8 @@ import all Init.Control.StateRef
 public import Init.Control.StateCps
 import all Init.Control.StateCps
 import all Init.Control.Id
-public import Init.Control.Lawful.MonadLift.Basic
-public import Init.Control.Option
-public import Init.Control.State
-public import Init.Control.StateRef
-import Init.Control.Lawful.Instances
-import Init.Control.Lawful.MonadLift.Lemmas
+public import Init.Control.Lawful.MonadLift.Lemmas
+public import Init.Control.Lawful.Instances
 
 public section
 
@@ -67,7 +63,7 @@ variable [Monad m] [LawfulMonad m]
 @[simp]
 theorem lift_bind {α β : Type u} (ma : m α) (f : α → m β) :
     OptionT.lift (ma >>= f) = OptionT.lift ma >>= (fun a => OptionT.lift (f a)) := by
-  simp only [bind, OptionT.bind, OptionT.mk, OptionT.lift, bind_pure_comp, bind_map_left,
+  simp only [instMonad, OptionT.bind, OptionT.mk, OptionT.lift, bind_pure_comp, bind_map_left,
     map_bind]
 
 instance : LawfulMonadLift m (OptionT m) where
@@ -83,7 +79,7 @@ variable [Monad m] [LawfulMonad m]
 @[simp]
 theorem lift_bind {α β ε : Type u} (ma : m α) (f : α → m β) :
     ExceptT.lift (ε := ε) (ma >>= f) = ExceptT.lift ma >>= (fun a => ExceptT.lift (f a)) := by
-  simp only [bind, ExceptT.bind, mk, ExceptT.lift, bind_map_left, ExceptT.bindCont, map_bind]
+  simp only [instMonad, ExceptT.bind, mk, ExceptT.lift, bind_map_left, ExceptT.bindCont, map_bind]
 
 instance : LawfulMonadLift m (ExceptT ε m) where
   monadLift_pure := lift_pure
@@ -93,7 +89,8 @@ instance : LawfulMonadLift (Except ε) (ExceptT ε m) where
   monadLift_pure _ := by
     simp only [MonadLift.monadLift, mk, pure, Except.pure, ExceptT.pure]
   monadLift_bind ma _ := by
-    simp only [bind, ExceptT.bind, mk, MonadLift.monadLift, pure_bind, ExceptT.bindCont, Except.bind]
+    simp only [instMonad, ExceptT.bind, mk, MonadLift.monadLift, pure_bind, ExceptT.bindCont,
+      Except.instMonad, Except.bind]
     rcases ma with _ | _ <;> simp
 
 end ExceptT

src/Init/Control/Lawful/MonadLift/Lemmas.lean

@@ -6,9 +6,9 @@ Authors: Quang Dao
 module
 
 prelude
+public import Init.Control.Id
 public import Init.Control.Lawful.Basic
 public import Init.Control.Lawful.MonadLift.Basic
-import Init.Ext
 
 public section
 
@@ -17,7 +17,7 @@ universe u v w
 theorem instMonadLiftTOfMonadLift_instMonadLiftTOfPure [Monad m] [Monad n] {_ : MonadLift m n}
     [LawfulMonadLift m n] : instMonadLiftTOfMonadLift Id m n = Id.instMonadLiftTOfPure := by
   have hext {a b : MonadLiftT Id n} (h : @a.monadLift = @b.monadLift) : a = b := by
-    cases a; cases b; simp [monadLift] at h; simp [h]
+    cases a <;> cases b <;> simp_all
   apply hext
   ext α x
   simp [monadLift, LawfulMonadLift.monadLift_pure]

src/Init/Control/MonadAttach.lean

@@ -6,7 +6,7 @@ Authors: Paul Reichert
 module
 
 prelude
-public import Init.Core
+public import Init.Control.Basic
 
 set_option linter.all true
 
@@ -70,7 +70,7 @@ information to the return value, except a trivial proof of {name}`True`.
 This instance is used whenever no more useful {name}`MonadAttach` instance can be implemented.
 It always has a {name}`WeaklyLawfulMonadAttach`, but usually no {name}`LawfulMonadAttach` instance.
 -/
-@[expose, implicit_reducible]
+@[expose]
 public protected def MonadAttach.trivial {m : Type u → Type v} [Monad m] : MonadAttach m where
   CanReturn _ _ := True
   attach x := (⟨·, .intro⟩) <$> x

src/Init/Control/Option.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Init.Data.Option.Basic
-public import Init.Control.MonadAttach
+public import Init.Control.Except
 
 public section
 

src/Init/Control/StateCps.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Init.Control.Lawful.Basic
-public import Init.Ext
 
 public section
 

src/Init/Control/StateRef.lean

@@ -9,7 +9,6 @@ module
 
 prelude
 public import Init.System.ST
-public import Init.Control.Reader
 
 public section