Merge PR #8991: coqide: use correct toplevel name in files

10 files changed, 98 insertions, 63 deletions

diff --git a/CHANGES.md b/CHANGES.md
index c830bc7a1c..e280cc2fb5 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,6 +1,18 @@
 Changes from 8.9 to 8.10
 ========================
 
+Coqide
+
+- CoqIDE now properly sets the module name for a given file based on
+  its path, see -topfile change entry for more details.
+
+Coqtop
+
+- new option -topfile filename, which will set the current module name
+  (à la -top) based on the filename passed, taking into account the
+  proper -R/-Q options. For example, given -R Foo foolib using
+  -topfile foolib/bar.v will set the module name to Foo.Bar.
+
 OCaml
 
 - Coq 8.10 requires OCaml >= 4.05.0, bumped from 4.02.3 See the
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 4190f43680..a26f7d1b94 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -89,20 +89,29 @@ let make_coqtop_args fname =
     | Ignore_args -> !sup_args
     | Append_args -> !sup_args
     | Subst_args -> [] in
-  if read_project#get = Ignore_args then "", base_args
-  else
-    match !custom_project_file, fname with
-    | Some (d,proj), _ -> d, coqtop_args_from_project proj @ base_args
-    | None, None -> "", base_args
-    | None, Some the_file ->
-       match
-         CoqProject_file.find_project_file
-           ~from:(Filename.dirname the_file)
-           ~projfile_name:project_file_name#get
-       with
-       | None -> "", base_args
-       | Some proj -> 
-           proj, coqtop_args_from_project (read_project_file proj) @ base_args
+  let proj, args =
+    if read_project#get = Ignore_args then "", base_args
+    else
+      match !custom_project_file, fname with
+      | Some (d,proj), _ -> d, coqtop_args_from_project proj @ base_args
+      | None, None -> "", base_args
+      | None, Some the_file ->
+        match
+          CoqProject_file.find_project_file
+            ~from:(Filename.dirname the_file)
+            ~projfile_name:project_file_name#get
+        with
+        | None -> "", base_args
+        | Some proj ->
+          proj, coqtop_args_from_project (read_project_file proj) @ base_args
+  in
+  let args = match fname with
+    | None -> args
+    | Some fname ->
+      if List.exists (String.equal "-top") args then args
+      else "-topfile"::fname::args
+  in
+  proj, args
 ;;
 
 (** Setting drag & drop on widgets *)
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 514b364af3..b474bd502a 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 =
@@ -2585,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 =
@@ -2609,20 +2632,28 @@ 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
-
-  | VoDoc ln ->
-    let ldir = Flags.verbosely Library.start_library ln in
-    VCS.set_ldir ldir;
-    set_compilation_hints ln
-
-  | 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
+    | Interactive ln ->
+      let dp = match ln with
+        | TopLogical dp -> dp
+        | TopPhysical f -> dirpath_of_file f
+      in
+      Safe_typing.allow_delayed_constants := true;
+      Declaremods.start_library dp
+
+    | 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 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. *)
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:
 
diff --git a/tools/coqc.ml b/tools/coqc.ml
index ad845470ec..ae841212a7 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -109,7 +109,7 @@ let parse_args () =
     | ("-outputstate"|"-inputstate"|"-is"|"-exclude-dir"|"-color"
       |"-load-vernac-source"|"-l"|"-load-vernac-object"
       |"-load-ml-source"|"-require"|"-load-ml-object"
-      |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"|"-top"
+      |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"|"-top"|"-topfile"
       |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs" |"-w"
       |"-o"|"-profile-ltac-cutoff"|"-mangle-names"|"-bytecode-compiler"|"-native-compiler"
       as o) :: rem ->
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 8c643a285e..7c28ef24d4 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -49,7 +49,7 @@ type coq_cmdopts = {
   batch_mode : bool;
   compilation_mode : compilation_mode;
 
-  toplevel_name : Names.DirPath.t;
+  toplevel_name : Stm.interactive_top;
 
   compile_list: (string * bool) list;  (* bool is verbosity  *)
   compilation_output_name : string option;
@@ -88,6 +88,8 @@ type coq_cmdopts = {
 
 }
 
+let default_toplevel = Names.(DirPath.make [Id.of_string "Top"])
+
 let init_args = {
 
   load_init   = true;
@@ -101,7 +103,7 @@ let init_args = {
   batch_mode = false;
   compilation_mode = BuildVo;
 
-  toplevel_name = Names.(DirPath.make [Id.of_string "Top"]);
+  toplevel_name = Stm.TopLogical default_toplevel;
 
   compile_list = [];
   compilation_output_name = None;
@@ -487,7 +489,10 @@ let parse_args arglist : coq_cmdopts * string list =
       let topname = Libnames.dirpath_of_string (next ()) in
       if Names.DirPath.is_empty topname then
         CErrors.user_err Pp.(str "Need a non empty toplevel module name");
-      { oval with toplevel_name = topname }
+      { oval with toplevel_name = Stm.TopLogical topname }
+
+    |"-topfile" ->
+      { oval with toplevel_name = Stm.TopPhysical (next()) }
 
     |"-main-channel" ->
       Spawned.main_channel := get_host_port opt (next()); oval
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index accb6c2beb..b709788dde 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -11,6 +11,8 @@
 type compilation_mode = BuildVo | BuildVio | Vio2Vo
 type color = [`ON | `AUTO | `OFF]
 
+val default_toplevel : Names.DirPath.t
+
 type coq_cmdopts = {
 
   load_init   : bool;
@@ -26,7 +28,7 @@ type coq_cmdopts = {
   batch_mode : bool;
   compilation_mode : compilation_mode;
 
-  toplevel_name : Names.DirPath.t;
+  toplevel_name : Stm.interactive_top;
 
   compile_list: (string * bool) list;  (* bool is verbosity  *)
   compilation_output_name : string option;
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index c2437836f3..c43538017c 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -32,6 +32,7 @@ let print_usage_channel co command =
 \n  -R dir coqdir          recursively map physical dir to logical coqdir\
 \n  -Q dir coqdir          map physical dir to logical coqdir\
 \n  -top coqdir            set the toplevel name to be coqdir instead of Top\
+\n  -topfile f             set the toplevel name as though compiling f\
 \n  -coqlib dir            set the coq standard library directory\
 \n  -exclude-dir f         exclude subdirectories named f for option -R\
 \n\