Skip to content

Commit 8c01b1b

Browse files
authored
Merge branch 'master' into wojciech/simpVarHead2
2 parents 224dc03 + 0d7e76e commit 8c01b1b

1,307 files changed

Lines changed: 2934768 additions & 2861193 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

.claude/CLAUDE.md

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -66,6 +66,8 @@ To rebuild individual stage 2 modules without a full `make stage2`, use Lake dir
6666
cd build/release/stage2 && lake build Init.Prelude
6767
```
6868

69+
To run tests in stage2, replace `-C build/release` from above with `-C build/release/stage2`.
70+
6971
## New features
7072

7173
When asked to implement new features:

.github/workflows/build-template.yml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -131,7 +131,7 @@ jobs:
131131
[ -d build ] || mkdir build
132132
cd build
133133
# arguments passed to `cmake`
134-
OPTIONS=(-DLEAN_EXTRA_MAKE_OPTS=-DwarningAsError=true)
134+
OPTIONS=(-DWFAIL=ON)
135135
if [[ -n '${{ matrix.release }}' ]]; then
136136
# this also enables githash embedding into stage 1 library, which prohibits reusing
137137
# `.olean`s across commits, so we don't do it in the fast non-release CI

.github/workflows/ci.yml

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -305,7 +305,8 @@ jobs:
305305
"test": true,
306306
"CMAKE_PRESET": "reldebug",
307307
// * `elab_bench/big_do` crashes with exit code 134
308-
"CTEST_OPTIONS": "-E 'elab_bench/big_do'",
308+
// * `compile_bench/channel` randomly segfaults
309+
"CTEST_OPTIONS": "-E 'elab_bench/big_do|compile_bench/channel'",
309310
},
310311
{
311312
"name": "Linux fsanitize",

.github/workflows/update-stage0.yml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -77,7 +77,7 @@ jobs:
7777
# sync options with `Linux Lake` to ensure cache reuse
7878
run: |
7979
mkdir -p build
80-
cmake --preset release -B build -DLEAN_EXTRA_MAKE_OPTS=-DwarningAsError=true
80+
cmake --preset release -B build -DWFAIL=ON
8181
shell: 'nix develop -c bash -euxo pipefail {0}'
8282
- if: env.should_update_stage0 == 'yes'
8383
run: |

.gitignore

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,3 +34,4 @@ wdErr.txt
3434
wdIn.txt
3535
wdOut.txt
3636
downstream_releases/
37+
.claude/worktrees/

.vscode/tasks.json

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,15 @@
1111
"isDefault": true
1212
}
1313
},
14+
{
15+
"label": "build stage2",
16+
"type": "shell",
17+
"command": "make -C build/release stage2 -j$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4)",
18+
"problemMatcher": [],
19+
"group": {
20+
"kind": "build"
21+
}
22+
},
1423
{
1524
"label": "build-old",
1625
"type": "shell",

CMakeLists.txt

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -127,7 +127,8 @@ if(USE_MIMALLOC)
127127
# Unnecessarily deep directory structure, but it saves us from a complicated
128128
# stage0 update for now. If we ever update the other dependencies like
129129
# cadical, it might be worth reorganizing the directory structure.
130-
SOURCE_DIR "${CMAKE_BINARY_DIR}/mimalloc/src/mimalloc"
130+
SOURCE_DIR
131+
"${CMAKE_BINARY_DIR}/mimalloc/src/mimalloc"
131132
)
132133
FetchContent_MakeAvailable(mimalloc)
133134
endif()
@@ -219,7 +220,9 @@ add_custom_target(
219220
DEPENDS stage2
220221
)
221222

222-
add_custom_target(clean-stdlib COMMAND $(MAKE) -C stage1 clean-stdlib DEPENDS stage1)
223+
add_custom_target(clean-stdlib COMMAND $(MAKE) -C stage1 clean-stdlib DEPENDS stage1-configure)
224+
225+
add_custom_target(cache-get COMMAND $(MAKE) -C stage1 cache-get DEPENDS stage1-configure)
223226

224227
install(CODE "execute_process(COMMAND make -C stage1 install)")
225228

script/release_repos.yml

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -28,6 +28,14 @@ repositories:
2828
branch: main
2929
dependencies: []
3030

31+
- name: leansqlite
32+
url: https://github.com/leanprover/leansqlite
33+
toolchain-tag: true
34+
stable-branch: false
35+
branch: main
36+
dependencies:
37+
- plausible
38+
3139
- name: verso
3240
url: https://github.com/leanprover/verso
3341
toolchain-tag: true
@@ -100,7 +108,7 @@ repositories:
100108
toolchain-tag: true
101109
stable-branch: false
102110
branch: main
103-
dependencies: [lean4-cli, BibtexQuery, mathlib4]
111+
dependencies: [lean4-cli, BibtexQuery, mathlib4, leansqlite]
104112

105113
- name: cslib
106114
url: https://github.com/leanprover/cslib

script/release_steps.py

Lines changed: 66 additions & 54 deletions
Original file line numberDiff line numberDiff line change
@@ -481,11 +481,9 @@ def execute_release_steps(repo, version, config):
481481
run_command("lake update", cwd=repo_path, stream_output=True)
482482
elif repo_name == "verso":
483483
# verso has nested Lake projects in test-projects/ that each have their own
484-
# lake-manifest.json with a subverso pin. After updating the root manifest via
485-
# `lake update`, sync the de-modulized subverso rev into all sub-manifests.
486-
# The sub-projects use an old toolchain (v4.21.0) that doesn't support module/prelude
487-
# syntax, so they need the de-modulized version (tagged no-modules/<root-rev>).
488-
# The "SubVerso version consistency" CI check accepts either the root or de-modulized rev.
484+
# lake-manifest.json with a subverso pin and their own lean-toolchain.
485+
# After updating the root manifest via `lake update`, sync the de-modulized
486+
# subverso rev into all sub-manifests, and update their lean-toolchain files.
489487
run_command("lake update", cwd=repo_path, stream_output=True)
490488
print(blue("Syncing de-modulized subverso rev to test-project sub-manifests..."))
491489
sync_script = (
@@ -498,6 +496,15 @@ def execute_release_steps(repo, version, config):
498496
)
499497
run_command(sync_script, cwd=repo_path)
500498
print(green("Synced de-modulized subverso rev to all test-project sub-manifests"))
499+
# Update all lean-toolchain files in test-projects/ to match the root
500+
print(blue("Updating lean-toolchain files in test-projects/..."))
501+
find_result = run_command("find test-projects -name lean-toolchain", cwd=repo_path)
502+
for tc_path in find_result.stdout.strip().splitlines():
503+
if tc_path:
504+
tc_file = repo_path / tc_path
505+
with open(tc_file, "w") as f:
506+
f.write(f"leanprover/lean4:{version}\n")
507+
print(green(f" Updated {tc_path}"))
501508
elif dependencies:
502509
run_command(f'perl -pi -e \'s/"v4\\.[0-9]+(\\.[0-9]+)?(-rc[0-9]+)?"/"' + version + '"/g\' lakefile.*', cwd=repo_path)
503510
run_command("lake update", cwd=repo_path, stream_output=True)
@@ -659,56 +666,61 @@ def execute_release_steps(repo, version, config):
659666
# Fetch latest changes to ensure we have the most up-to-date nightly-testing branch
660667
print(blue("Fetching latest changes from origin..."))
661668
run_command("git fetch origin", cwd=repo_path)
662-
663-
try:
664-
print(blue("Merging origin/nightly-testing..."))
665-
run_command("git merge origin/nightly-testing", cwd=repo_path)
666-
print(green("Merge completed successfully"))
667-
except subprocess.CalledProcessError:
668-
# Merge failed due to conflicts - check which files are conflicted
669-
print(blue("Merge conflicts detected, checking which files are affected..."))
670-
671-
# Get conflicted files using git status
672-
status_result = run_command("git status --porcelain", cwd=repo_path)
673-
conflicted_files = []
674-
675-
for line in status_result.stdout.splitlines():
676-
if len(line) >= 2 and line[:2] in ['UU', 'AA', 'DD', 'AU', 'UA', 'DU', 'UD']:
677-
# Extract filename (skip the first 3 characters which are status codes)
678-
conflicted_files.append(line[3:])
679-
680-
# Filter out allowed files
681-
allowed_patterns = ['lean-toolchain', 'lake-manifest.json']
682-
problematic_files = []
683-
684-
for file in conflicted_files:
685-
is_allowed = any(pattern in file for pattern in allowed_patterns)
686-
if not is_allowed:
687-
problematic_files.append(file)
688-
689-
if problematic_files:
690-
# There are conflicts in non-allowed files - fail
691-
print(red("❌ Merge failed!"))
692-
print(red(f"Merging nightly-testing resulted in conflicts in:"))
693-
for file in problematic_files:
694-
print(red(f" - {file}"))
695-
print(red("Please resolve these conflicts manually."))
696-
return
697-
else:
698-
# Only allowed files are conflicted - resolve them automatically
699-
print(green(f"✅ Only allowed files conflicted: {', '.join(conflicted_files)}"))
700-
print(blue("Resolving conflicts automatically..."))
701-
702-
# For lean-toolchain and lake-manifest.json, keep our versions
669+
670+
# Check if nightly-testing branch exists on origin (use local ref after fetch for exact match)
671+
nightly_check = run_command("git show-ref --verify --quiet refs/remotes/origin/nightly-testing", cwd=repo_path, check=False)
672+
if nightly_check.returncode != 0:
673+
print(yellow("No nightly-testing branch found on origin, skipping merge"))
674+
else:
675+
try:
676+
print(blue("Merging origin/nightly-testing..."))
677+
run_command("git merge origin/nightly-testing", cwd=repo_path)
678+
print(green("Merge completed successfully"))
679+
except subprocess.CalledProcessError:
680+
# Merge failed due to conflicts - check which files are conflicted
681+
print(blue("Merge conflicts detected, checking which files are affected..."))
682+
683+
# Get conflicted files using git status
684+
status_result = run_command("git status --porcelain", cwd=repo_path)
685+
conflicted_files = []
686+
687+
for line in status_result.stdout.splitlines():
688+
if len(line) >= 2 and line[:2] in ['UU', 'AA', 'DD', 'AU', 'UA', 'DU', 'UD']:
689+
# Extract filename (skip the first 3 characters which are status codes)
690+
conflicted_files.append(line[3:])
691+
692+
# Filter out allowed files
693+
allowed_patterns = ['lean-toolchain', 'lake-manifest.json']
694+
problematic_files = []
695+
703696
for file in conflicted_files:
704-
print(blue(f"Keeping our version of {file}"))
705-
run_command(f"git checkout --ours {file}", cwd=repo_path)
706-
707-
# Complete the merge
708-
run_command("git add .", cwd=repo_path)
709-
run_command("git commit --no-edit", cwd=repo_path)
710-
711-
print(green("✅ Merge completed successfully with automatic conflict resolution"))
697+
is_allowed = any(pattern in file for pattern in allowed_patterns)
698+
if not is_allowed:
699+
problematic_files.append(file)
700+
701+
if problematic_files:
702+
# There are conflicts in non-allowed files - fail
703+
print(red("❌ Merge failed!"))
704+
print(red(f"Merging nightly-testing resulted in conflicts in:"))
705+
for file in problematic_files:
706+
print(red(f" - {file}"))
707+
print(red("Please resolve these conflicts manually."))
708+
return
709+
else:
710+
# Only allowed files are conflicted - resolve them automatically
711+
print(green(f"✅ Only allowed files conflicted: {', '.join(conflicted_files)}"))
712+
print(blue("Resolving conflicts automatically..."))
713+
714+
# For lean-toolchain and lake-manifest.json, keep our versions
715+
for file in conflicted_files:
716+
print(blue(f"Keeping our version of {file}"))
717+
run_command(f"git checkout --ours {file}", cwd=repo_path)
718+
719+
# Complete the merge
720+
run_command("git add .", cwd=repo_path)
721+
run_command("git commit --no-edit", cwd=repo_path)
722+
723+
print(green("✅ Merge completed successfully with automatic conflict resolution"))
712724

713725
# Build and test (skip for Mathlib)
714726
if repo_name not in ["mathlib4"]:

src/CMakeLists.txt

Lines changed: 22 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -116,11 +116,19 @@ option(CHECK_OLEAN_VERSION "Only load .olean files compiled with the current ver
116116
option(USE_LAKE "Use Lake instead of lean.mk for building core libs from language server" ON)
117117
option(USE_LAKE_CACHE "Use the Lake artifact cache for stage 1 builds (requires USE_LAKE)" OFF)
118118

119-
set(LEAN_EXTRA_MAKE_OPTS "" CACHE STRING "extra options to lean --make")
119+
set(LEAN_EXTRA_OPTS "" CACHE STRING "extra options to lean (via lake or make)")
120+
set(LEAN_EXTRA_MAKE_OPTS "" CACHE STRING "extra options to leanmake")
120121
set(LEANC_CC ${CMAKE_C_COMPILER} CACHE STRING "C compiler to use in `leanc`")
121122

122123
# Temporary, core-only flags. Must be synced with stdlib_flags.h.
123-
string(APPEND LEAN_EXTRA_MAKE_OPTS " -Dbackward.do.legacy=false")
124+
string(APPEND LEAN_EXTRA_OPTS " -Dbackward.do.legacy=false")
125+
126+
# option used by the CI to fail on warnings
127+
option(WFAIL "Fail build if warnings are emitted by Lean" ON)
128+
if(WFAIL MATCHES "ON")
129+
string(APPEND LAKE_EXTRA_ARGS " --wfail")
130+
string(APPEND LEAN_EXTRA_MAKE_OPTS " -DwarningAsError=true")
131+
endif()
124132

125133
if(LAZY_RC MATCHES "ON")
126134
set(LEAN_LAZY_RC "#define LEAN_LAZY_RC")
@@ -198,7 +206,7 @@ set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/lib/lean")
198206

199207
# OSX default thread stack size is very small. Moreover, in Debug mode, each new stack frame consumes a lot of extra memory.
200208
if((MULTI_THREAD MATCHES "ON") AND (CMAKE_SYSTEM_NAME MATCHES "Darwin"))
201-
string(APPEND LEAN_EXTRA_MAKE_OPTS " -s40000")
209+
string(APPEND LEAN_EXTRA_OPTS " -s40000")
202210
endif()
203211

204212
# We want explicit stack probes in huge Lean stack frames for robust stack overflow detection
@@ -670,6 +678,9 @@ else()
670678
set(LEAN_PATH_SEPARATOR ":")
671679
endif()
672680

681+
# inherit genral options for lean.mk.in and stdlib.make.in
682+
string(APPEND LEAN_EXTRA_MAKE_OPTS " ${LEAN_EXTRA_OPTS}")
683+
673684
# Version
674685
configure_file("${LEAN_SOURCE_DIR}/version.h.in" "${LEAN_BINARY_DIR}/include/lean/version.h")
675686
if(STAGE EQUAL 0)
@@ -981,6 +992,13 @@ add_custom_target(
981992

982993
add_custom_target(clean-olean DEPENDS clean-stdlib)
983994

995+
if(USE_LAKE_CACHE)
996+
add_custom_target(
997+
cache-get
998+
COMMAND ${PREV_STAGE}/bin/lake${CMAKE_EXECUTABLE_SUFFIX} cache get --repo=leanprover/lean4
999+
)
1000+
endif()
1001+
9841002
install(
9851003
DIRECTORY "${CMAKE_BINARY_DIR}/lib/"
9861004
DESTINATION lib
@@ -1054,7 +1072,7 @@ string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}" LEANC_CC "${LEANC_CC}")
10541072
string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}" LEANC_INTERNAL_FLAGS "${LEANC_INTERNAL_FLAGS}")
10551073
string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}" LEANC_INTERNAL_LINKER_FLAGS "${LEANC_INTERNAL_LINKER_FLAGS}")
10561074

1057-
toml_escape("${LEAN_EXTRA_MAKE_OPTS}" LEAN_EXTRA_OPTS_TOML)
1075+
toml_escape("${LEAN_EXTRA_OPTS}" LEAN_EXTRA_OPTS_TOML)
10581076

10591077
if(CMAKE_BUILD_TYPE MATCHES "Debug|Release|RelWithDebInfo|MinSizeRel")
10601078
set(CMAKE_BUILD_TYPE_TOML "${CMAKE_BUILD_TYPE}")

0 commit comments

Comments
 (0)