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

.github/workflows/ci-github.yml

@@ -20,18 +20,18 @@ jobs:
             ocaml: 4.14
             test_disabled:
             # We exclude the coq-core package
-            packages: ./coqide-server.opam ./rocq*.opam
+            packages: ./rocq*.opam
           - name: Windows
             os: windows-latest
             ocaml: 4.14
             test_disabled: misc coq-makefile precomputed-time-tests
             # we don't support rocqide on Windows yet, so we filter it, see #20631
-            packages: ./coqide-server.opam ./rocq-*.opam
+            packages: ./rocqide-server.opam ./rocq-*.opam
           - name: Linux (latest OCaml)
             os: ubuntu-latest
             ocaml: 5.4
             test_disabled:
-            packages: ./coqide-server.opam ./rocq*.opam
+            packages: ./rocq*.opam
       fail-fast: false
 
     name: ${{ matrix.name }}

.gitignore

@@ -57,7 +57,7 @@ config/coq_config.ml
 config/coq_byte_config.ml
 config/coq_config.py
 config/dune.c_flags
-ide/coqide/config.ml
+ide/rocqide/config.ml
 dev/ocamldebug-coq
 coqdoc.sty
 coqdoc.css
@@ -132,9 +132,9 @@ doc/tools/docgram/updated_rsts
 
 # other auto-generated files
 
-ide/coqide/default.bindings
-ide/coqide/default_bindings_src.exe
-ide/coqide/index_urls.txt
+ide/rocqide/default.bindings
+ide/rocqide/default_bindings_src.exe
+ide/rocqide/index_urls.txt
 .lia.cache
 .nia.cache
 .nra.cache
@@ -146,13 +146,14 @@ ide/coqide/index_urls.txt
 # vscode local config
 .vscode/
 
-# coqide generated files (when testing)
+# rocqide generated files (when testing)
 *.crashcoqide
+*.crashrocqide
 
 .*.sw*
 .#*
 
-ide/coqide/coqide.keys
+ide/rocqide/rocqide.keys
 .dune.lock
 
 # bin compat directory, should be eventually be phased out

.gitlab-ci.yml

@@ -86,7 +86,7 @@ before_script:
   script:
     - cp dev/ci/dune-workspace.ci dune-workspace
 
-    - PKGS=rocq-runtime,coq-core,rocq-core,coqide-server,rocq-devtools
+    - PKGS=rocq-runtime,coq-core,rocq-core,rocqide-server,rocq-devtools
     - if [ "$ROCQIDE" != "no" ]; then PKGS=${PKGS},rocqide; fi
     - dev/ci/gitlab-section.sh start coq.clean coq.clean
     - make clean # ensure that `make clean` works on a fresh clone
@@ -251,7 +251,7 @@ before_script:
     - if [ "$ROCQ_CI_NATIVE" = true ]; then echo "Definition f x := x + x." > test_native.v; fi
     - if [ "$ROCQ_CI_NATIVE" = true ]; then rocq c test_native.v; fi
     - if [ "$ROCQ_CI_NATIVE" = true ]; then test -f .coq-native/Ntest_native.cmxs; fi
-    - opam pin add --kind=path coqide-server.dev .
+    - opam pin add --kind=path rocqide-server.dev .
     - opam pin add --kind=path rocqide.dev .
     - opam pin add --kind=path rocq-devtools .
     - opam pin add --kind=path rocq-test-suite.dev . -v
@@ -353,7 +353,7 @@ build:base:dev:dune:
   script:
     - cp theories/Corelib/dune.disabled theories/Corelib/dune
     - cp theories/Ltac2/dune.disabled theories/Ltac2/dune
-    - dune build -p rocq-runtime,coq-core,rocq-core,coqide-server
+    - dune build -p rocq-runtime,coq-core,rocq-core,rocqide-server
     - ls _build/install/default/lib/coq/theories/Init/Prelude.vo
     - ls _build/install/default/lib/coq/user-contrib/Ltac2/Ltac2.vo
   only: *full-ci

INSTALL.md

@@ -87,8 +87,8 @@ for more details.
 To build and install Rocq (and RocqIDE if desired) do:
 
     $ make dunestrap
-    $ dune build -p rocq-runtime,coq-core,rocq-core,coqide-server,rocqide
-    $ dune install --prefix=<install_prefix> rocq-runtime coq-core rocq-core coqide-server rocqide
+    $ dune build -p rocq-runtime,coq-core,rocq-core,rocqide-server,rocqide
+    $ dune install --prefix=<install_prefix> rocq-runtime coq-core rocq-core rocqide-server rocqide
 
 You can drop the `rocqide` packages if not needed.
 

