RocqIDE external command defaults still use compatibility Coq binaries

[zhaob1n]

Description

RocqIDE still defaults to several legacy Coq command names for external commands, even though the Rocq CLI provides corresponding rocq subcommands.

In ide/rocqide/preferences.ml, the defaults are currently:

let cmd_rocqc =
  new preference ~name:["cmd_coqc"] ~init:"coqc" ~repr:Repr.(string)

let cmd_rocqmakefile =
  new preference ~name:["cmd_coqmakefile"]
    ~init:"coq_makefile -o makefile *.v" ~repr:Repr.(string)

let cmd_rocqdoc =
  new preference ~name:["cmd_coqdoc"]
    ~init:"coqdoc -q -g" ~repr:Repr.(string)

Compile buffer then directly uses cmd_rocqc, so with the default preferences RocqIDE runs coqc rather than rocq compile.

The preferences UI also still exposes these commands using names such as coqc:, coqmakefile:, and coqdoc:.

Documentation inconsistency

The current RocqIDE manual says that Compile buffer compiles the current buffer with:

rocq compile

So the documented behavior and the current default configuration appear to disagree.

Suggested change

Would it make sense for RocqIDE to use the Rocq CLI commands as its defaults?

For example:

coqc              -> rocq compile
coq_makefile ...  -> rocq makefile ...
coqdoc ...        -> rocq doc ...

The old commands can of course remain available as compatibility binaries through coq-core; this issue is only about what RocqIDE itself uses by default.

The persisted preference names (cmd_coqc, cmd_coqmakefile, etc.) may need to remain supported for compatibility with existing RocqIDE configuration files, even if the displayed labels or defaults are updated.

Context

This looks like a remaining part of the staged Coq → Rocq migration:

• Rocq CLI #19927 introduced the Rocq CLI, including mappings such as:

  • coqc → rocq compile
  • coqdoc → rocq doc
  • coq_makefile → rocq makefile
    and explicitly kept the old commands as compatibility binaries.

• Rename coqide -> rocqide #20036 renamed coqide to rocqide.

• Coqide server renamed to RocqIDE server (coqidetop -> rocqidetop) #22327 renamed the IDE server from coqidetop to rocqidetop and cleaned up additional user-visible Coq naming.

Updating RocqIDE's external-command defaults seems like another small step in the same migration.

[HugoMartel]

Just a small precision about the rocqide-server renaming, only the opam derivation using the coqide-server was renamed in the end, not the binary produced by the opam derivation which still is coqidetop (the initial intent of the PR was to rename it indeed).

More details here:

• Coqide server renamed to RocqIDE server (coqidetop -> rocqidetop) #22327 (comment)
• https://github.com/HugoMartel/rocq/blob/13347054515936a6b04f7237a601e430a108bc12/doc/changelog/10-rocqide/22327-rocqide-server-Changed.rst

[ppedrot]

Honestly these commands are essentially unusable and don't play well with the project organization found nowadays in the typical Rocq developement, and I'm not even talking about the cardinality of the set of users of RocqIDE. I'd recommend removing those rather than trying to beat a dead horse.