From 29ae900b33ad5b621c85025340d70ee9056486b7 Mon Sep 17 00:00:00 2001 From: finalchild Date: Sun, 9 Aug 2026 01:38:16 +0900 Subject: [PATCH] Fix repeated Coqargs parsing with ~init Coqargs.parse_args returns ordered list fields, but a returned value reused as init was treated as a reverse-order accumulator. This could reorder existing options. Package declarations were also resolved on every parse, potentially inserting derived load paths repeatedly. Normalize init before entering the parser and normalize the result afterward. Keep package declarations unresolved until init_document so package load paths are installed once at their point of use. --- sysinit/coqargs.ml | 38 ++++++-------- sysinit/coqargs.mli | 3 ++ sysinit/coqinit.ml | 12 ++++- sysinit/dune | 4 +- test-suite/misc/rocq-find.sh | 41 ++++++++++++++++ test-suite/unit-tests/lib/coqargs_test.ml | 60 +++++++++++++++++++++++ 6 files changed, 133 insertions(+), 25 deletions(-) create mode 100644 test-suite/unit-tests/lib/coqargs_test.ml 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)