[plugins] Support for a findlib-based loader.

We introduce new syntax
```
Require ML Module pkg1 ... pkgn.
```
that uses findlib to locate and load a Coq plugin and its dependencies.

This makes feasible to actually develop Coq plugins that depend on
OCaml libraries not linked into the Coq main binaries without hitting
problems.

Fixes coq#5028, fixes coq#7698 .

This provides a workaround for coq#12607 , and helps with coq#9547 .

vernac/dune

@@ -3,6 +3,6 @@
  (synopsis "Coq's Vernacular Language")
  (public_name coq-core.vernac)
  (wrapped false)
- (libraries tactics parsing))
+ (libraries findlib.dynload tactics parsing))
 
 (coq.pp (modules g_proofs g_vernac))

vernac/g_vernac.mlg

@@ -897,7 +897,10 @@ GRAMMAR EXTEND Gram
         s = [ s = ne_string -> { s } | s = IDENT -> { s } ] ->
           { VernacLoad (verbosely, s) }
       | IDENT "Declare"; IDENT "ML"; IDENT "Module"; l = LIST1 ne_string ->
-          { VernacDeclareMLModule l }
+          { VernacDeclareMLModule { loader = CoqLoader ; modules = l } }
+
+      | IDENT "Require"; IDENT "ML"; IDENT "Module"; l = LIST1 ne_string ->
+          { VernacDeclareMLModule { loader = Findlib ; modules = l } }
 
       | IDENT "Locate"; l = locatable -> { VernacLocate l }
 

vernac/mltop.ml

@@ -377,3 +377,50 @@ let print_gc () =
     str "stack_size: " ++ int stat.Gc.stack_size
   in
   hv 0 msg
+
+(* TODO, what should we do here? *)
+type fl_module_object = {
+  mlocal : Vernacexpr.locality_flag;
+  mnames : (string * ml_module_digest) list
+}
+
+let cache_fl_objects (_,{mnames=mnames}) =
+  let iter (obj, _) = trigger_ml_object true true true obj in
+  List.iter iter mnames
+
+let load_fl_objects _ (_,{mnames=mnames}) =
+  let iter (obj, _) = trigger_ml_object true false true obj in
+  List.iter iter mnames
+
+let classify_fl_objects ({mlocal=mlocal} as o) =
+  if mlocal then Libobject.Dispose else Libobject.Substitute o
+
+let inFLModule : fl_module_object -> Libobject.obj =
+  let open Libobject in
+  declare_object
+    {(default_object "FL-MODULE") with
+      cache_function = cache_fl_objects;
+      load_function = load_fl_objects;
+      subst_function = (fun (_,o) -> o);
+      classify_function = classify_fl_objects }
+
+(* To get the location of a plugin we do
+   ocamlfind query -predicates native -format '%+(plugin)' coq.plugins.ltac
+
+In code this is:
+
+let pkg = "coq.plugins.ltac" in
+let d = Find.package_director pkg in
+let archs = Findlib.package_property ["native"] pkg "plugin" in
+let paths = Findlib.resolve_path ~base:d archs in
+...
+
+TODO: not clear if archs can return multiple objects so we'd need to
+   call `Fl_split.in_words`
+ *)
+let load_plugins ~local fl_names =
+  Fl_dynload.load_packages fl_names;
+  (* XXX: Fix with above info. *)
+  let l = List.map mod_of_name fl_names in
+  let l = List.map add_module_digest l in
+  Lib.add_anonymous_leaf ~cache_first:false (inFLModule {mlocal=local; mnames=l})

vernac/mltop.mli

@@ -62,10 +62,21 @@ val declare_cache_obj : (unit -> unit) -> string -> unit
 
 (** {5 Declaring modules} *)
 
+(** [declare_ml_modules mods] Load dynamically modules [mods] calling
+   low-level [Dynlink] API, cmxs/cma files are searched in the path
+   specified with add_ml_dir . [mods] are a string such that
+   [mod.cmxs] is the expected object file. Note this is a simple
+   wrapper over [Dynlink] thus no dependency or double-loading are, in
+   principle handled. *)
 val declare_ml_modules : Vernacexpr.locality_flag -> string list -> unit
 
+(** [load_plugins fl_name] load dynamically a plugin with findlib name
+   [fl_name] using [Fl_dynload]. Findlib will handle locating, and
+   loading the dependencies for the plugin, so the plugin should
+   install a META file and be in scope. *)
+val load_plugins : local:Vernacexpr.locality_flag -> string list -> unit
+
 (** {5 Utilities} *)
 
-val print_ml_path : unit -> Pp.t
-val print_ml_modules : unit -> Pp.t
-val print_gc : unit -> Pp.t
+val print_ml_path : unit -> Pp.t val print_ml_modules : unit -> Pp.t
+   val print_gc : unit -> Pp.t

vernac/ppvernac.ml

@@ -1077,9 +1077,13 @@ let pr_vernac_expr v =
       ++ keyword "ML Path"
       ++ qs s
     )
-  | VernacDeclareMLModule (l) ->
+  | VernacDeclareMLModule { loader; modules } ->
     return (
-      hov 2 (keyword "Declare ML Module" ++ spc() ++ prlist_with_sep sep qs l)
+      let require_type = function
+        | CoqLoader -> keyword "Declare ML Module"
+        | Findlib -> keyword "Require ML Module"
+      in
+      hov 2 (require_type loader ++ spc() ++ prlist_with_sep sep qs modules)
     )
   | VernacChdir s ->
     return (keyword "Cd" ++ pr_opt qs s)

vernac/vernacentries.ml

@@ -1364,9 +1364,13 @@ let vernac_remove_loadpath path =
 let vernac_add_ml_path path =
   Mltop.add_ml_dir (expand path)
 
-let vernac_declare_ml_module ~local l =
+let vernac_declare_ml_module ~local loader modules =
   let local = Option.default false local in
-  Mltop.declare_ml_modules local (List.map expand l)
+  match loader with
+  | CoqLoader ->
+    Mltop.declare_ml_modules local (List.map expand modules)
+  | Findlib ->
+    Mltop.load_plugins ~local modules
 
 let vernac_chdir = function
   | None -> Feedback.msg_notice (str (Sys.getcwd()))
@@ -2263,8 +2267,9 @@ let translate_vernac ?loc ~atts v = let open Vernacextend in match v with
     VtDefault(fun () ->
         unsupported_attributes atts;
         vernac_add_ml_path s)
-  | VernacDeclareMLModule l ->
-    VtDefault(fun () -> with_locality ~atts vernac_declare_ml_module l)
+  | VernacDeclareMLModule { loader; modules } ->
+    VtDefault(fun () ->
+        with_locality ~atts vernac_declare_ml_module loader modules)
   | VernacChdir s ->
     VtDefault(fun () -> unsupported_attributes atts; vernac_chdir s)
 

vernac/vernacexpr.ml

@@ -298,6 +298,8 @@ type reference_or_constr =
   | HintsReference of Libnames.qualid
   | HintsConstr of Constrexpr.constr_expr
 
+type ml_loader = CoqLoader | Findlib
+
 type hints_expr =
   | HintsResolve of (hint_info_expr * bool * reference_or_constr) list
   | HintsResolveIFF of bool * Libnames.qualid list * int option
@@ -394,7 +396,7 @@ type nonrec vernac_expr =
 
   | VernacRemoveLoadPath of string
   | VernacAddMLPath of string
-  | VernacDeclareMLModule of string list
+  | VernacDeclareMLModule of { loader : ml_loader; modules : string list }
   | VernacChdir of string option
 
   (* State management *)