fix(coq.el): (setq proof-shell-strip-crs-from-input nil) #774
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
|
If no one comments further, I will merge this PR in 4 working days (on Friday evening - June 21) |
|
Fine with me. |
Matafou
added a commit
to Matafou/PG
that referenced
this pull request
Jul 9, 2024
We cannot use the " ^^^ " thing to compute the error location because commands are not stripped of newlines anymoire (ProofGeneral#774). Solution: use the character position information with the following subtleties - position are given by coq **bytes** positions. - position given by coq is the position from the previous "." fed to coq. I.e. we must be careful to strip any blank after the final "." of a command.
Matafou
added a commit
to Matafou/PG
that referenced
this pull request
Jul 10, 2024
A test is also added to check the exact position of the error highlighting. Description of the fix. We cannot use the " ^^^ " thing to compute the error location because commands are not stripped of newlines anymoire (ProofGeneral#774). Solution: use the character position information with the following subtleties - position are given by coq **bytes** positions. - position given by coq is the position from the previous "." fed to coq. I.e. we must be careful to strip any blank after the final "." of a command.
Matafou
added a commit
to Matafou/PG
that referenced
this pull request
Sep 2, 2024
A test is also added to check the exact position of the error highlighting. Description of the fix. We cannot use the " ^^^ " thing to compute the error location because commands are not stripped of newlines anymoire (ProofGeneral#774). Solution: use the character position information with the following subtleties - position are given by coq **bytes** positions. - position given by coq is the position from the previous "." fed to coq. I.e. we must be careful to strip any blank after the final "." of a command. In the test we make the disappearing tuimeout of overlay bigger so that tests don't fail on slow VMs (maybe useless). Coq-8.11 has a small glitch on positions, the test is compatible with both behaviour.
Matafou
added a commit
to Matafou/PG
that referenced
this pull request
Sep 4, 2024
Tests is also added to check the exact position of the error highlighting. Description of the fix. We cannot use the " ^^^ " thing to compute the error location because commands are not stripped of newlines anymore (ProofGeneral#774). Solution: use the character position information given in the error message with the following subtleties: - position are given by coq **bytes** positions. - position given by coq is the position from the previous "." fed to coq. I.e. we must be careful to strip any blank after the final "." of a command. - Coq < 8.11 has a small glitch on positions, the test is compatible with both behaviour. - coq <= 8.20 has a bug on position for curly braces. In the test we make the disappearing timeout of overlay bigger so that tests don't fail on slow VMs (maybe useless).
Matafou
added a commit
to Matafou/PG
that referenced
this pull request
Sep 4, 2024
Tests is also added to check the exact position of the error highlighting. Description of the fix. We cannot use the " ^^^ " thing to compute the error location because commands are not stripped of newlines anymore (ProofGeneral#774). Solution: use the character position information given in the error message with the following subtleties: - position are given by coq **bytes** positions. - position given by coq is the position from the previous "." fed to coq. I.e. we must be careful to strip any blank after the final "." of a command. - Coq < 8.11 has a small glitch on positions, the test is compatible with both behaviour. - coq <= 8.20 has a bug on position for curly braces. In the test we make the disappearing timeout of overlay bigger so that tests don't fail on slow VMs (maybe useless).
Matafou
added a commit
to Matafou/PG
that referenced
this pull request
Sep 5, 2024
Tests is also added to check the exact position of the error highlighting. Description of the fix. We cannot use the " ^^^ " thing to compute the error location because commands are not stripped of newlines anymore (ProofGeneral#774). Solution: use the character position information given in the error message with the following subtleties: - position are given by coq **bytes** positions. - position given by coq is the position from the previous "." fed to coq. I.e. we must be careful to strip any blank after the final "." of a command. - Coq < 8.11 has a small glitch on positions, the test is compatible with both behaviour. - coq <= 8.20 has a bug on position for curly braces. In the test we make the disappearing timeout of overlay bigger so that tests don't fail on slow VMs (maybe useless).
Matafou
added a commit
to Matafou/PG
that referenced
this pull request
Sep 5, 2024
Tests is also added to check the exact position of the error highlighting. Description of the fix. We cannot use the " ^^^ " thing to compute the error location because commands are not stripped of newlines anymore (ProofGeneral#774). Solution: use the character position information given in the error message with the following subtleties: - position are given by coq **bytes** positions. - position given by coq is the position from the previous "." fed to coq. I.e. we must be careful to strip any blank after the final "." of a command. - Coq < 8.11 has a small glitch on positions, the test is compatible with both behaviour. - coq <= 8.20 has a bug on position for curly braces. In the test we make the disappearing timeout of overlay bigger so that tests don't fail on slow VMs (maybe useless). NOTE: coq error locations are quite wrong when we insert spaces (instead of a newline) after a command. PG was wrongly inserting a space after Set Silent./ Unset Silent, which triggered this problem. This is fixed by this PR. But other silent commends should triped of trailing blanks. I leave it to another PR.
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.
Related: #773
@hendriktews do you agree that we merge this ? (if the CI passes, of course)