+ "message": "Rocq `--config` Fix (#14093)\n\nReflecting on the issue in #13774, I think a solution that is both\nforwards and backwards compatible is to just always use `rocq c\n--config`. This PR implements this change and allows compilation of\n`rocq.theory` stanzas for Rocq 9.0+.\n\nDocumentation in the [Rocq\nCLI](https://rocq-prover.org/doc/master/refman/practical-tools/coq-commands.html#command-line-options)\nimplies this will be recognized by `compile/c` and [the message for this\ncommit](https://github.com/rocq-prover/rocq/commit/da931ccfe71144c2fb3e62f446b8684ad170b094)\nseems to imply that `--config` will need to access the environment\nregardless.\n\nMaybe there is some reason to utilize just `rocq --config` (note:\nmissing the `c`), but it is not immediately obvious to me.\n\n<details>\n<summary>It working with PR dune vs. failing previous version</summary>\n\n```bash\n\n$ rocq --version\nThe Rocq Prover, version 9.0.1\ncompiled with OCaml 5.3.0\n\n$ cat theories/dune\n(rocq.theory\n (name test_proj)\n (package test_proj)\n (theories Stdlib))\n\n$ cat dune-project\n(lang dune 3.22)\n(using rocq 0.12)\n(generate_opam_files)\n(package\n (name test_proj)\n (depends rocq-core))\n\n$ cat theories/Test.v\nFrom Stdlib Require Import Nat.\n\nLemma test : forall (x : nat), x = x.\nProof. reflexivity. Qed.\n\n$ ~/forks/dune/_boot/dune.exe build\n\n$ ~/forks/dune/_boot/dune.exe clean\n\n$ dune build\nWarning: Skipping installed theories due to 'rocq --config' failure:\n- .../.opam/package_dev/bin/rocq --config failed with exit code 1.\nHint: Try running 'rocq --config' manually to see the error.\nCouldn't find Rocq standard library, and theory is not using (stdlib no)\n-> required by _build/default/theories/.test_proj.theory.d\n-> required by alias theories/all\n-> required by alias default\nFile \"theories/dune\", line 4, characters 11-17:\n4 | (theories Stdlib))\n ^^^^^^\nTheory \"Stdlib\" has not been found.\n-> required by theory test_proj in theories/dune:2\n-> required by _build/default/theories/.test_proj.theory.d\n-> required by alias theories/all\n-> required by alias default\n```\n\n</details>",
0 commit comments