From ce2b2058587224ade9261cd4127ef4f6e94d356b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 27 Feb 2017 20:16:40 +0100 Subject: [stm] Port the toplevel to the STM. - We clean-up `Vernac` and make it use the STM API. - Now functions in `Vernac` for use in the toplevel and compiler take an starting `Stateid.t`. - Duplicated `Stm.interp` entry point is removed. - The XML protocol call `interp` is disabled. --- dev/doc/changes.txt | 13 ++++ ide/ide_slave.ml | 45 ++----------- lib/flags.ml | 2 - lib/flags.mli | 3 +- stm/stm.ml | 77 ++++++---------------- stm/stm.mli | 9 +-- toplevel/coqinit.ml | 11 ++-- toplevel/coqinit.mli | 2 +- toplevel/coqloop.ml | 31 +++++---- toplevel/coqloop.mli | 2 +- toplevel/coqtop.ml | 17 ++--- toplevel/vernac.ml | 179 +++++++++++++++++++------------------------------- toplevel/vernac.mli | 26 ++------ vernac/vernac.mllib | 1 + vernac/vernacprop.ml | 53 +++++++++++++++ vernac/vernacprop.mli | 19 ++++++ 16 files changed, 221 insertions(+), 269 deletions(-) create mode 100644 vernac/vernacprop.ml create mode 100644 vernac/vernacprop.mli diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 30edea7f2..7e7bb9858 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -156,6 +156,19 @@ document type". This allows for a more uniform handling of printing - A few unused hooks were removed due to cleanups, no clients known. +** Toplevel and Vernacular API ** + +- The components related to vernacular interpretation have been moved + to their own folder `vernac/` whereas toplevel now contains the + proper toplevel shell and compiler. + +- Coq's toplevel has been ported to directly use the common `Stm` + API. The signature of a few functions has changed as a result. + +** XML Protocol ** + +- The legacy `interp` call has been turned into a noop. + ========================================= = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 = ========================================= diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 889757764..bc7ce3883 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -8,6 +8,7 @@ (************************************************************************) open Vernacexpr +open Vernacprop open CErrors open Util open Pp @@ -60,25 +61,6 @@ let is_known_option cmd = match cmd with | VernacUnsetOption o -> coqide_known_option o | _ -> false -let is_debug cmd = match cmd with - | VernacSetOption (["Ltac";"Debug"], _) -> true - | _ -> false - -let is_query cmd = match cmd with - | VernacChdir None - | VernacMemOption _ - | VernacPrintOption _ - | VernacCheckMayEval _ - | VernacGlobalCheck _ - | VernacPrint _ - | VernacSearch _ - | VernacLocate _ -> true - | _ -> false - -let is_undo cmd = match cmd with - | VernacUndo _ | VernacUndoTo _ -> true - | _ -> false - (** Check whether a command is forbidden in the IDE *) let ide_cmd_checks (loc,ast) = @@ -87,7 +69,7 @@ let ide_cmd_checks (loc,ast) = user_error "Debug mode not available in the IDE"; if is_known_option ast then Feedback.msg_warning ~loc (strbrk "Set this option from the IDE menu instead"); - if Vernac.is_navigation_vernac ast || is_undo ast then + if is_navigation_vernac ast || is_undo ast then Feedback.msg_warning ~loc (strbrk "Use IDE navigation instead"); if is_query ast then Feedback.msg_warning ~loc (strbrk "Query commands should not be inserted in scripts") @@ -132,7 +114,7 @@ let query (s,id) = let annotate phrase = let (loc, ast) = let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in - Vernac.parse_sentence (pa,None) + Stm.parse_sentence (Stm.get_current_state ()) pa in (* XXX: Width should be a parameter of annotate... *) Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast) @@ -394,26 +376,9 @@ let init = initial_id end -(* Retrocompatibility stuff *) +(* Retrocompatibility stuff, disabled since 8.7 *) let interp ((_raw, verbose), s) = - let vernac_parse s = - let pa = Pcoq.Gram.parsable (Stream.of_string s) in - Flags.with_option Flags.we_are_parsing (fun () -> - match Pcoq.Gram.entry_parse Pcoq.main_entry pa with - | None -> raise (Invalid_argument "vernac_parse") - | Some ast -> ast) - () in - Stm.interp verbose (vernac_parse s); - (* TODO: the "" parameter is a leftover of the times the protocol - * used to include stderr/stdout output. - * - * Currently, we force all the output meant for the to go via the - * feedback mechanism, and we don't manipulate stderr/stdout, which - * are left to the client's discrection. The parameter is still there - * as not to break the core protocol for this minor change, but it should - * be removed in the next version of the protocol. - *) - Stm.get_current_state (), CSig.Inl "" + Stateid.dummy, CSig.Inr "The interp call has been disabled, please use Add." (** When receiving the Quit call, we don't directly do an [exit 0], but rather set this reference, in order to send a final answer diff --git a/lib/flags.ml b/lib/flags.ml index 5b080151c..ef5eddfb2 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -86,8 +86,6 @@ let in_toplevel = ref false let profile = false let print_emacs = ref false -let coqtop_ui = ref false - let xml_export = ref false let ide_slave = ref false diff --git a/lib/flags.mli b/lib/flags.mli index bd365e653..f5e1c96f9 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -46,9 +46,8 @@ val in_toplevel : bool ref val profile : bool +(* Legacy flags *) val print_emacs : bool ref -val coqtop_ui : bool ref - val xml_export : bool ref val ide_slave : bool ref diff --git a/stm/stm.ml b/stm/stm.ml index fb0a0514d..8d212a6a0 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -323,6 +323,15 @@ end = struct (* {{{ *) open Printf let print_dag vcs () = + + (* Due to threading, be wary that this will be called from the + toplevel with we_are_parsing set to true, as indeed, the + toplevel is waiting for input . What a race! XD + + In case you are hitting the race enable stm_debug. + *) + if stm_debug then Flags.we_are_parsing := false; + let fname = "stm_" ^ Str.global_replace (Str.regexp " ") "_" (System.process_id ()) in let string_of_transaction = function @@ -970,7 +979,6 @@ module Backtrack : sig val record : unit -> unit val backto : Stateid.t -> unit - val back_safe : unit -> unit (* we could navigate the dag, but this ways easy *) val branches_of : Stateid.t -> backup @@ -2342,22 +2350,18 @@ let observe id = VCS.restore vcs; iraise e -let pr_open_cur_subgoals () = - try Printer.pr_open_subgoals () - with Proof_global.NoCurrentProof -> Pp.str "" - -let finish ?(print_goals=false) () = +let finish () = let head = VCS.current_branch () in observe (VCS.get_branch_pos head); - if print_goals then msg_notice (pr_open_cur_subgoals ()); VCS.print (); + (* EJGA: Setting here the proof state looks really wrong, and it + hides true bugs cf bug #5363. Also, what happens with observe? *) (* Some commands may by side effect change the proof mode *) match VCS.get_branch head with | { VCS.kind = `Edit (mode,_,_,_,_) } -> Proof_global.activate_proof_mode mode | { VCS.kind = `Proof (mode, _) } -> Proof_global.activate_proof_mode mode | _ -> () - let wait () = Slaves.wait_all_done (); VCS.print () @@ -2435,29 +2439,17 @@ let merge_proof_branch ~valid ?id qast keep brname = (* When tty is true, this code also does some of the job of the user interface: jump back to a state that is valid *) -let handle_failure (e, info) vcs tty = +let handle_failure (e, info) vcs = if e = CErrors.Drop then iraise (e, info) else match Stateid.get info with | None -> VCS.restore vcs; VCS.print (); - if tty && interactive () = `Yes then begin - (* Hopefully the 1 to last state is valid *) - Backtrack.back_safe (); - VCS.checkout_shallowest_proof_branch (); - end; - VCS.print (); anomaly(str"error with no safe_id attached:" ++ spc() ++ CErrors.iprint_no_report (e, info)) | Some (safe_id, id) -> stm_prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id); VCS.restore vcs; - if tty && interactive () = `Yes then begin - (* We stay on a valid state *) - Backtrack.backto safe_id; - VCS.checkout_shallowest_proof_branch (); - Reach.known_state ~cache:(interactive ()) safe_id; - end; VCS.print (); iraise (e, info) @@ -2471,7 +2463,7 @@ let snapshot_vio ldir long_f_dot_vo = let reset_task_queue = Slaves.reset_task_queue (* Document building *) -let process_transaction ?(newtip=Stateid.fresh ()) ~tty +let process_transaction ?(newtip=Stateid.fresh ()) ({ verbose; loc; expr } as x) c = stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x); let vcs = VCS.backup () in @@ -2517,13 +2509,6 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty anomaly(str"classifier: VtBack + VtLater must imply part_of_script") (* Query *) - | VtQuery (false,(report_id,route)), VtNow when tty = true -> - finish (); - (try Future.purify (stm_vernac_interp report_id ~route) - {x with verbose = true } - with e when CErrors.noncritical e -> - let e = CErrors.push e in - iraise (State.exn_on ~valid:Stateid.dummy report_id e)); `Ok | VtQuery (false,(report_id,route)), VtNow -> (try stm_vernac_interp report_id ~route x with e -> @@ -2655,7 +2640,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty rc with e -> let e = CErrors.push e in - handle_failure e vcs tty + handle_failure e vcs let get_ast id = match VCS.visit id with @@ -2743,7 +2728,7 @@ let add ~ontop ?newtip verb (loc, ast) = (* XXX: Classifiy vernac should be moved inside process transaction *) let clas = classify_vernac ast in let aast = { verbose = verb; indentation; strlen; loc; expr = ast } in - match process_transaction ?newtip ~tty:false aast clas with + match process_transaction ?newtip aast clas with | `Ok -> VCS.cur_tip (), `NewTip | `Unfocus qed_id -> qed_id, `Unfocus (VCS.cur_tip ()) @@ -2766,10 +2751,9 @@ let query ~at ?(report_with=(Stateid.dummy,default_route)) s = let aast = { verbose = true; indentation; strlen; loc; expr = ast } in match clas with | VtStm (w,_), _ -> - ignore(process_transaction ~tty:false aast (VtStm (w,false), VtNow)) + ignore(process_transaction aast (VtStm (w,false), VtNow)) | _ -> - ignore(process_transaction - ~tty:false aast (VtQuery (false,report_with), VtNow))) + ignore(process_transaction aast (VtQuery (false,report_with), VtNow))) s let edit_at id = @@ -2898,32 +2882,11 @@ let edit_at id = let backup () = VCS.backup () let restore d = VCS.restore d +let get_current_state () = VCS.cur_tip () + (*********************** TTY API (PG, coqtop, coqc) ***************************) (******************************************************************************) -let interp verb (loc,e) = - let clas = classify_vernac e in - let aast = { verbose = verb; indentation = 0; strlen = 0; loc; expr = e } in - let rc = process_transaction ~tty:true aast clas in - if rc <> `Ok then anomaly(str"tty loop can't be mixed with the STM protocol"); - if interactive () = `Yes || - (!Flags.async_proofs_mode = Flags.APoff && - !Flags.compilation_mode = Flags.BuildVo) then - let vcs = VCS.backup () in - let print_goals = - verb && match clas with - | VtQuery _, _ -> false - | (VtProofStep _ | VtStm (VtBack _, _) | VtStartProof _), _ -> true - | _ -> not !Flags.coqtop_ui in - try finish ~print_goals () - with e -> - let e = CErrors.push e in - handle_failure e vcs true - -let finish () = finish () - -let get_current_state () = VCS.cur_tip () - let current_proof_depth () = let head = VCS.current_branch () in match VCS.get_branch head with diff --git a/stm/stm.mli b/stm/stm.mli index a31e4289d..30e9629c6 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -30,7 +30,7 @@ exception End_of_input If [newtip] is provided, then the returned state id is guaranteed to be [newtip] *) val add : ontop:Stateid.t -> ?newtip:Stateid.t -> - bool -> (Loc.t * Vernacexpr.vernac_expr) -> + bool -> Vernacexpr.vernac_expr Loc.located -> Stateid.t * [ `NewTip | `Unfocus of Stateid.t ] (* [query at ?report_with cmd] Executes [cmd] at a given state [at], @@ -205,13 +205,6 @@ type state = { val state_of_id : Stateid.t -> [ `Valid of state option | `Expired | `Error of exn ] -(** read-eval-print loop compatible interface ****************************** **) - -(* Adds a new line to the document. It replaces the core of Vernac.interp. - [finish] is called as the last bit of this function if the system - is running interactively (-emacs or coqtop). *) -val interp : bool -> vernac_expr located -> unit - (* Queries for backward compatibility *) val current_proof_depth : unit -> int val get_all_proof_names : unit -> Id.t list diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index ffd0d7805..2b9a04dad 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() = +let load_rcfile sid = if !load_rc then try if !rcfile_specified then if CUnix.file_readable_p !rcfile then - Vernac.load_vernac false !rcfile + Vernac.load_vernac false sid !rcfile else raise (Sys_error ("Cannot read rcfile: "^ !rcfile)) else try @@ -43,8 +43,8 @@ let load_rcfile() = Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version; Envars.home ~warn / "."^rcdefaultname ] in - Vernac.load_vernac false inferedrc - with Not_found -> () + Vernac.load_vernac false sid inferedrc + with Not_found -> sid (* Flags.if_verbose mSGNL (str ("No coqrc or coqrc."^Coq_config.version^ @@ -55,7 +55,8 @@ let load_rcfile() = let () = Feedback.msg_info (str"Load of rcfile failed.") in iraise reraise else - Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading.") + (Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading."); + sid) (* Recursively puts dir in the LoadPath if -nois was not passed *) let add_stdlib_path ~unix_path ~coq_root ~with_ml = diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index 4ff87628c..3b42289ee 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -13,7 +13,7 @@ val set_debug : unit -> unit val set_rcfile : string -> unit val no_load_rc : unit -> unit -val load_rcfile : unit -> unit +val load_rcfile : Stateid.t -> Stateid.t val push_include : string -> Names.DirPath.t -> bool -> unit (** [push_include phys_path log_path implicit] *) diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 2282932d4..17d8f5f49 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -257,7 +257,7 @@ let set_prompt prompt = let parse_to_dot = let rec dot st = match Stream.next st with | Tok.KEYWORD ("."|"...") -> () - | Tok.EOI -> raise End_of_input + | Tok.EOI -> raise Stm.End_of_input | _ -> dot st in Gram.Entry.of_parser "Coqtoplevel.dot" dot @@ -271,13 +271,11 @@ let rec discard_to_dot () = Gram.entry_parse parse_to_dot top_buffer.tokens with | Token.Error _ | CLexer.Error.E _ -> discard_to_dot () - | End_of_input -> raise End_of_input + | Stm.End_of_input -> raise Stm.End_of_input | e when CErrors.noncritical e -> () -let read_sentence input = - try - let (loc, _ as r) = Vernac.parse_sentence input in - CWarnings.set_current_loc loc; r +let read_sentence sid input = + try Stm.parse_sentence sid input with reraise -> let reraise = CErrors.push reraise in discard_to_dot (); @@ -312,25 +310,24 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in is caught and handled (i.e. not re-raised). *) -let do_vernac () = +let do_vernac sid = top_stderr (fnl()); if !print_emacs then top_stderr (str (top_buffer.prompt())); resynch_buffer top_buffer; try let input = (top_buffer.tokens, None) in - Vernac.process_expr top_buffer.tokens (read_sentence input) + Vernac.process_expr sid top_buffer.tokens (read_sentence sid (fst input)) with - | End_of_input | CErrors.Quit -> + | Stm.End_of_input | CErrors.Quit -> top_stderr (fnl ()); raise CErrors.Quit | CErrors.Drop -> (* Last chance *) if Mltop.is_ocaml_top() then raise CErrors.Drop - else Feedback.msg_error (str "There is no ML toplevel.") + else (Feedback.msg_error (str "There is no ML toplevel."); sid) (* Exception printing is done now by the feedback listener. *) (* XXX: We need this hack due to the side effects of the exception printer and the reliance of Stm.define on attaching crutial state to exceptions *) - | any -> ignore (CErrors.(iprint (push any))) - + | any -> ignore (CErrors.(iprint (push any))); sid (** Main coq loop : read vernacular expressions until Drop is entered. Ctrl-C is handled internally as Sys.Break instead of aborting Coq. @@ -349,10 +346,16 @@ let loop_flush_all () = let rec loop () = Sys.catch_break true; if !Flags.print_emacs then Vernacentries.qed_display_script := false; - Flags.coqtop_ui := true; try reset_input_buffer stdin top_buffer; - while true do do_vernac(); loop_flush_all () done + (* Be careful to keep this loop tail-recursive *) + let rec vernac_loop sid = + let nsid = do_vernac sid in + loop_flush_all (); + vernac_loop nsid + (* We recover the current stateid, threading from the caller is + not possible due exceptions. *) + in vernac_loop (Stm.get_current_state ()) with | CErrors.Drop -> () | CErrors.Quit -> exit 0 diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli index 8a34ded6d..66bbf43f6 100644 --- a/toplevel/coqloop.mli +++ b/toplevel/coqloop.mli @@ -31,7 +31,7 @@ val coqloop_feed : Feedback.feedback -> unit (** Parse and execute one vernac command. *) -val do_vernac : unit -> unit +val do_vernac : Stateid.t -> Stateid.t (** Main entry point of Coq: read and execute vernac commands. *) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 4968804fd..c8f3ca1ab 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -175,15 +175,15 @@ let set_include d p implicit = 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 () = - List.iter - (fun (s,b) -> +let load_vernacular sid = + List.fold_left + (fun sid (s,v) -> let s = Loadpath.locate_file s in if !Flags.beautify then - with_option beautify_file (Vernac.load_vernac b) s + with_option beautify_file (Vernac.load_vernac v sid) s else - Vernac.load_vernac b s) - (List.rev !load_vernacular_list) + Vernac.load_vernac v sid s) + 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 @@ -641,8 +641,9 @@ let init_toplevel arglist = load_vernac_obj (); require (); Stm.init (); - load_rcfile(); - load_vernacular (); + let sid = load_rcfile (Stm.get_current_state ()) in + (* XXX: We ignore this for now, but should be threaded to the toplevels *) + let _sid = load_vernacular sid in compile_files (); schedule_vio_checking (); schedule_vio_compilation (); diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index d5ceeaccd..98458a57a 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -13,111 +13,30 @@ open CErrors open Util open Flags open Vernacexpr +open Vernacprop (* The functions in this module may raise (unexplainable!) exceptions. Use the module Coqtoplevel, which catches these exceptions (the exceptions are explained only at the toplevel). *) -let user_error loc s = CErrors.user_err ~loc (str s) - -(* Navigation commands are allowed in a coqtop session but not in a .v file *) - -let rec is_navigation_vernac = function - | VernacResetInitial - | VernacResetName _ - | VernacBacktrack _ - | VernacBackTo _ - | VernacBack _ - | VernacStm _ -> true - | VernacRedirect (_, (_,c)) - | VernacTime (_,c) -> - is_navigation_vernac c (* Time Back* is harmless *) - | c -> is_deep_navigation_vernac c - -and is_deep_navigation_vernac = function - | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c - | _ -> false - -(* NB: Reset is now allowed again as asked by A. Chlipala *) - -let is_reset = function - | VernacResetInitial | VernacResetName _ -> true - | _ -> false - -let checknav_simple loc cmd = +let checknav_simple (loc, cmd) = if is_navigation_vernac cmd && not (is_reset cmd) then - user_error loc "Navigation commands forbidden in files." + CErrors.user_err ~loc (str "Navigation commands forbidden in files.") -let checknav_deep loc ast = +let checknav_deep (loc, ast) = if is_deep_navigation_vernac ast then - user_error loc "Navigation commands forbidden in nested commands." - -(* When doing Load on a file, two behaviors are possible: - - - either the history stack is grown by only one command, - the "Load" itself. This is mandatory for command-counting - interfaces (CoqIDE). - - - either each individual sub-commands in the file is added - to the history stack. This allows commands like Show Script - to work across the loaded file boundary (cf. bug #2820). - - The best of the two could probably be combined someday, - in the meanwhile we use a flag. *) - -let atomic_load = ref true - -let _ = - Goptions.declare_bool_option - { Goptions.optsync = true; - Goptions.optdepr = false; - Goptions.optname = "atomic registration of commands in a Load"; - Goptions.optkey = ["Atomic";"Load"]; - Goptions.optread = (fun () -> !atomic_load); - Goptions.optwrite = ((:=) atomic_load) } + CErrors.user_err ~loc (str "Navigation commands forbidden in nested commands.") let disable_drop = function | Drop -> CErrors.error "Drop is forbidden." | e -> e -(* Opening and closing a channel. Open it twice when verbose: the first - channel is used to read the commands, and the second one to print them. - Note: we could use only one thanks to seek_in, but seeking on and on in - the file we parse seems a bit risky to me. B.B. *) - -let open_file_twice_if verbosely longfname = - let in_chan = open_utf8_file_in longfname in - let verb_ch = - if verbosely then Some (open_utf8_file_in longfname) else None in - let po = Pcoq.Gram.parsable ~file:longfname (Stream.of_channel in_chan) in - (in_chan, longfname, (po, verb_ch)) - -let close_input in_chan (_,verb) = - try - close_in in_chan; - match verb with - | Some verb_ch -> close_in verb_ch - | _ -> () - with e when CErrors.noncritical e -> () - -let verbose_phrase verbch loc = - let loc = Loc.unloc loc in - match verbch with - | Some ch -> - let len = snd loc - fst loc in - let s = Bytes.create len in - seek_in ch (fst loc); - really_input ch s 0 len; - Feedback.msg_notice (str (Bytes.to_string s)) - | None -> () - -exception End_of_input - -let parse_sentence = Flags.with_option Flags.we_are_parsing - (fun (po, verbch) -> - match Pcoq.Gram.entry_parse Pcoq.main_entry po with - | Some (loc,_ as com) -> verbose_phrase verbch loc; com - | None -> raise End_of_input) +(* Echo from a buffer based on position. + XXX: Should move to utility file. *) +let vernac_echo loc in_chan = let open Loc in + let len = loc.ep - loc.bp in + seek_in in_chan loc.bp; + Feedback.msg_notice @@ str @@ really_input_string in_chan len (* vernac parses the given stream, executes interpfun on the syntax tree it * parses, and is verbose on "primitives" commands if verbosely is true *) @@ -184,20 +103,43 @@ let print_cmd_header loc com = Pp.pp_with !Topfmt.std_ft (pp_cmd_header loc com); Format.pp_print_flush !Topfmt.std_ft () -let rec interp_vernac po chan_beautify checknav (loc,com) = +let pr_open_cur_subgoals () = + try Printer.pr_open_subgoals () + with Proof_global.NoCurrentProof -> Pp.str "" + +let rec interp_vernac sid po (loc,com) = let interp = function | VernacLoad (verbosely, fname) -> 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 f - - | v -> Stm.interp (Flags.is_verbose()) (loc,v) + load_vernac verbosely sid f + | v -> + try + let nsid, ntip = Stm.add sid (Flags.is_verbose()) (loc,v) in + + (* Main STM interaction *) + if ntip <> `NewTip then + anomaly (str "vernac.ml: We got an unfocus operation on the toplevel!"); + (* Due to bug #5363 we cannot use observe here as we should, + it otherwise reveals bugs *) + (* Stm.observe nsid; *) + Stm.finish (); + + (* We could use a more refined criteria depending on the + vernac. For now we imitate the old approach. *) + let print_goals = not (!Flags.batch_mode || is_query v) in + + if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ()); + nsid + + with exn when CErrors.noncritical exn -> + ignore(Stm.edit_at sid); + raise exn in try - checknav loc com; - if !beautify then pr_new_syntax po chan_beautify loc (Some com); - (* XXX: This is not 100% correct if called from an IDE context *) + (* 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 interp com @@ -208,26 +150,39 @@ let rec interp_vernac po chan_beautify checknav (loc,com) = else iraise (reraise, info) (* Load a vernac file. CErrors are annotated with file and location *) -and load_vernac verbosely file = +and load_vernac verbosely sid file = let chan_beautify = if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout in - let (in_chan, fname, input) = open_file_twice_if verbosely file in + let in_chan = open_utf8_file_in file in + let in_echo = if verbosely then Some (open_utf8_file_in file) else None in + let in_pa = Pcoq.Gram.parsable ~file (Stream.of_channel in_chan) in + let rsid = ref sid in try (* we go out of the following infinite loop when a End_of_input is * raised, which means that we raised the end of the file being loaded *) while true do - let loc_ast = Flags.silently parse_sentence input in - CWarnings.set_current_loc (fst loc_ast); - Flags.silently (interp_vernac (fst input) chan_beautify checknav_simple) loc_ast; - done + let loc, ast = Stm.parse_sentence !rsid in_pa in + + (* Printing of vernacs *) + if !beautify then pr_new_syntax in_pa chan_beautify loc (Some ast); + Option.iter (vernac_echo loc) in_echo; + + checknav_simple (loc, ast); + let nsid = Flags.silently (interp_vernac !rsid in_pa) (loc, ast) in + rsid := nsid + done; + !rsid with any -> (* whatever the exception *) let (e, info) = CErrors.push any in - close_input in_chan input; (* we must close the file first *) + close_in in_chan; + Option.iter close_in in_echo; match e with - | End_of_input -> + | Stm.End_of_input -> + (* Is this called so comments at EOF are printed? *) if !beautify then - pr_new_syntax (fst input) chan_beautify (Loc.make_loc (max_int,max_int)) None; + pr_new_syntax in_pa chan_beautify (Loc.make_loc (max_int,max_int)) None; if !Flags.beautify_file then close_out chan_beautify; + !rsid | reraise -> if !Flags.beautify_file then close_out chan_beautify; iraise (disable_drop e, info) @@ -239,7 +194,9 @@ and load_vernac verbosely file = of a new state label). An example of state-preserving command is one coming from the query panel of Coqide. *) -let process_expr po loc_ast = interp_vernac po stdout checknav_deep loc_ast +let process_expr sid po loc_ast = + checknav_deep loc_ast; + interp_vernac sid po loc_ast (* XML output hooks *) let (f_xml_start_library, xml_start_library) = Hook.make ~default:ignore () @@ -308,7 +265,7 @@ let compile verbosely f = Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n"); if !Flags.xml_export then Hook.get f_xml_start_library (); let wall_clock1 = Unix.gettimeofday () in - let _ = load_vernac verbosely long_f_dot_v in + let _ = load_vernac verbosely (Stm.get_current_state ()) long_f_dot_v in Stm.join (); let wall_clock2 = Unix.gettimeofday () in check_pending_proofs (); @@ -328,7 +285,7 @@ let compile verbosely f = 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 long_f_dot_v in + let _ = load_vernac verbosely (Stm.get_current_state ()) long_f_dot_v in Stm.finish (); check_pending_proofs (); Stm.snapshot_vio ldir long_f_dot_vio; diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index 0d9f5871a..e75f8f9e8 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -8,30 +8,16 @@ (** Parsing of vernacular. *) -(** Read a vernac command on the specified input (parse only). - Raises [End_of_file] if EOF (or Ctrl-D) is reached. *) - -val parse_sentence : Pcoq.Gram.coq_parsable * in_channel option -> - Loc.t * Vernacexpr.vernac_expr - (** Reads and executes vernac commands from a stream. *) +val process_expr : Stateid.t -> Pcoq.Gram.coq_parsable -> Vernacexpr.vernac_expr Loc.located -> Stateid.t -exception End_of_input +(** [load_vernac echo sid file] Loads [file] on top of [sid], will + echo the commands if [echo] is set. *) +val load_vernac : bool -> Stateid.t -> string -> Stateid.t -val process_expr : Pcoq.Gram.coq_parsable -> Loc.t * Vernacexpr.vernac_expr -> unit +(** Compile a vernac file, (f is assumed without .v suffix) *) +val compile : bool -> string -> unit (** Set XML hooks *) val xml_start_library : (unit -> unit) Hook.t val xml_end_library : (unit -> unit) Hook.t - -(** Load a vernac file, verbosely or not. Errors are annotated with file - and location *) - -val load_vernac : bool -> string -> unit - - -(** Compile a vernac file, verbosely or not (f is assumed without .v suffix) *) - -val compile : bool -> string -> unit - -val is_navigation_vernac : Vernacexpr.vernac_expr -> bool diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 283c095eb..d631fae8a 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -1,3 +1,4 @@ +Vernacprop Lemmas Himsg ExplainErr diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml new file mode 100644 index 000000000..ec78d6012 --- /dev/null +++ b/vernac/vernacprop.ml @@ -0,0 +1,53 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* true + | VernacRedirect (_, (_,c)) + | VernacTime (_,c) -> + is_navigation_vernac c (* Time Back* is harmless *) + | c -> is_deep_navigation_vernac c + +and is_deep_navigation_vernac = function + | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c + | _ -> false + +(* NB: Reset is now allowed again as asked by A. Chlipala *) +let is_reset = function + | VernacResetInitial | VernacResetName _ -> true + | _ -> false + +let is_debug cmd = match cmd with + | VernacSetOption (["Ltac";"Debug"], _) -> true + | _ -> false + +let is_query cmd = match cmd with + | VernacChdir None + | VernacMemOption _ + | VernacPrintOption _ + | VernacCheckMayEval _ + | VernacGlobalCheck _ + | VernacPrint _ + | VernacSearch _ + | VernacLocate _ -> true + | _ -> false + +let is_undo cmd = match cmd with + | VernacUndo _ | VernacUndoTo _ -> true + | _ -> false diff --git a/vernac/vernacprop.mli b/vernac/vernacprop.mli new file mode 100644 index 000000000..c235ecfb5 --- /dev/null +++ b/vernac/vernacprop.mli @@ -0,0 +1,19 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* bool +val is_deep_navigation_vernac : vernac_expr -> bool +val is_reset : vernac_expr -> bool +val is_query : vernac_expr -> bool +val is_debug : vernac_expr -> bool +val is_undo : vernac_expr -> bool -- cgit v1.2.3