Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat: lake exe mk_all in CI #11874

Closed
wants to merge 48 commits into from
Closed

[Merged by Bors] - feat: lake exe mk_all in CI #11874

Show file tree
Hide file tree
Changes from 46 commits
Commits
Show all changes
48 commits
Select commit Hold shift + click to select a range
c2616fe
feat: `mk_all` script implemented in Lean
adomani Apr 2, 2024
2e159d0
move mkAll to Mathlib.Tactic
adomani Apr 2, 2024
6c7c746
Flag to use `walkDir` or `git ls-files`.
adomani Apr 2, 2024
6b80b6e
Rename file mkAll --> MKAll + update imports with itself!
adomani Apr 2, 2024
a2198f6
shake
adomani Apr 2, 2024
74966c0
reimplement as a Lean executable
YaelDillies Apr 2, 2024
44a4ba2
docs
adomani Apr 3, 2024
2cf953d
inline `git ls-files`
adomani Apr 3, 2024
66c5eab
golf
adomani Apr 3, 2024
d581e26
exit code
adomani Apr 3, 2024
a9362e7
Sort only once
adomani Apr 3, 2024
e214aae
Fix uncaught exception?
adomani Apr 3, 2024
67d9aae
Add Mario's getLeanLibs and use it!
adomani Apr 3, 2024
d8635b9
Special case package `mathlib`, as opposed to "containing `mathlib`.
adomani Apr 3, 2024
6485b73
docs and trim
adomani Apr 3, 2024
f9105d8
Only import existing files
adomani Apr 3, 2024
49729f9
Repetition and reverse
adomani Apr 3, 2024
50738b5
feat: mkAll in CI
adomani Apr 3, 2024
f2aaac2
Reorder steps
adomani Apr 4, 2024
16b6fdc
add check_imported
adomani Apr 4, 2024
049e0c6
remove check_imported
adomani Apr 4, 2024
b6e6e77
Merge remote-tracking branch 'origin/master' into yad/mkAll_in_CI
adomani May 7, 2024
6674129
Merge remote-tracking branch 'origin/master' into adomani/mkAll_in_lean
adomani May 9, 2024
b028d71
Merge branch 'adomani/mkAll_in_lean' into yad/mkAll_in_CI
adomani May 9, 2024
1ea08aa
shake
adomani May 9, 2024
f2bda6b
action lint
adomani May 9, 2024
11e062a
fix mkAll with Kim's code
adomani May 10, 2024
3b96989
Merge branch 'adomani/mkAll_in_lean' into yad/mkAll_in_CI
adomani May 10, 2024
210f2bb
remove mathlibextras
adomani May 10, 2024
2498357
rename to `mk_all`
YaelDillies May 10, 2024
c0d0ea2
Merge branch 'adomani/mkAll_in_lean' into yad/mkAll_in_CI
adomani May 10, 2024
ee40a0f
update to mk_all name
adomani May 10, 2024
7fb765a
docs
adomani May 10, 2024
4a80ca2
Merge branch 'adomani/mkAll_in_lean' into yad/mkAll_in_CI
adomani May 10, 2024
5c2814e
Merge branch 'master' into yad/mkAll_in_CI
adomani May 24, 2024
2407a79
Apply suggestions from code review
adomani May 24, 2024
0078b1b
rename and docs, after Michael's comments
adomani May 24, 2024
5de2a9a
Merge branch 'yad/mkAll_in_CI' of github.com:leanprover-community/mat…
adomani May 24, 2024
842b6af
Merge branch 'master' into adomani/mkAll_in_lean
adomani May 24, 2024
98dd85b
Merge branch 'master' into yad/mkAll_in_CI
adomani May 24, 2024
f6ef6c8
synch with branch with CI
adomani May 24, 2024
34f4972
remove shell-based `mk_all` script from CI
adomani May 25, 2024
baa366c
Merge remote-tracking branch 'origin/master' into adomani/mkAll_in_lean
adomani May 27, 2024
cc7b70a
getAll returns an array of strings. Add todo about dependencies
adomani May 27, 2024
982aebc
Merge branch 'adomani/mkAll_in_lean' into yad/mkAll_in_CI
adomani May 27, 2024
5d0e9b3
Merge branch 'master' into yad/mkAll_in_CI
adomani May 29, 2024
6564e5e
Also use the script in the reviewdog linter.
grunweg Jun 1, 2024
2228950
Remove step from bors.toml
grunweg Jun 1, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
28 changes: 8 additions & 20 deletions .github/workflows/bors.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -64,24 +64,6 @@ jobs:
run: |
./scripts/lint-bib.sh

