diff options
Diffstat (limited to 'checker/checker.ml')
| -rw-r--r-- | checker/checker.ml | 115 |
1 files changed, 62 insertions, 53 deletions
diff --git a/checker/checker.ml b/checker/checker.ml index 8dbb7e01..fd2725c8 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -1,25 +1,26 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp open CErrors open Util open System -open Flags open Names open Check let () = at_exit flush_all -let chk_pp = Pp.pp_with Format.std_formatter +let pp_arrayi pp fmt a = Array.iteri (fun i x -> pp fmt (i,x)) a let fatal_error info anomaly = - flush_all (); Feedback.msg_error info; flush_all (); + flush_all (); Format.eprintf "@[Fatal Error: @[%a@]@]@\n%!" Pp.pp_with info; flush_all (); exit (if anomaly then 129 else 1) let coq_root = Id.of_string "Coq" @@ -41,9 +42,10 @@ let dirpath_of_string s = [] -> Check.default_root_prefix | dir -> DirPath.make (List.map Id.of_string dir) let path_of_string s = - match parse_dir s with + if Filename.check_suffix s ".vo" then PhysicalFile s + else match parse_dir s with [] -> invalid_arg "path_of_string" - | l::dir -> {dirpath=dir; basename=l} + | l::dir -> LogicalFile {dirpath=dir; basename=l} let ( / ) = Filename.concat @@ -74,7 +76,7 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath = let convert_string d = try Id.of_string d with CErrors.UserError _ -> - if_verbose Feedback.msg_warning + Flags.if_verbose Feedback.msg_warning (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)"); raise Exit @@ -96,17 +98,13 @@ let add_rec_path ~unix_path ~coq_root = (* By the option -include -I or -R of the command line *) let includes = ref [] -let push_include (s, alias) = includes := (s,alias,false) :: !includes -let push_rec_include (s, alias) = includes := (s,alias,true) :: !includes +let push_include (s, alias) = includes := (s,alias) :: !includes let set_default_include d = push_include (d, Check.default_root_prefix) let set_include d p = let p = dirpath_of_string p in push_include (d,p) -let set_rec_include d p = - let p = dirpath_of_string p in - push_rec_include(d,p) (* Initializes the LoadPath *) let init_load_path () = @@ -132,8 +130,7 @@ let init_load_path () = add_path ~unix_path:"." ~coq_root:Check.default_root_prefix; (* additional loadpath, given with -I -include -R options *) List.iter - (fun (unix_path, coq_root, reci) -> - if reci then add_rec_path ~unix_path ~coq_root else add_path ~unix_path ~coq_root) + (fun (unix_path, coq_root) -> add_rec_path ~unix_path ~coq_root) (List.rev !includes); includes := [] @@ -145,15 +142,15 @@ let set_impredicative_set () = impredicative_set := Cic.ImpredicativeSet let engage () = Safe_typing.set_engagement (!impredicative_set) -let admit_list = ref ([] : section_path list) +let admit_list = ref ([] : object_file list) let add_admit s = admit_list := path_of_string s :: !admit_list -let norec_list = ref ([] : section_path list) +let norec_list = ref ([] : object_file list) let add_norec s = norec_list := path_of_string s :: !norec_list -let compile_list = ref ([] : section_path list) +let compile_list = ref ([] : object_file list) let add_compile s = compile_list := path_of_string s :: !compile_list @@ -179,7 +176,9 @@ let print_usage_channel co command = output_string co command; output_string co "coqchk options are:\n"; output_string co -" -R dir coqdir map physical dir to logical coqdir\ +" -Q dir coqdir map physical dir to logical coqdir\ +\n -R dir coqdir synonymous for -Q\ +\n\ \n\ \n -admit module load module and dependencies without checking\ \n -norec module check module but admit dependencies without checking\ @@ -211,15 +210,16 @@ let usage () = open Type_errors let anomaly_string () = str "Anomaly: " -let report () = (str "." ++ spc () ++ str "Please report" ++ - strbrk "at " ++ str Coq_config.wwwbugtracker ++ str ".") +let report () = strbrk (". Please report at " ^ Coq_config.wwwbugtracker ^ ".") let guill s = str "\"" ++ str s ++ str "\"" -let where s = +let where = function +| None -> mt () +| Some s -> if !Flags.debug then (str"in " ++ str s ++ str":" ++ spc ()) else (mt ()) -let rec explain_exn = function +let explain_exn = function | Stream.Failure -> hov 0 (anomaly_string () ++ str "uncaught Stream.Failure.") | Stream.Error txt -> @@ -269,26 +269,26 @@ let rec explain_exn = function | Generalization _ -> str"Generalization" | ActualType _ -> str"ActualType" | CantApplyBadType ((n,a,b),(hd,hdty),args) -> - Format.printf "====== ill-typed term ====@\n"; - Format.printf "@[<hov 2>application head=@ "; - Print.print_pure_constr hd; - Format.printf "@]@\n@[<hov 2>head type=@ "; - Print.print_pure_constr hdty; - Format.printf "@]@\narguments:@\n@[<hv>"; - Array.iteri (fun i (t,ty) -> - Format.printf "@[<hov 2>arg %d=@ " (i+1); - Print.print_pure_constr t; - Format.printf "@ type=@ "; - Print.print_pure_constr ty) args; - Format.printf "@]@\n====== type error ====@\n"; - Print.print_pure_constr b; - Format.printf "@\nis not convertible with@\n"; - Print.print_pure_constr a; - Format.printf "@\n====== universes ====@\n"; - chk_pp - (Univ.pr_universes - (ctx.Environ.env_stratification.Environ.env_universes)); - str "\nCantApplyBadType at argument " ++ int n + (* This mix of printf / pp was here before... *) + let fmt = Format.std_formatter in + let open Format in + let open Print in + fprintf fmt "====== ill-typed term ====@\n"; + fprintf fmt "@[<hov 2>application head=@ %a@]@\n" print_pure_constr hd; + fprintf fmt "@[<hov 2>head type=@ %a@]@\n" print_pure_constr hdty; + let pp_arg fmt (i,(t,ty)) = fprintf fmt "@[<hv>@[<1>arg %d=@ @[%a@]@]@,@[<1>type=@ @[%a@]@]@]@\n@," (i+1) + print_pure_constr t print_pure_constr ty + in + fprintf fmt "arguments:@\n@[<hv>%a@]@\n" (pp_arrayi pp_arg) args; + fprintf fmt "====== type error ====@\n"; + fprintf fmt "%a@\n" print_pure_constr b; + fprintf fmt "is not convertible with@\n"; + fprintf fmt "%a@\n" print_pure_constr a; + fprintf fmt "====== universes ====@\n"; + fprintf fmt "%a@\n%!" Pp.pp_with + (Univ.pr_universes + (ctx.Environ.env_stratification.Environ.env_universes)); + str "CantApplyBadType at argument " ++ int n | CantApplyNonFunctional _ -> str"CantApplyNonFunctional" | IllFormedRecBody _ -> str"IllFormedRecBody" | IllTypedRecBody _ -> str"IllTypedRecBody" @@ -309,6 +309,9 @@ let rec explain_exn = function report ()) | e -> CErrors.print e (* for anomalies and other uncaught exceptions *) +let deprecated flag = + Feedback.msg_warning (str "Deprecated flag " ++ quote (str flag)) + let parse_args argv = let rec parse = function | [] -> () @@ -322,25 +325,28 @@ let parse_args argv = Flags.coqlib_spec := true; parse rem - | ("-I"|"-include") :: d :: "-as" :: p :: rem -> set_include d p; parse rem + | ("-I"|"-include") :: d :: "-as" :: p :: rem -> deprecated "-I"; set_include d p; parse rem | ("-I"|"-include") :: d :: "-as" :: [] -> usage () - | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem + | ("-I"|"-include") :: d :: rem -> deprecated "-I"; set_default_include d; parse rem | ("-I"|"-include") :: [] -> usage () - | "-R" :: d :: p :: rem -> set_rec_include d p;parse rem + | "-Q" :: d :: p :: rem -> set_include d p;parse rem + | "-Q" :: ([] | [_]) -> usage () + + | "-R" :: d :: p :: rem -> set_include d p;parse rem | "-R" :: ([] | [_]) -> usage () | "-debug" :: rem -> set_debug (); parse rem | "-where" :: _ -> - Envars.set_coqlib ~fail:CErrors.error; + Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x)); print_endline (Envars.coqlib ()); exit 0 | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () | ("-v"|"--version") :: _ -> version () - | "-boot" :: rem -> boot := true; parse rem + | "-boot" :: rem -> Flags.boot := true; parse rem | ("-m" | "--memory") :: rem -> Check_stat.memory_stat := true; parse rem | ("-o" | "--output-context") :: rem -> Check_stat.output_context := true; parse rem @@ -352,7 +358,7 @@ let parse_args argv = | "-norec" :: [] -> usage () | "-silent" :: rem -> - Flags.make_silent true; parse rem + Flags.quiet := true; parse rem | s :: _ when s<>"" && s.[0]='-' -> fatal_error (str "Unknown option " ++ str s) false @@ -364,15 +370,18 @@ let parse_args argv = (* To prevent from doing the initialization twice *) let initialized = ref false +(* XXX: At some point we need to either port the checker to use the + feedback system or to remove its use completely. *) let init_with_argv argv = if not !initialized then begin initialized := true; Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *) + let _fhandle = Feedback.(add_feeder (console_feedback_listener Format.err_formatter)) in try parse_args argv; if !Flags.debug then Printexc.record_backtrace true; - Envars.set_coqlib ~fail:CErrors.error; - if_verbose print_header (); + Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x)); + Flags.if_verbose print_header (); init_load_path (); engage (); with e -> |