Compare commits

..

3 Commits

Author SHA1 Message Date
Scott Morrison
54de6271fd merge master 2024-02-14 12:14:04 +11:00
Leonardo de Moura
eb7951e872 chore: replace tactic builtin 2024-02-13 13:39:34 -08:00
Scott Morrison
e601cdb193 chore: upstream replace tactic 2024-02-13 22:57:16 +11:00
4838 changed files with 25392 additions and 187947 deletions

View File

@@ -9,15 +9,9 @@ assignees: ''
### Prerequisites
Please put an X between the brackets as you perform the following steps:
* [ ] Check that your issue is not already filed:
https://github.com/leanprover/lean4/issues
* [ ] Reduce the issue to a minimal, self-contained, reproducible test case.
Avoid dependencies to Mathlib or Batteries.
* [ ] Test your test case against the latest nightly release, for example on
https://live.lean-lang.org/#project=lean-nightly
(You can also use the settings there to switch to “Lean nightly”)
* [ ] Put an X between the brackets on this line if you have done all of the following:
* Check that your issue is not already [filed](https://github.com/leanprover/lean4/issues).
* Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.
### Description
@@ -25,7 +19,7 @@ Please put an X between the brackets as you perform the following steps:
### Context
[Broader context that the issue occurred in. If there was any prior discussion on [the Lean Zulip](https://leanprover.zulipchat.com), link it here as well.]
[Broader context that the issue occured in. If there was any prior discussion on [the Lean Zulip](https://leanprover.zulipchat.com), link it here as well.]
### Steps to Reproduce
@@ -39,8 +33,8 @@ Please put an X between the brackets as you perform the following steps:
### Versions
[Output of `#version` or `#eval Lean.versionString`]
[OS version, if not using live.lean-lang.org.]
[Output of `#eval Lean.versionString` or of `lean --version` in the folder that the issue occured in]
[OS version]
### Additional Information

View File

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

View File

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

View File

@@ -15,8 +15,8 @@ jobs:
runs-on: ubuntu-latest
steps:
- name: Checkout
uses: actions/checkout@v4
uses: actions/checkout@v3
- name: actionlint
uses: raven-actions/actionlint@v2
uses: raven-actions/actionlint@v1
with:
pyflakes: false # we do not use python scripts

View File

@@ -1,28 +0,0 @@
name: Check for modules that should use `prelude`
on: [pull_request]
jobs:
check-prelude:
runs-on: ubuntu-latest
steps:
- name: Checkout
uses: actions/checkout@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 }}
sparse-checkout: |
src/Lean
src/Std
- name: Check Prelude
run: |
failed_files=""
while IFS= read -r -d '' file; do
if ! grep -q "^prelude$" "$file"; then
failed_files="$failed_files$file\n"
fi
done < <(find src/Lean src/Std -name '*.lean' -print0)
if [ -n "$failed_files" ]; then
echo -e "The following files should use 'prelude':\n$failed_files"
exit 1
fi

View File

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

View File

@@ -6,20 +6,10 @@ on:
tags:
- '*'
pull_request:
types: [opened, synchronize, reopened, labeled]
merge_group:
schedule:
- cron: '0 7 * * *' # 8AM CET/11PM PT
# for manual re-release of a nightly
workflow_dispatch:
inputs:
action:
description: 'Action'
required: true
default: 'release nightly'
type: choice
options:
- release nightly
concurrency:
group: ${{ github.workflow }}-${{ github.ref }}-${{ github.event_name }}
@@ -31,10 +21,8 @@ jobs:
configure:
runs-on: ubuntu-latest
outputs:
# 0: PRs without special label
# 1: PRs with `merge-ci` label, merge queue checks, master commits
# 2: PRs with `release-ci` label, releases (incl. nightlies)
check-level: ${{ steps.set-level.outputs.check-level }}
# Should we run only a quick CI? Yes on a pull request without the full-ci label
quick: ${{ steps.set-quick.outputs.quick }}
# The build matrix, dynamically generated here
matrix: ${{ steps.set-matrix.outputs.result }}
# Should we make a nightly release? If so, this output contains the lean version string, else it is empty
@@ -51,12 +39,163 @@ jobs:
RELEASE_TAG: ${{ steps.set-release.outputs.RELEASE_TAG }}
steps:
- name: Run quick CI?
id: set-quick
env:
quick: ${{
github.event_name == 'pull_request' && !contains( github.event.pull_request.labels.*.name, 'full-ci')
}}
run: |
echo "quick=${{env.quick}}" >> "$GITHUB_OUTPUT"
- name: Configure build matrix
id: set-matrix
uses: actions/github-script@v7
with:
script: |
const quick = ${{ steps.set-quick.outputs.quick }};
console.log(`quick: ${quick}`)
let matrix = [
{
// portable release build: use channel with older glibc (2.27)
"name": "Linux LLVM",
"os": "ubuntu-latest",
"release": false,
"quick": false,
"shell": "nix-shell --arg pkgsDist \"import (fetchTarball \\\"channel:nixos-19.03\\\") {{}}\" --run \"bash -euxo pipefail {0}\"",
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst",
"prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
"binary-check": "ldd -v",
// foreign code may be linked against more recent glibc
// reverse-ffi needs to be updated to link to LLVM libraries
"CTEST_OPTIONS": "-E 'foreign|leanlaketest_reverse-ffi'",
"CMAKE_OPTIONS": "-DLLVM=ON -DLLVM_CONFIG=${GITHUB_WORKSPACE}/build/llvm-host/bin/llvm-config"
},
{
"name": "Linux release",
"os": "ubuntu-latest",
"release": true,
"quick": true,
"shell": "nix-shell --arg pkgsDist \"import (fetchTarball \\\"channel:nixos-19.03\\\") {{}}\" --run \"bash -euxo pipefail {0}\"",
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst",
"prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
"binary-check": "ldd -v",
// foreign code may be linked against more recent glibc
"CTEST_OPTIONS": "-E 'foreign'"
},
{
"name": "Linux",
"os": "ubuntu-latest",
"check-stage3": true,
"test-speedcenter": true,
"quick": false,
},
{
"name": "Linux Debug",
"os": "ubuntu-latest",
"quick": false,
"CMAKE_OPTIONS": "-DCMAKE_BUILD_TYPE=Debug",
// exclude seriously slow tests
"CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest'"
},
{
"name": "Linux fsanitize",
"os": "ubuntu-latest",
"quick": false,
// turn off custom allocator & symbolic functions to make LSAN do its magic
"CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address,undefined -DLEANC_EXTRA_FLAGS='-fsanitize=address,undefined -fsanitize-link-c++-runtime' -DSMALL_ALLOCATOR=OFF -DBSYMBOLIC=OFF",
// exclude seriously slow/problematic tests (laketests crash)
"CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest'"
},
{
"name": "macOS",
"os": "macos-latest",
"release": true,
"quick": false,
"shell": "bash -euxo pipefail {0}",
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/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
},
{
"name": "macOS aarch64",
"os": "macos-latest",
"release": true,
"quick": false,
"cross": true,
"cross_target": "aarch64-apple-darwin",
"shell": "bash -euxo pipefail {0}",
"CMAKE_OPTIONS": "-DUSE_GMP=OFF -DLEAN_INSTALL_SUFFIX=-darwin_aarch64",
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-apple-darwin.tar.zst https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-apple-darwin.tar.zst",
"prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm-aarch64-* lean-llvm-x86_64-*",
"binary-check": "otool -L",
"tar": "gtar" // https://github.com/actions/runner-images/issues/2619
},
{
"name": "Windows",
"os": "windows-2022",
"release": true,
"quick": false,
"shell": "msys2 {0}",
"CMAKE_OPTIONS": "-G \"Unix Makefiles\" -DUSE_GMP=OFF",
// for reasons unknown, interactivetests are flaky on Windows
"CTEST_OPTIONS": "--repeat until-pass:2",
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-w64-windows-gnu.tar.zst",
"prepare-llvm": "../script/prepare-llvm-mingw.sh lean-llvm*",
"binary-check": "ldd"
},
{
"name": "Linux aarch64",
"os": "ubuntu-latest",
"CMAKE_OPTIONS": "-DUSE_GMP=OFF -DLEAN_INSTALL_SUFFIX=-linux_aarch64",
"release": true,
"quick": false,
"cross": true,
"cross_target": "aarch64-unknown-linux-gnu",
"shell": "nix-shell --arg pkgsDist \"import (fetchTarball \\\"channel:nixos-19.03\\\") {{ localSystem.config = \\\"aarch64-unknown-linux-gnu\\\"; }}\" --run \"bash -euxo pipefail {0}\"",
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-linux-gnu.tar.zst",
"prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm-aarch64-* lean-llvm-x86_64-*"
},
{
"name": "Linux 32bit",
"os": "ubuntu-latest",
// Use 32bit on stage0 and stage1 to keep oleans compatible
"CMAKE_OPTIONS": "-DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_MMAP=OFF -DUSE_GMP=OFF -DLEAN_EXTRA_CXX_FLAGS='-m32' -DLEANC_OPTS='-m32' -DMMAP=OFF -DLEAN_INSTALL_SUFFIX=-linux_x86",
"cmultilib": true,
"release": true,
"quick": false,
"cross": true,
"shell": "bash -euxo pipefail {0}"
},
{
"name": "Web Assembly",
"os": "ubuntu-latest",
// Build a native 32bit binary in stage0 and use it to compile the oleans and the wasm build
"CMAKE_OPTIONS": "-DCMAKE_C_COMPILER_WORKS=1 -DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_CMAKE_CXX_COMPILER=clang++ -DSTAGE0_CMAKE_C_COMPILER=clang -DSTAGE0_CMAKE_EXECUTABLE_SUFFIX=\"\" -DUSE_GMP=OFF -DMMAP=OFF -DSTAGE0_MMAP=OFF -DCMAKE_AR=../emsdk/emsdk-main/upstream/emscripten/emar -DCMAKE_TOOLCHAIN_FILE=../emsdk/emsdk-main/upstream/emscripten/cmake/Modules/Platform/Emscripten.cmake -DLEAN_INSTALL_SUFFIX=-linux_wasm32",
"wasm": true,
"cmultilib": true,
"release": true,
"quick": false,
"cross": true,
"shell": "bash -euxo pipefail {0}",
// Just a few selected tests because wasm is slow
"CTEST_OPTIONS": "-R \"leantest_1007\\.lean|leantest_Format\\.lean|leanruntest\\_1037.lean|leanruntest_ac_rfl\\.lean\""
}
];
console.log(`matrix:\n${JSON.stringify(matrix, null, 2)}`)
if (quick) {
return matrix.filter((job) => job.quick)
} else {
return matrix
}
- name: Checkout
uses: actions/checkout@v4
uses: actions/checkout@v3
# don't schedule nightlies on forks
if: github.event_name == 'schedule' && github.repository == 'leanprover/lean4' || inputs.action == 'release nightly'
if: github.event_name == 'schedule' && github.repository == 'leanprover/lean4'
- name: Set Nightly
if: github.event_name == 'schedule' && github.repository == 'leanprover/lean4' || inputs.action == 'release nightly'
if: github.event_name == 'schedule' && github.repository == 'leanprover/lean4'
id: set-nightly
run: |
if [[ -n '${{ secrets.PUSH_NIGHTLY_TOKEN }}' ]]; then
@@ -101,168 +240,6 @@ jobs:
echo "Tag ${TAG_NAME} did not match SemVer regex."
fi
- name: Set check level
id: set-level
# We do not use github.event.pull_request.labels.*.name here because
# re-running a run does not update that list, and we do want to be able to
# rerun the workflow run after setting the `release-ci`/`merge-ci` labels.
run: |
check_level=0
if [[ -n "${{ steps.set-nightly.outputs.nightly }}" || -n "${{ steps.set-release.outputs.RELEASE_TAG }}" ]]; then
check_level=2
elif [[ "${{ github.event_name }}" != "pull_request" ]]; then
check_level=1
else
labels="$(gh api repos/${{ github.repository_owner }}/${{ github.event.repository.name }}/pulls/${{ github.event.pull_request.number }} --jq '.labels')"
if echo "$labels" | grep -q "release-ci"; then
check_level=2
elif echo "$labels" | grep -q "merge-ci"; then
check_level=1
fi
fi
echo "check-level=$check_level" >> "$GITHUB_OUTPUT"
env:
GH_TOKEN: ${{ github.token }}
- name: Configure build matrix
id: set-matrix
uses: actions/github-script@v7
with:
script: |
const level = ${{ steps.set-level.outputs.check-level }};
console.log(`level: ${level}`);
// use large runners where available (original repo)
let large = ${{ github.repository == 'leanprover/lean4' }};
let matrix = [
{
// portable release build: use channel with older glibc (2.27)
"name": "Linux LLVM",
"os": "ubuntu-latest",
"release": false,
"check-level": 2,
"shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst",
"prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
"binary-check": "ldd -v",
// foreign code may be linked against more recent glibc
// reverse-ffi needs to be updated to link to LLVM libraries
"CTEST_OPTIONS": "-E 'foreign|leanlaketest_reverse-ffi'",
"CMAKE_OPTIONS": "-DLLVM=ON -DLLVM_CONFIG=${GITHUB_WORKSPACE}/build/llvm-host/bin/llvm-config"
},
{
"name": "Linux release",
"os": large ? "nscloud-ubuntu-22.04-amd64-4x8" : "ubuntu-latest",
"release": true,
"check-level": 0,
"shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst",
"prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
"binary-check": "ldd -v",
// foreign code may be linked against more recent glibc
"CTEST_OPTIONS": "-E 'foreign'"
},
{
"name": "Linux",
"os": large ? "nscloud-ubuntu-22.04-amd64-4x8" : "ubuntu-latest",
"check-stage3": level >= 2,
"test-speedcenter": level >= 2,
"check-level": 1,
},
{
"name": "Linux Debug",
"os": "ubuntu-latest",
"check-level": 2,
"CMAKE_PRESET": "debug",
// exclude seriously slow tests
"CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest|bv_bitblast_stress'"
},
// TODO: suddenly started failing in CI
/*{
"name": "Linux fsanitize",
"os": "ubuntu-latest",
"check-level": 2,
// turn off custom allocator & symbolic functions to make LSAN do its magic
"CMAKE_PRESET": "sanitize",
// exclude seriously slow/problematic tests (laketests crash)
"CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest'"
},*/
{
"name": "macOS",
"os": "macos-13",
"release": true,
"check-level": 2,
"shell": "bash -euxo pipefail {0}",
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/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
},
{
"name": "macOS aarch64",
"os": "macos-14",
"CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-darwin_aarch64",
"release": true,
"check-level": 0,
"shell": "bash -euxo pipefail {0}",
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-apple-darwin.tar.zst",
"prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
"binary-check": "otool -L",
"tar": "gtar" // https://github.com/actions/runner-images/issues/2619
},
{
"name": "Windows",
"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/15.0.1/lean-llvm-x86_64-w64-windows-gnu.tar.zst",
"prepare-llvm": "../script/prepare-llvm-mingw.sh lean-llvm*",
"binary-check": "ldd"
},
{
"name": "Linux aarch64",
"os": "nscloud-ubuntu-22.04-arm64-4x8",
"CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-linux_aarch64",
"release": true,
"check-level": 2,
"shell": "nix develop .#oldGlibcAArch -c bash -euxo pipefail {0}",
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-linux-gnu.tar.zst",
"prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*"
},
{
"name": "Linux 32bit",
"os": "ubuntu-latest",
// Use 32bit on stage0 and stage1 to keep oleans compatible
"CMAKE_OPTIONS": "-DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_MMAP=OFF -DUSE_GMP=OFF -DLEAN_EXTRA_CXX_FLAGS='-m32' -DLEANC_OPTS='-m32' -DMMAP=OFF -DLEAN_INSTALL_SUFFIX=-linux_x86 -DCMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/ -DSTAGE0_CMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/",
"cmultilib": true,
"release": true,
"check-level": 2,
"cross": true,
"shell": "bash -euxo pipefail {0}"
},
{
"name": "Web Assembly",
"os": "ubuntu-latest",
// Build a native 32bit binary in stage0 and use it to compile the oleans and the wasm build
"CMAKE_OPTIONS": "-DCMAKE_C_COMPILER_WORKS=1 -DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_CMAKE_CXX_COMPILER=clang++ -DSTAGE0_CMAKE_C_COMPILER=clang -DSTAGE0_CMAKE_EXECUTABLE_SUFFIX=\"\" -DUSE_GMP=OFF -DMMAP=OFF -DSTAGE0_MMAP=OFF -DCMAKE_AR=../emsdk/emsdk-main/upstream/emscripten/emar -DCMAKE_TOOLCHAIN_FILE=../emsdk/emsdk-main/upstream/emscripten/cmake/Modules/Platform/Emscripten.cmake -DLEAN_INSTALL_SUFFIX=-linux_wasm32 -DSTAGE0_CMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/",
"wasm": true,
"cmultilib": true,
"release": true,
"check-level": 2,
"cross": true,
"shell": "bash -euxo pipefail {0}",
// Just a few selected tests because wasm is slow
"CTEST_OPTIONS": "-R \"leantest_1007\\.lean|leantest_Format\\.lean|leanruntest\\_1037.lean|leanruntest_ac_rfl\\.lean|leanruntest_tempfile.lean\\.|leanruntest_libuv\\.lean\""
}
];
console.log(`matrix:\n${JSON.stringify(matrix, null, 2)}`)
return matrix.filter((job) => level >= job["check-level"])
build:
needs: [configure]
if: github.event_name != 'schedule' || github.repository == 'leanprover/lean4'
@@ -274,7 +251,7 @@ jobs:
runs-on: ${{ matrix.os }}
defaults:
run:
shell: ${{ matrix.shell || 'nix develop -c bash -euxo pipefail {0}' }}
shell: ${{ matrix.shell || 'nix-shell --run "bash -euxo pipefail {0}"' }}
name: ${{ matrix.name }}
env:
# must be inside workspace
@@ -289,67 +266,63 @@ jobs:
CXX: c++
MACOSX_DEPLOYMENT_TARGET: 10.15
steps:
- name: Checkout
uses: actions/checkout@v3
with:
submodules: true
# 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: Install Nix
uses: DeterminateSystems/nix-installer-action@main
if: runner.os == 'Linux' && !matrix.cmultilib
uses: cachix/install-nix-action@v18
with:
install_url: https://releases.nixos.org/nix/nix-2.12.0/install
if: matrix.os == 'ubuntu-latest' && !matrix.cmultilib
- name: Install MSYS2
uses: msys2/setup-msys2@v2
with:
msystem: clang64
# `:` means do not prefix with msystem
pacboy: "make: python: cmake clang ccache gmp libuv git: zip: unzip: diffutils: binutils: tree: zstd tar:"
if: runner.os == 'Windows'
# `:p` means prefix with appropriate msystem prefix
pacboy: "make python cmake:p clang:p ccache:p gmp:p git zip unzip diffutils binutils tree zstd:p tar"
if: matrix.os == 'windows-2022'
- name: Install Brew Packages
run: |
brew install ccache tree zstd coreutils gmp libuv
if: runner.os == 'macOS'
- name: Checkout
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 }}
# Do check out some CI-relevant files from virtual merge commit to accommodate CI changes on
# master (as the workflow files themselves are always taken from the merge)
# (needs to be after "Install *" to use the right shell)
- name: CI Merge Checkout
run: |
git fetch --depth=1 origin ${{ github.sha }}
git checkout FETCH_HEAD flake.nix flake.lock
if: github.event_name == 'pull_request'
# (needs to be after "Checkout" so files don't get overridden)
brew install ccache tree zstd coreutils gmp
if: matrix.os == 'macos-latest'
- name: Setup emsdk
uses: mymindstorm/setup-emsdk@v14
uses: mymindstorm/setup-emsdk@v12
with:
version: 3.1.44
actions-cache-folder: emsdk
if: matrix.wasm
- name: Install 32bit c libs
run: |
sudo dpkg --add-architecture i386
sudo apt-get update
sudo apt-get install -y gcc-multilib g++-multilib ccache libuv1-dev:i386
sudo apt-get install -y gcc-multilib g++-multilib ccache
if: matrix.cmultilib
- name: Cache
uses: actions/cache@v4
uses: actions/cache@v3
with:
path: .ccache
key: ${{ matrix.name }}-build-v3-${{ github.event.pull_request.head.sha }}
key: ${{ matrix.name }}-build-v3-${{ github.sha }}
# fall back to (latest) previous cache
restore-keys: |
${{ matrix.name }}-build-v3
save-always: true
# open nix-shell once for initial setup
- name: Setup
run: |
ccache --zero-stats
if: runner.os == 'Linux'
- name: Set up NPROC
# open nix-shell once for initial setup
true
if: matrix.os == 'ubuntu-latest'
- name: Set up core dumps
run: |
echo "NPROC=$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4)" >> $GITHUB_ENV
mkdir -p $PWD/coredumps
# store in current directory, for easy uploading together with binary
echo $PWD/coredumps/%e.%p.%t | sudo tee /proc/sys/kernel/core_pattern
if: matrix.os == 'ubuntu-latest'
- name: Build
run: |
mkdir build
cd build
ulimit -c unlimited # coredumps
# arguments passed to `cmake`
# this also enables githash embedding into stage 1 library
OPTIONS=(-DCHECK_OLEAN_VERSION=ON)
@@ -375,19 +348,11 @@ jobs:
OPTIONS+=(-DLEAN_SPECIAL_VERSION_DESC=${{ needs.configure.outputs.LEAN_SPECIAL_VERSION_DESC }})
fi
# contortion to support empty OPTIONS with old macOS bash
cmake .. --preset ${{ matrix.CMAKE_PRESET || 'release' }} -B . ${{ matrix.CMAKE_OPTIONS }} ${OPTIONS[@]+"${OPTIONS[@]}"} -DLEAN_INSTALL_PREFIX=$PWD/..
time make -j$NPROC
- name: Install
run: |
make -C build install
cmake .. ${{ matrix.CMAKE_OPTIONS }} ${OPTIONS[@]+"${OPTIONS[@]}"} -DLEAN_INSTALL_PREFIX=$PWD/..
make -j4
make install
- name: Check Binaries
run: ${{ matrix.binary-check }} lean-*/bin/* || true
- name: Count binary symbols
run: |
for f in lean-*/bin/*; do
echo "$f: $(nm $f | grep " T " | wc -l) exported symbols"
done
if: matrix.name == 'Windows'
- name: List Install Tree
run: |
# omit contents of Init/, ...
@@ -403,7 +368,7 @@ jobs:
else
${{ matrix.tar || 'tar' }} cf - $dir | zstd -T0 --no-progress -o pack/$dir.tar.zst
fi
- uses: actions/upload-artifact@v4
- uses: actions/upload-artifact@v3
if: matrix.release
with:
name: build-${{ matrix.name }}
@@ -413,72 +378,78 @@ jobs:
build/stage1/bin/lean --stats src/Lean.lean
if: ${{ !matrix.cross }}
- name: Test
id: test
run: |
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) && needs.configure.outputs.check-level >= 1
- name: Test Summary
uses: test-summary/action@v2
with:
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'
cd build/stage1
ulimit -c unlimited # coredumps
# exclude nonreproducible test
ctest -j4 --output-on-failure ${{ matrix.CTEST_OPTIONS }} < /dev/null
if: (matrix.wasm || !matrix.cross) && needs.configure.outputs.quick == 'false'
- name: Check Test Binary
run: ${{ matrix.binary-check }} tests/compiler/534.lean.out
if: (!matrix.cross) && steps.test.conclusion != 'skipped'
if: ${{ !matrix.cross && needs.configure.outputs.quick == 'false' }}
- name: Build Stage 2
run: |
make -C build -j$NPROC stage2
cd build
ulimit -c unlimited # coredumps
make -j4 stage2
if: matrix.test-speedcenter
- name: Check Stage 3
run: |
make -C build -j$NPROC check-stage3
cd build
ulimit -c unlimited # coredumps
make -j4 check-stage3
if: matrix.test-speedcenter
- name: Test Speedcenter Benchmarks
run: |
# Necessary for some timing metrics but does not work on Namespace runners
# and we just want to test that the benchmarks run at all here
#echo -1 | sudo tee /proc/sys/kernel/perf_event_paranoid
echo -1 | sudo tee /proc/sys/kernel/perf_event_paranoid
export BUILD=$PWD/build PATH=$PWD/build/stage1/bin:$PATH
cd tests/bench
nix shell .#temci -c temci exec --config speedcenter.yaml --included_blocks fast --runs 1
if: matrix.test-speedcenter
- name: Check rebootstrap
run: |
# clean rebuild in case of Makefile changes
make -C build update-stage0 && rm -rf build/stage* && make -C build -j$NPROC
if: matrix.name == 'Linux' && needs.configure.outputs.check-level >= 1
cd build
ulimit -c unlimited # coredumps
make update-stage0 && make -j4
if: matrix.name == 'Linux' && needs.configure.outputs.quick == 'false'
- name: CCache stats
run: ccache -s
- name: Show stacktrace for coredumps
if: ${{ failure() && matrix.os == 'ubuntu-latest' }}
run: |
for c in coredumps/*; do
progbin="$(file $c | sed "s/.*execfn: '\([^']*\)'.*/\1/")"
echo bt | $GDB/bin/gdb -q $progbin $c || true
done
- name: Upload coredumps
uses: actions/upload-artifact@v3
if: ${{ failure() && matrix.os == 'ubuntu-latest' }}
with:
name: coredumps-${{ matrix.name }}
path: |
./coredumps
./build/stage0/bin/lean
./build/stage0/lib/lean/libleanshared.so
./build/stage1/bin/lean
./build/stage1/lib/lean/libleanshared.so
./build/stage2/bin/lean
./build/stage2/lib/lean/libleanshared.so
# This job collects results from all the matrix jobs
# This can be made the "required" job, instead of listing each
# This can be made the required job, instead of listing each
# matrix job separately
all-done:
name: Build matrix complete
runs-on: ubuntu-latest
needs: build
# mark as merely cancelled not failed if builds are cancelled
if: ${{ !cancelled() }}
if: ${{ always() }}
steps:
- if: ${{ contains(needs.*.result, 'failure') && github.repository == 'leanprover/lean4' && github.ref_name == 'master' }}
uses: zulip/github-actions-zulip/send-message@v1
with:
api-key: ${{ secrets.ZULIP_BOT_KEY }}
email: "github-actions-bot@lean-fro.zulipchat.com"
organization-url: "https://lean-fro.zulipchat.com"
to: "infrastructure"
topic: "Github actions"
type: "stream"
content: |
A build of `${{ github.ref_name }}`, triggered by event `${{ github.event_name }}`, [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}).
- if: contains(needs.*.result, 'failure')
- if: contains(needs.*.result, 'failure') || contains(needs.*.result, 'cancelled')
uses: actions/github-script@v7
with:
script: |
core.setFailed('Some jobs failed')
# This job creates releases from tags
# (whether they are "unofficial" releases for experiments, or official releases when the tag is "v" followed by a semver string.)
# We do not attempt to automatically construct a changelog here:
@@ -488,22 +459,16 @@ jobs:
runs-on: ubuntu-latest
needs: build
steps:
- uses: actions/download-artifact@v4
- uses: actions/download-artifact@v3
with:
path: artifacts
- name: Release
uses: softprops/action-gh-release@v2
uses: softprops/action-gh-release@v1
with:
files: artifacts/*/*
fail_on_unmatched_files: true
prerelease: ${{ !startsWith(github.ref, 'refs/tags/v') || contains(github.ref, '-rc') }}
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
- name: Update release.lean-lang.org
run: |
gh workflow -R leanprover/release-index run update-index.yml
env:
GITHUB_TOKEN: ${{ secrets.RELEASE_INDEX_TOKEN }}
# This job creates nightly releases during the cron job.
# It is responsible for creating the tag, and automatically generating a changelog.
@@ -513,12 +478,12 @@ jobs:
runs-on: ubuntu-latest
steps:
- name: Checkout
uses: actions/checkout@v4
uses: actions/checkout@v3
with:
# needed for tagging
fetch-depth: 0
token: ${{ secrets.PUSH_NIGHTLY_TOKEN }}
- uses: actions/download-artifact@v4
- uses: actions/download-artifact@v3
with:
path: artifacts
- name: Prepare Nightly Release
@@ -536,7 +501,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@v2
uses: softprops/action-gh-release@v1
with:
body_path: diff.md
prerelease: true
@@ -546,13 +511,3 @@ jobs:
repository: ${{ github.repository_owner }}/lean4-nightly
env:
GITHUB_TOKEN: ${{ secrets.PUSH_NIGHTLY_TOKEN }}
- name: Update release.lean-lang.org
run: |
gh workflow -R leanprover/release-index run update-index.yml
env:
GITHUB_TOKEN: ${{ secrets.RELEASE_INDEX_TOKEN }}
- name: Update toolchain on mathlib4's nightly-testing branch
run: |
gh workflow -R leanprover-community/mathlib4 run nightly_bump_toolchain.yml
env:
GITHUB_TOKEN: ${{ secrets.MATHLIB4_BOT }}

View File

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

View File

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

View File

@@ -1,7 +1,6 @@
# This workflow allows any user to add one of the `awaiting-review`, `awaiting-author`, `WIP`,
# or `release-ci` labels by commenting on the PR or issue.
# If any labels from the set {`awaiting-review`, `awaiting-author`, `WIP`} are added, other labels
# from that set are removed automatically at the same time.
# This workflow allows any user to add one of the `awaiting-review`, `awaiting-author`, or `WIP` labels,
# by commenting on the PR or issue.
# Other labels from this set are removed automatically at the same time.
name: Label PR based on Comment
@@ -11,7 +10,7 @@ on:
jobs:
update-label:
if: github.event.issue.pull_request != null && (contains(github.event.comment.body, 'awaiting-review') || contains(github.event.comment.body, 'awaiting-author') || contains(github.event.comment.body, 'WIP') || contains(github.event.comment.body, 'release-ci'))
if: github.event.issue.pull_request != null && (contains(github.event.comment.body, 'awaiting-review') || contains(github.event.comment.body, 'awaiting-author') || contains(github.event.comment.body, 'WIP'))
runs-on: ubuntu-latest
steps:
@@ -26,7 +25,6 @@ jobs:
const awaitingReview = commentLines.includes('awaiting-review');
const awaitingAuthor = commentLines.includes('awaiting-author');
const wip = commentLines.includes('WIP');
const releaseCI = commentLines.includes('release-ci');
if (awaitingReview || awaitingAuthor || wip) {
await github.rest.issues.removeLabel({ owner, repo, issue_number, name: 'awaiting-review' }).catch(() => {});
@@ -43,7 +41,3 @@ jobs:
if (wip) {
await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['WIP'] });
}
if (releaseCI) {
await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['release-ci'] });
}

View File

@@ -13,36 +13,18 @@ concurrency:
cancel-in-progress: true
jobs:
# see ci.yml
configure:
runs-on: ubuntu-latest
outputs:
matrix: ${{ steps.set-matrix.outputs.result }}
steps:
- name: Configure build matrix
id: set-matrix
uses: actions/github-script@v7
with:
script: |
let large = ${{ github.repository == 'leanprover/lean4' }};
let matrix = [
{
"name": "Nix Linux",
"os": large ? "nscloud-ubuntu-22.04-amd64-8x8" : "ubuntu-latest",
}
];
console.log(`matrix:\n${JSON.stringify(matrix, null, 2)}`);
return matrix;
Build:
needs: [configure]
runs-on: ${{ matrix.os }}
defaults:
run:
shell: nix run .#ciShell -- bash -euxo pipefail {0}
strategy:
matrix:
include: ${{fromJson(needs.configure.outputs.matrix)}}
include:
- name: Nix Linux
os: ubuntu-latest
#- name: Nix macOS
# os: macos-latest
# complete all jobs
fail-fast: false
name: ${{ matrix.name }}
@@ -50,19 +32,18 @@ jobs:
NIX_BUILD_ARGS: --print-build-logs --fallback
steps:
- name: Checkout
uses: actions/checkout@v4
uses: actions/checkout@v3
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: Set Up Nix Cache
uses: actions/cache@v4
uses: actions/cache@v3
with:
path: nix-store-cache
key: ${{ matrix.name }}-nix-store-cache-${{ github.sha }}
# fall back to (latest) previous cache
restore-keys: |
${{ matrix.name }}-nix-store-cache
save-always: true
- name: Further Set Up Nix Cache
shell: bash -euxo pipefail {0}
run: |
@@ -79,37 +60,47 @@ jobs:
sudo mkdir -m0770 -p /nix/var/cache/ccache
sudo chown -R $USER /nix/var/cache/ccache
- name: Setup CCache Cache
uses: actions/cache@v4
uses: actions/cache@v3
with:
path: /nix/var/cache/ccache
key: ${{ matrix.name }}-nix-ccache-${{ github.sha }}
# fall back to (latest) previous cache
restore-keys: |
${{ matrix.name }}-nix-ccache
save-always: true
- name: Further Set Up CCache Cache
run: |
sudo chown -R root:nixbld /nix/var/cache
sudo chmod -R 770 /nix/var/cache
- name: Install Cachix
uses: cachix/cachix-action@v12
with:
name: lean4
authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
skipPush: true # we push specific outputs only
- name: Build
run: |
nix build $NIX_BUILD_ARGS .#cacheRoots -o push-build
- name: Test
run: |
nix build --keep-failed $NIX_BUILD_ARGS .#test -o push-test || (ln -s /tmp/nix-build-*/build/source/src/build ./push-test; false)
- name: Test Summary
uses: test-summary/action@v2
with:
paths: push-test/test-results.xml
if: always()
continue-on-error: true
nix build $NIX_BUILD_ARGS .#test -o push-test
- name: Build manual
run: |
nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc#{lean-mdbook,leanInk,alectryon,inked} -o push-doc
nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc#{lean-mdbook,leanInk,alectryon,test,inked} -o push-doc
nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc
# https://github.com/netlify/cli/issues/1809
cp -r --dereference ./result ./dist
if: matrix.name == 'Nix Linux'
- name: Check manual for broken links
id: lychee
uses: lycheeverse/lychee-action@v1.9.0
with:
fail: false # report errors but do not block CI on temporary failures
# gmplib.org consistently times out from GH actions
# the GitHub token is to avoid rate limiting
args: --base './dist' --no-progress --github-token ${{ secrets.GITHUB_TOKEN }} --exclude 'gmplib.org' './dist/**/*.html'
- name: Push to Cachix
run: |
[ -z "${{ secrets.CACHIX_AUTH_TOKEN }}" ] || cachix push -j4 lean4 ./push-* || true
- name: Rebuild Nix Store Cache
run: |
rm -rf nix-store-cache || true
@@ -121,7 +112,7 @@ jobs:
python3 -c 'import base64; print("alias="+base64.urlsafe_b64encode(bytes.fromhex("${{github.sha}}")).decode("utf-8").rstrip("="))' >> "$GITHUB_OUTPUT"
echo "message=`git log -1 --pretty=format:"%s"`" >> "$GITHUB_OUTPUT"
- name: Publish manual to Netlify
uses: nwtgck/actions-netlify@v3.0
uses: nwtgck/actions-netlify@v2.0
id: publish-manual
with:
publish-dir: ./dist
@@ -140,3 +131,5 @@ jobs:
- name: Fixup CCache Cache
run: |
sudo chown -R $USER /nix/var/cache
- name: CCache stats
run: CCACHE_DIR=/nix/var/cache/ccache nix run .#nixpkgs.ccache -- -s

