-
Notifications
You must be signed in to change notification settings - Fork 331
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.
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
[Merged by Bors] - feat: lake exe mk_all
in CI
#11874
Conversation
lake exe mkAll
in CI
Running ```bash lake exe mk_all --git ``` should have the same effect as running ```bash ./script/mk_all.sh ``` that is, it creates the files `Mathlib.lean`, `Mathlib/Tactic.lean`, `Archive.lean`, `Counterexamples.lean`. It does *not* create analogous files for `Cache` and `LongestPole`. ```bash lake exe mk_all ``` is similar, but uses all the `.lean` files in `Mathlib`, not just the Git-managed ones. See #11874 for using the script in CI. Co-authored-by: Yaël Dillies <[email protected]>
This PR/issue depends on:
|
bors d=grunweg |
✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
This PR replaces the shell commands for importing all the mathlib libraries by a lean executable defined in #11853. Co-authored-by: Yaël Dillies <[email protected]>
Trying to see if I can wake up bors... |
Timed out. |
On the bors status page for the failed run, it says:
Since that step was deleted in this PR, I think you need to also delete it from bors.toml: Line 1 in daa801e
|
bors r+ |
This PR replaces the shell commands for importing all the mathlib libraries by a lean executable defined in #11853. Co-authored-by: Michael Rothgang <[email protected]> Co-authored-by: Yaël Dillies <[email protected]>
Pull request successfully merged into master. Build succeeded: |
lake exe mk_all
in CIlake exe mk_all
in CI
Running ```bash lake exe mk_all --git ``` should have the same effect as running ```bash ./script/mk_all.sh ``` that is, it creates the files `Mathlib.lean`, `Mathlib/Tactic.lean`, `Archive.lean`, `Counterexamples.lean`. It does *not* create analogous files for `Cache` and `LongestPole`. ```bash lake exe mk_all ``` is similar, but uses all the `.lean` files in `Mathlib`, not just the Git-managed ones. See #11874 for using the script in CI. Co-authored-by: Yaël Dillies <[email protected]>
This PR replaces the shell commands for importing all the mathlib libraries by a lean executable defined in #11853. Co-authored-by: Michael Rothgang <[email protected]> Co-authored-by: Yaël Dillies <[email protected]>
This PR replaces the shell commands for importing all the mathlib libraries by a lean executable defined in #11853. Co-authored-by: Michael Rothgang <[email protected]> Co-authored-by: Yaël Dillies <[email protected]>
Running ```bash lake exe mk_all --git ``` should have the same effect as running ```bash ./script/mk_all.sh ``` that is, it creates the files `Mathlib.lean`, `Mathlib/Tactic.lean`, `Archive.lean`, `Counterexamples.lean`. It does *not* create analogous files for `Cache` and `LongestPole`. ```bash lake exe mk_all ``` is similar, but uses all the `.lean` files in `Mathlib`, not just the Git-managed ones. See #11874 for using the script in CI. Co-authored-by: Yaël Dillies <[email protected]>
This PR replaces the shell commands for importing all the mathlib libraries by a lean executable defined in #11853. Co-authored-by: Michael Rothgang <[email protected]> Co-authored-by: Yaël Dillies <[email protected]>
This PR replaces the shell commands for importing all the mathlib libraries by a lean executable defined in #11853.
lake exe mk_all
as a Lean executable #11853