Makefile

@@ -102,7 +102,7 @@ help-install:
 	@echo "  - rocq-runtime: base Rocq package, toplevel compilers, plugins, tools, no corelib, no stdlib, no GTK"
 	@echo "  - coq-core: compat binaries (coqc instead of rocq compile, etc)"
 	@echo "  - rocq-core: Rocq's prelude and corelib"
-	@echo "  - coqide-server: XML protocol language server"
+	@echo "  - rocqide-server: XML protocol language server"
 	@echo "  - rocqide: RocqIDE gtk application"
 	@echo ""
 	@echo " To build a package, you can use:"
@@ -162,7 +162,7 @@ states: world
 	echo "'make states' is an alias for 'make world'"
 
 MAIN_TARGETS:=rocq-runtime.install coq-core.install rocq-core.install \
-  coqide-server.install rocq-devtools.install
+  rocqide-server.install rocq-devtools.install
 
 world: dunestrap
 	+$(WITHJOBS) dune build $(DUNEOPT) $(MAIN_TARGETS)

default.nix

@@ -122,7 +122,7 @@ stdenv.mkDerivation rec {
   # From https://github.com/NixOS/nixpkgs/blob/master/pkgs/build-support/ocaml/dune.nix
   installPhase = ''
     runHook preInstall
-    dune install --prefix $out --libdir $OCAMLFIND_DESTDIR rocq-runtime coq-core rocq-core coqide-server ${optionalString buildIde "rocqide"}
+    dune install --prefix $out --libdir $OCAMLFIND_DESTDIR rocq-runtime coq-core rocq-core rocqide-server ${optionalString buildIde "rocqide"}
     runHook postInstall
   '';
 

dev/bench/bench.sh

@@ -492,7 +492,7 @@ export PROFILING=1
 export ROCQ_PROFILE_COMPONENTS=command,parse_command,partac.perform
 
 # packages tied to the coq commit need to be pinned accordingly
-core_packages='rocq-runtime coq-core rocq-core coqide-server'
+core_packages='rocq-runtime coq-core rocq-core rocqide-server'
 
 for coq_opam_package in $core_packages $coq_opam_packages; do
 
@@ -623,7 +623,7 @@ $coq_opam_package (in $RUNNER)"
     done
 
     case $coq_opam_package in
-      coqide-server|coq)
+      rocqide-server|coq)
         # don't render results for these
         ;;
       *)

dev/ci/platform/coq-pf-03-build.bat

@@ -24,7 +24,7 @@ call coq_platform_make_windows.bat ^
   -override-dev-pkg="rocq-runtime=%GITHUB_SERVER_URL%/%GITHUB_REPOSITORY%/archive/%GITHUB_SHA%.tar.gz" ^
   -override-dev-pkg="rocq-core=%GITHUB_SERVER_URL%/%GITHUB_REPOSITORY%/archive/%GITHUB_SHA%.tar.gz" ^
   -override-dev-pkg="coq-core=%GITHUB_SERVER_URL%/%GITHUB_REPOSITORY%/archive/%GITHUB_SHA%.tar.gz" ^
-  -override-dev-pkg="coqide-server=%GITHUB_SERVER_URL%/%GITHUB_REPOSITORY%/archive/%GITHUB_SHA%.tar.gz" ^
+  -override-dev-pkg="rocqide-server=%GITHUB_SERVER_URL%/%GITHUB_REPOSITORY%/archive/%GITHUB_SHA%.tar.gz" ^
   -override-dev-pkg="rocqide=%GITHUB_SERVER_URL%/%GITHUB_REPOSITORY%/archive/%GITHUB_SHA%.tar.gz" ^
   || GOTO ErrorExit
 

dev/doc/release-process.md

@@ -27,7 +27,7 @@
 - [ ] For major releases, you can create new views in the above project by using the "Duplicate view" button in the menu of the views from the previous major release. After duplicating the view, you can edit the filter to match the field for the new branch, update the fields displayed, rename the view, and "save", so that the view is shared with everyone. This is best done after the first PR requiring backporting has been merged, because the new field will have been created by coqbot at that point.
 - [ ] Pin the versions of libraries and plugins in [`dev/ci/ci-basic-overlay.sh`](../ci/ci-basic-overlay.sh) to use commit hashes. You can use the [`dev/tools/pin-ci.sh`](../tools/pin-ci.sh) script to do this semi-automatically.
 - [ ] In a PR on `master` to be backported, add a new link to the `'versions'` list of the refman (in `html_context` in [`doc/sphinx/conf.py`](../../doc/sphinx/conf.py)). At the same time, update the links of previous versions that were targeting branches to target a tag instead if the latest patch-level release is out.
