Merge PR coq#19901: Add relocatable mode

Reviewed-by: ppedrot
Ack-by: Janno
Ack-by: ejgallego
Co-authored-by: ppedrot <[email protected]>

Author: coqbot-app[bot]

.gitlab-ci.yml

@@ -93,7 +93,7 @@ before_script:
     - dev/ci/gitlab-section.sh end coq.clean
 
     - dev/ci/gitlab-section.sh start coq.config coq.config
-    - ./configure -prefix "$(pwd)/_install_ci" $COQ_EXTRA_CONF
+    - ./configure -relocatable $COQ_EXTRA_CONF
     - dev/ci/gitlab-section.sh end coq.config
 
     - dev/ci/gitlab-section.sh start coq.build coq.build
@@ -157,7 +157,7 @@ before_script:
     - cd test-suite
     - make clean
     - export OCAMLPATH=$(readlink -f ../_install_ci/lib/):"$OCAMLPATH"
-    - COQEXTRAFLAGS="${COQEXTRAFLAGS}" make -j "$NJOBS" TIMED=1 all
+    - COQEXTRAFLAGS="${COQEXTRAFLAGS}" make -j "$NJOBS" TIMED=1 all ROCQ_EXE=$(pwd)/../_install_ci/bin/rocq
   artifacts:
     name: "$CI_JOB_NAME.logs"
     when: on_failure

INSTALL.md

@@ -89,17 +89,17 @@ for more details.
 
 To build and install Rocq (and RocqIDE if desired) do:
 
-    $ ./configure -prefix <install_prefix> $options
     $ make dunestrap
     $ dune build -p rocq-runtime,coq-core,rocq-core,coq,coqide-server,rocqide
     $ dune install --prefix=<install_prefix> rocq-runtime coq-core rocq-core coq coqide-server rocqide
 
 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
-where to find its standard library, but doesn't control any other
-installation path these days.
+installation paths, and the `-libdir` argument for `./configure` to tell Rocq
+where to find its standard library, (`configure` doesn't control
+installation paths these days). See refman "Command-line and graphical tools"
+-> "The Rocq Prover commands" -> "System configuration" for more info.
 
 OCaml toolchain advisory
 ------------------------

Makefile

@@ -89,7 +89,6 @@ help-install:
 	@echo "The Dune-based Rocq build is split into several packages; see Dune and dev/doc"
 	@echo "documentation for more details. A quick install of Rocq alone can be done with"
 	@echo ""
-	@echo " $$ ./configure -prefix <install_prefix>"
 	@echo " $$ make dunestrap"
 	@echo " $$ dune build -p rocq-runtime,coq-core,rocq-core"
 	@echo " $$ dune install --prefix=<install_prefix> rocq-runtime coq-core rocq-core"

boot/dune

@@ -6,7 +6,7 @@
  (synopsis "Rocq Enviroment and Paths facilities")
  ; until ocaml/dune#4892 fixed
  ; (private_modules util)
- (libraries rocq-runtime.config))
+ (libraries rocq-runtime.config rocq-runtime.clib))
 
 (deprecated_library_name
  (old_public_name coq-core.boot)

boot/env.ml

@@ -24,14 +24,6 @@ type t =
   ; lib : Path.t
   }
 
-(* fatal error *)
-let fail_msg =
-  "cannot guess a path for Rocq libraries; please use -coqlib option \
-   or ensure you have installed the package containing Rocq's prelude (rocq-core in OPAM) \
-   If you intend to use Rocq without prelude, the -boot -noinit options must be used."
-
-let fail s = Format.eprintf "%s@\n%!" fail_msg; exit 1
-
 (* This code needs to be refactored, for now it is just what used to be in envvars  *)
 
 let use_suffix prefix suffix =
@@ -54,21 +46,54 @@ let theories_dir = "theories"
 let plugins_dir = "plugins"
 let prelude = Filename.concat theories_dir "Init/Prelude.vo"
 
