[coqdep] Don't treat stdlib specially in boot mode.

This means the build system should pass the correct includes and
library bindings to `coqdep`.

We still have some discrepancies we won't be able to solve until
`Loadpath` and `coqdep` are fused [which depends on the dune build.

2 files changed, 5 insertions, 27 deletions

diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 8a994b99c7..745cf950b5 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -94,7 +94,6 @@ let usage () =
 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 add_r_include path l = add_rec_dir_import add_known path (split_period l)
 
 let treat_coqproject f =
@@ -108,6 +107,7 @@ let treat_coqproject f =
   iter_sourced (fun f -> treat_file None f) (all_files project)
 
 let rec parse = function
+  (* TODO, deprecate option -c *)
   | "-c" :: ll -> option_c := true; parse ll
   | "-boot" :: ll -> option_boot := true; parse ll
   | "-sort" :: ll -> option_sort := true; parse ll
@@ -144,19 +144,8 @@ let coqdep () =
   (* Add current dir with empty logical path if not set by options above. *)
   (try ignore (Coqdep_common.find_dir_logpath (Sys.getcwd()))
    with Not_found -> add_norec_dir_import add_known "." []);
-  (* NOTE: These directories are searched from last to first *)
-  if !option_boot then begin
-    add_rec_dir_import add_known "theories" ["Coq"];
-    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 *)
+  (* We don't setup any loadpath if the -boot is passed *)
+  if not !option_boot then begin
     Envars.set_coqlib ~fail:(fun msg -> raise (CoqlibError msg));
     let coqlib = Envars.coqlib () in
     add_rec_dir_import add_coqlib_known (coqlib//"theories") ["Coq"];
diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml
index 257d4cc0fd..1cebb3638e 100644
--- a/tools/coqdep_boot.ml
+++ b/tools/coqdep_boot.ml
@@ -19,6 +19,7 @@ open Coqdep_common
 
 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 add_r_include path l = add_rec_dir_import add_known path (split_period l)
 
 let rec parse = function
   | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll
@@ -26,7 +27,6 @@ let rec parse = function
   | "-dyndep" :: "byte" :: ll -> option_dynlink := Byte; parse ll
   | "-dyndep" :: "both" :: ll -> option_dynlink := Both; parse ll
   | "-dyndep" :: "var" :: ll -> option_dynlink := Variable; parse ll
-  | "-c" :: ll -> option_c := true; parse ll
   | "-boot" :: ll -> parse ll (* We're already in boot mode by default *)
   | "-I" :: r :: ll ->
        (* To solve conflict (e.g. same filename in kernel and checker)
@@ -34,6 +34,7 @@ let rec parse = function
        add_caml_dir r;
        norec_dirs := StrSet.add r !norec_dirs;
        parse ll
+  | "-R" :: r :: ln :: ll -> add_r_include r ln; parse ll
   | "-Q" :: r :: ln :: ll -> add_q_include r ln; parse ll
   | f :: ll -> treat_file None f; parse ll
   | [] -> ()
@@ -42,16 +43,4 @@ let _ =
   let () = option_boot := true in
   if Array.length Sys.argv < 2 then exit 1;
   parse (List.tl (Array.to_list Sys.argv));
-  if !option_c then begin
-    add_rec_dir_import add_known "." [];
-    add_rec_dir_import (fun _ -> add_caml_known) "." ["Coq"];
-  end
-  else begin
-    add_rec_dir_import add_known "theories" ["Coq"];
-    add_rec_dir_import add_known "plugins" ["Coq"];
-    add_caml_dir "tactics";
-    add_rec_dir_import (fun _ -> add_caml_known) "theories" ["Coq"];
-    add_rec_dir_import (fun _ -> add_caml_known) "plugins" ["Coq"];
-  end;
-  if !option_c then mL_dependencies ();
   coq_dependencies ()