-- [ ] Add `{rocq-runtime,coq-core,rocq-core,coqide-server}.X.X.dev` packages in [`core-dev`](https://github.com/rocq-prover/opam/tree/master/core-dev)
+- [ ] Add `{rocq-runtime,coq-core,rocq-core,rocqide-server}.X.X.dev` packages in [`core-dev`](https://github.com/rocq-prover/opam/tree/master/core-dev)
 - [ ] Ensure a `rocq-stdlib` package compatible with the new packages above exists either in [`ocaml repo`](https://github.com/ocaml/opam-repository) or in [`core-dev`](https://github.com/rocq-prover/opam/tree/master/core-dev)
 - [ ] Add `coq.X.X.dev` package in [`core-dev`](https://github.com/rocq-prover/opam/tree/master/core-dev)
 - [ ] Ping `@erikmd` and `@Zimmi48` to set up the infrastructure to have alpha Docker images built for the branch: the main steps amount to release `coq-bignums v9.Y.Y+coqX.X` in [`extra-dev`](https://github.com/rocq-prover/opam/tree/master/extra-dev), prepare a new [Docker-Rocq](https://github.com/rocq-community/docker-rocq) image `rocq/rocq-prover:X.X-alpha`, then browse <https://gitlab.inria.fr/coq/coq/-/hooks> to copy the `dev` webhook into a new `vX.X` webhook: `https://gitlab.com/api/v4/projects/19687072/trigger/pipeline?ref=master&variables[CRON_MODE]=rebuild-keyword&variables[ITEM]=X.X&token=_`, Push events → Wildcard pattern → `vX.X`, Test Push events. (If need be, the token can be regenerated at <https://gitlab.com/rocq-community/docker-rocq/-/settings/ci_cd>.)

dev/doc/xml-protocol.md

@@ -165,7 +165,7 @@ state that should become the next tip.
   Note that IDEs may need to convert byte offsets passed in the four position fields of the
   location to character offsets to correctly handle multi-byte characters. Also, due to
   asynchronous evaluation, line number fields of locations may need to be adjusted
-  if the sentence has moved since it was sent to Coqtop.
+  if the sentence has moved since it was sent to Rocqtop.
 
 -------------------------------
 
@@ -958,7 +958,7 @@ Currently these tags are used:
   or elsewhere
 * **prompt** - output for display in the Messages panel prompting the user to
   enter a debug command, allowing RocqIDE to display it without
-  appending a newline.  It also signals that coqidetop is waiting to receive
+  appending a newline.  It also signals that rocqidetop is waiting to receive
   a debugger-specific message such as [Db_cmd](#command-db_cmd).
 
 ```xml

doc/sphinx/practical-tools/coqide.rst

@@ -351,7 +351,8 @@ Preferences and key bindings are saved in the user configuration directory,
 which is ``$XDG_CONFIG_HOME/coq`` if the environment variable ``$XDG_CONFIG_HOME``
 is set.  If the variable isn't set, the directory is ``~/.config/coq`` on Linux
 and `C:\\Users\\<USERNAME>\\AppData\\Local\\coq` on Windows.
-Preferences are in the file `coqiderc` and key bindings are in the file `coqide.keys`.
+Preferences are in the file `rocqiderc` and key bindings are in the file
+`rocqide.keys`.
 
 .. _rocqide_key_bindings:
 
@@ -375,7 +376,7 @@ menu item without releasing the mouse button, pressing the keys you want
 for the new binding and then releasing the mouse button.
 
 Alternatively, you can edit the configuration file directly.
-Key bindings are saved in the file `coqide.keys` in
+Key bindings are saved in the file `rocqide.keys` in
 the :ref:`user configuration directory<user-configuration-directory>`.
 Make sure there are no RocqIDE processes running while you edit the file
 (RocqIDE creates or overwrites the file when it terminates,
@@ -485,9 +486,9 @@ of the preferences.
 Adding custom bindings
 ~~~~~~~~~~~~~~~~~~~~~~
 
-To extend the default set of bindings, create a file named ``coqide.bindings``
+To extend the default set of bindings, create a file named ``rocqide.bindings``
 in the :ref:`user configuration directory<user-configuration-directory>`.
-The file `coqide.bindings` should contain one
+The file `rocqide.bindings` should contain one
 binding per line, in the form ``\key value``, followed by an optional priority
 integer. (The key and value should not contain any space character.)
 
@@ -515,7 +516,7 @@ Each of the file tokens provided may consists of one of:
 
  -  a path to a custom bindings file,
  -  the token ``default``, which resolves to the default bindings file,
- -  the token ``local``, which resolves to the `coqide.bindings` file
+ -  the token ``local``, which resolves to the `rocqide.bindings` file
     stored in the :ref:`user configuration directory <user-configuration-directory>`.
 
 .. warning::

dune

@@ -22,7 +22,7 @@
 
 (alias
  (name default)
- (deps rocq-runtime.install coq-core.install rocq-core.install coqide-server.install))
+ (deps rocq-runtime.install coq-core.install rocq-core.install rocqide-server.install))
 
 (alias
  (name runtime)

dune-project

@@ -115,7 +115,7 @@ by Rocq in every .v file, as well as other modules bound to the
 Corelib.* and Ltac2.* namespaces."))
 
 (package
- (name coqide-server)
+ (name rocqide-server)
  (depends
   (rocq-runtime (= :version)))
  (synopsis "The Rocq Prover, XML protocol server")
@@ -124,7 +124,7 @@ a formal language to write mathematical definitions, executable
 algorithms and theorems together with an environment for
 semi-interactive development of machine-checked proofs.
 
-This package provides the `coqidetop` language server, an
+This package provides the `rocqidetop` language server, an
 implementation of Rocq's [XML protocol](https://github.com/rocq-prover/rocq/blob/master/dev/doc/xml-protocol.md)
 which allows clients, such as RocqIDE, to interact with the Rocq Prover in a
 structured way."))
@@ -135,7 +135,7 @@ structured way."))
   (ocamlfind :build)
   (conf-findutils :build)
   conf-adwaita-icon-theme
-  (coqide-server (= :version))
+  (rocqide-server (= :version))
   (cairo2 (>= 0.6.4))
   (lablgtk3-sourceview3 (and (>= 3.1.2) (or (>= 3.1.5) (<> :os-family "windows")))))
  (synopsis "The Rocq Prover --- GTK3 IDE")
@@ -152,7 +152,7 @@ development of interactive proofs."))
  (allow_empty)
  (depends
   (rocq-core (= :version))
-  coqide-server
+  rocqide-server
   ounit2
   conf-python-3
   conf-time)

ide/rocqide/FAQ

@@ -41,7 +41,7 @@ a module for LaTeX-like inputting.
 
 Q6) How to customize the shortcuts for menus?
 R6) Two solutions are offered:
-  - Edit $XDG_CONFIG_HOME/coq/coqide.keys by hand or
+  - Edit $XDG_CONFIG_HOME/coq/rocqide.keys by hand or
   - If your system allows it, from RocqIDE, you may select a menu entry and press the 
     desired shortcut. 
 

ide/rocqide/Make

@@ -3,4 +3,4 @@ xmlprotocol.mli
 xmlprotocol.ml
 ide_slave.ml
 
-coqidetop.mllib
+rocqidetop.mllib

ide/rocqide/config_lexer.mll

@@ -26,7 +26,7 @@ rule prefs m = parse
   |ignore* (ident as id) ignore* '=' { let conf = str_list [] lexbuf in
                                  prefs (Util.String.Map.add id conf m) lexbuf }
   | _     { let c = lexeme_start lexbuf in
-              eprintf "coqiderc: invalid character (%d)\n@." c;
+              eprintf "rocqiderc: invalid character (%d)\n@." c;
               prefs m lexbuf }
   | eof   { m }
 
@@ -42,7 +42,7 @@ and string = parse
   | '"'  { Buffer.add_char string_buffer '"' }
   | '\\' '"' | _
          { Buffer.add_string string_buffer (lexeme lexbuf); string lexbuf }
-  | eof  { eprintf "coqiderc: unterminated string\n@." }
+  | eof  { eprintf "rocqiderc: unterminated string\n@." }
 
 {
 

ide/rocqide/dune

@@ -3,17 +3,17 @@
 
 (library
  (name core)
- (public_name coqide-server.core)
+ (public_name rocqide-server.core)
  (wrapped false)
  (modules document)
  (libraries rocq-runtime.boot rocq-runtime.lib))
 
 (executable
  (name idetop)
- (public_name coqidetop)
- (package coqide-server)
+ (public_name rocqidetop)
+ (package rocqide-server)
  (modules idetop)
- (libraries rocq-runtime.toplevel coqide-server.protocol platform_specific)
+ (libraries rocq-runtime.toplevel rocqide-server.protocol platform_specific)
  (link_flags -linkall))
 
 ; IDE Client, we may want to add the macos_prehook.ml conditionally.
@@ -25,7 +25,7 @@
  (foreign_stubs
   (language c)
   (names rocqide_os_stubs))
- (libraries coqide-server.protocol coqide-server.core lablgtk3-sourceview3 platform_specific))
+ (libraries rocqide-server.protocol rocqide-server.core lablgtk3-sourceview3 platform_specific))
 
 (library
  (name platform_specific)

ide/rocqide/idetop.ml

@@ -315,7 +315,7 @@ let wait () =
 
 let status force =
   (* We remove the initial part of the current [DirPath.t]
-     (usually Top in an interactive session, cf "coqtop -top"),
+     (usually Top in an interactive session, cf "rocq top -top"),
      and display the other parts (opened sections and modules) *)
   ignore (Stm.finish ~doc:(get_doc ()) : Vernacstate.t);
   if force then Stm.join ~doc:(get_doc ());
@@ -552,7 +552,7 @@ let eval_call c =
 let xml_debug = ref false
 
 (** Message dispatching.
-    Since [coqidetop] starts 1 thread per slave, and each
+    Since [rocqidetop] starts 1 thread per slave, and each
     thread forwards feedback messages from the slave to the GUI on the same
     xml channel, we need mutual exclusion.  The mutex should be per-channel, but
     here we only use 1 channel. *)
@@ -690,10 +690,10 @@ let rec parse = function
   | [] -> []
 
 let rocqidetop_specific_usage = Boot.Usage.{
-  executable_name = "coqidetop";
+  executable_name = "rocqidetop";
   extra_args = "";
   extra_options = "\n\
-coqidetop specific options:\n\
+rocqidetop specific options:\n\
 \n  --xml_formatinclude dir           (idem)\
 \n  --xml_format=Ppcmds    serialize pretty printing messages using the std_ppcmds format\
 \n  --help-XML-protocol    print documentation of the Coq XML protocol\n"
@@ -703,7 +703,7 @@ let islave_parse opts extra_args =
   let open Coqtop in
   let ({ run_mode; color_mode }, stm_opts), extra_args = coqtop_toplevel.parse_extra opts extra_args in
   let extra_args = parse extra_args in
-  (* One of the role of coqidetop is to find the name of buffers to open *)
+  (* One of the role of rocqidetop is to find the name of buffers to open *)
   (* in the command line; Rocqide is waiting these names on stdout *)
   (* (see filter_rocq_opts in rocq.ml), so we send them now *)
   print_string (String.concat "\n" extra_args);

ide/rocqide/ideutils.ml

@@ -297,7 +297,7 @@ let filter_all_files () = GFile.filter
   ~patterns:["*"] ()
 
 let filter_rocq_files () =  GFile.filter
-  ~name:"Coq source code"
+  ~name:"Rocq source code"
   ~patterns:[ "*.v"] ()
 
 let current_dir () = match project_path#get with
@@ -406,7 +406,7 @@ let rocqtop_path () =
       | Some s -> s
       | None ->
         try
-          let new_prog = System.get_toplevel_path "coqidetop" in
+          let new_prog = System.get_toplevel_path "rocqidetop" in
             (* The file exists or it is to be found by path *)
             if Sys.file_exists new_prog ||
                CString.equal Filename.(basename new_prog) new_prog
@@ -417,8 +417,8 @@ let rocqtop_path () =
                   (Filename.dirname new_prog)
                   (Filename.concat "../Resources/bin" (Filename.basename new_prog))
               in if Sys.file_exists in_macos_bundle then in_macos_bundle
-                 else "coqidetop.opt"
-        with Not_found -> "coqidetop.opt"
+                 else "rocqidetop.opt"
+        with Not_found -> "rocqidetop.opt"
   in file
 
 (* In win32, when a command-line is to be executed via cmd.exe