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.

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

feat: whitespace and message ordering configurations for #guard_msgs #3883

Merged
merged 4 commits into from
Apr 13, 2024

Conversation

kmill
Copy link
Collaborator

@kmill kmill commented Apr 12, 2024

Adds options to control whitespace normalization and message ordering in #guard_msgs.

Examples:

  1. #guard_msgs (whitespace := lax) ignores differences in whitespace completely.
  2. #guard_msgs (whitespace := exact) requires an exact match for whitespace (after trimming).
  3. #guard_msgs (ordering := sorted) sorts the list of messages, to make it insensitive to message order.

src/Init/Notation.lean Outdated Show resolved Hide resolved
@digama0
Copy link
Collaborator

digama0 commented Apr 12, 2024

The code action also needs to be modified to take the ordering := sorted setting into account, or else it will suggest a docstring that will fail the command.

@kmill
Copy link
Collaborator Author

kmill commented Apr 12, 2024

@digama0 It's now about ready to come out of draft state. If you approve, then I'll go and create a PR for the first commit (bc75d48), then update stage0, and then this PR will just be for the third commit.

It turns out the code action didn't need special handling since the sorted version is passed into the info tree. I tested it by using it to create the docstrings in the test file.

@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 Apr 12, 2024
@kmill kmill marked this pull request as ready for review April 13, 2024 00:30
@kmill kmill requested a review from semorrison as a code owner April 13, 2024 00:30
@kmill
Copy link
Collaborator Author

kmill commented Apr 13, 2024

@digama0 The staging business is all worked out now in this PR, and it's set to trigger a stage0 update after it merges.

@digama0
Copy link
Collaborator

digama0 commented Apr 13, 2024

Okay, LGTM. Let's see if merging works...

@digama0 digama0 added this pull request to the merge queue Apr 13, 2024
Merged via the queue into leanprover:master with commit eef928b Apr 13, 2024
10 checks passed
@Kha
Copy link
Member

Kha commented Apr 18, 2024

#guard_msgs (ordering := sorted) sorts the list of messages, to make it insensitive to message order.

Should this be considered a workaround for #2335?

@kmill
Copy link
Collaborator Author

kmill commented Apr 18, 2024

@Kha Yes, though it goes a little further since, for example, a tactic might spawn multiple threads and report multiple messages nondeterministically at the same source position.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants