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: improved calc error messages #5719

Merged
merged 8 commits into from
Oct 28, 2024
Merged

feat: improved calc error messages #5719

merged 8 commits into from
Oct 28, 2024

Conversation

kmill
Copy link
Collaborator

@kmill kmill commented Oct 15, 2024 •
edited
Loading

Makes the error messages report on RHSs and LHSs that do not match the expected values when the relations are defeq. If the relations are not defeq, the error message now no longer mentions the value of the whole calc expression.

Adds a field to mkCoe with an optional callback to use to generate error messages.

Note: it is tempting to try to make use of expected types when elaborating the calc expression, but this runs into issue #2073.

Closes #4318

@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Oct 15, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 15, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#5719
d9a0da4
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 15, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#5719
a888289
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Oct 15, 2024 •
edited
Loading

Mathlib CI status (docs):

  • 💥 Mathlib branch lean-pr-testing-5719 build failed against this PR. (2024-10-15 07:20:40) View Log
  • 💥 Mathlib branch lean-pr-testing-5719 build failed against this PR. (2024-10-15 08:12:00) View Log
  • 💥 Mathlib branch lean-pr-testing-5719 build failed against this PR. (2024-10-15 08:56:17) View Log
  • ✅ Mathlib branch lean-pr-testing-5719 has successfully built against this PR. (2024-10-15 17:49:38) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 7c2425605c4c0eba47604c5132bd7617bea02e61 --onto 0bfe1a8c1a2e2eb6da0dad270d7b2bbdd5b97c3d. (2024-10-17 01:11:35)
  • ✅ Mathlib branch lean-pr-testing-5719 has successfully built against this PR. (2024-10-28 19:20:20) View Log
  • ✅ Mathlib branch lean-pr-testing-5719 has successfully built against this PR. (2024-10-28 21:22:41) View Log

@leanprover-community-bot leanprover-community-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Oct 15, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 15, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5719
d6f9699
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 15, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5719
4a79ee3
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 15, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5719
8650d3b
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 15, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5719
40e975c
@leanprover-community-bot leanprover-community-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Oct 15, 2024
@kmill
Copy link
Collaborator Author

kmill commented Oct 17, 2024

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 235ecbc.
There were significant changes against commit 7c24256:

  Benchmark             Metric                 Change
  =============================================================
+ bv_decide_mul         branch-misses           -2.5% (-11.2 σ)
+ bv_decide_realworld   branch-misses           -1.4% (-10.2 σ)
- import Lean           task-clock               8.4%  (16.1 σ)
- import Lean           wall-clock               8.4%  (15.8 σ)
- stdlib                dsimp                    1.4%  (21.9 σ)
- stdlib                instantiate metavars    17.2%  (26.8 σ)

kmill added 7 commits October 28, 2024 10:39
@kmill
feat: improved calc error messages
92dd0fd 
Makes the error messages report on RHSs, LHSs, and relations that do not match the expected types.

Adds postponement support to term-mode `calc`.

Uses expected type for elaboration (NOTE: can't do this because of 2073 )

Closes leanprover#4318
@kmill
Learned about issue 2073, where making use of the expected type is un…
4f6860a 
…wanted.
@kmill
add ref field to CalcStepView
b6e6875
@kmill
error reporting bug
8a77dbc
@kmill
modify SyntheticMVarKind.coe to allow custom error reporting. This …
8df852c 
…is needed since we need to interleave the isDefEq hints with other elaboration tasks!
@kmill
remove pp change
b75ebe1
@kmill
use lighter solution to .coe, with optional callback, to avoid allo…
5a0249e 
…cating closures all the time
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 28, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5719
2cfb041
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 28, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5719
c93155d
@kmill
Copy link
Collaborator Author

kmill commented Oct 28, 2024

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 5a0249e.
There were significant changes against commit 9847923:

  Benchmark   Metric                 Change
  ===================================================
+ stdlib      instantiate metavars    -5.7% (-10.4 σ)

@kmill kmill marked this pull request as ready for review October 28, 2024 20:23
@kmill kmill requested a review from kim-em as a code owner October 28, 2024 20:23
@kmill kmill enabled auto-merge October 28, 2024 20:31
@kmill kmill added this pull request to the merge queue Oct 28, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 28, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5719
ae039d9
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 28, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5719
43e6304
Merged via the queue into leanprover:master with commit 19bebfc Oct 28, 2024
15 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

Assignees
No one assigned
Labels
builds-mathlib CI has verified that Mathlib builds against this PR toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

RFC: Better error reports for incomplete calc
3 participants
@kmill @leanprover-community-bot @leanprover-bot