[coq] Fix coqlib file scanning. #7895
Merged
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
ejgallego
commented
Jun 5, 2023
ejgallego
commented
Jun 5, 2023
ejgallego
commented
Jun 5, 2023
ejgallego
force-pushed
the
fix_coqpath_scan
branch
from
612cc04
to
d976639
Compare
ejgallego
commented
Jun 5, 2023
| -I lib/coq/../coq-core/plugins/tutorial/p0 | ||
| -I lib/coq/../coq-core/plugins/tutorial/p1 | ||
| -I lib/coq/../coq-core/plugins/tutorial/p2 | ||
| -I lib/coq/../coq-core/plugins/tutorial/p3 |
There was a problem hiding this comment.
I've added this for consistency with what Coq does.
Coq also adds $opam_root/lib but I'd rather avoid this for now.
There was a problem hiding this comment.
We should make a bug upstream about this. For now it makes sense to keep the scanning behavior close.
ejgallego
commented
Jun 5, 2023
ejgallego
force-pushed
the
fix_coqpath_scan
branch
4 times, most recently
from
83e2bce
to
a04f40b
Compare
Alizter
reviewed
Jun 6, 2023
| -I lib/coq/../coq-core/plugins/tutorial/p0 | ||
| -I lib/coq/../coq-core/plugins/tutorial/p1 | ||
| -I lib/coq/../coq-core/plugins/tutorial/p2 | ||
| -I lib/coq/../coq-core/plugins/tutorial/p3 |
|
3.8.1 has been released, I'm removing it from the milestone. |
ejgallego
force-pushed
the
fix_coqpath_scan
branch
from
a04f40b
to
cddd197
Compare
|
Ok this should be ready. Can we add this to the 3.8.2 milestone ? |
|
@ejgallego Yes, it is already in the list of backports. The milestone won't make sense for PRs targeting the main branch. |
ejgallego
commented
Jun 8, 2023
| Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/c.v | ||
| Installing $TESTCASE_ROOT/lib/coq/user-contrib/B/c.vo | ||
|
|
||
| Now we should see that A is not rebuilt, however coqdep is called, this seems to fail |
There was a problem hiding this comment.
It is strange this is not working, we now correctly add the full list of .vo files to the deps for the A.v.d file.
Alizter
reviewed
Jun 8, 2023
Alizter
reviewed
Jun 8, 2023
Alizter
reviewed
Jun 8, 2023
Alizter
reviewed
Jun 8, 2023
Alizter
approved these changes
Jun 8, 2023
ejgallego
force-pushed
the
fix_coqpath_scan
branch
from
cddd197
to
5944f7c
Compare
The old code did indeed was nonsense, and among others was filtering all the files due to the `String.contains d '.'` condition. I wonder how the test for updating a file in user-contrib did pass tho, that seems pretty strange, as indeed we were not adding any .vo file to the .vo file list on the user-contrib deps, so this deserves more investigation. Fixes ocaml#7893 , thanks to Karl Palmskog for testing and detailed report. Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>
ejgallego
force-pushed
the
fix_coqpath_scan
branch
from
5944f7c
to
caf1870
Compare
emillon
added a commit
to emillon/opam-repository
that referenced
this pull request
Jun 16, 2023
CHANGES: - Switch back to threaded console for all systems; fix unresponsive console on Windows (ocaml/dune#7906, @nojb) - Respect `-p` / `--only-packages` for `melange.emit` artifacts (ocaml/dune#7849, @anmonteiro) - Fix scanning of Coq installed files (@ejgallego, reported by @palmskog, ocaml/dune#7895 , fixes ocaml/dune#7893) - Fix RPC buffer corruption issues due to multi threading. This issue was only reproducible with large RPC payloads (ocaml/dune#7418) - Fix printing errors from excerpts whenever character offsets span multiple lines (ocaml/dune#7950, fixes ocaml/dune#7905, @rgrinberg)
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.
The old code did indeed was nonsense, and among others was filtering all the files due to the
String.contains d '.'condition.I wonder how the test for updating a file in user-contrib did pass tho, that seems pretty strange, as indeed we were not adding any .vo file to the .vo file list on the user-contrib deps, so this deserves more investigation.
Fixes #7893 , thanks to Karl Palmskog for testing and detailed report.
TODO:
Coq_lib.Legacy.voalways returning the empty list.