-let coqbin =
-  canonical_path_name (Filename.dirname Sys.executable_name)
+let find_in_PATH f =
+  match Sys.getenv_opt "PATH" with
+  | None -> None
+  | Some paths ->
+    let sep = if Coq_config.arch_is_win32 then ';' else ':' in
+    let paths = String.split_on_char sep paths in
+    paths |> List.find_opt (fun path ->
+        Sys.file_exists (if path = "" then f else Filename.concat path f))
+
+let rocqbin =
+  (* avoid following symlinks if possible (Sys.executable_name followed symlinks) *)
+  if Filename.basename Sys.argv.(0) <> Sys.argv.(0) then
+    (* explicit directory (maybe relative to current dir) *)
+    canonical_path_name (Filename.dirname Sys.argv.(0))
+  else match find_in_PATH Sys.argv.(0) with
+    | Some p -> p
+    | None -> canonical_path_name (Filename.dirname Sys.executable_name)
 
 (** The following only makes sense when executables are running from
     source tree (e.g. during build or in local mode). *)
-let coqroot =
-  Filename.dirname coqbin
+let rocqroot =
+  let rec search = function
+    | [] ->
+      (* couldn't recognize the layout, guess the executable is 1 dir below the root
+         (eg "mybin/rocq")
+         XXX we should search only when we need the root
+         and produce an error if we can't find it *)
+      Filename.dirname rocqbin
+    | path :: rest ->
+      if Sys.file_exists (Filename.concat path "bin") then path
+      else search rest
+  in
+  (* we can be "bin/rocq" or "lib/rocq-runtime/rocqworker"
+     so rocqbin can be "bin/" or "lib/rocq-runtime/" *)
+  let dirname = Filename.dirname in
+  search [ dirname rocqbin; dirname @@ dirname rocqbin ]
+
+let relocate = function
+  | Coq_config.NotRelocatable p -> p
+  | Coq_config.Relocatable p -> Filename.concat rocqroot p
 
 (** [check_file_else ~dir ~file oth] checks if [file] exists in
     the installation directory [dir] given relatively to [coqroot],
     which maybe has been relocated.
     If the check fails, then [oth ()] is evaluated.
     Using file system equality seems well enough for this heuristic *)
 let check_file_else ~dir ~file oth =
-  let path = use_suffix coqroot dir in
+  let path = use_suffix rocqroot dir in
   if Sys.file_exists (Filename.concat path file) then path else oth ()
 
 let guess_coqlib () =
@@ -78,12 +103,10 @@ let guess_coqlib () =
     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 ())
+      (fun () -> relocate Coq_config.coqlib)
 
-(* Build layout uses coqlib = coqcorelib *)
+(* Build layout uses coqlib = coqcorelib
+   XXX we should be using -boot in build layout so is that dead code? *)
 let guess_coqcorelib lib =
   if Sys.file_exists (Path.relative lib plugins_dir)
   then lib
@@ -161,8 +184,8 @@ let ocamlfind () = match Util.getenv_opt "OCAMLFIND" with
 
 let docdir () =
   (* This assumes implicitly that the suffix is non-trivial *)
-  let path = use_suffix coqroot Coq_config.docdirsuffix in
-  if Sys.file_exists path then path else Coq_config.docdir
+  let path = use_suffix rocqroot Coq_config.docdirsuffix in
+  if Sys.file_exists path then path else relocate Coq_config.docdir
 
 (* Print the configuration information *)
 

boot/env.mli

@@ -117,3 +117,5 @@ val query_needs_env : Usage.query -> bool
 (** Internal, should be set automatically by passing cmdline args to
    init; note that this will set both [coqlib] and [corelib] for now. *)
 val set_coqlib : string -> unit
+
+val relocate : Coq_config.relocatable_path -> string

config/coq_config.mli

@@ -8,12 +8,16 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+type relocatable_path =
+  | NotRelocatable of string (* absolute path *)
+  | Relocatable of string (* relative to the inferred prefix *)
+
 (* The fields below are absolute paths *)