check_imported:
if: github.repository == 'leanprover-community/mathlib4'
name: Check all files imported
runs-on: ubuntu-latest
steps:
- name: cleanup
run: |
find . -name . -o -prune -exec rm -rf -- {} +

- uses: actions/checkout@v4

- name: update import-only files in {Mathlib Mathlib/Tactic Counterexamples Archive}.lean
run: |
./scripts/mk_all.sh

- name: check that all files are imported
run: git diff --exit-code

check_workflows:
if: github.repository == 'leanprover-community/mathlib4'
name: check workflows
Expand Down Expand Up @@ -152,7 +134,7 @@ jobs:
# but verify that this didn't change anything in the `check_imported` job.
- name: update Mathlib.lean
run: |
./scripts/mk_all.sh Mathlib
lake exe mk_all --lib Mathlib

- name: If using a lean-pr-release toolchain, uninstall
run: |
Expand All @@ -166,6 +148,12 @@ jobs:
lean --version
lake --version

- name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
adomani marked this conversation as resolved.
Show resolved Hide resolved
run: lake exe mk_all

- name: check_imported
run: git diff --exit-code

- name: build cache
run: |
lake build cache
Expand Down Expand Up @@ -319,7 +307,7 @@ jobs:
final:
name: Post-CI job
if: github.repository == 'leanprover-community/mathlib4'
needs: [style_lint, build, check_imported]
needs: [style_lint, build]
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
Expand Down
28 changes: 8 additions & 20 deletions .github/workflows/build.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -71,24 +71,6 @@ jobs:
run: |
./scripts/lint-bib.sh
check_imported:
if: github.repository == 'leanprover-community/mathlib4'
name: Check all files imported
runs-on: ubuntu-latest
steps:
- name: cleanup
run: |
find . -name . -o -prune -exec rm -rf -- {} +
- uses: actions/checkout@v4

- name: update import-only files in {Mathlib Mathlib/Tactic Counterexamples Archive}.lean
run: |
./scripts/mk_all.sh
- name: check that all files are imported
run: git diff --exit-code

check_workflows:
if: github.repository == 'leanprover-community/mathlib4'
name: check workflows
Expand Down Expand Up @@ -159,7 +141,7 @@ jobs:
# but verify that this didn't change anything in the `check_imported` job.
- name: update Mathlib.lean
run: |
./scripts/mk_all.sh Mathlib
lake exe mk_all --lib Mathlib
- name: If using a lean-pr-release toolchain, uninstall
run: |
Expand All @@ -173,6 +155,12 @@ jobs:
lean --version
lake --version
- name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
run: lake exe mk_all

- name: check_imported
run: git diff --exit-code

- name: build cache
run: |
lake build cache
Expand Down Expand Up @@ -326,7 +314,7 @@ jobs:
final:
name: Post-CI job
if: github.repository == 'leanprover-community/mathlib4'
needs: [style_lint, build, check_imported]
needs: [style_lint, build]
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
Expand Down
28 changes: 8 additions & 20 deletions .github/workflows/build.yml.in
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,24 +50,6 @@ jobs:
run: |
./scripts/lint-bib.sh

