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

all_goals + apply elaboration = lost errors #4888

Closed
3 tasks done
sacerdot opened this issue Jul 31, 2024 · 1 comment · Fixed by #5863
Closed
3 tasks done

all_goals + apply elaboration = lost errors #4888

sacerdot opened this issue Jul 31, 2024 · 1 comment · Fixed by #5863
Labels
bug Something isn't working P-medium We may work on this issue if we find the time

Comments

@sacerdot
Copy link

sacerdot commented Jul 31, 2024 •
edited
Loading

Prerequisites

Please put an X between the brackets as you perform the following steps:

Description

After a ton of minimization, here is an example where all_goals swallows typing errors generated by incorrect applications:

theorem bug: True := by
 all_goals exact Nat.succ True   -- Nat.succ True is not well typed, but the tactic succeeds
 trivial

The bug propagates to <;> and from there to many other tactics and macros that fail to fail.

Versions

"4.9.0-rc3"
@sacerdot sacerdot added the bug Something isn't working label Jul 31, 2024
@leanprover-bot leanprover-bot added the P-medium We may work on this issue if we find the time label Aug 2, 2024
@sacerdot
Copy link
Author

sacerdot commented Oct 3, 2024

See also the discussion on Zulip: https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/all_goals.20.2B.20apply.20elaboration.20.3D.20lost.20errors

kmill added a commit to kmill/lean4 that referenced this issue Oct 28, 2024
@kmill
fix: let simp arguments elaborate without disabling error recovery
37b4f4f 
Modifies `simp` to elaborate all simp arguments, and *then* failing if any had any elaboration issues, rather than failing on the first simp argument.

This enables better term info and things like tab completion.

Part of addressing leanprover#3831

Closes leanprover#4888
@kmill kmill mentioned this issue Oct 28, 2024
Merged
github-merge-queue bot pushed a commit that referenced this issue Oct 28, 2024
@kmill
fix: let simp arguments elaborate with error recovery (#5863)
b308f2b 
Modifies `simp` to elaborate all simp arguments without disabling error
recovery. Like in #4177, simp arguments with elaboration errors are not
added to the simp set. Error recovery is still disabled when `simp` is
used in combinators such as `first`.

This enables better term info and features like tab completion when
there are elaboration errors.

Also included is a fix to the `all_goals` and `<;>` tactic combinators.
Recall that `try`/`catch` for the Tactic monad restores the state on
failure. This meant that all messages were being cleared on tactic
failure. The fix is to use `Tactic.tryCatch` instead, which doesn't
restore state.

Part of addressing #3831

Closes #4888
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug Something isn't working P-medium We may work on this issue if we find the time
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

fix: let simp arguments elaborate with error recovery kmill/lean4
2 participants
@sacerdot @leanprover-bot