Skip to content

Commit 0a82ae8

Browse files
CoolRmalCoolRmal
authored
Merge branch 'leanprover-community:master' into derivativetest
2 parents 3872f4d + 20310f5 commit 0a82ae8

873 files changed

Lines changed: 18980 additions & 10418 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.

‎.devcontainer/Dockerfile‎

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,6 @@
1-
FROM mcr.microsoft.com/devcontainers/base:jammy
1+
FROM mcr.microsoft.com/devcontainers/base:ubuntu
22

33
USER vscode
44
WORKDIR /home/vscode
55

66
RUN curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
7-
8-
ENV PATH="/home/vscode/.elan/bin:${PATH}"

‎.devcontainer/devcontainer.json‎

Lines changed: 7 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,17 +1,20 @@
11
{
22
"name": "Mathlib4 dev container",
33

4-
"image": "ghcr.io/leanprover-community/mathlib4/gitpod",
4+
"build": {
5+
"dockerfile": "Dockerfile"
6+
},
57

68
"onCreateCommand": "lake exe cache get!",
79

810
"hostRequirements": {
9-
"cpus": 4
11+
"cpus": 4,
12+
"memory": "8gb"
1013
},
1114

1215
"customizations": {
13-
"vscode" : {
14-
"extensions" : [ "leanprover.lean4" ]
16+
"vscode": {
17+
"extensions": ["leanprover.lean4"]
1518
}
1619
}
1720
}

‎.github/build.in.yml‎

Lines changed: 16 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -495,20 +495,6 @@ jobs:
495495
# run: |
496496
# cd pr-branch
497497
# env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
498-
499-
- name: kill stray runLinter processes
500-
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
501-
continue-on-error: true
502-
shell: bash
503-
run: |
504-
echo "Checking for runLinter processes..."
505-
if ps -eo pid,lstart,command | grep -F runLinter | grep -v grep; then
506-
echo "Killing runLinter processes..."
507-
pkill -f runLinter || true
508-
else
509-
echo "No stray runLinter processes found."
510-
fi
511-
512498
- name: lint mathlib
513499
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
514500
id: lint
@@ -519,7 +505,7 @@ jobs:
519505
# Try running with --trace; if it fails due to argument parsing, the PR needs to merge master
520506
# We use .lake/ for the output file because landrun restricts /tmp access
521507
for attempt in 1 2; do
522-
if timeout 15m env LEAN_ABORT_ON_PANIC=1 stdbuf -oL lake exe runLinter --trace Mathlib 2>&1 | tee ".lake/lint_output_attempt_${attempt}.txt"; then
508+
if timeout 10m env LEAN_ABORT_ON_PANIC=1 stdbuf -oL lake exe runLinter --trace Mathlib 2>&1 | tee ".lake/lint_output_attempt_${attempt}.txt"; then
523509
break
524510
fi
525511
status=${PIPESTATUS[0]}
@@ -541,20 +527,27 @@ jobs:
541527
if [ "$status" -eq 124 ]; then
542528
echo "runLinter timed out (attempt $attempt)."
543529
if [ "$attempt" -lt 2 ]; then
544-
echo "Checking for runLinter processes..."
545-
if ps -eo pid,lstart,command | grep -F runLinter | grep -v grep; then
546-
echo "Killing runLinter processes..."
547-
pkill -f runLinter || true
548-
else
549-
echo "No stray runLinter processes found."
550-
fi
551530
echo "Retrying runLinter after timeout..."
552531
continue
553532
fi
554533
fi
555534
exit $status
556535
done
557536
537+
# We need to separate this step from the previous script because it needs to run outside of landrun
538+
- name: kill stray runLinter processes
539+
if: ${{ steps.lint.outcome == 'failure' }}
540+
continue-on-error: true
541+
shell: bash
542+
run: |
543+
echo "Checking for runLinter processes..."
544+
if pgrep -af runLinter; then
545+
echo "Killing runLinter processes..."
546+
pkill -f runLinter || true
547+
else
548+
echo "No stray runLinter processes found."
549+
fi
550+
558551
- name: end gh-problem-match-wrap for shake and lint steps
559552
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
560553
with:
@@ -579,15 +572,6 @@ jobs:
579572
exit 1
580573
fi
581574
582-
- name: list stray runLinter processes
583-
shell: bash
584-
if: always()
585-
run: |
586-
echo "Checking for runLinter processes..."
587-
if ! ps -eo pid,lstart,command | grep -F runLinter | grep -v grep; then
588-
echo "No stray runLinter processes found."
589-
fi
590-
591575
- name: Post comments for lean-pr-testing-NNNN and batteries-pr-testing-NNNN branches
592576
if: always()
593577
shell: bash
@@ -676,7 +660,7 @@ jobs:
676660
# make sure everything is available for test/import_all.lean
677661
# and that miscellaneous executables still work
678662
run: |
679-
lake build Batteries Qq Aesop ProofWidgets Plausible pole unused
663+
lake build Batteries Qq Aesop ProofWidgets Plausible
680664
681665
- name: build AesopTest (nightly-testing only)
682666
# Only run on the mathlib4-nightly-testing repository

‎.github/workflows/add_label_from_diff.yaml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,7 @@ jobs:
4040
labels="$(lake exe autolabel)"
4141
printf '%s\n' "${labels}"
4242
# extract
43-
label="$(printf '%s' "${labels}" | sed -n 's=.*#\[\([^,]*\)\].*=\1=p')"
43+
label="$(printf '%s' "${labels}" | sed -n 's=^::notice::.*#\[\([^,]*\)\].*=\1=p')"
4444
printf 'label: "%s"\n' "${label}"
4545
if [ -n "${label}" ]
4646
then

‎.github/workflows/bors.yml‎

Lines changed: 16 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -505,20 +505,6 @@ jobs:
505505
# run: |
506506
# cd pr-branch
507507
# env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
508-
509-
- name: kill stray runLinter processes
510-
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
511-
continue-on-error: true
512-
shell: bash
513-
run: |
514-
echo "Checking for runLinter processes..."
515-
if ps -eo pid,lstart,command | grep -F runLinter | grep -v grep; then
516-
echo "Killing runLinter processes..."
517-
pkill -f runLinter || true
518-
else
519-
echo "No stray runLinter processes found."
520-
fi
521-
522508
- name: lint mathlib
523509
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
524510
id: lint
@@ -529,7 +515,7 @@ jobs:
529515
# Try running with --trace; if it fails due to argument parsing, the PR needs to merge master
530516
# We use .lake/ for the output file because landrun restricts /tmp access
531517
for attempt in 1 2; do
532-
if timeout 15m env LEAN_ABORT_ON_PANIC=1 stdbuf -oL lake exe runLinter --trace Mathlib 2>&1 | tee ".lake/lint_output_attempt_${attempt}.txt"; then
518+
if timeout 10m env LEAN_ABORT_ON_PANIC=1 stdbuf -oL lake exe runLinter --trace Mathlib 2>&1 | tee ".lake/lint_output_attempt_${attempt}.txt"; then
533519
break
534520
fi
535521
status=${PIPESTATUS[0]}
@@ -551,20 +537,27 @@ jobs:
551537
if [ "$status" -eq 124 ]; then
552538
echo "runLinter timed out (attempt $attempt)."
553539
if [ "$attempt" -lt 2 ]; then
554-
echo "Checking for runLinter processes..."
555-
if ps -eo pid,lstart,command | grep -F runLinter | grep -v grep; then
556-
echo "Killing runLinter processes..."
557-
pkill -f runLinter || true
558-
else
559-
echo "No stray runLinter processes found."
560-
fi
561540
echo "Retrying runLinter after timeout..."
562541
continue
563542
fi
564543
fi
565544
exit $status
566545
done
567546
547+
# We need to separate this step from the previous script because it needs to run outside of landrun
548+
- name: kill stray runLinter processes
549+
if: ${{ steps.lint.outcome == 'failure' }}
550+
continue-on-error: true
551+
shell: bash
552+
run: |
553+
echo "Checking for runLinter processes..."
554+
if pgrep -af runLinter; then
555+
echo "Killing runLinter processes..."
556+
pkill -f runLinter || true
557+
else
558+
echo "No stray runLinter processes found."
559+
fi
560+
568561
- name: end gh-problem-match-wrap for shake and lint steps
569562
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
570563
with:
@@ -589,15 +582,6 @@ jobs:
589582
exit 1
590583
fi
591584
592-
- name: list stray runLinter processes
593-
shell: bash
594-
if: always()
595-
run: |
596-
echo "Checking for runLinter processes..."
597-
if ! ps -eo pid,lstart,command | grep -F runLinter | grep -v grep; then
598-
echo "No stray runLinter processes found."
599-
fi
600-
601585
- name: Post comments for lean-pr-testing-NNNN and batteries-pr-testing-NNNN branches
602586
if: always()
603587
shell: bash
@@ -686,7 +670,7 @@ jobs:
686670
# make sure everything is available for test/import_all.lean
687671
# and that miscellaneous executables still work
688672
run: |
689-
lake build Batteries Qq Aesop ProofWidgets Plausible pole unused
673+
lake build Batteries Qq Aesop ProofWidgets Plausible
690674
691675
- name: build AesopTest (nightly-testing only)
692676
# Only run on the mathlib4-nightly-testing repository

‎.github/workflows/build.yml‎

Lines changed: 16 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -511,20 +511,6 @@ jobs:
511511
# run: |
512512
# cd pr-branch
513513
# env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
514-
515-
- name: kill stray runLinter processes
516-
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
517-
continue-on-error: true
518-
shell: bash
519-
run: |
520-
echo "Checking for runLinter processes..."
521-
if ps -eo pid,lstart,command | grep -F runLinter | grep -v grep; then
522-
echo "Killing runLinter processes..."
523-
pkill -f runLinter || true
524-
else
525-
echo "No stray runLinter processes found."
526-
fi
527-
528514
- name: lint mathlib
529515
if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
530516
id: lint
@@ -535,7 +521,7 @@ jobs:
535521
# Try running with --trace; if it fails due to argument parsing, the PR needs to merge master
536522
# We use .lake/ for the output file because landrun restricts /tmp access
537523
for attempt in 1 2; do
538-
if timeout 15m env LEAN_ABORT_ON_PANIC=1 stdbuf -oL lake exe runLinter --trace Mathlib 2>&1 | tee ".lake/lint_output_attempt_${attempt}.txt"; then
524+
if timeout 10m env LEAN_ABORT_ON_PANIC=1 stdbuf -oL lake exe runLinter --trace Mathlib 2>&1 | tee ".lake/lint_output_attempt_${attempt}.txt"; then
539525
break
540526
fi
541527
status=${PIPESTATUS[0]}
@@ -557,20 +543,27 @@ jobs:
557543
if [ "$status" -eq 124 ]; then
558544
echo "runLinter timed out (attempt $attempt)."
559545
if [ "$attempt" -lt 2 ]; then
560-
echo "Checking for runLinter processes..."
561-
if ps -eo pid,lstart,command | grep -F runLinter | grep -v grep; then
562-
echo "Killing runLinter processes..."
563-
pkill -f runLinter || true
564-
else
565-
echo "No stray runLinter processes found."
566-
fi
567546
echo "Retrying runLinter after timeout..."
568547
continue
569548
fi
570549
fi
571550
exit $status
572551
done
573552
553+
# We need to separate this step from the previous script because it needs to run outside of landrun
554+
- name: kill stray runLinter processes
555+
if: ${{ steps.lint.outcome == 'failure' }}
556+
continue-on-error: true
557+
shell: bash
558+
run: |
559+
echo "Checking for runLinter processes..."
560+
if pgrep -af runLinter; then
561+
echo "Killing runLinter processes..."
562+
pkill -f runLinter || true
563+
else
564+
echo "No stray runLinter processes found."
565+
fi
566+
574567
- name: end gh-problem-match-wrap for shake and lint steps
575568
uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
576569
with:
@@ -595,15 +588,6 @@ jobs:
595588
exit 1
596589
fi
597590
598-
- name: list stray runLinter processes
599-
shell: bash
600-
if: always()
601-
run: |
602-
echo "Checking for runLinter processes..."
603-
if ! ps -eo pid,lstart,command | grep -F runLinter | grep -v grep; then
604-
echo "No stray runLinter processes found."
605-
fi
606-
607591
- name: Post comments for lean-pr-testing-NNNN and batteries-pr-testing-NNNN branches
608592
if: always()
609593
shell: bash
@@ -692,7 +676,7 @@ jobs:
692676
# make sure everything is available for test/import_all.lean
693677
# and that miscellaneous executables still work
694678
run: |
695-
lake build Batteries Qq Aesop ProofWidgets Plausible pole unused
679+
lake build Batteries Qq Aesop ProofWidgets Plausible
696680
697681
- name: build AesopTest (nightly-testing only)
698682
# Only run on the mathlib4-nightly-testing repository

0 commit comments

Comments
 (0)