-package delay resolving until -I have been processed

lib/coqProject_file.ml

@@ -349,13 +349,6 @@ let process_cmd_line ~warning_fn orig_dir parse_extra proj args =
       aux proj r
   in
   let proj = aux proj args in
-  let proj =
-    let packages_incs =
-      let get Rocq_package.{dir; logpath} = sourced (mk_path dir, logpath) in
-      List.map get (Rocq_package.resolve proj.packages)
-    in
-    {proj with q_includes = proj.q_includes @ packages_incs}
-  in
   (* Short-circuit -native-compiler options passed via -args *)
   let rec filter_extra proj = function
   | [] -> { proj with extra_args = [] }

sysinit/coqargs.ml

@@ -172,16 +172,6 @@ let add_vo_include opts unix_path rocq_path implicit =
 let add_package opts p =
   { opts with pre = { opts.pre with packages = p :: opts.pre.packages }}
 
-let resolve_packages args =
-  let packages = Rocq_package.resolve args.pre.packages in
-  let add p vo_includes =
-    let unix_path = p.Rocq_package.dir in
-    let rocq_path = p.Rocq_package.logpath in
-    { unix_path; rocq_path; implicit = false } :: vo_includes
-  in
-  let vo_includes = List.fold_right add packages args.pre.vo_includes in
-  { args with pre = { args.pre with vo_includes } }
-
 let add_vo_require opts d ?(allow_failure=false) p export =
   { opts with pre = { opts.pre with injections = RequireInjection {lib=d; prefix=p; export; allow_failure} :: opts.pre.injections }}
 
@@ -273,7 +263,7 @@ let parse_args ~init arglist : t * string list =
   let extras = ref [] in
   let rec parse oval = match !args with
   | [] ->
-    (resolve_packages oval, List.rev !extras)
+    (oval, List.rev !extras)
   | opt :: rem ->
     args := rem;
     let next () = match !args with

sysinit/coqinit.ml

@@ -97,6 +97,16 @@ let to_vo_path (x:Coqargs.vo_path) : Loadpath.vo_path = {
   installed = false;
   }
 
+(* NB implicit means -R vs -Q,
+   installed means explicitly added path (for warning about ambiguous requires) *)
+let package_vo_path (x:Rocq_package.t) : Loadpath.vo_path = {
+  implicit = false;
+  unix_path = x.dir;
+  coq_path = Libnames.dirpath_of_string x.logpath;
+  recursive = true;
+  installed = false;
+}
+
 let boot_env usage opts =
   let open Coqargs in
   let with_err = function
@@ -172,6 +182,8 @@ let init_document opts =
   (* this isn't in init_load_paths because processes (typically
      vscoqtop) are allowed to have states with differing vo paths (but
      not with differing -boot or ml paths) *)
+  let packages = Rocq_package.resolve opts.pre.packages in
+  List.iter (fun p -> Loadpath.add_vo_path (package_vo_path p)) packages;
   List.iter (fun x -> Loadpath.add_vo_path @@ to_vo_path x) opts.pre.vo_includes;
 
   (* Kernel configuration *)

test-suite/coq-makefile/package-ocamlpath/Foo.v

@@ -0,0 +1 @@
+From MyPack Require X.

test-suite/coq-makefile/package-ocamlpath/_CoqProject

@@ -0,0 +1,3 @@
+-I mylib
+-package mypackage
+Foo.v

test-suite/coq-makefile/package-ocamlpath/mylib/mypackage/META

@@ -0,0 +1 @@
+rocqpath = "MyPack"

test-suite/coq-makefile/package-ocamlpath/run.sh

@@ -0,0 +1,21 @@
+#!/usr/bin/env bash
+
+set -ex
+
+. ../template/path-init.sh
+
+rm -rf _test
+mkdir _test
+find . -maxdepth 1 -not -name . -not -name _test -exec cp -r '{}' -t _test ';'
+cd _test
+
+touch X.v
+rocq c -Q . MyPack X.v
+mkdir -p mylib/mypackage/rocq.d/
+cp X.vo mylib/mypackage/rocq.d/
+
+rocq makefile -f _CoqProject -o Makefile
+
+make
+
+test -e Foo.vo

tools/rocqmakefile.ml

@@ -324,24 +324,10 @@ let generate_meta_file p =
     Printf.eprintf "Error: %s\n" e;
     exit 1
 
-let remove_package_includes p =
-  let packages =
-    List.map (fun (Rocq_package.{ dir; logpath; _ }) ->
-      CUnix.canonical_path_name dir, logpath)
-      (Rocq_package.resolve p.packages)
-  in
-  let is_package_include { thing = ({ canonical_path; _ }, logic); _ } =
-    List.exists (fun (dir, logpath) ->
-      String.equal canonical_path dir && String.equal logic logpath) packages
-  in
-  { p with q_includes = List.filter (fun inc -> not (is_package_include inc)) p.q_includes }
-
 let setup_rocq_package project = match project.rocq_package with
