From 686cc1f4b5e6687a355425c2049d9c1b3aecc9b3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 13 Jan 2025 14:29:11 +0100 Subject: [PATCH] Rename coqide -> rocqide --- .github/workflows/ci-macos.yml | 4 +- .gitlab-ci.yml | 12 +- CONTRIBUTING.md | 4 +- INSTALL.md | 12 +- Makefile | 18 +- config/coq_config.mli | 6 +- coqide-server.opam | 2 +- default.nix | 6 +- dev/ci/README-developers.md | 2 +- dev/ci/platform/coq-pf-03-build.bat | 2 +- dev/doc/build-system.dune.md | 16 +- dev/doc/xml-protocol.md | 14 +- dev/dune | 2 +- dev/dune-dbg.in | 6 +- dev/shim/dune | 16 +- doc/changelog/10-coqide/00000-title.rst | 4 - doc/changelog/10-rocqide/00000-title.rst | 3 + .../19166-coqide.rst | 0 .../19188-warnings_in_table.rst | 0 .../19417-coqide-preferences.rst | 0 .../10-rocqide/20036-rename-coqide.rst | 4 + .../19378-make-world-coqide.rst | 4 +- doc/common/macros.tex | 2 +- ...pacted.png => diffs-rocqide-compacted.png} | Bin ...tigoal.png => diffs-rocqide-multigoal.png} | Bin ...ffs-coqide-on.png => diffs-rocqide-on.png} | Bin ...-removed.png => diffs-rocqide-removed.png} | Bin ...tor.png => rocqide-preferences-editor.png} | Bin ....png => rocqide-preferences-shortcuts.png} | Bin ...coqide-queries.png => rocqide-queries.png} | Bin .../_static/{coqide.png => rocqide.png} | Bin .../addendum/parallel-proof-processing.rst | 20 +- doc/sphinx/changes.rst | 4 +- doc/sphinx/language/core/modules.rst | 2 +- doc/sphinx/practical-tools/coq-commands.rst | 10 +- doc/sphinx/practical-tools/coqide.rst | 101 +++---- doc/sphinx/practical-tools/utilities.rst | 10 +- doc/sphinx/proof-engine/ltac.rst | 6 +- .../proofs/writing-proofs/proof-mode.rst | 32 +-- doc/sphinx/using/tools/index.rst | 4 +- dune-project | 6 +- ide/coqide/coq-ssreflect.lang | 249 ------------------ ide/coqide/coq_icon.rc | 1 - ide/coqide/index.mld | 3 - ide/{coqide => rocqide}/FAQ | 14 +- ide/{coqide => rocqide}/MacOS/coqfile.icns | Bin ide/{coqide => rocqide}/MacOS/coqide.icns | Bin ide/{coqide => rocqide}/Make | 0 ide/{coqide => rocqide}/config.mli | 0 ide/{coqide => rocqide}/config_lexer.mli | 0 ide/{coqide => rocqide}/config_lexer.mll | 14 +- ide/rocqide/coq-ssreflect.lang | 249 ++++++++++++++++++ ide/{coqide => rocqide}/coq.ico | Bin ide/{coqide => rocqide}/coq.lang | 0 ide/{coqide => rocqide}/coq.png | Bin ide/{coqide => rocqide}/coq2.ico | Bin ide/rocqide/coq_icon.rc | 1 + ide/{coqide => rocqide}/coq_style.xml | 2 +- .../default_bindings_src.ml | 0 .../default_bindings_src.mli | 0 ide/{coqide => rocqide}/document.ml | 0 ide/{coqide => rocqide}/document.mli | 0 ide/{coqide => rocqide}/dune | 14 +- ide/{coqide => rocqide}/fileOps.ml | 0 ide/{coqide => rocqide}/fileOps.mli | 0 ide/{coqide => rocqide}/gen_gtk_platform.ml | 0 ide/{coqide => rocqide}/gen_gtk_platform.mli | 0 ide/{coqide => rocqide}/gtk_parsing.ml | 0 ide/{coqide => rocqide}/gtk_parsing.mli | 0 ide/{coqide => rocqide}/idetop.ml | 2 +- ide/{coqide => rocqide}/idetop.mli | 0 ide/{coqide => rocqide}/ideutils.ml | 2 +- ide/{coqide => rocqide}/ideutils.mli | 0 ide/rocqide/index.mld | 3 + ide/{coqide => rocqide}/macos_prehook.ml | 0 ide/{coqide => rocqide}/macos_prehook.mli | 0 ide/{coqide => rocqide}/microPG.ml | 0 ide/{coqide => rocqide}/microPG.mli | 0 ide/{coqide => rocqide}/minilib.ml | 0 ide/{coqide => rocqide}/minilib.mli | 0 ide/{coqide => rocqide}/preferences.ml | 11 +- ide/{coqide => rocqide}/preferences.mli | 0 ide/{coqide => rocqide}/preferences_ui.ml | 0 ide/{coqide => rocqide}/preferences_ui.mli | 0 ide/{coqide => rocqide}/protocol/dune | 0 .../protocol/interface.mli | 4 +- ide/{coqide => rocqide}/protocol/richpp.ml | 0 ide/{coqide => rocqide}/protocol/richpp.mli | 0 ide/{coqide => rocqide}/protocol/serialize.ml | 0 .../protocol/serialize.mli | 0 .../protocol/xml_lexer.mli | 0 .../protocol/xml_lexer.mll | 0 .../protocol/xml_parser.ml | 0 .../protocol/xml_parser.mli | 0 .../protocol/xml_printer.ml | 0 .../protocol/xml_printer.mli | 0 .../protocol/xmlprotocol.ml | 3 +- .../protocol/xmlprotocol.mli | 2 +- ide/{coqide => rocqide}/rocqDriver.ml | 10 +- ide/{coqide => rocqide}/rocqDriver.mli | 6 +- ide/{coqide => rocqide}/rocqOps.ml | 4 +- ide/{coqide => rocqide}/rocqOps.mli | 0 ide/{coqide => rocqide}/rocq_commands.ml | 0 ide/{coqide => rocqide}/rocq_commands.mli | 0 ide/{coqide => rocqide}/rocq_lex.mli | 0 ide/{coqide => rocqide}/rocq_lex.mll | 0 ide/{coqide => rocqide}/rocqide.ml | 62 ++--- ide/{coqide => rocqide}/rocqide.mli | 10 +- ide/{coqide => rocqide}/rocqide_QUARTZ.c.in | 0 ide/{coqide => rocqide}/rocqide_QUARTZ.ml.in | 6 +- ide/{coqide => rocqide}/rocqide_WIN32.c.in | 4 +- ide/{coqide => rocqide}/rocqide_WIN32.ml.in | 6 +- ide/{coqide => rocqide}/rocqide_X11.c.in | 0 ide/{coqide => rocqide}/rocqide_X11.ml.in | 0 ide/{coqide => rocqide}/rocqide_main.ml | 4 +- ide/{coqide => rocqide}/rocqide_main.mli | 0 .../rocqide_os_specific.mli | 0 ide/{coqide => rocqide}/rocqide_ui.ml | 4 +- ide/{coqide => rocqide}/rocqide_ui.mli | 0 ide/{coqide => rocqide}/sentence.ml | 2 +- ide/{coqide => rocqide}/sentence.mli | 0 ide/{coqide => rocqide}/session.ml | 0 ide/{coqide => rocqide}/session.mli | 0 ide/{coqide => rocqide}/shared.ml | 2 +- ide/{coqide => rocqide}/shared.mli | 0 ide/{coqide => rocqide}/shared_QUARTZ.c.in | 0 ide/{coqide => rocqide}/shared_QUARTZ.ml.in | 0 ide/{coqide => rocqide}/shared_WIN32.c.in | 0 ide/{coqide => rocqide}/shared_WIN32.ml.in | 0 ide/{coqide => rocqide}/shared_X11.c.in | 0 ide/{coqide => rocqide}/shared_X11.ml.in | 0 .../shared_os_specific.mli | 0 ide/{coqide => rocqide}/tags.ml | 0 ide/{coqide => rocqide}/tags.mli | 0 ide/{coqide => rocqide}/ui_dialogs.ml | 0 ide/{coqide => rocqide}/ui_dialogs.mli | 0 ide/{coqide => rocqide}/unicode_bindings.ml | 0 ide/{coqide => rocqide}/unicode_bindings.mli | 0 ide/{coqide => rocqide}/utf8_convert.mli | 0 ide/{coqide => rocqide}/utf8_convert.mll | 24 +- ide/{coqide => rocqide}/wg_Command.ml | 0 ide/{coqide => rocqide}/wg_Command.mli | 0 ide/{coqide => rocqide}/wg_Completion.ml | 0 ide/{coqide => rocqide}/wg_Completion.mli | 0 ide/{coqide => rocqide}/wg_Debugger.ml | 0 ide/{coqide => rocqide}/wg_Debugger.mli | 0 ide/{coqide => rocqide}/wg_Detachable.ml | 1 - ide/{coqide => rocqide}/wg_Detachable.mli | 2 - ide/{coqide => rocqide}/wg_Find.ml | 0 ide/{coqide => rocqide}/wg_Find.mli | 0 ide/{coqide => rocqide}/wg_MessageView.ml | 0 ide/{coqide => rocqide}/wg_MessageView.mli | 0 ide/{coqide => rocqide}/wg_Notebook.ml | 1 - ide/{coqide => rocqide}/wg_Notebook.mli | 0 ide/{coqide => rocqide}/wg_ProofView.ml | 0 ide/{coqide => rocqide}/wg_ProofView.mli | 0 .../wg_RoutedMessageViews.ml | 0 .../wg_RoutedMessageViews.mli | 0 ide/{coqide => rocqide}/wg_ScriptView.ml | 0 ide/{coqide => rocqide}/wg_ScriptView.mli | 0 ide/{coqide => rocqide}/wg_Segment.ml | 0 ide/{coqide => rocqide}/wg_Segment.mli | 0 man/dune | 5 +- man/{coqide.1 => rocqide.1} | 51 ++-- plugins/extraction/extract_env.ml | 4 +- printing/proof_diffs.ml | 8 +- coqide.opam => rocqide.opam | 2 +- stm/asyncTaskQueue.mli | 2 +- test-suite/ide/blocking-futures.fake | 2 +- test-suite/ide/fake_ide.ml | 6 +- test-suite/ide/join-idem.fake | 2 +- test-suite/ide/join-module1.fake | 2 +- test-suite/ide/join-module2.fake | 2 +- test-suite/ide/join-sync.fake | 2 +- test-suite/ide/join.fake | 2 +- test-suite/ide/reopen.fake | 2 +- test-suite/ide/reopen1.fake | 2 +- test-suite/ide/undo001.fake | 2 +- test-suite/ide/undo002.fake | 2 +- test-suite/ide/undo003.fake | 2 +- test-suite/ide/undo004.fake | 2 +- test-suite/ide/undo005.fake | 2 +- test-suite/ide/undo006.fake | 2 +- test-suite/ide/undo008.fake | 2 +- test-suite/ide/undo009.fake | 2 +- test-suite/ide/undo010.fake | 2 +- test-suite/ide/undo012.fake | 2 +- test-suite/ide/undo013.fake | 2 +- test-suite/ide/undo014.fake | 2 +- test-suite/ide/undo015.fake | 2 +- test-suite/ide/undo016.fake | 2 +- test-suite/ide/undo017.fake | 2 +- test-suite/ide/undo018.fake | 2 +- test-suite/ide/undo019.fake | 2 +- test-suite/ide/undo020.fake | 2 +- test-suite/ide/undo021.fake | 2 +- test-suite/ide/undo022.fake | 2 +- test-suite/ide/univ.fake | 2 +- test-suite/success/RemoteUnivs.v | 2 +- tools/configure/cmdArgs.mli | 2 +- tools/configure/configure.ml | 4 +- tools/configure/util.ml | 1 - vernac/future.ml | 4 +- 203 files changed, 596 insertions(+), 609 deletions(-) delete mode 100644 doc/changelog/10-coqide/00000-title.rst create mode 100644 doc/changelog/10-rocqide/00000-title.rst rename doc/changelog/{10-coqide => 10-rocqide}/19166-coqide.rst (100%) rename doc/changelog/{10-coqide => 10-rocqide}/19188-warnings_in_table.rst (100%) rename doc/changelog/{10-coqide => 10-rocqide}/19417-coqide-preferences.rst (100%) create mode 100644 doc/changelog/10-rocqide/20036-rename-coqide.rst rename doc/sphinx/_static/{diffs-coqide-compacted.png => diffs-rocqide-compacted.png} (100%) rename doc/sphinx/_static/{diffs-coqide-multigoal.png => diffs-rocqide-multigoal.png} (100%) rename doc/sphinx/_static/{diffs-coqide-on.png => diffs-rocqide-on.png} (100%) rename doc/sphinx/_static/{diffs-coqide-removed.png => diffs-rocqide-removed.png} (100%) rename doc/sphinx/_static/{coqide-preferences-editor.png => rocqide-preferences-editor.png} (100%) rename doc/sphinx/_static/{coqide-preferences-shortcuts.png => rocqide-preferences-shortcuts.png} (100%) rename doc/sphinx/_static/{coqide-queries.png => rocqide-queries.png} (100%) rename doc/sphinx/_static/{coqide.png => rocqide.png} (100%) delete mode 100644 ide/coqide/coq-ssreflect.lang delete mode 100644 ide/coqide/coq_icon.rc delete mode 100644 ide/coqide/index.mld rename ide/{coqide => rocqide}/FAQ (91%) rename ide/{coqide => rocqide}/MacOS/coqfile.icns (100%) rename ide/{coqide => rocqide}/MacOS/coqide.icns (100%) rename ide/{coqide => rocqide}/Make (100%) rename ide/{coqide => rocqide}/config.mli (100%) rename ide/{coqide => rocqide}/config_lexer.mli (100%) rename ide/{coqide => rocqide}/config_lexer.mll (82%) create mode 100644 ide/rocqide/coq-ssreflect.lang rename ide/{coqide => rocqide}/coq.ico (100%) rename ide/{coqide => rocqide}/coq.lang (100%) rename ide/{coqide => rocqide}/coq.png (100%) rename ide/{coqide => rocqide}/coq2.ico (100%) create mode 100644 ide/rocqide/coq_icon.rc rename ide/{coqide => rocqide}/coq_style.xml (96%) rename ide/{coqide => rocqide}/default_bindings_src.ml (100%) rename ide/{coqide => rocqide}/default_bindings_src.mli (100%) rename ide/{coqide => rocqide}/document.ml (100%) rename ide/{coqide => rocqide}/document.mli (100%) rename ide/{coqide => rocqide}/dune (91%) rename ide/{coqide => rocqide}/fileOps.ml (100%) rename ide/{coqide => rocqide}/fileOps.mli (100%) rename ide/{coqide => rocqide}/gen_gtk_platform.ml (100%) rename ide/{coqide => rocqide}/gen_gtk_platform.mli (100%) rename ide/{coqide => rocqide}/gtk_parsing.ml (100%) rename ide/{coqide => rocqide}/gtk_parsing.mli (100%) rename ide/{coqide => rocqide}/idetop.ml (99%) rename ide/{coqide => rocqide}/idetop.mli (100%) rename ide/{coqide => rocqide}/ideutils.ml (99%) rename ide/{coqide => rocqide}/ideutils.mli (100%) create mode 100644 ide/rocqide/index.mld rename ide/{coqide => rocqide}/macos_prehook.ml (100%) rename ide/{coqide => rocqide}/macos_prehook.mli (100%) rename ide/{coqide => rocqide}/microPG.ml (100%) rename ide/{coqide => rocqide}/microPG.mli (100%) rename ide/{coqide => rocqide}/minilib.ml (100%) rename ide/{coqide => rocqide}/minilib.mli (100%) rename ide/{coqide => rocqide}/preferences.ml (98%) rename ide/{coqide => rocqide}/preferences.mli (100%) rename ide/{coqide => rocqide}/preferences_ui.ml (100%) rename ide/{coqide => rocqide}/preferences_ui.mli (100%) rename ide/{coqide => rocqide}/protocol/dune (100%) rename ide/{coqide => rocqide}/protocol/interface.mli (98%) rename ide/{coqide => rocqide}/protocol/richpp.ml (100%) rename ide/{coqide => rocqide}/protocol/richpp.mli (100%) rename ide/{coqide => rocqide}/protocol/serialize.ml (100%) rename ide/{coqide => rocqide}/protocol/serialize.mli (100%) rename ide/{coqide => rocqide}/protocol/xml_lexer.mli (100%) rename ide/{coqide => rocqide}/protocol/xml_lexer.mll (100%) rename ide/{coqide => rocqide}/protocol/xml_parser.ml (100%) rename ide/{coqide => rocqide}/protocol/xml_parser.mli (100%) rename ide/{coqide => rocqide}/protocol/xml_printer.ml (100%) rename ide/{coqide => rocqide}/protocol/xml_printer.mli (100%) rename ide/{coqide => rocqide}/protocol/xmlprotocol.ml (99%) rename ide/{coqide => rocqide}/protocol/xmlprotocol.mli (98%) rename ide/{coqide => rocqide}/rocqDriver.ml (98%) rename ide/{coqide => rocqide}/rocqDriver.mli (97%) rename ide/{coqide => rocqide}/rocqOps.ml (99%) rename ide/{coqide => rocqide}/rocqOps.mli (100%) rename ide/{coqide => rocqide}/rocq_commands.ml (100%) rename ide/{coqide => rocqide}/rocq_commands.mli (100%) rename ide/{coqide => rocqide}/rocq_lex.mli (100%) rename ide/{coqide => rocqide}/rocq_lex.mll (100%) rename ide/{coqide => rocqide}/rocqide.ml (97%) rename ide/{coqide => rocqide}/rocqide.mli (83%) rename ide/{coqide => rocqide}/rocqide_QUARTZ.c.in (100%) rename ide/{coqide => rocqide}/rocqide_QUARTZ.ml.in (86%) rename ide/{coqide => rocqide}/rocqide_WIN32.c.in (94%) rename ide/{coqide => rocqide}/rocqide_WIN32.ml.in (90%) rename ide/{coqide => rocqide}/rocqide_X11.c.in (100%) rename ide/{coqide => rocqide}/rocqide_X11.ml.in (100%) rename ide/{coqide => rocqide}/rocqide_main.ml (95%) rename ide/{coqide => rocqide}/rocqide_main.mli (100%) rename ide/{coqide => rocqide}/rocqide_os_specific.mli (100%) rename ide/{coqide => rocqide}/rocqide_ui.ml (98%) rename ide/{coqide => rocqide}/rocqide_ui.mli (100%) rename ide/{coqide => rocqide}/sentence.ml (99%) rename ide/{coqide => rocqide}/sentence.mli (100%) rename ide/{coqide => rocqide}/session.ml (100%) rename ide/{coqide => rocqide}/session.mli (100%) rename ide/{coqide => rocqide}/shared.ml (93%) rename ide/{coqide => rocqide}/shared.mli (100%) rename ide/{coqide => rocqide}/shared_QUARTZ.c.in (100%) rename ide/{coqide => rocqide}/shared_QUARTZ.ml.in (100%) rename ide/{coqide => rocqide}/shared_WIN32.c.in (100%) rename ide/{coqide => rocqide}/shared_WIN32.ml.in (100%) rename ide/{coqide => rocqide}/shared_X11.c.in (100%) rename ide/{coqide => rocqide}/shared_X11.ml.in (100%) rename ide/{coqide => rocqide}/shared_os_specific.mli (100%) rename ide/{coqide => rocqide}/tags.ml (100%) rename ide/{coqide => rocqide}/tags.mli (100%) rename ide/{coqide => rocqide}/ui_dialogs.ml (100%) rename ide/{coqide => rocqide}/ui_dialogs.mli (100%) rename ide/{coqide => rocqide}/unicode_bindings.ml (100%) rename ide/{coqide => rocqide}/unicode_bindings.mli (100%) rename ide/{coqide => rocqide}/utf8_convert.mli (100%) rename ide/{coqide => rocqide}/utf8_convert.mll (73%) rename ide/{coqide => rocqide}/wg_Command.ml (100%) rename ide/{coqide => rocqide}/wg_Command.mli (100%) rename ide/{coqide => rocqide}/wg_Completion.ml (100%) rename ide/{coqide => rocqide}/wg_Completion.mli (100%) rename ide/{coqide => rocqide}/wg_Debugger.ml (100%) rename ide/{coqide => rocqide}/wg_Debugger.mli (100%) rename ide/{coqide => rocqide}/wg_Detachable.ml (99%) rename ide/{coqide => rocqide}/wg_Detachable.mli (99%) rename ide/{coqide => rocqide}/wg_Find.ml (100%) rename ide/{coqide => rocqide}/wg_Find.mli (100%) rename ide/{coqide => rocqide}/wg_MessageView.ml (100%) rename ide/{coqide => rocqide}/wg_MessageView.mli (100%) rename ide/{coqide => rocqide}/wg_Notebook.ml (99%) rename ide/{coqide => rocqide}/wg_Notebook.mli (100%) rename ide/{coqide => rocqide}/wg_ProofView.ml (100%) rename ide/{coqide => rocqide}/wg_ProofView.mli (100%) rename ide/{coqide => rocqide}/wg_RoutedMessageViews.ml (100%) rename ide/{coqide => rocqide}/wg_RoutedMessageViews.mli (100%) rename ide/{coqide => rocqide}/wg_ScriptView.ml (100%) rename ide/{coqide => rocqide}/wg_ScriptView.mli (100%) rename ide/{coqide => rocqide}/wg_Segment.ml (100%) rename ide/{coqide => rocqide}/wg_Segment.mli (100%) rename man/{coqide.1 => rocqide.1} (68%) rename coqide.opam => rocqide.opam (94%) diff --git a/.github/workflows/ci-macos.yml b/.github/workflows/ci-macos.yml index 728de341ad53..013285241604 100644 --- a/.github/workflows/ci-macos.yml +++ b/.github/workflows/ci-macos.yml @@ -36,7 +36,7 @@ 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" @@ -44,7 +44,7 @@ jobs: - 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 index 034abc052658..f9d790765435 100644 --- 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 index 83fdc41a1a0e..059404fb6c8c 100644 --- 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 index be853454e714..fb1565883676 100644 --- 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 $options $ make dunestrap - $ dune build -p rocq-runtime,coq-core,rocq-core,coq,coqide-server,coqide - $ dune 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= 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 index f75ab05dadbc..0a5fc2bb5bef 100644 --- 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 index 24b38f5819c2..0a84cbafdb06 100644 --- 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 index d5265ce7b539..7a3b45d8f6d9 100644 --- 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 "] authors: ["The Rocq development team, INRIA, CNRS, and contributors"] diff --git a/default.nix b/default.nix index 8009bb3adbcb..b50eab1b3360 100644 --- 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 index 41a7ec0d93ef..cc31a7eaba2a 100644 --- 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 index 664f45abd798..38b2450768e4 100644 --- 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 index 5cf4bb4ccfe7..bb6678c4ae70 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -106,7 +106,7 @@ 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 @@ -114,13 +114,13 @@ work well unless you are using `dune exec -- coqtop -noinit`. The 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 index 161eeffde28f..5675c3da6a14 100644 --- 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. ------------------------------- ### **Status(force: bool)** -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: ``` -CoqIDE sends the following settings (defaults in parentheses): +RocqIDE sends the following settings (defaults in parentheses): ``` Printing Width : (60), Printing Coercions : (), @@ -705,7 +705,7 @@ processed when Coq is no longer busy or execution stops in the debugger. - /home/proj/coq/ide/coqide/debug.v + /home/proj/coq/ide/rocqide/debug.v 22 @@ -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, `ABC` indicates that "ABC" should be highlighted diff --git a/dev/dune b/dev/dune index 3e162eec0c5d..c8939446ae2f 100644 --- 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. diff --git a/dev/dune-dbg.in b/dev/dune-dbg.in index 2ee4d072a8b6..72d1da3e76ee 100755 --- a/dev/dune-dbg.in +++ b/dev/dune-dbg.in @@ -19,9 +19,9 @@ while [[ $# -gt 0 ]]; do opts+=($(ocamlfind query -recursive -i-format rocq-runtime.checklib)) break ;; - coqide) + rocqide) shift - exe=_build/default/ide/coqide/coqide_main.bc + exe=_build/default/ide/rocqide/rocqide_main.bc break ;; coqc) @@ -40,7 +40,7 @@ while [[ $# -gt 0 ]]; do break ;; *) - echo "usage: dune exec -- dev/dune-dbg [-emacs] {coqchk|coqide|coqc|coqtop|coqdep|coqnative} coqargs" + echo "usage: dune exec -- dev/dune-dbg [-emacs] {coqchk|rocqide|coqc|coqtop|coqdep|coqnative} coqargs" exit 1 ;; esac diff --git a/dev/shim/dune b/dev/shim/dune index 56bcdd216b19..726529064cde 100644 --- a/dev/shim/dune +++ b/dev/shim/dune @@ -102,27 +102,27 @@ (bash "echo '\"$(dirname \"$0\")\"/%{bin:coqtop.byte} -I \"$(dirname \"$0\")/%{workspace_root}/../install/default/lib\" -coqlib \"$(dirname \"$0\")\"/%{project_root} \"$@\"'") (run chmod +x %{targets}))))) -; coqide +; rocqide (alias - (name coqide-prelude) + (name rocqide-prelude) (deps ; without this if the gtk libs are not available dune can try to use - ; coqide from PATH instead of giving a nice error + ; rocqide from PATH instead of giving a nice error ; there is no problem with the other shims since they don't depend on optional build products - %{project_root}/ide/coqide/rocqide_main.exe + %{project_root}/ide/rocqide/rocqide_main.exe %{bin:rocqworker} %{bin:coqidetop} %{project_root}/theories/Init/Prelude.vo %{project_root}/coqide-server.install - %{project_root}/coqide.install)) + %{project_root}/rocqide.install)) (rule - (targets coqide) - (deps (alias coqide-prelude)) + (targets rocqide) + (deps (alias rocqide-prelude)) (action (with-stdout-to %{targets} (progn (echo "#!/usr/bin/env bash\n") - (bash "echo '\"$(dirname \"$0\")\"/%{bin:coqide} -I \"$(dirname \"$0\")/%{workspace_root}/../install/default/lib\" -coqlib \"$(dirname \"$0\")\"/%{project_root} \"$@\"'") + (bash "echo '\"$(dirname \"$0\")\"/%{bin:rocqide} -I \"$(dirname \"$0\")/%{workspace_root}/../install/default/lib\" -coqlib \"$(dirname \"$0\")\"/%{project_root} \"$@\"'") (run chmod +x %{targets}))))) diff --git a/doc/changelog/10-coqide/00000-title.rst b/doc/changelog/10-coqide/00000-title.rst deleted file mode 100644 index 81cf05b8440f..000000000000 --- a/doc/changelog/10-coqide/00000-title.rst +++ /dev/null @@ -1,4 +0,0 @@ - -CoqIDE -^^^^^^ - diff --git a/doc/changelog/10-rocqide/00000-title.rst b/doc/changelog/10-rocqide/00000-title.rst new file mode 100644 index 000000000000..e781c5c0e2e0 --- /dev/null +++ b/doc/changelog/10-rocqide/00000-title.rst @@ -0,0 +1,3 @@ + +RocqIDE +^^^^^^^ diff --git a/doc/changelog/10-coqide/19166-coqide.rst b/doc/changelog/10-rocqide/19166-coqide.rst similarity index 100% rename from doc/changelog/10-coqide/19166-coqide.rst rename to doc/changelog/10-rocqide/19166-coqide.rst diff --git a/doc/changelog/10-coqide/19188-warnings_in_table.rst b/doc/changelog/10-rocqide/19188-warnings_in_table.rst similarity index 100% rename from doc/changelog/10-coqide/19188-warnings_in_table.rst rename to doc/changelog/10-rocqide/19188-warnings_in_table.rst diff --git a/doc/changelog/10-coqide/19417-coqide-preferences.rst b/doc/changelog/10-rocqide/19417-coqide-preferences.rst similarity index 100% rename from doc/changelog/10-coqide/19417-coqide-preferences.rst rename to doc/changelog/10-rocqide/19417-coqide-preferences.rst diff --git a/doc/changelog/10-rocqide/20036-rename-coqide.rst b/doc/changelog/10-rocqide/20036-rename-coqide.rst new file mode 100644 index 000000000000..885c4819546a --- /dev/null +++ b/doc/changelog/10-rocqide/20036-rename-coqide.rst @@ -0,0 +1,4 @@ +- **Changed:** + CoqIDE is renamed to RocqIDE (the auxiliary binary `coqidetop` is not renamed) + (`#20036 `_, + by Gaëtan Gilbert). diff --git a/doc/changelog/12-infrastructure-and-dependencies/19378-make-world-coqide.rst b/doc/changelog/12-infrastructure-and-dependencies/19378-make-world-coqide.rst index d23e128dffde..cb9d01cacfc4 100644 --- a/doc/changelog/12-infrastructure-and-dependencies/19378-make-world-coqide.rst +++ b/doc/changelog/12-infrastructure-and-dependencies/19378-make-world-coqide.rst @@ -1,5 +1,5 @@ - **Changed:** - when building Coq, the makefile's `world` target and `dune build`'s default target do not build coqide anymore. - Use `make world coqide` or `dune build @default coqide.install` to build what they respectively used to build + when building Coq, the makefile's `world` target and `dune build`'s default target do not build rocqide anymore. + Use `make world rocqide` or `dune build @default rocqide.install` to build what they respectively used to build (`#19378 `_, by Gaëtan Gilbert). diff --git a/doc/common/macros.tex b/doc/common/macros.tex index e790d20e00c5..4b296a029d4b 100644 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -93,7 +93,7 @@ \newcommand{\Coq}{\textsc{Coq}} \newcommand{\gallina}{\textsc{Gallina}} \newcommand{\Gallina}{\textsc{Gallina}} -\newcommand{\CoqIDE}{\textsc{CoqIDE}} +\newcommand{\RocqIDE}{\textsc{RocqIDE}} \newcommand{\ocaml}{\textsc{OCaml}} \newcommand{\camlpppp}{\textsc{Camlp5}} \newcommand{\emacs}{\textsc{GNU Emacs}} diff --git a/doc/sphinx/_static/diffs-coqide-compacted.png b/doc/sphinx/_static/diffs-rocqide-compacted.png similarity index 100% rename from doc/sphinx/_static/diffs-coqide-compacted.png rename to doc/sphinx/_static/diffs-rocqide-compacted.png diff --git a/doc/sphinx/_static/diffs-coqide-multigoal.png b/doc/sphinx/_static/diffs-rocqide-multigoal.png similarity index 100% rename from doc/sphinx/_static/diffs-coqide-multigoal.png rename to doc/sphinx/_static/diffs-rocqide-multigoal.png diff --git a/doc/sphinx/_static/diffs-coqide-on.png b/doc/sphinx/_static/diffs-rocqide-on.png similarity index 100% rename from doc/sphinx/_static/diffs-coqide-on.png rename to doc/sphinx/_static/diffs-rocqide-on.png diff --git a/doc/sphinx/_static/diffs-coqide-removed.png b/doc/sphinx/_static/diffs-rocqide-removed.png similarity index 100% rename from doc/sphinx/_static/diffs-coqide-removed.png rename to doc/sphinx/_static/diffs-rocqide-removed.png diff --git a/doc/sphinx/_static/coqide-preferences-editor.png b/doc/sphinx/_static/rocqide-preferences-editor.png similarity index 100% rename from doc/sphinx/_static/coqide-preferences-editor.png rename to doc/sphinx/_static/rocqide-preferences-editor.png diff --git a/doc/sphinx/_static/coqide-preferences-shortcuts.png b/doc/sphinx/_static/rocqide-preferences-shortcuts.png similarity index 100% rename from doc/sphinx/_static/coqide-preferences-shortcuts.png rename to doc/sphinx/_static/rocqide-preferences-shortcuts.png diff --git a/doc/sphinx/_static/coqide-queries.png b/doc/sphinx/_static/rocqide-queries.png similarity index 100% rename from doc/sphinx/_static/coqide-queries.png rename to doc/sphinx/_static/rocqide-queries.png diff --git a/doc/sphinx/_static/coqide.png b/doc/sphinx/_static/rocqide.png similarity index 100% rename from doc/sphinx/_static/coqide.png rename to doc/sphinx/_static/rocqide.png diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst index 89bcbb2232bc..85b76cfc67dc 100644 --- a/doc/sphinx/addendum/parallel-proof-processing.rst +++ b/doc/sphinx/addendum/parallel-proof-processing.rst @@ -7,7 +7,7 @@ Asynchronous and Parallel Proof Processing This chapter explains how proofs can be asynchronously processed by Rocq. This feature improves the reactivity of the system when used in -interactive mode via CoqIDE. In addition, it allows Rocq to take +interactive mode via RocqIDE. In addition, it allows Rocq to take advantage of parallel hardware when used as a batch compiler by decoupling the checking of statements and definitions from the construction and checking of proofs objects. @@ -26,7 +26,7 @@ category are universe inconsistencies. At the time of writing, only opaque proofs (ending with :cmd:`Qed` or :cmd:`Admitted`) can be processed asynchronously. -Finally, asynchronous processing is disabled when running CoqIDE in +Finally, asynchronous processing is disabled when running RocqIDE in Windows. The current implementation of the feature is not stable on Windows. It can be enabled, as described below at :ref:`interactive-mode`, though doing so is not recommended. @@ -121,13 +121,13 @@ Caveats When a command fails the subsequent error messages may be bogus, i.e. caused by the first error. Error resilience for commands can be switched off by passing ``-async-proofs-command-error-resilience off`` -to CoqIDE. +to RocqIDE. An incorrect proof block detection can result into an incorrect error recovery and hence in bogus errors. Proof block detection cannot be precise for bullets or any other non-well parenthesized proof structure. Error resilience can be turned off or selectively activated -for any set of block kind passing to CoqIDE one of the following +for any set of block kind passing to RocqIDE one of the following options: - ``-async-proofs-tactic-error-resilience off`` @@ -143,13 +143,13 @@ Interactive mode .. todo: How about PG and coqtail? -CoqIDE and VsCoq support asynchronous proof processing. +RocqIDE and VsCoq support asynchronous proof processing. -When CoqIDE is started and async mode is enabled, two or more Rocq processes +When RocqIDE is started and async mode is enabled, two or more Rocq processes are created. The master one follows the user, giving feedback as soon as possible by skipping proofs, which are delegated to the worker processes. The worker processes -asynchronously processes the proofs. The *Jobs panel* in the main CoqIDE +asynchronously processes the proofs. The *Jobs panel* in the main RocqIDE window shows the status of each worker process. If a proof contains an error, it's reported in red in the label of the very same button, that can also be used to see the list of errors @@ -180,20 +180,20 @@ all the shells from which Rocq processes will be started. If one uses just one terminal running the bash shell, then `export $(rocq workmgr -j 4)` will do the job. -After that, all Coq processes, e.g. `coqide` and `rocq compile`, +After that, all Coq processes, e.g. `rocqide` and `rocq compile`, will honor the limit, globally. Caveats ``````` -The number of worker processes can be increased by passing CoqIDE +The number of worker processes can be increased by passing RocqIDE the ``-async-proofs-j n`` flag. Note that the memory consumption increases too, since each worker requires the same amount of memory as the master process. Also note that increasing the number of workers may reduce the reactivity of the master process to user commands. To disable this feature, one can pass the ``-async-proofs off`` flag to -CoqIDE. Conversely, on Windows, where the feature is disabled by +RocqIDE. Conversely, on Windows, where the feature is disabled by default, pass the ``-async-proofs on`` flag to enable it. Proofs that are known to take little time to process are not delegated diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index a88bc515c91a..61ad165da49d 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -4577,7 +4577,7 @@ CoqIDE visually and jumping to the stopping point plus continue, step over, step in and step out operations. Displays the call stack and variable values for each stack frame. Currently only for Ltac. - See the documentation :ref:`here ` + See the documentation :ref:`here ` (`#14644 `_, fixes `#13967 `_, by Jim Fehrle) @@ -8689,7 +8689,7 @@ reference manual. Here are the most important user-visible changes: ``\alpha`` then ``Shift+Space`` will insert the greek letter alpha. A larger number of default bindings are provided, following the latex naming convention. Bindings can be customized, either globally, or on a - per-project basis. See Section :ref:`coqide-unicode` for details + per-project basis. See Section :ref:`rocqide-unicode` for details (`#8560 `_, by Arthur Charguéraud). - Infrastructure and dependencies: diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst index 41368d74efb8..d49c550d90f0 100644 --- a/doc/sphinx/language/core/modules.rst +++ b/doc/sphinx/language/core/modules.rst @@ -566,7 +566,7 @@ as :n:`Stdlib.Init.Logic`, in which: corresponds to the file system path :n:`Init/Logic.v` on Linux) When Rocq is processing a script that hasn't been saved in a file, such as a new -buffer in CoqIDE or anything in `rocq repl`, definitions in the script are associated +buffer in RocqIDE or anything in `rocq repl`, definitions in the script are associated with the logical name :n:`Top` and there is no associated file system path. **Item part.** Items are further qualified by a suffix in the form diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 794c9f651334..2c3d0c2009b9 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -5,7 +5,7 @@ The Rocq Prover commands There are several Rocq commands: -+ ``coqide``: a graphical integrated development environment, described ++ ``rocqide``: a graphical integrated development environment, described :ref:`here `. In addition, there are several other IDEs such as Proof General, vsCoq and Coqtail that are not included with the Coq installation. @@ -61,13 +61,13 @@ See :ref:`rocq_makefile` and :ref:`building_dune`. To compile `foo.v` as part of a module `Mod1` that is rooted at `.` (i.e. the directory containing `foo.v`), run `rocq c -Q . Mod1 foo.v`. - To make the module available in `CoqIDE`, include the following line in the + To make the module available in `RocqIDE`, include the following line in the `_CoqProject` file (see :ref:`rocq_makefile`) in the directory from which you - start `CoqIDE` or give it as an argument to the ``coqide`` command. + start `RocqIDE` or give it as an argument to the ``rocqide`` command. ** is the pathname of the directory containing the module, which can be an absolute path or relative to Rocq's current directory. For now, - you must close and reload a named script file for `CoqIDE` to pick up the change, - or restart `CoqIDE`. + you must close and reload a named script file for `RocqIDE` to pick up the change, + or restart `RocqIDE`. The project file name is configurable in `Edit / Preferences / Project`. .. rocqdoc:: diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index ca11dd21b224..d0ae24abf7f5 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -2,29 +2,30 @@ .. _coqintegrateddevelopmentenvironment: -CoqIDE -====== +RocqIDE +========= +.. extra =s to avoid being a git conflict marker .. todo: how to say that a number of things are broken? Maybe list them somewhere--doesn't have to be super detailed -The Coq Integrated Development Environment (CoqIDE) is a user-friendly GUI +The Rocq Integrated Development Environment (RocqIDE) is a user-friendly GUI for Coq. Its main purpose is to allow users to edit Coq scripts and step forward and backward through them. Stepping forward executes commands and tactics while stepping backward undoes previously executed commands and tactics, returning to a previous state. -To run CoqIDE, enter `coqide` on the command line. +To run RocqIDE, enter `rocqide` on the command line. If you include script file names (which end with `.v`) as arguments, each is opened -in a separate tab. If you don't, CoqIDE opens a single unnamed buffer -(titled `*scratch*`). `coqide` also accepts many of the options of `coqtop` +in a separate tab. If you don't, RocqIDE opens a single unnamed buffer +(titled `*scratch*`). `rocqide` also accepts many of the options of `rocq top` (see :ref:`therocqcommands`), while ignoring the ones that aren't meaningful -for CoqIDE. Use `coqide --help` to see the list of command line options. +for RocqIDE. Use `rocqide --help` to see the list of command line options. -.. _coqide_mainscreen: +.. _rocqide_mainscreen: -.. image:: ../_static/coqide.png - :alt: CoqIDE main screen +.. image:: ../_static/rocqide.png + :alt: RocqIDE main screen .. Here is the code used in the screenshot: @@ -41,7 +42,7 @@ for CoqIDE. Use `coqide --help` to see the list of command line options. Proof. Induction n. -The screenshot shows CoqIDE as the user is stepping through the file `Fermat.v`. +The screenshot shows RocqIDE as the user is stepping through the file `Fermat.v`. A menu bar and a tool bar appear at the top of the window. The left-hand panel shows the current *script buffer*. Each script buffer corresponds to a separate Coq process. @@ -90,10 +91,10 @@ the cursor between `(*` and `*)` or select any text between them. Files are automatically saved periodically to a recovery file. For example, `foo.v` is saved to `#foo.v#` every 10 seconds by default. You can change the -interval in the *Edit / Preferences / Files* dialog. In some cases when CoqIDE -exits abruptly, it saves named buffers in ``.crashcoqide`` in the same +interval in the *Edit / Preferences / Files* dialog. In some cases when RocqIDE +exits abruptly, it saves named buffers in ``.crashrocqide`` in the same directory as ````. Unnamed buffers are saved in -``Unnamed_coqscript_.crashcoqide`` in the directory that CoqIDE was started in. +``Unnamed_rocqscript_.crashrocqide`` in the directory that RocqIDE was started in. In the *View* menu, you can set several printing options that correspond to options that can appear in the script. For example, *Display @@ -112,8 +113,8 @@ from the toolbar and from the keyboard. These include: - Reset Coq (`Alt-Home`) to restart the Coq process - Run to end (`Alt-End`) to run commands to the end of the buffer - Interrupt to stop processing commands after the current command completes. - (Note: on Windows but not on WSL, Interrupt doesn't work if you start CoqIDE - as a background process, e.g. `coqide &` in bash. See Coq issue + (Note: on Windows but not on WSL, Interrupt doesn't work if you start RocqIDE + as a background process, e.g. `rocqide &` in bash. See Rocq issue `#16142 `_.) On macOS, use `Cmd-Ctrl` instead of `Alt` for these operations. @@ -137,7 +138,7 @@ Commands may: Double click on an entry to jump to the point of the error. Execution of commands stops unless you're in async mode. -In the previous figure :ref:`CoqIDE main screen `, +In the previous figure :ref:`RocqIDE main screen `, the running buffer is `Fermat.v`. All commands until the ``Theorem`` have already been executed, then the user tried to go forward executing ``Induction n``. That command failed because no such @@ -159,7 +160,7 @@ The other buttons on the toolbar do the following: - Next occurrence (right arrow icon) - find the next occurrence of the current word -The colored ribbon appearing across the bottom of the CoqIDE window just above +The colored ribbon appearing across the bottom of the RocqIDE window just above the status bar represents the state of processing for the current script schematically. Blue means unprocessed, light green means successfully processed, red mean an error, light orange is used for :cmd:`Axiom` and :cmd:`Admitted` @@ -169,7 +170,7 @@ in the async mode section.) The left edge of the ribbon corresponds to the first command or tactic in the script and the right edge corresponds to the last command that has been passed -to Coq. Currently, for very long scripts, it may take many seconds for CoqIDE to +to Rocq. Currently, for very long scripts, it may take many seconds for RocqIDE to pass all the commands to the server, causing the display to jump around a lot. Perhaps this will be improved in a future release. The text at the far right hand side of the status bar (e.g. "0 / 1" gives the number of unprocessed proofs that have been @@ -218,8 +219,8 @@ commands like ``Fixpoint`` that you can conveniently fill in afterwards. Queries ------- -.. image:: ../_static/coqide-queries.png - :alt: CoqIDE queries +.. image:: ../_static/rocqide-queries.png + :alt: RocqIDE queries A *query* is any command that does not change the current state, such as :cmd:`About`, :cmd:`Check`, :cmd:`Print`, :cmd:`Search`, etc. The *query pane* @@ -257,7 +258,7 @@ the *Externals* section of the *Edit/Preferences* dialog. Output appears in the in :ref:`here `. Alternatively, you may find it easier to do your `make` and `rocq makefile` commands from the command line. -.. _coqide_make_note: +.. _rocqide_make_note: Note that you must explicitly save changed buffers before you run `make`. *File/Save all* is helpful for this. Notice that modified and unmodified buffers show @@ -284,14 +285,14 @@ Preferences You may customize your environment with the *Preferences* dialog, which is accessible from *Edit/Preferences* on the menu. There are several sections. -.. image:: ../_static/coqide-preferences-editor.png - :alt: CoqIDE preferences dialog, Editor section +.. image:: ../_static/rocqide-preferences-editor.png + :alt: RocqIDE preferences dialog, Editor section The *Files* section is devoted to file management: you may configure automatic saving of files, by periodically saving the contents into files named `#f#` for each opened file `f`. You may also activate the *auto reload* feature: in case an opened file is modified on disk by a -third party, CoqIDE may read it again for you. Note that in the case +third party, RocqIDE may read it again for you. Note that in the case you edited that same file, you will be prompted to choose to either discard your changes or not. The File charset encoding choice is described below in :ref:`character-encoding-saved-files`. @@ -304,7 +305,7 @@ customizing the editor. It includes in particular the ability to activate an Emacs mode named micro-Proof-General (use the Help menu to know more about the available bindings). -The *Appearance* section offers controls to set CoqIDE's window +The *Appearance* section offers controls to set RocqIDE's window default size and the position of tabs. The *Fonts* section is for selecting the text font used for scripts, @@ -316,7 +317,7 @@ as standard |GtkSourceView| styles are available. Other styles can be added e.g. in ``$HOME/.local/share/gtksourceview-3.0/styles/`` (see the general documentation about |GtkSourceView| for the various possibilities). Note that the style of the rest of graphical part of -CoqIDE is not under the control of |GtkSourceView| but of GTK+ and +RocqIDE is not under the control of |GtkSourceView| but of GTK+ and governed by files such as ``settings.ini`` and ``gtk.css`` in ``$XDG_CONFIG_HOME/gtk-3.0`` or files in ``$HOME/.themes/NameOfTheme/gtk-3.0``, as well as the environment @@ -352,7 +353,7 @@ 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`. -.. _coqide_key_bindings: +.. _rocqide_key_bindings: .. _key_bindings: @@ -363,8 +364,8 @@ As explained just above, the *Edit/Preferences/Shortcuts* panel offers buttons to modify in a few clicks the key bindings for a whole menu. Here is a screenshot of the panel: -.. image:: ../_static/coqide-preferences-shortcuts.png - :alt: CoqIDE preferences dialog, Shortcuts section +.. image:: ../_static/rocqide-preferences-shortcuts.png + :alt: RocqIDE preferences dialog, Shortcuts section Each menu item in the GUI shows its key binding, if one has been defined, on the right-hand side. Typing the key binding is equivalent to selecting @@ -376,8 +377,8 @@ 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 the :ref:`user configuration directory`. -Make sure there are no CoqIDE processes running while you edit the file -(CoqIDE creates or overwrites the file when it terminates, +Make sure there are no RocqIDE processes running while you edit the file +(RocqIDE creates or overwrites the file when it terminates, which may reorder the lines). The file contains lines such as: @@ -393,14 +394,14 @@ which was bound by default to `Shift-Ctrl-A`. `` indicates `Cmd` on mac and otherwise `Ctrl`. The second line is for a menu item that has no key binding. -Lines that begin with semicolons are comments created by CoqIDE. CoqIDE uses +Lines that begin with semicolons are comments created by RocqIDE. RocqIDE uses the default binding for these items. To change a key binding, remove the semicolon and set the third item in the list as desired, such as in the third line. Avoid assigning the same binding to multiple items. If the same menu item name appears on multiple lines in the file, the value from the last line is used. This is convenient for copying a group of changes from elsewhere–just -insert the changes at the end of the file. The next time CoqIDE terminates, it will +insert the changes at the end of the file. The next time RocqIDE terminates, it will resort the items. The end of @@ -417,9 +418,9 @@ Edit/Preferences/Shortcuts panel. See :ref:`Shortcuts`. Using Unicode symbols --------------------- -CoqIDE is based on GTK+ and inherits from it support for Unicode in +RocqIDE is based on GTK+ and inherits from it support for Unicode in its text panels. Consequently a large set of symbols is available for -notations. Furthermore, CoqIDE conveniently provides a simple way to +notations. Furthermore, RocqIDE conveniently provides a simple way to input Unicode characters. @@ -440,8 +441,8 @@ mathematical symbols ∀ and ∃, you may define: : type_scope. A small set of such notations are already defined in the Coq library -which you can enable with ``Require Import Unicode.Utf8`` inside CoqIDE, -or equivalently, by starting CoqIDE with ``coqide -l utf8``. +which you can enable with ``Require Import Unicode.Utf8`` inside RocqIDE, +or equivalently, by starting RocqIDE with ``rocqide -l utf8``. However, there are some issues when using such Unicode symbols: you of course need to use a character font which supports them. In the Fonts @@ -452,12 +453,12 @@ use antialiased fonts or not, by setting the environment variable `GDK_USE_XFT` to 1 or 0 respectively. -.. _coqide-unicode: +.. _rocqide-unicode: Bindings for input of Unicode symbols ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -CoqIDE supports a builtin mechanism to input non-ASCII symbols. +RocqIDE supports a builtin mechanism to input non-ASCII symbols. For example, to input ``π``, it suffices to type ``\pi`` then press the combination of key ``Ctrl-Space`` (default key binding). Often, it suffices to type a prefix of the LaTeX token, e.g. typing ``\p`` @@ -468,7 +469,7 @@ right arrow, or ``\>=`` for a greater than or equal sign. A larger number of LaTeX tokens are supported by default. The full list is available here: -https://github.com/coq/coq/blob/master/ide/coqide/default_bindings_src.ml +https://github.com/coq/coq/blob/master/ide/rocqide/default_bindings_src.ml Custom bindings may be added, as explained further on. @@ -478,7 +479,7 @@ of the preferences. .. note:: It remains possible to input non-ASCII symbols using system-wide - approaches independent of CoqIDE. + approaches independent of RocqIDE. Adding custom bindings @@ -508,7 +509,7 @@ Similarly, the above settings ensure than ``\l`` resolves to ``\le``, and that ``\la`` resolves to ``\lambda``. It can be useful to work with per-project binding files. For this purpose -CoqIDE accepts a command line argument of the form +RocqIDE accepts a command line argument of the form ``-unicode-bindings file1,file2,...,fileN``. Each of the file tokens provided may consists of one of: @@ -542,7 +543,7 @@ related to the way files are saved. If you have no need to exchange files with non-UTF-8 aware applications, it is better to choose the UTF-8 encoding, since it guarantees that your files will be read again without problems. (This -is because when CoqIDE reads a file, it tries to automatically detect +is because when RocqIDE reads a file, it tries to automatically detect its character encoding.) If you choose something else than UTF-8, then missing characters will @@ -550,13 +551,13 @@ be written encoded by `\x{....}` or `\x{........}` where each dot is an hexadecimal digit: the number between braces is the hexadecimal Unicode index for the missing character. -.. _coqide-debugger: +.. _rocqide-debugger: Debugger -------- Version 8.15 introduces a visual debugger for |Ltac| tactics within -CoqIDE. It supports setting breakpoints visually and automatically +RocqIDE. It supports setting breakpoints visually and automatically displaying the stopping point in the source code with "continue", "step over" "step in" and "step out" operations. The call stack and variable values for each stack frame are shown in a new panel. @@ -581,7 +582,7 @@ shown with a dark blue background. `Set Ltac Debug.` enables stopping in the debugger. .. image:: ../_static/debugger.png - :alt: CoqIDE Debugger + :alt: RocqIDE Debugger .. created with: Set Ltac Debug. (* enable the debugger *) @@ -647,7 +648,7 @@ Break (F11) Stops the debugger at the next possible stopping point, from which you can step or continue. (Not supported in Windows at this time.) -Note that the debugger is disabled when CoqIDE is running multiple worker processes, +Note that the debugger is disabled when RocqIDE is running multiple worker processes, i.e. running in async mode. Going "Forward" a single step at a time doesn't use async mode and will always enter the debugger as expected. In addition, the debugger doesn't work correctly in some cases involving editing failed proofs in asymc mode ( @@ -671,7 +672,7 @@ indication that this has happened. .. unfortunately not working: Note: This `Wiki page `_ - describes a way to change CoqIDE key bindings. + describes a way to change RocqIDE key bindings. Call Stack and Variables ~~~~~~~~~~~~~~~~~~~~~~~~ @@ -740,7 +741,7 @@ If a debugger instance is stopped in a secondary script, the debugger function keys are directed to the debugger instance associated with the primary script. The debugger doesn't attempt to support multiple instances stopped in the same secondary script. If you have a need to do this, run -each debugger instance in a separate CoqIDE process/window. +each debugger instance in a separate RocqIDE process/window. Note that if you set a breakpoint in a script that may be called by multiple debugger instances, you may inadvertently find you've gotten into unsupported territory. diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 342f9a84cc96..98a94b6b36d3 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -196,9 +196,9 @@ We recommend checking `CoqMakefile` and `CoqMakefile.conf` into your source code control system. Also we recommend updating them with `rocq makefile` when you switch to a new version of Rocq. -In CoqIDE, you must explicitly save modified buffers before running `make` and +In RocqIDE, you must explicitly save modified buffers before running `make` and restart the Rocq interpreter in any buffers in which you're running code. -More details :ref:`here `. +More details :ref:`here `. See :ref:`rocq_makefile` for a complete description of `rocq makefile` and the files it generates. @@ -244,7 +244,7 @@ permits loading files from the associated directory with just the basename of the script file, e.g. specify `Foo` to load `Foo.vo`. This entry corresponds to the current directory when Rocq was started. Note that the :cmd:`Cd` command -doesn't change the associated directory--you would need to restart CoqIDE. +doesn't change the associated directory--you would need to restart RocqIDE. With some exceptions noted below, the :term:`load path` is generated from files loaded from the following directories and their subdirectories in the order shown. The @@ -262,7 +262,7 @@ directory, e.g. the file `Foo/Bar/script.vo` becomes `Foo.Bar.script`: - the ``${XDG_DATA_HOME}/coq/`` directory (see `XDG base directory specification `_). - However, CoqIDE relies on the default setting; therefore we recommend not + However, RocqIDE relies on the default setting; therefore we recommend not setting this variable. - installed packages from the `user-contrib` directory in the Rocq installation, - the Rocq standard library from the `theories` directory in the Rocq installation @@ -438,7 +438,7 @@ name, e.g. ``DECLARE PLUGIN "my-package.plugin"``. The ``-native-compiler`` option given in the ``_CoqProject`` file overrides the global one passed at configure time. -CoqIDE, Proof General, VsCoq and Coqtail all +RocqIDE, Proof General, VsCoq and Coqtail all understand ``_CoqProject`` files and can be used to invoke Rocq with the desired options. The ``rocq makefile`` utility can be used to set up a build infrastructure diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 0fd6387de693..847e94c1a853 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -2400,8 +2400,8 @@ Interactive debugger This flag, when set, enables the step-by-step debugger in the |Ltac| interpreter. The debugger is supported in `rocq repl` and Proof General by printing information - on the console and accepting typed commands. In addition, CoqIDE now supports a - :ref:`visual debugger ` with additional capabilities. + on the console and accepting typed commands. In addition, RocqIDE now supports a + :ref:`visual debugger ` with additional capabilities. When the debugger is activated in `rocq repl`, it stops at every step of the evaluation of the current |Ltac| expression and prints information on what it is doing. @@ -2431,7 +2431,7 @@ A non-interactive mode for the debugger is available via the flag: This flag has the effect of presenting a newline at every prompt, when the debugger is on in `rocq repl`. (It has no effect when running the - CoqIDE debugger.) The debug log thus created, which does not require + RocqIDE debugger.) The debug log thus created, which does not require user input to generate when this flag is set, can then be run through external tools such as diff. diff --git a/doc/sphinx/proofs/writing-proofs/proof-mode.rst b/doc/sphinx/proofs/writing-proofs/proof-mode.rst index 84b365f9d9d4..b7bd321944f6 100644 --- a/doc/sphinx/proofs/writing-proofs/proof-mode.rst +++ b/doc/sphinx/proofs/writing-proofs/proof-mode.rst @@ -11,7 +11,7 @@ you complete a proof, such as with the :cmd:`Qed` command. Tactics, which are available only in proof mode, incrementally transform incomplete proofs to eventually generate a complete proof. -When you run Rocq interactively, such as through CoqIDE, Proof General or +When you run Rocq interactively, such as through RocqIDE, Proof General or `rocq repl`, Rocq shows the current proof state (the incomplete proof) as you enter tactics. This information isn't shown when you run Rocq in batch mode with `rocq compile`. @@ -1034,7 +1034,7 @@ Showing differences between proof steps Rocq can automatically highlight the differences between successive proof steps and between values in some error messages. Rocq can also highlight differences in the proof term. -For example, the following screenshots of CoqIDE and coqtop show the application +For example, the following screenshots of RocqIDE and coqtop show the application of the same :tacn:`intros` tactic. The tactic creates two new hypotheses, highlighted in green. The conclusion is entirely in pale green because although it’s changed, no tokens were added to it. The second screenshot uses the "removed" option, so it shows the conclusion a @@ -1057,25 +1057,25 @@ new, no line of old text is shown for them. .. - .. image:: ../../_static/diffs-coqide-on.png - :alt: CoqIDE with Set Diffs on + .. image:: ../../_static/diffs-rocqide-on.png + :alt: RocqIDE with Set Diffs on .. - .. image:: ../../_static/diffs-coqide-removed.png - :alt: CoqIDE with Set Diffs removed + .. image:: ../../_static/diffs-rocqide-removed.png + :alt: RocqIDE with Set Diffs removed .. .. image:: ../../_static/diffs-coqtop-on3.png :alt: coqtop with Set Diffs on -This image shows an error message with diff highlighting in CoqIDE: +This image shows an error message with diff highlighting in RocqIDE: .. .. image:: ../../_static/diffs-error-message.png - :alt: CoqIDE error message with diffs + :alt: RocqIDE error message with diffs How to enable diffs ``````````````````` @@ -1098,8 +1098,8 @@ Colors for `rocq repl` can be configured by setting the ``ROCQ_COLORS`` environm variable. See section :ref:`customization-by-environment-variables`. Diffs use the tags ``diff.added``, ``diff.added.bg``, ``diff.removed`` and ``diff.removed.bg``. -In CoqIDE, diffs should be enabled from the ``View`` menu. Don’t use the ``Set Diffs`` -command in CoqIDE. You can change the background colors shown for diffs from the +In RocqIDE, diffs should be enabled from the ``View`` menu. Don’t use the ``Set Diffs`` +command in RocqIDE. You can change the background colors shown for diffs from the ``Edit | Preferences | Tags`` panel by changing the settings for the ``diff.added``, ``diff.added.bg``, ``diff.removed`` and ``diff.removed.bg`` tags. This panel also lets you control other attributes of the highlights, such as the foreground @@ -1177,16 +1177,16 @@ the split because it has not changed. .. - .. image:: ../../_static/diffs-coqide-multigoal.png - :alt: coqide with Set Diffs on with multiple goals + .. image:: ../../_static/diffs-rocqide-multigoal.png + :alt: rocqide with Set Diffs on with multiple goals Diffs may appear like this after applying a :tacn:`intro` tactic that results in a compacted hypotheses: .. - .. image:: ../../_static/diffs-coqide-compacted.png - :alt: coqide with Set Diffs on with compacted hypotheses + .. image:: ../../_static/diffs-rocqide-compacted.png + :alt: rocqide with Set Diffs on with compacted hypotheses .. _showing_proof_diffs: @@ -1197,7 +1197,7 @@ To show differences in the proof term: - In `rocq repl` and Proof General, use the :cmd:`Show Proof` `Diffs` command. -- In CoqIDE, position the cursor on or just after a tactic to compare the proof term +- In RocqIDE, position the cursor on or just after a tactic to compare the proof term after the tactic with the proof term before the tactic, then select `View / Show Proof` from the menu or enter the associated key binding. Differences will be shown applying the current `Show Diffs` setting @@ -1209,7 +1209,7 @@ To show differences in the proof term: .. .. image:: ../../_static/diffs-show-proof.png - :alt: coqide with Set Diffs on with compacted hypotheses + :alt: rocqide with Set Diffs on with compacted hypotheses Delaying solving unification constraints ---------------------------------------- diff --git a/doc/sphinx/using/tools/index.rst b/doc/sphinx/using/tools/index.rst index 781411b7e67c..5fb433b15eb4 100644 --- a/doc/sphinx/using/tools/index.rst +++ b/doc/sphinx/using/tools/index.rst @@ -5,9 +5,9 @@ Command-line and graphical tools ================================ This chapter presents the command-line tools that users will need to -build their Rocq project, the documentation of the CoqIDE graphical +build their Rocq project, the documentation of the RocqIDE graphical user interface and the documentation of the parallel proof processing -feature that is supported by CoqIDE and several other GUIs. +feature that is supported by RocqIDE and several other GUIs. A list of available user interfaces to interact with Rocq is available on the `Coq website `_. diff --git a/dune-project b/dune-project index 4ca15ca32f0b..7ffc687c5eff 100644 --- a/dune-project +++ b/dune-project @@ -88,11 +88,11 @@ 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.")) (package - (name coqide) + (name rocqide) (depends (ocamlfind :build) (conf-findutils :build) @@ -106,7 +106,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 CoqIDE, a graphical user interface for the +This package provides the RocqIDE, a graphical user interface for the development of interactive proofs.")) (package diff --git a/ide/coqide/coq-ssreflect.lang b/ide/coqide/coq-ssreflect.lang deleted file mode 100644 index d71277f42cc1..000000000000 --- a/ide/coqide/coq-ssreflect.lang +++ /dev/null @@ -1,249 +0,0 @@ - - - - *.v - \(\* - \*\) - - - -