Skip to content

Commit 9240c30

Browse files
kim-emkim-em
committed
Merge branch 'master' into grind_cat2
2 parents e6b5207 + da57f1f commit 9240c30

209 files changed

Lines changed: 3045 additions & 1673 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.

‎.github/build.in.yml‎

Lines changed: 15 additions & 52 deletions
Original file line numberDiff line numberDiff line change
@@ -148,57 +148,6 @@ jobs:
148148
ls .lake/build/bin/check-yaml
149149
ls .lake/packages/importGraph/.lake/build/bin/graph
150150
151-
# TEMPORARY: remove everything below this after #27691 is merged
152-
cat << 'EOF' > scripts/lake-build-with-retry.sh
153-
#!/bin/bash
154-
# Script to run lake build on a target until --no-build succeeds
155-
# Usage: ./lake-build-with-retry.sh <target_name> [max_tries, default: 5]
156-
157-
# Make this script robust against unintentional errors.
158-
# See e.g. http://redsymbol.net/articles/unofficial-bash-strict-mode/ for explanation.
159-
set -euo pipefail
160-
IFS=$'\n\t'
161-
162-
TARGET_NAME="$1"
163-
MAX_TRIES="${2:-5}"
164-
165-
if [ -z "$TARGET_NAME" ]; then
166-
echo "Usage: $0 <target_name> [max_tries, default: 5]"
167-
echo "Example: $0 Mathlib 5"
168-
exit 1
169-
fi
170-
171-
echo "Building $TARGET_NAME with up to $MAX_TRIES attempts..."
172-
173-
counter=0
174-
while true; do
175-
counter=$((counter + 1))
176-
177-
echo "::group::{lake build: attempt $counter}"
178-
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI $TARGET_NAME"
179-
echo "::endgroup::"
180-
181-
echo "::group::{lake build --no-build: attempt $counter}"
182-
set +e
183-
lake build --no-build -v "$TARGET_NAME"
184-
result=$?
185-
set -e
186-
echo "::endgroup::"
187-
188-
if [ $result -eq 0 ]; then
189-
echo "lake build --no-build succeeded!"
190-
exit 0
191-
fi
192-
193-
if [ $counter -ge $MAX_TRIES ]; then
194-
echo "Failed to build good oleans for $TARGET_NAME after $MAX_TRIES attempts!"
195-
exit 1
196-
fi
197-
done
198-
EOF
199-
200-
chmod 755 scripts/lake-build-with-retry.sh
201-
202151
- name: cleanup .cache/mathlib
203152
# This needs write access to .cache/mathlib, so can't be run inside landrun.
204153
# However it is only using the `master` version of `cache`, so is safe to run outside landrun.
@@ -313,6 +262,13 @@ jobs:
313262
cd pr-branch
314263
du .lake/build/lib/lean/Mathlib || echo "This code should be unreachable"
315264
265+
- name: upload artifact containing contents of pr-branch
266+
# temporary measure for debugging no-build failures
267+
uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
268+
with:
269+
name: mathlib4_artifact
270+
path: pr-branch/
271+
316272
# The cache secrets are available here, so we must not run any untrusted code.
317273
- name: upload cache
318274
# We only upload the cache if the build started (whether succeeding, failing, or cancelled)
@@ -365,7 +321,14 @@ jobs:
365321
366322
- name: Check if building Archive or Counterexamples failed
367323
if: steps.archive.outcome == 'failure' || steps.counterexamples.outcome == 'failure'
368-
run: exit 1
324+
run: |
325+
if [ "${{ steps.archive.outcome }}" == "failure" ]; then
326+
echo "❌ The \"build archive\" step above failed; please check its logs."
327+
fi
328+
if [ "${{ steps.counterexamples.outcome }}" == "failure" ]; then
329+
echo "❌ The \"build counterexamples\" step above failed; please check its logs."
330+
fi
331+
exit 1
369332
370333
# The cache secrets are available here, so we must not run any untrusted code.
371334
- name: put archive and counterexamples cache

‎.github/workflows/bors.yml‎

