Skip to content

Coqide server renamed to RocqIDE server (coqidetop -> rocqidetop) - #22327

Open
HugoMartel wants to merge 2 commits into
rocq-prover:masterfrom
HugoMartel:rocqide-server
Open

Coqide server renamed to RocqIDE server (coqidetop -> rocqidetop)#22327
HugoMartel wants to merge 2 commits into
rocq-prover:masterfrom
HugoMartel:rocqide-server

Conversation

@HugoMartel

Copy link
Copy Markdown

Changed: coqide-server package name to rocqide-server, its executable from coqidetop to rocqidetop, and some leftover coq mentions in the UI and configuration files of RocqIDE.

I tried to not modify too much (e.g. coq occurences in the source code that will not appear on the UI, or OCaml module names still containing some Coq) otherwise this PR would have been a lot bigger in terms of changes.

I left some boxes unchecked since I am not aware if some software still rely directly on coqidetop, from what I 've seen this is not the case for at least VSRocq and PG ; and didn't test the GitLab CI

  • Added / updated test-suite.
  • Added changelog.
  • Added / updated documentation.
    • Documented any new / changed user messages.
  • Opened overlay pull requests.

@HugoMartel
HugoMartel requested review from a team and Justme0606 as code owners July 30, 2026 17:01
@coqbot-app

coqbot-app Bot commented Jul 30, 2026

Copy link
Copy Markdown
Contributor

I am not triggering a CI run on this PR because the CI configuration has been modified. CI can be triggered manually by an authorized contributor.

@coqbot-app coqbot-app Bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jul 30, 2026
@SkySkimmer

Copy link
Copy Markdown
Contributor

It was deliberately not renamed for backwards compatibility, considering it's not user facing and not the recommended way to interact with rocq.

@HugoMartel

Copy link
Copy Markdown
Author

It was deliberately not renamed for backwards compatibility, considering it's not user facing and not the recommended way to interact with rocq.

Ah I missed that fact from reading the previous renaming PRs. Since I am coming rather from the nixpkgs side of things than this side, I had the false idea that all binaries that contained coq were in fact considered "compatibility" binaries that linked to rocq equivalents (just like coq-makefile, coqtop, etc).

Would a similar coqidetop compatibility package be something of interest? (like the coq-core package in the dune definitions). I am willing to put more work in this PR or another related one if you feel that it may be worth it.

@SkySkimmer

Copy link
Copy Markdown
Contributor

Renaming coqidetop doesn't really seem useful IMO.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants