[rfc] [mltop] Removal of dynamic loading of object and `.ml` files

This seems seldom used and I think in general instrumentation this way
is pretty limited (usually better to use the build system to tweak)

It thus seems worth removing as to simplify `Mltop` a bit, but of
course comments are welcome.

8 files changed, 6 insertions, 42 deletions

diff --git a/doc/changelog/07-commands-and-options/11409-mltop+deprecate_use.rst b/doc/changelog/07-commands-and-options/11409-mltop+deprecate_use.rst
new file mode 100644
index 0000000000..db433ad64c
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/11409-mltop+deprecate_use.rst
@@ -0,0 +1,5 @@
+- **Removed:**
+  The `-load-ml-source` and `-load-ml-object` command line options
+  have been removed; their use was very limited, you can achieve the same adding
+  additional object files in the linking step or using a plugin.
+  (`#11409 <https://github.com/coq/coq/pull/11409>`_, by Emilio Jesus Gallego Arias).
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index ba43128bdc..98d222e317 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -157,8 +157,6 @@ and ``coqtop``, unless stated otherwise:
   loading the default resource file from the standard configuration
   directories.
 :-q: Do not to load the default resource file.
-:-load-ml-source *file*: Load the OCaml source file *file*.
-:-load-ml-object *file*: Load the OCaml object file *file*.
 :-l *file*, -load-vernac-source *file*: Load and execute the |Coq|
   script from *file.v*.
 :-lv *file*, -load-vernac-source-verbose *file*: Load and execute the
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 909804d0c9..fd689602df 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -138,7 +138,7 @@ module Make(T : Task) () = struct
           set_slave_opt tl
         (* We need to pass some options with one argument *)
         | ( "-I" | "-include" | "-top" | "-topfile" | "-coqlib" | "-exclude-dir" | "-compat"
-          | "-load-ml-object" | "-load-ml-source" | "-require" | "-w" | "-color" | "-init-file"
+          | "-require" | "-w" | "-color" | "-init-file"
           | "-profile-ltac-cutoff" | "-main-channel" | "-control-channel" | "-mangle-names" | "-set" | "-unset"
           | "-diffs" | "-mangle-name" | "-dump-glob" | "-bytecode-compiler" | "-native-compiler" as x) :: a :: tl ->
           x :: a :: set_slave_opt tl
diff --git a/topbin/coqtop_byte_bin.ml b/topbin/coqtop_byte_bin.ml
index 85d8a48eda..604c6e251a 100644
--- a/topbin/coqtop_byte_bin.ml
+++ b/topbin/coqtop_byte_bin.ml
@@ -31,7 +31,6 @@ let drop_setup () =
            { load_obj = (fun f -> if not (Topdirs.load_file ppf f)
                           then CErrors.user_err Pp.(str ("Could not load plugin "^f))
                         );
-             use_file = Topdirs.dir_use ppf;
              add_dir  = Topdirs.dir_directory;
              ml_loop  = (fun () -> Toploop.loop ppf);
            })
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 52e2562ae8..74d9c113d6 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -198,14 +198,6 @@ let set_query opts q =
   | Queries queries -> Queries (queries@[q])
   }
 
-let warn_depr_load_ml_object =
-  CWarnings.create ~name:"deprecated-mlobject" ~category:"deprecated"
-         (fun () -> Pp.strbrk "The -load-ml-object option is deprecated, see the changelog for more details.")
-
-let warn_depr_ml_load_source =
-  CWarnings.create ~name:"deprecated-mlsource" ~category:"deprecated"
-         (fun () -> Pp.strbrk "The -load-ml-source option is deprecated, see the changelog for more details.")
-
 let warn_deprecated_inputstate =
   CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated"
          (fun () -> Pp.strbrk "The inputstate option is deprecated and discouraged.")
@@ -403,14 +395,6 @@ let parse_args ~help ~init arglist : t * string list =
     |"-inputstate"|"-is" ->
       set_inputstate oval (next ())
 
-    |"-load-ml-object" ->
-      warn_depr_load_ml_object ();
-      Mltop.dir_ml_load (next ()); oval
-
-    |"-load-ml-source" ->
-      warn_depr_ml_load_source ();
-      Mltop.dir_ml_use (next ()); oval
-
     |"-load-vernac-object" ->
       add_vo_require oval (next ()) None None
 
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index b17ca71f4c..051638d53c 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -36,8 +36,6 @@ let print_usage_common co command =
 \n  -nois                  (idem)\
 \n  -compat X.Y            provides compatibility support for Coq version X.Y\
 \n\
-\n  -load-ml-object f      load ML object file f\
-\n  -load-ml-source f      load ML file f\
 \n  -load-vernac-source f  load Coq file f.v (Load \"f\".)\
 \n  -l f                   (idem)\
 \n  -load-vernac-source-verbose f  load Coq file f.v (Load Verbose \"f\".)\
diff --git a/vernac/mltop.ml b/vernac/mltop.ml
index 6621c1e6b1..2bac35b08f 100644
--- a/vernac/mltop.ml
+++ b/vernac/mltop.ml
@@ -56,7 +56,6 @@ let keep_copy_mlpath path =
 (* If there is a toplevel under Coq *)
 type toplevel = {
   load_obj : string -> unit;
-  use_file : string -> unit;
   add_dir  : string -> unit;
   ml_loop  : unit -> unit }
 
@@ -123,17 +122,6 @@ let dir_ml_load s =
         let _,gname = find_file_in_path ~warn !coq_mlpath_copy s in
         ml_load gname
 
-(* Dynamic interpretation of .ml *)
-let dir_ml_use s =
-  match !load with
-    | WithTop t -> t.use_file s
-    | _ ->
-       let moreinfo =
-         if Sys.(backend_type = Native) then " Loading ML code works only in bytecode."
-         else ""
-       in
-      user_err ~hdr:"Mltop.dir_ml_use" (str "Could not load ML code." ++ str moreinfo)
-
 (* Adds a path to the ML paths *)
 let add_ml_dir s =
   match !load with
@@ -258,7 +246,6 @@ let load_ml_object mname ?path fname=
   init_ml_object mname;
   path
 
-let dir_ml_load m = ignore(dir_ml_load m)
 let add_known_module m = add_known_module m None
 
 (* Summary of declared ML Modules *)
diff --git a/vernac/mltop.mli b/vernac/mltop.mli
index 56a28b64b0..271772d7ba 100644
--- a/vernac/mltop.mli
+++ b/vernac/mltop.mli
@@ -14,7 +14,6 @@
    record. *)
 type toplevel = {
   load_obj : string -> unit;
-  use_file : string -> unit;
   add_dir  : string -> unit;
   ml_loop  : unit -> unit }
 
@@ -38,12 +37,6 @@ val add_ml_dir : recursive:bool -> string -> unit
 (** Tests if we can load ML files *)
 val has_dynlink : bool
 
-(** Dynamic loading of .cmo *)
-val dir_ml_load : string -> unit
-
-(** Dynamic interpretation of .ml *)
-val dir_ml_use : string -> unit
-
 (** List of modules linked to the toplevel *)
 val add_known_module : string -> unit
 val module_is_known : string -> bool