[Merged by Bors] - feat: lint against stream-of-conciousness obtain syntax#13220
Closed
[Merged by Bors] - feat: lint against stream-of-conciousness obtain syntax#13220
Conversation
Also, move to the Linter directory and add to Tactic.Basic. Now, let CI do the work.
Rename the linter from "bad" to "old"; make the error more polite".
… just import Lean and Batteries there.
Contributor
Author
|
Also linted against the analogous |
YaelDillies
reviewed
May 26, 2024
Contributor
|
May I make you remark that this is really not a |
Contributor
Author
|
I would argue it's a feature in the "linters" category - but I'm also happy to change the title. Let me know if you prefer a different category. |
5d64b96 to
1957f58
Compare
Contributor
|
Maybe ask the question on Zulip |
PR summary 6751058336Import changesDependency changes
|
YaelDillies
reviewed
Jun 23, 2024
Contributor
YaelDillies
left a comment
There was a problem hiding this comment.
So that it displays well in the docs...
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Contributor
Author
|
Thanks for the tweaks (just applied them)! In markdown, the previous formatting looked fine to me - but I'll trust your judgement that the generated docs look better this way! |
Contributor
|
Once Bryan updates the Observable notebook, we will be able to preview docs again. For now, I believe this is fine. maintainer merge |
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
Contributor
|
Thanks for writing this syntax linter! bors merge |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Jun 24, 2024
Just the syntax replacements are split into #13219. Most of its occurrences were removed in #11045 and #12850; #13219 removed the last instances. **Why is this removed?** In a nutshell, my understanding is that this is preferred against for similar reasons as #10534: - it's a Lean3-ism, which can be unlearned now - the syntax `obtain foo : type := proof` is slightly shorter; particularly so when the next tactic is `exact` - when using it as `obtain foo : type; · proof`, there is an intermediate state with multiple goals right before the focusing dot (This gets amplified with the in-flight "multiple goal linter", which in my perception seems generally desired - for many reasons, including teachability. Granted, the linter could be tweaked to not lint in this case... but by now, the "old" syntax is not clearly better.) - the old syntax *could* be slightly nicer when deferring goals: In the 30 replacements of the last PR, this occurred *twice* (i.e., very rarely). In both cases, `suffices` or `rsuffices` can be used, and would imho be clearer. Alternatively, the `obtain` tactic in Lean core could also be changed: this change does not block this at all, but moves forward with something that is doable within mathlib today.
Contributor
|
Pull request successfully merged into master. Build succeeded: |
Contributor
Author
|
Thank you for reviewing it! |
kbuzzard
pushed a commit
that referenced
this pull request
Jun 26, 2024
Just the syntax replacements are split into #13219. Most of its occurrences were removed in #11045 and #12850; #13219 removed the last instances. **Why is this removed?** In a nutshell, my understanding is that this is preferred against for similar reasons as #10534: - it's a Lean3-ism, which can be unlearned now - the syntax `obtain foo : type := proof` is slightly shorter; particularly so when the next tactic is `exact` - when using it as `obtain foo : type; · proof`, there is an intermediate state with multiple goals right before the focusing dot (This gets amplified with the in-flight "multiple goal linter", which in my perception seems generally desired - for many reasons, including teachability. Granted, the linter could be tweaked to not lint in this case... but by now, the "old" syntax is not clearly better.) - the old syntax *could* be slightly nicer when deferring goals: In the 30 replacements of the last PR, this occurred *twice* (i.e., very rarely). In both cases, `suffices` or `rsuffices` can be used, and would imho be clearer. Alternatively, the `obtain` tactic in Lean core could also be changed: this change does not block this at all, but moves forward with something that is doable within mathlib today.
dagurtomas
pushed a commit
that referenced
this pull request
Jul 2, 2024
Just the syntax replacements are split into #13219. Most of its occurrences were removed in #11045 and #12850; #13219 removed the last instances. **Why is this removed?** In a nutshell, my understanding is that this is preferred against for similar reasons as #10534: - it's a Lean3-ism, which can be unlearned now - the syntax `obtain foo : type := proof` is slightly shorter; particularly so when the next tactic is `exact` - when using it as `obtain foo : type; · proof`, there is an intermediate state with multiple goals right before the focusing dot (This gets amplified with the in-flight "multiple goal linter", which in my perception seems generally desired - for many reasons, including teachability. Granted, the linter could be tweaked to not lint in this case... but by now, the "old" syntax is not clearly better.) - the old syntax *could* be slightly nicer when deferring goals: In the 30 replacements of the last PR, this occurred *twice* (i.e., very rarely). In both cases, `suffices` or `rsuffices` can be used, and would imho be clearer. Alternatively, the `obtain` tactic in Lean core could also be changed: this change does not block this at all, but moves forward with something that is doable within mathlib today.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Just the syntax replacements are split into #13219.
Most of its occurrences were removed in #11045 and #12850; #13219 removed the last instances.
Why is this removed? In a nutshell, my understanding is that this is preferred against for similar reasons as #10534:
obtain foo : type := proofis slightly shorter; particularly so when the next tactic isexactobtain foo : type; · proof, there is an intermediate state with multiple goals right before the focusing dot(This gets amplified with the in-flight "multiple goal linter", which in my perception seems generally desired - for many reasons, including teachability. Granted, the linter could be tweaked to not lint in this case... but by now, the "old" syntax is not clearly better.)
sufficesorrsufficescan be used, and would imho be clearer.Alternatively, the
obtaintactic in Lean core could also be changed: this change does not block this at all,but moves forward with something that is doable within mathlib today.