Skip to content

Commit

Permalink
Backport of coq#16658 for v8.16.
Browse files Browse the repository at this point in the history
[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

Co-authored-by: Emilio Jesús Gallego Arias <e@x80.org>
  • Loading branch information
rlepigre and ejgallego committed Oct 14, 2022
1 parent 9c4b592 commit 5f57359
Showing 1 changed file with 8 additions and 8 deletions.
16 changes: 8 additions & 8 deletions tools/coqdep/common.ml
Original file line number Diff line number Diff line change
Expand Up @@ -273,10 +273,9 @@ let find_META package =

let findlib_resolve f package legacy_name plugin =
let open Fl_metascanner in
match find_META package, legacy_name with
| None, Some p -> None, p
| None, None -> Error.no_meta f package
| Some (meta_file, meta), _ ->
match find_META package with
| None -> Error.no_meta f package
| Some (meta_file, meta) ->
let rec find_plugin path p { pkg_defs ; pkg_children } =
match p with
| [] -> path, pkg_defs
Expand All @@ -299,7 +298,7 @@ let findlib_resolve f package legacy_name plugin =
in
let path = [find_plugin_field "directory" (Some ".") meta.pkg_defs] in
let path, plug = find_plugin path plugin meta in
Some meta_file, String.concat "/" path ^ "/" ^
meta_file, String.concat "/" path ^ "/" ^
Filename.chop_extension @@ find_plugin_field "plugin" None plug

let legacy_mapping = Core_plugins_findlib_compat.legacy_to_findlib
Expand Down Expand Up @@ -343,13 +342,14 @@ let rec find_dependencies st basename =
| Declare sl ->
let public_to_private_name = function
| [[x]] when List.mem_assoc x legacy_mapping ->
findlib_resolve f "coq-core" (Some x) (List.assoc x legacy_mapping)
None, x
| [[x]] ->
Error.findlib_name f x
| [[legacy]; package :: plugin] ->
findlib_resolve f package (Some legacy) plugin
None, legacy
| [package :: plugin] ->
findlib_resolve f package None plugin
let meta, cmxs = findlib_resolve f package None plugin in
Some meta, cmxs
| plist ->
CErrors.user_err
Pp.(str "Failed to resolve plugin " ++
Expand Down

0 comments on commit 5f57359

Please sign in to comment.