Rename coqide -> rocqide

SkySkimmer · Jan 14, 2025 · 686cc1f · 686cc1f
1 parent 097d531
commit 686cc1f
Show file tree

Hide file tree

Showing 203 changed files with 596 additions and 609 deletions.
diff --git a/.github/workflows/ci-macos.yml b/.github/workflows/ci-macos.yml
@@ -36,15 +36,15 @@ jobs:
           eval $(opam env)
           ./configure -prefix "$(pwd)/_install_ci" -native-compiler no
           make dunestrap
-          dune build -p rocq-runtime,coq-core,rocq-core,coqide-server,coqide
+          dune build -p rocq-runtime,coq-core,rocq-core,coqide-server,rocqide
         env:
           MACOSX_DEPLOYMENT_TARGET: "10.11"
           NJOBS: "2"
 
       - name: Install Coq
         run: |
           eval $(opam env)
-          dune install --prefix="$(pwd)/_install_ci" rocq-runtime coq-core rocq-core coqide-server coqide
+          dune install --prefix="$(pwd)/_install_ci" rocq-runtime coq-core rocq-core coqide-server rocqide
 
       - name: Run Coq Test Suite
         run: |

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
@@ -70,7 +70,7 @@ before_script:
   interruptible: true
   extends: .auto-use-tags
   variables:
-    COQIDE: "opt"
+    ROCQIDE: "opt"
   artifacts:
     name: "$CI_JOB_NAME"
     paths:
@@ -86,7 +86,7 @@ before_script:
     - cp dev/ci/dune-workspace.ci dune-workspace
 
     - PKGS=rocq-runtime,coq-core,rocq-core,coqide-server
-    - if [ "$COQIDE" != "no" ]; then PKGS=${PKGS},coqide; fi
+    - 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
     - dev/ci/gitlab-section.sh end coq.clean
@@ -115,7 +115,7 @@ before_script:
     - make $DUNE_TARGET
     - tar cfj _build.tar.bz2 _build
   variables:
-    DUNE_TARGET: "world coqide"
+    DUNE_TARGET: "world rocqide"
   artifacts:
     name: "$CI_JOB_NAME"
     when: always
@@ -249,7 +249,7 @@ before_script:
     - if command -v coqc; then exit 1; fi # coq-core didn't get autoinstalled
     - opam pin add --kind=path coq-core.dev .
     - opam pin add --kind=path coqide-server.dev .
-    - opam pin add --kind=path coqide.dev .
+    - opam pin add --kind=path rocqide.dev .
   after_script:
     - eval $(opam env)
     - du -ha "$(coqc -where)" > files.listing
@@ -315,13 +315,13 @@ build:base:
     COQ_EXTRA_CONF: "-native-compiler yes"
   only: *full-ci
 
-# no coqide for 32bit: libgtk installation problems
+# no rocqide for 32bit: libgtk installation problems
 build:base+32bit:
   extends: .build-template
   variables:
     OPAM_VARIANT: "+32bit"
     COQ_EXTRA_CONF: "-native-compiler yes"
-    COQIDE: "no"
+    ROCQIDE: "no"
   only: *full-ci
 
 build:edge+flambda:

diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
@@ -232,7 +232,7 @@ manifesto's README][coq-community-manifesto].
 
 ### Contributing to the editor support packages ###
 
-Besides CoqIDE, whose sources are available in this repository, and to
+Besides Rocqide, whose sources are available in this repository, and to
 which you are welcome to contribute, there are a number of alternative
 user interfaces for Rocq, more often as an editor support package.
 
@@ -294,7 +294,7 @@ GitHub account).  You can file a bug for any of the following:
   find or don't understand some bit of documentation.
 - An error message that wasn't as helpful as you'd like. Bonus points
   for suggesting what information would have helped you.
