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

feat(simps): allow the user to specify the projections #1630

Merged
merged 10 commits into from Nov 4, 2019
Merged

feat(simps): allow the user to specify the projections #1630

merged 10 commits into from Nov 4, 2019

Conversation

fpvandoorn
Copy link
Member

  • Also add option to shorten generated lemma names
  • Add the attribute to more places in the category_theory library
  • The projection lemmas of inl_ and inr_ are now called inl__obj and similar
  • This PR is on top of feat(tactic/simps): allow let-expressions #1626

@fpvandoorn fpvandoorn added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Oct 29, 2019
robertylewis
robertylewis reviewed Oct 29, 2019
View reviewed changes
Copy link
Member

@robertylewis robertylewis left a comment

Choose a reason for hiding this comment

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

I'll leave the simps changes to be reviewed by someone more familiar with the category theory library. These are just minor doc comments.

src/meta/expr.lean Outdated Show resolved Hide resolved
src/meta/expr.lean Outdated Show resolved Hide resolved
semorrison
semorrison reviewed Oct 31, 2019
View reviewed changes
docs/tactics.md
@@ -1186,7 +1186,7 @@ begin
end
```

Although `reassoc_of` is not a tactic or a meta program, its type is generated
Although `reassoc_of` is not a tactic or a meta program, its type is generated
Copy link
Collaborator

Choose a reason for hiding this comment

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

@cipher1024, I think you're often committing changes with trailing whitespaces, that then result in spurious diffs as other people edit these files. Would you mind enabling "files.trimTrailingWhitespace": true if you use VS Code?

Copy link
Member

Choose a reason for hiding this comment

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

Unfortunately, @cipher1024 is a hardcore emacs user 😺 But I'm sure there is an emacs equivalent...

Copy link
Member Author

Choose a reason for hiding this comment

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

yes: (add-hook 'before-save-hook 'delete-trailing-whitespace)

Copy link
Collaborator

Choose a reason for hiding this comment

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

I have to apologize. I have that setting but often, I use the github interface to write missing documentation. Is there a setting for github to trim the spaces?

Copy link
Collaborator

@khoek khoek Nov 2, 2019 •
edited

Choose a reason for hiding this comment

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

https://stackoverflow.com/questions/591923/make-git-automatically-remove-trailing-whitespace-before-committing is the best I can do

semorrison
semorrison reviewed Oct 31, 2019
View reviewed changes
Copy link
Collaborator

@semorrison semorrison left a comment

Choose a reason for hiding this comment

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

I added a few comments in the category_theory changes, explaining in a few places why we were specifying the @[simp] lemmas to build explicitly. I'm happy otherwise, but didn't read the tactic side of this PR.

@semorrison semorrison removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Oct 31, 2019
fpvandoorn and others added 8 commits October 31, 2019 14:45
@fpvandoorn
feat(simps): allow the user to specify the projections
4522bcd 
Also add option to shorten generated lemma names
Add the attribute to more places in the category_theory library
The projection lemmas of inl_ and inr_ are now called inl__obj and similar
@fpvandoorn
use simps partially in limits/cones and whiskering
f2e1ce5
@fpvandoorn
revert whiskering
3deefdf
@fpvandoorn
rename last_name to short_name
5fa5876
@semorrison @fpvandoorn
Update src/category_theory/products/basic.lean
0e0e4dd
@fpvandoorn @semorrison
Update src/category_theory/limits/cones.lean
56f234b 
Co-Authored-By: Scott Morrison <scott@tqft.net>
@fpvandoorn @semorrison
Update src/category_theory/products/associator.lean
6bfab48 
Co-Authored-By: Scott Morrison <scott@tqft.net>
@fpvandoorn @semorrison
Update src/data/string/defs.lean
2a7266c 
Co-Authored-By: Scott Morrison <scott@tqft.net>
@fpvandoorn fpvandoorn added the awaiting-review The author would like community review of the PR label Oct 31, 2019
@robertylewis
Copy link
Member

@semorrison approves the library changes and the tactic work looks good to me, so I think this is ready. Tagging @rwbarton in case he has an opinion since he's commented on earlier simps PRs. Absent any word from him, I'll merge tonight.

robertylewis
robertylewis approved these changes Nov 4, 2019
View reviewed changes
Copy link
Member

@robertylewis robertylewis left a comment

Choose a reason for hiding this comment

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

Absent any word from him, I'll merge tonight.

Oops, I'm a little late!

@robertylewis robertylewis 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 Nov 4, 2019
@mergify mergify bot merged commit ee5b38d into master Nov 4, 2019
@mergify mergify bot deleted the simps_specify branch November 4, 2019 15:03
anrddh pushed a commit to anrddh/mathlib that referenced this pull request May 15, 2020
@fpvandoorn @anrddh
feat(simps): allow the user to specify the projections (leanprover-co…
0879bb1 
…mmunity#1630)

* feat(simps): allow the user to specify the projections

Also add option to shorten generated lemma names
Add the attribute to more places in the category_theory library
The projection lemmas of inl_ and inr_ are now called inl__obj and similar

* use simps partially in limits/cones and whiskering

* revert whiskering

* rename last_name to short_name

* Update src/category_theory/products/basic.lean

* Update src/category_theory/limits/cones.lean

Co-Authored-By: Scott Morrison <scott@tqft.net>

* Update src/category_theory/products/associator.lean

Co-Authored-By: Scott Morrison <scott@tqft.net>

* Update src/data/string/defs.lean

Co-Authored-By: Scott Morrison <scott@tqft.net>

* clarify is_eta_expansion docstrings
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@cipher1024 cipher1024 cipher1024 left review comments

@khoek khoek khoek left review comments

@semorrison semorrison semorrison left review comments

@jcommelin jcommelin jcommelin left review comments

@robertylewis robertylewis robertylewis approved these changes

Assignees
No one assigned
Labels
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
6 participants
@fpvandoorn @robertylewis @cipher1024 @khoek @semorrison @jcommelin