Skip to content

[Merged by Bors] - feat: port Control.Traversable.Basic#788

Closed
kbuzzard wants to merge 53 commits intomasterfrom
kbuzzard-port-control-traversable-basic
Closed

[Merged by Bors] - feat: port Control.Traversable.Basic#788
kbuzzard wants to merge 53 commits intomasterfrom
kbuzzard-port-control-traversable-basic

Conversation

@kbuzzard
Copy link
Copy Markdown
Member

@kbuzzard kbuzzard commented Nov 29, 2022 •
edited
Loading

thing copied from mathlib3port: 1fc36cc9c8264e6e81253f88be7fb2cb6c92d76a

@kim-em kim-em added the WIP Work in progress label Nov 29, 2022
@kbuzzard
Copy link
Copy Markdown
Member Author

kbuzzard commented Nov 30, 2022 •
edited
Loading

OK so this is compiling but needs one declaration from Data.List.Defs which is being ported in #803 (it's only compiling because I copied the declaration into this file; this should really be deleted).

The only other issue is the dubious translation error for Sum.traverse. The error is

/- warning: sum.traverse -> Sum.traverse is a dubious translation:
lean 3 declaration is
  forall {σ : Type.{u}} {F : Type.{u} -> Type.{u}} [_inst_1 : Applicative.{u u} F] {α : Type.{u_1}} {β : Type.{u}}, (α -> (F β)) -> (Sum.{u u_1} σ α) -> (F (Sum.{u u} σ β))
but is expected to have type
  forall {σ : Type.{u}} {F : Type.{u} -> Type.{u}} [_inst_1 : Applicative.{u u} F] {α : Type.{_aux_param_0}} {β : Type.{u}}, (α -> (F β)) -> (Sum.{u _aux_param_0} σ α) -> (F (Sum.{u u} σ β))
Case conversion may be inaccurate. Consider using '#align sum.traverse Sum.traverseₓ'. -/

There's also a similar dubious translation error for List.traverse in data.list.defs . Discussion here.

If there is a big rush for this file then it can be merged as is with the traverse def in the wrong place and then fixed later (although ideally we'll understand the dubious translation error, e.g. by someone assuring us that it's a bug)

@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Nov 30, 2022

I think no rush; the Control files are not really used much. :-)

@kbuzzard
Copy link
Copy Markdown
Member Author

kbuzzard commented Nov 30, 2022

@semorrison I ported the file because the port-status script was telling me about two days ago that it was the most important file to be ported right now :-)

@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Nov 30, 2022

Yes, in mathlib3 these files are all imported very early, but then not used much.

@hrmacbeth hrmacbeth added the mathlib-port This is a port of a theory file from mathlib. label Dec 1, 2022
@Ruben-VandeVelde Ruben-VandeVelde added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Dec 1, 2022
@kbuzzard
Copy link
Copy Markdown
Member Author

kbuzzard commented Dec 3, 2022

OK; the status of this PR now is that we're waiting on #803 and I'm still a little confused about a possible dubious translation which could well not be dubious; I've asked here.

@kbuzzard kbuzzard added awaiting-review and removed WIP Work in progress labels Dec 3, 2022
@kbuzzard
Copy link
Copy Markdown
Member Author

kbuzzard commented Dec 3, 2022 •
edited
Loading

Re the possibly dubious translation: I've explicitly checked the declarations in mathlib3 and mathlib4 and they're exactly the same including universes and even universe order, so I think this PR is ready to go when #803 is merged.

@kim-em kim-em removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Dec 6, 2022
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Dec 6, 2022

This PR/issue depends on:

@kim-em kim-em added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 6, 2022
@kim-em kim-em removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 6, 2022
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Dec 7, 2022

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Dec 7, 2022
bors bot pushed a commit that referenced this pull request Dec 7, 2022
@kbuzzard @arienmalec @Ruben-VandeVelde
feat: port Control.Traversable.Basic (#788)
d95a165 
thing copied from mathlib3port: 1fc36cc9c8264e6e81253f88be7fb2cb6c92d76a

- [x] Depends on: #803 (for `list.traverse`)

Co-authored-by: Arien Malec <arien.malec@gmail.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: arienmalec <arien.malec@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Dec 7, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port Control.Traversable.Basic [Merged by Bors] - feat: port Control.Traversable.Basic Dec 7, 2022
@bors bors bot closed this Dec 7, 2022
@bors bors bot deleted the kbuzzard-port-control-traversable-basic branch December 7, 2022 03:49
@github-actions github-actions bot mentioned this pull request Dec 8, 2022
Closed
bors bot pushed a commit to leanprover-community/mathlib3 that referenced this pull request Dec 8, 2022
chore(*): add mathlib4 synchronization comments (#17849)
1f93c64 
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following PRs:
* `algebra.euclidean_domain.defs`: leanprover-community/mathlib4#871
* `algebra.group.ext`: leanprover-community/mathlib4#850
* `algebra.group_power.basic`: leanprover-community/mathlib4#874
* `algebra.hom.equiv.units.basic`: leanprover-community/mathlib4#895
* `algebra.hom.equiv.units.group_with_zero`: leanprover-community/mathlib4#901
* `algebra.order.group.instances`: leanprover-community/mathlib4#890
* `algebra.order.group.order_iso`: leanprover-community/mathlib4#895
* `algebra.order.group.units`: leanprover-community/mathlib4#898
* `algebra.order.monoid.nat_cast`: leanprover-community/mathlib4#893
* `algebra.order.monoid.type_tags`: leanprover-community/mathlib4#873
* `algebra.order.monoid.units`: leanprover-community/mathlib4#873
* `algebra.order.zero_le_one`: leanprover-community/mathlib4#893
* `combinatorics.quiver.push`: leanprover-community/mathlib4#868
* `control.traversable.basic`: leanprover-community/mathlib4#788
* `data.sum.order`: leanprover-community/mathlib4#880
* `group_theory.group_action.option`: leanprover-community/mathlib4#884
* `group_theory.group_action.sigma`: leanprover-community/mathlib4#885
* `group_theory.group_action.sum`: leanprover-community/mathlib4#882
* `group_theory.group_action.units`: leanprover-community/mathlib4#878
* `order.antisymmetrization`: leanprover-community/mathlib4#876
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

mathlib-port This is a port of a theory file from mathlib. ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@kbuzzard @kim-em @hrmacbeth @Ruben-VandeVelde @arienmalec