Skip to content

Commit 51da749

Browse files
bryangingechenbryangingechen
committed
chore: remove inlined lake-build-with-retry.sh from workflow, improve log messages (leanprover-community#28016)
To merge leanprover-community#27691, I had to inline a copy of `lake-build-with-retry.sh` into the workflow file (since the workflow always tries to run the `master` branch version of scripts, etc.). Now that that file exists in the `master` branch, we can remove this code. I also improved the log messages for the step checking if the archive + counterexamples builds failed.
1 parent bfffa50 commit 51da749

4 files changed

Lines changed: 32 additions & 208 deletions

File tree

‎.github/build.in.yml‎

Lines changed: 8 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.
@@ -372,7 +321,14 @@ jobs:
372321
373322
- name: Check if building Archive or Counterexamples failed
374323
if: steps.archive.outcome == 'failure' || steps.counterexamples.outcome == 'failure'
375-
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
376332
377333
# The cache secrets are available here, so we must not run any untrusted code.
378334
- name: put archive and counterexamples cache

‎.github/workflows/bors.yml‎

Lines changed: 8 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.
@@ -382,7 +331,14 @@ jobs:
382331
383332
- name: Check if building Archive or Counterexamples failed
384333
if: steps.archive.outcome == 'failure' || steps.counterexamples.outcome == 'failure'
385-
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
386342
387343
# The cache secrets are available here, so we must not run any untrusted code.
388344
- name: put archive and counterexamples cache

‎.github/workflows/build.yml‎

Lines changed: 8 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.
@@ -389,7 +338,14 @@ jobs:
389338
390339
- name: Check if building Archive or Counterexamples failed
391340
if: steps.archive.outcome == 'failure' || steps.counterexamples.outcome == 'failure'
392-
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
393349
394350
# The cache secrets are available here, so we must not run any untrusted code.
395351
- name: put archive and counterexamples cache

‎.github/workflows/build_fork.yml‎

Lines changed: 8 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.
@@ -386,7 +335,14 @@ jobs:
386335
387336
- name: Check if building Archive or Counterexamples failed
388337
if: steps.archive.outcome == 'failure' || steps.counterexamples.outcome == 'failure'
389-
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
390346
391347
# The cache secrets are available here, so we must not run any untrusted code.
392348
- name: put archive and counterexamples cache

0 commit comments

Comments
 (0)