From 4f628fabb1660cd3fd8815d696e936413734ff33 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Fri, 10 Jul 2026 14:59:41 +0200 Subject: [PATCH] -package delay resolving until -I have been processed --- lib/coqProject_file.ml | 7 ---- sysinit/coqargs.ml | 12 +----- sysinit/coqinit.ml | 12 ++++++ .../coq-makefile/package-ocamlpath/Foo.v | 1 + .../package-ocamlpath/_CoqProject | 3 ++ .../package-ocamlpath/mylib/mypackage/META | 1 + .../coq-makefile/package-ocamlpath/run.sh | 21 +++++++++++ tools/rocqmakefile.ml | 23 ++---------- topbin/rocqnative.ml | 37 ++++++++----------- 9 files changed, 58 insertions(+), 59 deletions(-) create mode 100644 test-suite/coq-makefile/package-ocamlpath/Foo.v create mode 100644 test-suite/coq-makefile/package-ocamlpath/_CoqProject create mode 100644 test-suite/coq-makefile/package-ocamlpath/mylib/mypackage/META create mode 100755 test-suite/coq-makefile/package-ocamlpath/run.sh diff --git a/lib/coqProject_file.ml b/lib/coqProject_file.ml index fa2757be5d81..56478b140759 100644 --- a/lib/coqProject_file.ml +++ b/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 = [] } diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml index cc8c7373b310..5e7c237c30a2 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 diff --git a/sysinit/coqinit.ml b/sysinit/coqinit.ml index d6f777fbb8de..719cfb6e8e51 100644 --- a/sysinit/coqinit.ml +++ b/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 *) diff --git a/test-suite/coq-makefile/package-ocamlpath/Foo.v b/test-suite/coq-makefile/package-ocamlpath/Foo.v new file mode 100644 index 000000000000..7029c3c2c2e0 --- /dev/null +++ b/test-suite/coq-makefile/package-ocamlpath/Foo.v @@ -0,0 +1 @@ +From MyPack Require X. diff --git a/test-suite/coq-makefile/package-ocamlpath/_CoqProject b/test-suite/coq-makefile/package-ocamlpath/_CoqProject new file mode 100644 index 000000000000..40969246896b --- /dev/null +++ b/test-suite/coq-makefile/package-ocamlpath/_CoqProject @@ -0,0 +1,3 @@ +-I mylib +-package mypackage +Foo.v diff --git a/test-suite/coq-makefile/package-ocamlpath/mylib/mypackage/META b/test-suite/coq-makefile/package-ocamlpath/mylib/mypackage/META new file mode 100644 index 000000000000..27eba018246b --- /dev/null +++ b/test-suite/coq-makefile/package-ocamlpath/mylib/mypackage/META @@ -0,0 +1 @@ +rocqpath = "MyPack" diff --git a/test-suite/coq-makefile/package-ocamlpath/run.sh b/test-suite/coq-makefile/package-ocamlpath/run.sh new file mode 100755 index 000000000000..a25b33c8f464 --- /dev/null +++ b/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 diff --git a/tools/rocqmakefile.ml b/tools/rocqmakefile.ml index c943d773e357..54f94627e270 100644 --- a/tools/rocqmakefile.ml +++ b/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; diff --git a/topbin/rocqnative.ml b/topbin/rocqnative.ml index b3e2d52734fa..e8ea36c8c43e 100644 --- a/topbin/rocqnative.ml +++ b/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 ->