Lines changed: 15 additions & 52 deletions
Original file line numberDiff line numberDiff line change
@@ -158,57 +158,6 @@ jobs:
158158
ls .lake/build/bin/check-yaml
159159
ls .lake/packages/importGraph/.lake/build/bin/graph
160160
161-
# TEMPORARY: remove everything below this after #27691 is merged
162-
cat << 'EOF' > scripts/lake-build-with-retry.sh
163-
#!/bin/bash
164-
# Script to run lake build on a target until --no-build succeeds
165-
# Usage: ./lake-build-with-retry.sh <target_name> [max_tries, default: 5]
166-
167-
# Make this script robust against unintentional errors.
168-
# See e.g. http://redsymbol.net/articles/unofficial-bash-strict-mode/ for explanation.
169-
set -euo pipefail
170-
IFS=$'\n\t'
171-
172-
TARGET_NAME="$1"
173-
MAX_TRIES="${2:-5}"
174-
175-
if [ -z "$TARGET_NAME" ]; then
176-
echo "Usage: $0 <target_name> [max_tries, default: 5]"
177-
echo "Example: $0 Mathlib 5"
178-
exit 1
179-
fi
180-
181-
echo "Building $TARGET_NAME with up to $MAX_TRIES attempts..."
182-
183-
counter=0
184-
while true; do
185-
counter=$((counter + 1))
186-
187-
echo "::group::{lake build: attempt $counter}"
188-
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI $TARGET_NAME"
189-
echo "::endgroup::"
190-
191-
echo "::group::{lake build --no-build: attempt $counter}"
192-
set +e
193-
lake build --no-build -v "$TARGET_NAME"
194-
result=$?
195-
set -e
196-
echo "::endgroup::"
197-
198-
if [ $result -eq 0 ]; then
199-
echo "lake build --no-build succeeded!"
200-
exit 0
201-
fi
202-
203-
if [ $counter -ge $MAX_TRIES ]; then
204-
echo "Failed to build good oleans for $TARGET_NAME after $MAX_TRIES attempts!"
205-
exit 1
206-
fi
207-
done
208-
EOF
209-
210-
chmod 755 scripts/lake-build-with-retry.sh
211-
212161
- name: cleanup .cache/mathlib
213162
# This needs write access to .cache/mathlib, so can't be run inside landrun.
214163
# However it is only using the `master` version of `cache`, so is safe to run outside landrun.
@@ -323,6 +272,13 @@ jobs:
323272
cd pr-branch
324273
du .lake/build/lib/lean/Mathlib || echo "This code should be unreachable"
325274
275+
- name: upload artifact containing contents of pr-branch
276+
# temporary measure for debugging no-build failures
277+
uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
278+
with:
279+
name: mathlib4_artifact
280+
path: pr-branch/
281+
326282
# The cache secrets are available here, so we must not run any untrusted code.
327283
- name: upload cache
328284
# We only upload the cache if the build started (whether succeeding, failing, or cancelled)
@@ -375,7 +331,14 @@ jobs:
375331
376332
- name: Check if building Archive or Counterexamples failed
377333
if: steps.archive.outcome == 'failure' || steps.counterexamples.outcome == 'failure'
378-
run: exit 1
334+
run: |
335+
if [ "${{ steps.archive.outcome }}" == "failure" ]; then
336+
echo "❌ The \"build archive\" step above failed; please check its logs."
337+
fi
338+
if [ "${{ steps.counterexamples.outcome }}" == "failure" ]; then
339+
echo "❌ The \"build counterexamples\" step above failed; please check its logs."
340+
fi
341+
exit 1
379342
380343
# The cache secrets are available here, so we must not run any untrusted code.
381344
- name: put archive and counterexamples cache

‎.github/workflows/build.yml‎

Lines changed: 15 additions & 52 deletions
Original file line numberDiff line numberDiff line change
@@ -165,57 +165,6 @@ jobs:
165165
ls .lake/build/bin/check-yaml
166166
ls .lake/packages/importGraph/.lake/build/bin/graph
167167
168-
# TEMPORARY: remove everything below this after #27691 is merged
169-
cat << 'EOF' > scripts/lake-build-with-retry.sh
170-
#!/bin/bash
171-
# Script to run lake build on a target until --no-build succeeds
172-
# Usage: ./lake-build-with-retry.sh <target_name> [max_tries, default: 5]
173-
174-
# Make this script robust against unintentional errors.
175-
# See e.g. http://redsymbol.net/articles/unofficial-bash-strict-mode/ for explanation.
176-
set -euo pipefail
177-
IFS=$'\n\t'
178-
179-
TARGET_NAME="$1"
180-
MAX_TRIES="${2:-5}"
181-
182-
if [ -z "$TARGET_NAME" ]; then
183-
echo "Usage: $0 <target_name> [max_tries, default: 5]"
184-
echo "Example: $0 Mathlib 5"
185-
exit 1
186-
fi
187-
188-
echo "Building $TARGET_NAME with up to $MAX_TRIES attempts..."
189-
190-
counter=0
191-
while true; do
192-
counter=$((counter + 1))
193-
194-
echo "::group::{lake build: attempt $counter}"
195-
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI $TARGET_NAME"
196-
echo "::endgroup::"
197-
198-
echo "::group::{lake build --no-build: attempt $counter}"
199-
set +e
200-
lake build --no-build -v "$TARGET_NAME"
201-
result=$?
202-
set -e
203-
echo "::endgroup::"
204-
205-
if [ $result -eq 0 ]; then
206-
echo "lake build --no-build succeeded!"
207-
exit 0
208-
fi
209-
210-
if [ $counter -ge $MAX_TRIES ]; then
211-
echo "Failed to build good oleans for $TARGET_NAME after $MAX_TRIES attempts!"
212-
exit 1
213-
fi
214-
done
215-
EOF
216-
217-
chmod 755 scripts/lake-build-with-retry.sh
218-
219168
- name: cleanup .cache/mathlib
220169
# This needs write access to .cache/mathlib, so can't be run inside landrun.
221170
# However it is only using the `master` version of `cache`, so is safe to run outside landrun.
@@ -330,6 +279,13 @@ jobs:
330279
cd pr-branch
331280
du .lake/build/lib/lean/Mathlib || echo "This code should be unreachable"
332281
282+
- name: upload artifact containing contents of pr-branch
283+
# temporary measure for debugging no-build failures
284+
uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
285+
with:
286+
name: mathlib4_artifact
287+
path: pr-branch/
288+
333289
# The cache secrets are available here, so we must not run any untrusted code.
334290
- name: upload cache
335291
# We only upload the cache if the build started (whether succeeding, failing, or cancelled)
@@ -382,7 +338,14 @@ jobs:
382338
383339
- name: Check if building Archive or Counterexamples failed
384340
if: steps.archive.outcome == 'failure' || steps.counterexamples.outcome == 'failure'
385-
run: exit 1
341+
run: |
342+
if [ "${{ steps.archive.outcome }}" == "failure" ]; then
343+
echo "❌ The \"build archive\" step above failed; please check its logs."
344+
fi
345+
if [ "${{ steps.counterexamples.outcome }}" == "failure" ]; then
346+
echo "❌ The \"build counterexamples\" step above failed; please check its logs."
347+
fi
348+
exit 1
386349
387350
# The cache secrets are available here, so we must not run any untrusted code.
388351
- name: put archive and counterexamples cache

