Addressing issue #4712: keyword detection preserves contiguous characters forming a valid identifier subsequence #16322
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
herbelin
added
kind: enhancement
herbelin
force-pushed
the
master+addressing-issue4712-keyword-detection-preserve-contiguous-alphanumerical-chars
branch
from
1194cc4
to
d3e57fc
Compare
herbelin
added
the
needs: merge of dependency
|
The job library:ci-fiat_crypto_legacy has failed in allow failure mode |
herbelin
force-pushed
the
master+addressing-issue4712-keyword-detection-preserve-contiguous-alphanumerical-chars
branch
from
d3e57fc
to
17a56f8
Compare
|
🔴 CI failures at commit 17a56f8 without any failure in the test-suite ✔️ Corresponding jobs for the base commit 947398a succeeded ❔ Ask me to try to extract minimal test cases that can be added to the test-suite 🏃
|
|
The job library:ci-fiat_crypto_legacy has failed in allow failure mode |
herbelin
force-pushed
the
master+addressing-issue4712-keyword-detection-preserve-contiguous-alphanumerical-chars
branch
from
17a56f8
to
fd8c819
Compare
|
@coqbot ci minimize ci-category_theory |
|
I am now running minimization at commit fd8c819 on requested target ci-category_theory. I'll come back to you with the results once it's done. |
|
Error: Could not minimize file /github/workspace/builds/coq/coq-failing/_build_ci/category_theory/Instance/Lambda.v (from ci-category_theory) (full log on GitHub Actions, cc @JasonGross) build log (truncated to last 26KiB; full 3.0MiB file on GitHub Actions Artifacts under
|
|
It seems ci-category_theory is failing in multiple PRs, my guess is that it's a problem on their end, and the bug minimizer cannot minimize it because the file structure changed. |
|
Can confirm it fails on master https://gitlab.com/coq/coq/-/jobs/2731873554 |
herbelin
force-pushed
the
master+addressing-issue4712-keyword-detection-preserve-contiguous-alphanumerical-chars
branch
from
fd8c819
to
be9bad8
Compare
proux01
reviewed
Jul 29, 2022
proux01
approved these changes
Jul 29, 2022
proux01
added
the
needs: changelog entry
proux01
approved these changes
Jul 29, 2022
|
@herbelin could you rebase so as to avoid having a revert commit for a commit in the same PR? |
proux01
force-pushed
the
master+addressing-issue4712-keyword-detection-preserve-contiguous-alphanumerical-chars
branch
from
be9bad8
to
8758c0c
Compare
proux01
removed
the
needs: changelog entry
|
Rebased, changelog entry added, CI green, I'll merge by the end of the week if there is no further comment. |
proux01
force-pushed
the
master+addressing-issue4712-keyword-detection-preserve-contiguous-alphanumerical-chars
branch
from
8758c0c
to
1d61873
Compare
A contiguous sequence of characters must be fully inside or fully outside a keyword: no break of a keyword in the middle of a sequence of contiguous characters.
|
@coqbot merge now |
|
@proux01: You cannot merge this PR because:
|
proux01
removed
the
needs: merge of dependency
|
@coqbot merge now |
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.
Kind: wish granted, enhancement
This addresses two different kinds of examples:
Closes #4712
Depends on #16321