Merge PR coq#19863: coqdep: add -I from -f _CoqProject to findlib…

… search path, remove `-m`

Reviewed-by: gares
Reviewed-by: ejgallego
Ack-by: silene
Co-authored-by: gares <[email protected]>

doc/changelog/09-cli-tools/19863-coqdep-nom.rst

@@ -0,0 +1,4 @@
+- **Removed:**
+  `coqdep` flag `-m` (it was used through `coq_makefile`)
+  (`#19863 <https://github.com/coq/coq/pull/19863>`_,
+  by Gaëtan Gilbert).

test-suite/misc/non-marshalable-state.sh

@@ -8,7 +8,6 @@ export PATH=$COQBIN:$PATH
 cd misc/non-marshalable-state/
 
 if which cygpath >/dev/null 2>&1; then OCAMLFINDSEP=\;; else OCAMLFINDSEP=:; fi
-export OCAMLPATH=$PWD$OCAMLFINDSEP$OCAMLPATH
 
 coq_makefile -f _CoqProject -o Makefile
 

test-suite/misc/non-marshalable-state/_CoqProject

@@ -1,4 +1,4 @@
-META.coq-test-suite
+src/META.coq-test-suite
 -Q theories Marshal
 -I src
 

test-suite/misc/non-marshalable-state/META.coq-test-suite → test-suite/misc/non-marshalable-state/src/META.coq-test-suite

