[Merged by Bors] - refactor: do not import old-style have/suffices/replace within mathlib
#10534
Conversation
This file contains 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
eric-wieser
changed the title
have/suffices in mathlibhave/suffices within mathlib
eric-wieser
added
awaiting-review
|
I think it's really strange to have a tactic in mathlib which is not usable in mathlib. I'd rather remove the file completely, for coherence and predictability. |
|
I'd rather leave it in for now so as not to break anyone's teaching material. Perhaps we can have it raise a code action that rewrites it to the new style.
I don't think this is all that far away from our existing rule of "don't use |
|
Are you sure this change desactivate the stream of consciousness |
|
(Scratch that, my tests were done on a previous commit in whic |
|
It turns out that in fact there were some bad uses of |
|
I now see that #6964 recommends not spending manual effort here, and waiting for a syntax transformation tool instead. Sorry for the false claim that we already didn't use this syntax anywhere! |
|
Given the examples I've fixed (some of them very obfuscated), I don't think an automatic tool could do this. So I think I'm gonna fix this by hand instead of waiting, if you don't mind. |
|
Speaking of obfuscation, this one is quite nice: suffices; exact (encode_lt_pair cf cg).imp (fun h => lt_trans h this) fun h => lt_trans h this
change _; simp [encodeCode_eq, encodeCode]I think Mario knows too well for his own good how everything works. |
eric-wieser
commented
Feb 15, 2024
leanprover-community-mathlib4-bot
added
merge-conflict
grunweg
force-pushed
the
eric-wieser/remove-tactic.Have
branch
from
8e9ad34
to
89a5316
Compare
eric-wieser
changed the title
have/suffices within mathlibhave/suffices/replace within mathlib
grunweg
changed the title
have/suffices/replace within mathlibhave/replace/suffices within mathlib
|
|
|
I could use a hand fixing the two remaining tests. |
|
Now that everything is fixed (hopefully), I have extracted another PR keeping just the fixes to the library, and not touching the tactic files. Hopefully it shouldn't be controversial and can be merged quickly, and then we will discuss here what to do of the tactic files (disable them or remove them). |
leanprover-community-mathlib4-bot
added
blocked-by-other-PR
|
This PR/issue depends on: |
This syntax remains available downstream with `import Mathlib.Tactic`, but is not available in mathlib
sgouezel
reviewed
Feb 18, 2024
leanprover-community-mathlib4-bot
added
ready-to-merge
mathlib-bors bot
pushed a commit
that referenced
this pull request
Feb 20, 2024
…mathlib (#10534) This syntax remains available downstream with `import Mathlib.Tactic`, but is no longer available in mathlib itself. This follows on from #10640, which remove all current uses of this syntax. By removing these imports, we prevent further regressions in mathlib, and save reviewers from having to look out for this in review. In future we could delete this syntax entirely, but this would harm downstream code, especially mathport output. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
|
Build failed (retrying...):
|
mathlib-bors bot
pushed a commit
that referenced
this pull request
Feb 20, 2024
…mathlib (#10534) This syntax remains available downstream with `import Mathlib.Tactic`, but is no longer available in mathlib itself. This follows on from #10640, which remove all current uses of this syntax. By removing these imports, we prevent further regressions in mathlib, and save reviewers from having to look out for this in review. In future we could delete this syntax entirely, but this would harm downstream code, especially mathport output. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
have/suffices/replace within mathlibhave/suffices/replace within mathlib
thorimur
pushed a commit
that referenced
this pull request
Feb 24, 2024
…mathlib (#10534) This syntax remains available downstream with `import Mathlib.Tactic`, but is no longer available in mathlib itself. This follows on from #10640, which remove all current uses of this syntax. By removing these imports, we prevent further regressions in mathlib, and save reviewers from having to look out for this in review. In future we could delete this syntax entirely, but this would harm downstream code, especially mathport output. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
thorimur
pushed a commit
that referenced
this pull request
Feb 26, 2024
…mathlib (#10534) This syntax remains available downstream with `import Mathlib.Tactic`, but is no longer available in mathlib itself. This follows on from #10640, which remove all current uses of this syntax. By removing these imports, we prevent further regressions in mathlib, and save reviewers from having to look out for this in review. In future we could delete this syntax entirely, but this would harm downstream code, especially mathport output. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
riccardobrasca
pushed a commit
that referenced
this pull request
Mar 1, 2024
…mathlib (#10534) This syntax remains available downstream with `import Mathlib.Tactic`, but is no longer available in mathlib itself. This follows on from #10640, which remove all current uses of this syntax. By removing these imports, we prevent further regressions in mathlib, and save reviewers from having to look out for this in review. In future we could delete this syntax entirely, but this would harm downstream code, especially mathport output. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
riccardobrasca
pushed a commit
that referenced
this pull request
Mar 1, 2024
kbuzzard
pushed a commit
that referenced
this pull request
Mar 12, 2024
dagurtomas
pushed a commit
that referenced
this pull request
Mar 22, 2024
…mathlib (#10534) This syntax remains available downstream with `import Mathlib.Tactic`, but is no longer available in mathlib itself. This follows on from #10640, which remove all current uses of this syntax. By removing these imports, we prevent further regressions in mathlib, and save reviewers from having to look out for this in review. In future we could delete this syntax entirely, but this would harm downstream code, especially mathport output. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
dagurtomas
pushed a commit
that referenced
this pull request
Mar 22, 2024
Louddy
pushed a commit
that referenced
this pull request
Apr 15, 2024
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.
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.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
This syntax remains available downstream with
import Mathlib.Tactic, but is no longer available in mathlib itself.This follows on from #10640, which remove all current uses of this syntax.
By removing these imports, we prevent further regressions in mathlib,
and save reviewers from having to look out for this in review.
In future we could delete this syntax entirely, but this would harm downstream code, especially mathport output.
have,replaceandsuffices#10640