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] - chore(*): bump to Lean 3.18.4 #3610

Closed
wants to merge 42 commits into from
Closed

[Merged by Bors] - chore(*): bump to Lean 3.18.4 #3610

wants to merge 42 commits into from

Conversation

robertylewis
Copy link
Member

@robertylewis robertylewis commented Jul 28, 2020 •
edited by urkud
Loading

  • Remove pi_arity and the vm_override for by_cases, which have moved to core
  • Fix fallout from the change to the definition of max
  • Fix a small number of errors caused by changes to instance caching
  • Remove min_add, which is generalized by min_add_add_right and make to_additive generate some lemmas

Let's see what breaks!

@robertylewis
Copy link
Member Author

Huh, what's up with the CI failure on the olean cache stage?

@gebner
Copy link
Member

gebner commented Jul 28, 2020

Huh, what's up with the CI failure on the olean cache stage?

I think that's just a race condition where we fetched the cache at the same moment it was being uploaded.

@gebner
Copy link
Member

gebner commented Jul 28, 2020

leanprover-community/lean#411 😭

@robertylewis
Copy link
Member Author

Should we hold off on this upgrade until 3.18.1 then?

@robertylewis robertylewis added the WIP Work in progress label Jul 28, 2020
@gebner gebner changed the title chore(*): bump to Lean 3.18.0 chore(*): bump to Lean 3.18.1 Jul 28, 2020
@robertylewis robertylewis changed the title chore(*): bump to Lean 3.18.1 chore(*): bump to Lean 3.18.2 Jul 28, 2020
@robertylewis
Copy link
Member Author

Hmm. It's still failing on what looks like an innocent {(a : A)} example.

@gebner
Copy link
Member

gebner commented Jul 28, 2020

😞 leanprover-community/lean#419 leanprover-community/lean#418

@gebner gebner changed the title chore(*): bump to Lean 3.18.3 chore(*): bump to Lean 3.18.4 Jul 30, 2020
@gebner
Copy link
Member

gebner commented Jul 30, 2020

@urkud I think you know better what needs to be changed with max.

@urkud
Copy link
Member

urkud commented Jul 31, 2020

I can fix the rest of max-related bugs tonight.

@urkud urkud mentioned this pull request Aug 1, 2020
Closed
@TwoFX
Copy link
Member

TwoFX commented Aug 1, 2020

I had a look at the test failure in interval_cases.lean. The problem was that the change to max made the test trigger #3655. The change I made to interval_cases makes the test not trigger the bug any more, but does not actually fix it.

@bryangingechen
Copy link
Collaborator

Hooray, it builds (locally)! I'd still like to see a summary of required changes in the commit message before merging.

@TwoFX
Copy link
Member

TwoFX commented Aug 1, 2020

I'd still like to see a summary of required changes in the commit message before merging.

@bryangingechen I have written a short commit message.

@urkud
Copy link
Member

urkud commented Aug 1, 2020

LGTM

@urkud urkud added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels Aug 1, 2020
bryangingechen
bryangingechen approved these changes Aug 1, 2020
View reviewed changes
Copy link
Collaborator

@bryangingechen bryangingechen left a comment

Choose a reason for hiding this comment

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

LGTM as well (but I made the last commit, so I won't merge).

@urkud
Copy link
Member

urkud commented Aug 1, 2020

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Aug 1, 2020
bors bot pushed a commit that referenced this pull request Aug 1, 2020
@robertylewis @gebner
chore(*): bump to Lean 3.18.4 (#3610)
4274ddd 
* Remove `pi_arity` and the `vm_override` for `by_cases`, which have moved to core
* Fix fallout from the change to the definition of `max`
* Fix a small number of errors caused by changes to instance caching
* Remove `min_add`, which is generalized by `min_add_add_right`  and make `to_additive` generate some lemmas



Co-authored-by: Gabriel Ebner <gebner@gebner.org>
Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
@bors
Copy link

bors bot commented Aug 1, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore(*): bump to Lean 3.18.4 [Merged by Bors] - chore(*): bump to Lean 3.18.4 Aug 1, 2020
@bors bors bot closed this Aug 1, 2020
@bors bors bot deleted the robertylewis-patch-1 branch August 1, 2020 22:31
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@gebner gebner gebner left review comments

@jcommelin jcommelin jcommelin left review comments

@bryangingechen bryangingechen bryangingechen approved these changes

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
6 participants
@robertylewis @gebner @jcommelin @bryangingechen @urkud @TwoFX