chore: document ugly workaround

This is a workaround to minimize the number of exported symbols.
See issues #466 and PR #515

.claude/CLAUDE.md

@@ -1,143 +0,0 @@
-(In the following, use `sysctl -n hw.logicalcpu` instead of `nproc` on macOS)
-
-## 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; double-quote special chars like |)
-CTEST_PARALLEL_LEVEL="$(nproc)" CTEST_OUTPUT_ON_FAILURE=1 \
-make -C build/release -j "$(nproc)" test ARGS="-R 'grind_ematch'"
-
-# Multiple tests matching a pattern
-CTEST_PARALLEL_LEVEL="$(nproc)" CTEST_OUTPUT_ON_FAILURE=1 \
-make -C build/release -j "$(nproc)" test ARGS="-R 'treemap|phashmap'"
-
-# Rerun only previously failed tests
-CTEST_PARALLEL_LEVEL="$(nproc)" CTEST_OUTPUT_ON_FAILURE=1 \
-make -C build/release -j "$(nproc)" test ARGS='--rerun-failed'
-
-# Run a test manually without ctest (test pile: pass filename relative to the pile dir)
-tests/with_stage1_test_env.sh tests/elab_bench/run_bench.sh cbv_decide.lean
-tests/with_stage1_test_env.sh tests/elab/run_test.sh grind_indexmap.lean
-```
-
-## Benchmark vs Test Problem Sizes
-
-Benchmarks are also run as tests. Use the `TEST_BENCH` environment variable (unset in tests, set to `1` in benchmarks) to scale problem sizes:
-
-- In `compile_bench` `.init.sh` files: check `$TEST_BENCH` and set `TEST_ARGS` accordingly
-- In `elab_bench` Lean files: use `(← IO.getEnv "TEST_BENCH") == some "1"` to switch between small (test) and large (bench) inputs
-
-See `tests/README.md` for the full benchmark writing guide.
-
-## 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.
-
-## New features
-
-When asked to implement new features:
-* begin by reviewing existing relevant code and tests
-* write comprehensive tests first (expecting that these will initially fail)
-* and then iterate on the implementation until the tests pass.
-
-## Success Criteria
-
-*Never* report success on a task unless you have verified both a clean build without errors, and that the relevant tests pass.
-
-## 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`
-- 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.
-
-## Update prompting when the user is frustrated
-
-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
-
-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.

.claude/commands/release.md

