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

wants to merge 48 commits into from

Conversation

adomani
Copy link
Collaborator

@adomani adomani commented Apr 3, 2024 •
edited by YaelDillies
Loading

This PR replaces the shell commands for importing all the mathlib libraries by a lean executable defined in #11853.

Open in Gitpod

@adomani adomani changed the title feat: mk_all script implemented in Lean feat: lake exe mkAll in CI Apr 3, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 2, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 7, 2024
mathlib-bors bot pushed a commit that referenced this pull request May 29, 2024
@adomani @YaelDillies
feat: lake exe mk_all as a Lean executable (#11853)
1ea200b 
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 <yael.dillies@gmail.com>
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label May 29, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

This PR/issue depends on:

@jcommelin
Copy link
Member

bors d=grunweg

@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented May 31, 2024

✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@grunweg
Copy link
Collaborator

grunweg commented May 31, 2024

bors r+

mathlib-bors bot pushed a commit that referenced this pull request May 31, 2024
@adomani @YaelDillies
feat: lake exe mk_all in CI (#11874)
c9c411c 
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 <yael.dillies@gmail.com>
@Ruben-VandeVelde
Copy link
Collaborator

Trying to see if I can wake up bors...

@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented May 31, 2024

Timed out.

@bryangingechen
Copy link
Contributor

On the bors status page for the failed run, it says:

Date: 5/31/2024, 7:30:08 PM

Priority: 0

State: Failed

Status:

Build (Succeeded)
Check all files imported (Running)
Lint style (Succeeded)

Pull Requests:

#11874

Since that step was deleted in this PR, I think you need to also delete it from bors.toml:

mathlib4/bors.toml

Line 1 in daa801e

status = ["Build", "Lint style", "Check all files imported"]

@bryangingechen
Copy link
Contributor

bors r+

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Jun 1, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jun 1, 2024
@adomani @grunweg @YaelDillies
feat: lake exe mk_all in CI (#11874)
db4dcf5 
This PR replaces the shell commands for importing all the mathlib libraries by a lean executable defined in #11853.



Co-authored-by: Michael Rothgang <rothgami@math.hu-berlin.de>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jun 1, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: lake exe mk_all in CI [Merged by Bors] - feat: lake exe mk_all in CI Jun 1, 2024
@mathlib-bors mathlib-bors bot closed this Jun 1, 2024
@mathlib-bors mathlib-bors bot deleted the yad/mkAll_in_CI branch June 1, 2024 12:46
callesonne pushed a commit that referenced this pull request Jun 4, 2024
@adomani @YaelDillies @callesonne
feat: lake exe mk_all as a Lean executable (#11853)
9619ab7 
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 <yael.dillies@gmail.com>
callesonne pushed a commit that referenced this pull request Jun 4, 2024
@adomani @grunweg
@YaelDillies @callesonne
feat: lake exe mk_all in CI (#11874)
b6e3d84 
This PR replaces the shell commands for importing all the mathlib libraries by a lean executable defined in #11853.



Co-authored-by: Michael Rothgang <rothgami@math.hu-berlin.de>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@grunweg grunweg mentioned this pull request Jun 7, 2024
Closed
grunweg added a commit that referenced this pull request Jun 7, 2024
@adomani @grunweg @YaelDillies
feat: lake exe mk_all in CI (#11874)
c6c28c0 
This PR replaces the shell commands for importing all the mathlib libraries by a lean executable defined in #11853.



Co-authored-by: Michael Rothgang <rothgami@math.hu-berlin.de>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
js2357 pushed a commit that referenced this pull request Jun 18, 2024
@adomani @YaelDillies @js2357
feat: lake exe mk_all as a Lean executable (#11853)
2cc04ad 
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 <yael.dillies@gmail.com>
AntoineChambert-Loir pushed a commit that referenced this pull request Jun 20, 2024
@adomani @grunweg
@YaelDillies @AntoineChambert-Loir
feat: lake exe mk_all in CI (#11874)
905c3f0 
This PR replaces the shell commands for importing all the mathlib libraries by a lean executable defined in #11853.



Co-authored-by: Michael Rothgang <rothgami@math.hu-berlin.de>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@grunweg grunweg grunweg left review comments

@jcommelin jcommelin jcommelin left review comments

Assignees
No one assigned
Labels
CI Modifies the continuous integration / deployment setup delegated maintainer-merge ready-to-merge This PR has been sent to bors. t-meta Tactics, attributes or user commands
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
7 participants
@adomani @grunweg @leanprover-community-mathlib4-bot @jcommelin @Ruben-VandeVelde @bryangingechen @YaelDillies