diff options
| -rw-r--r-- | dev/ci/user-overlays/08914-ejgallego-lib+better_boot_coqproject.sh | 6 | ||||
| -rw-r--r-- | ide/coqide.ml | 7 | ||||
| -rw-r--r-- | lib/coqProject_file.ml | 18 | ||||
| -rw-r--r-- | lib/coqProject_file.mli | 4 | ||||
| -rw-r--r-- | tools/coq_makefile.ml | 5 | ||||
| -rw-r--r-- | tools/coqdep.ml | 3 |
6 files changed, 24 insertions, 19 deletions
diff --git a/dev/ci/user-overlays/08914-ejgallego-lib+better_boot_coqproject.sh b/dev/ci/user-overlays/08914-ejgallego-lib+better_boot_coqproject.sh new file mode 100644 index 0000000000..1c5157ba12 --- /dev/null +++ b/dev/ci/user-overlays/08914-ejgallego-lib+better_boot_coqproject.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "8914" ] || [ "$CI_BRANCH" = "lib+better_boot_coqproject" ]; then + + quickchick_CI_REF=lib+better_boot_coqproject + quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick + +fi diff --git a/ide/coqide.ml b/ide/coqide.ml index a26f7d1b94..b3160174ad 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -103,7 +103,8 @@ let make_coqtop_args fname = with | None -> "", base_args | Some proj -> - proj, coqtop_args_from_project (read_project_file proj) @ base_args + let warning_fn x = Feedback.msg_warning Pp.(str x) in + proj, coqtop_args_from_project (read_project_file ~warning_fn proj) @ base_args in let args = match fname with | None -> args @@ -112,7 +113,6 @@ let make_coqtop_args fname = else "-topfile"::fname::args in proj, args -;; (** Setting drag & drop on widgets *) @@ -1355,7 +1355,8 @@ let read_coqide_args argv = if project_files <> None then (output_string stderr "Error: multiple -f options"; exit 1); let d = CUnix.canonical_path_name (Filename.dirname file) in - let p = CoqProject_file.read_project_file file in + let warning_fn x = Format.eprintf "%s@\n%!" x in + let p = CoqProject_file.read_project_file ~warning_fn file in filter_coqtop coqtop (Some (d,p)) out args |"-f" :: [] -> output_string stderr "Error: missing project file name"; exit 1 diff --git a/lib/coqProject_file.ml b/lib/coqProject_file.ml index 7395654022..868042303d 100644 --- a/lib/coqProject_file.ml +++ b/lib/coqProject_file.ml @@ -12,10 +12,6 @@ ideally we would like to make this independent so it can be bootstrapped. *) -(* Note the problem with the error invokation below calling exit... *) -(* let error msg = Feedback.msg_error msg *) -let warning msg = Feedback.msg_warning Pp.(str msg) - type arg_source = CmdLine | ProjectFile type 'a sourced = { thing : 'a; source : arg_source } @@ -147,7 +143,7 @@ let exists_dir dir = try Sys.is_directory (strip_trailing_slash dir) with Sys_error _ -> false -let process_cmd_line orig_dir proj args = +let process_cmd_line ~warning_fn orig_dir proj args = let parsing_project_file = ref (proj.project_file <> None) in let sourced x = { thing = x; source = if !parsing_project_file then ProjectFile else CmdLine } in let orig_dir = (* avoids turning foo.v in ./foo.v *) @@ -170,7 +166,7 @@ let process_cmd_line orig_dir proj args = | ("-full"|"-opt") :: r -> aux { proj with use_ocamlopt = true } r | "-install" :: d :: r -> if proj.install_kind <> None then - (warning "-install set more than once.@\n%!"); + (warning_fn "-install set more than once."); let install = match d with | "user" -> UserInstall | "none" -> NoInstall @@ -197,7 +193,7 @@ let process_cmd_line orig_dir proj args = let file = CUnix.remove_path_dot (CUnix.correct_path file orig_dir) in let () = match proj.project_file with | None -> () - | Some _ -> warning "Multiple project files are deprecated.@\n%!" + | Some _ -> warning_fn "Multiple project files are deprecated." in parsing_project_file := true; let proj = aux { proj with project_file = Some file } (parse file) in @@ -236,11 +232,11 @@ let process_cmd_line orig_dir proj args = (******************************* API ************************************) -let cmdline_args_to_project ~curdir args = - process_cmd_line curdir (mk_project None None None true) args +let cmdline_args_to_project ~warning_fn ~curdir args = + process_cmd_line ~warning_fn curdir (mk_project None None None true) args -let read_project_file f = - process_cmd_line (Filename.dirname f) +let read_project_file ~warning_fn f = + process_cmd_line ~warning_fn (Filename.dirname f) (mk_project (Some f) None (Some NoInstall) true) (parse f) let rec find_project_file ~from ~projfile_name = diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli index 2a6a09a9a0..20b276ce8c 100644 --- a/lib/coqProject_file.mli +++ b/lib/coqProject_file.mli @@ -51,8 +51,8 @@ and install = | TraditionalInstall | UserInstall -val cmdline_args_to_project : curdir:string -> string list -> project -val read_project_file : string -> project +val cmdline_args_to_project : warning_fn:(string -> unit) -> curdir:string -> string list -> project +val read_project_file : warning_fn:(string -> unit) -> string -> project val coqtop_args_from_project : project -> string list val find_project_file : from:string -> projfile_name:string -> string option diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index ca5a232edb..8560bac786 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -396,8 +396,9 @@ let _ = | "-destination-of" :: tgt :: rest -> Some tgt, rest | _ -> None, args in - let project = - try cmdline_args_to_project ~curdir:Filename.current_dir_name args + let project = + let warning_fn x = Format.eprintf "%s@\n%!" x in + try cmdline_args_to_project ~warning_fn ~curdir:Filename.current_dir_name args with Parsing_error s -> prerr_endline s; usage_coq_makefile () in if only_destination <> None then begin diff --git a/tools/coqdep.ml b/tools/coqdep.ml index ba88069be9..226a19678f 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -473,7 +473,8 @@ let add_r_include path l = add_rec_dir_import add_known path (split_period l) let treat_coqproject f = let open CoqProject_file in let iter_sourced f = List.iter (fun {thing} -> f thing) in - let project = read_project_file f in + let warning_fn x = coqdep_warning "%s" x in + let project = read_project_file ~warning_fn f in iter_sourced (fun { path } -> add_caml_dir path) project.ml_includes; iter_sourced (fun ({ path }, l) -> add_q_include path l) project.q_includes; iter_sourced (fun ({ path }, l) -> add_r_include path l) project.r_includes; |