Compare commits

..

1 Commits

Author SHA1 Message Date
Kim Morrison
a99d08f0bc feat: move lean-pr-testing-NNNN branches to a fork 2025-06-23 02:31:45 +02:00
5534 changed files with 55551 additions and 155222 deletions

6
.gitattributes vendored
View File

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

View File

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

View File

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

View File

@@ -1,38 +0,0 @@
name: Check awaiting-manual label
on:
merge_group:
pull_request:
types: [opened, synchronize, reopened, labeled, unlabeled]
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'
uses: actions/github-script@v7
with:
script: |
const { labels, number: prNumber } = context.payload.pull_request;
const hasAwaiting = labels.some(label => label.name == "awaiting-manual");
const hasBreaks = labels.some(label => label.name == "breaks-manual");
const hasBuilds = labels.some(label => label.name == "builds-manual");
if (hasAwaiting && hasBreaks) {
core.setFailed('PR has both "awaiting-manual" and "breaks-manual" labels.');
} else if (hasAwaiting && !hasBreaks && !hasBuilds) {
core.info('PR is marked "awaiting-manual" but neither "breaks-manual" nor "builds-manual" labels are present.');
core.setOutput('awaiting', 'true');
}
- name: Wait for manual compatibility
if: github.event_name == 'pull_request' && steps.check-awaiting-manual-label.outputs.awaiting == 'true'
run: |
echo "::notice title=Awaiting manual::PR is marked 'awaiting-manual' but neither 'breaks-manual' nor 'builds-manual' labels are present."
echo "This check will remain in progress until the PR is updated with appropriate manual compatibility labels."
# Keep the job running indefinitely to show "in progress" status
while true; do
sleep 3600 # Sleep for 1 hour at a time
done

View File

