feat: simp to still work even if one simp arg does not work #4177
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
this fixes a usability paper cut that just annoyed me. When editing a larger simp proof, I usually want to see the goal state after the simp, and this is what I see while the `simp` command is complete. But then, when I start typing, and necessarily type incomplete lemma names, that error makes `simp` do nothing again and I see the original goal state. In fact, if a prefix of the simp theorem name I am typing is a valid identifier, it jumps even more around. With this PR, using `logException`, I still get the red squiggly lines for the unknown identifer, but `simp` just ignores that argument and still shows me the final goal. Much nicer. I also demoted the message for `[-foo]` when `foo` isn’t `simp` to a warning and gave it the correct `ref`.
nomeata
added
the
new-user-papercuts
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
leodemoura
reviewed
May 15, 2024
nomeata
commented
May 16, 2024
nomeata
commented
May 16, 2024
nomeata
commented
May 16, 2024
nomeata
commented
May 16, 2024
|
This has also bothered me - thanks for addressing it! |
|
Do you feel confident enough about the implementation to supplement my confidence and approve :-) |
Komyyy
pushed a commit
to Komyyy/lean4
that referenced
this pull request
Jun 4, 2024
…er#4177) this fixes a usability paper cut that just annoyed me. When editing a larger simp proof, I usually want to see the goal state after the simp, and this is what I see while the `simp` command is complete. But then, when I start typing, and necessarily type incomplete lemma names, that error makes `simp` do nothing again and I see the original goal state. In fact, if a prefix of the simp theorem name I am typing is a valid identifier, it jumps even more around. With this PR, using `logException`, I still get the red squiggly lines for the unknown identifer, but `simp` just ignores that argument and still shows me the final goal. Much nicer. I also demoted the message for `[-foo]` when `foo` isn’t `simp` to a warning and gave it the correct `ref`. See it in action here: (in the middle, when you suddenly see the terminal, I am switching lean versions.) https://github.com/leanprover/lean4/assets/148037/8cb3c563-1354-4c2d-bcee-26dfa1005ae0
kim-em
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jun 4, 2024
nomeata
added a commit
that referenced
this pull request
Jun 5, 2024
this is an amendment to #4177, after @kmill pointed out an issue: Users might expect that within a tactic combinator like `first`, `simp [h]` fails if `h` does not exist. Therefore the behavior introduced in PR #4177, which is really most useful in mormal interactive use of `skip`, is restricted to when `recover := true`.
github-merge-queue bot
pushed a commit
that referenced
this pull request
Jun 5, 2024
this is an amendment to #4177, after @kmill pointed out an issue: Users might expect that within a tactic combinator like `first`, `simp [h]` fails if `h` does not exist. Therefore the behavior introduced in PR #4177, which is really most useful in mormal interactive use of `skip`, is restricted to when `recover := true`.
kmill
added a commit
to kmill/lean4
that referenced
this pull request
Oct 28, 2024
github-merge-queue bot
pushed a commit
that referenced
this pull request
Oct 28, 2024
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
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 fixes a usability paper cut that just annoyed me. When editing a
larger simp proof, I usually want to see the goal state after the simp,
and this is what I see while the
simpcommand is complete. But then,when I start typing, and necessarily type incomplete lemma names, that
error makes
simpdo nothing again and I see the original goal state.In fact, if a prefix of the simp theorem name I am typing is a valid
identifier, it jumps even more around.
With this PR, using
logException, I still get the red squiggly linesfor the unknown identifer, but
simpjust ignores that argument andstill shows me the final goal. Much nicer.
I also demoted the message for
[-foo]whenfooisn’tsimpto awarning and gave it the correct
ref.See it in action here: (in the middle, when you suddenly see the terminal,
I am switching lean versions.)
Peek.2024-05-15.18-38.mp4