diff --git a/.github/workflows/ci-github.yml b/.github/workflows/ci-github.yml index 488b7dd2768e..5ad1cda84626 100644 --- a/.github/workflows/ci-github.yml +++ b/.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 }} diff --git a/.gitignore b/.gitignore index 829e0075be7c..9ea3a83bf148 100644 --- a/.gitignore +++ b/.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 diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 511c6a533dab..0f7525c1d8a5 100644 --- a/.gitlab-ci.yml +++ b/.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 diff --git a/INSTALL.md b/INSTALL.md index 6f815bda4bdb..f79bd77cf58a 100644 --- a/INSTALL.md +++ b/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= rocq-runtime coq-core rocq-core coqide-server rocqide + $ dune build -p rocq-runtime,coq-core,rocq-core,rocqide-server,rocqide + $ dune install --prefix= rocq-runtime coq-core rocq-core rocqide-server rocqide You can drop the `rocqide` packages if not needed. diff --git a/Makefile b/Makefile index f50763ef674a..c6577d428ee9 100644 --- a/Makefile +++ b/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) diff --git a/default.nix b/default.nix index 26b7883dce4f..cd7b1253814f 100644 --- a/default.nix +++ b/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 ''; diff --git a/dev/bench/bench.sh b/dev/bench/bench.sh index 70017e45dfd5..9a9d5e04d836 100755 --- a/dev/bench/bench.sh +++ b/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 ;; *) diff --git a/dev/ci/platform/coq-pf-03-build.bat b/dev/ci/platform/coq-pf-03-build.bat index dd399cd3da4a..440b12ab2dc8 100644 --- a/dev/ci/platform/coq-pf-03-build.bat +++ b/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 diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md index bb9c42180737..9d3d74d4db87 100644 --- a/dev/doc/release-process.md +++ b/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 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 .) diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md index b18874901a81..0b9c66438de9 100644 --- a/dev/doc/xml-protocol.md +++ b/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 diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index 767061fbf787..def07a016f05 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/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\\\\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`. 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`. -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 `. .. warning:: diff --git a/dune b/dune index 8e41a31c3451..b85b1df7073e 100644 --- a/dune +++ b/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) diff --git a/dune-project b/dune-project index 714bc1ceffbe..12fe847d48b2 100644 --- a/dune-project +++ b/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) diff --git a/ide/rocqide/FAQ b/ide/rocqide/FAQ index 1f8bd0ab170e..003465527ac2 100644 --- a/ide/rocqide/FAQ +++ b/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. diff --git a/ide/rocqide/Make b/ide/rocqide/Make index c0881ca3926f..b737555da117 100644 --- a/ide/rocqide/Make +++ b/ide/rocqide/Make @@ -3,4 +3,4 @@ xmlprotocol.mli xmlprotocol.ml ide_slave.ml -coqidetop.mllib +rocqidetop.mllib diff --git a/ide/rocqide/config_lexer.mll b/ide/rocqide/config_lexer.mll index 9a22ee670d3d..b89f78f4058f 100644 --- a/ide/rocqide/config_lexer.mll +++ b/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@." } { diff --git a/ide/rocqide/dune b/ide/rocqide/dune index f24e2c1dde44..dd114a3ce0cb 100644 --- a/ide/rocqide/dune +++ b/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) diff --git a/ide/rocqide/idetop.ml b/ide/rocqide/idetop.ml index 07c3c0eb646b..935a52271bdf 100644 --- a/ide/rocqide/idetop.ml +++ b/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); diff --git a/ide/rocqide/ideutils.ml b/ide/rocqide/ideutils.ml index ca0662ce86c5..b81eeb01c3f4 100644 --- a/ide/rocqide/ideutils.ml +++ b/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 diff --git a/ide/rocqide/preferences.ml b/ide/rocqide/preferences.ml index 5a8a8863ca50..9f89e343089d 100644 --- a/ide/rocqide/preferences.ml +++ b/ide/rocqide/preferences.ml @@ -249,7 +249,7 @@ let get_config_file dirs name = Filename.concat config_dir name let get_unicode_bindings_local_file () = - try Some (get_config_file [Minilib.rocqide_config_home ()] "coqide.bindings") + try Some (get_config_file [Minilib.rocqide_config_home ()] "rocqide.bindings") with Not_found -> None let get_unicode_bindings_default_file () = @@ -606,8 +606,8 @@ let diffs = (** Loading/saving preferences *) -let pref_file = Filename.concat (Minilib.rocqide_config_home ()) "coqiderc" -let accel_file = Filename.concat (Minilib.rocqide_config_home ()) "coqide.keys" +let pref_file = Filename.concat (Minilib.rocqide_config_home ()) "rocqiderc" +let accel_file = Filename.concat (Minilib.rocqide_config_home ()) "rocqide.keys" let accel_regex = Str.regexp {|\(; \|\)(gtk_accel_path "\([^""]*\)"|} @@ -628,7 +628,7 @@ let save_accel_pref () = mkdir_p (Minilib.rocqide_config_home ()) 0o700; let tmp_file, fd = Filename.open_temp_file ?perms:(Some 0o644) ?temp_dir:(Some (Filename.dirname accel_file)) - "coqide.keys_" "" in + "rocqide.keys_" "" in close_out fd; GtkData.AccelMap.save tmp_file; (* AccelMap.save writes entries in random order, so sort them: *) @@ -644,7 +644,7 @@ let save_accel_pref () = map := CString.Map.add key line !map else begin if not (CString.Map.is_empty !map) then begin - Minilib.log ("Unknown format for coqide.keys; sorting skipped"); + Minilib.log ("Unknown format for rocqide.keys; sorting skipped"); raise UnknownFormat end; top_lines := line :: !top_lines @@ -700,7 +700,7 @@ let load_pref_file loader warn name = warn ~delay:5000 ("No " ^ name ^ ", using default internal configuration") let load_accel_pref ~warn = - load_pref_file GtkData.AccelMap.load warn "coqide.keys" + load_pref_file GtkData.AccelMap.load warn "rocqide.keys" let load_rc_pref ~warn = let loader file = @@ -711,7 +711,7 @@ let load_rc_pref ~warn = else unknown_preferences := Util.String.Map.add name v !unknown_preferences in Util.String.Map.iter iter m in - load_pref_file loader warn "coqiderc"; + load_pref_file loader warn "rocqiderc"; attach_modifiers_callback () let load_pref ~warn = diff --git a/ide/rocqide/preferences_ui.ml b/ide/rocqide/preferences_ui.ml index 189bd0f82877..1304d716e072 100644 --- a/ide/rocqide/preferences_ui.ml +++ b/ide/rocqide/preferences_ui.ml @@ -625,7 +625,7 @@ let configure ?(apply = fun () -> ()) parent = in let externals_cmds = create_pref_box ~in_grid:true "Commands for external programs" [ - ptextexpr "coqidetop:" + ptextexpr "rocqidetop:" (match cmd_rocqtop#get with | None -> "AUTO" | Some x -> x) (fun s -> cmd_rocqtop#set (if s = "AUTO" then None else Some s)); pstring "coqc:" cmd_rocqc; @@ -641,7 +641,7 @@ let configure ?(apply = fun () -> ()) parent = let misc = create_pref_box "Miscellaneous" [ pbool "Stop interpreting before the current point" stop_before; - pbool "Reset coqtop on tab switch" reset_on_tab_switch; + pbool "Reset rocqtop on tab switch" reset_on_tab_switch; ] in diff --git a/ide/rocqide/protocol/dune b/ide/rocqide/protocol/dune index 955f12f545c9..102c8428ed5d 100644 --- a/ide/rocqide/protocol/dune +++ b/ide/rocqide/protocol/dune @@ -1,6 +1,6 @@ (library (name protocol) - (public_name coqide-server.protocol) + (public_name rocqide-server.protocol) (wrapped false) (modules_without_implementation interface) (libraries rocq-runtime.lib)) diff --git a/ide/rocqide/rocqDriver.ml b/ide/rocqide/rocqDriver.ml index 19200a524680..7ce13039f2a7 100644 --- a/ide/rocqide/rocqDriver.ml +++ b/ide/rocqide/rocqDriver.ml @@ -77,7 +77,7 @@ let rocq_error_popup ~code ~msg data = callback () let connection_error cmd lines exn = - rocq_error_popup ~code:1 ~msg:"Connection with coqtop failed!" + rocq_error_popup ~code:1 ~msg:"Connection with rocqtop failed!" [ "Command", cmd; "Answer", (String.concat "\n" lines); @@ -85,7 +85,7 @@ let connection_error cmd lines exn = ] let display_rocqtop_answer cmd lines = - rocq_error_popup ~code:0 ~msg:"The coqtop process has exited." + rocq_error_popup ~code:0 ~msg:"The rocqtop process has exited." [ "Command", cmd; "Answer", String.concat "\n" lines; @@ -110,7 +110,7 @@ let rec filter_rocq_opts args = and asks_for_rocqtop args = let pb_mes = GWindow.message_dialog - ~message:"Failed to load coqidetop. Reset the preference to default?" + ~message:"Failed to load rocqidetop. Reset the preference to default?" ~message_type:`QUESTION ~buttons:GWindow.Buttons.yes_no () in match pb_mes#run () with | `YES -> @@ -120,7 +120,7 @@ and asks_for_rocqtop args = filter_rocq_opts args | `DELETE_EVENT | `NO -> let file = select_file_for_open - ~title:"coqidetop to execute (edit your preference then)" + ~title:"rocqidetop to execute (edit your preference then)" ~filter:false ~filename:(rocqtop_path ()) () in match file with @@ -450,7 +450,7 @@ let rec respawn_rocqtop ?(why=Unexpected) rocqtop = let title = "Warning" in let icon = (warn_image ())#coerce in let buttons = ["Reset"; "Save all and quit"; "Quit without saving"] in - let ans = GToolbox.question_box ~title ~buttons ~icon (rocqtop.basename ^ ": coqidetop died.") in + let ans = GToolbox.question_box ~title ~buttons ~icon (rocqtop.basename ^ ": rocqidetop died.") in if ans = 2 then (!save_all (); GtkMain.Main.quit ()) else if ans = 3 then GtkMain.Main.quit () | Planned -> () diff --git a/ide/rocqide/rocqOps.ml b/ide/rocqide/rocqOps.ml index 41a45ef0f69e..91660cf950fe 100644 --- a/ide/rocqide/rocqOps.ml +++ b/ide/rocqide/rocqOps.ml @@ -788,7 +788,7 @@ object(self) let fill_queue = RocqDriver.lift (fun () -> let queue = Queue.create () in (* Lock everything and fill the waiting queue *) - Ideutils.push_info "Coq is computing"; + Ideutils.push_info "Rocq is computing"; messages#default_route#clear; script#set_editable false; self#fill_command_queue until queue; @@ -965,7 +965,7 @@ object(self) Minilib.log("backtrack_to_id "^Stateid.to_string to_id^ " (unfocus_needed="^string_of_bool unfocus_needed^")"); let opening () = - Ideutils.push_info "Coq is undoing" in + Ideutils.push_info "Rocq is undoing" in let conclusion () = Ideutils.pop_info (); if move_insert then begin @@ -1083,7 +1083,7 @@ object(self) let get_initial_state = let next = function | Fail (_, _, message) -> - let message = "Couldn't initialize coqtop\n\n" ^ (Pp.string_of_ppcmds message) in + let message = "Couldn't initialize rocqtop\n\n" ^ (Pp.string_of_ppcmds message) in let popup = GWindow.message_dialog ~buttons:GWindow.Buttons.ok ~message_type:`ERROR ~message () in ignore (popup#run ()); exit 1 | Good id -> initial_state <- id; RocqDriver.return () in diff --git a/ide/rocqide/rocqide.ml b/ide/rocqide/rocqide.ml index d78c32e9c20d..1ca103a280c4 100644 --- a/ide/rocqide/rocqide.ml +++ b/ide/rocqide/rocqide.ml @@ -1836,7 +1836,7 @@ let read_rocqide_args argv = set_debug (); filter_rocqtop rocqtop project_files bindings_files out args |"-xml-debug"::args -> - (* xml_debug ref only exists in coqidetop *) + (* xml_debug ref only exists in rocqidetop *) filter_rocqtop rocqtop project_files bindings_files ("-xml-debug"::out) args |"-coqtop-flags" :: flags :: args-> RocqDriver.ideslave_rocqtop_flags := Some flags; diff --git a/rocq-test-suite.opam b/rocq-test-suite.opam index 4dd35cc0b9c8..982833f84942 100644 --- a/rocq-test-suite.opam +++ b/rocq-test-suite.opam @@ -26,7 +26,7 @@ bug-reports: "https://github.com/rocq-prover/rocq/issues" depends: [ "dune" {>= "3.21"} "rocq-core" {= version} - "coqide-server" + "rocqide-server" "ounit2" "conf-python-3" "conf-time" diff --git a/coqide-server.opam b/rocqide-server.opam similarity index 95% rename from coqide-server.opam rename to rocqide-server.opam index 39e6f090e6e7..980190509655 100644 --- a/coqide-server.opam +++ b/rocqide-server.opam @@ -8,7 +8,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.""" diff --git a/rocqide.opam b/rocqide.opam index 8a1063d44e8a..19263356379e 100644 --- a/rocqide.opam +++ b/rocqide.opam @@ -23,7 +23,7 @@ depends: [ "ocamlfind" {build} "conf-findutils" {build} "conf-adwaita-icon-theme" - "coqide-server" {= version} + "rocqide-server" {= version} "cairo2" {>= "0.6.4"} "lablgtk3-sourceview3" {>= "3.1.2" & (>= "3.1.5" | os-family != "windows")} "odoc" {with-doc} diff --git a/test-suite/Makefile b/test-suite/Makefile index 925a9e98fae2..51a48b852b1a 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -101,7 +101,7 @@ coqchk := $(BIN)rocqchk -R prerequisite TestSuite coqdoc := $(BIN)rocq doc coqtop := $(BIN)rocq repl -q -test-mode -R prerequisite TestSuite -coqidetop := $(BIN)coqidetop +coqidetop := $(BIN)rocqidetop # async proofs off because the output order ends up different with and without async coqc_interactive := $(coqc) -test-mode -async-proofs off @@ -700,7 +700,7 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake)) ide/fake_ide.exe : ide/fake_ide.ml $(SHOW) 'OCAMLC $<' - $(HIDE)$(OCAMLBEST) -linkpkg -package coqide-server.protocol -package coqide-server.core $< -o $@ + $(HIDE)$(OCAMLBEST) -linkpkg -package rocqide-server.protocol -package rocqide-server.core $< -o $@ %.fake.log : %.fake ide/fake_ide.exe $(SHOW) "TEST $<" diff --git a/test-suite/dune b/test-suite/dune index 44c8049dac43..5c25db68a0e4 100644 --- a/test-suite/dune +++ b/test-suite/dune @@ -29,7 +29,7 @@ (package rocq-runtime) (package coq-core) (package rocq-core) - (package coqide-server) ; For fake_ide + (package rocqide-server) ; For fake_ide (package rocq-devtools) ; For bench-render (source_tree .)) ; Finer-grained dependencies would look like this and be generated diff --git a/test-suite/ide/fake_ide.ml b/test-suite/ide/fake_ide.ml index dc17a4a49d69..e0e0984ebd99 100644 --- a/test-suite/ide/fake_ide.ml +++ b/test-suite/ide/fake_ide.ml @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** Fake_ide : Simulate a [rocqide] talking to a [coqidetop]. *) +(** Fake_ide : Simulate a [rocqide] talking to a [rocqidetop]. *) let error s = prerr_endline ("fake_ide: error: "^s); @@ -302,7 +302,7 @@ let grammar = let read_command inc = Parser.parse grammar inc let usage () = - prerr_endline (Printf.sprintf "Usage: %s COQIDETOP ( file | - ) [ \"\" ]\n\ + prerr_endline (Printf.sprintf "Usage: %s ROCQIDETOP ( file | - ) [ \"\" ]\n\ Input syntax is:\n%s\n" (Filename.basename Sys.argv.(0)) (Parser.print grammar)); @@ -313,7 +313,7 @@ module Rocqide = Spawn.Sync () let main = if Sys.os_type = "Unix" then Sys.set_signal Sys.sigpipe (Sys.Signal_handle - (fun _ -> prerr_endline "Broken Pipe (coqtop died ?)"; exit 1)); + (fun _ -> prerr_endline "Broken Pipe (rocqtop died ?)"; exit 1)); let idetop_name, input_file, args = match Sys.argv with | [| _; p; f |] -> p, f, [] | [| _; p; f; args |] ->