Fix repeated Coqargs parsing with ~init

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
@@ -442,19 +432,23 @@ let parse_args ~init arglist : t * string list =
   in
   parse init
 
-(* We need to reverse a few lists *)
+(* These lists are accumulated in reverse order by the parser.  This helper
+   converts both from and to that representation. *)
+let reverse_accumulators opts =
+  { opts with
+    pre = { opts.pre with
+            ml_includes = List.rev opts.pre.ml_includes
+          ; vo_includes = List.rev opts.pre.vo_includes
+          ; packages = List.rev opts.pre.packages
+          ; load_vernacular_list = List.rev opts.pre.load_vernacular_list
+          ; injections = List.rev opts.pre.injections
+          }
+  }
+
 let parse_args ~init args =
+  let init = reverse_accumulators init in
   let opts, extra = parse_args ~init args in
-  let opts =
-    { opts with
-      pre = { opts.pre with
-              ml_includes = List.rev opts.pre.ml_includes
-            ; vo_includes = List.rev opts.pre.vo_includes
-            ; load_vernacular_list = List.rev opts.pre.load_vernacular_list
-            ; injections = List.rev opts.pre.injections
-            }
-    } in
-  opts, extra
+  reverse_accumulators opts, extra
 
 (******************************************************************************)
 (* Startup LoadPath and Modules                                               *)

sysinit/coqargs.mli

@@ -80,7 +80,10 @@ type coqargs_pre = {
 
   ml_includes : CUnix.physical_path list;
   vo_includes : vo_path list;
+  (** Explicit load paths specified with [-Q] or [-R]. *)
   packages : string list;
+  (** Findlib package names specified with [-package].  They are resolved when
+      the document is initialized. *)
 
   load_vernacular_list : string list;
   injections  : injection_command list;

sysinit/coqinit.ml

@@ -172,7 +172,17 @@ 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) *)
-  List.iter (fun x -> Loadpath.add_vo_path @@ to_vo_path x) opts.pre.vo_includes;
+  let package_includes =
+    let vo_path_of_package (x:Rocq_package.t) : vo_path = {
+      implicit = false;
+      unix_path = x.dir;
+      rocq_path = x.logpath;
+      }
+    in
+    List.rev_map vo_path_of_package (Rocq_package.resolve opts.pre.packages)
+  in
+  let vo_includes = opts.pre.vo_includes @ package_includes in
+  List.iter (fun x -> Loadpath.add_vo_path @@ to_vo_path x) vo_includes;
 
   (* Kernel configuration *)
   Global.set_impredicative_set opts.config.logic.impredicative_set;

sysinit/dune

@@ -5,12 +5,12 @@
  (modules coqargs)
  (wrapped false)
  ; don't depend on rocq-runtime.lib -> impossible to imperatively set random flags
- (libraries rocq-runtime.config rocq-runtime.boot rocq-runtime.clib rocq-runtime.lib))
+ (libraries rocq-runtime.config rocq-runtime.boot rocq-runtime.clib))
 
 (library
  (name sysinit)
  (public_name rocq-runtime.sysinit)
  (synopsis "Rocq's initialization")
  (wrapped false)
  (modules :standard \ coqargs)
- (libraries rocq-runtime.boot rocq-runtime.vernac coqargs findlib))
+ (libraries rocq-runtime.boot rocq-runtime.lib rocq-runtime.vernac coqargs findlib))

test-suite/misc/rocq-find.sh

@@ -80,3 +80,44 @@ cat > "$TMP/find-foo-flags.expected" <<EOT
 -Q '$FINDLIB_LIB/foo/rocq.d' Foo
 EOT
 diff -u "$TMP/find-foo-flags.expected" "$TMP/find-foo-flags.out"