@@ -1,5 +1,5 @@
 package "evil" (
-    directory = "src"
+    directory = "."
     version = "dev"
     description = "An evil test plugin"
     requires = "coq-core.plugins.ltac"
@@ -9,7 +9,7 @@ package "evil" (
     plugin(native) = "evil_plugin.cmxs"
 )
 package "good" (
-    directory = "src"
+    directory = "."
     version = "dev"
     description = "A good test plugin"
     requires = "coq-core.plugins.ltac"

test-suite/misc/quotation_token.sh

@@ -8,15 +8,15 @@ export PATH=$COQBIN:$PATH
 cd misc/quotation_token/
 
 if which cygpath >/dev/null 2>&1; then OCAMLFINDSEP=\;; else OCAMLFINDSEP=:; fi
-export OCAMLPATH=$PWD$OCAMLFINDSEP$OCAMLPATH
 
 coq_makefile -f _CoqProject -o Makefile
 
 make clean
 
 make src/quotation_plugin.cma
 
-TMP=`mktemp`
+TMP=output.txt
+rm -f $TMP
 
 if make > $TMP 2>&1; then
   echo "should fail"
@@ -25,10 +25,12 @@ if make > $TMP 2>&1; then
 fi
 
 if grep "File.*quotation.v., line 12, characters 6-30" $TMP; then
-  rm $TMP
   exit 0
+elif grep "File.*quotation.v" $TMP; then
+  echo "wrong loc"
+  exit 1
 else
-  echo "wong loc: `grep File.*quotation.v $TMP`"
-  rm $TMP
+  echo "wrong error:"
+  cat $TMP
   exit 1
 fi

test-suite/misc/quotation_token/.gitignore

@@ -1,2 +1,3 @@
 /Makefile*
 /src/quotation.ml
+/output.txt

test-suite/misc/quotation_token/META.coq-test-suite

@@ -1,7 +1,7 @@
 package "quotation" (
     directory = "src"
     version = "dev"
-    description = "An quotation test plugin"
+    description = "A quotation test plugin"
     requires = "coq-core.plugins.ltac"
     archive(byte) = "quotation_plugin.cma"
     archive(native) = "quotation_plugin.cmxa"

test-suite/misc/quotation_token/_CoqProject

@@ -1,5 +1,9 @@
 META.coq-test-suite
 -Q theories Quotation
+
+# we need -I . so coqdep can find the META
+# and -I src so ocamllibdep finds the contents
+-I .
 -I src
 
 src/quotation.mlg

tools/CoqMakefile.in

@@ -890,7 +890,7 @@ VDFILE_FLAGS:=$(if @PROJECT_FILE@,-f @PROJECT_FILE@,) $(CMDLINE_COQLIBS) $(CMDLI
 
 $(VDFILE): @PROJECT_FILE@ $(VFILES)
 	$(SHOW)'COQDEP VFILES'
-	$(HIDE)$(COQDEP) $(if $(strip $(METAFILE)),-m "$(METAFILE)") -vos -dyndep var $(VDFILE_FLAGS) $(redir_if_ok)
+	$(HIDE)$(COQDEP) -vos -dyndep var $(VDFILE_FLAGS) $(redir_if_ok)
 
 # Misc ########################################################################
 

tools/coqdep/lib/args.ml

@@ -13,11 +13,9 @@ type t =
   ; sort : bool
   ; vos : bool
   ; noglob : bool
-  ; coqproject : string option
   ; ml_path : string list
   ; vo_path : (bool * string * string) list
   ; dyndep : string
-  ; meta_files : string list
   ; files : string list
   }
 
@@ -26,11 +24,9 @@ let make () =
   ; sort = false
   ; vos = false
   ; noglob = false
-  ; coqproject = None
   ; ml_path = []
   ; vo_path = []
   ; dyndep = "both"
-  ; meta_files = []
   ; files = []
   }
 
@@ -55,10 +51,36 @@ let usage () =
   eprintf "  -exclude-dir dir : skip subdirectories named 'dir' during -R/-Q search\n";
   eprintf "  -coqlib dir : set the coq standard library directory\n";
   eprintf "  -dyndep (opt|byte|both|no|var) : set how dependencies over ML modules are printed\n";
-  eprintf "  -m META : resolve plugins names using the META file\n";
   eprintf "  -w (w1,..,wn) : configure display of warnings\n";
   exit 1
 
+let warn_project_file =
+  let category = CWarnings.CoreCategories.filesystem in
+  CWarnings.create ~name:"project-file" ~category Pp.str
+
+let add_ml_path st f = { st with ml_path = f :: st.ml_path }
+
+let add_vo_path st (isr,path,logic) =
+  let logic = if String.equal logic "Coq" then "Stdlib" else logic in
+  { st with vo_path = (isr,path,logic) :: st.vo_path }
+
+let add_file st f = { st with files = f :: st.files }
+
+let add_from_coqproject st f =
+  let open CoqProject_file in
+  let fold_sourced f acc l = List.fold_left (fun acc {thing} -> f acc thing) acc l in
+  let project =
+    try read_project_file ~warning_fn:warn_project_file f
+    with
+    | Parsing_error msg -> Error.cannot_parse_project_file f msg
+    | UnableToOpenProjectFile msg -> Error.cannot_open_project_file msg
+  in
+  let st = fold_sourced (fun st { path } -> add_ml_path st path) st project.ml_includes in
+  let st = fold_sourced (fun st ({path}, l) -> add_vo_path st (false,path,l)) st project.q_includes in
+  let st = fold_sourced (fun st ({path}, l) -> add_vo_path st (true,path,l)) st project.r_includes in
+  let st = fold_sourced add_file st (all_files project) in
+  st
+
 let parse st args =
   let rec parse st =
     function
@@ -67,22 +89,19 @@ let parse st args =
     | "-vos" :: ll -> parse { st with vos = true } ll
     | ("-noglob" | "-no-glob") :: ll -> parse { st with noglob = true } ll
     | "-noinit" :: ll -> (* do nothing *) parse st ll
-    | "-f" :: f :: ll -> parse { st with coqproject = Some f } ll
-    | "-I" :: r :: ll -> parse { st with ml_path = r :: st.ml_path } ll
+    | "-f" :: f :: ll -> parse (add_from_coqproject st f) ll
+    | "-I" :: r :: ll -> parse (add_ml_path st r) ll
     | "-I" :: [] -> usage ()
     | "-R" :: r :: ln :: ll ->
-       let ln = if String.equal ln "Coq" then "Stdlib" else ln in
-       parse { st with vo_path = (true, r, ln) :: st.vo_path } ll
+       parse (add_vo_path st (true, r, ln)) ll
     | "-Q" :: r :: ln :: ll ->
-       let ln = if String.equal ln "Coq" then "Stdlib" else ln in
-       parse { st with vo_path = (false, r, ln) :: st.vo_path } ll
-    | "-R" :: ([] | [_]) -> usage ()
+       parse (add_vo_path st (false, r, ln)) ll
+    | ("-Q"|"-R") :: ([] | [_]) -> usage ()
     | "-exclude-dir" :: r :: ll -> System.exclude_directory r; parse st ll
     | "-exclude-dir" :: [] -> usage ()
     | "-coqlib" :: r :: ll -> Boot.Env.set_coqlib r; parse st ll
     | "-coqlib" :: [] -> usage ()
     | "-dyndep" :: dyndep :: ll -> parse { st with dyndep } ll
-    | "-m" :: m :: ll -> parse { st with meta_files = st.meta_files @ [m]} ll
     | "-w" :: w :: ll ->
       let w = if w = "none" then w else CWarnings.get_flags() ^ "," ^ w in
       CWarnings.set_flags w;
@@ -91,7 +110,7 @@ let parse st args =
     | opt :: ll when String.length opt > 0 && opt.[0] = '-' ->
       warn_unknown_option opt;
       parse st ll
-    | f :: ll -> parse { st with files = f :: st.files } ll
+    | f :: ll -> parse (add_file st f) ll
     | [] -> st
   in
   let st = parse st args in

tools/coqdep/lib/args.mli

@@ -13,11 +13,9 @@ type t =
   ; sort : bool
   ; vos : bool
   ; noglob : bool
-  ; coqproject : string option
   ; ml_path : string list
   ; vo_path : (bool * string * string) list
   ; dyndep : string
-  ; meta_files : string list
   ; files : string list
   }
 

tools/coqdep/lib/common.ml

@@ -119,20 +119,17 @@ let warn_legacy_loading =
                argument ignored; please remove \"" ++
           str name ++ str ":\" from your Declare ML"))
 