@@ -36,7 +36,7 @@ jobs:
include: ${{fromJson(inputs.config)}}
# complete all jobs
fail-fast: false
runs-on: ${{ endsWith(matrix.os, '-with-cache') && fromJSON(format('["{0}", "nscloud-git-mirror-1gb"]', matrix.os)) || matrix.os }}
runs-on: ${{ matrix.os }}
defaults:
run:
shell: ${{ matrix.shell || 'nix develop -c bash -euxo pipefail {0}' }}
@@ -69,16 +69,10 @@ jobs:
brew install ccache tree zstd coreutils gmp libuv
if: runner.os == 'macOS'
- name: Checkout
if: (!endsWith(matrix.os, '-with-cache'))
uses: actions/checkout@v5
uses: actions/checkout@v4
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'
@@ -103,17 +97,16 @@ jobs:
sudo apt-get update
sudo apt-get install -y gcc-multilib g++-multilib ccache libuv1-dev:i386 pkgconf:i386
if: matrix.cmultilib
- name: Restore Cache
- name: Cache
id: restore-cache
uses: actions/cache/restore@v4
with:
# NOTE: must be in sync with `save` below and with `restore-cache` in `update-stage0.yml`
# NOTE: must be in sync with `save` below
path: |
.ccache
${{ matrix.name == 'Linux Lake' && 'build/stage1/**/*.trace
${{ matrix.name == 'Linux Lake' && false && 'build/stage1/**/*.trace
build/stage1/**/*.olean*
build/stage1/**/*.ilean
build/stage1/**/*.ir
build/stage1/**/*.c
build/stage1/**/*.c.o*' || '' }}
key: ${{ matrix.name }}-build-v3-${{ github.sha }}
@@ -125,15 +118,9 @@ jobs:
run: |
ccache --zero-stats
if: runner.os == 'Linux'
- name: Set up env
- name: Set up NPROC
run: |
echo "NPROC=$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4)" >> $GITHUB_ENV
if ! diff src/stdlib_flags.h stage0/src/stdlib_flags.h; then
echo "src/stdlib_flags.h and stage0/src/stdlib_flags.h differ, will test and pack stage 2"
echo "TARGET_STAGE=stage2" >> $GITHUB_ENV
else
echo "TARGET_STAGE=stage1" >> $GITHUB_ENV
fi
- name: Build
run: |
ulimit -c unlimited # coredumps
@@ -154,9 +141,6 @@ jobs:
if [[ -n '${{ matrix.prepare-llvm }}' ]]; then
wget -q ${{ matrix.llvm-url }}
PREPARE="$(${{ matrix.prepare-llvm }})"
if [ "$TARGET_STAGE" == "stage2" ]; then
cp -r stage1 stage2
fi
eval "OPTIONS+=($PREPARE)"
fi
if [[ -n '${{ matrix.release }}' && -n '${{ inputs.nightly }}' ]]; then
@@ -171,28 +155,10 @@ jobs:
fi
# contortion to support empty OPTIONS with old macOS bash
cmake .. --preset ${{ matrix.CMAKE_PRESET || 'release' }} -B . ${{ matrix.CMAKE_OPTIONS }} ${OPTIONS[@]+"${OPTIONS[@]}"} -DLEAN_INSTALL_PREFIX=$PWD/..
time make $TARGET_STAGE -j$NPROC
# Should be done as early as possible and in particular *before* "Check rebootstrap" which
# changes the state of stage1/
- name: Save Cache
# Caching on cancellation created some mysterious issues perhaps related to improper build
# shutdown
if: steps.restore-cache.outputs.cache-hit != 'true' && !cancelled()
uses: actions/cache/save@v4
with:
# NOTE: must be in sync with `restore` above
path: |
.ccache
${{ matrix.name == 'Linux Lake' && 'build/stage1/**/*.trace
build/stage1/**/*.olean*
build/stage1/**/*.ilean
build/stage1/**/*.ir
build/stage1/**/*.c
build/stage1/**/*.c.o*' || '' }}
key: ${{ steps.restore-cache.outputs.cache-primary-key }}
time make -j$NPROC
- name: Install
run: |
make -C build/$TARGET_STAGE install
make -C build install
- name: Check Binaries
run: ${{ matrix.binary-check }} lean-*/bin/* || true
- name: Count binary symbols
@@ -223,18 +189,18 @@ jobs:
path: pack/*
- name: Lean stats
run: |
build/$TARGET_STAGE/bin/lean --stats src/Lean.lean -Dexperimental.module=true
build/stage1/bin/lean --stats src/Lean.lean
if: ${{ !matrix.cross }}
- name: Test
id: test
run: |
ulimit -c unlimited # coredumps
time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/$TARGET_STAGE -j$NPROC --output-junit test-results.xml ${{ matrix.CTEST_OPTIONS }}
time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/stage1 -j$NPROC --output-junit test-results.xml ${{ matrix.CTEST_OPTIONS }}
if: (matrix.wasm || !matrix.cross) && (inputs.check-level >= 1 || matrix.test)
- name: Test Summary
uses: test-summary/action@v2
with:
paths: build/${{ env.TARGET_STAGE }}/test-results.xml
paths: build/stage1/test-results.xml
# prefix `if` above with `always` so it's run even if tests failed
if: always() && steps.test.conclusion != 'skipped'
- name: Check Test Binary
@@ -259,13 +225,8 @@ jobs:
if: matrix.test-speedcenter
- name: Check rebootstrap
run: |
set -e
# clean rebuild in case of Makefile changes/Lake does not detect uncommited stage 0
# changes yet
make -C build update-stage0
make -C build/stage1 clean-stdlib
time make -C build -j$NPROC
time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/stage1 -j$NPROC
# clean rebuild in case of Makefile changes
make -C build update-stage0 && rm -rf build/stage* && make -C build -j$NPROC
if: matrix.check-rebootstrap
- name: CCache stats
if: always()
@@ -277,3 +238,16 @@ jobs:
progbin="$(file $c | sed "s/.*execfn: '\([^']*\)'.*/\1/")"
echo bt | $GDB/bin/gdb -q $progbin $c || true
done
- name: Save Cache
if: always() && steps.restore-cache.outputs.cache-hit != 'true'
uses: actions/cache/save@v4
with:
# NOTE: must be in sync with `restore` above
path: |
.ccache
${{ matrix.name == 'Linux Lake' && false && 'build/stage1/**/*.trace
build/stage1/**/*.olean*
build/stage1/**/*.ilean
build/stage1/**/*.c
build/stage1/**/*.c.o*' || '' }}
key: ${{ steps.restore-cache.outputs.cache-primary-key }}

View File

@@ -7,7 +7,7 @@ jobs:
runs-on: ubuntu-latest
steps:
- name: Checkout
uses: actions/checkout@v5
uses: actions/checkout@v4
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@v5
- uses: actions/checkout@v4
with:
ref: ${{ github.event.pull_request.head.sha }}
filter: blob:none

View File

@@ -54,7 +54,7 @@ jobs:
steps:
- name: Checkout
uses: actions/checkout@v5
uses: actions/checkout@v4
# don't schedule nightlies on forks
if: github.event_name == 'schedule' && github.repository == 'leanprover/lean4' || inputs.action == 'release nightly'
- name: Set Nightly
@@ -145,7 +145,6 @@ jobs:
// use large runners where available (original repo)
let large = ${{ github.repository == 'leanprover/lean4' }};
const isPr = "${{ github.event_name }}" == "pull_request";
const isPushToMaster = "${{ github.event_name }}" == "push" && "${{ github.ref_name }}" == "master";
let matrix = [
/* TODO: to be updated to new LLVM
{
@@ -165,34 +164,31 @@ jobs:
{
// portable release build: use channel with older glibc (2.26)
"name": "Linux release",
"os": "ubuntu-latest",
"os": large && level < 2 ? "nscloud-ubuntu-22.04-amd64-4x16" : "ubuntu-latest",
"release": true,
// Special handling for release jobs. We want:
// 1. To run it in PRs so developers get PR toolchains (so secondary is sufficient)
// 1. To run it in PRs so developrs get PR toolchains (so secondary is sufficient)
// 2. To skip it in merge queues as it takes longer than the
// Linux lake build and adds little value in the merge queue
// 3. To run it in release (obviously)
// 4. To run it for pushes to master so that pushes to master have a Linux toolchain
// available as an artifact for Grove to use.
"check-level": (isPr || isPushToMaster) ? 0 : 2,
"check-level": isPr ? 0 : 2,
"secondary": isPr,
"shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-linux-gnu.tar.zst",
"prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
"binary-check": "ldd -v",
// foreign code may be linked against more recent glibc
"CTEST_OPTIONS": "-E 'foreign'",
"CTEST_OPTIONS": "-E 'foreign'"
},
{
"name": "Linux Lake",
"os": large ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
"os": large ? "nscloud-ubuntu-22.04-amd64-8x16" : "ubuntu-latest",
"check-level": 0,
"test": true,
"check-rebootstrap": level >= 1,
"check-stage3": level >= 2,
// NOTE: `test-speedcenter` currently seems to be broken on `ubuntu-latest`
"test-speedcenter": large && level >= 2,
// made explicit until it can be assumed to have propagated to PRs
"CMAKE_OPTIONS": "-DUSE_LAKE=ON",
},
{
@@ -200,6 +196,8 @@ jobs:
"os": "ubuntu-latest",
"check-level": 2,
"CMAKE_PRESET": "reldebug",
// exclude seriously slow/stackoverflowing tests
"CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest|bv_bitblast_stress|3807'"
},
// TODO: suddenly started failing in CI
/*{
@@ -220,13 +218,12 @@ jobs:
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-apple-darwin.tar.zst",
"prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
"binary-check": "otool -L",
"tar": "gtar", // https://github.com/actions/runner-images/issues/2619
"CTEST_OPTIONS": "-E 'leanlaketest_hello'", // started failing from unpack
"tar": "gtar" // https://github.com/actions/runner-images/issues/2619
},
{
"name": "macOS aarch64",
// standard GH runner only comes with 7GB so use large runner if possible when running tests
"os": large && !isPr ? "nscloud-macos-sonoma-arm64-6x14" : "macos-14",
// standard GH runner only comes with 7GB so use large runner if possible
"os": large ? "nscloud-macos-sonoma-arm64-6x14" : "macos-14",
"CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-darwin_aarch64",
"release": true,
"shell": "bash -euxo pipefail {0}",
@@ -234,20 +231,22 @@ jobs:
"prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
"binary-check": "otool -L",
"tar": "gtar", // https://github.com/actions/runner-images/issues/2619
// See "Linux release" for release job levels; Grove is not a concern here
// See above for release job levels
"check-level": isPr ? 0 : 2,
"secondary": isPr,
},
{
"name": "Windows",
"os": large && level == 2 ? "namespace-profile-windows-amd64-4x16" : "windows-2022",
"os": "windows-2022",
"release": true,
"check-level": 2,
"shell": "msys2 {0}",
"CMAKE_OPTIONS": "-G \"Unix Makefiles\"",
// for reasons unknown, interactivetests are flaky on Windows
"CTEST_OPTIONS": "--repeat until-pass:2",
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-w64-windows-gnu.tar.zst",
"prepare-llvm": "../script/prepare-llvm-mingw.sh lean-llvm*",
"binary-check": "ldd",
"binary-check": "ldd"
},
{
"name": "Linux aarch64",
@@ -257,7 +256,7 @@ jobs:
"check-level": 2,
"shell": "nix develop .#oldGlibcAArch -c bash -euxo pipefail {0}",
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-aarch64-linux-gnu.tar.zst",
"prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
"prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*"
},
// Started running out of memory building expensive modules, a 2GB heap is just not that much even before fragmentation
//{
@@ -286,12 +285,6 @@ jobs:
// "CTEST_OPTIONS": "-R \"leantest_1007\\.lean|leantest_Format\\.lean|leanruntest\\_1037.lean|leanruntest_ac_rfl\\.lean|leanruntest_tempfile.lean\\.|leanruntest_libuv\\.lean\""
// }
];
for (const job of matrix) {
if (job["prepare-llvm"]) {
// `USE_LAKE` is not compatible with `prepare-llvm` currently
job["CMAKE_OPTIONS"] = (job["CMAKE_OPTIONS"] ? job["CMAKE_OPTIONS"] + " " : "") + "-DUSE_LAKE=OFF";
}
}
console.log(`matrix:\n${JSON.stringify(matrix, null, 2)}`);
matrix = matrix.filter((job) => level >= job["check-level"]);
core.setOutput('matrix', matrix.filter((job) => !job["secondary"]));
@@ -363,11 +356,11 @@ jobs:
runs-on: ubuntu-latest
needs: build
steps:
- uses: actions/download-artifact@v5
- uses: actions/download-artifact@v4
with:
path: artifacts
- name: Release
uses: softprops/action-gh-release@72f2c25fcb47643c292f7107632f7a47c1df5cd8
uses: softprops/action-gh-release@da05d552573ad5aba039eaac05058a918a7bf631
with:
files: artifacts/*/*
fail_on_unmatched_files: true
@@ -388,12 +381,12 @@ jobs:
runs-on: ubuntu-latest
steps:
- name: Checkout
uses: actions/checkout@v5
uses: actions/checkout@v4
with:
# needed for tagging
fetch-depth: 0
token: ${{ secrets.PUSH_NIGHTLY_TOKEN }}
- uses: actions/download-artifact@v5
- uses: actions/download-artifact@v4
with:
path: artifacts
- name: Prepare Nightly Release
@@ -411,7 +404,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@72f2c25fcb47643c292f7107632f7a47c1df5cd8
uses: softprops/action-gh-release@da05d552573ad5aba039eaac05058a918a7bf631
with:
body_path: diff.md
prerelease: true

View File

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

View File

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

View File

@@ -34,7 +34,7 @@ jobs:
- name: Download artifact from the previous workflow.
if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
id: download-artifact
uses: dawidd6/action-download-artifact@v11 # https://github.com/marketplace/actions/download-workflow-artifact
uses: dawidd6/action-download-artifact@v10 # https://github.com/marketplace/actions/download-workflow-artifact
with:
run_id: ${{ github.event.workflow_run.id }}
path: artifacts
@@ -71,7 +71,7 @@ jobs:
GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
- name: Release (short format)
if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
uses: softprops/action-gh-release@72f2c25fcb47643c292f7107632f7a47c1df5cd8
uses: softprops/action-gh-release@da05d552573ad5aba039eaac05058a918a7bf631
with:
name: Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }}
# There are coredumps files here as well, but all in deeper subdirectories.
@@ -86,7 +86,7 @@ jobs:
- name: Release (SHA-suffixed format)
if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
uses: softprops/action-gh-release@72f2c25fcb47643c292f7107632f7a47c1df5cd8
uses: softprops/action-gh-release@da05d552573ad5aba039eaac05058a918a7bf631
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.
@@ -151,10 +151,10 @@ jobs:
- name: 'Setup jq'
if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
uses: dcarbone/install-jq-action@v3.2.0
uses: dcarbone/install-jq-action@v3.1.1
# 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
- name: Check merge-base and nightly-testing-YYYY-MM-DD
if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
id: ready
run: |
@@ -183,6 +183,7 @@ jobs:
echo "... but Batteries does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
MESSAGE="- ❗ Batteries CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Batteries CI should run now."
fi
else
echo "The most recently nightly tag on this branch has SHA: $NIGHTLY_SHA"
echo "but 'git merge-base origin/master HEAD' reported: $MERGE_BASE_SHA"
@@ -264,108 +265,6 @@ jobs:
echo "mathlib_ready=true" >> "$GITHUB_OUTPUT"
fi
- name: Check merge-base and nightly-testing-YYYY-MM-DD for reference manual
if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
id: reference-manual-ready
run: |
echo "Most recent nightly release in your branch: $MOST_RECENT_NIGHTLY"
NIGHTLY_SHA=$(git -C lean4.git rev-parse "nightly-$MOST_RECENT_NIGHTLY^{commit}")
echo "SHA of most recent nightly release: $NIGHTLY_SHA"
MERGE_BASE_SHA=$(git -C lean4.git merge-base origin/master "${{ steps.workflow-info.outputs.sourceHeadSha }}")
echo "SHA of merge-base: $MERGE_BASE_SHA"
if [ "$NIGHTLY_SHA" = "$MERGE_BASE_SHA" ]; then
echo "The merge base of this PR coincides with the nightly release"
MANUAL_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover/reference-manual.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
if [[ -n "$MANUAL_REMOTE_TAGS" ]]; then
echo "... and the reference manual has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
MESSAGE=""
else
echo "... but the reference manual does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
MESSAGE="- ❗ Reference manual CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-manual\`, reference manual CI should run now."
fi
else
echo "The most recently nightly tag on this branch has SHA: $NIGHTLY_SHA"
echo "but 'git merge-base origin/master HEAD' reported: $MERGE_BASE_SHA"
git -C lean4.git log -10 origin/master
git -C lean4.git fetch origin nightly-with-manual
NIGHTLY_WITH_MANUAL_SHA="$(git -C lean4.git rev-parse "origin/nightly-with-manual")"
MESSAGE="- ❗ Reference manual CI will not be attempted unless your PR branches off the \`nightly-with-manual\` branch. Try \`git rebase $MERGE_BASE_SHA --onto $NIGHTLY_WITH_MANUAL_SHA\`."
fi
if [[ -n "$MESSAGE" ]]; then
# Check if force-manual-ci label is present
LABELS="$(curl --retry 3 --location --silent \
-H "Authorization: token ${{ secrets.MANUAL_COMMENT_BOT }}" \
-H "Accept: application/vnd.github.v3+json" \
"https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/labels" \
| jq -r '.[].name')"
if echo "$LABELS" | grep -q "^force-manual-ci$"; then
echo "force-manual-ci label detected, forcing CI despite issues"
MESSAGE="Forcing reference manual CI because the \`force-manual-ci\` label is present, despite problem: $MESSAGE"
FORCE_CI=true
else
MESSAGE="$MESSAGE You can force reference manual CI using the \`force-manual-ci\` label."
fi
echo "Checking existing messages"
# The code for updating comments is duplicated in the reference manual's
# scripts/lean-pr-testing-comments.sh
# so keep in sync
# Use GitHub API to check if a comment already exists
existing_comment="$(curl --retry 3 --location --silent \
-H "Authorization: token ${{ secrets.MANUAL_COMMENT_BOT }}" \
-H "Accept: application/vnd.github.v3+json" \
"https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments" \
| jq 'first(.[] | select(.body | test("^- . Manual") or startswith("Reference manual CI status")) | select(.user.login == "leanprover-bot"))')"
existing_comment_id="$(echo "$existing_comment" | jq -r .id)"
existing_comment_body="$(echo "$existing_comment" | jq -r .body)"
if [[ "$existing_comment_body" != *"$MESSAGE"* ]]; then
MESSAGE="$MESSAGE ($(date "+%Y-%m-%d %H:%M:%S"))"
echo "Posting message to the comments: $MESSAGE"
# Append new result to the existing comment or post a new comment
# It's essential we use the MANUAL_COMMENT_BOT token here, so that reference manual CI can subsequently edit the comment.
if [ -z "$existing_comment_id" ]; then
INTRO="Reference manual CI status:"
# Post new comment with a bullet point
echo "Posting as new comment at leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments"
curl -L -s \
-X POST \
-H "Authorization: token ${{ secrets.MANUAL_COMMENT_BOT }}" \
-H "Accept: application/vnd.github.v3+json" \
-d "$(jq --null-input --arg intro "$INTRO" --arg val "$MESSAGE" '{"body":($intro + "\n" + $val)}')" \
"https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments"
else
# Append new result to the existing comment
echo "Appending to existing comment at leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments"
curl -L -s \
-X PATCH \
-H "Authorization: token ${{ secrets.MANUAL_COMMENT_BOT }}" \
-H "Accept: application/vnd.github.v3+json" \
-d "$(jq --null-input --arg existing "$existing_comment_body" --arg message "$MESSAGE" '{"body":($existing + "\n" + $message)}')" \
"https://api.github.com/repos/leanprover/lean4/issues/comments/$existing_comment_id"
fi
else
echo "The message already exists in the comment body."
fi
if [[ "$FORCE_CI" == "true" ]]; then
echo "manual_ready=true" >> "$GITHUB_OUTPUT"
else
echo "manual_ready=false" >> "$GITHUB_OUTPUT"
fi
else
echo "manual_ready=true" >> "$GITHUB_OUTPUT"
fi
- name: Report mathlib base
if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true' }}
uses: actions/github-script@v7
@@ -395,7 +294,7 @@ 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@v5
uses: actions/checkout@v4
with:
repository: leanprover-community/batteries
token: ${{ secrets.MATHLIB4_BOT }}
@@ -454,7 +353,7 @@ 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@v5
uses: actions/checkout@v4
with:
repository: leanprover-community/mathlib4-nightly-testing
token: ${{ secrets.MATHLIB4_BOT }}
@@ -512,63 +411,3 @@ jobs:
if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
run: |
git push origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
# We next automatically create a reference manual branch using this toolchain.
# Reference manual CI will be responsible for reporting back success or failure
# to the PR comments asynchronously (and thus transitively SubVerso/Verso).
- name: Cleanup workspace
if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.reference-manual-ready.outputs.manual_ready == 'true'
run: |
sudo rm -rf ./*
# Checkout the reference manual repository with all branches
- name: Checkout mathlib4 repository
if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.reference-manual-ready.outputs.manual_ready == 'true'
uses: actions/checkout@v5
with:
repository: leanprover/reference-manual
token: ${{ secrets.MANUAL_PR_BOT }}
ref: nightly-testing
fetch-depth: 0 # This ensures we check out all tags and branches.
- name: Check if tag in reference manual exists
if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.reference-manual-ready.outputs.manual_ready == 'true'
id: check_manual_tag
run: |
git config user.name "leanprover-bot"
git config user.email "leanprover-bot@lean-fro.org"
if git ls-remote --heads --tags --exit-code origin "nightly-testing-${MOST_RECENT_NIGHTLY}" >/dev/null; then
BASE="nightly-testing-${MOST_RECENT_NIGHTLY}"
else
echo "Couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' branch in the reference manual. Falling back to 'nightly-testing'."
BASE=nightly-testing
fi
echo "Using base tag: $BASE"
EXISTS="$(git ls-remote --heads origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} | wc -l)"
echo "Branch exists: $EXISTS"
if [ "$EXISTS" = "0" ]; then
echo "Branch does not exist, creating it."
git switch -c lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} "$BASE"
echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}" > lean-toolchain
git add lean-toolchain
git add lakefile.lean lake-manifest.json
git commit -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
else
echo "Branch already exists, updating lean-toolchain."
git switch lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
# The reference manual's `nightly-testing` branch or `nightly-testing-YYYY-MM-DD` tag may have moved since this branch was created, so merge their changes.
# (This should no longer be possible once `nightly-testing-YYYY-MM-DD` is a tag, but it is still safe to merge.)
git merge "$BASE" --strategy-option ours --no-commit --allow-unrelated-histories
echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}" > lean-toolchain
git add lean-toolchain
git add lake-manifest.json
git commit -m "Update lean-toolchain for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
fi
- name: Push changes
if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.reference-manual-ready.outputs.manual_ready == 'true'
run: |
git push origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}

View File

@@ -18,16 +18,12 @@ concurrency:
jobs:
update-stage0:
runs-on: nscloud-ubuntu-22.04-amd64-8x16
env:
CCACHE_DIR: ${{ github.workspace }}/.ccache
CCACHE_COMPRESS: true
CCACHE_MAXSIZE: 400M
runs-on: ubuntu-latest
steps:
# This action should push to an otherwise protected branch, so it
# uses a deploy key with write permissions, as suggested at
# https://stackoverflow.com/a/76135647/946226
- uses: actions/checkout@v5
- uses: actions/checkout@v4
with:
ssh-key: ${{secrets.STAGE0_SSH_KEY}}
- run: echo "should_update_stage0=yes" >> "$GITHUB_ENV"
@@ -56,32 +52,11 @@ jobs:
run: |
echo "NPROC=$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4)" >> $GITHUB_ENV
shell: 'nix develop -c bash -euxo pipefail {0}'
- name: Restore Cache
if: env.should_update_stage0 == 'yes'
uses: actions/cache/restore@v4
with:
# NOTE: must be in sync with `restore-cache` in `build-template.yml`
path: |
.ccache
build/stage1/**/*.trace
build/stage1/**/*.olean*
build/stage1/**/*.ilean
build/stage1/**/*.ir
build/stage1/**/*.c
build/stage1/**/*.c.o*
key: Linux Lake-build-v3-${{ github.sha }}
# fall back to (latest) previous cache
restore-keys: |
Linux Lake-build-v3
- if: env.should_update_stage0 == 'yes'
# sync options with `Linux Lake` to ensure cache reuse
run: |
mkdir -p build
cmake --preset release -B build -DLEAN_EXTRA_MAKE_OPTS=-DwarningAsError=true
run: cmake --preset release
shell: 'nix develop -c bash -euxo pipefail {0}'
- if: env.should_update_stage0 == 'yes'
run: |
make -j$NPROC -C build update-stage0-commit
run: make -j$NPROC -C build/release update-stage0-commit
shell: 'nix develop -c bash -euxo pipefail {0}'
- if: env.should_update_stage0 == 'yes'
run: git show --stat

1
.gitignore vendored
View File

@@ -31,4 +31,3 @@ fwOut.txt
wdErr.txt
wdIn.txt
wdOut.txt
downstream_releases/

View File

@@ -16,7 +16,7 @@ foreach(var ${vars})
list(APPEND STAGE1_ARGS "-D${CMAKE_MATCH_1}=${${var}}")
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")
# 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")
@@ -147,10 +147,6 @@ add_custom_target(test
COMMAND $(MAKE) -C stage1 test
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

View File

@@ -45,10 +45,3 @@
/src/Std/Tactic/BVDecide/ @hargoniX
/src/Lean/Elab/Tactic/BVDecide/ @hargoniX
/src/Std/Sat/ @hargoniX
/src/Std/Do @sgraf812
/src/Std/Tactic/Do @sgraf812
/src/Lean/Elab/Tactic/Do @sgraf812
/src/Init/Data/Range/Polymorphic @datokrat
/src/Init/Data/Slice @datokrat
/src/Init/Data/Iterators @datokrat
/src/Std/Data/Iterators @datokrat

View File

@@ -2,19 +2,19 @@ This is the repository for **Lean 4**.
# About
- [Quickstart](https://lean-lang.org/install/)
- [Quickstart](https://lean-lang.org/documentation/setup/)
- [Homepage](https://lean-lang.org)
- [Theorem Proving Tutorial](https://lean-lang.org/theorem_proving_in_lean4/)
- [Functional Programming in Lean](https://lean-lang.org/functional_programming_in_lean/)
- [Documentation Overview](https://lean-lang.org/learn/)
- [Documentation Overview](https://lean-lang.org/documentation/)
- [Language Reference](https://lean-lang.org/doc/reference/latest/)
- [Release notes](RELEASES.md) starting at v4.0.0-m3
- [Examples](https://lean-lang.org/examples/)
- [Examples](https://lean-lang.org/documentation/examples/)
- [External Contribution Guidelines](CONTRIBUTING.md)
# Installation
See [Install Lean](https://lean-lang.org/install/).
See [Setting Up Lean](https://lean-lang.org/documentation/setup/).
# Contributing

View File

@@ -1,6 +1,6 @@
# Lean Build Bootstrapping
Lean is a bootstrapped program: the
Since version 4, Lean is a partially bootstrapped program: most parts of the
frontend and compiler are written in Lean itself and thus need to be built before
building Lean itself - which is needed to again build those parts. This cycle is
broken by using pre-built C files checked into the repository (which ultimately
@@ -73,11 +73,6 @@ update the archived C source code of the stage 0 compiler in `stage0/src`.
The github repository will automatically update stage0 on `master` once
`src/stdlib_flags.h` and `stage0/src/stdlib_flags.h` are out of sync.
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 may want to explicitly call `clean-stdlib` to either observe changes from `.olean` files of modules that built successfully or to check that you did not break modules that built successfully at some prior point.
If you have write access to the lean4 repository, you can also manually
trigger that process, for example to be able to use new features in the compiler itself.
You can do that on <https://github.com/leanprover/lean4/actions/workflows/update-stage0.yml>
@@ -87,13 +82,13 @@ gh workflow run update-stage0.yml
```
Leaving stage0 updates to the CI automation is preferable, but should you need
to do it locally, you can use `make -C build/release update-stage0-commit` to
update `stage0` from `stage1` or `make -C build/release/stageN update-stage0-commit` to
to do it locally, you can use `make update-stage0-commit` in `build/release` to
update `stage0` from `stage1` or `make -C stageN update-stage0-commit` to
update from another stage. This command will automatically stage the updated files
and introduce a commit, so make sure to commit your work before that.
and introduce a commit,so make sure to commit your work before that.
If you rebased the branch (either onto a newer version of `master`, or fixing
up some commits prior to the stage0 update), recreate the stage0 update commits.
up some commits prior to the stage0 update, recreate the stage0 update commits.
The script `script/rebase-stage0.sh` can be used for that.
The CI should prevent PRs with changes to stage0 (besides `stdlib_flags.h`)

View File

@@ -68,7 +68,7 @@ The memory order of the fields is derived from the types and order of the fields
* Fields of type `USize`
* Other scalar fields, in decreasing order by size
Within each group the fields are ordered in declaration order. Trivial wrapper types count as their underlying wrapped type for this purpose.
Within each group the fields are ordered in declaration order. **Warning**: Trivial wrapper types still count toward a field being treated as non-scalar for this purpose.
* To access fields of the first kind, use `lean_ctor_get(val, i)` to get the `i`th non-scalar field.
* To access `USize` fields, use `lean_ctor_get_usize(val, n+i)` to get the `i`th usize field and `n` is the total number of fields of the first kind.
@@ -80,32 +80,32 @@ structure S where
ptr_1 : Array Nat
usize_1 : USize
sc64_1 : UInt64
sc64_2 : { x : UInt64 // x > 0 } -- wrappers of scalars count as scalars
sc64_3 : Float -- `Float` is 64 bit
ptr_2 : { x : UInt64 // x > 0 } -- wrappers don't count as scalars
sc64_2 : Float -- `Float` is 64 bit
sc8_1 : Bool
sc16_1 : UInt16
sc8_2 : UInt8
sc64_4 : UInt64
sc64_3 : UInt64
usize_2 : USize
sc32_1 : Char -- trivial wrapper around `UInt32`
sc32_2 : UInt32
ptr_3 : Char -- trivial wrapper around `UInt32`
sc32_1 : UInt32
sc16_2 : UInt16
```
would get re-sorted into the following memory order:
* `S.ptr_1` - `lean_ctor_get(val, 0)`
* `S.usize_1` - `lean_ctor_get_usize(val, 1)`
* `S.usize_2` - `lean_ctor_get_usize(val, 2)`
* `S.sc64_1` - `lean_ctor_get_uint64(val, sizeof(void*)*3)`
* `S.sc64_2` - `lean_ctor_get_uint64(val, sizeof(void*)*3 + 8)`
* `S.sc64_3` - `lean_ctor_get_float(val, sizeof(void*)*3 + 16)`
* `S.sc64_4` - `lean_ctor_get_uint64(val, sizeof(void*)*3 + 24)`
* `S.sc32_1` - `lean_ctor_get_uint32(val, sizeof(void*)*3 + 32)`
* `S.sc32_2` - `lean_ctor_get_uint32(val, sizeof(void*)*3 + 36)`
* `S.sc16_1` - `lean_ctor_get_uint16(val, sizeof(void*)*3 + 40)`
* `S.sc16_2` - `lean_ctor_get_uint16(val, sizeof(void*)*3 + 42)`
* `S.sc8_1` - `lean_ctor_get_uint8(val, sizeof(void*)*3 + 44)`
* `S.sc8_2` - `lean_ctor_get_uint8(val, sizeof(void*)*3 + 45)`
* `S.ptr_2` - `lean_ctor_get(val, 1)`
* `S.ptr_3` - `lean_ctor_get(val, 2)`
* `S.usize_1` - `lean_ctor_get_usize(val, 3)`
* `S.usize_2` - `lean_ctor_get_usize(val, 4)`
* `S.sc64_1` - `lean_ctor_get_uint64(val, sizeof(void*)*5)`
* `S.sc64_2` - `lean_ctor_get_float(val, sizeof(void*)*5 + 8)`
* `S.sc64_3` - `lean_ctor_get_uint64(val, sizeof(void*)*5 + 16)`
* `S.sc32_1` - `lean_ctor_get_uint32(val, sizeof(void*)*5 + 24)`
* `S.sc16_1` - `lean_ctor_get_uint16(val, sizeof(void*)*5 + 28)`
* `S.sc16_2` - `lean_ctor_get_uint16(val, sizeof(void*)*5 + 30)`
* `S.sc8_1` - `lean_ctor_get_uint8(val, sizeof(void*)*5 + 32)`
* `S.sc8_2` - `lean_ctor_get_uint8(val, sizeof(void*)*5 + 33)`
### Borrowing
@@ -131,21 +131,14 @@ Thus `[init]` functions are run iff their module is imported, regardless of whet
The initializer for module `A.B` is called `initialize_A_B` and will automatically initialize any imported modules.
Module initializers are idempotent (when run with the same `builtin` flag), but not thread-safe.
**Important for process-related functionality**: If your application needs to use process-related functions from libuv, such as `Std.Internal.IO.Process.getProcessTitle` and `Std.Internal.IO.Process.setProcessTitle`, you must call `lean_setup_args(argc, argv)` (which returns a potentially modified `argv` that must be used in place of the original) **before** calling `lean_initialize()` or `lean_initialize_runtime_module()`. This sets up process handling capabilities correctly, which is essential for certain system-level operations that Lean's runtime may depend on.
Together with initialization of the Lean runtime, you should execute code like the following exactly once before accessing any Lean declarations:
```c
void lean_initialize_runtime_module();
void lean_initialize();
char ** lean_setup_args(int argc, char ** argv);
lean_object * initialize_A_B(uint8_t builtin, lean_object *);
lean_object * initialize_C(uint8_t builtin, lean_object *);
...
argv = lean_setup_args(argc, argv); // if using process-related functionality
lean_initialize_runtime_module();
//lean_initialize(); // necessary (and replaces `lean_initialize_runtime_module`) if you (indirectly) access the `Lean` package

View File

@@ -8,8 +8,8 @@ You should not edit the `stage0` directory except using the commands described i
## Development Setup
You can use any of the [supported editors](https://lean-lang.org/install/manual/) for editing the Lean source code.
Please see below for specific instructions for VS Code.
You can use any of the [supported editors](../setup.md) for editing the Lean source code.
If you set up `elan` as below, opening `src/` as a *workspace folder* should ensure that stage 0 (i.e. the stage that first compiles `src/`) will be used for files in that directory.
### Dev setup using elan
@@ -68,10 +68,6 @@ code lean.code-workspace
```
on the command line.
You can use the `Refresh File Dependencies` command as in other projects to rebuild modules from inside VS Code but be aware that this does not trigger any non-Lake build targets.
In particular, after updating `stage0/` (or fetching an update to it), you will want to invoke `make` directly to rebuild `stage0/bin/lean` as described in [building Lean](../make/index.md).
You should then run the `Restart Server` command to update all open files and the server watchdog process as well.
### `ccache`
Lean's build process uses [`ccache`](https://ccache.dev/) if it is
@@ -92,26 +88,3 @@ CI will generate a branch of Mathlib and Batteries called `lean-pr-testing-NNNN`
on the `leanprover-community/mathlib4-nightly-testing` fork of Mathlib.
This branch uses the toolchain for your PR, and will report back to the Lean PR with results from Mathlib CI.
See https://leanprover-community.github.io/contribute/tags_and_branches.html for more details.
### Testing against the Lean Language Reference
You can test a Lean PR against the reference manual by rebasing your PR
on to `nightly-with-manual` branch. (It is fine to force push after rebasing.)
CI will generate a branch of the reference manual called `lean-pr-testing-NNNN`
in `leanprover/reference-manual`. This branch uses the toolchain for your PR,
and will report back to the Lean PR with results from Mathlib CI.
### Avoiding rebuilds for downstream projects
If you want to test changes to Lean on downstream projects and would like to avoid rebuilding modules you have already built/fetched using the project's configured Lean toolchain, you can often do so as long as your build of Lean is close enough to that Lean toolchain (compatible .olean format including structure of all relevant environment extensions).
To override the toolchain without rebuilding for a single command, for example `lake build` or `lake lean`, you can use the prefix
```
LEAN_GITHASH=$(lean --githash) lake +lean4 ...
```
Alternatively, use
```
export LEAN_GITHASH=$(lean --githash)
export ELAN_TOOLCHAIN=lean4
```
to persist these changes for the lifetime of the current shell, which will affect any processes spawned from it such as VS Code started via `code .`.
If you use a setup where you cannot directly start your editor from the command line, such as VS Code Remote, you might want to consider using [direnv](https://direnv.net/) together with an editor extension for it instead so that you can put the lines above into `.envrc`.

View File

@@ -282,7 +282,7 @@ theorem BinTree.find_insert_of_ne (b : BinTree β) (ne : k ≠ k') (v : β)
let t, h := b; simp
induction t with simp
| leaf =>
intro le
intros le
exact Nat.lt_of_le_of_ne le ne
| node left key value right ihl ihr =>
let .node hl hr bl br := h

View File

@@ -1,6 +1,6 @@
These are instructions to set up a working development environment for those who wish to make changes to Lean itself. It is part of the [Development Guide](../dev/index.md).
We strongly suggest that new users instead follow the [Installation Instructions](https://lean-lang.org/install/) to get started using Lean, since this sets up an environment that can automatically manage multiple Lean toolchain versions, which is necessary when working within the Lean ecosystem.
We strongly suggest that new users instead follow the [Quickstart](../quickstart.md) to get started using Lean, since this sets up an environment that can automatically manage multiple Lean toolchain versions, which is necessary when working within the Lean ecosystem.
Requirements
------------
@@ -44,12 +44,12 @@ Useful CMake Configuration Settings
Pass these along with the `cmake --preset release` command.
There are also two alternative presets that combine some of these options you can use instead of `release`: `debug` and `sandebug` (sanitize + debug).
* `-DCMAKE_BUILD_TYPE=`\
* `-D CMAKE_BUILD_TYPE=`\
Select the build type. Valid values are `RELEASE` (default), `DEBUG`,
`RELWITHDEBINFO`, and `MINSIZEREL`.
* `-DCMAKE_C_COMPILER=`\
`-DCMAKE_CXX_COMPILER=`\
* `-D CMAKE_C_COMPILER=`\
`-D CMAKE_CXX_COMPILER=`\
Select the C/C++ compilers to use. Official Lean releases currently use Clang;
see also `.github/workflows/ci.yml` for the CI config.

View File

@@ -1,4 +1,4 @@
# Install Packages on OS X
# Install Packages on OS X 14.5
We assume that you are using [homebrew][homebrew] as a package manager.
@@ -6,23 +6,23 @@ We assume that you are using [homebrew][homebrew] as a package manager.
## Compilers
You need a C++14-compatible compiler to build Lean. As of July
2025, you have three options:
You need a C++11-compatible compiler to build Lean. As of November
2014, you have three options:
- clang++ shipped with OSX (at time of writing v17.0.0)
- clang++ via homebrew (at time of writing, v20.1.8)
- gcc via homebrew (at time of writing, v15.1.0)
- clang++-3.5 (shipped with OSX, Apple LLVM version 6.0)
- gcc-4.9.1 (homebrew)
- clang++-3.5 (homebrew)
We recommend to use Apple's clang++ because it is pre-shipped with OS
X and requires no further installation.
To install gcc via homebrew, please execute:
To install gcc-4.9.1 via homebrew, please execute:
```bash
brew install gcc
```
To install clang via homebrew, please execute:
To install clang++-3.5 via homebrew, please execute:
```bash
brew install llvm lld
brew install llvm
```
To use compilers other than the default one (Apple's clang++), you
need to use `-DCMAKE_CXX_COMPILER` option to specify the compiler

View File

@@ -1,4 +0,0 @@
/.lake
!lake-manifest.json
metadata.json
invalidated.json

View File

@@ -1,22 +0,0 @@
import Grove.Framework
import GroveStdlib.Generated.«associative-query-operations»
import GroveStdlib.Generated.«associative-creation-operations»
import GroveStdlib.Generated.«associative-modification-operations»
import GroveStdlib.Generated.«associative-create-then-query»
import GroveStdlib.Generated.«associative-all-operations-covered»
/-
This file is autogenerated by grove. You can manually edit it, for example to resolve merge
conflicts, but be careful.
-/
open Grove.Framework Widget
namespace GroveStdlib.Generated
def restoreState : RestoreStateM Unit := do
«associative-query-operations».restoreState
«associative-creation-operations».restoreState
«associative-modification-operations».restoreState
«associative-create-then-query».restoreState
«associative-all-operations-covered».restoreState

View File

@@ -1,34 +0,0 @@
import Grove.Framework
/-
This file is autogenerated by grove. You can manually edit it, for example to resolve merge
conflicts, but be careful.
-/
open Grove.Framework Widget
namespace GroveStdlib.Generated.«associative-all-operations-covered»
def «all-covered» : Assertion.Fact where
widgetId := "associative-all-operations-covered"
factId := "all-covered"
assertionId := "all-covered"
state := {
assertionId := "all-covered"
description := "All operations should be covered"
passed := false
message := "There were 19697 operations that were not covered."
}
metadata := {
status := .bad
comment := "Still missing some!"
}
def table : Assertion.Data where
widgetId := "associative-all-operations-covered"
facts := #[
«all-covered»,
]
def restoreState : RestoreStateM Unit := do
addAssertion table

View File

@@ -1,357 +0,0 @@
import Grove.Framework
/-
This file is autogenerated by grove. You can manually edit it, for example to resolve merge
conflicts, but be careful.
-/
open Grove.Framework Widget
namespace GroveStdlib.Generated.«associative-create-then-query»
def «2cb3c441-9663-4ce7-9527-0f40fc29925a:::01f88623-fa5f-4380-9772-b30f2fec5c94:::Std.DHashMap::Std.DHashMap.Raw::Std.ExtDHashMap::Std.DTreeMap::Std.DTreeMap.Raw::Std.ExtDTreeMap» : Table.Fact .subexpression .subexpression .declaration where
widgetId := "associative-create-then-query"
factId := "2cb3c441-9663-4ce7-9527-0f40fc29925a:::01f88623-fa5f-4380-9772-b30f2fec5c94:::Std.DHashMap::Std.DHashMap.Raw::Std.ExtDHashMap::Std.DTreeMap::Std.DTreeMap.Raw::Std.ExtDTreeMap"
rowAssociationId := "2cb3c441-9663-4ce7-9527-0f40fc29925a"
columnAssociationId := "01f88623-fa5f-4380-9772-b30f2fec5c94"
selectedLayers := #["Std.DHashMap", "Std.DHashMap.Raw", "Std.ExtDHashMap", "Std.DTreeMap", "Std.DTreeMap.Raw", "Std.ExtDTreeMap", ]
layerStates := #[
{
layerIdentifier := "Std.DHashMap"
rowState :=
some "Std.DHashMap.emptyWithCapacity", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DHashMap.emptyWithCapacity,
renderedStatement := "Std.DHashMap.emptyWithCapacity.{u, v} {α : Type u} {β : α → Type v} [BEq α] [Hashable α]\n (capacity : Nat := 8) : Std.DHashMap α β",
isDeprecated := false })
columnState :=
some "Std.DHashMap.isEmpty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DHashMap.isEmpty,
renderedStatement := "Std.DHashMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n (m : Std.DHashMap α β) : Bool",
isDeprecated := false })
selectedCellStates := #[
]
},
{
layerIdentifier := "Std.DHashMap.Raw"
rowState :=
some "Std.DHashMap.Raw.emptyWithCapacity", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DHashMap.Raw.emptyWithCapacity,
renderedStatement := "Std.DHashMap.Raw.emptyWithCapacity.{u, v} {α : Type u} {β : α → Type v} (capacity : Nat := 8) :\n Std.DHashMap.Raw α β",
isDeprecated := false })
columnState :=
some "Std.DHashMap.Raw.isEmpty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DHashMap.Raw.isEmpty,
renderedStatement := "Std.DHashMap.Raw.isEmpty.{u, v} {α : Type u} {β : α → Type v} (m : Std.DHashMap.Raw α β) : Bool",
isDeprecated := false })
selectedCellStates := #[
]
},
{
layerIdentifier := "Std.ExtDHashMap"
rowState :=
some "Std.ExtDHashMap.emptyWithCapacity", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtDHashMap.emptyWithCapacity,
renderedStatement := "Std.ExtDHashMap.emptyWithCapacity.{u, v} {α : Type u} {β : α → Type v} [BEq α] [Hashable α]\n (capacity : Nat := 8) : Std.ExtDHashMap α β",
isDeprecated := false })
columnState :=
some "Std.ExtDHashMap.isEmpty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtDHashMap.isEmpty,
renderedStatement := "Std.ExtDHashMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n [EquivBEq α] [LawfulHashable α] (m : Std.ExtDHashMap α β) : Bool",
isDeprecated := false })
selectedCellStates := #[
]
},
{
layerIdentifier := "Std.DTreeMap"
rowState :=
some "Std.DTreeMap.empty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DTreeMap.empty,
renderedStatement := "Std.DTreeMap.empty.{u, v} {α : Type u} {β : α → Type v} {cmp : αα → Ordering} :\n Std.DTreeMap α β cmp",
isDeprecated := false })
columnState :=
some "Std.DTreeMap.isEmpty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DTreeMap.isEmpty,
renderedStatement := "Std.DTreeMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {cmp : αα → Ordering}\n (t : Std.DTreeMap α β cmp) : Bool",
isDeprecated := false })
selectedCellStates := #[
]
},
{
layerIdentifier := "Std.DTreeMap.Raw"
rowState :=
some "Std.DTreeMap.Raw.empty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DTreeMap.Raw.empty,
renderedStatement := "Std.DTreeMap.Raw.empty.{u, v} {α : Type u} {β : α → Type v} {cmp : αα → Ordering} :\n Std.DTreeMap.Raw α β cmp",
isDeprecated := false })
columnState :=
some "Std.DTreeMap.Raw.isEmpty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DTreeMap.Raw.isEmpty,
renderedStatement := "Std.DTreeMap.Raw.isEmpty.{u, v} {α : Type u} {β : α → Type v} {cmp : αα → Ordering}\n (t : Std.DTreeMap.Raw α β cmp) : Bool",
isDeprecated := false })
selectedCellStates := #[
]
},
{
layerIdentifier := "Std.ExtDTreeMap"
rowState :=
some "Std.ExtDTreeMap.empty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtDTreeMap.empty,
renderedStatement := "Std.ExtDTreeMap.empty.{u, v} {α : Type u} {β : α → Type v} {cmp : αα → Ordering} :\n Std.ExtDTreeMap α β cmp",
isDeprecated := false })
columnState :=
some "Std.ExtDTreeMap.isEmpty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtDTreeMap.isEmpty,
renderedStatement := "Std.ExtDTreeMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {cmp : αα → Ordering}\n (t : Std.ExtDTreeMap α β cmp) : Bool",
isDeprecated := false })
selectedCellStates := #[
]
},
]
metadata := {
status := .done
comment := "Not necessary for `ExtDHashMap` because of simp lemma turning into varno"
}
def «5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d:::01f88623-fa5f-4380-9772-b30f2fec5c94:::Std.DHashMap::Std.DHashMap.Raw::Std.ExtDHashMap::Std.DTreeMap::Std.DTreeMap.Raw::Std.ExtDTreeMap» : Table.Fact .subexpression .subexpression .declaration where
widgetId := "associative-create-then-query"
factId := "5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d:::01f88623-fa5f-4380-9772-b30f2fec5c94:::Std.DHashMap::Std.DHashMap.Raw::Std.ExtDHashMap::Std.DTreeMap::Std.DTreeMap.Raw::Std.ExtDTreeMap"
rowAssociationId := "5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d"
columnAssociationId := "01f88623-fa5f-4380-9772-b30f2fec5c94"
selectedLayers := #["Std.DHashMap", "Std.DHashMap.Raw", "Std.ExtDHashMap", "Std.DTreeMap", "Std.DTreeMap.Raw", "Std.ExtDTreeMap", ]
layerStates := #[
{
layerIdentifier := "Std.DHashMap"
rowState :=
some "app (EmptyCollection.emptyCollection) (Std.DHashMap*)", Grove.Framework.Subexpression.State.predicate
{ key := "app (EmptyCollection.emptyCollection) (Std.DHashMap*)", displayShort := "" }
columnState :=
some "Std.DHashMap.isEmpty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DHashMap.isEmpty,
renderedStatement := "Std.DHashMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n (m : Std.DHashMap α β) : Bool",
isDeprecated := false })
selectedCellStates := #[
"Std.DHashMap.isEmpty_empty", Grove.Framework.Declaration.thm
{ name := `Std.DHashMap.isEmpty_empty,
renderedStatement := "Std.DHashMap.isEmpty_empty.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} :\n ∅.isEmpty = true",
isSimp := true,
isDeprecated := false }
,
]
},
{
layerIdentifier := "Std.DHashMap.Raw"
rowState :=
some "app (EmptyCollection.emptyCollection) (Std.DHashMap.Raw*)", Grove.Framework.Subexpression.State.predicate
{ key := "app (EmptyCollection.emptyCollection) (Std.DHashMap.Raw*)", displayShort := "" }
columnState :=
some "Std.DHashMap.Raw.isEmpty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DHashMap.Raw.isEmpty,
renderedStatement := "Std.DHashMap.Raw.isEmpty.{u, v} {α : Type u} {β : α → Type v} (m : Std.DHashMap.Raw α β) : Bool",
isDeprecated := false })
selectedCellStates := #[
"Std.DHashMap.Raw.isEmpty_emptyc", Grove.Framework.Declaration.thm
{ name := `Std.DHashMap.Raw.isEmpty_emptyc,
renderedStatement := "Std.DHashMap.Raw.isEmpty_emptyc.{u_1, u_2} {α : Type u_1} {β : α → Type u_2} [BEq α] [Hashable α] :\n ∅.isEmpty = true",
isSimp := false,
isDeprecated := true }
,
]
},
{
layerIdentifier := "Std.ExtDHashMap"
rowState :=
some "app (EmptyCollection.emptyCollection) (Std.ExtDHashMap*)", Grove.Framework.Subexpression.State.predicate
{ key := "app (EmptyCollection.emptyCollection) (Std.ExtDHashMap*)", displayShort := "" }
columnState :=
some "Std.ExtDHashMap.isEmpty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtDHashMap.isEmpty,
renderedStatement := "Std.ExtDHashMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n [EquivBEq α] [LawfulHashable α] (m : Std.ExtDHashMap α β) : Bool",
isDeprecated := false })
selectedCellStates := #[
]
},
{
layerIdentifier := "Std.DTreeMap"
rowState :=
some "app (EmptyCollection.emptyCollection) (Std.DTreeMap*)", Grove.Framework.Subexpression.State.predicate
{ key := "app (EmptyCollection.emptyCollection) (Std.DTreeMap*)", displayShort := "" }
columnState :=
some "Std.DTreeMap.isEmpty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DTreeMap.isEmpty,
renderedStatement := "Std.DTreeMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {cmp : αα → Ordering}\n (t : Std.DTreeMap α β cmp) : Bool",
isDeprecated := false })
selectedCellStates := #[
"Std.DTreeMap.isEmpty_emptyc", Grove.Framework.Declaration.thm
{ name := `Std.DTreeMap.isEmpty_emptyc,
renderedStatement := "Std.DTreeMap.isEmpty_emptyc.{u, v} {α : Type u} {β : α → Type v} {cmp : αα → Ordering} :\n ∅.isEmpty = true",
isSimp := true,
isDeprecated := false }
,
]
},
{
layerIdentifier := "Std.DTreeMap.Raw"
rowState :=
some "app (EmptyCollection.emptyCollection) (Std.DTreeMap.Raw*)", Grove.Framework.Subexpression.State.predicate
{ key := "app (EmptyCollection.emptyCollection) (Std.DTreeMap.Raw*)", displayShort := "" }
columnState :=
some "Std.DTreeMap.Raw.isEmpty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DTreeMap.Raw.isEmpty,
renderedStatement := "Std.DTreeMap.Raw.isEmpty.{u, v} {α : Type u} {β : α → Type v} {cmp : αα → Ordering}\n (t : Std.DTreeMap.Raw α β cmp) : Bool",
isDeprecated := false })
selectedCellStates := #[
"Std.DTreeMap.Raw.isEmpty_emptyc", Grove.Framework.Declaration.thm
{ name := `Std.DTreeMap.Raw.isEmpty_emptyc,
renderedStatement := "Std.DTreeMap.Raw.isEmpty_emptyc.{u, v} {α : Type u} {β : α → Type v} {cmp : αα → Ordering} :\n ∅.isEmpty = true",
isSimp := true,
isDeprecated := false }
,
]
},
{
layerIdentifier := "Std.ExtDTreeMap"
rowState :=
some "app (EmptyCollection.emptyCollection) (Std.ExtDTreeMap*)", Grove.Framework.Subexpression.State.predicate
{ key := "app (EmptyCollection.emptyCollection) (Std.ExtDTreeMap*)", displayShort := "" }
columnState :=
some "Std.ExtDTreeMap.isEmpty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtDTreeMap.isEmpty,
renderedStatement := "Std.ExtDTreeMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {cmp : αα → Ordering}\n (t : Std.ExtDTreeMap α β cmp) : Bool",
isDeprecated := false })
selectedCellStates := #[
"Std.ExtDTreeMap.isEmpty_empty", Grove.Framework.Declaration.thm
{ name := `Std.ExtDTreeMap.isEmpty_empty,
renderedStatement := "Std.ExtDTreeMap.isEmpty_empty.{u, v} {α : Type u} {β : α → Type v} {cmp : αα → Ordering} :\n ∅.isEmpty = true",
isSimp := true,
isDeprecated := false }
,
]
},
]
metadata := {
status := .bad
comment := "Missing for `ExtDHashMap`"
}
def table : Table.Data .subexpression .subexpression .declaration where
widgetId := "associative-create-then-query"
selectedRowAssociations := #["2cb3c441-9663-4ce7-9527-0f40fc29925a", "7743a485-024d-43b6-bd5f-ebd3182eb94d", "5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d", ]
selectedColumnAssociations := #["01f88623-fa5f-4380-9772-b30f2fec5c94", "f084f852-af71-45b6-8ab3-d251a8144f72", ]
selectedLayers := #["Std.DHashMap", "Std.DHashMap.Raw", "Std.ExtDHashMap", "Std.DTreeMap", "Std.DTreeMap.Raw", "Std.ExtDTreeMap", ]
selectedCellOptions := #[
{
layerIdentifier := "Std.DHashMap"
rowValue := "2cb3c441-9663-4ce7-9527-0f40fc29925a"
columnValue := "01f88623-fa5f-4380-9772-b30f2fec5c94"
selectedCellOptions := #["Std.DHashMap.isEmpty_emptyWithCapacity", ]
},
{
layerIdentifier := "Std.DHashMap.Raw"
rowValue := "2cb3c441-9663-4ce7-9527-0f40fc29925a"
columnValue := "01f88623-fa5f-4380-9772-b30f2fec5c94"
selectedCellOptions := #["Std.DHashMap.Raw.isEmpty_emptyWithCapacity", ]
},
{
layerIdentifier := "Std.DHashMap"
rowValue := "5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d"
columnValue := "01f88623-fa5f-4380-9772-b30f2fec5c94"
selectedCellOptions := #["Std.DHashMap.isEmpty_empty", ]
},
{
layerIdentifier := "Std.DHashMap.Raw"
rowValue := "5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d"
columnValue := "01f88623-fa5f-4380-9772-b30f2fec5c94"
selectedCellOptions := #["Std.DHashMap.Raw.isEmpty_emptyc", ]
},
{
layerIdentifier := "Std.DTreeMap"
rowValue := "5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d"
columnValue := "01f88623-fa5f-4380-9772-b30f2fec5c94"
selectedCellOptions := #["Std.DTreeMap.isEmpty_emptyc", ]
},
{
layerIdentifier := "Std.DTreeMap.Raw"
rowValue := "5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d"
columnValue := "01f88623-fa5f-4380-9772-b30f2fec5c94"
selectedCellOptions := #["Std.DTreeMap.Raw.isEmpty_emptyc", ]
},
{
layerIdentifier := "Std.ExtDTreeMap"
rowValue := "5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d"
columnValue := "01f88623-fa5f-4380-9772-b30f2fec5c94"
selectedCellOptions := #["Std.ExtDTreeMap.isEmpty_empty", ]
},
]
facts := #[
«2cb3c441-9663-4ce7-9527-0f40fc29925a:::01f88623-fa5f-4380-9772-b30f2fec5c94:::Std.DHashMap::Std.DHashMap.Raw::Std.ExtDHashMap::Std.DTreeMap::Std.DTreeMap.Raw::Std.ExtDTreeMap»,
«5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d:::01f88623-fa5f-4380-9772-b30f2fec5c94:::Std.DHashMap::Std.DHashMap.Raw::Std.ExtDHashMap::Std.DTreeMap::Std.DTreeMap.Raw::Std.ExtDTreeMap»,
]
def restoreState : RestoreStateM Unit := do
addTable table

View File

@@ -1,216 +0,0 @@
import Grove.Framework
/-
This file is autogenerated by grove. You can manually edit it, for example to resolve merge
conflicts, but be careful.
-/
open Grove.Framework Widget
namespace GroveStdlib.Generated.«associative-creation-operations»
def «2cb3c441-9663-4ce7-9527-0f40fc29925a» : AssociationTable.Fact .subexpression where
widgetId := "associative-creation-operations"
factId := "2cb3c441-9663-4ce7-9527-0f40fc29925a"
rowId := "2cb3c441-9663-4ce7-9527-0f40fc29925a"
rowState := #["Std.DHashMap", "Std.DHashMap.emptyWithCapacity", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DHashMap.emptyWithCapacity,
renderedStatement := "Std.DHashMap.emptyWithCapacity.{u, v} {α : Type u} {β : α → Type v} [BEq α] [Hashable α]\n (capacity : Nat := 8) : Std.DHashMap α β",
isDeprecated := false }),"Std.DHashMap.Raw", "Std.DHashMap.Raw.emptyWithCapacity", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DHashMap.Raw.emptyWithCapacity,
renderedStatement := "Std.DHashMap.Raw.emptyWithCapacity.{u, v} {α : Type u} {β : α → Type v} (capacity : Nat := 8) :\n Std.DHashMap.Raw α β",
isDeprecated := false }),"Std.ExtDHashMap", "Std.ExtDHashMap.emptyWithCapacity", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtDHashMap.emptyWithCapacity,
renderedStatement := "Std.ExtDHashMap.emptyWithCapacity.{u, v} {α : Type u} {β : α → Type v} [BEq α] [Hashable α]\n (capacity : Nat := 8) : Std.ExtDHashMap α β",
isDeprecated := false }),"Std.DTreeMap", "Std.DTreeMap.empty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DTreeMap.empty,
renderedStatement := "Std.DTreeMap.empty.{u, v} {α : Type u} {β : α → Type v} {cmp : αα → Ordering} :\n Std.DTreeMap α β cmp",
isDeprecated := false }),"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.empty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DTreeMap.Raw.empty,
renderedStatement := "Std.DTreeMap.Raw.empty.{u, v} {α : Type u} {β : α → Type v} {cmp : αα → Ordering} :\n Std.DTreeMap.Raw α β cmp",
isDeprecated := false }),"Std.ExtDTreeMap", "Std.ExtDTreeMap.empty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtDTreeMap.empty,
renderedStatement := "Std.ExtDTreeMap.empty.{u, v} {α : Type u} {β : α → Type v} {cmp : αα → Ordering} :\n Std.ExtDTreeMap α β cmp",
isDeprecated := false }),"Std.HashMap", "Std.HashMap.emptyWithCapacity", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.HashMap.emptyWithCapacity,
renderedStatement := "Std.HashMap.emptyWithCapacity.{u, v} {α : Type u} {β : Type v} [BEq α] [Hashable α]\n (capacity : Nat := 8) : Std.HashMap α β",
isDeprecated := false }),"Std.HashMap.Raw", "Std.HashMap.Raw.emptyWithCapacity", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.HashMap.Raw.emptyWithCapacity,
renderedStatement := "Std.HashMap.Raw.emptyWithCapacity.{u, v} {α : Type u} {β : Type v} (capacity : Nat := 8) :\n Std.HashMap.Raw α β",
isDeprecated := false }),"Std.ExtHashMap", "Std.ExtHashMap.emptyWithCapacity", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtHashMap.emptyWithCapacity,
renderedStatement := "Std.ExtHashMap.emptyWithCapacity.{u, v} {α : Type u} {β : Type v} [BEq α] [Hashable α]\n (capacity : Nat := 8) : Std.ExtHashMap α β",
isDeprecated := false }),"Std.TreeMap", "Std.TreeMap.empty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.TreeMap.empty,
renderedStatement := "Std.TreeMap.empty.{u, v} {α : Type u} {β : Type v} {cmp : αα → Ordering} : Std.TreeMap α β cmp",
isDeprecated := false }),"Std.TreeMap.Raw", "Std.TreeMap.Raw.empty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.TreeMap.Raw.empty,
renderedStatement := "Std.TreeMap.Raw.empty.{u, v} {α : Type u} {β : Type v} {cmp : αα → Ordering} :\n Std.TreeMap.Raw α β cmp",
isDeprecated := false }),"Std.ExtTreeMap", "Std.ExtTreeMap.empty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtTreeMap.empty,
renderedStatement := "Std.ExtTreeMap.empty.{u, v} {α : Type u} {β : Type v} {cmp : αα → Ordering} :\n Std.ExtTreeMap α β cmp",
isDeprecated := false }),"Std.HashSet", "Std.HashSet.emptyWithCapacity", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.HashSet.emptyWithCapacity,
renderedStatement := "Std.HashSet.emptyWithCapacity.{u} {α : Type u} [BEq α] [Hashable α] (capacity : Nat := 8) :\n Std.HashSet α",
isDeprecated := false }),"Std.HashSet.Raw", "Std.HashSet.Raw.emptyWithCapacity", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.HashSet.Raw.emptyWithCapacity,
renderedStatement := "Std.HashSet.Raw.emptyWithCapacity.{u} {α : Type u} (capacity : Nat := 8) : Std.HashSet.Raw α",
isDeprecated := false }),"Std.ExtHashSet", "Std.ExtHashSet.emptyWithCapacity", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtHashSet.emptyWithCapacity,
renderedStatement := "Std.ExtHashSet.emptyWithCapacity.{u} {α : Type u} [BEq α] [Hashable α] (capacity : Nat := 8) :\n Std.ExtHashSet α",
isDeprecated := false }),"Std.TreeSet", "Std.TreeSet.empty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.TreeSet.empty,
renderedStatement := "Std.TreeSet.empty.{u} {α : Type u} {cmp : αα → Ordering} : Std.TreeSet α cmp",
isDeprecated := false }),"Std.TreeSet.Raw", "Std.TreeSet.Raw.empty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.TreeSet.Raw.empty,
renderedStatement := "Std.TreeSet.Raw.empty.{u} {α : Type u} {cmp : αα → Ordering} : Std.TreeSet.Raw α cmp",
isDeprecated := false }),"Std.ExtTreeSet", "Std.ExtTreeSet.empty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtTreeSet.empty,
renderedStatement := "Std.ExtTreeSet.empty.{u} {α : Type u} {cmp : αα → Ordering} : Std.ExtTreeSet α cmp",
isDeprecated := false }),]
metadata := {
status := .done
comment := ""
}
def «7743a485-024d-43b6-bd5f-ebd3182eb94d» : AssociationTable.Fact .subexpression where
widgetId := "associative-creation-operations"
factId := "7743a485-024d-43b6-bd5f-ebd3182eb94d"
rowId := "7743a485-024d-43b6-bd5f-ebd3182eb94d"
rowState := #["Std.DHashMap", "Std.DHashMap.ofList", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DHashMap.ofList,
renderedStatement := "Std.DHashMap.ofList.{u, v} {α : Type u} {β : α → Type v} [BEq α] [Hashable α]\n (l : List ((a : α) × β a)) : Std.DHashMap α β",
isDeprecated := false }),"Std.DHashMap.Raw", "Std.DHashMap.Raw.ofList", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DHashMap.Raw.ofList,
renderedStatement := "Std.DHashMap.Raw.ofList.{u, v} {α : Type u} {β : α → Type v} [BEq α] [Hashable α]\n (l : List ((a : α) × β a)) : Std.DHashMap.Raw α β",
isDeprecated := false }),"Std.ExtDHashMap", "Std.ExtDHashMap.ofList", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtDHashMap.ofList,
renderedStatement := "Std.ExtDHashMap.ofList.{u, v} {α : Type u} {β : α → Type v} [BEq α] [Hashable α]\n (l : List ((a : α) × β a)) : Std.ExtDHashMap α β",
isDeprecated := false }),"Std.DTreeMap", "Std.DTreeMap.ofList", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DTreeMap.ofList,
renderedStatement := "Std.DTreeMap.ofList.{u, v} {α : Type u} {β : α → Type v} (l : List ((a : α) × β a))\n (cmp : αα → Ordering := by exact compare) : Std.DTreeMap α β cmp",
isDeprecated := false }),"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.ofList", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DTreeMap.Raw.ofList,
renderedStatement := "Std.DTreeMap.Raw.ofList.{u, v} {α : Type u} {β : α → Type v} (l : List ((a : α) × β a))\n (cmp : αα → Ordering := by exact compare) : Std.DTreeMap.Raw α β cmp",
isDeprecated := false }),"Std.ExtDTreeMap", "Std.ExtDTreeMap.ofList", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtDTreeMap.ofList,
renderedStatement := "Std.ExtDTreeMap.ofList.{u, v} {α : Type u} {β : α → Type v} (l : List ((a : α) × β a))\n (cmp : αα → Ordering := by exact compare) : Std.ExtDTreeMap α β cmp",
isDeprecated := false }),"Std.HashMap", "Std.HashMap.ofList", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.HashMap.ofList,
renderedStatement := "Std.HashMap.ofList.{u, v} {α : Type u} {β : Type v} [BEq α] [Hashable α] (l : List (α × β)) :\n Std.HashMap α β",
isDeprecated := false }),"Std.HashMap.Raw", "Std.HashMap.Raw.ofList", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.HashMap.Raw.ofList,
renderedStatement := "Std.HashMap.Raw.ofList.{u, v} {α : Type u} {β : Type v} [BEq α] [Hashable α] (l : List (α × β)) :\n Std.HashMap.Raw α β",
isDeprecated := false }),"Std.ExtHashMap", "Std.ExtHashMap.ofList", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtHashMap.ofList,
renderedStatement := "Std.ExtHashMap.ofList.{u, v} {α : Type u} {β : Type v} [BEq α] [Hashable α] (l : List (α × β)) :\n Std.ExtHashMap α β",
isDeprecated := false }),"Std.TreeMap", "Std.TreeMap.ofList", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.TreeMap.ofList,
renderedStatement := "Std.TreeMap.ofList.{u, v} {α : Type u} {β : Type v} (l : List (α × β))\n (cmp : αα → Ordering := by exact compare) : Std.TreeMap α β cmp",
isDeprecated := false }),"Std.TreeMap.Raw", "Std.TreeMap.Raw.ofList", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.TreeMap.Raw.ofList,
renderedStatement := "Std.TreeMap.Raw.ofList.{u, v} {α : Type u} {β : Type v} (l : List (α × β))\n (cmp : αα → Ordering := by exact compare) : Std.TreeMap.Raw α β cmp",
isDeprecated := false }),"Std.ExtTreeMap", "Std.ExtTreeMap.ofList", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtTreeMap.ofList,
renderedStatement := "Std.ExtTreeMap.ofList.{u, v} {α : Type u} {β : Type v} (l : List (α × β))\n (cmp : αα → Ordering := by exact compare) : Std.ExtTreeMap α β cmp",
isDeprecated := false }),"Std.HashSet", "Std.HashSet.ofList", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.HashSet.ofList,
renderedStatement := "Std.HashSet.ofList.{u} {α : Type u} [BEq α] [Hashable α] (l : List α) : Std.HashSet α",
isDeprecated := false }),"Std.HashSet.Raw", "Std.HashSet.Raw.ofList", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.HashSet.Raw.ofList,
renderedStatement := "Std.HashSet.Raw.ofList.{u} {α : Type u} [BEq α] [Hashable α] (l : List α) : Std.HashSet.Raw α",
isDeprecated := false }),"Std.ExtHashSet", "Std.ExtHashSet.ofList", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtHashSet.ofList,
renderedStatement := "Std.ExtHashSet.ofList.{u} {α : Type u} [BEq α] [Hashable α] (l : List α) : Std.ExtHashSet α",
isDeprecated := false }),"Std.TreeSet", "Std.TreeSet.ofList", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.TreeSet.ofList,
renderedStatement := "Std.TreeSet.ofList.{u} {α : Type u} (l : List α) (cmp : αα → Ordering := by exact compare) :\n Std.TreeSet α cmp",
isDeprecated := false }),"Std.TreeSet.Raw", "Std.TreeSet.Raw.ofList", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.TreeSet.Raw.ofList,
renderedStatement := "Std.TreeSet.Raw.ofList.{u} {α : Type u} (l : List α) (cmp : αα → Ordering := by exact compare) :\n Std.TreeSet.Raw α cmp",
isDeprecated := false }),"Std.ExtTreeSet", "Std.ExtTreeSet.ofList", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtTreeSet.ofList,
renderedStatement := "Std.ExtTreeSet.ofList.{u} {α : Type u} (l : List α) (cmp : αα → Ordering := by exact compare) :\n Std.ExtTreeSet α cmp",
isDeprecated := false }),]
metadata := {
status := .done
comment := ""
}
def «5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d» : AssociationTable.Fact .subexpression where
widgetId := "associative-creation-operations"
factId := "5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d"
rowId := "5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d"
rowState := #["Std.DHashMap", "app (EmptyCollection.emptyCollection) (Std.DHashMap*)", Grove.Framework.Subexpression.State.predicate
{ key := "app (EmptyCollection.emptyCollection) (Std.DHashMap*)", displayShort := "" },"Std.DHashMap.Raw", "app (EmptyCollection.emptyCollection) (Std.DHashMap.Raw*)", Grove.Framework.Subexpression.State.predicate
{ key := "app (EmptyCollection.emptyCollection) (Std.DHashMap.Raw*)", displayShort := "" },"Std.ExtDHashMap", "app (EmptyCollection.emptyCollection) (Std.ExtDHashMap*)", Grove.Framework.Subexpression.State.predicate
{ key := "app (EmptyCollection.emptyCollection) (Std.ExtDHashMap*)", displayShort := "" },"Std.DTreeMap", "app (EmptyCollection.emptyCollection) (Std.DTreeMap*)", Grove.Framework.Subexpression.State.predicate
{ key := "app (EmptyCollection.emptyCollection) (Std.DTreeMap*)", displayShort := "" },"Std.DTreeMap.Raw", "app (EmptyCollection.emptyCollection) (Std.DTreeMap.Raw*)", Grove.Framework.Subexpression.State.predicate
{ key := "app (EmptyCollection.emptyCollection) (Std.DTreeMap.Raw*)", displayShort := "" },"Std.ExtDTreeMap", "app (EmptyCollection.emptyCollection) (Std.ExtDTreeMap*)", Grove.Framework.Subexpression.State.predicate
{ key := "app (EmptyCollection.emptyCollection) (Std.ExtDTreeMap*)", displayShort := "" },"Std.HashMap", "app (EmptyCollection.emptyCollection) (Std.HashMap*)", Grove.Framework.Subexpression.State.predicate
{ key := "app (EmptyCollection.emptyCollection) (Std.HashMap*)", displayShort := "" },"Std.HashMap.Raw", "app (EmptyCollection.emptyCollection) (Std.HashMap.Raw*)", Grove.Framework.Subexpression.State.predicate
{ key := "app (EmptyCollection.emptyCollection) (Std.HashMap.Raw*)", displayShort := "" },"Std.ExtHashMap", "app (EmptyCollection.emptyCollection) (Std.ExtHashMap*)", Grove.Framework.Subexpression.State.predicate
{ key := "app (EmptyCollection.emptyCollection) (Std.ExtHashMap*)", displayShort := "" },"Std.TreeMap", "app (EmptyCollection.emptyCollection) (Std.TreeMap*)", Grove.Framework.Subexpression.State.predicate
{ key := "app (EmptyCollection.emptyCollection) (Std.TreeMap*)", displayShort := "" },"Std.TreeMap.Raw", "app (EmptyCollection.emptyCollection) (Std.TreeMap.Raw*)", Grove.Framework.Subexpression.State.predicate
{ key := "app (EmptyCollection.emptyCollection) (Std.TreeMap.Raw*)", displayShort := "" },"Std.ExtTreeMap", "app (EmptyCollection.emptyCollection) (Std.ExtTreeMap*)", Grove.Framework.Subexpression.State.predicate
{ key := "app (EmptyCollection.emptyCollection) (Std.ExtTreeMap*)", displayShort := "" },"Std.HashSet", "app (EmptyCollection.emptyCollection) (Std.HashSet*)", Grove.Framework.Subexpression.State.predicate
{ key := "app (EmptyCollection.emptyCollection) (Std.HashSet*)", displayShort := "" },"Std.HashSet.Raw", "app (EmptyCollection.emptyCollection) (Std.HashSet.Raw*)", Grove.Framework.Subexpression.State.predicate
{ key := "app (EmptyCollection.emptyCollection) (Std.HashSet.Raw*)", displayShort := "" },"Std.ExtHashSet", "app (EmptyCollection.emptyCollection) (Std.ExtHashSet*)", Grove.Framework.Subexpression.State.predicate
{ key := "app (EmptyCollection.emptyCollection) (Std.ExtHashSet*)", displayShort := "" },"Std.TreeSet", "app (EmptyCollection.emptyCollection) (Std.TreeSet*)", Grove.Framework.Subexpression.State.predicate
{ key := "app (EmptyCollection.emptyCollection) (Std.TreeSet*)", displayShort := "" },"Std.TreeSet.Raw", "app (EmptyCollection.emptyCollection) (Std.TreeSet.Raw*)", Grove.Framework.Subexpression.State.predicate
{ key := "app (EmptyCollection.emptyCollection) (Std.TreeSet.Raw*)", displayShort := "" },"Std.ExtTreeSet", "app (EmptyCollection.emptyCollection) (Std.ExtTreeSet*)", Grove.Framework.Subexpression.State.predicate
{ key := "app (EmptyCollection.emptyCollection) (Std.ExtTreeSet*)", displayShort := "" },]
metadata := {
status := .done
comment := ""
}
def table : AssociationTable.Data .subexpression where
widgetId := "associative-creation-operations"
rows := #[
"2cb3c441-9663-4ce7-9527-0f40fc29925a", "empty", #["Std.DHashMap", "Std.DHashMap.emptyWithCapacity","Std.DHashMap.Raw", "Std.DHashMap.Raw.emptyWithCapacity","Std.ExtDHashMap", "Std.ExtDHashMap.emptyWithCapacity","Std.DTreeMap", "Std.DTreeMap.empty","Std.DTreeMap.Raw", "Std.DTreeMap.Raw.empty","Std.ExtDTreeMap", "Std.ExtDTreeMap.empty","Std.HashMap", "Std.HashMap.emptyWithCapacity","Std.HashMap.Raw", "Std.HashMap.Raw.emptyWithCapacity","Std.ExtHashMap", "Std.ExtHashMap.emptyWithCapacity","Std.TreeMap", "Std.TreeMap.empty","Std.TreeMap.Raw", "Std.TreeMap.Raw.empty","Std.ExtTreeMap", "Std.ExtTreeMap.empty","Std.HashSet", "Std.HashSet.emptyWithCapacity","Std.HashSet.Raw", "Std.HashSet.Raw.emptyWithCapacity","Std.ExtHashSet", "Std.ExtHashSet.emptyWithCapacity","Std.TreeSet", "Std.TreeSet.empty","Std.TreeSet.Raw", "Std.TreeSet.Raw.empty","Std.ExtTreeSet", "Std.ExtTreeSet.empty",],
"7743a485-024d-43b6-bd5f-ebd3182eb94d", "ofList", #["Std.DHashMap", "Std.DHashMap.ofList","Std.DHashMap.Raw", "Std.DHashMap.Raw.ofList","Std.ExtDHashMap", "Std.ExtDHashMap.ofList","Std.DTreeMap", "Std.DTreeMap.ofList","Std.DTreeMap.Raw", "Std.DTreeMap.Raw.ofList","Std.ExtDTreeMap", "Std.ExtDTreeMap.ofList","Std.HashMap", "Std.HashMap.ofList","Std.HashMap.Raw", "Std.HashMap.Raw.ofList","Std.ExtHashMap", "Std.ExtHashMap.ofList","Std.TreeMap", "Std.TreeMap.ofList","Std.TreeMap.Raw", "Std.TreeMap.Raw.ofList","Std.ExtTreeMap", "Std.ExtTreeMap.ofList","Std.HashSet", "Std.HashSet.ofList","Std.HashSet.Raw", "Std.HashSet.Raw.ofList","Std.ExtHashSet", "Std.ExtHashSet.ofList","Std.TreeSet", "Std.TreeSet.ofList","Std.TreeSet.Raw", "Std.TreeSet.Raw.ofList","Std.ExtTreeSet", "Std.ExtTreeSet.ofList",],
"5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d", "emptyCollection", #["Std.DHashMap", "app (EmptyCollection.emptyCollection) (Std.DHashMap*)","Std.DHashMap.Raw", "app (EmptyCollection.emptyCollection) (Std.DHashMap.Raw*)","Std.ExtDHashMap", "app (EmptyCollection.emptyCollection) (Std.ExtDHashMap*)","Std.DTreeMap", "app (EmptyCollection.emptyCollection) (Std.DTreeMap*)","Std.DTreeMap.Raw", "app (EmptyCollection.emptyCollection) (Std.DTreeMap.Raw*)","Std.ExtDTreeMap", "app (EmptyCollection.emptyCollection) (Std.ExtDTreeMap*)","Std.HashMap", "app (EmptyCollection.emptyCollection) (Std.HashMap*)","Std.HashMap.Raw", "app (EmptyCollection.emptyCollection) (Std.HashMap.Raw*)","Std.ExtHashMap", "app (EmptyCollection.emptyCollection) (Std.ExtHashMap*)","Std.TreeMap", "app (EmptyCollection.emptyCollection) (Std.TreeMap*)","Std.TreeMap.Raw", "app (EmptyCollection.emptyCollection) (Std.TreeMap.Raw*)","Std.ExtTreeMap", "app (EmptyCollection.emptyCollection) (Std.ExtTreeMap*)","Std.HashSet", "app (EmptyCollection.emptyCollection) (Std.HashSet*)","Std.HashSet.Raw", "app (EmptyCollection.emptyCollection) (Std.HashSet.Raw*)","Std.ExtHashSet", "app (EmptyCollection.emptyCollection) (Std.ExtHashSet*)","Std.TreeSet", "app (EmptyCollection.emptyCollection) (Std.TreeSet*)","Std.TreeSet.Raw", "app (EmptyCollection.emptyCollection) (Std.TreeSet.Raw*)","Std.ExtTreeSet", "app (EmptyCollection.emptyCollection) (Std.ExtTreeSet*)",],
]
facts := #[
«2cb3c441-9663-4ce7-9527-0f40fc29925a»,
«7743a485-024d-43b6-bd5f-ebd3182eb94d»,
«5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d»,
]
def restoreState : RestoreStateM Unit := do
addAssociationTable table

View File

@@ -1,21 +0,0 @@
import Grove.Framework
/-
This file is autogenerated by grove. You can manually edit it, for example to resolve merge
conflicts, but be careful.
-/
open Grove.Framework Widget
namespace GroveStdlib.Generated.«associative-modification-operations»
def table : AssociationTable.Data .subexpression where
widgetId := "associative-modification-operations"
rows := #[
]
facts := #[
]
def restoreState : RestoreStateM Unit := do
addAssociationTable table

View File

@@ -1,445 +0,0 @@
import Grove.Framework
/-
This file is autogenerated by grove. You can manually edit it, for example to resolve merge
conflicts, but be careful.
-/
open Grove.Framework Widget
namespace GroveStdlib.Generated.«associative-query-operations»
def «01f88623-fa5f-4380-9772-b30f2fec5c94» : AssociationTable.Fact .subexpression where
widgetId := "associative-query-operations"
factId := "01f88623-fa5f-4380-9772-b30f2fec5c94"
rowId := "01f88623-fa5f-4380-9772-b30f2fec5c94"
rowState := #["Std.DHashMap", "Std.DHashMap.isEmpty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DHashMap.isEmpty,
renderedStatement := "Std.DHashMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n (m : Std.DHashMap α β) : Bool",
isDeprecated := false }),"Std.DHashMap.Raw", "Std.DHashMap.Raw.isEmpty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DHashMap.Raw.isEmpty,
renderedStatement := "Std.DHashMap.Raw.isEmpty.{u, v} {α : Type u} {β : α → Type v} (m : Std.DHashMap.Raw α β) : Bool",
isDeprecated := false }),"Std.ExtDHashMap", "Std.ExtDHashMap.isEmpty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtDHashMap.isEmpty,
renderedStatement := "Std.ExtDHashMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n [EquivBEq α] [LawfulHashable α] (m : Std.ExtDHashMap α β) : Bool",
isDeprecated := false }),"Std.DTreeMap", "Std.DTreeMap.isEmpty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DTreeMap.isEmpty,
renderedStatement := "Std.DTreeMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {cmp : αα → Ordering}\n (t : Std.DTreeMap α β cmp) : Bool",
isDeprecated := false }),"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.isEmpty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DTreeMap.Raw.isEmpty,
renderedStatement := "Std.DTreeMap.Raw.isEmpty.{u, v} {α : Type u} {β : α → Type v} {cmp : αα → Ordering}\n (t : Std.DTreeMap.Raw α β cmp) : Bool",
isDeprecated := false }),"Std.ExtDTreeMap", "Std.ExtDTreeMap.isEmpty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtDTreeMap.isEmpty,
renderedStatement := "Std.ExtDTreeMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {cmp : αα → Ordering}\n (t : Std.ExtDTreeMap α β cmp) : Bool",
isDeprecated := false }),"Std.HashMap", "Std.HashMap.isEmpty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.HashMap.isEmpty,
renderedStatement := "Std.HashMap.isEmpty.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n (m : Std.HashMap α β) : Bool",
isDeprecated := false }),"Std.HashMap.Raw", "Std.HashMap.Raw.isEmpty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.HashMap.Raw.isEmpty,
renderedStatement := "Std.HashMap.Raw.isEmpty.{u, v} {α : Type u} {β : Type v} (m : Std.HashMap.Raw α β) : Bool",
isDeprecated := false }),"Std.ExtHashMap", "Std.ExtHashMap.isEmpty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtHashMap.isEmpty,
renderedStatement := "Std.ExtHashMap.isEmpty.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α]\n [LawfulHashable α] (m : Std.ExtHashMap α β) : Bool",
isDeprecated := false }),"Std.TreeMap", "Std.TreeMap.isEmpty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.TreeMap.isEmpty,
renderedStatement := "Std.TreeMap.isEmpty.{u, v} {α : Type u} {β : Type v} {cmp : αα → Ordering}\n (t : Std.TreeMap α β cmp) : Bool",
isDeprecated := false }),"Std.TreeMap.Raw", "Std.TreeMap.Raw.isEmpty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.TreeMap.Raw.isEmpty,
renderedStatement := "Std.TreeMap.Raw.isEmpty.{u, v} {α : Type u} {β : Type v} {cmp : αα → Ordering}\n (t : Std.TreeMap.Raw α β cmp) : Bool",
isDeprecated := false }),"Std.ExtTreeMap", "Std.ExtTreeMap.isEmpty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtTreeMap.isEmpty,
renderedStatement := "Std.ExtTreeMap.isEmpty.{u, v} {α : Type u} {β : Type v} {cmp : αα → Ordering}\n (t : Std.ExtTreeMap α β cmp) : Bool",
isDeprecated := false }),"Std.HashSet", "Std.HashSet.isEmpty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.HashSet.isEmpty,
renderedStatement := "Std.HashSet.isEmpty.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Std.HashSet α) : Bool",
isDeprecated := false }),"Std.HashSet.Raw", "Std.HashSet.Raw.isEmpty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.HashSet.Raw.isEmpty,
renderedStatement := "Std.HashSet.Raw.isEmpty.{u} {α : Type u} (m : Std.HashSet.Raw α) : Bool",
isDeprecated := false }),"Std.ExtHashSet", "Std.ExtHashSet.isEmpty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtHashSet.isEmpty,
renderedStatement := "Std.ExtHashSet.isEmpty.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α]\n [LawfulHashable α] (m : Std.ExtHashSet α) : Bool",
isDeprecated := false }),"Std.TreeSet", "Std.TreeSet.isEmpty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.TreeSet.isEmpty,
renderedStatement := "Std.TreeSet.isEmpty.{u} {α : Type u} {cmp : αα → Ordering} (t : Std.TreeSet α cmp) : Bool",
isDeprecated := false }),"Std.TreeSet.Raw", "Std.TreeSet.Raw.isEmpty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.TreeSet.Raw.isEmpty,
renderedStatement := "Std.TreeSet.Raw.isEmpty.{u} {α : Type u} {cmp : αα → Ordering} (t : Std.TreeSet.Raw α cmp) : Bool",
isDeprecated := false }),"Std.ExtTreeSet", "Std.ExtTreeSet.isEmpty", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtTreeSet.isEmpty,
renderedStatement := "Std.ExtTreeSet.isEmpty.{u} {α : Type u} {cmp : αα → Ordering} (t : Std.ExtTreeSet α cmp) : Bool",
isDeprecated := false }),]
metadata := {
status := .done
comment := ""
}
def «f084f852-af71-45b6-8ab3-d251a8144f72» : AssociationTable.Fact .subexpression where
widgetId := "associative-query-operations"
factId := "f084f852-af71-45b6-8ab3-d251a8144f72"
rowId := "f084f852-af71-45b6-8ab3-d251a8144f72"
rowState := #["Std.DHashMap", "Std.DHashMap.size", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DHashMap.size,
renderedStatement := "Std.DHashMap.size.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n (m : Std.DHashMap α β) : Nat",
isDeprecated := false }),"Std.DHashMap.Raw", "Std.DHashMap.Raw.size", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DHashMap.Raw.size,
renderedStatement := "Std.DHashMap.Raw.size.{u, v} {α : Type u} {β : α → Type v} (self : Std.DHashMap.Raw α β) : Nat",
isDeprecated := false }),"Std.ExtDHashMap", "Std.ExtDHashMap.size", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtDHashMap.size,
renderedStatement := "Std.ExtDHashMap.size.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n [EquivBEq α] [LawfulHashable α] (m : Std.ExtDHashMap α β) : Nat",
isDeprecated := false }),"Std.DTreeMap", "Std.DTreeMap.size", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DTreeMap.size,
renderedStatement := "Std.DTreeMap.size.{u, v} {α : Type u} {β : α → Type v} {cmp : αα → Ordering}\n (t : Std.DTreeMap α β cmp) : Nat",
isDeprecated := false }),"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.size", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DTreeMap.Raw.size,
renderedStatement := "Std.DTreeMap.Raw.size.{u, v} {α : Type u} {β : α → Type v} {cmp : αα → Ordering}\n (t : Std.DTreeMap.Raw α β cmp) : Nat",
isDeprecated := false }),"Std.ExtDTreeMap", "Std.ExtDTreeMap.size", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtDTreeMap.size,
renderedStatement := "Std.ExtDTreeMap.size.{u, v} {α : Type u} {β : α → Type v} {cmp : αα → Ordering}\n (t : Std.ExtDTreeMap α β cmp) : Nat",
isDeprecated := false }),"Std.HashMap", "Std.HashMap.size", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.HashMap.size,
renderedStatement := "Std.HashMap.size.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n (m : Std.HashMap α β) : Nat",
isDeprecated := false }),"Std.HashMap.Raw", "Std.HashMap.Raw.size", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.HashMap.Raw.size,
renderedStatement := "Std.HashMap.Raw.size.{u, v} {α : Type u} {β : Type v} (m : Std.HashMap.Raw α β) : Nat",
isDeprecated := false }),"Std.ExtHashMap", "Std.ExtHashMap.size", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtHashMap.size,
renderedStatement := "Std.ExtHashMap.size.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α]\n [LawfulHashable α] (m : Std.ExtHashMap α β) : Nat",
isDeprecated := false }),"Std.TreeMap", "Std.TreeMap.size", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.TreeMap.size,
renderedStatement := "Std.TreeMap.size.{u, v} {α : Type u} {β : Type v} {cmp : αα → Ordering}\n (t : Std.TreeMap α β cmp) : Nat",
isDeprecated := false }),"Std.TreeMap.Raw", "Std.TreeMap.Raw.size", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.TreeMap.Raw.size,
renderedStatement := "Std.TreeMap.Raw.size.{u, v} {α : Type u} {β : Type v} {cmp : αα → Ordering}\n (t : Std.TreeMap.Raw α β cmp) : Nat",
isDeprecated := false }),"Std.ExtTreeMap", "Std.ExtTreeMap.size", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtTreeMap.size,
renderedStatement := "Std.ExtTreeMap.size.{u, v} {α : Type u} {β : Type v} {cmp : αα → Ordering}\n (t : Std.ExtTreeMap α β cmp) : Nat",
isDeprecated := false }),"Std.HashSet", "Std.HashSet.size", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.HashSet.size,
renderedStatement := "Std.HashSet.size.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Std.HashSet α) : Nat",
isDeprecated := false }),"Std.HashSet.Raw", "Std.HashSet.Raw.size", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.HashSet.Raw.size,
renderedStatement := "Std.HashSet.Raw.size.{u} {α : Type u} (m : Std.HashSet.Raw α) : Nat",
isDeprecated := false }),"Std.ExtHashSet", "Std.ExtHashSet.size", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtHashSet.size,
renderedStatement := "Std.ExtHashSet.size.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]\n (m : Std.ExtHashSet α) : Nat",
isDeprecated := false }),"Std.TreeSet", "Std.TreeSet.size", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.TreeSet.size,
renderedStatement := "Std.TreeSet.size.{u} {α : Type u} {cmp : αα → Ordering} (t : Std.TreeSet α cmp) : Nat",
isDeprecated := false }),"Std.TreeSet.Raw", "Std.TreeSet.Raw.size", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.TreeSet.Raw.size,
renderedStatement := "Std.TreeSet.Raw.size.{u} {α : Type u} {cmp : αα → Ordering} (t : Std.TreeSet.Raw α cmp) : Nat",
isDeprecated := false }),"Std.ExtTreeSet", "Std.ExtTreeSet.size", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtTreeSet.size,
renderedStatement := "Std.ExtTreeSet.size.{u} {α : Type u} {cmp : αα → Ordering} (t : Std.ExtTreeSet α cmp) : Nat",
isDeprecated := false }),]
metadata := {
status := .done
comment := ""
}
def «f4e6fa70-5aed-439d-aaad-5f4ced65bf7b» : AssociationTable.Fact .subexpression where
widgetId := "associative-query-operations"
factId := "f4e6fa70-5aed-439d-aaad-5f4ced65bf7b"
rowId := "f4e6fa70-5aed-439d-aaad-5f4ced65bf7b"
rowState := #["Std.DTreeMap", "Std.DTreeMap.any", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DTreeMap.any,
renderedStatement := "Std.DTreeMap.any.{u, v} {α : Type u} {β : α → Type v} {cmp : αα → Ordering}\n (t : Std.DTreeMap α β cmp) (p : (a : α) → β a → Bool) : Bool",
isDeprecated := false }),"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.any", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DTreeMap.Raw.any,
renderedStatement := "Std.DTreeMap.Raw.any.{u, v} {α : Type u} {β : α → Type v} {cmp : αα → Ordering}\n (t : Std.DTreeMap.Raw α β cmp) (p : (a : α) → β a → Bool) : Bool",
isDeprecated := false }),"Std.ExtDTreeMap", "Std.ExtDTreeMap.any", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtDTreeMap.any,
renderedStatement := "Std.ExtDTreeMap.any.{u, v} {α : Type u} {β : α → Type v} {cmp : αα → Ordering} [Std.TransCmp cmp]\n (t : Std.ExtDTreeMap α β cmp) (p : (a : α) → β a → Bool) : Bool",
isDeprecated := false }),"Std.TreeMap", "Std.TreeMap.any", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.TreeMap.any,
renderedStatement := "Std.TreeMap.any.{u, v} {α : Type u} {β : Type v} {cmp : αα → Ordering} (t : Std.TreeMap α β cmp)\n (p : α → β → Bool) : Bool",
isDeprecated := false }),"Std.TreeMap.Raw", "Std.TreeMap.Raw.any", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.TreeMap.Raw.any,
renderedStatement := "Std.TreeMap.Raw.any.{u, v} {α : Type u} {β : Type v} {cmp : αα → Ordering}\n (t : Std.TreeMap.Raw α β cmp) (p : α → β → Bool) : Bool",
isDeprecated := false }),"Std.ExtTreeMap", "Std.ExtTreeMap.any", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtTreeMap.any,
renderedStatement := "Std.ExtTreeMap.any.{u, v} {α : Type u} {β : Type v} {cmp : αα → Ordering} [Std.TransCmp cmp]\n (t : Std.ExtTreeMap α β cmp) (p : α → β → Bool) : Bool",
isDeprecated := false }),"Std.HashSet", "Std.HashSet.any", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.HashSet.any,
renderedStatement := "Std.HashSet.any.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Std.HashSet α)\n (p : α → Bool) : Bool",
isDeprecated := false }),"Std.HashSet.Raw", "Std.HashSet.Raw.any", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.HashSet.Raw.any,
renderedStatement := "Std.HashSet.Raw.any.{u} {α : Type u} (m : Std.HashSet.Raw α) (p : α → Bool) : Bool",
isDeprecated := false }),"Std.TreeSet", "Std.TreeSet.any", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.TreeSet.any,
renderedStatement := "Std.TreeSet.any.{u} {α : Type u} {cmp : αα → Ordering} (t : Std.TreeSet α cmp) (p : α → Bool) :\n Bool",
isDeprecated := false }),"Std.TreeSet.Raw", "Std.TreeSet.Raw.any", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.TreeSet.Raw.any,
renderedStatement := "Std.TreeSet.Raw.any.{u} {α : Type u} {cmp : αα → Ordering} (t : Std.TreeSet.Raw α cmp)\n (p : α → Bool) : Bool",
isDeprecated := false }),"Std.ExtTreeSet", "Std.ExtTreeSet.any", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtTreeSet.any,
renderedStatement := "Std.ExtTreeSet.any.{u} {α : Type u} {cmp : αα → Ordering} [Std.TransCmp cmp]\n (t : Std.ExtTreeSet α cmp) (p : α → Bool) : Bool",
isDeprecated := false }),]
metadata := {
status := .bad
comment := "Missing for some containers"
}
def «c1d181f6-3204-4956-946f-e81619f9feb4» : AssociationTable.Fact .subexpression where
widgetId := "associative-query-operations"
factId := "c1d181f6-3204-4956-946f-e81619f9feb4"
rowId := "c1d181f6-3204-4956-946f-e81619f9feb4"
rowState := #["Std.DTreeMap", "Std.DTreeMap.all", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DTreeMap.all,
renderedStatement := "Std.DTreeMap.all.{u, v} {α : Type u} {β : α → Type v} {cmp : αα → Ordering}\n (t : Std.DTreeMap α β cmp) (p : (a : α) → β a → Bool) : Bool",
isDeprecated := false }),"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.all", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DTreeMap.Raw.all,
renderedStatement := "Std.DTreeMap.Raw.all.{u, v} {α : Type u} {β : α → Type v} {cmp : αα → Ordering}\n (t : Std.DTreeMap.Raw α β cmp) (p : (a : α) → β a → Bool) : Bool",
isDeprecated := false }),"Std.ExtDTreeMap", "Std.ExtDTreeMap.all", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtDTreeMap.all,
renderedStatement := "Std.ExtDTreeMap.all.{u, v} {α : Type u} {β : α → Type v} {cmp : αα → Ordering} [Std.TransCmp cmp]\n (t : Std.ExtDTreeMap α β cmp) (p : (a : α) → β a → Bool) : Bool",
isDeprecated := false }),"Std.TreeMap", "Std.TreeMap.all", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.TreeMap.all,
renderedStatement := "Std.TreeMap.all.{u, v} {α : Type u} {β : Type v} {cmp : αα → Ordering} (t : Std.TreeMap α β cmp)\n (p : α → β → Bool) : Bool",
isDeprecated := false }),"Std.TreeMap.Raw", "Std.TreeMap.Raw.all", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.TreeMap.Raw.all,
renderedStatement := "Std.TreeMap.Raw.all.{u, v} {α : Type u} {β : Type v} {cmp : αα → Ordering}\n (t : Std.TreeMap.Raw α β cmp) (p : α → β → Bool) : Bool",
isDeprecated := false }),"Std.ExtTreeMap", "Std.ExtTreeMap.all", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtTreeMap.all,
renderedStatement := "Std.ExtTreeMap.all.{u, v} {α : Type u} {β : Type v} {cmp : αα → Ordering} [Std.TransCmp cmp]\n (t : Std.ExtTreeMap α β cmp) (p : α → β → Bool) : Bool",
isDeprecated := false }),"Std.HashSet", "Std.HashSet.all", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.HashSet.all,
renderedStatement := "Std.HashSet.all.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Std.HashSet α)\n (p : α → Bool) : Bool",
isDeprecated := false }),"Std.HashSet.Raw", "Std.HashSet.Raw.all", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.HashSet.Raw.all,
renderedStatement := "Std.HashSet.Raw.all.{u} {α : Type u} (m : Std.HashSet.Raw α) (p : α → Bool) : Bool",
isDeprecated := false }),"Std.TreeSet", "Std.TreeSet.all", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.TreeSet.all,
renderedStatement := "Std.TreeSet.all.{u} {α : Type u} {cmp : αα → Ordering} (t : Std.TreeSet α cmp) (p : α → Bool) :\n Bool",
isDeprecated := false }),"Std.TreeSet.Raw", "Std.TreeSet.Raw.all", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.TreeSet.Raw.all,
renderedStatement := "Std.TreeSet.Raw.all.{u} {α : Type u} {cmp : αα → Ordering} (t : Std.TreeSet.Raw α cmp)\n (p : α → Bool) : Bool",
isDeprecated := false }),"Std.ExtTreeSet", "Std.ExtTreeSet.all", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtTreeSet.all,
renderedStatement := "Std.ExtTreeSet.all.{u} {α : Type u} {cmp : αα → Ordering} [Std.TransCmp cmp]\n (t : Std.ExtTreeSet α cmp) (p : α → Bool) : Bool",
isDeprecated := false }),]
metadata := {
status := .bad
comment := "Missing for some containers"
}
def «efe57f41-7db7-4303-b3a6-5216a70c43ce» : AssociationTable.Fact .subexpression where
widgetId := "associative-query-operations"
factId := "efe57f41-7db7-4303-b3a6-5216a70c43ce"
rowId := "efe57f41-7db7-4303-b3a6-5216a70c43ce"
rowState := #["Std.DHashMap", "Std.DHashMap.getD", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DHashMap.getD,
renderedStatement := "Std.DHashMap.getD.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α]\n (m : Std.DHashMap α β) (a : α) (fallback : β a) : β a",
isDeprecated := false }),"Std.DHashMap.Raw", "Std.DHashMap.Raw.getD", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DHashMap.Raw.getD,
renderedStatement := "Std.DHashMap.Raw.getD.{u, v} {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α]\n (m : Std.DHashMap.Raw α β) (a : α) (fallback : β a) : β a",
isDeprecated := false }),"Std.ExtDHashMap", "Std.ExtDHashMap.getD", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtDHashMap.getD,
renderedStatement := "Std.ExtDHashMap.getD.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n [LawfulBEq α] (m : Std.ExtDHashMap α β) (a : α) (fallback : β a) : β a",
isDeprecated := false }),"Std.DTreeMap", "Std.DTreeMap.getD", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DTreeMap.getD,
renderedStatement := "Std.DTreeMap.getD.{u, v} {α : Type u} {β : α → Type v} {cmp : αα → Ordering}\n [Std.LawfulEqCmp cmp] (t : Std.DTreeMap α β cmp) (a : α) (fallback : β a) : β a",
isDeprecated := false }),"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.getD", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DTreeMap.Raw.getD,
renderedStatement := "Std.DTreeMap.Raw.getD.{u, v} {α : Type u} {β : α → Type v} {cmp : αα → Ordering}\n [Std.LawfulEqCmp cmp] (t : Std.DTreeMap.Raw α β cmp) (a : α) (fallback : β a) : β a",
isDeprecated := false }),"Std.ExtDTreeMap", "Std.ExtDTreeMap.getD", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtDTreeMap.getD,
renderedStatement := "Std.ExtDTreeMap.getD.{u, v} {α : Type u} {β : α → Type v} {cmp : αα → Ordering}\n [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (t : Std.ExtDTreeMap α β cmp) (a : α) (fallback : β a) :\n β a",
isDeprecated := false }),"Std.HashMap", "Std.HashMap.getD", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.HashMap.getD,
renderedStatement := "Std.HashMap.getD.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n (m : Std.HashMap α β) (a : α) (fallback : β) : β",
isDeprecated := false }),"Std.HashMap.Raw", "Std.HashMap.Raw.getD", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.HashMap.Raw.getD,
renderedStatement := "Std.HashMap.Raw.getD.{u, v} {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Std.HashMap.Raw α β)\n (a : α) (fallback : β) : β",
isDeprecated := false }),"Std.ExtHashMap", "Std.ExtHashMap.getD", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtHashMap.getD,
renderedStatement := "Std.ExtHashMap.getD.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α]\n [LawfulHashable α] (m : Std.ExtHashMap α β) (a : α) (fallback : β) : β",
isDeprecated := false }),"Std.TreeMap", "Std.TreeMap.getD", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.TreeMap.getD,
renderedStatement := "Std.TreeMap.getD.{u, v} {α : Type u} {β : Type v} {cmp : αα → Ordering} (t : Std.TreeMap α β cmp)\n (a : α) (fallback : β) : β",
isDeprecated := false }),"Std.TreeMap.Raw", "Std.TreeMap.Raw.getD", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.TreeMap.Raw.getD,
renderedStatement := "Std.TreeMap.Raw.getD.{u, v} {α : Type u} {β : Type v} {cmp : αα → Ordering}\n (t : Std.TreeMap.Raw α β cmp) (a : α) (fallback : β) : β",
isDeprecated := false }),"Std.ExtTreeMap", "Std.ExtTreeMap.getD", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtTreeMap.getD,
renderedStatement := "Std.ExtTreeMap.getD.{u, v} {α : Type u} {β : Type v} {cmp : αα → Ordering} [Std.TransCmp cmp]\n (t : Std.ExtTreeMap α β cmp) (a : α) (fallback : β) : β",
isDeprecated := false }),"Std.HashSet", "Std.HashSet.getD", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.HashSet.getD,
renderedStatement := "Std.HashSet.getD.{u} {α : Type u} [BEq α] [Hashable α] (m : Std.HashSet α) (a fallback : α) : α",
isDeprecated := false }),"Std.HashSet.Raw", "Std.HashSet.Raw.getD", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.HashSet.Raw.getD,
renderedStatement := "Std.HashSet.Raw.getD.{u} {α : Type u} [BEq α] [Hashable α] (m : Std.HashSet.Raw α)\n (a fallback : α) : α",
isDeprecated := false }),"Std.ExtHashSet", "Std.ExtHashSet.getD", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtHashSet.getD,
renderedStatement := "Std.ExtHashSet.getD.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]\n (m : Std.ExtHashSet α) (a fallback : α) : α",
isDeprecated := false }),"Std.TreeSet", "Std.TreeSet.getD", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.TreeSet.getD,
renderedStatement := "Std.TreeSet.getD.{u} {α : Type u} {cmp : αα → Ordering} (t : Std.TreeSet α cmp)\n (a fallback : α) : α",
isDeprecated := false }),"Std.TreeSet.Raw", "Std.TreeSet.Raw.getD", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.TreeSet.Raw.getD,
renderedStatement := "Std.TreeSet.Raw.getD.{u} {α : Type u} {cmp : αα → Ordering} (t : Std.TreeSet.Raw α cmp)\n (a fallback : α) : α",
isDeprecated := false }),"Std.ExtTreeSet", "Std.ExtTreeSet.getD", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtTreeSet.getD,
renderedStatement := "Std.ExtTreeSet.getD.{u} {α : Type u} {cmp : αα → Ordering} [Std.TransCmp cmp]\n (t : Std.ExtTreeSet α cmp) (a fallback : α) : α",
isDeprecated := false }),]
metadata := {
status := .done
comment := ""
}
def «e23b1119-3b57-433e-a68d-68fd70b9943d» : AssociationTable.Fact .subexpression where
widgetId := "associative-query-operations"
factId := "e23b1119-3b57-433e-a68d-68fd70b9943d"
rowId := "e23b1119-3b57-433e-a68d-68fd70b9943d"
rowState := #["Std.DHashMap", "Std.DHashMap.get", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DHashMap.get,
renderedStatement := "Std.DHashMap.get.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α]\n (m : Std.DHashMap α β) (a : α) (h : a ∈ m) : β a",
isDeprecated := false }),"Std.DHashMap.Raw", "Std.DHashMap.Raw.Const.get", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DHashMap.Raw.Const.get,
renderedStatement := "Std.DHashMap.Raw.Const.get.{u, v} {α : Type u} {β : Type v} [BEq α] [Hashable α]\n (m : Std.DHashMap.Raw α fun x => β) (a : α) (h : a ∈ m) : β",
isDeprecated := false }),"Std.ExtDHashMap", "Std.ExtDHashMap.get", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtDHashMap.get,
renderedStatement := "Std.ExtDHashMap.get.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n [LawfulBEq α] (m : Std.ExtDHashMap α β) (a : α) (h : a ∈ m) : β a",
isDeprecated := false }),"Std.DTreeMap", "Std.DTreeMap.get", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DTreeMap.get,
renderedStatement := "Std.DTreeMap.get.{u, v} {α : Type u} {β : α → Type v} {cmp : αα → Ordering} [Std.LawfulEqCmp cmp]\n (t : Std.DTreeMap α β cmp) (a : α) (h : a ∈ t) : β a",
isDeprecated := false }),"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.get", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.DTreeMap.Raw.get,
renderedStatement := "Std.DTreeMap.Raw.get.{u, v} {α : Type u} {β : α → Type v} {cmp : αα → Ordering}\n [Std.LawfulEqCmp cmp] (t : Std.DTreeMap.Raw α β cmp) (a : α) (h : a ∈ t) : β a",
isDeprecated := false }),"Std.ExtDTreeMap", "Std.ExtDTreeMap.get", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtDTreeMap.get,
renderedStatement := "Std.ExtDTreeMap.get.{u, v} {α : Type u} {β : α → Type v} {cmp : αα → Ordering} [Std.TransCmp cmp]\n [Std.LawfulEqCmp cmp] (t : Std.ExtDTreeMap α β cmp) (a : α) (h : a ∈ t) : β a",
isDeprecated := false }),"Std.HashMap", "app (GetElem.getElem) (Std.HashMap*)", Grove.Framework.Subexpression.State.predicate
{ key := "app (GetElem.getElem) (Std.HashMap*)", displayShort := "Std.HashMap[·]" },"Std.HashMap.Raw", "app (GetElem.getElem) (Std.HashMap.Raw*)", Grove.Framework.Subexpression.State.predicate
{ key := "app (GetElem.getElem) (Std.HashMap.Raw*)", displayShort := "Std.HashMap.Raw[·]" },"Std.ExtHashMap", "app (GetElem.getElem) (Std.ExtHashMap*)", Grove.Framework.Subexpression.State.predicate
{ key := "app (GetElem.getElem) (Std.ExtHashMap*)", displayShort := "Std.ExtHashMap[·]" },"Std.TreeMap", "app (GetElem.getElem) (Std.TreeMap*)", Grove.Framework.Subexpression.State.predicate
{ key := "app (GetElem.getElem) (Std.TreeMap*)", displayShort := "Std.TreeMap[·]" },"Std.TreeMap.Raw", "app (GetElem.getElem) (Std.TreeMap.Raw*)", Grove.Framework.Subexpression.State.predicate
{ key := "app (GetElem.getElem) (Std.TreeMap.Raw*)", displayShort := "Std.TreeMap.Raw[·]" },"Std.ExtTreeMap", "app (GetElem.getElem) (Std.ExtTreeMap*)", Grove.Framework.Subexpression.State.predicate
{ key := "app (GetElem.getElem) (Std.ExtTreeMap*)", displayShort := "Std.ExtTreeMap[·]" },"Std.HashSet", "Std.HashSet.get", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.HashSet.get,
renderedStatement := "Std.HashSet.get.{u} {α : Type u} [BEq α] [Hashable α] (m : Std.HashSet α) (a : α) (h : a ∈ m) : α",
isDeprecated := false }),"Std.HashSet.Raw", "Std.HashSet.Raw.get", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.HashSet.Raw.get,
renderedStatement := "Std.HashSet.Raw.get.{u} {α : Type u} [BEq α] [Hashable α] (m : Std.HashSet.Raw α) (a : α)\n (h : a ∈ m) : α",
isDeprecated := false }),"Std.ExtHashSet", "Std.ExtHashSet.get", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtHashSet.get,
renderedStatement := "Std.ExtHashSet.get.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]\n (m : Std.ExtHashSet α) (a : α) (h : a ∈ m) : α",
isDeprecated := false }),"Std.TreeSet", "Std.TreeSet.get", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.TreeSet.get,
renderedStatement := "Std.TreeSet.get.{u} {α : Type u} {cmp : αα → Ordering} (t : Std.TreeSet α cmp) (a : α)\n (h : a ∈ t) : α",
isDeprecated := false }),"Std.TreeSet.Raw", "Std.TreeSet.Raw.get", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.TreeSet.Raw.get,
renderedStatement := "Std.TreeSet.Raw.get.{u} {α : Type u} {cmp : αα → Ordering} (t : Std.TreeSet.Raw α cmp) (a : α)\n (h : a ∈ t) : α",
isDeprecated := false }),"Std.ExtTreeSet", "Std.ExtTreeSet.get", Grove.Framework.Subexpression.State.declaration
(Grove.Framework.Declaration.def
{ name := `Std.ExtTreeSet.get,
renderedStatement := "Std.ExtTreeSet.get.{u} {α : Type u} {cmp : αα → Ordering} [Std.TransCmp cmp]\n (t : Std.ExtTreeSet α cmp) (a : α) (h : a ∈ t) : α",
isDeprecated := false }),]
metadata := {
status := .bad
comment := "Should *Set have GetElem?"
}
def table : AssociationTable.Data .subexpression where
widgetId := "associative-query-operations"
rows := #[
"01f88623-fa5f-4380-9772-b30f2fec5c94", "isEmpty", #["Std.DHashMap", "Std.DHashMap.isEmpty","Std.DHashMap.Raw", "Std.DHashMap.Raw.isEmpty","Std.ExtDHashMap", "Std.ExtDHashMap.isEmpty","Std.DTreeMap", "Std.DTreeMap.isEmpty","Std.DTreeMap.Raw", "Std.DTreeMap.Raw.isEmpty","Std.ExtDTreeMap", "Std.ExtDTreeMap.isEmpty","Std.HashMap", "Std.HashMap.isEmpty","Std.HashMap.Raw", "Std.HashMap.Raw.isEmpty","Std.ExtHashMap", "Std.ExtHashMap.isEmpty","Std.TreeMap", "Std.TreeMap.isEmpty","Std.TreeMap.Raw", "Std.TreeMap.Raw.isEmpty","Std.ExtTreeMap", "Std.ExtTreeMap.isEmpty","Std.HashSet", "Std.HashSet.isEmpty","Std.HashSet.Raw", "Std.HashSet.Raw.isEmpty","Std.ExtHashSet", "Std.ExtHashSet.isEmpty","Std.TreeSet", "Std.TreeSet.isEmpty","Std.TreeSet.Raw", "Std.TreeSet.Raw.isEmpty","Std.ExtTreeSet", "Std.ExtTreeSet.isEmpty",],
"f084f852-af71-45b6-8ab3-d251a8144f72", "size", #["Std.DHashMap", "Std.DHashMap.size","Std.DHashMap.Raw", "Std.DHashMap.Raw.size","Std.ExtDHashMap", "Std.ExtDHashMap.size","Std.DTreeMap", "Std.DTreeMap.size","Std.DTreeMap.Raw", "Std.DTreeMap.Raw.size","Std.ExtDTreeMap", "Std.ExtDTreeMap.size","Std.HashMap", "Std.HashMap.size","Std.HashMap.Raw", "Std.HashMap.Raw.size","Std.ExtHashMap", "Std.ExtHashMap.size","Std.TreeMap", "Std.TreeMap.size","Std.TreeMap.Raw", "Std.TreeMap.Raw.size","Std.ExtTreeMap", "Std.ExtTreeMap.size","Std.HashSet", "Std.HashSet.size","Std.HashSet.Raw", "Std.HashSet.Raw.size","Std.ExtHashSet", "Std.ExtHashSet.size","Std.TreeSet", "Std.TreeSet.size","Std.TreeSet.Raw", "Std.TreeSet.Raw.size","Std.ExtTreeSet", "Std.ExtTreeSet.size",],
"f4e6fa70-5aed-439d-aaad-5f4ced65bf7b", "any", #["Std.DTreeMap", "Std.DTreeMap.any","Std.DTreeMap.Raw", "Std.DTreeMap.Raw.any","Std.ExtDTreeMap", "Std.ExtDTreeMap.any","Std.TreeMap", "Std.TreeMap.any","Std.TreeMap.Raw", "Std.TreeMap.Raw.any","Std.ExtTreeMap", "Std.ExtTreeMap.any","Std.HashSet", "Std.HashSet.any","Std.HashSet.Raw", "Std.HashSet.Raw.any","Std.TreeSet", "Std.TreeSet.any","Std.TreeSet.Raw", "Std.TreeSet.Raw.any","Std.ExtTreeSet", "Std.ExtTreeSet.any",],
"c1d181f6-3204-4956-946f-e81619f9feb4", "all", #["Std.DTreeMap", "Std.DTreeMap.all","Std.DTreeMap.Raw", "Std.DTreeMap.Raw.all","Std.ExtDTreeMap", "Std.ExtDTreeMap.all","Std.TreeMap", "Std.TreeMap.all","Std.TreeMap.Raw", "Std.TreeMap.Raw.all","Std.ExtTreeMap", "Std.ExtTreeMap.all","Std.HashSet", "Std.HashSet.all","Std.HashSet.Raw", "Std.HashSet.Raw.all","Std.TreeSet", "Std.TreeSet.all","Std.TreeSet.Raw", "Std.TreeSet.Raw.all","Std.ExtTreeSet", "Std.ExtTreeSet.all",],
"efe57f41-7db7-4303-b3a6-5216a70c43ce", "getD", #["Std.DHashMap", "Std.DHashMap.getD","Std.DHashMap.Raw", "Std.DHashMap.Raw.getD","Std.ExtDHashMap", "Std.ExtDHashMap.getD","Std.DTreeMap", "Std.DTreeMap.getD","Std.DTreeMap.Raw", "Std.DTreeMap.Raw.getD","Std.ExtDTreeMap", "Std.ExtDTreeMap.getD","Std.HashMap", "Std.HashMap.getD","Std.HashMap.Raw", "Std.HashMap.Raw.getD","Std.ExtHashMap", "Std.ExtHashMap.getD","Std.TreeMap", "Std.TreeMap.getD","Std.TreeMap.Raw", "Std.TreeMap.Raw.getD","Std.ExtTreeMap", "Std.ExtTreeMap.getD","Std.HashSet", "Std.HashSet.getD","Std.HashSet.Raw", "Std.HashSet.Raw.getD","Std.ExtHashSet", "Std.ExtHashSet.getD","Std.TreeSet", "Std.TreeSet.getD","Std.TreeSet.Raw", "Std.TreeSet.Raw.getD","Std.ExtTreeSet", "Std.ExtTreeSet.getD",],
"e23b1119-3b57-433e-a68d-68fd70b9943d", "getElem", #["Std.DHashMap", "Std.DHashMap.get","Std.DHashMap.Raw", "Std.DHashMap.Raw.Const.get","Std.ExtDHashMap", "Std.ExtDHashMap.get","Std.DTreeMap", "Std.DTreeMap.get","Std.DTreeMap.Raw", "Std.DTreeMap.Raw.get","Std.ExtDTreeMap", "Std.ExtDTreeMap.get","Std.HashMap", "app (GetElem.getElem) (Std.HashMap*)","Std.HashMap.Raw", "app (GetElem.getElem) (Std.HashMap.Raw*)","Std.ExtHashMap", "app (GetElem.getElem) (Std.ExtHashMap*)","Std.TreeMap", "app (GetElem.getElem) (Std.TreeMap*)","Std.TreeMap.Raw", "app (GetElem.getElem) (Std.TreeMap.Raw*)","Std.ExtTreeMap", "app (GetElem.getElem) (Std.ExtTreeMap*)","Std.HashSet", "Std.HashSet.get","Std.HashSet.Raw", "Std.HashSet.Raw.get","Std.ExtHashSet", "Std.ExtHashSet.get","Std.TreeSet", "Std.TreeSet.get","Std.TreeSet.Raw", "Std.TreeSet.Raw.get","Std.ExtTreeSet", "Std.ExtTreeSet.get",],
]
facts := #[
«01f88623-fa5f-4380-9772-b30f2fec5c94»,
«f084f852-af71-45b6-8ab3-d251a8144f72»,
«f4e6fa70-5aed-439d-aaad-5f4ced65bf7b»,
«c1d181f6-3204-4956-946f-e81619f9feb4»,
«efe57f41-7db7-4303-b3a6-5216a70c43ce»,
«e23b1119-3b57-433e-a68d-68fd70b9943d»,
]
def restoreState : RestoreStateM Unit := do
addAssociationTable table

