Rocq --config Fix

[Durbatuluk1701]

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 implies this will be recognized by compile/c and the message for this commit 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.

It working with PR dune vs. failing previous version

$ 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

[rlepigre-skylabs-ai]

I think this is a reasonable approach, although I would consider it inferior to falling back to rocq c --config if rocq --config fails (not sure how hard that would be to do). The current approach would make it harder for Rocq to remove the --config option from rocq c, which I think would make sense eventually (CLI flags are kind of a mess in Rocq). That being said, I'm fine if we want to simply merge this.

[rlepigre-skylabs-ai]

We probably don't want this, right @Alizter?

[Alizter]

Actually, I think its fine. Otherwise the runtest-rocq alias will not build. We don't use test-all in CI anyway.

[Alizter]

@Durbatuluk1701 could you ask the Rocq maintainers on Zulip if they intend to change this flag in the future. That would probably give us the clearest path forward.

[Durbatuluk1701]

@Durbatuluk1701 could you ask the Rocq maintainers on Zulip if they intend to change this flag in the future. That would probably give us the clearest path forward.

Asked here

[Durbatuluk1701]

The endorsed fix is:

Always check rocq c --config: it works with 9.0, and if is not planned to get deprecated may be forward and backwards compatible

Which I think should align with what this PR currently contributes

[Alizter]

Could you add a changelog entry?

[Alizter]

Could you also check that we don't mention rocq --config in the documentation? Sometimes there are transient errors with rocq c --config not finding the stdlib, and users may be confused why things are not working (especially if they didn't do any rocq compilation just yet). We should therefore mention somewhere in the manual that the dune rules for rocq are running rocq c --config explicitly to explain.

[Durbatuluk1701]

Could you also check that we don't mention rocq --config in the documentation? Sometimes there are transient errors with rocq c --config not finding the stdlib, and users may be confused why things are not working (especially if they didn't do any rocq compilation just yet). We should therefore mention somewhere in the manual that the dune rules for rocq are running rocq c --config explicitly to explain.

So there is a rocqc --config that appears. This is part of a more general issue in the docs where lots of stuff from the coq -> rocq transformation got slightly off. I was planning to do a docs PR this weekend to clean up a lot of this stuff anyways (i.e. rocqdep -> rocq dep, etc.).

Given this, what would you prefer:

1. I do a full docs update in this PR
2. I do just the --config docs update in this PR and leave the rest for another one
3. Do the full docs update in a separate PR

[Alizter]

@Durbatuluk1701 Let's make the current state of the docs accurately reflect the change you've introduced. I do welcome improvement PRs afterwards in general however.