‎.github/workflows/build_fork.yml‎

Lines changed: 15 additions & 52 deletions
Original file line numberDiff line numberDiff line change
@@ -162,57 +162,6 @@ jobs:
162162
ls .lake/build/bin/check-yaml
163163
ls .lake/packages/importGraph/.lake/build/bin/graph
164164
165-
# TEMPORARY: remove everything below this after #27691 is merged
166-
cat << 'EOF' > scripts/lake-build-with-retry.sh
167-
#!/bin/bash
168-
# Script to run lake build on a target until --no-build succeeds
169-
# Usage: ./lake-build-with-retry.sh <target_name> [max_tries, default: 5]
170-
171-
# Make this script robust against unintentional errors.
172-
# See e.g. http://redsymbol.net/articles/unofficial-bash-strict-mode/ for explanation.
173-
set -euo pipefail
174-
IFS=$'\n\t'
175-
176-
TARGET_NAME="$1"
177-
MAX_TRIES="${2:-5}"
178-
179-
if [ -z "$TARGET_NAME" ]; then
180-
echo "Usage: $0 <target_name> [max_tries, default: 5]"
181-
echo "Example: $0 Mathlib 5"
182-
exit 1
183-
fi
184-
185-
echo "Building $TARGET_NAME with up to $MAX_TRIES attempts..."
186-
187-
counter=0
188-
while true; do
189-
counter=$((counter + 1))
190-
191-
echo "::group::{lake build: attempt $counter}"
192-
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI $TARGET_NAME"
193-
echo "::endgroup::"
194-
195-
echo "::group::{lake build --no-build: attempt $counter}"
196-
set +e
197-
lake build --no-build -v "$TARGET_NAME"
198-
result=$?
199-
set -e
200-
echo "::endgroup::"
201-
202-
if [ $result -eq 0 ]; then
203-
echo "lake build --no-build succeeded!"
204-
exit 0
205-
fi
206-
207-
if [ $counter -ge $MAX_TRIES ]; then
208-
echo "Failed to build good oleans for $TARGET_NAME after $MAX_TRIES attempts!"
209-
exit 1
210-
fi
211-
done
212-
EOF
213-
214-
chmod 755 scripts/lake-build-with-retry.sh
215-
216165
- name: cleanup .cache/mathlib
217166
# This needs write access to .cache/mathlib, so can't be run inside landrun.
218167
# However it is only using the `master` version of `cache`, so is safe to run outside landrun.
@@ -327,6 +276,13 @@ jobs:
327276
cd pr-branch
328277
du .lake/build/lib/lean/Mathlib || echo "This code should be unreachable"
329278
279+
- name: upload artifact containing contents of pr-branch
280+
# temporary measure for debugging no-build failures
281+
uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
282+
with:
283+
name: mathlib4_artifact
284+
path: pr-branch/
285+
330286
# The cache secrets are available here, so we must not run any untrusted code.
331287
- name: upload cache
332288
# We only upload the cache if the build started (whether succeeding, failing, or cancelled)
@@ -379,7 +335,14 @@ jobs:
379335
380336
- name: Check if building Archive or Counterexamples failed
381337
if: steps.archive.outcome == 'failure' || steps.counterexamples.outcome == 'failure'
382-
run: exit 1
338+
run: |
339+
if [ "${{ steps.archive.outcome }}" == "failure" ]; then
340+
echo "❌ The \"build archive\" step above failed; please check its logs."
341+
fi
342+
if [ "${{ steps.counterexamples.outcome }}" == "failure" ]; then
343+
echo "❌ The \"build counterexamples\" step above failed; please check its logs."
344+
fi
345+
exit 1
383346
384347
# The cache secrets are available here, so we must not run any untrusted code.
385348
- name: put archive and counterexamples cache

0 commit comments

Comments
 (0)