-let meta_files = ref []
-
 (* Transform "Declare ML %DECL" to a pair of (meta, cmxs). Something
    very similar is in ML top *)
 let declare_ml_to_file file (decl : string) =
   let legacy_decl = String.split_on_char ':' decl in
   let legacy_decl = List.map (String.split_on_char '.') legacy_decl in
-  let meta_files = !meta_files in
   match legacy_decl with
   | [package :: plugin_name] ->
-    Fl.findlib_resolve ~meta_files ~file ~package ~plugin_name
+    Fl.findlib_resolve ~file ~package ~plugin_name
   | [[cmxs]; (package :: plugin_name)] ->
     warn_legacy_loading cmxs;
-    Fl.findlib_resolve ~meta_files ~file ~package ~plugin_name
+    Fl.findlib_resolve ~file ~package ~plugin_name
   | bad_pkg ->
     CErrors.user_err Pp.(str "Failed to resolve plugin: " ++ str decl)
 
@@ -283,9 +280,6 @@ let rec treat_file old_dirname old_name =
 let treat_file_command_line old_name =
   treat_file None old_name
 
-let treat_file_coq_project where old_name =
-  treat_file None old_name
-
 (* "[sort]" outputs `.v` files required by others *)
 let sort st =
   let seen = Hashtbl.create 97 in
@@ -314,32 +308,13 @@ let sort st =
   in
   List.iter (fun (name, _) -> loop name) !vAccu
 
