Compare commits

..

1 Commits

Author SHA1 Message Date
Henrik Böving
406762f38f perf: annotate our allocators as such 2025-12-27 22:49:23 +00:00
8684 changed files with 25333 additions and 96168 deletions

View File

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

View File

@@ -13,54 +13,12 @@ These comments explain the scripts' behavior, which repositories get special han
## Arguments
- `version`: The version to release (e.g., v4.24.0)
## Release Notes (Required for -rc1 releases)
For first release candidates (`-rc1`), you must create release notes BEFORE the reference-manual toolchain bump PR can be merged.
**Steps to create release notes:**
1. Generate the release notes:
```bash
cd /path/to/lean4
python3 script/release_notes.py --since <previous_version> > /tmp/release-notes-<version>.md
```
Replace `<previous_version>` with the last stable release (e.g., `v4.27.0` when releasing `v4.28.0-rc1`).
2. Review `/tmp/release-notes-<version>.md` for common issues:
- **Unterminated code blocks**: Look for code fences that aren't closed. Fetch original PR with `gh pr view <number>` to repair.
- **Truncated descriptions**: Some may end mid-sentence. Complete them from the original PR.
- **Markdown issues**: Other syntax problems that could cause parsing errors.
3. Create the release notes file in the reference-manual repository:
- File path: `Manual/Releases/v<version>.lean` (e.g., `v4_28_0.lean`)
- Use Verso format with proper imports and `#doc (Manual)` block
- **Use `#` for headers, not `##`** (Verso uses level 1 for subsections)
- **Use plain ` ``` ` not ` ```lean `** (the latter executes code)
- **Wrap underscore identifiers in backticks**: `` `bv_decide` `` not `bv_decide`
4. Update `Manual/Releases.lean`:
- Add import: `import Manual.Releases.«v4_28_0»`
- Add include: `{include 0 Manual.Releases.«v4_28_0»}`
5. Build to verify: `lake build Manual.Releases.v4_28_0`
6. Create a **separate PR** for release notes (not bundled with toolchain bump):
```bash
git checkout -b v<version>-release-notes
gh pr create --title "doc: add v<version> release notes"
```
For subsequent RCs (`-rc2`, etc.) and stable releases, just update the version number in the existing release notes file title.
See `doc/dev/release_checklist.md` section "Writing the release notes" for full details.
## Process
1. Run `script/release_checklist.py {version}` to check the current status
2. **CRITICAL: If preliminary lean4 checks fail, STOP immediately and alert the user**
- Check for: release branch exists, CMake version correct, tag exists, release page exists, release notes file exists
- Check for: release branch exists, CMake version correct, tag exists, release page exists, release notes exist
- **IMPORTANT**: The release page is created AUTOMATICALLY by CI after pushing the tag - DO NOT create it manually
- **IMPORTANT**: For -rc1 releases, release notes must be created before proceeding
- Do NOT create any PRs or proceed with repository updates if these checks fail
3. Create a todo list tracking all repositories that need updates
4. **CRITICAL RULE: You can ONLY run `release_steps.py` for a repository if `release_checklist.py` explicitly says to do so**
@@ -103,38 +61,6 @@ Every time you run `release_checklist.py`, you MUST:
This summary should be provided EVERY time you run the checklist, not just after creating new PRs.
The user needs to see the complete picture of what's waiting for review.
## Checking PR Status When Asked
When the user asks for "status" or you need to report on PRs between checklist runs:
- **ALWAYS check actual PR state** using `gh pr view <number> --repo <repo> --json state,mergedAt`
- Do NOT rely on cached CI results or previous checklist output
- The user may have merged PRs since your last check
- Report which PRs are MERGED, which are OPEN with CI status, and which are still pending
- After discovering merged PRs, rerun `release_checklist.py` to advance the release process
## Nightly Infrastructure
The nightly build system uses branches and tags across two repositories:
- `leanprover/lean4` has **branches** `nightly` and `nightly-with-mathlib` tracking the latest nightly builds
- `leanprover/lean4-nightly` has **dated tags** like `nightly-2026-01-23`
When a nightly succeeds with mathlib, all three should point to the same commit. Don't confuse these: branches are in the main lean4 repo, dated tags are in lean4-nightly.
## 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.
## Error Handling
**CRITICAL**: If something goes wrong or a command fails:

View File

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

View File

@@ -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`.

View File

@@ -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.

View File

@@ -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)

View File

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

View File

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

View File

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

View File

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

View File

@@ -7,7 +7,7 @@ jobs:
runs-on: ubuntu-latest
steps:
- name: Checkout
uses: actions/checkout@v6
uses: actions/checkout@v5
with:
# the default is to use a virtual merge commit between the PR and master: just use the PR
ref: ${{ github.event.pull_request.head.sha }}

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

2
.gitignore vendored
View File

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

View File

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

View File

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

View File

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

View File

@@ -30,7 +30,7 @@ We'll use `v4.6.0` as the intended release version as a running example.
run `script/release_notes.py --since v4.5.0` on the `releases/v4.6.0` branch,
and see the section "Writing the release notes" below for more information.
- Release notes live in https://github.com/leanprover/reference-manual, in e.g. `Manual/Releases/v4.6.0.lean`.
It's best if you update these at the same time as you update the `lean-toolchain` for the `reference-manual` repository, see below.
It's best if you update these at the same time as a you update the `lean-toolchain` for the `reference-manual` repository, see below.
- Go to https://github.com/leanprover/lean4/releases and verify that the `v4.6.0` release appears.
- Verify on Github that "Set as the latest release" is checked.
- Next, we will move a curated list of downstream repos to the latest stable release.
@@ -54,7 +54,7 @@ We'll use `v4.6.0` as the intended release version as a running example.
- `verso`:
- The `subverso` dependency is unusual in that it needs to be compatible with _every_ Lean release simultaneously.
Usually you don't need to do anything.
If you think something is wrong here, please contact David Thrane Christiansen (@david-christiansen)
If you think something is wrong here please contact David Thrane Christiansen (@david-christiansen)
- Warnings during `lake update` and `lake build` are expected.
- `reference-manual`: the release notes generated by `script/release_notes.py` as described above must be included in
`Manual/Releases/v4.6.0.lean`, and `import` and `include` statements adding in `Manual/Releases.lean`.
@@ -65,14 +65,7 @@ We'll use `v4.6.0` as the intended release version as a running example.
- The `lakefile.toml` should always refer to dependencies via their `main` or `master` branch,
not a toolchain tag
(with the exception of `ProofWidgets4`, which *must* use a sequential version tag).
- **Important:** After creating and pushing the ProofWidgets4 tag (see above),
the mathlib4 lakefile must be updated to reference the new tag (e.g. `v0.0.87`).
The `release_steps.py` script handles this automatically by looking up the latest
ProofWidgets4 tag compatible with the target toolchain.
- Push the PR branch to the main Mathlib repository rather than a fork, or CI may not work reliably
- The "Verify Transient and Automated Commits" CI check on toolchain bump PRs can be ignored —
it often fails on automated commits (`x:` prefixed) from the nightly-testing history that can't be
reproduced in CI. This does not block merging.
- `repl`:
There are two copies of `lean-toolchain`/`lakefile.lean`:
in the root, and in `test/Mathlib/`. Edit both, and run `lake update` in both directories.
@@ -153,9 +146,6 @@ We'll use `v4.7.0-rc1` as the intended release version in this example.
* The repository does not need any changes to move to the new version.
* Note that sometimes there are *unreviewed* but necessary changes on the `nightly-testing` branch of the repository.
If so, you will need to merge these into the `bump_to_v4.7.0-rc1` branch manually.
* The `nightly-testing` branch may also contain temporary fix scripts (e.g. `fix_backward_defeq.py`,
`fix_deprecations.py`) that were used to adapt to breaking changes during the nightly cycle.
These should be reviewed and removed if no longer needed, as they can interfere with CI checks.
- For each of the repositories listed in `script/release_repos.yml`,
- Run `script/release_steps.py v4.7.0-rc1 <repo>` (e.g. replacing `<repo>` with `batteries`), which will walk you through the following steps:
- Create a new branch off `master`/`main` (as specified in the `branch` field), called `bump_to_v4.7.0-rc1`.
@@ -228,21 +218,6 @@ Please read https://leanprover-community.github.io/contribute/tags_and_branches.
# Writing the release notes
Release notes content is only written for the first release candidate (`-rc1`). For subsequent RCs and stable releases,
just update the title in the existing release notes file (see "Release notes title format" below).
## Release notes title format
The title in the `#doc (Manual)` line must follow these formats:
- **For -rc1**: `"Lean 4.7.0-rc1 (2024-03-15)"` — Include the RC suffix and the release date
- **For -rc2, -rc3, etc.**: `"Lean 4.7.0-rc2 (2024-03-20)"` — Update the RC number and date
- **For stable release**: `"Lean 4.7.0 (2024-04-01)"` — Remove the RC suffix but keep the date
The date should be the actual date when the tag was pushed (or when CI completed and created the release page).
## Generating the release notes
Release notes are automatically generated from the commit history, using `script/release_notes.py`.
Run this as `script/release_notes.py --since v4.6.0`, where `v4.6.0` is the *previous* release version.
@@ -257,113 +232,4 @@ Some judgement is required here: ignore commits which look minor,
but manually add items to the release notes for significant PRs that were rebase-merged.
There can also be pre-written entries in `./releases_drafts`, which should be all incorporated in the release notes and then deleted from the branch.
## Reviewing and fixing the generated markdown
Before adding the release notes to the reference manual, carefully review the generated markdown for these common issues:
1. **Unterminated code blocks**: PR descriptions sometimes have unclosed code fences. Look for code blocks
that don't have a closing ` ``` `. If found, fetch the original PR description with `gh pr view <number>`
and repair the code block with the complete content.
2. **Truncated descriptions**: Some PR descriptions may end abruptly mid-sentence. Review these and complete
the descriptions based on the original PR.
3. **Markdown syntax issues**: Check for other markdown problems that could cause parsing errors.
## Creating the release notes file
The release notes go in `Manual/Releases/v4_7_0.lean` in the reference-manual repository.
The file structure must follow the Verso format:
```lean
/-
Copyright (c) 2025 Lean FRO LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: <Your Name>
-/
import VersoManual
import Manual.Meta
import Manual.Meta.Markdown
open Manual
open Verso.Genre
open Verso.Genre.Manual
open Verso.Genre.Manual.InlineLean
#doc (Manual) "Lean 4.7.0-rc1 (2024-03-15)" =>
%%%
tag := "release-v4.7.0"
file := "v4.7.0"
%%%
<release notes content here>
```
**Important formatting rules for Verso:**
- Use `#` for section headers inside the document, not `##` (Verso uses header level 1 for subsections)
- Use plain ` ``` ` for code blocks, not ` ```lean ` (the latter will cause Lean to execute the code)
- Identifiers with underscores like `bv_decide` should be wrapped in backticks: `` `bv_decide` ``
(otherwise the underscore may be interpreted as markdown emphasis)
## Updating Manual/Releases.lean
After creating the release notes file, update `Manual/Releases.lean` to include it:
1. Add the import near the top with other version imports:
```lean
import Manual.Releases.«v4_7_0»
```
2. Add the include statement after the other includes:
```lean
{include 0 Manual.Releases.«v4_7_0»}
```
## Building and verifying
Build the release notes to check for errors:
```bash
lake build Manual.Releases.v4_7_0
```
Common errors and fixes:
- "Wrong header nesting - got ## but expected at most #": Change `##` to `#`
- "Tactic 'X' failed" or similar: Code is being executed; change ` ```lean ` to ` ``` `
- "'_'" errors: Underscore in identifier being parsed as emphasis; wrap in backticks
## Creating the PR
**Important: Timing with the reference-manual tag**
The reference-manual repository deploys documentation when a version tag is pushed. If you merge
release notes AFTER the tag is created, the deployed documentation won't include them.
You have two options:
1. **Preferred**: Include the release notes in the same PR as the toolchain bump (or merge the
release notes PR before creating the tag). This ensures the tag includes the release notes.
2. **If release notes are merged after the tag**: You must regenerate the tag to trigger a new deployment:
```bash
cd /path/to/reference-manual
git fetch origin
git tag -d v4.7.0-rc1 # Delete local tag
git tag v4.7.0-rc1 origin/main # Create tag at current main (which has release notes)
git push origin :refs/tags/v4.7.0-rc1 # Delete remote tag
git push origin v4.7.0-rc1 # Push new tag (triggers Deploy workflow)
```
If creating a separate PR for release notes:
```bash
git checkout -b v4.7.0-release-notes
git add Manual/Releases/v4_7_0.lean Manual/Releases.lean
git commit -m "doc: add v4.7.0 release notes"
git push -u origin v4.7.0-release-notes
gh pr create --title "doc: add v4.7.0 release notes" --body "This PR adds the release notes for Lean v4.7.0."
```
See `./releases_drafts/README.md` for more information about pre-written release note entries.
See `./releases_drafts/README.md` for more information.

View File

