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.34.0 #9824

Closed
wants to merge 129 commits into from
Closed

[Merged by Bors] - chore(*): bump to lean 3.34.0 #9824

wants to merge 129 commits into from

Conversation

semorrison
Copy link
Collaborator

@semorrison semorrison commented Oct 20, 2021 •
edited by urkud

Backport coercions from Lean 4

Now has_coe_to_fun and has_coe_to_sort take the output type as an out_param argument. This change comes with some changes in the elaboration order, so some proofs/definitions need more type annotations.

Smarter by_contra

Now by_contra h does better job if the goal is a negation.

open and current namespace

In

namespace A
open B _root_.C
end A

Lean will try to open A.B; if this fails, it will open B. It will also open C.
setup_tactic_parser_cmd command was updated to open appropriate _root_.* namespaces.

Open in Gitpod

urkud and others added 30 commits March 25, 2021 16:33
@urkud
Snapshot
8db6608
@urkud
Switch to a new tag
346a2e2
@urkud
Merge branch 'master' into coe-fn-backport
a0326d8
@urkud
migrate more
7bfde98
@urkud
Fix simps
da0284f
@urkud
Fix here and there
e45c8fc
@urkud
Fix
7ba9c9e
@urkud
Snapshot
9d9daee
@urkud
Merge branch 'master' into coe-fn-backport
c4af640
@urkud
...
3b84220
@b-mehta
try fix elementwise
15c2a6d
@b-mehta
fix more?
5ae5ef4
@b-mehta
fix more
2cbd529
@urkud
Fix more
b584b10
@urkud
Fix
1459c7a
@urkud
Fix
2ff65b1
@urkud
Fix
2fbc072
@urkud
Fix
2dd2c14
@urkud
Fix
c96d47c
@urkud
Fix
07d3c49
@urkud
Fix
b05bfaf
@urkud
Fix
18f569f
@urkud
Fix
dc0ef1a
@urkud
Fix
3788dda
@urkud
Fix
d381cad
@urkud
Fix some tests
9e5bb36
@urkud
Update lean
2088ac1
@urkud
Merge branch 'master' into coe-fn-backport
1db6830 
# Conflicts:
#	leanpkg.toml
#	src/algebra/category/Group/basic.lean
#	src/algebra/category/Mon/basic.lean
#	src/algebra/category/Semigroup/basic.lean
#	src/algebra/group/hom.lean
#	src/algebra/group_action_hom.lean
#	src/analysis/analytic/basic.lean
#	src/analysis/normed_space/dual.lean
#	src/analysis/normed_space/enorm.lean
#	src/analysis/normed_space/linear_isometry.lean
#	src/computability/partrec_code.lean
#	src/data/equiv/basic.lean
#	src/data/equiv/mul_add.lean
#	src/data/mv_polynomial/equiv.lean
#	src/data/nat/prime.lean
#	src/data/polynomial/basic.lean
#	src/field_theory/polynomial_galois_group.lean
#	src/geometry/manifold/bump_function.lean
#	src/group_theory/order_of_element.lean
#	src/linear_algebra/affine_space/affine_equiv.lean
#	src/linear_algebra/alternating.lean
#	src/linear_algebra/quadratic_form.lean
#	src/linear_algebra/special_linear_group.lean
#	src/logic/embedding.lean
#	src/measure_theory/integral/bochner.lean
#	src/measure_theory/measure/measure_space.lean
#	src/order/closure.lean
#	src/ring_theory/derivation.lean
#	src/ring_theory/fractional_ideal.lean
#	src/set_theory/pgame.lean
#	src/set_theory/zfc.lean
#	src/tactic/elementwise.lean
#	src/tactic/simps.lean
#	src/topology/category/CompHaus.lean
#	src/topology/category/Profinite.lean
#	src/topology/category/Top/open_nhds.lean
#	src/topology/category/Top/opens.lean
#	src/topology/metric_space/gromov_hausdorff.lean
#	src/topology/path_connected.lean
#	src/topology/topological_fiber_bundle.lean
#	src/topology/vector_bundle.lean
#	test/simps.lean
@urkud
Snapshot
78482c4
@urkud
Merge branch 'master' into coe-fn-backport
255dd48
@semorrison semorrison added awaiting-CI The author would like to see what CI has to say before doing more work. awaiting-review The author would like community review of the PR and removed help-wanted The author needs attention to resolve issues WIP Work in progress labels Oct 21, 2021
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Oct 21, 2021
@urkud
Copy link
Member

urkud commented Oct 21, 2021

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 Oct 21, 2021
bors bot pushed a commit that referenced this pull request Oct 21, 2021
@semorrison @urkud @b-mehta
chore(*): bump to lean 3.34.0 (#9824)
3c11bd7 
### Backport coercions from Lean 4

Now `has_coe_to_fun` and `has_coe_to_sort` take the output type as an `out_param` argument. This change comes with some changes in the elaboration order, so some proofs/definitions need more type annotations.

### Smarter `by_contra`

Now `by_contra h` does better job if the goal is a negation.

### `open` and current namespace

In
```lean
namespace A
open B _root_.C
end A
```
Lean will try to open `A.B`; if this fails, it will open `B`. It will also open `C`.
`setup_tactic_parser_cmd` command was updated to open appropriate `_root_.*` namespaces.



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
@bors
Copy link

bors bot commented Oct 21, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore(*): bump to lean 3.34.0 [Merged by Bors] - chore(*): bump to lean 3.34.0 Oct 21, 2021
@bors bors bot closed this Oct 21, 2021
@bors bors bot deleted the bump-3.34.0 branch October 21, 2021 05:27
@semorrison semorrison mentioned this pull request Oct 21, 2021
Closed
@bryangingechen bryangingechen mentioned this pull request Oct 21, 2021
Closed
1 task
@eric-wieser eric-wieser added the hacktoberfest-accepted Without this label hacktoberfest is scared off by bors label Oct 26, 2021
ericrbg pushed a commit that referenced this pull request Nov 9, 2021
@semorrison @urkud
@b-mehta @ericrbg
chore(*): bump to lean 3.34.0 (#9824)
594520d 
### Backport coercions from Lean 4

Now `has_coe_to_fun` and `has_coe_to_sort` take the output type as an `out_param` argument. This change comes with some changes in the elaboration order, so some proofs/definitions need more type annotations.

### Smarter `by_contra`

Now `by_contra h` does better job if the goal is a negation.

### `open` and current namespace

In
```lean
namespace A
open B _root_.C
end A
```
Lean will try to open `A.B`; if this fails, it will open `B`. It will also open `C`.
`setup_tactic_parser_cmd` command was updated to open appropriate `_root_.*` namespaces.



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@urkud urkud urkud left review comments

Assignees
No one assigned
Labels
hacktoberfest-accepted Without this label hacktoberfest is scared off by bors 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
5 participants
@semorrison @urkud @eric-wieser @b-mehta @Vierkantor