Skip to content

chore: update Mathlib dependencies 2024-08-31#16360

Closed
ghost wants to merge 0 commit intomasterfrom
update-dependencies-bot-use-only
Closed

chore: update Mathlib dependencies 2024-08-31#16360
ghost wants to merge 0 commit intomasterfrom
update-dependencies-bot-use-only

Conversation

@ghost
Copy link
Copy Markdown

@ghost ghost commented Aug 31, 2024

This PR updates the Mathlib dependencies.

@ghost ghost added the auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. label Aug 31, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 31, 2024 •
edited
Loading

PR summary bc55704c36

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

@ghost ghost force-pushed the update-dependencies-bot-use-only branch from 9ce1896 to bc55704 Compare August 31, 2024 14:05
@ghost
Copy link
Copy Markdown
Author

ghost commented Aug 31, 2024

As this PR is labelled auto-merge-after-CI, we are now sending it to bors:

bors merge

mathlib-bors bot added a commit that referenced this pull request Aug 31, 2024
@mathlib-bors
chore: update Mathlib dependencies 2024-08-31 (#16360)
6f6f8ab 
This PR updates the Mathlib dependencies.
@bryangingechen
Copy link
Copy Markdown
Contributor

bryangingechen commented Aug 31, 2024

bors r-
Something is wrong here, it's trying to push elan-init to the branch.

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 31, 2024

Canceled.

@bryangingechen bryangingechen added awaiting-author A reviewer has asked the author a question or requested changes. and removed auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. labels Aug 31, 2024
@bryangingechen bryangingechen mentioned this pull request Aug 31, 2024
Closed
mathlib-bors bot pushed a commit that referenced this pull request Aug 31, 2024
@bryangingechen
fix(update_dependencies.yml): restore order of install elan and check…
816c3ce 
…out repo (#16366)

In #16335, I swapped the order of checking out the repo and installing `elan`. That seems to have caused the bot to try to push `elan-init` to `master` in #16360. I've reverted that here.
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
@bryangingechen @bjoernkjoshanssen
fix(update_dependencies.yml): restore order of install elan and check…
d580edb 
…out repo (#16366)

In #16335, I swapped the order of checking out the repo and installing `elan`. That seems to have caused the bot to try to push `elan-init` to `master` in #16360. I've reverted that here.
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
@bryangingechen @bjoernkjoshanssen
fix(update_dependencies.yml): restore order of install elan and check…
205b1ec 
…out repo (#16366)

In #16335, I swapped the order of checking out the repo and installing `elan`. That seems to have caused the bot to try to push `elan-init` to `master` in #16360. I've reverted that here.
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 12, 2024
@bryangingechen @bjoernkjoshanssen
fix(update_dependencies.yml): restore order of install elan and check…
ab8bbce 
…out repo (#16366)

In #16335, I swapped the order of checking out the repo and installing `elan`. That seems to have caused the bot to try to push `elan-init` to `master` in #16360. I've reverted that here.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

awaiting-author A reviewer has asked the author a question or requested changes.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@bryangingechen @leanprover-community-bot-assistant