diff --git a/Makefile b/Makefile index 75b3f16770d..0fc35baf71d 100644 --- a/Makefile +++ b/Makefile @@ -116,7 +116,7 @@ test-melange: $(BIN) $(BIN) build @runtest-melange test-all: $(BIN) - $(BIN) build @runtest @runtest-js @runtest-rocq @runtest-melange + DUNE_ROCQ_TEST=enable $(BIN) build @runtest @runtest-js @runtest-rocq @runtest-melange test-ox: $(BIN) $(BIN) runtest test/blackbox-tests/test-cases/oxcaml diff --git a/doc/changes/fixed/14093.md b/doc/changes/fixed/14093.md new file mode 100644 index 00000000000..1df99da5cdf --- /dev/null +++ b/doc/changes/fixed/14093.md @@ -0,0 +1,2 @@ +- Fix Rocq configuration detection to use `rocq c --config` subcommand + instead of `rocq --config` (#14093, fixes #13774, @Durbatuluk1701) diff --git a/doc/rocq.rst b/doc/rocq.rst index 4ba692b3703..debb9702e26 100644 --- a/doc/rocq.rst +++ b/doc/rocq.rst @@ -283,7 +283,7 @@ Dune organises it's knowledge about Rocq theories in 3 databases: workspace-public theories, Dune will try to locate the theory in the list of installed locations Rocq knows about. - This list is built using the output of ``rocqc --config`` in order to infer + This list is built using the output of ``rocq c --config`` in order to infer the ``ROCQLIB`` and ``ROCQPATH`` environment variables. Each path in ``ROCQPATH`` and ``ROCQLIB/user-contrib`` is used to build the database of installed theories. @@ -815,9 +815,9 @@ configuration. These are: - ``%{rocq:version.suffix}`` the suffix version of Rocq (e.g., ``9.1.2`` gives ``.2`` and ``9.2+rc1`` gives ``+rc1``). - ``%{rocq:ocaml-version}`` the version of OCaml used to compile Rocq. -- ``%{rocq:rocqlib}`` the output of ``ROCQLIB`` from ``rocqc -config``. +- ``%{rocq:rocqlib}`` the output of ``ROCQLIB`` from ``rocq c --config``. - ``%{rocq:rocq_native_compiler_default}`` the output of - ``ROCQ_NATIVE_COMPILER_DEFAULT`` from ``rocqc -config``. + ``ROCQ_NATIVE_COMPILER_DEFAULT`` from ``rocq c --config``. See :doc:`concepts/variables` for more information on variables supported by Dune. diff --git a/src/dune_rules/rocq/rocq_config.ml b/src/dune_rules/rocq/rocq_config.ml index 12b7e2b9788..fd5877aa416 100644 --- a/src/dune_rules/rocq/rocq_config.ml +++ b/src/dune_rules/rocq/rocq_config.ml @@ -222,7 +222,7 @@ let impl_config bin = ~output_limit:Execution_parameters.Action_output_limit.default) Return bin - [ "--config" ] + [ "c"; "--config" ] ;; let config_memo = Memo.create "rocq-config" ~input:(module Path) impl_config @@ -230,7 +230,7 @@ let config_memo = Memo.create "rocq-config" ~input:(module Path) impl_config let make ~(rocq : Action.Prog.t) = let open Memo.O in let+ config_output = - get_output_from_config_or_version ~rocq ~what:"--config" config_memo + get_output_from_config_or_version ~rocq ~what:"c --config" config_memo in let open Result.O in let* config_output = config_output in @@ -243,7 +243,7 @@ let make ~(rocq : Action.Prog.t) = let rocq_native_compiler_default = Vars.get_opt vars "COQ_NATIVE_COMPILER_DEFAULT" in Ok { rocqlib; rocq_native_compiler_default } | Error msg -> - User_error.raise Pp.[ textf "Cannot parse output of rocq --config:"; msg ] + User_error.raise Pp.[ textf "Cannot parse output of 'rocq c --config':"; msg ] ;; let by_name { rocqlib; rocq_native_compiler_default } name = diff --git a/src/dune_rules/rocq/rocq_config.mli b/src/dune_rules/rocq/rocq_config.mli index a1935a1328c..af49db84907 100644 --- a/src/dune_rules/rocq/rocq_config.mli +++ b/src/dune_rules/rocq/rocq_config.mli @@ -56,11 +56,11 @@ end (** Data of a Rocq configuration. *) type t -(** [make ~rocq] runs rocq --config and returns the configuration data. Exceptionally, one +(** [make ~rocq] runs [rocq c --config] and returns the configuration data. Exceptionally, one of the following will happen: - - Return [Error message] if rocq --config exits with a non-zero code. - - Throw a user error if rocq --config is not parsable. + - Return [Error message] if rocq c --config exits with a non-zero code. + - Throw a user error if rocq c --config is not parsable. - Throw an [Action.Prog.Not_found] exception if the rocq binary is not found. *) val make : rocq:Action.Prog.t -> (t, User_message.Style.t Pp.t) result Memo.t diff --git a/src/dune_rules/rocq/rocq_path.ml b/src/dune_rules/rocq/rocq_path.ml index aa9575b2968..ce019bebd1a 100644 --- a/src/dune_rules/rocq/rocq_path.ml +++ b/src/dune_rules/rocq/rocq_path.ml @@ -36,11 +36,11 @@ let config_path_exn rocq_config key = (* This should never happen *) Code_error.raise "key is not a path" [ key, Rocq_config.Value.to_dyn path ]) | None -> - (* This happens if the output of rocq --config doesn't include the key *) + (* This happens if the output of rocq c --config doesn't include the key *) User_error.raise [ Pp.concat ~sep:Pp.space - [ Pp.text "key not found from"; User_message.command "rocq --config" ] + [ Pp.text "key not found from"; User_message.command "rocq c --config" ] |> Pp.hovbox ; Pp.text key ] @@ -144,7 +144,7 @@ let of_rocq_install rocq = [ Pp.concat ~sep:Pp.space [ Pp.text "Skipping installed theories due to" - ; User_message.command "rocq --config" + ; User_message.command "rocq c --config" ; Pp.text "failure:" ] |> Pp.hovbox @@ -154,7 +154,7 @@ let of_rocq_install rocq = [ Pp.concat ~sep:Pp.space [ Pp.text "Try running" - ; User_message.command "rocq --config" + ; User_message.command "rocq c --config" ; Pp.text "manually to see the error." ] |> Pp.hovbox diff --git a/test/blackbox-tests/test-cases/rocq/coqtop/coqtop-flags.t/run.t b/test/blackbox-tests/test-cases/rocq/coqtop/coqtop-flags.t/run.t index 4a671b20504..2527b63138d 100644 --- a/test/blackbox-tests/test-cases/rocq/coqtop/coqtop-flags.t/run.t +++ b/test/blackbox-tests/test-cases/rocq/coqtop/coqtop-flags.t/run.t @@ -6,6 +6,7 @@ The flags passed to coqc: { "name": "rocq", "args": [ + "c", "--config" ] } diff --git a/test/blackbox-tests/test-cases/rocq/failed-config.t/run.t b/test/blackbox-tests/test-cases/rocq/failed-config.t/run.t index d8644c36d73..71ccacf3b2e 100644 --- a/test/blackbox-tests/test-cases/rocq/failed-config.t/run.t +++ b/test/blackbox-tests/test-cases/rocq/failed-config.t/run.t @@ -1,4 +1,4 @@ -Here we test what happens when rocq --config or --print-version fails in an unexpected way +Here we test what happens when rocq c --config or --print-version fails in an unexpected way and how dune reacts to this failure. First we create a wrapper around coqc so we can make it fail. It should only fail on @@ -6,8 +6,8 @@ First we create a wrapper around coqc so we can make it fail. It should only fai $ mkdir bin $ cat > bin/rocq <<'EOF' > #!/bin/sh - > if [ "$1" = --config ] && [ -n "$FAIL_CONFIG" ]; then - > echo "rocq --config has failed for some reason" >&2 + > if [ "$1" = c ] && [ "$2" = --config ] && [ -n "$FAIL_CONFIG" ]; then + > echo "rocq c --config has failed for some reason" >&2 > exit 1 > elif [ "$1" = --print-version ] && [ -n "$FAIL_VERSION" ]; then > echo "rocq --print-version has failed for some reason" >&2 @@ -23,13 +23,13 @@ To make sure these are working correctly we test them. These should succeed. $ rocq --print-version > /dev/null - $ rocq --config > /dev/null + $ rocq c --config > /dev/null These should fail. $ FAIL_VERSION=1 \ > rocq --print-version 2> /dev/null [1] $ FAIL_CONFIG=1 \ - > rocq --config 2> /dev/null + > rocq c --config 2> /dev/null [1] Now we create a simple project that uses this coqc wrapper, should @@ -52,9 +52,9 @@ Should fail: first warning that installed theories are being skipped due to the failure, then, as the library requires the stdlib, it fails: $ FAIL_CONFIG=1 \ > dune build - Warning: Skipping installed theories due to 'rocq --config' failure: - - $TESTCASE_ROOT/bin/rocq --config failed with exit code 1. - Hint: Try running 'rocq --config' manually to see the error. + Warning: Skipping installed theories due to 'rocq c --config' failure: + - $TESTCASE_ROOT/bin/rocq c --config failed with exit code 1. + Hint: Try running 'rocq c --config' manually to see the error. Couldn't find Rocq standard library, and theory is not using (stdlib no) -> required by _build/default/.foo.theory.d -> required by alias all @@ -82,9 +82,9 @@ Should succeed, warning that installed theories are being skipped due to the failure (c.f. #8958): $ FAIL_CONFIG=1 \ > dune build - Warning: Skipping installed theories due to 'rocq --config' failure: - - $TESTCASE_ROOT/bin/rocq --config failed with exit code 1. - Hint: Try running 'rocq --config' manually to see the error. + Warning: Skipping installed theories due to 'rocq c --config' failure: + - $TESTCASE_ROOT/bin/rocq c --config failed with exit code 1. + Hint: Try running 'rocq c --config' manually to see the error. $ FAIL_VERSION=1 \ > dune build @@ -127,14 +127,14 @@ however a failing --print-version will not. > EOF Should fail. - $ export coqlib="$(rocq --config | grep COQLIB | sed 's/COQLIB=//')" + $ export coqlib="$(rocq c --config | grep COQLIB | sed 's/COQLIB=//')" $ FAIL_CONFIG=1 \ > dune build @config File "dune", line 4, characters 8-23: 4 | (echo %{rocq:rocqlib}))) ^^^^^^^^^^^^^^^ Error: Could not expand %{rocq:rocqlib} as running rocq failed. - $TESTCASE_ROOT/bin/rocq --config failed with exit code 1. + $TESTCASE_ROOT/bin/rocq c --config failed with exit code 1. [1] Should succeed. diff --git a/test/blackbox-tests/test-cases/rocq/flags.t b/test/blackbox-tests/test-cases/rocq/flags.t index cacd619838c..33266595128 100644 --- a/test/blackbox-tests/test-cases/rocq/flags.t +++ b/test/blackbox-tests/test-cases/rocq/flags.t @@ -23,7 +23,7 @@ Test case: default flags > } $ runFlags - {"name":"rocq","args":["--config"]} + {"name":"rocq","args":["c","--config"]} {"name":"rocq","args":["dep","-boot","-R","coq/theories","Corelib","-R",".","foo","-dyndep","opt","-vos","foo.v"]} {"name":"rocq","args":["compile","-q","-w","-deprecated-native-compiler-option","-w","-native-compiler-disabled","-native-compiler","ondemand","-boot","-R","coq/theories","Corelib","-R",".","foo","foo.v"]} @@ -36,7 +36,7 @@ TC: :standard > EOF $ runFlags - {"name":"rocq","args":["--config"]} + {"name":"rocq","args":["c","--config"]} {"name":"rocq","args":["dep","-boot","-R","coq/theories","Corelib","-R",".","foo","-dyndep","opt","-vos","foo.v"]} {"name":"rocq","args":["compile","-q","-w","-deprecated-native-compiler-option","-w","-native-compiler-disabled","-native-compiler","ondemand","-boot","-R","coq/theories","Corelib","-R",".","foo","foo.v"]} @@ -49,7 +49,7 @@ TC: override :standard > EOF $ runFlags - {"name":"rocq","args":["--config"]} + {"name":"rocq","args":["c","--config"]} {"name":"rocq","args":["dep","-boot","-R","coq/theories","Corelib","-R",".","foo","-dyndep","opt","-vos","foo.v"]} {"name":"rocq","args":["compile","-w","-deprecated-native-compiler-option","-w","-native-compiler-disabled","-native-compiler","ondemand","-boot","-R","coq/theories","Corelib","-R",".","foo","foo.v"]} @@ -62,7 +62,7 @@ TC: add to :standard > EOF $ runFlags - {"name":"rocq","args":["--config"]} + {"name":"rocq","args":["c","--config"]} {"name":"rocq","args":["dep","-boot","-R","coq/theories","Corelib","-R",".","foo","-dyndep","opt","-vos","foo.v"]} {"name":"rocq","args":["compile","-q","-type-in-type","-w","-deprecated-native-compiler-option","-w","-native-compiler-disabled","-native-compiler","ondemand","-boot","-R","coq/theories","Corelib","-R",".","foo","foo.v"]} @@ -80,7 +80,7 @@ TC: extend in workspace + override standard > EOF $ runFlags - {"name":"rocq","args":["--config"]} + {"name":"rocq","args":["c","--config"]} {"name":"rocq","args":["dep","-boot","-R","coq/theories","Corelib","-R",".","foo","-dyndep","opt","-vos","foo.v"]} {"name":"rocq","args":["compile","-type-in-type","-w","-deprecated-native-compiler-option","-w","-native-compiler-disabled","-native-compiler","ondemand","-boot","-R","coq/theories","Corelib","-R",".","foo","foo.v"]} @@ -92,7 +92,7 @@ TC: extend in workspace + override standard > EOF $ runFlags - {"name":"rocq","args":["--config"]} + {"name":"rocq","args":["c","--config"]} {"name":"rocq","args":["dep","-boot","-R","coq/theories","Corelib","-R",".","foo","-dyndep","opt","-vos","foo.v"]} {"name":"rocq","args":["compile","-q","-type-in-type","-w","-deprecated-native-compiler-option","-w","-native-compiler-disabled","-native-compiler","ondemand","-boot","-R","coq/theories","Corelib","-R",".","foo","foo.v"]} @@ -105,7 +105,7 @@ TC: extend in dune (env) + override standard > EOF $ runFlags - {"name":"rocq","args":["--config"]} + {"name":"rocq","args":["c","--config"]} {"name":"rocq","args":["dep","-boot","-R","coq/theories","Corelib","-R",".","foo","-dyndep","opt","-vos","foo.v"]} {"name":"rocq","args":["compile","-type-in-type","-w","-deprecated-native-compiler-option","-w","-native-compiler-disabled","-native-compiler","ondemand","-boot","-R","coq/theories","Corelib","-R",".","foo","foo.v"]} @@ -118,7 +118,7 @@ TC: extend in dune (env) + standard > EOF $ runFlags - {"name":"rocq","args":["--config"]} + {"name":"rocq","args":["c","--config"]} {"name":"rocq","args":["dep","-boot","-R","coq/theories","Corelib","-R",".","foo","-dyndep","opt","-vos","foo.v"]} {"name":"rocq","args":["compile","-q","-type-in-type","-type-in-type","-w","-deprecated-native-compiler-option","-w","-native-compiler-disabled","-native-compiler","ondemand","-boot","-R","coq/theories","Corelib","-R",".","foo","foo.v"]} @@ -136,6 +136,6 @@ TC: extend in dune (env) + workspace + standard > EOF $ runFlags - {"name":"rocq","args":["--config"]} + {"name":"rocq","args":["c","--config"]} {"name":"rocq","args":["dep","-boot","-R","coq/theories","Corelib","-R",".","foo","-dyndep","opt","-vos","foo.v"]} {"name":"rocq","args":["compile","-q","-type-in-type","-bt","-w","-deprecated-native-compiler-option","-w","-native-compiler-disabled","-native-compiler","ondemand","-boot","-R","coq/theories","Corelib","-R",".","foo","foo.v"]} diff --git a/test/blackbox-tests/test-cases/rocq/rocq-native/coqtop/coqtop-flags.t/run.t b/test/blackbox-tests/test-cases/rocq/rocq-native/coqtop/coqtop-flags.t/run.t index 645c4dbb0c5..be8a81142d8 100644 --- a/test/blackbox-tests/test-cases/rocq/rocq-native/coqtop/coqtop-flags.t/run.t +++ b/test/blackbox-tests/test-cases/rocq/rocq-native/coqtop/coqtop-flags.t/run.t @@ -6,6 +6,7 @@ The flags passed to coqc: { "name": "rocq", "args": [ + "c", "--config" ] } diff --git a/test/blackbox-tests/test-cases/rocq/rocq-native/flags.t b/test/blackbox-tests/test-cases/rocq/rocq-native/flags.t index bee408d21d1..d0521c1e411 100644 --- a/test/blackbox-tests/test-cases/rocq/rocq-native/flags.t +++ b/test/blackbox-tests/test-cases/rocq/rocq-native/flags.t @@ -23,7 +23,7 @@ Test case: default flags > EOF $ runFlags - {"name":"rocq","args":["--config"]} + {"name":"rocq","args":["c","--config"]} {"name":"rocq","args":["dep","-boot","-R","coq/theories","Corelib","-R",".","foo","-dyndep","opt","-vos","foo.v"]} {"name":"rocq","args":["compile","-q","-w","-deprecated-native-compiler-option","-native-output-dir",".","-native-compiler","on","-nI","rocq-runtime/kernel","-nI",".","-boot","-R","coq/theories","Corelib","-R",".","foo","foo.v"]} @@ -36,7 +36,7 @@ TC: :standard > EOF $ runFlags - {"name":"rocq","args":["--config"]} + {"name":"rocq","args":["c","--config"]} {"name":"rocq","args":["dep","-boot","-R","coq/theories","Corelib","-R",".","foo","-dyndep","opt","-vos","foo.v"]} {"name":"rocq","args":["compile","-q","-w","-deprecated-native-compiler-option","-native-output-dir",".","-native-compiler","on","-nI","rocq-runtime/kernel","-nI",".","-boot","-R","coq/theories","Corelib","-R",".","foo","foo.v"]} @@ -49,7 +49,7 @@ TC: override :standard > EOF $ runFlags - {"name":"rocq","args":["--config"]} + {"name":"rocq","args":["c","--config"]} {"name":"rocq","args":["dep","-boot","-R","coq/theories","Corelib","-R",".","foo","-dyndep","opt","-vos","foo.v"]} {"name":"rocq","args":["compile","-w","-deprecated-native-compiler-option","-native-output-dir",".","-native-compiler","on","-nI","rocq-runtime/kernel","-nI",".","-boot","-R","coq/theories","Corelib","-R",".","foo","foo.v"]} @@ -62,7 +62,7 @@ TC: add to :standard > EOF $ runFlags - {"name":"rocq","args":["--config"]} + {"name":"rocq","args":["c","--config"]} {"name":"rocq","args":["dep","-boot","-R","coq/theories","Corelib","-R",".","foo","-dyndep","opt","-vos","foo.v"]} {"name":"rocq","args":["compile","-q","-type-in-type","-w","-deprecated-native-compiler-option","-native-output-dir",".","-native-compiler","on","-nI","rocq-runtime/kernel","-nI",".","-boot","-R","coq/theories","Corelib","-R",".","foo","foo.v"]} @@ -80,7 +80,7 @@ TC: extend in workspace + override standard > EOF $ runFlags - {"name":"rocq","args":["--config"]} + {"name":"rocq","args":["c","--config"]} {"name":"rocq","args":["dep","-boot","-R","coq/theories","Corelib","-R",".","foo","-dyndep","opt","-vos","foo.v"]} {"name":"rocq","args":["compile","-type-in-type","-w","-deprecated-native-compiler-option","-native-output-dir",".","-native-compiler","on","-nI","rocq-runtime/kernel","-nI",".","-boot","-R","coq/theories","Corelib","-R",".","foo","foo.v"]} @@ -92,7 +92,7 @@ TC: extend in workspace + override standard > EOF $ runFlags - {"name":"rocq","args":["--config"]} + {"name":"rocq","args":["c","--config"]} {"name":"rocq","args":["dep","-boot","-R","coq/theories","Corelib","-R",".","foo","-dyndep","opt","-vos","foo.v"]} {"name":"rocq","args":["compile","-q","-type-in-type","-w","-deprecated-native-compiler-option","-native-output-dir",".","-native-compiler","on","-nI","rocq-runtime/kernel","-nI",".","-boot","-R","coq/theories","Corelib","-R",".","foo","foo.v"]} @@ -105,7 +105,7 @@ TC: extend in dune (env) + override standard > EOF $ runFlags - {"name":"rocq","args":["--config"]} + {"name":"rocq","args":["c","--config"]} {"name":"rocq","args":["dep","-boot","-R","coq/theories","Corelib","-R",".","foo","-dyndep","opt","-vos","foo.v"]} {"name":"rocq","args":["compile","-type-in-type","-w","-deprecated-native-compiler-option","-native-output-dir",".","-native-compiler","on","-nI","rocq-runtime/kernel","-nI",".","-boot","-R","coq/theories","Corelib","-R",".","foo","foo.v"]} @@ -118,7 +118,7 @@ TC: extend in dune (env) + standard > EOF $ runFlags - {"name":"rocq","args":["--config"]} + {"name":"rocq","args":["c","--config"]} {"name":"rocq","args":["dep","-boot","-R","coq/theories","Corelib","-R",".","foo","-dyndep","opt","-vos","foo.v"]} {"name":"rocq","args":["compile","-q","-type-in-type","-type-in-type","-w","-deprecated-native-compiler-option","-native-output-dir",".","-native-compiler","on","-nI","rocq-runtime/kernel","-nI",".","-boot","-R","coq/theories","Corelib","-R",".","foo","foo.v"]} @@ -136,6 +136,6 @@ TC: extend in dune (env) + workspace + standard > EOF $ runFlags - {"name":"rocq","args":["--config"]} + {"name":"rocq","args":["c","--config"]} {"name":"rocq","args":["dep","-boot","-R","coq/theories","Corelib","-R",".","foo","-dyndep","opt","-vos","foo.v"]} {"name":"rocq","args":["compile","-q","-type-in-type","-bt","-w","-deprecated-native-compiler-option","-native-output-dir",".","-native-compiler","on","-nI","rocq-runtime/kernel","-nI",".","-boot","-R","coq/theories","Corelib","-R",".","foo","foo.v"]}