View File

@@ -1,31 +0,0 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Markus Himmel
-/
import GroveStdlib.Std.CoreTypesAndOperations
import GroveStdlib.Std.LanguageConstructs
import GroveStdlib.Std.Libraries
import GroveStdlib.Std.OperatingSystemAbstractions
open Grove.Framework Widget
namespace GroveStdlib
namespace Std
def introduction : Node :=
.text "Welcome to the interactive Lean standard library outline!"
end Std
def std : Node :=
.section "stdlib" "The Lean standard library" #[
Std.introduction,
Std.coreTypesAndOperations,
Std.languageConstructs,
Std.libraries,
Std.operatingSystemAbstractions
]
end GroveStdlib

View File

@@ -1,28 +0,0 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Markus Himmel
-/
import Grove.Framework
import GroveStdlib.Std.CoreTypesAndOperations.BasicTypes
import GroveStdlib.Std.CoreTypesAndOperations.Containers
import GroveStdlib.Std.CoreTypesAndOperations.Numbers
import GroveStdlib.Std.CoreTypesAndOperations.StringsAndFormatting
open Grove.Framework Widget
namespace GroveStdlib.Std
namespace CoreTypesAndOperations
end CoreTypesAndOperations
def coreTypesAndOperations : Node :=
.section "core-types-and-operations" "Core types and operations" #[
CoreTypesAndOperations.basicTypes,
CoreTypesAndOperations.containers,
CoreTypesAndOperations.numbers,
CoreTypesAndOperations.stringsAndFormatting
]
end GroveStdlib.Std

