Integrate build and documentation of Ltac2

Since Ltac2 cannot be put under the stdlib logical root (some file names
would clash), we move it to the `user-contrib` directory, to avoid adding
another hardcoded path in `coqinit.ml`, following a suggestion by @ejgallego.

Thanks to @Zimmi48 for the thorough documentation review and the
numerous suggestions.

3 files changed, 20 insertions, 7 deletions

diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml
index fa8b771a74..6ddc503542 100644
--- a/tools/coq_dune.ml
+++ b/tools/coq_dune.ml
@@ -214,7 +214,7 @@ let record_dune d ff =
   if Sys.file_exists sd && Sys.is_directory sd then
     let out = open_out (bpath [sd;"dune"]) in
     let fmt = formatter_of_out_channel out in
-    if List.nth d 0 = "plugins" then
+    if List.nth d 0 = "plugins" || List.nth d 0 = "user-contrib" then
       fprintf fmt "(include plugin_base.dune)@\n";
     out_install fmt d ff;
     List.iter (pp_dep d fmt) ff;
@@ -224,17 +224,20 @@ let record_dune d ff =
     eprintf "error in coq_dune, a directory disappeared: %s@\n%!" sd
 
 (* File Scanning *)
-let scan_mlg m d =
-  let dir = ["plugins"; d] in
+let scan_mlg ~root m d =
+  let dir = [root; d] in
   let m = DirMap.add dir [] m in
   let mlg = Sys.(List.filter (fun f -> Filename.(check_suffix f ".mlg"))
                    Array.(to_list @@ readdir (bpath dir))) in
-  List.fold_left (fun m f -> add_map_list ["plugins"; d] (MLG f) m) m mlg
+  List.fold_left (fun m f -> add_map_list [root; d] (MLG f) m) m mlg
 
-let scan_plugins m =
+let scan_dir ~root m =
   let is_plugin_directory dir = Sys.(is_directory dir && file_exists (bpath [dir;"plugin_base.dune"])) in
-  let dirs = Sys.(List.filter (fun f -> is_plugin_directory @@ bpath ["plugins";f]) Array.(to_list @@ readdir "plugins")) in
-  List.fold_left scan_mlg m dirs
+  let dirs = Sys.(List.filter (fun f -> is_plugin_directory @@ bpath [root;f]) Array.(to_list @@ readdir root)) in
+  List.fold_left (scan_mlg ~root) m dirs
+
+let scan_plugins m = scan_dir ~root:"plugins" m
+let scan_usercontrib m = scan_dir ~root:"user-contrib" m
 
 (* This will be removed when we drop support for Make *)
 let fix_cmo_cma file =
@@ -291,5 +294,6 @@ let exec_ifile f =
 let _ =
   exec_ifile (fun ic ->
       let map = scan_plugins DirMap.empty in
+      let map = scan_usercontrib map in
       let map = read_vfiles ic map in
       out_map map)
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 7114965a11..8823206252 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -529,6 +529,11 @@ let coqdep () =
     add_rec_dir_import add_known "plugins" ["Coq"];
     add_rec_dir_import (fun _ -> add_caml_known) "theories" ["Coq"];
     add_rec_dir_import (fun _ -> add_caml_known) "plugins" ["Coq"];
+    let user = "user-contrib" in
+    if Sys.file_exists user then begin
+      add_rec_dir_no_import add_known user [];
+      add_rec_dir_no_import (fun _ -> add_caml_known) user [];
+    end;
   end else begin
     (* option_boot is actually always false in this branch *)
     Envars.set_coqlib ~fail:(fun msg -> raise (CoqlibError msg));
diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml
index aa023e6986..a638906c11 100644
--- a/tools/coqdep_boot.ml
+++ b/tools/coqdep_boot.ml
@@ -17,6 +17,9 @@ open Coqdep_common
     options (see for instance [option_natdynlk] below).
 *)
 
+let split_period = Str.split (Str.regexp (Str.quote "."))
+let add_q_include path l = add_rec_dir_no_import add_known path (split_period l)
+
 let rec parse = function
   | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll
   | "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll
@@ -33,6 +36,7 @@ let rec parse = function
        add_caml_dir r;
        norec_dirs := StrSet.add r !norec_dirs;
        parse ll
+  | "-Q" :: r :: ln :: ll -> add_q_include r ln; parse ll
   | f :: ll -> treat_file None f; parse ll
   | [] -> ()