@@ -1,9 +1,5 @@
# Test Suite
**Warning:** This document is partially outdated.
It describes the old test suite, which is currently in the process of being replaced.
The new test suite's documentation can be found at [`tests/README.md`](../../tests/README.md).
After [building Lean](../make/index.md) you can run all the tests using
```
cd build/release

View File

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

View File

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

View File

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

View File

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

View File

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

8
flake.lock generated
View File

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

View File

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

View File

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

View File

@@ -2,9 +2,21 @@
"folders": [
{
"path": "."
},
{
"path": "src"
},
{
"path": "tests"
},
{
"path": "script"
}
],
"settings": {
// Open terminal at root, not current workspace folder
// (there is not way to directly refer to the root folder included as `.` above)
"terminal.integrated.cwd": "${workspaceFolder:src}/..",
"files.insertFinalNewline": true,
"files.trimTrailingWhitespace": true,
"cmake.buildDirectory": "${workspaceFolder}/build/release",

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

@@ -1,779 +0,0 @@
#!/usr/bin/env python3
"""
Lean name demangler.
Demangles C symbol names produced by the Lean 4 compiler back into
readable Lean hierarchical names.
Usage as a filter (like c++filt):
echo "l_Lean_Meta_Sym_main" | python lean_demangle.py
Usage as a module:
from lean_demangle import demangle_lean_name
print(demangle_lean_name("l_Lean_Meta_Sym_main"))
"""
import sys
# ---------------------------------------------------------------------------
# String.mangle / unmangle
# ---------------------------------------------------------------------------
def _is_ascii_alnum(ch):
"""Check if ch is an ASCII letter or digit (matching Lean's isAlpha/isDigit)."""
return ('a' <= ch <= 'z') or ('A' <= ch <= 'Z') or ('0' <= ch <= '9')
def mangle_string(s):
"""Port of Lean's String.mangle: escape a single string for C identifiers."""
result = []
for ch in s:
if _is_ascii_alnum(ch):
result.append(ch)
elif ch == '_':
result.append('__')
else:
code = ord(ch)
if code < 0x100:
result.append('_x' + format(code, '02x'))
elif code < 0x10000:
result.append('_u' + format(code, '04x'))
else:
result.append('_U' + format(code, '08x'))
return ''.join(result)
def _parse_hex(s, pos, n):
"""Parse n lowercase hex digits at pos. Returns (new_pos, value) or None."""
if pos + n > len(s):
return None
val = 0
for i in range(n):
c = s[pos + i]
if '0' <= c <= '9':
val = (val << 4) | (ord(c) - ord('0'))
elif 'a' <= c <= 'f':
val = (val << 4) | (ord(c) - ord('a') + 10)
else:
return None
return (pos + n, val)
# ---------------------------------------------------------------------------
# Name mangling (for round-trip verification)
# ---------------------------------------------------------------------------
def _check_disambiguation(m):
"""Port of Lean's checkDisambiguation: does mangled string m need a '00' prefix?"""
pos = 0
while pos < len(m):
ch = m[pos]
if ch == '_':
pos += 1
continue
if ch == 'x':
return _parse_hex(m, pos + 1, 2) is not None
if ch == 'u':
return _parse_hex(m, pos + 1, 4) is not None
if ch == 'U':
return _parse_hex(m, pos + 1, 8) is not None
if '0' <= ch <= '9':
return True
return False
# all underscores or empty
return True
def _need_disambiguation(prev_component, mangled_next):
"""Port of Lean's needDisambiguation."""
# Check if previous component (as a string) ends with '_'
prev_ends_underscore = (isinstance(prev_component, str) and
len(prev_component) > 0 and
prev_component[-1] == '_')
return prev_ends_underscore or _check_disambiguation(mangled_next)
def mangle_name(components, prefix="l_"):
"""
Mangle a list of name components (str or int) into a C symbol.
Port of Lean's Name.mangle.
"""
if not components:
return prefix
parts = []
prev = None
for i, comp in enumerate(components):
if isinstance(comp, int):
if i == 0:
parts.append(str(comp) + '_')
else:
parts.append('_' + str(comp) + '_')
else:
m = mangle_string(comp)
if i == 0:
if _check_disambiguation(m):
parts.append('00' + m)
else:
parts.append(m)
else:
if _need_disambiguation(prev, m):
parts.append('_00' + m)
else:
parts.append('_' + m)
prev = comp
return prefix + ''.join(parts)
# ---------------------------------------------------------------------------
# Name demangling
# ---------------------------------------------------------------------------
def demangle_body(s):
"""
Demangle a string produced by Name.mangleAux (without prefix).
Returns a list of components (str or int).
This is a faithful port of Lean's Name.demangleAux from NameMangling.lean.
"""
components = []
length = len(s)
def emit(comp):
components.append(comp)
def decode_num(pos, n):
"""Parse remaining digits, emit numeric component, continue."""
while pos < length:
ch = s[pos]
if '0' <= ch <= '9':
n = n * 10 + (ord(ch) - ord('0'))
pos += 1
else:
# Expect '_' (trailing underscore of numeric encoding)
pos += 1 # skip '_'
emit(n)
if pos >= length:
return pos
# Skip separator '_' and go to name_start
pos += 1
return name_start(pos)
# End of string
emit(n)
return pos
def name_start(pos):
"""Start parsing a new name component."""
if pos >= length:
return pos
ch = s[pos]
pos += 1
if '0' <= ch <= '9':
# Check for '00' disambiguation
if ch == '0' and pos < length and s[pos] == '0':
pos += 1
return demangle_main(pos, "", 0)
else:
return decode_num(pos, ord(ch) - ord('0'))
elif ch == '_':
return demangle_main(pos, "", 1)
else:
return demangle_main(pos, ch, 0)
def demangle_main(pos, acc, ucount):
"""Main demangling loop."""
while pos < length:
ch = s[pos]
pos += 1
if ch == '_':
ucount += 1
continue
if ucount % 2 == 0:
# Even underscores: literal underscores in component name
acc += '_' * (ucount // 2) + ch
ucount = 0
continue
# Odd ucount: separator or escape
if '0' <= ch <= '9':
# End current str component, start number
emit(acc + '_' * (ucount // 2))
if ch == '0' and pos < length and s[pos] == '0':
pos += 1
return demangle_main(pos, "", 0)
else:
return decode_num(pos, ord(ch) - ord('0'))
# Try hex escapes
if ch == 'x':
result = _parse_hex(s, pos, 2)
if result is not None:
new_pos, val = result
acc += '_' * (ucount // 2) + chr(val)
pos = new_pos
ucount = 0
continue
if ch == 'u':
result = _parse_hex(s, pos, 4)
if result is not None:
new_pos, val = result
acc += '_' * (ucount // 2) + chr(val)
pos = new_pos
ucount = 0
continue
if ch == 'U':
result = _parse_hex(s, pos, 8)
if result is not None:
new_pos, val = result
acc += '_' * (ucount // 2) + chr(val)
pos = new_pos
ucount = 0
continue
# Name separator
emit(acc)
acc = '_' * (ucount // 2) + ch
ucount = 0
# End of string
acc += '_' * (ucount // 2)
if acc:
emit(acc)
return pos
name_start(0)
return components
# ---------------------------------------------------------------------------
# Prefix handling for lp_ (package prefix)
# ---------------------------------------------------------------------------
def _is_valid_string_mangle(s):
"""Check if s is a valid output of String.mangle (no trailing bare _)."""
pos = 0
length = len(s)
while pos < length:
ch = s[pos]
if _is_ascii_alnum(ch):
pos += 1
elif ch == '_':
if pos + 1 >= length:
return False # trailing bare _
nch = s[pos + 1]
if nch == '_':
pos += 2
elif nch == 'x' and _parse_hex(s, pos + 2, 2) is not None:
pos = _parse_hex(s, pos + 2, 2)[0]
elif nch == 'u' and _parse_hex(s, pos + 2, 4) is not None:
pos = _parse_hex(s, pos + 2, 4)[0]
elif nch == 'U' and _parse_hex(s, pos + 2, 8) is not None:
pos = _parse_hex(s, pos + 2, 8)[0]
else:
return False
else:
return False
return True
def _skip_string_mangle(s, pos):
"""
Skip past a String.mangle output in s starting at pos.
Returns the position after the mangled string (where we expect the separator '_').
This is a greedy scan.
"""
length = len(s)
while pos < length:
ch = s[pos]
if _is_ascii_alnum(ch):
pos += 1
elif ch == '_':
if pos + 1 < length:
nch = s[pos + 1]
if nch == '_':
pos += 2
elif nch == 'x' and _parse_hex(s, pos + 2, 2) is not None:
pos = _parse_hex(s, pos + 2, 2)[0]
elif nch == 'u' and _parse_hex(s, pos + 2, 4) is not None:
pos = _parse_hex(s, pos + 2, 4)[0]
elif nch == 'U' and _parse_hex(s, pos + 2, 8) is not None:
pos = _parse_hex(s, pos + 2, 8)[0]
else:
return pos # bare '_': separator
else:
return pos
else:
return pos
return pos
def _find_lp_body(s):
"""
Given s = everything after 'lp_' in a symbol, find where the declaration
body (Name.mangleAux output) starts.
Returns the start index of the body within s, or None.
Strategy: try all candidate split points where the package part is a valid
String.mangle output and the body round-trips. Prefer the longest valid
package name (most specific match).
"""
length = len(s)
# Collect candidate split positions: every '_' that could be the separator
candidates = []
pos = 0
while pos < length:
if s[pos] == '_':
candidates.append(pos)
pos += 1
# Try each candidate; collect all valid splits
valid_splits = []
for split_pos in candidates:
pkg_part = s[:split_pos]
if not pkg_part:
continue
if not _is_valid_string_mangle(pkg_part):
continue
body = s[split_pos + 1:]
if not body:
continue
components = demangle_body(body)
if not components:
continue
remangled = mangle_name(components, prefix="")
if remangled == body:
first = components[0]
# Score: prefer first component starting with uppercase
has_upper = isinstance(first, str) and first and first[0].isupper()
valid_splits.append((split_pos, has_upper))
if valid_splits:
# Among splits where first decl component starts uppercase, pick longest pkg.
# Otherwise pick shortest pkg.
upper_splits = [s for s in valid_splits if s[1]]
if upper_splits:
best = max(upper_splits, key=lambda x: x[0])
else:
best = min(valid_splits, key=lambda x: x[0])
return best[0] + 1
# Fallback: greedy String.mangle scan
greedy_pos = _skip_string_mangle(s, 0)
if greedy_pos < length and s[greedy_pos] == '_':
return greedy_pos + 1
return None
# ---------------------------------------------------------------------------
# Format name components for display
# ---------------------------------------------------------------------------
def format_name(components):
"""Format a list of name components as a dot-separated string."""
return '.'.join(str(c) for c in components)
# ---------------------------------------------------------------------------
# Human-friendly postprocessing
# ---------------------------------------------------------------------------
# Compiler-generated suffix components — exact match
_SUFFIX_FLAGS_EXACT = {
'_redArg': 'arity\u2193',
'_boxed': 'boxed',
'_impl': 'impl',
}
# Compiler-generated suffix prefixes — match with optional _N index
# e.g., _lam, _lam_0, _lam_3, _lambda_0, _closed_2
_SUFFIX_FLAGS_PREFIX = {
'_lam': '\u03bb',
'_lambda': '\u03bb',
'_elam': '\u03bb',
'_jp': 'jp',
'_closed': 'closed',
}
def _match_suffix(component):
"""
Check if a string component is a compiler-generated suffix.
Returns the flag label or None.
Handles both exact matches (_redArg, _boxed) and indexed suffixes
(_lam_0, _lambda_2, _closed_0) produced by appendIndexAfter.
"""
if not isinstance(component, str):
return None
if component in _SUFFIX_FLAGS_EXACT:
return _SUFFIX_FLAGS_EXACT[component]
if component in _SUFFIX_FLAGS_PREFIX:
return _SUFFIX_FLAGS_PREFIX[component]
# Check for indexed suffix: prefix + _N
for prefix, label in _SUFFIX_FLAGS_PREFIX.items():
if component.startswith(prefix + '_'):
rest = component[len(prefix) + 1:]
if rest.isdigit():
return label
return None
def _strip_private(components):
"""Strip _private.Module.0. prefix. Returns (stripped_parts, is_private)."""
if (len(components) >= 3 and isinstance(components[0], str) and
components[0] == '_private'):
for i in range(1, len(components)):
if components[i] == 0:
if i + 1 < len(components):
return components[i + 1:], True
break
return components, False
def _strip_spec_suffixes(components):
"""Strip trailing spec_N components (from appendIndexAfter)."""
parts = list(components)
while parts and isinstance(parts[-1], str) and parts[-1].startswith('spec_'):
rest = parts[-1][5:]
if rest.isdigit():
parts.pop()
else:
break
return parts
def _is_spec_index(component):
"""Check if a component is a spec_N index (from appendIndexAfter)."""
return (isinstance(component, str) and
component.startswith('spec_') and component[5:].isdigit())
def _parse_spec_entries(rest):
"""Parse _at_..._spec pairs into separate spec context entries.
Given components starting from the first _at_, returns:
- entries: list of component lists, one per _at_..._spec block
- remaining: components after the last _spec N (trailing suffixes)
"""
entries = []
current_ctx = None
remaining = []
skip_next = False
for p in rest:
if skip_next:
skip_next = False
continue
if isinstance(p, str) and p == '_at_':
if current_ctx is not None:
entries.append(current_ctx)
current_ctx = []
continue
if isinstance(p, str) and p == '_spec':
if current_ctx is not None:
entries.append(current_ctx)
current_ctx = None
skip_next = True
continue
if isinstance(p, str) and p.startswith('_spec'):
if current_ctx is not None:
entries.append(current_ctx)
current_ctx = None
continue
if current_ctx is not None:
current_ctx.append(p)
else:
remaining.append(p)
if current_ctx is not None:
entries.append(current_ctx)
return entries, remaining
def _process_spec_context(components):
"""Process a spec context into a clean name and its flags.
Returns (name_parts, flags) where name_parts are the cleaned components
and flags is a deduplicated list of flag labels from compiler suffixes.
"""
parts = list(components)
parts, _ = _strip_private(parts)
name_parts = []
ctx_flags = []
seen = set()
for p in parts:
flag = _match_suffix(p)
if flag is not None:
if flag not in seen:
ctx_flags.append(flag)
seen.add(flag)
elif _is_spec_index(p):
pass
else:
name_parts.append(p)
return name_parts, ctx_flags
def postprocess_name(components):
"""
Transform raw demangled components into a human-friendly display string.
Applies:
- Private name cleanup: _private.Module.0.Name.foo -> Name.foo [private]
- Hygienic name cleanup: strips _@.module._hygCtx._hyg.N
- Suffix folding: _redArg, _boxed, _lam_0, etc. -> [flags]
- Specialization: f._at_.g._spec.N -> f spec at g
Shown after base [flags], with context flags: spec at g[ctx_flags]
"""
if not components:
return ""
parts = list(components)
flags = []
spec_entries = []
# --- Strip _private prefix ---
parts, is_private = _strip_private(parts)
# --- Strip hygienic suffixes: everything from _@ onward ---
at_idx = None
for i, p in enumerate(parts):
if isinstance(p, str) and p.startswith('_@'):
at_idx = i
break
if at_idx is not None:
parts = parts[:at_idx]
# --- Handle specialization: _at_ ... _spec N ---
at_positions = [i for i, p in enumerate(parts)
if isinstance(p, str) and p == '_at_']
if at_positions:
first_at = at_positions[0]
base = parts[:first_at]
rest = parts[first_at:]
entries, remaining = _parse_spec_entries(rest)
for ctx_components in entries:
ctx_name, ctx_flags = _process_spec_context(ctx_components)
if ctx_name or ctx_flags:
spec_entries.append((ctx_name, ctx_flags))
parts = base + remaining
# --- Collect suffix flags from the end ---
while parts:
last = parts[-1]
flag = _match_suffix(last)
if flag is not None:
flags.append(flag)
parts.pop()
elif isinstance(last, int) and len(parts) >= 2:
prev_flag = _match_suffix(parts[-2])
if prev_flag is not None:
flags.append(prev_flag)
parts.pop() # remove the number
parts.pop() # remove the suffix
else:
break
else:
break
if is_private:
flags.append('private')
# --- Format result ---
name = '.'.join(str(c) for c in parts) if parts else '?'
result = name
if flags:
flag_str = ', '.join(flags)
result += f' [{flag_str}]'
for ctx_name, ctx_flags in spec_entries:
ctx_str = '.'.join(str(c) for c in ctx_name) if ctx_name else '?'
if ctx_flags:
ctx_flag_str = ', '.join(ctx_flags)
result += f' spec at {ctx_str}[{ctx_flag_str}]'
else:
result += f' spec at {ctx_str}'
return result
# ---------------------------------------------------------------------------
# Main demangling entry point
# ---------------------------------------------------------------------------
def demangle_lean_name_raw(mangled):
"""
Demangle a Lean C symbol, preserving all internal name components.
Returns the exact demangled name with all compiler-generated suffixes
intact. Use demangle_lean_name() for human-friendly output.
"""
try:
return _demangle_lean_name_inner(mangled, human_friendly=False)
except Exception:
return mangled
def demangle_lean_name(mangled):
"""
Demangle a C symbol name produced by the Lean 4 compiler.
Returns a human-friendly demangled name with compiler suffixes folded
into readable flags. Use demangle_lean_name_raw() to preserve all
internal components.
"""
try:
return _demangle_lean_name_inner(mangled, human_friendly=True)
except Exception:
return mangled
def _demangle_lean_name_inner(mangled, human_friendly=True):
"""Inner demangle that may raise on malformed input."""
if mangled == "_lean_main":
return "[lean] main"
# Handle lean_ runtime functions
if human_friendly and mangled.startswith("lean_apply_"):
rest = mangled[11:]
if rest.isdigit():
return f"<apply/{rest}>"
# Strip .cold.N suffix (LLVM linker cold function clones)
cold_suffix = ""
core = mangled
dot_pos = core.find('.cold.')
if dot_pos >= 0:
cold_suffix = " " + core[dot_pos:]
core = core[:dot_pos]
elif core.endswith('.cold'):
cold_suffix = " .cold"
core = core[:-5]
result = _demangle_core(core, human_friendly)
if result is None:
return mangled
return result + cold_suffix
def _demangle_core(mangled, human_friendly=True):
"""Demangle a symbol without .cold suffix. Returns None if not a Lean name."""
fmt = postprocess_name if human_friendly else format_name
# _init_ prefix
if mangled.startswith("_init_"):
rest = mangled[6:]
body, pkg_display = _strip_lean_prefix(rest)
if body is None:
return None
components = demangle_body(body)
if not components:
return None
name = fmt(components)
if pkg_display:
return f"[init] {name} ({pkg_display})"
return f"[init] {name}"
# initialize_ prefix (module init functions)
if mangled.startswith("initialize_"):
rest = mangled[11:]
# With package: initialize_lp_{pkg}_{body} or initialize_l_{body}
body, pkg_display = _strip_lean_prefix(rest)
if body is not None:
components = demangle_body(body)
if components:
name = fmt(components)
if pkg_display:
return f"[module_init] {name} ({pkg_display})"
return f"[module_init] {name}"
# Without package: initialize_{Name.mangleAux(moduleName)}
if rest:
components = demangle_body(rest)
if components:
return f"[module_init] {fmt(components)}"
return None
# l_ or lp_ prefix
body, pkg_display = _strip_lean_prefix(mangled)
if body is None:
return None
components = demangle_body(body)
if not components:
return None
name = fmt(components)
if pkg_display:
return f"{name} ({pkg_display})"
return name
def _strip_lean_prefix(s):
"""
Strip the l_ or lp_ prefix from a mangled symbol.
Returns (body, pkg_display) where body is the Name.mangleAux output
and pkg_display is None or a string describing the package.
Returns (None, None) if the string doesn't have a recognized prefix.
"""
if s.startswith("l_"):
return (s[2:], None)
if s.startswith("lp_"):
after_lp = s[3:]
body_start = _find_lp_body(after_lp)
if body_start is not None:
pkg_mangled = after_lp[:body_start - 1]
# Unmangle the package name
pkg_components = demangle_body(pkg_mangled)
if pkg_components and len(pkg_components) == 1 and isinstance(pkg_components[0], str):
pkg_display = pkg_components[0]
else:
pkg_display = pkg_mangled
return (after_lp[body_start:], pkg_display)
# Fallback: treat everything after lp_ as body
return (after_lp, "?")
return (None, None)
# ---------------------------------------------------------------------------
# CLI
# ---------------------------------------------------------------------------
def main():
"""Filter stdin or arguments, demangling Lean names."""
import argparse
parser = argparse.ArgumentParser(
description="Demangle Lean 4 C symbol names (like c++filt for Lean)")
parser.add_argument('names', nargs='*',
help='Names to demangle (reads stdin if none given)')
parser.add_argument('--raw', action='store_true',
help='Output exact demangled names without postprocessing')
args = parser.parse_args()
demangle = demangle_lean_name_raw if args.raw else demangle_lean_name
if args.names:
for name in args.names:
print(demangle(name))
else:
for line in sys.stdin:
print(demangle(line.rstrip('\n')))
if __name__ == '__main__':
main()

View File

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

View File

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

View File

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

View File

@@ -1,670 +0,0 @@
#!/usr/bin/env python3
"""Tests for the Lean name demangler."""
import unittest
import json
import gzip
import tempfile
import os
from lean_demangle import (
mangle_string, mangle_name, demangle_body, format_name,
demangle_lean_name, demangle_lean_name_raw, postprocess_name,
_parse_hex, _check_disambiguation,
)
class TestStringMangle(unittest.TestCase):
"""Test String.mangle (character-level escaping)."""
def test_alphanumeric(self):
self.assertEqual(mangle_string("hello"), "hello")
self.assertEqual(mangle_string("abc123"), "abc123")
def test_underscore(self):
self.assertEqual(mangle_string("a_b"), "a__b")
self.assertEqual(mangle_string("_"), "__")
self.assertEqual(mangle_string("__"), "____")
def test_special_chars(self):
self.assertEqual(mangle_string("."), "_x2e")
self.assertEqual(mangle_string("a.b"), "a_x2eb")
def test_unicode(self):
self.assertEqual(mangle_string("\u03bb"), "_u03bb")
self.assertEqual(mangle_string("\U0001d55c"), "_U0001d55c")
def test_empty(self):
self.assertEqual(mangle_string(""), "")
class TestNameMangle(unittest.TestCase):
"""Test Name.mangle (hierarchical name mangling)."""
def test_simple(self):
self.assertEqual(mangle_name(["Lean", "Meta", "Sym", "main"]),
"l_Lean_Meta_Sym_main")
def test_single_component(self):
self.assertEqual(mangle_name(["main"]), "l_main")
def test_numeric_component(self):
self.assertEqual(
mangle_name(["_private", "Lean", "Meta", "Basic", 0,
"Lean", "Meta", "withMVarContextImp"]),
"l___private_Lean_Meta_Basic_0__Lean_Meta_withMVarContextImp")
def test_component_with_underscore(self):
self.assertEqual(mangle_name(["a_b"]), "l_a__b")
self.assertEqual(mangle_name(["a_b", "c"]), "l_a__b_c")
def test_disambiguation_digit_start(self):
self.assertEqual(mangle_name(["0foo"]), "l_000foo")
def test_disambiguation_escape_start(self):
self.assertEqual(mangle_name(["a", "x27"]), "l_a_00x27")
def test_numeric_root(self):
self.assertEqual(mangle_name([42]), "l_42_")
self.assertEqual(mangle_name([42, "foo"]), "l_42__foo")
def test_component_ending_with_underscore(self):
self.assertEqual(mangle_name(["a_", "b"]), "l_a___00b")
def test_custom_prefix(self):
self.assertEqual(mangle_name(["foo"], prefix="lp_pkg_"),
"lp_pkg_foo")
class TestDemangleBody(unittest.TestCase):
"""Test demangle_body (the core Name.demangleAux algorithm)."""
def test_simple(self):
self.assertEqual(demangle_body("Lean_Meta_Sym_main"),
["Lean", "Meta", "Sym", "main"])
def test_single(self):
self.assertEqual(demangle_body("main"), ["main"])
def test_empty(self):
self.assertEqual(demangle_body(""), [])
def test_underscore_in_component(self):
self.assertEqual(demangle_body("a__b"), ["a_b"])
self.assertEqual(demangle_body("a__b_c"), ["a_b", "c"])
def test_numeric_component(self):
self.assertEqual(demangle_body("foo_42__bar"), ["foo", 42, "bar"])
def test_numeric_root(self):
self.assertEqual(demangle_body("42_"), [42])
def test_numeric_at_end(self):
self.assertEqual(demangle_body("foo_42_"), ["foo", 42])
def test_disambiguation_00(self):
self.assertEqual(demangle_body("a_00x27"), ["a", "x27"])
def test_disambiguation_00_at_root(self):
self.assertEqual(demangle_body("000foo"), ["0foo"])
def test_hex_escape_x(self):
self.assertEqual(demangle_body("a_x2eb"), ["a.b"])
def test_hex_escape_u(self):
self.assertEqual(demangle_body("_u03bb"), ["\u03bb"])
def test_hex_escape_U(self):
self.assertEqual(demangle_body("_U0001d55c"), ["\U0001d55c"])
def test_private_name(self):
body = "__private_Lean_Meta_Basic_0__Lean_Meta_withMVarContextImp"
self.assertEqual(demangle_body(body),
["_private", "Lean", "Meta", "Basic", 0,
"Lean", "Meta", "withMVarContextImp"])
def test_boxed_suffix(self):
body = "foo___boxed"
self.assertEqual(demangle_body(body), ["foo", "_boxed"])
def test_redArg_suffix(self):
body = "foo_bar___redArg"
self.assertEqual(demangle_body(body), ["foo", "bar", "_redArg"])
def test_component_ending_underscore_disambiguation(self):
self.assertEqual(demangle_body("a___00b"), ["a_", "b"])
class TestRoundTrip(unittest.TestCase):
"""Test that mangle(demangle(x)) == x for various names."""
def _check_roundtrip(self, components):
mangled = mangle_name(components, prefix="")
demangled = demangle_body(mangled)
self.assertEqual(demangled, components,
f"Round-trip failed: {components} -> '{mangled}' -> {demangled}")
mangled_with_prefix = mangle_name(components, prefix="l_")
self.assertTrue(mangled_with_prefix.startswith("l_"))
body = mangled_with_prefix[2:]
demangled2 = demangle_body(body)
self.assertEqual(demangled2, components)
def test_simple_names(self):
self._check_roundtrip(["Lean", "Meta", "main"])
self._check_roundtrip(["a"])
self._check_roundtrip(["Foo", "Bar", "baz"])
def test_numeric(self):
self._check_roundtrip(["foo", 0, "bar"])
self._check_roundtrip([42])
self._check_roundtrip(["a", 1, "b", 2, "c"])
def test_underscores(self):
self._check_roundtrip(["_private"])
self._check_roundtrip(["a_b", "c_d"])
self._check_roundtrip(["_at_", "_spec"])
def test_private_name(self):
self._check_roundtrip(["_private", "Lean", "Meta", "Basic", 0,
"Lean", "Meta", "withMVarContextImp"])
def test_boxed(self):
self._check_roundtrip(["Lean", "Meta", "foo", "_boxed"])
def test_redArg(self):
self._check_roundtrip(["Lean", "Meta", "foo", "_redArg"])
def test_specialization(self):
self._check_roundtrip(["List", "map", "_at_", "Foo", "bar", "_spec", 3])
def test_lambda(self):
self._check_roundtrip(["Foo", "bar", "_lambda", 0])
self._check_roundtrip(["Foo", "bar", "_lambda", 2])
def test_closed(self):
self._check_roundtrip(["myConst", "_closed", 0])
def test_special_chars(self):
self._check_roundtrip(["a.b"])
self._check_roundtrip(["\u03bb"])
self._check_roundtrip(["a", "b\u2192c"])
def test_disambiguation_cases(self):
self._check_roundtrip(["a", "x27"])
self._check_roundtrip(["0foo"])
self._check_roundtrip(["a_", "b"])
def test_complex_real_names(self):
"""Names modeled after real Lean compiler output."""
self._check_roundtrip(
["Lean", "MVarId", "withContext", "_at_",
"_private", "Lean", "Meta", "Sym", 0,
"Lean", "Meta", "Sym", "BackwardRule", "apply",
"_spec", 2, "_redArg", "_lambda", 0, "_boxed"])
class TestDemangleRaw(unittest.TestCase):
"""Test demangle_lean_name_raw (exact demangling, no postprocessing)."""
def test_l_prefix(self):
self.assertEqual(
demangle_lean_name_raw("l_Lean_Meta_Sym_main"),
"Lean.Meta.Sym.main")
def test_l_prefix_private(self):
result = demangle_lean_name_raw(
"l___private_Lean_Meta_Basic_0__Lean_Meta_withMVarContextImp")
self.assertEqual(result,
"_private.Lean.Meta.Basic.0.Lean.Meta.withMVarContextImp")
def test_l_prefix_boxed(self):
result = demangle_lean_name_raw("l_foo___boxed")
self.assertEqual(result, "foo._boxed")
def test_l_prefix_redArg(self):
result = demangle_lean_name_raw(
"l___private_Lean_Meta_Basic_0__Lean_Meta_withMVarContextImp___redArg")
self.assertEqual(
result,
"_private.Lean.Meta.Basic.0.Lean.Meta.withMVarContextImp._redArg")
def test_lean_main(self):
self.assertEqual(demangle_lean_name_raw("_lean_main"), "[lean] main")
def test_non_lean_names(self):
self.assertEqual(demangle_lean_name_raw("printf"), "printf")
self.assertEqual(demangle_lean_name_raw("malloc"), "malloc")
self.assertEqual(demangle_lean_name_raw("lean_apply_5"), "lean_apply_5")
self.assertEqual(demangle_lean_name_raw(""), "")
def test_init_prefix(self):
result = demangle_lean_name_raw("_init_l_Lean_Meta_foo")
self.assertEqual(result, "[init] Lean.Meta.foo")
def test_lp_prefix_simple(self):
mangled = mangle_name(["Lean", "Meta", "foo"], prefix="lp_std_")
self.assertEqual(mangled, "lp_std_Lean_Meta_foo")
result = demangle_lean_name_raw(mangled)
self.assertEqual(result, "Lean.Meta.foo (std)")
def test_lp_prefix_underscore_pkg(self):
pkg_mangled = mangle_string("my_pkg")
self.assertEqual(pkg_mangled, "my__pkg")
mangled = mangle_name(["Lean", "Meta", "foo"],
prefix=f"lp_{pkg_mangled}_")
self.assertEqual(mangled, "lp_my__pkg_Lean_Meta_foo")
result = demangle_lean_name_raw(mangled)
self.assertEqual(result, "Lean.Meta.foo (my_pkg)")
def test_lp_prefix_private_decl(self):
mangled = mangle_name(
["_private", "X", 0, "Y", "foo"], prefix="lp_pkg_")
self.assertEqual(mangled, "lp_pkg___private_X_0__Y_foo")
result = demangle_lean_name_raw(mangled)
self.assertEqual(result, "_private.X.0.Y.foo (pkg)")
def test_complex_specialization(self):
components = [
"Lean", "MVarId", "withContext", "_at_",
"_private", "Lean", "Meta", "Sym", 0,
"Lean", "Meta", "Sym", "BackwardRule", "apply",
"_spec", 2, "_redArg", "_lambda", 0, "_boxed"
]
mangled = mangle_name(components)
result = demangle_lean_name_raw(mangled)
expected = format_name(components)
self.assertEqual(result, expected)
def test_cold_suffix(self):
result = demangle_lean_name_raw("l_Lean_Meta_foo___redArg.cold.1")
self.assertEqual(result, "Lean.Meta.foo._redArg .cold.1")
def test_cold_suffix_plain(self):
result = demangle_lean_name_raw("l_Lean_Meta_foo.cold")
self.assertEqual(result, "Lean.Meta.foo .cold")
def test_initialize_no_pkg(self):
result = demangle_lean_name_raw("initialize_Init_Control_Basic")
self.assertEqual(result, "[module_init] Init.Control.Basic")
def test_initialize_with_l_prefix(self):
result = demangle_lean_name_raw("initialize_l_Lean_Meta_foo")
self.assertEqual(result, "[module_init] Lean.Meta.foo")
def test_never_crashes(self):
"""Demangling should never raise, just return the original."""
weird_inputs = [
"", "l_", "lp_", "lp_x", "_init_", "initialize_",
"l_____", "lp____", "l_00", "l_0",
"some random string", "l_ space",
]
for inp in weird_inputs:
result = demangle_lean_name_raw(inp)
self.assertIsInstance(result, str)
class TestPostprocess(unittest.TestCase):
"""Test postprocess_name (human-friendly suffix folding, etc.)."""
def test_no_change(self):
self.assertEqual(postprocess_name(["Lean", "Meta", "main"]),
"Lean.Meta.main")
def test_boxed(self):
self.assertEqual(postprocess_name(["foo", "_boxed"]),
"foo [boxed]")
def test_redArg(self):
self.assertEqual(postprocess_name(["foo", "bar", "_redArg"]),
"foo.bar [arity\u2193]")
def test_lambda_separate(self):
# _lam as separate component + numeric index
self.assertEqual(postprocess_name(["foo", "_lam", 0]),
"foo [\u03bb]")
def test_lambda_indexed(self):
# _lam_0 as single string (appendIndexAfter)
self.assertEqual(postprocess_name(["foo", "_lam_0"]),
"foo [\u03bb]")
self.assertEqual(postprocess_name(["foo", "_lambda_2"]),
"foo [\u03bb]")
def test_lambda_boxed(self):
# _lam_0 followed by _boxed
self.assertEqual(
postprocess_name(["Lean", "Meta", "Simp", "simpLambda",
"_lam_0", "_boxed"]),
"Lean.Meta.Simp.simpLambda [boxed, \u03bb]")
def test_closed(self):
self.assertEqual(postprocess_name(["myConst", "_closed", 3]),
"myConst [closed]")
def test_closed_indexed(self):
self.assertEqual(postprocess_name(["myConst", "_closed_0"]),
"myConst [closed]")
def test_multiple_suffixes(self):
self.assertEqual(postprocess_name(["foo", "_redArg", "_boxed"]),
"foo [boxed, arity\u2193]")
def test_redArg_lam(self):
# _redArg followed by _lam_0 (issue #4)
self.assertEqual(
postprocess_name(["Lean", "profileitIOUnsafe",
"_redArg", "_lam_0"]),
"Lean.profileitIOUnsafe [\u03bb, arity\u2193]")
def test_private_name(self):
self.assertEqual(
postprocess_name(["_private", "Lean", "Meta", "Basic", 0,
"Lean", "Meta", "withMVarContextImp"]),
"Lean.Meta.withMVarContextImp [private]")
def test_private_with_suffix(self):
self.assertEqual(
postprocess_name(["_private", "Lean", "Meta", "Basic", 0,
"Lean", "Meta", "foo", "_redArg"]),
"Lean.Meta.foo [arity\u2193, private]")
def test_hygienic_strip(self):
self.assertEqual(
postprocess_name(["Lean", "Meta", "foo", "_@", "Lean", "Meta",
"_hyg", 42]),
"Lean.Meta.foo")
def test_specialization(self):
self.assertEqual(
postprocess_name(["List", "map", "_at_", "Foo", "bar",
"_spec", 3]),
"List.map spec at Foo.bar")
def test_specialization_with_suffix(self):
# Base suffix _boxed appears in [flags] before spec at
self.assertEqual(
postprocess_name(["Lean", "MVarId", "withContext", "_at_",
"Foo", "bar", "_spec", 2, "_boxed"]),
"Lean.MVarId.withContext [boxed] spec at Foo.bar")
def test_spec_context_with_flags(self):
# Compiler suffixes in spec context become context flags
self.assertEqual(
postprocess_name(["Lean", "Meta", "foo", "_at_",
"Lean", "Meta", "bar", "_elam_1", "_redArg",
"_spec", 2]),
"Lean.Meta.foo spec at Lean.Meta.bar[\u03bb, arity\u2193]")
def test_spec_context_flags_dedup(self):
# Duplicate flag labels are deduplicated
self.assertEqual(
postprocess_name(["f", "_at_",
"g", "_lam_0", "_elam_1", "_redArg",
"_spec", 1]),
"f spec at g[\u03bb, arity\u2193]")
def test_multiple_at(self):
# Multiple _at_ entries become separate spec at clauses
self.assertEqual(
postprocess_name(["f", "_at_", "g", "_spec", 1,
"_at_", "h", "_spec", 2]),
"f spec at g spec at h")
def test_multiple_at_with_flags(self):
# Multiple spec at with flags on base and contexts
self.assertEqual(
postprocess_name(["f", "_at_", "g", "_redArg", "_spec", 1,
"_at_", "h", "_lam_0", "_spec", 2,
"_boxed"]),
"f [boxed] spec at g[arity\u2193] spec at h[\u03bb]")
def test_base_flags_before_spec(self):
# Base trailing suffixes appear in [flags] before spec at
self.assertEqual(
postprocess_name(["f", "_at_", "g", "_spec", 1, "_lam_0"]),
"f [\u03bb] spec at g")
def test_spec_context_strip_spec_suffixes(self):
# spec_0 in context should be stripped
self.assertEqual(
postprocess_name(["Lean", "Meta", "transformWithCache", "visit",
"_at_",
"_private", "Lean", "Meta", "Transform", 0,
"Lean", "Meta", "transform",
"Lean", "Meta", "Sym", "unfoldReducible",
"spec_0", "spec_0",
"_spec", 1]),
"Lean.Meta.transformWithCache.visit "
"spec at Lean.Meta.transform.Lean.Meta.Sym.unfoldReducible")
def test_spec_context_strip_private(self):
# _private in spec context should be stripped
self.assertEqual(
postprocess_name(["Array", "mapMUnsafe", "map", "_at_",
"_private", "Lean", "Meta", "Transform", 0,
"Lean", "Meta", "transformWithCache", "visit",
"_spec", 1]),
"Array.mapMUnsafe.map "
"spec at Lean.Meta.transformWithCache.visit")
def test_empty(self):
self.assertEqual(postprocess_name([]), "")
class TestDemangleHumanFriendly(unittest.TestCase):
"""Test demangle_lean_name (human-friendly output)."""
def test_simple(self):
self.assertEqual(demangle_lean_name("l_Lean_Meta_main"),
"Lean.Meta.main")
def test_boxed(self):
self.assertEqual(demangle_lean_name("l_foo___boxed"),
"foo [boxed]")
def test_redArg(self):
self.assertEqual(demangle_lean_name("l_foo___redArg"),
"foo [arity\u2193]")
def test_private(self):
self.assertEqual(
demangle_lean_name(
"l___private_Lean_Meta_Basic_0__Lean_Meta_foo"),
"Lean.Meta.foo [private]")
def test_private_with_redArg(self):
self.assertEqual(
demangle_lean_name(
"l___private_Lean_Meta_Basic_0__Lean_Meta_foo___redArg"),
"Lean.Meta.foo [arity\u2193, private]")
def test_cold_with_suffix(self):
self.assertEqual(
demangle_lean_name("l_Lean_Meta_foo___redArg.cold.1"),
"Lean.Meta.foo [arity\u2193] .cold.1")
def test_lean_apply(self):
self.assertEqual(demangle_lean_name("lean_apply_5"), "<apply/5>")
self.assertEqual(demangle_lean_name("lean_apply_12"), "<apply/12>")
def test_lean_apply_raw_unchanged(self):
self.assertEqual(demangle_lean_name_raw("lean_apply_5"),
"lean_apply_5")
def test_init_private(self):
self.assertEqual(
demangle_lean_name(
"_init_l___private_X_0__Y_foo"),
"[init] Y.foo [private]")
def test_complex_specialization(self):
components = [
"Lean", "MVarId", "withContext", "_at_",
"_private", "Lean", "Meta", "Sym", 0,
"Lean", "Meta", "Sym", "BackwardRule", "apply",
"_spec", 2, "_redArg", "_lambda", 0, "_boxed"
]
mangled = mangle_name(components)
result = demangle_lean_name(mangled)
# Base: Lean.MVarId.withContext with trailing _redArg, _lambda 0, _boxed
# Spec context: Lean.Meta.Sym.BackwardRule.apply (private stripped)
self.assertEqual(
result,
"Lean.MVarId.withContext [boxed, \u03bb, arity\u2193] "
"spec at Lean.Meta.Sym.BackwardRule.apply")
def test_non_lean_unchanged(self):
self.assertEqual(demangle_lean_name("printf"), "printf")
self.assertEqual(demangle_lean_name("malloc"), "malloc")
self.assertEqual(demangle_lean_name(""), "")
class TestDemangleProfile(unittest.TestCase):
"""Test the profile rewriter."""
def _make_profile_shared(self, strings):
"""Create a profile with shared.stringArray (newer format)."""
return {
"meta": {"version": 28},
"libs": [],
"shared": {
"stringArray": list(strings),
},
"threads": [{
"name": "main",
"pid": "1",
"tid": 1,
"funcTable": {
"name": list(range(len(strings))),
"isJS": [False] * len(strings),
"relevantForJS": [False] * len(strings),
"resource": [-1] * len(strings),
"fileName": [None] * len(strings),
"lineNumber": [None] * len(strings),
"columnNumber": [None] * len(strings),
"length": len(strings),
},
"frameTable": {"length": 0},
"stackTable": {"length": 0},
"samples": {"length": 0},
"markers": {"length": 0},
"resourceTable": {"length": 0},
"nativeSymbols": {"length": 0},
}],
"pages": [],
"counters": [],
}
def _make_profile_per_thread(self, strings):
"""Create a profile with per-thread stringArray (samply format)."""
return {
"meta": {"version": 28},
"libs": [],
"threads": [{
"name": "main",
"pid": "1",
"tid": 1,
"stringArray": list(strings),
"funcTable": {
"name": list(range(len(strings))),
"isJS": [False] * len(strings),
"relevantForJS": [False] * len(strings),
"resource": [-1] * len(strings),
"fileName": [None] * len(strings),
"lineNumber": [None] * len(strings),
"columnNumber": [None] * len(strings),
"length": len(strings),
},
"frameTable": {"length": 0},
"stackTable": {"length": 0},
"samples": {"length": 0},
"markers": {"length": 0},
"resourceTable": {"length": 0},
"nativeSymbols": {"length": 0},
}],
"pages": [],
"counters": [],
}
def test_profile_rewrite_shared(self):
from lean_demangle_profile import rewrite_profile
strings = [
"l_Lean_Meta_Sym_main",
"printf",
"lean_apply_5",
"l___private_Lean_Meta_Basic_0__Lean_Meta_foo",
]
profile = self._make_profile_shared(strings)
rewrite_profile(profile)
sa = profile["shared"]["stringArray"]
self.assertEqual(sa[0], "Lean.Meta.Sym.main")
self.assertEqual(sa[1], "printf")
self.assertEqual(sa[2], "<apply/5>")
self.assertEqual(sa[3], "Lean.Meta.foo [private]")
def test_profile_rewrite_per_thread(self):
from lean_demangle_profile import rewrite_profile
strings = [
"l_Lean_Meta_Sym_main",
"printf",
"lean_apply_5",
"l___private_Lean_Meta_Basic_0__Lean_Meta_foo",
]
profile = self._make_profile_per_thread(strings)
count = rewrite_profile(profile)
sa = profile["threads"][0]["stringArray"]
self.assertEqual(sa[0], "Lean.Meta.Sym.main")
self.assertEqual(sa[1], "printf")
self.assertEqual(sa[2], "<apply/5>")
self.assertEqual(sa[3], "Lean.Meta.foo [private]")
self.assertEqual(count, 3)
def test_profile_json_roundtrip(self):
from lean_demangle_profile import process_profile_file
strings = ["l_Lean_Meta_main", "malloc"]
profile = self._make_profile_shared(strings)
with tempfile.NamedTemporaryFile(mode='w', suffix='.json',
delete=False) as f:
json.dump(profile, f)
inpath = f.name
outpath = inpath.replace('.json', '-demangled.json')
try:
process_profile_file(inpath, outpath)
with open(outpath) as f:
result = json.load(f)
self.assertEqual(result["shared"]["stringArray"][0],
"Lean.Meta.main")
self.assertEqual(result["shared"]["stringArray"][1], "malloc")
finally:
os.unlink(inpath)
if os.path.exists(outpath):
os.unlink(outpath)
def test_profile_gzip_roundtrip(self):
from lean_demangle_profile import process_profile_file
strings = ["l_Lean_Meta_main", "malloc"]
profile = self._make_profile_shared(strings)
with tempfile.NamedTemporaryFile(suffix='.json.gz',
delete=False) as f:
with gzip.open(f, 'wt') as gz:
json.dump(profile, gz)
inpath = f.name
outpath = inpath.replace('.json.gz', '-demangled.json.gz')
try:
process_profile_file(inpath, outpath)
with gzip.open(outpath, 'rt') as f:
result = json.load(f)
self.assertEqual(result["shared"]["stringArray"][0],
"Lean.Meta.main")
finally:
os.unlink(inpath)
if os.path.exists(outpath):
os.unlink(outpath)
if __name__ == '__main__':
unittest.main()

View File

@@ -185,30 +185,6 @@ def get_release_notes(tag_name):
except Exception:
return None
def check_release_notes_file_exists(toolchain, github_token):
"""Check if the release notes file exists in the reference-manual repository.
For -rc1 releases, this checks that the release notes have been created.
For subsequent RCs and stable releases, release notes should already exist.
Returns tuple (exists: bool, is_rc1: bool) where is_rc1 indicates if this is
the first release candidate (when release notes need to be written).
"""
# Determine the release notes file path
# e.g., v4.28.0-rc1 -> Manual/Releases/v4_28_0.lean
base_version = strip_rc_suffix(toolchain.lstrip('v')) # "4.28.0"
file_name = f"v{base_version.replace('.', '_')}.lean" # "v4_28_0.lean"
file_path = f"Manual/Releases/{file_name}"
is_rc1 = toolchain.endswith("-rc1")
repo_url = "https://github.com/leanprover/reference-manual"
# Check if the file exists on main branch
content = get_branch_content(repo_url, "main", file_path, github_token)
return (content is not None, is_rc1)
def get_branch_content(repo_url, branch, file_path, github_token):
api_url = repo_url.replace("https://github.com/", "https://api.github.com/repos/") + f"/contents/{file_path}?ref={branch}"
headers = {'Authorization': f'token {github_token}'} if github_token else {}
@@ -525,76 +501,6 @@ def check_proofwidgets4_release(repo_url, target_toolchain, github_token):
print(f" You will need to create and push a tag v0.0.{next_version}")
return False
def check_reference_manual_release_title(repo_url, toolchain, pr_branch, github_token):
"""Check if the reference-manual release notes title matches the release type.
For RC releases (e.g., v4.27.0-rc1), the title should contain the exact RC suffix.
For final releases (e.g., v4.27.0), the title should NOT contain any "-rc".
Returns True if check passes or is not applicable, False if title needs updating.
"""
is_rc = is_release_candidate(toolchain)
# For RC releases, get the base version and RC suffix
# e.g., "v4.27.0-rc1" -> version="4.27.0", rc_suffix="-rc1"
if is_rc:
parts = toolchain.lstrip('v').split('-', 1)
version = parts[0]
rc_suffix = '-' + parts[1] if len(parts) > 1 else ''
else:
version = toolchain.lstrip('v')
rc_suffix = ''
# Construct the release notes file path (e.g., Manual/Releases/v4_27_0.lean for v4.27.0)
file_name = f"v{version.replace('.', '_')}.lean" # "v4_27_0.lean"
file_path = f"Manual/Releases/{file_name}"
# Try to get the file from the PR branch first, then fall back to main branch
content = get_branch_content(repo_url, pr_branch, file_path, github_token)
if content is None:
# Try the default branch
content = get_branch_content(repo_url, "main", file_path, github_token)
if content is None:
print(f" ⚠️ Could not check release notes file: {file_path}")
return True # Don't block on this
# Look for the #doc line with the title
for line in content.splitlines():
if line.strip().startswith('#doc') and 'Manual' in line:
has_rc_in_title = '-rc' in line.lower()
if is_rc:
# For RC releases, title should contain the exact RC suffix (e.g., "-rc1")
# Use regex to match exact suffix followed by non-digit (to avoid -rc1 matching -rc10)
# Pattern matches the RC suffix followed by a non-digit or end-of-string context
# e.g., "-rc1" followed by space, quote, paren, or similar
exact_match = re.search(rf'{re.escape(rc_suffix)}(?![0-9])', line, re.IGNORECASE)
if exact_match:
print(f" ✅ Release notes title correctly shows {rc_suffix}")
return True
elif has_rc_in_title:
print(f" ❌ Release notes title shows wrong RC version (expected {rc_suffix})")
print(f" Update {file_path} to use '{rc_suffix}' in the title")
return False
else:
print(f" ❌ Release notes title missing RC suffix")
print(f" Update {file_path} to include '{rc_suffix}' in the title")
return False
else:
# For final releases, title should NOT contain -rc
if has_rc_in_title:
print(f" ❌ Release notes title still shows RC version")
print(f" Update {file_path} to remove '-rcN' from the title")
return False
else:
print(f" ✅ Release notes title is updated for final release")
return True
# If we didn't find the #doc line, don't block
print(f" ⚠️ Could not find release notes title in {file_path}")
return True
def run_mathlib_verify_version_tags(toolchain, verbose=False):
"""Run mathlib4's verify_version_tags.py script to validate the release tag.
@@ -738,27 +644,6 @@ def main():
else:
print(f" ✅ Release notes page title looks good ('{actual_title}').")
# Check if release notes file exists in reference-manual repository
# For -rc1 releases, this is when release notes need to be written
# For subsequent RCs and stable releases, they should already exist
release_notes_exists, is_rc1 = check_release_notes_file_exists(toolchain, github_token)
base_version = strip_rc_suffix(toolchain.lstrip('v'))
release_notes_file = f"Manual/Releases/v{base_version.replace('.', '_')}.lean"
if not release_notes_exists:
if is_rc1:
print(f" ❌ Release notes file not found: {release_notes_file}")
print(f" This is an -rc1 release, so release notes need to be written.")
print(f" Run `script/release_notes.py --since <previous_version>` to generate them.")
print(f" See doc/dev/release_checklist.md section 'Writing the release notes' for details.")
lean4_success = False
else:
print(f" ❌ Release notes file not found: {release_notes_file}")
print(f" Release notes should have been created for -rc1. Check the reference-manual repository.")
lean4_success = False
else:
print(f" ✅ Release notes file exists: {release_notes_file}")
repo_status["lean4"] = lean4_success
# If the release page doesn't exist, skip repository checks and master branch checks
@@ -824,11 +709,6 @@ def main():
print(f" ⚠️ CI: {ci_message}")
else:
print(f" ❓ CI: {ci_message}")
# For reference-manual, check that the release notes title has been updated
if name == "reference-manual":
pr_branch = f"bump_to_{toolchain}"
check_reference_manual_release_title(url, toolchain, pr_branch, github_token)
else:
print(f" ❌ PR with title '{pr_title}' does not exist")
print(f" Run `script/release_steps.py {toolchain} {name}` to create it")
@@ -836,14 +716,6 @@ def main():
continue
print(f" ✅ On compatible toolchain (>= {toolchain})")
# For reference-manual, check that the release notes title is correct BEFORE tagging.
# This catches the case where the toolchain bump PR was merged without updating
# the release notes title (e.g., still showing "-rc1" for a stable release).
if name == "reference-manual":
if not check_reference_manual_release_title(url, toolchain, branch, github_token):
repo_status[name] = False
continue
# Special handling for ProofWidgets4
if name == "ProofWidgets4":
if not check_proofwidgets4_release(url, toolchain, github_token):
@@ -924,8 +796,8 @@ def main():
print(f" ✅ Bump branch {bump_branch} exists")
# Update the lean-toolchain to the latest nightly for newly created bump branches
if branch_created:
# For batteries and mathlib4, update the lean-toolchain to the latest nightly
if branch_created and name in ["batteries", "mathlib4"]:
latest_nightly = get_latest_nightly_tag(github_token)
if latest_nightly:
nightly_toolchain = f"leanprover/lean4:{latest_nightly}"

View File

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

View File

@@ -24,7 +24,6 @@ What this script does:
- Safety checks for repositories using bump branches
- Custom build and test procedures
- lean-fro.org: runs scripts/update.sh to regenerate site content
- mathlib4: updates ProofWidgets4 pin (v0.0.X sequential tags, not v4.X.Y)
6. Commits the changes with message "chore: bump toolchain to {version}"
@@ -60,8 +59,6 @@ import re
import subprocess
import shutil
import json
import requests
import base64
from pathlib import Path
# Color functions for terminal output
@@ -118,60 +115,6 @@ def find_repo(repo_name, config):
sys.exit(1)
return matching_repos[0]
def get_github_token():
try:
result = subprocess.run(['gh', 'auth', 'token'], capture_output=True, text=True)
if result.returncode == 0:
return result.stdout.strip()
except FileNotFoundError:
pass
return None
def find_proofwidgets_tag(version):
"""Find the latest ProofWidgets4 tag that uses the given toolchain version.
ProofWidgets4 uses sequential version tags (v0.0.X) rather than toolchain-based tags.
This function finds the most recent tag whose lean-toolchain matches the target version
exactly, checking the 20 most recent tags.
"""
github_token = get_github_token()
api_base = "https://api.github.com/repos/leanprover-community/ProofWidgets4"
headers = {'Authorization': f'token {github_token}'} if github_token else {}
response = requests.get(f"{api_base}/git/matching-refs/tags/v0.0.", headers=headers, timeout=30)
if response.status_code != 200:
return None
tags = response.json()
tag_names = []
for tag in tags:
ref = tag['ref']
if ref.startswith('refs/tags/v0.0.'):
tag_name = ref.replace('refs/tags/', '')
try:
version_num = int(tag_name.split('.')[-1])
tag_names.append((version_num, tag_name))
except (ValueError, IndexError):
continue
if not tag_names:
return None
# Sort by version number (descending) and check recent tags
tag_names.sort(reverse=True)
target = f"leanprover/lean4:{version}"
for _, tag_name in tag_names[:20]:
# Fetch lean-toolchain for this tag
api_url = f"{api_base}/contents/lean-toolchain?ref={tag_name}"
resp = requests.get(api_url, headers=headers, timeout=30)
if resp.status_code != 200:
continue
content = base64.b64decode(resp.json().get("content", "").replace("\n", "")).decode('utf-8').strip()
if content == target:
return tag_name
return None
def setup_downstream_releases_dir():
"""Create the downstream_releases directory if it doesn't exist."""
downstream_dir = Path("downstream_releases")
@@ -483,62 +426,6 @@ def execute_release_steps(repo, version, config):
run_command(f'perl -pi -e \'s/"v4\\.[0-9]+(\\.[0-9]+)?(-rc[0-9]+)?"/"' + version + '"/g\' lakefile.*', cwd=repo_path)
run_command("lake update", cwd=repo_path, stream_output=True)
# For reference-manual, update the release notes title to match the target version.
# e.g., for a stable release, change "Lean 4.28.0-rc1 (date)" to "Lean 4.28.0 (date)"
# e.g., for rc2, change "Lean 4.28.0-rc1 (date)" to "Lean 4.28.0-rc2 (date)"
if repo_name == "reference-manual":
base_version = version.lstrip('v').split('-')[0] # "4.28.0"
file_name = f"v{base_version.replace('.', '_')}.lean"
release_notes_file = repo_path / "Manual" / "Releases" / file_name
if release_notes_file.exists():
is_rc = "-rc" in version
if is_rc:
# For RC releases, update to the exact RC version
display_version = version.lstrip('v') # "4.28.0-rc2"
else:
# For stable releases, strip any RC suffix
display_version = base_version # "4.28.0"
print(blue(f"Updating release notes title in {file_name}..."))
content = release_notes_file.read_text()
# Match the #doc line title: "Lean X.Y.Z-rcN (date)" or "Lean X.Y.Z (date)"
new_content = re.sub(
r'(#doc\s+\(Manual\)\s+"Lean\s+)\d+\.\d+\.\d+(-rc\d+)?(\s+\([^)]*\)"\s*=>)',
rf'\g<1>{display_version}\3',
content
)
if new_content != content:
release_notes_file.write_text(new_content)
print(green(f"Updated release notes title to Lean {display_version}"))
else:
print(green("Release notes title already correct"))
else:
print(yellow(f"Release notes file {file_name} not found, skipping title update"))
# For mathlib4, update ProofWidgets4 pin (it uses sequential v0.0.X tags, not v4.X.Y)
if repo_name == "mathlib4":
print(blue("Checking ProofWidgets4 version pin..."))
pw_tag = find_proofwidgets_tag(version)
if pw_tag:
print(blue(f"Updating ProofWidgets4 pin to {pw_tag}..."))
for lakefile in repo_path.glob("lakefile.*"):
content = lakefile.read_text()
# Only update the ProofWidgets4 dependency line, not other v0.0.X pins
new_content = re.sub(
r'(require\s+"leanprover-community"\s*/\s*"proofwidgets"\s*@\s*git\s+"v)0\.0\.\d+(")',
rf'\g<1>{pw_tag.removeprefix("v")}\2',
content
)
if new_content != content:
lakefile.write_text(new_content)
print(green(f"Updated ProofWidgets4 pin in {lakefile.name}"))
run_command("lake update proofwidgets", cwd=repo_path, stream_output=True)
print(green(f"Updated ProofWidgets4 to {pw_tag}"))
else:
print(yellow(f"Could not find a ProofWidgets4 tag for toolchain {version}"))
print(yellow("You may need to update the ProofWidgets4 pin manually"))
# Commit changes (only if there are changes)
print(blue("Checking for changes to commit..."))
try:

File diff suppressed because it is too large Load Diff

View File

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

View File

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

View File

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

View File

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

View File

@@ -102,7 +102,7 @@ noncomputable def strongIndefiniteDescription {α : Sort u} (p : α → Prop) (h
xp.val, fun _ => xp.property)
(fun hp => choice h, fun h => absurd h hp)
/-- The Hilbert epsilon function. -/
/-- the Hilbert epsilon Function -/
noncomputable def epsilon {α : Sort u} [h : Nonempty α] (p : α Prop) : α :=
(strongIndefiniteDescription p h).val
@@ -142,7 +142,6 @@ is classically true but not constructively. -/
/-- Transfer decidability of `¬ p` to decidability of `p`. -/
-- This can not be an instance as it would be tried everywhere.
@[implicit_reducible]
def decidable_of_decidable_not (p : Prop) [h : Decidable (¬ p)] : Decidable p :=
match h with
| isFalse h => isTrue (Classical.not_not.mp h)

View File

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

View File

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

View File

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

View File

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

View File

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

View File

@@ -8,6 +8,7 @@ The identity Monad.
module
prelude
public import Init.Core
public import Init.Control.MonadAttach
public section
@@ -79,11 +80,3 @@ instance : LawfulMonadAttach Id where
exact x.run.2
end Id
/-- Turn a collection with a pure `ForIn` instance into an array. -/
def ForIn.toArray {α : Type u} [inst : ForIn Id ρ α] (xs : ρ) : Array α :=
ForIn.forIn xs Array.empty (fun a acc => pure (.yield (acc.push a))) |> Id.run
/-- Turn a collection with a pure `ForIn` instance into a list. -/
def ForIn.toList {α : Type u} [ForIn Id ρ α] (xs : ρ) : List α :=
ForIn.toArray xs |>.toList

View File

@@ -6,9 +6,7 @@ Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro
module
prelude
public import Init.Control.Id
public import Init.Grind.Tactics
import Init.Ext
public import Init.Ext
public section

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

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

View File

@@ -51,21 +51,6 @@ scoped syntax (name := withAnnotateState)
/-- `skip` does nothing. -/
syntax (name := skip) "skip" : conv
/--
`cbv` performs simplification that closely mimics call-by-value evaluation.
It reduces the target term by unfolding definitions using their defining equations and
applying matcher equations. The unfolding is propositional, so `cbv` also works
with functions defined via well-founded recursion or partial fixpoints.
The proofs produced by `cbv` only use the three standard axioms.
In particular, they do not require trust in the correctness of the code
generator.
This tactic is experimental and its behavior is likely to change in upcoming
releases of Lean.
-/
syntax (name := cbv) "cbv" : conv
/--
Traverses into the left subterm of a binary operator.

View File

@@ -9,15 +9,10 @@ module
prelude
public import Init.SizeOf
public import Init.Tactics
public section
set_option linter.missingDocs true -- keep it documented
-- BEq instance for Option defined here so it's available early in the import chain
-- (before Init.Grind.Config and Init.MetaTypes which need BEq (Option Nat))
deriving instance BEq for Option
@[expose] section
universe u v w
@@ -342,7 +337,7 @@ inductive Exists {α : Sort u} (p : α → Prop) : Prop where
An indication of whether a loop's body terminated early that's used to compile the `for x in xs`
notation.
A collection's `ForIn` or `ForIn'` instance describes how to iterate over its elements. The monadic
A collection's `ForIn` or `ForIn'` instance describe's how to iterate over its elements. The monadic
action that represents the body of the loop returns a `ForInStep α`, where `α` is the local state
used to implement features such as `let mut`.
-/
@@ -489,8 +484,6 @@ class HasEquiv (α : Sort u) where
the notion of equivalence is type-dependent. -/
Equiv : α α Sort v
attribute [reducible] HasEquiv.Equiv
@[inherit_doc] infix:50 "" => HasEquiv.Equiv
recommended_spelling "equiv" for "" in [HasEquiv.Equiv, «term__»]
@@ -517,12 +510,12 @@ abbrev SSuperset [HasSSubset α] (a b : α) := SSubset b a
/-- Notation type class for the union operation ``. -/
class Union (α : Type u) where
/-- `a b` is the union of `a` and `b`. -/
/-- `a b` is the union of`a` and `b`. -/
union : α α α
/-- Notation type class for the intersection operation `∩`. -/
class Inter (α : Type u) where
/-- `a ∩ b` is the intersection of `a` and `b`. -/
/-- `a ∩ b` is the intersection of`a` and `b`. -/
inter : α α α
/-- Notation type class for the set difference `\`. -/
@@ -545,10 +538,10 @@ infix:50 " ⊇ " => Superset
/-- Strict superset relation: `a ⊃ b` -/
infix:50 "" => SSuperset
/-- `a b` is the union of `a` and `b`. -/
/-- `a b` is the union of`a` and `b`. -/
infixl:65 " " => Union.union
/-- `a ∩ b` is the intersection of `a` and `b`. -/
/-- `a ∩ b` is the intersection of`a` and `b`. -/
infixl:70 "" => Inter.inter
/--
@@ -935,14 +928,6 @@ noncomputable def HEq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : {β : Sor
noncomputable def HEq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : {β : Sort u2} β Sort u1} {β : Sort u2} {b : β} (h : a b) (m : motive a) : motive b :=
h.rec m
/-- `HEq.ndrec` specialized to homogeneous heterogeneous equality -/
noncomputable def HEq.homo_ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : α Sort u1} (m : motive a) {b : α} (h : a b) : motive b :=
(eq_of_heq h).ndrec m
/-- `HEq.ndrec` specialized to homogeneous heterogeneous equality, symmetric variant -/
noncomputable def HEq.homo_ndrec_symm.{u1, u2} {α : Sort u2} {a : α} {motive : α Sort u1} (m : motive a) {b : α} (h : b a) : motive b :=
(eq_of_heq h).ndrec_symm m
/-- `HEq.ndrec` variant -/
noncomputable def HEq.elim {α : Sort u} {a : α} {p : α Sort v} {b : α} (h₁ : a b) (h₂ : p a) : p b :=
eq_of_heq h₁ h₂
@@ -1339,10 +1324,10 @@ transitive and contains `r`. `TransGen r a z` if and only if there exists a sequ
-/
inductive Relation.TransGen {α : Sort u} (r : α α Prop) : α α Prop
/-- If `r a b`, then `TransGen r a b`. This is the base case of the transitive closure. -/
| single {a b : α} : r a b TransGen r a b
| single {a b} : r a b TransGen r a b
/-- If `TransGen r a b` and `r b c`, then `TransGen r a c`.
This is the inductive case of the transitive closure. -/
| tail {a b c : α} : TransGen r a b r b c TransGen r a c
| tail {a b c} : TransGen r a b r b c TransGen r a c
/-- The transitive closure is transitive. -/
theorem Relation.TransGen.trans {α : Sort u} {r : α α Prop} {a b c} :
@@ -1489,29 +1474,6 @@ def Prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂
/-! # Dependent products -/
instance {α : Type u} {β : α Type v} [h₁ : DecidableEq α] [h₂ : a, DecidableEq (β a)] :
DecidableEq (Sigma β)
| a₁, b₁, a₂, b₂ =>
match a₁, b₁, a₂, b₂, h₁ a₁ a₂ with
| _, b₁, _, b₂, isTrue (Eq.refl _) =>
match b₁, b₂, h₂ _ b₁ b₂ with
| _, _, isTrue (Eq.refl _) => isTrue rfl
| _, _, isFalse n => isFalse fun h
Sigma.noConfusion rfl .rfl (heq_of_eq h) fun _ e₂ n (eq_of_heq e₂)
| _, _, _, _, isFalse n => isFalse fun h
Sigma.noConfusion rfl .rfl (heq_of_eq h) fun e₁ _ n (eq_of_heq e₁)
instance {α : Sort u} {β : α Sort v} [h₁ : DecidableEq α] [h₂ : a, DecidableEq (β a)] : DecidableEq (PSigma β)
| a₁, b₁, a₂, b₂ =>
match a₁, b₁, a₂, b₂, h₁ a₁ a₂ with
| _, b₁, _, b₂, isTrue (Eq.refl _) =>
match b₁, b₂, h₂ _ b₁ b₂ with
| _, _, isTrue (Eq.refl _) => isTrue rfl
| _, _, isFalse n => isFalse fun h
PSigma.noConfusion rfl .rfl (heq_of_eq h) fun _ e₂ n (eq_of_heq e₂)
| _, _, _, _, isFalse n => isFalse fun h
PSigma.noConfusion rfl .rfl (heq_of_eq h) fun e₁ _ n (eq_of_heq e₁)
theorem Exists.of_psigma_prop {α : Sort u} {p : α Prop} : (PSigma (fun x => p x)) Exists (fun x => p x)
| x, hx => x, hx
@@ -1599,10 +1561,6 @@ instance {p q : Prop} [d : Decidable (p ↔ q)] : Decidable (p = q) :=
| isTrue h => isTrue (propext h)
| isFalse h => isFalse fun heq => h (heq Iff.rfl)
/-- Helper theorem for proving injectivity theorems -/
theorem Lean.injEq_helper {P Q R : Prop} :
(P Q R) (P Q R) := by intro h h₁,h₂; exact h h₁ h₂
gen_injective_theorems% Array
gen_injective_theorems% BitVec
gen_injective_theorems% ByteArray
@@ -2313,13 +2271,6 @@ instance Pi.instSubsingleton {α : Sort u} {β : α → Sort v} [∀ a, Subsingl
/-! # Squash -/
theorem equivalence_true (α : Sort u) : Equivalence fun _ _ : α => True :=
fun _ => trivial, fun _ => trivial, fun _ _ => trivial
/-- Always-true relation as a `Setoid`. -/
protected def Setoid.trivial (α : Sort u) : Setoid α :=
_, equivalence_true α
/--
The quotient of `α` by the universal relation. The elements of `Squash α` are those of `α`, but all
of them are equal and cannot be distinguished.
@@ -2333,11 +2284,8 @@ and its representation in compiled code is identical to that of `α`.
Consequently, `Squash.lift` may extract an `α` value into any subsingleton type `β`, while
`Nonempty.rec` can only do the same when `β` is a proposition.
`Squash` is defined in terms of `Quotient`, so `Squash` can be used when a `Quotient` argument is
expected.
-/
def Squash (α : Sort u) := Quotient (Setoid.trivial α)
def Squash (α : Sort u) := Quot (fun (_ _ : α) => True)
/--
Places a value into its squash type, in which it cannot be distinguished from any other.
@@ -2373,10 +2321,8 @@ namespace Lean
/--
Depends on the correctness of the Lean compiler, interpreter, and all `[implemented_by ...]` and `[extern ...]` annotations.
-/
@[deprecated "in-kernel native reduction is deprecated; assert native evaluations with axioms instead" (since := "2026-02-01")]
axiom trustCompiler : True
set_option linter.deprecated false in
/--
When the kernel tries to reduce a term `Lean.reduceBool c`, it will invoke the Lean interpreter to evaluate `c`.
The kernel will not use the interpreter if `c` is not a constant.
@@ -2396,13 +2342,11 @@ Recall that the compiler trusts the correctness of all `[implemented_by ...]` an
If an extern function is executed, then the trusted code base will also include the implementation of the associated
foreign function.
-/
@[deprecated "in-kernel native reduction is deprecated; assert native evaluations with axioms instead" (since := "2026-02-01")]
opaque reduceBool (b : Bool) : Bool :=
-- This ensures that `#print axioms` will track use of `reduceBool`.
have := trustCompiler
b
set_option linter.deprecated false in
/--
Similar to `Lean.reduceBool` for closed `Nat` terms.
@@ -2410,14 +2354,12 @@ Remark: we do not have plans for supporting a generic `reduceValue {α} (a : α)
The main issue is that it is non-trivial to convert an arbitrary runtime object back into a Lean expression.
We believe `Lean.reduceBool` enables most interesting applications (e.g., proof by reflection).
-/
@[deprecated "in-kernel native reduction is deprecated; assert native evaluations with axioms instead" (since := "2026-02-01")]
opaque reduceNat (n : Nat) : Nat :=
-- This ensures that `#print axioms` will track use of `reduceNat`.
have := trustCompiler
n
set_option linter.deprecated false in
/--
The axiom `ofReduceBool` is used to perform proofs by reflection. See `reduceBool`.
@@ -2431,10 +2373,8 @@ external type checkers that do not implement this feature.
Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter.
So, you are mainly losing the capability of type checking your development using external checkers.
-/
@[deprecated "in-kernel native reduction is deprecated; assert native evaluations with axioms instead" (since := "2026-02-01")]
axiom ofReduceBool (a b : Bool) (h : reduceBool a = b) : a = b
set_option linter.deprecated false in
/--
The axiom `ofReduceNat` is used to perform proofs by reflection. See `reduceBool`.
@@ -2444,7 +2384,6 @@ external type checkers that do not implement this feature.
Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter.
So, you are mainly losing the capability of type checking your development using external checkers.
-/
@[deprecated "in-kernel native reduction is deprecated; assert native evaluations with axioms instead" (since := "2026-02-01")]
axiom ofReduceNat (a b : Nat) (h : reduceNat a = b) : a = b
@@ -2495,7 +2434,7 @@ class IdempotentOp (op : ααα) : Prop where
idempotent : (x : α) op x x = x
/--
`LeftIdentity op o` indicates `o` is a left identity of `op`.
`LeftIdentify op o` indicates `o` is a left identity of `op`.
This class does not require a proof that `o` is an identity, and
is used primarily for inferring the identity using class resolution.
@@ -2503,7 +2442,7 @@ is used primarily for inferring the identity using class resolution.
class LeftIdentity (op : α β β) (o : outParam α) : Prop
/--
`LawfulLeftIdentity op o` indicates `o` is a verified left identity of
`LawfulLeftIdentify op o` indicates `o` is a verified left identity of
`op`.
-/
class LawfulLeftIdentity (op : α β β) (o : outParam α) : Prop extends LeftIdentity op o where
@@ -2511,7 +2450,7 @@ class LawfulLeftIdentity (op : α → β → β) (o : outParam α) : Prop extend
left_id : a, op o a = a
/--
`RightIdentity op o` indicates `o` is a right identity `o` of `op`.
`RightIdentify op o` indicates `o` is a right identity `o` of `op`.
This class does not require a proof that `o` is an identity, and is used
primarily for inferring the identity using class resolution.
@@ -2519,7 +2458,7 @@ primarily for inferring the identity using class resolution.
class RightIdentity (op : α β α) (o : outParam β) : Prop
/--
`LawfulRightIdentity op o` indicates `o` is a verified right identity of
`LawfulRightIdentify op o` indicates `o` is a verified right identity of
`op`.
-/
class LawfulRightIdentity (op : α β α) (o : outParam β) : Prop extends RightIdentity op o where
@@ -2593,11 +2532,3 @@ class Trichotomous (r : αα → Prop) : Prop where
trichotomous (a b : α) : ¬ r a b ¬ r b a a = b
end Std
@[simp] theorem flip_flip {α : Sort u} {β : Sort v} {φ : Sort w} {f : α β φ} :
flip (flip f) = f := by
apply funext
intro a
apply funext
intro b
rw [flip, flip]

