Rocq --config Fix (#14093)

Reflecting on the issue in #13774, I think a solution that is both
forwards and backwards compatible is to just always use `rocq c
--config`. This PR implements this change and allows compilation of
`rocq.theory` stanzas for Rocq 9.0+.

Documentation in the [Rocq
CLI](https://rocq-prover.org/doc/master/refman/practical-tools/coq-commands.html#command-line-options)
implies this will be recognized by `compile/c` and [the message for this
commit](rocq-prover/rocq@da931cc)
seems to imply that `--config` will need to access the environment
regardless.

Maybe there is some reason to utilize just `rocq --config` (note:
missing the `c`), but it is not immediately obvious to me.

<details>
<summary>It working with PR dune vs. failing previous version</summary>

```bash

$ rocq --version
The Rocq Prover, version 9.0.1
compiled with OCaml 5.3.0

$ cat theories/dune
(rocq.theory
 (name test_proj)
 (package test_proj)
 (theories Stdlib))

$ cat dune-project
(lang dune 3.22)
(using rocq 0.12)
(generate_opam_files)
(package
 (name test_proj)
 (depends rocq-core))

$ cat theories/Test.v
From Stdlib Require Import Nat.

Lemma test : forall (x : nat), x = x.
Proof.  reflexivity. Qed.

$ ~/forks/dune/_boot/dune.exe build

$ ~/forks/dune/_boot/dune.exe clean

$ dune build
Warning: Skipping installed theories due to 'rocq --config' failure:
- .../.opam/package_dev/bin/rocq --config failed with exit code 1.
Hint: Try running 'rocq --config' manually to see the error.
Couldn't find Rocq standard library, and theory is not using (stdlib no)
-> required by _build/default/theories/.test_proj.theory.d
-> required by alias theories/all
-> required by alias default
File "theories/dune", line 4, characters 11-17:
4 |  (theories Stdlib))
               ^^^^^^
Theory "Stdlib" has not been found.
-> required by theory test_proj in theories/dune:2
-> required by _build/default/theories/.test_proj.theory.d
-> required by alias theories/all
-> required by alias default
```

</details>

Author: Alizter

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

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)

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.
@@ -829,9 +829,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.

src/dune_rules/rocq/rocq_config.ml

@@ -222,15 +222,15 @@ 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
 
 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 =

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
 

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

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"
     ]
   }

test/blackbox-tests/test-cases/rocq/failed-config.t/run.t

@@ -1,13 +1,13 @@
-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
 --config and --print-version.
   $ 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.

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"]}

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"
     ]
   }