Move generating library dirpath to stm in compile mode.

3 files changed, 35 insertions, 41 deletions

diff --git a/library/library.ml b/library/library.ml
index 0ff82d7cc4..9b9bd07c93 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -611,28 +611,6 @@ let import_module export modl =
 (************************************************************************)
 (*s Initializing the compilation of a library. *)
 
-let check_coq_overwriting p id =
-  let l = DirPath.repr p in
-  let is_empty = match l with [] -> true | _ -> false in
-  if not !Flags.boot && not is_empty && Id.equal (List.last l) coq_root then
-    user_err 
-      (str "Cannot build module " ++ DirPath.print p ++ str "." ++ Id.print id ++ str "." ++ spc () ++
-      str "it starts with prefix \"Coq\" which is reserved for the Coq library.")
-
-let start_library fo =
-  let ldir0 =
-    try
-      let lp = Loadpath.find_load_path (Filename.dirname fo) in
-      Loadpath.logical lp
-    with Not_found -> Libnames.default_root_prefix
-  in
-  let file = Filename.chop_extension (Filename.basename fo) in
-  let id = Id.of_string file in
-  check_coq_overwriting ldir0 id;
-  let ldir = add_dirpath_suffix ldir0 id in
-  Declaremods.start_library ldir;
-  ldir
-
 let load_library_todo f =
   let longf = Loadpath.locate_file (f^".v") in
   let f = longf^"io" in
diff --git a/library/library.mli b/library/library.mli
index d5815afc40..d298a371b5 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -38,11 +38,6 @@ type seg_proofs = Constr.constr Future.computation array
    an export otherwise just a simple import *)
 val import_module : bool -> qualid list -> unit
 
-(** Start the compilation of a file as a library. The first argument must be
-    output file, and the 
-    returned path is the associated absolute logical path of the library. *)
-val start_library : CUnix.physical_path -> DirPath.t
-
 (** End the compilation of a library and save it to a ".vo" file *)
 val save_library_to :
   ?todo:(((Future.UUID.t,'document) Stateid.request * bool) list * 'counters) ->
diff --git a/stm/stm.ml b/stm/stm.ml
index 9a2beca0ce..b474bd502a 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2587,6 +2587,27 @@ let init_core () =
   if !cur_opt.async_proofs_mode = APon then Control.enable_thread_delay := true;
   State.register_root_state ()
 
+let check_coq_overwriting p =
+  let l = DirPath.repr p in
+  let id, l = match l with id::l -> id,l | [] -> assert false in
+  let is_empty = match l with [] -> true | _ -> false in
+  if not !Flags.boot && not is_empty && Id.equal (CList.last l) Libnames.coq_root then
+    user_err
+      (str "Cannot build module " ++ DirPath.print p ++ str "." ++ spc () ++
+      str "it starts with prefix \"Coq\" which is reserved for the Coq library.")
+
+let dirpath_of_file f =
+  let ldir0 =
+    try
+      let lp = Loadpath.find_load_path (Filename.dirname f) in
+      Loadpath.logical lp
+    with Not_found -> Libnames.default_root_prefix
+  in
+  let file = Filename.chop_extension (Filename.basename f) in
+  let id = Id.of_string file in
+  let ldir = Libnames.add_dirpath_suffix ldir0 id in
+  ldir
+
 let new_doc { doc_type ; iload_path; require_libs; stm_options } =
 
   let load_objs libs =
@@ -2614,25 +2635,25 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } =
     | Interactive ln ->
       let dp = match ln with
         | TopLogical dp -> dp
-        | TopPhysical f ->
-          let base = try Loadpath.logical (Loadpath.find_load_path (Filename.dirname f))
-            with Not_found -> Libnames.default_root_prefix
-          in
-          Libnames.add_dirpath_suffix base (Id.of_string Filename.(chop_extension (basename f)))
+        | TopPhysical f -> dirpath_of_file f
       in
       Safe_typing.allow_delayed_constants := true;
       Declaremods.start_library dp
 
-  | VoDoc ln ->
-    let ldir = Flags.verbosely Library.start_library ln in
-    VCS.set_ldir ldir;
-    set_compilation_hints ln
+    | VoDoc f ->
+      let ldir = dirpath_of_file f in
+      check_coq_overwriting ldir;
+      let () = Flags.verbosely Declaremods.start_library ldir in
+      VCS.set_ldir ldir;
+      set_compilation_hints f
 
-  | VioDoc ln ->
-    Safe_typing.allow_delayed_constants := true;
-    let ldir = Flags.verbosely Library.start_library ln in
-    VCS.set_ldir ldir;
-    set_compilation_hints ln
+    | VioDoc f ->
+      Safe_typing.allow_delayed_constants := true;
+      let ldir = dirpath_of_file f in
+      check_coq_overwriting ldir;
+      let () = Flags.verbosely Declaremods.start_library ldir in
+      VCS.set_ldir ldir;
+      set_compilation_hints f
   end;
 
   (* Import initial libraries. *)