View File

@@ -7,9 +7,7 @@ Authors: Dany Fabian
module
prelude
public import Init.GetElem
import Init.ByCases
import Init.PropLemmas
public import Init.ByCases
@[expose] public section

View File

@@ -30,8 +30,3 @@ public import Init.Data.Array.Erase
public import Init.Data.Array.Zip
public import Init.Data.Array.InsertIdx
public import Init.Data.Array.Extract
public import Init.Data.Array.MinMax
public import Init.Data.Array.Nat
public import Init.Data.Array.Int
public import Init.Data.Array.Count
public import Init.Data.Array.Sort

View File

@@ -6,10 +6,8 @@ Authors: Joachim Breitner, Mario Carneiro
module
prelude
public import Init.Data.Array.Count
import all Init.Data.List.Attach
public import Init.Data.Array.Lemmas
import Init.Data.Array.Bootstrap
import Init.Data.Array.Count
public section

View File

@@ -6,15 +6,11 @@ Authors: Leonardo de Moura
module
prelude
public import Init.Control.Do
public import Init.GetElem
public import Init.Data.List.ToArrayImpl
import all Init.Data.List.ToArrayImpl
public import Init.Data.Array.Set
import all Init.Data.Array.Set
public import Init.WF
meta import Init.MetaTypes
import Init.WFTactics
public section
@@ -171,15 +167,6 @@ This avoids overhead due to unboxing a `Nat` used as an index.
def uget (xs : @& Array α) (i : USize) (h : i.toNat < xs.size) : α :=
xs[i.toNat]
/--
Version of `Array.uget` that does not increment the reference count of its result.
This is only intended for direct use by the compiler.
-/
@[extern "lean_array_uget_borrowed"]
unsafe opaque ugetBorrowed (xs : @& Array α) (i : USize) (h : i.toNat < xs.size) : α :=
xs.uget i h
/--
Low-level modification operator which is as fast as a C array write. The modification is performed
in-place when the reference to the array is unique.
@@ -2135,7 +2122,7 @@ Examples:
/-! ### Repr and ToString -/
protected def repr {α : Type u} [Repr α] (xs : Array α) : Std.Format :=
protected def Array.repr {α : Type u} [Repr α] (xs : Array α) : Std.Format :=
let _ : Std.ToFormat α := repr
if xs.size == 0 then
"#[]"

