diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/asyncTaskQueue.ml | 19 | ||||
| -rw-r--r-- | stm/asyncTaskQueue.mli | 9 | ||||
| -rw-r--r-- | stm/coqworkmgrApi.ml | 25 | ||||
| -rw-r--r-- | stm/coqworkmgrApi.mli | 8 | ||||
| -rw-r--r-- | stm/proofBlockDelimiter.ml | 25 | ||||
| -rw-r--r-- | stm/proofworkertop.ml | 2 | ||||
| -rw-r--r-- | stm/queryworkertop.ml | 2 | ||||
| -rw-r--r-- | stm/spawned.ml | 6 | ||||
| -rw-r--r-- | stm/spawned.mli | 2 | ||||
| -rw-r--r-- | stm/stm.ml | 437 | ||||
| -rw-r--r-- | stm/stm.mli | 62 | ||||
| -rw-r--r-- | stm/tacworkertop.ml | 2 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 100 | ||||
| -rw-r--r-- | stm/vernac_classifier.mli | 2 | ||||
| -rw-r--r-- | stm/workerLoop.ml | 10 | ||||
| -rw-r--r-- | stm/workerLoop.mli | 5 |
16 files changed, 455 insertions, 261 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 4662c55432..26aef53552 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -10,11 +10,11 @@ open CErrors open Pp open Util -let stm_pr_err pp = Format.eprintf "%s] @[%a@]\n%!" (System.process_id ()) Pp.pp_with pp - +let stm_pr_err pp = Format.eprintf "%s] @[%a@]\n%!" (Spawned.process_id ()) Pp.pp_with pp let stm_prerr_endline s = if !Flags.debug then begin stm_pr_err (str s) end else () type cancel_switch = bool ref +let async_proofs_flags_for_workers = ref [] module type Task = sig @@ -58,7 +58,7 @@ module Make(T : Task) () = struct type request = Request of T.request type more_data = - | MoreDataUnivLevel of Univ.Level.t list + | MoreDataUnivLevel of Universes.universe_id list let slave_respond (Request r) = let res = T.perform r in @@ -117,12 +117,12 @@ module Make(T : Task) () = struct let name = Printf.sprintf "%s:%d" !T.name id in let proc, ic, oc = let rec set_slave_opt = function - | [] -> !Flags.async_proofs_flags_for_workers @ + | [] -> !async_proofs_flags_for_workers @ ["-toploop"; !T.name^"top"; "-worker-id"; name; "-async-proofs-worker-priority"; - Flags.string_of_priority !Flags.async_proofs_worker_priority] - | ("-ideslave"|"-emacs"|"-batch")::tl -> set_slave_opt tl + CoqworkmgrApi.(string_of_priority !WorkerLoop.async_proofs_worker_priority)] + | ("-ideslave"|"-emacs"|"-emacs-U"|"-batch")::tl -> set_slave_opt tl | ("-async-proofs" |"-toploop" |"-vio2vo" |"-load-vernac-source" |"-l" |"-load-vernac-source-verbose" |"-lv" |"-compile" |"-compile-verbose" @@ -169,8 +169,7 @@ module Make(T : Task) () = struct | Unix.WSIGNALED sno -> Printf.sprintf "signalled(%d)" sno | Unix.WSTOPPED sno -> Printf.sprintf "stopped(%d)" sno) in let more_univs n = - CList.init n (fun _ -> - Universes.new_univ_level (Global.current_dirpath ())) in + CList.init n (fun _ -> Universes.new_univ_id ()) in let rec kill_if () = if not (Worker.is_alive proc) then () @@ -296,7 +295,7 @@ module Make(T : Task) () = struct let slave_handshake () = Pool.worker_handshake (Option.get !slave_ic) (Option.get !slave_oc) - let pp_pid pp = Pp.(str (System.process_id () ^ " ") ++ pp) + let pp_pid pp = Pp.(str (Spawned.process_id () ^ " ") ++ pp) let debug_with_pid = Feedback.(function | { contents = Message(Debug, loc, pp) } as fb -> @@ -309,7 +308,7 @@ module Make(T : Task) () = struct Marshal.to_channel oc (RespFeedback (debug_with_pid fb)) []; flush oc in ignore (Feedback.add_feeder (fun x -> slave_feeder (Option.get !slave_oc) x)); (* We ask master to allocate universe identifiers *) - Universes.set_remote_new_univ_level (bufferize (fun () -> + Universes.set_remote_new_univ_id (bufferize (fun () -> marshal_response (Option.get !slave_oc) RespGetCounterNewUnivLevel; match unmarshal_more_data (Option.get !slave_ic) with | MoreDataUnivLevel l -> l)); diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli index ccd643deba..706d36e1d5 100644 --- a/stm/asyncTaskQueue.mli +++ b/stm/asyncTaskQueue.mli @@ -6,6 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Default flags for workers *) +val async_proofs_flags_for_workers : string list ref + (** This file provides an API for defining and managing a queue of tasks to be done by external workers. @@ -68,7 +71,7 @@ module type Task = sig (** Extra arguments of the task kind, for -toploop *) val extra_env : unit -> string array - (** {5} Master API, it is run by the master, on a thread *) + (** {5 Master API, it is run by the master, on a thread} *) (** [request_of_task status t] takes the [status] of the worker and a task [t] and creates the corresponding [Some request] to be @@ -113,8 +116,8 @@ module type Task = sig (** [forward_feedback fb] sends fb to all the workers. *) val forward_feedback : Feedback.feedback -> unit - (** {5} Worker API, it is run by worker, on a different fresh - process *) + (** {5 Worker API, it is run by worker, on a different fresh + process} *) (** [perform in] synchronously processes a request [in] *) val perform : request -> response diff --git a/stm/coqworkmgrApi.ml b/stm/coqworkmgrApi.ml index 6d6a198c5f..14fd97a6d5 100644 --- a/stm/coqworkmgrApi.ml +++ b/stm/coqworkmgrApi.ml @@ -8,8 +8,15 @@ let debug = false +type priority = Low | High +let string_of_priority = function Low -> "low" | High -> "high" +let priority_of_string = function + | "low" -> Low + | "high" -> High + | _ -> raise (Invalid_argument "priority_of_string") + type request = - | Hello of Flags.priority + | Hello of priority | Get of int | TryGet of int | GiveBack of int @@ -36,8 +43,8 @@ let positive_int_of_string n = let parse_request s = if debug then Printf.eprintf "parsing '%s'\n" s; match Str.split (Str.regexp " ") (strip_r s) with - | [ "HELLO"; "LOW" ] -> Hello Flags.Low - | [ "HELLO"; "HIGH" ] -> Hello Flags.High + | [ "HELLO"; "LOW" ] -> Hello Low + | [ "HELLO"; "HIGH" ] -> Hello High | [ "GET"; n ] -> Get (positive_int_of_string n) | [ "TRYGET"; n ] -> TryGet (positive_int_of_string n) | [ "GIVEBACK"; n ] -> GiveBack (positive_int_of_string n) @@ -57,8 +64,8 @@ let parse_response s = | _ -> raise ParseError let print_request = function - | Hello Flags.Low -> "HELLO LOW\n" - | Hello Flags.High -> "HELLO HIGH\n" + | Hello Low -> "HELLO LOW\n" + | Hello High -> "HELLO HIGH\n" | Get n -> Printf.sprintf "GET %d\n" n | TryGet n -> Printf.sprintf "TRYGET %d\n" n | GiveBack n -> Printf.sprintf "GIVEBACK %d\n" n @@ -106,8 +113,7 @@ let with_manager f g = let get n = with_manager - (fun () -> - min n (min !Flags.async_proofs_n_workers !Flags.async_proofs_n_tacworkers)) + (fun () -> n) (fun cin cout -> output_string cout (print_request (Get n)); flush cout; @@ -118,10 +124,7 @@ let get n = let tryget n = with_manager - (fun () -> - Some - (min n - (min !Flags.async_proofs_n_workers !Flags.async_proofs_n_tacworkers))) + (fun () -> Some n) (fun cin cout -> output_string cout (print_request (TryGet n)); flush cout; diff --git a/stm/coqworkmgrApi.mli b/stm/coqworkmgrApi.mli index 70d4173ae8..953903810e 100644 --- a/stm/coqworkmgrApi.mli +++ b/stm/coqworkmgrApi.mli @@ -8,9 +8,13 @@ (* High level api for clients of the service (like coqtop) *) +type priority = Low | High +val string_of_priority : priority -> string +val priority_of_string : string -> priority + (* Connects to a work manager if any. If no worker manager, then -async-proofs-j and -async-proofs-tac-j are used *) -val init : Flags.priority -> unit +val init : priority -> unit (* blocking *) val get : int -> int @@ -21,7 +25,7 @@ val giveback : int -> unit (* Low level *) type request = - | Hello of Flags.priority + | Hello of priority | Get of int | TryGet of int | GiveBack of int diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index 77642946cd..bebc4d5d5f 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -23,8 +23,8 @@ val crawl : val unit_val : Stm.DynBlockData.t val of_bullet_val : Vernacexpr.bullet -> Stm.DynBlockData.t val to_bullet_val : Stm.DynBlockData.t -> Vernacexpr.bullet -val of_vernac_expr_val : Vernacexpr.vernac_expr -> Stm.DynBlockData.t -val to_vernac_expr_val : Stm.DynBlockData.t -> Vernacexpr.vernac_expr +val of_vernac_control_val : Vernacexpr.vernac_control -> Stm.DynBlockData.t +val to_vernac_control_val : Stm.DynBlockData.t -> Vernacexpr.vernac_control end = struct @@ -32,7 +32,7 @@ let unit_tag = DynBlockData.create "unit" let unit_val = DynBlockData.Easy.inj () unit_tag let of_bullet_val, to_bullet_val = DynBlockData.Easy.make_dyn "bullet" -let of_vernac_expr_val, to_vernac_expr_val = DynBlockData.Easy.make_dyn "vernac_expr" +let of_vernac_control_val, to_vernac_control_val = DynBlockData.Easy.make_dyn "vernac_control" let simple_goal sigma g gs = let open Evar in @@ -74,14 +74,16 @@ include Util (* ****************** - foo - bar - baz *********************************** *) let static_bullet ({ entry_point; prev_node } as view) = - match entry_point.ast with + assert (not (Vernacprop.has_Fail entry_point.ast)); + match Vernacprop.under_control entry_point.ast with | Vernacexpr.VernacBullet b -> let base = entry_point.indentation in let last_tac = prev_node entry_point in crawl view ~init:last_tac (fun prev node -> if node.indentation < base then `Stop else if node.indentation > base then `Cont node else - match node.ast with + if Vernacprop.has_Fail node.ast then `Stop + else match Vernacprop.under_control node.ast with | Vernacexpr.VernacBullet b' when b = b' -> `Found { block_stop = entry_point.id; block_start = prev.id; dynamic_switch = node.id; carry_on_data = of_bullet_val b } @@ -94,7 +96,7 @@ let dynamic_bullet doc { dynamic_switch = id; carry_on_data = b } = `ValidBlock { base_state = id; goals_to_admit = focused; - recovery_command = Some (Vernacexpr.VernacBullet (to_bullet_val b)) + recovery_command = Some (Vernacexpr.VernacExpr([], Vernacexpr.VernacBullet (to_bullet_val b))) } | `Not -> `Leaks @@ -104,9 +106,10 @@ let () = register_proof_block_delimiter (* ******************** { block } ***************************************** *) let static_curly_brace ({ entry_point; prev_node } as view) = - assert(entry_point.ast = Vernacexpr.VernacEndSubproof); + assert(Vernacprop.under_control entry_point.ast = Vernacexpr.VernacEndSubproof); crawl view (fun (nesting,prev) node -> - match node.ast with + if Vernacprop.has_Fail node.ast then `Cont (nesting,node) + else match Vernacprop.under_control node.ast with | Vernacexpr.VernacSubproof _ when nesting = 0 -> `Found { block_stop = entry_point.id; block_start = prev.id; dynamic_switch = node.id; carry_on_data = unit_val } @@ -122,7 +125,7 @@ let dynamic_curly_brace doc { dynamic_switch = id } = `ValidBlock { base_state = id; goals_to_admit = focused; - recovery_command = Some Vernacexpr.VernacEndSubproof + recovery_command = Some (Vernacexpr.VernacExpr ([], Vernacexpr.VernacEndSubproof)) } | `Not -> `Leaks @@ -164,7 +167,7 @@ let static_indent ({ entry_point; prev_node } as view) = else `Found { block_stop = entry_point.id; block_start = node.id; dynamic_switch = node.id; - carry_on_data = of_vernac_expr_val entry_point.ast } + carry_on_data = of_vernac_control_val entry_point.ast } ) last_tac let dynamic_indent doc { dynamic_switch = id; carry_on_data = e } = @@ -176,7 +179,7 @@ let dynamic_indent doc { dynamic_switch = id; carry_on_data = e } = `ValidBlock { base_state = id; goals_to_admit = but_last; - recovery_command = Some (to_vernac_expr_val e); + recovery_command = Some (to_vernac_control_val e); } | `Not -> `Leaks diff --git a/stm/proofworkertop.ml b/stm/proofworkertop.ml index 10b42f7e91..81637f143d 100644 --- a/stm/proofworkertop.ml +++ b/stm/proofworkertop.ml @@ -10,5 +10,5 @@ module W = AsyncTaskQueue.MakeWorker(Stm.ProofTask) () let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout -let () = Coqtop.toploop_run := (fun _ -> W.main_loop ()) +let () = Coqtop.toploop_run := (fun _ ~state:_ -> W.main_loop ()) diff --git a/stm/queryworkertop.ml b/stm/queryworkertop.ml index a1fe50c63e..7862f2f447 100644 --- a/stm/queryworkertop.ml +++ b/stm/queryworkertop.ml @@ -10,5 +10,5 @@ module W = AsyncTaskQueue.MakeWorker(Stm.QueryTask) () let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout -let () = Coqtop.toploop_run := (fun _ -> W.main_loop ()) +let () = Coqtop.toploop_run := (fun _ ~state:_ -> W.main_loop ()) diff --git a/stm/spawned.ml b/stm/spawned.ml index 6ab096abf9..fb5708f3a3 100644 --- a/stm/spawned.ml +++ b/stm/spawned.ml @@ -73,3 +73,9 @@ let get_channels () = Printf.eprintf "Fatal error: ideslave communication channels not set.\n"; exit 1 | Some(ic, oc) -> ic, oc + +let process_id () = + Printf.sprintf "%d:%s:%d" (Unix.getpid ()) + (if Flags.async_proofs_is_worker () then !Flags.async_proofs_worker_id + else "master") + (Thread.id (Thread.self ())) diff --git a/stm/spawned.mli b/stm/spawned.mli index c3cf4d67b0..7f463c6a6e 100644 --- a/stm/spawned.mli +++ b/stm/spawned.mli @@ -20,3 +20,5 @@ val init_channels : unit -> unit (* Once initialized, these are the channels to talk with our master *) val get_channels : unit -> CThread.thread_ic * out_channel +(** {6 Name of current process.} *) +val process_id : unit -> string diff --git a/stm/stm.ml b/stm/stm.ml index ab44cc98b2..92587b8ea5 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -8,21 +8,70 @@ (* enable in case of stm problems *) (* let stm_debug () = !Flags.debug *) -let stm_debug () = !Flags.stm_debug +let stm_debug = ref false -let stm_pr_err s = Format.eprintf "%s] %s\n%!" (System.process_id ()) s -let stm_pp_err pp = Format.eprintf "%s] @[%a@]\n%!" (System.process_id ()) Pp.pp_with pp +let stm_pr_err s = Format.eprintf "%s] %s\n%!" (Spawned.process_id ()) s +let stm_pp_err pp = Format.eprintf "%s] @[%a@]\n%!" (Spawned.process_id ()) Pp.pp_with pp -let stm_prerr_endline s = if stm_debug () then begin stm_pr_err (s ()) end else () -let stm_pperr_endline s = if stm_debug () then begin stm_pp_err (s ()) end else () +let stm_prerr_endline s = if !stm_debug then begin stm_pr_err (s ()) end else () +let stm_pperr_endline s = if !stm_debug then begin stm_pp_err (s ()) end else () let stm_prerr_debug s = if !Flags.debug then begin stm_pr_err (s ()) end else () open Pp open CErrors +open Names open Feedback open Vernacexpr +module AsyncOpts = struct + + type cache = Force + type async_proofs = APoff | APonLazy | APon + type tac_error_filter = [ `None | `Only of string list | `All ] + + type stm_opt = { + async_proofs_n_workers : int; + async_proofs_n_tacworkers : int; + + async_proofs_cache : cache option; + async_proofs_mode : async_proofs; + + async_proofs_private_flags : string option; + async_proofs_full : bool; + async_proofs_never_reopen_branch : bool; + + async_proofs_tac_error_resilience : tac_error_filter; + async_proofs_cmd_error_resilience : bool; + async_proofs_delegation_threshold : float; + } + + let default_opts = { + async_proofs_n_workers = 1; + async_proofs_n_tacworkers = 2; + + async_proofs_cache = None; + + async_proofs_mode = APoff; + + async_proofs_private_flags = None; + async_proofs_full = false; + async_proofs_never_reopen_branch = false; + + async_proofs_tac_error_resilience = `Only [ "curly" ]; + async_proofs_cmd_error_resilience = true; + async_proofs_delegation_threshold = 0.03; + } + + let cur_opt = ref default_opts +end + +open AsyncOpts + +let async_proofs_is_master opt = + opt.async_proofs_mode = APon && + !Flags.async_proofs_worker_id = "master" + (* Protect against state changes *) let stm_purify f x = let st = Vernacstate.freeze_interp_state `No in @@ -36,8 +85,7 @@ let stm_purify f x = Exninfo.iraise e let execution_error ?loc state_id msg = - feedback ~id:state_id - (Message (Error, loc, msg)) + feedback ~id:state_id (Message (Error, loc, msg)) module Hooks = struct @@ -82,7 +130,7 @@ type aast = { loc : Loc.t option; indentation : int; strlen : int; - mutable expr : vernac_expr; (* mutable: Proof using hinted by aux file *) + mutable expr : vernac_control; (* mutable: Proof using hinted by aux file *) } let pr_ast { expr; indentation } = Pp.(int indentation ++ str " " ++ Ppvernac.pr_vernac expr) @@ -90,14 +138,14 @@ let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml. (* Commands piercing opaque *) let may_pierce_opaque = function - | { expr = VernacPrint _ } -> true - | { expr = VernacExtend (("Extraction",_), _) } -> true - | { expr = VernacExtend (("SeparateExtraction",_), _) } -> true - | { expr = VernacExtend (("ExtractionLibrary",_), _) } -> true - | { expr = VernacExtend (("RecursiveExtractionLibrary",_), _) } -> true - | { expr = VernacExtend (("ExtractionConstant",_), _) } -> true - | { expr = VernacExtend (("ExtractionInlinedConstant",_), _) } -> true - | { expr = VernacExtend (("ExtractionInductive",_), _) } -> true + | VernacPrint _ + | VernacExtend (("Extraction",_), _) + | VernacExtend (("SeparateExtraction",_), _) + | VernacExtend (("ExtractionLibrary",_), _) + | VernacExtend (("RecursiveExtractionLibrary",_), _) + | VernacExtend (("ExtractionConstant",_), _) + | VernacExtend (("ExtractionInlinedConstant",_), _) + | VernacExtend (("ExtractionInductive",_), _) -> true | _ -> false let update_global_env () = @@ -158,9 +206,10 @@ let mkTransCmd cast cids ceff cqueue = Cmd { ctac = false; cast; cblock = None; cqueue; cids; ceff } (* Parts of the system state that are morally part of the proof state *) -let summary_pstate = [ Evarutil.meta_counter_summary_name; - Evd.evar_counter_summary_name; - "program-tcc-table" ] +let summary_pstate = Evarutil.meta_counter_summary_tag, + Evd.evar_counter_summary_tag, + Obligations.program_tcc_summary_tag + type cached_state = | Empty | Error of Exninfo.iexn @@ -352,10 +401,10 @@ end = struct (* {{{ *) In case you are hitting the race enable stm_debug. *) - if stm_debug () then Flags.we_are_parsing := false; + if !stm_debug then Flags.we_are_parsing := false; let fname = - "stm_" ^ Str.global_replace (Str.regexp " ") "_" (System.process_id ()) in + "stm_" ^ Str.global_replace (Str.regexp " ") "_" (Spawned.process_id ()) in let string_of_transaction = function | Cmd { cast = t } | Fork (t, _,_,_) -> (try Pp.string_of_ppcmds (pr_ast t) with _ -> "ERR") @@ -515,12 +564,10 @@ end = struct (* {{{ *) vcs := rewrite_merge !vcs id ~ours ~theirs:Noop ~at branch let reachable id = reachable !vcs id let mk_branch_name { expr = x } = Branch.make - (let rec aux x = match x with - | VernacDefinition (_,((_,i),_),_) -> Names.Id.to_string i - | VernacStartTheoremProof (_,[Some ((_,i),_),_]) -> Names.Id.to_string i - | VernacTime (_, e) - | VernacTimeout (_, e) -> aux e - | _ -> "branch" in aux x) + (match Vernacprop.under_control x with + | VernacDefinition (_,((_, Name i),_),_) -> Id.to_string i + | VernacStartTheoremProof (_,[((_,i),_),_]) -> Id.to_string i + | _ -> "branch") let edit_branch = Branch.make "edit" let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind let get_info id = @@ -529,7 +576,7 @@ end = struct (* {{{ *) | None -> raise Vcs_aux.Expired let set_state id s = (get_info id).state <- s; - if Flags.async_proofs_is_master () then Hooks.(call state_ready id) + if async_proofs_is_master !cur_opt then Hooks.(call state_ready id) let get_state id = (get_info id).state let reached id = let info = get_info id in @@ -762,15 +809,21 @@ end = struct (* {{{ *) let fix_exn_ref = ref (fun x -> x) type proof_part = - Proof_global.state * Summary.frozen_bits (* only meta counters *) + Proof_global.t * + int * (* Evarutil.meta_counter_summary_tag *) + int * (* Evd.evar_counter_summary_tag *) + Obligations.program_info Names.Id.Map.t (* Obligations.program_tcc_summary_tag *) type partial_state = [ `Full of Vernacstate.t | `ProofOnly of Stateid.t * proof_part ] let proof_part_of_frozen { Vernacstate.proof; system } = + let st = States.summary_of_state system in proof, - Summary.project_summary (States.summary_of_state system) summary_pstate + Summary.project_from_summary st Util.(pi1 summary_pstate), + Summary.project_from_summary st Util.(pi2 summary_pstate), + Summary.project_from_summary st Util.(pi3 summary_pstate) let freeze marshallable id = VCS.set_state id (Valid (Vernacstate.freeze_interp_state marshallable)) @@ -830,16 +883,21 @@ end = struct (* {{{ *) else s with VCS.Expired -> s in VCS.set_state id (Valid s) - | `ProofOnly(ontop,(pstate,counters)) -> + | `ProofOnly(ontop,(pstate,c1,c2,c3)) -> if is_cached_and_valid ontop then let s = get_cached ontop in let s = { s with proof = Proof_global.copy_terminators ~src:s.proof ~tgt:pstate } in let s = { s with system = States.replace_summary s.system - (Summary.surgery_summary - (States.summary_of_state s.system) - counters) } in + begin + let st = States.summary_of_state s.system in + let st = Summary.modify_summary st Util.(pi1 summary_pstate) c1 in + let st = Summary.modify_summary st Util.(pi2 summary_pstate) c2 in + let st = Summary.modify_summary st Util.(pi3 summary_pstate) c3 in + st + end + } in VCS.set_state id (Valid s) with VCS.Expired -> () @@ -854,10 +912,10 @@ end = struct (* {{{ *) let same_env { Vernacstate.system = s1 } { Vernacstate.system = s2 } = let s1 = States.summary_of_state s1 in - let e1 = Summary.project_summary s1 [Global.global_env_summary_name] in + let e1 = Summary.project_from_summary s1 Global.global_env_summary_tag in let s2 = States.summary_of_state s2 in - let e2 = Summary.project_summary s2 [Global.global_env_summary_name] in - Summary.pointer_equal e1 e2 + let e2 = Summary.project_from_summary s2 Global.global_env_summary_tag in + e1 == e2 let define ?safe_id ?(redefine=false) ?(cache=`No) ?(feedback_processed=true) f id @@ -943,7 +1001,7 @@ let indent_script_item ((ng1,ngl1),nl,beginend,ppl) (cmd,ng) = in (* Some special handling of bullets and { }, to get a nicer display *) let pred n = max 0 (n-1) in - let ind, nl, new_beginend = match cmd with + let ind, nl, new_beginend = match Vernacprop.under_control cmd with | VernacSubproof _ -> pred ind, nl, (pred ind)::beginend | VernacEndSubproof -> List.hd beginend, false, List.tl beginend | VernacBullet _ -> pred ind, nl, beginend @@ -1008,25 +1066,26 @@ let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacstate.t (* We need to check if a command should be filtered from * vernac_entries, as it cannot handle it. This should go away in * future refactorings. - *) - let rec is_filtered_command = function - | VernacResetName _ | VernacResetInitial | VernacBack _ - | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _ - | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true - | VernacTime (_,e) | VernacTimeout (_,e) | VernacRedirect (_,(_,e)) -> is_filtered_command e - | _ -> false + *) + let is_filtered_command = function + | VernacResetName _ | VernacResetInitial | VernacBack _ + | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _ + | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true + | _ -> false in - let aux_interp st cmd = - if is_filtered_command cmd then - (stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr); st) - else match cmd with - | VernacShow ShowScript -> ShowScript.show_script (); st - | expr -> - stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr); - try Vernacentries.interp ?verbosely:(Some verbose) ?proof ~st (Loc.tag ?loc expr) - with e -> - let e = CErrors.push e in - Exninfo.iraise Hooks.(call_process_error_once e) + let aux_interp st expr = + let cmd = Vernacprop.under_control expr in + if is_filtered_command cmd then + (stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr); st) + else + match cmd with + | VernacShow ShowScript -> ShowScript.show_script (); st (** XX we are ignoring control here *) + | _ -> + stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr); + try Vernacentries.interp ?verbosely:(Some verbose) ?proof ~st (Loc.tag ?loc expr) + with e -> + let e = CErrors.push e in + Exninfo.iraise Hooks.(call_process_error_once e) in aux_interp st expr (****************************** CRUFT *****************************************) @@ -1042,7 +1101,7 @@ module Backtrack : sig val branches_of : Stateid.t -> backup (* Returns the state that the command should backtract to *) - val undo_vernac_classifier : vernac_expr -> Stateid.t * vernac_when + val undo_vernac_classifier : vernac_control -> Stateid.t * vernac_when end = struct (* {{{ *) @@ -1090,7 +1149,11 @@ end = struct (* {{{ *) match VCS.visit id with | { step = `Fork ((_,_,_,l),_) } -> l, false,0 | { step = `Cmd { cids = l; ctac } } -> l, ctac,0 - | { step = `Alias (_,{ expr = VernacUndo n}) } -> [], false, n + | { step = `Alias (_,{ expr }) } when not (Vernacprop.has_Fail expr) -> + begin match Vernacprop.under_control expr with + | VernacUndo n -> [], false, n + | _ -> [],false,0 + end | _ -> [],false,0 in match f acc (id, vcs, ids, tactic, undo) with | `Stop x -> x @@ -1105,10 +1168,10 @@ end = struct (* {{{ *) " the \"-async-proofs-cache force\" option to Coq.")) let undo_vernac_classifier v = - if VCS.is_interactive () = `No && !Flags.async_proofs_cache <> Some Flags.Force + if VCS.is_interactive () = `No && !cur_opt.async_proofs_cache <> Some Force then undo_costly_in_batch_mode v; try - match v with + match Vernacprop.under_control v with | VernacResetInitial -> Stateid.initial, VtNow | VernacResetName (_,name) -> @@ -1201,7 +1264,7 @@ let _ = CErrors.register_handler (function type document_node = { indentation : int; - ast : Vernacexpr.vernac_expr; + ast : Vernacexpr.vernac_control; id : Stateid.t; } @@ -1216,7 +1279,7 @@ type static_block_detection = type recovery_action = { base_state : Stateid.t; goals_to_admit : Goal.goal list; - recovery_command : Vernacexpr.vernac_expr option; + recovery_command : Vernacexpr.vernac_control option; } type dynamic_block_error_recovery = @@ -1241,7 +1304,7 @@ let prev_node { id } = let cur_node id = mk_doc_node id (VCS.visit id) let is_block_name_enabled name = - match !Flags.async_proofs_tac_error_resilience with + match !cur_opt.async_proofs_tac_error_resilience with | `None -> false | `All -> true | `Only l -> List.mem name l @@ -1249,7 +1312,7 @@ let is_block_name_enabled name = let detect_proof_block id name = let name = match name with None -> "indent" | Some x -> x in if is_block_name_enabled name && - (Flags.async_proofs_is_master () || Flags.async_proofs_is_worker ()) + (async_proofs_is_master !cur_opt || Flags.async_proofs_is_worker ()) then ( match cur_node id with | None -> () @@ -1351,7 +1414,7 @@ end = struct (* {{{ *) let task_match age t = match age, t with | Fresh, BuildProof { t_states } -> - not !Flags.async_proofs_full || + not !cur_opt.async_proofs_full || List.exists (fun x -> CList.mem_f Stateid.equal x !perspective) t_states | Old my_states, States l -> List.for_all (fun x -> CList.mem_f Stateid.equal x my_states) l @@ -1388,7 +1451,7 @@ end = struct (* {{{ *) feedback (InProgress ~-1); t_assign (`Val pl); record_pb_time ?loc:t_loc t_name time; - if !Flags.async_proofs_full || t_drop + if !cur_opt.async_proofs_full || t_drop then `Stay(t_states,[States t_states]) else `End | Fresh, BuildProof { t_assign; t_loc; t_name; t_states }, @@ -1453,7 +1516,7 @@ end = struct (* {{{ *) stm_vernac_interp stop ~proof:(pobject, terminator) st { verbose = false; loc; indentation = 0; strlen = 0; - expr = (VernacEndProof (Proved (Opaque,None))) }) in + expr = VernacExpr ([], VernacEndProof (Proved (Opaque,None))) }) in ignore(Future.join checked_proof); end; (* STATE: Restore the state XXX: handle exn *) @@ -1515,12 +1578,13 @@ end = struct (* {{{ *) | ReqStates sl -> RespStates (perform_states sl) let on_marshal_error s = function - | States _ -> msg_error(Pp.strbrk("Marshalling error: "^s^". "^ - "The system state could not be sent to the master process.")) + | States _ -> + msg_warning Pp.(strbrk("Marshalling error: "^s^". "^ + "The system state could not be sent to the master process.")) | BuildProof { t_exn_info; t_stop; t_assign; t_loc; t_drop = drop_pt } -> - msg_error(Pp.strbrk("Marshalling error: "^s^". "^ - "The system state could not be sent to the worker process. "^ - "Falling back to local, lazy, evaluation.")); + msg_warning Pp.(strbrk("Marshalling error: "^s^". "^ + "The system state could not be sent to the worker process. "^ + "Falling back to local, lazy, evaluation.")); t_assign(`Comp(build_proof_here ?loc:t_loc ~drop_pt t_exn_info t_stop)); feedback (InProgress ~-1) @@ -1562,8 +1626,8 @@ end = struct (* {{{ *) let queue = ref None let init () = - if Flags.async_proofs_is_master () then - queue := Some (TaskQueue.create !Flags.async_proofs_n_workers) + if async_proofs_is_master !cur_opt then + queue := Some (TaskQueue.create !cur_opt.async_proofs_n_workers) else queue := Some (TaskQueue.create 0) @@ -1601,14 +1665,14 @@ end = struct (* {{{ *) let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp stop ~proof st { verbose = false; loc; indentation = 0; strlen = 0; - expr = (VernacEndProof (Proved (Opaque,None))) }); + expr = VernacExpr ([], VernacEndProof (Proved (Opaque,None))) }); `OK proof end with e -> let (e, info) = CErrors.push e in (try match Stateid.get info with | None -> - msg_error Pp.( + msg_warning Pp.( str"File " ++ str name ++ str ": proof of " ++ str r_name ++ spc () ++ iprint (e, info)) | Some (_, cur) -> @@ -1618,17 +1682,17 @@ end = struct (* {{{ *) | { step = `Qed ( { qast = { loc } }, _) } | { step = `Sideff (ReplayCommand { loc }, _) } -> let start, stop = Option.cata Loc.unloc (0,0) loc in - msg_error Pp.( + msg_warning Pp.( str"File " ++ str name ++ str ": proof of " ++ str r_name ++ str ": chars " ++ int start ++ str "-" ++ int stop ++ spc () ++ iprint (e, info)) | _ -> - msg_error Pp.( + msg_warning Pp.( str"File " ++ str name ++ str ": proof of " ++ str r_name ++ spc () ++ iprint (e, info)) with e -> - msg_error Pp.(str"unable to print error message: " ++ - str (Printexc.to_string e))); + msg_warning Pp.(str"unable to print error message: " ++ + str (Printexc.to_string e))); if drop then `ERROR_ADMITTED else `ERROR let finish_task name (u,cst,_) d p l i = @@ -1890,15 +1954,16 @@ end = struct (* {{{ *) let vernac_interp ~solve ~abstract ~cancel_switch nworkers safe_id id { indentation; verbose; loc; expr = e; strlen } = - let e, time, fail = - let rec find ~time ~fail = function - | VernacTime (_,e) -> find ~time:true ~fail e - | VernacRedirect (_,(_,e)) -> find ~time ~fail e - | VernacFail e -> find ~time ~fail:true e - | e -> e, time, fail in find ~time:false ~fail:false e in + let e, time, batch, fail = + let rec find ~time ~batch ~fail = function + | VernacTime (batch,(_,e)) -> find ~time:true ~batch ~fail e + | VernacRedirect (_,(_,e)) -> find ~time ~batch ~fail e + | VernacFail e -> find ~time ~batch ~fail:true e + | e -> e, time, batch, fail in + find ~time:false ~batch:false ~fail:false e in let st = Vernacstate.freeze_interp_state `No in Vernacentries.with_fail st fail (fun () -> - (if time then System.with_time !Flags.time else (fun x -> x)) (fun () -> + (if time then System.with_time ~batch else (fun x -> x)) (fun () -> ignore(TaskQueue.with_n_workers nworkers (fun queue -> Proof_global.with_current_proof (fun _ p -> let goals, _, _, _, _ = Proof.proof p in @@ -2028,7 +2093,7 @@ end = struct (* {{{ *) QueryTask.({ t_where = prev; t_for = id; t_what = q }) ~cancel_switch let init () = queue := Some (TaskQueue.create - (if !Flags.async_proofs_full then 1 else 0)) + (if !cur_opt.async_proofs_full then 1 else 0)) end (* }}} *) @@ -2040,20 +2105,17 @@ and Reach : sig end = struct (* {{{ *) -let pstate = summary_pstate - let async_policy () = - let open Flags in - if is_universe_polymorphism () then false + if Flags.is_universe_polymorphism () then false else if VCS.is_interactive () = `Yes then - (async_proofs_is_master () || !async_proofs_mode = APonLazy) + (async_proofs_is_master !cur_opt || !cur_opt.async_proofs_mode = APonLazy) else - (VCS.is_vio_doc () || !async_proofs_mode <> APoff) + (VCS.is_vio_doc () || !cur_opt.async_proofs_mode <> APoff) let delegate name = - get_hint_bp_time name >= !Flags.async_proofs_delegation_threshold + get_hint_bp_time name >= !cur_opt.async_proofs_delegation_threshold || VCS.is_vio_doc () - || !Flags.async_proofs_full + || !cur_opt.async_proofs_full let warn_deprecated_nested_proofs = CWarnings.create ~name:"deprecated-nested-proofs" ~category:"deprecated" @@ -2068,30 +2130,43 @@ let collect_proof keep cur hd brkind id = | [] -> no_name | id :: _ -> Names.Id.to_string id in let loc = (snd cur).loc in - let rec is_defined_expr = function + let is_defined_expr = function | VernacEndProof (Proved (Transparent,_)) -> true - | VernacTime (_, e) -> is_defined_expr e - | VernacRedirect (_, (_, e)) -> is_defined_expr e - | VernacTimeout (_, e) -> is_defined_expr e | _ -> false in let is_defined = function - | _, { expr = e } -> is_defined_expr e in + | _, { expr = e } -> is_defined_expr (Vernacprop.under_control e) + && (not (Vernacprop.has_Fail e)) in + let proof_using_ast = function + | VernacProof(_,Some _) -> true + | _ -> false + in let proof_using_ast = function - | Some (_, ({ expr = VernacProof(_,Some _) } as v)) -> Some v + | Some (_, v) when proof_using_ast (Vernacprop.under_control v.expr) + && (not (Vernacprop.has_Fail v.expr)) -> Some v | _ -> None in let has_proof_using x = proof_using_ast x <> None in let proof_no_using = function - | Some (_, ({ expr = VernacProof(t,None) } as v)) -> t,v + | VernacProof(t,None) -> t + | _ -> assert false + in + let proof_no_using = function + | Some (_, v) -> proof_no_using (Vernacprop.under_control v.expr), v | _ -> assert false in let has_proof_no_using = function - | Some (_, { expr = VernacProof(_,None) }) -> true + | VernacProof(_,None) -> true + | _ -> false + in + let has_proof_no_using = function + | Some (_, v) -> has_proof_no_using (Vernacprop.under_control v.expr) + && (not (Vernacprop.has_Fail v.expr)) | _ -> false in let too_complex_to_delegate = function - | { expr = (VernacDeclareModule _ - | VernacDefineModule _ - | VernacDeclareModuleType _ - | VernacInclude _) } -> true - | { expr = (VernacRequire _ | VernacImport _) } -> true + | VernacDeclareModule _ + | VernacDefineModule _ + | VernacDeclareModuleType _ + | VernacInclude _ + | VernacRequire _ + | VernacImport _ -> true | ast -> may_pierce_opaque ast in let parent = function Some (p, _) -> p | None -> assert false in let is_empty = function `Async(_,[],_,_) | `MaybeASync(_,[],_,_) -> true | _ -> false in @@ -2099,7 +2174,8 @@ let collect_proof keep cur hd brkind id = let view = VCS.visit id in match view.step with | (`Sideff (ReplayCommand x,_) | `Cmd { cast = x }) - when too_complex_to_delegate x -> `Sync(no_name,`Print) + when too_complex_to_delegate (Vernacprop.under_control x.expr) -> + `Sync(no_name,`Print) | `Cmd { cast = x } -> collect (Some (id,x)) (id::accn) view.next | `Sideff (ReplayCommand x,_) -> collect (Some (id,x)) (id::accn) view.next (* An Alias could jump everywhere... we hope we can ignore it*) @@ -2119,7 +2195,7 @@ let collect_proof keep cur hd brkind id = (try let name, hint = name ids, get_hint_ctx loc in let t, v = proof_no_using last in - v.expr <- VernacProof(t, Some hint); + v.expr <- VernacExpr([], VernacProof(t, Some hint)); `ASync (parent last,accn,name,delegate name) with Not_found -> let name = name ids in @@ -2138,9 +2214,13 @@ let collect_proof keep cur hd brkind id = | `ASync(_,_,name,_) -> `Sync (name,why) in let check_policy rc = if async_policy () then rc else make_sync `Policy rc in + let is_vernac_exact = function + | VernacExactProof _ -> true + | _ -> false + in match cur, (VCS.visit id).step, brkind with - | (parent, { expr = VernacExactProof _ }), `Fork _, _ - | (parent, { expr = VernacTime (_, VernacExactProof _) }), `Fork _, _ -> + | (parent, x), `Fork _, _ when is_vernac_exact (Vernacprop.under_control x.expr) + && (not (Vernacprop.has_Fail x.expr)) -> `Sync (no_name,`Immediate) | _, _, { VCS.kind = `Edit _ } -> check_policy (collect (Some cur) [] id) | _ -> @@ -2150,7 +2230,7 @@ let collect_proof keep cur hd brkind id = let rc = collect (Some cur) [] id in if is_empty rc then make_sync `AlreadyEvaluated rc else if (keep == VtKeep || keep == VtKeepAsAxiom) && - (not(State.is_cached_and_valid id) || !Flags.async_proofs_full) + (not(State.is_cached_and_valid id) || !cur_opt.async_proofs_full) then check_policy rc else make_sync `AlreadyEvaluated rc @@ -2232,9 +2312,9 @@ let known_state ?(redefine_qed=false) ~cache id = (* Absorb tactic errors from f () *) let resilient_tactic id blockname f = - if !Flags.async_proofs_tac_error_resilience = `None || - (Flags.async_proofs_is_master () && - !Flags.async_proofs_mode = Flags.APoff) + if !cur_opt.async_proofs_tac_error_resilience = `None || + (async_proofs_is_master !cur_opt && + !cur_opt.async_proofs_mode = APoff) then f () else try f () @@ -2243,9 +2323,9 @@ let known_state ?(redefine_qed=false) ~cache id = error_absorbing_tactic id blockname ie in (* Absorb errors from f x *) let resilient_command f x = - if not !Flags.async_proofs_cmd_error_resilience || - (Flags.async_proofs_is_master () && - !Flags.async_proofs_mode = Flags.APoff) + if not !cur_opt.async_proofs_cmd_error_resilience || + (async_proofs_is_master !cur_opt && + !cur_opt.async_proofs_mode = APoff) then f x else try f x @@ -2254,10 +2334,14 @@ let known_state ?(redefine_qed=false) ~cache id = (* ugly functions to process nested lemmas, i.e. hard to reproduce * side effects *) let cherry_pick_non_pstate () = - Summary.freeze_summary ~marshallable:`No ~complement:true pstate, - Lib.freeze ~marshallable:`No in + let st = Summary.freeze_summaries ~marshallable:`No in + let st = Summary.remove_from_summary st Util.(pi1 summary_pstate) in + let st = Summary.remove_from_summary st Util.(pi2 summary_pstate) in + let st = Summary.remove_from_summary st Util.(pi3 summary_pstate) in + st, Lib.freeze ~marshallable:`No in + let inject_non_pstate (s,l) = - Summary.unfreeze_summary s; Lib.unfreeze l; update_global_env () + Summary.unfreeze_summaries ~partial:true s; Lib.unfreeze l; update_global_env () in let rec pure_cherry_pick_non_pstate safe_id id = stm_purify (fun id -> @@ -2287,10 +2371,10 @@ let known_state ?(redefine_qed=false) ~cache id = resilient_tactic id cblock (fun () -> reach ~cache:`Shallow view.next; Partac.vernac_interp ~solve ~abstract ~cancel_switch - !Flags.async_proofs_n_tacworkers view.next id x) + !cur_opt.async_proofs_n_tacworkers view.next id x) ), cache, true | `Cmd { cast = x; cqueue = `QueryQueue cancel_switch } - when Flags.async_proofs_is_master () -> (fun () -> + when async_proofs_is_master !cur_opt -> (fun () -> reach view.next; Query.vernac_interp ~cancel_switch view.next id x ), cache, false @@ -2304,10 +2388,10 @@ let known_state ?(redefine_qed=false) ~cache id = if eff then update_global_env () ), (if eff then `Yes else cache), true | `Cmd { cast = x; ceff = eff } -> (fun () -> - (match !Flags.async_proofs_mode with - | Flags.APon | Flags.APonLazy -> + (match !cur_opt.async_proofs_mode with + | APon | APonLazy -> resilient_command reach view.next - | Flags.APoff -> reach view.next); + | APoff -> reach view.next); let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id st x); if eff then update_global_env () @@ -2344,7 +2428,7 @@ let known_state ?(redefine_qed=false) ~cache id = | { VCS.kind = `Edit (_,_,_, okeep, _) }, Some (ofp, cancel) -> assert(redefine_qed = true); if okeep != keep then - msg_error(strbrk("The command closing the proof changed. " + msg_warning(strbrk("The command closing the proof changed. " ^"The kernel cannot take this into account and will " ^(if keep == VtKeep then "not check " else "reject ") ^"the "^(if keep == VtKeep then "new" else "incomplete") @@ -2434,7 +2518,7 @@ let known_state ?(redefine_qed=false) ~cache id = ), cache, true in let cache_step = - if !Flags.async_proofs_cache = Some Flags.Force then `Yes + if !cur_opt.async_proofs_cache = Some Force then `Yes else cache_step in State.define ?safe_id ~cache:cache_step ~redefine:redefine_qed ~feedback_processed step id; @@ -2447,15 +2531,28 @@ end (* }}} *) (********************************* STM API ************************************) (******************************************************************************) +(* Main initalization routine *) type stm_init_options = { + (* The STM will set some internal flags differently depending on the + specified [doc_type]. This distinction should dissappear at some + some point. *) doc_type : stm_doc_type; + + (* Initial load path in scope for the document. Usually extracted + from -R options / _CoqProject *) + iload_path : Mltop.coq_path list; + + (* Require [require_libs] before the initial state is + ready. Parameters follow [Library], that is to say, + [lib,prefix,import_export] means require library [lib] from + optional [prefix] and [import_export] if [Some false/Some true] + is used. *) require_libs : (string * string option * bool option) list; -(* - fb_handler : Feedback.feedback -> unit; - iload_path : (string list * string * bool) list; - implicit_std : bool; -*) + + (* STM options that apply to the current document. *) + stm_options : AsyncOpts.stm_opt; } +(* fb_handler : Feedback.feedback -> unit; *) (* let doc_type_module_name (std : stm_doc_type) = @@ -2465,9 +2562,11 @@ let doc_type_module_name (std : stm_doc_type) = *) let init_core () = + if !cur_opt.async_proofs_mode = APon then Control.enable_thread_delay := true; State.register_root_state () -let new_doc { doc_type ; require_libs } = +let new_doc { doc_type ; iload_path; require_libs; stm_options } = + let load_objs libs = let rq_file (dir, from, exp) = let mp = Libnames.(Qualid (Loc.tag @@ qualid_of_string dir)) in @@ -2476,11 +2575,19 @@ let new_doc { doc_type ; require_libs } = List.(iter rq_file (rev libs)) in + (* Set the options from the new documents *) + AsyncOpts.cur_opt := stm_options; + (* We must reset the whole state before creating a document! *) State.restore_root_state (); let doc = VCS.init doc_type Stateid.initial in + (* Set load path; important, this has to happen before we declare + the library below as [Declaremods/Library] will infer the module + name by looking at the load path! *) + List.iter Mltop.add_coq_path iload_path; + begin match doc_type with | Interactive ln -> Safe_typing.allow_delayed_constants := true; @@ -2497,16 +2604,18 @@ let new_doc { doc_type ; require_libs } = VCS.set_ldir ldir; set_compilation_hints ln end; + + (* Import initial libraries. *) load_objs require_libs; - (* We record the state here! *) + (* We record the state at this point! *) State.define ~cache:`Yes ~redefine:true (fun () -> ()) Stateid.initial; Backtrack.record (); Slaves.init (); - if Flags.async_proofs_is_master () then begin + if async_proofs_is_master !cur_opt then begin stm_prerr_endline (fun () -> "Initializing workers"); Query.init (); - let opts = match !Flags.async_proofs_private_flags with + let opts = match !cur_opt.async_proofs_private_flags with | None -> [] | Some s -> Str.split_delim (Str.regexp ",") s in begin try @@ -2592,7 +2701,7 @@ let finish_tasks name u d p (t,rcbackup as tasks) = (u,a,true), p with e -> let e = CErrors.push e in - msg_error (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e); + msg_warning (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e); exit 1 let merge_proof_branch ~valid ?id qast keep brname = @@ -2705,10 +2814,10 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) | VtQuery (true, route), w -> let id = VCS.new_node ~id:newtip () in let queue = - if !Flags.async_proofs_full then `QueryQueue (ref false) + if !cur_opt.async_proofs_full then `QueryQueue (ref false) else if VCS.is_vio_doc () && VCS.((get_branch head).kind = `Master) && - may_pierce_opaque x + may_pierce_opaque (Vernacprop.under_control x.expr) then `SkipQueue else `MainQueue in VCS.commit id (mkTransCmd x [] false queue); @@ -2770,7 +2879,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) rc (* Side effect on all branches *) - | VtUnknown, _ when expr = VernacToplevelControl Drop -> + | VtUnknown, _ when Vernacprop.under_control expr = VernacToplevelControl Drop -> let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp (VCS.get_branch_pos head) st x); `Ok @@ -2782,7 +2891,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) VCS.commit id (mkTransCmd x l in_proof `MainQueue); (* We can't replay a Definition since universes may be differently * inferred. This holds in Coq >= 8.5 *) - let action = match x.expr with + let action = match Vernacprop.under_control x.expr with | VernacDefinition(_, _, DefineBody _) -> CherryPickEnv | _ -> ReplayCommand x in VCS.propagate_sideff ~action; @@ -2805,12 +2914,11 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) if not in_proof && Proof_global.there_are_pending_proofs () then begin let bname = VCS.mk_branch_name x in - let rec opacity_of_produced_term = function + let opacity_of_produced_term = function (* This AST is ambiguous, hence we check it dynamically *) | VernacInstance (false, _,_ , None, _) -> GuaranteesOpacity - | VernacLocal (_,e) -> opacity_of_produced_term e | _ -> Doesn'tGuaranteeOpacity in - VCS.commit id (Fork (x,bname,opacity_of_produced_term x.expr,[])); + VCS.commit id (Fork (x,bname,opacity_of_produced_term (Vernacprop.under_control x.expr),[])); let proof_mode = default_proof_mode () in VCS.branch bname (`Proof (proof_mode, VCS.proof_nesting () + 1)); Proof_global.activate_proof_mode proof_mode [@ocaml.warning "-3"]; @@ -2870,7 +2978,7 @@ let parse_sentence ~doc sid pa = (str "Currently, the parsing api only supports parsing at the tip of the document." ++ fnl () ++ str "You wanted to parse at: " ++ str (Stateid.to_string sid) ++ str " but the current tip is: " ++ str (Stateid.to_string cur_tip)) ; - if not (Stateid.equal sid real_tip) && !Flags.debug && stm_debug () then + if not (Stateid.equal sid real_tip) && !Flags.debug && !stm_debug then Feedback.msg_debug (str "Warning, the real tip doesn't match the current tip." ++ str "You wanted to parse at: " ++ str (Stateid.to_string sid) ++ @@ -2950,16 +3058,25 @@ let query ~doc ~at ~route s = stm_purify (fun s -> if Stateid.equal at Stateid.dummy then ignore(finish ~doc:dummy_doc) else Reach.known_state ~cache:`Yes at; - let loc, ast = parse_sentence ~doc at s in - let indentation, strlen = compute_indentation ?loc at in - CWarnings.set_current_loc loc; - let clas = Vernac_classifier.classify_vernac ast in - let aast = { verbose = true; indentation; strlen; loc; expr = ast } in - match clas with - | VtMeta , _ -> (* TODO: can this still happen ? *) - ignore(process_transaction ~part_of_script:false aast (VtMeta,VtNow)) - | _ -> - ignore(process_transaction aast (VtQuery (false, route), VtNow))) + try + while true do + let loc, ast = parse_sentence ~doc at s in + let indentation, strlen = compute_indentation ?loc at in + CWarnings.set_current_loc loc; + let clas = Vernac_classifier.classify_vernac ast in + let aast = { verbose = true; indentation; strlen; loc; expr = ast } in + match clas with + | VtMeta , _ -> (* TODO: can this still happen ? *) + ignore(process_transaction ~part_of_script:false aast (VtMeta,VtNow)) + | _ -> + ignore(process_transaction aast (VtQuery (false,route), VtNow)) + done; + with + | End_of_input -> () + | exn -> + let iexn = CErrors.push exn in + Exninfo.iraise iexn + ) s let edit_at ~doc id = @@ -3029,7 +3146,7 @@ let edit_at ~doc id = VCS.delete_boxes_of id; VCS.gc (); VCS.print (); - if not !Flags.async_proofs_full then + if not !cur_opt.async_proofs_full then Reach.known_state ~cache:(VCS.is_interactive ()) id; VCS.checkout_shallowest_proof_branch (); `NewTip in @@ -3045,7 +3162,7 @@ let edit_at ~doc id = | _, Some _, None -> assert false | false, Some { qed = qed_id ; lemma = start }, Some(mode,bn) -> let tip = VCS.cur_tip () in - if has_failed qed_id && is_pure qed_id && not !Flags.async_proofs_never_reopen_branch + if has_failed qed_id && is_pure qed_id && not !cur_opt.async_proofs_never_reopen_branch then reopen_branch start id mode qed_id tip bn else backto id (Some bn) | true, Some { qed = qed_id }, Some(mode,bn) -> diff --git a/stm/stm.mli b/stm/stm.mli index 9fd35a0d38..8a4de34b4a 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -10,6 +10,33 @@ open Names (** state-transaction-machine interface *) +(* Flags *) +module AsyncOpts : sig + + type cache = Force + type async_proofs = APoff | APonLazy | APon + type tac_error_filter = [ `None | `Only of string list | `All ] + + type stm_opt = { + async_proofs_n_workers : int; + async_proofs_n_tacworkers : int; + + async_proofs_cache : cache option; + async_proofs_mode : async_proofs; + + async_proofs_private_flags : string option; + async_proofs_full : bool; + async_proofs_never_reopen_branch : bool; + + async_proofs_tac_error_resilience : tac_error_filter; + async_proofs_cmd_error_resilience : bool; + async_proofs_delegation_threshold : float; + } + + val default_opts : stm_opt + +end + (** The STM doc type determines some properties such as what uncompleted proofs are allowed and recording of aux files. *) type stm_doc_type = @@ -19,14 +46,26 @@ type stm_doc_type = (* Main initalization routine *) type stm_init_options = { + (* The STM will set some internal flags differently depending on the + specified [doc_type]. This distinction should dissappear at some + some point. *) doc_type : stm_doc_type; + + (* Initial load path in scope for the document. Usually extracted + from -R options / _CoqProject *) + iload_path : Mltop.coq_path list; + + (* Require [require_libs] before the initial state is + ready. Parameters follow [Library], that is to say, + [lib,prefix,import_export] means require library [lib] from + optional [prefix] and [import_export] if [Some false/Some true] + is used. *) require_libs : (string * string option * bool option) list; -(* - fb_handler : Feedback.feedback -> unit; - iload_path : (string list * string * bool) list; - implicit_std : bool; -*) + + (* STM options that apply to the current document. *) + stm_options : AsyncOpts.stm_opt; } +(* fb_handler : Feedback.feedback -> unit; *) (** The type of a STM document *) type doc @@ -39,7 +78,7 @@ 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 *) val parse_sentence : doc:doc -> Stateid.t -> Pcoq.Gram.coq_parsable -> - Vernacexpr.vernac_expr Loc.located + Vernacexpr.vernac_control Loc.located (* Reminder: A parsable [pa] is constructed using [Pcoq.Gram.coq_parsable stream], where [stream : char Stream.t]. *) @@ -53,7 +92,7 @@ exception End_of_input If [newtip] is provided, then the returned state id is guaranteed to be [newtip] *) val add : doc:doc -> ontop:Stateid.t -> ?newtip:Stateid.t -> - bool -> Vernacexpr.vernac_expr Loc.located -> + bool -> Vernacexpr.vernac_control Loc.located -> doc * Stateid.t * [ `NewTip | `Unfocus of Stateid.t ] (* [query at ?report_with cmd] Executes [cmd] at a given state [at], @@ -111,7 +150,7 @@ 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 +val get_ast : doc:doc -> Stateid.t -> (Vernacexpr.vernac_control Loc.located) option (* Filename *) val set_compilation_hints : string -> unit @@ -174,7 +213,7 @@ type static_block_declaration = { type document_node = { indentation : int; - ast : Vernacexpr.vernac_expr; + ast : Vernacexpr.vernac_control; id : Stateid.t; } @@ -189,7 +228,7 @@ type static_block_detection = type recovery_action = { base_state : Stateid.t; goals_to_admit : Goal.goal list; - recovery_command : Vernacexpr.vernac_expr option; + recovery_command : Vernacexpr.vernac_control option; } type dynamic_block_error_recovery = @@ -225,3 +264,6 @@ val state_of_id : doc:doc -> (* Queries for backward compatibility *) val current_proof_depth : doc:doc -> int val get_all_proof_names : doc:doc -> Id.t list + +(** Enable STM debugging *) +val stm_debug : bool ref diff --git a/stm/tacworkertop.ml b/stm/tacworkertop.ml index 17f90b7b15..22b45a9be8 100644 --- a/stm/tacworkertop.ml +++ b/stm/tacworkertop.ml @@ -10,5 +10,5 @@ module W = AsyncTaskQueue.MakeWorker(Stm.TacTask) () let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout -let () = Coqtop.toploop_run := (fun _ -> W.main_loop ()) +let () = Coqtop.toploop_run := (fun _ ~state:_ -> W.main_loop ()) diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 3aa2cd707e..cbbb54e45b 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -8,6 +8,7 @@ open Vernacexpr open CErrors +open Util open Pp let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"] @@ -47,36 +48,19 @@ let declare_vernac_classifier = classifiers := !classifiers @ [s,f] -let make_polymorphic (a, b as x) = - match a with - | VtStartProof (x, _, ids) -> - VtStartProof (x, Doesn'tGuaranteeOpacity, ids), b - | _ -> x +let idents_of_name : Names.Name.t -> Names.Id.t list = + function + | Names.Anonymous -> [] + | Names.Name n -> [n] -let rec classify_vernac e = - let static_classifier e = match e with +let classify_vernac e = + let static_classifier ~poly e = match e with (* Univ poly compatibility: we run it now, so that we can just * look at Flags in stm.ml. Would be nicer to have the stm * look at the entire dag to detect this option. *) - | VernacSetOption (["Universe"; "Polymorphism"],_) - | VernacUnsetOption (["Universe"; "Polymorphism"]) -> VtSideff [], VtNow - (* Nested vernac exprs *) - | VernacProgram e -> classify_vernac e - | VernacLocal (_,e) -> classify_vernac e - | VernacPolymorphic (b, e) -> - if b || Flags.is_universe_polymorphism () (* Ok or not? *) then - make_polymorphic (classify_vernac e) - else classify_vernac e - | VernacTimeout (_,e) -> classify_vernac e - | VernacTime (_,e) | VernacRedirect (_, (_,e)) -> classify_vernac e - | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) - (match classify_vernac e with - | ( VtQuery _ | VtProofStep _ | VtSideff _ - | VtProofMode _ | VtMeta), _ as x -> x - | VtQed _, _ -> - VtProofStep { parallel = `No; proof_block_detection = None }, - VtNow - | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow) + | ( VernacSetOption (l,_) | VernacUnsetOption l) + when CList.equal String.equal l Vernacentries.universe_polymorphism_option_name -> + VtSideff [], VtNow (* Qed *) | VernacAbort _ -> VtQed VtDrop, VtLater | VernacEndProof Admitted -> VtQed VtKeepAsAxiom, VtLater @@ -103,35 +87,42 @@ let rec classify_vernac e = | VernacUnsetOption (["Default";"Proof";"Using"]) | VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow (* StartProof *) - | VernacDefinition ( - (Some Decl_kinds.Discharge,Decl_kinds.Definition),((_,i),_),ProveBody _) -> - VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity,[i]), VtLater + | VernacDefinition ((Decl_kinds.DoDischarge,_),((_,i),_),ProveBody _) -> + VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity, idents_of_name i), VtLater | VernacDefinition (_,((_,i),_),ProveBody _) -> - VtStartProof(default_proof_mode (),GuaranteesOpacity,[i]), VtLater + let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in + VtStartProof(default_proof_mode (),guarantee, idents_of_name i), VtLater | VernacStartTheoremProof (_,l) -> - let ids = - CList.map_filter (function (Some ((_,i),pl), _) -> Some i | _ -> None) l in - VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater - | VernacGoal _ -> VtStartProof (default_proof_mode (),GuaranteesOpacity,[]), VtLater - | VernacFixpoint (_,l) -> + let ids = List.map (fun (((_, i), _), _) -> i) l in + let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in + VtStartProof (default_proof_mode (),guarantee,ids), VtLater + | VernacFixpoint (discharge,l) -> + let guarantee = + if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity + else GuaranteesOpacity + in let ids, open_proof = List.fold_left (fun (l,b) ((((_,id),_),_,_,_,p),_) -> id::l, b || p = None) ([],false) l in if open_proof - then VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater + then VtStartProof (default_proof_mode (),guarantee,ids), VtLater else VtSideff ids, VtLater - | VernacCoFixpoint (_,l) -> + | VernacCoFixpoint (discharge,l) -> + let guarantee = + if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity + else GuaranteesOpacity + in let ids, open_proof = List.fold_left (fun (l,b) ((((_,id),_),_,_,p),_) -> id::l, b || p = None) ([],false) l in if open_proof - then VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater + then VtStartProof (default_proof_mode (),guarantee,ids), VtLater else VtSideff ids, VtLater (* Sideff: apply to all open branches. usually run on master only *) | VernacAssumption (_,_,l) -> let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map (fun (id, _) -> snd id) l) l) in VtSideff ids, VtLater - | VernacDefinition (_,((_,id),_),DefineBody _) -> VtSideff [id], VtLater + | VernacDefinition (_,((_,id),_),DefineBody _) -> VtSideff (idents_of_name id), VtLater | VernacInductive (_, _,_,l) -> let ids = List.map (fun (((_,((_,id),_)),_,_,_,cl),_) -> id :: match cl with | Constructors l -> List.map (fun (_,((_,id),_)) -> id) l @@ -176,12 +167,12 @@ let rec classify_vernac e = (* These commands alter the parser *) | VernacOpenCloseScope _ | VernacDelimiters _ | VernacBindScope _ | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _ - | VernacSyntaxExtension _ + | VernacSyntaxExtension _ | VernacSyntacticDefinition _ | VernacRequire _ | VernacImport _ | VernacInclude _ | VernacDeclareMLModule _ | VernacContext _ (* TASSI: unsure *) - | VernacProofMode _ + | VernacProofMode _ -> VtSideff [], VtNow (* These are ambiguous *) | VernacInstance _ -> VtUnknown, VtNow (* Stm will install a new classifier to handle these *) @@ -192,16 +183,33 @@ let rec classify_vernac e = (* What are these? *) | VernacToplevelControl _ | VernacRestoreState _ - | VernacWriteState _ -> VtUnknown, VtNow + | VernacWriteState _ -> VtSideff [], VtNow (* Plugins should classify their commands *) | VernacExtend (s,l) -> try List.assoc s !classifiers l () with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".") in - let res = static_classifier e in - if Flags.is_universe_polymorphism () then - make_polymorphic res - else res + let rec static_control_classifier ~poly = function + | VernacExpr (f, e) -> + let poly = List.fold_left (fun poly f -> + match f with + | VernacPolymorphic b -> b + | (VernacProgram | VernacLocal _) -> poly + ) poly f in + static_classifier ~poly e + | VernacTimeout (_,e) -> static_control_classifier ~poly e + | VernacTime (_,(_,e)) | VernacRedirect (_, (_,e)) -> + static_control_classifier ~poly e + | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) + (match static_control_classifier ~poly e with + | ( VtQuery _ | VtProofStep _ | VtSideff _ + | VtProofMode _ | VtMeta), _ as x -> x + | VtQed _, _ -> + VtProofStep { parallel = `No; proof_block_detection = None }, + VtNow + | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow) + in + static_control_classifier ~poly:(Flags.is_universe_polymorphism ()) e let classify_as_query = VtQuery (true,Feedback.default_route), VtLater let classify_as_sideeff = VtSideff [], VtLater diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli index fe42a03a3d..c0571c1d6f 100644 --- a/stm/vernac_classifier.mli +++ b/stm/vernac_classifier.mli @@ -12,7 +12,7 @@ open Genarg val string_of_vernac_classification : vernac_classification -> string (** What does a vernacular do *) -val classify_vernac : vernac_expr -> vernac_classification +val classify_vernac : vernac_control -> vernac_classification (** Install a vernacular classifier for VernacExtend *) val declare_vernac_classifier : diff --git a/stm/workerLoop.ml b/stm/workerLoop.ml index 64121eb3d5..d606f19bff 100644 --- a/stm/workerLoop.ml +++ b/stm/workerLoop.ml @@ -6,14 +6,18 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Default priority *) +open CoqworkmgrApi +let async_proofs_worker_priority = ref Low + let rec parse = function | "--xml_format=Ppcmds" :: rest -> parse rest | x :: rest -> x :: parse rest | [] -> [] -let loop init args = - let args = parse args in +let loop init _coq_args extra_args = + let args = parse extra_args in Flags.quiet := true; init (); - CoqworkmgrApi.init !Flags.async_proofs_worker_priority; + CoqworkmgrApi.init !async_proofs_worker_priority; args diff --git a/stm/workerLoop.mli b/stm/workerLoop.mli index 53f7459357..c42b48a287 100644 --- a/stm/workerLoop.mli +++ b/stm/workerLoop.mli @@ -6,4 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -val loop : (unit -> unit) -> string list -> string list +(* Default priority *) +val async_proofs_worker_priority : CoqworkmgrApi.priority ref + +val loop : (unit -> unit) -> Coqargs.coq_cmdopts -> string list -> string list |