View File

@@ -1,25 +0,0 @@
name: Check PR body for changelog convention
on:
merge_group:
pull_request:
types: [opened, synchronize, reopened, edited, labeled, converted_to_draft, ready_for_review]
jobs:
check-pr-body:
runs-on: ubuntu-latest
steps:
- name: Check PR body
if: github.event_name == 'pull_request'
uses: actions/github-script@v7
with:
script: |
const { title, body, labels, draft } = context.payload.pull_request;
if (!draft && /^(feat|fix):/.test(title) && !labels.some(label => label.name == "changelog-no")) {
if (!labels.some(label => label.name.startsWith("changelog-"))) {
core.setFailed('feat/fix PR must have a `changelog-*` label');
}
if (!/^This PR [^<]/.test(body)) {
core.setFailed('feat/fix PR must have changelog summary starting with "This PR ..." as first line.');
}
}

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@v6 # https://github.com/marketplace/actions/download-workflow-artifact
uses: dawidd6/action-download-artifact@v2 # https://github.com/marketplace/actions/download-workflow-artifact
with:
run_id: ${{ github.event.workflow_run.id }}
path: artifacts
@@ -60,7 +60,7 @@ jobs:
GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
- name: Release
if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
uses: softprops/action-gh-release@v2
uses: softprops/action-gh-release@v1
with:
name: Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }}
# There are coredumps files here as well, but all in deeper subdirectories.
@@ -75,7 +75,7 @@ jobs:
- name: Report release status
if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
uses: actions/github-script@v7
uses: actions/github-script@v6
with:
script: |
await github.rest.repos.createCommitStatus({
@@ -111,7 +111,7 @@ jobs:
- name: 'Setup jq'
if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
uses: dcarbone/install-jq-action@v2.1.0
uses: dcarbone/install-jq-action@v1.0.1
# Check that the most recently nightly coincides with 'git merge-base HEAD master'
- name: Check merge-base and nightly-testing-YYYY-MM-DD
@@ -126,22 +126,24 @@ jobs:
if [ "$NIGHTLY_SHA" = "$MERGE_BASE_SHA" ]; then
echo "The merge base of this PR coincides with the nightly release"
BATTERIES_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/batteries.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
MATHLIB_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/mathlib4.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
if [[ -n "$BATTERIES_REMOTE_TAGS" ]]; then
echo "... and Batteries has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
if [[ -n "$MATHLIB_REMOTE_TAGS" ]]; then
echo "... and Mathlib has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
MESSAGE=""
if [[ -n "$MATHLIB_REMOTE_TAGS" ]]; then
echo "... and Mathlib has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
else
echo "... but Mathlib does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
MESSAGE="- ❗ Mathlib CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Mathlib CI should run now."
fi
else
echo "... 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."
echo "... but Mathlib does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
MESSAGE="- ❗ Mathlib CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Mathlib CI should run now."
fi
STD_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover/std4.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
if [[ -n "$STD_REMOTE_TAGS" ]]; then
echo "... and Std has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
MESSAGE=""
else
echo "... but Std does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
MESSAGE="- ❗ Std 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\`, Std CI should run now."
fi
else
@@ -149,9 +151,7 @@ jobs:
echo "but 'git merge-base origin/master HEAD' reported: $MERGE_BASE_SHA"
git -C lean4.git log -10 origin/master
git -C lean4.git fetch origin nightly-with-mathlib
NIGHTLY_WITH_MATHLIB_SHA="$(git -C lean4.git rev-parse "origin/nightly-with-mathlib")"
MESSAGE="- ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch. Try \`git rebase $MERGE_BASE_SHA --onto $NIGHTLY_WITH_MATHLIB_SHA\`."
MESSAGE="- ❗ Std/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch."
fi
if [[ -n "$MESSAGE" ]]; then
@@ -163,11 +163,10 @@ jobs:
# 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.MATHLIB4_COMMENT_BOT }}" \
existing_comment="$(curl -L -s -H "Authorization: token ${{ secrets.MATHLIB4_BOT }}" \
-H "Accept: application/vnd.github.v3+json" \
"https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments" \
| jq 'first(.[] | select(.body | test("^- . Mathlib") or startswith("Mathlib CI status")) | select(.user.login == "leanprover-community-bot"))')"
| jq 'first(.[] | select(.body | test("^- . Mathlib") or startswith("Mathlib CI status")) | select(.user.login == "leanprover-community-mathlib4-bot"))')"
existing_comment_id="$(echo "$existing_comment" | jq -r .id)"
existing_comment_body="$(echo "$existing_comment" | jq -r .body)"
@@ -177,14 +176,14 @@ jobs:
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 MATHLIB4_COMMENT_BOT token here, so that Mathlib CI can subsequently edit the comment.
# It's essential we use the MATHLIB4_BOT token here, so that Mathlib CI can subsequently edit the comment.
if [ -z "$existing_comment_id" ]; then
INTRO="Mathlib CI status ([docs](https://leanprover-community.github.io/contribute/tags_and_branches.html)):"
# Post new comment with a bullet point
echo "Posting as new comment at leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments"
curl -L -s \
-X POST \
-H "Authorization: token ${{ secrets.MATHLIB4_COMMENT_BOT }}" \
-H "Authorization: token ${{ secrets.MATHLIB4_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"
@@ -193,7 +192,7 @@ jobs:
echo "Appending to existing comment at leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments"
curl -L -s \
-X PATCH \
-H "Authorization: token ${{ secrets.MATHLIB4_COMMENT_BOT }}" \
-H "Authorization: token ${{ secrets.MATHLIB4_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"
@@ -208,7 +207,7 @@ jobs:
- name: Report mathlib base
if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true' }}
uses: actions/github-script@v7
uses: actions/github-script@v6
with:
script: |
const description =
@@ -224,27 +223,27 @@ jobs:
description: description,
});
# We next automatically create a Batteries branch using this toolchain.
# Batteries doesn't itself have a mechanism to report results of CI from this branch back to Lean
# Instead this is taken care of by Mathlib CI, which will fail if Batteries fails.
# We next automatically create a Std branch using this toolchain.
# Std doesn't itself have a mechanism to report results of CI from this branch back to Lean
# Instead this is taken care of by Mathlib CI, which will fail if Std fails.
- name: Cleanup workspace
if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
run: |
sudo rm -rf ./*
# Checkout the Batteries repository with all branches
- name: Checkout Batteries repository
# Checkout the Std repository with all branches
- name: Checkout Std repository
if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
uses: actions/checkout@v4
uses: actions/checkout@v3
with:
repository: leanprover-community/batteries
repository: leanprover/std4
token: ${{ secrets.MATHLIB4_BOT }}
ref: nightly-testing
fetch-depth: 0 # This ensures we check out all tags and branches.
- name: Check if tag exists
if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
id: check_batteries_tag
id: check_std_tag
run: |
git config user.name "leanprover-community-mathlib4-bot"
git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com"
@@ -252,7 +251,7 @@ jobs:
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 "This shouldn't be possible: couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' tag at Batteries. Falling back to 'nightly-testing'."
echo "This shouldn't be possible: couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' tag at Std. Falling back to 'nightly-testing'."
BASE=nightly-testing
fi
@@ -269,7 +268,7 @@ jobs:
else
echo "Branch already exists, pushing an empty commit."
git switch lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
# The Batteries `nightly-testing` or `nightly-testing-YYYY-MM-DD` branch may have moved since this branch was created, so merge their changes.
# The Std `nightly-testing` or `nightly-testing-YYYY-MM-DD` branch may have moved since this branch was created, so merge their changes.
# (This should no longer be possible once `nightly-testing-YYYY-MM-DD` is a tag, but it is still safe to merge.)
git merge "$BASE" --strategy-option ours --no-commit --allow-unrelated-histories
git commit --allow-empty -m "Trigger CI for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
@@ -292,20 +291,13 @@ 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@v4
uses: actions/checkout@v3
with:
repository: leanprover-community/mathlib4
token: ${{ secrets.MATHLIB4_BOT }}
ref: nightly-testing
fetch-depth: 0 # This ensures we check out all tags and branches.
- name: install elan
run: |
set -o pipefail
curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
./elan-init -y --default-toolchain none
echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
- name: Check if tag exists
if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
id: check_mathlib_tag
@@ -329,18 +321,15 @@ jobs:
git switch -c lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} "$BASE"
echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}" > lean-toolchain
git add lean-toolchain
sed -i 's,require "leanprover-community" / "batteries" @ git ".\+",require "leanprover-community" / "batteries" @ git "lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}",' lakefile.lean
lake update batteries
git add lakefile.lean lake-manifest.json
sed -i "s/require std from git \"https:\/\/github.com\/leanprover\/std4\" @ \".\+\"/require std from git \"https:\/\/github.com\/leanprover\/std4\" @ \"nightly-testing-${MOST_RECENT_NIGHTLY}\"/" lakefile.lean
git add lakefile.lean
git commit -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
else
echo "Branch already exists, merging $BASE and bumping Batteries."
echo "Branch already exists, pushing an empty commit."
git switch lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
# The Mathlib `nightly-testing` branch or `nightly-testing-YYYY-MM-DD` tag may have moved since this branch was created, so merge their changes.
# (This should no longer be possible once `nightly-testing-YYYY-MM-DD` is a tag, but it is still safe to merge.)
git merge "$BASE" --strategy-option ours --no-commit --allow-unrelated-histories
lake update batteries
git add lake-manifest.json
git commit --allow-empty -m "Trigger CI for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
fi

View File

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

View File

@@ -11,7 +11,7 @@ jobs:
stale:
runs-on: ubuntu-latest
steps:
- uses: actions/stale@v9
- uses: actions/stale@v8
with:
days-before-stale: -1
days-before-pr-stale: 30

View File

@@ -23,7 +23,7 @@ jobs:
# This action should push to an otherwise protected branch, so it
# uses a deploy key with write permissions, as suggested at
# https://stackoverflow.com/a/76135647/946226
- uses: actions/checkout@v4
- uses: actions/checkout@v3
with:
ssh-key: ${{secrets.STAGE0_SSH_KEY}}
- run: echo "should_update_stage0=yes" >> "$GITHUB_ENV"
@@ -40,32 +40,18 @@ jobs:
run: |
git config --global user.name "Lean stage0 autoupdater"
git config --global user.email "<>"
- if: env.should_update_stage0 == 'yes'
uses: DeterminateSystems/nix-installer-action@main
# Would be nice, but does not work yet:
# https://github.com/DeterminateSystems/magic-nix-cache/issues/39
# This action does not run that often and building runs in a few minutes, so ok for now
#- if: env.should_update_stage0 == 'yes'
# uses: DeterminateSystems/magic-nix-cache-action@v2
- if: env.should_update_stage0 == 'yes'
name: Restore Build Cache
uses: actions/cache/restore@v4
name: Install Cachix
uses: cachix/cachix-action@v12
with:
path: nix-store-cache
key: Nix Linux-nix-store-cache-${{ github.sha }}
# fall back to (latest) previous cache
restore-keys: |
Nix Linux-nix-store-cache
- if: env.should_update_stage0 == 'yes'
name: Further Set Up Nix Cache
shell: bash -euxo pipefail {0}
run: |
# Nix seems to mutate the cache, so make a copy
cp -r nix-store-cache nix-store-cache-copy || true
- if: env.should_update_stage0 == 'yes'
name: Install Nix
uses: DeterminateSystems/nix-installer-action@main
with:
extra-conf: |
substituters = file://${{ github.workspace }}/nix-store-cache-copy?priority=10&trusted=true https://cache.nixos.org
name: lean4
- if: env.should_update_stage0 == 'yes'
run: nix run .#update-stage0-commit
- if: env.should_update_stage0 == 'yes'

6
.gitignore vendored
View File

@@ -4,10 +4,8 @@
*.lock
.lake
lake-manifest.json
/build
/src/lakefile.toml
/tests/lakefile.toml
/lakefile.toml
build
!/src/lake/Lake/Build
GPATH
GRTAGS
GSYMS

View File

@@ -30,35 +30,6 @@ if(NOT (DEFINED STAGE0_CMAKE_EXECUTABLE_SUFFIX))
set(STAGE0_CMAKE_EXECUTABLE_SUFFIX "${CMAKE_EXECUTABLE_SUFFIX}")
endif()
# Don't do anything with cadical on wasm
if (NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
# On CI Linux, we source cadical from Nix instead; see flake.nix
find_program(CADICAL cadical)
if(NOT CADICAL)
set(CADICAL_CXX c++)
find_program(CCACHE ccache)
if(CCACHE)
set(CADICAL_CXX "${CCACHE} ${CADICAL_CXX}")
endif()
# missing stdio locking API on Windows
if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
string(APPEND CADICAL_CXXFLAGS " -DNUNLOCKED")
endif()
ExternalProject_add(cadical
PREFIX cadical
GIT_REPOSITORY https://github.com/arminbiere/cadical
GIT_TAG rel-1.9.5
CONFIGURE_COMMAND ""
# https://github.com/arminbiere/cadical/blob/master/BUILD.md#manual-build
BUILD_COMMAND $(MAKE) -f ${CMAKE_SOURCE_DIR}/src/cadical.mk CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX} CXX=${CADICAL_CXX} CXXFLAGS=${CADICAL_CXXFLAGS}
BUILD_IN_SOURCE ON
INSTALL_COMMAND "")
set(CADICAL ${CMAKE_BINARY_DIR}/cadical/cadical${CMAKE_EXECUTABLE_SUFFIX} CACHE FILEPATH "path to cadical binary" FORCE)
set(EXTRA_DEPENDS "cadical")
endif()
list(APPEND CL_ARGS -DCADICAL=${CADICAL})
endif()
ExternalProject_add(stage0
SOURCE_DIR "${LEAN_SOURCE_DIR}/stage0"
SOURCE_SUBDIR src
@@ -107,10 +78,6 @@ add_custom_target(update-stage0
COMMAND $(MAKE) -C stage1 update-stage0
DEPENDS stage1)
add_custom_target(update-stage0-commit
COMMAND $(MAKE) -C stage1 update-stage0-commit
DEPENDS stage1)
add_custom_target(test
COMMAND $(MAKE) -C stage1 test
DEPENDS stage1)

View File

@@ -1,83 +0,0 @@
{
"version": 2,
"cmakeMinimumRequired": {
"major": 3,
"minor": 10,
"patch": 0
},
"configurePresets": [
{
"name": "release",
"displayName": "Default development optimized build config",
"generator": "Unix Makefiles",
"binaryDir": "${sourceDir}/build/release"
},
{
"name": "debug",
"displayName": "Debug build config",
"cacheVariables": {
"CMAKE_BUILD_TYPE": "Debug"
},
"generator": "Unix Makefiles",
"binaryDir": "${sourceDir}/build/debug"
},
{
"name": "sanitize",
"displayName": "Sanitize build config",
"cacheVariables": {
"LEAN_EXTRA_CXX_FLAGS": "-fsanitize=address,undefined",
"LEANC_EXTRA_FLAGS": "-fsanitize=address,undefined -fsanitize-link-c++-runtime",
"SMALL_ALLOCATOR": "OFF",
"BSYMBOLIC": "OFF"
},
"generator": "Unix Makefiles",
"binaryDir": "${sourceDir}/build/sanitize"
},
{
"name": "sandebug",
"inherits": ["debug", "sanitize"],
"displayName": "Sanitize+debug build config",
"binaryDir": "${sourceDir}/build/sandebug"
}
],
"buildPresets": [
{
"name": "release",
"configurePreset": "release"
},
{
"name": "debug",
"configurePreset": "debug"
},
{
"name": "sanitize",
"configurePreset": "sanitize"
},
{
"name": "sandebug",
"configurePreset": "sandebug"
}
],
"testPresets": [
{
"name": "release",
"configurePreset": "release",
"output": {"outputOnFailure": true, "shortProgress": true}
},
{
"name": "debug",
"configurePreset": "debug",
"inherits": "release"
},
{
"name": "sanitize",
"configurePreset": "sanitize",
"inherits": "release"
},
{
"name": "sandebug",
"configurePreset": "sandebug",
"inherits": "release"
}
]
}

View File

@@ -4,45 +4,19 @@
# Listed persons will automatically be asked by GitHub to review a PR touching these paths.
# If multiple names are listed, a review by any of them is considered sufficient by default.
/.github/ @Kha @kim-em
/RELEASES.md @kim-em
/.github/ @Kha @semorrison
/RELEASES.md @semorrison
/src/ @leodemoura @Kha
/src/Init/IO.lean @joehendrix
/src/kernel/ @leodemoura
/src/lake/ @tydeu
/src/Lean/Compiler/ @leodemoura
/src/Lean/Data/Lsp/ @mhuisi
/src/Lean/Elab/Deriving/ @kim-em
/src/Lean/Elab/Tactic/ @kim-em
/src/Lean/Language/ @Kha
/src/Lean/Elab/Deriving/ @semorrison
/src/Lean/Elab/Tactic/ @semorrison
/src/Lean/Meta/Tactic/ @leodemoura
/src/Lean/Parser/ @Kha
/src/Lean/PrettyPrinter/ @Kha
/src/Lean/PrettyPrinter/Delaborator/ @kmill
/src/Lean/Server/ @mhuisi
/src/Lean/Widget/ @Vtec234
/src/Init/Data/ @kim-em
/src/Init/Data/Array/Lemmas.lean @digama0
/src/Init/Data/List/Lemmas.lean @digama0
/src/Init/Data/List/BasicAux.lean @digama0
/src/Init/Data/Array/Subarray.lean @david-christiansen
/src/Lean/Elab/Tactic/RCases.lean @digama0
/src/Init/RCases.lean @digama0
/src/Lean/Elab/Tactic/Ext.lean @digama0
/src/Init/Ext.lean @digama0
/src/Lean/Elab/Tactic/Simpa.lean @digama0
/src/Lean/Elab/Tactic/NormCast.lean @digama0
/src/Lean/Meta/Tactic/NormCast.lean @digama0
/src/Lean/Meta/Tactic/TryThis.lean @digama0
/src/Lean/Elab/Tactic/SimpTrace.lean @digama0
/src/Lean/Elab/Tactic/NoMatch.lean @digama0
/src/Lean/Elab/Tactic/ShowTerm.lean @digama0
/src/Lean/Elab/Tactic/Repeat.lean @digama0
/src/Lean/Meta/Tactic/Repeat.lean @digama0
/src/Lean/Meta/CoeAttr.lean @digama0
/src/Lean/Elab/GuardMsgs.lean @digama0
/src/Lean/Elab/Tactic/Guard.lean @digama0
/src/Init/Guard.lean @digama0
/src/Lean/Server/CodeActions/ @digama0
/src/Std/ @TwoFX
/src/Std/Tactic/BVDecide/ @hargoniX
/src/Lean/Elab/Tactic/BVDecide/ @hargoniX
/src/Std/Sat/ @hargoniX
/src/runtime/io.cpp @joehendrix

View File

@@ -63,20 +63,6 @@ Because the change will be squashed, there is no need to polish the commit messa
Reviews and Feedback:
----
The lean4 repo is managed by the Lean FRO's *triage team* that aims to provide initial feedback on new bug reports, PRs, and RFCs weekly.
This feedback generally consists of prioritizing the ticket using one of the following categories:
* label `P-high`: We will work on this issue
* label `P-medium`: We may work on this issue if we find the time
* label `P-low`: We are not planning to work on this issue
* *closed*: This issue is already fixed, it is not an issue, or is not sufficiently compatible with our roadmap for the project and we will not work on it nor accept external contributions on it
For *bug reports*, the listed priority reflects our commitment to fixing the issue.
It is generally indicative but not necessarily identical to the priority an external contribution addressing this bug would receive.
For *PRs* and *RFCs*, the priority reflects our commitment to reviewing them and getting them to an acceptable state.
Accepted RFCs are marked with the label `RFC accepted` and afterwards assigned a new "implementation" priority as with bug reports.
General guidelines for interacting with reviews and feedback:
**Be Patient**: Given the limited number of full-time maintainers and the volume of PRs, reviews may take some time.
**Engage Constructively**: Always approach feedback positively and constructively. Remember, reviews are about ensuring the best quality for the project, not personal criticism.

View File

@@ -1341,33 +1341,3 @@ whether future versions of the GNU Lesser General Public License shall
apply, that proxy's public statement of acceptance of any version is
permanent authorization for you to choose that version for the
Library.
==============================================================================
CaDiCaL is under the MIT License:
==============================================================================
MIT License
Copyright (c) 2016-2021 Armin Biere, Johannes Kepler University Linz, Austria
Copyright (c) 2020-2021 Mathias Fleury, Johannes Kepler University Linz, Austria
Copyright (c) 2020-2021 Nils Froleyks, Johannes Kepler University Linz, Austria
Copyright (c) 2022-2024 Katalin Fazekas, Vienna University of Technology, Austria
Copyright (c) 2021-2024 Armin Biere, University of Freiburg, Germany
Copyright (c) 2021-2024 Mathias Fleury, University of Freiburg, Germany
Copyright (c) 2023-2024 Florian Pollitt, University of Freiburg, Germany
Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all
copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
SOFTWARE.

View File

@@ -22,4 +22,4 @@ Please read our [Contribution Guidelines](CONTRIBUTING.md) first.
# Building from Source
See [Building Lean](https://lean-lang.org/lean4/doc/make/index.html) (documentation source: [doc/make/index.md](doc/make/index.md)).
See [Building Lean](https://lean-lang.org/lean4/doc/make/index.html).

File diff suppressed because it is too large Load Diff

View File

@@ -1 +0,0 @@
[0829/202002.254:ERROR:crashpad_client_win.cc(868)] not connected

9
default.nix Normal file
View File

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

View File

@@ -1,4 +1,4 @@
open Batteries
open Std
open Lean
inductive BoolExpr where

View File

@@ -89,6 +89,5 @@
- [Testing](./dev/testing.md)
- [Debugging](./dev/debugging.md)
- [Commit Convention](./dev/commit_convention.md)
- [Release checklist](./dev/release_checklist.md)
- [Building This Manual](./dev/mdbook.md)
- [Foreign Function Interface](./dev/ffi.md)

View File

@@ -1,11 +1 @@
# Characters
A value of type `Char`, also known as a character, is a [Unicode scalar value](https://www.unicode.org/glossary/#unicode_scalar_value). It is represented using an unsigned 32-bit integer and is statically guaranteed to be a valid Unicode scalar value.
Syntactically, character literals are enclosed in single quotes.
```lean
#eval 'a' -- 'a'
#eval '' -- '∀'
```
Characters are ordered and can be decidably compared using the relational operators `=`, `<`, `≤`, `>`, `≥`.

View File

@@ -73,30 +73,28 @@ 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.
If you have write access to the lean4 repository, you can also manually
If you have write access to the lean4 repository, you can also 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>
You can do that on <https://github.com/nomeata/lean4/actions/workflows/update-stage0.yml>
or using Github CLI with
```
gh workflow run update-stage0.yml
```
Leaving stage0 updates to the CI automation is preferable, but should you need
to do it locally, you can use `make 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.
If you rebased the branch (either onto a newer version of `master`, or fixing
up some commits prior to the stage0 update, recreate the stage0 update commits.
The script `script/rebase-stage0.sh` can be used for that.
The CI should prevent PRs with changes to stage0 (besides `stdlib_flags.h`)
from entering `master` through the (squashing!) merge queue, and label such PRs
with the `changes-stage0` label. Such PRs should have a cleaned up history,
with separate stage0 update commits; then coordinate with the admins to merge
your PR using rebase merge, bypassing the merge queue.
Leaving stage0 updates to the CI automation is preferrable, but should you need
to do it locally, you can use `make update-stage0` in `build/release`, to
update `stage0` from `stage1`, `make -C stageN update-stage0` to update from
another stage, or `nix run .#update-stage0-commit` to update using nix.
Updates to `stage0` should be their own commits in the Git history. So should
you have to include the stage0 update in your PR (rather than using above
automation after merging changes), commit your work before running `make
update-stage0`, commit the updated `stage0` compiler code with the commit
message:
```
chore: update stage0
```
and coordinate with the admins to not squash your PR.
## Further Bootstrapping Complications

View File

@@ -5,7 +5,7 @@ Some notes on how to debug Lean, which may also be applicable to debugging Lean
## Tracing
In `CoreM` and derived monads, we use `trace[traceCls] "msg with {interpolations}"` to fill the structured trace viewable with `set_option trace.traceCls true`.
In `CoreM` and derived monads, we use `trace![traceCls] "msg with {interpolations}"` to fill the structured trace viewable with `set_option trace.traceCls true`.
New trace classes have to be registered using `registerTraceClass` first.
Notable trace classes:
@@ -22,9 +22,7 @@ Notable trace classes:
In pure contexts or when execution is aborted before the messages are finally printed, one can instead use the term `dbg_trace "msg with {interpolations}"; val` (`;` can also be replaced by a newline), which will print the message to stderr before evaluating `val`. `dbgTraceVal val` can be used as a shorthand for `dbg_trace "{val}"; val`.
Note that if the return value is not actually used, the trace code is silently dropped as well.
By default, such stderr output is buffered and shown as messages after a command has been elaborated, which is necessary to ensure deterministic ordering of messages under parallelism.
If Lean aborts the process before it can finish the command or takes too long to do that, using `-DstderrAsMessages=false` avoids this buffering and shows `dbg_trace` output (but not `trace`s or other diagnostics) immediately.
In the language server, stderr output is buffered and shown as messages after a command has been elaborated, unless the option `server.stderrAsMessages` is deactivated.
## Debuggers

View File

@@ -53,59 +53,10 @@ In the case of `@[extern]` all *irrelevant* types are removed first; see next se
Its runtime value is either a pointer to an opaque bignum object or, if the lowest bit of the "pointer" is 1 (`lean_is_scalar`), an encoded unboxed natural number (`lean_box`/`lean_unbox`).
* A universe `Sort u`, type constructor `... → Sort u`, or proposition `p : Prop` is *irrelevant* and is either statically erased (see above) or represented as a `lean_object *` with the runtime value `lean_box(0)`
* Any other type is represented by `lean_object *`.
Its runtime value is a pointer to an object of a subtype of `lean_object` (see the "Inductive types" section below) or the unboxed value `lean_box(cidx)` for the `cidx`th constructor of an inductive type if this constructor does not have any relevant parameters.
Its runtime value is a pointer to an object of a subtype of `lean_object` (see respective declarations in `lean.h`) or the unboxed value `lean_box(cidx)` for the `cidx`th constructor of an inductive type if this constructor does not have any relevant parameters.
Example: the runtime value of `u : Unit` is always `lean_box(0)`.
#### Inductive types
For inductive types which are in the fallback `lean_object *` case above and not trivial constructors, the type is stored as a `lean_ctor_object`, and `lean_is_ctor` will return true. A `lean_ctor_object` stores the constructor index in the header, and the fields are stored in the `m_objs` portion of the object.
The memory order of the fields is derived from the types and order of the fields in the declaration. They are ordered as follows:
* Non-scalar fields stored as `lean_object *`
* Fields of type `USize`
* Other scalar fields, in decreasing order by size
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.
* To access other scalar fields, use `lean_ctor_get_uintN(val, off)` or `lean_ctor_get_usize(val, off)` as appropriate. Here `off` is the byte offset of the field in the structure, starting at `n*sizeof(void*)` where `n` is the number of fields of the first two kinds.
For example, a structure such as
```lean
structure S where
ptr_1 : Array Nat
usize_1 : USize
sc64_1 : UInt64
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_3 : UInt64
usize_2 : USize
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.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
By default, all `lean_object *` parameters of an `@[extern]` function are considered *owned*, i.e. the external code is passed a "virtual RC token" and is responsible for passing this token along to another consuming function (exactly once) or freeing it via `lean_dec`.
@@ -160,15 +111,6 @@ if (lean_io_result_is_ok(res)) {
lean_io_mark_end_initialization();
```
In addition, any other thread not spawned by the Lean runtime itself must be initialized for Lean use by calling
```c
void lean_initialize_thread();
```
and should be finalized in order to free all thread-local resources by calling
```c
void lean_finalize_thread();
```
## `@[extern]` in the Interpreter
The interpreter can run Lean declarations for which symbols are available in loaded shared libraries, which includes `@[extern]` declarations.

View File

@@ -74,9 +74,3 @@ Lean's build process uses [`ccache`](https://ccache.dev/) if it is
installed to speed up recompilation of the generated C code. Without
`ccache`, you'll likely spend more time than necessary waiting on
rebuilds - it's a good idea to make sure it's installed.
### `prelude`
Unlike most Lean projects, all submodules of the `Lean` module begin with the
`prelude` keyword. This disables the automated import of `Init`, meaning that
developers need to figure out their own subset of `Init` to import. This is done
such that changing files in `Init` doesn't force a full rebuild of `Lean`.

View File

@@ -1,262 +0,0 @@
# Releasing a stable version
This checklist walks you through releasing a stable version.
See below for the checklist for release candidates.
We'll use `v4.6.0` as the intended release version as a running example.
- One week before the planned release, ensure that
(1) someone has written the release notes and
(2) someone has written the first draft of the release blog post.
If there is any material in `./releases_drafts/` on the `releases/v4.6.0` branch, then the release notes are not done.
(See the section "Writing the release notes".)
- `git checkout releases/v4.6.0`
(This branch should already exist, from the release candidates.)
- `git pull`
- In `src/CMakeLists.txt`, verify you see
- `set(LEAN_VERSION_MINOR 6)` (for whichever `6` is appropriate)
- `set(LEAN_VERSION_IS_RELEASE 1)`
- (both of these should already be in place from the release candidates)
- `git tag v4.6.0`
- `git push $REMOTE v4.6.0`, where `$REMOTE` is the upstream Lean repository (e.g., `origin`, `upstream`)
- Now wait, while CI runs.
- You can monitor this at `https://github.com/leanprover/lean4/actions/workflows/ci.yml`,
looking for the `v4.6.0` tag.
- This step can take up to an hour.
- If you are intending to cut the next release candidate on the same day,
you may want to start on the release candidate checklist now.
- Go to https://github.com/leanprover/lean4/releases and verify that the `v4.6.0` release appears.
- Edit the release notes on Github to select the "Set as the latest release".
- Follow the instructions in creating a release candidate for the "GitHub release notes" step,
now that we have a written `RELEASES.md` section.
Do a quick sanity check.
- Next, we will move a curated list of downstream repos to the latest stable release.
- For each of the repositories listed below:
- Make a PR to `master`/`main` changing the toolchain to `v4.6.0`
- Update the toolchain file
- In the Lakefile, if there are dependencies on specific version tags of dependencies that you've already pushed as part of this process, update them to the new tag.
If they depend on `main` or `master`, don't change this; you've just updated the dependency, so it will work and be saved in the manifest
- Run `lake update`
- The PR title should be "chore: bump toolchain to v4.6.0".
- Merge the PR once CI completes.
- Create the tag `v4.6.0` from `master`/`main` and push it.
- Merge the tag `v4.6.0` into the `stable` branch and push it.
- We do this for the repositories:
- [lean4checker](https://github.com/leanprover/lean4checker)
- No dependencies
- Toolchain bump PR
- Create and push the tag
- Merge the tag into `stable`
- [Batteries](https://github.com/leanprover-community/batteries)
- No dependencies
- Toolchain bump PR
- Create and push the tag
- Merge the tag into `stable`
- [ProofWidgets4](https://github.com/leanprover-community/ProofWidgets4)
- Dependencies: `Batteries`
- Note on versions and branches:
- `ProofWidgets` uses a sequential version tagging scheme, e.g. `v0.0.29`,
which does not refer to the toolchain being used.
- Make a new release in this sequence after merging the toolchain bump PR.
- `ProofWidgets` does not maintain a `stable` branch.
- Toolchain bump PR
- Create and push the tag, following the version convention of the repository
- [Aesop](https://github.com/leanprover-community/aesop)
- Dependencies: `Batteries`
- Toolchain bump PR including updated Lake manifest
- Create and push the tag
- Merge the tag into `stable`
- [doc-gen4](https://github.com/leanprover/doc-gen4)
- Dependencies: exist, but they're not part of the release workflow
- Toolchain bump PR including updated Lake manifest
- Create and push the tag
- There is no `stable` branch; skip this step
- [Verso](https://github.com/leanprover/verso)
- Dependencies: exist, but they're not part of the release workflow
- The `SubVerso` dependency should be compatible with _every_ Lean release simultaneously, rather than following this workflow
- Toolchain bump PR including updated Lake manifest
- Create and push the tag
- There is no `stable` branch; skip this step
- [import-graph](https://github.com/leanprover-community/import-graph)
- Toolchain bump PR including updated Lake manifest
- Create and push the tag
- There is no `stable` branch; skip this step
- [Mathlib](https://github.com/leanprover-community/mathlib4)
- Dependencies: `Aesop`, `ProofWidgets4`, `lean4checker`, `Batteries`, `doc-gen4`, `import-graph`
- Toolchain bump PR notes:
- In addition to updating the `lean-toolchain` and `lakefile.lean`,
in `.github/workflows/lean4checker.yml` update the line
`git checkout v4.6.0` to the appropriate tag.
- Push the PR branch to the main Mathlib repository rather than a fork, or CI may not work reliably
- Create and push the tag
- Create a new branch from the tag, push it, and open a pull request against `stable`.
Coordinate with a Mathlib maintainer to get this merged.
- [REPL](https://github.com/leanprover-community/repl)
- Dependencies: `Mathlib` (for test code)
- Note that there are two copies of `lean-toolchain`/`lakefile.lean`:
in the root, and in `test/Mathlib/`. Edit both, and run `lake update` in both directories.
- Toolchain bump PR including updated Lake manifest
- Create and push the tag
- Merge the tag into `stable`
- The `v4.6.0` section of `RELEASES.md` is out of sync between
`releases/v4.6.0` and `master`. This should be reconciled:
- Replace the `v4.6.0` section on `master` with the `v4.6.0` section on `releases/v4.6.0`
and commit this to `master`.
- Merge the release announcement PR for the Lean website - it will be deployed automatically
- Finally, make an announcement!
This should go in https://leanprover.zulipchat.com/#narrow/stream/113486-announce, with topic `v4.6.0`.
Please see previous announcements for suggested language.
You will want a few bullet points for main topics from the release notes.
Link to the blog post from the Zulip announcement.
- Make sure that whoever is handling social media knows the release is out.
## Optimistic(?) time estimates:
- Initial checks and push the tag: 30 minutes.
- Waiting for the release: 60 minutes.
- Fixing release notes: 10 minutes.
- Bumping toolchains in downstream repositories, up to creating the Mathlib PR: 30 minutes.
- Waiting for Mathlib CI and bors: 120 minutes.
- Finalizing Mathlib tags and stable branch, and updating REPL: 15 minutes.
- Posting announcement and/or blog post: 20 minutes.
# Creating a release candidate.
This checklist walks you through creating the first release candidate for a version of Lean.
We'll use `v4.7.0-rc1` as the intended release version in this example.
- Decide which nightly release you want to turn into a release candidate.
We will use `nightly-2024-02-29` in this example.
- It is essential that Batteries and Mathlib already have reviewed branches compatible with this nightly.
- Check that both Batteries and Mathlib's `bump/v4.7.0` branch contain `nightly-2024-02-29`
in their `lean-toolchain`.
- The steps required to reach that state are beyond the scope of this checklist, but see below!
- Create the release branch from this nightly tag:
```
git remote add nightly https://github.com/leanprover/lean4-nightly.git
git fetch nightly tag nightly-2024-02-29
git checkout nightly-2024-02-29
git checkout -b releases/v4.7.0
```
- In `RELEASES.md` replace `Development in progress` in the `v4.7.0` section with `Release notes to be written.`
- We will rely on automatically generated release notes for release candidates,
and the written release notes will be used for stable versions only.
It is essential to choose the nightly that will become the release candidate as early as possible, to avoid confusion.
- In `src/CMakeLists.txt`,
- verify that you see `set(LEAN_VERSION_MINOR 7)` (for whichever `7` is appropriate); this should already have been updated when the development cycle began.
- `set(LEAN_VERSION_IS_RELEASE 1)` (this should be a change; on `master` and nightly releases it is always `0`).
- Commit your changes to `src/CMakeLists.txt`, and push.
- `git tag v4.7.0-rc1`
- `git push origin v4.7.0-rc1`
- Ping the FRO Zulip that release notes need to be written. The release notes do not block completing the rest of this checklist.
- Now wait, while CI runs.
- You can monitor this at `https://github.com/leanprover/lean4/actions/workflows/ci.yml`, looking for the `v4.7.0-rc1` tag.
- This step can take up to an hour.
- (GitHub release notes) Once the release appears at https://github.com/leanprover/lean4/releases/
- Verify that the release is marked as a prerelease (this should have been done automatically by the CI release job).
- In the "previous tag" dropdown, select `v4.6.0`, and click "Generate release notes".
This will add a list of all the commits since the last stable version.
- Delete "update stage0" commits, and anything with a completely inscrutable commit message.
- Next, we will move a curated list of downstream repos to the release candidate.
- This assumes that for each repository either:
* There is already a *reviewed* branch `bump/v4.7.0` containing the required adaptations.
The preparation of this branch is beyond the scope of this document.
* The repository does not need any changes to move to the new version.
- For each of the target repositories:
- If the repository does not need any changes (i.e. `bump/v4.7.0` does not exist) then create
a new PR updating `lean-toolchain` to `leanprover/lean4:v4.7.0-rc1` and running `lake update`.
- Otherwise:
- Checkout the `bump/v4.7.0` branch.
- Verify that the `lean-toolchain` is set to the nightly from which the release candidate was created.
- `git merge origin/master`
- Change the `lean-toolchain` to `leanprover/lean4:v4.7.0-rc1`
- In `lakefile.lean`, change any dependencies which were using `nightly-testing` or `bump/v4.7.0` branches
back to `master` or `main`, and run `lake update` for those dependencies.
- Run `lake build` to ensure that dependencies are found (but it's okay to stop it after a moment).
- `git commit`
- `git push`
- Open a PR from `bump/v4.7.0` to `master`, and either merge it yourself after CI, if appropriate,
or notify the maintainers that it is ready to go.
- Once the PR has been merged, tag `master` with `v4.7.0-rc1` and push this tag.
- We do this for the same list of repositories as for stable releases, see above.
As above, there are dependencies between these, and so the process above is iterative.
It greatly helps if you can merge the `bump/v4.7.0` PRs yourself!
It is essential for Mathlib CI that you then create the next `bump/v4.8.0` branch
for the next development cycle.
Set the `lean-toolchain` file on this branch to same `nightly` you used for this release.
- For Batteries/Aesop/Mathlib, which maintain a `nightly-testing` branch, make sure there is a tag
`nightly-testing-2024-02-29` with date corresponding to the nightly used for the release
(create it if not), and then on the `nightly-testing` branch `git reset --hard master`, and force push.
- Make an announcement!
This should go in https://leanprover.zulipchat.com/#narrow/stream/113486-announce, with topic `v4.7.0-rc1`.
Please see previous announcements for suggested language.
You will want a few bullet points for main topics from the release notes.
Please also make sure that whoever is handling social media knows the release is out.
- Begin the next development cycle (i.e. for `v4.8.0`) on the Lean repository, by making a PR that:
- Updates `src/CMakeLists.txt` to say `set(LEAN_VERSION_MINOR 8)`
- Replaces the "release notes will be copied" text in the `v4.6.0` section of `RELEASES.md` with the
finalized release notes from the `releases/v4.6.0` branch.
- Replaces the "development in progress" in the `v4.7.0` section of `RELEASES.md` with
```
Release candidate, release notes will be copied from the branch `releases/v4.7.0` once completed.
```
and inserts the following section before that section:
```
v4.8.0
----------
Development in progress.
```
- Removes all the entries from the `./releases_drafts/` folder.
- Titled "chore: begin development cycle for v4.8.0"
## Time estimates:
Slightly longer than the corresponding steps for a stable release.
Similar process, but more things go wrong.
In particular, updating the downstream repositories is significantly more work
(because we need to merge existing `bump/v4.7.0` branches, not just update a toolchain).
# Preparing `bump/v4.7.0` branches
While not part of the release process per se,
this is a brief summary of the work that goes into updating Batteries/Aesop/Mathlib to new versions.
Please read https://leanprover-community.github.io/contribute/tags_and_branches.html
* Each repo has an unreviewed `nightly-testing` branch that
receives commits automatically from `master`, and
has its toolchain updated automatically for every nightly.
(Note: the aesop branch is not automated, and is updated on an as needed basis.)
As a consequence this branch is often broken.
A bot posts in the (private!) "Mathlib reviewers" stream on Zulip about the status of these branches.
* We fix the breakages by committing directly to `nightly-testing`: there is no PR process.
* This can either be done by the person managing this process directly,
or by soliciting assistance from authors of files, or generally helpful people on Zulip!
* Each repo has a `bump/v4.7.0` which accumulates reviewed changes adapting to new versions.
* Once `nightly-testing` is working on a given nightly, say `nightly-2024-02-15`, we will create a PR to `bump/v4.7.0`.
* For Mathlib, there is a script in `scripts/create-adaptation-pr.sh` that automates this process.
* For Batteries and Aesop it is currently manual.
* For all of these repositories, the process is the same:
* Make sure `bump/v4.7.0` is up to date with `master` (by merging `master`, no PR necessary)
* Create from `bump/v4.7.0` a `bump/nightly-2024-02-15` branch.
* In that branch, `git merge nightly-testing` to bring across changes from `nightly-testing`.
* Sanity check changes, commit, and make a PR to `bump/v4.7.0` from the `bump/nightly-2024-02-15` branch.
* Solicit review, merge the PR into `bump/v4.7.0`.
* It is always okay to merge in the following directions:
`master` -> `bump/v4.7.0` -> `bump/nightly-2024-02-15` -> `nightly-testing`.
Please remember to push any merges you make to intermediate steps!
# Writing the release notes
We are currently trying a system where release notes are compiled all at once from someone looking through the commit history.
The exact steps are a work in progress.
Here is the general idea:
* The work is done right on the `releases/v4.6.0` branch sometime after it is created but before the stable release is made.
The release notes for `v4.6.0` will later be copied to `master` when we begin a new development cycle.
* There can be material for release notes entries in commit messages.
* There can also be pre-written entries in `./releases_drafts`, which should be all incorporated in the release notes and then deleted from the branch.
See `./releases_drafts/README.md` for more information.
* The release notes should be written from a downstream expert user's point of view.
This section will be updated when the next release notes are written (for `v4.10.0`).

View File

@@ -4,16 +4,16 @@ def ack : Nat → Nat → Nat
| 0, y => y+1
| x+1, 0 => ack x 1
| x+1, y+1 => ack x (ack (x+1) y)
termination_by x y => (x, y)
termination_by ack x y => (x, y)
def sum (a : Array Int) : Int :=
let rec go (i : Nat) :=
if _ : i < a.size then
if i < a.size then
a[i] + go (i+1)
else
0
termination_by a.size - i
go 0
termination_by go i => a.size - i
set_option pp.proofs true
#print sum.go

View File

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

View File

@@ -5,15 +5,15 @@ open Lean Meta
def ex1 (declName : Name) : MetaM Unit := do
let info getConstInfo declName
IO.println s!"{declName} : {← ppExpr info.type}"
if let some val := info.value? then
if let some val := info.value? then
IO.println s!"{declName} : {← ppExpr val}"
#eval ex1 ``Nat
def ex2 (declName : Name) : MetaM Unit := do
let info getConstInfo declName
trace[Meta.debug] "{declName} : {info.type}"
if let some val := info.value? then
if let some val := info.value? then
trace[Meta.debug] "{declName} : {val}"
#eval ex2 ``Add.add
@@ -30,9 +30,9 @@ def ex3 (declName : Name) : MetaM Unit := do
trace[Meta.debug] "{x} : {← inferType x}"
def myMin [LT α] [DecidableRel (α := α) (·<·)] (a b : α) : α :=
if a < b then
if a < b then
a
else
else
b
set_option trace.Meta.debug true in
@@ -40,7 +40,7 @@ set_option trace.Meta.debug true in
def ex4 : MetaM Unit := do
let nat := mkConst ``Nat
withLocalDeclD `a nat fun a =>
withLocalDeclD `a nat fun a =>
withLocalDeclD `b nat fun b => do
let e mkAppM ``HAdd.hAdd #[a, b]
trace[Meta.debug] "{e} : {← inferType e}"
@@ -66,17 +66,15 @@ open Elab Term
def ex5 : TermElabM Unit := do
let nat := Lean.mkConst ``Nat
withLocalDeclD `a nat fun a => do
withLocalDeclD `a nat fun a => do
withLocalDeclD `b nat fun b => do
let ab mkAppM ``HAdd.hAdd #[a, b]
let abStx exprToSyntax ab
let aStx exprToSyntax a
let stx `(fun x => if x < 10 then $abStx + x else x + $aStx)
let stx `(fun x => if x < 10 then $( exprToSyntax ab) + x else x + $( exprToSyntax a))
let e elabTerm stx none
trace[Meta.debug] "{e} : {← inferType e}"
let e := mkApp e (mkNatLit 5)
let e whnf e
trace[Meta.debug] "{e}"
set_option trace.Meta.debug true in
#eval ex5

View File

@@ -4,16 +4,16 @@ def ack : Nat → Nat → Nat
| 0, y => y+1
| x+1, 0 => ack x 1
| x+1, y+1 => ack x (ack (x+1) y)
termination_by x y => (x, y)
termination_by ack x y => (x, y)
def sum (a : Array Int) : Int :=
let rec go (i : Nat) :=
if _ : i < a.size then
if i < a.size then
a[i] + go (i+1)
else
0
termination_by a.size - i
go 0
termination_by go i => a.size - i
set_option pp.proofs true
#print sum.go

View File

@@ -277,13 +277,14 @@ theorem BinTree.find_insert (b : BinTree β) (k : Nat) (v : β)
. by_cases' key < k
cases h; apply ihr; assumption
theorem BinTree.find_insert_of_ne (b : BinTree β) (ne : k k') (v : β)
theorem BinTree.find_insert_of_ne (b : BinTree β) (h : k k') (v : β)
: (b.insert k v).find? k' = b.find? k' := by
let t, h := b; simp
induction t with simp
| leaf =>
intros le
exact Nat.lt_of_le_of_ne le ne
split <;> (try simp) <;> split <;> (try simp)
have_eq k k'
contradiction
| node left key value right ihl ihr =>
let .node hl hr bl br := h
specialize ihl bl

View File

@@ -1 +0,0 @@
build

View File

@@ -149,7 +149,7 @@ We now define the constant folding optimization that traverses a term if replace
/-!
The correctness of the `Term.constFold` is proved using induction, case-analysis, and the term simplifier.
We prove all cases but the one for `plus` using `simp [*]`. This tactic instructs the term simplifier to
use hypotheses such as `a = b` as rewriting/simplifications rules.
use hypotheses such as `a = b` as rewriting/simplications rules.
We use the `split` to break the nested `match` expression in the `plus` case into two cases.
The local variables `iha` and `ihb` are the induction hypotheses for `a` and `b`.
The modifier `←` in a term simplifier argument instructs the term simplifier to use the equation as a rewriting rule in

View File

@@ -149,4 +149,4 @@ def fact : Expr ctx (Ty.fn Ty.int Ty.int) :=
(op (·*·) (delay fun _ => app fact (op (·-·) (var stop) (val 1))) (var stop)))
decreasing_by sorry
#eval! fact.interp Env.nil 10
#eval fact.interp Env.nil 10

View File

@@ -225,7 +225,7 @@ We now define the constant folding optimization that traverses a term if replace
/-!
The correctness of the `constFold` is proved using induction, case-analysis, and the term simplifier.
We prove all cases but the one for `plus` using `simp [*]`. This tactic instructs the term simplifier to
use hypotheses such as `a = b` as rewriting/simplifications rules.
use hypotheses such as `a = b` as rewriting/simplications rules.
We use the `split` to break the nested `match` expression in the `plus` case into two cases.
The local variables `iha` and `ihb` are the induction hypotheses for `a` and `b`.
The modifier `←` in a term simplifier argument instructs the term simplifier to use the equation as a rewriting rule in

View File

@@ -29,7 +29,7 @@ inductive HasType : Expr → Ty → Prop
/-!
We can easily show that if `e` has type `t₁` and type `t₂`, then `t₁` and `t₂` must be equal
by using the `cases` tactic. This tactic creates a new subgoal for every constructor,
by using the the `cases` tactic. This tactic creates a new subgoal for every constructor,
and automatically discharges unreachable cases. The tactic combinator `tac₁ <;> tac₂` applies
`tac₂` to each subgoal produced by `tac₁`. Then, the tactic `rfl` is used to close all produced
goals using reflexivity.
@@ -82,7 +82,7 @@ theorem Expr.typeCheck_correct (h₁ : HasType e ty) (h₂ : e.typeCheck ≠ .un
/-!
Now, we prove that if `Expr.typeCheck e` returns `Maybe.unknown`, then forall `ty`, `HasType e ty` does not hold.
The notation `e.typeCheck` is sugar for `Expr.typeCheck e`. Lean can infer this because we explicitly said that `e` has type `Expr`.
The proof is by induction on `e` and case analysis. The tactic `rename_i` is used to rename "inaccessible" variables.
The proof is by induction on `e` and case analysis. The tactic `rename_i` is used to to rename "inaccessible" variables.
We say a variable is inaccessible if it is introduced by a tactic (e.g., `cases`) or has been shadowed by another variable introduced
by the user. Note that the tactic `simp [typeCheck]` is applied to all goal generated by the `induction` tactic, and closes
the cases corresponding to the constructors `Expr.nat` and `Expr.bool`.

View File

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

View File

@@ -4,18 +4,15 @@ open Lean Widget
/-!
# The user-widgets system
Proving and programming are inherently interactive tasks.
Lots of mathematical objects and data structures are visual in nature.
*User widgets* let you associate custom interactive UIs
with sections of a Lean document.
User widgets are rendered in the Lean infoview.
Proving and programming are inherently interactive tasks. Lots of mathematical objects and data
structures are visual in nature. *User widgets* let you associate custom interactive UIs with
sections of a Lean document. User widgets are rendered in the Lean infoview.
![Rubik's cube](../images/widgets_rubiks.png)
## Trying it out
To try it out, type in the following code and place your cursor over the `#widget` command.
You can also [view this manual entry in the online editor](https://live.lean-lang.org/#url=https%3A%2F%2Fraw.githubusercontent.com%2Fleanprover%2Flean4%2Fmaster%2Fdoc%2Fexamples%2Fwidgets.lean).
To try it out, simply type in the following code and place your cursor over the `#widget` command.
-/
@[widget_module]
@@ -24,37 +21,38 @@ def helloWidget : Widget.Module where
import * as React from 'react';
export default function(props) {
const name = props.name || 'world'
return React.createElement('p', {}, 'Hello ' + name + '!')
return React.createElement('p', {}, name + '!')
}"
#widget helloWidget
/-!
If you want to dive into a full sample right away, check out
[`Rubiks`](https://github.com/leanprover-community/ProofWidgets4/blob/main/ProofWidgets/Demos/Rubiks.lean).
This sample uses higher-level widget components from the ProofWidgets library.
[`RubiksCube`](https://github.com/leanprover/lean4-samples/blob/main/RubiksCube/).
Below, we'll explain the system piece by piece.
⚠️ WARNING: All of the user widget APIs are **unstable** and subject to breaking changes.
## Widget modules and instances
## Widget sources and instances
A [widget module](https://leanprover-community.github.io/mathlib4_docs/Lean/Widget/UserWidget.html#Lean.Widget.Module)
is a valid JavaScript [ESModule](https://developer.mozilla.org/en-US/docs/Web/JavaScript/Guide/Modules)
that can execute in the Lean infoview.
Most widget modules export a [React component](https://reactjs.org/docs/components-and-props.html)
as the piece of user interface to be rendered.
To access React, the module can use `import * as React from 'react'`.
Our first example of a widget module is `helloWidget` above.
Widget modules must be registered with the `@[widget_module]` attribute.
A *widget source* is a valid JavaScript [ESModule](https://developer.mozilla.org/en-US/docs/Web/JavaScript/Guide/Modules)
which exports a [React component](https://reactjs.org/docs/components-and-props.html). To access
React, the module must use `import * as React from 'react'`. Our first example of a widget source
is of course the value of `helloWidget.javascript`.
A [widget instance](https://leanprover-community.github.io/mathlib4_docs/Lean/Widget/Types.html#Lean.Widget.WidgetInstance)
is then the identifier of a widget module (e.g. `` `helloWidget ``)
bundled with a value for its props.
This value is passed as the argument to the React component.
In our first invocation of `#widget`, we set it to `.null`.
Try out what happens when you type in:
We can register a widget source with the `@[widget]` attribute, giving it a friendlier name
in the `name` field. This is bundled together in a `UserWidgetDefinition`.
A *widget instance* is then the identifier of a `UserWidgetDefinition` (so `` `helloWidget ``,
not `"Hello"`) associated with a range of positions in the Lean source code. Widget instances
are stored in the *infotree* in the same manner as other information about the source file
such as the type of every expression. In our example, the `#widget` command stores a widget instance
with the entire line as its range. We can think of a widget instance as an instruction for the
infoview: "when the user places their cursor here, please render the following widget".
Every widget instance also contains a `props : Json` value. This value is passed as an argument
to the React component. In our first invocation of `#widget`, we set it to `.null`. Try out what
happens when you type in:
-/
structure HelloWidgetProps where
@@ -64,37 +62,21 @@ structure HelloWidgetProps where
#widget helloWidget with { name? := "<your name here>" : HelloWidgetProps }
/-!
Under the hood, widget instances are associated with a range of positions in the source file.
Widget instances are stored in the *infotree*
in the same manner as other information about the source file
such as the type of every expression.
In our example, the `#widget` command stores a widget instance
with the entire line as its range.
One can think of the infotree entry as an instruction for the infoview:
"when the user places their cursor here, please render the following widget".
-/
💡 NOTE: The RPC system presented below does not depend on JavaScript. However the primary use case
is the web-based infoview in VSCode.
/-!
## Querying the Lean server
💡 NOTE: The RPC system presented below does not depend on JavaScript.
However, the primary use case is the web-based infoview in VSCode.
Besides enabling us to create cool client-side visualizations, user widgets come with the ability
to communicate with the Lean server. Thanks to this, they have the same metaprogramming capabilities
as custom elaborators or the tactic framework. To see this in action, let's implement a `#check`
command as a web input form. This example assumes some familiarity with React.
Besides enabling us to create cool client-side visualizations,
user widgets have the ability to communicate with the Lean server.
Thanks to this, they have the same metaprogramming capabilities
as custom elaborators or the tactic framework.
To see this in action, let's implement a `#check` command as a web input form.
This example assumes some familiarity with React.
The first thing we'll need is to create an *RPC method*.
Meaning "Remote Procedure Call",this is a Lean function callable from widget code
(possibly remotely over the internet).
The first thing we'll need is to create an *RPC method*. Meaning "Remote Procedure Call", this
is basically a Lean function callable from widget code (possibly remotely over the internet).
Our method will take in the `name : Name` of a constant in the environment and return its type.
By convention, we represent the input data as a `structure`.
Since it will be sent over from JavaScript,
we need `FromJson` and `ToJson` instance.
We'll see why the position field is needed later.
By convention, we represent the input data as a `structure`. Since it will be sent over from JavaScript,
we need `FromJson` and `ToJson`. We'll see below why the position field is needed.
-/
structure GetTypeParams where
@@ -105,33 +87,25 @@ structure GetTypeParams where
deriving FromJson, ToJson
/-!
After its argument structure, we define the `getType` method.
RPCs method execute in the `RequestM` monad and must return a `RequestTask α`
where `α` is the "actual" return type.
The `Task` is so that requests can be handled concurrently.
As a first guess, we'd use `Expr` as `α`.
However, expressions in general can be large objects
which depend on an `Environment` and `LocalContext`.
Thus we cannot directly serialize an `Expr` and send it to JavaScript.
Instead, there are two options:
After its arguments, we define the `getType` method. Every RPC method executes in the `RequestM`
monad and must return a `RequestTask α` where `α` is its "actual" return type. The `Task` is so
that requests can be handled concurrently. A first guess for `α` might be `Expr`. However,
expressions in general can be large objects which depend on an `Environment` and `LocalContext`.
Thus we cannot directly serialize an `Expr` and send it to the widget. Instead, there are two
options:
- One is to send a *reference* which points to an object residing on the server. From JavaScript's
point of view, references are entirely opaque, but they can be sent back to other RPC methods for
further processing.
- Two is to pretty-print the expression and send its textual representation called `CodeWithInfos`.
This representation contains extra data which the infoview uses for interactivity. We take this
strategy here.
- One is to send a *reference* which points to an object residing on the server.
From JavaScript's point of view, references are entirely opaque,
but they can be sent back to other RPC methods for further processing.
- The other is to pretty-print the expression and send its textual representation called `CodeWithInfos`.
This representation contains extra data which the infoview uses for interactivity.
We take this strategy here.
RPC methods execute in the context of a file,
but not of any particular `Environment`,
so they don't know about the available `def`initions and `theorem`s.
Thus, we need to pass in a position at which we want to use the local `Environment`.
This is why we store it in `GetTypeParams`.
The `withWaitFindSnapAtPos` method launches a concurrent computation
whose job is to find such an `Environment` for us,
in the form of a `snap : Snapshot`.
With this in hand, we can call `MetaM` procedures
to find out the type of `name` and pretty-print it.
RPC methods execute in the context of a file, but not any particular `Environment` so they don't
know about the available `def`initions and `theorem`s. Thus, we need to pass in a position at which
we want to use the local `Environment`. This is why we store it in `GetTypeParams`. The `withWaitFindSnapAtPos`
method launches a concurrent computation whose job is to find such an `Environment` and a bit
more information for us, in the form of a `snap : Snapshot`. With this in hand, we can call
`MetaM` procedures to find out the type of `name` and pretty-print it.
-/
open Server RequestM in
@@ -147,22 +121,18 @@ def getType (params : GetTypeParams) : RequestM (RequestTask CodeWithInfos) :=
/-!
## Using infoview components
Now that we have all we need on the server side, let's write the widget module.
By importing `@leanprover/infoview`, widgets can render UI components used to implement the infoview itself.
For example, the `<InteractiveCode>` component displays expressions
with `term : type` tooltips as seen in the goal view.
We will use it to implement our custom `#check` display.
Now that we have all we need on the server side, let's write the widget source. By importing
`@leanprover/infoview`, widgets can render UI components used to implement the infoview itself.
For example, the `<InteractiveCode>` component displays expressions with `term : type` tooltips
as seen in the goal view. We will use it to implement our custom `#check` display.
⚠️ WARNING: Like the other widget APIs, the infoview JS API is **unstable** and subject to breaking changes.
The code below demonstrates useful parts of the API.
To make RPC method calls, we invoke the `useRpcSession` hook.
The `useAsync` helper packs the results of an RPC call into an `AsyncState` structure
which indicates whether the call has resolved successfully,
has returned an error, or is still in-flight.
Based on this we either display an `InteractiveCode` component with the result,
`mapRpcError` the error in order to turn it into a readable message,
or show a `Loading..` message, respectively.
The code below demonstrates useful parts of the API. To make RPC method calls, we use the `RpcContext`.
The `useAsync` helper packs the results of a call into an `AsyncState` structure which indicates
whether the call has resolved successfully, has returned an error, or is still in-flight. Based
on this we either display an `InteractiveCode` with the type, `mapRpcError` the error in order
to turn it into a readable message, or show a `Loading..` message, respectively.
-/
@[widget_module]
@@ -170,10 +140,10 @@ def checkWidget : Widget.Module where
javascript := "
import * as React from 'react';
const e = React.createElement;
import { useRpcSession, InteractiveCode, useAsync, mapRpcError } from '@leanprover/infoview';
import { RpcContext, InteractiveCode, useAsync, mapRpcError } from '@leanprover/infoview';
export default function(props) {
const rs = useRpcSession()
const rs = React.useContext(RpcContext)
const [name, setName] = React.useState('getType')
const st = useAsync(() =>
@@ -189,7 +159,7 @@ export default function(props) {
"
/-!
We can now try out the widget.
Finally we can try out the widget.
-/
#widget checkWidget
@@ -199,31 +169,30 @@ We can now try out the widget.
## Building widget sources
While typing JavaScript inline is fine for a simple example,
for real developments we want to use packages from NPM, a proper build system, and JSX.
Thus, most actual widget sources are built with Lake and NPM.
They consist of multiple files and may import libraries which don't work as ESModules by default.
On the other hand a widget module must be a single, self-contained ESModule in the form of a string.
Readers familiar with web development may already have guessed that to obtain such a string, we need a *bundler*.
Two popular choices are [`rollup.js`](https://rollupjs.org/guide/en/)
and [`esbuild`](https://esbuild.github.io/).
If we go with `rollup.js`, to make a widget work with the infoview we need to:
While typing JavaScript inline is fine for a simple example, for real developments we want to use
packages from NPM, a proper build system, and JSX. Thus, most actual widget sources are built with
Lake and NPM. They consist of multiple files and may import libraries which don't work as ESModules
by default. On the other hand a widget source must be a single, self-contained ESModule in the form
of a string. Readers familiar with web development may already have guessed that to obtain such a
string, we need a *bundler*. Two popular choices are [`rollup.js`](https://rollupjs.org/guide/en/)
and [`esbuild`](https://esbuild.github.io/). If we go with `rollup.js`, to make a widget work with
the infoview we need to:
- Set [`output.format`](https://rollupjs.org/guide/en/#outputformat) to `'es'`.
- [Externalize](https://rollupjs.org/guide/en/#external) `react`, `react-dom`, `@leanprover/infoview`.
These libraries are already loaded by the infoview so they should not be bundled.
ProofWidgets provides a working `rollup.js` build configuration in
[rollup.config.js](https://github.com/leanprover-community/ProofWidgets4/blob/main/widget/rollup.config.js).
In the RubiksCube sample, we provide a working `rollup.js` build configuration in
[rollup.config.js](https://github.com/leanprover/lean4-samples/blob/main/RubiksCube/widget/rollup.config.js).
## Inserting text
Besides making RPC calls, widgets can instruct the editor to carry out certain actions.
We can insert text, copy text to the clipboard, or highlight a certain location in the document.
To do this, use the `EditorContext` React context.
This will return an `EditorConnection`
whose `api` field contains a number of methods that interact with the editor.
We can also instruct the editor to insert text, copy text to the clipboard, or
reveal a certain location in the document.
To do this, use the `React.useContext(EditorContext)` React context.
This will return an `EditorConnection` whose `api` field contains a number of methods to
interact with the text editor.
The full API can be viewed [here](https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview-api/src/infoviewApi.ts#L52).
You can see the full API for this [here](https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview-api/src/infoviewApi.ts#L52)
-/
@[widget_module]
@@ -243,4 +212,6 @@ export default function(props) {
}
"
/-! Finally, we can try this out: -/
#widget insertTextWidget

View File

@@ -396,7 +396,7 @@ Every expression in Lean has a natural computational interpretation, unless it i
* *β-reduction* : An expression ``(λ x, t) s`` β-reduces to ``t[s/x]``, that is, the result of replacing ``x`` by ``s`` in ``t``.
* *ζ-reduction* : An expression ``let x := s in t`` ζ-reduces to ``t[s/x]``.
* *δ-reduction* : If ``c`` is a defined constant with definition ``t``, then ``c`` δ-reduces to ``t``.
* *δ-reduction* : If ``c`` is a defined constant with definition ``t``, then ``c`` δ-reduces to to ``t``.
* *ι-reduction* : When a function defined by recursion on an inductive type is applied to an element given by an explicit constructor, the result ι-reduces to the specified function value, as described in [Inductive Types](inductive.md).
The reduction relation is transitive, which is to say, is ``s`` reduces to ``s'`` and ``t`` reduces to ``t'``, then ``s t`` reduces to ``s' t'``, ``λ x, s`` reduces to ``λ x, s'``, and so on. If ``s`` and ``t`` reduce to a common term, they are said to be *definitionally equal*. Definitional equality is defined to be the smallest equivalence relation that satisfies all these properties and also includes α-equivalence and the following two relations:

138
doc/flake.lock generated
View File

@@ -18,15 +18,12 @@
}
},
"flake-utils": {
"inputs": {
"systems": "systems"
},
"locked": {
"lastModified": 1710146030,
"narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=",
"lastModified": 1656928814,
"narHash": "sha256-RIFfgBuKz6Hp89yRr7+NR5tzIAbn52h8vT6vXkYjZoM=",
"owner": "numtide",
"repo": "flake-utils",
"rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a",
"rev": "7e2a3b3dfd9af950a856d66b0a7d01e3c18aa249",
"type": "github"
},
"original": {
@@ -38,12 +35,13 @@
"lean": {
"inputs": {
"flake-utils": "flake-utils",
"nixpkgs": "nixpkgs",
"nixpkgs-old": "nixpkgs-old"
"lean4-mode": "lean4-mode",
"nix": "nix",
"nixpkgs": "nixpkgs_2"
},
"locked": {
"lastModified": 0,
"narHash": "sha256-saRAtQ6VautVXKDw1XH35qwP0KEBKTKZbg/TRa4N9Vw=",
"narHash": "sha256-YnYbmG0oou1Q/GE4JbMNb8/yqUVXBPIvcdQQJHBqtPk=",
"path": "../.",
"type": "path"
},
@@ -52,6 +50,22 @@
"type": "path"
}
},
"lean4-mode": {
"flake": false,
"locked": {
"lastModified": 1659020985,
"narHash": "sha256-+dRaXB7uvN/weSZiKcfSKWhcdJVNg9Vg8k0pJkDNjpc=",
"owner": "leanprover",
"repo": "lean4-mode",
"rev": "37d5c99b7b29c80ab78321edd6773200deb0bca6",
"type": "github"
},
"original": {
"owner": "leanprover",
"repo": "lean4-mode",
"type": "github"
}
},
"leanInk": {
"flake": false,
"locked": {
@@ -69,6 +83,22 @@
"type": "github"
}
},
"lowdown-src": {
"flake": false,
"locked": {
"lastModified": 1633514407,
"narHash": "sha256-Dw32tiMjdK9t3ETl5fzGrutQTzh2rufgZV4A/BbxuD4=",
"owner": "kristapsdz",
"repo": "lowdown",
"rev": "d2c2b44ff6c27b936ec27358a2653caaef8f73b8",
"type": "github"
},
"original": {
"owner": "kristapsdz",
"repo": "lowdown",
"type": "github"
}
},
"mdBook": {
"flake": false,
"locked": {
@@ -85,13 +115,65 @@
"type": "github"
}
},
"nix": {
"inputs": {
"lowdown-src": "lowdown-src",
"nixpkgs": "nixpkgs",
"nixpkgs-regression": "nixpkgs-regression"
},
"locked": {
"lastModified": 1657097207,
"narHash": "sha256-SmeGmjWM3fEed3kQjqIAO8VpGmkC2sL1aPE7kKpK650=",
"owner": "NixOS",
"repo": "nix",
"rev": "f6316b49a0c37172bca87ede6ea8144d7d89832f",
"type": "github"
},
"original": {
"owner": "NixOS",
"repo": "nix",
"type": "github"
}
},
"nixpkgs": {
"locked": {
"lastModified": 1710889954,
"narHash": "sha256-Pr6F5Pmd7JnNEMHHmspZ0qVqIBVxyZ13ik1pJtm2QXk=",
"lastModified": 1653988320,
"narHash": "sha256-ZaqFFsSDipZ6KVqriwM34T739+KLYJvNmCWzErjAg7c=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "7872526e9c5332274ea5932a0c3270d6e4724f3b",
"rev": "2fa57ed190fd6c7c746319444f34b5917666e5c1",
"type": "github"
},
"original": {
"owner": "NixOS",
"ref": "nixos-22.05-small",
"repo": "nixpkgs",
"type": "github"
}
},
"nixpkgs-regression": {
"locked": {
"lastModified": 1643052045,
"narHash": "sha256-uGJ0VXIhWKGXxkeNnq4TvV3CIOkUJ3PAoLZ3HMzNVMw=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2",
"type": "github"
},
"original": {
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2",
"type": "github"
}
},
"nixpkgs_2": {
"locked": {
"lastModified": 1657208011,
"narHash": "sha256-BlIFwopAykvdy1DYayEkj6ZZdkn+cVgPNX98QVLc0jM=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "2770cc0b1e8faa0e20eb2c6aea64c256a706d4f2",
"type": "github"
},
"original": {
@@ -101,23 +183,6 @@
"type": "github"
}
},
"nixpkgs-old": {
"flake": false,
"locked": {
"lastModified": 1581379743,
"narHash": "sha256-i1XCn9rKuLjvCdu2UeXKzGLF6IuQePQKFt4hEKRU5oc=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "34c7eb7545d155cc5b6f499b23a7cb1c96ab4d59",
"type": "github"
},
"original": {
"owner": "NixOS",
"ref": "nixos-19.03",
"repo": "nixpkgs",
"type": "github"
}
},
"root": {
"inputs": {
"alectryon": "alectryon",
@@ -129,21 +194,6 @@
"leanInk": "leanInk",
"mdBook": "mdBook"
}
},
"systems": {
"locked": {
"lastModified": 1681028828,
"narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
"owner": "nix-systems",
"repo": "default",
"rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
"type": "github"
},
"original": {
"owner": "nix-systems",
"repo": "default",
"type": "github"
}
}
},
"root": "root",

View File

@@ -17,7 +17,7 @@
};
outputs = inputs@{ self, ... }: inputs.flake-utils.lib.eachDefaultSystem (system:
with inputs.lean.packages.${system}.deprecated; with nixpkgs;
with inputs.lean.packages.${system}; with nixpkgs;
let
doc-src = lib.sourceByRegex ../. ["doc.*" "tests(/lean(/beginEndAsMacro.lean)?)?"];
in {
@@ -27,7 +27,7 @@
src = inputs.mdBook;
cargoDeps = drv.cargoDeps.overrideAttrs (_: {
inherit src;
outputHash = "sha256-CO3A9Kpp4sIvkT9X3p+GTidazk7Fn4jf0AP2PINN44A=";
outputHash = "sha256-1YlPS6cqgxE4fjy9G8pWrpP27YrrbCDnfeyIsX81ZNw=";
});
doCheck = false;
});
@@ -44,6 +44,21 @@
mdbook build -d $out
'';
};
# We use a separate derivation instead of `checkPhase` so we can push it but not `doc` to the binary cache
test = stdenv.mkDerivation {
name ="lean-doc-test";
src = doc-src;
buildInputs = [ lean-mdbook stage1.Lean.lean-package strace ];
patchPhase = ''
cd doc
patchShebangs test
'';
buildPhase = ''
mdbook test
touch $out
'';
dontInstall = true;
};
leanInk = (buildLeanPackage {
name = "Main";
src = inputs.leanInk;

Binary file not shown.

Before

Width:  |  Height:  |  Size: 19 KiB

After

Width:  |  Height:  |  Size: 12 KiB

Binary file not shown.

Before

Width:  |  Height:  |  Size: 65 KiB

After

Width:  |  Height:  |  Size: 57 KiB

Binary file not shown.

Before

Width:  |  Height:  |  Size: 33 KiB

After

Width:  |  Height:  |  Size: 23 KiB

View File

@@ -13,7 +13,7 @@ Recall that nonnegative numerals are considered to be a `Nat` if there are no ty
The operator `/` for `Int` implements integer division.
```lean
#eval -10 / 4 -- -3
#eval -10 / 4 -- -2
```
Similar to `Nat`, the internal representation of `Int` is optimized. Small integers are

100
doc/latex/lean4.py Normal file
View File

@@ -0,0 +1,100 @@
# -*- coding: utf-8 -*-
"""
pygments.lexers.theorem
~~~~~~~~~~~~~~~~~~~~~~~
Lexers for theorem-proving languages.
:copyright: Copyright 2006-2017 by the Pygments team, see AUTHORS.
:license: BSD, see LICENSE for details.
"""
import re
from pygments.lexer import RegexLexer, default, words
from pygments.token import Text, Comment, Operator, Keyword, Name, String, \
Number, Punctuation, Generic
__all__ = ['Lean4Lexer']
class Lean4Lexer(RegexLexer):
"""
For the `Lean 4 <https://github.com/leanprover/lean4>`_
theorem prover.
.. versionadded:: 2.0
"""
name = 'Lean4'
aliases = ['lean4']
filenames = ['*.lean']
mimetypes = ['text/x-lean']
flags = re.MULTILINE | re.UNICODE
keywords1 = (
'import', 'abbreviation', 'opaque_hint', 'tactic_hint', 'definition',
'renaming', 'inline', 'hiding', 'parameter', 'lemma', 'variable',
'theorem', 'axiom', 'inductive', 'structure', 'universe', 'alias',
'help', 'options', 'precedence', 'postfix', 'prefix',
'infix', 'infixl', 'infixr', 'notation', '#eval',
'#check', '#reduce', '#exit', 'coercion', 'end', 'private', 'using', 'namespace',
'including', 'instance', 'section', 'context', 'protected', 'expose',
'export', 'set_option', 'extends', 'open', 'example',
'constant', 'constants', 'print', 'opaque', 'reducible', 'irreducible',
'def', 'macro', 'elab', 'syntax', 'macro_rules', 'reduce', 'where',
'abbrev', 'noncomputable', 'class', 'attribute', 'synth', 'mutual',
)
keywords2 = (
'forall', 'fun', 'Pi', 'obtain', 'from', 'have', 'show', 'assume',
'take', 'let', 'if', 'else', 'then', 'by', 'in', 'with', 'begin',
'proof', 'qed', 'calc', 'match', 'nomatch', 'do', 'at',
)
keywords3 = (
# Sorts
'Type', 'Prop', 'Sort',
)
operators = (
u'!=', u'#', u'&', u'&&', u'*', u'+', u'-', u'/', u'@', u'!', u'`',
u'-.', u'->', u'.', u'..', u'...', u'::', u':>', u';', u';;', u'<',
u'<-', u'=', u'==', u'>', u'_', u'|', u'||', u'~', u'=>', u'<=', u'>=',
u'/\\', u'\\/', u'', u'Π', u'λ', u'', u'', u'', u'', u'', u'',
u'¬', u'⁻¹', u'', u'', u'', u'', u'', u'', u'', u'×', u'',
u'', u'', u'', u'',
)
punctuation = (u'(', u')', u':', u'{', u'}', u'[', u']', u'', u'',
u':=', u',')
tokens = {
'root': [
(r'\s+', Text),
(r'/-', Comment, 'comment'),
(r'--.*?$', Comment.Single),
(words(keywords1, prefix=r'\b', suffix=r'\b'), Keyword.Namespace),
(words(keywords2, prefix=r'\b', suffix=r'\b'), Keyword),
(words(keywords3, prefix=r'\b', suffix=r'\b'), Keyword.Type),
(words(operators), Name.Builtin.Pseudo),
(words(punctuation), Operator),
(u"[A-Za-z_\u03b1-\u03ba\u03bc-\u03fb\u1f00-\u1ffe\u2100-\u214f]"
u"[A-Za-z_'\u03b1-\u03ba\u03bc-\u03fb\u1f00-\u1ffe\u2070-\u2079"
u"\u207f-\u2089\u2090-\u209c\u2100-\u214f0-9]*", Name),
(r'\d+', Number.Integer),
(r'"', String.Double, 'string'),
(r'[~?][a-z][\w\']*:', Name.Variable)
],
'comment': [
# Multiline Comments
(r'[^/-]', Comment.Multiline),
(r'/-', Comment.Multiline, '#push'),
(r'-/', Comment.Multiline, '#pop'),
(r'[/-]', Comment.Multiline)
],
'string': [
(r'[^\\"]+', String.Double),
(r'\\[n"\\]', String.Escape),
('"', String.Double, '#pop'),
],
}

View File

@@ -1,14 +1,9 @@
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 [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
------------
- C++14 compatible compiler
- [CMake](http://www.cmake.org)
- [GMP (GNU multiprecision library)](http://gmplib.org/)
- [LibUV](https://libuv.org/)
Platform-Specific Setup
-----------------------
@@ -17,32 +12,44 @@ Platform-Specific Setup
- [Windows (msys2)](msys2.md)
- [Windows (WSL)](wsl.md)
- [macOS (homebrew)](osx-10.9.md)
- Linux/macOS/WSL via [Nix](https://nixos.org/nix/): Call `nix develop` in the project root. That's it.
- Linux/macOS/WSL via [Nix](https://nixos.org/nix/): Call `nix-shell` in the project root. That's it.
Generic Build Instructions
--------------------------
Setting up a basic parallelized release build:
Setting up a basic release build:
```bash
git clone https://github.com/leanprover/lean4
git clone https://github.com/leanprover/lean4 --recurse-submodules
cd lean4
cmake --preset release
make -C build/release -j$(nproc || sysctl -n hw.logicalcpu)
mkdir -p build/release
cd build/release
cmake ../..
make
```
You can replace `$(nproc || sysctl -n hw.logicalcpu)` with the desired parallelism amount.
For regular development, we recommend running
```bash
git config submodule.recurse true
```
in the checkout so that `--recurse-submodules` doesn't have to be
specified with `git pull/checkout/...`.
The above commands will compile the Lean library and binaries into the
`stage1` subfolder; see below for details.
`stage1` subfolder; see below for details. Add `-j N` for an
appropriate `N` to `make` for a parallel build.
You should not usually run `cmake --install` after a successful build.
For example, on an AMD Ryzen 9 `make` takes 00:04:55, whereas `make -j 10`
takes 00:01:38. Your results may vary depending on the speed of your hard
drive.
You should not usually run `make install` after a successful build.
See [Dev setup using elan](../dev/index.md#dev-setup-using-elan) on how to properly set up your editor to use the correct stage depending on the source directory.
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).
Pass these along with the `cmake ../..` command.
* `-D CMAKE_BUILD_TYPE=`\
Select the build type. Valid values are `RELEASE` (default), `DEBUG`,

39
doc/make/msvc.md Normal file
View File

@@ -0,0 +1,39 @@
# Compiling Lean with Visual Studio
WARNING: Compiling Lean with Visual Studio doesn't currently work.
There's an ongoing effort to port Lean to Visual Studio.
The instructions below are for VS 2017.
In the meantime you can use [MSYS2](msys2.md) or [WSL](wsl.md).
## Installing dependencies
First, install `vcpkg` from https://github.com/Microsoft/vcpkg if you haven't
done so already.
Then, open a console in the directory you cloned `vcpkg` to, and type:
`vcpkg install mpir` for the 32-bit library or
`vcpkg install mpir:x64-windows` for the x64 one.
In Visual Studio, use the "open folder" feature and open the Lean directory.
Go to the `CMake->Change CMake Settings` menu. File `CMakeSettings.json` opens.
In each of the targets, add the following snippet (i.e., after every
`ctestCommandArgs`):
```json
"variables": [
{
"name": "CMAKE_TOOLCHAIN_FILE",
"value": "C:\\path\\to\\vcpkg\\scripts\\buildsystems\\vcpkg.cmake"
}
]
```
## Enable Intellisense
In Visual Studio, press Ctrl+Q and type `CppProperties.json` and press Enter.
Ensure `includePath` variables include `"${workspaceRoot}\\src"`.
## Build Lean
Press F7.

View File

@@ -15,24 +15,17 @@ Mode](https://docs.microsoft.com/en-us/windows/apps/get-started/enable-your-devi
which will allow Lean to create symlinks that e.g. enable go-to-definition in
the stdlib.
## Installing the Windows SDK
Install the Windows SDK from [Microsoft](https://developer.microsoft.com/en-us/windows/downloads/windows-sdk/).
The oldest supported version is 10.0.18362.0. If you installed the Windows SDK to the default location,
then there should be a directory with the version number at `C:\Program Files (x86)\Windows Kits\10\Include`.
If there are multiple directories, only the highest version number matters.
## Installing dependencies
[The official webpage of MSYS2][msys2] provides one-click installers.
Once installed, you should run the "MSYS2 CLANG64" shell from the start menu (the one that runs `clang64.exe`).
Do not run "MSYS2 MSYS" or "MSYS2 MINGW64" instead!
MSYS2 has a package management system, [pacman][pacman].
Once installed, you should run the "MSYS2 MinGW 64-bit shell" from the start menu (the one that runs `mingw64.exe`).
Do not run "MSYS2 MSYS" instead!
MSYS2 has a package management system, [pacman][pacman], which is used in Arch Linux.
Here are the commands to install all dependencies needed to compile Lean on your machine.
```bash
pacman -S make python mingw-w64-clang-x86_64-cmake mingw-w64-clang-x86_64-clang mingw-w64-clang-x86_64-ccache mingw-w64-clang-x86_64-libuv mingw-w64-clang-x86_64-gmp git unzip diffutils binutils
pacman -S make python mingw-w64-x86_64-cmake mingw-w64-x86_64-clang mingw-w64-x86_64-ccache git unzip diffutils binutils
```
You should now be able to run these commands:
@@ -45,9 +38,10 @@ cmake --version
Then follow the [generic build instructions](index.md) in the MSYS2
MinGW shell, using:
```
cmake --preset release -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++
cmake ../.. -G "Unix Makefiles" -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++
```
instead of `cmake --preset release`. This will use the clang compiler instead of gcc, which is required with msys2.
instead of `cmake ../..`. This ensures that cmake will call `sh` instead of `cmd.exe`
for script tasks and it will use the clang compiler instead of gcc, which is required.
## Install lean
@@ -68,9 +62,9 @@ If you want a version that can run independently of your MSYS install
then you need to copy the following dependent DLL's from where ever
they are installed in your MSYS setup:
- libc++.dll
- libgcc_s_seh-1.dll
- libstdc++-6.dll
- libgmp-10.dll
- libuv-1.dll
- libwinpthread-1.dll
The following linux command will do that:
@@ -88,6 +82,6 @@ version clang to your path.
**-bash: gcc: command not found**
Make sure `/clang64/bin` is in your PATH environment. If it is not then
check you launched the MSYS2 CLANG64 shell from the start menu.
(The one that runs `clang64.exe`).
Make sure `/mingw64/bin` is in your PATH environment. If it is not then
check you launched the MSYS2 MinGW 64-bit shell from the start menu.
(The one that runs `mingw64.exe`).

View File

@@ -1,4 +1,4 @@
# Install Packages on OS X 14.5
# Install Packages on OS X 10.9
We assume that you are using [homebrew][homebrew] as a package manager.
@@ -22,7 +22,7 @@ brew install gcc
```
To install clang++-3.5 via homebrew, please execute:
```bash
brew install llvm
brew install llvm --with-clang --with-asan
```
To use compilers other than the default one (Apple's clang++), you
need to use `-DCMAKE_CXX_COMPILER` option to specify the compiler
@@ -32,16 +32,15 @@ following to use `g++`.
cmake -DCMAKE_CXX_COMPILER=g++ ...
```
## Required Packages: CMake, GMP, libuv
## Required Packages: CMake, GMP
```bash
brew install cmake
brew install gmp
brew install libuv
```
## Recommended Packages: CCache
```bash
brew install ccache
```
```

View File

@@ -8,5 +8,5 @@ follow the [generic build instructions](index.md).
## Basic packages
```bash
sudo apt-get install git libgmp-dev libuv1-dev cmake ccache clang
sudo apt-get install git libgmp-dev cmake ccache clang
```

View File

@@ -138,8 +138,8 @@ definition:
-/
instance : Applicative List where
pure := List.singleton
seq f x := List.flatMap f fun y => Functor.map y (x ())
pure := List.pure
seq f x := List.bind f fun y => Functor.map y (x ())
/-!
Notice you can now sequence a _list_ of functions and a _list_ of items.

View File

@@ -33,7 +33,7 @@ convert the pure non-monadic value `x / y` into the required `Except` object. S
Now this return typing would get tedious if you had to include it everywhere that you call this
function, however, Lean type inference can clean this up. For example, you can define a test
function that calls the `divide` function and you don't need to say anything here about the fact that
function can calls the `divide` function and you don't need to say anything here about the fact that
it might throw an error, because that is inferred:
-/
def test := divide 5 0

View File

@@ -128,8 +128,8 @@ Applying the identity function through an applicative structure should not chang
values or structure. For example:
-/
instance : Applicative List where
pure := List.singleton
seq f x := List.flatMap f fun y => Functor.map y (x ())
pure := List.pure
seq f x := List.bind f fun y => Functor.map y (x ())
#eval pure id <*> [1, 2, 3] -- [1, 2, 3]
/-!
@@ -171,7 +171,7 @@ of data contained in the container resulting in a new container that has the sam
`u <*> pure y = pure (. y) <*> u`.
This law is a little more complicated, so don't sweat it too much. It states that the order that
This law is is a little more complicated, so don't sweat it too much. It states that the order that
you wrap things shouldn't matter. One the left, you apply any applicative `u` over a pure wrapped
object. On the right, you first wrap a function applying the object as an argument. Note that `(·
y)` is short hand for: `fun f => f y`. Then you apply this to the first applicative `u`. These
@@ -235,8 +235,8 @@ structure or its values.
Left identity is `x >>= pure = x` and is demonstrated by the following examples on a monadic `List`:
-/
instance : Monad List where
pure := List.singleton
bind := List.flatMap
pure := List.pure
bind := List.bind
def a := ["apple", "orange"]

View File

@@ -192,8 +192,8 @@ implementation of `pure` and `bind`.
-/
instance : Monad List where
pure := List.singleton
bind := List.flatMap
pure := List.pure
bind := List.bind
/-!
Like you saw with the applicative `seq` operator, the `bind` operator applies the given function

View File

@@ -15,7 +15,7 @@ data type containing several important pieces of information. First and foremost
current player, and it has a random generator.
-/
open Batteries (HashMap)
open Std (HashMap)
abbrev TileIndex := Nat × Nat -- a 2D index
inductive TileState where

View File

@@ -5,19 +5,14 @@ See [Setup](./setup.md) for supported platforms and other ways to set up Lean 4.
1. Install [VS Code](https://code.visualstudio.com/).
1. Launch VS Code and install the `Lean 4` extension by clicking on the 'Extensions' sidebar entry and searching for 'Lean 4'.
1. Launch VS Code and install the `lean4` extension by clicking on the "Extensions" sidebar entry and searching for "lean4".
![installing the vscode-lean4 extension](images/code-ext.png)
![installing the vscode-lean4 extension](images/code-ext.png)
1. Open the Lean 4 setup guide by creating a new text file using 'File > New Text File' (`Ctrl+N` / `Cmd+N`), clicking on the ∀-symbol in the top right and selecting 'Documentation… > Docs: Show Setup Guide'.
1. Open the Lean 4 setup guide by creating a new text file using "File > New Text File" (`Ctrl+N`), clicking on the ∀-symbol in the top right and selecting "Documentation… > Setup: Show Setup Guide".
![show setup guide](images/show-setup-guide.png)
![show setup guide](images/show-setup-guide.png)
1. Follow the Lean 4 setup guide. It will:
1. Follow the Lean 4 setup guide. It will walk you through learning resources for Lean 4, teach you how to set up Lean's dependencies on your platform, install Lean 4 for you at the click of a button and help you set up your first project.
- walk you through learning resources for Lean,
- teach you how to set up Lean's dependencies on your platform,
- install Lean 4 for you at the click of a button,
- help you set up your first project.
![setup guide](images/setup_guide.png)
![setup guide](images/setup_guide.png)

View File

@@ -6,8 +6,7 @@ Platforms built & tested by our CI, available as binary releases via elan (see b
* x86-64 Linux with glibc 2.27+
* x86-64 macOS 10.15+
* aarch64 (Apple Silicon) macOS 10.15+
* x86-64 Windows 11 (any version), Windows 10 (version 1903 or higher), Windows Server 2022
* x86-64 Windows 10+
### Tier 2
@@ -17,6 +16,7 @@ Releases may be silently broken due to the lack of automated testing.
Issue reports and fixes are welcome.
* aarch64 Linux with glibc 2.27+
* aarch64 (Apple Silicon) macOS
* x86 (32-bit) Linux
* Emscripten Web Assembly

View File

@@ -43,8 +43,7 @@ $ pdflatex test.tex
## Example with `minted`
First [install Pygments](https://pygments.org/download/) (version 2.18 or newer).
Then save the following sample LaTeX file `test.tex` into the same directory:
First [install Pygments](https://pygments.org/download/). Then save [`lean4.py`](https://raw.githubusercontent.com/leanprover/lean4/master/doc/latex/lean4.py), which contains an version of the Lean highlighter updated for Lean 4, and the following sample LaTeX file `test.tex` into the same directory:
```latex
\documentclass{article}
@@ -52,8 +51,9 @@ Then save the following sample LaTeX file `test.tex` into the same directory:
% switch to a monospace font supporting more Unicode characters
\setmonofont{FreeMono}
\usepackage{minted}
\newmintinline[lean]{lean4}{bgcolor=white}
\newminted[leancode]{lean4}{fontsize=\footnotesize}
% instruct minted to use our local theorem.py
\newmintinline[lean]{lean4.py:Lean4Lexer -x}{bgcolor=white}
\newminted[leancode]{lean4.py:Lean4Lexer -x}{fontsize=\footnotesize}
\usemintedstyle{tango} % a nice, colorful theme
\begin{document}
@@ -67,6 +67,9 @@ theorem funext {f₁ f₂ : ∀ (x : α), β x} (h : ∀ x, f₁ x = f₂ x) : f
\end{document}
```
If your version of `minted` is v2.7 or newer, but before v3.0,
you will additionally need to follow the workaround described in https://github.com/gpoore/minted/issues/360.
You can then compile `test.tex` by executing the following command:
```bash
@@ -78,14 +81,11 @@ Some remarks:
- either `xelatex` or `lualatex` is required to handle Unicode characters in the code.
- `--shell-escape` is needed to allow `xelatex` to execute `pygmentize` in a shell.
- If the chosen monospace font is missing some Unicode symbols, you can direct them to be displayed using a fallback font or other replacement LaTeX code.
``` latex
\usepackage{newunicodechar}
\newfontfamily{\freeserif}{DejaVu Sans}
\newunicodechar{✝}{\freeserif{✝}}
\newunicodechar{𝓞}{\ensuremath{\mathcal{O}}}
```
- If you are using an old version of Pygments, you can copy
[`lean.py`](https://raw.githubusercontent.com/pygments/pygments/master/pygments/lexers/lean.py) into your working directory,
and use `lean4.py:Lean4Lexer -x` instead of `lean4` above.
If your version of `minted` is v2.7 or newer, but before v3.0,
you will additionally need to follow the workaround described in https://github.com/gpoore/minted/issues/360.
``` latex
\usepackage{newunicodechar}
\newfontfamily{\freeserif}{DejaVu Sans}
\newunicodechar{✝}{\freeserif{✝}}
\newunicodechar{𝓞}{\ensuremath{\mathcal{O}}}
```
- minted has a "helpful" feature that draws red boxes around characters the chosen lexer doesn't recognize.
Since the Lean lexer cannot encompass all user-defined syntax, it is advisable to [work around](https://tex.stackexchange.com/a/343506/14563) this feature.

153
flake.lock generated
View File

@@ -1,15 +1,12 @@
{
"nodes": {
"flake-utils": {
"inputs": {
"systems": "systems"
},
"locked": {
"lastModified": 1710146030,
"narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=",
"lastModified": 1656928814,
"narHash": "sha256-RIFfgBuKz6Hp89yRr7+NR5tzIAbn52h8vT6vXkYjZoM=",
"owner": "numtide",
"repo": "flake-utils",
"rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a",
"rev": "7e2a3b3dfd9af950a856d66b0a7d01e3c18aa249",
"type": "github"
},
"original": {
@@ -18,13 +15,97 @@
"type": "github"
}
},
"lean4-mode": {
"flake": false,
"locked": {
"lastModified": 1676498134,
"narHash": "sha256-u3WvyKxOViZG53hkb8wd2/Og6muTecbh+NdflIgVeyk=",
"owner": "leanprover",
"repo": "lean4-mode",
"rev": "2c6ef33f476fdf5eb5e4fa4fa023ba8b11372440",
"type": "github"
},
"original": {
"owner": "leanprover",
"repo": "lean4-mode",
"type": "github"
}
},
"lowdown-src": {
"flake": false,
"locked": {
"lastModified": 1633514407,
"narHash": "sha256-Dw32tiMjdK9t3ETl5fzGrutQTzh2rufgZV4A/BbxuD4=",
"owner": "kristapsdz",
"repo": "lowdown",
"rev": "d2c2b44ff6c27b936ec27358a2653caaef8f73b8",
"type": "github"
},
"original": {
"owner": "kristapsdz",
"repo": "lowdown",
"type": "github"
}
},
"nix": {
"inputs": {
"lowdown-src": "lowdown-src",
"nixpkgs": "nixpkgs",
"nixpkgs-regression": "nixpkgs-regression"
},
"locked": {
"lastModified": 1657097207,
"narHash": "sha256-SmeGmjWM3fEed3kQjqIAO8VpGmkC2sL1aPE7kKpK650=",
"owner": "NixOS",
"repo": "nix",
"rev": "f6316b49a0c37172bca87ede6ea8144d7d89832f",
"type": "github"
},
"original": {
"owner": "NixOS",
"repo": "nix",
"type": "github"
}
},
"nixpkgs": {
"locked": {
"lastModified": 1710889954,
"narHash": "sha256-Pr6F5Pmd7JnNEMHHmspZ0qVqIBVxyZ13ik1pJtm2QXk=",
"lastModified": 1653988320,
"narHash": "sha256-ZaqFFsSDipZ6KVqriwM34T739+KLYJvNmCWzErjAg7c=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "7872526e9c5332274ea5932a0c3270d6e4724f3b",
"rev": "2fa57ed190fd6c7c746319444f34b5917666e5c1",
"type": "github"
},
"original": {
"owner": "NixOS",
"ref": "nixos-22.05-small",
"repo": "nixpkgs",
"type": "github"
}
},
"nixpkgs-regression": {
"locked": {
"lastModified": 1643052045,
"narHash": "sha256-uGJ0VXIhWKGXxkeNnq4TvV3CIOkUJ3PAoLZ3HMzNVMw=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2",
"type": "github"
},
"original": {
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2",
"type": "github"
}
},
"nixpkgs_2": {
"locked": {
"lastModified": 1686089707,
"narHash": "sha256-LTNlJcru2qJ0XhlhG9Acp5KyjB774Pza3tRH0pKIb3o=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "af21c31b2a1ec5d361ed8050edd0303c31306397",
"type": "github"
},
"original": {
@@ -34,60 +115,12 @@
"type": "github"
}
},
"nixpkgs-cadical": {
"locked": {
"lastModified": 1722221733,
"narHash": "sha256-sga9SrrPb+pQJxG1ttJfMPheZvDOxApFfwXCFO0H9xw=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "12bf09802d77264e441f48e25459c10c93eada2e",
"type": "github"
},
"original": {
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "12bf09802d77264e441f48e25459c10c93eada2e",
"type": "github"
}
},
"nixpkgs-old": {
"flake": false,
"locked": {
"lastModified": 1581379743,
"narHash": "sha256-i1XCn9rKuLjvCdu2UeXKzGLF6IuQePQKFt4hEKRU5oc=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "34c7eb7545d155cc5b6f499b23a7cb1c96ab4d59",
"type": "github"
},
"original": {
"owner": "NixOS",
"ref": "nixos-19.03",
"repo": "nixpkgs",
"type": "github"
}
},
"root": {
"inputs": {
"flake-utils": "flake-utils",
"nixpkgs": "nixpkgs",
"nixpkgs-cadical": "nixpkgs-cadical",
"nixpkgs-old": "nixpkgs-old"
}
},
"systems": {
"locked": {
"lastModified": 1681028828,
"narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
"owner": "nix-systems",
"repo": "default",
"rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
"type": "github"
},
"original": {
"owner": "nix-systems",
"repo": "default",
"type": "github"
"lean4-mode": "lean4-mode",
"nix": "nix",
"nixpkgs": "nixpkgs_2"
}
}
},

120
flake.nix
View File

@@ -1,77 +1,63 @@
{
description = "Lean development flake. Not intended for end users.";
description = "Lean interactive theorem prover";
inputs.nixpkgs.url = "github:NixOS/nixpkgs/nixpkgs-unstable";
# old nixpkgs used for portable release with older glibc (2.27)
inputs.nixpkgs-old.url = "github:NixOS/nixpkgs/nixos-19.03";
inputs.nixpkgs-old.flake = false;
# for cadical 1.9.5; sync with CMakeLists.txt
inputs.nixpkgs-cadical.url = "github:NixOS/nixpkgs/12bf09802d77264e441f48e25459c10c93eada2e";
inputs.flake-utils.url = "github:numtide/flake-utils";
inputs.nix.url = "github:NixOS/nix";
inputs.lean4-mode = {
url = "github:leanprover/lean4-mode";
flake = false;
};
# used *only* by `stage0-from-input` below
#inputs.lean-stage0 = {
# url = github:leanprover/lean4;
# inputs.nixpkgs.follows = "nixpkgs";
# inputs.flake-utils.follows = "flake-utils";
# inputs.nix.follows = "nix";
# inputs.lean4-mode.follows = "lean4-mode";
#};
outputs = { self, nixpkgs, nixpkgs-old, flake-utils, ... }@inputs: flake-utils.lib.eachDefaultSystem (system:
outputs = { self, nixpkgs, flake-utils, nix, lean4-mode, ... }@inputs: flake-utils.lib.eachDefaultSystem (system:
let
pkgs = import nixpkgs { inherit system; };
# An old nixpkgs for creating releases with an old glibc
pkgsDist-old = import nixpkgs-old { inherit system; };
# An old nixpkgs for creating releases with an old glibc
pkgsDist-old-aarch = import nixpkgs-old { localSystem.config = "aarch64-unknown-linux-gnu"; };
pkgsCadical = import inputs.nixpkgs-cadical { inherit system; };
cadical = if pkgs.stdenv.isLinux then
# use statically-linked cadical on Linux to avoid glibc versioning troubles
pkgsCadical.pkgsStatic.cadical.overrideAttrs { doCheck = false; }
else pkgsCadical.cadical;
lean-packages = pkgs.callPackage (./nix/packages.nix) { src = ./.; };
devShellWithDist = pkgsDist: pkgs.mkShell.override {
stdenv = pkgs.overrideCC pkgs.stdenv lean-packages.llvmPackages.clang;
} ({
buildInputs = with pkgs; [
cmake gmp libuv ccache cadical
lean-packages.llvmPackages.llvm # llvm-symbolizer for asan/lsan
gdb
tree # for CI
];
# https://github.com/NixOS/nixpkgs/issues/60919
hardeningDisable = [ "all" ];
# more convenient `ctest` output
CTEST_OUTPUT_ON_FAILURE = 1;
} // pkgs.lib.optionalAttrs pkgs.stdenv.isLinux {
GMP = (pkgsDist.gmp.override { withStatic = true; }).overrideAttrs (attrs:
pkgs.lib.optionalAttrs (pkgs.stdenv.system == "aarch64-linux") {
# would need additional linking setup on Linux aarch64, we don't use it anywhere else either
hardeningDisable = [ "stackprotector" ];
});
LIBUV = pkgsDist.libuv.overrideAttrs (attrs: {
configureFlags = ["--enable-static"];
hardeningDisable = [ "stackprotector" ];
# Sync version with CMakeLists.txt
version = "1.48.0";
src = pkgs.fetchFromGitHub {
owner = "libuv";
repo = "libuv";
rev = "v1.48.0";
sha256 = "100nj16fg8922qg4m2hdjh62zv4p32wyrllsvqr659hdhjc03bsk";
};
doCheck = false;
});
GLIBC = pkgsDist.glibc;
GLIBC_DEV = pkgsDist.glibc.dev;
GCC_LIB = pkgsDist.gcc.cc.lib;
ZLIB = pkgsDist.zlib;
GDB = pkgsDist.gdb;
});
pkgs = import nixpkgs {
inherit system;
# for `vscode-with-extensions`
config.allowUnfree = true;
};
lean-packages = pkgs.callPackage (./nix/packages.nix) { src = ./.; inherit nix lean4-mode; };
in {
packages = {
# to be removed when Nix CI is not needed anymore
inherit (lean-packages) cacheRoots test update-stage0-commit ciShell;
deprecated = lean-packages;
packages = lean-packages // rec {
debug = lean-packages.override { debug = true; };
stage0debug = lean-packages.override { stage0debug = true; };
asan = lean-packages.override { extraCMakeFlags = [ "-DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address" "-DLEANC_EXTRA_FLAGS=-fsanitize=address" "-DSMALL_ALLOCATOR=OFF" "-DSYMBOLIC=OFF" ]; };
asandebug = asan.override { debug = true; };
tsan = lean-packages.override {
extraCMakeFlags = [ "-DLEAN_EXTRA_CXX_FLAGS=-fsanitize=thread" "-DLEANC_EXTRA_FLAGS=-fsanitize=thread" "-DCOMPRESSED_OBJECT_HEADER=OFF" ];
stage0 = (lean-packages.override {
# Compressed headers currently trigger data race reports in tsan.
# Turn them off for stage 0 as well so stage 1 can read its own stdlib.
extraCMakeFlags = [ "-DCOMPRESSED_OBJECT_HEADER=OFF" ];
}).stage1;
};
tsandebug = tsan.override { debug = true; };
stage0-from-input = lean-packages.override {
stage0 = pkgs.writeShellScriptBin "lean" ''
exec ${inputs.lean-stage0.packages.${system}.lean}/bin/lean -Dinterpreter.prefer_native=false "$@"
'';
};
inherit self;
};
defaultPackage = lean-packages.lean-all;
inherit (lean-packages) devShell;
checks.lean = lean-packages.test;
}) // rec {
templates.pkg = {
path = ./nix/templates/pkg;
description = "A custom Lean package";
};
# The default development shell for working on lean itself
devShells.default = devShellWithDist pkgs;
devShells.oldGlibc = devShellWithDist pkgsDist-old;
devShells.oldGlibcAArch = devShellWithDist pkgsDist-old-aarch;
});
defaultTemplate = templates.pkg;
};
}

View File

@@ -1,13 +1,13 @@
{ src, debug ? false, stage0debug ? false, extraCMakeFlags ? [],
stdenv, lib, cmake, gmp, libuv, cadical, git, gnumake, bash, buildLeanPackage, writeShellScriptBin, runCommand, symlinkJoin, lndir, perl, gnused, darwin, llvmPackages, linkFarmFromDrvs,
stdenv, lib, cmake, gmp, 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 {
rec {
inherit stdenv;
sourceByRegex = p: rs: lib.sourceByRegex p (map (r: "(/src/)?${r}") rs);
buildCMake = args: stdenv.mkDerivation ({
nativeBuildInputs = [ cmake ];
buildInputs = [ gmp libuv llvmPackages.llvm ];
buildInputs = [ gmp llvmPackages.llvm ];
# https://github.com/NixOS/nixpkgs/issues/60919
hardeningDisable = [ "all" ];
dontStrip = (args.debug or debug);
@@ -17,7 +17,7 @@ lib.warn "The Nix-based build is deprecated" rec {
'';
} // args // {
src = args.realSrc or (sourceByRegex args.src [ "[a-z].*" "CMakeLists\.txt" ]);
cmakeFlags = (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" ];
cmakeFlags = (args.cmakeFlags or [ "-DSTAGE=1" "-DPREV_STAGE=./faux-prev-stage" "-DUSE_GITHASH=OFF" ]) ++ (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
@@ -26,7 +26,11 @@ lib.warn "The Nix-based build is deprecated" rec {
lean-bin-tools-unwrapped = buildCMake {
name = "lean-bin-tools";
outputs = [ "out" "leanc_src" ];
realSrc = sourceByRegex (src + "/src") [ "CMakeLists\.txt" "[a-z].*" ".*\.in" "Leanc\.lean" ];
realSrc = sourceByRegex (src + "/src") [ "CMakeLists\.txt" "cmake.*" "bin.*" "include.*" ".*\.in" "Leanc\.lean" ];
preConfigure = ''
touch empty.cpp
sed -i 's/add_subdirectory.*//;s/set(LEAN_OBJS.*/set(LEAN_OBJS empty.cpp)/' CMakeLists.txt
'';
dontBuild = true;
installPhase = ''
mkdir $out $leanc_src
@@ -41,10 +45,11 @@ lib.warn "The Nix-based build is deprecated" rec {
leancpp = buildCMake {
name = "leancpp";
src = src + "/src";
buildFlags = [ "leancpp" "leanrt" "leanrt_initial-exec" "leanshell" "leanmain" ];
buildFlags = [ "leancpp" "leanrt" "leanrt_initial-exec" "shell" ];
installPhase = ''
mkdir -p $out
mv lib/ $out/
mv shell/CMakeFiles/shell.dir/lean.cpp.o $out/lib
mv runtime/libleanrt_initial-exec.a $out/lib
'';
};
@@ -60,7 +65,12 @@ lib.warn "The Nix-based build is deprecated" rec {
installPhase = ''
mkdir -p $out/bin $out/lib/lean
mv bin/lean $out/bin/
mv lib/lean/*.{so,dylib} $out/lib/lean
mv lib/lean/libleanshared.* $out/lib/lean
'' + lib.optionalString stdenv.isDarwin ''
for lib in $(otool -L $out/bin/lean | tail -n +2 | cut -d' ' -f1); do
if [[ "$lib" == *lean* ]]; then install_name_tool -change "$lib" "$out/lib/lean/$(basename $lib)" $out/bin/lean; fi
done
otool -L $out/bin/lean
'';
meta.mainProgram = "lean";
});
@@ -82,8 +92,7 @@ lib.warn "The Nix-based build is deprecated" rec {
leanFlags = [ "-DwarningAsError=true" ];
} // args);
Init' = build { name = "Init"; deps = []; };
Std' = build { name = "Std"; deps = [ Init' ]; };
Lean' = build { name = "Lean"; deps = [ Std' ]; };
Lean' = build { name = "Lean"; deps = [ Init' ]; };
attachSharedLib = sharedLib: pkg: pkg // {
inherit sharedLib;
mods = mapAttrs (_: m: m // { inherit sharedLib; propagatedLoadDynlibs = []; }) pkg.mods;
@@ -91,61 +100,49 @@ lib.warn "The Nix-based build is deprecated" rec {
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 ]; };
Lean = attachSharedLib leanshared Lean' // { allExternalDeps = [ Init ]; };
Lake = build {
name = "Lake";
sharedLibName = "Lake_shared";
src = src + "/src/lake";
deps = [ Init Lean ];
};
Lake-Main = build {
name = "LakeMain";
roots = [{ glob = "one"; mod = "LakeMain"; }];
name = "Lake.Main";
roots = [ "Lake.Main" ];
executableName = "lake";
deps = [ Lake ];
linkFlags = lib.optional stdenv.isLinux "-rdynamic";
src = src + "/src/lake";
};
stdlib = [ Init Std Lean Lake ];
stdlib = [ Init 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
'';
stdlibLinkFlags = "-L${Init.staticLib} -L${Lean.staticLib} -L${Lake.staticLib} -L${leancpp}/lib/lean";
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} \
${if stdenv.isDarwin then "-Wl,-force_load,${Init.staticLib}/libInit.a -Wl,-force_load,${Lean.staticLib}/libLean.a -Wl,-force_load,${leancpp}/lib/lean/libleancpp.a ${leancpp}/lib/libleanrt_initial-exec.a -lc++"
else "-Wl,--whole-archive -lInit -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_CC=${stdenv.cc}/bin/cc ${Leanc.executable}/bin/leanc -I${lean-bin-tools-unwrapped}/include ${stdlibLinkFlags} -L${leanshared} "$@"
'';
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
${leanc}/bin/leanc ${leancpp}/lib/lean.cpp.o ${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/
ln -sf ${leancpp}/lib/lean/* ${lib.concatMapStringsSep " " (l: "${l.modRoot}/* ${l.staticLib}/*") (lib.reverseList stdlib)} ${leanshared}/* $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`
@@ -153,13 +150,15 @@ lib.warn "The Nix-based build is deprecated" rec {
'';
meta.mainProgram = "lean";
};
cacheRoots = linkFarmFromDrvs "cacheRoots" ([
cacheRoots = linkFarmFromDrvs "cacheRoots" [
stage0 lean leanc lean-all iTree modDepsFiles depRoots Leanc.src
] ++ map (lib: lib.oTree) stdlib);
# .o files are not a runtime dependency on macOS because of lack of thin archives
Lean.oTree Lake.oTree
];
test = buildCMake {
name = "lean-test-${desc}";
realSrc = lib.sourceByRegex src [ "src.*" "tests.*" ];
buildInputs = [ gmp libuv perl git cadical ];
buildInputs = [ gmp perl git ];
preConfigure = ''
cd src
'';
@@ -170,17 +169,16 @@ lib.warn "The Nix-based build is deprecated" rec {
ln -sf ${lean-all}/* .
'';
buildPhase = ''
ctest --output-junit test-results.xml --output-on-failure -E 'leancomptest_(doc_example|foreign)|leanlaketest_reverse-ffi' -j$NIX_BUILD_CORES
ctest --output-on-failure -E 'leancomptest_(doc_example|foreign)' -j$NIX_BUILD_CORES
'';
installPhase = ''
mkdir $out
mv test-results.xml $out
touch $out
'';
};
update-stage0 =
let cTree = symlinkJoin { name = "cs"; paths = map (lib: lib.cTree) (stdlib ++ [Lake-Main]); }; in
let cTree = symlinkJoin { name = "cs"; paths = [ Init.cTree Lean.cTree ]; }; in
writeShellScriptBin "update-stage0" ''
CSRCS=${cTree} CP_C_PARAMS="--dereference --no-preserve=all" ${src + "/script/lib/update-stage0"}
CSRCS=${cTree} CP_C_PARAMS="--dereference --no-preserve=all" ${src + "/script/update-stage0"}
'';
update-stage0-commit = writeShellScriptBin "update-stage0-commit" ''
set -euo pipefail

View File

@@ -1,16 +1,16 @@
{ lean, lean-leanDeps ? lean, lean-final ? lean, leanc,
stdenv, lib, coreutils, gnused, writeShellScriptBin, bash, substituteAll, symlinkJoin, linkFarmFromDrvs,
stdenv, lib, coreutils, gnused, writeShellScriptBin, bash, lean-emacs, lean-vscode, nix, 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 ],
deps ? [ 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 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 ? [],
@@ -30,7 +30,7 @@ lib.makeOverridable (
pluginDeps ? [],
# `overrideAttrs` for `buildMod`
overrideBuildModAttrs ? null,
debug ? false, leanFlags ? [], leancFlags ? [], linkFlags ? [], executableName ? lib.toLower name, libName ? name, sharedLibName ? libName,
debug ? false, leanFlags ? [], leancFlags ? [], linkFlags ? [], executableName ? lib.toLower name, libName ? name,
srcTarget ? "..#stage0", srcArgs ? "(\${args[*]})", lean-final ? lean-final' }@args:
with builtins; let
# "Init.Core" ~> "Init/Core"
@@ -88,9 +88,9 @@ with builtins; let
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`,
# 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 =
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}";
@@ -176,7 +176,7 @@ with builtins; let
# 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"}
leanc -c -o $out/$oPath $leancFlags -fPIC ${if debug then "${drv.c}/${drv.cPath} -g" else "src.c -O3 -DNDEBUG"}
'';
};
mkMod = mod: deps:
@@ -197,6 +197,19 @@ with builtins; let
then map (m: m.module) header.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;
makeEmacsWrapper = name: emacs: lean: writeShellScriptBin name ''
${emacs} --eval "(progn (setq lean4-rootdir \"${lean}\"))" "$@"
'';
makeVSCodeWrapper = name: lean: writeShellScriptBin name ''
PATH=${lean}/bin:$PATH ${lean-vscode}/bin/code "$@"
'';
printPaths = deps: writeShellScriptBin "print-paths" ''
echo '${toJSON {
oleanPath = [(depRoot "print-paths" deps)];
srcPath = ["."] ++ map (dep: dep.src) allExternalDeps;
loadDynlibPaths = map pathOfSharedLib (loadDynlibsOfDeps deps);
}}'
'';
expandGlob = g:
if typeOf g == "string" then [g]
else if g.glob == "one" then [g.mod]
@@ -211,8 +224,7 @@ with builtins; let
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 ]; } ''
staticLib = runCommand "${name}-lib" { buildInputs = [ stdenv.cc.bintools.bintools ]; } ''
mkdir -p $out
ar Trcs $out/lib${libName}.a ${lib.concatStringsSep " " (map (drv: "${drv}/${drv.oPath}") (attrValues objects))};
'';
@@ -233,7 +245,7 @@ in rec {
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}" ''
sharedLib = mkSharedLib "lib${libName}" ''
${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
@@ -244,4 +256,48 @@ in rec {
-o $out/bin/${executableName} \
${lib.concatStringsSep " " allLinkFlags}
'') {};
lean-package = writeShellScriptBin "lean" ''
LEAN_PATH=${modRoot}:$LEAN_PATH LEAN_SRC_PATH=$LEAN_SRC_PATH:${src} exec ${lean-final}/bin/lean "$@"
'';
emacs-package = makeEmacsWrapper "emacs-package" lean-package;
vscode-package = makeVSCodeWrapper "vscode-package" lean-package;
link-ilean = writeShellScriptBin "link-ilean" ''
dest=''${1:-.}
mkdir -p $dest/build/lib
ln -sf ${iTree}/* $dest/build/lib
'';
makePrintPathsFor = deps: mods: printPaths deps // mapAttrs (_: mod: makePrintPathsFor (deps ++ [mod]) mods) mods;
print-paths = makePrintPathsFor [] (mods' // externalModMap);
# `lean` wrapper that dynamically runs Nix for the actual `lean` executable so the same editor can be
# used for multiple projects/after upgrading the `lean` input/for editing both stage 1 and the tests
lean-bin-dev = substituteAll {
name = "lean";
dir = "bin";
src = ./lean-dev.in;
isExecutable = true;
srcRoot = fullSrc; # use root flake.nix in case of Lean repo
inherit bash nix srcTarget srcArgs;
};
lake-dev = substituteAll {
name = "lake";
dir = "bin";
src = ./lake-dev.in;
isExecutable = true;
srcRoot = fullSrc; # use root flake.nix in case of Lean repo
inherit bash nix srcTarget srcArgs;
};
lean-dev = symlinkJoin { name = "lean-dev"; paths = [ lean-bin-dev lake-dev ]; };
emacs-dev = makeEmacsWrapper "emacs-dev" "${lean-emacs}/bin/emacs" lean-dev;
emacs-path-dev = makeEmacsWrapper "emacs-path-dev" "emacs" lean-dev;
vscode-dev = makeVSCodeWrapper "vscode-dev" lean-dev;
devShell = mkShell {
buildInputs = [ nix ];
shellHook = ''
export LEAN_SRC_PATH="${srcPath}"
'';
};
})

View File

@@ -1,6 +1,9 @@
{ src, pkgs, ... } @ args:
{ src, pkgs, nix, ... } @ args:
with pkgs;
let
nix-pinned = writeShellScriptBin "nix" ''
${nix.packages.${system}.default}/bin/nix --experimental-features 'nix-command flakes' --extra-substituters https://lean4.cachix.org/ --option warn-dirty false "$@"
'';
# https://github.com/NixOS/nixpkgs/issues/130963
llvmPackages = if stdenv.isDarwin then llvmPackages_11 else llvmPackages_15;
cc = (ccacheWrapper.override rec {
@@ -39,9 +42,40 @@ let
inherit (lean) stdenv;
lean = lean.stage1;
inherit (lean.stage1) leanc;
inherit lean-emacs lean-vscode;
nix = nix-pinned;
}));
lean4-mode = emacsPackages.melpaBuild {
pname = "lean4-mode";
version = "1";
commit = "1";
src = args.lean4-mode;
packageRequires = with pkgs.emacsPackages.melpaPackages; [ dash f flycheck magit-section lsp-mode s ];
recipe = pkgs.writeText "recipe" ''
(lean4-mode
:repo "leanprover/lean4-mode"
:fetcher github
:files ("*.el" "data"))
'';
};
lean-emacs = emacsWithPackages [ lean4-mode ];
# updating might be nicer by building from source from a flake input, but this is good enough for now
vscode-lean4 = vscode-utils.extensionFromVscodeMarketplace {
name = "lean4";
publisher = "leanprover";
version = "0.0.63";
sha256 = "sha256-kjEex7L0F2P4pMdXi4NIZ1y59ywJVubqDqsoYagZNkI=";
};
lean-vscode = vscode-with-extensions.override {
vscodeExtensions = [ vscode-lean4 ];
};
in {
inherit cc buildLeanPackage llvmPackages;
inherit cc lean4-mode buildLeanPackage llvmPackages vscode-lean4;
lean = lean.stage1;
stage0print-paths = lean.stage1.Lean.print-paths;
HEAD-as-stage0 = (lean.stage1.Lean.overrideArgs { srcTarget = "..#stage0-from-input.stage0"; srcArgs = "(--override-input lean-stage0 ..\?rev=$(git rev-parse HEAD) -- -Dinterpreter.prefer_native=false \"$@\")"; });
HEAD-as-stage1 = (lean.stage1.Lean.overrideArgs { srcTarget = "..\?rev=$(git rev-parse HEAD)#stage0"; });
nix = nix-pinned;
nixpkgs = pkgs;
ciShell = writeShellScriptBin "ciShell" ''
set -o pipefail
@@ -49,4 +83,5 @@ in {
# prefix lines with cumulative and individual execution time
"$@" |& ts -i "(%.S)]" | ts -s "[%M:%S"
'';
} // lean.stage1
vscode = lean-vscode;
} // lean.stage1.Lean // lean.stage1 // lean

View File

@@ -1,22 +0,0 @@
Draft release notes
-------------------
This folder contains drafts of release notes for inclusion in `RELEASES.md`.
During the process to create a release candidate, we look through all the commits that make up the release
to prepare the release notes, and in that process we take these drafts into account.
Guidelines:
- You should prefer adding release notes to commit messages over adding anything to this folder.
A release note should briefly explain the impact of a change from a user's point of view.
Please mark these parts out with words such as **release notes** and/or **breaking changes**.
- It is not necessary to add anything to this folder. It is meant for larger features that span multiple PRs,
or for anything that would be helpful when preparing the release notes that might be missed
by someone reading through the change log.
- If the PR that adds a feature simultaneously adds a draft release note, including the PR number is not required
since it can be obtained from the git history for the file.
When release notes are prepared, all the draft release notes are deleted from this folder.
For release candidates beyond the first one, you can either update `RELEASE.md` directly
or continue to add drafts.
When a release is finalized, we will copy the completed release notes from `RELEASE.md` to the `master` branch.

View File

@@ -1,8 +1,3 @@
/-
Copyright (c) 2022 Sebastian Ullrich. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sebastian Ullrich
-/
import Lean.Runtime
abbrev M := ReaderT IO.FS.Stream IO
@@ -21,7 +16,7 @@ def mkTypedefFn (i : Nat) : M Unit := do
emit s!"typedef obj* (*fn{i})({args}); // NOLINT\n"
emit s!"#define FN{i}(f) reinterpret_cast<fn{i}>(lean_closure_fun(f))\n"
def genSeq (n : Nat) (f : Nat String) (sep := ", ") : String :=
def genSeq (n : Nat) (f : Nat String) (sep := ", ") : String :=
List.range n |>.map f |>.intersperse sep |> .join
-- make string: "obj* a1, obj* a2, ..., obj* an"

View File

@@ -1,28 +0,0 @@
import Lean.Util.Profiler
/-!
Usage:
```sh
lean --run ./script/collideProfiles.lean **/*.lean.json ... > merged.json
```
Merges multiple `trace.profiler.output` profiles into a single one while deduplicating samples with
the same stack. This is useful for building cumulative profiles of medium-to-large projects because
Firefox Profiler cannot handle hundreds of tracks and the deduplication will also ensure that the
profile is small enough for uploading.
As ordering of samples is not meaningful after this transformation, only "Call Tree" and "Flame
Graph" are useful for such profiles.
-/
open Lean
def main (args : List String) : IO Unit := do
let profiles args.toArray.mapM fun path => do
let json IO.FS.readFile path
let profile IO.ofExcept $ Json.parse json
IO.ofExcept <| fromJson? profile
-- NOTE: `collide` should not be interpreted
let profile := Firefox.Profile.collide profiles
IO.println <| Json.compress <| toJson profile

View File

@@ -1,39 +0,0 @@
#!/bin/bash
# https://chat.openai.com/share/7469c7c3-aceb-4d80-aee5-62982e1f1538
# Output CSV Header
echo '"Issue URL","Title","Days Since Creation","Days Since Last Update","Total Reactions","Assignee","Labels"'
# Get the current date in YYYY-MM-DD format
today=$(date +%Y-%m-%d)
# Fetch only open issues (excluding PRs and closed issues) from the repository 'leanprover/lean4'
issues=$(gh api repos/leanprover/lean4/issues --paginate --jq '.[] | select(.pull_request == null and .state == "open") | {url: .html_url, title: .title, created_at: (.created_at | split("T")[0]), updated_at: (.updated_at | split("T")[0]), number: .number, assignee: (.assignee.login // ""), labels: [.labels[].name] | join(",")}')
# Process each JSON object
echo "$issues" | while IFS= read -r issue; do
# Extract fields from JSON
url=$(echo "$issue" | jq -r '.url')
title=$(echo "$issue" | jq -r '.title')
created_at=$(echo "$issue" | jq -r '.created_at')
updated_at=$(echo "$issue" | jq -r '.updated_at')
issue_number=$(echo "$issue" | jq -r '.number')
assignee=$(echo "$issue" | jq -r '.assignee')
labels=$(echo "$issue" | jq -r '.labels')
# Calculate days since creation and update using macOS compatible date calculation
days_since_created=$(( ($(date -jf "%Y-%m-%d" "$today" +%s) - $(date -jf "%Y-%m-%d" "$created_at" +%s)) / 86400 ))
days_since_updated=$(( ($(date -jf "%Y-%m-%d" "$today" +%s) - $(date -jf "%Y-%m-%d" "$updated_at" +%s)) / 86400 ))
# Fetch the total number of reactions for each issue
reaction_data=$(gh api repos/leanprover/lean4/issues/$issue_number/reactions --paginate --jq 'length' 2>&1)
if [[ $reaction_data == *"Not Found"* ]]; then
total_reactions="Error fetching reactions"
else
total_reactions=$reaction_data
fi
# Format output as CSV by escaping quotes and delimiting with commas
echo "\"$url\",\"${title//\"/\"\"}\",\"$days_since_created\",\"$days_since_updated\",\"$total_reactions\",\"$assignee\",\"$labels\""
done

View File

@@ -1,2 +0,0 @@
This directory contains various scripts that are *not* meant to be called
directly, but through other scripts or makefiles.

View File

@@ -1,19 +0,0 @@
#!/usr/bin/env bash
# Script internal to `./script/rebase-stage0.sh`
# Determine OS type for sed in-place editing
SED_CMD=("sed" "-i")
if [[ "$OSTYPE" == "darwin"* ]]
then
# macOS requires an empty string argument with -i for in-place editing
SED_CMD=("sed" "-i" "")
fi
if [ "$STAGE0_WITH_NIX" = true ]
then
"${SED_CMD[@]}" '/chore: update stage0/ s,.*,x nix run .#update-stage0-commit,' "$1"
else
"${SED_CMD[@]}" '/chore: update stage0/ s,.*,x make -j32 -C build/release update-stage0 \&\& git commit -m "chore: update stage0",' "$1"
fi

View File

@@ -1,33 +0,0 @@
#!/usr/bin/env bash
set -euo pipefail
rm -r stage0 || true
# don't copy untracked files
# `:!` is git glob flavor for exclude patterns
for f in $(git ls-files src ':!:src/lake/*' ':!:src/Leanc.lean'); do
if [[ $f == *.lean ]]; then
f=${f#src/}
f=${f%.lean}.c
mkdir -p $(dirname stage0/stdlib/$f)
cp ${CP_C_PARAMS:-} $CSRCS/$f stage0/stdlib/$f
else
mkdir -p $(dirname stage0/$f)
cp $f stage0/$f
fi
done
# special handling for Lake files due to its nested directory
# copy the README to ensure the `stage0/src/lake` directory is committed
for f in $(git ls-files 'src/lake/Lake/*' src/lake/Lake.lean src/lake/LakeMain.lean src/lake/README.md ':!:src/lakefile.toml'); do
if [[ $f == *.lean ]]; then
f=${f#src/lake}
f=${f%.lean}.c
mkdir -p $(dirname stage0/stdlib/$f)
cp ${CP_C_PARAMS:-} $CSRCS/$f stage0/stdlib/$f
else
mkdir -p $(dirname stage0/$f)
cp $f stage0/$f
fi
done
git add stage0

View File

@@ -25,8 +25,6 @@ cp -L llvm/bin/llvm-ar stage1/bin/
# dependencies of the above
$CP llvm/lib/lib{clang-cpp,LLVM}*.so* stage1/lib/
$CP $ZLIB/lib/libz.so* stage1/lib/
# general clang++ dependency, breaks cross-library C++ exceptions if linked statically
$CP $GCC_LIB/lib/libgcc_s.so* stage1/lib/
# bundle libatomic (referenced by LLVM >= 15, and required by the lean executable to run)
$CP $GCC_LIB/lib/libatomic.so* stage1/lib/
@@ -38,7 +36,7 @@ $CP $GLIBC/lib/*crt* llvm/lib/
$CP $GLIBC/lib/*crt* stage1/lib/
# runtime
(cd llvm; $CP --parents lib/clang/*/lib/*/{clang_rt.*.o,libclang_rt.builtins*} ../stage1)
$CP llvm/lib/*/lib{c++,c++abi,unwind}.* $GMP/lib/libgmp.a $LIBUV/lib/libuv.a stage1/lib/
$CP llvm/lib/*/lib{c++,c++abi,unwind}.* $GMP/lib/libgmp.a stage1/lib/
# LLVM 15 appears to ship the dependencies in 'llvm/lib/<target-triple>/' and 'llvm/include/<target-triple>/'
# but clang-15 that we use to compile is linked against 'llvm/lib/' and 'llvm/include'
# https://github.com/llvm/llvm-project/issues/54955
@@ -48,8 +46,6 @@ $CP llvm-host/lib/*/lib{c++,c++abi,unwind}.* llvm-host/lib/
$CP -r llvm/include/*-*-* llvm-host/include/
# glibc: use for linking (so Lean programs don't embed newer symbol versions), but not for running (because libc.so, librt.so, and ld.so must be compatible)!
$CP $GLIBC/lib/libc_nonshared.a stage1/lib/glibc
# libpthread_nonshared.a must be linked in order to be able to use `pthread_atfork(3)`. LibUV uses this function.
$CP $GLIBC/lib/libpthread_nonshared.a stage1/lib/glibc
for f in $GLIBC/lib/lib{c,dl,m,rt,pthread}-*; do b=$(basename $f); cp $f stage1/lib/glibc/${b%-*}.so; done
OPTIONS=()
echo -n " -DLEAN_STANDALONE=ON"
@@ -64,8 +60,8 @@ fi
# use `-nostdinc` to make sure headers are not visible by default (in particular, not to `#include_next` in the clang headers),
# but do not change sysroot so users can still link against system libs
echo -n " -DLEANC_INTERNAL_FLAGS='-nostdinc -isystem ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang"
echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/glibc ROOT/lib/glibc/libc_nonshared.a ROOT/lib/glibc/libpthread_nonshared.a -Wl,--as-needed -Wl,-Bstatic -lgmp -lunwind -luv -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld'"
echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/glibc ROOT/lib/glibc/libc_nonshared.a -Wl,--as-needed -static-libgcc -Wl,-Bstatic -lgmp -lunwind -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld'"
# when not using the above flags, link GMP dynamically/as usual
echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-Wl,--as-needed -lgmp -luv -lpthread -ldl -lrt -Wl,--no-as-needed'"
echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-Wl,--as-needed -lgmp -Wl,--no-as-needed'"
# do not set `LEAN_CC` for tests
echo -n " -DLEAN_TEST_VARS=''"

View File

@@ -9,7 +9,6 @@ set -uxo pipefail
# use full LLVM release for compiling C++ code, but subset for compiling C code and distribution
GMP=${GMP:-$(brew --prefix)}
LIBUV=${LIBUV:-$(brew --prefix)}
[[ -d llvm ]] || (mkdir llvm; gtar xf $1 --strip-components 1 --directory llvm)
[[ -d llvm-host ]] || if [[ "$#" -gt 1 ]]; then
@@ -47,9 +46,8 @@ echo -n " -DLEAN_EXTRA_CXX_FLAGS='${EXTRA_FLAGS:-}'"
if [[ -L llvm-host ]]; then
echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang"
gcp $GMP/lib/libgmp.a stage1/lib/
gcp $LIBUV/lib/libuv.a stage1/lib/
echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/libc -fuse-ld=lld'"
echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp -luv'"
echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp'"
else
echo -n " -DCMAKE_C_COMPILER=$PWD/llvm-host/bin/clang -DLEANC_OPTS='--sysroot $PWD/stage1 -resource-dir $PWD/stage1/lib/clang/15.0.1 ${EXTRA_FLAGS:-}'"
echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/libc -fuse-ld=lld'"

View File

@@ -31,21 +31,15 @@ cp /clang64/lib/{crtbegin,crtend,crt2,dllcrt2}.o stage1/lib/
# runtime
(cd llvm; cp --parents lib/clang/*/lib/*/libclang_rt.builtins* ../stage1)
# further dependencies
# Note: even though we're linking against libraries like `libbcrypt.a` which appear to be static libraries from the file name,
# we're not actually linking statically against the code.
# Rather, `libbcrypt.a` is an import library (see https://en.wikipedia.org/wiki/Dynamic-link_library#Import_libraries) that just
# tells the compiler how to dynamically link against `bcrypt.dll` (which is located in the System32 folder).
# This distinction is relevant specifically for `libicu.a`/`icu.dll` because there we want updates to the time zone database to
# be delivered to users via Windows Update without having to recompile Lean or Lean programs.
cp /clang64/lib/lib{m,bcrypt,mingw32,moldname,mingwex,msvcrt,pthread,advapi32,shell32,user32,kernel32,ucrtbase,psapi,iphlpapi,userenv,ws2_32,dbghelp,ole32,icu}.* /clang64/lib/libgmp.a /clang64/lib/libuv.a llvm/lib/lib{c++,c++abi,unwind}.a stage1/lib/
cp /clang64/lib/lib{m,bcrypt,mingw32,moldname,mingwex,msvcrt,pthread,advapi32,shell32,user32,kernel32,ucrtbase}.* /clang64/lib/libgmp.a llvm/lib/lib{c++,c++abi,unwind}.a stage1/lib/
echo -n " -DLEAN_STANDALONE=ON"
echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang.exe -DCMAKE_C_COMPILER_WORKS=1 -DCMAKE_CXX_COMPILER=$PWD/llvm/bin/clang++.exe -DCMAKE_CXX_COMPILER_WORKS=1 -DLEAN_CXX_STDLIB='-lc++ -lc++abi'"
echo -n " -DSTAGE0_CMAKE_C_COMPILER=clang -DSTAGE0_CMAKE_CXX_COMPILER=clang++"
echo -n " -DLEAN_EXTRA_CXX_FLAGS='--sysroot $PWD/llvm -idirafter /clang64/include/'"
echo -n " -DLEANC_INTERNAL_FLAGS='--sysroot ROOT -nostdinc -isystem ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang.exe"
echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -static-libgcc -Wl,-Bstatic -lgmp $(pkg-config --static --libs libuv) -lunwind -Wl,-Bdynamic -fuse-ld=lld'"
# when not using the above flags, link GMP dynamically/as usual. Always link ICU dynamically.
echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp $(pkg-config --libs libuv) -lucrtbase'"
echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -static-libgcc -Wl,-Bstatic -lgmp -lunwind -Wl,-Bdynamic -fuse-ld=lld'"
# when not using the above flags, link GMP dynamically/as usual
echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp -lucrtbase'"
# do not set `LEAN_CC` for tests
echo -n " -DAUTO_THREAD_FINALIZATION=OFF -DSTAGE0_AUTO_THREAD_FINALIZATION=OFF"
echo -n " -DLEAN_TEST_VARS=''"

View File

@@ -1,24 +0,0 @@
#!/usr/bin/env bash
# This script rebases onto the given branch/commit, and updates
# all `chore: update stage0` commits along the way.
# Whether to use nix or make to update stage0
if [ "$1" = "-nix" ]
then
export STAGE0_WITH_NIX=true
shift
fi
# Check if an argument is provided
if [ "$#" -eq 0 ]; then
echo "Usage: $0 [-nix] <options to git rebase -i>"
exit 1
fi
REPO_ROOT=$(git rev-parse --show-toplevel)
# Run git rebase in interactive mode, but automatically edit the todo list
# using the defined GIT_SEQUENCE_EDITOR command
GIT_SEQUENCE_EDITOR="$REPO_ROOT/script/lib/rebase-editor.sh" git rebase -i "$@"

18
script/update-stage0 Executable file
View File

@@ -0,0 +1,18 @@
#!/usr/bin/env bash
set -euo pipefail
rm -r stage0 || true
# don't copy untracked files
# `:!` is git glob flavor for exclude patterns
for f in $(git ls-files src ':!:src/lake/*' ':!:src/Leanc.lean'); do
if [[ $f == *.lean ]]; then
f=${f#src/}
f=${f%.lean}.c
mkdir -p $(dirname stage0/stdlib/$f)
cp ${CP_C_PARAMS:-} $CSRCS/$f stage0/stdlib/$f
else
mkdir -p $(dirname stage0/$f)
cp $f stage0/$f
fi
done
git add stage0

27
shell.nix Normal file
View File

@@ -0,0 +1,27 @@
let
flake = (import ./default.nix);
flakePkgs = flake.packages.${builtins.currentSystem};
in { pkgs ? flakePkgs.nixpkgs, pkgsDist ? pkgs }:
# use `shell` as default
(attribs: attribs.shell // attribs) rec {
shell = pkgs.mkShell.override {
stdenv = pkgs.overrideCC pkgs.stdenv flakePkgs.llvmPackages.clang;
} (rec {
buildInputs = with pkgs; [
cmake gmp ccache
flakePkgs.llvmPackages.llvm # llvm-symbolizer for asan/lsan
];
# https://github.com/NixOS/nixpkgs/issues/60919
hardeningDisable = [ "all" ];
# more convenient `ctest` output
CTEST_OUTPUT_ON_FAILURE = 1;
} // pkgs.lib.optionalAttrs pkgs.stdenv.isLinux {
GMP = pkgsDist.gmp.override { withStatic = true; };
GLIBC = pkgsDist.glibc;
GLIBC_DEV = pkgsDist.glibc.dev;
GCC_LIB = pkgsDist.gcc.cc.lib;
ZLIB = pkgsDist.zlib;
GDB = pkgsDist.gdb;
});
nix = flake.devShell.${builtins.currentSystem};
}

View File

@@ -1,6 +1,5 @@
cmake_minimum_required(VERSION 3.10)
cmake_policy(SET CMP0054 NEW)
cmake_policy(SET CMP0110 NEW)
if(NOT (${CMAKE_GENERATOR} MATCHES "Unix Makefiles"))
message(FATAL_ERROR "The only supported CMake generator at the moment is 'Unix Makefiles'")
endif()
@@ -10,15 +9,13 @@ endif()
include(ExternalProject)
project(LEAN CXX C)
set(LEAN_VERSION_MAJOR 4)
set(LEAN_VERSION_MINOR 15)
set(LEAN_VERSION_MINOR 7)
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'")
set(LEAN_VERSION_STRING "${LEAN_VERSION_MAJOR}.${LEAN_VERSION_MINOR}.${LEAN_VERSION_PATCH}")
if (LEAN_SPECIAL_VERSION_DESC)
string(APPEND LEAN_VERSION_STRING "-${LEAN_SPECIAL_VERSION_DESC}")
elseif (NOT LEAN_VERSION_IS_RELEASE)
string(APPEND LEAN_VERSION_STRING "-pre")
endif()
set(LEAN_PLATFORM_TARGET "" CACHE STRING "LLVM triple of the target platform")
@@ -76,7 +73,6 @@ option(USE_GMP "USE_GMP" 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" 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`")
@@ -157,10 +153,6 @@ endif ()
# We want explicit stack probes in huge Lean stack frames for robust stack overflow detection
string(APPEND LEANC_EXTRA_FLAGS " -fstack-clash-protection")
# This makes signed integer overflow guaranteed to match 2's complement.
string(APPEND CMAKE_CXX_FLAGS " -fwrapv")
string(APPEND LEANC_EXTRA_FLAGS " -fwrapv")
if(NOT MULTI_THREAD)
message(STATUS "Disabled multi-thread support, it will not be safe to run multiple threads in parallel")
set(AUTO_THREAD_FINALIZATION OFF)
@@ -249,77 +241,6 @@ if("${USE_GMP}" MATCHES "ON")
endif()
endif()
# LibUV
if("${CMAKE_SYSTEM_NAME}" MATCHES "Emscripten")
# Only on WebAssembly we compile LibUV ourselves
set(LIBUV_EMSCRIPTEN_FLAGS "${EMSCRIPTEN_SETTINGS}")
# LibUV does not compile on WebAssembly without modifications because
# building LibUV on a platform requires including stub implementations
# for features not present on the target platform. This patch includes
# the minimum amount of stub implementations needed for successfully
# running Lean on WebAssembly and using LibUV's temporary file support.
# It still leaves several symbols completely undefined: uv__fs_event_close,
# uv__hrtime, uv__io_check_fd, uv__io_fork, uv__io_poll, uv__platform_invalidate_fd
# uv__platform_loop_delete, uv__platform_loop_init. Making additional
# LibUV features available on WebAssembly might require adapting the
# patch to include additional LibUV source files.
set(LIBUV_PATCH_IN "
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 5e8e0166..f3b29134 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -317,6 +317,11 @@ if(CMAKE_SYSTEM_NAME STREQUAL \"GNU\")
src/unix/hurd.c)
endif()
+if(CMAKE_SYSTEM_NAME STREQUAL \"Emscripten\")
+ list(APPEND uv_sources
+ src/unix/no-proctitle.c)
+endif()
+
if(CMAKE_SYSTEM_NAME STREQUAL \"Linux\")
list(APPEND uv_defines _GNU_SOURCE _POSIX_C_SOURCE=200112)
list(APPEND uv_libraries dl rt)
")
string(REPLACE "\n" "\\n" LIBUV_PATCH ${LIBUV_PATCH_IN})
ExternalProject_add(libuv
PREFIX libuv
GIT_REPOSITORY https://github.com/libuv/libuv
# Sync version with flake.nix
GIT_TAG v1.48.0
CMAKE_ARGS -DCMAKE_BUILD_TYPE=Release -DLIBUV_BUILD_TESTS=OFF -DLIBUV_BUILD_SHARED=OFF -DCMAKE_AR=${CMAKE_AR} -DCMAKE_TOOLCHAIN_FILE=${CMAKE_TOOLCHAIN_FILE} -DCMAKE_POSITION_INDEPENDENT_CODE=ON -DCMAKE_C_FLAGS=${LIBUV_EMSCRIPTEN_FLAGS}
PATCH_COMMAND git reset --hard HEAD && printf "${LIBUV_PATCH}" > patch.diff && git apply patch.diff
BUILD_IN_SOURCE ON
INSTALL_COMMAND "")
set(LIBUV_INCLUDE_DIR "${CMAKE_BINARY_DIR}/libuv/src/libuv/include")
set(LIBUV_LIBRARIES "${CMAKE_BINARY_DIR}/libuv/src/libuv/libuv.a")
else()
find_package(LibUV 1.0.0 REQUIRED)
endif()
include_directories(${LIBUV_INCLUDE_DIR})
if(NOT LEAN_STANDALONE)
string(APPEND LEAN_EXTRA_LINKER_FLAGS " ${LIBUV_LIBRARIES}")
endif()
# Windows SDK (for ICU)
if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
# Pass 'tools' to skip MSVC version check (as MSVC/Visual Studio is not necessarily installed)
find_package(WindowsSDK REQUIRED COMPONENTS tools)
# This will give a semicolon-separated list of include directories
get_windowssdk_include_dirs(${WINDOWSSDK_LATEST_DIR} WINDOWSSDK_INCLUDE_DIRS)
# To successfully build against Windows SDK headers, the Windows SDK headers must have lower
# priority than other system headers, so use `-idirafter`. Unfortunately, CMake does not
# support this using `include_directories`.
string(REPLACE ";" "\" -idirafter \"" WINDOWSSDK_INCLUDE_DIRS "${WINDOWSSDK_INCLUDE_DIRS}")
string(APPEND CMAKE_CXX_FLAGS " -idirafter \"${WINDOWSSDK_INCLUDE_DIRS}\"")
string(APPEND LEAN_EXTRA_LINKER_FLAGS " -licu")
endif()
# ccache
if(CCACHE AND NOT CMAKE_CXX_COMPILER_LAUNCHER AND NOT CMAKE_C_COMPILER_LAUNCHER)
find_program(CCACHE_PATH ccache)
@@ -378,12 +299,13 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
cmake_path(GET ZLIB_LIBRARY PARENT_PATH ZLIB_LIBRARY_PARENT_PATH)
string(APPEND LEANSHARED_LINKER_FLAGS " -L ${ZLIB_LIBRARY_PARENT_PATH}")
endif()
string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " -lleancpp -lInit -lStd -lLean -lleanrt")
string(APPEND LEANC_STATIC_LINKER_FLAGS " -lleancpp -lInit -lLean -lleanrt")
elseif(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " -lleancpp -lInit -lStd -lLean -lnodefs.js -lleanrt")
string(APPEND LEANC_STATIC_LINKER_FLAGS " -lleancpp -lInit -lLean -lnodefs.js -lleanrt")
else()
string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " -Wl,--start-group -lleancpp -lLean -Wl,--end-group -lStd -Wl,--start-group -lInit -lleanrt -Wl,--end-group")
string(APPEND LEANC_STATIC_LINKER_FLAGS " -Wl,--start-group -lleancpp -lLean -Wl,--end-group -Wl,--start-group -lInit -lleanrt -Wl,--end-group")
endif()
string(APPEND LEANC_STATIC_LINKER_FLAGS " -lLake")
set(LEAN_CXX_STDLIB "-lstdc++" CACHE STRING "C++ stdlib linker flags")
@@ -391,22 +313,8 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
set(LEAN_CXX_STDLIB "-lc++")
endif()
string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
# in local builds, link executables and not just dynlibs against C++ stdlib as well,
# which is required for e.g. asan
if(NOT LEAN_STANDALONE)
string(APPEND CMAKE_EXE_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
endif()
# flags for user binaries = flags for toolchain binaries + Lake
set(LEANC_STATIC_LINKER_FLAGS " ${TOOLCHAIN_STATIC_LINKER_FLAGS} -lLake")
if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
set(LEANC_SHARED_LINKER_FLAGS " ${TOOLCHAIN_SHARED_LINKER_FLAGS} -Wl,--as-needed -lLake_shared -Wl,--no-as-needed")
else()
set(LEANC_SHARED_LINKER_FLAGS " ${TOOLCHAIN_SHARED_LINKER_FLAGS} -lLake_shared")
endif()
string(APPEND LEANC_STATIC_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
string(APPEND LEANSHARED_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
if (LLVM)
string(APPEND LEANSHARED_LINKER_FLAGS " -L${LLVM_CONFIG_LIBDIR} ${LLVM_CONFIG_LDFLAGS} ${LLVM_CONFIG_LIBS} ${LLVM_CONFIG_SYSTEM_LIBS}")
@@ -434,9 +342,9 @@ endif()
# get rid of unused parts of C++ stdlib
if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-dead_strip")
string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,-dead_strip")
elseif(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,--gc-sections")
string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,--gc-sections")
endif()
if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
@@ -446,25 +354,26 @@ endif()
if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
if(BSYMBOLIC)
string(APPEND LEANC_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic")
string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic")
string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,-Bsymbolic")
endif()
string(APPEND CMAKE_CXX_FLAGS " -fPIC -ftls-model=initial-exec")
string(APPEND LEANC_EXTRA_FLAGS " -fPIC")
string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN")
string(APPEND LAKESHARED_LINKER_FLAGS " -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/temp/libLake.a.export -Wl,--no-whole-archive")
string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean")
string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN")
string(APPEND CMAKE_EXE_LINKER_FLAGS " -lleanshared -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean")
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_LINKER_FLAGS " -install_name @rpath/libleanshared.dylib")
string(APPEND LAKESHARED_LINKER_FLAGS " -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/temp/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")
string(APPEND CMAKE_EXE_LINKER_FLAGS " -lleanshared -Wl,-rpath,@executable_path/../lib -Wl,-rpath,@executable_path/../lib/lean")
elseif(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
string(APPEND CMAKE_CXX_FLAGS " -fPIC")
string(APPEND LEANC_EXTRA_FLAGS " -fPIC")
# We do not use dynamic linking via leanshared for Emscripten to keep things
# simple. (And we are not interested in `Lake` anyway.) To use dynamic
# linking, we would probably have to set MAIN_MODULE=2 on `leanshared`,
# SIDE_MODULE=2 on `lean`, and set CMAKE_SHARED_LIBRARY_SUFFIX to ".js".
string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,--whole-archive -lInit -lLean -lleancpp -lleanrt ${EMSCRIPTEN_SETTINGS} -lnodefs.js -s EXIT_RUNTIME=1 -s MAIN_MODULE=1 -s LINKABLE=1 -s EXPORT_ALL=1")
elseif(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
string(APPEND LAKESHARED_LINKER_FLAGS " -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libLake_shared.dll.a -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/temp/libLake.a.export -Wl,--no-whole-archive")
string(APPEND CMAKE_EXE_LINKER_FLAGS " -lleanshared")
endif()
if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
@@ -489,8 +398,8 @@ endif()
# executable or `leanshared`, plugins would try to look them up at load time (even though they
# 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_1 -lleanshared")
# import library created by the `leanshared` target
string(APPEND LEANC_SHARED_LINKER_FLAGS " -lleanshared")
elseif("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin")
string(APPEND LEANC_SHARED_LINKER_FLAGS " -Wl,-undefined,dynamic_lookup")
endif()
@@ -503,7 +412,7 @@ endif()
# Git HASH
if(USE_GITHASH)
include(GetGitRevisionDescription)
get_git_head_revision(GIT_REFSPEC GIT_SHA1 ALLOW_LOOKING_ABOVE_CMAKE_SOURCE_DIR)
get_git_head_revision(GIT_REFSPEC GIT_SHA1)
if(${GIT_SHA1} MATCHES "GITDIR-NOTFOUND")
message(STATUS "Failed to read git_sha1")
set(GIT_SHA1 "")
@@ -547,22 +456,6 @@ if(CMAKE_OSX_SYSROOT AND NOT LEAN_STANDALONE)
string(APPEND LEANC_EXTRA_FLAGS " ${CMAKE_CXX_SYSROOT_FLAG}${CMAKE_OSX_SYSROOT}")
endif()
add_subdirectory(initialize)
add_subdirectory(shell)
# 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
ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib/temp
OUTPUT_NAME leaninitialize)
add_library(leanshell STATIC util/shell.cpp)
set_target_properties(leanshell PROPERTIES
ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib/temp
OUTPUT_NAME leanshell)
if (${CMAKE_SYSTEM_NAME} MATCHES "Windows")
string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,--whole-archive -lleanmanifest -Wl,--no-whole-archive")
endif()
if(${STAGE} GREATER 1)
# reuse C++ parts, which don't change
add_library(leanrt_initial-exec STATIC IMPORTED)
@@ -571,17 +464,13 @@ if(${STAGE} GREATER 1)
add_library(leanrt STATIC IMPORTED)
set_target_properties(leanrt PROPERTIES
IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/lib/lean/libleanrt.a")
add_library(leancpp_1 STATIC IMPORTED)
set_target_properties(leancpp_1 PROPERTIES
IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/lib/temp/libleancpp_1.a")
add_library(leancpp STATIC IMPORTED)
set_target_properties(leancpp PROPERTIES
IMPORTED_LOCATION "${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a")
add_custom_target(copy-leancpp
COMMAND cmake -E copy_if_different "${PREV_STAGE}/runtime/libleanrt_initial-exec.a" "${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a"
COMMAND cmake -E copy_if_different "${PREV_STAGE}/lib/lean/libleanrt.a" "${CMAKE_BINARY_DIR}/lib/lean/libleanrt.a"
COMMAND cmake -E copy_if_different "${PREV_STAGE}/lib/lean/libleancpp.a" "${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a"
COMMAND cmake -E copy_if_different "${PREV_STAGE}/lib/temp/libleancpp_1.a" "${CMAKE_BINARY_DIR}/lib/temp/libleancpp_1.a")
COMMAND cmake -E copy_if_different "${PREV_STAGE}/lib/lean/libleancpp.a" "${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a")
add_dependencies(leancpp copy-leancpp)
if(LLVM)
add_custom_target(copy-lean-h-bc
@@ -590,10 +479,6 @@ if(${STAGE} GREATER 1)
endif()
else()
add_subdirectory(runtime)
if("${CMAKE_SYSTEM_NAME}" MATCHES "Emscripten")
add_dependencies(leanrt libuv)
add_dependencies(leanrt_initial-exec libuv)
endif()
add_subdirectory(util)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:util>)
@@ -605,23 +490,14 @@ else()
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:constructions>)
add_subdirectory(library/compiler)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:compiler>)
add_subdirectory(initialize)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:initialize>)
# leancpp without `initialize` (see `leaninitialize` above)
add_library(leancpp_1 STATIC ${LEAN_OBJS})
set_target_properties(leancpp_1 PROPERTIES
ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib/temp
OUTPUT_NAME leancpp_1)
add_library(leancpp STATIC ${LEAN_OBJS} $<TARGET_OBJECTS:initialize>)
add_library(leancpp STATIC ${LEAN_OBJS})
set_target_properties(leancpp PROPERTIES
OUTPUT_NAME leancpp)
endif()
if((${STAGE} GREATER 0) AND CADICAL)
add_custom_target(copy-cadical
COMMAND cmake -E copy_if_different "${CADICAL}" "${CMAKE_BINARY_DIR}/bin/cadical${CMAKE_EXECUTABLE_SUFFIX}")
add_dependencies(leancpp copy-cadical)
endif()
# MSYS2 bash usually handles Windows paths relatively well, but not when putting them in the PATH
string(REGEX REPLACE "^([a-zA-Z]):" "/\\1" LEAN_BIN "${CMAKE_BINARY_DIR}/bin")
@@ -629,15 +505,13 @@ string(REGEX REPLACE "^([a-zA-Z]):" "/\\1" LEAN_BIN "${CMAKE_BINARY_DIR}/bin")
# (also looks nicer in the build log)
file(RELATIVE_PATH LIB ${LEAN_SOURCE_DIR} ${CMAKE_BINARY_DIR}/lib)
if (${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
# We do not use dynamic linking via leanshared for Emscripten to keep things
# simple. (And we are not interested in `Lake` anyway.) To use dynamic
# linking, we would probably have to set MAIN_MODULE=2 on `leanshared`,
# SIDE_MODULE=2 on `lean`, and set CMAKE_SHARED_LIBRARY_SUFFIX to ".js".
# We set `ERROR_ON_UNDEFINED_SYMBOLS=0` because our build of LibUV does not
# define all symbols, see the comment about LibUV on WebAssembly further up
# in this file.
string(APPEND LEAN_EXE_LINKER_FLAGS " ${LIB}/temp/libleanshell.a ${TOOLCHAIN_STATIC_LINKER_FLAGS} ${EMSCRIPTEN_SETTINGS} -lnodefs.js -s EXIT_RUNTIME=1 -s MAIN_MODULE=1 -s LINKABLE=1 -s EXPORT_ALL=1 -s ERROR_ON_UNDEFINED_SYMBOLS=0")
if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
set(LEANSHARED_LINKER_FLAGS "-Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libInit.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLean.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
else()
set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive -lInit -lLean -lleancpp -Wl,--no-whole-archive ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libleanshared.dll.a")
endif()
endif()
# Build the compiler using the bootstrapped C sources for stage0, and use
@@ -646,12 +520,16 @@ if (LLVM AND ${STAGE} GREATER 0)
set(EXTRA_LEANMAKE_OPTS "LLVM=1")
endif()
# Escape for `make`. Yes, twice.
string(REPLACE "$" "$$" CMAKE_EXE_LINKER_FLAGS_MAKE "${CMAKE_EXE_LINKER_FLAGS}")
string(REPLACE "$" "$$" CMAKE_EXE_LINKER_FLAGS_MAKE_MAKE "${CMAKE_EXE_LINKER_FLAGS_MAKE}")
configure_file(${LEAN_SOURCE_DIR}/stdlib.make.in ${CMAKE_BINARY_DIR}/stdlib.make)
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 Init Std Lean
COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Init Lean
VERBATIM)
# if we have LLVM enabled, then build `lean.h.bc` which has the LLVM bitcode
@@ -663,69 +541,34 @@ endif()
# We declare these as separate custom targets so they use separate `make` invocations, which makes `make` recompute which dependencies
# (e.g. `libLean.a`) are now newer than the target file
if(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
# dummy targets, see `MAIN_MODULE` discussion above
add_custom_target(Init_shared ALL
DEPENDS make_stdlib leanrt_initial-exec
COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX}
)
add_custom_target(leanshared ALL
DEPENDS Init_shared leancpp
COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_1${CMAKE_SHARED_LIBRARY_SUFFIX}
COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}
)
add_custom_target(lake_shared ALL
DEPENDS leanshared
COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}
)
else()
add_custom_target(Init_shared ALL
WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
DEPENDS make_stdlib leanrt_initial-exec
COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Init_shared
VERBATIM)
add_custom_target(leanshared ALL
WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
DEPENDS make_stdlib leancpp leanrt_initial-exec
COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make leanshared
VERBATIM)
add_custom_target(leanshared ALL
WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
DEPENDS Init_shared leancpp_1 leancpp leanshell leaninitialize
COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make leanshared
VERBATIM)
if(${STAGE} GREATER 0)
if(NOT EXISTS ${LEAN_SOURCE_DIR}/lake/Lake.lean)
message(FATAL_ERROR "src/lake does not exist. Please check out the Lake submodule using `git submodule update --init src/lake`.")
endif()
string(APPEND CMAKE_EXE_LINKER_FLAGS " -lInit_shared -lleanshared_1 -lleanshared")
endif()
if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
add_custom_target(lake_lib ALL
add_custom_target(lake ALL
WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
DEPENDS leanshared
COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Lake
VERBATIM)
add_custom_target(lake_shared ALL
WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
DEPENDS lake_lib
COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make libLake_shared
VERBATIM)
add_custom_target(lake ALL
WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
DEPENDS lake_shared
COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make lake
VERBATIM)
endif()
if(PREV_STAGE)
add_custom_target(update-stage0
COMMAND bash -c 'CSRCS=${CMAKE_BINARY_DIR}/lib/temp script/lib/update-stage0'
COMMAND bash -c 'CSRCS=${CMAKE_BINARY_DIR}/lib/temp script/update-stage0'
DEPENDS make_stdlib
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/..")
add_custom_target(update-stage0-commit
COMMAND git commit -m "chore: update stage0"
DEPENDS update-stage0)
endif()
# use Bash version for building, use Lean version in bin/ for tests & distribution
configure_file("${LEAN_SOURCE_DIR}/bin/leanc.in" "${CMAKE_BINARY_DIR}/leanc.sh" @ONLY)
if(${STAGE} GREATER 0 AND EXISTS ${LEAN_SOURCE_DIR}/Leanc.lean AND NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
if(${STAGE} GREATER 0 AND EXISTS ${LEAN_SOURCE_DIR}/Leanc.lean)
configure_file("${LEAN_SOURCE_DIR}/Leanc.lean" "${CMAKE_BINARY_DIR}/leanc/Leanc.lean" @ONLY)
add_custom_target(leanc ALL
WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/leanc
@@ -738,9 +581,7 @@ file(COPY ${LEAN_SOURCE_DIR}/bin/leanmake DESTINATION ${CMAKE_BINARY_DIR}/bin)
install(DIRECTORY "${CMAKE_BINARY_DIR}/bin/" USE_SOURCE_PERMISSIONS DESTINATION bin)
if (${STAGE} GREATER 0 AND CADICAL)
install(PROGRAMS "${CADICAL}" DESTINATION bin)
endif()
add_subdirectory(shell)
add_custom_target(clean-stdlib
COMMAND rm -rf "${CMAKE_BINARY_DIR}/lib" || true)
@@ -778,14 +619,3 @@ if(LEAN_INSTALL_PREFIX)
set(LEAN_INSTALL_SUFFIX "-${LOWER_SYSTEM_NAME}" CACHE STRING "If LEAN_INSTALL_PREFIX is set, append this value to CMAKE_INSTALL_PREFIX")
set(CMAKE_INSTALL_PREFIX "${LEAN_INSTALL_PREFIX}/lean-${LEAN_VERSION_STRING}${LEAN_INSTALL_SUFFIX}")
endif()
# Escape for `make`. Yes, twice.
string(REPLACE "$" "$$" CMAKE_EXE_LINKER_FLAGS_MAKE "${CMAKE_EXE_LINKER_FLAGS}")
string(REPLACE "$" "$$" CMAKE_EXE_LINKER_FLAGS_MAKE_MAKE "${CMAKE_EXE_LINKER_FLAGS_MAKE}")
configure_file(${LEAN_SOURCE_DIR}/stdlib.make.in ${CMAKE_BINARY_DIR}/stdlib.make)
if(USE_LAKE AND STAGE EQUAL 1)
configure_file(${LEAN_SOURCE_DIR}/lakefile.toml.in ${LEAN_SOURCE_DIR}/lakefile.toml)
configure_file(${LEAN_SOURCE_DIR}/lakefile.toml.in ${LEAN_SOURCE_DIR}/../tests/lakefile.toml)
configure_file(${LEAN_SOURCE_DIR}/lakefile.toml.in ${LEAN_SOURCE_DIR}/../lakefile.toml)
endif()

View File

@@ -8,7 +8,6 @@ import Init.Prelude
import Init.Notation
import Init.Tactics
import Init.TacticsExtra
import Init.ByCases
import Init.RCases
import Init.Core
import Init.Control
@@ -24,16 +23,8 @@ 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.While
import Init.Syntax

View File

@@ -1,82 +0,0 @@
/-
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Gabriel Ebner
-/
prelude
import Init.NotationExtra
namespace Lean
/--
The syntax category of binder predicates contains predicates like `> 0`, `∈ s`, etc.
(`: t` should not be a binder predicate because it would clash with the built-in syntax for ∀/∃.)
-/
declare_syntax_cat binderPred
/--
`satisfies_binder_pred% t pred` expands to a proposition expressing that `t` satisfies `pred`.
-/
syntax "satisfies_binder_pred% " term:max binderPred : term
-- Extend ∀ and ∃ to binder predicates.
/--
The notation `∃ x < 2, p x` is shorthand for `∃ x, x < 2 ∧ p x`,
and similarly for other binary operators.
-/
syntax "" binderIdent binderPred ", " term : term
/--
The notation `∀ x < 2, p x` is shorthand for `∀ x, x < 2 → p x`,
and similarly for other binary operators.
-/
syntax "" binderIdent binderPred ", " term : term
macro_rules
| `( $x:ident $pred:binderPred, $p) =>
`( $x:ident, satisfies_binder_pred% $x $pred $p)
| `( _ $pred:binderPred, $p) =>
`( x, satisfies_binder_pred% x $pred $p)
macro_rules
| `( $x:ident $pred:binderPred, $p) =>
`( $x:ident, satisfies_binder_pred% $x $pred $p)
| `( _ $pred:binderPred, $p) =>
`( x, satisfies_binder_pred% x $pred $p)
/-- Declare `∃ x > y, ...` as syntax for `∃ x, x > y ∧ ...` -/
binder_predicate x " > " y:term => `($x > $y)
/-- Declare `∃ x ≥ y, ...` as syntax for `∃ x, x ≥ y ∧ ...` -/
binder_predicate x "" y:term => `($x $y)
/-- Declare `∃ x < y, ...` as syntax for `∃ x, x < y ∧ ...` -/
binder_predicate x " < " y:term => `($x < $y)
/-- Declare `∃ x ≤ y, ...` as syntax for `∃ x, x ≤ y ∧ ...` -/
binder_predicate x "" y:term => `($x $y)
/-- Declare `∃ x ≠ y, ...` as syntax for `∃ x, x ≠ y ∧ ...` -/
binder_predicate x "" y:term => `($x $y)
/-- Declare `∀ x ∈ y, ...` as syntax for `∀ x, x ∈ y → ...` and `∃ x ∈ y, ...` as syntax for
`∃ x, x ∈ y ∧ ...` -/
binder_predicate x "" y:term => `($x $y)
/-- Declare `∀ x ∉ y, ...` as syntax for `∀ x, x ∉ y → ...` and `∃ x ∉ y, ...` as syntax for
`∃ x, x ∉ y ∧ ...` -/
binder_predicate x "" y:term => `($x $y)
/-- Declare `∀ x ⊆ y, ...` as syntax for `∀ x, x ⊆ y → ...` and `∃ x ⊆ y, ...` as syntax for
`∃ x, x ⊆ y ∧ ...` -/
binder_predicate x "" y:term => `($x $y)
/-- Declare `∀ x ⊂ y, ...` as syntax for `∀ x, x ⊂ y → ...` and `∃ x ⊂ y, ...` as syntax for
`∃ x, x ⊂ y ∧ ...` -/
binder_predicate x "" y:term => `($x $y)
/-- Declare `∀ x ⊇ y, ...` as syntax for `∀ x, x ⊇ y → ...` and `∃ x ⊇ y, ...` as syntax for
`∃ x, x ⊇ y ∧ ...` -/
binder_predicate x "" y:term => `($x $y)
/-- Declare `∀ x ⊃ y, ...` as syntax for `∀ x, x ⊃ y → ...` and `∃ x ⊃ y, ...` as syntax for
`∃ x, x ⊃ y ∧ ...` -/
binder_predicate x "" y:term => `($x $y)
end Lean

View File

@@ -1,62 +0,0 @@
/-
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Mario Carneiro
-/
prelude
import Init.Classical
/-! # by_cases tactic and if-then-else support -/
/--
`by_cases (h :)? p` splits the main goal into two cases, assuming `h : p` in the first branch, and `h : ¬ p` in the second branch.
-/
syntax "by_cases " (atomic(ident " : "))? term : tactic
macro_rules
| `(tactic| by_cases $e) => `(tactic| by_cases h : $e)
macro_rules
| `(tactic| by_cases $h : $e) =>
`(tactic| open Classical in refine if $h:ident : $e then ?pos else ?neg)
/-! ## if-then-else -/
@[simp] theorem if_true {_ : Decidable True} (t e : α) : ite True t e = t := if_pos trivial
@[simp] theorem if_false {_ : Decidable False} (t e : α) : ite False t e = e := if_neg id
theorem ite_id [Decidable c] {α} (t : α) : (if c then t else t) = t := by split <;> rfl
/-- A function applied to a `dite` is a `dite` of that function applied to each of the branches. -/
theorem apply_dite (f : α β) (P : Prop) [Decidable P] (x : P α) (y : ¬P α) :
f (dite P x y) = dite P (fun h => f (x h)) (fun h => f (y h)) := by
by_cases h : P <;> simp [h]
/-- A function applied to a `ite` is a `ite` of that function applied to each of the branches. -/
theorem apply_ite (f : α β) (P : Prop) [Decidable P] (x y : α) :
f (ite P x y) = ite P (f x) (f y) :=
apply_dite f P (fun _ => x) (fun _ => y)
/-- A `dite` whose results do not actually depend on the condition may be reduced to an `ite`. -/
@[simp] theorem dite_eq_ite [Decidable P] : (dite P (fun _ => a) fun _ => b) = ite P a b := rfl
@[deprecated "Use `ite_eq_right_iff`" (since := "2024-09-18")]
theorem ite_some_none_eq_none [Decidable P] :
(if P then some x else none) = none ¬ P := by
simp only [ite_eq_right_iff, reduceCtorEq]
rfl
@[deprecated "Use `Option.ite_none_right_eq_some`" (since := "2024-09-18")]
theorem ite_some_none_eq_some [Decidable P] :
(if P then some x else none) = some y P x = y := by
split <;> simp_all
@[deprecated "Use `dite_eq_right_iff" (since := "2024-09-18")]
theorem dite_some_none_eq_none [Decidable P] {x : P α} :
(if h : P then some (x h) else none) = none ¬P := by
simp
@[deprecated "Use `Option.dite_none_right_eq_some`" (since := "2024-09-18")]
theorem dite_some_none_eq_some [Decidable P] {x : P α} {y : α} :
(if h : P then some (x h) else none) = some y h : P, x h = y := by
by_cases h : P <;> simp [h]

View File

@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Mario Carneiro
-/
prelude
import Init.PropLemmas
import Init.Core
import Init.NotationExtra
universe u v
@@ -15,13 +16,6 @@ namespace Classical
noncomputable def indefiniteDescription {α : Sort u} (p : α Prop) (h : x, p x) : {x // p x} :=
choice <| let x, px := h; x, px
/--
Given that there exists an element satisfying `p`, returns one such element.
This is a straightforward consequence of, and equivalent to, `Classical.choice`.
See also `choose_spec`, which asserts that the returned value has property `p`.
-/
noncomputable def choose {α : Sort u} {p : α Prop} (h : x, p x) : α :=
(indefiniteDescription p h).val
@@ -80,8 +74,6 @@ noncomputable scoped instance (priority := low) propDecidable (a : Prop) : Decid
noncomputable def decidableInhabited (a : Prop) : Inhabited (Decidable a) where
default := inferInstance
instance (a : Prop) : Nonempty (Decidable a) := propDecidable a
noncomputable def typeDecidableEq (α : Sort u) : DecidableEq α :=
fun _ _ => inferInstance
@@ -120,84 +112,26 @@ theorem skolem {α : Sort u} {b : α → Sort v} {p : ∀ x, b x → Prop} : (
theorem propComplete (a : Prop) : a = True a = False :=
match em a with
| Or.inl ha => Or.inl (eq_true ha)
| Or.inr hn => Or.inr (eq_false hn)
| Or.inl ha => Or.inl (propext (Iff.intro (fun _ => ) (fun _ => ha)))
| Or.inr hn => Or.inr (propext (Iff.intro (fun h => hn h) (fun h => False.elim h)))
-- this supersedes byCases in Decidable
-- this supercedes byCases in Decidable
theorem byCases {p q : Prop} (hpq : p q) (hnpq : ¬p q) : q :=
Decidable.byCases (dec := propDecidable _) hpq hnpq
-- this supersedes byContradiction in Decidable
-- this supercedes byContradiction in Decidable
theorem byContradiction {p : Prop} (h : ¬p False) : p :=
Decidable.byContradiction (dec := propDecidable _) h
/-- The Double Negation Theorem: `¬¬P` is equivalent to `P`.
The left-to-right direction, double negation elimination (DNE),
is classically true but not constructively. -/
@[simp] theorem not_not : ¬¬a a := Decidable.not_not
/-- Transfer decidability of `¬ p` to decidability of `p`. -/
-- This can not be an instance as it would be tried everywhere.
def decidable_of_decidable_not (p : Prop) [h : Decidable (¬ p)] : Decidable p :=
match h with
| isFalse h => isTrue (Classical.not_not.mp h)
| isTrue h => isFalse h
attribute [local instance] decidable_of_decidable_not in
/-- Negation of the condition `P : Prop` in a `dite` is the same as swapping the branches. -/
@[simp low] protected theorem dite_not [hn : Decidable (¬p)] (x : ¬p α) (y : ¬¬p α) :
dite (¬p) x y = dite p (fun h => y (not_not_intro h)) x := by
cases hn <;> rename_i g
· simp [not_not.mp g]
· simp [g]
attribute [local instance] decidable_of_decidable_not in
/-- Negation of the condition `P : Prop` in a `ite` is the same as swapping the branches. -/
@[simp low] protected theorem ite_not (p : Prop) [Decidable (¬ p)] (x y : α) : ite (¬p) x y = ite p y x :=
dite_not (fun _ => x) (fun _ => y)
attribute [local instance] decidable_of_decidable_not in
@[simp low] protected theorem decide_not (p : Prop) [Decidable (¬ p)] : decide (¬p) = !decide p :=
byCases (fun h : p => by simp_all) (fun h => by simp_all)
@[simp low] theorem not_forall {p : α Prop} : (¬ x, p x) x, ¬p x := Decidable.not_forall
theorem not_forall_not {p : α Prop} : (¬ x, ¬p x) x, p x := Decidable.not_forall_not
theorem not_exists_not {p : α Prop} : (¬ x, ¬p x) x, p x := Decidable.not_exists_not
theorem forall_or_exists_not (P : α Prop) : ( a, P a) a, ¬ P a := by
rw [ not_forall]; exact em _
theorem exists_or_forall_not (P : α Prop) : ( a, P a) a, ¬ P a := by
rw [ not_exists]; exact em _
theorem or_iff_not_imp_left : a b (¬a b) := Decidable.or_iff_not_imp_left
theorem or_iff_not_imp_right : a b (¬b a) := Decidable.or_iff_not_imp_right
theorem not_imp_iff_and_not : ¬(a b) a ¬b := Decidable.not_imp_iff_and_not
theorem not_and_iff_or_not_not : ¬(a b) ¬a ¬b := Decidable.not_and_iff_or_not_not
theorem not_iff : ¬(a b) (¬a b) := Decidable.not_iff
@[simp] theorem imp_iff_left_iff : (b a b) a b := Decidable.imp_iff_left_iff
@[simp] theorem imp_iff_right_iff : (a b b) a b := Decidable.imp_iff_right_iff
@[simp] theorem and_or_imp : a b (a c) a b c := Decidable.and_or_imp
@[simp] theorem not_imp : ¬(a b) a ¬b := Decidable.not_imp_iff_and_not
@[simp] theorem imp_and_neg_imp_iff (p : Prop) {q : Prop} : (p q) (¬p q) q :=
Iff.intro (fun (a : _ _) => (Classical.em p).rec a.left a.right)
(fun a => And.intro (fun _ => a) (fun _ => a))
end Classical
/- Export for Mathlib compat. -/
export Classical (imp_iff_right_iff imp_and_neg_imp_iff and_or_imp not_imp)
/--
`by_cases (h :)? p` splits the main goal into two cases, assuming `h : p` in the first branch, and `h : ¬ p` in the second branch.
-/
syntax "by_cases " (atomic(ident " : "))? term : tactic
/-- Extract an element from a existential statement, using `Classical.choose`. -/
-- This enables projection notation.
@[reducible] noncomputable def Exists.choose {p : α Prop} (P : a, p a) : α := Classical.choose P
/-- Show that an element extracted from `P : ∃ a, p a` using `P.choose` satisfies `p`. -/
theorem Exists.choose_spec {p : α Prop} (P : a, p a) : p P.choose := Classical.choose_spec P
macro_rules
| `(tactic| by_cases $e) => `(tactic| by_cases h : $e)
macro_rules
| `(tactic| by_cases $h : $e) =>
`(tactic| open Classical in refine if $h:ident : $e then ?pos else ?neg)

View File

@@ -321,7 +321,7 @@ Helper definition used by the elaborator. It is not meant to be used directly by
This is used for coercions between monads, in the case where we want to apply
a monad lift and a coercion on the result type at the same time.
-/
@[coe_decl] abbrev Lean.Internal.liftCoeM {m : Type u Type v} {n : Type u Type w} {α β : Type u}
@[inline, coe_decl] def Lean.Internal.liftCoeM {m : Type u Type v} {n : Type u Type w} {α β : Type u}
[MonadLiftT m n] [ a, CoeT α a β] [Monad n] (x : m α) : n β := do
let a liftM x
pure (CoeT.coe a)
@@ -331,7 +331,7 @@ Helper definition used by the elaborator. It is not meant to be used directly by
This is used for coercing the result type under a monad.
-/
@[coe_decl] abbrev Lean.Internal.coeM {m : Type u Type v} {α β : Type u}
@[inline, coe_decl] def Lean.Internal.coeM {m : Type u Type v} {α β : Type u}
[ a, CoeT α a β] [Monad m] (x : m α) : m β := do
let a x
pure (CoeT.coe a)

View File

@@ -8,42 +8,6 @@ import Init.Core
universe u v w
/--
A `ForIn'` instance, which handles `for h : x in c do`,
can also handle `for x in x do` by ignoring `h`, and so provides a `ForIn` instance.
Note that this instance will cause a potentially non-defeq duplication if both `ForIn` and `ForIn'`
instances are provided for the same type.
-/
-- We set the priority to 500 so it is below the default,
-- but still above the low priority instance from `Stream`.
instance (priority := 500) instForInOfForIn' [ForIn' m ρ α d] : ForIn m ρ α where
forIn x b f := forIn' x b fun a _ => f a
@[simp] theorem forIn'_eq_forIn [d : Membership α ρ] [ForIn' m ρ α d] {β} [Monad m] (x : ρ) (b : β)
(f : (a : α) a x β m (ForInStep β)) (g : (a : α) β m (ForInStep β))
(h : a m b, f a m b = g a b) :
forIn' x b f = forIn x b g := by
simp [instForInOfForIn']
congr
apply funext
intro a
apply funext
intro m
apply funext
intro b
simp [h]
rfl
/-- Extract the value from a `ForInStep`, ignoring whether it is `done` or `yield`. -/
def ForInStep.value (x : ForInStep α) : α :=
match x with
| ForInStep.done b => b
| ForInStep.yield b => b
@[simp] theorem ForInStep.value_done (b : β) : (ForInStep.done b).value = b := rfl
@[simp] theorem ForInStep.value_yield (b : β) : (ForInStep.yield b).value = b := rfl
@[reducible]
def Functor.mapRev {f : Type u Type v} [Functor f] {α β : Type u} : f α (α β) f β :=
fun a f => f <$> a
@@ -56,29 +20,8 @@ def Functor.discard {f : Type u → Type v} {α : Type u} [Functor f] (x : f α)
export Functor (discard)
/--
An `Alternative` functor is an `Applicative` functor that can "fail" or be "empty"
and a binary operation `<|>` that “collects values” or finds the “left-most success”.
Important instances include
* `Option`, where `failure := none` and `<|>` returns the left-most `some`.
* Parser combinators typically provide an `Applicative` instance for error-handling and
backtracking.
Error recovery and state can interact subtly. For example, the implementation of `Alternative` for `OptionT (StateT σ Id)` keeps modifications made to the state while recovering from failure, while `StateT σ (OptionT Id)` discards them.
-/
-- NB: List instance is in mathlib. Once upstreamed, add
-- * `List`, where `failure` is the empty list and `<|>` concatenates.
class Alternative (f : Type u Type v) extends Applicative f : Type (max (u+1) v) where
/--
Produces an empty collection or recoverable failure. The `<|>` operator collects values or recovers
from failures. See `Alternative` for more details.
-/
failure : {α : Type u} f α
/--
Depending on the `Alternative` instance, collects values or recovers from `failure`s by
returning the leftmost success. Can be written using the `<|>` operator syntax.
-/
orElse : {α : Type u} f α (Unit f α) f α
instance (f : Type u Type v) (α : Type u) [Alternative f] : OrElse (f α) := Alternative.orElse
@@ -87,15 +30,9 @@ variable {f : Type u → Type v} [Alternative f] {α : Type u}
export Alternative (failure)
/--
If the proposition `p` is true, does nothing, else fails (using `failure`).
-/
@[always_inline, inline] def guard {f : Type Type v} [Alternative f] (p : Prop) [Decidable p] : f Unit :=
if p then pure () else failure
/--
Returns `some x` if `f` succeeds with value `x`, else returns `none`.
-/
@[always_inline, inline] def optional (x : f α) : f (Option α) :=
some <$> x <|> pure none

View File

@@ -131,7 +131,7 @@ protected def adapt {ε' α : Type u} (f : ε → ε') : ExceptT ε m α → Exc
end ExceptT
@[always_inline]
instance (m : Type u Type v) (ε₁ : Type u) (ε₂ : Type u) [MonadExceptOf ε₁ m] : MonadExceptOf ε₁ (ExceptT ε₂ m) where
instance (m : Type u Type v) (ε₁ : Type u) (ε₂ : Type u) [Monad m] [MonadExceptOf ε₁ m] : MonadExceptOf ε₁ (ExceptT ε₂ m) where
throw e := ExceptT.mk <| throwThe ε₁ e
tryCatch x handle := ExceptT.mk <| tryCatchThe ε₁ x handle

View File

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Control.Lawful.Basic
import Init.Control.Lawful
/-!
The Exception monad transformer using CPS style.
@@ -18,7 +18,6 @@ namespace ExceptCpsT
def run {ε α : Type u} [Monad m] (x : ExceptCpsT ε m α) : m (Except ε α) :=
x _ (fun a => pure (Except.ok a)) (fun e => pure (Except.error e))
set_option linter.unusedVariables false in -- `s` unused
@[always_inline, inline]
def runK {ε α : Type u} (x : ExceptCpsT ε m α) (s : ε) (ok : α m β) (error : ε m β) : m β :=
x _ ok error
@@ -34,7 +33,7 @@ instance : Monad (ExceptCpsT ε m) where
bind x f := fun _ k₁ k₂ => x _ (fun a => f a _ k₁ k₂) k₂
instance : LawfulMonad (ExceptCpsT σ m) := by
refine LawfulMonad.mk' _ ?_ ?_ ?_ <;> intros <;> rfl
refine' { .. } <;> intros <;> rfl
instance : MonadExceptOf ε (ExceptCpsT ε m) where
throw e := fun _ _ k => k e

View File

@@ -1,8 +1,309 @@
/-
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro
Authors: Sebastian Ullrich, Leonardo de Moura
-/
prelude
import Init.Control.Lawful.Basic
import Init.Control.Lawful.Instances
import Init.SimpLemmas
import Init.Control.Except
import Init.Control.StateRef
open Function
@[simp] theorem monadLift_self [Monad m] (x : m α) : monadLift x = x :=
rfl
class LawfulFunctor (f : Type u Type v) [Functor f] : Prop where
map_const : (Functor.mapConst : α f β f α) = Functor.map const β
id_map (x : f α) : id <$> x = x
comp_map (g : α β) (h : β γ) (x : f α) : (h g) <$> x = h <$> g <$> x
export LawfulFunctor (map_const id_map comp_map)
attribute [simp] id_map
@[simp] theorem id_map' [Functor m] [LawfulFunctor m] (x : m α) : (fun a => a) <$> x = x :=
id_map x
class LawfulApplicative (f : Type u Type v) [Applicative f] extends LawfulFunctor f : Prop where
seqLeft_eq (x : f α) (y : f β) : x <* y = const β <$> x <*> y
seqRight_eq (x : f α) (y : f β) : x *> y = const α id <$> x <*> y
pure_seq (g : α β) (x : f α) : pure g <*> x = g <$> x
map_pure (g : α β) (x : α) : g <$> (pure x : f α) = pure (g x)
seq_pure {α β : Type u} (g : f (α β)) (x : α) : g <*> pure x = (fun h => h x) <$> g
seq_assoc {α β γ : Type u} (x : f α) (g : f (α β)) (h : f (β γ)) : h <*> (g <*> x) = ((@comp α β γ) <$> h) <*> g <*> x
comp_map g h x := (by
repeat rw [ pure_seq]
simp [seq_assoc, map_pure, seq_pure])
export LawfulApplicative (seqLeft_eq seqRight_eq pure_seq map_pure seq_pure seq_assoc)
attribute [simp] map_pure seq_pure
@[simp] theorem pure_id_seq [Applicative f] [LawfulApplicative f] (x : f α) : pure id <*> x = x := by
simp [pure_seq]
class LawfulMonad (m : Type u Type v) [Monad m] extends LawfulApplicative m : Prop where
bind_pure_comp (f : α β) (x : m α) : x >>= (fun a => pure (f a)) = f <$> x
bind_map {α β : Type u} (f : m (α β)) (x : m α) : f >>= (. <$> x) = f <*> x
pure_bind (x : α) (f : α m β) : pure x >>= f = f x
bind_assoc (x : m α) (f : α m β) (g : β m γ) : x >>= f >>= g = x >>= fun x => f x >>= g
map_pure g x := (by rw [ bind_pure_comp, pure_bind])
seq_pure g x := (by rw [ bind_map]; simp [map_pure, bind_pure_comp])
seq_assoc x g h := (by simp [ bind_pure_comp, bind_map, bind_assoc, pure_bind])
export LawfulMonad (bind_pure_comp bind_map pure_bind bind_assoc)
attribute [simp] pure_bind bind_assoc
@[simp] theorem bind_pure [Monad m] [LawfulMonad m] (x : m α) : x >>= pure = x := by
show x >>= (fun a => pure (id a)) = x
rw [bind_pure_comp, id_map]
theorem map_eq_pure_bind [Monad m] [LawfulMonad m] (f : α β) (x : m α) : f <$> x = x >>= fun a => pure (f a) := by
rw [ bind_pure_comp]
theorem seq_eq_bind_map {α β : Type u} [Monad m] [LawfulMonad m] (f : m (α β)) (x : m α) : f <*> x = f >>= (. <$> x) := by
rw [ bind_map]
theorem bind_congr [Bind m] {x : m α} {f g : α m β} (h : a, f a = g a) : x >>= f = x >>= g := by
simp [funext h]
@[simp] theorem bind_pure_unit [Monad m] [LawfulMonad m] {x : m PUnit} : (x >>= fun _ => pure ) = x := by
rw [bind_pure]
theorem map_congr [Functor m] {x : m α} {f g : α β} (h : a, f a = g a) : (f <$> x : m β) = g <$> x := by
simp [funext h]
theorem seq_eq_bind {α β : Type u} [Monad m] [LawfulMonad m] (mf : m (α β)) (x : m α) : mf <*> x = mf >>= fun f => f <$> x := by
rw [bind_map]
theorem seqRight_eq_bind [Monad m] [LawfulMonad m] (x : m α) (y : m β) : x *> y = x >>= fun _ => y := by
rw [seqRight_eq]
simp [map_eq_pure_bind, seq_eq_bind_map, const]
theorem seqLeft_eq_bind [Monad m] [LawfulMonad m] (x : m α) (y : m β) : x <* y = x >>= fun a => y >>= fun _ => pure a := by
rw [seqLeft_eq]; simp [map_eq_pure_bind, seq_eq_bind_map]
/-! # Id -/
namespace Id
@[simp] theorem map_eq (x : Id α) (f : α β) : f <$> x = f x := rfl
@[simp] theorem bind_eq (x : Id α) (f : α id β) : x >>= f = f x := rfl
@[simp] theorem pure_eq (a : α) : (pure a : Id α) = a := rfl
instance : LawfulMonad Id := by
refine' { .. } <;> intros <;> rfl
end Id
/-! # ExceptT -/
namespace ExceptT
theorem ext [Monad m] {x y : ExceptT ε m α} (h : x.run = y.run) : x = y := by
simp [run] at h
assumption
@[simp] theorem run_pure [Monad m] (x : α) : run (pure x : ExceptT ε m α) = pure (Except.ok x) := rfl
@[simp] theorem run_lift [Monad.{u, v} m] (x : m α) : run (ExceptT.lift x : ExceptT ε m α) = (Except.ok <$> x : m (Except ε α)) := rfl
@[simp] theorem run_throw [Monad m] : run (throw e : ExceptT ε m β) = pure (Except.error e) := rfl
@[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, map_eq_pure_bind]
@[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]
theorem run_bind [Monad m] (x : ExceptT ε m α)
: run (x >>= f : ExceptT ε m β)
=
run x >>= fun
| Except.ok x => run (f x)
| Except.error e => pure (Except.error e) :=
rfl
@[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] 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, map_eq_pure_bind]
apply bind_congr
intro a; cases a <;> simp [Except.map]
protected theorem seq_eq {α β ε : Type u} [Monad m] (mf : ExceptT ε m (α β)) (x : ExceptT ε m α) : mf <*> x = mf >>= fun f => f <$> x :=
rfl
protected theorem bind_pure_comp [Monad m] [LawfulMonad m] (f : α β) (x : ExceptT ε m α) : x >>= pure f = f <$> x := by
intros; rfl
protected theorem seqLeft_eq {α β ε : Type u} {m : Type u Type v} [Monad m] [LawfulMonad m] (x : ExceptT ε m α) (y : ExceptT ε m β) : x <* y = const β <$> x <*> y := by
show (x >>= fun a => y >>= fun _ => pure a) = (const (α := α) β <$> x) >>= fun f => f <$> y
rw [ ExceptT.bind_pure_comp]
apply ext
simp [run_bind]
apply bind_congr
intro
| Except.error _ => simp
| Except.ok _ =>
simp [map_eq_pure_bind]; apply bind_congr; intro b;
cases b <;> simp [comp, Except.map, const]
protected theorem seqRight_eq [Monad m] [LawfulMonad m] (x : ExceptT ε m α) (y : ExceptT ε m β) : x *> y = const α id <$> x <*> y := by
show (x >>= fun _ => y) = (const α id <$> x) >>= fun f => f <$> y
rw [ ExceptT.bind_pure_comp]
apply ext
simp [run_bind]
apply bind_congr
intro a; cases a <;> simp
instance [Monad m] [LawfulMonad m] : LawfulMonad (ExceptT ε m) where
id_map := by intros; apply ext; simp
map_const := by intros; rfl
seqLeft_eq := ExceptT.seqLeft_eq
seqRight_eq := ExceptT.seqRight_eq
pure_seq := by intros; apply ext; simp [ExceptT.seq_eq, run_bind]
bind_pure_comp := ExceptT.bind_pure_comp
bind_map := by intros; rfl
pure_bind := by intros; apply ext; simp [run_bind]
bind_assoc := by intros; apply ext; simp [run_bind]; apply bind_congr; intro a; cases a <;> simp
end ExceptT
/-! # ReaderT -/
namespace ReaderT
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] theorem run_pure [Monad m] (a : α) (ctx : ρ) : (pure a : ReaderT ρ m α).run ctx = pure a := rfl
@[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] theorem run_mapConst [Monad m] (a : α) (x : ReaderT ρ m β) (ctx : ρ)
: (Functor.mapConst a x).run ctx = Functor.mapConst a (x.run ctx) := rfl
@[simp] theorem run_map [Monad m] (f : α β) (x : ReaderT ρ m α) (ctx : ρ)
: (f <$> x).run ctx = f <$> x.run ctx := rfl
@[simp] theorem run_monadLift [MonadLiftT n m] (x : n α) (ctx : ρ)
: (monadLift x : ReaderT ρ m α).run ctx = (monadLift x : m α) := rfl
@[simp] theorem run_monadMap [MonadFunctor 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] 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
@[simp] theorem run_seqRight [Monad m] (x : ReaderT ρ m α) (y : ReaderT ρ m β) (ctx : ρ)
: (x *> y).run ctx = (x.run ctx *> y.run ctx) := rfl
@[simp] theorem run_seqLeft [Monad m] (x : ReaderT ρ m α) (y : ReaderT ρ m β) (ctx : ρ)
: (x <* y).run ctx = (x.run ctx <* y.run ctx) := rfl
instance [Monad m] [LawfulFunctor m] : LawfulFunctor (ReaderT ρ m) where
id_map := by intros; apply ext; simp
map_const := by intros; funext a b; apply ext; intros; simp [map_const]
comp_map := by intros; apply ext; intros; simp [comp_map]
instance [Monad m] [LawfulApplicative m] : LawfulApplicative (ReaderT ρ m) where
seqLeft_eq := by intros; apply ext; intros; simp [seqLeft_eq]
seqRight_eq := by intros; apply ext; intros; simp [seqRight_eq]
pure_seq := by intros; apply ext; intros; simp [pure_seq]
map_pure := by intros; apply ext; intros; simp [map_pure]
seq_pure := by intros; apply ext; intros; simp [seq_pure]
seq_assoc := by intros; apply ext; intros; simp [seq_assoc]
instance [Monad m] [LawfulMonad m] : LawfulMonad (ReaderT ρ m) where
bind_pure_comp := by intros; apply ext; intros; simp [LawfulMonad.bind_pure_comp]
bind_map := by intros; apply ext; intros; simp [bind_map]
pure_bind := by intros; apply ext; intros; simp
bind_assoc := by intros; apply ext; intros; simp
end ReaderT
/-! # StateRefT -/
instance [Monad m] [LawfulMonad m] : LawfulMonad (StateRefT' ω σ m) :=
inferInstanceAs (LawfulMonad (ReaderT (ST.Ref ω σ) m))
/-! # StateT -/
namespace StateT
theorem ext {x y : StateT σ m α} (h : s, x.run s = y.run s) : x = y :=
funext h
@[simp] theorem run'_eq [Monad m] (x : StateT σ m α) (s : σ) : run' x s = (·.1) <$> run x s :=
rfl
@[simp] theorem run_pure [Monad m] (a : α) (s : σ) : (pure a : StateT σ m α).run s = pure (a, s) := rfl
@[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] 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, map_eq_pure_bind]
@[simp] theorem run_get [Monad m] (s : σ) : (get : StateT σ m σ).run s = pure (s, s) := rfl
@[simp] theorem run_set [Monad m] (s s' : σ) : (set s' : StateT σ m PUnit).run s = pure (, s') := rfl
@[simp] theorem run_modify [Monad m] (f : σ σ) (s : σ) : (modify f : StateT σ m PUnit).run s = pure (, f s) := rfl
@[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] 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_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] 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_monadMap [Monad m] [MonadFunctor 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
show (f >>= fun g => g <$> x).run s = _
simp
@[simp] theorem run_seqRight [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) (s : σ) : (x *> y).run s = (x.run s >>= fun p => y.run p.2) := by
show (x >>= fun _ => y).run s = _
simp
@[simp] theorem run_seqLeft {α β σ : Type u} [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) (s : σ) : (x <* y).run s = (x.run s >>= fun p => y.run p.2 >>= fun p' => pure (p.1, p'.2)) := by
show (x >>= fun a => y >>= fun _ => pure a).run s = _
simp
theorem seqRight_eq [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) : x *> y = const α id <$> x <*> y := by
apply ext; intro s
simp [map_eq_pure_bind, const]
apply bind_congr; intro p; cases p
simp [Prod.eta]
theorem seqLeft_eq [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) : x <* y = const β <$> x <*> y := by
apply ext; intro s
simp [map_eq_pure_bind]
instance [Monad m] [LawfulMonad m] : LawfulMonad (StateT σ m) where
id_map := by intros; apply ext; intros; simp[Prod.eta]
map_const := by intros; rfl
seqLeft_eq := seqLeft_eq
seqRight_eq := seqRight_eq
pure_seq := by intros; apply ext; intros; simp
bind_pure_comp := by intros; apply ext; intros; simp; apply LawfulMonad.bind_pure_comp
bind_map := by intros; rfl
pure_bind := by intros; apply ext; intros; simp
bind_assoc := by intros; apply ext; intros; simp
end StateT

View File

@@ -1,191 +0,0 @@
/-
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro
-/
prelude
import Init.SimpLemmas
import Init.Meta
open Function
@[simp] theorem monadLift_self {m : Type u Type v} (x : m α) : monadLift x = x :=
rfl
/--
The `Functor` typeclass only contains the operations of a functor.
`LawfulFunctor` further asserts that these operations satisfy the laws of a functor,
including the preservation of the identity and composition laws:
```
id <$> x = x
(h ∘ g) <$> x = h <$> g <$> x
```
-/
class LawfulFunctor (f : Type u Type v) [Functor f] : Prop where
map_const : (Functor.mapConst : α f β f α) = Functor.map const β
id_map (x : f α) : id <$> x = x
comp_map (g : α β) (h : β γ) (x : f α) : (h g) <$> x = h <$> g <$> x
export LawfulFunctor (map_const id_map comp_map)
attribute [simp] id_map
@[simp] theorem id_map' [Functor m] [LawfulFunctor m] (x : m α) : (fun a => a) <$> x = x :=
id_map x
@[simp] theorem Functor.map_map [Functor f] [LawfulFunctor f] (m : α β) (g : β γ) (x : f α) :
g <$> m <$> x = (fun a => g (m a)) <$> x :=
(comp_map _ _ _).symm
/--
The `Applicative` typeclass only contains the operations of an applicative functor.
`LawfulApplicative` further asserts that these operations satisfy the laws of an applicative functor:
```
pure id <*> v = v
pure (·∘·) <*> u <*> v <*> w = u <*> (v <*> w)
pure f <*> pure x = pure (f x)
u <*> pure y = pure (· y) <*> u
```
-/
class LawfulApplicative (f : Type u Type v) [Applicative f] extends LawfulFunctor f : Prop where
seqLeft_eq (x : f α) (y : f β) : x <* y = const β <$> x <*> y
seqRight_eq (x : f α) (y : f β) : x *> y = const α id <$> x <*> y
pure_seq (g : α β) (x : f α) : pure g <*> x = g <$> x
map_pure (g : α β) (x : α) : g <$> (pure x : f α) = pure (g x)
seq_pure {α β : Type u} (g : f (α β)) (x : α) : g <*> pure x = (fun h => h x) <$> g
seq_assoc {α β γ : Type u} (x : f α) (g : f (α β)) (h : f (β γ)) : h <*> (g <*> x) = ((@comp α β γ) <$> h) <*> g <*> x
comp_map g h x := (by
repeat rw [ pure_seq]
simp [seq_assoc, map_pure, seq_pure])
export LawfulApplicative (seqLeft_eq seqRight_eq pure_seq map_pure seq_pure seq_assoc)
attribute [simp] map_pure seq_pure
@[simp] theorem pure_id_seq [Applicative f] [LawfulApplicative f] (x : f α) : pure id <*> x = x := by
simp [pure_seq]
/--
The `Monad` typeclass only contains the operations of a monad.
`LawfulMonad` further asserts that these operations satisfy the laws of a monad,
including associativity and identity laws for `bind`:
```
pure x >>= f = f x
x >>= pure = x
x >>= f >>= g = x >>= (fun x => f x >>= g)
```
`LawfulMonad.mk'` is an alternative constructor containing useful defaults for many fields.
-/
class LawfulMonad (m : Type u Type v) [Monad m] extends LawfulApplicative m : Prop where
bind_pure_comp (f : α β) (x : m α) : x >>= (fun a => pure (f a)) = f <$> x
bind_map {α β : Type u} (f : m (α β)) (x : m α) : f >>= (. <$> x) = f <*> x
pure_bind (x : α) (f : α m β) : pure x >>= f = f x
bind_assoc (x : m α) (f : α m β) (g : β m γ) : x >>= f >>= g = x >>= fun x => f x >>= g
map_pure g x := (by rw [ bind_pure_comp, pure_bind])
seq_pure g x := (by rw [ bind_map]; simp [map_pure, bind_pure_comp])
seq_assoc x g h := (by simp [ bind_pure_comp, bind_map, bind_assoc, pure_bind])
export LawfulMonad (bind_pure_comp bind_map pure_bind bind_assoc)
attribute [simp] pure_bind bind_assoc bind_pure_comp
@[simp] theorem bind_pure [Monad m] [LawfulMonad m] (x : m α) : x >>= pure = x := by
show x >>= (fun a => pure (id a)) = x
rw [bind_pure_comp, id_map]
/--
Use `simp [← bind_pure_comp]` rather than `simp [map_eq_pure_bind]`,
as `bind_pure_comp` is in the default simp set, so also using `map_eq_pure_bind` would cause a loop.
-/
theorem map_eq_pure_bind [Monad m] [LawfulMonad m] (f : α β) (x : m α) : f <$> x = x >>= fun a => pure (f a) := by
rw [ bind_pure_comp]
theorem seq_eq_bind_map {α β : Type u} [Monad m] [LawfulMonad m] (f : m (α β)) (x : m α) : f <*> x = f >>= (. <$> x) := by
rw [ bind_map]
theorem bind_congr [Bind m] {x : m α} {f g : α m β} (h : a, f a = g a) : x >>= f = x >>= g := by
simp [funext h]
@[simp] theorem bind_pure_unit [Monad m] [LawfulMonad m] {x : m PUnit} : (x >>= fun _ => pure ) = x := by
rw [bind_pure]
theorem map_congr [Functor m] {x : m α} {f g : α β} (h : a, f a = g a) : (f <$> x : m β) = g <$> x := by
simp [funext h]
theorem seq_eq_bind {α β : Type u} [Monad m] [LawfulMonad m] (mf : m (α β)) (x : m α) : mf <*> x = mf >>= fun f => f <$> x := by
rw [bind_map]
theorem seqRight_eq_bind [Monad m] [LawfulMonad m] (x : m α) (y : m β) : x *> y = x >>= fun _ => y := by
rw [seqRight_eq]
simp only [map_eq_pure_bind, const, seq_eq_bind_map, bind_assoc, pure_bind, id_eq, bind_pure]
theorem seqLeft_eq_bind [Monad m] [LawfulMonad m] (x : m α) (y : m β) : x <* y = x >>= fun a => y >>= fun _ => pure a := by
rw [seqLeft_eq]
simp only [map_eq_pure_bind, seq_eq_bind_map, bind_assoc, pure_bind, const_apply]
@[simp] theorem map_bind [Monad m] [LawfulMonad m] (f : β γ) (x : m α) (g : α m β) :
f <$> (x >>= g) = x >>= fun a => f <$> g a := by
rw [ bind_pure_comp, LawfulMonad.bind_assoc]
simp [bind_pure_comp]
@[simp] theorem bind_map_left [Monad m] [LawfulMonad m] (f : α β) (x : m α) (g : β m γ) :
((f <$> x) >>= fun b => g b) = (x >>= fun a => g (f a)) := by
rw [ bind_pure_comp]
simp only [bind_assoc, pure_bind]
@[simp] theorem Functor.map_unit [Monad m] [LawfulMonad m] {a : m PUnit} : (fun _ => PUnit.unit) <$> a = a := by
simp [map]
/--
An alternative constructor for `LawfulMonad` which has more
defaultable fields in the common case.
-/
theorem LawfulMonad.mk' (m : Type u Type v) [Monad m]
(id_map : {α} (x : m α), id <$> x = x)
(pure_bind : {α β} (x : α) (f : α m β), pure x >>= f = f x)
(bind_assoc : {α β γ} (x : m α) (f : α m β) (g : β m γ),
x >>= f >>= g = x >>= fun x => f x >>= g)
(map_const : {α β} (x : α) (y : m β),
Functor.mapConst x y = Function.const β x <$> y := by intros; rfl)
(seqLeft_eq : {α β} (x : m α) (y : m β),
x <* y = (x >>= fun a => y >>= fun _ => pure a) := by intros; rfl)
(seqRight_eq : {α β} (x : m α) (y : m β), x *> y = (x >>= fun _ => y) := by intros; rfl)
(bind_pure_comp : {α β} (f : α β) (x : m α),
x >>= (fun y => pure (f y)) = f <$> x := by intros; rfl)
(bind_map : {α β} (f : m (α β)) (x : m α), f >>= (. <$> x) = f <*> x := by intros; rfl)
: LawfulMonad m :=
have map_pure {α β} (g : α β) (x : α) : g <$> (pure x : m α) = pure (g x) := by
rw [ bind_pure_comp]; simp [pure_bind]
{ id_map, bind_pure_comp, bind_map, pure_bind, bind_assoc, map_pure,
comp_map := by simp [ bind_pure_comp, bind_assoc, pure_bind]
pure_seq := by intros; rw [ bind_map]; simp [pure_bind]
seq_pure := by intros; rw [ bind_map]; simp [map_pure, bind_pure_comp]
seq_assoc := by simp [ bind_pure_comp, bind_map, bind_assoc, pure_bind]
map_const := funext fun x => funext (map_const x)
seqLeft_eq := by simp [seqLeft_eq, bind_map, bind_pure_comp, pure_bind, bind_assoc]
seqRight_eq := fun x y => by
rw [seqRight_eq, bind_map, bind_pure_comp, bind_assoc]; simp [pure_bind, id_map] }
/-! # Id -/
namespace Id
@[simp] theorem map_eq (x : Id α) (f : α β) : f <$> x = f x := rfl
@[simp] theorem bind_eq (x : Id α) (f : α id β) : x >>= f = f x := rfl
@[simp] theorem pure_eq (a : α) : (pure a : Id α) = a := rfl
instance : LawfulMonad Id := by
refine LawfulMonad.mk' _ ?_ ?_ ?_ <;> intros <;> rfl
end Id
/-! # Option -/
instance : LawfulMonad Option := LawfulMonad.mk'
(id_map := fun x => by cases x <;> rfl)
(pure_bind := fun _ _ => rfl)
(bind_assoc := fun x _ _ => by cases x <;> rfl)
(bind_pure_comp := fun _ x => by cases x <;> rfl)
instance : LawfulApplicative Option := inferInstance
instance : LawfulFunctor Option := inferInstance

View File

@@ -1,254 +0,0 @@
/-
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro
-/
prelude
import Init.Control.Lawful.Basic
import Init.Control.Except
import Init.Control.StateRef
import Init.Ext
open Function
/-! # ExceptT -/
namespace ExceptT
@[ext] theorem ext {x y : ExceptT ε m α} (h : x.run = y.run) : x = y := by
simp [run] at h
assumption
@[simp] theorem run_pure [Monad m] (x : α) : run (pure x : ExceptT ε m α) = pure (Except.ok x) := rfl
@[simp] theorem run_lift [Monad.{u, v} m] (x : m α) : run (ExceptT.lift x : ExceptT ε m α) = (Except.ok <$> x : m (Except ε α)) := rfl
@[simp] theorem run_throw [Monad m] : run (throw e : ExceptT ε m β) = pure (Except.error e) := rfl
@[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] 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]
theorem run_bind [Monad m] (x : ExceptT ε m α)
: run (x >>= f : ExceptT ε m β)
=
run x >>= fun
| Except.ok x => run (f x)
| Except.error e => pure (Except.error e) :=
rfl
@[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] 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
intro a; cases a <;> simp [Except.map]
protected theorem seq_eq {α β ε : Type u} [Monad m] (mf : ExceptT ε m (α β)) (x : ExceptT ε m α) : mf <*> x = mf >>= fun f => f <$> x :=
rfl
protected theorem bind_pure_comp [Monad m] (f : α β) (x : ExceptT ε m α) : x >>= pure f = f <$> x := by
intros; rfl
protected theorem seqLeft_eq {α β ε : Type u} {m : Type u Type v} [Monad m] [LawfulMonad m] (x : ExceptT ε m α) (y : ExceptT ε m β) : x <* y = const β <$> x <*> y := by
show (x >>= fun a => y >>= fun _ => pure a) = (const (α := α) β <$> x) >>= fun f => f <$> y
rw [ ExceptT.bind_pure_comp]
apply ext
simp [run_bind]
apply bind_congr
intro
| Except.error _ => simp
| Except.ok _ =>
simp [bind_pure_comp]; apply bind_congr; intro b;
cases b <;> simp [comp, Except.map, const]
protected theorem seqRight_eq [Monad m] [LawfulMonad m] (x : ExceptT ε m α) (y : ExceptT ε m β) : x *> y = const α id <$> x <*> y := by
show (x >>= fun _ => y) = (const α id <$> x) >>= fun f => f <$> y
rw [ ExceptT.bind_pure_comp]
apply ext
simp [run_bind]
apply bind_congr
intro a; cases a <;> simp
instance [Monad m] [LawfulMonad m] : LawfulMonad (ExceptT ε m) where
id_map := by intros; apply ext; simp
map_const := by intros; rfl
seqLeft_eq := ExceptT.seqLeft_eq
seqRight_eq := ExceptT.seqRight_eq
pure_seq := by intros; apply ext; simp [ExceptT.seq_eq, run_bind]
bind_pure_comp := ExceptT.bind_pure_comp
bind_map := by intros; rfl
pure_bind := by intros; apply ext; simp [run_bind]
bind_assoc := by intros; apply ext; simp [run_bind]; apply bind_congr; intro a; cases a <;> simp
@[simp] theorem map_throw [Monad m] [LawfulMonad m] {α β : Type _} (f : α β) (e : ε) :
f <$> (throw e : ExceptT ε m α) = (throw e : ExceptT ε m β) := by
simp only [ExceptT.instMonad, ExceptT.map, ExceptT.mk, throw, throwThe, MonadExceptOf.throw,
pure_bind]
end ExceptT
/-! # Except -/
instance : LawfulMonad (Except ε) := LawfulMonad.mk'
(id_map := fun x => by cases x <;> rfl)
(pure_bind := fun _ _ => rfl)
(bind_assoc := fun a _ _ => by cases a <;> rfl)
instance : LawfulApplicative (Except ε) := inferInstance
instance : LawfulFunctor (Except ε) := inferInstance
/-! # ReaderT -/
namespace ReaderT
@[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] theorem run_pure [Monad m] (a : α) (ctx : ρ) : (pure a : ReaderT ρ m α).run ctx = pure a := rfl
@[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] theorem run_mapConst [Monad m] (a : α) (x : ReaderT ρ m β) (ctx : ρ)
: (Functor.mapConst a x).run ctx = Functor.mapConst a (x.run ctx) := rfl
@[simp] theorem run_map [Monad m] (f : α β) (x : ReaderT ρ m α) (ctx : ρ)
: (f <$> x).run ctx = f <$> x.run ctx := rfl
@[simp] theorem run_monadLift [MonadLiftT n m] (x : n α) (ctx : ρ)
: (monadLift x : ReaderT ρ m α).run ctx = (monadLift x : m α) := rfl
@[simp] theorem run_monadMap [MonadFunctor 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] 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
@[simp] theorem run_seqRight [Monad m] (x : ReaderT ρ m α) (y : ReaderT ρ m β) (ctx : ρ)
: (x *> y).run ctx = (x.run ctx *> y.run ctx) := rfl
@[simp] theorem run_seqLeft [Monad m] (x : ReaderT ρ m α) (y : ReaderT ρ m β) (ctx : ρ)
: (x <* y).run ctx = (x.run ctx <* y.run ctx) := rfl
instance [Monad m] [LawfulFunctor m] : LawfulFunctor (ReaderT ρ m) where
id_map := by intros; apply ext; simp
map_const := by intros; funext a b; apply ext; intros; simp [map_const]
comp_map := by intros; apply ext; intros; simp [comp_map]
instance [Monad m] [LawfulApplicative m] : LawfulApplicative (ReaderT ρ m) where
seqLeft_eq := by intros; apply ext; intros; simp [seqLeft_eq]
seqRight_eq := by intros; apply ext; intros; simp [seqRight_eq]
pure_seq := by intros; apply ext; intros; simp [pure_seq]
map_pure := by intros; apply ext; intros; simp [map_pure]
seq_pure := by intros; apply ext; intros; simp [seq_pure]
seq_assoc := by intros; apply ext; intros; simp [seq_assoc]
instance [Monad m] [LawfulMonad m] : LawfulMonad (ReaderT ρ m) where
bind_pure_comp := by intros; apply ext; intros; simp [LawfulMonad.bind_pure_comp]
bind_map := by intros; apply ext; intros; simp [bind_map]
pure_bind := by intros; apply ext; intros; simp
bind_assoc := by intros; apply ext; intros; simp
end ReaderT
/-! # StateRefT -/
instance [Monad m] [LawfulMonad m] : LawfulMonad (StateRefT' ω σ m) :=
inferInstanceAs (LawfulMonad (ReaderT (ST.Ref ω σ) m))
/-! # StateT -/
namespace StateT
@[ext] theorem ext {x y : StateT σ m α} (h : s, x.run s = y.run s) : x = y :=
funext h
@[simp] theorem run'_eq [Monad m] (x : StateT σ m α) (s : σ) : run' x s = (·.1) <$> run x s :=
rfl
@[simp] theorem run_pure [Monad m] (a : α) (s : σ) : (pure a : StateT σ m α).run s = pure (a, s) := rfl
@[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] 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] theorem run_get [Monad m] (s : σ) : (get : StateT σ m σ).run s = pure (s, s) := rfl
@[simp] theorem run_set [Monad m] (s s' : σ) : (set s' : StateT σ m PUnit).run s = pure (, s') := rfl
@[simp] theorem run_modify [Monad m] (f : σ σ) (s : σ) : (modify f : StateT σ m PUnit).run s = pure (, f s) := rfl
@[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] theorem run_lift {α σ : Type u} [Monad m] (x : m α) (s : σ) : (StateT.lift x : StateT σ m α).run s = x >>= fun a => pure (a, s) := rfl
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] 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_monadMap [MonadFunctor 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
show (f >>= fun g => g <$> x).run s = _
simp
@[simp] theorem run_seqRight [Monad m] (x : StateT σ m α) (y : StateT σ m β) (s : σ) : (x *> y).run s = (x.run s >>= fun p => y.run p.2) := by
show (x >>= fun _ => y).run s = _
simp
@[simp] theorem run_seqLeft {α β σ : Type u} [Monad m] (x : StateT σ m α) (y : StateT σ m β) (s : σ) : (x <* y).run s = (x.run s >>= fun p => y.run p.2 >>= fun p' => pure (p.1, p'.2)) := by
show (x >>= fun a => y >>= fun _ => pure a).run s = _
simp
theorem seqRight_eq [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) : x *> y = const α id <$> x <*> y := by
apply ext; intro s
simp [bind_pure_comp, const]
apply bind_congr; intro p; cases p
simp [Prod.eta]
theorem seqLeft_eq [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) : x <* y = const β <$> x <*> y := by
apply ext; intro s
simp [bind_pure_comp]
instance [Monad m] [LawfulMonad m] : LawfulMonad (StateT σ m) where
id_map := by intros; apply ext; intros; simp[Prod.eta]
map_const := by intros; rfl
seqLeft_eq := seqLeft_eq
seqRight_eq := seqRight_eq
pure_seq := by intros; apply ext; intros; simp
bind_pure_comp := by intros; apply ext; intros; simp
bind_map := by intros; rfl
pure_bind := by intros; apply ext; intros; simp
bind_assoc := by intros; apply ext; intros; simp
end StateT
/-! # EStateM -/
instance : LawfulMonad (EStateM ε σ) := .mk'
(id_map := fun x => funext <| fun s => by
dsimp only [EStateM.instMonad, EStateM.map]
match x s with
| .ok _ _ => rfl
| .error _ _ => rfl)
(pure_bind := fun _ _ => rfl)
(bind_assoc := fun x _ _ => funext <| fun s => by
dsimp only [EStateM.instMonad, EStateM.bind]
match x s with
| .ok _ _ => rfl
| .error _ _ => rfl)
(map_const := fun _ _ => rfl)

View File

@@ -10,7 +10,7 @@ import Init.Control.Except
universe u v
instance : ToBool (Option α) := Option.isSome
instance : ToBool (Option α) := Option.toBool
def OptionT (m : Type u Type v) (α : Type u) : Type v :=
m (Option α)
@@ -67,7 +67,7 @@ instance : MonadExceptOf Unit (OptionT m) where
throw := fun _ => OptionT.fail
tryCatch := OptionT.tryCatch
instance (ε : Type u) [MonadExceptOf ε m] : MonadExceptOf ε (OptionT m) where
instance (ε : Type u) [Monad m] [MonadExceptOf ε m] : MonadExceptOf ε (OptionT m) where
throw e := OptionT.mk <| throwThe ε e
tryCatch x handle := OptionT.mk <| tryCatchThe ε x handle

View File

@@ -32,7 +32,7 @@ instance : MonadControl m (ReaderT ρ m) where
restoreM x _ := x
@[always_inline]
instance ReaderT.tryFinally [MonadFinally m] : MonadFinally (ReaderT ρ m) where
instance ReaderT.tryFinally [MonadFinally m] [Monad m] : MonadFinally (ReaderT ρ m) where
tryFinally' x h ctx := tryFinally' (x ctx) (fun a? => h a? ctx)
@[reducible] def ReaderM (ρ : Type u) := ReaderT ρ Id

View File

@@ -87,7 +87,7 @@ protected def lift {α : Type u} (t : m α) : StateT σ m α :=
instance : MonadLift m (StateT σ m) := StateT.lift
@[always_inline]
instance (σ m) : MonadFunctor m (StateT σ m) := fun f x s => f (x s)
instance (σ m) [Monad m] : MonadFunctor m (StateT σ m) := fun f x s => f (x s)
@[always_inline]
instance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (StateT σ m) := {

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