env vars: try reading ROCQRUNTIMELIB and ROCQLIB before COQCORELIB / …

…COQLIB

should we stop reading COQCORELIB? It meaning the location of
rocq-runtime is a bit wrong.

INSTALL.md

@@ -114,10 +114,10 @@ implementation mismatch on ...`.
 
 coq_environment.txt
 -------------------
-Coq binaries which honor environment variables, such as `COQLIB`, can
+Coq binaries which honor environment variables, such as `ROCQLIB`, can
 be seeded values for these variables by placing a text file named
 `coq_environment.txt` next to them. The file can contain assignments
-like `COQLIB="some path"`, that is a variable name followed by `=` and
+like `ROCQLIB="some path"`, that is a variable name followed by `=` and
 a string that follows OCaml's escaping conventions. This feature can be
 used by installers of binary package to make Coq aware of its installation
 path.

Makefile

@@ -235,7 +235,7 @@ CONTEXT=_build/install/default
 .PHONY: plugin-tutorial
 plugin-tutorial: dunestrap
 	dune build $(CONTEXT)/lib/rocq-runtime/META $(CONTEXT)/lib/coq-core/META rocq-runtime.install coq-core.install theories/Init/Prelude.vo
-	+$(MAKE) OCAMLPATH=$(shell pwd)/$(CONTEXT)/lib/ COQBIN=$(shell pwd)/$(CONTEXT)/bin/ COQCORELIB=$(shell pwd)/$(CONTEXT)/lib/rocq-runtime COQLIB=$(shell pwd)/_build/default/ -C doc/plugin_tutorial
+	+$(MAKE) OCAMLPATH=$(shell pwd)/$(CONTEXT)/lib/ COQBIN=$(shell pwd)/$(CONTEXT)/bin/ ROCQRUNTIMELIB=$(shell pwd)/$(CONTEXT)/lib/rocq-runtime ROCQLIB=$(shell pwd)/_build/default/ -C doc/plugin_tutorial
 
 # This is broken in a very weird way with a permission error... see
 # the rule in doc/plugin_tutorial/dune:

boot/env.ml

@@ -39,14 +39,15 @@ let plugins_dir = "plugins"
 let prelude = Filename.concat theories_dir "Init/Prelude.vo"
 
 let guess_coqlib () =
+  Util.getenv_else "ROCQLIB" (fun () ->
   Util.getenv_else "COQLIB" (fun () ->
   Util.check_file_else
     ~dir:Coq_config.coqlibsuffix
     ~file:prelude
     (fun () ->
       if Sys.file_exists (Filename.concat Coq_config.coqlib prelude)
       then Coq_config.coqlib
-      else fail ()))
+      else fail ())))
 
 (* Build layout uses coqlib = coqcorelib *)
 let guess_coqcorelib lib =
@@ -59,15 +60,15 @@ let fail_lib lib =
   eprintf "File not found: %s\n" lib;
   eprintf "The path for Coq libraries is wrong.\n";
   eprintf "Coq prelude is shipped in the rocq-core package.\n";
-  eprintf "Please check the COQLIB env variable or the -coqlib option.\n";
+  eprintf "Please check the ROCQLIB env variable or the -coqlib option.\n";
   exit 1
 
 let fail_core plugin =
   let open Printf in
   eprintf "File not found: %s\n" plugin;
   eprintf "The path for Coq plugins is wrong.\n";
   eprintf "Coq plugins are shipped in the rocq-runtime package.\n";
-  eprintf "Please check the COQCORELIB env variable.\n";
+  eprintf "Please check the ROCQRUNTIMELIB env variable.\n";
   exit 1
 
 let validate_env ({ core; lib } as env) =
@@ -81,8 +82,9 @@ let validate_env ({ core; lib } as env) =
    mis-use for example when we pass command line arguments *)
 let init () =
   let lib = guess_coqlib () in
-  let core = Util.getenv_else "COQCORELIB"
-      (fun () -> guess_coqcorelib lib) in
+  let core = Util.getenv_else "ROCQRUNTIMELIB"
+      (fun () -> Util.getenv_else "COQCORELIB"
+      (fun () -> guess_coqcorelib lib)) in
   validate_env { core ; lib }
 
 let env_ref = ref None

boot/env.mli

@@ -27,17 +27,17 @@ multiple accesses to the environment, do initialize it once and keep a ref
 to it. We don't forbid yet double initialization, (second time is a noop)
 but we may do so in the future. Rules for "coqlib" are:
 
-- the [COQLIB] env variable will be used if set
+- the [ROCQLIB] env variable will be used if set
 - if not, the existence of [theories/Init/Prelude.vo] will be checked,
   in the following order:
   + [coqlibsuffix] given in configure
   + [coqlib] given in configure
 - if none of the above succeeds, the initialization will fail
 
-- The [COQCORELIB] env variable is also used if set, if not, the location
-  of the rocq-runtime files will be assumed to be [COQLIB/../rocq-runtime], except
-  if [COQLIB/plugins] exists [as in some developers layouts], in which case
-  we will set [COQCORELIB:=COQLIB].
+- The [ROCQRUNTIMELIB] env variable is also used if set, if not, the location
+  of the rocq-runtime files will be assumed to be [ROCQLIB/../rocq-runtime], except
+  if [ROCQLIB/plugins] exists [as in some developers layouts], in which case
+  we will set [ROCQRUNTIMELIB:=ROCQLIB].
 
 Note that [set_coqlib] is used by some commands to process the [-coqlib] option,
 as of now this sets both [coqlib] and [coqcorelib]; this part of the initialization

dev/ci/ci-common.sh

@@ -8,7 +8,7 @@ export NJOBS
 
 if which cygpath >/dev/null 2>&1; then OCAMLFINDSEP=\;; else OCAMLFINDSEP=:; fi
 
-# We can remove setting COQLIB and COQCORELIB from here, but better to
+# We can remove setting ROCQLIB and ROCQRUNTIMELIB from here, but better to
 # wait until we have merged the coq.boot patch so we can do this in a
 # more controlled way.
 if [ -n "${GITLAB_CI}" ];
@@ -32,8 +32,8 @@ 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 COQCORELIB="$PWD/_build/install/default/lib/rocq-runtime"
+    export ROCQLIB="$PWD/_build/install/default/lib/coq"
+    export ROCQRUNTIMELIB="$PWD/_build/install/default/lib/rocq-runtime"
 
     CI_INSTALL_DIR="$PWD/_build/install/default/"
 

dev/ci/nix/unicoq/default.nix

@@ -15,7 +15,7 @@ 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 = [ "ROCQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
 
   postInstall = ''
     cp ${META} META

doc/plugin_tutorial/dune

@@ -7,7 +7,7 @@
 ;    ../../tools/CoqMakefile.in
 ;    ../../theories/Init/Prelude.vo)
 ;  (action
-;    (bash "make COQCORELIB=$(pwd)/../../ COQLIB=$(pwd)/../../")))
+;    (bash "make ROCQRUNTIMELIB=$(pwd)/../../ ROCQLIB=$(pwd)/../../")))
 
 
 (env

doc/sphinx/changes.rst

@@ -11514,7 +11514,7 @@ Interfaces
 - Coqtop/coqc outputs highlighted syntax. Colors can be configured thanks
   to the COQ_COLORS environment variable, and their current state can
   be displayed with the -list-tags command line option.
-- Third party user interfaces can install their main loop in $COQLIB/toploop
+- Third party user interfaces can install their main loop in $ROCQLIB/toploop
   and call coqtop with the -toploop flag to select it.
 
 Internal Infrastructure

doc/sphinx/practical-tools/coq-commands.rst

@@ -158,7 +158,7 @@ except that ``space_overhead`` is set to 120 and ``minor_heap_size`` is set to 3
    an incorrect warning: coq-commands.rst:4: WARNING: Duplicate explicit target name: "here".
    The warning doesn't even have the right line number. :-(
 
-.. todo how about COQLIB, COQCORELIB, DOCDIR
+.. todo how about ROCQLIB, ROCQRUNTIMELIB, DOCDIR
 
 .. _ROCQ_PROFILE_COMPONENTS:
 
@@ -637,7 +637,7 @@ relative paths in object files ``-Q`` and ``-R`` have exactly the same meaning.
   assumptions and variables (constants without a :term:`body`).
 :-silent: Do not write progress information to the standard output.
 
-Environment variable ``$COQLIB`` can be set to override the location of
+Environment variable ``$ROCQLIB`` can be set to override the location of
 the standard library.
 
 The algorithm for deciding which modules are checked or admitted is

doc/sphinx/practical-tools/utilities.rst

@@ -645,7 +645,7 @@ section of the generated makefile. These include:
 :COQLIBINSTALL, COQPLUGININSTALL, COQDOCINSTALL:
    specify where the Rocq libraries, plugins and documentation will be installed.
    By default a combination of ``$(DESTDIR)`` (if defined) with
-   ``$(COQLIB)/user-contrib``, ``$(COQCORELIB)/..`` and ``$(DOCDIR)/coq/user-contrib``.
+   ``$(ROCQLIB)/user-contrib``, ``$(ROCQRUNTIMELIB)/..`` and ``$(DOCDIR)/coq/user-contrib``.
 
 Use :ref:`rocqmakefilelocallate` instead to access more variables.
 

doc/sphinx/user-extensions/syntax-extensions.rst

@@ -1453,7 +1453,7 @@ Note that `_` by itself is a valid :n:`@name` but is not a valid :n:`@ident`.
           time. Type checking is done only at the time of use of the notation.
 
 .. note:: Some examples of Notation may be found in the files composing
-          the initial state of Rocq (see directory :file:`$COQLIB/theories/Init`).
+          the initial state of Rocq (see directory :file:`$ROCQLIB/theories/Init`).
 
 .. note:: The notation ``"{ x }"`` has a special status in the main grammars of
           terms and patterns so that
@@ -2612,7 +2612,7 @@ Tactic notations allow customizing the syntax of tactics.
       Tactic Notation "destruct_with_eqn" constr(x) := destruct x eqn:?.
 
    For a complex example, examine the 16 `Tactic Notation "setoid_replace"`\s
-   defined in :file:`$COQLIB/theories/Classes/SetoidTactics.v`, which are designed
+   defined in :file:`$ROCQLIB/theories/Classes/SetoidTactics.v`, which are designed
    to accept any subset of 4 optional parameters.
 
    The nonterminals that can specified in the tactic notation are:

sysinit/coqinit.mli

@@ -42,7 +42,7 @@ val parse_arguments :
 
 (** 3 initialization of global runtime data
 
-    All global setup is done here, like COQLIB and the paths for native
+    All global setup is done here, like ROCQLIB and the paths for native
     compilation. If Coq is used to process multiple libraries, what is set up
     here is really global and common to all of them.
 

test-suite/Makefile

@@ -58,19 +58,19 @@ endif
 export OCAMLPATH := $(shell echo $(COQPREFIX)/lib$(FINDLIB_SEP)$$OCAMLPATH)
 export CAML_LD_LIBRARY_PATH:=$(shell echo $(COQPREFIX)/lib/stublibs):$(CAML_LD_LIBRARY_PATH)
 
-# COQLIB is an env variable so no quotes
-COQLIB?=
+# ROCQLIB is an env variable so no quotes
+ROCQLIB?=
 
-ifeq ($(COQLIB),)
+ifeq ($(ROCQLIB),)
 # Guard againt the COQLIBINSTALL directory not existing, otherwise
 # ocaml_pwd will error
 ifneq ($(wildcard $(shell echo $(COQLIBINSTALL))),)
-	COQLIB := $(shell ocaml ocaml_pwd.ml $(COQLIBINSTALL))
+	ROCQLIB := $(shell ocaml ocaml_pwd.ml $(COQLIBINSTALL))
 endif
 endif
-export COQLIB
+export ROCQLIB
 
-ifeq ($(wildcard $(COQLIB)/theories/Init/Prelude.vo),)
+ifeq ($(wildcard $(ROCQLIB)/theories/Init/Prelude.vo),)
   COQLIB_NOT_FOUND:=true
 else
   COQLIB_NOT_FOUND:=false

test-suite/misc/coq_environment.sh

@@ -11,22 +11,22 @@ mkdir overridden/plugins
 touch overridden/theories/Init/Prelude.vo
 
 cat > coq_environment.txt <<EOT
-# we override COQLIB because we can
-COQLIB="$TMP/overridden" # bla bla
-COQCORELIB="$TMP/overridden" # bla bla
+# we override ROCQLIB because we can
+ROCQLIB="$TMP/overridden" # bla bla
+ROCQRUNTIMELIB="$TMP/overridden" # bla bla
 OCAMLFIND="$TMP/overridden"
 FOOBAR="one more"
 EOT
 
 cp $BIN/rocq .
 cp $BIN/rocq makefile .
 mkdir -p overridden/tools/
-cp $COQLIB/../rocq-runtime/tools/CoqMakefile.in overridden/tools/
+cp $ROCQLIB/../rocq-runtime/tools/CoqMakefile.in overridden/tools/
 
-unset COQLIB
+unset ROCQLIB
 N=`./rocq c -config | grep COQLIB | grep /overridden | wc -l`
 if [ $N -ne 1 ]; then
-  echo COQLIB not overridden by coq_environment
+  echo ROCQLIB not overridden by coq_environment
   coqc -config
   exit 1
 fi
@@ -49,10 +49,10 @@ mkdir -p overridden2/theories/Init/
 mkdir overridden2/plugins
 touch overridden2/theories/Init/Prelude.vo
 
-export COQLIB="$PWD/overridden2"
+export ROCQLIB="$PWD/overridden2"
 N=`./rocq c -config | grep COQLIB | grep overridden2 | wc -l`
 if [ $N -ne 1 ]; then
-  echo COQLIB not overridden by COQLIB when coq_environment present
+  echo ROCQLIB not overridden by ROCQLIB when coq_environment present
   coqc -config
   exit 1
 fi

tools/update-require

@@ -4,7 +4,7 @@
 # targets (or the current directory if none).
 #
 # It assumes that all the prerequisites are already installed. The
-# install location is found using the COQLIB, COQC, COQBIN variables if
+# install location is found using the ROCQLIB, COQC, COQBIN variables if
 # set, 'coqc' otherwise.
 #
 # Option --exclude can be used to ignore a given user contribution. In
@@ -14,10 +14,10 @@
 # Option --stdlib can be used to also qualify the files from the standard
 # library.
 
-if test ! "$COQLIB"; then
+if test ! "$ROCQLIB"; then
   if test ${COQBIN##*/}; then COQBIN=$COQBIN/; fi
   if test ! "$COQC"; then COQC=`which ${COQBIN}coqc`; fi
-  COQLIB=`"$COQC" -where`
+  ROCQLIB=`"$COQC" -where`
 fi
 
 stdlib=no
@@ -30,10 +30,10 @@ scan_dir () {
 
 scan_all_dir () {
   if test $stdlib = yes; then
-    scan_dir "$COQLIB/theories" "Coq."
-    scan_dir "$COQLIB/plugins" "Coq."
+    scan_dir "$ROCQLIB/theories" "Coq."
+    scan_dir "$ROCQLIB/plugins" "Coq."
   fi
-  scan_dir "$COQLIB/user-contrib" "" "$exclude"
+  scan_dir "$ROCQLIB/user-contrib" "" "$exclude"
 }
 
 create_script () {

topbin/rocqshim.ml

@@ -120,7 +120,7 @@ let parse_opts = function
   | args -> { debug_shim = false }, args
 
 let init { debug_shim=debug } args =
-  (* important to putenv before reading OCAMLPATH / COQLIB *)
+  (* important to putenv before reading OCAMLPATH / ROCQLIB *)
   let () = putenv_from_file ~debug () in
   let opts = parse_args args in
   let env_ocamlpath = make_ocamlpath opts in