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 LinearAlgebra.Contraction #4124

Closed
wants to merge 48 commits into from
Closed

[Merged by Bors] - feat: port LinearAlgebra.Contraction #4124

wants to merge 48 commits into from

Conversation

mattrobball
Copy link
Collaborator

@mattrobball mattrobball commented May 19, 2023 •
edited by github-actions bot
Loading

urkud and others added 30 commits April 26, 2023 02:06
@urkud
feat: port LinearAlgebra.Dual
276d3bd
@urkud
Initial file copy from mathport
21a61de
@urkud
automated fixes
fa8ed05 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@urkud
Partial fix
2d228ed
@mo271
quick pass
ce5afcd 
drive-by: correct "ő" in Erdős
@Parcly-Taxel
182 errors remain
b704c9a
@Parcly-Taxel
Merge branch 'port/LinearAlgebra.Dual' of github.com:leanprover-commu…
d08869b 
…nity/mathlib4 into port/LinearAlgebra.Dual
@urkud
Add ext
11c4a8e
@kmill
some progress by using conv/rw rather than simp_rw
01b2d0d
@mattrobball
Merge branch 'master' into port/LinearAlgebra.Dual
3d0c4d6
@mattrobball
remove etaExp
498e055
@mattrobball
fix some errors with universes and missing tacs
753ce19
@mattrobball
Merge branch 'master' into port/LinearAlgebra.Dual
cc28e81
@mattrobball
fix some errors
89152ed
@mattrobball
forward port changes
4c3968c
@mattrobball
fix some more
412a9ce
@mattrobball
fix errors on another pass
e70ef65 
and bump heartbeats everyone to have a working file
@mattrobball
fix some more
b868f46
@mattrobball
fix more errors
de852e1 
mainly dealing with timeouts at this point
@mattrobball
initial file from mathport
67f801d
@mattrobball
fix mathlib.lean
ad0f81e
@mattrobball
propagate changes
fc1184f 
timeouts have improved for the most part
@mattrobball
propagate the intro naming
6ef28d4
@mattrobball
fix all but timeouts
b254c25
@mattrobball
remove old file
d1cd5f0
@mattrobball
Merge branch 'master' into port/LinearAlgebra.Dual
5e4a364
@mattrobball
Merge branch 'port/LinearAlgebra.Dual.theReportering' into port/Linea…
5e0844b 
…rAlgebra.Dual
@ChrisHughes24
delete <<<<<HEAD
8e28f19
@ChrisHughes24
undo commenting out CoeFun
f553dad
@ChrisHughes24
fix merge conflict and use FunLike
717c838
@mattrobball mattrobball added mathlib-port This is a port of a theory file from mathlib. help-wanted The author needs attention to resolve issues labels May 19, 2023
@semorrison semorrison added the blocked-by-other-PR This PR depends on another PR to Mathlib label May 19, 2023
@mattrobball
Copy link
Collaborator Author

mattrobball commented May 19, 2023 •
edited
Loading

Things left to do:

  • align names in the comments with #naming4
  • decide the naming convention for left tensor, Ltensor or LTensor, and right tensor
  • diagnose the timeouts in the failing simps

@mattrobball
Copy link
Collaborator Author

I won't be able to touch it for a bit probably.

@mattrobball mattrobball removed the help-wanted The author needs attention to resolve issues label May 20, 2023
@semorrison semorrison added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label May 20, 2023
@semorrison semorrison removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label May 20, 2023
@semorrison semorrison removed the blocked-by-other-PR This PR depends on another PR to Mathlib label May 22, 2023
@semorrison
Copy link
Contributor

This PR/issue depends on:

@mattrobball mattrobball added the awaiting-review The author would like community review of the PR label May 22, 2023
@semorrison
Copy link
Contributor

I merged master to get a clean diff.

semorrison
semorrison reviewed May 22, 2023
View reviewed changes
Mathlib/LinearAlgebra/Contraction.lean Outdated
Comment on lines 32 to 33
-- Porting note: apparently `high` is necessary for this to fire below, odd
attribute [local ext high] TensorProduct.ext
Copy link
Contributor

Choose a reason for hiding this comment

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

The problem is not that it doesn't fire, but just that a different @[ext] lemma fires first.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

D'oh!

@semorrison
Copy link
Contributor

Otherwise looks good!

bors d+

@bors
Copy link

bors bot commented May 22, 2023

✌️ mattrobball 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 May 22, 2023
@mattrobball
Copy link
Collaborator Author

bors merge

bors bot pushed a commit that referenced this pull request May 22, 2023
@ChrisHughes24 @mattrobball
@Parcly-Taxel @semorrison @urkud @mo271 @kmill
feat: port LinearAlgebra.Contraction (#4124)
f9055df 
Co-authored-by: Matthew Ballard <matt@mrb.email>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
@bors
Copy link

bors bot commented May 22, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title feat: port LinearAlgebra.Contraction [Merged by Bors] - feat: port LinearAlgebra.Contraction May 22, 2023
@bors bors bot closed this May 22, 2023
@bors bors bot deleted the port/LinearAlgebra.Contraction branch May 22, 2023 13:50
qawbecrdtey pushed a commit to qawbecrdtey/greedoid-mathlib4 that referenced this pull request Jun 12, 2023
@ChrisHughes24 @mattrobball
@Parcly-Taxel @semorrison @urkud @mo271 @kmill @qawbecrdtey
feat: port LinearAlgebra.Contraction (leanprover-community#4124)
38bfdcd 
Co-authored-by: Matthew Ballard <matt@mrb.email>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: Kyle Miller <kmill31415@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

Assignees
No one assigned
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
@mattrobball @semorrison @urkud @mo271 @Parcly-Taxel @kmill @ChrisHughes24