View File

@@ -1,19 +0,0 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Markus Himmel
-/
import Grove.Framework
open Grove.Framework Widget
namespace GroveStdlib.Std.CoreTypesAndOperations
namespace BasicTypes
end BasicTypes
def basicTypes : Node :=
.section "basic-types" "Basic types" #[]
end GroveStdlib.Std.CoreTypesAndOperations

View File

@@ -1,110 +0,0 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Markus Himmel
-/
import Grove.Framework
open Grove.Framework Widget
namespace GroveStdlib.Std.CoreTypesAndOperations
namespace Containers
namespace SequentialContainers
end SequentialContainers
def sequentialContainers : Node :=
.section "sequential-containers" "Sequential containers" #[]
namespace AssociativeContainers
def associativeContainers : List Lean.Name :=
[`Std.DHashMap, `Std.DHashMap.Raw, `Std.ExtDHashMap, `Std.DTreeMap, `Std.DTreeMap.Raw, `Std.ExtDTreeMap, `Std.HashMap,
`Std.HashMap.Raw, `Std.ExtHashMap, `Std.TreeMap, `Std.TreeMap.Raw, `Std.ExtTreeMap, `Std.HashSet, `Std.HashSet.Raw, `Std.ExtHashSet,
`Std.TreeSet, `Std.TreeSet.Raw, `Std.ExtTreeSet]
def associativeQueryOperations : AssociationTable .subexpression associativeContainers where
id := "associative-query-operations"
title := "Associative query operations"
description := "Operations that take as input an associative container and return a 'single' piece of information (e.g., `GetElem` or `isEmpty`, but not `toList`)."
dataSources n :=
(DataSource.definitionsInNamespace n)
|>.map Subexpression.declaration
|>.or (DataSource.getElem n)
def associativeCreationOperations : AssociationTable .subexpression associativeContainers where
id := "associative-creation-operations"
title := "Associative creation operations"
description := "Operations that create a new associative container"
dataSources n :=
(DataSource.definitionsInNamespace n)
|>.map Subexpression.declaration
|>.or (DataSource.emptyCollection n)
def associativeModificationOperations : AssociationTable .subexpression associativeContainers where
id := "associative-modification-operations"
title := "Associative modification operations"
description := "Operations that both accept and return an associative container"
dataSources n :=
(DataSource.definitionsInNamespace n)
|>.map Subexpression.declaration
def associativeCreateThenQuery : Table .subexpression .subexpression .declaration associativeContainers where
id := "associative-create-then-query"
title := "Associative create then query"
description := "Lemmas that say what happens when creating a new associative container and then immediately querying from it"
rowsFrom := .table associativeCreationOperations
columnsFrom := .table associativeQueryOperations
cellData := .classic _ { relevantNamespaces := associativeContainers }
def allOperationsCovered : Assertion where
widgetId := "associative-all-operations-covered"
title := "All operations on associative containers covered"
description := "All operations on an associative container should appear in at least one of the tables"
check := do
let allValuesArray : Array String #[associativeQueryOperations, associativeCreationOperations, associativeModificationOperations].flatMapM valuesInAssociationTable
let allValues : Std.HashSet String := Std.HashSet.ofArray allValuesArray
let env Lean.getEnv
let mut numBad := 0
for (n, _) in env.constants do
if associativeContainers.any (fun namesp => namesp.isPrefixOf n) then
if !n.toString allValues then
numBad := numBad + 1
return #[{
assertionId := "all-covered"
description := "All operations should be covered"
passed := numBad == 0
message := if numBad = 0 then "All operations were covered" else s!"There were {numBad} operations that were not covered."
}]
end AssociativeContainers
open AssociativeContainers in
def associativeContainers : Node :=
.section "associative-containers" "Associative containers" #[
.associationTable associativeQueryOperations,
.associationTable associativeCreationOperations,
.associationTable associativeModificationOperations,
.table associativeCreateThenQuery,
.assertion allOperationsCovered
]
namespace PersistentDataStructures
end PersistentDataStructures
def persistentDataStructures : Node :=
.section "persistent-data-structures" "Persistent data structures" #[]
end Containers
def containers : Node :=
.section "containers" "Containers" #[
Containers.sequentialContainers,
Containers.associativeContainers,
Containers.persistentDataStructures
]
end GroveStdlib.Std.CoreTypesAndOperations

View File

@@ -1,19 +0,0 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Markus Himmel
-/
import Grove.Framework
open Grove.Framework Widget
namespace GroveStdlib.Std.CoreTypesAndOperations
namespace Numbers
end Numbers
def numbers : Node :=
.section "numbers" "Numbers" #[]
end GroveStdlib.Std.CoreTypesAndOperations

View File

@@ -1,19 +0,0 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Markus Himmel
-/
import Grove.Framework
open Grove.Framework Widget
namespace GroveStdlib.Std.CoreTypesAndOperations
namespace StringsAndFormatting
end StringsAndFormatting
def stringsAndFormatting : Node :=
.section "strings-and-formatting" "Strings and formatting" #[]
end GroveStdlib.Std.CoreTypesAndOperations

View File

@@ -1,26 +0,0 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Markus Himmel
-/
import Grove.Framework
import GroveStdlib.Std.LanguageConstructs.ComparisonOrderingHashing
import GroveStdlib.Std.LanguageConstructs.Monads
import GroveStdlib.Std.LanguageConstructs.RangesAndIterators
open Grove.Framework Widget
namespace GroveStdlib.Std
namespace LanguageConstructs
end LanguageConstructs
def languageConstructs : Node :=
.section "language-constructs" "Language constructs" #[
LanguageConstructs.comparisonOrderingHashing,
LanguageConstructs.monads,
LanguageConstructs.rangesAndIterators
]
end GroveStdlib.Std

View File

@@ -1,19 +0,0 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Markus Himmel
-/
import Grove.Framework
open Grove.Framework Widget
namespace GroveStdlib.Std.LanguageConstructs
namespace ComparisonOrderingHashing
end ComparisonOrderingHashing
def comparisonOrderingHashing : Node :=
.section "comparison-ordering-hashing" "Comparison, ordering, hashing" #[]
end GroveStdlib.Std.LanguageConstructs

View File

@@ -1,19 +0,0 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Markus Himmel
-/
import Grove.Framework
open Grove.Framework Widget
namespace GroveStdlib.Std.LanguageConstructs
namespace Monads
end Monads
def monads : Node :=
.section "monads" "Monads" #[]
end GroveStdlib.Std.LanguageConstructs

View File

@@ -1,19 +0,0 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Markus Himmel
-/
import Grove.Framework
open Grove.Framework Widget
namespace GroveStdlib.Std.LanguageConstructs
namespace RangesAndIterators
end RangesAndIterators
def rangesAndIterators : Node :=
.section "ranges-and-iterators" "Ranges and iterators" #[]
end GroveStdlib.Std.LanguageConstructs

View File

@@ -1,24 +0,0 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Markus Himmel
-/
import Grove.Framework
import GroveStdlib.Std.Libraries.DateAndTime
import GroveStdlib.Std.Libraries.RandomNumbers
open Grove.Framework Widget
namespace GroveStdlib.Std
namespace Libraries
end Libraries
def libraries : Node :=
.section "libraries" "Libraries" #[
Libraries.dateAndTime,
Libraries.randomNumbers
]
end GroveStdlib.Std

View File

@@ -1,19 +0,0 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Markus Himmel
-/
import Grove.Framework
open Grove.Framework Widget
namespace GroveStdlib.Std.Libraries
namespace DateAndTime
end DateAndTime
def dateAndTime : Node :=
.section "date-and-time" "Date and time" #[]
end GroveStdlib.Std.Libraries

View File

@@ -1,19 +0,0 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Markus Himmel
-/
import Grove.Framework
open Grove.Framework Widget
namespace GroveStdlib.Std.Libraries
namespace RandomNumbers
end RandomNumbers
def randomNumbers : Node :=
.section "random-numbers" "Random numbers" #[]
end GroveStdlib.Std.Libraries

View File

@@ -1,30 +0,0 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Markus Himmel
-/
import Grove.Framework
import GroveStdlib.Std.OperatingSystemAbstractions.AsynchronousIO
import GroveStdlib.Std.OperatingSystemAbstractions.BasicIO
import GroveStdlib.Std.OperatingSystemAbstractions.ConcurrencyAndParallelism
import GroveStdlib.Std.OperatingSystemAbstractions.EnvironmentFileSystemProcesses
import GroveStdlib.Std.OperatingSystemAbstractions.Locales
open Grove.Framework Widget
namespace GroveStdlib.Std
namespace OperatingSystemAbstractions
end OperatingSystemAbstractions
def operatingSystemAbstractions : Node :=
.section "operating-system-abstractions" "Operating system abstractions" #[
OperatingSystemAbstractions.asynchronousIO,
OperatingSystemAbstractions.basicIO,
OperatingSystemAbstractions.concurrencyAndParallelism,
OperatingSystemAbstractions.environmentFileSystemProcesses,
OperatingSystemAbstractions.locales
]
end GroveStdlib.Std

