Can't find Coq plugin cmxs on loadpath error #7893
Labels
Comments
|
Thanks a lot for the reproduction instructions @palmskog , for the sake to be sure what the problem is, can you confirm that the Can you also post the contents of the |
|
For the first confirmation: $ ls ~/.opam/4.14.1+flambda+coq.8.16/lib/coq/user-contrib/Equations/
CoreTactics.glob CoreTactics.v CoreTactics.vo equations_plugin.cmxs Init.glob Init.v Init.vo Prop Signature.glob Signature.v Signature.vo TypeFor the contents of |
|
Thanks @palmskog , that's the succesful run with the [I correctly see |
|
@ejgallego you're right, my mistake, here is the erroring log with |
|
I looked at the code that should add the |
|
@Alizter a |
|
Bug confirmed by printing the list of inferred coqpaths: |
|
The scanning code seems pretty bogus, first bug is: The latter condition makes indeed us to scan all files as they contain a dot (examples: Once we disable that, there are quite a few additional bugs:
I've exhausted my time bugdet for this for today, but that should provide a lead on the fix. |
|
I did produce a fix in the end, see new PR. |
ejgallego
added a commit
to ejgallego/dune
that referenced
this issue
Jun 5, 2023
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. TODO: - changelog - new test cases [installed plugin] - figure out why old test-cases were not catching `Coq_lib.Legacy.vo` always returning the empty list.
ejgallego
added a commit
to ejgallego/dune
that referenced
this issue
Jun 5, 2023
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. TODO: - changelog - new test cases [installed plugin] - figure out why old test-cases were not catching `Coq_lib.Legacy.vo` always returning the empty list.
ejgallego
added a commit
to ejgallego/dune
that referenced
this issue
Jun 5, 2023
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. TODO: - changelog - new test cases [installed plugin] - figure out why old test-cases were not catching `Coq_lib.Legacy.vo` always returning the empty list. Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
ejgallego
added a commit
to ejgallego/dune
that referenced
this issue
Jun 5, 2023
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 <e+git@x80.org>
ejgallego
added a commit
to ejgallego/dune
that referenced
this issue
Jun 5, 2023
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 <e+git@x80.org>
ejgallego
added a commit
to ejgallego/dune
that referenced
this issue
Jun 5, 2023
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 <e+git@x80.org>
ejgallego
added a commit
to ejgallego/dune
that referenced
this issue
Jun 8, 2023
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 <e+git@x80.org>
ejgallego
added a commit
to ejgallego/dune
that referenced
this issue
Jun 8, 2023
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 <e+git@x80.org>
ejgallego
added a commit
to ejgallego/dune
that referenced
this issue
Jun 9, 2023
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 <e+git@x80.org>
ejgallego
added a commit
that referenced
this issue
Jun 9, 2023
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. Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
emillon
pushed a commit
to emillon/dune
that referenced
this issue
Jun 13, 2023
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 <e+git@x80.org>
Merged
emillon
added a commit
that referenced
this issue
Jun 15, 2023
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. Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org> Co-authored-by: Emilio Jesus Gallego Arias <e+git@x80.org>
emillon
added a commit
to emillon/opam-repository
that referenced
this issue
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
Expected Behavior
When I create a
dune-projectanddunefile for a Coq project with Dune 3.8 and depend on a Coq plugin installed via coq_makefile like Equations, it should suffice to add(theories Equations)into(coq.theory ...)to enable compilation of the project.Actual Behavior
When I run
dune build, I get the following error:Reproduction
dune-projectfile like the following:dunefile like the following:Eqn.vor other.vfile like the following:dune build, get the following error:Note that the error disappears if
;(plugins coq-equations)induneis uncommented.Specifications
dune(output ofdune --version): 3.8.0ocaml(output ofocamlc --version): 4.14.1Additional information
This bug report was submitted at the suggestion of @ejgallego.
The text was updated successfully, but these errors were encountered: