From e47ef6323e7ce4c00ae38a23ed5542059abbda6e Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 13 Nov 2018 22:51:29 +0100
Subject: coqide: use correct toplevel name in files

Fix #8989.

This adds an option -topfile taking a path so that inferring the right
dirpath is done by the toplevel after processing -Q/-R instead of the
client having to do it.
---
 stm/stm.ml  | 20 +++++++++++++++-----
 stm/stm.mli |  4 +++-
 2 files changed, 18 insertions(+), 6 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index 514b364af3..9a2beca0ce 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -308,11 +308,13 @@ end (* }}} *)
 (*************************** THE DOCUMENT *************************************)
 (******************************************************************************)
 
+type interactive_top = TopLogical of DirPath.t | TopPhysical of string
+
 (* The main document type associated to a VCS *)
 type stm_doc_type =
   | VoDoc       of string
   | VioDoc      of string
-  | Interactive of Names.DirPath.t
+  | Interactive of interactive_top
 
 (* Dummy until we land the functional interp patch + fixed start_library *)
 type doc = int
@@ -522,7 +524,7 @@ end = struct (* {{{ *)
   type vcs = (branch_type, transaction, vcs state_info, box) t
   let vcs : vcs ref = ref (empty Stateid.dummy)
 
-  let doc_type = ref (Interactive (Names.DirPath.make []))
+  let doc_type = ref (Interactive (TopLogical (Names.DirPath.make [])))
   let ldir = ref Names.DirPath.empty
 
   let init dt id =
@@ -2609,9 +2611,17 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } =
   List.iter Mltop.add_coq_path iload_path;
 
   begin match doc_type with
-  | Interactive ln ->
-    Safe_typing.allow_delayed_constants := true;
-    Declaremods.start_library ln
+    | 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)))
+      in
+      Safe_typing.allow_delayed_constants := true;
+      Declaremods.start_library dp
 
   | VoDoc ln ->
     let ldir = Flags.verbosely Library.start_library ln in
diff --git a/stm/stm.mli b/stm/stm.mli
index 1e5ceb7e23..95117f04f4 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -39,13 +39,15 @@ module AsyncOpts : sig
 
 end
 
+type interactive_top = TopLogical of DirPath.t | TopPhysical of string
+
 (** The STM document type [stm_doc_type] determines some properties
    such as what uncompleted proofs are allowed and what gets recorded
    to aux files. *)
 type stm_doc_type =
   | VoDoc       of string       (* file path *)
   | VioDoc      of string       (* file path *)
-  | Interactive of DirPath.t    (* module path *)
+  | Interactive of interactive_top    (* module path *)
 
 (** Coq initalization options:
 
-- 
cgit v1.2.3


From d4a751b55e52ba546c36c9427957d80524a14d43 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 14 Nov 2018 00:15:18 +0100
Subject: Move generating library dirpath to stm in compile mode.

---
 stm/stm.ml | 49 +++++++++++++++++++++++++++++++++++--------------
 1 file changed, 35 insertions(+), 14 deletions(-)

(limited to 'stm')

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. *)
-- 
cgit v1.2.3