Skip to content

lean 3.49.0#115498

Closed
tchajed wants to merge 1 commit intoHomebrew:masterfrom
tchajed:bump-lean-3.49.0
Closed

lean 3.49.0#115498
tchajed wants to merge 1 commit intoHomebrew:masterfrom
tchajed:bump-lean-3.49.0

Conversation

@tchajed
Copy link
Copy Markdown
Contributor

@tchajed tchajed commented Nov 11, 2022

Created with brew bump-formula-pr.

@BrewTestBot BrewTestBot added the bump-formula-pr PR was created using `brew bump-formula-pr` label Nov 11, 2022
@tchajed tchajed mentioned this pull request Nov 11, 2022
Closed
@tchajed
Copy link
Copy Markdown
Contributor Author

tchajed commented Nov 11, 2022

It looks like mathlib doesn't have a 3.49.0 branch. It actually doesn't seem to be compatible, so I opened leanprover-community/mathlib3#17486.

@chenrui333
Copy link
Copy Markdown
Member

chenrui333 commented Nov 11, 2022

It looks like mathlib doesn't have a 3.49.0 branch. It actually doesn't seem to be compatible, so I opened leanprover-community/mathlib#17486.

yeah, they always released mathlib a couple of days later

@chenrui333
Copy link
Copy Markdown
Member

chenrui333 commented Nov 11, 2022

This is my previous issue on the similar matter, leanprover-community/mathlib3#14234

@github-actions
Copy link
Copy Markdown
Contributor

github-actions bot commented Nov 13, 2022

This pull request has been automatically marked as stale because it has not had recent activity. It will be closed if no further activity occurs. To keep this pull request open, add a help wanted or in progress label.

@github-actions github-actions bot added the stale No recent activity label Nov 13, 2022
@github-actions github-actions bot closed this Nov 15, 2022
@tchajed
Copy link
Copy Markdown
Contributor Author

tchajed commented Nov 15, 2022

This PR should now work, since mathlib created a lean-3.49.0 branch.

@chenrui333 chenrui333 reopened this Nov 16, 2022
@chenrui333 chenrui333 added ready to merge PR can be merged once CI is green and removed stale No recent activity labels Nov 16, 2022
@chenrui333
Copy link
Copy Markdown
Member

chenrui333 commented Nov 16, 2022

This should be marked in progress in the first place 😄

@chenrui333
Copy link
Copy Markdown
Member

chenrui333 commented Nov 16, 2022

Gonna do a rerun before the approval/merge

@BrewTestBot
Copy link
Copy Markdown
Contributor

BrewTestBot commented Nov 17, 2022

🤖 A scheduled task has triggered a merge.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@chenrui333 chenrui333 chenrui333 approved these changes

Assignees

No one assigned

Labels

bump-formula-pr PR was created using `brew bump-formula-pr` ready to merge PR can be merged once CI is green

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@tchajed @chenrui333 @BrewTestBot