-  | None -> project
+  | None -> ()
   | Some _ ->
-      let project = remove_package_includes project in
-      ignore (single_package_rocqpath project);
-      project
+    ignore (single_package_rocqpath project)
 
 let section oc s =
   let pad = String.make (76 - String.length s) ' ' in
@@ -375,8 +361,7 @@ let generate_conf_includes oc { ml_includes; r_includes; q_includes; packages; r
     (S.concat " " (map_cmdline (fun { path } -> dash1 "I" path) ml_includes))
     (S.concat " " (map_cmdline (fun ({ path },l) -> dash2 "Q" path l) q_includes))
     (S.concat " " (map_cmdline (fun ({ path },l) -> dash2 "R" path l) r_includes));
-  fprintf oc "COQMF_PACKAGES = %s\n"
-    (match rocq_package with None -> "" | Some _ -> S.concat " " packages);
+  fprintf oc "COQMF_PACKAGES = %s\n" (S.concat " " packages);
 ;;
 
 let windrive s =
@@ -617,7 +602,7 @@ let normal_mode ~coqlib project prog args =
 
   let project = ensure_root_dir project in
 
-  let project = setup_rocq_package project in
+  setup_rocq_package project;
 
   check_overlapping_include project;
 

topbin/rocqnative.ml

@@ -4,6 +4,14 @@ open Util
 open Names
 open Pp
 
+type opts = {
+  boot : bool;
+  coqlib : string option;
+  vo_path : (string * DirPath.t) list;
+  ml_path : string list;
+  packages : string list;
+}
+
 module Loadpath :
 sig
   val add_load_path : string * DirPath.t -> unit
@@ -245,7 +253,7 @@ let init_load_path_std env ~default_ml () =
   (* then directories in ROCQPATH *)
   List.iter (fun s -> add_rec_path ~unix_path:s ~rocq_root:Loadpath.default_root_prefix) (rocqpath())
 
-let init_load_path ~boot ~coqlib ~vo_path ~ml_path =
+let init_load_path { boot; coqlib; vo_path; ml_path; packages } =
   let default_ml = CList.is_empty ml_path in
   let coqenv = Boot.Env.maybe_init ~boot ~coqlib
       ~warn_ignored_coqlib:CWarnings.warn_ignored_coqlib
@@ -258,7 +266,11 @@ let init_load_path ~boot ~coqlib ~vo_path ~ml_path =
   let () = if not default_ml then Nativelib.include_dirs := ml_path in
   (* always add current directory *)
   add_path ~unix_path:"." ~rocq_root:Loadpath.default_root_prefix;
-  (* additional loadpath, given with -R/-Q options *)
+  (* additional loadpath, given with -R/-Q/-package options *)
+  let packages = Rocq_package.resolve packages in
+  List.iter (fun (p:Rocq_package.t) ->
+      add_rec_path ~unix_path:p.dir ~rocq_root:(Loadpath.dirpath_of_string p.logpath))
+    packages;
   List.iter
     (fun (unix_path, rocq_root) -> add_rec_path ~unix_path ~rocq_root)
     (List.rev vo_path)
@@ -334,14 +346,6 @@ let usage () =
 
 end
 
-type opts = {
-  boot : bool;
-  coqlib : string option;
-  vo_path : (string * DirPath.t) list;
-  ml_path : string list;
-  packages : string list;
-}
-
 let rec parse_args (args : string list) accu =
   match args with
   | [] -> CErrors.user_err (Pp.str "parse args error: missing argument")
@@ -378,23 +382,12 @@ let rec parse_args (args : string list) accu =
     let args_msg = String.concat " " args in
     CErrors.user_err Pp.(str "parse args error, too many arguments: " ++ str args_msg)
 
-let resolve_packages opts =
-  List.fold_left (fun opts p ->
-    let logpath = Loadpath.dirpath_of_string p.Rocq_package.logpath in
-    { opts with vo_path = (p.Rocq_package.dir, logpath) :: opts.vo_path }
-  ) opts (Rocq_package.resolve opts.packages)
-
 let () =
   let _ = Feedback.add_feeder fb_handler in
   try
     let opts = { boot = false; coqlib = None; vo_path = []; ml_path = []; packages = [] } in
     let opts, in_file = parse_args (List.tl @@ Array.to_list Sys.argv) opts in
-    let opts = resolve_packages opts in
-    let () = init_load_path ~boot:opts.boot
-        ~coqlib:opts.coqlib
-        ~vo_path:(List.rev opts.vo_path)
-        ~ml_path:(List.rev opts.ml_path)
-    in
+    let () = init_load_path opts in
     let senv = init_rocq () in
     compile senv ~in_file
   with exn ->