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] - feat: port Data.Typevec #891

Closed
wants to merge 36 commits into from
Closed

[Merged by Bors] - feat: port Data.Typevec #891

wants to merge 36 commits into from

Conversation

j-loreaux
Copy link
Collaborator

mathlib3 SHA: 39af7d3bf61a98e928812dbc3e16f4ea8b795ca3

porting notes: currently this is full of major issues. Help welcome

@semorrison semorrison added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Dec 7, 2022
@Ruben-VandeVelde Ruben-VandeVelde added help-wanted The author needs attention to resolve issues awaiting-author A reviewer has asked the author a question or requested changes mathlib-port This is a port of a theory file from mathlib. and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. labels Dec 7, 2022
@alexkeizer
Copy link
Collaborator

alexkeizer commented Dec 13, 2022 •
edited

I actually have a manual port of this (and a bunch of other QPF-related mathlib) files at https://github.com/alexkeizer/qpf4. It's fairly messy, since it also contains a lot of new developments, but it should serve as a good basis for porting efforts!

I'm currently in the progress of updating my version to be compatible with the latest mathlib4, then I'll have a look at seeing if I can transplant just the parts needed for a direct port.

@semorrison semorrison added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Dec 13, 2022
@semorrison semorrison removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Dec 13, 2022
@alexkeizer alexkeizer added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jan 13, 2023
jcommelin
jcommelin reviewed Jan 13, 2023
View reviewed changes
Mathlib/Data/TypeVec.lean Outdated Show resolved Hide resolved
Mathlib/Data/TypeVec.lean Outdated Show resolved Hide resolved
Mathlib/Data/TypeVec.lean Outdated Show resolved Hide resolved
Mathlib/Data/TypeVec.lean Outdated Show resolved Hide resolved
@alexkeizer alexkeizer self-assigned this Jan 13, 2023
@alexkeizer
Fix naming of
2edb69c 
TypevecCasesNil and TypevecCasesCons in subsequent theorems
@jcommelin
Copy link
Member

One more comment. Otherwise, LGTM.

bors d+

@bors
Copy link

bors bot commented Jan 13, 2023

✌️ j-loreaux can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@github-actions github-actions bot added delegated and removed awaiting-review The author would like community review of the PR labels Jan 13, 2023
@alexkeizer @jcommelin
Fix porting note for typevec simp attr
edd3ab2 
Co-authored-by: Johan Commelin <johan@commelin.net>
@alexkeizer alexkeizer removed the request for review from semorrison January 13, 2023 19:07
@alexkeizer
Copy link
Collaborator

alexkeizer commented Jan 13, 2023 •
edited

One more comment. Otherwise, LGTM.

bors d+

Could you delegate it to me (I adopted this PR, but am not the original author), or just go ahead and merge it!
Or is it customary that the original PR author gets the final say?

EDIT: @j-loreaux: could you approve and merge this PR?

@jcommelin
Copy link
Member

bors d=alexkeizer

@bors
Copy link

bors bot commented Jan 17, 2023

✌️ alexkeizer can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@alexkeizer
Copy link
Collaborator

bors r+

bors bot pushed a commit that referenced this pull request Jan 17, 2023
@j-loreaux @mcdoll
@Ruben-VandeVelde @alexkeizer @semorrison
feat: port Data.Typevec (#891)
80eb126 
mathlib3 SHA: 39af7d3bf61a98e928812dbc3e16f4ea8b795ca3

porting notes: currently this is full of major issues. Help welcome

Co-authored-by: Moritz Doll <moritz.doll@googlemail.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Alex Keizer <alex@keizer.dev>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link

bors bot commented Jan 17, 2023

Build failed:

  • Build

@alexkeizer
Copy link
Collaborator

bors merge

bors bot pushed a commit that referenced this pull request Jan 17, 2023
@j-loreaux @mcdoll
@Ruben-VandeVelde @alexkeizer @semorrison
feat: port Data.Typevec (#891)
9e50514 
mathlib3 SHA: 39af7d3bf61a98e928812dbc3e16f4ea8b795ca3

porting notes: currently this is full of major issues. Help welcome

Co-authored-by: Moritz Doll <moritz.doll@googlemail.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Alex Keizer <alex@keizer.dev>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link

bors bot commented Jan 17, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port Data.Typevec [Merged by Bors] - feat: port Data.Typevec Jan 17, 2023
@bors bors bot closed this Jan 17, 2023
@bors bors bot deleted the j-loreaux/data.typevec branch January 17, 2023 19:27
jcommelin pushed a commit that referenced this pull request Jan 23, 2023
@j-loreaux @mcdoll
@Ruben-VandeVelde @alexkeizer @semorrison @jcommelin
feat: port Data.Typevec (#891)
60742eb 
mathlib3 SHA: 39af7d3bf61a98e928812dbc3e16f4ea8b795ca3

porting notes: currently this is full of major issues. Help welcome

Co-authored-by: Moritz Doll <moritz.doll@googlemail.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Alex Keizer <alex@keizer.dev>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@semorrison semorrison semorrison left review comments

@jcommelin jcommelin jcommelin left review comments

@alexkeizer alexkeizer alexkeizer left review comments

Assignees

@alexkeizer alexkeizer

Labels
delegated mathlib-port This is a port of a theory file from mathlib.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
7 participants
@j-loreaux @alexkeizer @jcommelin @semorrison @rwbarton @Ruben-VandeVelde @mcdoll