Rename default install location (lib/coq -> lib/rocq)

.github/workflows/ci-macos.yml

@@ -53,7 +53,7 @@ jobs:
           make clean
           export OCAMLPATH="$(pwd)/../_install_ci/lib":"$OCAMLPATH"
           BIN="$(pwd)/../_install_ci/bin/"
-          LIB="$(pwd)/../_install_ci/lib/coq/"
+          LIB="$(pwd)/../_install_ci/lib/rocq/"
           make -j "$NJOBS" BIN="$BIN" COQLIB="$LIB" PRINT_LOGS=1 TIMED=1 all
         env:
           NJOBS: "2"

.gitlab-ci.yml

@@ -173,8 +173,8 @@ before_script:
     - not-a-real-job
   script:
     - cd _install_ci
-    - find lib/coq/ -name '*.vo' -fprint0 vofiles
-    - xargs -0 --arg-file=vofiles bin/coqchk -o -m -coqlib lib/coq/ > ../coqchk.log 2>&1 || touch coqchk.failed
+    - find lib/rocq/ -name '*.vo' -fprint0 vofiles
+    - xargs -0 --arg-file=vofiles bin/coqchk -o -m -coqlib lib/rocq/ > ../coqchk.log 2>&1 || touch coqchk.failed
     - tail -n 1000 ../coqchk.log # the log is too big for gitlab so pipe to a file and display the tail
     - "[ ! -f coqchk.failed ]" # needs quoting for yml syntax reasons
   artifacts:
@@ -346,8 +346,8 @@ build:base:dev:dune:
     - cp theories/dune.disabled theories/dune
     - cp user-contrib/Ltac2/dune.disabled user-contrib/Ltac2/dune
     - dune build -p rocq-runtime,coq-core,rocq-core,coqide-server
-    - ls _build/install/default/lib/coq/theories/Init/Prelude.vo
-    - ls _build/install/default/lib/coq/user-contrib/Ltac2/Ltac2.vo
+    - ls _build/install/default/lib/rocq/theories/Init/Prelude.vo
+    - ls _build/install/default/lib/rocq/user-contrib/Ltac2/Ltac2.vo
   only: *full-ci
 
 build:base+async:

Makefile

@@ -267,7 +267,7 @@ define subtarget =
   .PHONY: theories-$(2)
 
   $(2)_FILES=$$(wildcard $(1)*.v)
-  $(2)_FILES_PATH=$$(addprefix _build/install/default/lib/coq/, $$($(2)_FILES:.v=.vo))
+  $(2)_FILES_PATH=$$(addprefix _build/install/default/lib/rocq/, $$($(2)_FILES:.v=.vo))
 
   theories-$(2):
 	@echo "DUNE $(1)*.vo"

default.nix