View File

@@ -7,9 +7,7 @@ module
prelude
import all Init.Data.Array.Basic
public import Init.Data.Array.Set
public import Init.Util
import Init.Data.Nat.Linear
public import Init.Data.Nat.Linear
public section

View File

@@ -6,10 +6,7 @@ Authors: Leonardo de Moura
module
prelude
public import Init.Data.Array.Basic
import Init.Data.Bool
import Init.Omega
import Init.WFTactics
public import Init.Data.Int.DivMod.Lemmas
public section
universe u v

View File

@@ -7,10 +7,8 @@ Authors: Mario Carneiro
module
prelude
public import Init.Data.List.TakeDrop
import all Init.Data.Array.Basic
public import Init.Data.List.Control
import Init.Data.List.Lemmas
import Init.Data.List.TakeDrop
public section
@@ -52,9 +50,7 @@ theorem foldrM_eq_reverse_foldlM_toList.aux [Monad m]
unfold foldrM.fold
match i with
| 0 => simp
| i+1 =>
set_option backward.isDefEq.respectTransparency false in
rw [ List.take_concat_get h]; simp [ aux]
| i+1 => rw [ List.take_concat_get h]; simp [ aux]
theorem foldrM_eq_reverse_foldlM_toList [Monad m] {f : α β m β} {init : β} {xs : Array α} :
xs.foldrM f init = xs.toList.reverse.foldlM (fun x y => f y x) init := by