View File

@@ -1,19 +0,0 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Markus Himmel
-/
import Grove.Framework
open Grove.Framework Widget
namespace GroveStdlib.Std.OperatingSystemAbstractions
namespace AsynchronousIO
end AsynchronousIO
def asynchronousIO : Node :=
.section "asynchronous-io" "Asynchronous I/O" #[]
end GroveStdlib.Std.OperatingSystemAbstractions

View File

@@ -1,19 +0,0 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Markus Himmel
-/
import Grove.Framework
open Grove.Framework Widget
namespace GroveStdlib.Std.OperatingSystemAbstractions
namespace BasicIO
end BasicIO
def basicIO : Node :=
.section "basic-io" "Basic I/O" #[]
end GroveStdlib.Std.OperatingSystemAbstractions

View File

@@ -1,19 +0,0 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Markus Himmel
-/
import Grove.Framework
open Grove.Framework Widget
namespace GroveStdlib.Std.OperatingSystemAbstractions
namespace ConcurrencyAndParallelism
end ConcurrencyAndParallelism
def concurrencyAndParallelism : Node :=
.section "concurrency-and-parallelism" "Concurrency and parallelism" #[]
end GroveStdlib.Std.OperatingSystemAbstractions

View File

@@ -1,19 +0,0 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Markus Himmel
-/
import Grove.Framework
open Grove.Framework Widget
namespace GroveStdlib.Std.OperatingSystemAbstractions
namespace EnvironmentFileSystemProcesses
end EnvironmentFileSystemProcesses
def environmentFileSystemProcesses : Node :=
.section "environment-filesystem-processes" "Environment, file system, processes" #[]
end GroveStdlib.Std.OperatingSystemAbstractions

View File

@@ -1,19 +0,0 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Markus Himmel
-/
import Grove.Framework
open Grove.Framework Widget
namespace GroveStdlib.Std.OperatingSystemAbstractions
namespace Locales
end Locales
def locales : Node :=
.section "locales" "Locales" #[]
end GroveStdlib.Std.OperatingSystemAbstractions

View File

@@ -1,18 +0,0 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Markus Himmel
-/
import GroveStdlib.Std
import GroveStdlib.Generated
def config : Grove.Framework.Project.Configuration where
projectNamespace := `GroveStdlib
def project : Grove.Framework.Project where
config := config
rootNode := GroveStdlib.std
restoreState := GroveStdlib.Generated.restoreState
def main (args : List String) : IO UInt32 :=
Grove.Framework.main project #[`Init, `Std, `Lean] args

View File

@@ -1,3 +0,0 @@
# Standard library QA
This directory contains the [Grove](github.com/TwoFX/grove) data files for the standard library.

View File

@@ -1,12 +0,0 @@
#!/bin/sh
lake exe grove-stdlib --full metadata.json
cd .lake/packages/grove/frontend
npm install
cp ../../../../metadata.json public/metadata.json
if [ -f "../../../../invalidated.json" ]; then
cp ../../../../invalidated.json public/invalidated.json
GROVE_DATA_LOCATION=public/metadata.json GROVE_UPSTREAM_INVALIDATED_FACTS_LOCATION=public/invalidated.json npm run dev
else
GROVE_DATA_LOCATION=public/metadata.json npm run dev
fi

View File

@@ -1,25 +0,0 @@
{"version": "1.1.0",
"packagesDir": ".lake/packages",
"packages":
[{"url": "https://github.com/TwoFx/grove.git",
"type": "git",
"subDir": "backend",
"scope": "",
"rev": "3e8aabdea58c11813c5d3b7eeb187ded44ee9a34",
"name": "grove",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
"inherited": false,
"configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover/lean4-cli",
"type": "git",
"subDir": null,
"scope": "leanprover",
"rev": "1604206fcd0462da9a241beeac0e2df471647435",
"name": "Cli",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
"configFile": "lakefile.toml"}],
"name": "grovestdlib",
"lakeDir": ".lake"}

View File

@@ -1,18 +0,0 @@
name = "grovestdlib"
version = "0.1.0"
defaultTargets = ["grove-stdlib"]
[[require]]
name = "grove"
git = "https://github.com/TwoFx/grove.git"
rev = "master"
subDir = "backend"
[[lean_lib]]
name = "GroveStdlib"
root = "GroveStdlib"
[[lean_exe]]
name = "grove-stdlib"
supportInterpreter = true
root = "Main"

View File

@@ -1 +0,0 @@
lean4

View File

@@ -1,3 +0,0 @@
#!/bin/sh
lake exe grove-stdlib --invalidated invalidated.json

View File

