[build] Split stdlib to it's own opam package.

We introduce a new package structure for Coq:

- `coq-core`: Coq's OCaml tools code and plugins
- `coq-stdlib`: Coq's stdlib [.vo files]
- `coq`: meta-package that pulls `coq-{core,stdlib}`

This has several advantages, in particular it allows to install Coq
without the stdlib which is useful in several scenarios, it also open
the door towards a versioning of the stdlib at the package level.

The main user-visible change is that Coq's ML development files now
live in `$lib/coq-core`, for compatibility in the regular build we
install a symlink and support both setups for a while.

Note that plugin developers and even `coq_makefile` should actually
rely on `ocamlfind` to locate Coq's OCaml libs as to be more robust.

There is a transient state where we actually look for both
`$coqlib/plugins` and `$coqlib/../coq-core/plugins` as to support
the non-ocamlfind plus custom variables.

This will be much improved once #13617 is merged (which requires this
PR first), then, we will introduce a `coq.boot` library so finally
`coqdep`, `coqchk`, etc... can share the same path setup code.

IMHO the plan should work fine.

6 files changed, 54 insertions, 27 deletions

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 0ebb97d0bf..f2f2111fae 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -37,6 +37,7 @@ COQLIBS_NOML      := $(COQMF_COQLIBS_NOML)
 CMDLINE_COQLIBS   := $(COQMF_CMDLINE_COQLIBS)
 LOCAL             := $(COQMF_LOCAL)
 COQLIB            := $(COQMF_COQLIB)
+COQCORELIB        := $(COQMF_COQCORELIB)
 DOCDIR            := $(COQMF_DOCDIR)
 OCAMLFIND         := $(COQMF_OCAMLFIND)
 CAMLFLAGS         := $(COQMF_CAMLFLAGS)
@@ -97,9 +98,9 @@ COQMKFILE ?= "$(COQBIN)coq_makefile"
 OCAMLLIBDEP ?= "$(COQBIN)ocamllibdep"
 
 # Timing scripts
-COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file.py"
-COQMAKE_BOTH_TIME_FILES ?= "$(COQLIB)/tools/make-both-time-files.py"
-COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQLIB)/tools/make-both-single-timing-files.py"
+COQMAKE_ONE_TIME_FILE ?= "$(COQCORELIB)/tools/make-one-time-file.py"
+COQMAKE_BOTH_TIME_FILES ?= "$(COQCORELIB)/tools/make-both-time-files.py"
+COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQCORELIB)/tools/make-both-single-timing-files.py"
 BEFORE ?=
 AFTER ?=
 
@@ -220,7 +221,7 @@ COQDOCLIBS?=$(COQLIBS_NOML)
 COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1)
 COQMAKEFILE_VERSION:=@COQ_VERSION@
 
-COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)/$(d)")
+COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQCORELIB)/$(d)")
 
 CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS)
 # ocamldoc fails with unknown argument otherwise
@@ -822,6 +823,7 @@ printenv::
 	$(warning write extensions in @LOCAL_FILE@ or include @CONF_FILE@)
 	@echo 'LOCAL = $(LOCAL)'
 	@echo 'COQLIB = $(COQLIB)'
+	@echo 'COQCORELIB = $(COQCORELIB)'
 	@echo 'DOCDIR = $(DOCDIR)'
 	@echo 'OCAMLFIND = $(OCAMLFIND)'
 	@echo 'HASNATDYNLINK = $(HASNATDYNLINK)'
@@ -840,12 +842,12 @@ printenv::
 .merlin:
 	$(SHOW)'FILL .merlin'
 	$(HIDE)echo 'FLG $(COQMF_CAMLFLAGS)' > .merlin
-	$(HIDE)echo 'B $(COQLIB)' >> .merlin
-	$(HIDE)echo 'S $(COQLIB)' >> .merlin
+	$(HIDE)echo 'B $(COQCORELIB)' >> .merlin
+	$(HIDE)echo 'S $(COQCORELIB)' >> .merlin
 	$(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \
-		echo 'B $(COQLIB)$(d)' >> .merlin;)
+		echo 'B $(COQCORELIB)$(d)' >> .merlin;)
 	$(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \
-		echo 'S $(COQLIB)$(d)' >> .merlin;)
+		echo 'S $(COQCORELIB)$(d)' >> .merlin;)
 	$(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'B $(d)' >> .merlin;)
 	$(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'S $(d)' >> .merlin;)
 	$(HIDE)$(MAKE) merlin-hook -f "$(SELF)"
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 07550b67e3..cddb840693 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -125,8 +125,17 @@ let quote s = if String.contains s ' ' || CString.is_empty s then "'" ^ s ^ "'"
 let generate_makefile oc conf_file local_file dep_file args project =
   let coqlib = Envars.coqlib () in
   let makefile_template =
