diff options
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/check.ml | 2 | ||||
| -rw-r--r-- | checker/checker.ml | 36 | ||||
| -rw-r--r-- | checker/dune | 7 | ||||
| -rw-r--r-- | checker/values.ml | 2 |
4 files changed, 25 insertions, 22 deletions
diff --git a/checker/check.ml b/checker/check.ml index 1ff1425dea..587bb90d43 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -149,7 +149,7 @@ let remove_load_path dir = load_paths := List.filter2 (fun p d -> p <> dir) physical logical let add_load_path (phys_path,coq_path) = - if !Flags.debug then + if CDebug.(get_flag misc) then Feedback.msg_notice (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++ str phys_path); let phys_path = CUnix.canonical_path_name phys_path in diff --git a/checker/checker.ml b/checker/checker.ml index bdfc5f07be..f55ed9e8d6 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -48,19 +48,17 @@ let path_of_string s = let ( / ) = Filename.concat -let get_version_date () = +let get_version () = try let ch = open_in (Envars.coqlib () / "revision") in let ver = input_line ch in let rev = input_line ch in let () = close_in ch in - (ver,rev) - with _ -> (Coq_config.version,Coq_config.date) + Printf.sprintf "%s (%s)" ver rev + with _ -> Coq_config.version let print_header () = - let (ver,rev) = (get_version_date ()) in - Printf.printf "Welcome to Chicken %s (%s)\n" ver rev; - flush stdout + Printf.printf "Welcome to Chicken %s\n%!" (get_version ()) (* Adding files to Coq loadpath *) @@ -109,7 +107,15 @@ let init_load_path () = let user_contrib = coqlib/"user-contrib" in let xdg_dirs = Envars.xdg_dirs in let coqpath = Envars.coqpath in - let plugins = coqlib/"plugins" in + let plugins = + CPath.choose_existing + [ CPath.make [ coqlib ; "plugins" ] + ; CPath.make [ coqlib ; ".."; "coq-core"; "plugins" ] + ] |> function + | None -> + CErrors.user_err (Pp.str "Cannot find plugins directory") + | Some f -> (f :> string) + in (* NOTE: These directories are searched from last to first *) (* first standard library *) add_rec_path ~unix_path:(coqlib/"theories") ~coq_root:(Names.DirPath.make[coq_root]); @@ -132,8 +138,6 @@ let init_load_path () = includes := [] -let set_debug () = Flags.debug := true - let impredicative_set = ref Declarations.PredicativeSet let set_impredicative_set () = impredicative_set := Declarations.ImpredicativeSet @@ -170,9 +174,7 @@ let compile_files senv = ~check:(List.rev !compile_list) let version () = - Printf.printf "The Coq Proof Checker, version %s (%s)\n" - Coq_config.version Coq_config.date; - Printf.printf "compiled on %s\n" Coq_config.compile_date; + Printf.printf "The Coq Proof Checker, version %s\n" Coq_config.version; exit 0 (* print the usage of coqtop (or coqc) on channel co *) @@ -222,7 +224,7 @@ let guill s = str "\"" ++ str s ++ str "\"" let where = function | None -> mt () | Some s -> - if !Flags.debug then (str"in " ++ str s ++ str":" ++ spc ()) else (mt ()) + if CDebug.(get_flag misc) then (str"in " ++ str s ++ str":" ++ spc ()) else (mt ()) let explain_exn = function | Stream.Failure -> @@ -251,7 +253,7 @@ let explain_exn = function hov 0 (fnl () ++ str "User interrupt.") | Univ.UniverseInconsistency i -> let msg = - if !Flags.debug then + if CDebug.(get_flag misc) then str "." ++ spc() ++ Univ.explain_universe_inconsistency Univ.Level.pr i else @@ -339,7 +341,7 @@ let parse_args argv = | ("-Q"|"-R") :: d :: p :: rem -> set_include d p;parse rem | ("-Q"|"-R") :: ([] | [_]) -> usage () - | "-debug" :: rem -> set_debug (); parse rem + | "-debug" :: rem -> CDebug.set_debug_all true; parse rem | "-where" :: _ -> Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x)); @@ -377,7 +379,7 @@ let init_with_argv argv = try parse_args argv; CWarnings.set_flags ("+"^Typeops.warn_bad_relevance_name); - if !Flags.debug then Printexc.record_backtrace true; + if CDebug.(get_flag misc) then Printexc.record_backtrace true; Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x)); Flags.if_verbose print_header (); init_load_path (); @@ -392,7 +394,7 @@ let run senv = let senv = compile_files senv in flush_all(); senv with e -> - if !Flags.debug then Printexc.print_backtrace stderr; + if CDebug.(get_flag misc) then Printexc.print_backtrace stderr; fatal_error (explain_exn e) (is_anomaly e) let start () = diff --git a/checker/dune b/checker/dune index af7d4f2923..78b4032141 100644 --- a/checker/dune +++ b/checker/dune @@ -7,13 +7,14 @@ (synopsis "Coq's Standalone Proof Checker") (modules :standard \ coqchk votour) (wrapped true) - (libraries coq.kernel)) + (libraries coq-core.kernel)) (executable (name coqchk) (public_name coqchk) (modes exe byte) - (package coq) + ; Move to coq-checker? + (package coq-core) (modules coqchk) (flags :standard -open Coq_checklib) (libraries coq_checklib)) @@ -21,7 +22,7 @@ (executable (name votour) (public_name votour) - (package coq) + (package coq-core) (modules votour) (flags :standard -open Coq_checklib) (libraries coq_checklib)) diff --git a/checker/values.ml b/checker/values.ml index 907f9f7e32..f7a367b986 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -240,7 +240,7 @@ let v_template_universes = v_tuple "template_universes" [|List(Opt v_level);v_context_set|] let v_primitive = - v_enum "primitive" 50 (* Number of "Primitive" in Int63.v and PrimFloat.v *) + v_enum "primitive" 54 (* Number of constructors of the CPrimitives.t type *) let v_cst_def = v_sum "constant_def" 0 |