check_imported:
if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
name: Check all files importedJOB_NAME
runs-on: ubuntu-latest
steps:
- name: cleanup
run: |
find . -name . -o -prune -exec rm -rf -- {} +

- uses: actions/checkout@v4

- name: update import-only files in {Mathlib Mathlib/Tactic Counterexamples Archive}.lean
run: |
./scripts/mk_all.sh

- name: check that all files are imported
run: git diff --exit-code

check_workflows:
if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
name: check workflowsJOB_NAME
Expand Down Expand Up @@ -138,7 +120,7 @@ jobs:
# but verify that this didn't change anything in the `check_imported` job.
- name: update Mathlib.lean
run: |
./scripts/mk_all.sh Mathlib
lake exe mk_all --lib Mathlib

- name: If using a lean-pr-release toolchain, uninstall
run: |
Expand All @@ -152,6 +134,12 @@ jobs:
lean --version
lake --version

- name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
run: lake exe mk_all

- name: check_imported
run: git diff --exit-code

- name: build cache
run: |
lake build cache
Expand Down Expand Up @@ -305,7 +293,7 @@ jobs:
final:
name: Post-CI jobJOB_NAME
if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
needs: [style_lint, build, check_imported]
needs: [style_lint, build]
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
Expand Down
28 changes: 8 additions & 20 deletions .github/workflows/build_fork.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -68,24 +68,6 @@ jobs:
run: |
./scripts/lint-bib.sh
check_imported:
if: github.repository != 'leanprover-community/mathlib4'
name: Check all files imported (fork)
runs-on: ubuntu-latest
steps:
- name: cleanup
run: |
find . -name . -o -prune -exec rm -rf -- {} +
- uses: actions/checkout@v4

- name: update import-only files in {Mathlib Mathlib/Tactic Counterexamples Archive}.lean
run: |
./scripts/mk_all.sh
- name: check that all files are imported
run: git diff --exit-code

check_workflows:
if: github.repository != 'leanprover-community/mathlib4'
name: check workflows (fork)
Expand Down Expand Up @@ -156,7 +138,7 @@ jobs:
# but verify that this didn't change anything in the `check_imported` job.
- name: update Mathlib.lean
run: |
./scripts/mk_all.sh Mathlib
lake exe mk_all --lib Mathlib
- name: If using a lean-pr-release toolchain, uninstall
run: |
Expand All @@ -170,6 +152,12 @@ jobs:
lean --version
lake --version
- name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why did this move? I presume when this was a tactic, you needed mathlib to be built - is this still the case now? I would think this script could build independently of mathlib.

(Same question for the other three copies.)

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

To update my question: this didn't move, this got added - is this intentional or a merge mishap?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ok, that's weird. There should be a CI step that recreates Mathlib, Tactic, Counterexamples and Archive: this is used to make sure that they get built and work.

This step was not introduced in this PR, but should be already present in regular CI. This PR should simply shift to using lake exe mk_all for this, instead of the bash script.

Besides this, it is true that regular CI builds Mathlib once before this step. I suspect that this is the step that was present before Archive and Counterexamples were added to be able to cache their oleans. It is possible that there could be a single step that updates these "import all" files, but I would not investigate this here.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@grunweg is this now considered "resolved" at least as far as this PR is concerned?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, it is: the check if all imports are present (for mathlib, archive, counterexamples and Mathlib/Tactic) is removed as a separate workflow step, but is now part of the build workflow (and runs before getting the cache or building mathlib). So, users still get early feedback, just via a different channel.

run: lake exe mk_all

- name: check_imported
run: git diff --exit-code

- name: build cache
run: |
lake build cache
Expand Down Expand Up @@ -323,7 +311,7 @@ jobs:
final:
name: Post-CI job (fork)
if: github.repository != 'leanprover-community/mathlib4'
needs: [style_lint, build, check_imported]
needs: [style_lint, build]
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
Expand Down
Loading