-    let template = Filename.concat "tools" "CoqMakefile.in" in
-    Filename.concat coqlib template in
+    CPath.choose_existing
+      [ CPath.make [ coqlib; "tools"; "CoqMakefile.in" ]
+      ; CPath.make [ coqlib; ".."; "coq-core"; "tools"; "CoqMakefile.in" ]
+      ]
+  in
+  let makefile_template = match makefile_template with
+    | None ->
+      Format.eprintf "Error: cannot find CoqMakefile.in";
+      exit 1
+    | Some v -> (v :> string)
+  in
   let s = read_whole_file makefile_template in
   let s = List.fold_left
     (* We use global_substitute to avoid running into backslash issues due to \1 etc. *)
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 2177da0c75..f1dbac889b 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -97,8 +97,16 @@ let coqdep () =
   if not !option_boot then begin
     Envars.set_coqlib ~fail:(fun msg -> raise (CoqlibError msg));
     let coqlib = Envars.coqlib () in
+    let coq_plugins_dir = CPath.choose_existing
+      [ CPath.make [ coqlib; "plugins" ]
+      ; CPath.make [ coqlib; ".."; "coq-core"; "plugins" ]
+      ] |> function
+    | None ->
+      CErrors.user_err (Pp.str "coqdep: cannot find plugins directory\n");
+    | Some f -> (f :> string)
+    in
     add_rec_dir_import add_coqlib_known (coqlib//"theories") ["Coq"];
-    add_rec_dir_import add_coqlib_known (coqlib//"plugins") ["Coq"];
+    add_rec_dir_import add_coqlib_known (coq_plugins_dir) ["Coq"];
     let user = coqlib//"user-contrib" in
     if Sys.file_exists user then add_rec_dir_no_import add_coqlib_known user [];
     List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s [])
diff --git a/tools/coqdoc/dune b/tools/coqdoc/dune
index e3c792f277..cc888a959f 100644
--- a/tools/coqdoc/dune
+++ b/tools/coqdoc/dune
@@ -1,6 +1,6 @@
 (install
  (section lib)
- (package coq)
+ (package coq-core)
  (files
   (coqdoc.css as tools/coqdoc/coqdoc.css)
   (coqdoc.sty as tools/coqdoc/coqdoc.sty)))
@@ -8,7 +8,7 @@
 (executable
  (name main)
  (public_name coqdoc)
- (package coq)
- (libraries str coq.config coq.clib))
+ (package coq-core)
+ (libraries str coq-core.config coq-core.clib))
 
 (ocamllex cpretty)
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index b8d5032373..c95d1ee7db 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -471,9 +471,17 @@ let index_module = function
   | Latex_file _ -> ()
 
 let copy_style_file file =
-  let src =
-    List.fold_left
-      Filename.concat !Cdglobals.coqlib_path ["tools";"coqdoc";file] in
+  (* We give preference to coqlib in case it is overriden *)
+  let src_dir = CPath.choose_existing
+      [ CPath.make [ !Cdglobals.coqlib_path; "tools"; "coqdoc" ]
+      ; CPath.make [ !Cdglobals.coqlib_path; ".."; "coq-core"; "tools"; "coqdoc" ]
+      ] |> function
+    | None ->
+      eprintf "coqdoc: cannot find coqdoc style files\n";
+      exit 1
+    | Some f -> f
+  in
+  let src = (CPath.relative src_dir file :> string) in
   let dst = coqdoc_out file in
   if Sys.file_exists src then copy src dst
   else eprintf "Warning: file %s does not exist\n" src
diff --git a/tools/dune b/tools/dune
index d591bb0c37..703342b15c 100644
--- a/tools/dune
+++ b/tools/dune
@@ -1,6 +1,6 @@
 (install
  (section lib)
- (package coq)
+ (package coq-core)
  (files
   (CoqMakefile.in as tools/CoqMakefile.in)
   (TimeFileMaker.py as tools/TimeFileMaker.py)
@@ -11,30 +11,30 @@
 (executable
  (name coq_makefile)
  (public_name coq_makefile)
- (package coq)
+ (package coq-core)
  (modules coq_makefile)
- (libraries coq.lib))
+ (libraries coq-core.lib))
 
 (executable
  (name coqworkmgr)
  (public_name coqworkmgr)
- (package coq)
+ (package coq-core)
  (modules coqworkmgr)
- (libraries coq.stm))
+ (libraries coq-core.stm))
 
 (executable
  (name coqdep)
  (public_name coqdep)
- (package coq)
+ (package coq-core)
  (modules coqdep_lexer coqdep_common coqdep)
- (libraries coq.lib))
+ (libraries coq-core.lib))
 
 ; Bare-bones mllib/mlpack parser
 (executable
  (name ocamllibdep)
  (public_name ocamllibdep)
  (modules ocamllibdep)
- (package coq)
+ (package coq-core)
  (libraries unix))
 
 (ocamllex coqdep_lexer ocamllibdep)
@@ -42,7 +42,7 @@
 (executable
  (name coqwc)
  (public_name coqwc)
- (package coq)
+ (package coq-core)
  (modules coqwc)
  (libraries))
 
@@ -51,6 +51,6 @@
 (executables
  (names coq_tex)
  (public_names coq-tex)
- (package coq)
+ (package coq-core)
  (modules coq_tex)
  (libraries str))