[coqdep] Be more deterministic w.r.t. the plugin loading mode

If the legacy mode is set, we don't even attempt to use findlib to
resolve anything, we also won't emit a META dependency, even if this
dependency is in scope.

This is morally the right thing to do, should reduce non-determinism,
and helps a bit to isolate the legacy code more.

This should help with problems such as
ocaml/dune#5833

tools/coqdep/lib/common.ml

@@ -131,13 +131,14 @@ let declare_ml_to_file file decl =
   let meta_files = !meta_files in
   match decl with
   | [[x]] when List.mem_assoc x legacy_mapping ->
-    Fl.findlib_resolve ~meta_files ~file ~package:"coq-core" ~legacy_name:(Some x) ~plugin_name:(List.assoc x legacy_mapping)
+    None, x                     (* This case only exists for 3rd party packages, should remove in 8.17 *)
   | [[x]] ->
     Error.findlib_name file x
   | [[legacy]; package :: plugin_name] ->
-    Fl.findlib_resolve ~meta_files ~file ~package ~legacy_name:(Some legacy) ~plugin_name
+    None, legacy
   | [package :: plugin_name] ->
-    Fl.findlib_resolve ~meta_files ~file ~package ~legacy_name:None ~plugin_name
+    let meta, cmxs = Fl.findlib_resolve ~meta_files ~file ~package ~plugin_name in
+    Some meta, cmxs
   | plist ->
     CErrors.user_err
       Pp.(str "Failed to resolve plugin " ++

tools/coqdep/lib/fl.ml

@@ -86,11 +86,10 @@ let rec find_plugin meta_file plugin_name path p { Fl_metascanner.pkg_defs ; pkg
     let path = path @ [find_plugin_field "directory" "." c.Fl_metascanner.pkg_defs] in
     find_plugin meta_file plugin_name path ps c
 
-let findlib_resolve ~meta_files ~file ~package ~legacy_name ~plugin_name =
-  match find_parsable_META meta_files package, legacy_name with
-  | None, None -> Error.no_meta file package
-  | None, Some p -> None, p
-  | Some (meta_file, meta), _ ->
+let findlib_resolve ~meta_files ~file ~package ~plugin_name =
+  match find_parsable_META meta_files package with
+  | None -> Error.no_meta file package
+  | Some (meta_file, meta) ->
     (* let meta = parse_META meta_file package in *)
     let path = [find_plugin_field "directory" "." meta.Fl_metascanner.pkg_defs] in
     let path, plug = find_plugin meta_file plugin_name path plugin_name meta in
@@ -101,4 +100,4 @@ let findlib_resolve ~meta_files ~file ~package ~legacy_name ~plugin_name =
       | Some res_file ->
         String.concat "/" path ^ "/" ^ Filename.chop_extension res_file
     in
-    Some meta_file, cmxs_file
+    meta_file, cmxs_file

tools/coqdep/lib/fl.mli

@@ -8,22 +8,20 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** [findlib_resolve meta_files file package legacy_name plugin_name]
-   tries to locate a [.cmxs] for a given [package.plugin_name]
+(** [findlib_resolve meta_files file package plugin_name] tries to
+   locate a [.cmxs] for a given [package.plugin_name]
 
     If a [META] file for [package] is found, it will try to use it to
-   resolve the path to the [.cmxs], and return both. If not, it will
-   return [None, legacy_name]. If [legacy_name] is absent, it errors.
+   resolve the path to the [.cmxs], and return both. If not, it
+   errors.
 
     The [META] file for [package] is search among the list of
    [meta_files] first, then using [Findlib.package_meta_file]. note
    that coqdep doesn't initialize findlib so that function performs
-   implicity initialization.
-*)
+   implicity initialization.  *)
 val findlib_resolve
   : meta_files:string list
   -> file:string
   -> package:string
-  -> legacy_name:string option
   -> plugin_name:string list
-  -> string option * string
+  -> string * string