aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/coqinit.ml112
-rw-r--r--toplevel/coqinit.mli6
-rw-r--r--toplevel/coqloop.ml10
-rw-r--r--toplevel/coqloop.mli4
-rw-r--r--toplevel/coqtop.ml50
-rw-r--r--toplevel/vernac.ml24
-rw-r--r--toplevel/vernac.mli4
7 files changed, 117 insertions, 93 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 3a195c1df..b3b5375bf 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -27,12 +27,12 @@ let set_rcfile s = rcfile := s; rcfile_specified := true
let load_rc = ref true
let no_load_rc () = load_rc := false
-let load_rcfile doc sid =
+let load_rcfile ~time doc sid =
if !load_rc then
try
if !rcfile_specified then
if CUnix.file_readable_p !rcfile then
- Vernac.load_vernac ~verbosely:false ~interactive:false ~check:true doc sid !rcfile
+ Vernac.load_vernac ~time ~verbosely:false ~interactive:false ~check:true doc sid !rcfile
else raise (Sys_error ("Cannot read rcfile: "^ !rcfile))
else
try
@@ -43,7 +43,7 @@ let load_rcfile doc sid =
Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version;
Envars.home ~warn / "."^rcdefaultname
] in
- Vernac.load_vernac ~verbosely:false ~interactive:false ~check:true doc sid inferedrc
+ Vernac.load_vernac ~time ~verbosely:false ~interactive:false ~check:true doc sid inferedrc
with Not_found -> doc, sid
(*
Flags.if_verbose
@@ -59,13 +59,23 @@ let load_rcfile doc sid =
doc, sid)
(* Recursively puts dir in the LoadPath if -nois was not passed *)
-let add_stdlib_path ~load_init ~unix_path ~coq_root ~with_ml =
- let add_ml = if with_ml then Mltop.AddRecML else Mltop.AddNoML in
- Mltop.add_rec_path add_ml ~unix_path ~coq_root ~implicit:load_init
+let build_stdlib_path ~load_init ~unix_path ~coq_path ~with_ml =
+ let open Mltop in
+ let add_ml = if with_ml then AddRecML else AddNoML in
+ { recursive = true;
+ path_spec = VoPath { unix_path; coq_path ; has_ml = add_ml; implicit = load_init }
+ }
-let add_userlib_path ~unix_path =
- Mltop.add_rec_path Mltop.AddRecML ~unix_path
- ~coq_root:Libnames.default_root_prefix ~implicit:false
+let build_userlib_path ~unix_path =
+ let open Mltop in
+ { recursive = true;
+ path_spec = VoPath {
+ unix_path;
+ coq_path = Libnames.default_root_prefix;
+ has_ml = Mltop.AddRecML;
+ implicit = false;
+ }
+ }
(* Options -I, -I-as, and -R of the command line *)
let includes = ref []
@@ -74,51 +84,65 @@ let push_include s alias implicit =
let ml_includes = ref []
let push_ml_include s = ml_includes := s :: !ml_includes
+let ml_path_if c p =
+ let open Mltop in
+ let f x = { recursive = false; path_spec = MlPath x } in
+ if c then List.map f p else []
+
(* Initializes the LoadPath *)
let init_load_path ~load_init =
+ let open Mltop in
let coqlib = Envars.coqlib () in
let user_contrib = coqlib/"user-contrib" in
let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x)) in
let coqpath = Envars.coqpath in
- let coq_root = Names.DirPath.make [Libnames.coq_root] in
- (* NOTE: These directories are searched from last to first *)
- (* first, developer specific directory to open *)
- if Coq_config.local then
- Mltop.add_ml_dir (coqlib/"dev");
- (* main loops *)
- if Coq_config.local || !Flags.boot then begin
- Mltop.add_ml_dir (coqlib/"stm");
- Mltop.add_ml_dir (coqlib/"ide")
- end;
- if System.exists_dir (coqlib/"toploop") then
- Mltop.add_ml_dir (coqlib/"toploop");
- (* then standard library *)
- add_stdlib_path ~load_init ~unix_path:(coqlib/"theories") ~coq_root ~with_ml:false;
- (* then plugins *)
- add_stdlib_path ~load_init ~unix_path:(coqlib/"plugins") ~coq_root ~with_ml:true;
- (* then user-contrib *)
- if Sys.file_exists user_contrib then
- add_userlib_path ~unix_path:user_contrib;
- (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME *)
- List.iter (fun s -> add_userlib_path ~unix_path:s) xdg_dirs;
- (* then directories in COQPATH *)
- List.iter (fun s -> add_userlib_path ~unix_path:s) coqpath;
- (* then current directory (not recursively!) *)
- Mltop.add_ml_dir ".";
- Loadpath.add_load_path "." Libnames.default_root_prefix ~implicit:false;
- (* additional loadpath, given with options -Q and -R *)
- List.iter
- (fun (unix_path, coq_root, implicit) ->
- Mltop.add_rec_path Mltop.AddNoML ~unix_path ~coq_root ~implicit)
- (List.rev !includes);
- (* additional ml directories, given with option -I *)
- List.iter Mltop.add_ml_dir (List.rev !ml_includes)
+ let coq_path = Names.DirPath.make [Libnames.coq_root] in
+
+ (* NOTE: These directories are searched from last to first *)
+ (* first, developer specific directory to open *)
+ ml_path_if Coq_config.local [coqlib/"dev"] @
+
+ (* main loops *)
+ ml_path_if (Coq_config.local || !Flags.boot) [coqlib/"stm"; coqlib/"ide"] @
+ ml_path_if (System.exists_dir (coqlib/"toploop")) [coqlib/"toploop"] @
+
+ (* then standard library and plugins *)
+ [build_stdlib_path ~load_init ~unix_path:(coqlib/"theories") ~coq_path ~with_ml:false;
+ build_stdlib_path ~load_init ~unix_path:(coqlib/"plugins") ~coq_path ~with_ml:true ] @
+
+ (* then user-contrib *)
+ (if Sys.file_exists user_contrib then
+ [build_userlib_path ~unix_path:user_contrib] else []
+ ) @
+
+ (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME and COQPATH *)
+ List.map (fun s -> build_userlib_path ~unix_path:s) (xdg_dirs @ coqpath) @
+
+ (* then current directory (not recursively!) *)
+ [ { recursive = false;
+ path_spec = VoPath { unix_path = ".";
+ coq_path = Libnames.default_root_prefix;
+ implicit = false;
+ has_ml = AddTopML }
+ } ] @
+
+ (* additional loadpaths, given with options -Q and -R *)
+ List.map
+ (fun (unix_path, coq_path, implicit) ->
+ { recursive = true;
+ path_spec = VoPath { unix_path; coq_path; has_ml = Mltop.AddNoML; implicit } })
+ (List.rev !includes) @
+
+ (* additional ml directories, given with option -I *)
+ List.map (fun s -> {recursive = false; path_spec = MlPath s}) (List.rev !ml_includes)
(* Initialises the Ocaml toplevel before launching it, so that it can
find the "include" file in the *source* directory *)
let init_ocaml_path () =
+ let open Mltop in
+ let lp s = { recursive = false; path_spec = MlPath s } in
let add_subdir dl =
- Mltop.add_ml_dir (List.fold_left (/) Envars.coqroot [dl])
+ Mltop.add_coq_path (lp (List.fold_left (/) Envars.coqroot [dl]))
in
- Mltop.add_ml_dir (Envars.coqlib ());
+ Mltop.add_coq_path (lp (Envars.coqlib ()));
List.iter add_subdir Coq_config.all_src_dirs
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index 60ed698b8..089847f5d 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -13,13 +13,11 @@ val set_debug : unit -> unit
val set_rcfile : string -> unit
val no_load_rc : unit -> unit
-val load_rcfile : Stm.doc -> Stateid.t -> Stm.doc * Stateid.t
+val load_rcfile : time:bool -> Stm.doc -> Stateid.t -> Stm.doc * Stateid.t
val push_include : string -> Names.DirPath.t -> bool -> unit
(** [push_include phys_path log_path implicit] *)
val push_ml_include : string -> unit
-
-val init_load_path : load_init:bool -> unit
-
+val init_load_path : load_init:bool -> Mltop.coq_path list
val init_ocaml_path : unit -> unit
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 910c81381..5c1b27c33 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -300,13 +300,13 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in
is caught and handled (i.e. not re-raised).
*)
-let do_vernac doc sid =
+let do_vernac ~time doc sid =
top_stderr (fnl());
if !print_emacs then top_stderr (str (top_buffer.prompt doc));
resynch_buffer top_buffer;
try
let input = (top_buffer.tokens, None) in
- Vernac.process_expr doc sid (read_sentence ~doc sid (fst input))
+ Vernac.process_expr ~time doc sid (read_sentence ~doc sid (fst input))
with
| Stm.End_of_input | CErrors.Quit ->
top_stderr (fnl ()); raise CErrors.Quit
@@ -337,13 +337,13 @@ let loop_flush_all () =
Format.pp_print_flush !Topfmt.std_ft ();
Format.pp_print_flush !Topfmt.err_ft ()
-let rec loop doc =
+let rec loop ~time doc =
Sys.catch_break true;
try
reset_input_buffer doc stdin top_buffer;
(* Be careful to keep this loop tail-recursive *)
let rec vernac_loop doc sid =
- let ndoc, nsid = do_vernac doc sid in
+ let ndoc, nsid = do_vernac ~time doc sid in
loop_flush_all ();
vernac_loop ndoc nsid
(* We recover the current stateid, threading from the caller is
@@ -358,4 +358,4 @@ let rec loop doc =
fnl() ++
str"Please report" ++
strbrk" at " ++ str Coq_config.wwwbugtracker ++ str ".");
- loop doc
+ loop ~time doc
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index 46934f326..09240ec82 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -32,8 +32,8 @@ val coqloop_feed : Feedback.feedback -> unit
(** Parse and execute one vernac command. *)
-val do_vernac : Stm.doc -> Stateid.t -> Stm.doc * Stateid.t
+val do_vernac : time:bool -> Stm.doc -> Stateid.t -> Stm.doc * Stateid.t
(** Main entry point of Coq: read and execute vernac commands. *)
-val loop : Stm.doc -> Stm.doc
+val loop : time:bool -> Stm.doc -> Stm.doc
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 437b7b0ac..9719f60bb 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -80,6 +80,7 @@ let toploop_init = ref begin fun x ->
bogus. For now we just print to the console too *)
let coqtop_init_feed = Coqloop.coqloop_feed
let drop_last_doc = ref None
+let measure_time = ref false
(* Default toplevel loop *)
let console_toploop_run doc =
@@ -89,7 +90,7 @@ let console_toploop_run doc =
Flags.if_verbose warning "Dumpglob cannot be used in interactive mode.";
Dumpglob.noglob ()
end;
- let doc = Coqloop.loop doc in
+ let doc = Coqloop.loop ~time:!measure_time doc in
(* Initialise and launch the Ocaml toplevel *)
drop_last_doc := Some doc;
Coqinit.init_ocaml_path();
@@ -180,19 +181,19 @@ let load_vernacular_list = ref ([] : (string * bool) list)
let add_load_vernacular verb s =
load_vernacular_list := ((CUnix.make_suffix s ".v"),verb) :: !load_vernacular_list
-let load_vernacular doc sid =
+let load_vernacular ~time doc sid =
List.fold_left
(fun (doc,sid) (f_in, verbosely) ->
let s = Loadpath.locate_file f_in in
if !Flags.beautify then
- Flags.with_option Flags.beautify_file (Vernac.load_vernac ~verbosely ~interactive:false ~check:true doc sid) f_in
+ Flags.with_option Flags.beautify_file (Vernac.load_vernac ~time ~verbosely ~interactive:false ~check:true doc sid) f_in
else
- Vernac.load_vernac ~verbosely ~interactive:false ~check:true doc sid s)
+ Vernac.load_vernac ~time ~verbosely ~interactive:false ~check:true doc sid s)
(doc, sid) (List.rev !load_vernacular_list)
-let load_init_vernaculars doc sid =
- let doc, sid = Coqinit.load_rcfile doc sid in
- load_vernacular doc sid
+let load_init_vernaculars ~time doc sid =
+ let doc, sid = Coqinit.load_rcfile ~time doc sid in
+ load_vernacular ~time doc sid
(******************************************************************************)
(* Required Modules *)
@@ -291,7 +292,7 @@ let ensure_exists f =
compile_error (hov 0 (str "Can't find file" ++ spc () ++ str f))
(* Compile a vernac file *)
-let compile ~verbosely ~f_in ~f_out =
+let compile ~time ~verbosely ~f_in ~f_out =
let check_pending_proofs () =
let pfs = Proof_global.get_all_proof_names () in
if not (CList.is_empty pfs) then
@@ -316,7 +317,7 @@ let compile ~verbosely ~f_in ~f_out =
require_libs = require_libs ()
}) in
- let doc, sid = load_init_vernaculars doc sid in
+ let doc, sid = load_init_vernaculars ~time doc sid in
let ldir = Stm.get_ldir ~doc in
Aux_file.(start_aux_file
~aux_file:(aux_file_name_for long_f_dot_vo)
@@ -324,7 +325,7 @@ let compile ~verbosely ~f_in ~f_out =
Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo;
Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n");
let wall_clock1 = Unix.gettimeofday () in
- let doc, _ = Vernac.load_vernac ~verbosely ~check:true ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in
+ let doc, _ = Vernac.load_vernac ~time ~verbosely ~check:true ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in
let _doc = Stm.join ~doc in
let wall_clock2 = Unix.gettimeofday () in
check_pending_proofs ();
@@ -351,10 +352,10 @@ let compile ~verbosely ~f_in ~f_out =
require_libs = require_libs ()
}) in
- let doc, sid = load_init_vernaculars doc sid in
+ let doc, sid = load_init_vernaculars ~time doc sid in
let ldir = Stm.get_ldir ~doc in
- let doc, _ = Vernac.load_vernac ~verbosely ~check:false ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in
+ let doc, _ = Vernac.load_vernac ~time ~verbosely ~check:false ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in
let doc = Stm.finish ~doc in
check_pending_proofs ();
let _doc = Stm.snapshot_vio ~doc ldir long_f_dot_vio in
@@ -369,9 +370,9 @@ let compile ~verbosely ~f_in ~f_out =
let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in
Library.save_library_raw lfdv sum lib univs proofs
-let compile ~verbosely ~f_in ~f_out =
+let compile ~time ~verbosely ~f_in ~f_out =
ignore(CoqworkmgrApi.get 1);
- compile ~verbosely ~f_in ~f_out;
+ compile ~time ~verbosely ~f_in ~f_out;
CoqworkmgrApi.giveback 1
let compile_file (verbosely,f_in) =
@@ -381,9 +382,9 @@ let compile_file (verbosely,f_in) =
else
compile ~verbosely ~f_in ~f_out:None
-let compile_files doc =
+let compile_files ~time =
if !compile_list == [] then ()
- else List.iter compile_file (List.rev !compile_list)
+ else List.iter (compile_file ~time) (List.rev !compile_list)
(******************************************************************************)
(* VIO Dispatching *)
@@ -488,11 +489,11 @@ exception NoCoqLib
let usage batch =
begin
- try
- Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib);
- Coqinit.init_load_path ~load_init:!load_init;
- with NoCoqLib -> usage_no_coqlib ()
+ try Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib)
+ with NoCoqLib -> usage_no_coqlib ()
end;
+ let lp = Coqinit.init_load_path ~load_init:!load_init in
+ List.iter Mltop.add_coq_path lp;
if batch then Usage.print_usage_coqc ()
else begin
Mltop.load_ml_objects_raw_rex
@@ -736,7 +737,7 @@ let parse_args arglist =
|"-quiet"|"-silent" -> Flags.quiet := true; Flags.make_warn false
|"-quick" -> compilation_mode := BuildVio
|"-list-tags" -> print_tags := true
- |"-time" -> Flags.time := true
+ |"-time" -> measure_time := true
|"-type-in-type" -> set_type_in_type ()
|"-unicode" -> add_require ("Utf8_core", None, Some false)
|"-v"|"--version" -> Usage.version (exitcode ())
@@ -775,7 +776,8 @@ let init_toplevel arglist =
if !print_config then (Envars.print_config stdout Coq_config.all_src_dirs; exit (exitcode ()));
if !print_tags then (print_style_tags (); exit (exitcode ()));
if !filter_opts then (print_string (String.concat "\n" extras); exit 0);
- Coqinit.init_load_path ~load_init:!load_init;
+ let lp = Coqinit.init_load_path ~load_init:!load_init in
+ List.iter Mltop.add_coq_path lp;
Option.iter Mltop.load_ml_object_raw !toploop;
let extras = !toploop_init extras in
if not (CList.is_empty extras) then begin
@@ -812,12 +814,12 @@ let init_toplevel arglist =
{ doc_type = Interactive !toplevel_name;
require_libs = require_libs ()
}) in
- Some (load_init_vernaculars doc sid)
+ Some (load_init_vernaculars ~time:!measure_time doc sid)
with any -> flush_all(); fatal_error any
(* Non interactive *)
end else begin
try
- compile_files ();
+ compile_files ~time:!measure_time;
schedule_vio_checking ();
schedule_vio_compilation ();
check_vio_tasks ();
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 8fdaedbaf..6b45a94bc 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -110,15 +110,15 @@ let pr_open_cur_subgoals () =
(* Stm.End_of_input -> true *)
(* | _ -> false *)
-let rec interp_vernac ~check ~interactive doc sid (loc,com) =
- let interp = function
+let rec interp_vernac ~time ~check ~interactive doc sid (loc,com) =
+ let interp v =
+ match under_control v with
| VernacLoad (verbosely, fname) ->
- let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in
+ let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in
let fname = CUnix.make_suffix fname ".v" in
let f = Loadpath.locate_file fname in
- load_vernac ~verbosely ~check ~interactive doc sid f
- | v ->
-
+ load_vernac ~time ~verbosely ~check ~interactive doc sid f
+ | _ ->
(* XXX: We need to run this before add as the classification is
highly dynamic and depends on the structure of the
document. Hopefully this is fixed when VtMeta can be removed
@@ -157,8 +157,8 @@ let rec interp_vernac ~check ~interactive doc sid (loc,com) =
try
(* The -time option is only supported from console-based
clients due to the way it prints. *)
- if !Flags.time then print_cmd_header ?loc com;
- let com = if !Flags.time then VernacTime (loc,com) else com in
+ if time then print_cmd_header ?loc com;
+ let com = if time then VernacTime(time,(loc,com)) else com in
interp com
with reraise ->
(* XXX: In non-interactive mode edit_at seems to do very weird
@@ -172,7 +172,7 @@ let rec interp_vernac ~check ~interactive doc sid (loc,com) =
end in iraise (reraise, info)
(* Load a vernac file. CErrors are annotated with file and location *)
-and load_vernac ~verbosely ~check ~interactive doc sid file =
+and load_vernac ~time ~verbosely ~check ~interactive doc sid file =
let ft_beautify, close_beautify =
if !Flags.beautify_file then
let chan_beautify = open_out (file^beautify_suffix) in
@@ -214,7 +214,7 @@ and load_vernac ~verbosely ~check ~interactive doc sid file =
Option.iter (vernac_echo ?loc) in_echo;
checknav_simple (loc, ast);
- let ndoc, nsid = Flags.silently (interp_vernac ~check ~interactive !rdoc !rsid) (loc, ast) in
+ let ndoc, nsid = Flags.silently (interp_vernac ~time ~check ~interactive !rdoc !rsid) (loc, ast) in
rsid := nsid;
rdoc := ndoc
done;
@@ -241,6 +241,6 @@ and load_vernac ~verbosely ~check ~interactive doc sid file =
of a new state label). An example of state-preserving command is one coming
from the query panel of Coqide. *)
-let process_expr doc sid loc_ast =
+let process_expr ~time doc sid loc_ast =
checknav_deep loc_ast;
- interp_vernac ~interactive:true ~check:true doc sid loc_ast
+ interp_vernac ~time ~interactive:true ~check:true doc sid loc_ast
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index f9a430026..b77b024fa 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -12,9 +12,9 @@
expected to handle and print errors in form of exceptions, however
care is taken so the state machine is left in a consistent
state. *)
-val process_expr : Stm.doc -> Stateid.t -> Vernacexpr.vernac_expr Loc.located -> Stm.doc * Stateid.t
+val process_expr : time:bool -> Stm.doc -> Stateid.t -> Vernacexpr.vernac_control Loc.located -> Stm.doc * Stateid.t
(** [load_vernac echo sid file] Loads [file] on top of [sid], will
echo the commands if [echo] is set. Callers are expected to handle
and print errors in form of exceptions. *)
-val load_vernac : verbosely:bool -> check:bool -> interactive:bool -> Stm.doc -> Stateid.t -> string -> Stm.doc * Stateid.t
+val load_vernac : time:bool -> verbosely:bool -> check:bool -> interactive:bool -> Stm.doc -> Stateid.t -> string -> Stm.doc * Stateid.t
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 13:07:15 +0000