@@ -18,14 +18,14 @@
# 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_15;
lean-packages = pkgs.callPackage (./nix/packages.nix) { src = ./.; };
devShellWithDist = pkgsDist: pkgs.mkShell.override {
stdenv = pkgs.overrideCC pkgs.stdenv llvmPackages.clang;
stdenv = pkgs.overrideCC pkgs.stdenv lean-packages.llvmPackages.clang;
} ({
buildInputs = with pkgs; [
cmake gmp libuv ccache pkg-config
llvmPackages.llvm # llvm-symbolizer for asan/lsan
lean-packages.llvmPackages.llvm # llvm-symbolizer for asan/lsan
gdb
tree # for CI
];
@@ -60,6 +60,12 @@
GDB = pkgsDist.gdb;
});
in {
packages.${system} = {
# to be removed when Nix CI is not needed anymore
inherit (lean-packages) cacheRoots test update-stage0-commit ciShell;
deprecated = lean-packages;
};
devShells.${system} = {
# The default development shell for working on lean itself
default = devShellWithDist pkgs;

View File

@@ -37,15 +37,6 @@
"isDefault": true
}
},
{
"label": "build-old",
"type": "shell",
"command": "make -C build/release -j$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4) LAKE_EXTRA_ARGS=--old",
"problemMatcher": [],
"group": {
"kind": "build"
}
},
{
"label": "test",
"type": "shell",

7
nix/bareStdenv/setup Normal file
View File

@@ -0,0 +1,7 @@
set -eo pipefail
for pkg in $buildInputs; do
export PATH=$PATH:$pkg/bin
done
: ${outputs:=out}

208
nix/bootstrap.nix Normal file
View File

@@ -0,0 +1,208 @@
{ src, debug ? false, stage0debug ? false, extraCMakeFlags ? [],
stdenv, lib, cmake, pkg-config, gmp, libuv, cadical, git, gnumake, bash, buildLeanPackage, writeShellScriptBin, runCommand, symlinkJoin, lndir, perl, gnused, darwin, llvmPackages, linkFarmFromDrvs,
... } @ args:
with builtins;
lib.warn "The Nix-based build is deprecated" rec {
inherit stdenv;
sourceByRegex = p: rs: lib.sourceByRegex p (map (r: "(/src/)?${r}") rs);
buildCMake = args: stdenv.mkDerivation ({
nativeBuildInputs = [ cmake pkg-config ];
buildInputs = [ gmp libuv llvmPackages.llvm ];
# https://github.com/NixOS/nixpkgs/issues/60919
hardeningDisable = [ "all" ];
dontStrip = (args.debug or debug);
postConfigure = ''
patchShebangs .
'';
} // args // {
src = args.realSrc or (sourceByRegex args.src [ "[a-z].*" "CMakeLists\.txt" ]);
cmakeFlags = ["-DSMALL_ALLOCATOR=ON" "-DUSE_MIMALLOC=OFF"] ++ (args.cmakeFlags or [ "-DSTAGE=1" "-DPREV_STAGE=./faux-prev-stage" "-DUSE_GITHASH=OFF" "-DCADICAL=${cadical}/bin/cadical" ]) ++ (args.extraCMakeFlags or extraCMakeFlags) ++ lib.optional (args.debug or debug) [ "-DCMAKE_BUILD_TYPE=Debug" ];
preConfigure = args.preConfigure or "" + ''
# ignore absence of submodule
sed -i 's!lake/Lake.lean!!' CMakeLists.txt
'';
});
lean-bin-tools-unwrapped = buildCMake {
name = "lean-bin-tools";
outputs = [ "out" "leanc_src" ];
realSrc = sourceByRegex (src + "/src") [ "CMakeLists\.txt" "[a-z].*" ".*\.in" "Leanc\.lean" ];
dontBuild = true;
installPhase = ''
mkdir $out $leanc_src
mv bin/ include/ share/ $out/
mv leanc.sh $out/bin/leanc
mv leanc/Leanc.lean $leanc_src/
substituteInPlace $out/bin/leanc --replace '$root' "$out" --replace " sed " " ${gnused}/bin/sed "
substituteInPlace $out/bin/leanmake --replace "make" "${gnumake}/bin/make"
substituteInPlace $out/share/lean/lean.mk --replace "/usr/bin/env bash" "${bash}/bin/bash"
'';
};
leancpp = buildCMake {
name = "leancpp";
src = src + "/src";
buildFlags = [ "leancpp" "leanrt" "leanrt_initial-exec" "leanshell" "leanmain" ];
installPhase = ''
mkdir -p $out
mv lib/ $out/
mv runtime/libleanrt_initial-exec.a $out/lib
'';
};
stage0 = args.stage0 or (buildCMake {
name = "lean-stage0";
realSrc = src + "/stage0/src";
debug = stage0debug;
cmakeFlags = [ "-DSTAGE=0" ];
extraCMakeFlags = [];
preConfigure = ''
ln -s ${src + "/stage0/stdlib"} ../stdlib
'';
installPhase = ''
mkdir -p $out/bin $out/lib/lean
mv bin/lean $out/bin/
mv lib/lean/*.{so,dylib} $out/lib/lean
'';
meta.mainProgram = "lean";
});
stage = { stage, prevStage, self }:
let
desc = "stage${toString stage}";
build = args: buildLeanPackage.override {
lean = prevStage;
leanc = lean-bin-tools-unwrapped;
# use same stage for retrieving dependencies
lean-leanDeps = stage0;
lean-final = self;
} ({
src = src + "/src";
roots = [ { mod = args.name; glob = "andSubmodules"; } ];
fullSrc = src;
srcPath = "$PWD/src:$PWD/src/lake";
inherit debug;
leanFlags = [ "-DwarningAsError=true" ];
} // args);
Init' = build { name = "Init"; deps = []; };
Std' = build { name = "Std"; deps = [ Init' ]; };
Lean' = build { name = "Lean"; deps = [ Std' ]; };
attachSharedLib = sharedLib: pkg: pkg // {
inherit sharedLib;
mods = mapAttrs (_: m: m // { inherit sharedLib; propagatedLoadDynlibs = []; }) pkg.mods;
};
in (all: all // all.lean) rec {
inherit (Lean) emacs-dev emacs-package vscode-dev vscode-package;
Init = attachSharedLib leanshared Init';
Std = attachSharedLib leanshared Std' // { allExternalDeps = [ Init ]; };
Lean = attachSharedLib leanshared Lean' // { allExternalDeps = [ Std ]; };
Lake = build {
name = "Lake";
sharedLibName = "Lake_shared";
src = src + "/src/lake";
deps = [ Init Lean ];
};
Lake-Main = build {
name = "LakeMain";
roots = [{ glob = "one"; mod = "LakeMain"; }];
executableName = "lake";
deps = [ Lake ];
linkFlags = lib.optional stdenv.isLinux "-rdynamic";
src = src + "/src/lake";
};
stdlib = [ Init Std Lean Lake ];
modDepsFiles = symlinkJoin { name = "modDepsFiles"; paths = map (l: l.modDepsFile) (stdlib ++ [ Leanc ]); };
depRoots = symlinkJoin { name = "depRoots"; paths = map (l: l.depRoots) stdlib; };
iTree = symlinkJoin { name = "ileans"; paths = map (l: l.iTree) stdlib; };
Leanc = build { name = "Leanc"; src = lean-bin-tools-unwrapped.leanc_src; deps = stdlib; roots = [ "Leanc" ]; };
stdlibLinkFlags = "${lib.concatMapStringsSep " " (l: "-L${l.staticLib}") stdlib} -L${leancpp}/lib/lean";
libInit_shared = runCommand "libInit_shared" { buildInputs = [ stdenv.cc ]; libName = "libInit_shared${stdenv.hostPlatform.extensions.sharedLibrary}"; } ''
mkdir $out
touch empty.c
${stdenv.cc}/bin/cc -shared -o $out/$libName empty.c
'';
leanshared_1 = runCommand "leanshared_1" { buildInputs = [ stdenv.cc ]; libName = "leanshared_1${stdenv.hostPlatform.extensions.sharedLibrary}"; } ''
mkdir $out
touch empty.c
${stdenv.cc}/bin/cc -shared -o $out/$libName empty.c
'';
leanshared = runCommand "leanshared" { buildInputs = [ stdenv.cc ]; libName = "libleanshared${stdenv.hostPlatform.extensions.sharedLibrary}"; } ''
mkdir $out
LEAN_CC=${stdenv.cc}/bin/cc ${lean-bin-tools-unwrapped}/bin/leanc -shared ${lib.optionalString stdenv.isLinux "-Wl,-Bsymbolic"} \
-Wl,--whole-archive ${leancpp}/lib/temp/libleanshell.a -lInit -lStd -lLean -lleancpp ${leancpp}/lib/libleanrt_initial-exec.a -Wl,--no-whole-archive -lstdc++ \
-lm ${stdlibLinkFlags} \
$(${llvmPackages.libllvm.dev}/bin/llvm-config --ldflags --libs) \
-o $out/$libName
'';
mods = foldl' (mods: pkg: mods // pkg.mods) {} stdlib;
print-paths = Lean.makePrintPathsFor [] mods;
leanc = writeShellScriptBin "leanc" ''
LEAN_CC=${stdenv.cc}/bin/cc ${Leanc.executable}/bin/leanc -I${lean-bin-tools-unwrapped}/include ${stdlibLinkFlags} -L${libInit_shared} -L${leanshared_1} -L${leanshared} -L${Lake.sharedLib} "$@"
'';
lean = runCommand "lean" { buildInputs = lib.optional stdenv.isDarwin darwin.cctools; } ''
mkdir -p $out/bin
${leanc}/bin/leanc ${leancpp}/lib/temp/libleanmain.a ${libInit_shared}/* ${leanshared_1}/* ${leanshared}/* -o $out/bin/lean
'';
# derivation following the directory layout of the "basic" setup, mostly useful for running tests
lean-all = stdenv.mkDerivation {
name = "lean-${desc}";
buildCommand = ''
mkdir -p $out/bin $out/lib/lean
ln -sf ${leancpp}/lib/lean/* ${lib.concatMapStringsSep " " (l: "${l.modRoot}/* ${l.staticLib}/*") (lib.reverseList stdlib)} ${libInit_shared}/* ${leanshared_1}/* ${leanshared}/* ${Lake.sharedLib}/* $out/lib/lean/
# put everything in a single final derivation so `IO.appDir` references work
cp ${lean}/bin/lean ${leanc}/bin/leanc ${Lake-Main.executable}/bin/lake $out/bin
# NOTE: `lndir` will not override existing `bin/leanc`
${lndir}/bin/lndir -silent ${lean-bin-tools-unwrapped} $out
'';
meta.mainProgram = "lean";
};
cacheRoots = linkFarmFromDrvs "cacheRoots" ([
stage0 lean leanc lean-all iTree modDepsFiles depRoots Leanc.src
] ++ map (lib: lib.oTree) stdlib);
test = buildCMake {
name = "lean-test-${desc}";
realSrc = lib.sourceByRegex src [ "src.*" "tests.*" ];
buildInputs = [ gmp libuv perl git cadical ];
preConfigure = ''
cd src
'';
extraCMakeFlags = [ "-DLLVM=OFF" ];
postConfigure = ''
patchShebangs ../../tests ../lake
rm -r bin lib include share
ln -sf ${lean-all}/* .
'';
buildPhase = ''
ctest --output-junit test-results.xml --output-on-failure -E 'leancomptest_(doc_example|foreign)|leanlaketest_reverse-ffi|leanruntest_timeIO' -j$NIX_BUILD_CORES
'';
installPhase = ''
mkdir $out
mv test-results.xml $out
'';
};
update-stage0 =
let cTree = symlinkJoin { name = "cs"; paths = map (lib: lib.cTree) (stdlib ++ [Lake-Main]); }; in
writeShellScriptBin "update-stage0" ''
CSRCS=${cTree} CP_C_PARAMS="--dereference --no-preserve=all" ${src + "/script/lib/update-stage0"}
'';
update-stage0-commit = writeShellScriptBin "update-stage0-commit" ''
set -euo pipefail
${update-stage0}/bin/update-stage0
git commit -m "chore: update stage0"
'';
link-ilean = writeShellScriptBin "link-ilean" ''
dest=''${1:-src}
rm -rf $dest/build/lib || true
mkdir -p $dest/build/lib
ln -s ${iTree}/* $dest/build/lib
'';
benchmarks =
let
entries = attrNames (readDir (src + "/tests/bench"));
leanFiles = map (n: elemAt n 0) (filter (n: n != null) (map (match "(.*)\.lean") entries));
in lib.genAttrs leanFiles (n: (buildLeanPackage {
name = n;
src = filterSource (e: _: baseNameOf e == "${n}.lean") (src + "/tests/bench");
}).executable);
};
stage1 = stage { stage = 1; prevStage = stage0; self = stage1; };
stage2 = stage { stage = 2; prevStage = stage1; self = stage2; };
stage3 = stage { stage = 3; prevStage = stage2; self = stage3; };
}

247
nix/buildLeanPackage.nix Normal file
View File

@@ -0,0 +1,247 @@
{ lean, lean-leanDeps ? lean, lean-final ? lean, leanc,
stdenv, lib, coreutils, gnused, writeShellScriptBin, bash, substituteAll, symlinkJoin, linkFarmFromDrvs,
runCommand, darwin, mkShell, ... }:
let lean-final' = lean-final; in
lib.makeOverridable (
{ name, src, fullSrc ? src, srcPrefix ? "", srcPath ? "$PWD/${srcPrefix}",
# Lean dependencies. Each entry should be an output of buildLeanPackage.
deps ? [ lean.Init lean.Std lean.Lean ],
# Static library dependencies. Each derivation `static` should contain a static library in the directory `${static}`.
staticLibDeps ? [],
# Whether to wrap static library inputs in a -Wl,--start-group [...] -Wl,--end-group to ensure dependencies are resolved.
groupStaticLibs ? false,
# Shared library dependencies included at interpretation with --load-dynlib and linked to. Each derivation `shared` should contain a
# shared library at the path `${shared}/${shared.libName or shared.name}` and a name to link to like `-l${shared.linkName or shared.name}`.
# These libs are also linked to in packages that depend on this one.
nativeSharedLibs ? [],
# Lean modules to include.
# A set of Lean modules names as strings (`"Foo.Bar"`) or attrsets (`{ name = "Foo.Bar"; glob = "one" | "submodules" | "andSubmodules"; }`);
# see Lake README for glob meanings. Dependencies of selected modules are always included.
roots ? [ name ],
# Output from `lean --deps-json` on package source files. Persist the corresponding output attribute to a file and pass it back in here to avoid IFD.
# Must be refreshed on any change in `import`s or set of source file names.
modDepsFile ? null,
# Whether to compile each module into a native shared library that is loaded whenever the module is imported in order to accelerate evaluation
precompileModules ? false,
# Whether to compile the package into a native shared library that is loaded whenever *any* of the package's modules is imported into another package.
# If `precompileModules` is also `true`, the latter only affects imports within the current package.
precompilePackage ? precompileModules,
# Lean plugin dependencies. Each derivation `plugin` should contain a plugin library at path `${plugin}/${plugin.name}`.
pluginDeps ? [],
# `overrideAttrs` for `buildMod`
overrideBuildModAttrs ? null,
debug ? false, leanFlags ? [], leancFlags ? [], linkFlags ? [], executableName ? lib.toLower name, libName ? name, sharedLibName ? libName,
srcTarget ? "..#stage0", srcArgs ? "(\${args[*]})", lean-final ? lean-final' }@args:
with builtins; let
# "Init.Core" ~> "Init/Core"
modToPath = mod: replaceStrings ["."] ["/"] mod;
modToAbsPath = mod: "${src}/${modToPath mod}";
# sanitize file name before copying to store, except when already in store
copyToStoreSafe = base: suffix: if lib.isDerivation base then base + suffix else
builtins.path { name = lib.strings.sanitizeDerivationName (baseNameOf suffix); path = base + suffix; };
modToLean = mod: copyToStoreSafe src "/${modToPath mod}.lean";
bareStdenv = ./bareStdenv;
mkBareDerivation = args: derivation (args // {
name = lib.strings.sanitizeDerivationName args.name;
stdenv = bareStdenv;
inherit (stdenv) system;
buildInputs = (args.buildInputs or []) ++ [ coreutils ];
builder = stdenv.shell;
args = [ "-c" ''
source $stdenv/setup
set -u
${args.buildCommand}
'' ];
}) // { overrideAttrs = f: mkBareDerivation (lib.fix (lib.extends f (_: args))); };
runBareCommand = name: args: buildCommand: mkBareDerivation (args // { inherit name buildCommand; });
runBareCommandLocal = name: args: buildCommand: runBareCommand name (args // {
preferLocalBuild = true;
allowSubstitutes = false;
}) buildCommand;
mkSharedLib = name: args: runBareCommand "${name}-dynlib" {
buildInputs = [ stdenv.cc ] ++ lib.optional stdenv.isDarwin darwin.cctools;
libName = "${name}${stdenv.hostPlatform.extensions.sharedLibrary}";
} ''
mkdir -p $out
${leanc}/bin/leanc -shared ${args} -o $out/$libName
'';
depRoot = name: deps: mkBareDerivation {
name = "${name}-depRoot";
inherit deps;
depRoots = map (drv: drv.LEAN_PATH) deps;
passAsFile = [ "deps" "depRoots" ];
buildCommand = ''
mkdir -p $out
for i in $(cat $depRootsPath); do
cp -dru --no-preserve=mode $i/. $out
done
for i in $(cat $depsPath); do
cp -drsu --no-preserve=mode $i/. $out
done
'';
};
srcRoot = src;
# A flattened list of Lean-module dependencies (`deps`)
allExternalDeps = lib.unique (lib.foldr (dep: allExternalDeps: allExternalDeps ++ [ dep ] ++ dep.allExternalDeps) [] deps);
allNativeSharedLibs =
lib.unique (lib.flatten (nativeSharedLibs ++ (map (dep: dep.allNativeSharedLibs or []) allExternalDeps)));
# A flattened list of all static library dependencies: this and every dep module's explicitly provided `staticLibDeps`,
# plus every dep module itself: `dep.staticLib`
allStaticLibDeps =
lib.unique (lib.flatten (staticLibDeps ++ (map (dep: [dep.staticLib] ++ dep.staticLibDeps or []) allExternalDeps)));
pathOfSharedLib = dep: dep.libPath or "${dep}/${dep.libName or dep.name}";
leanPluginFlags = lib.concatStringsSep " " (map (dep: "--plugin=${pathOfSharedLib dep}") pluginDeps);
loadDynlibsOfDeps = deps: lib.unique (concatMap (d: d.propagatedLoadDynlibs) deps);
# submodules "Init" = ["Init.List.Basic", "Init.Core", ...]
submodules = mod: let
dir = readDir (modToAbsPath mod);
f = p: t:
if t == "directory" then
submodules "${mod}.${p}"
else
let m = builtins.match "(.*)\.lean" p;
in lib.optional (m != null) "${mod}.${head m}";
in concatLists (lib.mapAttrsToList f dir);
# conservatively approximate list of source files matched by glob
expandGlobAllApprox = g:
if typeOf g == "string" then
# we can't know the required files without parsing dependencies (which is what we want this
# function for), so we approximate to the entire package.
let root = (head (split "\\." g));
in lib.optional (pathExists (src + "/${modToPath root}.lean")) root ++ lib.optionals (pathExists (modToAbsPath root)) (submodules root)
else if g.glob == "one" then expandGlobAllApprox g.mod
else if g.glob == "submodules" then submodules g.mod
else if g.glob == "andSubmodules" then [g.mod] ++ submodules g.mod
else throw "unknown glob kind '${g}'";
# list of modules that could potentially be involved in the build
candidateMods = lib.unique (concatMap expandGlobAllApprox roots);
candidateFiles = map modToLean candidateMods;
modDepsFile = args.modDepsFile or mkBareDerivation {
name = "${name}-deps.json";
candidateFiles = lib.concatStringsSep " " candidateFiles;
passAsFile = [ "candidateFiles" ];
buildCommand = ''
mkdir $out
${lean-leanDeps}/bin/lean --deps-json --stdin < $candidateFilesPath > $out/$name
'';
};
modDeps = fromJSON (
# the only possible references to store paths in the JSON should be inside errors, so no chance of missed dependencies from this
unsafeDiscardStringContext (readFile "${modDepsFile}/${modDepsFile.name}"));
# map from module name to list of imports
modDepsMap = listToAttrs (lib.zipListsWith lib.nameValuePair candidateMods modDeps.imports);
maybeOverrideAttrs = f: x: if f != null then x.overrideAttrs f else x;
# build module (.olean and .c) given derivations of all (immediate) dependencies
# TODO: make `rec` parts override-compatible?
buildMod = mod: deps: maybeOverrideAttrs overrideBuildModAttrs (mkBareDerivation rec {
name = "${mod}";
LEAN_PATH = depRoot mod deps;
LEAN_ABORT_ON_PANIC = "1";
relpath = modToPath mod;
buildInputs = [ lean ];
leanPath = relpath + ".lean";
# should be either single .lean file or directory directly containing .lean file plus dependencies
src = copyToStoreSafe srcRoot ("/" + leanPath);
outputs = [ "out" "ilean" "c" ];
oleanPath = relpath + ".olean";
ileanPath = relpath + ".ilean";
cPath = relpath + ".c";
inherit leanFlags leanPluginFlags;
leanLoadDynlibFlags = map (p: "--load-dynlib=${pathOfSharedLib p}") (loadDynlibsOfDeps deps);
buildCommand = ''
dir=$(dirname $relpath)
mkdir -p $dir $out/$dir $ilean/$dir $c/$dir
if [ -d $src ]; then cp -r $src/. .; else cp $src $leanPath; fi
lean -o $out/$oleanPath -i $out/$ileanPath -c $c/$cPath $leanPath $leanFlags $leanPluginFlags $leanLoadDynlibFlags
'';
}) // {
inherit deps;
propagatedLoadDynlibs = loadDynlibsOfDeps deps;
};
compileMod = mod: drv: mkBareDerivation {
name = "${mod}-cc";
buildInputs = [ leanc stdenv.cc ];
hardeningDisable = [ "all" ];
oPath = drv.relpath + ".o";
inherit leancFlags;
buildCommand = ''
mkdir -p $out/$(dirname ${drv.relpath})
# make local "copy" so `drv`'s Nix store path doesn't end up in ccache's hash
ln -s ${drv.c}/${drv.cPath} src.c
# on the other hand, a debug build is pretty fast anyway, so preserve the path for gdb
leanc -c -o $out/$oPath $leancFlags -fPIC ${if debug then "${drv.c}/${drv.cPath} -g" else "src.c -O3 -DNDEBUG -DLEAN_EXPORTING"}
'';
};
mkMod = mod: deps:
let drv = buildMod mod deps;
obj = compileMod mod drv;
# this attribute will only be used if any dependent module is precompiled
sharedLib = mkSharedLib mod "${obj}/${obj.oPath} ${lib.concatStringsSep " " (map (d: pathOfSharedLib d.sharedLib) deps)}";
in drv // {
inherit obj sharedLib;
} // lib.optionalAttrs precompileModules {
propagatedLoadDynlibs = [sharedLib];
};
externalModMap = lib.foldr (dep: depMap: depMap // dep.mods) {} allExternalDeps;
# map from module name to derivation
modCandidates = mapAttrs (mod: header:
let
deps = if header.errors == []
then map (m: m.module) header.result.imports
else abort "errors while parsing imports of ${mod}:\n${lib.concatStringsSep "\n" header.errors}";
in mkMod mod (map (dep: if modDepsMap ? ${dep} then modCandidates.${dep} else externalModMap.${dep}) deps)) modDepsMap;
expandGlob = g:
if typeOf g == "string" then [g]
else if g.glob == "one" then [g.mod]
else if g.glob == "submodules" then submodules g.mod
else if g.glob == "andSubmodules" then [g.mod] ++ submodules g.mod
else throw "unknown glob kind '${g}'";
# subset of `modCandidates` that is transitively reachable from `roots`
mods' = listToAttrs (map (e: { name = e.key; value = modCandidates.${e.key}; }) (genericClosure {
startSet = map (m: { key = m; }) (concatMap expandGlob roots);
operator = e: if modDepsMap ? ${e.key} then map (m: { key = m.module; }) (filter (m: modCandidates ? ${m.module}) modDepsMap.${e.key}.result.imports) else [];
}));
allLinkFlags = lib.foldr (shared: acc: acc ++ [ "-L${shared}" "-l${shared.linkName or shared.name}" ]) linkFlags allNativeSharedLibs;
objects = mapAttrs (_: m: m.obj) mods';
bintools = if stdenv.isDarwin then darwin.cctools else stdenv.cc.bintools.bintools;
staticLib = runCommand "${name}-lib" { buildInputs = [ bintools ]; } ''
mkdir -p $out
ar Trcs $out/lib${libName}.a ${lib.concatStringsSep " " (map (drv: "${drv}/${drv.oPath}") (attrValues objects))};
'';
staticLibLinkWrapper = libs: if groupStaticLibs && !stdenv.isDarwin
then "-Wl,--start-group ${libs} -Wl,--end-group"
else "${libs}";
in rec {
inherit name lean deps staticLibDeps allNativeSharedLibs allLinkFlags allExternalDeps src objects staticLib modDepsFile;
mods = mapAttrs (_: m:
m //
# if neither precompilation option was set but a dependent module wants to be precompiled, default to precompiling this package whole
lib.optionalAttrs (precompilePackage || !precompileModules) { inherit sharedLib; } //
lib.optionalAttrs precompilePackage { propagatedLoadDynlibs = [sharedLib]; })
mods';
modRoot = depRoot name (attrValues mods);
depRoots = linkFarmFromDrvs "depRoots" (map (m: m.LEAN_PATH) (attrValues mods));
cTree = symlinkJoin { name = "${name}-cTree"; paths = map (mod: mod.c) (attrValues mods); };
oTree = symlinkJoin { name = "${name}-oTree"; paths = (attrValues objects); };
iTree = symlinkJoin { name = "${name}-iTree"; paths = map (mod: mod.ilean) (attrValues mods); };
sharedLib = mkSharedLib "lib${sharedLibName}" ''
${if stdenv.isDarwin then "-Wl,-force_load,${staticLib}/lib${libName}.a" else "-Wl,--whole-archive ${staticLib}/lib${libName}.a -Wl,--no-whole-archive"} \
${lib.concatStringsSep " " (map (d: "${d.sharedLib}/*") deps)}'';
executable = lib.makeOverridable ({ withSharedStdlib ? true }: let
objPaths = map (drv: "${drv}/${drv.oPath}") (attrValues objects) ++ lib.optional withSharedStdlib "${lean-final.leanshared}/*";
in runCommand executableName { buildInputs = [ stdenv.cc leanc ]; } ''
mkdir -p $out/bin
leanc ${staticLibLinkWrapper (lib.concatStringsSep " " (objPaths ++ map (d: "${d}/*.a") allStaticLibDeps))} \
-o $out/bin/${executableName} \
${lib.concatStringsSep " " allLinkFlags}
'') {};
})

42
nix/lake-dev.in Normal file
View File

@@ -0,0 +1,42 @@
#!@bash@/bin/bash
set -euo pipefail
function pebkac() {
echo 'This is just a simple Nix adapter for `lake print-paths|serve`.'
exit 1
}
[[ $# -gt 0 ]] || pebkac
case $1 in
--version)
# minimum version for `lake serve` with fallback
echo 3.1.0
;;
print-paths)
shift
deps="$@"
root=.
# fall back to initial package if not in package
[[ ! -f "$root/flake.nix" ]] && root="@srcRoot@"
target="$root#print-paths"
args=()
# HACK: use stage 0 instead of 1 inside Lean's own `src/`
[[ -d Lean && -f ../flake.nix ]] && target="@srcTarget@print-paths" && args=@srcArgs@
for dep in $deps; do
target="$target.\"$dep\""
done
echo "Building dependencies..." >&2
# -v only has "built ...", but "-vv" is a bit too verbose
exec @nix@/bin/nix run "$target" ${args[*]} -v
;;
serve)
shift
[[ ${1:-} == "--" ]] && shift
# `link-ilean` puts them there
LEAN_PATH=${LEAN_PATH:+$LEAN_PATH:}$PWD/build/lib exec $(dirname $0)/lean --server "$@"
;;
*)
pebkac
;;
esac

28
nix/lean-dev.in Normal file
View File

@@ -0,0 +1,28 @@
#!@bash@/bin/bash
set -euo pipefail
root="."
# find package root
while [[ "$root" != / ]]; do
[ -f "$root/flake.nix" ] && break
root="$(realpath "$root/..")"
done
# fall back to initial package if not in package
[[ ! -f "$root/flake.nix" ]] && root="@srcRoot@"
# use Lean w/ package unless in server mode (which has its own LEAN_PATH logic)
target="$root#lean-package"
for arg in "$@"; do
case $arg in
--server | --worker | -v | --version)
target="$root#lean"
;;
esac
done
args=(-- "$@")
# HACK: use stage 0 instead of 1 inside Lean's own `src/`
[[ -d Lean && -f ../flake.nix ]] && target="@srcTarget@" && args=@srcArgs@
LEAN_SYSROOT="$(dirname "$0")/.." exec @nix@/bin/nix ${LEAN_NIX_ARGS:-} run "$target" ${args[*]}

52
nix/packages.nix Normal file
View File

@@ -0,0 +1,52 @@
{ src, pkgs, ... } @ args:
with pkgs;
let
# https://github.com/NixOS/nixpkgs/issues/130963
llvmPackages = if stdenv.isDarwin then llvmPackages_11 else llvmPackages_15;
cc = (ccacheWrapper.override rec {
cc = llvmPackages.clang;
extraConfig = ''
export CCACHE_DIR=/nix/var/cache/ccache
export CCACHE_UMASK=007
export CCACHE_BASE_DIR=$NIX_BUILD_TOP
# https://github.com/NixOS/nixpkgs/issues/109033
args=("$@")
for ((i=0; i<"''${#args[@]}"; i++)); do
case ''${args[i]} in
-frandom-seed=*) unset args[i]; break;;
esac
done
set -- "''${args[@]}"
[ -d $CCACHE_DIR ] || exec ${cc}/bin/$(basename "$0") "$@"
'';
}).overrideAttrs (old: {
# https://github.com/NixOS/nixpkgs/issues/119779
installPhase = builtins.replaceStrings ["use_response_file_by_default=1"] ["use_response_file_by_default=0"] old.installPhase;
});
stdenv' = if stdenv.isLinux then useGoldLinker stdenv else stdenv;
lean = callPackage (import ./bootstrap.nix) (args // {
stdenv = overrideCC stdenv' cc;
inherit src buildLeanPackage llvmPackages;
});
makeOverridableLeanPackage = f:
let newF = origArgs: f origArgs // {
overrideArgs = newArgs: makeOverridableLeanPackage f (origArgs // newArgs);
};
in lib.setFunctionArgs newF (lib.getFunctionArgs f) // {
override = args: makeOverridableLeanPackage (f.override args);
};
buildLeanPackage = makeOverridableLeanPackage (callPackage (import ./buildLeanPackage.nix) (args // {
inherit (lean) stdenv;
lean = lean.stage1;
inherit (lean.stage1) leanc;
}));
in {
inherit cc buildLeanPackage llvmPackages;
nixpkgs = pkgs;
ciShell = writeShellScriptBin "ciShell" ''
set -o pipefail
export PATH=${moreutils}/bin:$PATH
# prefix lines with cumulative and individual execution time
"$@" |& ts -i "(%.S)]" | ts -s "[%M:%S"
'';
} // lean.stage1

View File

@@ -0,0 +1 @@
#eval "Hello, world!"

View File

@@ -0,0 +1,21 @@
{
description = "My Lean package";
inputs.lean.url = "github:leanprover/lean4";
inputs.flake-utils.url = "github:numtide/flake-utils";
outputs = { self, lean, flake-utils }: flake-utils.lib.eachDefaultSystem (system:
let
leanPkgs = lean.packages.${system};
pkg = leanPkgs.buildLeanPackage {
name = "MyPackage"; # must match the name of the top-level .lean file
src = ./.;
};
in {
packages = pkg // {
inherit (leanPkgs) lean;
};
defaultPackage = pkg.modRoot;
});
}

View File

@@ -1,132 +0,0 @@
/-
Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean
namespace Lean.Meta.Grind.Analyzer
/-!
A simple E-matching annotation analyzer.
For each theorem annotated as an E-matching candidate, it creates an artificial goal, executes `grind` and shows the
number of instances created.
For a theorem of the form `params -> type`, the artificial goal is of the form `params -> type -> False`.
-/
/--
`grind` configuration for the analyzer. We disable case-splits and lookahead,
increase the number of generations, and limit the number of instances generated.
-/
def config : Grind.Config := {
splits := 0
lookahead := false
mbtc := false
ematch := 20
instances := 100
gen := 10
}
structure Config where
/-- Minimum number of instantiations to trigger summary report -/
min : Nat := 10
/-- Minimum number of instantiations to trigger detailed report -/
detailed : Nat := 50
def mkParams : MetaM Params := do
let params Grind.mkParams config
let ematch getEMatchTheorems
let casesTypes Grind.getCasesTypes
return { params with ematch, casesTypes }
/-- Returns the total number of generated instances. -/
private def sum (cs : PHashMap Origin Nat) : Nat := Id.run do
let mut r := 0
for (_, c) in cs do
r := r + c
return r
private def thmsToMessageData (thms : PHashMap Origin Nat) : MetaM MessageData := do
let data := thms.toArray.filterMap fun (origin, c) =>
match origin with
| .decl declName => some (declName, c)
| _ => none
let data := data.qsort fun (d₁, c₁) (d₂, c₂) => if c₁ == c₂ then Name.lt d₁ d₂ else c₁ > c₂
let data data.mapM fun (declName, counter) =>
return .trace { cls := `thm } m!"{.ofConst (← mkConstWithLevelParams declName)} ↦ {counter}" #[]
return .trace { cls := `thm } "instances" data
/--
Analyzes theorem `declName`. That is, creates the artificial goal based on `declName` type,
and invokes `grind` on it.
-/
def analyzeEMatchTheorem (declName : Name) (c : Config) : MetaM Unit := do
let info getConstInfo declName
let mvarId forallTelescope info.type fun _ type => do
withLocalDeclD `h type fun _ => do
return ( mkFreshExprMVar (mkConst ``False)).mvarId!
let result Grind.main mvarId ( mkParams) (pure ())
let thms := result.counters.thm
let s := sum thms
if s > c.min then
IO.println s!"{declName} : {s}"
if s > c.detailed then
logInfo m!"{declName}\n{← thmsToMessageData thms}"
-- Not sure why this is failing: `down_pure` perhaps has an unnecessary universe parameter?
run_meta analyzeEMatchTheorem ``Std.Do.SPred.down_pure {}
/-- Analyzes all theorems in the standard library marked as E-matching theorems. -/
def analyzeEMatchTheorems (c : Config := {}) : MetaM Unit := do
let origins := ( getEMatchTheorems).getOrigins
let decls := origins.filterMap fun | .decl declName => some declName | _ => none
for declName in decls.mergeSort Name.lt do
try
analyzeEMatchTheorem declName c
catch e =>
logError m!"{declName} failed with {e.toMessageData}"
logInfo m!"Finished analyzing {decls.length} theorems"
/-- Macro for analyzing E-match theorems with unlimited heartbeats -/
macro "#analyzeEMatchTheorems" : command => `(
set_option maxHeartbeats 0 in
run_meta analyzeEMatchTheorems
)
#analyzeEMatchTheorems
-- -- We can analyze specific theorems using commands such as
set_option trace.grind.ematch.instance true
-- 1. grind immediately sees `(#[] : Array α) = ([] : List α).toArray` but probably this should be hidden.
-- 2. `Vector.toArray_empty` keys on `Array.mk []` rather than `#v[].toArray`
-- I guess we could add `(#[].extract _ _).extract _ _` as a stop pattern.
run_meta analyzeEMatchTheorem ``Array.extract_empty {}
-- Neither `Option.bind_some` nor `Option.bind_fun_some` fire, because the terms appear inside
-- lambdas. So we get crazy things like:
-- `fun x => ((some x).bind some).bind fun x => (some x).bind fun x => (some x).bind some`
-- We could consider replacing `filterMap_some` with
-- `filterMap g (filterMap f xs) = filterMap (f >=> g) xs`
-- to avoid the lambda that `grind` struggles with, but this would require more API around the fish.
run_meta analyzeEMatchTheorem ``Array.filterMap_some {}
-- Not entirely certain what is wrong here, but certainly
-- `eq_empty_of_append_eq_empty` is firing too often.
-- Ideally we could instantiate this is we fine `xs ++ ys` in the same equivalence class,
-- note just as soon as we see `xs ++ ys`.
-- I've tried removing this in https://github.com/leanprover/lean4/pull/10162
run_meta analyzeEMatchTheorem ``Array.range'_succ {}
-- Perhaps the same story here.
run_meta analyzeEMatchTheorem ``Array.range_succ {}
-- `zip_map_left` and `zip_map_right` are bad grind lemmas,
-- checking if they can be removed in https://github.com/leanprover/lean4/pull/10163
run_meta analyzeEMatchTheorem ``Array.zip_map {}
-- It seems crazy to me that as soon as we have `0 >>> n = 0`, we instantiate based on the
-- pattern `0 >>> n >>> m` by substituting `0` into `0 >>> n` to produce the `0 >>> n >>> n`.
-- I don't think any forbidden subterms can help us here. I don't know what to do. :-(
run_meta analyzeEMatchTheorem ``Int.zero_shiftRight {}

View File

@@ -1,96 +1,9 @@
#!/usr/bin/env bash
set -euxo pipefail
set -euo pipefail
cmake --preset release 1>&2
# We benchmark against stage2/bin to test new optimizations.
timeout -s KILL 1h time make -C build/release -j$(nproc) stage3 1>&2
# We benchmark against stage 2 to test new optimizations.
timeout -s KILL 1h time bash -c 'mkdir -p build/release; cd build/release; cmake ../.. && make -j$(nproc) stage2' 1>&2
export PATH=$PWD/build/release/stage2/bin:$PATH
# The extra opts used to be passed to the Makefile during benchmarking only but with Lake it is
# easier to configure them statically.
cmake -B build/release/stage3 -S src -DLEAN_EXTRA_LAKEFILE_TOML='weakLeanArgs=["-Dprofiler=true", "-Dprofiler.threshold=9999999", "--stats"]' 1>&2
(
cd tests/bench
timeout -s KILL 1h time temci exec --config speedcenter.yaml --in speedcenter.exec.velcom.yaml 1>&2
temci report run_output.yaml --reporter codespeed2
)
if [ -d .git ]; then
DIR="$(git rev-parse @)"
BASE_URL="https://speed.lean-lang.org/lean4-out/$DIR"
{
cat <<'EOF'
<!DOCTYPE html>
<html>
<head>
<meta charset="UTF-8">
<title>Lakeprof Report</title>
</head>
<h1>Lakeprof Report</h1>
<button type="button" id="btn_fetch">View build trace in Perfetto</button>
<script type="text/javascript">
const ORIGIN = 'https://ui.perfetto.dev';
const btnFetch = document.getElementById('btn_fetch');
async function fetchAndOpen(traceUrl) {
const resp = await fetch(traceUrl);
// Error checking is left as an exercise to the reader.
const blob = await resp.blob();
const arrayBuffer = await blob.arrayBuffer();
openTrace(arrayBuffer, traceUrl);
}
function openTrace(arrayBuffer, traceUrl) {
const win = window.open(ORIGIN);
if (!win) {
btnFetch.style.background = '#f3ca63';
btnFetch.onclick = () => openTrace(arrayBuffer);
btnFetch.innerText = 'Popups blocked, click here to open the trace file';
return;
}
const timer = setInterval(() => win.postMessage('PING', ORIGIN), 50);
const onMessageHandler = (evt) => {
if (evt.data !== 'PONG') return;
// We got a PONG, the UI is ready.
window.clearInterval(timer);
window.removeEventListener('message', onMessageHandler);
const reopenUrl = new URL(location.href);
reopenUrl.hash = `#reopen=${traceUrl}`;
win.postMessage({
perfetto: {
buffer: arrayBuffer,
title: 'Lake Build Trace',
url: reopenUrl.toString(),
}}, ORIGIN);
};
window.addEventListener('message', onMessageHandler);
}
// This is triggered when following the link from the Perfetto UI's sidebar.
if (location.hash.startsWith('#reopen=')) {
const traceUrl = location.hash.substr(8);
fetchAndOpen(traceUrl);
}
EOF
cat <<EOF
btnFetch.onclick = () => fetchAndOpen("$BASE_URL/lakeprof.trace_event");
</script>
EOF
echo "<pre><code>"
(cd src; lakeprof report -prc)
echo "</code></pre>"
echo "</body></html>"
} | tee index.html
curl -T index.html $BASE_URL/index.html
curl -T src/lakeprof.log $BASE_URL/lakeprof.log
curl -T src/lakeprof.trace_event $BASE_URL/lakeprof.trace_event
fi

View File

@@ -5,7 +5,6 @@ Merge a tag into a branch on a GitHub repository.
This script checks if a specified tag can be merged cleanly into a branch and performs
the merge if possible. If the merge cannot be done cleanly, it prints a helpful message.
Merge conflicts in the lean-toolchain file are automatically resolved by accepting the incoming changes.
Usage:
python3 merge_remote.py <org/repo> <branch> <tag>
@@ -59,32 +58,6 @@ def clone_repo(repo, temp_dir):
return True
def get_conflicted_files():
"""Get list of files with merge conflicts."""
result = run_command("git diff --name-only --diff-filter=U", check=False)
if result.returncode == 0:
return result.stdout.strip().split('\n') if result.stdout.strip() else []
return []
def resolve_lean_toolchain_conflict(tag):
"""Resolve lean-toolchain conflict by accepting incoming (tag) changes."""
print("Resolving lean-toolchain conflict by accepting incoming changes...")
# Accept theirs (incoming) version for lean-toolchain
result = run_command(f"git checkout --theirs lean-toolchain", check=False)
if result.returncode != 0:
print("Failed to resolve lean-toolchain conflict")
return False
# Add the resolved file
add_result = run_command("git add lean-toolchain", check=False)
if add_result.returncode != 0:
print("Failed to stage resolved lean-toolchain")
return False
return True
def check_and_merge(repo, branch, tag, temp_dir):
"""Check if tag can be merged into branch and perform the merge if possible."""
# Change to the temporary directory
@@ -125,37 +98,12 @@ def check_and_merge(repo, branch, tag, temp_dir):
# Try merging the tag directly
print(f"Merging {tag} into {branch}...")
merge_result = run_command(f"git merge {tag} --no-edit", check=False)
if merge_result.returncode != 0:
# Check which files have conflicts
conflicted_files = get_conflicted_files()
if conflicted_files == ['lean-toolchain']:
# Only lean-toolchain has conflicts, resolve it
print("Merge conflict detected only in lean-toolchain.")
if resolve_lean_toolchain_conflict(tag):
# Continue the merge with the resolved conflict
print("Continuing merge with resolved lean-toolchain...")
continue_result = run_command(f"git commit --no-edit", check=False)
if continue_result.returncode != 0:
print("Failed to complete merge after resolving lean-toolchain")
run_command("git merge --abort")
return False
else:
print("Failed to resolve lean-toolchain conflict")
run_command("git merge --abort")
return False
else:
# Other files have conflicts, or unable to determine
if conflicted_files:
print(f"Cannot merge {tag} cleanly into {branch}.")
print(f"Merge conflicts in: {', '.join(conflicted_files)}")
else:
print(f"Cannot merge {tag} cleanly into {branch}.")
print("Merge conflicts would occur.")
print("Aborting merge.")
run_command("git merge --abort")
return False
print(f"Cannot merge {tag} cleanly into {branch}.")
print("Merge conflicts would occur. Aborting merge.")
run_command("git merge --abort")
return False
print(f"Pushing changes to remote...")
push_result = run_command(f"git push origin {branch}")

View File

@@ -3,32 +3,6 @@ import sys
import subprocess
import requests
def check_gh_auth():
"""Check if GitHub CLI is properly authenticated."""
try:
result = subprocess.run(["gh", "auth", "status"], capture_output=True, text=True)
if result.returncode != 0:
return False, result.stderr
return True, None
except FileNotFoundError:
return False, "GitHub CLI (gh) is not installed. Please install it first."
except Exception as e:
return False, f"Error checking authentication: {e}"
def handle_gh_error(error_output):
"""Handle GitHub CLI errors and provide helpful messages."""
if "Not Found (HTTP 404)" in error_output:
return "Repository not found or access denied. Please check:\n" \
"1. The repository name is correct\n" \
"2. You have access to the repository\n" \
"3. Your GitHub CLI authentication is valid"
elif "Bad credentials" in error_output or "invalid" in error_output.lower():
return "Authentication failed. Please run 'gh auth login' to re-authenticate."
elif "rate limit" in error_output.lower():
return "GitHub API rate limit exceeded. Please try again later."
else:
return f"GitHub API error: {error_output}"
def main():
if len(sys.argv) != 4:
print("Usage: ./push_repo_release_tag.py <repo> <branch> <version_tag>")
@@ -40,13 +14,6 @@ def main():
print(f"Error: Branch '{branch}' is not 'master' or 'main'.")
sys.exit(1)
# Check GitHub CLI authentication first
auth_ok, auth_error = check_gh_auth()
if not auth_ok:
print(f"Authentication error: {auth_error}")
print("\nTo fix this, run: gh auth login")
sys.exit(1)
# Get the `lean-toolchain` file content
lean_toolchain_url = f"https://raw.githubusercontent.com/{repo}/{branch}/lean-toolchain"
try:
@@ -76,23 +43,12 @@ def main():
for tag in existing_tags:
print(tag.replace("refs/tags/", ""))
sys.exit(1)
elif list_tags_output.returncode != 0:
# Handle API errors when listing tags
error_msg = handle_gh_error(list_tags_output.stderr)
print(f"Error checking existing tags: {error_msg}")
sys.exit(1)
# Get the SHA of the branch
get_sha_cmd = [
"gh", "api", f"repos/{repo}/git/ref/heads/{branch}", "--jq", ".object.sha"
]
sha_result = subprocess.run(get_sha_cmd, capture_output=True, text=True)
if sha_result.returncode != 0:
error_msg = handle_gh_error(sha_result.stderr)
print(f"Error getting branch SHA: {error_msg}")
sys.exit(1)
sha_result = subprocess.run(get_sha_cmd, capture_output=True, text=True, check=True)
sha = sha_result.stdout.strip()
# Create the tag
@@ -102,20 +58,11 @@ def main():
"-F", f"ref=refs/tags/{version_tag}",
"-F", f"sha={sha}"
]
create_result = subprocess.run(create_tag_cmd, capture_output=True, text=True)
if create_result.returncode != 0:
error_msg = handle_gh_error(create_result.stderr)
print(f"Error creating tag: {error_msg}")
sys.exit(1)
subprocess.run(create_tag_cmd, capture_output=True, text=True, check=True)
print(f"Successfully created and pushed tag '{version_tag}' to {repo}.")
except subprocess.CalledProcessError as e:
error_msg = handle_gh_error(e.stderr.strip() if e.stderr else str(e))
print(f"Error while creating/pushing tag: {error_msg}")
sys.exit(1)
except Exception as e:
print(f"Unexpected error: {e}")
print(f"Error while creating/pushing tag: {e.stderr.strip() if e.stderr else e}")
sys.exit(1)
if __name__ == "__main__":

View File

@@ -231,43 +231,6 @@ def get_next_version(version):
# Next version is always .0
return f"v{major}.{minor + 1}.0"
def get_latest_nightly_tag(github_token):
"""Get the most recent nightly tag from leanprover/lean4-nightly."""
api_url = "https://api.github.com/repos/leanprover/lean4-nightly/tags"
headers = {'Authorization': f'token {github_token}'} if github_token else {}
response = requests.get(api_url, headers=headers)
if response.status_code != 200:
return None
tags = response.json()
if not tags:
return None
# Return the most recent tag name
return tags[0]['name']
def update_lean_toolchain_in_branch(org_repo, branch, toolchain_content, github_token):
"""Update the lean-toolchain file in a specific branch."""
api_url = f"https://api.github.com/repos/{org_repo}/contents/lean-toolchain"
headers = {'Authorization': f'token {github_token}'} if github_token else {}
# First get the current file to get its SHA
response = requests.get(f"{api_url}?ref={branch}", headers=headers)
if response.status_code != 200:
return False
current_file = response.json()
file_sha = current_file['sha']
# Update the file
update_data = {
"message": f"chore: update lean-toolchain to {toolchain_content}",
"content": base64.b64encode(toolchain_content.encode('utf-8')).decode('utf-8'),
"sha": file_sha,
"branch": branch
}
response = requests.put(api_url, json=update_data, headers=headers)
return response.status_code in [200, 201]
def check_bump_branch_toolchain(url, bump_branch, github_token):
"""Check if the lean-toolchain file in bump branch starts with either 'leanprover/lean4:nightly-' or the next version."""
content = get_branch_content(url, bump_branch, "lean-toolchain", github_token)
@@ -299,61 +262,6 @@ def pr_exists_with_title(repo_url, title, github_token):
return pr['number'], pr['html_url']
return None
def check_proofwidgets4_release(repo_url, target_toolchain, github_token):
"""Check if ProofWidgets4 has a release tag that uses the target toolchain."""
api_base = repo_url.replace("https://github.com/", "https://api.github.com/repos/")
headers = {'Authorization': f'token {github_token}'} if github_token else {}
# Get all tags matching v0.0.* pattern
response = requests.get(f"{api_base}/git/matching-refs/tags/v0.0.", headers=headers)
if response.status_code != 200:
print(f" ❌ Could not fetch ProofWidgets4 tags")
return False
tags = response.json()
if not tags:
print(f" ❌ No v0.0.* tags found for ProofWidgets4")
return False
# Extract tag names and sort by version number (descending)
tag_names = []
for tag in tags:
ref = tag['ref']
if ref.startswith('refs/tags/v0.0.'):
tag_name = ref.replace('refs/tags/', '')
try:
# Extract the number after v0.0.
version_num = int(tag_name.split('.')[-1])
tag_names.append((version_num, tag_name))
except (ValueError, IndexError):
continue
if not tag_names:
print(f" ❌ No valid v0.0.* tags found for ProofWidgets4")
return False
# Sort by version number (descending) and take the most recent 10
tag_names.sort(reverse=True)
recent_tags = tag_names[:10]
# Check each recent tag to see if it uses the target toolchain
for version_num, tag_name in recent_tags:
toolchain_content = get_branch_content(repo_url, tag_name, "lean-toolchain", github_token)
if toolchain_content is None:
continue
if is_version_gte(toolchain_content.strip(), target_toolchain):
print(f" ✅ Found release {tag_name} using compatible toolchain (>= {target_toolchain})")
return True
# If we get here, no recent release uses the target toolchain
# Find the highest version number to suggest the next one
highest_version = max(version_num for version_num, _ in recent_tags)
next_version = highest_version + 1
print(f" ❌ No recent ProofWidgets4 release uses toolchain >= {target_toolchain}")
print(f" You will need to create and push a tag v0.0.{next_version}")
return False
def main():
parser = argparse.ArgumentParser(description="Check release status of Lean4 repositories")
parser.add_argument("toolchain", help="The toolchain version to check (e.g., v4.6.0)")
@@ -478,12 +386,6 @@ def main():
continue
print(f" ✅ On compatible toolchain (>= {toolchain})")
# Special handling for ProofWidgets4
if name == "ProofWidgets4":
if not check_proofwidgets4_release(url, toolchain, github_token):
repo_status[name] = False
continue
if check_tag:
tag_exists_initially = tag_exists(url, toolchain, github_token)
if not tag_exists_initially:
@@ -492,7 +394,7 @@ def main():
repo_status[name] = False
continue
else:
print(f" Tag {toolchain} does not exist. Running `script/push_repo_release_tag.py {org_repo} {branch} {toolchain}`...")
print(f" Tag {toolchain} does not exist. Running `script/push_repo_release_tag.py {org_repo} {branch} {toolchain}`...")
# Run the script to create the tag
subprocess.run(["script/push_repo_release_tag.py", org_repo, branch, toolchain])
@@ -515,7 +417,7 @@ def main():
repo_status[name] = False
continue
else:
print(f" Tag {toolchain} is not merged into stable. Running `script/merge_remote.py {org_repo} stable {toolchain}`...")
print(f" Tag {toolchain} is not merged into stable. Running `script/merge_remote.py {org_repo} stable {toolchain}`...")
# Run the script to merge the tag
subprocess.run(["script/merge_remote.py", org_repo, "stable", toolchain])
@@ -532,49 +434,19 @@ def main():
if check_bump:
next_version = get_next_version(toolchain)
bump_branch = f"bump/{next_version}"
# For mathlib4, use the nightly-testing fork for bump branches
bump_org_repo = org_repo
bump_url = url
if name == "mathlib4":
bump_org_repo = "leanprover-community/mathlib4-nightly-testing"
bump_url = "https://github.com/leanprover-community/mathlib4-nightly-testing"
branch_created = False
if not branch_exists(bump_url, bump_branch, github_token):
if not branch_exists(url, bump_branch, github_token):
if args.dry_run:
latest_nightly = get_latest_nightly_tag(github_token)
nightly_note = f" (will set lean-toolchain to {latest_nightly})" if name in ["batteries", "mathlib4"] and latest_nightly else ""
print(f" ❌ Bump branch {bump_branch} does not exist. Run `gh api -X POST /repos/{bump_org_repo}/git/refs -f ref=refs/heads/{bump_branch} -f sha=$(gh api /repos/{org_repo}/git/refs/heads/{branch} --jq .object.sha)` to create it{nightly_note}.")
print(f" ❌ Bump branch {bump_branch} does not exist. Run `gh api -X POST /repos/{org_repo}/git/refs -f ref=refs/heads/{bump_branch} -f sha=$(gh api /repos/{org_repo}/git/refs/heads/{branch} --jq .object.sha)` to create it.")
repo_status[name] = False
continue
print(f" Bump branch {bump_branch} does not exist. Creating it...")
result = run_command(f"gh api -X POST /repos/{bump_org_repo}/git/refs -f ref=refs/heads/{bump_branch} -f sha=$(gh api /repos/{org_repo}/git/refs/heads/{branch} --jq .object.sha)", check=False)
print(f" Bump branch {bump_branch} does not exist. Creating it...")
result = run_command(f"gh api -X POST /repos/{org_repo}/git/refs -f ref=refs/heads/{bump_branch} -f sha=$(gh api /repos/{org_repo}/git/refs/heads/{branch} --jq .object.sha)", check=False)
if result.returncode != 0:
print(f" ❌ Failed to create bump branch {bump_branch}")
repo_status[name] = False
continue
branch_created = True
print(f" ✅ Bump branch {bump_branch} exists")
# 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}"
print(f" ⮕ Updating lean-toolchain to {nightly_toolchain}...")
if update_lean_toolchain_in_branch(bump_org_repo, bump_branch, nightly_toolchain, github_token):
print(f" ✅ Updated lean-toolchain to {nightly_toolchain}")
else:
print(f" ❌ Failed to update lean-toolchain to {nightly_toolchain}")
repo_status[name] = False
continue
else:
print(f" ❌ Could not fetch latest nightly tag")
repo_status[name] = False
continue
if not check_bump_branch_toolchain(bump_url, bump_branch, github_token):
if not check_bump_branch_toolchain(url, bump_branch, github_token):
repo_status[name] = False
continue

View File

@@ -1,11 +1,4 @@
repositories:
- name: lean4-cli
url: https://github.com/leanprover/lean4-cli
toolchain-tag: true
stable-branch: false
branch: main
dependencies: []
- name: batteries
url: https://github.com/leanprover-community/batteries
toolchain-tag: true
@@ -14,13 +7,6 @@ repositories:
bump-branch: true
dependencies: []
- name: verso
url: https://github.com/leanprover/verso
toolchain-tag: true
stable-branch: false
branch: main
dependencies: []
- name: lean4checker
url: https://github.com/leanprover/lean4checker
toolchain-tag: true
@@ -35,21 +21,13 @@ repositories:
branch: master
dependencies: []
- name: plausible
url: https://github.com/leanprover-community/plausible
- name: lean4-cli
url: https://github.com/leanprover/lean4-cli
toolchain-tag: true
stable-branch: false
branch: main
dependencies: []
- name: import-graph
url: https://github.com/leanprover-community/import-graph
toolchain-tag: true
stable-branch: false
branch: main
dependencies:
- lean4-cli
- name: doc-gen4
url: https://github.com/leanprover/doc-gen4
toolchain-tag: true
@@ -57,6 +35,13 @@ repositories:
branch: main
dependencies: [lean4-cli]
- name: verso
url: https://github.com/leanprover/verso
toolchain-tag: true
stable-branch: false
branch: main
dependencies: []
- name: reference-manual
url: https://github.com/leanprover/reference-manual
toolchain-tag: true
@@ -80,6 +65,22 @@ repositories:
dependencies:
- batteries
- name: import-graph
url: https://github.com/leanprover-community/import-graph
toolchain-tag: true
stable-branch: false
branch: main
dependencies:
- lean4-cli
- batteries
- name: plausible
url: https://github.com/leanprover-community/plausible
toolchain-tag: true
stable-branch: false
branch: main
dependencies: []
- name: mathlib4
url: https://github.com/leanprover-community/mathlib4
toolchain-tag: true
@@ -96,15 +97,6 @@ repositories:
- import-graph
- plausible
- name: cslib
url: https://github.com/leanprover/cslib
toolchain-tag: true
stable-branch: true
branch: main
bump-branch: true
dependencies:
- mathlib4
- name: repl
url: https://github.com/leanprover-community/repl
toolchain-tag: true

View File

@@ -1,10 +1,10 @@
#!/usr/bin/env python3
"""
Execute release steps for Lean4 repositories.
Generate release steps script for Lean4 repositories.
This script helps automate the release process for Lean4 and its dependent repositories
by actually executing the step-by-step instructions for updating toolchains, creating tags,
by generating step-by-step instructions for updating toolchains, creating tags,
and managing branches.
Usage:
@@ -12,11 +12,11 @@ Usage:
Arguments:
version: The version to set in the lean-toolchain file (e.g., v4.6.0)
repo: The repository name as specified in release_repos.yml
repo: A substring of the repository name as specified in release_repos.yml
Example:
python3 release_steps.py v4.6.0 mathlib4
python3 release_steps.py v4.6.0 batteries
python3 release_steps.py v4.6.0 mathlib
python3 release_steps.py v4.6.0 batt
The script reads repository configurations from release_repos.yml in the same directory.
Each repository may have specific requirements for:
@@ -32,124 +32,23 @@ import yaml
import os
import sys
import re
import subprocess
import shutil
import json
from pathlib import Path
# Color functions for terminal output
def blue(text):
"""Blue text for 'I'm doing something' messages."""
return f"\033[94m{text}\033[0m"
def green(text):
"""Green text for 'successful step' messages."""
return f"\033[92m{text}\033[0m"
def red(text):
"""Red text for 'this looks bad' messages."""
return f"\033[91m{text}\033[0m"
def yellow(text):
"""Yellow text for warnings."""
return f"\033[93m{text}\033[0m"
def run_command(cmd, cwd=None, check=True, stream_output=False):
"""Run a shell command and return the result."""
print(blue(f"Running: {cmd}"))
try:
if stream_output:
# Stream output in real-time for long-running commands
result = subprocess.run(cmd, shell=True, cwd=cwd, check=check, text=True)
return result
else:
# Capture output for commands where we need to process the result
result = subprocess.run(cmd, shell=True, cwd=cwd, check=check,
capture_output=True, text=True)
if result.stdout:
# Command output in plain white (default terminal color)
print(result.stdout)
return result
except subprocess.CalledProcessError as e:
print(red(f"Error running command: {cmd}"))
print(red(f"Exit code: {e.returncode}"))
if not stream_output:
print(f"Stdout: {e.stdout}")
print(f"Stderr: {e.stderr}")
raise
def load_repos_config(file_path):
with open(file_path, "r") as f:
return yaml.safe_load(f)["repositories"]
def find_repo(repo_name, config):
matching_repos = [r for r in config if r["name"] == repo_name]
def find_repo(repo_substring, config):
pattern = re.compile(re.escape(repo_substring), re.IGNORECASE)
matching_repos = [r for r in config if pattern.search(r["name"])]
if not matching_repos:
print(red(f"Error: No repository named '{repo_name}' found in configuration."))
available_repos = [r["name"] for r in config]
print(yellow(f"Available repositories: {', '.join(available_repos)}"))
print(f"Error: No repository matching '{repo_substring}' found in configuration.")
sys.exit(1)
if len(matching_repos) > 1:
print(f"Error: Multiple repositories matching '{repo_substring}' found in configuration: {', '.join(r['name'] for r in matching_repos)}")
sys.exit(1)
return matching_repos[0]
def setup_downstream_releases_dir():
"""Create the downstream_releases directory if it doesn't exist."""
downstream_dir = Path("downstream_releases")
if not downstream_dir.exists():
print(blue(f"Creating {downstream_dir} directory..."))
downstream_dir.mkdir()
print(green(f"Created {downstream_dir} directory"))
return downstream_dir
def clone_or_update_repo(repo_url, repo_dir, downstream_dir):
"""Clone the repository if it doesn't exist, or update it if it does."""
repo_path = downstream_dir / repo_dir
if repo_path.exists():
print(blue(f"Repository {repo_dir} already exists, updating..."))
run_command("git fetch", cwd=repo_path)
print(green(f"Updated repository {repo_dir}"))
else:
print(blue(f"Cloning {repo_url} to {repo_path}..."))
run_command(f"git clone {repo_url}", cwd=downstream_dir)
print(green(f"Cloned repository {repo_dir}"))
return repo_path
def get_remotes_for_repo(repo_name):
"""Get the appropriate remotes for bump and nightly-testing branches based on repository."""
if repo_name == "mathlib4":
return "nightly-testing", "nightly-testing"
else:
return "origin", "origin"
def check_and_abort_merge(repo_path):
"""Check if repository is in the middle of a merge and abort it if so."""
merge_head_file = repo_path / ".git" / "MERGE_HEAD"
if merge_head_file.exists():
print(yellow(f"Repository {repo_path.name} is in the middle of a merge. Aborting merge..."))
run_command("git merge --abort", cwd=repo_path)
print(green("Merge aborted successfully"))
return True
# Also check git status for other merge-related states
try:
result = run_command("git status --porcelain=v1", cwd=repo_path, check=False)
if result.returncode == 0:
# Check for unmerged paths (indicated by 'UU', 'AA', etc. in git status)
for line in result.stdout.splitlines():
if len(line) >= 2 and line[:2] in ['UU', 'AA', 'DD', 'AU', 'UA', 'DU', 'UD']:
print(yellow(f"Repository {repo_path.name} has unmerged paths. Aborting merge..."))
run_command("git merge --abort", cwd=repo_path)
print(green("Merge aborted successfully"))
return True
except subprocess.CalledProcessError:
# If git status fails, we'll let the main process handle it
pass
return False
def execute_release_steps(repo, version, config):
def generate_script(repo, version, config):
repo_config = find_repo(repo, config)
repo_name = repo_config['name']
repo_url = repo_config['url']
@@ -160,496 +59,92 @@ def execute_release_steps(repo, version, config):
requires_tagging = repo_config.get("toolchain-tag", True)
has_stable_branch = repo_config.get("stable-branch", True)
# Setup downstream releases directory
downstream_dir = setup_downstream_releases_dir()
# Clone or update the repository
repo_path = clone_or_update_repo(repo_url, repo_dir, downstream_dir)
# Special remote setup for mathlib4
if repo_name == "mathlib4":
print(blue("Setting up special remotes for mathlib4..."))
try:
# Check if nightly-testing remote already exists
result = run_command("git remote get-url nightly-testing", cwd=repo_path, check=False)
if result.returncode != 0:
# Add the nightly-testing remote
run_command("git remote add nightly-testing https://github.com/leanprover-community/mathlib4-nightly-testing.git", cwd=repo_path)
print(green("Added nightly-testing remote"))
else:
print(green("nightly-testing remote already exists"))
# Fetch from the nightly-testing remote
run_command("git fetch nightly-testing", cwd=repo_path)
print(green("Fetched from nightly-testing remote"))
except subprocess.CalledProcessError as e:
print(red(f"Error setting up mathlib4 remotes: {e}"))
print(yellow("Continuing with default remote setup..."))
print(blue(f"\n=== Executing release steps for {repo_name} ==="))
# Check if repository is in the middle of a merge and abort it if necessary
check_and_abort_merge(repo_path)
# Execute the release steps
run_command(f"git checkout {default_branch} && git pull", cwd=repo_path)
# Special rc1 safety check for batteries and mathlib4 (before creating any branches)
if repo_name in ["batteries", "mathlib4"] and version.endswith('-rc1'):
print(blue("This repo has nightly-testing infrastructure"))
print(blue(f"Checking if nightly-testing can be safely merged into bump/{version.split('-rc')[0]}..."))
# Get the base version (e.g., v4.6.0 from v4.6.0-rc1)
base_version = version.split('-rc')[0]
bump_branch = f"bump/{base_version}"
# Determine which remote to use for bump and nightly-testing branches
bump_remote, nightly_remote = get_remotes_for_repo(repo_name)
try:
# Fetch latest changes from the appropriate remote
run_command(f"git fetch {bump_remote}", cwd=repo_path)
# Check if the bump branch exists
result = run_command(f"git show-ref --verify --quiet refs/remotes/{bump_remote}/{bump_branch}", cwd=repo_path, check=False)
if result.returncode != 0:
print(red(f"Bump branch {bump_remote}/{bump_branch} does not exist. Cannot perform safety check."))
print(yellow("Please ensure the bump branch exists before proceeding."))
return
# Create a temporary branch for testing the merge
temp_branch = f"temp-merge-test-{base_version}"
# Clean up any existing temp branch from previous runs
result = run_command(f"git show-ref --verify --quiet refs/heads/{temp_branch}", cwd=repo_path, check=False)
if result.returncode == 0:
print(blue(f"Cleaning up existing temp branch {temp_branch}..."))
# Make sure we're not on the temp branch before deleting it
run_command(f"git checkout {default_branch}", cwd=repo_path)
run_command(f"git branch -D {temp_branch}", cwd=repo_path)
print(green(f"Deleted existing temp branch {temp_branch}"))
run_command(f"git checkout -b {temp_branch} {bump_remote}/{bump_branch}", cwd=repo_path)
# Try to merge nightly-testing
try:
run_command(f"git merge {nightly_remote}/nightly-testing", cwd=repo_path)
# Check what files have changed compared to the bump branch
changed_files = run_command(f"git diff --name-only {bump_remote}/{bump_branch}..HEAD", cwd=repo_path)
# Filter out allowed changes
allowed_patterns = ['lean-toolchain', 'lake-manifest.json']
problematic_files = []
for file in changed_files.stdout.strip().split('\n'):
if file.strip(): # Skip empty lines
is_allowed = any(pattern in file for pattern in allowed_patterns)
if not is_allowed:
problematic_files.append(file)
# Clean up temporary branch and return to default branch
run_command(f"git checkout {default_branch}", cwd=repo_path)
run_command(f"git branch -D {temp_branch}", cwd=repo_path)
if problematic_files:
print(red("❌ Safety check failed!"))
print(red(f"Merging nightly-testing into {bump_branch} would result in changes to:"))
for file in problematic_files:
print(red(f" - {file}"))
print(yellow("\nYou need to make a PR merging the changes from nightly-testing into the bump branch first."))
print(yellow(f"Create a PR from nightly-testing targeting {bump_branch} to resolve these changes."))
return
else:
print(green("✅ Safety check passed - only lean-toolchain and/or lake-manifest.json would change"))
except subprocess.CalledProcessError:
# Merge failed due to conflicts - check which files are conflicted
print(blue("Merge failed, checking which files are affected..."))
# Get all changed files using git status
status_result = run_command("git status --porcelain", cwd=repo_path)
changed_files = []
for line in status_result.stdout.splitlines():
if line.strip(): # Skip empty lines
# Extract filename (skip the first 3 characters which are status codes)
changed_files.append(line[3:])
# Filter out allowed files
allowed_patterns = ['lean-toolchain', 'lake-manifest.json']
problematic_files = []
for file in changed_files:
is_allowed = any(pattern in file for pattern in allowed_patterns)
if not is_allowed:
problematic_files.append(file)
if problematic_files:
# There are changes in non-allowed files - fail the safety check
# First abort the merge to clean up the conflicted state
run_command("git merge --abort", cwd=repo_path)
run_command(f"git checkout {default_branch}", cwd=repo_path)
run_command(f"git branch -D {temp_branch}", cwd=repo_path)
print(red("❌ Safety check failed!"))
print(red(f"Merging nightly-testing into {bump_branch} would result in changes to:"))
for file in problematic_files:
print(red(f" - {file}"))
print(yellow("\nYou need to make a PR merging the changes from nightly-testing into the bump branch first."))
print(yellow(f"Create a PR from nightly-testing targeting {bump_branch} to resolve these changes."))
return
else:
# Only allowed files are changed - resolve them and continue
print(green(f"✅ Only allowed files changed: {', '.join(changed_files)}"))
print(blue("Resolving conflicts by taking nightly-testing version..."))
# For each changed allowed file, take the nightly-testing version
for file in changed_files:
run_command(f"git checkout --theirs {file}", cwd=repo_path)
# Complete the merge
run_command("git add .", cwd=repo_path)
run_command("git commit --no-edit", cwd=repo_path)
print(green("✅ Safety check passed - changes only in allowed files"))
# Clean up temporary branch and return to default branch
run_command(f"git checkout {default_branch}", cwd=repo_path)
run_command(f"git branch -D {temp_branch}", cwd=repo_path)
except subprocess.CalledProcessError as e:
# Ensure we're back on the default branch even if setup failed
try:
run_command(f"git checkout {default_branch}", cwd=repo_path)
except subprocess.CalledProcessError:
print(red(f"Cannot return to {default_branch} branch. Repository is in an inconsistent state."))
print(red("Please manually check the repository state and fix any issues."))
return
print(red(f"Error during safety check: {e}"))
print(yellow("Skipping safety check and proceeding with normal merge..."))
# Check if the branch already exists
branch_name = f"bump_to_{version}"
try:
# Check if branch exists locally
result = run_command(f"git show-ref --verify --quiet refs/heads/{branch_name}", cwd=repo_path, check=False)
if result.returncode == 0:
print(blue(f"Branch {branch_name} already exists, checking it out..."))
run_command(f"git checkout {branch_name}", cwd=repo_path)
print(green(f"Checked out existing branch {branch_name}"))
else:
print(blue(f"Creating new branch {branch_name}..."))
run_command(f"git checkout -b {branch_name}", cwd=repo_path)
print(green(f"Created new branch {branch_name}"))
except subprocess.CalledProcessError:
print(blue(f"Creating new branch {branch_name}..."))
run_command(f"git checkout -b {branch_name}", cwd=repo_path)
print(green(f"Created new branch {branch_name}"))
# Update lean-toolchain
print(blue("Updating lean-toolchain file..."))
toolchain_file = repo_path / "lean-toolchain"
with open(toolchain_file, "w") as f:
f.write(f"leanprover/lean4:{version}\n")
print(green(f"Updated lean-toolchain to leanprover/lean4:{version}"))
script_lines = [
f"cd {repo_dir}",
"git fetch",
f"git checkout {default_branch} && git pull",
f"git checkout -b bump_to_{version}",
f"echo leanprover/lean4:{version} > lean-toolchain",
]
# Special cases for specific repositories
if repo_name == "repl":
run_command("lake update", cwd=repo_path, stream_output=True)
mathlib_test_dir = repo_path / "test" / "Mathlib"
run_command(f'perl -pi -e \'s/rev = "v\\d+\\.\\d+\\.\\d+(-rc\\d+)?"/rev = "{version}"/g\' lakefile.toml', cwd=mathlib_test_dir)
# Update lean-toolchain in test/Mathlib
print(blue("Updating test/Mathlib/lean-toolchain..."))
mathlib_toolchain = mathlib_test_dir / "lean-toolchain"
with open(mathlib_toolchain, "w") as f:
f.write(f"leanprover/lean4:{version}\n")
print(green(f"Updated test/Mathlib/lean-toolchain to leanprover/lean4:{version}"))
run_command("lake update", cwd=mathlib_test_dir, stream_output=True)
try:
result = run_command("./test.sh", cwd=repo_path, stream_output=True, check=False)
if result.returncode == 0:
print(green("Tests completed successfully"))
else:
print(red("Tests failed, but continuing with PR creation..."))
print(red(f"Test exit code: {result.returncode}"))
except subprocess.CalledProcessError as e:
print(red("Tests failed, but continuing with PR creation..."))
print(red(f"Test error: {e}"))
elif repo_name == "cslib":
print(blue("Updating lakefile.toml..."))
run_command(f'perl -pi -e \'s/"v4\\.[0-9]+(\\.[0-9]+)?(-rc[0-9]+)?"/"' + version + '"/g\' lakefile.*', cwd=repo_path)
print(blue("Updating docs/lakefile.toml..."))
run_command(f'perl -pi -e \'s/"v4\\.[0-9]+(\\.[0-9]+)?(-rc[0-9]+)?"/"' + version + '"/g\' lakefile.*', cwd=repo_path / "docs")
# Update lean-toolchain in docs
print(blue("Updating docs/lean-toolchain..."))
docs_toolchain = repo_path / "docs" / "lean-toolchain"
with open(docs_toolchain, "w") as f:
f.write(f"leanprover/lean4:{version}\n")
print(green(f"Updated docs/lean-toolchain to leanprover/lean4:{version}"))
run_command("lake update", cwd=repo_path, stream_output=True)
script_lines.extend([
"lake update",
"cd test/Mathlib",
f"perl -pi -e 's/rev = \"v\\d+\\.\\d+\\.\\d+(-rc\\d+)?\"/rev = \"{version}\"/g' lakefile.toml",
f"echo leanprover/lean4:{version} > lean-toolchain",
"lake update",
"cd ../..",
"./test.sh"
])
elif dependencies:
run_command(f'perl -pi -e \'s/"v4\\.[0-9]+(\\.[0-9]+)?(-rc[0-9]+)?"/"' + version + '"/g\' lakefile.*', cwd=repo_path)
run_command("lake update", cwd=repo_path, stream_output=True)
script_lines.append('perl -pi -e \'s/"v4\\.[0-9]+(\\.[0-9]+)?(-rc[0-9]+)?"/"' + version + '"/g\' lakefile.*')
script_lines.append("lake update")
# Commit changes (only if there are changes)
print(blue("Checking for changes to commit..."))
try:
# Check if there are any changes to commit (staged or unstaged)
result = run_command("git status --porcelain", cwd=repo_path, check=False)
if result.stdout.strip(): # There are changes
print(blue("Committing changes..."))
run_command(f'git commit -am "chore: bump toolchain to {version}"', cwd=repo_path)
print(green(f"Committed changes: chore: bump toolchain to {version}"))
else:
print(green("No changes to commit - toolchain already up to date"))
except subprocess.CalledProcessError:
print(yellow("Failed to check for changes, attempting commit anyway..."))
try:
run_command(f'git commit -am "chore: bump toolchain to {version}"', cwd=repo_path)
except subprocess.CalledProcessError as e:
if "nothing to commit" in e.stderr:
print(green("No changes to commit - toolchain already up to date"))
else:
raise
script_lines.append("")
# Handle special merging cases
if version.endswith('-rc1') and repo_name in ["batteries", "mathlib4"]:
print(blue("This repo uses `bump/v4.X.0` branches for reviewed content from nightly-testing."))
# Determine which remote to use for bump branches
bump_remote, nightly_remote = get_remotes_for_repo(repo_name)
# Fetch latest changes to ensure we have the most up-to-date bump branch
print(blue(f"Fetching latest changes from {bump_remote}..."))
run_command(f"git fetch {bump_remote}", cwd=repo_path)
try:
print(blue(f"Merging {bump_remote}/bump/{version.split('-rc')[0]}..."))
run_command(f"git merge {bump_remote}/bump/{version.split('-rc')[0]}", cwd=repo_path)
print(green("Merge completed successfully"))
except subprocess.CalledProcessError:
# Merge failed due to conflicts - check which files are conflicted
print(blue("Merge conflicts detected, checking which files are affected..."))
# Get conflicted files using git status
status_result = run_command("git status --porcelain", cwd=repo_path)
conflicted_files = []
for line in status_result.stdout.splitlines():
if len(line) >= 2 and line[:2] in ['UU', 'AA', 'DD', 'AU', 'UA', 'DU', 'UD']:
# Extract filename (skip the first 3 characters which are status codes)
conflicted_files.append(line[3:])
# Filter out allowed files
allowed_patterns = ['lean-toolchain', 'lake-manifest.json']
problematic_files = []
for file in conflicted_files:
is_allowed = any(pattern in file for pattern in allowed_patterns)
if not is_allowed:
problematic_files.append(file)
if problematic_files:
# There are conflicts in non-allowed files - fail
print(red("❌ Merge failed!"))
print(red(f"Merging {bump_remote}/bump/{version.split('-rc')[0]} resulted in conflicts in:"))
for file in problematic_files:
print(red(f" - {file}"))
print(red("Please resolve these conflicts manually."))
return
else:
# Only allowed files are conflicted - resolve them automatically
print(green(f"✅ Only allowed files conflicted: {', '.join(conflicted_files)}"))
print(blue("Resolving conflicts automatically..."))
# Overwrite lean-toolchain with our target version
if 'lean-toolchain' in conflicted_files:
print(blue(f"Overwriting lean-toolchain with target version {version}"))
toolchain_file = repo_path / "lean-toolchain"
with open(toolchain_file, "w") as f:
f.write(f"leanprover/lean4:{version}\n")
# For other allowed files, take our version (since we want our changes)
for file in conflicted_files:
if file != 'lean-toolchain':
run_command(f"git checkout --ours {file}", cwd=repo_path)
# Run lake update to rebuild lake-manifest.json
print(blue("Running lake update to rebuild lake-manifest.json..."))
run_command("lake update", cwd=repo_path, stream_output=True)
# Complete the merge
run_command("git add .", cwd=repo_path)
run_command("git commit --no-edit", cwd=repo_path)
print(green("✅ Merge completed successfully with automatic conflict resolution"))
elif version.endswith('-rc1'):
# For all other repos with rc versions, merge nightly-testing
if repo_name in ["verso", "reference-manual"]:
print(yellow("This repo does development on nightly-testing: remember to rebase merge the PR."))
# Fetch latest changes to ensure we have the most up-to-date nightly-testing branch
print(blue("Fetching latest changes from origin..."))
run_command("git fetch origin", cwd=repo_path)
try:
print(blue("Merging origin/nightly-testing..."))
run_command("git merge origin/nightly-testing", cwd=repo_path)
print(green("Merge completed successfully"))
except subprocess.CalledProcessError:
# Merge failed due to conflicts - check which files are conflicted
print(blue("Merge conflicts detected, checking which files are affected..."))
# Get conflicted files using git status
status_result = run_command("git status --porcelain", cwd=repo_path)
conflicted_files = []
for line in status_result.stdout.splitlines():
if len(line) >= 2 and line[:2] in ['UU', 'AA', 'DD', 'AU', 'UA', 'DU', 'UD']:
# Extract filename (skip the first 3 characters which are status codes)
conflicted_files.append(line[3:])
# Filter out allowed files
allowed_patterns = ['lean-toolchain', 'lake-manifest.json']
problematic_files = []
for file in conflicted_files:
is_allowed = any(pattern in file for pattern in allowed_patterns)
if not is_allowed:
problematic_files.append(file)
if problematic_files:
# There are conflicts in non-allowed files - fail
print(red("❌ Merge failed!"))
print(red(f"Merging nightly-testing resulted in conflicts in:"))
for file in problematic_files:
print(red(f" - {file}"))
print(red("Please resolve these conflicts manually."))
return
else:
# Only allowed files are conflicted - resolve them automatically
print(green(f"✅ Only allowed files conflicted: {', '.join(conflicted_files)}"))
print(blue("Resolving conflicts automatically..."))
# For lean-toolchain and lake-manifest.json, keep our versions
for file in conflicted_files:
print(blue(f"Keeping our version of {file}"))
run_command(f"git checkout --ours {file}", cwd=repo_path)
# Complete the merge
run_command("git add .", cwd=repo_path)
run_command("git commit --no-edit", cwd=repo_path)
print(green("✅ Merge completed successfully with automatic conflict resolution"))
script_lines.extend([
f'git commit -am "chore: bump toolchain to {version}"',
""
])
# Build and test (skip for Mathlib)
if repo_name not in ["mathlib4"]:
print(blue("Building project..."))
# Clean lake cache for a fresh build
print(blue("Cleaning lake cache..."))
run_command("rm -rf .lake", cwd=repo_path)
try:
run_command("lake build", cwd=repo_path, stream_output=True)
print(green("Build completed successfully"))
except subprocess.CalledProcessError as e:
print(red("Build failed, but continuing with PR creation..."))
print(red(f"Build error: {e}"))
# Check if lake check-test exists before running tests
print(blue("Running tests..."))
check_test_result = run_command("lake check-test", cwd=repo_path, check=False)
if check_test_result.returncode == 0:
try:
run_command("lake test", cwd=repo_path, stream_output=True)
print(green("Tests completed successfully"))
except subprocess.CalledProcessError as e:
print(red("Tests failed, but continuing with PR creation..."))
print(red(f"Test error: {e}"))
else:
print(yellow("lake check-test reports that there is no test suite"))
if re.search(r'rc\d+$', version) and repo_name in ["batteries", "mathlib4"]:
script_lines.extend([
"echo 'This repo has nightly-testing infrastructure'",
f"git merge origin/bump/{version.split('-rc')[0]}",
"echo 'Please resolve any conflicts.'",
"grep nightly-testing lakefile.* && echo 'Please ensure the lakefile does not include nightly-testing versions.'",
""
])
if re.search(r'rc\d+$', version) and repo_name in ["verso", "reference-manual"]:
script_lines.extend([
"echo 'This repo does development on nightly-testing: remember to rebase merge the PR.'",
f"git merge origin/nightly-testing",
"echo 'Please resolve any conflicts.'",
""
])
if repo_name != "Mathlib":
script_lines.extend([
"lake build && if lake check-test; then lake test; fi",
""
])
# Push the branch to remote before creating PR
print(blue("Checking remote branch status..."))
try:
# Check if branch exists on remote
result = run_command(f"git ls-remote --heads origin {branch_name}", cwd=repo_path, check=False)
if not result.stdout.strip():
print(blue(f"Pushing branch {branch_name} to remote..."))
run_command(f"git push -u origin {branch_name}", cwd=repo_path)
print(green(f"Successfully pushed branch {branch_name} to remote"))
else:
print(blue(f"Branch {branch_name} already exists on remote, pushing any new commits..."))
run_command(f"git push", cwd=repo_path)
print(green("Successfully pushed commits to remote"))
except subprocess.CalledProcessError:
print(red("Failed to push branch to remote. Please check your permissions and network connection."))
print(yellow(f"You may need to run: git push -u origin {branch_name}"))
return
script_lines.extend([
'gh pr create --title "chore: bump toolchain to ' + version + '" --body ""',
"echo 'Please review the PR and merge or rebase it.'",
""
])
# Create pull request (only if one doesn't already exist)
print(blue("Checking for existing pull request..."))
try:
# Check if PR already exists for this branch
result = run_command(f'gh pr list --head {branch_name} --json number', cwd=repo_path, check=False)
if result.returncode == 0 and result.stdout.strip() != "[]":
print(green(f"Pull request already exists for branch {branch_name}"))
# Get the PR URL
pr_result = run_command(f'gh pr view {branch_name} --json url', cwd=repo_path, check=False)
if pr_result.returncode == 0:
pr_data = json.loads(pr_result.stdout)
print(green(f"PR URL: {pr_data.get('url', 'N/A')}"))
else:
# Create new PR
print(blue("Creating new pull request..."))
run_command(f'gh pr create --title "chore: bump toolchain to {version}" --body ""', cwd=repo_path)
print(green("Pull request created successfully!"))
except subprocess.CalledProcessError:
print(red("Failed to check for existing PR or create new PR."))
print(yellow("This could be due to:"))
print(yellow("1. GitHub CLI not authenticated"))
print(yellow("2. No push permissions to the repository"))
print(yellow("3. Network issues"))
print(f"Branch: {branch_name}")
print(f"Title: chore: bump toolchain to {version}")
print(yellow("Please create the PR manually if needed."))
return "\n".join(script_lines)
def main():
parser = argparse.ArgumentParser(
description="Execute release steps for Lean4 repositories.",
description="Generate release steps script for Lean4 repositories.",
formatter_class=argparse.RawDescriptionHelpFormatter,
epilog="""
Examples:
%(prog)s v4.6.0 mathlib4 Execute steps for updating Mathlib to v4.6.0
%(prog)s v4.6.0 batteries Execute steps for updating Batteries to v4.6.0
%(prog)s v4.6.0 mathlib Generate steps for updating Mathlib to v4.6.0
%(prog)s v4.6.0 batt Generate steps for updating Batteries to v4.6.0
The script will:
1. Create a downstream_releases/ directory
2. Clone or update the target repository
3. Update the lean-toolchain file
4. Create appropriate branches and commits
5. Build and test the project
6. Create pull requests
The script will generate shell commands to:
1. Update the lean-toolchain file
2. Create appropriate branches and commits
3. Create pull requests
(Note that the steps of creating toolchain version tags, and merging these into `stable` branches,
are handled by `script/release_checklist.py`.)
"""
)
parser.add_argument("version", help="The version to set in the lean-toolchain file (e.g., v4.6.0)")
parser.add_argument("repo", help="The repository name as specified in release_repos.yml")
parser.add_argument("repo", help="A substring of the repository name as specified in release_repos.yml")
args = parser.parse_args()
config_path = os.path.join(os.path.dirname(__file__), "release_repos.yml")
config = load_repos_config(config_path)
execute_release_steps(args.repo, args.version, config)
script = generate_script(args.repo, args.version, config)
print(script)
if __name__ == "__main__":
main()

View File

@@ -10,7 +10,7 @@ endif()
include(ExternalProject)
project(LEAN CXX C)
set(LEAN_VERSION_MAJOR 4)
set(LEAN_VERSION_MINOR 25)
set(LEAN_VERSION_MINOR 22)
set(LEAN_VERSION_PATCH 0)
set(LEAN_VERSION_IS_RELEASE 0) # This number is 1 in the release revision, and 0 otherwise.
set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")
@@ -81,7 +81,7 @@ option(USE_MIMALLOC "use mimalloc" ON)
# development-specific options
option(CHECK_OLEAN_VERSION "Only load .olean files compiled with the current version of Lean" OFF)
option(USE_LAKE "Use Lake instead of lean.mk for building core libs from language server" ON)
option(USE_LAKE "Use Lake instead of lean.mk for building core libs from language server" OFF)
set(LEAN_EXTRA_MAKE_OPTS "" CACHE STRING "extra options to lean --make")
set(LEANC_CC ${CMAKE_C_COMPILER} CACHE STRING "C compiler to use in `leanc`")
@@ -469,7 +469,6 @@ elseif(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
string(APPEND CMAKE_CXX_FLAGS " -ftls-model=initial-exec")
string(APPEND INIT_SHARED_LINKER_FLAGS " -install_name @rpath/libInit_shared.dylib")
string(APPEND LEANSHARED_1_LINKER_FLAGS " -install_name @rpath/libleanshared_1.dylib")
string(APPEND LEANSHARED_2_LINKER_FLAGS " -install_name @rpath/libleanshared_2.dylib")
string(APPEND LEANSHARED_LINKER_FLAGS " -install_name @rpath/libleanshared.dylib")
string(APPEND LAKESHARED_LINKER_FLAGS " -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -install_name @rpath/libLake_shared.dylib")
string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath,@executable_path/../lib -Wl,-rpath,@executable_path/../lib/lean")
@@ -503,7 +502,7 @@ endif()
# are already loaded) and probably fail unless we set up LD_LIBRARY_PATH.
if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
# import libraries created by the stdlib.make targets
string(APPEND LEANC_SHARED_LINKER_FLAGS " -lInit_shared -lleanshared_2 -lleanshared_1 -lleanshared")
string(APPEND LEANC_SHARED_LINKER_FLAGS " -lInit_shared -lleanshared_1 -lleanshared")
elseif("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin")
# The second flag is necessary to even *load* dylibs without resolved symbols, as can happen
# if a Lake `extern_lib` depends on a symbols defined by the Lean library but is loaded even
@@ -534,21 +533,12 @@ else()
OUTPUT_VARIABLE GIT_SHA1
OUTPUT_STRIP_TRAILING_WHITESPACE)
message(STATUS "stage0 sha1: ${GIT_SHA1}")
# Now that we've prepared the information for the next stage, we can forget that we will use
# Lake in the future as we won't use it in this stage
set(USE_LAKE OFF)
else()
set(GIT_SHA1 "")
endif()
endif()
configure_file("${LEAN_SOURCE_DIR}/githash.h.in" "${LEAN_BINARY_DIR}/githash.h")
if(USE_LAKE AND ${STAGE} EQUAL 0)
# Now that we've prepared the information for the next stage, we can forget that we will use
# Lake in the future as we won't use it in this stage
set(USE_LAKE OFF)
endif()
# Windows uses ";" as a path separator. We use `LEAN_PATH_SEPARATOR` on scripts such as lean.mk.in
if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
set(LEAN_PATH_SEPARATOR ";")
@@ -590,7 +580,7 @@ endif()
add_subdirectory(initialize)
add_subdirectory(shell)
# to be included in `leanshared` but not the smaller `leanshared_*` (as it would pull
# to be included in `leanshared` but not the smaller `leanshared_1` (as it would pull
# in the world)
add_library(leaninitialize STATIC $<TARGET_OBJECTS:initialize>)
set_target_properties(leaninitialize PROPERTIES
@@ -644,6 +634,8 @@ else()
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:library>)
add_subdirectory(library/constructions)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:constructions>)
add_subdirectory(library/compiler)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:compiler>)
# leancpp without `initialize` (see `leaninitialize` above)
add_library(leancpp_1 STATIC ${LEAN_OBJS})
@@ -685,17 +677,12 @@ if (LLVM AND ${STAGE} GREATER 0)
set(EXTRA_LEANMAKE_OPTS "LLVM=1")
endif()
set(STDLIBS Init Std Lean Leanc)
if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
list(APPEND STDLIBS Lake)
endif()
add_custom_target(make_stdlib ALL
WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
# The actual rule is in a separate makefile because we want to prefix it with '+' to use the Make job server
# for a parallelized nested build, but CMake doesn't let us do that.
# We use `lean` from the previous stage, but `leanc`, headers, etc. from the current stage
COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make ${STDLIBS}
COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Init Std Lean Leanc
VERBATIM)
# if we have LLVM enabled, then build `lean.h.bc` which has the LLVM bitcode
@@ -715,7 +702,6 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
)
add_custom_target(leanshared ALL
DEPENDS Init_shared leancpp
COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_2${CMAKE_SHARED_LIBRARY_SUFFIX}
COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_1${CMAKE_SHARED_LIBRARY_SUFFIX}
COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}
)
@@ -736,13 +722,18 @@ else()
COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make leanshared
VERBATIM)
string(APPEND CMAKE_EXE_LINKER_FLAGS " -lInit_shared -lleanshared_2 -lleanshared_1 -lleanshared")
string(APPEND CMAKE_EXE_LINKER_FLAGS " -lInit_shared -lleanshared_1 -lleanshared")
endif()
if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
add_custom_target(lake_shared
add_custom_target(lake_lib
WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
DEPENDS leanshared
COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Lake
VERBATIM)
add_custom_target(lake_shared
WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
DEPENDS lake_lib
COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make libLake_shared
VERBATIM)
add_custom_target(lake ALL
@@ -823,12 +814,6 @@ if(LEAN_INSTALL_PREFIX)
set(CMAKE_INSTALL_PREFIX "${LEAN_INSTALL_PREFIX}/lean-${LEAN_VERSION_STRING}${LEAN_INSTALL_SUFFIX}")
endif()
if (STAGE GREATER 1)
# The build of stage2+ may depend on local changes made to src/ that are not reflected by the
# commit hash in stage1/bin/lean, so we make sure to disable the global cache
string(APPEND LEAN_EXTRA_LAKEFILE_TOML "\n\nenableArtifactCache = false")
endif()
# Escape for `make`. Yes, twice.
string(REPLACE "$" "\\\$$" CMAKE_EXE_LINKER_FLAGS_MAKE "${CMAKE_EXE_LINKER_FLAGS}")
configure_file(${LEAN_SOURCE_DIR}/stdlib.make.in ${CMAKE_BINARY_DIR}/stdlib.make)
@@ -855,10 +840,6 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
set(LAKE_LIB_PREFIX "lib")
endif()
if(USE_LAKE)
configure_file(${LEAN_SOURCE_DIR}/lakefile.toml.in ${CMAKE_BINARY_DIR}/lakefile.toml)
# copy for editing
if(STAGE EQUAL 1)
configure_file(${LEAN_SOURCE_DIR}/lakefile.toml.in ${LEAN_SOURCE_DIR}/lakefile.toml)
endif()
if(USE_LAKE AND STAGE EQUAL 1)
configure_file(${LEAN_SOURCE_DIR}/lakefile.toml.in ${LEAN_SOURCE_DIR}/lakefile.toml)
endif()

View File

@@ -6,44 +6,41 @@ Authors: Leonardo de Moura
module
prelude
public import Init.Prelude
public import Init.Notation
public import Init.Tactics
public import Init.TacticsExtra
public import Init.ByCases
public import Init.RCases
public import Init.Core
public import Init.Control
public import Init.Data.Basic
public import Init.WF
public import Init.WFTactics
public import Init.Data
public import Init.System
public import Init.Util
public import Init.Dynamic
public import Init.ShareCommon
public import Init.MetaTypes
public import Init.Meta
public import Init.NotationExtra
public import Init.SimpLemmas
public import Init.PropLemmas
public import Init.Hints
public import Init.Conv
public import Init.Guard
public import Init.Simproc
public import Init.SizeOfLemmas
public import Init.BinderPredicates
public import Init.Ext
public import Init.Omega
public import Init.MacroTrace
public import Init.Grind
public import Init.GrindInstances
public import Init.While
public import Init.Syntax
public import Init.Internal
public import Init.Try
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
public import Init.LawfulBEqTactics
import Init.Prelude
import Init.Notation
import Init.Tactics
import Init.TacticsExtra
import Init.ByCases
import Init.RCases
import Init.Core
import Init.Control
import Init.Data.Basic
import Init.WF
import Init.WFTactics
import Init.Data
import Init.System
import Init.Util
import Init.Dynamic
import Init.ShareCommon
import Init.MetaTypes
import Init.Meta
import Init.NotationExtra
import Init.SimpLemmas
import Init.PropLemmas
import Init.Hints
import Init.Conv
import Init.Guard
import Init.Simproc
import Init.SizeOfLemmas
import Init.BinderPredicates
import Init.Ext
import Init.Omega
import Init.MacroTrace
import Init.Grind
import Init.GrindInstances
import Init.While
import Init.Syntax
import Init.Internal
import Init.Try
import Init.BinderNameHint
import Init.Task

View File

@@ -7,10 +7,8 @@ Authors: Joachim Breitner
module
prelude
public import Init.Prelude
public import Init.Tactics
public section
import Init.Prelude
import Init.Tactics
set_option linter.unusedVariables false in
/--
@@ -39,7 +37,7 @@ This gadget is supported by
* `simp`, `dsimp` and `rw` in the right-hand-side of an equation
* `simp` in the assumptions of congruence rules
It is ineffective in other positions (hypotheses of rewrite rules) or when used by other tactics
It is ineffective in other positions (hyptheses of rewrite rules) or when used by other tactics
(e.g. `apply`).
-/
@[simp , expose]

View File

@@ -6,9 +6,7 @@ Authors: Gabriel Ebner
module
prelude
public import Init.NotationExtra
public section
import Init.NotationExtra
namespace Lean

View File

@@ -6,9 +6,7 @@ Authors: Leonardo de Moura, Mario Carneiro
module
prelude
public import Init.Classical
public section
import Init.Classical
/-! # by_cases tactic and if-then-else support -/

View File

@@ -6,9 +6,7 @@ Authors: Leonardo de Moura, Mario Carneiro
module
prelude
public import Init.PropLemmas
public section
import Init.PropLemmas
universe u v

View File

@@ -6,10 +6,8 @@ Authors: Leonardo de Moura, Mario Carneiro
module
prelude
public import Init.Prelude
public meta import Init.Prelude
public section
import Init.Prelude
meta import Init.Prelude
set_option linter.missingDocs true -- keep it documented
/-!

View File

@@ -6,15 +6,13 @@ Authors: Leonardo de Moura
module
prelude
public import Init.Control.Basic
public import Init.Control.State
public import Init.Control.StateRef
public import Init.Control.Id
public import Init.Control.Except
public import Init.Control.Reader
public import Init.Control.Option
public import Init.Control.Lawful
public import Init.Control.StateCps
public import Init.Control.ExceptCps
public section
import Init.Control.Basic
import Init.Control.State
import Init.Control.StateRef
import Init.Control.Id
import Init.Control.Except
import Init.Control.Reader
import Init.Control.Option
import Init.Control.Lawful
import Init.Control.StateCps
import Init.Control.ExceptCps

View File

@@ -6,10 +6,8 @@ Author: Leonardo de Moura, Sebastian Ullrich
module
prelude
public import Init.Core
public import Init.BinderNameHint
@[expose] public section
import Init.Core
import Init.BinderNameHint
universe u v w

View File

@@ -6,11 +6,9 @@ Authors: Leonardo de Moura
module
prelude
public import Init.Control.State
public import Init.Control.Except
public import Init.Data.ToString.Basic
public section
import Init.Control.State
import Init.Control.Except
import Init.Data.ToString.Basic
universe u v
namespace EStateM
@@ -19,8 +17,8 @@ variable {ε σ α : Type u}
instance [ToString ε] [ToString α] : ToString (Result ε σ α) where
toString
| Result.ok a _ => String.Internal.append "ok: " (toString a)
| Result.error e _ => String.Internal.append "error: " (toString e)
| Result.ok a _ => "ok: " ++ toString a
| Result.error e _ => "error: " ++ toString e
instance [Repr ε] [Repr α] : Repr (Result ε σ α) where
reprPrec

View File

@@ -8,11 +8,9 @@ The Except monad transformer.
module
prelude
public import Init.Control.Basic
public import Init.Control.Id
public import Init.Coe
@[expose] public section
import Init.Control.Basic
import Init.Control.Id
import Init.Coe
namespace Except
variable {ε : Type u}

View File

@@ -6,9 +6,7 @@ Authors: Leonardo de Moura
module
prelude
public import Init.Control.Lawful.Basic
public section
import Init.Control.Lawful.Basic
/-!
The Exception monad transformer using CPS style.

View File

@@ -8,9 +8,7 @@ The identity Monad.
module
prelude
public import Init.Core
public section
import Init.Core
universe u
@@ -64,7 +62,4 @@ protected def run (x : Id α) : α := x
instance [OfNat α n] : OfNat (Id α) n :=
inferInstanceAs (OfNat α n)
instance {m : Type u Type v} [Pure m] : MonadLiftT Id m where
monadLift x := pure x.run
end Id

View File

@@ -6,9 +6,7 @@ Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro
module
prelude
public import Init.Control.Lawful.Basic
public import Init.Control.Lawful.Instances
public import Init.Control.Lawful.Lemmas
public import Init.Control.Lawful.MonadLift
public section
import Init.Control.Lawful.Basic
import Init.Control.Lawful.Instances
import Init.Control.Lawful.Lemmas
import Init.Control.Lawful.MonadLift

View File

@@ -6,11 +6,9 @@ Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro
module
prelude
public import Init.Ext
public import Init.SimpLemmas
public import Init.Meta
public section
import Init.Ext
import Init.SimpLemmas
import Init.Meta
open Function
@@ -147,7 +145,7 @@ class LawfulMonad (m : Type u → Type v) [Monad m] : Prop extends LawfulApplica
export LawfulMonad (bind_pure_comp bind_map pure_bind bind_assoc)
attribute [simp] pure_bind bind_assoc bind_pure_comp
attribute [grind <=] pure_bind
attribute [grind] pure_bind
@[simp] theorem bind_pure [Monad m] [LawfulMonad m] (x : m α) : x >>= pure = x := by
change x >>= (fun a => pure (id a)) = x

View File

@@ -6,15 +6,11 @@ Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro
module
prelude
public import Init.Control.Lawful.Basic
public import Init.Control.Except
import Init.Control.Lawful.Basic
import all Init.Control.Except
public import Init.Control.State
import all Init.Control.State
public import Init.Control.StateRef
public import Init.Ext
public section
import Init.Control.StateRef
import Init.Ext
open Function
@@ -22,24 +18,23 @@ open Function
namespace ExceptT
@[ext, grind ext] theorem ext {x y : ExceptT ε m α} (h : x.run = y.run) : x = y := by
@[ext] theorem ext {x y : ExceptT ε m α} (h : x.run = y.run) : x = y := by
simp [run] at h
assumption
@[simp, grind =] theorem run_pure [Monad m] (x : α) : run (pure x : ExceptT ε m α) = pure (Except.ok x) := rfl
@[simp] theorem run_pure [Monad m] (x : α) : run (pure x : ExceptT ε m α) = pure (Except.ok x) := rfl
@[simp, grind =] theorem run_lift [Monad.{u, v} m] (x : m α) : run (ExceptT.lift x : ExceptT ε m α) = (Except.ok <$> x : m (Except ε α)) := rfl
@[simp] theorem run_lift [Monad.{u, v} m] (x : m α) : run (ExceptT.lift x : ExceptT ε m α) = (Except.ok <$> x : m (Except ε α)) := rfl
@[simp, grind =] theorem run_throw [Monad m] : run (throw e : ExceptT ε m β) = pure (Except.error e) := rfl
@[simp] theorem run_throw [Monad m] : run (throw e : ExceptT ε m β) = pure (Except.error e) := rfl
@[simp, grind =] theorem run_bind_lift [Monad m] [LawfulMonad m] (x : m α) (f : α ExceptT ε m β) : run (ExceptT.lift x >>= f : ExceptT ε m β) = x >>= fun a => run (f a) := by
@[simp] theorem run_bind_lift [Monad m] [LawfulMonad m] (x : m α) (f : α ExceptT ε m β) : run (ExceptT.lift x >>= f : ExceptT ε m β) = x >>= fun a => run (f a) := by
simp [ExceptT.run, ExceptT.lift, bind, ExceptT.bind, ExceptT.mk, ExceptT.bindCont]
@[simp, grind =] theorem bind_throw [Monad m] [LawfulMonad m] (f : α ExceptT ε m β) : (throw e >>= f) = throw e := by
@[simp] theorem bind_throw [Monad m] [LawfulMonad m] (f : α ExceptT ε m β) : (throw e >>= f) = throw e := by
simp [throw, throwThe, MonadExceptOf.throw, bind, ExceptT.bind, ExceptT.bindCont, ExceptT.mk]
@[grind =]
theorem run_bind [Monad m] (x : ExceptT ε m α) (f : α ExceptT ε m β)
theorem run_bind [Monad m] (x : ExceptT ε m α)
: run (x >>= f : ExceptT ε m β)
=
run x >>= fun
@@ -47,10 +42,10 @@ theorem run_bind [Monad m] (x : ExceptT ε m α) (f : α → ExceptT ε m β)
| Except.error e => pure (Except.error e) :=
rfl
@[simp, grind =] theorem lift_pure [Monad m] [LawfulMonad m] (a : α) : ExceptT.lift (pure a) = (pure a : ExceptT ε m α) := by
@[simp] theorem lift_pure [Monad m] [LawfulMonad m] (a : α) : ExceptT.lift (pure a) = (pure a : ExceptT ε m α) := by
simp [ExceptT.lift, pure, ExceptT.pure]
@[simp, grind =] theorem run_map [Monad m] [LawfulMonad m] (f : α β) (x : ExceptT ε m α)
@[simp] theorem run_map [Monad m] [LawfulMonad m] (f : α β) (x : ExceptT ε m α)
: (f <$> x).run = Except.map f <$> x.run := by
simp [Functor.map, ExceptT.map, bind_pure_comp]
apply bind_congr
@@ -114,28 +109,28 @@ instance : LawfulFunctor (Except ε) := inferInstance
namespace ReaderT
@[ext, grind ext] theorem ext {x y : ReaderT ρ m α} (h : ctx, x.run ctx = y.run ctx) : x = y := by
@[ext] theorem ext {x y : ReaderT ρ m α} (h : ctx, x.run ctx = y.run ctx) : x = y := by
simp [run] at h
exact funext h
@[simp, grind =] theorem run_pure [Monad m] (a : α) (ctx : ρ) : (pure a : ReaderT ρ m α).run ctx = pure a := rfl
@[simp] theorem run_pure [Monad m] (a : α) (ctx : ρ) : (pure a : ReaderT ρ m α).run ctx = pure a := rfl
@[simp, grind =] theorem run_bind [Monad m] (x : ReaderT ρ m α) (f : α ReaderT ρ m β) (ctx : ρ)
@[simp] theorem run_bind [Monad m] (x : ReaderT ρ m α) (f : α ReaderT ρ m β) (ctx : ρ)
: (x >>= f).run ctx = x.run ctx >>= λ a => (f a).run ctx := rfl
@[simp, grind =] theorem run_mapConst [Monad m] (a : α) (x : ReaderT ρ m β) (ctx : ρ)
@[simp] theorem run_mapConst [Monad m] (a : α) (x : ReaderT ρ m β) (ctx : ρ)
: (Functor.mapConst a x).run ctx = Functor.mapConst a (x.run ctx) := rfl
@[simp, grind =] theorem run_map [Monad m] (f : α β) (x : ReaderT ρ m α) (ctx : ρ)
@[simp] theorem run_map [Monad m] (f : α β) (x : ReaderT ρ m α) (ctx : ρ)
: (f <$> x).run ctx = f <$> x.run ctx := rfl
@[simp, grind =] theorem run_monadLift [MonadLiftT n m] (x : n α) (ctx : ρ)
@[simp] theorem run_monadLift [MonadLiftT n m] (x : n α) (ctx : ρ)
: (monadLift x : ReaderT ρ m α).run ctx = (monadLift x : m α) := rfl
@[simp, grind =] theorem run_monadMap [MonadFunctorT n m] (f : {β : Type u} n β n β) (x : ReaderT ρ m α) (ctx : ρ)
@[simp] theorem run_monadMap [MonadFunctorT n m] (f : {β : Type u} n β n β) (x : ReaderT ρ m α) (ctx : ρ)
: (monadMap @f x : ReaderT ρ m α).run ctx = monadMap @f (x.run ctx) := rfl
@[simp, grind =] theorem run_read [Monad m] (ctx : ρ) : (ReaderT.read : ReaderT ρ m ρ).run ctx = pure ctx := rfl
@[simp] theorem run_read [Monad m] (ctx : ρ) : (ReaderT.read : ReaderT ρ m ρ).run ctx = pure ctx := rfl
@[simp] theorem run_seq {α β : Type u} [Monad m] (f : ReaderT ρ m (α β)) (x : ReaderT ρ m α) (ctx : ρ)
: (f <*> x).run ctx = (f.run ctx <*> x.run ctx) := rfl
@@ -176,39 +171,38 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (StateRefT' ω σ m) :=
namespace StateT
@[ext, grind ext] theorem ext {x y : StateT σ m α} (h : s, x.run s = y.run s) : x = y :=
@[ext] theorem ext {x y : StateT σ m α} (h : s, x.run s = y.run s) : x = y :=
funext h
@[simp, grind =] theorem run'_eq [Monad m] (x : StateT σ m α) (s : σ) : run' x s = (·.1) <$> run x s :=
@[simp] theorem run'_eq [Monad m] (x : StateT σ m α) (s : σ) : run' x s = (·.1) <$> run x s :=
rfl
@[simp, grind =] theorem run_pure [Monad m] (a : α) (s : σ) : (pure a : StateT σ m α).run s = pure (a, s) := rfl
@[simp] theorem run_pure [Monad m] (a : α) (s : σ) : (pure a : StateT σ m α).run s = pure (a, s) := rfl
@[simp, grind =] theorem run_bind [Monad m] (x : StateT σ m α) (f : α StateT σ m β) (s : σ)
@[simp] theorem run_bind [Monad m] (x : StateT σ m α) (f : α StateT σ m β) (s : σ)
: (x >>= f).run s = x.run s >>= λ p => (f p.1).run p.2 := by
simp [bind, StateT.bind, run]
@[simp, grind =] theorem run_map {α β σ : Type u} [Monad m] [LawfulMonad m] (f : α β) (x : StateT σ m α) (s : σ) : (f <$> x).run s = (fun (p : α × σ) => (f p.1, p.2)) <$> x.run s := by
@[simp] theorem run_map {α β σ : Type u} [Monad m] [LawfulMonad m] (f : α β) (x : StateT σ m α) (s : σ) : (f <$> x).run s = (fun (p : α × σ) => (f p.1, p.2)) <$> x.run s := by
simp [Functor.map, StateT.map, run, bind_pure_comp]
@[simp, grind =] theorem run_get [Monad m] (s : σ) : (get : StateT σ m σ).run s = pure (s, s) := rfl
@[simp] theorem run_get [Monad m] (s : σ) : (get : StateT σ m σ).run s = pure (s, s) := rfl
@[simp, grind =] theorem run_set [Monad m] (s s' : σ) : (set s' : StateT σ m PUnit).run s = pure (, s') := rfl
@[simp] theorem run_set [Monad m] (s s' : σ) : (set s' : StateT σ m PUnit).run s = pure (, s') := rfl
@[simp, grind =] theorem run_modify [Monad m] (f : σ σ) (s : σ) : (modify f : StateT σ m PUnit).run s = pure (, f s) := rfl
@[simp] theorem run_modify [Monad m] (f : σ σ) (s : σ) : (modify f : StateT σ m PUnit).run s = pure (, f s) := rfl
@[simp, grind =] theorem run_modifyGet [Monad m] (f : σ α × σ) (s : σ) : (modifyGet f : StateT σ m α).run s = pure ((f s).1, (f s).2) := by
@[simp] theorem run_modifyGet [Monad m] (f : σ α × σ) (s : σ) : (modifyGet f : StateT σ m α).run s = pure ((f s).1, (f s).2) := by
simp [modifyGet, MonadStateOf.modifyGet, StateT.modifyGet, run]
@[simp, grind =] theorem run_lift {α σ : Type u} [Monad m] (x : m α) (s : σ) : (StateT.lift x : StateT σ m α).run s = x >>= fun a => pure (a, s) := rfl
@[simp] theorem run_lift {α σ : Type u} [Monad m] (x : m α) (s : σ) : (StateT.lift x : StateT σ m α).run s = x >>= fun a => pure (a, s) := rfl
@[grind =]
theorem run_bind_lift {α σ : Type u} [Monad m] [LawfulMonad m] (x : m α) (f : α StateT σ m β) (s : σ) : (StateT.lift x >>= f).run s = x >>= fun a => (f a).run s := by
simp [StateT.lift, StateT.run, bind, StateT.bind]
@[simp, grind =] theorem run_monadLift {α σ : Type u} [Monad m] [MonadLiftT n m] (x : n α) (s : σ) : (monadLift x : StateT σ m α).run s = (monadLift x : m α) >>= fun a => pure (a, s) := rfl
@[simp] theorem run_monadLift {α σ : Type u} [Monad m] [MonadLiftT n m] (x : n α) (s : σ) : (monadLift x : StateT σ m α).run s = (monadLift x : m α) >>= fun a => pure (a, s) := rfl
@[simp, grind =] theorem run_monadMap [MonadFunctorT n m] (f : {β : Type u} n β n β) (x : StateT σ m α) (s : σ) :
@[simp] theorem run_monadMap [MonadFunctorT n m] (f : {β : Type u} n β n β) (x : StateT σ m α) (s : σ) :
(monadMap @f x : StateT σ m α).run s = monadMap @f (x.run s) := rfl
@[simp] theorem run_seq {α β σ : Type u} [Monad m] [LawfulMonad m] (f : StateT σ m (α β)) (x : StateT σ m α) (s : σ) : (f <*> x).run s = (f.run s >>= fun fs => (fun (p : α × σ) => (fs.1 p.1, p.2)) <$> x.run fs.2) := by

View File

@@ -6,11 +6,9 @@ Authors: Kim Morrison
module
prelude
public import Init.Control.Lawful.Basic
public import Init.RCases
public import Init.ByCases
public section
import Init.Control.Lawful.Basic
import Init.RCases
import Init.ByCases
-- Mapping by a function with a left inverse is injective.
theorem map_inj_of_left_inverse [Functor m] [LawfulFunctor m] {f : α β}

View File

@@ -6,8 +6,6 @@ Authors: Paul Reichert
module
prelude
public import Init.Control.Lawful.MonadLift.Basic
public import Init.Control.Lawful.MonadLift.Lemmas
public import Init.Control.Lawful.MonadLift.Instances
public section
import Init.Control.Lawful.MonadLift.Basic
import Init.Control.Lawful.MonadLift.Lemmas
import Init.Control.Lawful.MonadLift.Instances

View File

@@ -6,9 +6,7 @@ Authors: Quang Dao
module
prelude
public import Init.Control.Basic
public section
import Init.Control.Basic
/-!
# LawfulMonadLift and LawfulMonadLiftT

View File

@@ -6,22 +6,13 @@ Authors: Quang Dao, Paul Reichert
module
prelude
public import Init.Control.Option
import all Init.Control.Option
public import Init.Control.Except
import all Init.Control.Except
public import Init.Control.ExceptCps
import all Init.Control.ExceptCps
public import Init.Control.StateRef
import all Init.Control.StateRef
public import Init.Control.StateCps
import all Init.Control.StateCps
public import Init.Control.Id
import all Init.Control.Id
public import Init.Control.Lawful.MonadLift.Lemmas
public import Init.Control.Lawful.Instances
public section
import Init.Control.Lawful.MonadLift.Lemmas
import Init.Control.Lawful.Instances
universe u v w x
@@ -144,11 +135,3 @@ instance {ε : Type u} [Monad m] [LawfulMonad m] : LawfulMonadLift m (ExceptCpsT
simp only [bind_assoc]
end ExceptCpsT
namespace Id
instance [Monad m] [LawfulMonad m] : LawfulMonadLiftT Id m where
monadLift_pure a := by simp [monadLift]
monadLift_bind a f := by simp [monadLift]
end Id

View File

@@ -6,10 +6,8 @@ Authors: Quang Dao
module
prelude
public import Init.Control.Lawful.Basic
public import Init.Control.Lawful.MonadLift.Basic
public section
import Init.Control.Lawful.Basic
import Init.Control.Lawful.MonadLift.Basic
universe u v w

View File

@@ -6,11 +6,9 @@ Authors: Leonardo de Moura, Sebastian Ullrich
module
prelude
public import Init.Data.Option.Basic
public import Init.Control.Basic
public import Init.Control.Except
public section
import Init.Data.Option.Basic
import Init.Control.Basic
import Init.Control.Except
set_option linter.missingDocs true

View File

@@ -8,11 +8,9 @@ The Reader monad transformer for passing immutable State.
module
prelude
public import Init.Control.Basic
public import Init.Control.Id
public import Init.Control.Except
public section
import Init.Control.Basic
import Init.Control.Id
import Init.Control.Except
set_option linter.missingDocs true
@@ -52,4 +50,4 @@ instance ReaderT.tryFinally [MonadFinally m] : MonadFinally (ReaderT ρ m) where
A monad with access to a read-only value of type `ρ`. The value can be locally overridden by
`withReader`, but it cannot be mutated.
-/
abbrev ReaderM (ρ : Type u) := ReaderT ρ Id
@[reducible] def ReaderM (ρ : Type u) := ReaderT ρ Id

View File

@@ -8,11 +8,9 @@ The State monad transformer.
module
prelude
public import Init.Control.Basic
public import Init.Control.Id
public import Init.Control.Except
public section
import Init.Control.Basic
import Init.Control.Id
import Init.Control.Except
set_option linter.missingDocs true

View File

@@ -6,9 +6,7 @@ Authors: Leonardo de Moura
module
prelude
public import Init.Control.Lawful.Basic
public section
import Init.Control.Lawful.Basic
set_option linter.missingDocs true

View File

@@ -8,9 +8,7 @@ The State monad transformer using IO references.
module
prelude
public import Init.System.ST
public section
import Init.System.ST
set_option linter.missingDocs true

View File

@@ -8,10 +8,8 @@ Notation for operators defined at Prelude.lean
module
prelude
public import Init.Tactics
public meta import Init.Meta
public section
import Init.Tactics
meta import Init.Meta
namespace Lean.Parser.Tactic.Conv
@@ -187,9 +185,6 @@ match [a, b] with
simplifies to `a`. -/
syntax (name := simpMatch) "simp_match" : conv
/-- Removes one or more hypotheses from the local context. -/
syntax (name := clear) "clear" (ppSpace colGt term:max)+ : conv
/-- Executes the given tactic block without converting `conv` goal into a regular goal. -/
syntax (name := nestedTacticCore) "tactic'" " => " tacticSeq : conv
@@ -265,7 +260,7 @@ resulting in `t'`, which becomes the new target subgoal. -/
syntax (name := convConvSeq) "conv" " => " convSeq : conv
/-- `· conv` focuses on the main conv goal and tries to solve it using `s`. -/
macro dot:patternIgnore("· " <|> ". ") s:convSeq : conv => `(conv| {%$dot ($s) })
macro dot:patternIgnore("·" <|> ".") s:convSeq : conv => `(conv| {%$dot ($s) })
/-- `fail_if_success t` fails if the tactic `t` succeeds. -/
@@ -290,17 +285,13 @@ macro "right" : conv => `(conv| rhs)
/-- `intro` traverses into binders. Synonym for `ext`. -/
macro "intro" xs:(ppSpace colGt binderIdent)* : conv => `(conv| ext $xs*)
syntax enterPattern := "in " (occs)? term
syntax enterArg := binderIdent <|> argArg <|> enterPattern
syntax enterArg := binderIdent <|> argArg
/-- `enter [arg, ...]` is a compact way to describe a path to a subterm.
It is a shorthand for other conv tactics as follows:
* `enter [i]` is equivalent to `arg i`.
* `enter [@i]` is equivalent to `arg @i`.
* `enter [x]` (where `x` is an identifier) is equivalent to `ext x`.
* `enter [in e]` (where `e` is a term) is equivalent to `pattern e`.
Occurrences can be specified with `enter [in (occs := ...) e]`.
For example, given the target `f (g a (fun x => x b))`, `enter [1, 2, x, 1]`
will traverse to the subterm `b`. -/
syntax (name := enter) "enter" " [" withoutPosition(enterArg,+) "]" : conv
@@ -330,7 +321,7 @@ macro_rules
| `(conv| repeat $seq) => `(conv| first | ($seq); repeat $seq | skip)
/--
Extracts `let` and `have` expressions from within the target expression.
Extracts `let` and `let_fun` expressions from within the target expression.
This is the conv mode version of the `extract_lets` tactic.
- `extract_lets` extracts all the lets from the target.
@@ -343,17 +334,11 @@ See also `lift_lets`, which does not extract lets as local declarations.
syntax (name := extractLets) "extract_lets " optConfig (ppSpace colGt (ident <|> hole))* : conv
/--
Lifts `let` and `have` expressions within the target expression as far out as possible.
Lifts `let` and `let_fun` expressions within the target expression as far out as possible.
This is the conv mode version of the `lift_lets` tactic.
-/
syntax (name := liftLets) "lift_lets " optConfig : conv
/--
Transforms `let` expressions into `have` expressions within the target expression when possible.
This is the conv mode version of the `let_to_have` tactic.
-/
syntax (name := letToHave) "let_to_have" : conv
/--
`conv => ...` allows the user to perform targeted rewriting on a goal or hypothesis,
by focusing on particular subexpressions.

View File

@@ -8,10 +8,8 @@ notation, basic datatypes and type classes
module
prelude
public meta import Init.Prelude
public import Init.SizeOf
public section
meta import Init.Prelude
import Init.SizeOf
set_option linter.missingDocs true -- keep it documented
@[expose] section
@@ -29,29 +27,6 @@ theorem id_def {α : Sort u} (a : α) : id a = a := rfl
attribute [grind] id
/--
A helper gadget for instructing the kernel to eagerly reduce terms.
When the gadget wraps the argument of an application, then when checking that
the expected and inferred type of the argument match, the kernel will evaluate terms more eagerly.
It is often used to wrap `Eq.refl true` proof terms as `eagerReduce (Eq.refl true)`
when using proof by reflection.
As an example, consider the theorem:
```
theorem eq_norm (ctx : Context) (p₁ p₂ : Poly) (h : (p₁.norm == p₂) = true) :
p₁.denote ctx = 0 → p₂.denote ctx = 0
```
The argument `h : (p₁.norm == p₂) = true` is a candidate for `eagerReduce`.
When applying this theorem, we would write:
```
eq_norm ctx p q (eagerReduce (Eq.refl true)) h
```
to instruct the kernel to use eager reduction when establishing that `(p.norm == q) = true` is
definitionally equal to `true = true`.
-/
@[expose] def eagerReduce {α : Sort u} (a : α) : α := a
/--
`flip f a b` is `f b a`. It is useful for "point-free" programming,
since it can sometimes be used to avoid introducing variables.
@@ -775,8 +750,6 @@ Unlike `x ≠ y` (which is notation for `Ne x y`), this is `Bool` valued instead
@[inherit_doc] infix:50 " != " => bne
macro_rules | `($x != $y) => `(binrel_no_prop% bne $x $y)
recommended_spelling "bne" for "!=" in [bne, «term_!=_»]
/-- `ReflBEq α` says that the `BEq` implementation is reflexive. -/
@@ -878,8 +851,6 @@ and asserts that `a` and `b` are not equal.
@[inherit_doc] infix:50 "" => Ne
macro_rules | `($x $y) => `(binrel% Ne $x $y)
recommended_spelling "ne" for "" in [Ne, «term__»]
section Ne
@@ -1559,13 +1530,38 @@ end Setoid
/-! # Propositional extensionality -/
/--
The [axiom](lean-manual://section/axioms) of **propositional extensionality**. It asserts that if
propositions `a` and `b` are logically equivalent (that is, if `a` can be proved from `b` and vice
versa), then `a` and `b` are *equal*, meaning `a` can be replaced with `b` in all contexts.
The axiom of **propositional extensionality**. It asserts that if propositions
`a` and `b` are logically equivalent (i.e. we can prove `a` from `b` and vice versa),
then `a` and `b` are *equal*, meaning that we can replace `a` with `b` in all
contexts.
The standard logical connectives provably respect propositional extensionality. However, an axiom is
needed for higher order expressions like `P a` where `P : Prop → Prop` is unknown, as well as for
equality. Propositional extensionality is intuitionistically valid.
For simple expressions like `a ∧ c d → e` we can prove that because all the logical
connectives respect logical equivalence, we can replace `a` with `b` in this expression
without using `propext`. However, for higher order expressions like `P a` where
`P : Prop → Prop` is unknown, or indeed for `a = b` itself, we cannot replace `a` with `b`
without an axiom which says exactly this.
This is a relatively uncontroversial axiom, which is intuitionistically valid.
It does however block computation when using `#reduce` to reduce proofs directly
(which is not recommended), meaning that canonicity,
the property that all closed terms of type `Nat` normalize to numerals,
fails to hold when this (or any) axiom is used:
```
set_option pp.proofs true
def foo : Nat := by
have : (True → True) ↔ True := ⟨λ _ => trivial, λ _ _ => trivial⟩
have := propext this ▸ (2 : Nat)
exact this
#reduce foo
-- propext { mp := fun x x => True.intro, mpr := fun x => True.intro } ▸ 2
#eval foo -- 2
```
`#eval` can evaluate it to a numeral because the compiler erases casts and
does not evaluate proofs, so `propext`, whose return type is a proposition,
can never block it.
-/
axiom propext {a b : Prop} : (a b) a = b
@@ -1596,7 +1592,6 @@ gen_injective_theorems% MProd
gen_injective_theorems% NonScalar
gen_injective_theorems% Option
gen_injective_theorems% PLift
gen_injective_theorems% PULift
gen_injective_theorems% PNonScalar
gen_injective_theorems% PProd
gen_injective_theorems% Prod
@@ -2522,17 +2517,12 @@ class Antisymm (r : αα → Prop) : Prop where
/-- An antisymmetric relation `r` satisfies `r a b → r b a → a = b`. -/
antisymm (a b : α) : r a b r b a a = b
/-- `Asymm r` means that the binary relation `r` is asymmetric, that is,
/-- `Asymm X r` means that the binary relation `r` on `X` is asymmetric, that is,
`r a b → ¬ r b a`. -/
class Asymm (r : α α Prop) : Prop where
/-- An asymmetric relation satisfies `r a b → ¬ r b a`. -/
asymm : a b, r a b ¬r b a
/-- `Symm r` means that the binary relation `r` is symmetric, that is, `r a b → r b a`. -/
class Symm (r : α α Prop) : Prop where
/-- A symmetric relation satisfies `r a b → r b a`. -/
symm : a b, r a b r b a
/-- `Total X r` means that the binary relation `r` on `X` is total, that is, that for any
`x y : X` we have `r x y` or `r y x`. -/
class Total (r : α α Prop) : Prop where

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