-val install_prefix : string   (* Install prefix passed by the user *)
-val coqlib : string     (* where the std library is installed *)
-val configdir : string  (* where configuration files are installed *)
-val datadir : string    (* where extra data files are installed *)
-val docdir : string     (* where the doc is installed *)
+val install_prefix : relocatable_path   (* Install prefix passed by the user *)
+val coqlib : relocatable_path     (* where the std library is installed *)
+val configdir : relocatable_path  (* where configuration files are installed *)
+val datadir : relocatable_path    (* where extra data files are installed *)
+val docdir : relocatable_path     (* where the doc is installed *)
 
 (* The fields below are paths relative to the installation prefix *)
 (* However, if an absolute path, it means discarding the actual prefix *)

config/dune

@@ -36,4 +36,4 @@
    %{project_root}/dev/header.c
    ; Needed to generate include lists for coq_makefile
    plugin_list)
- (action (chdir %{project_root} (run %{project_root}/tools/configure/configure.exe -quiet -prefix %{workspace_root}/../install/default))))
+ (action (chdir %{project_root} (run %{project_root}/tools/configure/configure.exe -quiet -relocatable))))

dev/ci/scripts/ci-coq_lsp.sh

@@ -9,6 +9,11 @@ git_download coq_lsp
 
 if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi
 