-- Bugs in CoqIDE should also be filed in the [Rocq issue
+- Bugs in Rocqide should also be filed in the [Rocq issue
   tracker][Rocq-issue-tracker].  Bugs in the Emacs plugin should be
   filed against [ProofGeneral][ProofGeneral-issues], or against
   [company-coq][company-coq-issues] if they are specific to

diff --git a/INSTALL.md b/INSTALL.md
@@ -34,7 +34,7 @@ To compile Rocq yourself, you need:
   ties to even as default rounding mode (most architectures
   should work nowadays)
 
-- for CoqIDE, the
+- for RocqIDE, the
   [lablgtk3-sourceview3](https://github.com/garrigue/lablgtk) library
   (version >= 3.1.2), and the corresponding GTK 3.x libraries, as
   of today (gtk+3 >= 3.18 and gtksourceview3 >= 3.18)
@@ -55,7 +55,7 @@ this moment) must be properly registered with `findlib/ocamlfind`
 since Rocq's build system uses `findlib` to locate them.
 
 Debian / Ubuntu users can get the necessary system packages for
-CoqIDE with:
+RocqIDE with:
 
     $ sudo apt-get install libgtksourceview-3.0-dev
 
@@ -87,14 +87,14 @@ but final users must always use the release build. See
 [dev/doc/build-system.dune.md](dev/doc/build-system.dune.md)
 for more details.
 
-To build and install Rocq (and CoqIDE if desired) do:
+To build and install Rocq (and RocqIDE if desired) do:
 
     $ ./configure -prefix <install_prefix> $options
     $ make dunestrap
-    $ dune build -p rocq-runtime,coq-core,rocq-core,coq,coqide-server,coqide
-    $ dune install --prefix=<install_prefix> rocq-runtime coq-core rocq-core coq coqide-server coqide
+    $ dune build -p rocq-runtime,coq-core,rocq-core,coq,coqide-server,rocqide
+    $ dune install --prefix=<install_prefix> rocq-runtime coq-core rocq-core coq coqide-server rocqide
 
-You can drop the `coqide` packages if not needed.
+You can drop the `rocqide` packages if not needed.
 
 Packagers may want to play with `dune install` options as to tweak
 installation path, the `-prefix` argument in `./configure` tells Rocq

diff --git a/Makefile b/Makefile
@@ -10,7 +10,7 @@
 
 # Dune Makefile for Rocq
 
-.PHONY: help help-install states world coqide watch check    # Main developer targets
+.PHONY: help help-install states world rocqide watch check    # Main developer targets
 .PHONY: refman-html refman-pdf corelib-html apidoc     # Documentation targets
 .PHONY: test-suite dev-targets
 .PHONY: fmt ocheck obuild ireport clean               # Maintenance targets
@@ -39,9 +39,9 @@ help:
 	@echo "make help-install for installation instructions. Common developer targets are:"
 	@echo ""
 	@echo "  - states: build a minimal functional rocq repl"
-	@echo "  - world:  build main public binaries and libraries in developer mode (no coqide)"
+	@echo "  - world:  build main public binaries and libraries in developer mode (no rocqide)"
 	@echo "  - watch:  build main public binaries and libraries [continuous build]"
-	@echo "  - coqide: build coqide binary in developer mode"
+	@echo "  - rocqide: build rocqide binary in developer mode"
 	@echo "  - check:  build all ML files as fast as possible"
 	@echo "  - test-suite: run Rocq's test suite [env NJOBS=N to set job parallelism]"
 	@echo "  - dunestrap: Generate the dune rules for vo files"
@@ -51,7 +51,7 @@ help:
 	@echo "  Note: these targets produce a developer build, not suitable"
 	@echo "        for distribution to end-users or install"
 	@echo ""
-	@echo " To run an \$$app \\in {coqc,coqtop,coqtop.byte,coqide}:"
+	@echo " To run an \$$app \\in {coqc,coqtop,coqtop.byte,rocqide}:"
 	@echo ""
 	@echo "  - use 'dune exec -- dev/shim/\$$app args'"
 	@echo "    Example: 'dune exec -- dev/shim/coqc file.v'"
@@ -100,7 +100,7 @@ help-install:
 	@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 "  - coqide: CoqIDE gtk application"
+	@echo "  - rocqide: RocqIDE gtk application"
 	@echo "  - rocq: meta package depending on rocq-runtime rocq-core rocq-stdlib"
 	@echo "    (also calls the test suite when using --with-test)"
 	@echo "  - coq: meta package depending on rocq coq-core coq-stdlib"
@@ -167,8 +167,8 @@ MAIN_TARGETS:=rocq-runtime.install coq-core.install rocq-core.install coqide-ser
 world: dunestrap
 	dune build $(DUNEOPT) $(MAIN_TARGETS)
 
-coqide:
-	dune build $(DUNEOPT) coqide.install
+rocqide:
+	dune build $(DUNEOPT) rocqide.install
 
 watch:
 	dune build $(DUNEOPT) $(MAIN_TARGETS) -w
@@ -282,9 +282,9 @@ $(foreach subdir,$(wildcard theories/*/),$(eval $(call subtarget,$(subdir),$(she
 #
 # dune build rocq-runtime.install
 # dune build coq.install
-# dune build coqide.install
+# dune build rocqide.install
 #
 # Packaging / OPAM targets:
 #
 # dune -p coq @install
-# dune -p coqide @install
+# dune -p rocqide @install
diff --git a/config/coq_config.mli b/config/coq_config.mli
@@ -28,7 +28,7 @@ val ocamlfind : string
 (* used in envars for coq_makefile *)
 val caml_flags : string     (* arguments passed to ocamlc (ie. CAMLFLAGS) *)
 
-(* Used in coqide *)
+(* Used in rocqide *)
 val arch : string       (* architecture *)
 
 (* dubious use in envars, use in coqmakefile *)
@@ -45,7 +45,7 @@ val all_src_dirs : string list
 (* Used in micromega *)
 val exec_extension : string (* "" under Unix, ".exe" under MS-windows *)
 
-(* Used in coqide *)
+(* Used in rocqide *)
 val browser : string
 (** default web browser to use, may be overridden by environment
     variable COQREMOTEBROWSER *)
@@ -57,7 +57,7 @@ val has_natdynlink : bool
 val wwwcoq : string
 val wwwstdlib : string
 
-(* used in coqide *)
+(* used in rocqide *)
 val wwwrefman : string
 
 (* for error reporting *)

diff --git a/coqide-server.opam b/coqide-server.opam
@@ -10,7 +10,7 @@ semi-interactive development of machine-checked proofs.
 
 This package provides the `coqidetop` language server, an
 implementation of Coq's [XML protocol](https://github.com/coq/coq/blob/master/dev/doc/xml-protocol.md)
-which allows clients, such as CoqIDE, to interact with Coq in a
+which allows clients, such as RocqIDE, to interact with Coq in a
 structured way."""
 maintainer: ["The Rocq development team <[email protected]>"]
 authors: ["The Rocq development team, INRIA, CNRS, and contributors"]

diff --git a/default.nix b/default.nix
@@ -1,7 +1,7 @@
 # How to use?
 
 # If you have Nix installed, you can get in an environment with everything
-# needed to compile Rocq and CoqIDE by running:
+# needed to compile Rocq and RocqIDE by running:
 # $ nix-shell
 # at the root of the Rocq repository.
 
@@ -111,7 +111,7 @@ stdenv.mkDerivation rec {
 
   enableParallelBuilding = true;
 
-  buildFlags = [ "world" ] ++ optional buildIde "coqide";
+  buildFlags = [ "world" ] ++ optional buildIde "rocqide";
 
   # TODO, building of documentation package when not in dev mode
   # https://github.com/coq/coq/issues/16198
@@ -120,7 +120,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 "coqide"}
+    dune install --prefix $out --libdir $OCAMLFIND_DESTDIR rocq-runtime coq-core rocq-core coqide-server ${optionalString buildIde "rocqide"}
     runHook postInstall
   '';
 

diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md
@@ -8,7 +8,7 @@ unless these tests pass.
 We are currently running tests on the following platforms:
 
 - GitLab CI is the main CI platform. It tests the compilation of Rocq,
-  of the documentation, and of CoqIDE on Linux with several versions
+  of the documentation, and of RocqIDE on Linux with several versions
   of OCaml and with warnings as errors; it runs the test-suite and
   tests the compilation of several external developments. It also runs
   a linter that checks whitespace discipline. A [pre-commit

diff --git a/dev/ci/platform/coq-pf-03-build.bat b/dev/ci/platform/coq-pf-03-build.bat
@@ -27,7 +27,7 @@ call coq_platform_make_windows.bat ^
   -override-dev-pkg="coq-core=%GITHUB_SERVER_URL%/%GITHUB_REPOSITORY%/archive/%GITHUB_SHA%.tar.gz" ^
   -override-dev-pkg="coq=%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="coqide=%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
 
 GOTO :EOF

diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md
@@ -106,21 +106,21 @@ Dune will read the file `~/.config/dune/config`; see `man
 dune-config`. Among others, you can set in this file the custom number
 of build threads `(jobs N)` and display options `(display _mode_)`.
 
-## Running binaries [coqtop / coqide]
+## Running binaries [coqtop / rocqide]
 
 Running `coqtop` directly with `dune exec -- coqtop` won't in general
 work well unless you are using `dune exec -- coqtop -noinit`. The
 `coqtop` binary doesn't depend itself on Rocq's prelude, so plugins /
 vo files may go stale if you rebuild only `coqtop`.
 
 Instead, you should use the provided "shims" for running `coqtop` and
-`coqide` in a fast build. In order to use them, do:
+`rocqide` in a fast build. In order to use them, do:
 
 ```
 $ dune exec -- dev/shim/coqtop
 ```
 
-or `quickide` / `dev/shim/coqide` for CoqIDE, etc.... See `dev/shim/dune` for a
+or `quickide` / `dev/shim/rocqide` for RocqIDE, etc.... See `dev/shim/dune` for a
 complete list of targets. These targets enjoy quick incremental compilation
 thanks to `-opaque` so they tend to be very fast while developing.
 
@@ -207,7 +207,7 @@ dune exec -- dev/dune-dbg coqc foo.v
 (ocd) source db
 ```
 
-to start `coqc.byte foo.v`, other targets are `{checker,coqide,coqtop}`:
+to start `coqc.byte foo.v`, other targets are `{checker,rocqide,coqtop}`:
 
 ```
 dune exec -- dev/dune-dbg checker foo.vo
@@ -257,10 +257,10 @@ plugin will correctly track dependencies and rebuild incrementally as
 needed.
 
 However, it is not always desirable to go this way. For example, the
-current Rocq source tree contains two packages [Rocq and CoqIDE], and in
-the OPAM CoqIDE package we don't want to build CoqIDE against the
+current Rocq source tree contains two packages [Rocq and RocqIDE], and in
+the OPAM RocqIDE package we don't want to build RocqIDE against the
 local copy of Rocq. For this purpose, Dune supports the `-p` option, so
-`dune build -p coqide` will build CoqIDE against the system-installed
+`dune build -p rocqide` will build RocqIDE against the system-installed
 version of Rocq libs, and use a "release" profile that for example
 enables stronger compiler optimizations.
 
@@ -316,7 +316,7 @@ useful to Rocq, some examples are:
 
   You are likely running a partial build which doesn't include
   implicitly loaded plugins / vo files. See the "Running binaries
-  [coqtop / coqide]" section above as to how to correctly call Rocq's
+  [coqtop / rocqide]" section above as to how to correctly call Rocq's
   binaries.
 
 ## Dune cheat sheet

diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md
@@ -5,7 +5,7 @@ for his [vscoq](https://github.com/coq-community/vscoq/) project.
 
 Here, the aim is to provide a "hands on" description of the XML
 protocol that coqtop and IDEs use to communicate. The protocol first appeared 
-with Coq 8.5, and is used by CoqIDE, [vscoq](https://github.com/coq-community/vscoq/), and other user interfaces.
+with Coq 8.5, and is used by RocqDE, [vscoq legacy](https://github.com/coq-community/vscoq-legacy/), and other user interfaces.
 
 A somewhat out-of-date description of the async state machine is
 [documented here](https://github.com/ejgallego/jscoq/blob/v8.16/etc/notes/coq-notes.md).
@@ -331,7 +331,7 @@ many there are.
 -------------------------------
 
 ### <a name="command-status">**Status(force: bool)**</a>
-Returns information about the current proofs. CoqIDE typically sends this
+Returns information about the current proofs. RocqIDE typically sends this
 message with `force = false` after each sentence, and with `force = true` if
 the user wants to force the checking of all proofs (wheels button). In terms of
 the STM API, `force` triggers a `Join`.
@@ -544,7 +544,7 @@ Sends a list of option settings, where each setting roughly looks like:
   </list>
 </call>
 ```
-CoqIDE sends the following settings (defaults in parentheses):
+RocqIDE sends the following settings (defaults in parentheses):
 ```
 Printing Width : (<option_value val="intvalue"><int>60</int></option_value>),
 Printing Coercions : (<option_value val="boolvalue"><bool val="false"/></option_value>),
@@ -705,7 +705,7 @@ processed when Coq is no longer busy or execution stops in the debugger.
   <list>
     <pair>
       <pair>
-        <string>/home/proj/coq/ide/coqide/debug.v</string>
+        <string>/home/proj/coq/ide/rocqide/debug.v</string>
         <int>22</int>
       </pair>
       <bool val="true"/>
@@ -957,7 +957,7 @@ Currently these tags are used:
 * **goal** - the current goal for the debugger, for display in the Messages panel
   or elsewhere
 * **prompt** - output for display in the Messages panel prompting the user to
-  enter a debug command, allowing CoqIDE to display it without
+  enter a debug command, allowing RocqIDE to display it without
   appending a newline.  It also signals that coqidetop is waiting to receive
   a debugger-specific message such as [Db_cmd](#command-db_cmd).
 
@@ -984,8 +984,8 @@ There are 4 tags that indicate how the enclosed text should be highlighted:
 - diff.added.bg - unchanged text in a line that has additions ("bg" for "background")
 - diff.removed.bg - unchanged text in a line that has removals
 
-CoqIDE, Proof General and coqtop currently use 2 shades of green and 2 shades of red
-as the background color for highlights.  Coqtop and CoqIDE also apply underlining and/or
+RocqIDE, Proof General and coqtop currently use 2 shades of green and 2 shades of red
+as the background color for highlights.  Coqtop and RocqIDE also apply underlining and/or
 strikeout highlighting for the sake of the color blind.
 
 For example, `<diff.added>ABC</diff.added>` indicates that "ABC" should be highlighted

diff --git a/dev/dune b/dev/dune
@@ -24,7 +24,7 @@
     ../checker/coqchk.bc
     ../topbin/rocqworker.bc
     ../topbin/rocqnative.bc
-    ../ide/coqide/rocqide_main.bc
+    ../ide/rocqide/rocqide_main.bc
     ; We require all the OCaml libs to be in place and searchable
     ; by OCamlfind, this is a bit of a hack but until Dune gets
     ; proper ocamldebug support we have to live with that.