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.

8 files changed, 66 insertions, 25 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/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:
 
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\