diff options
| -rw-r--r-- | lib/flags.ml | 1 | ||||
| -rw-r--r-- | lib/flags.mli | 1 | ||||
| -rw-r--r-- | stm/stm.ml | 78 | ||||
| -rw-r--r-- | stm/stm.mli | 12 | ||||
| -rw-r--r-- | toplevel/coqinit.ml | 10 | ||||
| -rw-r--r-- | toplevel/coqinit.mli | 2 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 293 | ||||
| -rw-r--r-- | toplevel/coqtop.mli | 2 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 107 | ||||
| -rw-r--r-- | toplevel/vernac.mli | 5 |
10 files changed, 298 insertions, 213 deletions
diff --git a/lib/flags.ml b/lib/flags.ml index a178eb755..a53a866ab 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -42,7 +42,6 @@ let with_extra_values o l f x = Exninfo.iraise reraise let boot = ref false -let load_init = ref true let record_aux_file = ref false diff --git a/lib/flags.mli b/lib/flags.mli index 8ec2a8073..5233e72a2 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -11,7 +11,6 @@ (** Command-line flags *) val boot : bool ref -val load_init : bool ref (** Set by coqtop to tell the kernel to output to the aux file; will be eventually removed by cleanups such as PR#1103 *) diff --git a/stm/stm.ml b/stm/stm.ml index 220ed9be4..770ccf22d 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -250,8 +250,8 @@ end (* }}} *) (* The main document type associated to a VCS *) type stm_doc_type = - | VoDoc of Names.DirPath.t - | VioDoc of Names.DirPath.t + | VoDoc of string + | VioDoc of string | Interactive of Names.DirPath.t (* Dummy until we land the functional interp patch + fixed start_library *) @@ -276,6 +276,9 @@ module VCS : sig val init : stm_doc_type -> id -> doc (* val get_type : unit -> stm_doc_type *) + val set_ldir : Names.DirPath.t -> unit + val get_ldir : unit -> Names.DirPath.t + val is_interactive : unit -> [`Yes | `No | `Shallow] val is_vio_doc : unit -> bool @@ -460,6 +463,7 @@ end = struct (* {{{ *) let vcs : vcs ref = ref (empty Stateid.dummy) let doc_type = ref (Interactive (Names.DirPath.make [])) + let ldir = ref Names.DirPath.empty let init dt id = doc_type := dt; @@ -467,6 +471,10 @@ end = struct (* {{{ *) vcs := set_info !vcs id (default_info ()); dummy_doc + let set_ldir ld = + ldir := ld + + let get_ldir () = !ldir (* let get_type () = !doc_type *) let is_interactive () = @@ -697,7 +705,7 @@ let state_of_id ~doc id = (****** A cache: fills in the nodes of the VCS document with their value ******) module State : sig - + (** The function is from unit, so it uses the current state to define a new one. I.e. one may been to install the right state before defining a new one. @@ -713,7 +721,6 @@ module State : sig val is_cached : ?cache:Summary.marshallable -> Stateid.t -> bool val is_cached_and_valid : ?cache:Summary.marshallable -> Stateid.t -> bool - val exn_on : Stateid.t -> valid:Stateid.t -> Exninfo.iexn -> Exninfo.iexn (* to send states across worker/master *) type frozen_state @@ -727,9 +734,15 @@ module State : sig val proof_part_of_frozen : frozen_state -> proof_part val assign : Stateid.t -> partial_state -> unit + (* Handlers for initial state, prior to document creation. *) + val register_root_state : unit -> unit + val restore_root_state : unit -> unit + (* Only for internal use to catch problems in parse_sentence, should be removed in the state handling refactoring. *) val cur_id : Stateid.t ref + + end = struct (* {{{ *) (* cur_id holds Stateid.dummy in case the last attempt to define a state @@ -879,6 +892,15 @@ end = struct (* {{{ *) Hooks.(call unreachable_state id ie); Exninfo.iraise ie + let init_state = ref None + + let register_root_state () = + init_state := Some (freeze_global_state `No) + + let restore_root_state () = + cur_id := Stateid.dummy; + unfreeze_global_state Option.(get !init_state) + end (* }}} *) (* indentation code for Show Script, initially contributed @@ -2365,19 +2387,55 @@ end (* }}} *) type stm_init_options = { doc_type : stm_doc_type; + require_libs : (string * string option * bool option) list; (* fb_handler : Feedback.feedback -> unit; iload_path : (string list * string * bool) list; - require_libs : (Names.DirPath.t * string * bool option) list; implicit_std : bool; *) } -let init { doc_type } = +(* +let doc_type_module_name (std : stm_doc_type) = + match std with + | VoDoc mn | VioDoc mn | Vio2Vo mn -> mn + | Interactive mn -> Names.DirPath.to_string mn +*) + +let init_core () = + State.register_root_state () + +let new_doc { doc_type ; require_libs } = + let load_objs libs = + let rq_file (dir, from, exp) = + let mp = Libnames.(Qualid (Loc.tag @@ qualid_of_string dir)) in + let mfrom = Option.map (fun fr -> Libnames.(Qualid (Loc.tag @@ qualid_of_string fr))) from in + Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] in + List.(iter rq_file (rev libs)) + in + + (* We must reset the whole state before creating a document! *) + State.restore_root_state (); + let doc = VCS.init doc_type Stateid.initial in set_undo_classifier Backtrack.undo_vernac_classifier; - (* we declare the library here XXX: *) - State.define ~cache:`Yes (fun () -> ()) Stateid.initial; + + begin match doc_type with + | Interactive ln -> + Declaremods.start_library ln + | VoDoc ln -> + let ldir = Flags.verbosely Library.start_library ln in + VCS.set_ldir ldir; + set_compilation_hints ln + | VioDoc ln -> + let ldir = Flags.verbosely Library.start_library ln in + VCS.set_ldir ldir; + set_compilation_hints ln + end; + load_objs require_libs; + + (* We record the state here! *) + State.define ~cache:`Yes ~redefine:true (fun () -> ()) Stateid.initial; Backtrack.record (); Slaves.init (); if Flags.async_proofs_is_master () then begin @@ -2393,7 +2451,7 @@ let init { doc_type } = (Str.split_delim (Str.regexp ";") (Str.replace_first env_opt "" env)) with Not_found -> () end; end; - doc + doc, VCS.cur_tip () let observe ~doc id = let vcs = VCS.backup () in @@ -2456,6 +2514,7 @@ let check_task name (tasks,rcbackup) i = rc with e when CErrors.noncritical e -> VCS.restore vcs; false let info_tasks (tasks,_) = Slaves.info_tasks tasks + let finish_tasks name u d p (t,rcbackup as tasks) = RemoteCounter.restore rcbackup; let finish_task u (_,_,i) = @@ -2953,6 +3012,7 @@ let edit_at ~doc id = Exninfo.iraise (e, info) let get_current_state ~doc = VCS.cur_tip () +let get_ldir ~doc = VCS.get_ldir () let get_doc did = dummy_doc diff --git a/stm/stm.mli b/stm/stm.mli index 47963e5d8..c65cf6a9a 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -13,17 +13,17 @@ open Names (** The STM doc type determines some properties such as what uncompleted proofs are allowed and recording of aux files. *) type stm_doc_type = - | VoDoc of DirPath.t - | VioDoc of DirPath.t + | VoDoc of string + | VioDoc of string | Interactive of DirPath.t (* Main initalization routine *) type stm_init_options = { doc_type : stm_doc_type; + require_libs : (string * string option * bool option) list; (* fb_handler : Feedback.feedback -> unit; iload_path : (string list * string * bool) list; - require_libs : (Names.DirPath.t * string * bool option) list; implicit_std : bool; *) } @@ -31,7 +31,10 @@ type stm_init_options = { (** The type of a STM document *) type doc -val init : stm_init_options -> doc +val init_core : unit -> unit + +(* Starts a new document *) +val new_doc : stm_init_options -> doc * Stateid.t (* [parse_sentence sid pa] Reads a sentence from [pa] with parsing state [sid] Returns [End_of_input] if the stream ends *) @@ -105,6 +108,7 @@ val finish_tasks : string -> (* Id of the tip of the current branch *) val get_current_state : doc:doc -> Stateid.t +val get_ldir : doc:doc -> Names.DirPath.t (* This returns the node at that position *) val get_ast : doc:doc -> Stateid.t -> (Vernacexpr.vernac_expr Loc.located) option diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index bf22c16cd..c80899288 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -59,9 +59,9 @@ let load_rcfile doc sid = doc, sid) (* Recursively puts dir in the LoadPath if -nois was not passed *) -let add_stdlib_path ~unix_path ~coq_root ~with_ml = +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:(!Flags.load_init) + Mltop.add_rec_path add_ml ~unix_path ~coq_root ~implicit:load_init let add_userlib_path ~unix_path = Mltop.add_rec_path Mltop.AddRecML ~unix_path @@ -75,7 +75,7 @@ let ml_includes = ref [] let push_ml_include s = ml_includes := s :: !ml_includes (* Initializes the LoadPath *) -let init_load_path () = +let init_load_path ~load_init = 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 @@ -93,9 +93,9 @@ let init_load_path () = if System.exists_dir (coqlib/"toploop") then Mltop.add_ml_dir (coqlib/"toploop"); (* then standard library *) - add_stdlib_path ~unix_path:(coqlib/"theories") ~coq_root ~with_ml:false; + add_stdlib_path ~load_init ~unix_path:(coqlib/"theories") ~coq_root ~with_ml:false; (* then plugins *) - add_stdlib_path ~unix_path:(coqlib/"plugins") ~coq_root ~with_ml:true; + 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; diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index 2c275a00d..60ed698b8 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -20,6 +20,6 @@ val push_include : string -> Names.DirPath.t -> bool -> unit val push_ml_include : string -> unit -val init_load_path : unit -> unit +val init_load_path : load_init:bool -> unit val init_ocaml_path : unit -> unit diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 9b58c9a65..e9fdaac5b 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -188,11 +188,9 @@ let load_vernacular doc sid = Vernac.load_vernac ~verbosely ~interactive:false ~check:true doc sid s) (doc, sid) (List.rev !load_vernacular_list) -let load_vernacular_obj = ref ([] : string list) -let add_vernac_obj s = load_vernacular_obj := s :: !load_vernacular_obj -let load_vernac_obj () = - let map dir = Qualid (Loc.tag @@ qualid_of_string dir) in - Vernacentries.vernac_require None None (List.rev_map map !load_vernacular_obj) +let load_init_vernaculars doc sid = + let doc, sid = Coqinit.load_rcfile doc sid in + load_vernacular doc sid (******************************************************************************) (* Required Modules *) @@ -201,26 +199,23 @@ let set_include d p implicit = let p = dirpath_of_string p in Coqinit.push_include d p implicit -let require_prelude () = - let vo = Envars.coqlib () / "theories/Init/Prelude.vo" in - let vio = Envars.coqlib () / "theories/Init/Prelude.vio" in - let m = - if Sys.file_exists vo then vo else - if Sys.file_exists vio then vio else vo in - Library.require_library_from_dirpath [Coqlib.prelude_module,m] (Some true) - -let require_list = ref ([] : string list) +(* None = No Import; Some false = Import; Some true = Export *) +let require_list = ref ([] : (string * string option * bool option) list) let add_require s = require_list := s :: !require_list -let require () = - let () = if !Flags.load_init then Flags.silently require_prelude () in - let map dir = Qualid (Loc.tag @@ qualid_of_string dir) in - Vernacentries.vernac_require None (Some false) (List.rev_map map !require_list) + +let load_init = ref true + +(* From Coq Require Import Prelude. *) +let prelude_data = "Prelude", Some "Coq", Some true + +let require_libs () = + if !load_init then prelude_data :: !require_list else !require_list let add_compat_require v = match v with - | Flags.V8_5 -> add_require "Coq.Compat.Coq85" - | Flags.V8_6 -> add_require "Coq.Compat.Coq86" - | Flags.V8_7 -> add_require "Coq.Compat.Coq87" + | Flags.V8_5 -> add_require ("Coq.Compat.Coq85", None, Some false) + | Flags.V8_6 -> add_require ("Coq.Compat.Coq86", None, Some false) + | Flags.V8_7 -> add_require ("Coq.Compat.Coq87", None, Some false) | Flags.VOld | Flags.Current -> () (******************************************************************************) @@ -230,9 +225,9 @@ let add_compat_require v = let glob_opt = ref false let compile_list = ref ([] : (bool * string) list) -let _compilation_list : Stm.stm_doc_type list ref = ref [] -let compilation_mode = ref Vernac.BuildVo +type compilation_mode = BuildVo | BuildVio | Vio2Vo +let compilation_mode = ref BuildVo let compilation_output_name = ref None let batch_mode = ref false @@ -253,21 +248,140 @@ let add_compile verbose s = in compile_list := (verbose,s) :: !compile_list -let compile_file mode doc (verbosely,f_in) = +let warn_file_no_extension = + CWarnings.create ~name:"file-no-extension" ~category:"filesystem" + (fun (f,ext) -> + str "File \"" ++ str f ++ + strbrk "\" has been implicitly expanded to \"" ++ + str f ++ str ext ++ str "\"") + +let ensure_ext ext f = + if Filename.check_suffix f ext then f + else begin + warn_file_no_extension (f,ext); + f ^ ext + end + +let chop_extension f = + try Filename.chop_extension f with _ -> f + +let compile_error msg = + Topfmt.std_logger Feedback.Error msg; + flush_all (); + exit 1 + +let ensure_bname src tgt = + let src, tgt = Filename.basename src, Filename.basename tgt in + let src, tgt = chop_extension src, chop_extension tgt in + if src <> tgt then + compile_error (str "Source and target file names must coincide, directories can differ" ++ fnl () ++ + str "Source: " ++ str src ++ fnl () ++ + str "Target: " ++ str tgt) + +let ensure ext src tgt = ensure_bname src tgt; ensure_ext ext tgt + +let ensure_v v = ensure ".v" v v +let ensure_vo v vo = ensure ".vo" v vo +let ensure_vio v vio = ensure ".vio" v vio + +let ensure_exists f = + if not (Sys.file_exists f) then + compile_error (hov 0 (str "Can't find file" ++ spc () ++ str f)) + +(* Compile a vernac file *) +let compile ~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 + compile_error (str "There are pending proofs: " + ++ (pfs + |> List.rev + |> prlist_with_sep pr_comma Names.Id.print) + ++ str ".") + in + match !compilation_mode with + | BuildVo -> + Flags.record_aux_file := true; + let long_f_dot_v = ensure_v f_in in + ensure_exists long_f_dot_v; + let long_f_dot_vo = + match f_out with + | None -> long_f_dot_v ^ "o" + | Some f -> ensure_vo long_f_dot_v f in + + let doc, sid = Stm.(new_doc + { doc_type = VoDoc long_f_dot_vo; + require_libs = require_libs () + }) in + + let doc, sid = load_init_vernaculars 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) + ~v_file:long_f_dot_v); + 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 = Stm.join ~doc in + let wall_clock2 = Unix.gettimeofday () in + check_pending_proofs (); + Library.save_library_to ldir long_f_dot_vo (Global.opaque_tables ()); + Aux_file.record_in_aux_at "vo_compile_time" + (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1)); + Aux_file.stop_aux_file (); + Dumpglob.end_dump_glob () + | BuildVio -> + + Flags.record_aux_file := false; + Dumpglob.noglob (); + + let long_f_dot_v = ensure_v f_in in + ensure_exists long_f_dot_v; + + let long_f_dot_vio = + match f_out with + | None -> long_f_dot_v ^ "io" + | Some f -> ensure_vio long_f_dot_v f in + + let doc, sid = Stm.(new_doc + { doc_type = VioDoc long_f_dot_vio; + require_libs = require_libs () + }) in + + let doc, sid = load_init_vernaculars 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 = Stm.finish ~doc in + check_pending_proofs (); + let _doc = Stm.snapshot_vio ~doc ldir long_f_dot_vio in + Stm.reset_task_queue () + + | Vio2Vo -> + let open Filename in + Flags.record_aux_file := false; + Dumpglob.noglob (); + let f = if check_suffix f_in ".vio" then chop_extension f_in else f_in in + let lfdv, sum, lib, univs, disch, tasks, proofs = Library.load_library_todo f in + 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 = + ignore(CoqworkmgrApi.get 1); + compile ~verbosely ~f_in ~f_out; + CoqworkmgrApi.giveback 1 + +let compile_file (verbosely,f_in) = if !Flags.beautify then - Flags.with_option Flags.beautify_file (fun f_in -> Vernac.compile ~verbosely ~mode ~doc ~f_in ~f_out:None) f_in + Flags.with_option Flags.beautify_file + (fun f_in -> compile ~verbosely ~f_in ~f_out:None) f_in else - Vernac.compile ~verbosely ~mode ~doc ~f_in ~f_out:None + compile ~verbosely ~f_in ~f_out:None let compile_files doc = if !compile_list == [] then () - else - let init_state = States.freeze ~marshallable:`No in - let mode = !compilation_mode in - List.iter (fun vf -> - States.unfreeze init_state; - compile_file mode doc vf) - (List.rev !compile_list) + else List.iter compile_file (List.rev !compile_list) (******************************************************************************) (* VIO Dispatching *) @@ -279,7 +393,7 @@ let add_vio_task f = Flags.quiet := true; vio_tasks := f :: !vio_tasks -let check_vio_tasks doc = +let check_vio_tasks () = let rc = List.fold_left (fun acc t -> Vio_checking.check_vio t && acc) true (List.rev !vio_tasks) in @@ -303,7 +417,7 @@ let set_vio_checking_j opt j = prerr_endline "setting the J variable like in 'make vio2vo J=3'"; exit 1 -let schedule_vio_checking doc = +let schedule_vio_checking () = if !vio_files <> [] && !vio_checking then Vio_checking.schedule_vio_checking !vio_files_j !vio_files @@ -374,7 +488,7 @@ let usage batch = begin try Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib); - Coqinit.init_load_path (); + Coqinit.init_load_path ~load_init:!load_init; with NoCoqLib -> usage_no_coqlib () end; if batch then Usage.print_usage_coqc () @@ -563,20 +677,20 @@ let parse_args arglist = |"-inputstate"|"-is" -> set_inputstate (next ()) |"-load-ml-object" -> Mltop.dir_ml_load (next ()) |"-load-ml-source" -> Mltop.dir_ml_use (next ()) - |"-load-vernac-object" -> add_vernac_obj (next ()) + |"-load-vernac-object" -> add_require (next (), None, None) |"-load-vernac-source"|"-l" -> add_load_vernacular false (next ()) |"-load-vernac-source-verbose"|"-lv" -> add_load_vernacular true (next ()) |"-outputstate" -> set_outputstate (next ()) |"-print-mod-uid" -> let s = String.concat " " (List.map get_native_name rem) in print_endline s; exit 0 |"-profile-ltac-cutoff" -> Flags.profile_ltac := true; Flags.profile_ltac_cutoff := get_float opt (next ()) - |"-require" -> add_require (next ()) + |"-require" -> add_require (next (), None, Some false) |"-top" -> set_toplevel_name (dirpath_of_string (next ())) |"-with-geoproof" -> Coq_config.with_geoproof := get_bool opt (next ()) |"-main-channel" -> Spawned.main_channel := get_host_port opt (next()) |"-control-channel" -> Spawned.control_channel := get_host_port opt (next()) |"-vio2vo" -> add_compile false (next ()); - compilation_mode := Vernac.Vio2Vo + compilation_mode := Vio2Vo |"-toploop" -> set_toploop (next ()) |"-w" | "-W" -> let w = next () in @@ -609,7 +723,7 @@ let parse_args arglist = |"-impredicative-set" -> set_impredicative_set () |"-indices-matter" -> Indtypes.enforce_indices_matter () |"-m"|"--memory" -> memory_stat := true - |"-noinit"|"-nois" -> Flags.load_init := false + |"-noinit"|"-nois" -> load_init := false |"-no-glob"|"-noglob" -> Dumpglob.noglob (); glob_opt := true |"-native-compiler" -> if Coq_config.no_native_compiler then @@ -621,11 +735,11 @@ let parse_args arglist = |"-quiet"|"-silent" -> Flags.quiet := true; Flags.make_warn false |"-quick" -> Safe_typing.allow_delayed_constants := true; - compilation_mode := Vernac.BuildVio + compilation_mode := BuildVio |"-list-tags" -> print_tags := true |"-time" -> Flags.time := true |"-type-in-type" -> set_type_in_type () - |"-unicode" -> add_require "Utf8_core" + |"-unicode" -> add_require ("Utf8_core", None, Some false) |"-v"|"--version" -> Usage.version (exitcode ()) |"-print-version"|"--print-version" -> Usage.machine_readable_version (exitcode ()) |"-where" -> print_where := true @@ -640,12 +754,18 @@ let parse_args arglist = with any -> fatal_error any let init_toplevel arglist = + (* Coq's init process, phase 1: + - OCaml parameters, and basic structures and IO + *) Profile.init_profile (); init_gc (); Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *) let init_feeder = Feedback.add_feeder coqtop_init_feed in Lib.init(); - let doc = begin + (* Coq's init process, phase 2: + - Basic Coq environment, load-path, plugins. + *) + let res = begin try let extras = parse_args arglist in (* If we have been spawned by the Spawn module, this has to be done @@ -656,7 +776,7 @@ 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 (); + Coqinit.init_load_path ~load_init:!load_init; Option.iter Mltop.load_ml_object_raw !toploop; let extras = !toploop_init extras in if not (CList.is_empty extras) then begin @@ -665,52 +785,67 @@ let init_toplevel arglist = exit 1 end; Flags.if_verbose print_header (); - inputstate (); Mltop.init_known_plugins (); engage (); + + (* Allow the user to load an arbitrary state here *) + inputstate (); + + (* This state will be shared by all the documents *) + Stm.init_core (); + + (* Coq init process, phase 3: Stm initialization, backtracking state. + + It is essential that the module system is in a consistent + state before we take the first snapshot. This was not + guaranteed in the past. In particular, we want to be sure we + have called start_library before loading the prelude and rest + of required files. + + We split the codepath here depending whether coqtop is called + in interactive mode or not. *) + if (not !batch_mode || CList.is_empty !compile_list) - && Global.env_is_initial () - then Declaremods.start_library !toplevel_name; - load_vernac_obj (); - require (); - let doc = Stm.(init { doc_type = Interactive Names.DirPath.empty }) in - let doc, sid = Coqinit.load_rcfile doc (Stm.get_current_state ~doc) in - (* XXX: We ignore this for now, but should be threaded to the toplevels *) - let doc, _sid = load_vernacular doc sid in - compile_files doc; - (* All these tasks use coqtop as a driver to invoke more coqtop, - * they should be really orthogonal to coqtop. - *) - schedule_vio_checking doc; - schedule_vio_compilation (); - check_vio_tasks doc; - outputstate (); - doc + (* Interactive *) + then begin + try + let doc, sid = Stm.(new_doc + { doc_type = Interactive !toplevel_name; + require_libs = require_libs () + }) in + Some (load_init_vernaculars doc sid) + with any -> flush_all(); fatal_error any + (* Non interactive *) + end else begin + try + compile_files (); + schedule_vio_checking (); + schedule_vio_compilation (); + check_vio_tasks (); + (* Allow the user to output an arbitrary state *) + outputstate (); + None + with any -> flush_all(); fatal_error any + end; with any -> flush_all(); - let extra = None - (* XXX: Must refine once Stm.init takes care of the start_library & friends *) - (* if !batch_mode && not Stateid.(equal (Stm.get_current_state ~doc) dummy) *) - (* then None *) - (* else Some (str "Error during initialization: ") *) - in + let extra = Some (str "Error during initialization: ") in fatal_error ?extra any end in - if !batch_mode then begin + Feedback.del_feeder init_feeder; + res + +let start () = + match init_toplevel (List.tl (Array.to_list Sys.argv)) with + (* Batch mode *) + | Some (doc, sid) when not !batch_mode -> + !toploop_run doc; + exit 1 + | _ -> flush_all(); if !output_context then Feedback.msg_notice Flags.(with_option raw_print Prettyp.print_full_pure_context () ++ fnl ()); Profile.print_profile (); exit 0 - end; - Feedback.del_feeder init_feeder; - doc - -let start () = - let doc = init_toplevel (List.tl (Array.to_list Sys.argv)) in - (* In batch mode, Coqtop has already exited at this point. In interactive one, - dump glob is nothing but garbage ... *) - !toploop_run doc; - exit 1 (* [Coqtop.start] will be called by the code produced by coqmktop *) diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index 4c26a6ebc..1c7c3f944 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -11,7 +11,7 @@ state, load the files given on the command line, load the resource file, produce the output state if any, and finally will launch [Coqloop.loop]. *) -val init_toplevel : string list -> Stm.doc +val init_toplevel : string list -> (Stm.doc * Stateid.t) option val start : unit -> unit diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 1e09a1c0d..d736975d3 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -103,11 +103,6 @@ let pr_open_cur_subgoals () = try Printer.pr_open_subgoals () with Proof_global.NoCurrentProof -> Pp.str "" -let vernac_error msg = - Topfmt.std_logger Feedback.Error msg; - flush_all (); - exit 1 - (* Reenable when we get back to feedback printing *) (* let is_end_of_input any = match any with *) (* Stm.End_of_input -> true *) @@ -247,105 +242,3 @@ and load_vernac ~verbosely ~check ~interactive doc sid file = let process_expr doc sid loc_ast = checknav_deep loc_ast; interp_vernac ~interactive:true ~check:true doc sid loc_ast - -let warn_file_no_extension = - CWarnings.create ~name:"file-no-extension" ~category:"filesystem" - (fun (f,ext) -> - str "File \"" ++ str f ++ - strbrk "\" has been implicitly expanded to \"" ++ - str f ++ str ext ++ str "\"") - -let ensure_ext ext f = - if Filename.check_suffix f ext then f - else begin - warn_file_no_extension (f,ext); - f ^ ext - end - -let chop_extension f = - try Filename.chop_extension f with _ -> f - -let ensure_bname src tgt = - let src, tgt = Filename.basename src, Filename.basename tgt in - let src, tgt = chop_extension src, chop_extension tgt in - if src <> tgt then - vernac_error (str "Source and target file names must coincide, directories can differ" ++ fnl () ++ - str "Source: " ++ str src ++ fnl () ++ - str "Target: " ++ str tgt) - -let ensure ext src tgt = ensure_bname src tgt; ensure_ext ext tgt - -let ensure_v v = ensure ".v" v v -let ensure_vo v vo = ensure ".vo" v vo -let ensure_vio v vio = ensure ".vio" v vio - -let ensure_exists f = - if not (Sys.file_exists f) then - vernac_error (hov 0 (str "Can't find file" ++ spc () ++ str f)) - -type compilation_mode = BuildVo | BuildVio | Vio2Vo - -(* Compile a vernac file *) -let compile ~verbosely ~mode ~doc ~f_in ~f_out= - let check_pending_proofs () = - let pfs = Proof_global.get_all_proof_names () in - if not (List.is_empty pfs) then - vernac_error (str "There are pending proofs: " - ++ (pfs - |> List.rev - |> prlist_with_sep pr_comma Names.Id.print) - ++ str ".") - in - match mode with - | BuildVo -> - let long_f_dot_v = ensure_v f_in in - ensure_exists long_f_dot_v; - let long_f_dot_vo = - match f_out with - | None -> long_f_dot_v ^ "o" - | Some f -> ensure_vo long_f_dot_v f in - let ldir = Flags.verbosely Library.start_library long_f_dot_vo in - Stm.set_compilation_hints long_f_dot_vo; - Aux_file.(start_aux_file - ~aux_file:(aux_file_name_for long_f_dot_vo) - ~v_file:long_f_dot_v); - 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 _ = load_vernac ~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 (); - Library.save_library_to ldir long_f_dot_vo (Global.opaque_tables ()); - Aux_file.record_in_aux_at "vo_compile_time" - (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1)); - Aux_file.stop_aux_file (); - Dumpglob.end_dump_glob () - | BuildVio -> - let long_f_dot_v = ensure_v f_in in - ensure_exists long_f_dot_v; - let long_f_dot_vio = - match f_out with - | None -> long_f_dot_v ^ "io" - | Some f -> ensure_vio long_f_dot_v f in - let ldir = Flags.verbosely Library.start_library long_f_dot_vio in - Dumpglob.noglob (); - Stm.set_compilation_hints long_f_dot_vio; - let _ = load_vernac ~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 - Stm.reset_task_queue () - | Vio2Vo -> - let open Filename in - Dumpglob.noglob (); - let f = if check_suffix f_in ".vio" then chop_extension f_in else f_in in - let lfdv, sum, lib, univs, disch, tasks, proofs = Library.load_library_todo f in - Stm.set_compilation_hints lfdv; - let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in - Library.save_library_raw lfdv sum lib univs proofs - -let compile ~verbosely ~mode ~doc ~f_in ~f_out = - ignore(CoqworkmgrApi.get 1); - compile ~verbosely ~mode ~doc ~f_in ~f_out; - CoqworkmgrApi.giveback 1 diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index d3a45ce9d..f9a430026 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -18,8 +18,3 @@ val process_expr : Stm.doc -> Stateid.t -> Vernacexpr.vernac_expr Loc.located -> 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 - -type compilation_mode = BuildVo | BuildVio | Vio2Vo - -(** Compile a vernac file, (f is assumed without .v suffix) *) -val compile : verbosely:bool -> mode:compilation_mode -> doc:Stm.doc -> f_in:string -> f_out:string option -> unit |