+if [ -n "${GITLAB_CI}" ]; then
+  export ROCQLIB="$PWD/_install_ci/lib/coq"
+  export ROCQRUNTIMELIB="$PWD/_install_ci/lib/rocq-runtime"
+fi
+
 ( cd "${CI_BUILD_DIR}/coq_lsp"
   dune build --root . --only-packages=coq-lsp @install
   # Tests

dev/ci/scripts/ci-vscoq.sh

@@ -9,6 +9,11 @@ git_download vscoq
 
 if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi
 
+if [ -n "${GITLAB_CI}" ]; then
+  export ROCQLIB="$PWD/_install_ci/lib/coq"
+  export ROCQRUNTIMELIB="$PWD/_install_ci/lib/rocq-runtime"
+fi
+
 ( cd "$CI_BUILD_DIR/vscoq/language-server"
   dune build --root . --only-packages=vscoq-language-server @install
   dune runtest --root .

dev/ci/user-overlays/19901-SkySkimmer-configure-clean.sh

@@ -0,0 +1 @@
+overlay coq_lsp https://github.com/SkySkimmer/coq-lsp configure-clean 19901

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

@@ -73,6 +73,85 @@ See :ref:`rocq_makefile` and :ref:`building_dune`.
       .. rocqdoc::
          -R <PATH> Mod1
 
+System configuration
+--------------------
+
+Running `rocq` (or the `coq` compatibility commands) will fail if it
+cannot find certain expected files (except for subcommands like
+`rocq wc` which do not need to find anything).
+
+The files are searched according to Rocq's build time configuration,
+the location of the `rocq` executable and the available command line
+arguments and environment variables.
+
+.. note::
+
+   If `configure` is not explicitly called, it is equivalent to
+   `configure -relocatable`.
+
+Let `$root` be the parent directory of the directory of the `rocq`
+executable (typically `rocq` is `$root/bin/rocq`, or
+`$root\bin\rocq.exe` on Windows).
+
+Let `$libdirconf` be the value passed to `configure -libdir`, or
+`coq/lib` if `libdir` was not used.
+
+Let `$libdir` be
+
+- if the `coqlib` command line argument was used, its value
+
+- otherwise, if the `ROCQLIB` environment variable is defined, its value
+
+- otherwise, if the deprecated `COQLIB` environment variable is defined, its value
+
+- otherwise, if `$libdirconf` is absolute, its value
+
+- otherwise, if `$root/$libdirconf/theories/Init/Prelude.vo` exists or
+  Rocq was configured with `-relocatable`, `$root/$libdirconf`
+
+- otherwise, if Rocq was configured with `-prefix $prefix`, `$prefix/$libdirconf`
+  (if the user gave a relative `$prefix`, it is turned into an absolute
+  path based on the working directory of the `configure` invocation)
+
+.. note::
+
+   Rocq must be configured with either `-prefix` or `-relocatable`.
+
+   If `$libdirconf` is relative, and `-prefix` was used, usually either
+   `$root/$libdirconf/theories/Init/Prelude.vo` does not exist so we
+   use `$prefix/$libdirconf`, or it is the same as `$prefix/$libdirconf`.
+   If `-relocatable` was used we only have `$root/$libdirconf`.
+
+.. exn:: The path for Rocq libraries is wrong.
+
+   Unless `-boot` was passed, Rocq fails with this error if
+   `$libdir/theories/Init/Prelude.vo` does not exist.
+
+Unless `-boot` was passed, Rocq acts as though `-R $libdir/theories
+Corelib -Q $libdir/user-contrib ""` was passed.
+
+Let `$runtimelib` be
+
+- if the `ROCQRUNTIMELIB` environment variable is defined, its value
+
+- otherwise, if the deprecated `COQCORELIB` environment variable is defined, its value
+
+- otherwise, `$libdir/../rocq-runtime`
+
+.. exn:: The path for Rocq plugins is wrong.
+
+   Unless `-boot` was passed, Rocq fails with this error if
+   `$runtimelib/plugins` does not exist.
+
+If `-boot` was not passed, Rocq will add `$runtimelib/..` to the
+OCamlfind search path (as though `-I $runtimelib/..` was passed).
+
+Then regardless of `-boot` Rocq will search for OCamlfind package `rocq-runtime`.
+
+.. exn:: Could not find package rocq-runtime.
+
+   Rocq fails with this error if OCamlfind package `rocq-runtime` could not be found.
+
 Customization at launch time
 ---------------------------------
 

lib/envars.ml

@@ -81,34 +81,23 @@ let expand_path_macros ~warn s =
 
 (** {2 Rocq paths} *)
 
-let coqbin =
-  CUnix.canonical_path_name (Filename.dirname Sys.executable_name)
-
-(** The following only makes sense when executables are running from
-    source tree (e.g. during build or in local mode). *)
-let coqroot =
-  Filename.dirname coqbin
-
-(** On win32, we add coqbin to the PATH at launch-time (this used to be
-    done in a .bat script). *)
-let _ =
-  if Coq_config.arch_is_win32 then
-    Unix.putenv "PATH" (coqbin ^ ";" ^ getenv_else "PATH" (fun () -> ""))
-
 (** Add a local installation suffix (unless the suffix is itself
     absolute in which case the prefix does not matter) *)
-let use_suffix prefix suffix =
-  if String.length suffix > 0 && suffix.[0] = '/' then suffix else prefix / suffix
+let use_suffix suffix =
+  if String.length suffix > 0 && suffix.[0] = '/' then suffix
+  else Boot.Env.relocate (Relocatable suffix)
 
-let datadir () =
+(* XXX do we actually need the local_suffix? *)
+let relocate local_suffix path =
   (* This assumes implicitly that the suffix is non-trivial *)
-  let path = use_suffix coqroot Coq_config.datadirsuffix in
-  if Sys.file_exists path then path else Coq_config.datadir
+  let local_path = use_suffix local_suffix in
+  if Sys.file_exists local_path
+  then local_path
+  else Boot.Env.relocate path
 
-let configdir () =
-  (* This assumes implicitly that the suffix is non-trivial *)
-  let path = use_suffix coqroot Coq_config.configdirsuffix in
-  if Sys.file_exists path then path else Coq_config.configdir
+let datadir () = relocate Coq_config.datadirsuffix Coq_config.datadir
+
+let configdir () = relocate Coq_config.configdirsuffix Coq_config.configdir
 
 let coqpath () =
   let make_search_path path =

lib/envars.mli

@@ -37,15 +37,6 @@ val datadir : unit -> string
 (** [configdir] is the path to the installed config directory. *)
 val configdir : unit -> string
 
-(** [coqbin] is the name of the current executable. *)
-val coqbin : string
-
-(** [coqroot] is the path to [coqbin].
-    The following value only makes sense when executables are running from
-    source tree (e.g. during build or in local mode).
-*)
-val coqroot : string
-
 (** [coqpath] is the standard path to coq.
     Notice that coqpath is stored in reverse order, since that is
     the order it gets added to the search path. *)