+
+# Package arguments are resolved when a document is initialized.  Check that
+# this still installs the package and its transitive dependencies.
+rm -rf "$LIB/rocq-runtime"
+mkdir -p "$LIB/foo/rocq.d" "$LIB/bar/rocq.d"
+
+cat > "$LIB/bar/rocq.d/BarValue.v" <<'EOT'
+Axiom answer : Type.
+EOT
+
+$coqc -boot -noinit -Q "$LIB/bar/rocq.d" Bar \
+  "$LIB/bar/rocq.d/BarValue.v"
+
+cat > "$LIB/foo/rocq.d/FooValue.v" <<'EOT'
+From Bar Require Import BarValue.
+Definition answer := BarValue.answer.
+EOT
+
+$coqc -boot -noinit \
+  -Q "$LIB/bar/rocq.d" Bar \
+  -Q "$LIB/foo/rocq.d" Foo \
+  "$LIB/foo/rocq.d/FooValue.v"
+
+cat > "$TMP/client.v" <<'EOT'
+From Foo Require Import FooValue.
+Check FooValue.answer.
+EOT
+
+PACKAGE_OCAMLPATH="$FINDLIB_LIB${FINDLIB_SEP:-:}${OCAMLPATH:-}"
+OCAMLPATH="$PACKAGE_OCAMLPATH" \
+  $coqc -boot -noinit -package foo "$TMP/client.v"
+
+if OCAMLPATH="$PACKAGE_OCAMLPATH" \
+  $coqc -boot -noinit \
+  -package missing-package "$TMP/client.v" \
+  >"$TMP/missing.out" 2>&1; then
+  echo "rocq c unexpectedly accepted a missing package" >&2
+  exit 1
+fi
+
+grep -q "Failed to locate package missing-package" "$TMP/missing.out"

test-suite/unit-tests/lib/coqargs_test.ml

@@ -0,0 +1,60 @@
+open OUnit
+open Utest
+
+let tests = ref []
+let add_test name test = tests := mk_test name (TestCase test) :: !tests
+
+let parse ?(init=Coqargs.default) args =
+  fst (Coqargs.parse_args ~init args)
+
+let first_args =
+  [ "-I"; "ml-a"
+  ; "-R"; "."; "Test"
+  ; "-load-vernac-source"; "first"
+  ; "-set"; "Printing Depth=10"
+  ; "-package"; "package-a"
+  ]
+
+let second_args =
+  [ "-I"; "ml-b"
+  ; "-R"; "_build/default"; "Test"
+  ; "-load-vernac-source"; "second"
+  ; "-unset"; "Printing Depth"
+  ; "-package"; "package-b"
+  ]
+
+let test_compositional () =
+  let one_pass = parse (first_args @ second_args) in
+  let split = parse ~init:(parse first_args) second_args in
+  assert_equal one_pass split
+
+let () = add_test "one-pass and incremental parsing agree" test_compositional
+
+let test_empty_parse_identity () =
+  let opts = parse (first_args @ second_args) in
+  assert_equal opts (parse ~init:opts [])
+
+let () = add_test "empty incremental parse preserves init" test_empty_parse_identity
+
+let test_normalized_order () =
+  let opts = parse (first_args @ second_args) in
+  let expected_vo_includes : Coqargs.vo_path list =
+    [ { implicit = true; unix_path = "."; rocq_path = "Test" }
+    ; { implicit = true; unix_path = "_build/default"; rocq_path = "Test" }
+    ]
+  in
+  assert_equal ["ml-a"; "ml-b"] opts.pre.ml_includes;
+  assert_equal expected_vo_includes opts.pre.vo_includes;
+  assert_equal ["package-a"; "package-b"] opts.pre.packages;
+  assert_equal ["first.v"; "second.v"] opts.pre.load_vernacular_list
+
+let () = add_test "ordered options are returned in declaration order" test_normalized_order
+
+let test_packages_are_not_resolved_during_parsing () =
+  let opts = parse ["-package"; "a-package-that-does-not-exist"] in
+  assert_equal ["a-package-that-does-not-exist"] opts.pre.packages;
+  assert_equal [] opts.pre.vo_includes
+
+let () = add_test "package resolution is deferred" test_packages_are_not_resolved_during_parsing
+
+let () = run_tests __FILE__ (open_log_out_ch __FILE__) (List.rev !tests)