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

fix: cdot parser error message range #4528

Merged
merged 2 commits into from
Jun 21, 2024
Merged

Conversation

nomeata
Copy link
Contributor

@nomeata nomeata commented Jun 21, 2024

as #4527 describes there is inconsistency between by, case and
next on the one hand who, if the goal isn’t closed, put squiggly
underlines on the first line, and ., which so far only squiggled the
dot (which is a very short symbol!)

With this change the same mechanism as used by case, namely
withCaseRef, is also used for ..

There is an argument for the status quo: The . tactic is more commonly used
with further tactics on the same line, and thus there is now a higher risk that
the user might think that the first tactic is broken. But

  • the same argument does apply to by and case where there was an intentional
    choice to do it this way
  • consistency and
  • a squiggly line just under the short . is easy to miss, so it is actually
    better to underlining more here (at least until we have a better way to
    indicate incomplete proofs, which I have hopes for)

Fixes #4527, at least most of it.

as #4527 describes there is inconsistency between `by`, `case` and
`next` on the one hand who, if the goal isn’t closed, put squiggly
underlines on the first line, and `.`, which so far only squiggled the
dot (which is a very short symbol!)

With this change the same mechanism as used by `case`, namely
`withCaseRef`, is also used for `.`.
@nomeata nomeata requested a review from semorrison as a code owner June 21, 2024 13:54
@nomeata nomeata added the awaiting-review Waiting for someone to review the PR label Jun 21, 2024
@nomeata nomeata requested a review from Kha June 21, 2024 13:55
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc June 21, 2024 14:13 Inactive
@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 Jun 21, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries CI can not be attempted yet, as the nightly-testing-2024-06-21 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. (2024-06-21 14:19:54)

@nomeata nomeata added this pull request to the merge queue Jun 21, 2024
Merged via the queue into master with commit 073b2cf Jun 21, 2024
14 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
awaiting-review Waiting for someone to review the PR 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.

inconsistent range and fullRange of by, ., next
3 participants