diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml index cc8c7373b310..5a8b120d03d5 100644 --- a/sysinit/coqargs.ml +++ b/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 *) diff --git a/sysinit/coqargs.mli b/sysinit/coqargs.mli index fc14db70196f..ad01ee900133 100644 --- a/sysinit/coqargs.mli +++ b/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; diff --git a/sysinit/coqinit.ml b/sysinit/coqinit.ml index d6f777fbb8de..17dea4712673 100644 --- a/sysinit/coqinit.ml +++ b/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; diff --git a/sysinit/dune b/sysinit/dune index 16954aea3731..2f35ff3d5004 100644 --- a/sysinit/dune +++ b/sysinit/dune @@ -5,7 +5,7 @@ (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) @@ -13,4 +13,4 @@ (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)) diff --git a/test-suite/misc/rocq-find.sh b/test-suite/misc/rocq-find.sh index b2c6d6bcac8a..4ee4a5eaf478 100755 --- a/test-suite/misc/rocq-find.sh +++ b/test-suite/misc/rocq-find.sh @@ -80,3 +80,44 @@ cat > "$TMP/find-foo-flags.expected" < "$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" diff --git a/test-suite/unit-tests/lib/coqargs_test.ml b/test-suite/unit-tests/lib/coqargs_test.ml new file mode 100644 index 000000000000..f678f097a90b --- /dev/null +++ b/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)