View File

@@ -7,14 +7,8 @@ module
prelude
import all Init.Data.Array.Basic
import Init.Grind.Util -- shake: keep (`@[grind]` dependency)
public import Init.BinderPredicates
public import Init.Ext
public import Init.NotationExtra
import Init.Data.Array.Lemmas
import Init.Data.Bool
import Init.Data.List.Count
import Init.Data.List.Nat.Count
public import Init.Data.Array.Lemmas
public import Init.Data.List.Nat.Count
public section
@@ -98,18 +92,6 @@ theorem countP_le_size : countP p xs ≤ xs.size := by
rcases xs with xs
simp
/-- This lemma is only relevant for `grind`. -/
@[grind =]
theorem _root_.Std.Internal.Array.countP_eq_zero_of_forall {xs : Array α} (h : x xs, ¬ p x) : xs.countP p = 0 :=
countP_eq_zero.mpr h
/-- This lemma is only relevant for `grind`. -/
theorem _root_.Std.Internal.Array.not_of_countP_eq_zero_of_mem {xs : Array α} (h : xs.countP p = 0) (h' : x xs) : ¬ p x :=
countP_eq_zero.mp h _ h'
grind_pattern Std.Internal.Array.not_of_countP_eq_zero_of_mem => xs.countP p, x xs where
guard xs.countP p = 0
@[simp] theorem countP_eq_size {p} : countP p xs = xs.size a xs, p a := by
rcases xs with xs
simp
@@ -117,13 +99,11 @@ grind_pattern Std.Internal.Array.not_of_countP_eq_zero_of_mem => xs.countP p, x
theorem countP_replicate {a : α} {n : Nat} : countP p (replicate n a) = if p a then n else 0 := by
simp [ List.toArray_replicate, List.countP_replicate]
set_option backward.isDefEq.respectTransparency false in
theorem boole_getElem_le_countP {xs : Array α} {i : Nat} (h : i < xs.size) :
(if p xs[i] then 1 else 0) xs.countP p := by
rcases xs with xs
simp [List.boole_getElem_le_countP]
set_option backward.isDefEq.respectTransparency false in
@[grind =]
theorem countP_set {xs : Array α} {i : Nat} {a : α} (h : i < xs.size) :
(xs.set i a).countP p = xs.countP p - (if p xs[i] then 1 else 0) + (if p a then 1 else 0) := by

View File

@@ -7,14 +7,8 @@ module
prelude
import all Init.Data.Array.Basic
public import Init.Data.Array.Basic
public import Init.Data.Nat.Lemmas
import Init.ByCases
import Init.Classical
import Init.Data.BEq
import Init.Data.Bool
import Init.Data.List.Nat.BEq
import Init.RCases
public import Init.Data.BEq
public import Init.Data.List.Nat.BEq
public section
@@ -76,7 +70,7 @@ theorem isEqv_eq_decide (xs ys : Array α) (r) :
simpa [isEqv_iff_rel] using h'
@[simp, grind =] theorem isEqv_toList [BEq α] (xs ys : Array α) : (xs.toList.isEqv ys.toList r) = (xs.isEqv ys r) := by
simp [isEqv_eq_decide, List.isEqv_eq_decide, Array.size]; rfl
simp [isEqv_eq_decide, List.isEqv_eq_decide, Array.size]
theorem eq_of_isEqv [DecidableEq α] (xs ys : Array α) (h : Array.isEqv xs ys (fun x y => x = y)) : xs = ys := by
have h, h' := rel_of_isEqv h
@@ -87,7 +81,6 @@ private theorem isEqvAux_self (r : αα → Bool) (hr : ∀ a, r a a) (xs :
induction i with
| zero => simp [Array.isEqvAux]
| succ i ih =>
set_option backward.isDefEq.respectTransparency false in
simp_all only [isEqvAux, Bool.and_self]
theorem isEqv_self_beq [BEq α] [ReflBEq α] (xs : Array α) : Array.isEqv xs xs (· == ·) = true := by
@@ -132,29 +125,13 @@ instance instDecidableEmpEq (ys : Array α) : Decidable (#[] = ys) :=
| [] => isTrue rfl
| _ :: _ => isFalse (fun h => Array.noConfusion rfl (heq_of_eq h) (fun h => List.noConfusion rfl h))
@[inline]
def instDecidableEqEmpImpl (xs : Array α) : Decidable (xs = #[]) :=
decidable_of_iff xs.isEmpty <| by rcases xs with <;> simp [Array.isEmpty]
@[inline]
def instDecidableEmpEqImpl (xs : Array α) : Decidable (#[] = xs) :=
decidable_of_iff xs.isEmpty <| by rcases xs with <;> simp [Array.isEmpty]
@[csimp]
theorem instDecidableEqEmp_csimp : @instDecidableEqEmp = @instDecidableEqEmpImpl :=
Subsingleton.allEq _ _
@[csimp]
theorem instDecidableEmpEq_csimp : @instDecidableEmpEq = @instDecidableEmpEqImpl :=
Subsingleton.allEq _ _
theorem beq_eq_decide [BEq α] (xs ys : Array α) :
(xs == ys) = if h : xs.size = ys.size then
decide ( (i : Nat) (h' : i < xs.size), xs[i] == ys[i]'(h h')) else false := by
simp [BEq.beq, isEqv_eq_decide]
@[simp, grind =] theorem beq_toList [BEq α] (xs ys : Array α) : (xs.toList == ys.toList) = (xs == ys) := by
simp [beq_eq_decide, List.beq_eq_decide, Array.size]; rfl
simp [beq_eq_decide, List.beq_eq_decide, Array.size]
end Array

View File

@@ -8,13 +8,6 @@ module
prelude
import all Init.Data.Array.Basic
public import Init.Data.Array.Lemmas
import Init.Data.Array.Bootstrap
import Init.Data.Bool
import Init.Data.List.Erase
import Init.Data.List.Nat.Basic
import Init.Data.List.Nat.Erase
import Init.Data.List.TakeDrop
import Init.Omega
public section
@@ -329,7 +322,7 @@ theorem eraseIdx_eq_take_drop_succ {xs : Array α} {i : Nat} (h) :
rcases xs with xs
simp only [List.size_toArray] at h
simp only [List.eraseIdx_toArray, List.eraseIdx_eq_take_drop_succ, take_eq_extract,
List.extract_toArray, List.extract_eq_take_drop, Nat.sub_zero, List.drop_zero, drop_eq_extract,
List.extract_toArray, List.extract_eq_drop_take, Nat.sub_zero, List.drop_zero, drop_eq_extract,
List.size_toArray, List.append_toArray, mk.injEq, List.append_cancel_left_eq]
rw [List.take_of_length_le]
simp

View File

@@ -6,16 +6,7 @@ Authors: Kim Morrison
module
prelude
public import Init.BinderPredicates
public import Init.Ext
public import Init.NotationExtra
import Init.ByCases
import Init.Data.Array.Bootstrap
import Init.Data.Array.Lemmas
import Init.Data.Bool
import Init.Data.List.Nat.TakeDrop
import Init.Data.List.TakeDrop
import Init.Omega
public import Init.Data.Array.Lemmas
public section

View File

@@ -6,11 +6,7 @@ Authors: François G. Dorais
module
prelude
public import Init.Data.Array.Basic
import Init.Data.Array.Lemmas
import Init.Data.Array.OfFn
import Init.Data.Fin.Lemmas
import Init.Omega
public import Init.Data.Array.OfFn
public section

View File

@@ -6,22 +6,9 @@ Authors: Kim Morrison
module
prelude
import Init.Data.List.Nat.Sum
public import Init.Data.List.Nat.Find
import all Init.Data.Array.Basic
public import Init.Data.Array.Attach
public import Init.Data.Option.BasicAux
import Init.ByCases
import Init.Data.Array.Bootstrap
import Init.Data.Array.MapIdx
import Init.Data.Bool
import Init.Data.Fin.Lemmas
import Init.Data.List.Count
import Init.Data.List.Find
import Init.Data.List.Impl
import Init.Data.List.Nat.Find
import Init.Data.List.Nat.TakeDrop
import Init.Data.List.TakeDrop
import Init.Omega
public import Init.Data.Array.Range
public section
@@ -83,10 +70,6 @@ theorem findSome?_eq_some_iff {f : α → Option β} {xs : Array α} {b : β} :
· rintro xs, a, ys, h₀, h₁, h₂
exact xs.toList, a, ys.toList, by simpa using congrArg toList h₀, h₁, by simpa
theorem isSome_findSome? {xs : Array α} {f : α Option β} :
(xs.findSome? f).isSome = xs.any (f · |>.isSome) := by
simp [ findSome?_toList, List.isSome_findSome?]
@[simp, grind =] theorem findSome?_guard {xs : Array α} : findSome? (Option.guard p) xs = find? p xs := by
cases xs; simp
@@ -131,7 +114,7 @@ theorem getElem_zero_flatten.proof {xss : Array (Array α)} (h : 0 < xss.flatten
simp only [List.findSome?_toArray, List.findSome?_map, Function.comp_def, List.getElem?_toArray,
List.findSome?_isSome_iff, isSome_getElem?]
simp only [flatten_toArray_map_toArray, List.size_toArray, List.length_flatten,
List.sum_pos_iff_exists_pos_nat, List.mem_map] at h
Nat.sum_pos_iff_exists_pos, List.mem_map] at h
obtain _, xs, m, rfl, h := h
exact xs, m, by simpa using h
@@ -201,10 +184,6 @@ theorem find?_eq_some_iff_append {xs : Array α} :
exact as.toList, l, by simpa using congrArg Array.toList h',
by simpa using h
theorem isSome_find? {xs : Array α} {f : α Bool} :
(xs.find? f).isSome = xs.any (f ·) := by
simp [ find?_toList, List.isSome_find?]
theorem find?_push {xs : Array α} : (xs.push a).find? p = (xs.find? p).or (if p a then some a else none) := by
cases xs; simp
@@ -433,7 +412,6 @@ theorem lt_findIdx_of_not {p : α → Bool} {xs : Array α} {i : Nat} (h : i < x
simp only [Nat.not_lt] at f
exact absurd (@findIdx_getElem _ p xs (Nat.lt_of_le_of_lt f h)) (h2 (xs.findIdx p) f)
set_option backward.isDefEq.respectTransparency false in
/-- `xs.findIdx p = i` iff `p xs[i]` and `¬ p xs [j]` for all `j < i`. -/
theorem findIdx_eq {p : α Bool} {xs : Array α} {i : Nat} (h : i < xs.size) :
xs.findIdx p = i p xs[i] j (hji : j < i), p (xs[j]'(Nat.lt_trans hji h)) = false := by
@@ -622,12 +600,12 @@ theorem findIdx?_eq_some_le_of_findIdx?_eq_some {xs : Array α} {p q : α → Bo
/-! ### findFinIdx? -/
@[grind =]
theorem findFinIdx?_empty {p : α Bool} : findFinIdx? p #[] = none := by simp; rfl
theorem findFinIdx?_empty {p : α Bool} : findFinIdx? p #[] = none := by simp
@[grind =]
theorem findFinIdx?_singleton {a : α} {p : α Bool} :
#[a].findFinIdx? p = if p a then some 0, by simp else none := by
simp; rfl
simp
-- We can't mark this as a `@[congr]` lemma since the head of the RHS is not `findFinIdx?`.
theorem findFinIdx?_congr {p : α Bool} {xs ys : Array α} (w : xs = ys) :
@@ -696,39 +674,6 @@ theorem isNone_findFinIdx? {xs : Array α} {p : α → Bool} :
simp only [Option.map_map, Function.comp_def, Fin.cast_cast]
simp [Array.size]
/-! ### find? and findFinIdx? -/
theorem find?_eq_map_findFinIdx?_getElem {xs : Array α} {p : α Bool} :
xs.find? p = (xs.findFinIdx? p).map (xs[·]) := by
cases xs
simp [List.find?_eq_map_findFinIdx?_getElem]
rfl
theorem find?_eq_bind_findIdx?_getElem? {xs : Array α} {p : α Bool} :
xs.find? p = (xs.findIdx? p).bind (xs[·]?) := by
cases xs
simp [List.find?_eq_bind_findIdx?_getElem?]
theorem find?_eq_getElem?_findIdx {xs : Array α} {p : α Bool} :
xs.find? p = xs[xs.findIdx p]? := by
cases xs
simp [List.find?_eq_getElem?_findIdx]
theorem findIdx?_eq_bind_find?_idxOf? [BEq α] [LawfulBEq α] {xs : Array α} {p : α Bool} :
xs.findIdx? p = (xs.find? p).bind (xs.idxOf? ·) := by
cases xs
simp [List.findIdx?_eq_bind_find?_idxOf?]
theorem findFinIdx?_eq_bind_find?_finIdxOf? [BEq α] [LawfulBEq α] {xs : Array α} {p : α Bool} :
xs.findFinIdx? p = (xs.find? p).bind (xs.finIdxOf? ·) := by
cases xs
simp [List.findFinIdx?_eq_bind_find?_finIdxOf?]
theorem findIdx_eq_getD_bind_find?_idxOf? [BEq α] [LawfulBEq α] {xs : Array α} {p : α Bool} :
xs.findIdx p = ((xs.find? p).bind (xs.idxOf? ·)).getD xs.size := by
cases xs
simp [List.findIdx_eq_getD_bind_find?_idxOf?]
/-! ### idxOf
The verification API for `idxOf` is still incomplete.
@@ -801,7 +746,7 @@ theorem idxOf?_eq_map_finIdxOf?_val [BEq α] {xs : Array α} {a : α} :
xs.idxOf? a = (xs.finIdxOf? a).map (·.val) := by
simp [idxOf?, finIdxOf?]
@[grind =] theorem finIdxOf?_empty [BEq α] : (#[] : Array α).finIdxOf? a = none := by simp; rfl
@[grind =] theorem finIdxOf?_empty [BEq α] : (#[] : Array α).finIdxOf? a = none := by simp
@[simp, grind =] theorem finIdxOf?_eq_none_iff [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
xs.finIdxOf? a = none a xs := by

View File

@@ -7,8 +7,7 @@ Authors: Leonardo de Moura
module
prelude
public import Init.GetElem
import Init.Data.Array.Basic
public import Init.Data.Array.Basic
public section

View File

@@ -6,11 +6,7 @@ Authors: Kim Morrison
module
prelude
public import Init.Data.Array.Basic
import Init.Data.List.Nat.InsertIdx
import Init.Data.List.ToArray
import Init.Data.Nat.Lemmas
import Init.Omega
public import Init.Data.Array.Lemmas
public section

View File

@@ -1,77 +0,0 @@
/-
Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kim Morrison, Sebastian Graf, Paul Reichert
-/
module
prelude
public import Init.Data.List.Int.Sum
public import Init.Data.Array.MinMax
import Init.Data.Int.Lemmas
public section
set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
set_option linter.indexVariables true -- Enforce naming conventions for index variables.
namespace Array
@[simp] theorem sum_replicate_int {n : Nat} {a : Int} : (replicate n a).sum = n * a := by
rw [ List.toArray_replicate, List.sum_toArray]
simp
theorem sum_append_int {as₁ as₂ : Array Int} : (as₁ ++ as₂).sum = as₁.sum + as₂.sum := by
simp [sum_append]
theorem sum_reverse_int (xs : Array Int) : xs.reverse.sum = xs.sum := by
simp [sum_reverse]
theorem sum_eq_foldl_int {xs : Array Int} : xs.sum = xs.foldl (init := 0) (· + ·) := by
simp only [foldl_eq_foldr_reverse, Int.add_comm, sum_eq_foldr, sum_reverse_int]
theorem min_mul_length_le_sum_int {xs : Array Int} (h : xs #[]) :
xs.min h * xs.size xs.sum := by
rcases xs with l
simpa [List.min_toArray, List.sum_toArray] using List.min_mul_length_le_sum_int (by simpa using h)
theorem mul_length_le_sum_of_min?_eq_some_int {xs : Array Int} (h : xs.min? = some x) :
x * xs.size xs.sum := by
rcases xs with l
simpa [List.min?_toArray, List.sum_toArray] using
List.mul_length_le_sum_of_min?_eq_some_int (by simpa using h)
theorem min_le_sum_div_length_int {xs : Array Int} (h : xs #[]) :
xs.min h xs.sum / xs.size := by
rcases xs with l
simpa [List.min_toArray, List.sum_toArray] using List.min_le_sum_div_length_int (by simpa using h)
theorem le_sum_div_length_of_min?_eq_some_int {xs : Array Int} (h : xs.min? = some x) :
x xs.sum / xs.size := by
rcases xs with l
simpa [List.min?_toArray, List.sum_toArray] using
List.le_sum_div_length_of_min?_eq_some_int (by simpa using h)
theorem sum_le_max_mul_length_int {xs : Array Int} (h : xs #[]) :
xs.sum xs.max h * xs.size := by
rcases xs with l
simpa [List.max_toArray, List.sum_toArray] using List.sum_le_max_mul_length_int (by simpa using h)
theorem sum_le_max_mul_length_of_max?_eq_some_int {xs : Array Int} (h : xs.max? = some x) :
xs.sum x * xs.size := by
rcases xs with l
simpa [List.max?_toArray, List.sum_toArray] using
List.sum_le_max_mul_length_of_max?_eq_some_int (by simpa using h)
theorem sum_div_length_le_max_int {xs : Array Int} (h : xs #[]) :
xs.sum / xs.size xs.max h := by
rcases xs with l
simpa [List.max_toArray, List.sum_toArray] using List.sum_div_length_le_max_int (by simpa using h)
theorem sum_div_length_le_max_of_max?_eq_some_int {xs : Array Int} (h : xs.max? = some x) :
xs.sum / xs.size x := by
rcases xs with l
simpa [List.max?_toArray, List.sum_toArray] using
List.sum_div_length_le_max_of_max?_eq_some_int (by simpa using h)
end Array

View File

@@ -6,28 +6,14 @@ Authors: Mario Carneiro, Kim Morrison
module
prelude
public import Init.Data.List.Nat.Basic
public import Init.Data.Array.Mem
public import Init.Data.Array.DecidableEq
public import Init.Data.Range.Lemmas
public import Init.Data.List.ToArray
import all Init.Data.List.Control
import all Init.Data.Array.Basic
import all Init.Data.Array.Bootstrap
public import Init.Data.Nat.Lemmas
public import Init.Data.Nat.MinMax
import Init.ByCases
import Init.Data.Array.DecidableEq
import Init.Data.Bool
import Init.Data.Fin.Lemmas
import Init.Data.List.Find
import Init.Data.List.Nat.Basic
import Init.Data.List.Nat.Modify
import Init.Data.List.Nat.TakeDrop
import Init.Data.List.Range
import Init.Data.List.Zip
import Init.Data.Nat.Linear
import Init.Data.Nat.Simproc
import Init.Data.Option.Lemmas
import Init.Data.Prod
import Init.Omega
import Init.TacticsExtra
public section
@@ -72,9 +58,6 @@ theorem toArray_eq : List.toArray as = xs ↔ as = xs.toList := by
/-! ### size -/
theorem size_singleton {x : α} : #[x].size = 1 := by
simp
theorem eq_empty_of_size_eq_zero (h : xs.size = 0) : xs = #[] := by
cases xs
simp_all
@@ -132,8 +115,7 @@ theorem none_eq_getElem?_iff {xs : Array α} {i : Nat} : none = xs[i]? ↔ xs.si
theorem getElem?_eq_none {xs : Array α} (h : xs.size i) : xs[i]? = none := by
simp [h]
grind_pattern Array.getElem?_eq_none => xs.size, xs[i]? where
guard xs.size i
grind_pattern Array.getElem?_eq_none => xs.size, xs[i]?
@[simp] theorem getElem?_eq_getElem {xs : Array α} {i : Nat} (h : i < xs.size) : xs[i]? = some xs[i] :=
getElem?_pos ..
@@ -173,7 +155,6 @@ theorem getD_getElem? {xs : Array α} {i : Nat} {d : α} :
@[simp] theorem getElem?_empty {i : Nat} : (#[] : Array α)[i]? = none := rfl
set_option backward.isDefEq.respectTransparency false in
theorem getElem_push_lt {xs : Array α} {x : α} {i : Nat} (h : i < xs.size) :
have : i < (xs.push x).size := by simp [*, Nat.lt_succ_of_le, Nat.le_of_lt]
(xs.push x)[i] = xs[i] := by
@@ -500,18 +481,9 @@ theorem mem_iff_getElem {a} {xs : Array α} : a ∈ xs ↔ ∃ (i : Nat) (h : i
theorem mem_iff_getElem? {a} {xs : Array α} : a xs i : Nat, xs[i]? = some a := by
simp [getElem?_eq_some_iff, mem_iff_getElem]
theorem exists_mem_iff_exists_getElem {P : α Prop} {xs : Array α} :
( x xs, P x) (i : Nat), (hi : i < xs.size), P (xs[i]) := by
cases xs; simp [List.exists_mem_iff_exists_getElem]
theorem forall_mem_iff_forall_getElem {P : α Prop} {xs : Array α} :
( x xs, P x) (i : Nat) (hi : i < xs.size), P (xs[i]) := by
cases xs; simp [List.forall_mem_iff_forall_getElem]
@[deprecated forall_mem_iff_forall_getElem (since := "2026-01-29")]
theorem forall_getElem {xs : Array α} {p : α Prop} :
( (i : Nat) h, p (xs[i]'h)) a, a xs p a := by
exact forall_mem_iff_forall_getElem.symm
cases xs; simp [List.forall_getElem]
/-! ### isEmpty -/
@@ -1996,14 +1968,6 @@ theorem append_eq_append_iff {ws xs ys zs : Array α} :
· left; exact as.toList, by simp
· right; exact cs.toList, by simp
theorem append_eq_append_iff_of_size_eq_left {ws xs ys zs : Array α} (h : ws.size = xs.size) :
ws ++ ys = xs ++ zs ws = xs ys = zs := by
simpa [ Array.toList_inj] using List.append_eq_append_iff_of_size_eq_left h
theorem append_eq_append_iff_of_size_eq_right {ws xs ys zs : Array α} (h : ys.size = zs.size) :
ws ++ ys = xs ++ zs ws = xs ys = zs := by
simpa [ Array.toList_inj] using List.append_eq_append_iff_of_size_eq_right h
@[grind =] theorem set_append {xs ys : Array α} {i : Nat} {x : α} (h : i < (xs ++ ys).size) :
(xs ++ ys).set i x =
if h' : i < xs.size then
@@ -2535,6 +2499,10 @@ theorem flatMap_replicate {f : α → Array β} : (replicate n a).flatMap f = (r
rw [ List.toArray_replicate, List.isEmpty_toArray]
simp
@[simp] theorem sum_replicate_nat {n : Nat} {a : Nat} : (replicate n a).sum = n * a := by
rw [ List.toArray_replicate, List.sum_toArray]
simp
/-! ### Preliminaries about `swap` needed for `reverse`. -/
@[grind =]
@@ -3096,18 +3064,6 @@ theorem foldl_eq_foldlM {f : β → α → β} {b} {xs : Array α} {start stop :
theorem foldr_eq_foldrM {f : α β β} {b} {xs : Array α} {start stop : Nat} :
xs.foldr f b start stop = (xs.foldrM (m := Id) (pure <| f · ·) b start stop).run := rfl
public theorem foldl_eq_foldl_extract {xs : Array α} {f : β α β} {init : β} :
xs.foldl (init := init) (start := start) (stop := stop) f =
(xs.extract start stop).foldl (init := init) f := by
simp only [foldl_eq_foldlM]
rw [foldlM_start_stop]
public theorem foldr_eq_foldr_extract {xs : Array α} {f : α β β} {init : β} :
xs.foldr (init := init) (start := start) (stop := stop) f =
(xs.extract stop start).foldr (init := init) f := by
simp only [foldr_eq_foldrM]
rw [foldrM_start_stop]
@[simp] theorem id_run_foldlM {f : β α Id β} {b} {xs : Array α} {start stop : Nat} :
Id.run (xs.foldlM f b start stop) = xs.foldl (f · · |>.run) b start stop := rfl
@@ -3486,21 +3442,6 @@ theorem foldl_eq_foldr_reverse {xs : Array α} {f : β → α → β} {b} :
theorem foldr_eq_foldl_reverse {xs : Array α} {f : α β β} {b} :
xs.foldr f b = xs.reverse.foldl (fun x y => f y x) b := by simp
theorem foldl_eq_apply_foldr {xs : Array α} {f : α α α}
[Std.Associative f] [Std.LawfulRightIdentity f init] :
xs.foldl f x = f x (xs.foldr f init) := by
simp [ foldl_toList, foldr_toList, List.foldl_eq_apply_foldr]
theorem foldr_eq_apply_foldl {xs : Array α} {f : α α α}
[Std.Associative f] [Std.LawfulLeftIdentity f init] :
xs.foldr f x = f (xs.foldl f init) x := by
simp [ foldl_toList, foldr_toList, List.foldr_eq_apply_foldl]
theorem foldr_eq_foldl {xs : Array α} {f : α α α}
[Std.Associative f] [Std.LawfulIdentity f init] :
xs.foldr f init = xs.foldl f init := by
simp [foldl_eq_apply_foldr, Std.LawfulLeftIdentity.left_id]
@[simp] theorem foldr_push_eq_append {as : Array α} {bs : Array β} {f : α β} (w : start = as.size) :
as.foldr (fun a xs => Array.push xs (f a)) bs start 0 = bs ++ (as.map f).reverse := by
subst w
@@ -3993,7 +3934,6 @@ theorem all_filterMap {xs : Array α} {f : α → Option β} {p : β → Bool} :
· simp only [Id.run_pure]
rw [if_neg (mt (by rintro rfl; exact h) (by simp_all))]
set_option backward.isDefEq.respectTransparency false in
@[simp, grind =] theorem toList_modify {xs : Array α} {f : α α} {i : Nat} :
(xs.modify i f).toList = xs.toList.modify i f := by
apply List.ext_getElem
@@ -4166,7 +4106,7 @@ variable [LawfulBEq α]
(xs.replace a b)[i]? = if xs[i]? == some a then if a xs.take i then some a else some b else xs[i]? := by
rcases xs with xs
simp only [List.replace_toArray, List.getElem?_toArray, List.getElem?_replace, take_eq_extract,
List.extract_toArray, List.extract_eq_take_drop, Nat.sub_zero, List.drop_zero, List.mem_toArray]
List.extract_toArray, List.extract_eq_drop_take, Nat.sub_zero, List.drop_zero, List.mem_toArray]
theorem getElem?_replace_of_ne {xs : Array α} {i : Nat} (h : xs[i]? some a) :
(xs.replace a b)[i]? = xs[i]? := by
@@ -4279,7 +4219,6 @@ private theorem getElem_ofFn_go {f : Fin n → α} {acc i k} (h : i ≤ n) (w₁
· simp
omega
set_option backward.isDefEq.respectTransparency false in
@[simp] theorem getElem_ofFn {f : Fin n α} {i : Nat} (h : i < (ofFn f).size) :
(ofFn f)[i] = f i, size_ofFn (f := f) h := by
unfold ofFn
@@ -4337,48 +4276,19 @@ theorem getElem?_range {n : Nat} {i : Nat} : (Array.range n)[i]? = if i < n then
/-! ### sum -/
@[simp, grind =] theorem sum_empty [Add α] [Zero α] : (#[] : Array α).sum = 0 := rfl
theorem sum_eq_foldr [Add α] [Zero α] {xs : Array α} :
xs.sum = xs.foldr (init := 0) (· + ·) :=
rfl
-- Without further algebraic hypotheses, there's no useful `sum_push` lemma.
@[simp, grind =]
theorem sum_toList [Add α] [Zero α] {as : Array α} : as.toList.sum = as.sum := by
theorem sum_eq_sum_toList [Add α] [Zero α] {as : Array α} : as.toList.sum = as.sum := by
cases as
simp [Array.sum, List.sum]
@[deprecated sum_toList (since := "2026-01-14")]
def sum_eq_sum_toList := @sum_toList
@[simp, grind =]
theorem sum_append [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
[Std.LawfulLeftIdentity (α := α) (· + ·) 0]
{as as₂ : Array α} : (as₁ ++ as₂).sum = as₁.sum + as₂.sum := by
simp [ sum_toList, List.sum_append]
@[simp, grind =]
theorem sum_singleton [Add α] [Zero α] [Std.LawfulRightIdentity (· + ·) (0 : α)] {x : α} :
#[x].sum = x := by
simp [Array.sum_eq_foldr, Std.LawfulRightIdentity.right_id x]
@[simp, grind =]
theorem sum_push [Add α] [Zero α] [Std.Associative (α := α) (· + ·)]
[Std.LawfulIdentity (· + ·) (0 : α)] {xs : Array α} {x : α} :
(xs.push x).sum = xs.sum + x := by
simp [Array.sum_eq_foldr, Std.LawfulRightIdentity.right_id, Std.LawfulLeftIdentity.left_id,
Array.foldr_assoc]
@[simp, grind =]
theorem sum_reverse [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
[Std.Commutative (α := α) (· + ·)]
[Std.LawfulLeftIdentity (α := α) (· + ·) 0] (xs : Array α) : xs.reverse.sum = xs.sum := by
simp [ sum_toList, List.sum_reverse]
theorem sum_eq_foldl [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
[Std.LawfulIdentity (· + ·) (0 : α)] {xs : Array α} :
xs.sum = xs.foldl (init := 0) (· + ·) := by
simp [ sum_toList, List.sum_eq_foldl]
theorem sum_append_nat {as₁ as₂ : Array Nat} : (as₁ ++ as₂).sum = as₁.sum + as₂.sum := by
cases as₁
cases as₂
simp [List.sum_append_nat]
theorem foldl_toList_eq_flatMap {l : List α} {acc : Array β}
{F : Array β α Array β} {G : α List β}
@@ -4528,13 +4438,11 @@ theorem getElem?_push_eq {xs : Array α} {x : α} : (xs.push x)[xs.size]? = some
cases xs
simp
set_option backward.isDefEq.respectTransparency false in
@[simp, grind =] theorem finIdxOf?_toList [BEq α] {a : α} {xs : Array α} :
xs.toList.finIdxOf? a = (xs.finIdxOf? a).map (Fin.cast (by simp)) := by
cases xs
simp
set_option backward.isDefEq.respectTransparency false in
@[simp, grind =] theorem findFinIdx?_toList {p : α Bool} {xs : Array α} :
xs.toList.findFinIdx? p = (xs.findFinIdx? p).map (Fin.cast (by simp)) := by
cases xs
@@ -4659,7 +4567,6 @@ namespace List
as.toArray.unzip = Prod.map List.toArray List.toArray as.unzip := by
ext1 <;> simp
set_option backward.isDefEq.respectTransparency false in
@[simp, grind =] theorem firstM_toArray [Alternative m] {as : List α} {f : α m β} :
as.toArray.firstM f = as.firstM f := by
unfold Array.firstM

View File

@@ -6,10 +6,9 @@ Author: Kim Morrison
module
prelude
public import Init.Data.Range.Polymorphic.RangeIterator
import Init.Data.Range.Polymorphic.Iterators
import Init.Data.Range.Polymorphic.Nat
import Init.Omega
public import Init.Data.Range.Polymorphic.Iterators
public import Init.Data.Range.Polymorphic.Nat
import Init.Data.Iterators.Consumers
public section

View File

@@ -8,13 +8,9 @@ module
prelude
import all Init.Data.Array.Lex.Basic
public import Init.Data.Array.Lex.Basic
public import Init.Data.Array.Lemmas
public import Init.Data.List.Lex
import Init.Data.Range.Polymorphic.NatLemmas
public import Init.Data.BEq
import Init.Data.Array.DecidableEq
import Init.Data.Array.Lemmas
import Init.Data.Bool
import Init.Data.List.Lex
import Init.Data.Range.Polymorphic.Lemmas
public section

View File

@@ -7,9 +7,9 @@ module
prelude
import all Init.Data.Array.Basic
public import Init.Data.Array.OfFn
public import Init.Data.List.MapIdx
import all Init.Data.List.MapIdx
import Init.Data.Array.OfFn
public section

Some files were not shown because too many files have changed in this diff Show More