@@ -1,166 +0,0 @@
-# Release Management Command
-
-Execute the release process for a given version by running the release checklist and following its instructions.
-
-## Before Starting
-
-**IMPORTANT**: Before beginning the release process, read the in-file documentation:
-- Read `script/release_checklist.py` for what the checklist script does
-- Read `script/release_steps.py` for what the release steps script does
-
-These comments explain the scripts' behavior, which repositories get special handling, and how errors are handled.
-
-## 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
-   - **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**
-   - The checklist output will say "Run `script/release_steps.py {version} {repo_name}` to create it"
-   - If a repository shows "🟡 Dependencies not ready", you CANNOT create a PR for it yet
-   - You MUST rerun `release_checklist.py` before attempting to create PRs for any new repositories
-5. For each repository that the checklist says needs updating:
-   - Run `script/release_steps.py {version} {repo_name}` to create the PR
-   - Mark it complete when the PR is created
-6. After creating PRs, notify the user which PRs need review and merging
-7. **MANDATORY: Rerun `release_checklist.py` to check current status**
-   - Do this after creating each batch of PRs
-   - Do this after the user reports PRs have been merged
-   - NEVER assume a repository is ready without checking the checklist output
-8. As PRs are merged and tagged, dependent repositories will become ready
-9. Continue the cycle: run checklist → create PRs for ready repos → wait for merges → repeat
-10. Continue until all repositories are updated and the release is complete
-
-## Important Notes
-
-- **NEVER merge PRs autonomously** - always wait for the user to merge PRs themselves
-- The `release_steps.py` script is idempotent - it's safe to rerun
-- The `release_checklist.py` script is idempotent - it's safe to rerun
-- Some repositories depend on others (e.g., mathlib4 depends on batteries, aesop, etc.)
-- Wait for user to merge PRs before dependent repos can be updated
-- Alert user if anything unusual or scary happens
-- Use appropriate timeouts for long-running builds (verso can take 10+ minutes)
-- ProofWidgets4 uses semantic versioning (v0.0.X) - it's okay to create and push the next sequential tag yourself when needed for a release
-
-## PR Status Reporting
-
-Every time you run `release_checklist.py`, you MUST:
-1. Parse the output to identify ALL open PRs mentioned (lines with "✅ PR with title ... exists")
-2. Provide a summary to the user listing ALL open PRs that need review
-3. Group them by status:
-   - PRs for repositories that are blocked by dependencies (show these but note they're blocked)
-   - PRs for repositories that are ready to merge (highlight these)
-4. Format the summary clearly with PR numbers and URLs
-
-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:
-- **DO NOT** try to manually reproduce the failing steps yourself
-- **DO NOT** try to fix things by running git commands or other manual operations
-- Both scripts are idempotent and designed to handle partial completion gracefully
-- If a script continues to fail after retrying, report the error to the user and wait for instructions

.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

@@ -1,7 +1,3 @@
-*.lean text eol=lf
 *.expected.out -text
-RELEASES.md merge=union
+doc/changes.md merge=union
 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

.github/ISSUE_TEMPLATE.md

@@ -0,0 +1,30 @@
+### Prerequisites
+
+* [ ] Put an X between the brackets on this line if you have done all of the following:
+    * Checked that your issue isn't already [filed](https://github.com/leanprover/lean4/issues).
+    * Reduced the issue to a self-contained, reproducible test case.
+
+### Description
+
+[Description of the issue]
+
+### Steps to Reproduce
+
+1. [First Step]
+2. [Second Step]
+3. [and so on...]
+
+**Expected behavior:** [What you expect to happen]
+
+**Actual behavior:** [What actually happens]
+
+**Reproduces how often:** [What percentage of the time does it reproduce?]
+
+### Versions
+
+You can get this information from copy and pasting the output of `lean --version`,
+please include the OS and what version of the OS you're running.
+
+### Additional Information
+
+Any additional information, configuration or data that might be necessary to reproduce the issue.

.github/ISSUE_TEMPLATE/bug_report.md

@@ -1,51 +0,0 @@
----
-name: Bug report
-about: Create a bug report
-title: ''
-labels: bug
-assignees: ''
-
----
-
-### Prerequisites
-
-<!-- Please put an X between the brackets as you perform the following steps: -->
-
-* [ ] Check that your issue is not already filed:
-      https://github.com/leanprover/lean4/issues
-* [ ] Reduce the issue to a minimal, self-contained, reproducible test case.
-      Avoid dependencies to Mathlib or Batteries.
-* [ ] Test your test case against the latest nightly release, for example on
-      https://live.lean-lang.org/#project=lean-nightly
-      (You can also use the settings there to switch to “Lean nightly”)
-
-### Description
-
-[Clear and concise description of the issue]
-
-### Context
-
-[Broader context that the issue occurred in. If there was any prior discussion on [the Lean Zulip](https://leanprover.zulipchat.com), link it here as well.]
-
-### Steps to Reproduce
-
-1.
-2.
-3.
-
-**Expected behavior:** [Clear and concise description of what you expect to happen]
-
-**Actual behavior:** [Clear and concise description of what actually happens]
-
-### Versions
-
-[Output of `#version` or `#eval Lean.versionString`]
-[OS version, if not using live.lean-lang.org.]
-
-### Additional Information
-
-[Additional information, configuration or data that might be necessary to reproduce the issue]
-
-### Impact
-
-Add :+1: to [issues you consider important](https://github.com/leanprover/lean4/issues?q=is%3Aissue+is%3Aopen+sort%3Areactions-%2B1-desc). If others are impacted by this issue, please ask them to add :+1: to it.

.github/ISSUE_TEMPLATE/rfc.md

@@ -1,26 +0,0 @@
----
-name: Request for comments
-about: Create a feature proposal
-title: 'RFC: '
-labels: RFC
-assignees: ''
-
----
-
-### Proposal
-
-Clear and detailed description of the proposal. Consider the following questions:
-
-  - **User Experience**: How does this feature improve the user experience?
-
-  - **Beneficiaries**: Which Lean users and projects benefit most from this feature/change?
-
-  - **Maintainability**: Will this change streamline code maintenance or simplify its structure?
-
-### Community Feedback
-
-Ideas should be discussed on [the Lean Zulip](https://leanprover.zulipchat.com) prior to submitting a proposal. Summarize all prior discussions and link them here.
-
-### Impact
-
-Add :+1: to [issues you consider important](https://github.com/leanprover/lean4/issues?q=is%3Aissue+is%3Aopen+sort%3Areactions-%2B1-desc). If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.

.github/PULL_REQUEST_TEMPLATE.md

@@ -1,21 +0,0 @@
-# Read this section before submitting
-
-* Ensure your PR follows the [External Contribution Guidelines](https://github.com/leanprover/lean4/blob/master/CONTRIBUTING.md).
-* Please make sure the PR has excellent documentation and tests. If we label it `missing documentation` or `missing tests` then it needs fixing!
-* Include the link to your `RFC` or `bug` issue in the description.
-* If the issue does not already have approval from a developer, submit the PR as draft.
-* The PR title/description will become the commit message. Keep it up-to-date as the PR evolves.
-* For `feat/fix` PRs, the first paragraph starting with "This PR" must be present and will become a
-  changelog entry unless the PR is labeled with `no-changelog`. If the PR does not have this label,
-  it must instead be categorized with one of the `changelog-*` labels (which will be done by a
-  reviewer for external PRs).
-* A toolchain of the form `leanprover/lean4-pr-releases:pr-release-NNNN` for Linux and M-series Macs will be generated upon build. To generate binaries for Windows and Intel-based Macs as well, write a comment containing `release-ci` on its own line.
-* If you rebase your PR onto `nightly-with-mathlib` then CI will test Mathlib against your PR.
-* You can manage the `awaiting-review`, `awaiting-author`, and `WIP` labels yourself, by writing a comment containing one of these labels on its own line.
-* Remove this section, up to and including the `---` before submitting.
-
----
-
-This PR <short changelog summary for feat/fix, see above>.
-
-Closes <`RFC` or `bug` issue number fixed by this PR, if any>

.github/actionlint.yaml

@@ -1,5 +0,0 @@
-self-hosted-runner:
-  labels:
-    - nscloud-ubuntu-22.04-amd64-4x16
-    - nscloud-ubuntu-22.04-amd64-8x16
-    - nscloud-macos-sonoma-arm64-6x14

.github/dependabot.yml

@@ -1,8 +0,0 @@
-version: 2
-updates:
-  - package-ecosystem: "github-actions"
-    directory: "/"
-    schedule:
-      interval: "monthly"
-    commit-message:
-      prefix: "chore: CI"

.github/workflows/actionlint.yml

@@ -1,22 +0,0 @@
-name: Actionlint
-on:
-  push:
-    branches:
-      - 'master'
-    paths:
-      - '.github/**'
-  pull_request:
-    paths:
-      - '.github/**'
-  merge_group:
-
-jobs:
-  actionlint:
-    runs-on: ubuntu-latest
-    steps:
-    - name: Checkout
-      uses: actions/checkout@v6
-    - name: actionlint
-      uses: raven-actions/actionlint@v2
-      with:
-        pyflakes: false # we do not use python scripts

.github/workflows/awaiting-manual.yml

@@ -1,41 +0,0 @@
-name: Check awaiting-manual label
-
-on:
-  merge_group:
-  pull_request_target:
-    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'
-        uses: actions/github-script@v8
-        with:
-          script: |
-            const { labels, number: prNumber } = context.payload.pull_request;
-            const hasAwaiting = labels.some(label => label.name == "awaiting-manual");
-            const hasBreaks = labels.some(label => label.name == "breaks-manual");
-            const hasBuilds = labels.some(label => label.name == "builds-manual");
-
-            if (hasAwaiting && hasBreaks) {
-              core.setFailed('PR has both "awaiting-manual" and "breaks-manual" labels.');
-            } else if (hasAwaiting && !hasBreaks && !hasBuilds) {
-              core.info('PR is marked "awaiting-manual" but neither "breaks-manual" nor "builds-manual" labels are present.');
-              core.setOutput('awaiting', 'true');
-            }
-      
-      - name: Wait for manual compatibility
-        if: github.event_name == 'pull_request_target' && 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."
-          # Keep the job running indefinitely to show "in progress" status
-          while true; do
-            sleep 3600  # Sleep for 1 hour at a time
-          done

.github/workflows/awaiting-mathlib.yml

@@ -1,41 +0,0 @@
-name: Check awaiting-mathlib label
-
-on:
-  merge_group:
-  pull_request_target:
-    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'
-        uses: actions/github-script@v8
-        with:
-          script: |
-            const { labels, number: prNumber } = context.payload.pull_request;
-            const hasAwaiting = labels.some(label => label.name == "awaiting-mathlib");
-            const hasBreaks = labels.some(label => label.name == "breaks-mathlib");
-            const hasBuilds = labels.some(label => label.name == "builds-mathlib");
-
-            if (hasAwaiting && hasBreaks) {
-              core.setFailed('PR has both "awaiting-mathlib" and "breaks-mathlib" labels.');
-            } else if (hasAwaiting && !hasBreaks && !hasBuilds) {
-              core.info('PR is marked "awaiting-mathlib" but neither "breaks-mathlib" nor "builds-mathlib" labels are present.');
-              core.setOutput('awaiting', 'true');
-            }
-      
-      - name: Wait for mathlib compatibility
-        if: github.event_name == 'pull_request_target' && 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."
-          # Keep the job running indefinitely to show "in progress" status
-          while true; do
-            sleep 3600  # Sleep for 1 hour at a time
-          done

.github/workflows/backport.yml

@@ -1,26 +0,0 @@
-name: Backport
-on:
-  pull_request_target:
-    types:
-      - closed
-      - labeled
-
-jobs:
-  backport:
-    name: Backport
-    runs-on: ubuntu-latest
-    # Only react to merged PRs for security reasons.
-    # See https://docs.github.com/en/actions/using-workflows/events-that-trigger-workflows#pull_request_target.
-    if: >
-      github.event.pull_request.merged
-      && (
-        github.event.action == 'closed'
-        || (
-          github.event.action == 'labeled'
-          && contains(github.event.label.name, 'backport')
-        )
-      )
-    steps:
-      - uses: tibdex/backport@v2
-        with:
-          github_token: ${{ secrets.GITHUB_TOKEN }}

.github/workflows/build-template.yml

@@ -1,295 +0,0 @@
-# instantiated by ci.yml
-name: build-template
-on:
-  workflow_call:
-    inputs:
-      config:
-        type: string
-        required: true
-      nightly:
-        type: string
-        required: true
-      LEAN_VERSION_MAJOR:
-        type: string
-        required: true
-      LEAN_VERSION_MINOR:
-        type: string
-        required: true
-      LEAN_VERSION_PATCH:
-        type: string
-        required: true
-      LEAN_SPECIAL_VERSION_DESC:
-        type: string
-        required: true
-      RELEASE_TAG:
-        type: string
-        required: true
-
-jobs:
-  build:
-    if: github.event_name != 'schedule' || github.repository == 'leanprover/lean4'
-    strategy:
-      matrix:
-        include: ${{fromJson(inputs.config)}}
-      # complete all jobs
-      fail-fast: false
-    runs-on: ${{ endsWith(matrix.os, '-with-cache') && fromJSON(format('["{0}", "nscloud-git-mirror-5gb"]', matrix.os)) || matrix.os }}
-    defaults:
-      run:
-        shell: ${{ matrix.shell || 'nix develop -c bash -euxo pipefail {0}' }}
-    name: ${{ matrix.name }}
-    env:
-      # must be inside workspace
-      CCACHE_DIR: ${{ github.workspace }}/.ccache
-      CCACHE_COMPRESS: true
-      # current cache limit
-      CCACHE_MAXSIZE: 400M
-      # squelch error message about missing nixpkgs channel
-      NIX_BUILD_SHELL: bash
-      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
-    steps:
-      - name: Install Nix
-        uses: DeterminateSystems/nix-installer-action@main
-        if: runner.os == 'Linux' && !matrix.cmultilib
-      - name: Install MSYS2
-        uses: msys2/setup-msys2@v2
-        with:
-          msystem: clang64
-          # `:` means do not prefix with msystem
-          pacboy: "make: python: cmake clang ccache gmp libuv git: zip: unzip: diffutils: binutils: tree: zstd tar:"
-        if: runner.os == 'Windows'
-      - name: Install Brew Packages
-        run: |
-          brew install ccache tree zstd coreutils gmp libuv
-        if: runner.os == 'macOS'
-      - name: Checkout
-        uses: actions/checkout@v6
-        with:
-          # the default is to use a virtual merge commit between the PR and master: just use the PR
-          ref: ${{ github.event.pull_request.head.sha }}
-      - name: Open Nix shell once
-        run: true
-        if: runner.os == 'Linux'
-      # Do check out some CI-relevant files from virtual merge commit to accommodate CI changes on
-      # master (as the workflow files themselves are always taken from the merge)
-      # (needs to be after "Install *" to use the right shell)
-      - name: CI Merge Checkout
-        run: |
-          git fetch --depth=${{ matrix.name == 'Linux Lake (Cached)' && '10' || '1' }} origin ${{ github.sha }}
-          git checkout FETCH_HEAD flake.nix flake.lock script/prepare-* tests/elab/importStructure.lean
-        if: github.event_name == 'pull_request'
-      # (needs to be after "Checkout" so files don't get overridden)
-      - name: Setup emsdk
-        uses: mymindstorm/setup-emsdk@v14
-        with:
-          version: 3.1.44
-          actions-cache-folder: emsdk
-        if: matrix.wasm
-      - name: Install 32bit c libs
-        run: |
-          sudo dpkg --add-architecture i386
-          sudo apt-get update
-          sudo apt-get install -y gcc-multilib g++-multilib ccache libuv1-dev:i386 pkgconf:i386
-        if: matrix.cmultilib
-      - name: Restore Cache
-        id: restore-cache
-        uses: actions/cache/restore@v5
-        with:
-          # NOTE: must be in sync with `save` below and with `restore-cache` in `update-stage0.yml`
-          path: |
-            .ccache
-            ${{ matrix.name == 'Linux Lake' && 'build/stage1/**/*.trace
-            build/stage1/**/*.olean*
-            build/stage1/**/*.ilean
-            build/stage1/**/*.ir
-            build/stage1/**/*.c
-            build/stage1/**/*.c.o*' || '' }}
-          key: ${{ matrix.name }}-build-v4-${{ github.sha }}
-          # fall back to (latest) previous cache
-          restore-keys: |
-            ${{ matrix.name }}-build-v4
-      # open nix-shell once for initial setup
-      - name: Setup
-        run: |
-          ccache --zero-stats
-        if: runner.os == 'Linux'
-      - name: Set up env
-        run: |
-          echo "NPROC=$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4)" >> $GITHUB_ENV
-          if ! diff src/stdlib_flags.h stage0/src/stdlib_flags.h; then
-            echo "src/stdlib_flags.h and stage0/src/stdlib_flags.h differ, will test and pack stage 2"
-            echo "TARGET_STAGE=stage2" >> $GITHUB_ENV
-          else
-            echo "TARGET_STAGE=stage1" >> $GITHUB_ENV
-          fi
-      - name: Configure Build
-        run: |
-          ulimit -c unlimited  # coredumps
-          [ -d build ] || mkdir build
-          cd build
-          # arguments passed to `cmake`
-          OPTIONS=(-DLEAN_EXTRA_MAKE_OPTS=-DwarningAsError=true)
-          if [[ -n '${{ matrix.release }}' ]]; then
-            # this also enables githash embedding into stage 1 library, which prohibits reusing
-            # `.olean`s across commits, so we don't do it in the fast non-release CI
-            OPTIONS+=(-DCHECK_OLEAN_VERSION=ON)
-          fi
-          if [[ -n '${{ matrix.cross_target }}' ]]; then
-            # used by `prepare-llvm`
-            export EXTRA_FLAGS=--target=${{ matrix.cross_target }}
-            OPTIONS+=(-DLEAN_PLATFORM_TARGET=${{ matrix.cross_target }})
-          fi
-          if [[ -n '${{ matrix.prepare-llvm }}' ]]; then
-            wget -q ${{ matrix.llvm-url }}
-            PREPARE="$(${{ matrix.prepare-llvm }})"
-            if [ "$TARGET_STAGE" == "stage2" ]; then
-              cp -r stage1 stage2
-            fi
-            eval "OPTIONS+=($PREPARE)"
-          fi
-          if [[ -n '${{ matrix.release }}' && -n '${{ inputs.nightly }}' ]]; then
-            OPTIONS+=(-DLEAN_SPECIAL_VERSION_DESC=${{ inputs.nightly }})
-          fi
-          if [[ -n '${{ matrix.release }}' && -n '${{ inputs.RELEASE_TAG }}' ]]; then
-            OPTIONS+=(-DLEAN_VERSION_MAJOR=${{ inputs.LEAN_VERSION_MAJOR }})
-            OPTIONS+=(-DLEAN_VERSION_MINOR=${{ inputs.LEAN_VERSION_MINOR }})
-            OPTIONS+=(-DLEAN_VERSION_PATCH=${{ inputs.LEAN_VERSION_PATCH }})
-            OPTIONS+=(-DLEAN_VERSION_IS_RELEASE=1)
-            OPTIONS+=(-DLEAN_SPECIAL_VERSION_DESC=${{ inputs.LEAN_SPECIAL_VERSION_DESC }})
-          fi
-          # contortion to support empty OPTIONS with old macOS bash
-          cmake .. --preset ${{ matrix.CMAKE_PRESET || 'release' }} -B . ${{ matrix.CMAKE_OPTIONS }} ${OPTIONS[@]+"${OPTIONS[@]}"} -DLEAN_INSTALL_PREFIX=$PWD/..
-      - name: Build Stage 0 & Configure Stage 1
-        run: |
-          ulimit -c unlimited  # coredumps
-          time make -C build stage1-configure -j$NPROC
-      - name: Download Lake Cache
-        if: matrix.name == 'Linux Lake (Cached)'
-        run: |
-          cd src
-          ../build/stage0/bin/lake cache get --repo=${{ github.repository }}
-        timeout-minutes: 20 # prevent excessive hanging from network issues
-        continue-on-error: true
-      - name: Build Target Stage
-        run: |
-          ulimit -c unlimited  # coredumps
-          time make -C build $TARGET_STAGE -j$NPROC
-      # Should be done as early as possible and in particular *before* "Check rebootstrap" which
-      # changes the state of stage1/
-      - name: Save Cache
-        # 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
-        with:
-          # NOTE: must be in sync with `restore` above
-          path: |
-            .ccache
-            ${{ matrix.name == 'Linux Lake' && 'build/stage1/**/*.trace
-            build/stage1/**/*.olean*
-            build/stage1/**/*.ilean
-            build/stage1/**/*.ir
-            build/stage1/**/*.c
-            build/stage1/**/*.c.o*' || '' }}
-          key: ${{ steps.restore-cache.outputs.cache-primary-key }}
-      - name: Upload Lake Cache
-        # Caching on cancellation created some mysterious issues perhaps related to improper build
-        # shutdown. Also, since this needs access to secrets, it cannot be run on forks.
-        if: matrix.name == 'Linux Lake' && !cancelled() && (github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name == github.repository)
-        run: |
-          curl --version
-          cd src
-          time ../build/stage0/bin/lake build -o ../build/lake-mappings.jsonl
-          time ../build/stage0/bin/lake cache put ../build/lake-mappings.jsonl --repo=${{ github.repository }}
-        env:
-          LAKE_CACHE_KEY: ${{ secrets.LAKE_CACHE_KEY }}
-          LAKE_CACHE_ARTIFACT_ENDPOINT: ${{ vars.LAKE_CACHE_ENDPOINT }}/a1
-          LAKE_CACHE_REVISION_ENDPOINT: ${{ vars.LAKE_CACHE_ENDPOINT }}/r1
-        timeout-minutes: 20 # prevent excessive hanging from network issues
-        continue-on-error: true
-      - name: Install
-        run: |
-          make -C build/$TARGET_STAGE install
-      - name: Check Binaries
-        run: ${{ matrix.binary-check }} lean-*/bin/* || true
-      - name: Count binary symbols
-        run: |
-          for f in lean-*/bin/*; do
-            echo "$f: $(nm $f | grep " T " | wc -l) exported symbols"
-          done
-        if: matrix.name == 'Windows'
-      - name: List Install Tree
-        run: |
-          # omit contents of Init/, ...
-          tree --du -h lean-*-* | grep -E ' (Init|Lean|Lake|LICENSE|[a-z])'
-      - name: Pack
-        run: |
-          dir=$(echo lean-*-*)
-          mkdir pack
-          # high-compression tar.zst + zip for release, fast tar.zst otherwise
-          if [[ '${{ startsWith(github.ref, 'refs/tags/') && matrix.release }}' == true || -n '${{ inputs.nightly }}' || -n '${{ inputs.RELEASE_TAG }}' ]]; then
-            ${{ matrix.tar || 'tar' }} cf - $dir | zstd -T0 --no-progress -19 -o pack/$dir.tar.zst
-            zip -rq pack/$dir.zip $dir
-          else
-            ${{ matrix.tar || 'tar' }} cf - $dir | zstd -T0 --no-progress -o pack/$dir.tar.zst
-          fi
-      - uses: actions/upload-artifact@v5
-        if: matrix.release
-        with:
-          name: build-${{ matrix.name }}
-          path: pack/*
-      - name: Lean stats
-        run: |
-          build/$TARGET_STAGE/bin/lean --stats src/Lean.lean
-        if: ${{ !matrix.cross }}
-      - name: Test
-        id: test
-        run: |
-          ulimit -c unlimited  # coredumps
-          time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/$TARGET_STAGE -j$NPROC --output-junit test-results.xml ${{ matrix.CTEST_OPTIONS }}
-        if: matrix.test
-      - name: Test Summary
-        uses: test-summary/action@v2
-        with:
-          paths: build/${{ env.TARGET_STAGE }}/test-results.xml
-        # 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
-        if: (!matrix.cross) && steps.test.conclusion != 'skipped'
-      - name: Build Stage 2
-        run: |
-          make -C build -j$NPROC stage2
-        if: matrix.test-bench
-      - name: Check Stage 3
-        run: |
-          make -C build -j$NPROC check-stage3
-        if: matrix.check-stage3
-      - name: Test Benchmarks
-        run: |
-          cd tests
-          nix develop -c make -C ../build -j$NPROC bench
-        if: matrix.test-bench
-      - name: Check rebootstrap
-        run: |
-          set -e
-          # clean rebuild in case of Makefile changes/Lake does not detect uncommited stage 0
-          # changes yet
-          make -C build update-stage0
-          make -C build/stage1 clean-stdlib
-          time make -C build -j$NPROC
-          time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/stage1 -j$NPROC
-        if: matrix.check-rebootstrap
-      - name: CCache stats
-        if: always()
-        run: ccache -s
-      - name: Show stacktrace for coredumps
-        if: failure() && runner.os == 'Linux'
-        run: |
-          for c in $(find . -name core); do
-            progbin="$(file $c | sed "s/.*execfn: '\([^']*\)'.*/\1/")"
-            echo bt | $GDB/bin/gdb -q $progbin $c || true
-          done

.github/workflows/check-empty-pr.yml

@@ -1,29 +0,0 @@
-name: Check for empty PR
-
-on:
-  merge_group:
-  pull_request:
-
-jobs:
-  check-empty-pr:
-    runs-on: ubuntu-latest
-    steps:
-    - uses: actions/checkout@v6
-      with:
-        ref: ${{ github.event_name == 'pull_request' && github.event.pull_request.head.sha || github.sha }}
-        fetch-depth: 0
-        filter: tree:0
-
-    - name: Check for empty diff
-      run: |
-        if [[ "${{ github.event_name }}" == "pull_request" ]]; then
-          base=$(git merge-base "origin/${{ github.base_ref }}" HEAD)
-        else
-          base=$(git rev-parse HEAD^1)
-        fi
-        if git diff --quiet "$base" HEAD --; then
-          echo "This PR introduces no changes compared to its base branch." | tee "$GITHUB_STEP_SUMMARY"
-          echo "It may be a duplicate of an already-merged PR." | tee -a "$GITHUB_STEP_SUMMARY"
-          exit 1
-        fi
-      shell: bash

.github/workflows/check-prelude.yml

@@ -1,29 +0,0 @@
-name: Check for modules that should use `prelude`
-
-on: [pull_request]
-
-jobs:
-  check-prelude:
-    runs-on: ubuntu-latest
-    steps:
-      - name: Checkout
-        uses: actions/checkout@v6
-        with:
-          # the default is to use a virtual merge commit between the PR and master: just use the PR
-          ref: ${{ github.event.pull_request.head.sha }}
-          sparse-checkout: |
-            src/Lean
-            src/Std
-            src/lake/Lake
-      - name: Check Prelude
-        run: |
-          failed_files=""
-          while IFS= read -r -d '' file; do
-            if ! grep -q "^prelude$" "$file"; then
-              failed_files="$failed_files$file\n"
-            fi
-          done < <(find src/Lean src/Std src/lake/Lake -name '*.lean' -print0)
-          if [ -n "$failed_files" ]; then
-            echo -e "The following files should use 'prelude':\n$failed_files"
-            exit 1
-          fi

.github/workflows/check-stage0.yml

@@ -1,55 +0,0 @@
-name: Check for stage0 changes
-
-on:
-  merge_group:
-  pull_request:
-
-jobs:
-  check-stage0-on-queue:
-    runs-on: ubuntu-latest
-    steps:
-    - uses: actions/checkout@v6
-      with:
-        ref: ${{ github.event.pull_request.head.sha }}
-        fetch-depth: 0
-        filter: tree:0
-
-    - name: Find base commit
-      if: github.event_name == 'pull_request'
-      run: echo "BASE=$(git merge-base origin/${{ github.base_ref }} HEAD)" >> "$GITHUB_ENV"
-
-    - name: Identify stage0 changes
-      run: |
-        git diff "${BASE:-HEAD^}..HEAD" --name-only -- stage0/stdlib > "$RUNNER_TEMP/stage0" || true
-        if test -s "$RUNNER_TEMP/stage0"
-        then
-          echo "CHANGES=yes" >> "$GITHUB_ENV"
-        else
-          echo "CHANGES=no" >> "$GITHUB_ENV"
-        fi
-      shell: bash
-
-    - if: github.event_name == 'pull_request'
-      name: Set label
-      uses: actions/github-script@v8
-      with:
-        script: |
-          const { owner, repo, number: issue_number  } = context.issue;
-          if (process.env.CHANGES == 'yes') {
-            await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['changes-stage0'] }).catch(() => {});
-          } else {
-            await github.rest.issues.removeLabel({ owner, repo, issue_number, name: 'changes-stage0' }).catch(() => {});
-          }
-
-    - if: env.CHANGES == 'yes'
-      name: Report changes
-      run: |
-        echo "Found changes to stage0/, please do not merge using the merge queue." | tee "$GITHUB_STEP_SUMMARY"
-        # shellcheck disable=SC2129
-        echo '```'                  >> "$GITHUB_STEP_SUMMARY"
-        cat  "$RUNNER_TEMP/stage0"  >> "$GITHUB_STEP_SUMMARY"
-        echo '```'                  >> "$GITHUB_STEP_SUMMARY"
-
-    - if: github.event_name == 'merge_group' && env.CHANGES == 'yes'
-      name: Fail when on the merge queue
-      run: exit 1

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

@@ -1,60 +0,0 @@
-name: Check stdlib_flags.h modifications
-
-on:
-  pull_request_target:
-    types: [opened, synchronize, reopened, labeled, unlabeled]
-
-permissions:
-  pull-requests: read
-
-jobs:
-  check-stdlib-flags:
-    runs-on: ubuntu-latest
-    steps:
-      - name: Check if stdlib_flags.h was modified
-        uses: actions/github-script@v8
-        with:
-          script: |
-            // Get the list of files changed in this PR
-            const files = await github.paginate(
-              github.rest.pulls.listFiles,
-              {
-                owner: context.repo.owner,
-                repo: context.repo.repo,
-                pull_number: context.payload.pull_request.number,
-              }
-            );
-
-            // Check if stdlib_flags.h was modified
-            const stdlibFlagsModified = files.some(file =>
-              file.filename === 'src/stdlib_flags.h'
-            );
-
-            if (stdlibFlagsModified) {
-              console.log('src/stdlib_flags.h was modified in this PR');
-
-              // Check if the unlock label is present
-
-              const { data: pr } = await github.rest.pulls.get({
-                owner: context.repo.owner,
-                repo: context.repo.repo,
-                pull_number: context.issue.number,
-              });
-
-              const hasUnlockLabel = pr.labels.some(label =>
-                label.name === 'unlock-upstream-stdlib-flags'
-              );
-
-              if (!hasUnlockLabel) {
-                core.setFailed(
-                  'src/stdlib_flags.h was modified. This is likely a mistake. If you would like to change ' +
-                  'bootstrapping settings or request a stage0 update, you should modify stage0/src/stdlib_flags.h. ' +
-                  'If you really want to change src/stdlib_flags.h (which should be extremely rare), set the ' +
-                  'unlock-upstream-stdlib-flags label.'
-                );
-              } else {
-                console.log('Found unlock-upstream-stdlib-flags');
-              }
-            } else {
-              console.log('src/stdlib_flags.h was not modified');
-            }

.github/workflows/ci.yml

@@ -2,558 +2,194 @@ name: CI
 on:
   push:
     branches:
-      - 'master'
+      - master
     tags:
       - '*'
   pull_request:
-  merge_group:
+    branches:
+      - master
   schedule:
-    - cron: '0 7 * * *'  # 8AM CET/11PM PT
-  # for manual re-release of a nightly
-  workflow_dispatch:
-    inputs:
-      action:
-        description: 'Action'
-        required: true
-        default: 'release nightly'
-        type: choice
-        options:
-        - release nightly
-
-
-concurrency:
-  group: ${{ github.workflow }}-${{ github.ref }}-${{ github.event_name }}
-  cancel-in-progress: true
+    - cron: '0 0 * * *'
 
 jobs:
-
-  # This job determines various settings for the following CI runs; see the `outputs` for details
-  configure:
-    runs-on: ubuntu-latest
-    outputs:
-      # The build matrix, dynamically generated here
-      matrix: ${{ steps.set-matrix.outputs.matrix }}
-      # secondary build jobs that should not block the CI success/merge queue
-      matrix-secondary: ${{ steps.set-matrix.outputs.matrix-secondary }}
-      # Should we make a nightly release? If so, this output contains the lean version string, else it is empty
-      nightly: ${{ steps.set-nightly.outputs.nightly }}
-      # Should this be the CI for a tagged release?
-      # Yes only if a tag is pushed to the `leanprover` repository, and the tag is "v" followed by a valid semver.
-      # It sets `set-release.outputs.RELEASE_TAG` to the tag
-      # and sets `set-release.outputs.{LEAN_VERSION_MAJOR,LEAN_VERSION_MINOR,LEAN_VERSION_PATCH,LEAN_SPECIAL_VERSION_DESC}`
-      # to the semver components parsed via regex.
-      LEAN_VERSION_MAJOR: ${{ steps.set-release.outputs.LEAN_VERSION_MAJOR }}
-      LEAN_VERSION_MINOR: ${{ steps.set-release.outputs.LEAN_VERSION_MINOR }}
-      LEAN_VERSION_PATCH: ${{ steps.set-release.outputs.LEAN_VERSION_PATCH }}
-      LEAN_SPECIAL_VERSION_DESC: ${{ steps.set-release.outputs.LEAN_SPECIAL_VERSION_DESC }}
-      RELEASE_TAG: ${{ steps.set-release.outputs.RELEASE_TAG }}
-
+  Build:
+    # don't schedule nightlies on forks
+    if: github.event_name != 'schedule' || github.repository == 'leanprover/lean4'
+    runs-on: ${{ matrix.os }}
+    defaults:
+      run:
+        shell: ${{ matrix.shell || 'nix-shell --run "bash -euxo pipefail {0}"' }}
+    strategy:
+      matrix:
+        include:
+          # portable release build: link most libraries statically and use channel with older glibc (2.27; LLVM 7)
+          - name: Linux release
+            os: ubuntu-latest
+            release: true
+            CMAKE_OPTIONS: -DSTATIC=ON
+            shell: nix-shell --arg pkgs "import (fetchTarball \"channel:nixos-19.03\") {{}}" --argstr llvmPackages latest --run "bash -euxo pipefail {0}"
+          - name: Linux
+            os: ubuntu-latest
+            check-stage3: true
+            test-speedcenter: true
+          - name: Linux Debug
+            os: ubuntu-latest
+            CMAKE_OPTIONS: -DCMAKE_BUILD_TYPE=Debug
+          - name: Linux fsanitize
+            os: ubuntu-latest
+            # turn off custom allocator to make LSAN do its magic
+            CMAKE_OPTIONS: -DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address,undefined -DLEANC_EXTRA_FLAGS=-fsanitize=address,undefined -DSMALL_ALLOCATOR=OFF
+          - name: macOS
+            os: macos-latest
+            release: true
+            CMAKE_OPTIONS: -DSTATIC=ON
+          - name: Windows
+            os: windows-latest
+            release: true
+            shell: msys2 {0}
+            CMAKE_OPTIONS: -G "Unix Makefiles" -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++ -DSTATIC=ON
+      # complete all jobs
+      fail-fast: false
+    name: ${{ matrix.name }}
+    env:
+      # must be inside workspace
+      CCACHE_DIR: ${{ github.workspace }}/.ccache
+      CCACHE_COMPRESS: true
+      # current cache limit
+      CCACHE_MAXSIZE: 200M
     steps:
       - name: Checkout
-        uses: actions/checkout@v6
-        # 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
-        if: github.event_name == 'schedule' && github.repository == 'leanprover/lean4' || inputs.action == 'release nightly'
-        id: set-nightly
+        uses: actions/checkout@v2
+        with:
+          # interferes with lean4-nightly authentication
+          persist-credentials: false
+      - name: Install Nix
+        uses: cachix/install-nix-action@v12
+        with:
+          # used only for providing a more recent `bash` on macOS
+          nix_path: nixpkgs=channel:nixos-unstable
+        if: matrix.os != 'windows-latest'
+      - name: Install MSYS2
+        uses: msys2/setup-msys2@v2
+        with:
+          install: make python mingw-w64-x86_64-cmake mingw-w64-x86_64-clang mingw-w64-x86_64-ccache git diffutils
+        if: matrix.os == 'windows-latest'
+      - name: Cache
+        uses: actions/cache@v2
+        with:
+          path: .ccache
+          key: ${{ matrix.name }}-build-${{ github.sha }}
+          # fall back to (latest) previous cache
+          restore-keys: |
+            ${{ matrix.name }}-build
+      - name: Setup
         run: |
-          if [[ -n '${{ secrets.PUSH_NIGHTLY_TOKEN }}' ]]; then
+          # open nix-shell once for initial setup
+          true
+        if: matrix.os != 'windows-latest'
+      # remove problematic tests for sanitized build
+      - name: Pre build
+        run: rm tests/compiler/StackOverflow.lean tests/compiler/StackOverflowTask.lean
+        if: matrix.name == 'Linux fsanitize'
+      - name: Build
+        run: |
+          mkdir build
+          cd build
+          OPTIONS=
+          if [[ $GITHUB_EVENT_NAME == 'schedule' && -n '${{ matrix.release }}' && -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: retry today's nightly, or create a revision if it already exists
-              TODAY_NIGHTLY="nightly-$(date -u +%F)"
-              if git rev-parse "refs/tags/${TODAY_NIGHTLY}" >/dev/null 2>&1; then
-                # Today's nightly already exists, create a revision
-                REV=1
-                while git rev-parse "refs/tags/${TODAY_NIGHTLY}-rev${REV}" >/dev/null 2>&1; do
-                  REV=$((REV + 1))
-                done
-                LEAN_VERSION_STRING="${TODAY_NIGHTLY}-rev${REV}"
-              else
-                # Today's nightly doesn't exist yet (e.g. scheduled run failed), create it
-                LEAN_VERSION_STRING="${TODAY_NIGHTLY}"
-              fi
-              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
+            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
+              OPTIONS=-DLEAN_SPECIAL_VERSION_DESC=$LEAN_VERSION_STRING
+              echo "LEAN_VERSION_STRING=$LEAN_VERSION_STRING" >> $GITHUB_ENV
             fi
           fi
-
-      - name: Check for official release
-        if: startsWith(github.ref, 'refs/tags/') && github.repository == 'leanprover/lean4'
-        id: set-release
+          cmake .. ${{ matrix.CMAKE_OPTIONS }} $OPTIONS
+          make -j4
+      # de-Nix-ify binaries
+      - name: Patch
         run: |
-          TAG_NAME="${GITHUB_REF##*/}"
-
-          # From https://github.com/fsaintjacques/semver-tool/blob/master/src/semver
-
-          NAT='0|[1-9][0-9]*'
-          ALPHANUM='[0-9]*[A-Za-z-][0-9A-Za-z-]*'
-          IDENT="$NAT|$ALPHANUM"
-          FIELD='[0-9A-Za-z-]+'
-
-          SEMVER_REGEX="\
-          ^[vV]?\
-          ($NAT)\\.($NAT)\\.($NAT)\
-          (\\-(${IDENT})(\\.(${IDENT}))*)?\
-          (\\+${FIELD}(\\.${FIELD})*)?$"
-
-          if [[ ${TAG_NAME} =~ ${SEMVER_REGEX} ]]; then
-            echo "Tag ${TAG_NAME} matches SemVer regex, with groups ${BASH_REMATCH[1]} ${BASH_REMATCH[2]} ${BASH_REMATCH[3]} ${BASH_REMATCH[4]}"
-            {
-              echo "LEAN_VERSION_MAJOR=${BASH_REMATCH[1]}"
-              echo "LEAN_VERSION_MINOR=${BASH_REMATCH[2]}"
-              echo "LEAN_VERSION_PATCH=${BASH_REMATCH[3]}"
-              echo "LEAN_SPECIAL_VERSION_DESC=${BASH_REMATCH[4]##-}"
-              echo "RELEASE_TAG=$TAG_NAME"
-            } >> "$GITHUB_OUTPUT"
-          else
-            echo "Tag ${TAG_NAME} did not match SemVer regex."
-          fi
-
-      - name: Check for custom releases (e.g., not in the main lean repository)
-        if: startsWith(github.ref, 'refs/tags/') && github.repository != 'leanprover/lean4'
-        id: set-release-custom
+          for f in lean leanpkg; do
+            patchelf --set-interpreter /lib64/ld-linux-x86-64.so.2 --remove-rpath build/stage1/bin/$f
+          done
+        if: matrix.name == 'Linux release'
+      - name: Patch
         run: |
-          TAG_NAME="${GITHUB_REF##*/}"
-          echo "RELEASE_TAG=$TAG_NAME" >> "$GITHUB_OUTPUT"
-
-      - name: Validate CMakeLists.txt version matches tag
-        if: steps.set-release.outputs.RELEASE_TAG != ''
-        run: |
-          echo "Validating CMakeLists.txt version matches tag ${{ steps.set-release.outputs.RELEASE_TAG }}"
-
-          # Extract version values from CMakeLists.txt
-          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')
-
-          # Expected values from tag parsing
-          TAG_MAJOR="${{ steps.set-release.outputs.LEAN_VERSION_MAJOR }}"
-          TAG_MINOR="${{ steps.set-release.outputs.LEAN_VERSION_MINOR }}"
-          TAG_PATCH="${{ steps.set-release.outputs.LEAN_VERSION_PATCH }}"
-
-          ERRORS=""
-
-          if [[ "$CMAKE_MAJOR" != "$TAG_MAJOR" ]]; then
-            ERRORS+="LEAN_VERSION_MAJOR: expected $TAG_MAJOR, found $CMAKE_MAJOR\n"
-          fi
-          if [[ "$CMAKE_MINOR" != "$TAG_MINOR" ]]; then
-            ERRORS+="LEAN_VERSION_MINOR: expected $TAG_MINOR, found $CMAKE_MINOR\n"
-          fi
-          if [[ "$CMAKE_PATCH" != "$TAG_PATCH" ]]; then
-            ERRORS+="LEAN_VERSION_PATCH: expected $TAG_PATCH, found $CMAKE_PATCH\n"
-          fi
-          if [[ "$CMAKE_IS_RELEASE" != "1" ]]; then
-            ERRORS+="LEAN_VERSION_IS_RELEASE: expected 1, found $CMAKE_IS_RELEASE\n"
-          fi
-
-          if [[ -n "$ERRORS" ]]; then
-            echo "::error::Version mismatch between tag and src/CMakeLists.txt"
-            echo ""
-            echo "Tag ${{ steps.set-release.outputs.RELEASE_TAG }} expects version $TAG_MAJOR.$TAG_MINOR.$TAG_PATCH"
-            echo "But src/CMakeLists.txt has mismatched values:"
-            echo -e "$ERRORS"
-            echo ""
-            echo "Fix src/CMakeLists.txt, delete the tag, and re-tag."
-            exit 1
-          fi
-
-          echo "Version validation passed: $TAG_MAJOR.$TAG_MINOR.$TAG_PATCH"
-
-      # 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
-      - name: Set check level
-        id: set-level
-        # We do not use github.event.pull_request.labels.*.name here because
-        # re-running a run does not update that list, and we do want to be able to
-        # rerun the workflow run after setting the `release-ci`/`merge-ci` labels.
-        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
-          elif [[ -n "${{ steps.set-nightly.outputs.nightly }}" ]]; then
-            check_level=2
-          elif [[ "${{ github.event_name }}" != "pull_request" ]]; then
-            check_level=1
-          else
-            labels="$(gh api repos/${{ github.repository_owner }}/${{ github.event.repository.name }}/pulls/${{ github.event.pull_request.number }} --jq '.labels')"
-            if echo "$labels" | grep -q "release-ci"; then
-              check_level=3
-            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"
-        env:
-          GH_TOKEN: ${{ github.token }}
-
-      - name: Configure build matrix
-        id: set-matrix
-        uses: actions/github-script@v8
+          for f in lean leanpkg; do
+            for lib in $(otool -L build/stage1/bin/$f | tail -n +2 | cut -d' ' -f1); do
+              install_name_tool -change "$lib" "/usr/lib/$(basename $lib | sed 's/libc++\.1\.0/libc++.1/')" build/stage1/bin/$f
+            done
+          done
+        if: matrix.name == 'macOS'
+      - name: Pack
+        run: cd build/stage1; cpack
+      - uses: actions/upload-artifact@v2
         with:
-          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' }};
-            const isPr = "${{ github.event_name }}" == "pull_request";
-            const isPushToMaster = "${{ github.event_name }}" == "push" && "${{ github.ref_name }}" == "master";
-            let matrix = [
-              /* TODO: to be updated to new LLVM
-              {
-                "name": "Linux LLVM",
-                "os": "ubuntu-latest",
-                "release": false,
-                "enabled": level >= 2,
-                "test": true,
-                "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
-                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-linux-gnu.tar.zst",
-                "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
-                "binary-check": "ldd -v",
-                // foreign code may be linked against more recent glibc
-                // reverse-ffi needs to be updated to link to LLVM libraries
-                "CTEST_OPTIONS": "-E 'foreign|leanlaketest_reverse-ffi'",
-                "CMAKE_OPTIONS": "-DLLVM=ON -DLLVM_CONFIG=${GITHUB_WORKSPACE}/build/llvm-host/bin/llvm-config"
-              }, */
-              {
-                // portable release build: use channel with older glibc (2.26)
-                "name": "Linux release",
-                // usually not a bottleneck so make exclusive to `fast-ci`
-                "os": large && fast ? "nscloud-ubuntu-24.04-amd64-8x16-with-cache" : "ubuntu-latest",
-                "release": true,
-                // Special handling for release jobs. We want:
-                // 1. To run it in PRs so developers get PR toolchains (so secondary without tests is sufficient)
-                // 2. To skip it in merge queues as it takes longer than the
-                //    Linux lake build and adds little value in the merge queue
-                // 3. To run it in release (obviously)
-                // 4. To run it for pushes to master so that pushes to master have a Linux toolchain
-                //    available as an artifact for Grove to use.
-                "enabled": isPr || level != 1 || isPushToMaster,
-                "test": level >= 1,
-                "secondary": level == 0,
-                "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
-                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-linux-gnu.tar.zst",
-                "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
-                "binary-check": "ldd -v",
-                // foreign code may be linked against more recent glibc
-                "CTEST_OPTIONS": "-E 'foreign'",
-              },
-              {
-                "name": "Linux Lake",
-                "os": large ? "nscloud-ubuntu-24.04-amd64-8x16-with-cache" : "ubuntu-latest",
-                "enabled": true,
-                "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,
-                // We are not warning-free yet on all platforms, start here
-                "CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-Werror -DUSE_LAKE_CACHE=ON",
-              },
-              {
-                "name": "Linux Lake (Cached)",
-                "os": large ? "nscloud-ubuntu-24.04-amd64-8x16-with-cache" : "ubuntu-latest",
-                "enabled": true,
-                "check-rebootstrap": level >= 1,
-                "check-stage3": level >= 2,
-                "test": true,
-                "secondary": true,
-                // NOTE: `test-bench` currently seems to be broken on `ubuntu-latest`
-                "test-bench": large && level >= 2,
-                "CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-Werror -DUSE_LAKE_CACHE=ON",
-              },
-              {
-                "name": "Linux Reldebug",
-                "os": "ubuntu-latest",
-                "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-24.04-amd64-16x32-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/'"
-              },
-              {
-                "name": "macOS",
-                "os": "macos-15-intel",
-                "release": true,
-                "test": false,  // Tier 2 platform
-                "enabled": level >= 2,
-                "shell": "bash -euxo pipefail {0}",
-                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-apple-darwin.tar.zst",
-                "prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
-                "binary-check": "otool -L",
-                "tar": "gtar", // https://github.com/actions/runner-images/issues/2619
-                "CTEST_OPTIONS": "-E 'leanlaketest_hello'", // started failing from unpack
-              },
-              {
-                "name": "macOS aarch64",
-                // standard GH runner only comes with 7GB so use large runner if possible when running tests
-                "os": large && (fast || level >= 1) ? "nscloud-macos-sequoia-arm64-6x14" : "macos-15",
-                "CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-darwin_aarch64",
-                "release": true,
-                "shell": "bash -euxo pipefail {0}",
-                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-aarch64-apple-darwin.tar.zst",
-                "prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
-                "binary-check": "otool -L",
-                "tar": "gtar", // https://github.com/actions/runner-images/issues/2619
-                // See "Linux release" for release job levels; Grove is not a concern here
-                "enabled": isPr || level != 1,
-                "test": level >= 1,
-                "secondary": level == 0,
-              },
-              {
-                "name": "Windows",
-                "os": large && (fast || level >= 2) ? "namespace-profile-windows-amd64-4x16" : "windows-2022",
-                "release": true,
-                "enabled": level >= 2,
-                "test": true,
-                "shell": "msys2 {0}",
-                "CMAKE_OPTIONS": "-G \"Unix Makefiles\"",
-                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-w64-windows-gnu.tar.zst",
-                "prepare-llvm": "../script/prepare-llvm-mingw.sh lean-llvm*",
-                "binary-check": "ldd",
-              },
-              {
-                "name": "Linux aarch64",
-                "os": "nscloud-ubuntu-22.04-arm64-4x16",
-                "CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-linux_aarch64",
-                "release": true,
-                "enabled": level >= 2,
-                "test": true,
-                "shell": "nix develop .#oldGlibcAArch -c bash -euxo pipefail {0}",
-                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-aarch64-linux-gnu.tar.zst",
-                "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
-              },
-              // Started running out of memory building expensive modules, a 2GB heap is just not that much even before fragmentation
-              //{
-              //  "name": "Linux 32bit",
-              //  "os": "ubuntu-latest",
-              //  // Use 32bit on stage0 and stage1 to keep oleans compatible
-              //  "CMAKE_OPTIONS": "-DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_MMAP=OFF -DUSE_GMP=OFF -DLEAN_EXTRA_CXX_FLAGS='-m32' -DLEANC_OPTS='-m32' -DMMAP=OFF -DLEAN_INSTALL_SUFFIX=-linux_x86 -DCMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/ -DSTAGE0_CMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/ -DPKG_CONFIG_EXECUTABLE=/usr/bin/i386-linux-gnu-pkg-config",
-              //  "cmultilib": true,
-              //  "release": true,
-              //  "enabled": level >= 2,
-              //  "cross": true,
-              //  "shell": "bash -euxo pipefail {0}"
-              //}
-              // {
-              //   "name": "Web Assembly",
-              //   "os": "ubuntu-latest",
-              //   // Build a native 32bit binary in stage0 and use it to compile the oleans and the wasm build
-              //   "CMAKE_OPTIONS": "-DCMAKE_C_COMPILER_WORKS=1 -DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_CMAKE_CXX_COMPILER=clang++ -DSTAGE0_CMAKE_C_COMPILER=clang -DSTAGE0_CMAKE_EXECUTABLE_SUFFIX=\"\" -DUSE_GMP=OFF -DMMAP=OFF -DSTAGE0_MMAP=OFF -DCMAKE_AR=../emsdk/emsdk-main/upstream/emscripten/emar -DCMAKE_TOOLCHAIN_FILE=../emsdk/emsdk-main/upstream/emscripten/cmake/Modules/Platform/Emscripten.cmake -DLEAN_INSTALL_SUFFIX=-linux_wasm32 -DSTAGE0_CMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/",
-              //   "wasm": true,
-              //   "cmultilib": true,
-              //   "release": true,
-              //   "enabled": level >= 2,
-              //   "cross": true,
-              //   "shell": "bash -euxo pipefail {0}",
-              //   // Just a few selected tests because wasm is slow
-              //   "CTEST_OPTIONS": "-R \"leantest_1007\\.lean|leantest_Format\\.lean|leanruntest\\_1037.lean|leanruntest_ac_rfl\\.lean|leanruntest_tempfile.lean\\.|leanruntest_libuv\\.lean\""
-              // }
-            ];
-            for (const job of matrix) {
-              if (job["prepare-llvm"]) {
-                // `USE_LAKE` is not compatible with `prepare-llvm` currently
-                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"]));
-            core.setOutput('matrix-secondary', matrix.filter((job) => job["secondary"]));
-
-  build:
-    if: github.event_name != 'schedule' || github.repository == 'leanprover/lean4'
-    needs: [configure]
-    uses: ./.github/workflows/build-template.yml
-    with:
-      config: ${{needs.configure.outputs.matrix}}
-      nightly: ${{ needs.configure.outputs.nightly }}
-      LEAN_VERSION_MAJOR: ${{ needs.configure.outputs.LEAN_VERSION_MAJOR }}
-      LEAN_VERSION_MINOR: ${{ needs.configure.outputs.LEAN_VERSION_MINOR }}
-      LEAN_VERSION_PATCH: ${{ needs.configure.outputs.LEAN_VERSION_PATCH }}
-      LEAN_SPECIAL_VERSION_DESC: ${{ needs.configure.outputs.LEAN_SPECIAL_VERSION_DESC }}
-      RELEASE_TAG: ${{ needs.configure.outputs.RELEASE_TAG }}
-    secrets: inherit
-
-  # build jobs that should not be considered by `all-done` below
-  build-secondary:
-    needs: [configure]
-    if: needs.configure.outputs.matrix-secondary != '[]'
-    uses: ./.github/workflows/build-template.yml
-    with:
-      config: ${{needs.configure.outputs.matrix-secondary}}
-      nightly: ${{ needs.configure.outputs.nightly }}
-      LEAN_VERSION_MAJOR: ${{ needs.configure.outputs.LEAN_VERSION_MAJOR }}
-      LEAN_VERSION_MINOR: ${{ needs.configure.outputs.LEAN_VERSION_MINOR }}
-      LEAN_VERSION_PATCH: ${{ needs.configure.outputs.LEAN_VERSION_PATCH }}
-      LEAN_SPECIAL_VERSION_DESC: ${{ needs.configure.outputs.LEAN_SPECIAL_VERSION_DESC }}
-      RELEASE_TAG: ${{ needs.configure.outputs.RELEASE_TAG }}
-    secrets: inherit
-
-  # This job collects results from all the matrix jobs
-  # This can be made the "required" job, instead of listing each
-  # matrix job separately
-  all-done:
-    name: Build matrix complete
-    runs-on: ubuntu-latest
-    needs: build
-    # mark as merely cancelled not failed if builds are cancelled
-    if: ${{ !cancelled() }}
-    steps:
-    - if: ${{ contains(needs.*.result, 'failure') && github.repository == 'leanprover/lean4' && github.ref_name == 'master' }}
-      uses: zulip/github-actions-zulip/send-message@v1
-      with:
-        api-key: ${{ secrets.ZULIP_BOT_KEY }}
-        email: "github-actions-bot@lean-fro.zulipchat.com"
-        organization-url: "https://lean-fro.zulipchat.com"
-        to: "infrastructure"
-        topic: "Github actions"
-        type: "stream"
-        content: |
-          A build of `${{ github.ref_name }}`, triggered by event `${{ github.event_name }}`, [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}).
-    - if: contains(needs.*.result, 'failure')
-      uses: actions/github-script@v8
-      with:
-        script: |
-            core.setFailed('Some jobs failed')
-
-
-  # This job creates releases from tags
-  # (whether they are "unofficial" releases for experiments, or official releases when the tag is "v" followed by a semver string.)
-  release:
-    if: startsWith(github.ref, 'refs/tags/')
-    runs-on: ubuntu-latest
-    needs: build
-    steps:
-      - uses: actions/download-artifact@v7
-        with:
-          path: artifacts
+          name: build-${{ matrix.name }}
+          path: build/stage1/lean-*
+      - name: Test
+        run: |
+          cd build/stage1
+          ctest -j4 --output-on-failure < /dev/null
+      - name: Build Stage 2
+        run: |
+          cd build
+          make -j4 stage2
+        if: matrix.build-stage2 || matrix.check-stage3
+      - name: Check Stage 3
+        run: |
+          cd build
+          make -j4 check-stage3
+        if: matrix.check-stage3
+      - name: Test Speedcenter Benchmarks
+        run: |
+          echo -1 | sudo tee /proc/sys/kernel/perf_event_paranoid
+          export BUILD=$PWD/build PATH=$PWD/build/stage1/bin:$PATH
+          cd tests/bench; temci exec --config speedcenter.yaml --included_blocks fast --runs 1
+        if: matrix.test-speedcenter
+      - name: Check rebootstrap
+        run: |
+          cd build
+          make update-stage0 && make -j4
+        if: matrix.name == 'Linux'
+      - name: CCache stats
+        run: ccache -s
       - name: Release
-        uses: softprops/action-gh-release@a06a81a03ee405af7f2048a818ed3f03bbf83c7b
+        uses: softprops/action-gh-release@v1
+        if: ${{ startsWith(github.ref, 'refs/tags/v') && matrix.release }}
         with:
-          files: artifacts/*/*
-          fail_on_unmatched_files: true
-          prerelease: ${{ !startsWith(github.ref, 'refs/tags/v') || contains(github.ref, '-rc') }}
+          files: build/stage1/lean-*
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-      - name: Update release.lean-lang.org
-        run: |
-          gh workflow -R leanprover/release-index run update-index.yml
-        env:
-          GITHUB_TOKEN: ${{ secrets.RELEASE_INDEX_TOKEN }}
-
-  # This job creates nightly releases during the cron job.
-  # It is responsible for creating the tag, and automatically generating a changelog.
-  release-nightly:
-    needs: [configure, build]
-    if: needs.configure.outputs.nightly
-    runs-on: ubuntu-latest
-    steps:
-      - name: Checkout
-        uses: actions/checkout@v6
-        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
-        with:
-          path: artifacts
       - name: Prepare Nightly Release
+        if: env.LEAN_VERSION_STRING
         run: |
-          git remote add nightly https://foo:'${{ secrets.PUSH_NIGHTLY_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-nightly.git
+          # can't push shallow checkout
+          git fetch --unshallow
           git fetch nightly --tags
-          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)"
-          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
-          diff --changed-group-format='%>' --unchanged-group-format='' old.md RELEASES.md >> diff.md || true
-          echo -e "\n*Full commit log*\n" >> diff.md
-          git log --oneline "$last_tag"..HEAD | sed 's/^/* /' >> diff.md
+          if git tag $LEAN_VERSION_STRING && git push nightly $LEAN_VERSION_STRING; then
+            last_tag=$(git describe HEAD^ --abbrev=0 --tags)
+            echo -e "Changes since ${last_tag}:\n\n" > diff.md
+            #git show $last_tag:doc/changes.md > old.md
+            #./script/diff_changelogs.py old.md doc/changes.md >> diff.md
+            echo -e "*Full commit log*\n" >> diff.md
+            git log --oneline $last_tag..HEAD | sed 's/^/* /' >> diff.md
+          else
+            # make sure every runner is building the same commit
+            [ $(git rev-parse HEAD) == $(git rev-parse $LEAN_VERSION_STRING) ] || exit 11
+            echo -n > diff.md
+          fi
       - name: Release Nightly
-        uses: softprops/action-gh-release@a06a81a03ee405af7f2048a818ed3f03bbf83c7b
+        # need unreleased version for fixed `repository`
+        uses: Kha/action-gh-release@master
+        if: env.LEAN_VERSION_STRING
         with:
           body_path: diff.md
           prerelease: true
-          files: artifacts/*/*
-          fail_on_unmatched_files: true
-          tag_name: ${{ needs.configure.outputs.nightly }}
+          files: build/stage1/lean-*
+          tag_name: ${{ env.LEAN_VERSION_STRING }}
           repository: ${{ github.repository_owner }}/lean4-nightly
         env:
           GITHUB_TOKEN: ${{ secrets.PUSH_NIGHTLY_TOKEN }}
-      - name: Update release.lean-lang.org
-        run: |
-          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
-        env:
-          GITHUB_TOKEN: ${{ steps.mathlib-app-token.outputs.token }}

.github/workflows/copyright-header.yml

@@ -1,20 +0,0 @@
-name: Check for copyright header
-
-on: [pull_request]
-
-jobs:
-  check-lean-files:
-    runs-on: ubuntu-latest
-    steps:
-    - uses: actions/checkout@v6
-
-    - name: Verify .lean files start with a copyright header.
-      run: |
-        FILES=$(find ./src -type d \( -path "./src/lake/examples" -o -path "./src/lake/tests" \) -prune -o -type f -name "*.lean" -exec perl -ne 'BEGIN { $/ = undef; } print "$ARGV\n" if !m{\A/-\nCopyright}; exit;' {} \;)
-        if [ -n "$FILES" ]; then
-          echo "Found .lean files which do not have a copyright header:"
-          echo "$FILES"
-          exit 1
-        else
-          echo "All copyright headers present."
-        fi

.github/workflows/grove.yml

@@ -1,162 +0,0 @@
-name: Grove
-
-on:
-  workflow_run: # https://docs.github.com/en/actions/using-workflows/events-that-trigger-workflows#workflow_run
-    workflows: [CI]
-    types: [completed]
-
-permissions:
-  pull-requests: write
-
-jobs:
-  grove-build:
-    runs-on: ubuntu-latest
-    if: github.event.workflow_run.conclusion == 'success' && 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
-        # This action is deprecated and archived, but it seems hard to find a
-        # better solution for getting the PR number
-        # see https://github.com/orgs/community/discussions/25220 for some discussion
-        id: workflow-info
-        with:
-          token: ${{ secrets.GITHUB_TOKEN }}
-          sourceRunId: ${{ github.event.workflow_run.id }}
-
-      - name: Check if should run
-        id: should-run
-        run: |
-          # Check if it's a push to master (no PR number and target branch is master)
-          if [ -z "${{ steps.workflow-info.outputs.pullRequestNumber }}" ]; then
-            if [ "${{ github.event.workflow_run.head_branch }}" = "master" ]; then
-              echo "Push to master detected. Running Grove."
-              echo "should-run=true" >> "$GITHUB_OUTPUT"
-            else
-              echo "Push to non-master branch, skipping"
-              echo "should-run=false" >> "$GITHUB_OUTPUT"
-            fi
-          else
-            # Check if it's a PR with grove label
-            PR_LABELS='${{ steps.workflow-info.outputs.pullRequestLabels }}'
-            if echo "$PR_LABELS" | grep -q '"grove"'; then
-              echo "PR with grove label detected. Running Grove."
-              echo "should-run=true" >> "$GITHUB_OUTPUT"
-            else
-              echo "PR without grove label, skipping"
-              echo "should-run=false" >> "$GITHUB_OUTPUT"
-            fi
-          fi
-
-      - name: Fetch upstream invalidated facts
-        if: ${{ steps.should-run.outputs.should-run == 'true' && steps.workflow-info.outputs.pullRequestNumber != '' }}
-        id: fetch-upstream
-        uses: TwoFx/grove-action/fetch-upstream@v0.5
-        with:
-          artifact-name: grove-invalidated-facts
-          base-ref: master
-
-      - name: Download toolchain for this commit
-        if: ${{ steps.should-run.outputs.should-run == 'true' }}
-        id: download-toolchain
-        uses: dawidd6/action-download-artifact@v11
-        with:
-          commit: ${{ steps.workflow-info.outputs.sourceHeadSha }}
-          workflow: ci.yml
-          path: artifacts
-          name: "build-Linux release"
-          allow_forks: true
-          name_is_regexp: true
-
-      - name: Unpack toolchain
-        if: ${{ steps.should-run.outputs.should-run == 'true' }}
-        id: unpack-toolchain
-        run: |
-          cd artifacts
-          # Find the tar.zst file
-          TAR_FILE=$(find . -name "lean-*.tar.zst" -type f | head -1)
-          if [ -z "$TAR_FILE" ]; then
-            echo "Error: No lean-*.tar.zst file found"
-            exit 1
-          fi
-          echo "Found archive: $TAR_FILE"
-
-          # Extract the archive
-          tar --zstd -xf "$TAR_FILE"
-
-          # Find the extracted directory name
-          LEAN_DIR=$(find . -maxdepth 1 -name "lean-*" -type d | head -1)
-          if [ -z "$LEAN_DIR" ]; then
-            echo "Error: No lean-* directory found after extraction"
-            exit 1
-          fi
-          echo "Extracted directory: $LEAN_DIR"
-          echo "lean-dir=$LEAN_DIR" >> "$GITHUB_OUTPUT"
-
-      - name: Build
-        if: ${{ steps.should-run.outputs.should-run == 'true' }}
-        id: build
-        uses: TwoFx/grove-action/build@v0.5
-        with:
-          project-path: doc/std/grove
-          script-name: grove-stdlib
-          invalidated-facts-artifact-name: grove-invalidated-facts
-          comment-artifact-name: grove-comment
-          toolchain-id: lean4
-          toolchain-path: artifacts/${{ steps.unpack-toolchain.outputs.lean-dir }}
-          project-ref: ${{ steps.workflow-info.outputs.sourceHeadSha }}
-
-      # deploy-alias computes a URL component for the PR preview. This
-      # is so we can have a stable name to use for feedback on draft
-      # material.
-      - id: deploy-alias
-        if: ${{ steps.should-run.outputs.should-run == 'true' }}
-        uses: actions/github-script@v8
-        name: Compute Alias
-        with:
-          result-encoding: string
-          script: |
-            if (process.env.PR) {
-                return `pr-${process.env.PR}`
-            } else {
-                return 'deploy-preview-main';
-            }
-        env:
-          PR: ${{ steps.workflow-info.outputs.pullRequestNumber }}
-
-      - name: Deploy to Netlify
-        if: ${{ steps.should-run.outputs.should-run == 'true' }}
-        id: deploy-draft
-        uses: nwtgck/actions-netlify@v3.0
-        with:
-          publish-dir: ${{ steps.build.outputs.out-path }}
-          production-deploy: false
-          github-token: ${{ secrets.GITHUB_TOKEN }}
-          alias: ${{ steps.deploy-alias.outputs.result }}
-          enable-commit-comment: false
-          enable-pull-request-comment: false
-          fails-without-credentials: true
-          enable-github-deployment: false
-          enable-commit-status: false
-        env:
-          NETLIFY_AUTH_TOKEN: ${{ secrets.NETLIFY_AUTH_TOKEN }}
-          NETLIFY_SITE_ID: "1cacfa39-a11c-467c-99e7-2e01d7b4089e"
-
-      # actions-netlify cannot add deploy links to a PR because it assumes a
-      # pull_request context, not a workflow_run context, see
-      # https://github.com/nwtgck/actions-netlify/issues/545
-      # We work around by using a comment to post the latest link
-      - name: "Comment on PR with preview links"
-        uses: marocchino/sticky-pull-request-comment@v2
-        if: ${{ steps.should-run.outputs.should-run == 'true' && steps.workflow-info.outputs.pullRequestNumber != '' }}
-        with:
-          number: ${{ env.PR_NUMBER }}
-          header: preview-comment
-          recreate: true
-          message: |
-            [Grove](${{ steps.deploy-draft.outputs.deploy-url }}) for revision ${{ steps.workflow-info.outputs.sourceHeadSha }}.
-
-            ${{ steps.build.outputs.comment-text }}
-        env:
-          PR_NUMBER: ${{ steps.workflow-info.outputs.pullRequestNumber }}
-          PR_HEADSHA: ${{ steps.workflow-info.outputs.sourceHeadSha }}

.github/workflows/jira.yml

@@ -1,34 +0,0 @@
-name: Jira sync
-
-on:
-  issues:
-    types: [closed]
-
-jobs:
-  jira-sync:
-    runs-on: ubuntu-latest
-
-    steps:
-      - name: Move Jira issue to Done
-        env:
-          JIRA_API_TOKEN: ${{ secrets.JIRA_API_TOKEN }}
-          JIRA_USERNAME: ${{ secrets.JIRA_USERNAME }}
-          JIRA_BASE_URL: ${{ secrets.JIRA_BASE_URL }}
-        run: |
-          issue_number=${{ github.event.issue.number }}
-
-          jira_issue_key=$(curl -s -u "${JIRA_USERNAME}:${JIRA_API_TOKEN}" \
-            -X GET -H "Content-Type: application/json" \
-            "${JIRA_BASE_URL}/rest/api/2/search?jql=summary~\"${issue_number}\"" | \
-            jq -r '.issues[0].key')
-
-          if [ -z "$jira_issue_key" ]; then
-            exit
-          fi
-
-          curl -s -u "${JIRA_USERNAME}:${JIRA_API_TOKEN}" \
-            -X POST -H "Content-Type: application/json" \
-            --data "{\"transition\": {\"id\": \"41\"}}" \
-            "${JIRA_BASE_URL}/rest/api/2/issue/${jira_issue_key}/transitions"
-
-          echo "Moved Jira issue ${jira_issue_key} to Done"

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

@@ -1,71 +0,0 @@
-# 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.
-# 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.
-
-name: Label PR based on Comment
-
-on:
-  issue_comment:
-    types: [created]
-
-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-'))
-    runs-on: ubuntu-latest
-
-    steps:
-    - name: Add label based on comment
-      uses: actions/github-script@v8
-      with:
-        github-token: ${{ secrets.GITHUB_TOKEN }}
-        script: |
-          const { owner, repo, number: issue_number } = context.issue;
-          const commentLines = context.payload.comment.body.split('\r\n');
-
-          const awaitingReview = commentLines.includes('awaiting-review');
-          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) {
-            await github.rest.issues.removeLabel({ owner, repo, issue_number, name: 'awaiting-review' }).catch(() => {});
-            await github.rest.issues.removeLabel({ owner, repo, issue_number, name: 'awaiting-author' }).catch(() => {});
-            await github.rest.issues.removeLabel({ owner, repo, issue_number, name: 'WIP' }).catch(() => {});
-          }
-
-          if (awaitingReview) {
-            await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['awaiting-review'] });
-          }
-          if (awaitingAuthor) {
-            await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['awaiting-author'] });
-          }
-          if (wip) {
-            await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['WIP'] });
-          }
-
-          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();
-            const { data: existingLabels } = await github.rest.issues.listLabelsOnIssue({ owner, repo, issue_number });
-            const changelogLabels = existingLabels.filter(label => label.name.startsWith('changelog-'));
-
-            // Remove all other changelog labels
-            for (const label of changelogLabels) {
-              if (label.name !== changelogLabel) {
-                await github.rest.issues.removeLabel({ owner, repo, issue_number, name: label.name }).catch(() => {});
-              }
-            }
-
-            // Add the new changelog label
-            await github.rest.issues.addLabels({ owner, repo, issue_number, labels: [changelogLabel] });
-          }

.github/workflows/nix-ci.yml

@@ -0,0 +1,102 @@
+name: Nix CI
+on:
+  push:
+    branches:
+      - master
+    tags:
+      - '*'
+  pull_request:
+    branches:
+      - master
+
+jobs:
+  Build:
+    runs-on: ${{ matrix.os }}
+    defaults:
+      run:
+        # Can't use `nix-shell` without configured nixpkgs path on macOS
+        shell: nix -v --experimental-features "nix-command flakes" run .#ciShell -- bash -euxo pipefail {0}
+    strategy:
+      matrix:
+        include:
+          - name: Linux
+            os: ubuntu-latest
+            # latest builds on https://hydra.nixos.org/jobset/nix/master/all at the time
+            nix_url: https://hydra.nixos.org/build/135773533/download/1/nix-2.4pre20210125_36c4d6f-x86_64-linux.tar.xz
+          - name: macOS
+            os: macos-latest
+            nix_url: https://hydra.nixos.org/build/135773542/download/1/nix-2.4pre20210125_36c4d6f-x86_64-darwin.tar.xz
+      # complete all jobs
+      fail-fast: false
+    name: ${{ matrix.name }}
+    env:
+      NIX_BUILD_ARGS: -v --print-build-logs --fallback
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v2
+      # Install flakes-enabled Nix manually from Hydra since `install-nix-action` doesn't accept raw tarballs
+      - name: Install Nix
+        shell: bash -euo pipefail {0}
+        run: |
+          curl ${{ matrix.nix_url }} | tar -xJ
+          # Do a single-user install so actions/cache doesn't get confused about permissions
+          nix-*/install --no-daemon --no-channel-add --darwin-use-unencrypted-nix-store-volume
+          rm -rf nix-*
+      # Call `install-nix-action` anyways to run its Actions-specific setup
+      - name: Setup Nix
+        uses: cachix/install-nix-action@v12
+      - name: Fixup install-nix-action
+        shell: bash -euo pipefail {0}
+        run: |
+          # the path set by install-nix-action is valid only for multi-user installations
+          echo "NIX_SSL_CERT_FILE=$HOME/.nix-profile/etc/ssl/certs/ca-bundle.crt" > $GITHUB_ENV
+        if: matrix.name == 'macOS'
+      - name: Further setup Nix
+        run: |
+          mkdir -p ~/.config/nix
+          echo '
+            max-jobs = auto
+            extra-sandbox-paths = /nix/var/cache/ccache
+            extra-trusted-substituters = https://lean4.cachix.org/
+            extra-trusted-public-keys = lean4.cachix.org-1:mawtxSxcaiWE24xCXXgh3qnvlTkyU7evRRnGeAhD4Wk=' > ~/.config/nix/nix.conf
+          sudo mkdir -m0770 -p /nix/var/cache/ccache
+          # macOS standard chown doesn't support --reference
+          nix shell .#nixpkgs.coreutils -c sudo chown --reference=/nix /nix/var/cache/ccache
+          echo 'max_size = 50M' > /nix/var/cache/ccache/ccache.conf
+
+          # install & use Cachix manually since `cachix-action` pushes *all* derivations (incl. `$mod-deps`, stage 2&3, etc.)
+          nix-env -iA cachix -f https://cachix.org/api/v1/install
+      - name: Setup CCache Cache
+        uses: actions/cache@v2
+        with:
+          path: /nix/var/cache/ccache
+          key: ${{ matrix.name }}-nix-ccache-${{ github.sha }}
+          # fall back to (latest) previous cache
+          restore-keys: |
+            ${{ matrix.name }}-nix-ccache
+      - name: Build
+        run: |
+          # .o files are not a runtime dependency on macOS because of lack of thin archives
+          nix build $NIX_BUILD_ARGS .#stage0 .#stage1 .#Lean.oTree -o push-build
+      - name: Test
+        run: |
+          nix build $NIX_BUILD_ARGS .#test -o push-test
+      - name: Build manual
+        run: |
+          nix build $NIX_BUILD_ARGS .#mdbook .#doc-test -o push-doc
+          nix build $NIX_BUILD_ARGS .#doc
+        if: matrix.name == 'Linux'
+      - name: Push to Cachix
+        run: |
+          [ -z "$CACHIX_AUTH_TOKEN" ] || cachix push -j4 lean4 ./push-* || true
+        env:
+          CACHIX_AUTH_TOKEN: '${{ secrets.CACHIX_AUTH_TOKEN }}'
+      - name: Publish manual
+        uses: peaceiris/actions-gh-pages@v3
+        with:
+          github_token: ${{ secrets.GITHUB_TOKEN }}
+          publish_dir: ./result
+          destination_dir: ./doc
+        if: matrix.name == 'Linux' && github.ref == 'refs/heads/master' && github.event_name == 'push'
+      - name: CCache stats
+        run: CCACHE_DIR=/nix/var/cache/ccache nix run .#nixpkgs.ccache -- -s

.github/workflows/pr-body.yml

@@ -1,31 +0,0 @@
-name: Check PR body for changelog convention
-
-on:
-  merge_group:
-  pull_request_target:
-    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'
-        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")) {
-              if (!labels.some(label => label.name.startsWith("changelog-"))) {
-                core.setFailed('feat/fix PR must have a `changelog-*` label');
-              }
-              if (!/^This PR [^<]/.test(body)) {
-                core.setFailed('feat/fix PR must have changelog summary starting with "This PR ..." as first line.');
-              }
-            }

.github/workflows/pr-release.yml

@@ -1,623 +0,0 @@
-# Push a release to the lean4-pr-releases repository, whenever someone pushes to a PR branch.
-
-# This needs to run with the `secrets.PR_RELEASES_TOKEN` token available,
-# but PR branches will generally come from forks,
-# so it is not possible to run this using the `pull_request` or `pull_request_target` workflows.
-# Instead we use `workflow_run`, which essentially allows us to escalate privileges
-# (but only runs the CI as described in the `master` branch, not in the PR branch).
-
-# The main specification/documentation for this workflow is at
-# https://leanprover-community.github.io/contribute/tags_and_branches.html
-# Keep that in sync!
-
-name: PR release
-
-on:
-  workflow_run: # https://docs.github.com/en/actions/using-workflows/events-that-trigger-workflows#workflow_run
-    workflows: [CI]
-    types: [completed]
-
-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'
-    steps:
-      - name: Retrieve information about the original workflow
-        uses: potiuk/get-workflow-origin@v1_1 # https://github.com/marketplace/actions/get-workflow-origin
-        # This action is deprecated and archived, but it seems hard to find a better solution for getting the PR number
-        # see https://github.com/orgs/community/discussions/25220 for some discussion
-        id: workflow-info
-        with:
-          token: ${{ secrets.GITHUB_TOKEN }}
-          sourceRunId: ${{ github.event.workflow_run.id }}
-
-      - name: Download artifact from the previous workflow.
-        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        id: download-artifact
-        uses: dawidd6/action-download-artifact@v11 # https://github.com/marketplace/actions/download-workflow-artifact
-        with:
-          run_id: ${{ github.event.workflow_run.id }}
-          path: artifacts
-          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: |
-          git init --bare lean4.git
-          git -C lean4.git remote add origin https://github.com/${{ github.repository_owner }}/lean4.git
-          git -C lean4.git fetch -n origin master
-          git -C lean4.git fetch -n origin "${{ steps.workflow-info.outputs.sourceHeadSha }}"
-
-          # Create both the original tag and the SHA-suffixed tag
-          SHORT_SHA="${{ steps.workflow-info.outputs.sourceHeadSha }}"
-          SHORT_SHA="${SHORT_SHA:0:7}"
-
-          # Export the short SHA for use in subsequent steps
-          echo "SHORT_SHA=${SHORT_SHA}" >> "$GITHUB_ENV"
-
-          git -C lean4.git tag -f pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} "${{ steps.workflow-info.outputs.sourceHeadSha }}"
-          git -C lean4.git tag -f pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-"${SHORT_SHA}" "${{ steps.workflow-info.outputs.sourceHeadSha }}"
-
-          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
-        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.
-          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/*/*
-        env:
-          GH_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/*/*
-        env:
-          GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
-
-      - name: Report release status (short format)
-        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: actions/github-script@v8
-        with:
-          script: |
-            await github.rest.repos.createCommitStatus({
-              owner: context.repo.owner,
-              repo: context.repo.repo,
-              sha: "${{ steps.workflow-info.outputs.sourceHeadSha }}",
-              state: "success",
-              context: "PR toolchain",
-              description: "${{ github.repository_owner }}/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}",
-            });
-
-      - name: Report release status (SHA-suffixed format)
-        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: actions/github-script@v8
-        with:
-          script: |
-            await github.rest.repos.createCommitStatus({
-              owner: context.repo.owner,
-              repo: context.repo.repo,
-              sha: "${{ steps.workflow-info.outputs.sourceHeadSha }}",
-              state: "success",
-              context: "PR toolchain (SHA-suffixed)",
-              description: "${{ github.repository_owner }}/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}",
-            });
-
-      - name: Add toolchain-available label
-        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: actions/github-script@v8
-        with:
-          script: |
-            await github.rest.issues.addLabels({
-              issue_number: ${{ steps.workflow-info.outputs.pullRequestNumber }},
-              owner: context.repo.owner,
-              repo: context.repo.repo,
-              labels: ['toolchain-available']
-            })
-
-      # Next, determine the most recent nightly release in this PR's history.
-      - name: Find most recent nightly in feature branch
-        id: most-recent-nightly-tag
-        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        run: |
-          git -C lean4.git remote add nightly https://github.com/leanprover/lean4-nightly.git
-          git -C lean4.git fetch nightly '+refs/tags/nightly-*:refs/tags/nightly-*'
-          git -C lean4.git tag --merged "${{ steps.workflow-info.outputs.sourceHeadSha }}" --list "nightly-*" \
-            | sort -rV | head -n 1 | sed "s/^nightly-*/MOST_RECENT_NIGHTLY=/" | tee -a "$GITHUB_ENV"
-
-      - name: 'Setup jq'
-        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 != '' }}
-        id: ready
-        run: |
-          echo "Most recent nightly release in your branch: $MOST_RECENT_NIGHTLY"
-          NIGHTLY_SHA=$(git -C lean4.git rev-parse "nightly-$MOST_RECENT_NIGHTLY^{commit}")
-          echo "SHA of most recent nightly release: $NIGHTLY_SHA"
-          MERGE_BASE_SHA=$(git -C lean4.git merge-base origin/master "${{ steps.workflow-info.outputs.sourceHeadSha }}")
-          echo "SHA of merge-base: $MERGE_BASE_SHA"
-          if [ "$NIGHTLY_SHA" = "$MERGE_BASE_SHA" ]; then
-            echo "The merge base of this PR coincides with the nightly release"
-
-            MATHLIB_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/mathlib4-nightly-testing.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
-
-            if [[ -n "$MATHLIB_REMOTE_TAGS" ]]; then
-              echo "... and Mathlib has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
-              MESSAGE=""
-            else
-              echo "... but Mathlib does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
-              MESSAGE="- ❗ Mathlib CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Mathlib CI should run now."
-            fi
-          else
-            echo "The most recently nightly tag on this branch has SHA: $NIGHTLY_SHA"
-            echo "but 'git merge-base origin/master HEAD' reported: $MERGE_BASE_SHA"
-            git -C lean4.git log -10 origin/master
-
-            git -C lean4.git fetch origin nightly-with-mathlib
-            NIGHTLY_WITH_MATHLIB_SHA="$(git -C lean4.git rev-parse "origin/nightly-with-mathlib")"
-            MESSAGE="- ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch. Try \`git rebase $MERGE_BASE_SHA --onto $NIGHTLY_WITH_MATHLIB_SHA\`."
-          fi
-
-          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 "Accept: application/vnd.github.v3+json" \
-                          "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/labels" \
-                          | jq -r '.[].name')"
-
-            if echo "$LABELS" | grep -q "^force-mathlib-ci$"; then
-              echo "force-mathlib-ci label detected, forcing CI despite issues"
-              MESSAGE="Forcing Mathlib CI because the \`force-mathlib-ci\` label is present, despite problem: $MESSAGE"
-              FORCE_CI=true
-            else
-              MESSAGE="$MESSAGE You can force Mathlib CI using the \`force-mathlib-ci\` label."
-            fi
-
-            echo "Checking existing messages"
-
-            # The code for updating comments is duplicated in mathlib's
-            # scripts/lean-pr-testing-comments.sh
-            # so keep in sync
-
-            # 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 "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]"))')"
-            existing_comment_id="$(echo "$existing_comment" | jq -r .id)"
-            existing_comment_body="$(echo "$existing_comment" | jq -r .body)"
-
-            if [[ "$existing_comment_body" != *"$MESSAGE"* ]]; then
-              MESSAGE="$MESSAGE ($(date "+%Y-%m-%d %H:%M:%S"))"
-
-              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.
-              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 "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"
-              else
-                # Append new result to the existing comment
-                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 "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"
-              fi
-            else
-              echo "The message already exists in the comment body."
-            fi
-
-            if [[ "$FORCE_CI" == "true" ]]; then
-              echo "mathlib_ready=true" >> "$GITHUB_OUTPUT"
-            else
-              echo "mathlib_ready=false" >> "$GITHUB_OUTPUT"
-            fi
-          else
-            echo "mathlib_ready=true" >> "$GITHUB_OUTPUT"
-          fi
-
-      - name: Check merge-base and nightly-testing-YYYY-MM-DD for reference manual
-        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        id: reference-manual-ready
-        run: |
-          echo "Most recent nightly release in your branch: $MOST_RECENT_NIGHTLY"
-          NIGHTLY_SHA=$(git -C lean4.git rev-parse "nightly-$MOST_RECENT_NIGHTLY^{commit}")
-          echo "SHA of most recent nightly release: $NIGHTLY_SHA"
-          MERGE_BASE_SHA=$(git -C lean4.git merge-base origin/master "${{ steps.workflow-info.outputs.sourceHeadSha }}")
-          echo "SHA of merge-base: $MERGE_BASE_SHA"
-          if [ "$NIGHTLY_SHA" = "$MERGE_BASE_SHA" ]; then
-            echo "The merge base of this PR coincides with the nightly release"
-
-            MANUAL_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover/reference-manual.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
-            if [[ -n "$MANUAL_REMOTE_TAGS" ]]; then
-              echo "... and the reference manual has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
-              MESSAGE=""
-            else
-              echo "... but the reference manual does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
-              MESSAGE="- ❗ Reference manual CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-manual\`, reference manual CI should run now."
-            fi
-          else
-            echo "The most recently nightly tag on this branch has SHA: $NIGHTLY_SHA"
-            echo "but 'git merge-base origin/master HEAD' reported: $MERGE_BASE_SHA"
-            git -C lean4.git log -10 origin/master
-
-            git -C lean4.git fetch origin nightly-with-manual
-            NIGHTLY_WITH_MANUAL_SHA="$(git -C lean4.git rev-parse "origin/nightly-with-manual")"
-            MESSAGE="- ❗ Reference manual CI will not be attempted unless your PR branches off the \`nightly-with-manual\` branch. Try \`git rebase $MERGE_BASE_SHA --onto $NIGHTLY_WITH_MANUAL_SHA\`."
-          fi
-
-          if [[ -n "$MESSAGE" ]]; then
-            # Check if force-manual-ci label is present
-            LABELS="$(curl --retry 3 --location --silent \
-                          -H "Authorization: token ${{ secrets.MANUAL_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')"
-
-            if echo "$LABELS" | grep -q "^force-manual-ci$"; then
-              echo "force-manual-ci label detected, forcing CI despite issues"
-              MESSAGE="Forcing reference manual CI because the \`force-manual-ci\` label is present, despite problem: $MESSAGE"
-              FORCE_CI=true
-            else
-              MESSAGE="$MESSAGE You can force reference manual CI using the \`force-manual-ci\` label."
-            fi
-
-            echo "Checking existing messages"
-
-            # The code for updating comments is duplicated in the reference manual's
-            # scripts/lean-pr-testing-comments.sh
-            # so keep in sync
-
-            # Use GitHub API to check if a comment already exists
-            existing_comment="$(curl --retry 3 --location --silent \
-                                    -H "Authorization: token ${{ secrets.MANUAL_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("^- . Manual") or startswith("Reference manual CI status")) | select(.user.login == "leanprover-bot"))')"
-            existing_comment_id="$(echo "$existing_comment" | jq -r .id)"
-            existing_comment_body="$(echo "$existing_comment" | jq -r .body)"
-
-            if [[ "$existing_comment_body" != *"$MESSAGE"* ]]; then
-              MESSAGE="$MESSAGE ($(date "+%Y-%m-%d %H:%M:%S"))"
-
-              echo "Posting message to the comments: $MESSAGE"
-
-              # Append new result to the existing comment or post a new comment
-              # It's essential we use the MANUAL_COMMENT_BOT token here, so that reference manual CI can subsequently edit the comment.
-              if [ -z "$existing_comment_id" ]; then
-                INTRO="Reference manual CI status:"
-                # 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 ${{ secrets.MANUAL_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"
-              else
-                # Append new result to the existing comment
-                echo "Appending to existing comment at leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments"
-                curl -L -s \
-                  -X PATCH \
-                  -H "Authorization: token ${{ secrets.MANUAL_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"
-              fi
-            else
-              echo "The message already exists in the comment body."
-            fi
-
-            if [[ "$FORCE_CI" == "true" ]]; then
-              echo "manual_ready=true" >> "$GITHUB_OUTPUT"
-            else
-              echo "manual_ready=false" >> "$GITHUB_OUTPUT"
-            fi
-          else
-            echo "manual_ready=true" >> "$GITHUB_OUTPUT"
-          fi
-
-
-      - name: Report mathlib base
-        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true' }}
-        uses: actions/github-script@v8
-        with:
-          script: |
-            const description =
-              process.env.MOST_RECENT_NIGHTLY ?
-              "nightly-" + process.env.MOST_RECENT_NIGHTLY :
-              "not branched off nightly";
-            await github.rest.repos.createCommitStatus({
-              owner: context.repo.owner,
-              repo: context.repo.repo,
-              sha: "${{ steps.workflow-info.outputs.sourceHeadSha }}",
-              state: "success",
-              context: "PR branched off:",
-              description: description,
-            });
-
-      # 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: |
-          sudo rm -rf ./*
-
-      # 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
-        with:
-          repository: leanprover-community/batteries
-          token: ${{ steps.mathlib-app-token.outputs.token }}
-          ref: nightly-testing
-          fetch-depth: 0 # This ensures we check out all tags and branches.
-          filter: tree:0
-
-      - name: Check if tag exists
-        if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
-        id: check_batteries_tag
-        run: |
-          git config user.name "leanprover-community-mathlib4-bot"
-          git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com"
-
-          if git ls-remote --heads --tags --exit-code origin "nightly-testing-${MOST_RECENT_NIGHTLY}" >/dev/null; then
-            BASE="nightly-testing-${MOST_RECENT_NIGHTLY}"
-          else
-            echo "Couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' tag at Batteries. Falling back to 'nightly-testing'."
-            BASE=nightly-testing
-          fi
-
-          echo "Using base branch: $BASE"
-
-          EXISTS="$(git ls-remote --heads origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} | wc -l)"
-          echo "Branch exists: $EXISTS"
-          if [ "$EXISTS" = "0" ]; then
-            echo "Branch does not exist, creating it."
-            git switch -c lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} "$BASE"
-            echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}" > lean-toolchain
-            git add lean-toolchain
-            git commit --allow-empty -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
-          else
-            echo "Branch already exists, updating lean-toolchain."
-            git switch lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
-            # The Batteries `nightly-testing` or `nightly-testing-YYYY-MM-DD` branch may have moved since this branch was created, so merge their changes.
-            # (This should no longer be possible once `nightly-testing-YYYY-MM-DD` is a tag, but it is still safe to merge.)
-            git merge "$BASE" --strategy-option ours --no-commit --allow-unrelated-histories
-            echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}" > lean-toolchain
-            git add lean-toolchain
-            git commit --allow-empty -m "Update lean-toolchain for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
-          fi
-
-      - name: Push changes
-        if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
-        run: |
-          git push origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
-
-
-      # We next automatically create a Mathlib branch using this toolchain.
-      # Mathlib CI will be responsible for reporting back success or failure
-      # to the PR comments asynchronously.
-      - name: Cleanup workspace
-        if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
-        run: |
-          sudo rm -rf ./*
-
-      # 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
-        with:
-          repository: leanprover-community/mathlib4-nightly-testing
-          token: ${{ steps.mathlib-app-token.outputs.token }}
-          ref: nightly-testing
-          fetch-depth: 0 # This ensures we check out all tags and branches.
-          filter: tree:0
-
-      - name: install elan
-        run: |
-          set -o pipefail
-          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
-          ./elan-init -y --default-toolchain none
-          echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
-
-      - name: Check if tag exists
-        if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
-        id: check_mathlib_tag
-        run: |
-          git config user.name "leanprover-community-mathlib4-bot"
-          git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com"
-
-          if git ls-remote --heads --tags --exit-code origin "nightly-testing-${MOST_RECENT_NIGHTLY}" >/dev/null; then
-            BASE="nightly-testing-${MOST_RECENT_NIGHTLY}"
-          else
-            echo "Couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' branch at Mathlib. Falling back to 'nightly-testing'."
-            BASE=nightly-testing
-          fi
-
-          echo "Using base tag: $BASE"
-
-          EXISTS="$(git ls-remote --heads origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} | wc -l)"
-          echo "Branch exists: $EXISTS"
-          if [ "$EXISTS" = "0" ]; then
-            echo "Branch does not exist, creating it."
-            git switch -c lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} "$BASE"
-            echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}" > lean-toolchain
-            git add lean-toolchain
-            sed -i 's,require "leanprover-community" / "batteries" @ git ".\+",require "leanprover-community" / "batteries" @ git "lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}",' lakefile.lean
-            lake update batteries
-            git add lakefile.lean lake-manifest.json
-            git commit --allow-empty -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
-          else
-            echo "Branch already exists, updating lean-toolchain and bumping Batteries."
-            git switch lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
-            # The Mathlib `nightly-testing` branch or `nightly-testing-YYYY-MM-DD` tag may have moved since this branch was created, so merge their changes.
-            # (This should no longer be possible once `nightly-testing-YYYY-MM-DD` is a tag, but it is still safe to merge.)
-            git merge "$BASE" --strategy-option ours --no-commit --allow-unrelated-histories
-            echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}" > lean-toolchain
-            git add lean-toolchain
-            lake update batteries
-            git add lake-manifest.json
-            git commit --allow-empty -m "Update lean-toolchain for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
-          fi
-
-      - name: Push changes
-        if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
-        run: |
-          git push origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
-
-      - name: Add mathlib4-nightly-available label
-        if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
-        uses: actions/github-script@v8
-        with:
-          script: |
-            await github.rest.issues.addLabels({
-              issue_number: ${{ steps.workflow-info.outputs.pullRequestNumber }},
-              owner: context.repo.owner,
-              repo: context.repo.repo,
-              labels: ['mathlib4-nightly-available']
-            })
-
-      # We next automatically create a reference manual branch using this toolchain.
-      # Reference manual CI will be responsible for reporting back success or failure
-      # to the PR comments asynchronously (and thus transitively SubVerso/Verso).
-      - name: Cleanup workspace
-        if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.reference-manual-ready.outputs.manual_ready == 'true'
-        run: |
-          sudo rm -rf ./*
-
-      # 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
-        with:
-          repository: leanprover/reference-manual
-          token: ${{ secrets.MANUAL_PR_BOT }}
-          ref: nightly-testing
-          fetch-depth: 0 # This ensures we check out all tags and branches.
-          filter: tree:0
-
-      - name: Check if tag in reference manual exists
-        if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.reference-manual-ready.outputs.manual_ready == 'true'
-        id: check_manual_tag
-        run: |
-          git config user.name "leanprover-bot"
-          git config user.email "leanprover-bot@lean-fro.org"
-
-          if git ls-remote --heads --tags --exit-code origin "nightly-testing-${MOST_RECENT_NIGHTLY}" >/dev/null; then
-            BASE="nightly-testing-${MOST_RECENT_NIGHTLY}"
-          else
-            echo "Couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' branch in the reference manual. Falling back to 'nightly-testing'."
-            BASE=nightly-testing
-          fi
-
-          echo "Using base tag: $BASE"
-
-          EXISTS="$(git ls-remote --heads origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} | wc -l)"
-          echo "Branch exists: $EXISTS"
-          if [ "$EXISTS" = "0" ]; then
-            echo "Branch does not exist, creating it."
-            git switch -c lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} "$BASE"
-            echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}" > lean-toolchain
-            git add lean-toolchain
-            git add lakefile.lean lake-manifest.json
-            git commit --allow-empty -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
-          else
-            echo "Branch already exists, updating lean-toolchain."
-            git switch lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
-            # The reference manual's `nightly-testing` branch or `nightly-testing-YYYY-MM-DD` tag may have moved since this branch was created, so merge their changes.
-            # (This should no longer be possible once `nightly-testing-YYYY-MM-DD` is a tag, but it is still safe to merge.)
-            git merge "$BASE" --strategy-option ours --no-commit --allow-unrelated-histories
-            echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}" > lean-toolchain
-            git add lean-toolchain
-            git add lake-manifest.json
-            git commit --allow-empty -m "Update lean-toolchain for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
-          fi
-
-      - name: Push changes
-        if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.reference-manual-ready.outputs.manual_ready == 'true'
-        run: |
-          git push origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}

.github/workflows/pr-title.yml

@@ -1,20 +0,0 @@
-name: Check PR title for commit convention
-
-on:
-  merge_group:
-  pull_request:
-    types: [opened, synchronize, reopened, edited]
-
-jobs:
-  check-pr-title:
-    runs-on: ubuntu-latest
-    steps:
-      - name: Check PR title
-        uses: actions/github-script@v8
-        with:
-          script: |
-            const msg = context.payload.pull_request? context.payload.pull_request.title : context.payload.merge_group.head_commit.message;
-            console.log(`Message: ${msg}`)
-            if (!/^(feat|fix|doc|style|refactor|test|chore|perf): (?![A-Z][a-z]).*[^.]($|\n\n)/.test(msg)) {
-              core.setFailed('PR title does not follow the Commit Convention (https://leanprover.github.io/lean4/doc/dev/commit_convention.html).');
-            }

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

@@ -1,35 +0,0 @@
-name: Restart by label
-on:
-  pull_request_target:
-    types:
-      - unlabeled
-      - labeled
-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')
-    steps:
-    - run: |
-        # Finding latest CI workflow run on current pull request
-        # (unfortunately cannot search by PR number, only base branch,
-        # and that is't even unique given PRs from forks, but the risk
-        # of confusion is low and the danger is mild)
-        echo "Trying to find a run with branch $head_ref and commit $head_sha"
-        run_id="$(gh run list -e pull_request -b "$head_ref" -c "$head_sha" \
-          --workflow 'CI' --limit 1 --json databaseId --jq '.[0].databaseId')"
-        echo "Run id: ${run_id}"
-        gh run view "$run_id"
-        echo "Cancelling (just in case)"
-        gh run cancel "$run_id" || echo "(failed)"
-        echo "Waiting for 30s"
-        sleep 30
-        gh run view "$run_id"
-        echo "Rerunning"
-        gh run rerun "$run_id"
-        gh run view "$run_id"
-      shell: bash
-      env:
-        head_ref: ${{ github.head_ref }}
-        head_sha: ${{ github.event.pull_request.head.sha }}
-        GH_TOKEN: ${{ github.token }}
-        GH_REPO: ${{ github.repository }}

.github/workflows/stale.yml

@@ -1,20 +0,0 @@
-name: 'Label stale PRs'
-on:
-  schedule:
-    - cron: '30 1 * * *'
-  workflow_dispatch:
-
-permissions:
-  pull-requests: write
-
-jobs:
-  stale:
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/stale@v10
-        with:
-          days-before-stale: -1
-          days-before-pr-stale: 30
-          days-before-close: -1
-          stale-pr-label: 'stale'
-          only-labels: 'awaiting-author'

.github/workflows/update-stage0.yml

@@ -1,93 +0,0 @@
-name: Update stage0
-
-# This action will update stage0 on master as soon as
-# src/stdlib_flags.h and stage0/src/stdlib_flags.h
-# are out of sync there, or when manually triggered.
-# The update bypasses the merge queue to be quick.
-# Also see <doc/dev/bootstrap.md>.
-
-on:
-  push:
-    branches:
-      - 'master'
-  workflow_dispatch:
-
-concurrency:
-  group: stage0
-  cancel-in-progress: true
-
-jobs:
-  update-stage0:
-    runs-on: nscloud-ubuntu-22.04-amd64-8x16
-    env:
-      CCACHE_DIR: ${{ github.workspace }}/.ccache
-      CCACHE_COMPRESS: true
-      CCACHE_MAXSIZE: 400M
-    steps:
-    # 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
-      with:
-        ssh-key: ${{secrets.STAGE0_SSH_KEY}}
-    - run: echo "should_update_stage0=yes" >> "$GITHUB_ENV"
-    - name: Check if automatic update is needed
-      if: github.event_name == 'push'
-      run: |
-        if diff -u src/stdlib_flags.h stage0/src/stdlib_flags.h
-        then
-          echo "src/stdlib_flags.h and stage0/src/stdlib_flags.h agree, nothing to do"
-          echo "should_update_stage0=no" >> "$GITHUB_ENV"
-        fi
-    - name: Setup git user
-      if: env.should_update_stage0 == 'yes'
-      run: |
-          git config --global user.name "Lean stage0 autoupdater"
-          git config --global user.email "<>"
-    - if: env.should_update_stage0 == 'yes'
-      name: Install Nix
-      uses: DeterminateSystems/nix-installer-action@main
-    - name: Open Nix shell once
-      if: env.should_update_stage0 == 'yes'
-      run: true
-      shell: 'nix develop -c bash -euxo pipefail {0}'
-    - name: Set up NPROC
-      if: env.should_update_stage0 == 'yes'
-      run: |
-        echo "NPROC=$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4)" >> $GITHUB_ENV
-      shell: 'nix develop -c bash -euxo pipefail {0}'
-    - name: Restore Cache
-      if: env.should_update_stage0 == 'yes'
-      uses: actions/cache/restore@v5
-      with:
-        # NOTE: must be in sync with `restore-cache` in `build-template.yml`
-        path: |
-          .ccache
-          build/stage1/**/*.trace
-          build/stage1/**/*.olean*
-          build/stage1/**/*.ilean
-          build/stage1/**/*.ir
-          build/stage1/**/*.c
-          build/stage1/**/*.c.o*
-        key: Linux Lake-build-v4-${{ github.sha }}
-        # fall back to (latest) previous cache
-        restore-keys: |
-          Linux Lake-build-v4
-    - if: env.should_update_stage0 == 'yes'
-      # sync options with `Linux Lake` to ensure cache reuse
-      run: |
-        mkdir -p build
-        cmake --preset release -B build -DLEAN_EXTRA_MAKE_OPTS=-DwarningAsError=true
-      shell: 'nix develop -c bash -euxo pipefail {0}'
-    - if: env.should_update_stage0 == 'yes'
-      run: |
-        make -j$NPROC -C build update-stage0-commit
-      shell: 'nix develop -c bash -euxo pipefail {0}'
-    - if: env.should_update_stage0 == 'yes'
-      run: git show --stat
-    - if: env.should_update_stage0 == 'yes' && github.event_name == 'push'
-      name: Sanity check # to avoid loops
-      run: |
-        diff -u src/stdlib_flags.h stage0/src/stdlib_flags.h || exit 1
-    - if: env.should_update_stage0 == 'yes'
-      run: git push origin

.gitignore

@@ -1,11 +1,8 @@
 *~
 \#*
 .#*
-.lake
-lake-manifest.json
-/build
-/src/lakefile.toml
-/lakefile.toml
+*.lock
+build
 GPATH
 GRTAGS
 GSYMS
@@ -17,20 +14,9 @@ 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__
+.vscode
 *.produced.out
 CMakeSettings.json
 CppProperties.json
 result
-fwIn.txt
-fwOut.txt
-wdErr.txt
-wdIn.txt
-wdOut.txt
-downstream_releases/

.gitpod.Dockerfile

@@ -1,14 +0,0 @@
-# You can find the new timestamped tags here: https://hub.docker.com/r/gitpod/workspace-full/tags
-FROM gitpod/workspace-full
-
-USER root
-RUN apt-get update && apt-get install git libgmp-dev libuv1-dev cmake ccache clang -y && apt-get clean
-
-USER gitpod
-
-# Install and configure elan
-RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
-ENV PATH="/home/gitpod/.elan/bin:${PATH}"
-# Create a dummy toolchain so that we can pre-register it with elan
-RUN mkdir -p /workspace/lean4/build/release/stage1/bin && touch /workspace/lean4/build/release/stage1/bin/lean && elan toolchain link lean4 /workspace/lean4/build/release/stage1
-RUN mkdir -p /workspace/lean4/build/release/stage0/bin && touch /workspace/lean4/build/release/stage0/bin/lean && elan toolchain link lean4-stage0 /workspace/lean4/build/release/stage0

.gitpod.yml

@@ -1,11 +0,0 @@
-image:
-    file: .gitpod.Dockerfile
-
-vscode:
-  extensions:
-    - leanprover.lean4
-
-tasks:
-  - name: Release build
-    init: cmake --preset release
-    command: make -C build/release -j$(nproc || sysctl -n hw.logicalcpu)

.ignore

@@ -1 +0,0 @@
-stage0/

.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,35 +1,14 @@
-cmake_minimum_required(VERSION 3.21)
-
-if(NOT CMAKE_GENERATOR MATCHES "Makefiles")
-  message(FATAL_ERROR "Only makefile generators are supported")
-endif()
-
-option(USE_MIMALLOC "use mimalloc" ON)
-
+cmake_minimum_required(VERSION 3.11)
 # store all variables passed on the command line into CL_ARGS so we can pass them to the stage builds
 # https://stackoverflow.com/a/48555098/161659
 # MUST be done before call to 'project'
-# Use standard release build (discarding LEAN_EXTRA_CXX_FLAGS etc.) for stage0 by default since it is assumed to be "good", but still pass through CMake platform arguments (compiler, toolchain file, ..).
-# Use `STAGE0_` prefix to pass variables to stage0 explicitly.
 get_cmake_property(vars CACHE_VARIABLES)
 foreach(var ${vars})
   get_property(currentHelpString CACHE "${var}" PROPERTY HELPSTRING)
-  if(var MATCHES "STAGE0_(.*)")
-    list(APPEND STAGE0_ARGS "-D${CMAKE_MATCH_1}=${${var}}")
-  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 "")
+  if("${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")
-      # 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")
-      list(APPEND STAGE0_ARGS "-D${var}=${${var}}")
-    endif()
-  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"))
+  endif()
+  if(("${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()
@@ -37,190 +16,77 @@ endforeach()
 include(ExternalProject)
 project(LEAN CXX C)
 
-if(NOT (DEFINED STAGE0_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")
-  find_program(CADICAL cadical)
-  if(NOT CADICAL)
-    set(CADICAL_CXX c++)
-    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.
-      set(CADICAL_CXXFLAGS "${CMAKE_CXX_FLAGS}")
-      set(CADICAL_LDFLAGS "-Wl,-rpath=\\$$ORIGIN/../lib")
-    endif()
-    find_program(CCACHE ccache)
-    if(CCACHE)
-      set(CADICAL_CXX "${CCACHE} ${CADICAL_CXX}")
-    endif()
-    # missing stdio locking API on Windows
-    if(CMAKE_SYSTEM_NAME MATCHES "Windows")
-      string(APPEND CADICAL_CXXFLAGS " -DNUNLOCKED")
-    endif()
-    string(APPEND CADICAL_CXXFLAGS " -DNCLOSEFROM")
-    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_IN_SOURCE ON
-      INSTALL_COMMAND ""
-    )
-    set(CADICAL ${CMAKE_BINARY_DIR}/cadical/cadical${CMAKE_EXECUTABLE_SUFFIX})
-    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 STAGE0_ARGS -DLEANTAR=${LEANTAR})
-  list(APPEND CL_ARGS -DCADICAL=${CADICAL} -DLEANTAR=${LEANTAR})
-endif()
-
-if(USE_MIMALLOC)
+if("${CMAKE_SYSTEM_NAME}" MATCHES "Emscripten")
+  # For Emscripten, we build GMP before any of the stages and reuse it in all of them.
+  set(GMP_INSTALL_PREFIX ${CMAKE_BINARY_DIR}/gmp-root)
+  set(EMSCRIPTEN_FLAGS "-s ALLOW_MEMORY_GROWTH=1 -s MAIN_MODULE=1 -O3")
   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 ""
+    gmp
+    URL https://gmplib.org/download/gmp/gmp-6.2.1.tar.bz2
+    URL_HASH SHA256=eae9326beb4158c386e39a356818031bd28f3124cf915f8c5b1dc4c7a36b4d7c
+    BUILD_IN_SOURCE 1
+    CONFIGURE_COMMAND emconfigure ./configure "CFLAGS=${EMSCRIPTEN_FLAGS}" --host=wasm32-unknown-emscripten --disable-assembly --prefix=${GMP_INSTALL_PREFIX}
+    BUILD_COMMAND emmake make -j4
+    INSTALL_COMMAND emmake make install
   )
-  list(APPEND EXTRA_DEPENDS mimalloc)
+  set(EXTRA_DEPENDS "gmp")
+  list(APPEND CL_ARGS "-DGMP_INSTALL_PREFIX=${GMP_INSTALL_PREFIX}")
+  list(APPEND PLATFORM_ARGS "-DGMP_INSTALL_PREFIX=${GMP_INSTALL_PREFIX}")
 endif()
-
-if(NOT STAGE1_PREV_STAGE)
-  ExternalProject_Add(
-    stage0
-    SOURCE_DIR "${LEAN_SOURCE_DIR}/stage0"
-    SOURCE_SUBDIR src
-    BINARY_DIR stage0
-    # do not rebuild stage0 when git hash changes; it's not from this commit anyway
-    # (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
-    DEPENDS ${EXTRA_DEPENDS}
-  )
-  list(APPEND EXTRA_DEPENDS stage0)
-endif()
-ExternalProject_Add(
-  stage1
+ExternalProject_add(stage0
+  SOURCE_DIR "${LEAN_SOURCE_DIR}/stage0"
+  SOURCE_SUBDIR src
+  BINARY_DIR stage0
+  # always use standard release build (discarding LEAN_CXX_EXTRA_FLAGS etc.) for stage0 since it is assumed to be "good", but still pass through CMake platform arguments (compiler, toolchain file, ..)
+  # do not rebuild stage0 when git hash changes; it's not from this commit anyway
+  CMAKE_ARGS -DSTAGE=0 -DCMAKE_BUILD_TYPE=Release -DUSE_GITHASH=OFF ${PLATFORM_ARGS}
+  BUILD_ALWAYS ON  # cmake doesn't auto-detect changes without a download method
+  INSTALL_COMMAND ""  # skip install
+  DEPENDS ${EXTRA_DEPENDS}
+)
+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 ${CL_ARGS}
   BUILD_ALWAYS ON
   INSTALL_COMMAND ""
-  DEPENDS ${EXTRA_DEPENDS}
-  STEP_TARGETS configure
+  DEPENDS stage0
 )
-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}
+  # reuse libleancpp.a, which doesn't change
+  CMAKE_ARGS -DSTAGE=2 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage1 -DLEANCPP="${CMAKE_BINARY_DIR}/stage1/lib/lean/libleancpp.a" ${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 -DLEANCPP="${CMAKE_BINARY_DIR}/stage1/lib/lean/libleancpp.a" ${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(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(test
+  COMMAND $(MAKE) -C stage1 test
+  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

@@ -1,105 +0,0 @@
-{
-  "version": 2,
-  "cmakeMinimumRequired": {
-    "major": 3,
-    "minor": 10,
-    "patch": 0
-  },
-  "configurePresets": [
-    {
-      "name": "release",
-      "displayName": "Default development optimized build config",
-      "generator": "Unix Makefiles",
-      "binaryDir": "${sourceDir}/build/release"
-    },
-    {
-      "name": "debug",
-      "displayName": "Debug build config",
-      "cacheVariables": {
-        "LEAN_EXTRA_CXX_FLAGS": "-DLEAN_DEFAULT_THREAD_STACK_SIZE=16*1024*1024",
-        "CMAKE_BUILD_TYPE": "Debug"
-      },
-      "generator": "Unix Makefiles",
-      "binaryDir": "${sourceDir}/build/debug"
-    },
-    {
-      "name": "reldebug",
-      "displayName": "Release with assertions enabled",
-      "cacheVariables": {
-        "CMAKE_BUILD_TYPE": "RelWithAssert"
-      },
-      "generator": "Unix Makefiles",
-      "binaryDir": "${sourceDir}/build/reldebug"
-    },
-    {
-      "name": "sanitize",
-      "displayName": "Sanitize build config",
-      "cacheVariables": {
-        "LEAN_EXTRA_CXX_FLAGS": "-fsanitize=address,undefined -DLEAN_DEFAULT_THREAD_STACK_SIZE=16*1024*1024",
-        "LEANC_EXTRA_CC_FLAGS": "-fsanitize=address,undefined",
-        "LEAN_EXTRA_LINKER_FLAGS": "-fsanitize=address,undefined -fsanitize-link-c++-runtime",
-        "SMALL_ALLOCATOR": "OFF",
-        "USE_MIMALLOC": "OFF",
-        "BSYMBOLIC": "OFF",
-        "LEAN_TEST_VARS": "MAIN_STACK_SIZE=16000 TEST_STACK_SIZE=16000 LSAN_OPTIONS=max_leaks=10"
-      },
-      "generator": "Unix Makefiles",
-      "binaryDir": "${sourceDir}/build/sanitize"
-    },
-    {
-      "name": "sandebug",
-      "inherits": ["sanitize", "debug"],
-      "displayName": "Sanitize+debug build config",
-      "binaryDir": "${sourceDir}/build/sandebug"
-    }
-  ],
-  "buildPresets": [
-    {
-      "name": "release",
-      "configurePreset": "release"
-    },
-    {
-      "name": "debug",
-      "configurePreset": "debug"
-    },
-    {
-      "name": "reldebug",
-      "configurePreset": "reldebug"
-    },
-    {
-      "name": "sanitize",
-      "configurePreset": "sanitize"
-    },
-    {
-      "name": "sandebug",
-      "configurePreset": "sandebug"
-    }
-  ],
-  "testPresets": [
-    {
-      "name": "release",
-      "configurePreset": "release",
-      "output": {"outputOnFailure": true, "shortProgress": true}
-    },
-    {
-      "name": "debug",
-      "configurePreset": "debug",
-      "inherits": "release"
-    },
-    {
-      "name": "reldebug",
-      "configurePreset": "reldebug",
-      "inherits": "release"
-    },
-    {
-      "name": "sanitize",
-      "configurePreset": "sanitize",
-      "inherits": "release"
-    },
-    {
-      "name": "sandebug",
-      "configurePreset": "sandebug",
-      "inherits": "release"
-    }
-  ]
-}

CODEOWNERS

@@ -1,54 +0,0 @@
-# Code Owners
-#
-# Documents responsible people per component.
-# Listed persons will automatically be asked by GitHub to review a PR touching these paths.
-# If multiple names are listed, a review by any of them is considered sufficient by default.
-
-/.github/ @kim-em
-/RELEASES.md @kim-em
-/src/kernel/ @leodemoura
-/src/library/compiler/ @hargoniX
-/src/lake/ @tydeu
-/src/Lean/Compiler/ @leodemoura @hargoniX
-/src/Lean/Data/Lsp/ @mhuisi
-/src/Lean/Elab/Deriving/ @kim-em
-/src/Lean/Elab/Tactic/ @kim-em
-/src/Lean/Language/ @Kha
-/src/Lean/Meta/Tactic/ @leodemoura
-/src/Lean/PrettyPrinter/ @kmill
-/src/Lean/Server/ @mhuisi
-/src/Lean/Widget/ @Vtec234
-/src/Init/Data/ @kim-em
-/src/Init/Data/Array/Lemmas.lean @digama0
-/src/Init/Data/List/Lemmas.lean @digama0
-/src/Init/Data/List/BasicAux.lean @digama0
-/src/Init/Data/Array/Subarray.lean @david-christiansen
-/src/Lean/Elab/Tactic/RCases.lean @digama0
-/src/Init/RCases.lean @digama0
-/src/Lean/Elab/Tactic/Ext.lean @digama0
-/src/Init/Ext.lean @digama0
-/src/Lean/Elab/Tactic/Simpa.lean @digama0
-/src/Lean/Elab/Tactic/NormCast.lean @digama0
-/src/Lean/Meta/Tactic/NormCast.lean @digama0
-/src/Lean/Meta/Tactic/TryThis.lean @digama0
-/src/Lean/Elab/Tactic/SimpTrace.lean @digama0
-/src/Lean/Elab/Tactic/NoMatch.lean @digama0
-/src/Lean/Elab/Tactic/ShowTerm.lean @digama0
-/src/Lean/Elab/Tactic/Repeat.lean @digama0
-/src/Lean/Meta/Tactic/Repeat.lean @digama0
-/src/Lean/Meta/CoeAttr.lean @digama0
-/src/Lean/Elab/GuardMsgs.lean @digama0
-/src/Lean/Elab/Tactic/Guard.lean @digama0
-/src/Init/Guard.lean @digama0
-/src/Lean/Server/CodeActions/ @digama0
-/src/Std/ @TwoFX
-/src/Std/Tactic/BVDecide/ @hargoniX
-/src/Lean/Elab/Tactic/BVDecide/ @hargoniX
-/src/Std/Sat/ @hargoniX
-/src/Std/Do @sgraf812
-/src/Std/Tactic/Do @sgraf812
-/src/Lean/Elab/Tactic/Do @sgraf812
-/src/Init/Data/Range/Polymorphic @datokrat
-/src/Init/Data/Slice @datokrat
-/src/Init/Data/Iterators @datokrat
-/src/Std/Data/Iterators @datokrat

CONTRIBUTING.md

@@ -1,93 +1,57 @@
-External Contribution Guidelines
-============
+# Contribution Guidelines
 
-In the past, we accepted most pull requests. This practice produced hard to maintain code, performance problems, and bugs. In order to improve the quality and maintainability of our codebase, we've established the following guidelines for external contributions.
+Thank you for your interest in contributing to Lean! There are many ways to contribute and we appreciate all of them.
 
-Helpful links
--------
+## Bug reports
 
-* [Development Setup](./doc/dev/index.md)
-* [Testing](./tests/README.md)
-* [Commit convention](./doc/dev/commit_convention.md)
+Bug reports as new issues are always welcome. Please check the existing [issues](https://github.com/leanprover/lean4/issues) first.
+Reduce the issue to a self-contained, reproducible test case.
+If you have the chance, before reporting a bug, please search existing issues, as it's possible that
+someone else has already reported your error.
+If you're not sure if something is a bug or not, feel free to file a bug anyway. You may also want to discuss it with the Lean
+community using the [lean4 Zulip channel](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4).
 
-Before You Submit a Pull Request (PR):
--------
+## Simple fixes
 
-**Start with an Issue**: Before submitting a PR, always open an issue discussing the problem you wish to solve or the feature you'd like to add. Use the prefix `RFC:` (request for comments) if you are proposing a new feature. Ask for feedback from other users. Take the time to summarize all the feedback. This allows the maintainers to evaluate your proposal more efficiently. When creating a RFC, consider the following questions:
+Simple fixes for **typos and clear bugs** are welcome.
 
-  - **User Experience**: How does this feature improve the user experience?
+## Documentation
 
-  - **Beneficiaries**: Which Lean users and projects do benefit most from this feature/change?
+Tutorial-like examples are very welcome.
+They are useful for finding rough edges and bugs in Lean 4, for highlighting new features, and for showing how to use Lean.
+If you want to store your tutorial in the Lean 4 repository to make sure future changes will not break it, we suggest the following workflow:
+* Contact one of the Lean developers on Zulip, and check whether your tutorial is a good match for the Lean 4 repository.
+* Send bug reports and report rough edges. We will work with you until the tutorial looks great.
+* Add plenty of comments and make sure others will be able to follow it.
+* Create a pull request in the Lean 4 repository. After merging, we will link it to the official documentation and make sure it becomes part of our test suite.
 
-  - **Community Feedback**: Have you sought feedback or insights from other Lean users?
+You can use `.lean` or `.md` files to create your tutorial. The `.md` files are ideal when you want to format your prose using markdown. For an example, see [this `.md` file](https://github.com/leanprover/lean4/blob/master/doc/lean3changes.md).
 
-  - **Maintainability**: Will this change streamline code maintenance or simplify its structure?
+Contributions to the reference manual are also welcome, but since Lean 4 is changing rapidly, please contact us first using Zulip
+to find out which parts are stable enough to document. We will work with you to get this kind of
+pull request merged. We are also happy to meet using Zoom, Skype or Google hangout to coordinate this kind of effort.
 
-**Understand the Project**: Familiarize yourself with the project, existing issues, and latest commits. Ensure your contribution aligns with the project's direction and priorities.
+As Lean 4 matures, other forms of documentation (e.g., doc-strings) will be welcome too.
 
-**Stay Updated**: Regularly fetch and merge changes from the main branch to ensure your branch is up-to-date and can be smoothly integrated.
+## "Help wanted"
 
-**Help wanted**: We have issues tagged with ["help wanted"](https://github.com/leanprover/lean4/issues?q=is%3Aissue+is%3Aopen+label%3A%22help+wanted%22), if you want to contribute to the project, please take a look at them. If you are interested in one of them, post comments, ask questions, and engage with the core developers there.
+For issues marked as [`help wanted`](https://github.com/leanprover/lean4/issues?q=is%3Aissue+is%3Aopen+label%3A%22help+wanted%22), pull requests (PR) are welcome and we will work with you to get a PR merged. Some of these issues are nontrivial. If you are interested, please consider adding comments to the issue and/or messaging the Lean developers in [Zulip](https://leanprover.zulipchat.com/#).
 
-Quality Over Quantity:
------
+## Unexpected Pull Requests
 
-**Focused Changes**: Each PR should address a single, clearly-defined issue or feature. Avoid making multiple unrelated changes in a single PR.
+We have very few core developers, and we cannot review arbitrary pull requests (PRs). Moreover, many features involve subtle tradeoffs, and it may require significant time and energy to even assess a proposed design. We suggest the following workflow:
 
-**Write Tests**: Every new feature or bug fix should come with relevant tests. This ensures the robustness and reliability of the contribution.
+* First, discuss your idea with the Lean community on Zulip. Ask the community to help collect examples, document the requirements, and detect complications.
+* If there is broad support, create a detailed issue for it on the Lean 4 repository at GitHub, and tag the issue with `RFC`.
+* Ask the community for help documenting the requirements, and for collecting examples and concerns.
+* Wait for one of the core developers to give you a "go ahead". At this point, the core developers will work with you to make sure your PR gets merged.
 
-**Documentation**: Update relevant documentation, including comments in the code, to explain the logic and reasoning behind your changes.
+We don't want to waste your time by you implementing a feature and then us not being able to merge it.
 
-Coding Standards:
-----
+## How to Contribute
 
-**Follow the Code Style**: Ensure that your code follows the established coding style of the project.
-
-**Lean on Lean**: Use Lean's built-in features and libraries effectively, avoiding reinventions.
-
-**Performance**: Make sure that your changes do not introduce performance regressions. If possible, optimize the solution for speed and resource usage.
-
-PR Submission:
----
-
-**Descriptive Title and Summary**: The PR title should briefly explain the purpose of the PR. The summary should give more detailed information on what changes are made and why. Links to Zulip threads are not acceptable as a summary. You are responsible for summarizing the discussion, and getting support for it.
-
-**Follow the commit convention**: Pull requests are squash merged, and the
-commit message is taken from the pull request title and body, so make sure they adhere to the [commit convention](https://github.com/leanprover/lean4/blob/master/doc/dev/commit_convention.md). Put questions and extra information, which should not be part of the final commit message, into a first comment rather than the Pull Request description.
-Because the change will be squashed, there is no need to polish the commit messages and history on the branch.
-
-**Link to Relevant Issues**: Reference any issues that your PR addresses to provide context.
-
-**Stay Responsive**: Once the PR is submitted, stay responsive to feedback and be prepared to make necessary revisions. We will close any PR that has been inactive (no response or updates from the submitter) for more than a month.
-
-Reviews and Feedback:
-----
-
-The lean4 repo is managed by the Lean FRO's *triage team* that aims to provide initial feedback on new bug reports, PRs, and RFCs weekly.
-This feedback generally consists of prioritizing the ticket using one of the following categories:
-* label `P-high`: We will work on this issue
-* label `P-medium`: We may work on this issue if we find the time
-* label `P-low`: We are not planning to work on this issue
-* *closed*: This issue is already fixed, it is not an issue, or is not sufficiently compatible with our roadmap for the project and we will not work on it nor accept external contributions on it
-
-For *bug reports*, the listed priority reflects our commitment to fixing the issue.
-It is generally indicative but not necessarily identical to the priority an external contribution addressing this bug would receive.
-For *PRs* and *RFCs*, the priority reflects our commitment to reviewing them and getting them to an acceptable state.
-Accepted RFCs are marked with the label `RFC accepted` and afterwards assigned a new "implementation" priority as with bug reports.
-
-General guidelines for interacting with reviews and feedback:
-
-**Be Patient**: Given the limited number of full-time maintainers and the volume of PRs, reviews may take some time.
-
-**Engage Constructively**: Always approach feedback positively and constructively. Remember, reviews are about ensuring the best quality for the project, not personal criticism.
-
-**Continuous Integration**: Ensure that all CI checks pass on your PR. Failed checks will delay the review process. The maintainers will not check PRs containing failures.
-
-What to Expect:
-----
-
-**Not All PRs Get Merged**: While we appreciate every contribution, not all PRs will be merged. Ensure your changes align with the project's goals and quality standards.
-
-**Feedback is a Gift**: It helps improve the project and can also help you grow as a developer or contributor.
-
-**Community Involvement**: Engage with the Lean community on our communication channels. This can lead to better collaboration and understanding of the project's direction.
+* Always follow the [commit convention](https://leanprover.github.io/lean4/doc/commit_convention.html).
+* Follow the style of the surrounding code. When in doubt, look at other files using the particular syntax as well.
+* Make sure your code is documented.
+* New features or bug fixes should come with appropriate tests.
+* Ensure all tests work before submitting a PR; see [Development Setup](https://leanprover.github.io/lean4/doc/make/index.html#development-setup) and [Fixing Tests](https://leanprover.github.io/lean4/doc/fixing_tests.html).

README.md

@@ -1,20 +1,15 @@
-This is the repository for **Lean 4**.
+This is the repository for **Lean 4**, which is currently being released as milestone releases towards a first stable release.
+[Lean 3](https://github.com/leanprover/lean) is still the latest stable release.
 
 # About
 
-- [Quickstart](https://lean-lang.org/install/)
-- [Homepage](https://lean-lang.org)
-- [Theorem Proving Tutorial](https://lean-lang.org/theorem_proving_in_lean4/)
-- [Functional Programming in Lean](https://lean-lang.org/functional_programming_in_lean/)
-- [Documentation Overview](https://lean-lang.org/learn/)
-- [Language Reference](https://lean-lang.org/doc/reference/latest/)
-- [Release notes](RELEASES.md) starting at v4.0.0-m3
-- [Examples](https://lean-lang.org/examples/)
-- [External Contribution Guidelines](CONTRIBUTING.md)
+- [Homepage](https://leanprover.github.io)
+- [Manual](https://leanprover.github.io/lean4/doc/)
+- [FAQ](https://leanprover.github.io/lean4/doc/faq.html)
 
 # Installation
 
-See [Install Lean](https://lean-lang.org/install/).
+See [Setting Up Lean](https://leanprover.github.io/lean4/doc/setup.html).
 
 # Contributing
 
@@ -22,4 +17,4 @@ Please read our [Contribution Guidelines](CONTRIBUTING.md) first.
 
 # Building from Source
 
-See [Building Lean](doc/make/index.md).
+See [Building Lean](https://leanprover.github.io/lean4/doc/make/index.html).

RELEASES.md

@@ -1,9 +0,0 @@
-# Lean 4 releases
-
-We intend to provide regular "minor version" releases of the Lean language at approximately monthly intervals.
-There is not yet a strong guarantee of backwards compatibility between versions,
-only an expectation that breaking changes will be documented in the release notes.
-
-[Release notes](https://lean-lang.org/doc/reference/latest/releases/#release-notes) are available in the Lean language reference.
-
-Release notes for the current release candidate are available on the GitHub [releases](https://github.com/leanprover/lean4/releases) page.

default.nix

@@ -0,0 +1,9 @@
+# used for `nix-shell https://github.com/leanprover/lean4/archive/master.tar.gz -A nix`
+{ nix = (import ./shell.nix {}).nix; } //
+(import (
+  fetchTarball {
+    url = "https://github.com/edolstra/flake-compat/archive/c75e76f80c57784a6734356315b306140646ee84.tar.gz";
+    sha256 = "071aal00zp2m9knnhddgr2wqzlx6i6qa1263lv1y7bdn2w20h10h"; }
+) {
+  src =  ./.;
+}).defaultNix

doc/.gitignore

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

doc/BoolExpr.lean

@@ -1,4 +1,5 @@
-open Batteries
+import Std
+open Std
 open Lean
 
 inductive BoolExpr where
@@ -103,9 +104,9 @@ syntax entry := ident " ↦ " term:max
 syntax entry,* "⊢" term : term
 
 macro_rules
-  | `( $[$xs ↦ $vs],* ⊢ $p) =>
+  | `( $[$xs:ident ↦ $vs:term],* ⊢ $p:term ) =>
     let xs := xs.map fun x => quote x.getId.toString
-    `(denote (List.toAssocList [$[($xs, $vs)],*]) `[BExpr| $p])
+    `(denote (List.toAssocList [$[( $xs , $vs )],*]) `[BExpr| $p])
 
 #check b ↦ true ⊢ b ∨ b
 #eval  a ↦ false, b ↦ false ⊢ b ∨ a

doc/README.md

@@ -1,10 +0,0 @@
-# Developer Documentation and Examples
-
-This directory contains documentation that describes how to work on
-Lean itself, as well as examples that are included in documentation
-that's hosted on the Lean website.  The `make` directory contains
-information on building Lean, and the `dev` directory describes how to
-work on Lean.
-
-The [documentation section](https://lean-lang.org/documentation) has
-links to documentation that describes how to use Lean itself.

doc/SUMMARY.md

@@ -0,0 +1,61 @@
+# Summary
+
+- [What is Lean](./whatIsLean.md)
+- [Tour of Lean](./tour.md)
+- [Setting Up Lean](./setup.md)
+  - [Quickstart](./quickstart.md)
+
+# Language Manual
+
+- [Dependent Types](./deptypes.md)
+  - [Simple Type Theory](./simptypes.md)
+  - [Types as objects](./typeobjs.md)
+  - [Function Abstraction and Evaluation](./funabst.md)
+  - [Introducing Definitions](./introdef.md)
+  - [What makes dependent type theory dependent?](./dep.md)
+- [Organizational features](./organization.md)
+  - [Sections](./sections.md)
+  - [Namespaces](./namespaces.md)
+  - [Implicit Arguments](./implicit.md)
+  - [Auto Bound Implicit Arguments](./autobound.md)
+- [Declaring New Types](./decltypes.md)
+  - [Enumerated Types](./enum.md)
+  - [Inductive Types](./inductive.md)
+  - [Structures](./struct.md)
+  - [Type classes](./typeclass.md)
+  - [Unification Hints](./unifhint.md)
+- [Builtin Types](./builtintypes.md)
+  - [Natural number](./nat.md)
+  - [Integer](./int.md)
+  - [Fixed precision unsigned integer](./uint.md)
+  - [Float](./float.md)
+  - [Array](./array.md)
+  - [List](./list.md)
+  - [Character](./char.md)
+  - [String](./string.md)
+  - [Option](./option.md)
+  - [Thunk](./thunk.md)
+  - [Task and Thread](./task.md)
+- [Functions](./functions.md)
+- [Tactics](./tactics.md)
+- [Syntax Extensions](./syntax.md)
+  - [The `do` Notation](./do.md)
+  - [String Interpolation](./stringinterp.md)
+
+# Other
+
+- [Frequently Asked Questions](./faq.md)
+- [Significant Changes from Lean 3](./lean3changes.md)
+- [Syntax Highlighting Lean in LaTeX](./syntax_highlight_in_latex.md)
+
+# Development
+
+- [Commit Convention](./commit_convention.md)
+- [Building Lean](./make/index.md)
+  - [Ubuntu Setup](./make/ubuntu-16.04.md)
+  - [macOS Setup](./make/osx-10.9.md)
+  - [Windows Setup](./make/msys2.md)
+  - [Nix Setup (*Experimental*)](./make/nix.md)
+- [Building This Manual](./mdbook.md)
+- [Fixing Tests](./fixing_tests.md)
+- [Debugging](./debugging.md)

doc/array.md

@@ -0,0 +1,62 @@
+# Arrays
+
+The `Array` type implements a *dynamic* (aka growable) array.
+It is defined as
+```lean
+# namespace hidden
+structure Array (α : Type u) where
+  data : List α
+# end hidden
+```
+but its execution time representation is optimized, and it is similar to C++ `std::vector<T>` and Rust `Vec<T>`.
+The Lean type checker has no special support for reducing `Array`s.
+
+You can create arrays in several ways. You can create a small array by listing consecutive values between
+`#[` and `]` and separated by commas, as shown in the following examples.
+
+```lean
+#check #[1, 2, 3] -- Array Nat
+
+#check #[] -- Array ?m
+```
+
+The type of the array elements is inferred from the literals used and must be consistent.
+```lean
+#check #["hello", "world"] -- Array String
+
+-- The following is not valid
+#check_failure #[10, "hello"]
+```
+Recall that the command `#check_failure <term>` only succeeds when the given term is not type correct.
+
+To create an array of size `n` in which all the elements are initialized to some value `a`, use `mkArray`.
+```lean
+#eval mkArray 5 'a'
+-- #['a', 'a', 'a', 'a', 'a']
+```
+
+## Accessing elements
+
+You can access array elements by using brackets (`[` and `]`).
+```lean
+#eval #['a', 'b', 'c'][1]
+-- 'b'
+
+def getThird (xs : Array Nat) : Nat :=
+  xs[2]
+
+#eval getThird #[10, 20, 30, 40]
+-- 30
+```
+The bracket operator is whitespace sensitive.
+```lean
+def f (xs : List Nat) : List Nat :=
+  xs ++ xs
+
+def as : Array Nat :=
+  #[1, 2, 3, 4]
+
+#eval f [1, 2, 3] -- This is a function application
+
+#eval as[2] -- This is an array access
+```

doc/autobound.md

@@ -0,0 +1,45 @@
+## Auto Bound Implicit Arguments
+
+In the previous section, we have shown how implicit arguments make functions more convenient to use.
+However, functions such as `compose` are still quite verbose to define. Note that the universe
+polymorphic `compose` is even more verbose than the one previously defined.
+
+```lean
+universes u v w
+def compose {α : Type u} {β : Type v} {γ : Type w}
+            (g : β → γ) (f : α → β) (x : α) : γ :=
+  g (f x)
+```
+
+You can avoid the `universe` command by providing the universe parameters when defining `compose`.
+
+```lean
+def compose.{u, v, w}
+            {α : Type u} {β : Type v} {γ : Type w}
+            (g : β → γ) (f : α → β) (x : α) : γ :=
+  g (f x)
+```
+
+Lean 4 supports a new feature called *auto bound implicit arguments*. It makes functions such as
+`compose` much more convenient to write. When Lean processes the header of a declaration,
+any unbound identifier is automatically added as an implicit argument *if* it is a single lower case or
+greek letter. With this feature, we can write `compose` as
+
+```lean
+def compose (g : β → γ) (f : α → β) (x : α) : γ :=
+  g (f x)
+
+#check @compose
+-- {β : Sort u_1} → {γ : Sort u_2} → {α : Sort u_3} → (β → γ) → (α → β) → α → γ
+```
+Note that, Lean inferred a more general type using `Sort` instead of `Type`.
+
+Although we love this feature and use it extensively when implementing Lean,
+we realize some users may feel uncomfortable with it. Thus, you can disable it using
+the command `set_option autoBoundImplicitLocal false`.
+```lean
+set_option autoBoundImplicitLocal false
+/- The following definition produces `unknown identifier` errors -/
+-- def compose (g : β → γ) (f : α → β) (x : α) : γ :=
+--   g (f x)
+```

doc/bin/README.md

@@ -0,0 +1,14 @@
+Lean binary distribution
+------------------------
+
+The binary distribution package contains:
+
+- Lean executable (located in the sub-directory bin)
+- Standard library (located in the sub-directory lib/lean/library)
+
+Assuming you are in the same directory this file is located,
+the following command executes a simple set of examples
+
+% bin/lean examples/ex.lean
+
+For more information on Lean and supported editors, please see https://leanprover.github.io/documentation/.

doc/book.toml

@@ -0,0 +1,15 @@
+[book]
+authors = ["Leonardo de Moura", "Sebastian Ullrich"]
+language = "en"
+multilingual = false
+src = "."
+title = "Lean Manual"
+
+[build]
+build-dir = "out"
+
+[output.html]
+git-repository-url = "https://github.com/leanprover/lean4"
+
+[output.html.playground.boring-prefixes]
+lean = "# "

doc/builtintypes.md

@@ -0,0 +1,25 @@
+# Builtin Types
+
+## Numeric Operations
+
+Lean supports the basic mathematical operations you’d expect for all of the number types: addition, subtraction, multiplication, division, and remainder.
+The following code shows how you’d use each one in a `def` commands:
+
+```lean
+-- addition
+def sum := 5 + 10
+
+-- subtraction
+def difference := 95.5 - 4.3
+
+-- multiplication
+def product := 4 * 30
+
+-- division
+def quotient := 53.7 / 32.2
+
+-- remainder/modulo
+def modulo := 43 % 5
+```
+
+Each expression in these statements uses a mathematical operator and evaluates to a single value.

doc/char.md

@@ -0,0 +1 @@
+# Characters

doc/coding_style.md

@@ -0,0 +1,244 @@
+Coding Style
+============
+
+[C++11](http://en.wikipedia.org/wiki/C%2B%2B11) features
+--------------------------------------------------------
+
+We make extensive use of new features in the C++ 11 standard.
+Developers must be familiar with the standard to be able to understand
+the code.
+Here are some of the features that are extensively used.
+
+- Type inference (aka `auto` keyword).
+- Initializer lists.
+- Lambda functions and expressions.
+- `nullptr` constant.
+- Strongly typed enumerations.
+- Right angle bracket.
+- Thread local storage.
+- Threading facilities.
+- Tuple types.
+
+Comments
+--------
+
+The comments in the Lean codebase contain
+[Doxygen](http://www.stack.nl/~dimitri/doxygen/) commands.
+Doxygen is the de facto standard tool for generating documentation from
+annotated C++ sources.
+
+Namespaces
+----------
+
+All code is in the `lean` namespace. Each frontend is stored in a
+separate nested namespace. For example, the SMT 2.0 frontend is stored
+in the `lean::smt` namespace.
+
+Exception: some debugging functions are stored outside of the `lean`
+namespace. These functions are called `print` and are meant to be used
+when debugging Lean using `gdb`.
+
+Smart pointers
+--------------
+
+We only use `std::shared_ptr` template for class `C` only if we expect
+to create only a few objects (< 1000) of class `C`. Otherwise, we
+implement our own intrusive smart pointer. For example, the class
+`expr` is an intrusive smart pointer to `expr_cell`. We may have
+millions of `expr` objects. We say it is intrusive because the
+reference counter is stored in `expr_cell`.
+
+We use `std::unique_ptr` to make sure unique resources will be freed
+correctly.
+
+Template
+--------
+We organize template source code using the approach described at http://www.codeproject.com/Articles/3515/How-To-Organize-Template-Source-Code
+
+Idioms
+------
+
+We use some popular C++ idioms:
+
+- [Pimpl](http://c2.com/cgi/wiki?PimplIdiom)
+- [RAII](http://en.wikipedia.org/wiki/Resource_Acquisition_Is_Initialization) Resource Acquisition Is Initialization
+
+Formatting
+----------
+
+* We use 4 spaces for indentation.
+
+* Class, method, and function names are lower case
+We use `_` for composite names. Example: `type_checker`.
+
+* Class/struct fields should start with the prefix `m_`.
+
+Example:
+
+     class point {
+         int m_x;
+         int m_y;
+     public:
+         ...
+     };
+
+* We do **not** use the `#ifndef-#define-#endif` idiom for header files.
+Instead we use `#pragma once`.
+
+* We write `type const & v` instead of `const type & v`.
+
+* We use `const` extensively.
+
+* `if-then-else`
+
+The following forms are acceptable:
+
+     if (cond) {
+         ...
+     } else {
+         ...
+     }
+
+and
+
+     if (cond)
+        statement1;
+     else
+        statement2;
+
+In *exceptional cases*, we also use
+
+     if (cond) statement;
+
+and
+
+     if (cond) statement1; else stament2;
+
+* `if-then-else-if-else`
+
+The following forms are acceptable:
+
+     if (cond) {
+         ...
+     } else if (cond) {
+         ...
+     } else {
+         ...
+     }
+
+and
+
+     if (cond)
+         statement1;
+     else if (cond)
+         statement2;
+     else
+         statement3;
+
+* We frequently format code using extra spaces
+
+For example, we write
+
+    environment const & m_env;
+    cache               m_cache;
+    normalizer          m_normalizer;
+    volatile bool       m_interrupted;
+
+instead of
+
+    environment const & m_env;
+    cache m_cache;
+    normalizer m_normalizer;
+    volatile bool m_interrupted;
+
+* We use the macro `lean_assert` for assertions.
+The macro `lean_assert` is extensively used when writing unit tests.
+
+* Spaces in expressions
+We write `a == b` instead of `a==b`.
+Similarly, we write `x < y + 1` instead of `x<y+1`.
+
+Google's C++ Style Guide
+------------------------
+
+We are using a modified version of [Google's C++ Style Guide][google-style].
+We also have our version of Google's style checker [cpplint.py][cpplint].
+You can run the checker over the codebase by typing:
+
+    make style
+
+If you use Ninja, you can check by ``ninja style``. It is also a part of testcases and can be run by
+
+    ctest -R style_check
+
+*Disabled* Features:
+
+ - Namespace should be terminated with "namespace"
+ - At least two spaces is best between code and comments
+ - Do not use ``dynamic_cast<>``.  If you need to cast within a class
+   hierarchy, use ``static_cast<>`` to upcast.  Google doesn't support
+   RTTI.
+ - "public:" should be preceded by a blank line
+ - Missing space before ``{``
+ - Found C system header after C++ system header. Should be:
+   environment.h, c system, c++ system, other.
+ - Labels should always be indented at least one space.  If this is
+   a member-initializer list in a constructor or the base class list in
+   a class definition, the colon should be on the following line.
+ - You don't need a ``;`` after a ``}``
+ - No ``#ifndef`` header guard found
+ - Streams are highly discouraged.
+ - Extra space before ``(`` in function call
+ - Else clause should never be on same line as else
+ - Extra space before ``)``
+ - Is this a non-const reference? If so, make const or use a pointer.
+ - All parameters should be named in a function
+ - Do not use anonymous constructor notation (e.g., ``{a1, ..., an}``)
+
+Modified Features:
+
+  - Add ``#include <list>`` for ``list<>``
+
+    => *Check* ``std::list`` instead of ``list`` because we do have our own ``lean::list`` type.
+
+  - Add ``#include <algorithm>`` for copy
+
+    => *Check* ``std::copy`` instead of ``copy`` because we do have our own ``lean::copy`` method.
+
+  - Do not use namespace using-directives. Use using-declarations instead.
+
+    => *Allow* this if filename contains "tests/"
+
+  - Small and focused functions are preferred: foo()
+    has xxx non-comment lines (error triggered by exceeding 500 lines).
+
+    => *Allow* this if filename contains "tests/"
+
+  - Include the directory when naming .h files
+
+    => *Allow* this if the included filename is "version.h" which is generated by cmake.
+
+[google-style]: http://google-styleguide.googlecode.com/svn/trunk/cppguide.xml
+[cpplint]: /src/cmake/Modules/cpplint.py
+
+Git pre-push hook
+-----------------
+
+Since [git 1.8.2][git-pre-push-hook], git introduced *pre-push* hook
+which is executed *before* actual push operation is performed. Using this,
+we can *automatically* run the style checker over the changed files *before*
+we push commits to repositories. This is useful because it prevents us
+from accidentally pushing the commits which contain style problems.
+
+[git-pre-push-hook]: https://github.com/git/git/blob/master/Documentation/RelNotes/1.8.2.txt
+
+To activate the hook, execute
+
+```bash
+ln -s ../../script/pre-push .git/hooks
+```
+
+in the project root directory.
+
+You can change the ``CHECKER`` variable in the script if you want to use other
+checkers.

doc/commit_convention.md

@@ -0,0 +1,71 @@
+Git Commit Convention
+=====================
+
+We are using the following convention for writing git-commit messages.
+It is based on the one from AngularJS project([doc][angularjs-doc],
+[commits][angularjs-git]).
+
+[angularjs-git]: https://github.com/angular/angular.js/commits/master
+[angularjs-doc]: https://docs.google.com/document/d/1QrDFcIiPjSLDn3EL15IJygNPiHORgU1_OOAqWjiDU5Y/edit#
+
+Format of the commit message
+----------------------------
+
+    <type>: <subject>
+    <NEWLINE>
+    <body>
+    <NEWLINE>
+    <footer>
+
+``<type>`` is:
+
+ - feat (feature)
+ - fix (bug fix)
+ - doc (documentation)
+ - style (formatting, missing semicolons, ...)
+ - refactor
+ - test (when adding missing tests)
+ - chore (maintain, ex: travis-ci)
+ - perf (performance improvement, optimization, ...)
+
+``<subject>`` has the following constraints:
+
+ - use imperative, present tense: "change" not "changed" nor "changes"
+ - do not capitalize the first letter
+ - no dot(.) at the end
+
+``<body>`` has the following constraints:
+
+ - just as in ``<subject>``, use imperative, present tense
+ - includes motivation for the change and contrasts with previous
+   behavior
+
+``<footer>`` is optional and may contain two items:
+
+ - Breaking changes: All breaking changes have to be mentioned in
+   footer with the description of the change, justification and
+   migration notes
+ - Referencing issues: Closed bugs should be listed on a separate line
+   in the footer prefixed with "Closes" keyword like this:
+
+    Closes #123, #456
+
+Examples
+--------
+
+fix: add declarations for operator<<(std::ostream&, expr const&) and operator<<(std::ostream&, context const&) in the kernel
+
+The actual implementation of these two operators is outside of the
+kernel. They are implemented in the file 'library/printer.cpp'. We
+declare them in the kernel to prevent the following problem. Suppose
+there is a file 'foo.cpp' that does not include 'library/printer.h',
+but contains
+
+    expr a;
+    ...
+    std::cout << a << "\n";
+    ...
+
+The compiler does not generate an error message. It silently uses the
+operator bool() to coerce the expression into a Boolean. This produces
+counter-intuitive behavior, and may confuse developers.

doc/debugging.md

@@ -0,0 +1,31 @@
+Debugging
+=========
+
+Some notes on how to debug Lean, which may also be applicable to debugging Lean programs in general.
+
+## Tracing
+
+In `CoreM` and derived monads, we use `trace![traceCls] "msg with {interpolations}"` to fill the structured trace viewable with `set_option trace.traceCls true`.
+New trace classes have to be registered using `registerTraceClass` first.
+
+Notable trace classes:
+* `Elab.command`/`Elab.step`: command/term macro expansion/elaboration steps
+
+  Useful options modifying these traces for debugging syntax trees:
+  ```
+  set_option pp.raw true
+  set_option pp.raw.maxDepth 10
+  ```
+* `Meta.synthInstance`: typeclass resolution
+* `Meta.isDefEq`: unification
+* `interpreter`: full execution trace of the interpreter. Only available in debug builds.
+
+In pure contexts or when execution is aborted before the messages are finally printed, one can instead use the term `dbg_trace "msg with {interpolations}"; val` (`;` can also be replaced by a newline), which will print the message directly to stderr before evaluating `val`. `dbgTraceVal val` can be used as a shorthand for `dbg_trace "{val}"; val`.
+Note that if the return value is not actually used, the trace code is silently dropped as well.
+
+## Debuggers
+
+`gdb`/`lldb` can be used to inspect stack traces of compiled Lean code, though they cannot print values of Lean variables and terms in any legible way yet.
+For example, `b lean_panic_fn` can be used to look at the stack trace of a panic.
+
+The [`rr` reverse debugger](https://github.com/rr-debugger/rr) is an amazing tool for investigating e.g. segfaults from reference counting errors, though better hope you will never need it...

doc/decltypes.md

@@ -0,0 +1,29 @@
+# Declaring New Types
+
+In Lean's library, every concrete type other than the universes and every type constructor other than the dependent function type is
+an instance of a general family of type constructions known as *inductive types*. It is remarkable that it is possible to develop
+complex programs and formalize mathematics based on nothing more than the type universes, dependent function types,
+and inductive types; everything else follows from those.
+
+Intuitively, an inductive type is built up from a specified list of constructors. In Lean, the basic syntax for specifying such a type is as follows:
+```
+inductive NewType where
+  | constructor_1 : ... → NewType
+  | constructor_2 : ... → NewType
+  ...
+  | constructor_n : ... → NewType
+```
+
+The intuition is that each constructor specifies a way of building new objects of ``NewType``, possibly from previously constructed values.
+The type ``NewType`` consists of nothing more than the objects that are constructed in this way.
+
+We will see below that the arguments to the constructors can include objects of type ``NewType``,
+subject to a certain "positivity" constraint, which guarantees that elements of ``NewType`` are built
+from the bottom up. Roughly speaking, each ``...`` can be any function type constructed from ``NewType``
+and previously defined types, in which ``NewType`` appears, if at all, only as the "target" of the function type.
+
+We will provide a number of examples of inductive types. We will also consider slight generalizations of the scheme above,
+to mutually defined inductive types, and so-called *inductive families*.
+
+Every inductive type comes with constructors, which show how to construct an element of the type, and elimination rules,
+which show how to "use" an element of the type in another construction.

doc/definitions.md

@@ -0,0 +1 @@
+# Definitions

doc/dep.md

@@ -0,0 +1,66 @@
+## What makes dependent type theory dependent?
+
+The short explanation is that what makes dependent type theory dependent is that types can depend on parameters.
+You have already seen a nice example of this: the type ``List α`` depends on the argument ``α``, and
+this dependence is what distinguishes ``List Nat`` and ``List Bool``.
+For another example, consider the type ``Vector α n``, the type of vectors of elements of ``α`` of length ``n``.
+This type depends on *two* parameters: the type ``α : Type`` of the elements in the vector and the length ``n : Nat``.
+
+Suppose we wish to write a function ``cons`` which inserts a new element at the head of a list.
+What type should ``cons`` have? Such a function is *polymorphic*: we expect the ``cons`` function for ``Nat``, ``Bool``,
+or an arbitrary type ``α`` to behave the same way.
+So it makes sense to take the type to be the first argument to ``cons``, so that for any type, ``α``, ``cons α``
+is the insertion function for lists of type ``α``. In other words, for every ``α``, ``cons α`` is the function that takes an element ``a : α``
+and a list ``as : List α``, and returns a new list, so we have ``cons α a as : list α``.
+
+It is clear that ``cons α`` should have type ``α → List α → List α``. But what type should ``cons`` have?
+A first guess might be ``Type → α → list α → list α``, but, on reflection, this does not make sense:
+the ``α`` in this expression does not refer to anything, whereas it should refer to the argument of type ``Type``.
+In other words, *assuming* ``α : Type`` is the first argument to the function, the type of the next two elements are ``α`` and ``List α``.
+These types vary depending on the first argument, ``α``.
+
+This is an instance of a *dependent function type*, or *dependent arrow type*. Given ``α : Type`` and ``β : α → Type``,
+think of ``β`` as a family of types over ``α``, that is, a type ``β a`` for each ``a : α``.
+In that case, the type ``(a : α) → β a`` denotes the type of functions ``f`` with the property that,
+for each ``a : α``, ``f a`` is an element of ``β a``. In other words, the type of the value returned by ``f`` depends on its input.
+
+Notice that ``(a : α) → β`` makes sense for any expression ``β : Type``. When the value of ``β`` depends on ``a``
+(as does, for example, the expression ``β a`` in the previous paragraph), ``(a : α) → β`` denotes a dependent function type.
+When ``β`` doesn't depend on ``a``, ``(a : α) → β`` is no different from the type ``α → β``.
+Indeed, in dependent type theory (and in Lean), ``α → β`` is just notation for ``(a : α) → β`` when ``β`` does not depend on ``a``.
+
+Returning to the example of lists, we can use the command `#check` to inspect the type of the following `List` functions
+We will explain the ``@`` symbol and the difference between the round and curly braces momentarily.
+
+```lean
+#check @List.cons    -- {α : Type u_1} → α → List α → List α
+#check @List.nil     -- {α : Type u_1} → List α
+#check @List.length  -- {α : Type u_1} → List α → Nat
+#check @List.append  -- {α : Type u_1} → List α → List α → List α
+```
+
+Just as dependent function types ``(a : α) → β a`` generalize the notion of a function type ``α → β`` by allowing ``β`` to depend on ``α``,
+dependent Cartesian product types ``(a : α) × β a`` generalize the Cartesian product ``α × β`` in the same way. Dependent products are also
+called *sigma* types, and you can also write them as `Σ a : α, β a`. You can use `⟨a, b⟩` or `Sigma.mk a b` to create a dependent pair.
+
+```lean
+universes u v
+
+def f (α : Type u) (β : α → Type v) (a : α) (b : β a) : (a : α) × β a :=
+  ⟨a, b⟩
+
+def g (α : Type u) (β : α → Type v) (a : α) (b : β a) : Σ a : α, β a :=
+  Sigma.mk a b
+
+#reduce f
+#reduce g
+
+#reduce f Type (fun α => α) Nat 10
+#reduce g Type (fun α => α) Nat 10
+
+#reduce (f Type (fun α => α) Nat 10).1 -- Nat
+#reduce (g Type (fun α => α) Nat 10).1 -- Nat
+#reduce (f Type (fun α => α) Nat 10).2 -- 10
+#reduce (g Type (fun α => α) Nat 10).2 -- 10
+```
+The function `f` and `g` above denote the same function.

doc/deptypes.md

@@ -0,0 +1,3 @@
+# Dependent Types
+
+In this section, we introduce simple type theory, types as objects, definitions, and explain what makes dependent type theory *dependent*.

doc/dev/bootstrap.md

@@ -1,155 +0,0 @@
-# Lean Build Bootstrapping
-
-Lean is a bootstrapped program: the
-frontend and compiler are written in Lean itself and thus need to be built before
-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:
-
-```bash
-stage0/
-  # Bootstrap binary built from stage0/src/.
-  # We do not use any other files from this directory in further stages.
-  bin/lean
-stage1/
-  include/
-    config.h  # config variables used to build `lean` such as used allocator
-    runtime/lean.h  # runtime header, used by extracted C code, uses `config.h`
-  share/lean/
-    lean.mk  # used by `leanmake`
-  lib/
-    lean/**/*.olean  # the Lean library (incl. the compiler) compiled by the previous stage's `lean`
-    temp/**/*.{c,o}  # the library extracted to C and compiled by `leanc`
-    libInit.a libLean.a  # static libraries of the Lean library
-    libleancpp.a  # a static library of the C++ sources of Lean
-    libleanshared.so  # a dynamic library including the static libraries above
-  bin/
-    lean  # the Lean compiler & server, a small executable that calls directly into libleanshared.so
-    leanc  # a wrapper around a C compiler supplying search paths etc
-    leanmake  # a wrapper around `make` supplying the Makefile above
-stage2/...
-stage3/...
-```
-
-Stage 0 can be viewed as a blackbox since it does not depend on any local
-changes and is equivalent to downloading a bootstrapping binary as done in other
-compilers. The build for any other stage starts by building the runtime and
-standard library from `src/`, using the `lean` binary from the previous stage in
-the latter case, which are then assembled into a new `bin/lean` binary.
-
-Each stage can be built by calling `make stageN` in the root build folder.
-Running just `make` will default to stage 1, which is usually sufficient for
-testing changes on the test suite or other files outside of the stdlib. However,
-it might happen that the stage 1 compiler is not able to load its own stdlib,
-e.g. when changing the .olean format: the stage 1 stdlib will use the format
-generated by the stage 0 compiler, but the stage 1 compiler will expect the new
-format. In this case, we should continue with building and testing stage 2
-instead, which will both build and expect the new format. Note that this is only
-possible because when building a stage's stdlib, we use the previous compiler
-but never load the previous stdlib (since everything is `prelude`). We can also
-use stage 2 to test changes in the compiler or other "meta" parts, i.e. changes
-that affect the produced (.olean or .c) code, on the stdlib and compiler itself.
-We are not aware of any "meta-meta" parts that influence more than two stages of
-compilation, so stage 3 should always be identical to stage 2 and only exists as
-a sanity check.
-
-In summary, doing a standard build via `make` internally involves these steps:
-
-1. compile the `stage0/src` archived sources into `stage0/bin/lean`
-1. use it to compile the current library (*including* your changes) into `stage1/lib`
-1. link that and the current C++ code from `src/` into `stage1/bin/lean`
-
-You now have a Lean binary and library that include your changes, though their
-own compilation was not influenced by them, that you can use to test your
-changes on test programs whose compilation *will* be influenced by the changes.
-
-## Updating stage0
-
-Finally, when we want to use new language features in the library, we need to
-update the archived C source code of the stage 0 compiler in `stage0/src`.
-
-The github repository will automatically update stage0 on `master` once
-`src/stdlib_flags.h` and `stage0/src/stdlib_flags.h` are out of sync.
-To trigger this, modify `stage0/src/stdlib_flags.h` (e.g., by adding or changing
-a comment). When `update-stage0` runs, it will overwrite `stage0/src/stdlib_flags.h`
-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.
-
-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.
-You can do that on <https://github.com/leanprover/lean4/actions/workflows/update-stage0.yml>
-or using Github CLI with
-```
-gh workflow run update-stage0.yml
-```
-
-Leaving stage0 updates to the CI automation is preferable, but should you need
-to do it locally, you can use `make -C build/release update-stage0-commit` to
-update `stage0` from `stage1` or `make -C build/release/stageN update-stage0-commit` to
-update from another stage. This command will automatically stage the updated files
-and introduce a commit, so make sure to commit your work before that.
-
-If you rebased the branch (either onto a newer version of `master`, or fixing
-up some commits prior to the stage0 update), recreate the stage0 update commits.
-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 separate stage0 update commits; then coordinate with the admins to merge
-your PR using rebase merge, bypassing the merge queue.
-
-
-## Further Bootstrapping Complications
-
-As written above, changes in meta code in the current stage usually will only
-affect later stages. This is an issue in two specific cases.
-
-* For the special case of *quotations*, it is desirable to have changes in builtin parsers affect them immediately: when the changes in the parser become active in the next stage, builtin macros implemented via quotations should generate syntax trees compatible with the new parser, and quotation patterns in builtin macros and elaborators should be able to match syntax created by the new parser and macros.
-  Since quotations capture the syntax tree structure during execution of the current stage and turn it into code for the next stage, we need to run the current stage's builtin parsers in quotations via the interpreter for this to work.
-  Caveats:
-  * We activate this behavior by default when building stage 1 by setting `-Dinternal.parseQuotWithCurrentStage=true`.
-    We force-disable it inside `macro/macro_rules/elab/elab_rules` via `suppressInsideQuot` as they are guaranteed not to run in the next stage and may need to be run in the current one, so the stage 0 parser is the correct one to use for them.
-    It may be necessary to extend this disabling to functions that contain quotations and are (exclusively) used by one of the mentioned commands. A function using quotations should never be used by both builtin and non-builtin macros/elaborators. Example: https://github.com/leanprover/lean4/blob/f70b7e5722da6101572869d87832494e2f8534b7/src/Lean/Elab/Tactic/Config.lean#L118-L122
-  * The parser needs to be reachable via an `import` statement, otherwise the version of the previous stage will silently be used.
-  * Only the parser code (`Parser.fn`) is affected; all metadata such as leading tokens is taken from the previous stage.
-
-  For an example, see https://github.com/leanprover/lean4/commit/f9dcbbddc48ccab22c7674ba20c5f409823b4cc1#diff-371387aed38bb02bf7761084fd9460e4168ae16d1ffe5de041b47d3ad2d22422R13
-
-* For *non-builtin* meta code such as `notation`s or `macro`s in
-  `Notation.lean`, we expect changes to affect the current file and all later
-  files of the same stage immediately, just like outside the stdlib. To ensure
-  this, we build stage 1 using `-Dinterpreter.prefer_native=false` -
-  otherwise, when executing a macro, the interpreter would notice that there is
-  already a native symbol available for this function and run it instead of the
-  new IR, but the symbol is from the previous stage!
-
-  To make matters more complicated, while `false` is a reasonable default
-  incurring only minor overhead (`ParserDescr`s and simple macros are cheap to
-  interpret), there are situations where we *need* to set the option to `true`:
-  when the interpreter is executed from the native code of the previous stage,
-  the type of the value it computes must be identical to/ABI-compatible with the
-  type in the previous stage. For example, if we add a new parameter to `Macro`
-  or reorder constructors in `ParserDescr`, building the stage with the
-  interpreter will likely fail. Thus we need to set `interpreter.prefer_native`
-  to `true` in such cases to "freeze" meta code at their versions in the
-  previous stage; no new meta code should be introduced in this stage. Any
-  further stages (e.g. after an `update-stage0`) will then need to be compiled
-  with the flag set to `false` again since they will expect the new signature.
-
-  When enabling `prefer_native`, we usually want to *disable* `parseQuotWithCurrentStage` as it would otherwise make quotations use the interpreter after all.
-  However, there is a specific case where we want to set both options to `true`: when we make changes to a non-builtin parser like `simp` that has a builtin elaborator, we cannot have the new parser be active outside of quotations in stage 1 as the builtin elaborator from stage 0 would not understand them; on the other hand, we need quotations in e.g. the builtin `simp` elaborator to produce the new syntax in the next stage.
-  As this issue usually affects only tactics, enabling `debug.byAsSorry` instead of `prefer_native` can be a simpler solution.
-
-  For a `prefer_native` example, see https://github.com/leanprover/lean4/commit/da4c46370d85add64ef7ca5e7cc4638b62823fbb.
-
-To modify either of these flags both for building and editing the stdlib, adjust
-the code in `stage0/src/stdlib_flags.h`. The flags will automatically be reset
-on the next `update-stage0` when the file is overwritten with the original
-version in `src/`.

doc/dev/commit_convention.md

@@ -1,84 +0,0 @@
-Git Commit Convention
-=====================
-
-We are using the following convention for writing git commit messages. For pull
-requests, make sure the pull request title and description follow this
-convention, as the squash-merge commit will inherit title and body from the
-pull request.
-
-This convention is based on the one from the AngularJS project ([doc][angularjs-doc],
-[commits][angularjs-git]).
-
-
-[angularjs-git]: https://github.com/angular/angular.js/commits/master
-[angularjs-doc]: https://docs.google.com/document/d/1QrDFcIiPjSLDn3EL15IJygNPiHORgU1_OOAqWjiDU5Y/edit#
-
-Format of the commit message
-----------------------------
-
-    <type>: <subject>
-    <NEWLINE>
-    <body>
-    <NEWLINE>
-    <footer>
-
-``<type>`` is:
-
- - feat (feature)
- - fix (bug fix)
- - doc (documentation)
- - style (formatting, missing semicolons, ...)
- - refactor
- - test (when adding missing tests)
- - chore (maintain, ex: travis-ci)
- - perf (performance improvement, optimization, ...)
-
-Every `feat` or `fix` commit must have a `changelog-*` label, and a commit message
-beginning with "This PR " that will be included in the changelog.
-
-``<subject>`` has the following constraints:
-
- - use imperative, present tense: "change" not "changed" nor "changes"
- - do not capitalize the first letter
- - no dot(.) at the end
-
-``<body>`` has the following constraints:
-
- - just as in ``<subject>``, use imperative, present tense
- - includes motivation for the change and contrasts with previous
-   behavior
- - If a `changelog-*` label is present, the body must begin with "This PR ".
-
-``<footer>`` is optional and may contain two items:
-
- - Breaking changes: All breaking changes have to be mentioned in
-   footer with the description of the change, justification and
-   migration notes
- - Referencing issues: Closed bugs should be listed on a separate line
-   in the footer prefixed with "Closes" keyword like this:
-
-    Closes #123, #456
-
-Examples
---------
-
-fix: add declarations for operator<<(std::ostream&, expr const&) and operator<<(std::ostream&, context const&) in the kernel
-
-This PR adds declarations `operator<<` for raw printing.
-The actual implementation of these two operators is outside of the
-kernel. They are implemented in the file 'library/printer.cpp'.
-
-We declare them in the kernel to prevent the following problem.
-Suppose there is a file 'foo.cpp' that does not include 'library/printer.h',
-but contains
-```cpp
-expr a;
-...
-std::cout << a << "\n";
-...
-```
-
-The compiler does not generate an error message. It silently uses the
-operator bool() to coerce the expression into a Boolean. This produces
-counter-intuitive behavior, and may confuse developers.
-

doc/dev/debugging.md

@@ -1,34 +0,0 @@
-Debugging
-=========
-
-Some notes on how to debug Lean, which may also be applicable to debugging Lean programs in general.
-
-## Tracing
-
-In `CoreM` and derived monads, we use `trace[traceCls] "msg with {interpolations}"` to fill the structured trace viewable with `set_option trace.traceCls true`.
-New trace classes have to be registered using `registerTraceClass` first.
-
-Notable trace classes:
-* `Elab.command`/`Elab.step`: command/term macro expansion/elaboration steps
-
-  Useful options modifying these traces for debugging syntax trees:
-  ```
-  set_option pp.raw true
-  set_option pp.raw.maxDepth 10
-  ```
-* `Meta.synthInstance`: typeclass resolution
-* `Meta.isDefEq`: unification
-* `interpreter`: full execution trace of the interpreter. Only available in debug builds.
-
-In pure contexts or when execution is aborted before the messages are finally printed, one can instead use the term `dbg_trace "msg with {interpolations}"; val` (`;` can also be replaced by a newline), which will print the message to stderr before evaluating `val`. `dbgTraceVal val` can be used as a shorthand for `dbg_trace "{val}"; val`.
-Note that if the return value is not actually used, the trace code is silently dropped as well.
-
-By default, such stderr output is buffered and shown as messages after a command has been elaborated, which is necessary to ensure deterministic ordering of messages under parallelism.
-If Lean aborts the process before it can finish the command or takes too long to do that, using `-DstderrAsMessages=false` avoids this buffering and shows `dbg_trace` output (but not `trace`s or other diagnostics) immediately.
-
-## Debuggers
-
-`gdb`/`lldb` can be used to inspect stack traces of compiled Lean code, though they cannot print values of Lean variables and terms in any legible way yet.
-For example, `b lean_panic_fn` can be used to look at the stack trace of a panic.
-
-The [`rr` reverse debugger](https://github.com/rr-debugger/rr) is an amazing tool for investigating e.g. segfaults from reference counting errors, though better hope you will never need it...

doc/dev/ffi.md

@@ -1,9 +0,0 @@
-# Foreign Function Interface
-
-The Lean FFI documentation is now part of the [Lean language reference](https://lean-lang.org/doc/reference/latest/).
-
- * [General FFI](https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=ffi)
- * [Representation of inductive types](https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=inductive-types-ffi)
- * [String](https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=string-ffi)
- * [Array](https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=array-ffi)
-

doc/dev/index.md

@@ -1,119 +0,0 @@
-# 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).
-
-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.
-
-## Development Setup
-
-You can use any of the [supported editors](https://lean-lang.org/install/manual/) for editing the Lean source code.
-Please see below for specific instructions for VS Code.
-
-### Dev setup using elan
-
-You can use [`elan`](https://github.com/leanprover/elan) to easily
-switch between stages and build configurations based on the current
-directory, both for the `lean`, `leanc`, and `leanmake` binaries in your shell's
-PATH and inside your editor.
-
-To install elan, you can do so, without installing a default version of Lean, using (Unix)
-
-```bash
-curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none
-```
-or (Windows)
-```
-curl -O --location https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1
-powershell -f elan-init.ps1 --default-toolchain none
-del elan-init.ps1
-```
-
-The `lean-toolchain` files in the Lean 4 repository are set up to use the `lean4-stage0`
-toolchain for editing files in `src` and the `lean4` toolchain for editing files in `tests`.
-
-Run the following commands to make `lean4` point at `stage1` and `lean4-stage0` point at `stage0`:
-```bash
-# in the Lean rootdir
-elan toolchain link lean4 build/release/stage1
-elan toolchain link lean4-stage0 build/release/stage0
-```
-
-You can also use the `+toolchain` shorthand (e.g. `lean +lean4-debug`) to switch
-toolchains on the spot. `lean4-mode` will automatically use the `lean` executable
-associated with the directory of the current file as long as `lean4-rootdir` is
-unset and `~/.elan/bin` is in your `exec-path`. Where Emacs sources the
-`exec-path` from can be a bit unclear depending on your configuration, so
-alternatively you can also set `lean4-rootdir` to `"~/.elan"` explicitly.
-
-You might find that debugging through elan, e.g. via `gdb lean`, disables some
-things like symbol autocompletion because at first only the elan proxy binary
-is loaded. You can instead pass the explicit path to `bin/lean` in your build
-folder to gdb, or use `gdb $(elan which lean)`.
-
-It is also possible to generate releases that others can use,
-simply by pushing a tag to your fork of the Lean 4 github repository
-(and waiting about an hour; check the `Actions` tab for completion).
-If you push `my-tag` to a fork in your github account `my_name`,
-you can then put `my_name/lean4:my-tag` in your `lean-toolchain` file in a project using `lake`.
-(You must use a tag name that does not start with a numeral, or contain `_`).
-
-### 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
-```
-code .
-```
-on the command line.
-
-You can use the `Refresh File Dependencies` command as in other projects to rebuild modules from inside VS Code but be aware that this does not trigger any non-Lake build targets.
-In particular, after updating `stage0/` (or fetching an update to it), you will want to invoke `make` directly to rebuild `stage0/bin/lean` as described in [building Lean](../make/index.md).
-You should then run the `Restart Server` command to update all open files and the server watchdog process as well.
-
-### `ccache`
-
-Lean's build process uses [`ccache`](https://ccache.dev/) if it is
-installed to speed up recompilation of the generated C code. Without
-`ccache`, you'll likely spend more time than necessary waiting on
-rebuilds - it's a good idea to make sure it's installed.
-
-### `prelude`
-Unlike most Lean projects, all submodules of the `Lean` module begin with the
-`prelude` keyword. This disables the automated import of `Init`, meaning that
-developers need to figure out their own subset of `Init` to import. This is done
-such that changing files in `Init` doesn't force a full rebuild of `Lean`.
-
-### Testing against Mathlib/Batteries
-You can test a Lean PR against Mathlib and Batteries by rebasing your PR
-on to `nightly-with-mathlib` branch. (It is fine to force push after rebasing.)
-CI will generate a branch of Mathlib and Batteries called `lean-pr-testing-NNNN`
-on the `leanprover-community/mathlib4-nightly-testing` fork of Mathlib.
-This branch uses the toolchain for your PR, and will report back to the Lean PR with results from Mathlib CI.
-See https://leanprover-community.github.io/contribute/tags_and_branches.html for more details.
-
-### Testing against the Lean Language Reference
-You can test a Lean PR against the reference manual by rebasing your PR
-on to `nightly-with-manual` branch. (It is fine to force push after rebasing.)
-CI will generate a branch of the reference manual called `lean-pr-testing-NNNN`
-in `leanprover/reference-manual`. This branch uses the toolchain for your PR,
-and will report back to the Lean PR with results from Mathlib CI.
-
-### Avoiding rebuilds for downstream projects
-
-If you want to test changes to Lean on downstream projects and would like to avoid rebuilding modules you have already built/fetched using the project's configured Lean toolchain, you can often do so as long as your build of Lean is close enough to that Lean toolchain (compatible .olean format including structure of all relevant environment extensions).
-
-To override the toolchain without rebuilding for a single command, for example `lake build` or `lake lean`, you can use the prefix
-```
-LEAN_GITHASH=$(lean --githash) lake +lean4 ...
-```
-Alternatively, use
-```
-export LEAN_GITHASH=$(lean --githash)
-export ELAN_TOOLCHAIN=lean4
-```
-to persist these changes for the lifetime of the current shell, which will affect any processes spawned from it such as VS Code started via `code .`.
-If you use a setup where you cannot directly start your editor from the command line, such as VS Code Remote, you might want to consider using [direnv](https://direnv.net/) together with an editor extension for it instead so that you can put the lines above into `.envrc`.

doc/dev/release_checklist.md

@@ -1,369 +0,0 @@
-# Releasing a stable version
-
-This checklist walks you through releasing a stable version.
-See below for the checklist for release candidates.
-
-We'll use `v4.6.0` as the intended release version as a running example.
-
-- Run `script/release_checklist.py v4.6.0` to check the status of the release.
-  This script is idempotent, and should be safe to run at any stage of the release process.
-  Note that as of v4.19.0, this script takes some autonomous actions, which can be prevented via `--dry-run`.
-- `git checkout releases/v4.6.0`
-  (This branch should already exist, from the release candidates.)
-- `git pull`
-- In `src/CMakeLists.txt`, verify you see
-  - `set(LEAN_VERSION_MINOR 6)` (for whichever `6` is appropriate)
-  - `set(LEAN_VERSION_IS_RELEASE 1)`
-  - (all of these should already be in place from the release candidates)
-- `git tag v4.6.0`
-- `git push $REMOTE v4.6.0`, where `$REMOTE` is the upstream Lean repository (e.g., `origin`, `upstream`)
-- Now wait, while CI runs.
-  - You can monitor this at `https://github.com/leanprover/lean4/actions/workflows/ci.yml`,
-    looking for the `v4.6.0` tag.
-  - This step can take up to two hours.
-  - If you are intending to cut the next release candidate on the same day,
-    you may want to start on the release candidate checklist now.
-- Next we need to prepare the release notes.
-  - If the stable release is identical to the last release candidate (this should usually be the case),
-    you can reuse the release notes that are already in the Lean Language Reference.
-  - If you want to regenerate the release notes,
-    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.
-- 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.
-  - In order to have the access rights to push to these repositories and merge PRs,
-    you will need to be a member of the `lean-release-managers` team at both `leanprover-community` and `leanprover`.
-    Contact Kim Morrison (@kim-em) to arrange access.
-  - For each of the repositories listed in `script/release_repos.yml`,
-    - Run `script/release_steps.py v4.6.0 <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.6.0`.
-      - Update the contents of `lean-toolchain` to `leanprover/lean4:v4.6.0`.
-      - In the `lakefile.toml` or `lakefile.lean`, if there are dependencies on specific version tags of dependencies, update them to the new tag.
-        If they depend on `main` or `master`, don't change this; you've just updated the dependency, so `lake update` will take care of modifying the manifest.
-      - Run `lake update`
-      - Commit the changes as `chore: bump toolchain to v4.6.0` and push.
-      - Create a PR with title "chore: bump toolchain to v4.6.0".
-    - Merge the PR once CI completes.
-    - Re-running `script/release_checklist.py` will then create the tag `v4.6.0` from `master`/`main` and push it (unless `toolchain-tag: false` in the `release_repos.yml` file)
-    - `script/release_checklist.py` will then merge the tag `v4.6.0` into the `stable` branch and push it (unless `stable-branch: false` in the `release_repos.yml` file).
-  - Special notes on repositories with exceptional requirements:
-    - `doc-gen4` has additional dependencies which we do not update at each toolchain release, although occasionally these break and need to be updated manually.
-    - `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)
-      - 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`. 
-    - `ProofWidgets4` uses a non-standard sequential version tagging scheme, e.g. `v0.0.29`, which does not refer to the toolchain being used.
-      You will need to identify the next available version number from https://github.com/leanprover-community/ProofWidgets4/releases,
-      and push a new tag after merging the PR to `main`.
-    - `mathlib4`:
-      - 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.
-    - `lean-fro.org`:
-      After updating the toolchains and running `lake update`, you must run `scripts/update.sh` to regenerate
-      the site content. This script updates generated files that depend on the Lean version.
-      The `release_steps.py` script handles this automatically.
-- An awkward situation that sometimes occurs (e.g. with Verso) is that the `master`/`main` branch has already been moved
-  to a nightly toolchain that comes *after* the stable toolchain we are
-  targeting. In this case it is necessary to create a branch `releases/v4.6.0` from the last commit which was on
-  an earlier toolchain, move that branch to the stable toolchain, and create the toolchain tag from that branch.
-- Run `script/release_checklist.py v4.6.0` one last time to check that everything is in order.
-- Finally, make an announcement!
-  This should go in https://leanprover.zulipchat.com/#narrow/stream/113486-announce, with topic `v4.6.0`.
-  Please see previous announcements for suggested language.
-  You will want a few bullet points for main topics from the release notes.
-  If there is a blog post, link to that from the zulip announcement.
-- Make sure that whoever is handling social media knows the release is out.
-
-## Time estimates:
-- Initial checks and push the tag: 10 minutes.
-- Waiting for the release: 120 minutes.
-- Preparing release notes: 10 minutes.
-- Bumping toolchains in downstream repositories, up to creating the Mathlib PR: 60 minutes.
-- Waiting for Mathlib CI and bors: 120 minutes.
-- Finalizing Mathlib tags and stable branch, and updating REPL: 20 minutes.
-- Posting announcement and/or blog post: 30 minutes.
-
-# Creating a release candidate.
-
-This checklist walks you through creating the first release candidate for a version of Lean.
-
-For subsequent release candidates, the process is essentially the same, but we start out with the `releases/v4.7.0` branch already created.
-
-We'll use `v4.7.0-rc1` as the intended release version in this example.
-
-- Decide which nightly release you want to turn into a release candidate.
-  We will use `nightly-2024-02-29` in this example.
-- It is essential to choose the nightly that will become the release candidate as early as possible, to avoid confusion.
-- Throughout this process you can use `script/release_checklist.py v4.7.0-rc1` to track progress.
-  This script will also try to do some steps autonomously. It is idempotent and safe to run at any point.
-  You can prevent it taking any actions using `--dry-run`.
-- It is essential that Batteries and Mathlib already have reviewed branches compatible with this nightly.
-  - Check that both Batteries and Mathlib's `bump/v4.7.0` branch contain `nightly-2024-02-29`
-    in their `lean-toolchain`.
-  - The steps required to reach that state are beyond the scope of this checklist, but see below!
-- Create the release branch from this nightly tag:
-    ```
-    git remote add nightly https://github.com/leanprover/lean4-nightly.git
-    git fetch nightly tag nightly-2024-02-29
-    git checkout nightly-2024-02-29
-    git checkout -b releases/v4.7.0
-    git push --set-upstream origin releases/v4.7.0
-    ```
-- In `src/CMakeLists.txt`,
-  - verify that you see `set(LEAN_VERSION_MINOR 7)` (for whichever `7` is appropriate); this should already have been updated when the development cycle began.
-  - change the `LEAN_VERSION_IS_RELEASE` line to `set(LEAN_VERSION_IS_RELEASE 1)` (this should be a change; on `master` and nightly releases it is always `0`).
-  - Commit your changes to `src/CMakeLists.txt`, and push.
-- `git tag v4.7.0-rc1`
-- `git push origin v4.7.0-rc1`
-- Now wait, while CI runs.
-  - The CI setup parses the tag to discover the `-rc1` special description, and passes it to `cmake` using a `-D` option. The `-rc1` doesn't need to be placed in the configuration file.
-  - You can monitor this at `https://github.com/leanprover/lean4/actions/workflows/ci.yml`, looking for the `v4.7.0-rc1` tag.
-  - This step can take up to two hours.
-- Verify that the release appears at https://github.com/leanprover/lean4/releases/, marked as a prerelease (this should have been done automatically by the CI release job).
-- Next we need to prepare the release notes.
-  - Run `script/release_notes.py --since v4.6.0` on the `releases/v4.7.0` branch,
-    which will report diagnostic messages on `stderr`
-    (including reporting commits that it couldn't associate with a PR, and hence will be omitted)
-    and then a chunk of markdown on `stdout`.
-    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.7.0.lean`.
-    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. 
-- Next, we will move a curated list of downstream repos to the release candidate.
-  - This assumes that for each repository either:
-    * There is already a *reviewed* branch `bump/v4.7.0` containing the required adaptations.
-      The preparation of this branch is beyond the scope of this document.
-    * 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`.
-      - Merge `origin/bump/v4.7.0` if relevant (i.e. `bump-branch: true` appears in `release_repos.yml`).
-      - Otherwise, you *may* need to merge `origin/nightly-testing`.
-      - Note that for `verso` and `reference-manual` development happens on `nightly-testing`, so
-        we will merge that branch into `bump_to_v4.7.0-rc1`, but it is essential in the GitHub interface that we do a rebase merge,
-        in order to preserve the history.
-      - Update the contents of `lean-toolchain` to `leanprover/lean4:v4.7.0-rc1`.
-      - In the `lakefile.toml` or `lakefile.lean`, if there are dependencies on `nightly-testing`, `bump/v4.7.0`, or specific version tags, update them to the new tag.
-        If they depend on `main` or `master`, don't change this; you've just updated the dependency, so `lake update` will take care of modifying the manifest.
-      - Run `lake update`
-      - Run `lake build && if lake check-test; then lake test; fi` to check things are working.
-      - Commit the changes as `chore: bump toolchain to v4.7.0-rc1` and push.
-      - Create a PR with title "chore: bump toolchain to v4.7.0-rc1".
-    - Merge the PR once CI completes. (Recall: for `verso` and `reference-manual` you will need to do a rebase merge.)
-    - Re-running `script/release_checklist.py` will then create the tag `v4.7.0-rc1` from `master`/`main` and push it (unless `toolchain-tag: false` in the `release_repos.yml` file)
-  - We do this for the same list of repositories as for stable releases, see above for notes about special cases.
-    As above, there are dependencies between these, and so the process above is iterative.
-    It greatly helps if you can merge the `bump/v4.7.0` PRs yourself!
-  - It is essential for Mathlib and Batteries CI that you then create the next `bump/v4.8.0` branch
-    for the next development cycle.
-    Set the `lean-toolchain` file on this branch to same `nightly` you used for this release.
-- Run `script/release_checklist.py v4.7.0-rc1` one last time to check that everything is in order.
-- Make an announcement!
-  This should go in https://leanprover.zulipchat.com/#narrow/stream/113486-announce, with topic `v4.7.0-rc1`.
-  Please see previous announcements for suggested language.
-  You will want a few bullet points for main topics from the release notes.
-  Please also make sure that whoever is handling social media knows the release is out.
-- Begin the next development cycle (i.e. for `v4.8.0`) on the Lean repository, by making a PR that:
-  - Uses branch name `dev_cycle_v4.8`.
-  - Updates `src/CMakeLists.txt` to say `set(LEAN_VERSION_MINOR 8)`
-  - Titled "chore: begin development cycle for v4.8.0"
-
-## Time estimates:
-Slightly longer than the corresponding steps for a stable release.
-Similar process, but more things go wrong.
-In particular, updating the downstream repositories is significantly more work
-(because we need to merge existing `bump/v4.7.0` branches, not just update a toolchain).
-
-# Preparing `bump/v4.7.0` branches
-
-While not part of the release process per se,
-this is a brief summary of the work that goes into updating Batteries/Aesop/Mathlib to new versions.
-
-Please read https://leanprover-community.github.io/contribute/tags_and_branches.html
-
-* Each repo has an unreviewed `nightly-testing` branch that
-  receives commits automatically from `master`, and
-  has its toolchain updated automatically for every nightly.
-  (Note: the aesop branch is not automated, and is updated on an as needed basis.)
-  As a consequence this branch is often broken.
-  A bot posts in the (private!) "Mathlib reviewers" stream on Zulip about the status of these branches.
-* We fix the breakages by committing directly to `nightly-testing`: there is no PR process.
-  * This can either be done by the person managing this process directly,
-    or by soliciting assistance from authors of files, or generally helpful people on Zulip!
-* Each repo has a `bump/v4.7.0` which accumulates reviewed changes adapting to new versions.
-* Once `nightly-testing` is working on a given nightly, say `nightly-2024-02-15`, we will create a PR to `bump/v4.7.0`.
-* For Mathlib, there is a script in `scripts/create-adaptation-pr.sh` that automates this process.
-* For Batteries and Aesop it is currently manual.
-* For all of these repositories, the process is the same:
-  * Make sure `bump/v4.7.0` is up to date with `master` (by merging `master`, no PR necessary)
-  * Create from `bump/v4.7.0` a `bump/nightly-2024-02-15` branch.
-  * In that branch, `git merge nightly-testing` to bring across changes from `nightly-testing`.
-  * Sanity check changes, commit, and make a PR to `bump/v4.7.0` from the `bump/nightly-2024-02-15` branch.
-  * Solicit review, merge the PR into `bump/v4.7.0`.
-* It is always okay to merge in the following directions:
-  `master` -> `bump/v4.7.0` -> `bump/nightly-2024-02-15` -> `nightly-testing`.
-  Please remember to push any merges you make to intermediate steps!
-
-# 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.
-This script should be run on the `releases/v4.7.0` branch.
-This will generate output for all commits since that tag.
-Note that there is output on both stderr, which should be manually reviewed,
-and on stdout, which should be manually copied into the `reference-manual` repository, in the file `Manual/Releases/v4.7.0.lean`.
-
-The output on stderr should mostly be about commits for which the script could not find an associated PR,
-usually because a PR was rebase-merged because it contained an update to stage0.
-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/do.md

@@ -0,0 +1,377 @@
+# The `do` notation
+
+Lean is a pure functional programming language, but you can write effectful code using the `do` embedded domain specific language (DSL). The following simple program prints two strings "hello" and "world" in the standard output and terminates with exit code 0. Note that the type of the program is `IO UInt32`. You can read this type as the type of values that perform input-output effects and produce a value of type `UInt32`.
+
+```lean
+def main : IO UInt32 := do
+  IO.println "hello"
+  IO.println "world"
+  return 0
+```
+The type of `IO.println` is `String → IO Unit`. That is, it is a function from `String` to `IO Unit` which indicates it may perform input-output effects and produce a value of type `Unit`. We often say that functions that may perform effects are *methods*.
+We also say a method application, such as `IO.println "hello"` is an *action*.
+Note that the examples above also demonstrates that braceless `do` blocks are whitespace sensitive.
+If you like `;`s and curly braces, you can write the example above as
+```lean
+def main : IO UInt32 := do {
+  IO.println "hello";
+  IO.println "world";
+  return 0;
+}
+```
+Semicolons can be used even when curly braces are not used. They are particularly useful when you want to "pack" more than one action in a single line.
+```lean
+def main : IO UInt32 := do
+  IO.println "hello"; IO.println "world"
+  return 0
+```
+Whitespace sensitivity in programming languages is a controversial topic
+among programmers. You should use your own style. We, the Lean developers, **love** the
+braceless and semicolon-free style.
+We believe it is clean and beautiful.
+
+The `do` DSL expands into the core Lean language. Let's inspect the different components using the commands `#print` and `#check`.
+
+```lean
+# def main : IO UInt32 := do
+#  IO.println "hello"
+#  IO.println "world"
+#  return 0
+
+#check IO.println "hello"
+-- IO Unit
+#print main
+-- Output contains the infix operator `>>=` and `pure`
+-- The following `set_option` disables notation such as `>>=` in the output
+set_option pp.notation false in
+#print main
+-- Output contains `bind` and `pure`
+#print bind
+-- bind : {m : Type u → Type v} → [self : Bind m] → {α β : Type u} →
+--        m α → (α → m β) → m β
+#print pure
+-- pure : {m : Type u → Type v} → [self : Pure m] → {α : Type u} →
+--        α → m α
+
+-- IO implements the type classes `Bind` and `Pure`.
+#check (inferInstance : Bind IO)
+#check (inferInstance : Pure IO)
+```
+The types of `bind` and `pure` may look daunting at first sight.
+They both have many implicit arguments. Let's focus first on the explicit arguments.
+`bind` has two explicit arguments `m α` and `α → m β`. The first one should
+be viewed as an action with effects `m` and producing a value of type `α`.
+The second is a function that takes a value of type `α` and produces an action
+with effects `m` and a value of type `β`. The result is `m β`. The method `bind` is composing
+these two actions. We often say `bind` is an abstract semicolon. The method `pure` converts
+a value `α` into an action that produces an action `m α`.
+
+Here is the same function being defined using `bind` and `pure` without the `do` DSL.
+```lean
+def main : IO UInt32 :=
+  bind (IO.println "hello") fun _ =>
+  bind (IO.println "world") fun _ =>
+  pure 0
+```
+
+The notations `let x <- action1; action2` and `let x ← action1; action2` are just syntax sugar for `bind action1 fun x => action2`.
+Here is a small example using it.
+```lean
+def isGreaterThan0 (x : Nat) : IO Bool := do
+  IO.println s!"value: {x}"
+  return x > 0
+
+def f (x : Nat) : IO Unit := do
+  let c <- isGreaterThan0 x
+  if c then
+    IO.println s!"{x} is greater than 0"
+  else
+    pure ()
+
+#eval f 10
+-- value: 10
+-- 10 is greater than 0
+```
+
+
+## Nested actions
+
+Note that we cannot write `if isGreaterThan0 x then ... else ...` because the condition in a `if-then-else` is a **pure** value without effects, but `isGreaterThan0 x` has type `IO Bool`. You can use the nested action notation to avoid this annoyance. Here is an equivalent definition for `f` using a nested action.
+```lean
+# def isGreaterThan0 (x : Nat) : IO Bool := do
+#  IO.println s!"x: {x}"
+#  return x > 0
+
+def f (x : Nat) : IO Unit := do
+  if (<- isGreaterThan0 x) then
+    IO.println s!"{x} is greater than 0"
+  else
+    pure ()
+
+#print f
+```
+Lean "lifts" the nested actions and introduces the `bind` for us.
+Here is an example with two nested actions. Note that both actions are executed
+even if `x = 0`.
+```lean
+# def isGreaterThan0 (x : Nat) : IO Bool := do
+#  IO.println s!"x: {x}"
+#  return x > 0
+
+def f (x y : Nat) : IO Unit := do
+  if (<- isGreaterThan0 x) && (<- isGreaterThan0 y) then
+    IO.println s!"{x} and {y} are greater than 0"
+  else
+    pure ()
+
+#eval f 0 10
+-- value: 0
+-- value: 10
+
+-- The function `f` above is equivalent to
+def g (x y : Nat) : IO Unit := do
+  let c1 <- isGreaterThan0 x
+  let c2 <- isGreaterThan0 y
+  if c1 && c2 then
+    IO.println s!"{x} and {y} are greater than 0"
+  else
+    pure ()
+
+theorem fgEqual : f = g :=
+  rfl -- proof by reflexivity
+```
+Here are two ways to achieve the short-circuit semantics in the example above
+```lean
+# def isGreaterThan0 (x : Nat) : IO Bool := do
+#  IO.println s!"x: {x}"
+#  return x > 0
+
+def f1 (x y : Nat) : IO Unit := do
+  if (<- isGreaterThan0 x <&&> isGreaterThan0 y) then
+    IO.println s!"{x} and {y} are greater than 0"
+  else
+    pure ()
+
+-- `<&&>` is the effectful version of `&&`
+-- Given `x y : IO Bool`, `x <&&> y` : m Bool`
+-- It only executes `y` if `x` returns `true`.
+
+#eval f1 0 10
+-- value: 0
+#eval f1 1 10
+-- value: 1
+-- value: 10
+-- 1 and 10 are greater than 0
+
+def f2 (x y : Nat) : IO Unit := do
+  if (<- isGreaterThan0 x) then
+    if (<- isGreaterThan0 y) then
+      IO.println s!"{x} and {y} are greater than 0"
+    else
+      pure ()
+  else
+    pure ()
+```
+
+## `if-then` notation
+
+In the `do` DSL, we can write `if c then action` as a shorthand for `if c then action else pure ()`. Here is the method `f2` using this shorthand.
+```lean
+# def isGreaterThan0 (x : Nat) : IO Bool := do
+#  IO.println s!"x: {x}"
+#  return x > 0
+
+def f2 (x y : Nat) : IO Unit := do
+  if (<- isGreaterThan0 x) then
+    if (<- isGreaterThan0 y) then
+      IO.println s!"{x} and {y} are greater than 0"
+```
+
+## Reassignments
+
+When writing effectful code, it is natural to think imperatively.
+For example, suppose we want to create an empty array `xs`,
+add `0` if some condition holds, add `1` if another condition holds,
+and then print it. In the following example, we use variable
+"shadowing" to simulate this kind of "update".
+
+```lean
+def f (b1 b2 : Bool) : IO Unit := do
+  let xs := #[]
+  let xs := if b1 then xs.push 0 else xs
+  let xs := if b2 then xs.push 1 else xs
+  IO.println xs
+
+#eval f true true
+-- #[0, 1]
+#eval f false true
+-- #[1]
+#eval f true false
+-- #[0]
+#eval f false false
+-- #[]
+```
+
+We can use tuples to simulate updates on multiple variables.
+
+```lean
+def f (b1 b2 : Bool) : IO Unit := do
+  let xs := #[]
+  let ys := #[]
+  let (xs, ys) := if b1 then (xs.push 0, ys) else (xs, ys.push 0)
+  let (xs, ys) := if b2 then (xs.push 1, ys) else (xs, ys.push 1)
+  IO.println s!"xs: {xs}, ys: {ys}"
+
+#eval f true false
+-- xs: #[0], ys: #[1]
+```
+
+We can also simulate the control-flow above using *join-points*.
+A join-point is a `let` that is always tail called and fully applied.
+The Lean compiler implements them using `goto`s.
+Here is the same example using join-points.
+
+```lean
+def f (b1 b2 : Bool) : IO Unit := do
+  let jp1 xs ys := IO.println s!"xs: {xs}, ys: {ys}"
+  let jp2 xs ys := if b2 then jp1 (xs.push 1) ys else jp1 xs (ys.push 1)
+  let xs := #[]
+  let ys := #[]
+  if b1 then jp2 (xs.push 0) ys else jp2 xs (ys.push 0)
+
+#eval f true false
+-- xs: #[0], ys: #[1]
+```
+
+You can capture complex control-flow using join-points.
+The `do` DSL offers the variable reassignment feature to make this kind of code more comfortable to write. In the following example, the `mut` modifier at `let mut xs := #[]` indicates that variable `xs` can be reassigned. The example contains two reassignments `xs := xs.push 0` and `xs := xs.push 1`. The reassignments are compiled using join-points. There is no hidden state being updated.
+
+```lean
+def f (b1 b2 : Bool) : IO Unit := do
+  let mut xs := #[]
+  if b1 then xs := xs.push 0
+  if b2 then xs := xs.push 1
+  IO.println xs
+
+#eval f true true
+-- #[0, 1]
+```
+The notation `x <- action` reassigns `x` with the value produced by the action. It is equivalent to `x := (<- action)`
+
+## Iteration
+
+The `do` DSL provides a unified notation for iterating over datastructures. Here are a few examples.
+
+```lean
+def sum (xs : Array Nat) : IO Nat := do
+  let mut s := 0
+  for x in xs do
+    IO.println s!"x: {x}"
+    s := s + x
+  return s
+
+#eval sum #[1, 2, 3]
+-- x: 1
+-- x: 2
+-- x: 3
+-- 6
+
+-- We can write pure code using the `do` DSL too.
+def sum' (xs : Array Nat) : Nat := do
+  let mut s := 0
+  for x in xs do
+    s := s + x
+  return s
+
+#eval sum' #[1, 2, 3]
+-- 6
+
+def sumEven (xs : Array Nat) : IO Nat := do
+  let mut s := 0
+  for x in xs do
+    if x % 2 == 0 then
+      IO.println s!"x: {x}"
+      s := s + x
+  return s
+
+#eval sumEven #[1, 2, 3, 6]
+-- x: 2
+-- x: 6
+-- 8
+
+def splitEvenOdd (xs : List Nat) : IO Unit := do
+  let mut evens := #[]
+  let mut odds  := #[]
+  for x in xs do
+    if x % 2 == 0 then
+      evens := evens.push x
+    else
+      odds := odds.push x
+  IO.println s!"evens: {evens}, odds: {odds}"
+
+#eval splitEvenOdd [1, 2, 3, 4]
+-- evens: #[2, 4], odds: #[1, 3]
+
+def findNatLessThan (x : Nat) (p : Nat → Bool) : IO Nat := do
+  -- [:x] is notation for the range [0, x)
+  for i in [:x] do
+    if p i then
+      return i -- `return` from the `do` block
+  throw (IO.userError "value not found")
+
+#eval findNatLessThan 10 (fun x => x > 5 && x % 4 == 0)
+-- 8
+
+def sumOddUpTo (xs : List Nat) (threshold : Nat) : IO Nat := do
+  let mut s := 0
+  for x in xs do
+    if x % 2 == 0 then
+      continue -- it behaves like the `continue` statement in imperative languages
+    IO.println s!"x: {x}"
+    s := s + x
+    if s > threshold then
+      break -- it behave like the `continue` statement in imperative languages
+  IO.println s!"result: {s}"
+  return s
+
+#eval sumOddUpTo [2, 3, 4, 11, 20, 31, 41, 51, 107] 40
+-- x: 3
+-- x: 11
+-- x: 31
+-- result: 45
+-- 45
+```
+
+TODO: describe `forIn`
+
+## Try-catch
+
+TODO
+
+## Pattern matching
+
+TODO
+
+## Monads
+
+TODO
+
+## ReaderT
+
+TODO
+
+## StateT
+
+TODO
+
+## StateRefT
+
+TODO
+
+## ExceptT
+
+TODO
+
+## MonadLift and automatic lifting
+
+TODO

doc/enum.md

@@ -0,0 +1,190 @@
+# Enumerated Types
+
+The simplest kind of inductive type is simply a type with a finite, enumerated list of elements.
+The following command declares the enumerated type `Weekday`.
+```lean
+inductive Weekday where
+  | sunday    : Weekday
+  | monday    : Weekday
+  | tuesday   : Weekday
+  | wednesday : Weekday
+  | thursday  : Weekday
+  | friday    : Weekday
+  | saturday  : Weekday
+```
+
+The `Weekday` type has 7 constructors/elements. The constructors live in the `Weekday` namespace
+Think of `sunday`, `monday`, …, `saturday` as being distinct elements of `Weekday`,
+with no other distinguishing properties.
+```lean
+# inductive Weekday where
+#  | sunday    : Weekday
+#  | monday    : Weekday
+#  | tuesday   : Weekday
+#  | wednesday : Weekday
+#  | thursday  : Weekday
+#  | friday    : Weekday
+#  | saturday  : Weekday
+#check Weekday.sunday   -- Weekday
+#check Weekday.monday   -- Weekday
+```
+
+You can define functions by pattern matching.
+The following function converts a `Weekday` into a natural number.
+```lean
+# inductive Weekday where
+#  | sunday    : Weekday
+#  | monday    : Weekday
+#  | tuesday   : Weekday
+#  | wednesday : Weekday
+#  | thursday  : Weekday
+#  | friday    : Weekday
+#  | saturday  : Weekday
+def natOfWeekday (d : Weekday) : Nat :=
+  match d with
+  | Weekday.sunday    => 1
+  | Weekday.monday    => 2
+  | Weekday.tuesday   => 3
+  | Weekday.wednesday => 4
+  | Weekday.thursday  => 5
+  | Weekday.friday    => 6
+  | Weekday.saturday  => 7
+
+#eval natOfWeekday Weekday.tuesday -- 3
+```
+
+It is often useful to group definitions related to a type in a namespace with the same name.
+For example, we can put the function above into the ``Weekday`` namespace.
+We are then allowed to use the shorter name when we open the namespace.
+
+In the following example, we define functions from ``Weekday`` to ``Weekday`` in the namespace `Weekday`.
+```lean
+# inductive Weekday where
+#  | sunday    : Weekday
+#  | monday    : Weekday
+#  | tuesday   : Weekday
+#  | wednesday : Weekday
+#  | thursday  : Weekday
+#  | friday    : Weekday
+#  | saturday  : Weekday
+namespace Weekday
+
+def next (d : Weekday) : Weekday :=
+  match d with
+  | sunday    => monday
+  | monday    => tuesday
+  | tuesday   => wednesday
+  | wednesday => thursday
+  | thursday  => friday
+  | friday    => saturday
+  | saturday  => sunday
+
+end Weekday
+```
+It is so common to start a definition with a `match` in Lean, that Lean provides a syntax sugar for it.
+```lean
+# inductive Weekday where
+#  | sunday    : Weekday
+#  | monday    : Weekday
+#  | tuesday   : Weekday
+#  | wednesday : Weekday
+#  | thursday  : Weekday
+#  | friday    : Weekday
+#  | saturday  : Weekday
+# namespace Weekday
+def previous : Weekday -> Weekday
+  | sunday    => saturday
+  | monday    => sunday
+  | tuesday   => monday
+  | wednesday => tuesday
+  | thursday  => wednesday
+  | friday    => thursday
+  | saturday  => friday
+# end Weekday
+```
+We can use the command `#eval` to test our definitions.
+```lean
+# inductive Weekday where
+#  | sunday    : Weekday
+#  | monday    : Weekday
+#  | tuesday   : Weekday
+#  | wednesday : Weekday
+#  | thursday  : Weekday
+#  | friday    : Weekday
+#  | saturday  : Weekday
+# namespace Weekday
+# def next (d : Weekday) : Weekday :=
+#  match d with
+#  | sunday    => monday
+#  | monday    => tuesday
+#  | tuesday   => wednesday
+#  | wednesday => thursday
+#  | thursday  => friday
+#  | friday    => saturday
+#  | saturday  => sunday
+# def previous : Weekday -> Weekday
+#  | sunday    => saturday
+#  | monday    => sunday
+#  | tuesday   => monday
+#  | wednesday => tuesday
+#  | thursday  => wednesday
+#  | friday    => thursday
+#  | saturday  => friday
+def toString : Weekday -> String
+  | sunday    => "Sunday"
+  | monday    => "Monday"
+  | tuesday   => "Tuesday"
+  | wednesday => "Wednesday"
+  | thursday  => "Thursday"
+  | friday    => "Friday"
+  | saturday  => "Saturday"
+
+#eval toString (next sunday)             -- "Monday"
+#eval toString (next tuesday)            -- "Wednesday"
+#eval toString (previous wednesday)      -- "Tuesday"
+#eval toString (next (previous sunday))  -- "Sunday"
+#eval toString (next (previous monday))  -- "Monday"
+-- ..
+# end Weekday
+```
+We can now prove the general theorem that ``next (previous d) = d`` for any weekday ``d``.
+The idea is to perform a proof by cases using `match`, and rely on the fact for each constructor both
+sides of the equality reduce to the same term.
+```lean
+# inductive Weekday where
+#  | sunday    : Weekday
+#  | monday    : Weekday
+#  | tuesday   : Weekday
+#  | wednesday : Weekday
+#  | thursday  : Weekday
+#  | friday    : Weekday
+#  | saturday  : Weekday
+# namespace Weekday
+# def next (d : Weekday) : Weekday :=
+#  match d with
+#  | sunday    => monday
+#  | monday    => tuesday
+#  | tuesday   => wednesday
+#  | wednesday => thursday
+#  | thursday  => friday
+#  | friday    => saturday
+#  | saturday  => sunday
+# def previous : Weekday -> Weekday
+#  | sunday    => saturday
+#  | monday    => sunday
+#  | tuesday   => monday
+#  | wednesday => tuesday
+#  | thursday  => wednesday
+#  | friday    => thursday
+#  | saturday  => friday
+theorem nextOfPrevious (d : Weekday) : next (previous d) = d :=
+  match d with
+  | sunday    => rfl
+  | monday    => rfl
+  | tuesday   => rfl
+  | wednesday => rfl
+  | thursday  => rfl
+  | friday    => rfl
+  | saturday  => rfl
+# end Weekday
+```

doc/examples/.gitignore

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

doc/examples/Certora2022/ex1.lean

@@ -1,22 +0,0 @@
-/- "Hello world" -/
-
-#eval "hello" ++ " " ++ "world"
--- "hello world"
-
-#check true
--- Bool
-
-def x := 10
-
-#eval x + 2
--- 12
-
-def double (x : Int) := 2*x
-
-#eval double 3
--- 6
-#check double
--- Int → Int
-example : double 4 = 8 := rfl
-
-

doc/examples/Certora2022/ex10.lean

@@ -1,19 +0,0 @@
-/- Dependent pattern matching -/
-
-inductive Vector (α : Type u) : Nat → Type u
-  | nil : Vector α 0
-  | cons : α → Vector α n → Vector α (n+1)
-
-infix:67 "::" => Vector.cons
-
-def Vector.zip : Vector α n → Vector β n → Vector (α × β) n
-  | nil, nil => nil
-  | a::as, b::bs => (a, b) :: zip as bs
-
-#print Vector.zip
-/-
-def Vector.zip.{u_1, u_2} : {α : Type u_1} → {n : Nat} → {β : Type u_2} → Vector α n → Vector β n → Vector (α × β) n :=
-fun {α} {n} {β} x x_1 =>
-  Vector.brecOn (motive := fun {n} x => {β : Type u_2} → Vector β n → Vector (α × β) n) x
-    ...
--/

doc/examples/Certora2022/ex11.lean

@@ -1,22 +0,0 @@
-/- Structures -/
-
-structure Point where
-  x : Int := 0
-  y : Int := 0
-  deriving Repr
-
-#eval Point.x (Point.mk 10 20)
--- 10
-
-#eval { x := 10, y := 20 : Point }
-
-def p : Point := { y := 20 }
-
-#eval p.x
-#eval p.y
-#eval { p with x := 5 }
--- { x := 5, y := 20 }
-
-structure Point3D extends Point where
-  z : Int
-

doc/examples/Certora2022/ex12.lean

@@ -1,28 +0,0 @@
-/- Type classes -/
-namespace Example
-
-class ToString (α : Type u) where
-  toString : α → String
-
-#check @ToString.toString
--- {α : Type u_1} → [self : ToString α] → α → String
-
-instance : ToString String where
-  toString s := s
-
-instance : ToString Bool where
-  toString b := if b then "true" else "false"
-
-#eval ToString.toString "hello"
-export ToString (toString)
-#eval toString true
--- "true"
--- #eval toString (true, "hello") -- Error
-
-instance [ToString α] [ToString β] : ToString (α × β) where
-  toString p := "(" ++ toString p.1 ++ ", " ++ toString p.2 ++ ")"
-
-#eval toString (true, "hello")
--- "(true, hello)"
-
-end Example

doc/examples/Certora2022/ex13.lean

@@ -1,44 +0,0 @@
-/- Type classes are heavily used in Lean -/
-namespace Example
-
-class Mul (α : Type u) where
-  mul : α → α → α
-
-infixl:70 " * " => Mul.mul
-
-def double [Mul α] (a : α) := a * a
-
-class Semigroup (α : Type u) extends Mul α where
-  mul_assoc : ∀ a b c : α, (a * b) * c = a * (b * c)
-
-instance : Semigroup Nat where
-  mul := Nat.mul
-  mul_assoc := Nat.mul_assoc
-
-#eval double 5
-
-class Functor (f : Type u → Type v) : Type (max (u+1) v) where
-  map : (α → β) → f α → f β
-
-infixr:100 " <$> " => Functor.map
-
-class LawfulFunctor (f : Type u → Type v) [Functor f] : Prop where
-  id_map   (x : f α) : id <$> x = x
-  comp_map (g : α → β) (h : β → γ) (x : f α) :(h ∘ g) <$> x = h <$> g <$> x
-
-end Example
-
-/-
-`Deriving instances automatically`
-
-We have seen `deriving Repr` in a few examples.
-It is an instance generator.
-Lean comes equipped with generators for the following classes.
-`Repr`, `Inhabited`, `BEq`, `DecidableEq`,
-`Hashable`, `Ord`, `FromToJson`, `SizeOf`
--/
-
-inductive Tree (α : Type u) where
-  | leaf (val : α)
-  | node (left right : Tree α)
-  deriving DecidableEq, Ord, Inhabited, Repr

doc/examples/Certora2022/ex14.lean

@@ -1,31 +0,0 @@
-/- Tactics -/
-
-example : p → q → p ∧ q ∧ p := by
-  intro hp hq
-  apply And.intro
-  exact hp
-  apply And.intro
-  exact hq
-  exact hp
-
-example : p → q → p ∧ q ∧ p := by
-  intro hp hq; apply And.intro hp; exact And.intro hq hp
-
-/- Structuring proofs -/
-
-example : p → q → p ∧ q ∧ p := by
-  intro hp hq
-  apply And.intro
-  case left => exact hp
-  case right =>
-    apply And.intro
-    case left => exact hq
-    case right => exact hp
-
-example : p → q → p ∧ q ∧ p := by
-  intro hp hq
-  apply And.intro
-  . exact hp
-  . apply And.intro
-    . exact hq
-    . exact hp

doc/examples/Certora2022/ex15.lean

@@ -1,19 +0,0 @@
-/- intro tactic variants -/
-
-example (p q : α → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by
-  intro h
-  match h with
-  | Exists.intro w (And.intro hp hq) => exact Exists.intro w (And.intro hq hp)
-
-example (p q : α → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by
-  intro (Exists.intro _ (And.intro hp hq))
-  exact Exists.intro _ (And.intro hq hp)
-
-example (p q : α → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by
-  intro ⟨_, hp, hq⟩
-  exact ⟨_, hq, hp⟩
-
-example (α : Type) (p q : α → Prop) : (∃ x, p x ∨ q x) → ∃ x, q x ∨ p x := by
-  intro
-    | ⟨_, .inl h⟩ => exact ⟨_, .inr h⟩
-    | ⟨_, .inr h⟩ => exact ⟨_, .inl h⟩

doc/examples/Certora2022/ex16.lean

@@ -1,12 +0,0 @@
-/- Inaccessible names -/
-
-example : ∀ x y : Nat, x = y → y = x := by
-  intros
-  apply Eq.symm
-  assumption
-
-example : ∀ x y : Nat, x = y → y = x := by
-  intros
-  apply Eq.symm
-  rename_i a b hab
-  exact hab

doc/examples/Certora2022/ex17.lean

@@ -1,19 +0,0 @@
-/- More tactics -/
-
-example (p q : Nat → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by
-  intro h
-  cases h with
-  | intro x hpq =>
-    cases hpq with
-    | intro hp hq =>
-      exists x
-
-example : p ∧ q → q ∧ p := by
-  intro p
-  cases p
-  constructor <;> assumption
-
-example : p ∧ ¬ p → q := by
-  intro h
-  cases h
-  contradiction

doc/examples/Certora2022/ex18.lean

@@ -1,20 +0,0 @@
-/- Structuring proofs (cont.) -/
-
-example : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := by
-  intro h
-  have hp : p := h.left
-  have hqr : q ∨ r := h.right
-  show (p ∧ q) ∨ (p ∧ r)
-  cases hqr with
-  | inl hq => exact Or.inl ⟨hp, hq⟩
-  | inr hr => exact Or.inr ⟨hp, hr⟩
-
-example : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := by
-  intro ⟨hp, hqr⟩
-  cases hqr with
-  | inl hq =>
-    have := And.intro hp hq
-    apply Or.inl; exact this
-  | inr hr =>
-    have := And.intro hp hr
-    apply Or.inr; exact this

doc/examples/Certora2022/ex19.lean

@@ -1,10 +0,0 @@
-/- Tactic combinators -/
-
-example : p → q → r → p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := by
-  intros
-  repeat (any_goals constructor)
-  all_goals assumption
-
-example : p → q → r → p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := by
-  intros
-  repeat (any_goals (first | assumption | constructor))

doc/examples/Certora2022/ex2.lean

@@ -1,14 +0,0 @@
-/- First-class functions -/
-
-def twice (f : Nat → Nat) (a : Nat) :=
-  f (f a)
-
-#check twice
--- (Nat → Nat) → Nat → Nat
-
-#eval twice (fun x => x + 2) 10
-
-theorem twice_add_2 (a : Nat) : twice (fun x => x + 2) a = a + 4 := rfl
-
--- `(· + 2)` is syntax sugar for `(fun x => x + 2)`.
-#eval twice (· + 2) 10

doc/examples/Certora2022/ex20.lean

@@ -1,22 +0,0 @@
-/- Rewriting -/
-
-example (f : Nat → Nat) (k : Nat) (h₁ : f 0 = 0) (h₂ : k = 0) : f k = 0 := by
-  rw [h₂] -- replace k with 0
-  rw [h₁] -- replace f 0 with 0
-
-example (f : Nat → Nat) (k : Nat) (h₁ : f 0 = 0) (h₂ : k = 0) : f k = 0 := by
-  rw [h₂, h₁]
-
-example (f : Nat → Nat) (a b : Nat) (h₁ : a = b) (h₂ : f a = 0) : f b = 0 := by
-  rw [← h₁, h₂]
-
-example (f : Nat → Nat) (a : Nat) (h : 0 + a = 0) : f a = f 0 := by
-  rw [Nat.zero_add] at h
-  rw [h]
-
-def Tuple (α : Type) (n : Nat) :=
-  { as : List α // as.length = n }
-
-example (n : Nat) (h : n = 0) (t : Tuple α n) : Tuple α 0 := by
-  rw [h] at t
-  exact t

doc/examples/Certora2022/ex21.lean

@@ -1,21 +0,0 @@
-/- Simplifier -/
-
-example (p : Nat → Prop) : (x + 0) * (0 + y * 1 + z * 0) = x * y := by
-  simp
-
-example (p : Nat → Prop) (h : p (x * y)) : p ((x + 0) * (0 + y * 1 + z * 0)) := by
-  simp; assumption
-
-example (p : Nat → Prop) (h : p ((x + 0) * (0 + y * 1 + z * 0))) : p (x * y) := by
-  simp at h; assumption
-
-def f (m n : Nat) : Nat :=
-  m + n + m
-
-example (h : n = 1) (h' : 0 = m) : (f m n) = n := by
-  simp [h, ←h', f]
-
-example (p : Nat → Prop) (h₁ : x + 0 = x') (h₂ : y + 0 = y')
-        : x + y + 0 = x' + y' := by
-  simp at *
-  simp [*]

doc/examples/Certora2022/ex22.lean

@@ -1,13 +0,0 @@
-/- Simplifier -/
-
-def mk_symm (xs : List α) :=
-  xs ++ xs.reverse
-
-@[simp] theorem reverse_mk_symm : (mk_symm xs).reverse = mk_symm xs := by
-  simp [mk_symm]
-
-theorem tst : (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse := by
-  simp
-
-#print tst
--- Lean reverse_mk_symm, and List.reverse_append

doc/examples/Certora2022/ex23.lean

@@ -1,26 +0,0 @@
-/- split tactic -/
-
-def f (x y z : Nat) : Nat :=
-  match x, y, z with
-  | 5, _, _ => y
-  | _, 5, _ => y
-  | _, _, 5 => y
-  | _, _, _ => 1
-
-example : x ≠ 5 → y ≠ 5 → z ≠ 5 → z = w → f x y w = 1 := by
-  intros
-  simp [f]
-  split
-  . contradiction
-  . contradiction
-  . contradiction
-  . rfl
-
-def g (xs ys : List Nat) : Nat :=
-  match xs, ys with
-  | [a, b], _ => a+b+1
-  | _, [b, c] => b+1
-  | _, _      => 1
-
-example (xs ys : List Nat) (h : g xs ys = 0) : False := by
-  unfold g at h; split at h <;> simp_arith at h

doc/examples/Certora2022/ex24.lean

@@ -1,9 +0,0 @@
-/- induction tactic -/
-
-example (as : List α) (a : α) : (as.concat a).length = as.length + 1 := by
-  induction as with
-  | nil => rfl
-  | cons _ xs ih => simp [List.concat, ih]
-
-example (as : List α) (a : α) : (as.concat a).length = as.length + 1 := by
-  induction as <;> simp! [*]

doc/examples/Certora2022/ex3.lean

@@ -1,59 +0,0 @@
-/- Enumerated types -/
-
-inductive Weekday where
-  | sunday | monday | tuesday | wednesday
-  | thursday | friday | saturday
-
-#check Weekday.sunday
--- Weekday
-
-open Weekday
-#check sunday
-
-def natOfWeekday (d : Weekday) : Nat :=
-  match d with
-  | sunday    => 1
-  | monday    => 2
-  | tuesday   => 3
-  | wednesday => 4
-  | thursday  => 5
-  | friday    => 6
-  | saturday  => 7
-
-def Weekday.next (d : Weekday) : Weekday :=
-  match d with
-  | sunday    => monday
-  | monday    => tuesday
-  | tuesday   => wednesday
-  | wednesday => thursday
-  | thursday  => friday
-  | friday    => saturday
-  | saturday  => sunday
-
-def Weekday.previous : Weekday → Weekday
-  | sunday    => saturday
-  | monday    => sunday
-  | tuesday   => monday
-  | wednesday => tuesday
-  | thursday  => wednesday
-  | friday    => thursday
-  | saturday  => friday
-
-/- Proving theorems using tactics -/
-
-theorem Weekday.next_previous (d : Weekday) : d.next.previous = d :=
-  match d with
-  | sunday    => rfl
-  | monday    => rfl
-  | tuesday   => rfl
-  | wednesday => rfl
-  | thursday  => rfl
-  | friday    => rfl
-  | saturday  => rfl
-
-theorem Weekday.next_previous' (d : Weekday) : d.next.previous = d := by -- switch to tactic mode
-  cases d -- Creates 7 goals
-  rfl; rfl; rfl; rfl; rfl; rfl; rfl
-
-theorem Weekday.next_previous'' (d : Weekday) : d.next.previous = d := by
-  cases d <;> rfl

doc/examples/Certora2022/ex4.lean

@@ -1,20 +0,0 @@
-/- What is the type of Nat? -/
-
-#check 0
--- Nat
-#check Nat
--- Type
-#check Type
--- Type 1
-#check Type 1
--- Type 2
-#check Eq.refl 2
--- 2 = 2
-#check 2 = 2
--- Prop
-#check Prop
--- Type
-
-example : Prop = Sort 0   := rfl
-example : Type = Sort 1   := rfl
-example : Type 1 = Sort 2 := rfl

doc/examples/Certora2022/ex5.lean

@@ -1,21 +0,0 @@
-/- Implicit arguments and universe polymorphism -/
-
-def f (α β : Sort u) (a : α) (b : β) : α := a
-
-#eval f Nat String 1 "hello"
--- 1
-
-def g {α β : Sort u} (a : α) (b : β) : α := a
-
-#eval g 1 "hello"
-
-def h (a : α) (b : β) : α := a
-
-#check g
--- ?m.1 → ?m.2 → ?m.1
-#check @g
--- {α β : Sort u} → α → β → α
-#check @h
--- {α : Sort u_1} → {β : Sort u_2} → α → β → α
-#check g (α := Nat) (β := String)
--- Nat → String → Nat

doc/examples/Certora2022/ex6.lean

@@ -1,14 +0,0 @@
-/- Inductive Types -/
-
-inductive Tree (β : Type v) where
-  | leaf
-  | node (left : Tree β) (key : Nat) (value : β) (right : Tree β)
-  deriving Repr
-
-#eval Tree.node .leaf 10 true .leaf
--- Tree.node Tree.leaf 10 true Tree.leaf
-
-inductive Vector (α : Type u) : Nat → Type u
-  | nil : Vector α 0
-  | cons : α → Vector α n → Vector α (n+1)
-

doc/examples/Certora2022/ex7.lean

@@ -1,25 +0,0 @@
-/- Recursive functions -/
-
-#print Nat -- Nat is an inductive datatype
-
-def fib (n : Nat) : Nat :=
-  match n with
-  | 0 => 1
-  | 1 => 1
-  | n+2 => fib (n+1) + fib n
-
-example : fib 5 = 8 := rfl
-
-example : fib (n+2) = fib (n+1) + fib n := rfl
-
-#print fib
-/-
-def fib : Nat → Nat :=
-fun n =>
-  Nat.brecOn n fun n f =>
-    (match (motive := (n : Nat) → Nat.below n → Nat) n with
-      | 0 => fun x => 1
-      | 1 => fun x => 1
-      | Nat.succ (Nat.succ n) => fun x => x.fst.fst + x.fst.snd.fst.fst)
-      f
--/

doc/examples/Certora2022/ex8.lean

@@ -1,25 +0,0 @@
-/- Well-founded recursion -/
-
-def ack : Nat → Nat → Nat
-  | 0,   y   => y+1
-  | x+1, 0   => ack x 1
-  | x+1, y+1 => ack x (ack (x+1) y)
-termination_by x y => (x, y)
-
-def sum (a : Array Int) : Int :=
-  let rec go (i : Nat) :=
-     if _ : i < a.size then
-        a[i] + go (i+1)
-     else
-        0
-  termination_by a.size - i
-  go 0
-
-set_option pp.proofs true
-#print sum.go
-/-
-def sum.go : Array Int → Nat → Int :=
-fun a =>
-  WellFounded.fix (sum.go.proof_1 a) fun i a_1 =>
-    if h : i < Array.size a then Array.getOp a i + a_1 (i + 1) (sum.go.proof_2 a i h) else 0
--/

doc/examples/Certora2022/ex9.lean

@@ -1,44 +0,0 @@
-/- Mutual recursion -/
-
-inductive Term where
- | const : String → Term
- | app   : String → List Term → Term
-
-namespace Term
-mutual
- def numConsts : Term → Nat
-   | const _ => 1
-   | app _ cs => numConstsLst cs
-
- def numConstsLst : List Term → Nat
-   | [] => 0
-   | c :: cs => numConsts c + numConstsLst cs
-end
-
-mutual
-  def replaceConst (a b : String) : Term → Term
-   | const c => if a = c then const b else const c
-   | app f cs => app f (replaceConstLst a b cs)
-
-  def replaceConstLst (a b : String) : List Term → List Term
-   | [] => []
-   | c :: cs => replaceConst a b c :: replaceConstLst a b cs
-end
-
-/- Mutual recursion in theorems -/
-
-mutual
-  theorem numConsts_replaceConst (a b : String) (e : Term)
-            : numConsts (replaceConst a b e) = numConsts e := by
-    match e with
-    | const c => simp [replaceConst]; split <;> simp [numConsts]
-    | app f cs => simp [replaceConst, numConsts, numConsts_replaceConstLst a b cs]
-
-  theorem numConsts_replaceConstLst (a b : String) (es : List Term)
-            : numConstsLst (replaceConstLst a b es) = numConstsLst es := by
-    match es with
-    | [] => simp [replaceConstLst, numConstsLst]
-    | c :: cs =>
-      simp [replaceConstLst, numConstsLst, numConsts_replaceConst a b c,
-            numConsts_replaceConstLst a b cs]
-end

doc/examples/ICERM2022/ctor.lean

@@ -1,45 +0,0 @@
-import Lean
-
-open Lean Meta
-
-def ctor (mvarId : MVarId) (idx : Nat) : MetaM (List MVarId) := do
-  /- Set `MetaM` context using `mvarId` -/
-  mvarId.withContext do
-    /- Fail if the metavariable is already assigned. -/
-    mvarId.checkNotAssigned `ctor
-    /- Retrieve the target type, instantiateMVars, and use `whnf`. -/
-    let target ← mvarId.getType'
-    let .const declName us := target.getAppFn
-      | throwTacticEx `ctor mvarId "target is not an inductive datatype"
-    let .inductInfo { ctors, .. } ← getConstInfo declName
-      | throwTacticEx `ctor mvarId "target is not an inductive datatype"
-    if idx = 0 then
-      throwTacticEx `ctor mvarId "invalid index, it must be > 0"
-    else if h : idx - 1 < ctors.length then
-      mvarId.apply (.const ctors[idx - 1] us)
-    else
-      throwTacticEx `ctor mvarId "invalid index, inductive datatype has only {ctors.length} constructors"
-
-open Elab Tactic
-
-elab "ctor" idx:num : tactic =>
-  liftMetaTactic (ctor · idx.getNat)
-
-example (p : Prop) : p := by
-  ctor 1 -- Error
-
-example (h : q) : p ∨ q := by
-  ctor 0 -- Error
-  exact h
-
-example (h : q) : p ∨ q := by
-  ctor 3 -- Error
-  exact h
-
-example (h : q) : p ∨ q := by
-  ctor 2
-  exact h
-
-example (h : q) : p ∨ q := by
-  ctor 1
-  exact h -- Error