The "dune coq top" is unreliable when not called from the workspace root #7344
Labels
Comments
rlepigre
added a commit
to rlepigre/dune
that referenced
this issue
Mar 17, 2023
Signed-off-by: Rodolphe Lepigre <[email protected]>
|
I see the same issue for |
|
In fact this is an issue for a regular OCaml project too. Calling the build command within a sub directory means it is unable to detect the root. The workaround for |
|
I am reminded that |
|
Oh I see! That explains why I was really confused by the kinds of errors I was getting in cram tests. |
|
@rlepigre Can you confirm that this is still an issue outside of the cram tests? |
|
The issue is definitely real, I experienced the problem in an actual Coq project. I wrote the cram test to more easily experiment with the |
|
Here you go: 7344.tar.gz. This contains the same setup as in the cram test, but as a shell script. |
|
I also found out that this diff is enough to make everything work: diff --git a/bin/coq/coqtop.ml b/bin/coq/coqtop.ml
index 9621de830..ff1e2ba20 100644
--- a/bin/coq/coqtop.ml
+++ b/bin/coq/coqtop.ml
@@ -31,7 +31,6 @@ let term =
Arg.(value & pos_right 0 string [] (Arg.info [] ~docv:"ARGS"))
in
let config = Common.init common in
- let root = Common.root common in
let prefix_target = Common.prefix_target common in
let coqtop, argv, env =
Scheduler.go ~common ~config (fun () ->
@@ -40,25 +39,6 @@ let term =
let* setup = Memo.run setup in
let sctx = Import.Main.find_scontext_exn setup ~name:context in
let context = Dune_rules.Super_context.context sctx in
- (* Try to compute a relative path if we got an absolute path. *)
- let coq_file_arg =
- if Filename.is_relative coq_file_arg then
- Path.relative Path.root (root.reach_from_root_prefix ^ coq_file_arg)
- |> Path.to_string
- else
- let cwd = Path.external_ Path.External.initial_cwd in
- let file =
- (* Best-effort symbolic link unfolding. *)
- let file = Fpath.follow_symlinks coq_file_arg in
- Option.value file ~default:coq_file_arg
- in
- let file = Path.of_filename_relative_to_initial_cwd file in
- let cwd = Path.to_string cwd in
- let file = Path.to_string file in
- match String.drop_prefix ~prefix:(cwd ^ "/") file with
- | None -> coq_file_arg
- | Some s -> s
- in
let coq_file_build =
let p = prefix_target coq_file_arg in
Path.Build.relative context.build_dir pThis disables some hack I added to work with absolute paths, but that was a terrible idea since The actual problem was calling |
|
Note that I can't seem to be able to fix the cram test I wrote in any way, even if I specify |
|
Did you unset |
Dune should be able to handle the absolute paths correctly, there is infrastructure to do that. I'll take a closer look this week. Thanks for the debugging! |
No I did not, I just added |
rlepigre
added a commit
to rlepigre/dune
that referenced
this issue
Mar 20, 2023
Signed-off-by: Rodolphe Lepigre <[email protected]>
rlepigre
added a commit
to rlepigre/dune
that referenced
this issue
Mar 20, 2023
Signed-off-by: Rodolphe Lepigre <[email protected]>
rlepigre
added a commit
to rlepigre/dune
that referenced
this issue
Mar 20, 2023
This currently disables a hack previously meant at supporting absolute file paths for [dune coq top]. Signed-off-by: Rodolphe Lepigre <[email protected]>
|
Actually I managed to fix the cram test, and used the functions for my script in there @Alizter. I also created an MR to fix the bug: feel free to take it over if you want to investigate absolute file path stuff (I won't have time to work more on this this week). |
|
Hi @rlepigre ,
Yes, it looks like the problem was this one, actually I recall when I saw that code we are removing I was thinking it was suspicious. Note that Dune does fine with absolute paths indeed, there is this bug about an absolute path being a symlink we got hit with but that it is a bug. |
|
Yeah, we also have an example where resolving symbolic links (in the workspace) is a bad thing. So I'm 100% for removing this code. |
rlepigre
added a commit
to rlepigre/dune
that referenced
this issue
Mar 20, 2023
Signed-off-by: Rodolphe Lepigre <[email protected]>
rlepigre
added a commit
to rlepigre/dune
that referenced
this issue
Mar 20, 2023
This currently disables a hack previously meant at supporting absolute file paths for [dune coq top]. Signed-off-by: Rodolphe Lepigre <[email protected]>
Alizter
pushed a commit
to rlepigre/dune
that referenced
this issue
Mar 20, 2023
Signed-off-by: Rodolphe Lepigre <[email protected]>
Alizter
pushed a commit
to rlepigre/dune
that referenced
this issue
Mar 20, 2023
This currently disables a hack previously meant at supporting absolute file paths for [dune coq top]. Signed-off-by: Rodolphe Lepigre <[email protected]>
Alizter
pushed a commit
that referenced
this issue
Mar 21, 2023
Signed-off-by: Rodolphe Lepigre <[email protected]>
emillon
added a commit
to emillon/opam-repository
that referenced
this issue
Apr 18, 2023
CHANGES: - When a rule's action is interrupted, delete any leftover directory targets. This is consistent with how we treat file targets. (@rgrinberg, 7564) - Fix plugin loading with findlib. The functionality was broken in 3.7.0. (ocaml/dune#7556, @anmonteiro) - Introduce a `public_headers` field on libraries. This field is like `install_c_headers`, but it allows to choose the extension and choose the paths for the installed headers. (ocaml/dune#7512, @rgrinberg) - Load the host context `findlib.conf` when cross-compiling (ocaml/dune#7428, fixes ocaml/dune#1701, @rgrinberg, @anmonteiro) - Resolve `ppx_runtime_libraries` in the target context when cross compiling (ocaml/dune#7450, fixes ocaml/dune#2794, @anmonteiro) - Use `$PKG_CONFIG`, when set, to find the `pkg-config` binary (ocaml/dune#7469, fixes ocaml/dune#2572, @anmonteiro) - Preliminary support for Coq compiled intefaces (`.vos` files) enabled via `(mode vos)` in `coq.theory` stanzas. This can be used in combination with `dune coq top` to obtain fast re-building of dependencies (with no checking of proofs) prior to stepping into a file. (ocaml/dune#7406, @rlepigre) - Fix dune crashing on MacOS in watch mode whenever `$PATH` contains `$PWD` (ocaml/dune#7441, fixes ocaml/dune#6907, @rgrinberg) - Fix `dune install` when cross compiling (ocaml/dune#7410, fixes ocaml/dune#6191, @anmonteiro, @rizo) - Find `pps` dependencies in the host context when cross-compiling, (ocaml/dune#7410, fixes ocaml/dune#4156, @anmonteiro) - Dune in watch mode no longer builds concurrent rules in serial (ocaml/dune#7395 @rgrinberg, @jchavarri) - `dune coq top` now correctly respects the project root when called from a subdirectory. However, absolute filenames passed to `dune coq top` are no longer supported (due to being buggy) (ocaml/dune#7357, fixes ocaml/dune#7344, @rlepigre and @Alizter) - Added a `--no-build` option to `dune coq top` for avoiding rebuilds (ocaml/dune#7380, fixes ocaml/dune#7355, @Alizter) - RPC: Ignore SIGPIPE when clients suddenly disconnect (ocaml/dune#7299, ocaml/dune#7319, fixes ocaml/dune#6879, @rgrinberg) - Always clean up the UI on exit. (ocaml/dune#7271, fixes ocaml/dune#7142 @rgrinberg) - Bootstrap: remove reliance on shell. Previously, we'd use the shell to get the number of processors. (ocaml/dune#7274, @rgrinberg) - Bootstrap: correctly detect the number of processors by allowing `nproc` to be looked up in `$PATH` (ocaml/dune#7272, @Alizter) - Speed up file copying on macos by using `clonefile` when available (@rgrinberg, ocaml/dune#7210) - Adds support for loading plugins in toplevels (ocaml/dune#6082, fixes ocaml/dune#6081, @ivg, @richardlford) - Support commands that output 8-bit and 24-bit colors in the terminal (ocaml/dune#7188, @Alizter) - Speed up rule generation for libraries and executables with many modules (ocaml/dune#7187, @jchavarri) - Add `--watch-exclusions` to Dune build options (ocaml/dune#7216, @jonahbeckford) - Do not re-render UI on every frame if the UI doesn't change (ocaml/dune#7186, fix ocaml/dune#7184, @rgrinberg) - Make coq_db creation in scope lazy (@ejgallego, ocaml/dune#7133) - Non-user proccesses such as version control or config checking are now run silently. (ocaml/dune#6994, fixes ocaml/dune#4066, @Alizter) - Add the `--display-separate-messages` flag to separate the error messages produced by commands with a blank line. (ocaml/dune#6823, fixes ocaml/dune#6158, @esope) - Accept the Ordered Set Language for the `modes` field in `library` stanzas (ocaml/dune#6611, @anmonteiro). - dune install now respects --display quiet mode (ocaml/dune#7116, fixes ocaml/dune#4573, fixes ocaml/dune#7106, @Alizter) - Stub shared libraries (dllXXX_stubs.so) in Dune-installed libraries could not be used as dependencies of libraries in the workspace (eg when compiling to bytecode and/or Javascript). This is now fixed. (ocaml/dune#7151, @nojb) - Allow the main module of a library with `(stdlib ...)` to depend on other libraries (ocaml/dune#7154, @anmonteiro). - Bytecode executables built for JSOO are linked with `-noautolink` and no longer depend on the shared stubs of their dependent libraries (ocaml/dune#7156, @nojb) - Added a new user action `(concurrent )` which is like `(progn )` but runs the actions concurrently. (ocaml/dune#6933, @Alizter) - Allow `(stdlib ...)` to be used with `(wrapped false)` in library stanzas (ocaml/dune#7139, @anmonteiro). - Allow parallel execution of inline tests partitions (ocaml/dune#7012, @hhugo) - Support `(link_flags ...)` in `(cinaps ...)` stanza. (ocaml/dune#7423, fixes ocaml/dune#7416, @nojb) - Allow `(package ...)` in any position within `(rule ...)` stanza (ocaml/dune#7445, @Leonidas-from-XIV) - Always include `opam` files in the generated `.install` file. Previously, it would not be included whenever `(generate_opam_files true)` was set and the `.install` file wasn't yet generated. (ocaml/dune#7547, @rgrinberg)
emillon
added a commit
to emillon/opam-repository
that referenced
this issue
May 23, 2023
CHANGES: - Fix string quoting in the json file written by `--trace-file` (ocaml/dune#7773, @rleshchinskiy) - Read `pkg-config` arguments from the `PKG_CONFIG_ARGN` environment variable (ocaml/dune#1492, ocaml/dune#7734, @anmonteiro) - Correctly set `MANPATH` in `dune exec`. Previously, we would use the `bin/` directory of the context. (ocaml/dune#7655, @rgrinberg) - Allow overriding the `ocaml` binary with findlib configuration (ocaml/dune#7648, @rgrinberg) - merlin: ignore instrumentation settings for preprocessing. (ocaml/dune#7606, fixes ocaml/dune#7465, @Alizter) - When a rule's action is interrupted, delete any leftover directory targets. This is consistent with how we treat file targets. (ocaml/dune#7564, @rgrinberg) - Fix plugin loading with findlib. The functionality was broken in 3.7.0. (ocaml/dune#7556, @anmonteiro) - Introduce a `public_headers` field on libraries. This field is like `install_c_headers`, but it allows to choose the extension and choose the paths for the installed headers. (ocaml/dune#7512, @rgrinberg) - Load the host context `findlib.conf` when cross-compiling (ocaml/dune#7428, fixes ocaml/dune#1701, @rgrinberg, @anmonteiro) - Add a `coqdoc_flags` field to the `coq.theory` stanza allowing the user to pass extra arguments to `coqdoc`. (ocaml/dune#7676, fixes ocaml/dune#7954 @Alizter) - Resolve `ppx_runtime_libraries` in the target context when cross compiling (ocaml/dune#7450, fixes ocaml/dune#2794, @anmonteiro) - Use `$PKG_CONFIG`, when set, to find the `pkg-config` binary (ocaml/dune#7469, fixes ocaml/dune#2572, @anmonteiro) - Modules that were declared in `(modules_without_implementation)`, `(private_modules)` or `(virtual_modules)` but not declared in `(modules)` will cause Dune to emit a warning which will become an error in 3.9. (ocaml/dune#7608, fixes ocaml/dune#7026, @Alizter) - Preliminary support for Coq compiled intefaces (`.vos` files) enabled via `(mode vos)` in `coq.theory` stanzas. This can be used in combination with `dune coq top` to obtain fast re-building of dependencies (with no checking of proofs) prior to stepping into a file. (ocaml/dune#7406, @rlepigre) - Fix dune crashing on MacOS in watch mode whenever `$PATH` contains `$PWD` (ocaml/dune#7441, fixes ocaml/dune#6907, @rgrinberg) - Fix `dune install` when cross compiling (ocaml/dune#7410, fixes ocaml/dune#6191, @anmonteiro, @rizo) - Find `pps` dependencies in the host context when cross-compiling, (ocaml/dune#7410, fixes ocaml/dune#4156, @anmonteiro) - Dune in watch mode no longer builds concurrent rules in serial (ocaml/dune#7395 @rgrinberg, @jchavarri) - Dune can now detect Coq theories from outside the workspace. This allows for composition with installed theories (not necessarily installed with Dune). (ocaml/dune#7047, @Alizter, @ejgallego) - `dune coq top` now correctly respects the project root when called from a subdirectory. However, absolute filenames passed to `dune coq top` are no longer supported (due to being buggy) (ocaml/dune#7357, fixes ocaml/dune#7344, @rlepigre and @Alizter) - Added a `--no-build` option to `dune coq top` for avoiding rebuilds (ocaml/dune#7380, fixes ocaml/dune#7355, @Alizter) - RPC: Ignore SIGPIPE when clients suddenly disconnect (ocaml/dune#7299, ocaml/dune#7319, fixes ocaml/dune#6879, @rgrinberg) - Always clean up the UI on exit. (ocaml/dune#7271, fixes ocaml/dune#7142 @rgrinberg) - Bootstrap: remove reliance on shell. Previously, we'd use the shell to get the number of processors. (ocaml/dune#7274, @rgrinberg) - Bootstrap: correctly detect the number of processors by allowing `nproc` to be looked up in `$PATH` (ocaml/dune#7272, @Alizter) - Speed up file copying on macos by using `clonefile` when available (@rgrinberg, ocaml/dune#7210) - Adds support for loading plugins in toplevels (ocaml/dune#6082, fixes ocaml/dune#6081, @ivg, @richardlford) - Support commands that output 8-bit and 24-bit colors in the terminal (ocaml/dune#7188, @Alizter) - Speed up rule generation for libraries and executables with many modules (ocaml/dune#7187, @jchavarri) - Add `--watch-exclusions` to Dune build options (ocaml/dune#7216, @jonahbeckford) - Do not re-render UI on every frame if the UI doesn't change (ocaml/dune#7186, fix ocaml/dune#7184, @rgrinberg) - Make coq_db creation in scope lazy (@ejgallego, ocaml/dune#7133) - Non-user proccesses such as version control or config checking are now run silently. (ocaml/dune#6994, fixes ocaml/dune#4066, @Alizter) - Add the `--display-separate-messages` flag to separate the error messages produced by commands with a blank line. (ocaml/dune#6823, fixes ocaml/dune#6158, @esope) - Accept the Ordered Set Language for the `modes` field in `library` stanzas (ocaml/dune#6611, @anmonteiro). - dune install now respects --display quiet mode (ocaml/dune#7116, fixes ocaml/dune#4573, fixes ocaml/dune#7106, @Alizter) - Stub shared libraries (dllXXX_stubs.so) in Dune-installed libraries could not be used as dependencies of libraries in the workspace (eg when compiling to bytecode and/or Javascript). This is now fixed. (ocaml/dune#7151, @nojb) - Allow the main module of a library with `(stdlib ...)` to depend on other libraries (ocaml/dune#7154, @anmonteiro). - Bytecode executables built for JSOO are linked with `-noautolink` and no longer depend on the shared stubs of their dependent libraries (ocaml/dune#7156, @nojb) - Added a new user action `(concurrent )` which is like `(progn )` but runs the actions concurrently. (ocaml/dune#6933, @Alizter) - Allow `(stdlib ...)` to be used with `(wrapped false)` in library stanzas (ocaml/dune#7139, @anmonteiro). - Allow parallel execution of inline tests partitions (ocaml/dune#7012, @hhugo) - Support `(link_flags ...)` in `(cinaps ...)` stanza. (ocaml/dune#7423, fixes ocaml/dune#7416, @nojb) - Allow `(package ...)` in any position within `(rule ...)` stanza (ocaml/dune#7445, @Leonidas-from-XIV) - Always include `opam` files in the generated `.install` file. Previously, it would not be included whenever `(generate_opam_files true)` was set and the `.install` file wasn't yet generated. (ocaml/dune#7547, @rgrinberg) - Fix regression where Merlin was unable to handle filenames with uppercase letters under Windows. (ocaml/dune#7577, @nojb) - On nix+macos, pass `-f` to the codesign hook to avoid errors when the binary is already signed (ocaml/dune#7183, fixes ocaml/dune#6265, @greedy) - Fix bug where RPC clients built with dune-rpc-lwt would crash when closing their connection to the server (ocaml/dune#7581, @gridbugs) - Introduce mdx stanza 0.4 requiring mdx >= 2.3.0 which updates the default list of files to include `*.mld` files (ocaml/dune#7582, @Leonidas-from-XIV) - Fix RPC server on Windows (used for OCaml-LSP). (ocaml/dune#7666, @nojb) - Coq language versions less 0.8 are deprecated, and will be removed in an upcoming Dune version. All users are required to migrate to `(coq lang 0.8)` which provides the right semantics for theories that have been globally installed, such as those coming from opam (@ejgallego, @Alizter) - Bump minimum version of the dune language for the melange syntax extension from 3.7 to 3.8 (ocaml/dune#7665, @jchavarri)
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Expected Behavior
I would expect that whenever
dune coq topis invoked from wherever in a dune workspace, with a relative path to a file that is part of a stanza in the workspace, then it simply works.Actual Behavior
Currently
dune coq topseems to only really work well when invoked from the workspace root. That is probably my fault, since I wrote the initial implementation.Note that similarly to #7335, it may happen that invokingThis probably does not actually happen, see #7348 for why I was confused.dune coq topin a sub-project of a workspace create a_buildfolder in a subdirectory (instead of at the dune workspace root).Reproduction
See #7345.
The text was updated successfully, but these errors were encountered: