[Merged by Bors] - chore: better failures for linear_combination
#15791
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
PR summary 0440177643Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for |
hrmacbeth
added
the
easy
|
Seems good. Maybe it could make sense to move withoutErrToSorry earlier, but where you have it currently is definitely justified since it's for elaboration of syntax generated by the tactic itself. bors r+ |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Aug 15, 2024
The implementation of `linear_combination` is as a macro performing effectively `refine ******; ring`. If the term provided to `refine` fails to elaborate, Lean inserts sorries where needed and then continues on to `ring`. This produces a confusing error message. For example, the problem ```lean example (x y : ℤ) (h1 : x * y + 2 * x = 1) (h2 : x = y) : x * y + 2 * x = 1 := by linear_combination h1 + (0 : ℝ) * h2 ``` produces both the "true" error message ``` application type mismatch Mathlib.Tactic.LinearCombination.c_mul_pf h2 0 argument 0 has type ℝ : Type but is expected to have type ℤ : Type ``` and the "tactic is confused because it persevered when it shouldn't have" error message ``` ring failed, ring expressions not equal x y : ℤ h1 : x * y + 2 * x = 1 h2 : x = y ⊢ -(x * sorryAx ℤ true) + y * sorryAx ℤ true = 0 ``` This PR fixes this by strategically inserting a `Term.withoutErrToSorry`. In examples such as the above, it now stops after the `refine`, so the second error message does not appear.
|
Build failed (retrying...): |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Aug 16, 2024
The implementation of `linear_combination` is as a macro performing effectively `refine ******; ring`. If the term provided to `refine` fails to elaborate, Lean inserts sorries where needed and then continues on to `ring`. This produces a confusing error message. For example, the problem ```lean example (x y : ℤ) (h1 : x * y + 2 * x = 1) (h2 : x = y) : x * y + 2 * x = 1 := by linear_combination h1 + (0 : ℝ) * h2 ``` produces both the "true" error message ``` application type mismatch Mathlib.Tactic.LinearCombination.c_mul_pf h2 0 argument 0 has type ℝ : Type but is expected to have type ℤ : Type ``` and the "tactic is confused because it persevered when it shouldn't have" error message ``` ring failed, ring expressions not equal x y : ℤ h1 : x * y + 2 * x = 1 h2 : x = y ⊢ -(x * sorryAx ℤ true) + y * sorryAx ℤ true = 0 ``` This PR fixes this by strategically inserting a `Term.withoutErrToSorry`. In examples such as the above, it now stops after the `refine`, so the second error message does not appear.
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
linear_combinationlinear_combination
bjoernkjoshanssen
pushed a commit
that referenced
this pull request
Sep 9, 2024
The implementation of `linear_combination` is as a macro performing effectively `refine ******; ring`. If the term provided to `refine` fails to elaborate, Lean inserts sorries where needed and then continues on to `ring`. This produces a confusing error message. For example, the problem ```lean example (x y : ℤ) (h1 : x * y + 2 * x = 1) (h2 : x = y) : x * y + 2 * x = 1 := by linear_combination h1 + (0 : ℝ) * h2 ``` produces both the "true" error message ``` application type mismatch Mathlib.Tactic.LinearCombination.c_mul_pf h2 0 argument 0 has type ℝ : Type but is expected to have type ℤ : Type ``` and the "tactic is confused because it persevered when it shouldn't have" error message ``` ring failed, ring expressions not equal x y : ℤ h1 : x * y + 2 * x = 1 h2 : x = y ⊢ -(x * sorryAx ℤ true) + y * sorryAx ℤ true = 0 ``` This PR fixes this by strategically inserting a `Term.withoutErrToSorry`. In examples such as the above, it now stops after the `refine`, so the second error message does not appear.
bjoernkjoshanssen
pushed a commit
that referenced
this pull request
Sep 9, 2024
The implementation of `linear_combination` is as a macro performing effectively `refine ******; ring`. If the term provided to `refine` fails to elaborate, Lean inserts sorries where needed and then continues on to `ring`. This produces a confusing error message. For example, the problem ```lean example (x y : ℤ) (h1 : x * y + 2 * x = 1) (h2 : x = y) : x * y + 2 * x = 1 := by linear_combination h1 + (0 : ℝ) * h2 ``` produces both the "true" error message ``` application type mismatch Mathlib.Tactic.LinearCombination.c_mul_pf h2 0 argument 0 has type ℝ : Type but is expected to have type ℤ : Type ``` and the "tactic is confused because it persevered when it shouldn't have" error message ``` ring failed, ring expressions not equal x y : ℤ h1 : x * y + 2 * x = 1 h2 : x = y ⊢ -(x * sorryAx ℤ true) + y * sorryAx ℤ true = 0 ``` This PR fixes this by strategically inserting a `Term.withoutErrToSorry`. In examples such as the above, it now stops after the `refine`, so the second error message does not appear.
bjoernkjoshanssen
pushed a commit
that referenced
this pull request
Sep 12, 2024
The implementation of `linear_combination` is as a macro performing effectively `refine ******; ring`. If the term provided to `refine` fails to elaborate, Lean inserts sorries where needed and then continues on to `ring`. This produces a confusing error message. For example, the problem ```lean example (x y : ℤ) (h1 : x * y + 2 * x = 1) (h2 : x = y) : x * y + 2 * x = 1 := by linear_combination h1 + (0 : ℝ) * h2 ``` produces both the "true" error message ``` application type mismatch Mathlib.Tactic.LinearCombination.c_mul_pf h2 0 argument 0 has type ℝ : Type but is expected to have type ℤ : Type ``` and the "tactic is confused because it persevered when it shouldn't have" error message ``` ring failed, ring expressions not equal x y : ℤ h1 : x * y + 2 * x = 1 h2 : x = y ⊢ -(x * sorryAx ℤ true) + y * sorryAx ℤ true = 0 ``` This PR fixes this by strategically inserting a `Term.withoutErrToSorry`. In examples such as the above, it now stops after the `refine`, so the second error message does not appear.
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.
The implementation of
linear_combinationis as a macro performing effectivelyrefine ******; ring. If the term provided torefinefails to elaborate, Lean inserts sorries where needed and then continues on toring. This produces a confusing error message. For example, the problemproduces both the "true" error message
and the "tactic is confused because it persevered when it shouldn't have" error message
This PR fixes this by strategically inserting a
Term.withoutErrToSorry. In examples such as the above, it now stops after therefine, so the second error message does not appear.