@@ -150,8 +150,8 @@ stdenv.mkDerivation rec {
 
   setupHook = writeText "setupHook.sh" "
     addCoqPath () {
-      if test -d \"$1/lib/coq/${coq-version}/user-contrib\"; then
-        export COQPATH=\"\${COQPATH-}\${COQPATH:+:}$1/lib/coq/${coq-version}/user-contrib/\"
+      if test -d \"$1/lib/rocq/${coq-version}/user-contrib\"; then
+        export COQPATH=\"\${COQPATH-}\${COQPATH:+:}$1/lib/rocq/${coq-version}/user-contrib/\"
       fi
     }
 

dev/ci/ci-common.sh

@@ -32,7 +32,7 @@ then
     # Full Dune build, we basically do what `dune exec --` does
     export OCAMLPATH="$PWD/_build/install/default/lib/$OCAMLFINDSEP$OCAMLPATH"
     export COQBIN="$PWD/_build/install/default/bin"
-    export COQLIB="$PWD/_build/install/default/lib/coq"
+    export COQLIB="$PWD/_build/install/default/lib/rocq"
     export COQCORELIB="$PWD/_build/install/default/lib/rocq-runtime"
 
     CI_INSTALL_DIR="$PWD/_build/install/default/"

dev/ci/ci-compcert.sh

@@ -13,7 +13,7 @@ if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi
 # but with excessive memory requirements
 export COQCOPTS='-native-compiler no -w -undeclared-scope -w -omega-is-deprecated'
 ( cd "${CI_BUILD_DIR}/compcert"
-  [ -e Makefile.config ] || ./configure -ignore-coq-version x86_32-linux -install-coqdev -clightgen -use-external-MenhirLib -use-external-Flocq -prefix ${CI_INSTALL_DIR} -coqdevdir ${CI_INSTALL_DIR}/lib/coq/user-contrib/compcert
+  [ -e Makefile.config ] || ./configure -ignore-coq-version x86_32-linux -install-coqdev -clightgen -use-external-MenhirLib -use-external-Flocq -prefix ${CI_INSTALL_DIR} -coqdevdir ${CI_INSTALL_DIR}/lib/rocq/user-contrib/compcert
   make
   make check-proof COQCHK='"$(COQBIN)coqchk" -silent -o $(COQINCLUDES)'
   make install

dev/ci/nix/default.nix

@@ -78,7 +78,7 @@ let flocq = coqPackages.flocq.overrideAttrs (o: {
     src = fetchTarball "https://gitlab.inria.fr/flocq/flocq/-/archive/master/flocq-master.tar.gz";
     configurePhase = ''
       autoreconf
-      ${bash}/bin/bash configure --libdir=$out/lib/coq/${coq.coq-version}/user-contrib/Flocq
+      ${bash}/bin/bash configure --libdir=$out/lib/rocq/${coq.coq-version}/user-contrib/Flocq
     '';
     buildPhase = ''
       ./remake

dev/ci/nix/unicoq/default.nix

@@ -15,12 +15,12 @@ stdenv.mkDerivation {
   buildInputs = [ coq ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 num ]);
 
   configurePhase = "coq_makefile -f Make -o Makefile";
-  installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
+  installFlags = [ "COQLIB=$(out)/lib/rocq/${coq.coq-version}/" ];
 
   postInstall = ''
     cp ${META} META
     install -d $OCAMLFIND_DESTDIR
-    ln -s $out/lib/coq/${coq.coq-version}/user-contrib/Unicoq $OCAMLFIND_DESTDIR/
+    ln -s $out/lib/rocq/${coq.coq-version}/user-contrib/Unicoq $OCAMLFIND_DESTDIR/
     install -m 0644 META src/unicoq.a $OCAMLFIND_DESTDIR/Unicoq
   '';
 }

doc/sphinx/practical-tools/utilities.rst

@@ -218,15 +218,15 @@ which is a list of (logical path, :term:`physical path`) pairs for directories.
 For example, you may see::
 
   Logical Path / Physical path:
-  Bignums /home/jef/coq/lib/coq/user-contrib/Bignums
-  Bignums.BigZ /home/jef/coq/lib/coq/user-contrib/Bignums/BigZ
-  Ltac2 /home/jef/coq/lib/coq/user-contrib/Ltac2
-  Stdlib /home/jef/coq/lib/coq/theories
-  Stdlib.Numbers /home/jef/coq/lib/coq/theories/Numbers
-  Stdlib.Numbers.Natural /home/jef/coq/lib/coq/theories/Numbers/Natural
-  Stdlib.Numbers.Natural.Binary /home/jef/coq/lib/coq/theories/Numbers/Natural/Binary
-  Stdlib.Numbers.Integer /home/jef/coq/lib/coq/theories/Numbers/Integer
-  Stdlib.Arith /home/jef/coq/lib/coq/theories/Arith
+  Bignums /home/jef/coq/lib/rocq/user-contrib/Bignums
+  Bignums.BigZ /home/jef/coq/lib/rocq/user-contrib/Bignums/BigZ
+  Ltac2 /home/jef/coq/lib/rocq/user-contrib/Ltac2
+  Stdlib /home/jef/coq/lib/rocq/theories
+  Stdlib.Numbers /home/jef/coq/lib/rocq/theories/Numbers
+  Stdlib.Numbers.Natural /home/jef/coq/lib/rocq/theories/Numbers/Natural
+  Stdlib.Numbers.Natural.Binary /home/jef/coq/lib/rocq/theories/Numbers/Natural/Binary
+  Stdlib.Numbers.Integer /home/jef/coq/lib/rocq/theories/Numbers/Integer
+  Stdlib.Arith /home/jef/coq/lib/rocq/theories/Arith
   <> /home/jef/myproj
 
 The components of each pair share suffixes, e.g. `Bignums.BigZ` and `Bignums/BigZ` or

doc/sphinx/proof-engine/ltac2.rst

@@ -193,7 +193,7 @@ APIs
 ~~~~
 
 Ltac2 provides over 150 API functions that provide various capabilities.  These
-are declared with :cmd:`Ltac2 external` in :n:`lib/coq/user-contrib/Ltac2/*.v`.
+are declared with :cmd:`Ltac2 external` in :n:`lib/rocq/user-contrib/Ltac2/*.v`.
 For example, `Message.print` defined in `Message.v` is used to print messages:
 
 .. rocqtop:: none

tools/configure/cmdArgs.mli

@@ -19,7 +19,7 @@ type t =
   ; interactive : bool
   (** whether to display a summary *)
   ; libdir : string option
-  (** override $prefix/lib/coq *)
+  (** override $prefix/lib/rocq *)
   ; configdir : string option
   (** override /etc/xdg/coq *)
   ; datadir : string option

tools/configure/configure.ml

@@ -228,7 +228,7 @@ end
 
 let install prefs =
   [ InstallDir.make "COQPREFIX" "Corelib" prefs.prefix (Relative "") (Relative "")
-  ; InstallDir.make "COQLIBINSTALL" "the Coq library" prefs.libdir (Relative "lib/coq") (Relative "lib/coq")
+  ; InstallDir.make "COQLIBINSTALL" "the Coq library" prefs.libdir (Relative "lib/rocq") (Relative "lib/rocq")
   ; InstallDir.make "CONFIGDIR" "the Coqide configuration files" prefs.configdir (Relative "config") (Absolute "/etc/xdg/coq")
   ; InstallDir.make "DATADIR" "the Coqide data files" prefs.datadir (Relative "share/coq") (Relative "share/coq")
   ; InstallDir.make "MANDIR" "the Coq man pages" prefs.mandir (Relative "share/man") (Relative "share/man")

tools/dune_rule_gen/coq_rules.ml

@@ -275,7 +275,7 @@ let coqnative_rules ~dir_info ~cctx = gen_rules ~dir_info ~cctx ~f:coqnative_mod
 
 let install_rule ~(cctx : Context.t) coq_module =
   let tname, rule, package = cctx.theory.dirname, cctx.rule, cctx.theory.directory in
-  let dst_base = Filename.concat "coq" (Path.to_string package) in
+  let dst_base = Filename.concat "rocq" (Path.to_string package) in
   let files =
     Coq_module.install_files ~tname ~rule coq_module
     |> List.map (fun (src,dst) -> src, Filename.concat dst_base dst) in