Skip to content

[Merged by Bors] - feat: add to_additive linter checking whether additive decl exists#1881

Closed
fpvandoorn wants to merge 14 commits intomasterfrom
toadditiveexisting
Closed

[Merged by Bors] - feat: add to_additive linter checking whether additive decl exists#1881
fpvandoorn wants to merge 14 commits intomasterfrom
toadditiveexisting

Conversation

@fpvandoorn
Copy link
Copy Markdown
Member

@fpvandoorn fpvandoorn commented Jan 27, 2023 •
edited by github-actions bot
Loading

  • Force the user to specify whether the additive declaration already exists.
  • Will raise a linter error if the user specified it wrongly
  • Requested on Zulip

neither of the following are functional dependencies, just trying to minimize merge conflicts

Open in Gitpod

@fpvandoorn fpvandoorn added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) awaiting-author A reviewer has asked the author a question or requested changes. awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jan 27, 2023
@fpvandoorn
Copy link
Copy Markdown
Member Author

fpvandoorn commented Jan 27, 2023

Ideally I would like to get a bors d+ before I fix all linter errors generated by this. That allows me to go through the library only once, instead of multiple times.

@fpvandoorn fpvandoorn added the t-meta Tactics, attributes or user commands label Jan 27, 2023
@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 Jan 29, 2023
rwbarton
rwbarton reviewed Jan 30, 2023
View reviewed changes
@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 Feb 3, 2023
@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 Feb 17, 2023
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Feb 17, 2023

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 Feb 17, 2023
@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 Feb 17, 2023
@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 Feb 20, 2023
@fpvandoorn fpvandoorn mentioned this pull request Feb 28, 2023
Closed
@kmill
Copy link
Copy Markdown
Contributor

kmill commented Feb 28, 2023

Looks like a helpful feature

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Feb 28, 2023

✌️ fpvandoorn 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 This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Feb 28, 2023
@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 Feb 28, 2023
@fpvandoorn
Copy link
Copy Markdown
Member Author

fpvandoorn commented Feb 28, 2023

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Feb 28, 2023
bors bot pushed a commit that referenced this pull request Feb 28, 2023
@fpvandoorn
feat: add to_additive linter checking whether additive decl exists (#…
77e6315 
…1881)

* Force the user to specify whether the additive declaration already exists.
* Will raise a linter error if the user specified it wrongly
* Requested on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/to_additive.20clashes)
@bors
Copy link
Copy Markdown

bors bot commented Feb 28, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: add to_additive linter checking whether additive decl exists [Merged by Bors] - feat: add to_additive linter checking whether additive decl exists Feb 28, 2023
@bors bors bot closed this Feb 28, 2023
@bors bors bot deleted the toadditiveexisting branch February 28, 2023 21:06
bors bot pushed a commit that referenced this pull request Mar 1, 2023
@fpvandoorn @jcommelin
feat: port LinearAlgebra.TensorProduct (#2539)
7b9199f 
It was quite smooth. I didn't have to make changes that I expect to change downstream files, so I left few porting notes.

Comments that I didn't make into porting notes:
* `attribute [local ext] ext` had to be changed to `attribute [local ext high] ext`
* Sometimes `M ⊗ N` needed to be replaced by `M ⊗[R] N` in theorem statements.
* I needed to make a few fixes in other files. I want to go through the library globally and fix this error, but I'm waiting on #1881 to get merged, because those two things would have many merge conflicts.



Co-authored-by: Johan Commelin <johan@commelin.net>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

1 more reviewer

@rwbarton rwbarton rwbarton left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors. t-meta Tactics, attributes or user commands

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@fpvandoorn @kim-em @kmill @rwbarton