-let warn_project_file =
-  let category = CWarnings.CoreCategories.filesystem in
-  CWarnings.create ~name:"project-file" ~category Pp.str
-
-let treat_coqproject st f =
-  let open CoqProject_file in
-  let iter_sourced f = List.iter (fun {thing} -> f thing) in
-  let project =
-    try read_project_file ~warning_fn:warn_project_file f
-    with
-    | Parsing_error msg -> Error.cannot_parse_project_file f msg
-    | UnableToOpenProjectFile msg -> Error.cannot_open_project_file msg
-  in
-  (* EJGA: This should add to findlib search path *)
-  (* iter_sourced (fun { path } -> Loadpath.add_caml_dir st path) project.ml_includes; *)
-  iter_sourced (fun ({ path }, l) -> Loadpath.add_q_include st path l) project.q_includes;
-  iter_sourced (fun ({ path }, l) -> Loadpath.add_r_include st path l) project.r_includes;
-  iter_sourced (fun f' -> treat_file_coq_project f f') (all_files project)
-
 let add_include st (rc, r, ln) =
   if rc then
     Loadpath.add_r_include st r ln
   else
     Loadpath.add_q_include st r ln
 
-let add_findlib_dir dirs =
+let findlib_init dirs =
   let env_ocamlpath =
     try [Sys.getenv "OCAMLPATH"]
     with Not_found -> []
@@ -356,10 +331,8 @@ let init ~make_separator_hack args =
   let st = Loadpath.State.make ~boot:args.Args.boot in
   Makefile.set_write_vos args.Args.vos;
   Makefile.set_noglob args.Args.noglob;
-  Option.iter (treat_coqproject st) args.Args.coqproject;
   (* Add to the findlib search path, common with sysinit/coqinit *)
-  add_findlib_dir args.Args.ml_path;
+  findlib_init args.Args.ml_path;
   List.iter (add_include st) args.Args.vo_path;
   Makefile.set_dyndep args.Args.dyndep;
-  meta_files := args.Args.meta_files;
   st

tools/coqdep/lib/fl.ml

@@ -53,17 +53,11 @@ let parse_META meta_file package =
      it without bumping our version requirements. TODO pass the message on once we bump. *)
   | _ -> Error.cannot_parse_meta_file package ""
 
-let rec find_parsable_META meta_files package =
-  match meta_files with
-  | [] ->
-    (try
-       let meta_file = Findlib.package_meta_file package in
-       Option.map (fun meta -> meta_file, meta) (parse_META meta_file package)
-     with Fl_package_base.No_such_package _ -> None)
-  | meta_file :: ms ->
-    if String.equal (Filename.extension meta_file) ("." ^ package)
-    then Option.map (fun meta -> meta_file, meta) (parse_META meta_file package)
-    else find_parsable_META ms package
+let find_parsable_META package =
+  (try
+     let meta_file = Findlib.package_meta_file package in
+     Option.map (fun meta -> meta_file, meta) (parse_META meta_file package)
+   with Fl_package_base.No_such_package _ -> None)
 
 let rec find_plugin_field_opt fld = function
   | [] ->
@@ -88,9 +82,9 @@ 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 ~plugin_name =
+let findlib_resolve ~file ~package ~plugin_name =
   let (meta_file, meta) =
-    match find_parsable_META meta_files package with
+    match find_parsable_META package with
     | None   -> Error.no_meta file package
     | Some v -> v
   in

tools/coqdep/lib/fl.mli

@@ -8,20 +8,14 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** [findlib_resolve ~meta_files ~file ~package ~plugin_name] tries to locate
+(** [findlib_resolve ~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 a relative path to both. If not, it
-    errors.
-
-    The [META] file for [package] is first searched in the [meta_files] list,
-    and if it is not found then [Findlib.package_meta_file] is used. Note that
-    coqdep does not initialize findlib, so that function performs implicity
-    initialization. *)
+    errors. *)
 val findlib_resolve
-  : meta_files:string list
-  -> file:string
+  :  file:string
   -> package:string
   -> plugin_name:string list
   -> string * string