diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/asyncTaskQueue.ml | 70 | ||||
| -rw-r--r-- | stm/asyncTaskQueue.mli | 185 | ||||
| -rw-r--r-- | stm/coqworkmgrApi.ml | 25 | ||||
| -rw-r--r-- | stm/coqworkmgrApi.mli | 8 | ||||
| -rw-r--r-- | stm/proofBlockDelimiter.ml | 2 | ||||
| -rw-r--r-- | stm/spawned.ml | 6 | ||||
| -rw-r--r-- | stm/spawned.mli | 2 | ||||
| -rw-r--r-- | stm/stm.ml | 395 | ||||
| -rw-r--r-- | stm/stm.mli | 29 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 27 | ||||
| -rw-r--r-- | stm/workerLoop.ml | 6 | ||||
| -rw-r--r-- | stm/workerLoop.mli | 3 |
12 files changed, 501 insertions, 257 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index a356f32e9..26aef5355 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -10,17 +10,19 @@ 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 'a worker_status = [ `Fresh | `Old of 'a ] +type cancel_switch = bool ref +let async_proofs_flags_for_workers = ref [] module type Task = sig type task type competence + type worker_status = Fresh | Old of competence + (* Marshallable *) type request type response @@ -29,15 +31,14 @@ module type Task = sig val extra_env : unit -> string array (* run by the master, on a thread *) - val request_of_task : competence worker_status -> task -> request option - val task_match : competence worker_status -> task -> bool - val use_response : - competence worker_status -> task -> response -> - [ `Stay of competence * task list | `End ] + val request_of_task : worker_status -> task -> request option + val task_match : worker_status -> task -> bool + val use_response : worker_status -> task -> response -> + [ `Stay of competence * task list | `End ] val on_marshal_error : string -> task -> unit val on_task_cancellation_or_expiration_or_slave_death : task option -> unit val forward_feedback : Feedback.feedback -> unit - + (* run by the worker *) val perform : request -> response @@ -47,8 +48,6 @@ module type Task = sig end -type expiration = bool ref - module Make(T : Task) () = struct exception Die @@ -59,45 +58,45 @@ module Make(T : Task) () = struct type request = Request of T.request type more_data = - | MoreDataUnivLevel of Univ.universe_level list + | MoreDataUnivLevel of Universes.universe_id list let slave_respond (Request r) = let res = T.perform r in Response res exception MarshalError of string - + let marshal_to_channel oc data = Marshal.to_channel oc data []; flush oc - + let marshal_err s = raise (MarshalError s) - + let marshal_request oc (req : request) = try marshal_to_channel oc req with Failure s | Invalid_argument s | Sys_error s -> marshal_err ("marshal_request: "^s) - + let unmarshal_request ic = try (CThread.thread_friendly_input_value ic : request) with Failure s | Invalid_argument s | Sys_error s -> marshal_err ("unmarshal_request: "^s) - + let marshal_response oc (res : response) = try marshal_to_channel oc res with Failure s | Invalid_argument s | Sys_error s -> marshal_err ("marshal_response: "^s) - + let unmarshal_response ic = try (CThread.thread_friendly_input_value ic : response) with Failure s | Invalid_argument s | Sys_error s -> marshal_err ("unmarshal_response: "^s) - + let marshal_more_data oc (res : more_data) = try marshal_to_channel oc res with Failure s | Invalid_argument s | Sys_error s -> marshal_err ("marshal_more_data: "^s) - + let unmarshal_more_data ic = try (CThread.thread_friendly_input_value ic : more_data) with Failure s | Invalid_argument s | Sys_error s -> @@ -112,18 +111,18 @@ module Make(T : Task) () = struct module Model = struct type process = Worker.process - type extra = (T.task * expiration) TQueue.t + type extra = (T.task * cancel_switch) TQueue.t let spawn id = 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" @@ -140,7 +139,7 @@ module Make(T : Task) () = struct let { WorkerPool.extra = queue; exit; cancelled } = cpanel in let exit () = report_status ~id "Dead"; exit () in let last_task = ref None in - let worker_age = ref `Fresh in + let worker_age = ref T.Fresh in let got_token = ref false in let giveback_exec_token () = if !got_token then (CoqworkmgrApi.giveback 1; got_token := false) in @@ -170,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 () @@ -213,7 +211,7 @@ module Make(T : Task) () = struct | `Stay(competence, new_tasks) -> last_task := None; giveback_exec_token (); - worker_age := `Old competence; + worker_age := T.Old competence; add_tasks new_tasks in continue () @@ -236,7 +234,7 @@ module Make(T : Task) () = struct type queue = { active : Pool.pool; - queue : (T.task * expiration) TQueue.t; + queue : (T.task * cancel_switch) TQueue.t; cleaner : Thread.t option; } @@ -252,16 +250,16 @@ module Make(T : Task) () = struct queue; cleaner = if size > 0 then Some (Thread.create cleaner queue) else None; } - + let destroy { active; queue } = Pool.destroy active; TQueue.destroy queue let broadcast { queue } = TQueue.broadcast queue - let enqueue_task { queue; active } (t, _ as item) = + let enqueue_task { queue; active } t ~cancel_switch = stm_prerr_endline ("Enqueue task "^T.name_of_task t); - TQueue.push queue item + TQueue.push queue (t, cancel_switch) let cancel_worker { active } n = Pool.cancel n active @@ -297,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 -> @@ -310,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)); @@ -339,14 +337,14 @@ module Make(T : Task) () = struct let clear { queue; active } = assert(Pool.is_empty active); (* We allow that only if no slaves *) TQueue.clear queue - + let snapshot { queue; active } = List.map fst (TQueue.wait_until_n_are_waiting_then_snapshot (Pool.n_workers active) queue) let with_n_workers n f = - let q = create n in + let q = create n in try let rc = f q in destroy q; rc with e -> let e = CErrors.push e in destroy q; iraise e diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli index 1044e668b..07689389f 100644 --- a/stm/asyncTaskQueue.mli +++ b/stm/asyncTaskQueue.mli @@ -6,79 +6,214 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -type 'a worker_status = [ `Fresh | `Old of 'a ] +(* 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. + + A queue of items of type [task] is maintained, then for each task, + a request is generated, then sent to a worker using marshalling. + + The workers will then eventually return a result, using marshalling + again: + ____ ____ ____ ________ + | T1 | T2 | T3 | => [request ] => | Worker | + |____|____|____| <= [response] <= |________| + | Master Proc. | + \--------------/ + + Thus [request] and [response] must be safely marshallable. + + Operations for managing the task queue are provide, see below + for more details. + + *) + +(** The [Task] module type defines an abstract message-processing + queue. *) module type Task = sig + (** Main description of a task. Elements are stored in the "master" + process, and then converted into a request. + *) type task + + (** [competence] stores the information about what kind of work a + worker has completed / has available. *) type competence - (* Marshallable *) + (** A worker_status is: + + - [`Fresh] when a worker is born. + + - [`Old of competence]: When a worker ends a job it can either die + (and be replaced by a fresh new worker) or hang there as an [`Old] + worker. In such case some data can be carried by the [`Old] + constructor, typically used to implement [request_of_task]. + + This allows to implement both one-shot workers and "persistent" + ones. E.g. par: is implement using workers that don't + "reboot". Proof workers do reboot mainly because the vm has some + C state that cannot be cleared, so you have a real memory leak if + you don't reboot the worker. *) + type worker_status = Fresh | Old of competence + + (** Type of input and output data for workers. + + The data must be marshallable as it send through the network + using [Marshal] . *) type request type response - val name : string ref (* UID of the task kind, for -toploop *) + (** UID of the task kind, for -toploop *) + val name : string ref + (** Extra arguments of the task kind, for -toploop *) val extra_env : unit -> string array - (* run by the master, on a thread *) - val request_of_task : competence worker_status -> task -> request option - val task_match : competence worker_status -> task -> bool - val use_response : - competence worker_status -> task -> response -> - [ `Stay of competence * task list | `End ] + (** {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 + sent to the worker or it is not valid anymore [None]. *) + val request_of_task : worker_status -> task -> request option + + (** [task_match status tid] Allows to discard tasks based on the + worker status. *) + val task_match : worker_status -> task -> bool + + (** [use_response status t out] + + For a response [out] to a task [t] with [status] we can choose + to end the worker of to keep it alive with some data and + immediately inject extra tasks in the queue. + + For example, the proof worker runs a proof and finds an error, + the response signals that, e.g. + + [ReponseError {state = 34; msg = "oops"}] + + When the manager uses such a response he can tell the worker to + stay there and inject into the queue an extra task requesting + state 33 (to implement efficient proof repair). *) + val use_response : worker_status -> task -> response -> + [ `Stay of competence * task list | `End ] + + (** [on_marshal_error err_msg tid] notifies of marshaling failure. *) val on_marshal_error : string -> task -> unit + + (** [on_task_cancellation_or_expiration_or_slave_death tid] + + These functions are meant to parametrize the worker manager on + the actions to be taken when things go wrong or are cancelled + (you can kill a worker in CoqIDE, or using kill -9...) + + E.g. master can decide to inhabit the (delegate) Future.t with a + closure (to be run in master), i.e. make the document still + checkable. This is what I do for marshaling errors. *) val on_task_cancellation_or_expiration_or_slave_death : task option -> unit + + (** [forward_feedback fb] sends fb to all the workers. *) val forward_feedback : Feedback.feedback -> unit - - (* run by the worker *) + + (** {5} Worker API, it is run by worker, on a different fresh + process *) + + (** [perform in] synchronously processes a request [in] *) val perform : request -> response - (* debugging *) + (** debugging *) val name_of_task : task -> string val name_of_request : request -> string end -type expiration = bool ref +(** [cancel_switch] to be flipped to true by anyone to signal the task + is not relevant anymore. When the STM performs an undo/edit-at, it + crawls the document and flips these flags (the Qed node carries a + pointer to the flag IIRC). +*) +type cancel_switch = bool ref +(** Client-side functor. [MakeQueue T] creates a task queue for task [T] *) module MakeQueue(T : Task) () : sig + (** [queue] is the abstract queue type. *) type queue - (* Number of workers, 0 = lazy local *) + (** [create n] will initialize the queue with [n] workers. If [n] is + 0, the queue won't spawn any process, working in a lazy local + manner. [not imposed by the this API] *) val create : int -> queue + + (** [destroy q] Deallocates [q], cancelling all pending tasks. *) val destroy : queue -> unit + (** [n_workers q] returns the number of workers of [q] *) val n_workers : queue -> int - val enqueue_task : queue -> T.task * expiration -> unit + (** [enqueue_task q t ~cancel_switch] schedules [t] for execution in + [q]. [cancel_switch] can be flipped to true to cancel the task. *) + val enqueue_task : queue -> T.task -> cancel_switch:cancel_switch -> unit - (* blocking function that waits for the task queue to be empty *) + (** [join q] blocks until the task queue is empty *) val join : queue -> unit + + (** [cancel_all q] Cancels all tasks *) val cancel_all : queue -> unit + (** [cancel_worker q wid] cancels a particular worker [wid] *) val cancel_worker : queue -> WorkerPool.worker_id -> unit + (** [set_order q cmp] reorders [q] using ordering [cmp] *) val set_order : queue -> (T.task -> T.task -> int) -> unit + (** [broadcast q] + + This is nasty. Workers can be picky, e.g. pick tasks only when + they are "on screen". Of course the screen is scrolled, and that + changes the potential choice of workers to pick up a task or + not. + + This function wakes up the workers (the managers) that give a + look (again) to the tasks in the queue. + + The STM calls it when the perspective (as in PIDE) changes. + + A problem here is that why task_match has access to the + competence data in order to decide if the task is palatable to + the worker or not... such data is local to the worker (manager). + The perspective is global, so it does not quite fit this + picture. This API to make all managers reconsider the tasks in + the queue is the best I could came up with. + + This API is crucial to Coqoon (or any other UI that invokes + Stm.finish eagerly but wants the workers to "focus" on the visible + part of the document). + *) val broadcast : queue -> unit - (* Take a snapshot (non destructive but waits until all workers are - * enqueued) *) + (** [snapshot q] Takes a snapshot (non destructive but waits until + all workers are enqueued) *) val snapshot : queue -> T.task list - (* Clears the queue, only if the worker prool is empty *) - val clear : queue -> unit - - (* create a queue, run the function, destroy the queue. - * the user should call join *) + (** [clear q] Clears [q], only if the worker prool is empty *) + val clear : queue -> unit + + (** [with_n_workers n f] create a queue, run the function, destroy + the queue. The user should call join *) val with_n_workers : int -> (queue -> 'a) -> 'a end +(** Server-side functor. [MakeWorker T] creates the server task + dispatcher. *) module MakeWorker(T : Task) () : sig - val main_loop : unit -> unit + (** [init_stdout ()] is called at [Coqtop.toploop_init] time. *) val init_stdout : unit -> unit - + + (** [main_loop ()] is called at [Coqtop.toploop_run] time. *) + val main_loop : unit -> unit + end diff --git a/stm/coqworkmgrApi.ml b/stm/coqworkmgrApi.ml index 6d6a198c5..14fd97a6d 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 70d4173ae..953903810 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 01b75e496..77642946c 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -46,7 +46,7 @@ let simple_goal sigma g gs = let is_focused_goal_simple ~doc id = match state_of_id ~doc id with | `Expired | `Error _ | `Valid None -> `Not - | `Valid (Some { Vernacentries.proof }) -> + | `Valid (Some { Vernacstate.proof }) -> let proof = Proof_global.proof_of_state proof in let focused, r1, r2, r3, sigma = Proof.proof proof in let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in diff --git a/stm/spawned.ml b/stm/spawned.ml index 6ab096abf..fb5708f3a 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 c3cf4d67b..7f463c6a6 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 6c22d3771..1d46e0833 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -8,13 +8,13 @@ (* 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 () @@ -23,16 +23,45 @@ open CErrors open Feedback open Vernacexpr +module AsyncOpts = struct + + let async_proofs_n_workers = ref 1 + let async_proofs_n_tacworkers = ref 2 + + type cache = Force + let async_proofs_cache : cache option ref = ref None + + type async_proofs = APoff | APonLazy | APon + let async_proofs_mode = ref APoff + + let async_proofs_private_flags = ref None + let async_proofs_full = ref false + let async_proofs_never_reopen_branch = ref false + + type tac_error_filter = [ `None | `Only of string list | `All ] + let async_proofs_tac_error_resilience = ref (`Only [ "curly" ]) + let async_proofs_cmd_error_resilience = ref true + + let async_proofs_delegation_threshold = ref 0.03 + +end + +open AsyncOpts + +let async_proofs_is_master () = + !async_proofs_mode = APon && + !Flags.async_proofs_worker_id = "master" + (* Protect against state changes *) let stm_purify f x = - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in try let res = f x in - Vernacentries.unfreeze_interp_state st; + Vernacstate.unfreeze_interp_state st; res with e -> let e = CErrors.push e in - Vernacentries.unfreeze_interp_state st; + Vernacstate.unfreeze_interp_state st; Exninfo.iraise e let execution_error ?loc state_id msg = @@ -48,7 +77,7 @@ let state_computed, state_computed_hook = Hook.make let state_ready, state_ready_hook = Hook.make ~default:(fun state_id -> ()) () -let forward_feedback, forward_feedback_hook = +let forward_feedback, forward_feedback_hook = let m = Mutex.create () in Hook.make ~default:(function | { doc_id = did; span_id = id; route; contents } -> @@ -108,7 +137,6 @@ module Vcs_ = Vcs.Make(Stateid.Self) type future_proof = Proof_global.closed_proof_output Future.computation type proof_mode = string type depth = int -type cancel_switch = bool ref type branch_type = [ `Master | `Proof of proof_mode * depth @@ -122,14 +150,14 @@ type cmd_t = { cids : Names.Id.t list; cblock : proof_block_name option; cqueue : [ `MainQueue - | `TacQueue of solving_tac * anon_abstracting_tac * cancel_switch - | `QueryQueue of cancel_switch + | `TacQueue of solving_tac * anon_abstracting_tac * AsyncTaskQueue.cancel_switch + | `QueryQueue of AsyncTaskQueue.cancel_switch | `SkipQueue ] } type fork_t = aast * Vcs_.Branch.t * Vernacexpr.opacity_guarantee * Names.Id.t list type qed_t = { qast : aast; keep : vernac_qed_type; - mutable fproof : (future_proof * cancel_switch) option; + mutable fproof : (future_proof * AsyncTaskQueue.cancel_switch) option; brname : Vcs_.Branch.t; brinfo : branch_type Vcs_.branch_info } @@ -159,13 +187,14 @@ 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 - | Valid of Vernacentries.interp_state + | Valid of Vernacstate.t type branch = Vcs_.Branch.t * branch_type Vcs_.branch_info type backup = { mine : branch; others : branch list } @@ -318,7 +347,7 @@ module VCS : sig (* cuts from start -> stop, raising Expired if some nodes are not there *) val slice : block_start:id -> block_stop:id -> vcs val nodes_in_slice : block_start:id -> block_stop:id -> Stateid.t list - + val create_proof_task_box : id list -> qed:id -> block_start:id -> unit val create_proof_block : static_block_declaration -> string -> unit val box_of : id -> box list @@ -353,10 +382,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") @@ -367,7 +396,7 @@ end = struct (* {{{ *) | Noop -> " " | Alias (id,_) -> sprintf "Alias(%s)" (Stateid.to_string id) | Qed { qast } -> Pp.string_of_ppcmds (pr_ast qast) in - let is_green id = + let is_green id = match get_info vcs id with | Some { state = Valid _ } -> true | _ -> false in @@ -435,7 +464,7 @@ end = struct (* {{{ *) let outerboxes boxes = List.filter (fun b -> not (List.exists (fun b1 -> - not (same_box b1 b) && contains b1 b) boxes) + not (same_box b1 b) && contains b1 b) boxes) ) boxes in let rec rec_print b = boxes := CList.remove same_box b !boxes; @@ -530,7 +559,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 () then Hooks.(call state_ready id) let get_state id = (get_info id).state let reached id = let info = get_info id in @@ -565,7 +594,7 @@ end = struct (* {{{ *) let id = new_node () in merge id ~ours:(Sideff action) ~into:b Branch.master) (List.filter (fun b -> not (Branch.equal b Branch.master)) (branches ())) - + let visit id = Vcs_aux.visit !vcs id let nodes_in_slice ~block_start ~block_stop = @@ -664,7 +693,7 @@ end = struct (* {{{ *) val command : now:bool -> (unit -> unit) -> unit end = struct - + let m = Mutex.create () let c = Condition.create () let job = ref None @@ -735,16 +764,16 @@ module State : sig val exn_on : Stateid.t -> valid:Stateid.t -> Exninfo.iexn -> Exninfo.iexn (* to send states across worker/master *) - val get_cached : Stateid.t -> Vernacentries.interp_state - val same_env : Vernacentries.interp_state -> Vernacentries.interp_state -> bool + val get_cached : Stateid.t -> Vernacstate.t + val same_env : Vernacstate.t -> Vernacstate.t -> bool type proof_part type partial_state = - [ `Full of Vernacentries.interp_state + [ `Full of Vernacstate.t | `ProofOnly of Stateid.t * proof_part ] - val proof_part_of_frozen : Vernacentries.interp_state -> proof_part + val proof_part_of_frozen : Vernacstate.t -> proof_part val assign : Stateid.t -> partial_state -> unit (* Handlers for initial state, prior to document creation. *) @@ -757,26 +786,30 @@ module State : sig end = struct (* {{{ *) - open Vernacentries - (* cur_id holds Stateid.dummy in case the last attempt to define a state * failed, so the global state may contain garbage *) let cur_id = ref Stateid.dummy 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 Vernacentries.interp_state + [ `Full of Vernacstate.t | `ProofOnly of Stateid.t * proof_part ] - let proof_part_of_frozen { Vernacentries.proof; system } = + 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 (Vernacentries.freeze_interp_state marshallable)) + VCS.set_state id (Valid (Vernacstate.freeze_interp_state marshallable)) let freeze_invalid id iexn = VCS.set_state id (Error iexn) @@ -800,7 +833,7 @@ end = struct (* {{{ *) let install_cached id = match VCS.get_info id with | { state = Valid s } -> - Vernacentries.unfreeze_interp_state s; + Vernacstate.unfreeze_interp_state s; cur_id := id | { state = Error ie } -> @@ -819,6 +852,7 @@ end = struct (* {{{ *) with VCS.Expired -> anomaly Pp.(str "not a cached state (expired).") let assign id what = + let open Vernacstate in if VCS.get_state id <> Empty then () else try match what with | `Full s -> @@ -826,22 +860,27 @@ end = struct (* {{{ *) try let prev = (VCS.visit id).next in if is_cached_and_valid prev - then { s with Vernacentries.proof = + then { s with proof = Proof_global.copy_terminators ~src:(get_cached prev).proof ~tgt:s.proof } 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,12 +893,12 @@ end = struct (* {{{ *) execution_error ?loc id (iprint (e, info)); (e, Stateid.add info ~valid id) - let same_env { system = s1 } { system = s2 } = + 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 @@ -902,11 +941,11 @@ end = struct (* {{{ *) let init_state = ref None let register_root_state () = - init_state := Some (Vernacentries.freeze_interp_state `No) + init_state := Some (Vernacstate.freeze_interp_state `No) let restore_root_state () = cur_id := Stateid.dummy; - Vernacentries.unfreeze_interp_state (Option.get !init_state); + Vernacstate.unfreeze_interp_state (Option.get !init_state); end (* }}} *) @@ -973,7 +1012,7 @@ let get_script prf = find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next | `Sideff (CherryPickEnv, id) -> find acc id | `Cmd {cast = x; ctac} when ctac -> (* skip non-tactics *) - find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next + find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next | `Cmd _ -> find acc view.next | `Alias (id,_) -> find acc id | `Fork _ -> find acc view.next @@ -1001,7 +1040,7 @@ end (* Wrapper for Vernacentries.interp to set the feedback id *) (* It is currently called 19 times, this number should be certainly reduced... *) -let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacentries.interp_state = +let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacstate.t = (* The Stm will gain the capability to interpret commmads affecting the whole document state, such as backtrack, etc... so we start to design the stm command interpreter now *) @@ -1025,7 +1064,7 @@ let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacentries | 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) + 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) @@ -1107,7 +1146,7 @@ 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 && !async_proofs_cache <> Some Force then undo_costly_in_batch_mode v; try match v with @@ -1139,7 +1178,7 @@ end = struct (* {{{ *) let m = match e with VernacUndoTo m -> m | _ -> 0 in let id = VCS.get_branch_pos (VCS.current_branch ()) in let vcs = - match (VCS.get_info id).vcs_backup with + match (VCS.get_info id).vcs_backup with | None, _ -> anomaly Pp.(str"Backtrack: tip with no vcs_backup.") | Some vcs, _ -> vcs in let cb, _ = @@ -1192,7 +1231,7 @@ let record_pb_time ?loc proof_name time = Aux_file.record_in_aux_at proof_name proof_build_time; hints := Aux_file.set !hints proof_name proof_build_time end - + exception RemoteException of Pp.t let _ = CErrors.register_handler (function | RemoteException ppcmd -> ppcmd @@ -1243,15 +1282,15 @@ 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 !async_proofs_tac_error_resilience with | `None -> false | `All -> true | `Only l -> List.mem name l let detect_proof_block id name = - let name = match name with None -> "indent" | Some x -> x in + 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 () || Flags.async_proofs_is_worker ()) then ( match cur_node id with | None -> () @@ -1272,7 +1311,7 @@ let detect_proof_block id name = (* Unused module warning doesn't understand [module rec] *) [@@@ocaml.warning "-60"] module rec ProofTask : sig - + type competence = Stateid.t list type task_build_proof = { t_exn_info : Stateid.t * Stateid.t; @@ -1295,8 +1334,8 @@ module rec ProofTask : sig include AsyncTaskQueue.Task with type task := task - and type competence := competence - and type request := request + and type competence := competence + and type request := request val build_proof_here : ?loc:Loc.t -> @@ -1305,7 +1344,7 @@ module rec ProofTask : sig Proof_global.closed_proof_output Future.computation (* If set, only tasks overlapping with this list are processed *) - val set_perspective : Stateid.t list -> unit + val set_perspective : Stateid.t list -> unit end = struct (* {{{ *) @@ -1327,10 +1366,12 @@ end = struct (* {{{ *) | BuildProof of task_build_proof | States of Stateid.t list + type worker_status = Fresh | Old of competence + type request = | ReqBuildProof of (Future.UUID.t,VCS.vcs) Stateid.request * bool * competence | ReqStates of Stateid.t list - + type error = { e_error_at : Stateid.t; e_safe_id : Stateid.t; @@ -1350,10 +1391,10 @@ end = struct (* {{{ *) let task_match age t = match age, t with - | `Fresh, BuildProof { t_states } -> - not !Flags.async_proofs_full || + | Fresh, BuildProof { t_states } -> + not !async_proofs_full || List.exists (fun x -> CList.mem_f Stateid.equal x !perspective) t_states - | `Old my_states, States l -> + | Old my_states, States l -> List.for_all (fun x -> CList.mem_f Stateid.equal x my_states) l | _ -> false @@ -1369,7 +1410,7 @@ end = struct (* {{{ *) | BuildProof { t_exn_info;t_start;t_stop;t_loc;t_uuid;t_name;t_states;t_drop } -> - assert(age = `Fresh); + assert(age = Fresh); try Some (ReqBuildProof ({ Stateid.exn_info = t_exn_info; stop = t_stop; @@ -1379,19 +1420,19 @@ end = struct (* {{{ *) name = t_name }, t_drop, t_states)) with VCS.Expired -> None - let use_response (s : competence AsyncTaskQueue.worker_status) t r = + let use_response (s : worker_status) t r = match s, t, r with - | `Old c, States _, RespStates l -> + | Old c, States _, RespStates l -> List.iter (fun (id,s) -> State.assign id s) l; `End - | `Fresh, BuildProof { t_assign; t_loc; t_name; t_states; t_drop }, + | Fresh, BuildProof { t_assign; t_loc; t_name; t_states; t_drop }, RespBuiltProof (pl, time) -> feedback (InProgress ~-1); t_assign (`Val pl); record_pb_time ?loc:t_loc t_name time; - if !Flags.async_proofs_full || t_drop + if !async_proofs_full || t_drop then `Stay(t_states,[States t_states]) else `End - | `Fresh, BuildProof { t_assign; t_loc; t_name; t_states }, + | Fresh, BuildProof { t_assign; t_loc; t_name; t_states }, RespError { e_error_at; e_safe_id = valid; e_msg; e_safe_states } -> feedback (InProgress ~-1); let info = Stateid.add ~valid Exninfo.null e_error_at in @@ -1437,19 +1478,19 @@ end = struct (* {{{ *) * a bad fixpoint *) let fix_exn = Future.fix_exn_of future_proof in (* STATE: We use the current installed imperative state *) - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in if not drop then begin let checked_proof = Future.chain future_proof (fun p -> (* Unfortunately close_future_proof and friends are not pure so we need to set the state manually here *) - Vernacentries.unfreeze_interp_state st; + Vernacstate.unfreeze_interp_state st; let pobject, _ = Proof_global.close_future_proof ~feedback_id:stop (Future.from_val ~fix_exn p) in let terminator = (* The one sent by master is an InvalidKey *) Lemmas.(standard_proof_terminator [] (mk_hook (fun _ _ -> ()))) in - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in stm_vernac_interp stop ~proof:(pobject, terminator) st { verbose = false; loc; indentation = 0; strlen = 0; @@ -1457,7 +1498,7 @@ end = struct (* {{{ *) ignore(Future.join checked_proof); end; (* STATE: Restore the state XXX: handle exn *) - Vernacentries.unfreeze_interp_state st; + Vernacstate.unfreeze_interp_state st; RespBuiltProof(proof,time) with | e when CErrors.noncritical e || e = Stack_overflow -> @@ -1478,7 +1519,7 @@ end = struct (* {{{ *) | VtProofStep _, _ -> true | _ -> false in - let initial = + let initial = let rec aux id = try match VCS.visit id with { next } -> aux next with VCS.Expired -> id in @@ -1491,7 +1532,7 @@ end = struct (* {{{ *) then Some (prev, State.get_cached prev, step) else None with VCS.Expired -> None in - let this = + let this = if State.is_cached_and_valid id then Some (State.get_cached id) else None in match prev, this with | _, None -> None @@ -1533,11 +1574,11 @@ and Slaves : sig val build_proof : ?loc:Loc.t -> drop_pt:bool -> exn_info:(Stateid.t * Stateid.t) -> block_start:Stateid.t -> block_stop:Stateid.t -> - name:string -> future_proof * cancel_switch + name:string -> future_proof * AsyncTaskQueue.cancel_switch (* blocking function that waits for the task queue to be empty *) val wait_all_done : unit -> unit - + (* initialize the whole machinery (optional) *) val init : unit -> unit @@ -1559,11 +1600,11 @@ and Slaves : sig end = struct (* {{{ *) module TaskQueue = AsyncTaskQueue.MakeQueue(ProofTask) () - + 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 () then + queue := Some (TaskQueue.create !async_proofs_n_workers) else queue := Some (TaskQueue.create 0) @@ -1598,7 +1639,7 @@ end = struct (* {{{ *) * => takes nothing from the itermediate states. *) (* STATE We use the state resulting from reaching start. *) - let st = Vernacentries.freeze_interp_state `No in + 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))) }); @@ -1614,8 +1655,8 @@ end = struct (* {{{ *) | Some (_, cur) -> match VCS.visit cur with | { step = `Cmd { cast = { loc } } } - | { step = `Fork (( { loc }, _, _, _), _) } - | { step = `Qed ( { qast = { loc } }, _) } + | { step = `Fork (( { loc }, _, _, _), _) } + | { step = `Qed ( { qast = { loc } }, _) } | { step = `Sideff (ReplayCommand { loc }, _) } -> let start, stop = Option.cata Loc.unloc (0,0) loc in msg_error Pp.( @@ -1665,7 +1706,7 @@ end = struct (* {{{ *) u.(bucket) <- uc; p.(bucket) <- pr; u, Univ.ContextSet.union cst extra, false - + let check_task name l i = match check_task_aux "" name l i with | `OK _ | `OK_ADMITTED -> true @@ -1710,11 +1751,11 @@ end = struct (* {{{ *) t_exn_info; t_start = block_start; t_stop = block_stop; t_drop = drop_pt; t_assign = assign; t_loc = loc; t_uuid; t_name = pname; t_states = VCS.nodes_in_slice ~block_start ~block_stop }) in - TaskQueue.enqueue_task (Option.get !queue) (task,cancel_switch); + TaskQueue.enqueue_task (Option.get !queue) task ~cancel_switch; f, cancel_switch end else ProofTask.build_proof_here ?loc ~drop_pt t_exn_info block_stop, cancel_switch - else + else let f, t_assign = Future.create_delegate ~name:pname (State.exn_on id ~valid) in let t_uuid = Future.uuid f in feedback (InProgress 1); @@ -1722,7 +1763,7 @@ end = struct (* {{{ *) t_exn_info; t_start = block_start; t_stop = block_stop; t_assign; t_drop = drop_pt; t_loc = loc; t_uuid; t_name = pname; t_states = VCS.nodes_in_slice ~block_start ~block_stop }) in - TaskQueue.enqueue_task (Option.get !queue) (task,cancel_switch); + TaskQueue.enqueue_task (Option.get !queue) task ~cancel_switch; f, cancel_switch let wait_all_done () = TaskQueue.join (Option.get !queue) @@ -1736,7 +1777,7 @@ end = struct (* {{{ *) let reqs = CList.map_filter ProofTask.(fun x -> - match request_of_task `Fresh x with + match request_of_task Fresh x with | Some (ReqBuildProof (r, b, _)) -> Some(r, b) | _ -> None) tasks in @@ -1749,7 +1790,7 @@ end (* }}} *) and TacTask : sig - type output = (Constr.constr * Evd.evar_universe_context) option + type output = (Constr.constr * UState.t) option type task = { t_state : Stateid.t; t_state_fb : Stateid.t; @@ -1757,14 +1798,14 @@ and TacTask : sig t_ast : int * aast; t_goal : Goal.goal; t_kill : unit -> unit; - t_name : string } + t_name : string } include AsyncTaskQueue.Task with type task := task end = struct (* {{{ *) - type output = (Constr.constr * Evd.evar_universe_context) option - + type output = (Constr.constr * UState.t) option + let forward_feedback msg = Hooks.(call forward_feedback msg) type task = { @@ -1774,7 +1815,7 @@ end = struct (* {{{ *) t_ast : int * aast; t_goal : Goal.goal; t_kill : unit -> unit; - t_name : string } + t_name : string } type request = { r_state : Stateid.t; @@ -1785,13 +1826,15 @@ end = struct (* {{{ *) r_name : string } type response = - | RespBuiltSubProof of (Constr.constr * Evd.evar_universe_context) + | RespBuiltSubProof of (Constr.constr * UState.t) | RespError of Pp.t | RespNoProgress let name = ref "tacworker" let extra_env () = [||] type competence = unit + type worker_status = Fresh | Old of competence + let task_match _ _ = true (* run by the master, on a thread *) @@ -1800,13 +1843,13 @@ end = struct (* {{{ *) r_state = t_state; r_state_fb = t_state_fb; r_document = - if age <> `Fresh then None + if age <> Fresh then None else Some (VCS.slice ~block_start:t_state ~block_stop:t_state); r_ast = t_ast; r_goal = t_goal; r_name = t_name } with VCS.Expired -> None - + let use_response _ { t_assign; t_state; t_state_fb; t_kill } resp = match resp with | RespBuiltSubProof o -> t_assign (`Val (Some o)); `Stay ((),[]) @@ -1819,7 +1862,7 @@ end = struct (* {{{ *) t_assign (`Exn e); t_kill (); `Stay ((),[]) - + let on_marshal_error err { t_name } = stm_pr_err ("Fatal marshal error: " ^ t_name ); flush_all (); exit 1 @@ -1827,7 +1870,7 @@ end = struct (* {{{ *) let on_task_cancellation_or_expiration_or_slave_death = function | Some { t_kill } -> t_kill () | _ -> () - + let command_focus = Proof.new_focus_kind () let focus_cond = Proof.no_cond command_focus @@ -1855,7 +1898,7 @@ end = struct (* {{{ *) * => captures state id in a future closure, which will discard execution state but for the proof + univs. *) - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp r_state_fb st ast); let _,_,_,_,sigma = Proof.proof (Proof_global.give_me_the_proof ()) in match Evd.(evar_body (find sigma r_goal)) with @@ -1872,21 +1915,20 @@ end = struct (* {{{ *) let name_of_task { t_name } = t_name let name_of_request { r_name } = r_name - + end (* }}} *) and Partac : sig val vernac_interp : - solve:bool -> abstract:bool -> cancel_switch -> - int -> Stateid.t -> Stateid.t -> aast -> - unit + solve:bool -> abstract:bool -> cancel_switch:AsyncTaskQueue.cancel_switch -> + int -> Stateid.t -> Stateid.t -> aast -> unit end = struct (* {{{ *) - + module TaskQueue = AsyncTaskQueue.MakeQueue(TacTask) () - let vernac_interp ~solve ~abstract cancel nworkers safe_id id + let vernac_interp ~solve ~abstract ~cancel_switch nworkers safe_id id { indentation; verbose; loc; expr = e; strlen } = let e, time, fail = @@ -1895,7 +1937,7 @@ end = struct (* {{{ *) | 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 st = Vernacentries.freeze_interp_state `No 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 () -> ignore(TaskQueue.with_n_workers nworkers (fun queue -> @@ -1910,10 +1952,10 @@ end = struct (* {{{ *) let t_ast = (i, { indentation; verbose; loc; expr = e; strlen }) in let t_name = Goal.uid g in TaskQueue.enqueue_task queue - ({ t_state = safe_id; t_state_fb = id; + { t_state = safe_id; t_state_fb = id; t_assign = assign; t_ast; t_goal = g; t_name; - t_kill = (fun () -> if solve then TaskQueue.cancel_all queue) }, - cancel); + t_kill = (fun () -> if solve then TaskQueue.cancel_all queue) } + ~cancel_switch; g,f) 1 goals in TaskQueue.join queue; @@ -1932,9 +1974,10 @@ end = struct (* {{{ *) let open Notations in match Future.join f with | Some (pt, uc) -> + let sigma, env = Pfedit.get_current_context () in stm_pperr_endline (fun () -> hov 0 ( str"g=" ++ int (Evar.repr gid) ++ spc () ++ - str"t=" ++ (Printer.pr_constr pt) ++ spc () ++ + str"t=" ++ (Printer.pr_constr_env env sigma pt) ++ spc () ++ str"uc=" ++ Termops.pr_evar_universe_context uc)); (if abstract then Tactics.tclABSTRACT None else (fun x -> x)) (V82.tactic (Refiner.tclPUSHEVARUNIVCONTEXT uc) <*> @@ -1944,7 +1987,7 @@ end = struct (* {{{ *) end) in Proof.run_tactic (Global.env()) assign_tac p)))) ()) - + end (* }}} *) and QueryTask : sig @@ -1953,10 +1996,10 @@ and QueryTask : sig include AsyncTaskQueue.Task with type task := task end = struct (* {{{ *) - + type task = { t_where : Stateid.t; t_for : Stateid.t ; t_what : aast } - + type request = { r_where : Stateid.t ; r_for : Stateid.t ; r_what : aast; r_doc : VCS.vcs } type response = unit @@ -1964,6 +2007,8 @@ end = struct (* {{{ *) let name = ref "queryworker" let extra_env _ = [||] type competence = unit + type worker_status = Fresh | Old of competence + let task_match _ _ = true let request_of_task _ { t_where; t_what; t_for } = @@ -1973,7 +2018,7 @@ end = struct (* {{{ *) r_doc = VCS.slice ~block_start:t_where ~block_stop:t_where; r_what = t_what } with VCS.Expired -> None - + let use_response _ _ _ = `End let on_marshal_error _ _ = @@ -1981,7 +2026,7 @@ end = struct (* {{{ *) flush_all (); exit 1 let on_task_cancellation_or_expiration_or_slave_death _ = () - + let forward_feedback msg = Hooks.(call forward_feedback msg) let perform { r_where; r_doc; r_what; r_for } = @@ -1989,7 +2034,7 @@ end = struct (* {{{ *) VCS.print (); Reach.known_state ~cache:`No r_where; (* STATE *) - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in try (* STATE SPEC: * - start: r_where @@ -2001,16 +2046,16 @@ end = struct (* {{{ *) let e = CErrors.push e in let msg = iprint e in feedback ~id:r_for (Message (Error, None, msg)) - + let name_of_task { t_what } = string_of_ppcmds (pr_ast t_what) let name_of_request { r_what } = string_of_ppcmds (pr_ast r_what) end (* }}} *) -and Query : sig +and Query : sig val init : unit -> unit - val vernac_interp : cancel_switch -> Stateid.t -> Stateid.t -> aast -> unit + val vernac_interp : cancel_switch:AsyncTaskQueue.cancel_switch -> Stateid.t -> Stateid.t -> aast -> unit end = struct (* {{{ *) @@ -2018,13 +2063,13 @@ end = struct (* {{{ *) let queue = ref None - let vernac_interp switch prev id q = + let vernac_interp ~cancel_switch prev id q = assert(TaskQueue.n_workers (Option.get !queue) > 0); TaskQueue.enqueue_task (Option.get !queue) - QueryTask.({ t_where = prev; t_for = id; t_what = q }, switch) + 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 !async_proofs_full then 1 else 0)) end (* }}} *) @@ -2036,8 +2081,6 @@ and Reach : sig end = struct (* {{{ *) -let pstate = summary_pstate - let async_policy () = let open Flags in if is_universe_polymorphism () then false @@ -2047,10 +2090,10 @@ let async_policy () = (VCS.is_vio_doc () || !async_proofs_mode <> APoff) let delegate name = - get_hint_bp_time name >= !Flags.async_proofs_delegation_threshold + get_hint_bp_time name >= !async_proofs_delegation_threshold || VCS.is_vio_doc () - || !Flags.async_proofs_full - + || !async_proofs_full + let warn_deprecated_nested_proofs = CWarnings.create ~name:"deprecated-nested-proofs" ~category:"deprecated" (fun () -> @@ -2065,6 +2108,7 @@ let collect_proof keep cur hd brkind id = | id :: _ -> Names.Id.to_string id in let loc = (snd cur).loc in let rec 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 @@ -2145,7 +2189,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) || !async_proofs_full) then check_policy rc else make_sync `AlreadyEvaluated rc @@ -2175,7 +2219,7 @@ let log_processing_sync id name reason = log_string Printf.(sprintf let wall_clock_last_fork = ref 0.0 let known_state ?(redefine_qed=false) ~cache id = - + let error_absorbing_tactic id blockname exn = (* We keep the static/dynamic part of block detection separate, since the static part could be performed earlier. As of today there is @@ -2203,7 +2247,7 @@ let known_state ?(redefine_qed=false) ~cache id = Proofview.give_up else Proofview.tclUNIT () end in match (VCS.get_info base_state).state with - | Valid { Vernacentries.proof } -> + | Valid { Vernacstate.proof } -> Proof_global.unfreeze proof; Proof_global.with_current_proof (fun _ p -> feedback ~id:id Feedback.AddedAxiom; @@ -2213,7 +2257,7 @@ let known_state ?(redefine_qed=false) ~cache id = * - end : maybe after recovery command. *) (* STATE: We use an updated state with proof *) - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in Option.iter (fun expr -> ignore(stm_vernac_interp id st { verbose = true; loc = None; expr; indentation = 0; strlen = 0 } )) @@ -2227,9 +2271,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 !async_proofs_tac_error_resilience = `None || + (async_proofs_is_master () && + !async_proofs_mode = APoff) then f () else try f () @@ -2238,9 +2282,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 !async_proofs_cmd_error_resilience || + (async_proofs_is_master () && + !async_proofs_mode = APoff) then f x else try f x @@ -2249,10 +2293,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 -> @@ -2277,39 +2325,39 @@ let known_state ?(redefine_qed=false) ~cache id = ), cache, true | `Cmd { cast = x; cqueue = `SkipQueue } -> (fun () -> reach view.next), cache, true - | `Cmd { cast = x; cqueue = `TacQueue (solve,abstract,cancel); cblock } -> + | `Cmd { cast = x; cqueue = `TacQueue (solve,abstract,cancel_switch); cblock } -> (fun () -> resilient_tactic id cblock (fun () -> reach ~cache:`Shallow view.next; - Partac.vernac_interp ~solve ~abstract - cancel !Flags.async_proofs_n_tacworkers view.next id x) + Partac.vernac_interp ~solve ~abstract ~cancel_switch + !async_proofs_n_tacworkers view.next id x) ), cache, true - | `Cmd { cast = x; cqueue = `QueryQueue cancel } - when Flags.async_proofs_is_master () -> (fun () -> + | `Cmd { cast = x; cqueue = `QueryQueue cancel_switch } + when async_proofs_is_master () -> (fun () -> reach view.next; - Query.vernac_interp cancel view.next id x + Query.vernac_interp ~cancel_switch view.next id x ), cache, false | `Cmd { cast = x; ceff = eff; ctac = true; cblock } -> (fun () -> resilient_tactic id cblock (fun () -> reach view.next; (* State resulting from reach *) - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id st x) ); 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 !async_proofs_mode with + | APon | APonLazy -> resilient_command reach view.next - | Flags.APoff -> reach view.next); - let st = Vernacentries.freeze_interp_state `No in + | 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 () ), (if eff then `Yes else cache), true | `Fork ((x,_,_,_), None) -> (fun () -> resilient_command reach view.next; - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id st x); wall_clock_last_fork := Unix.gettimeofday () ), `Yes, true @@ -2318,7 +2366,7 @@ let known_state ?(redefine_qed=false) ~cache id = reach view.next; (try - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id st x); with e when CErrors.noncritical e -> let (e, info) = CErrors.push e in @@ -2369,16 +2417,16 @@ let known_state ?(redefine_qed=false) ~cache id = Proof_global.close_future_proof ~feedback_id:id fp in if not delegate then ignore(Future.compute fp); reach view.next; - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id ~proof st x); feedback ~id:id Incomplete | { VCS.kind = `Master }, _ -> assert false end; Proof_global.discard_all () ), (if redefine_qed then `No else `Yes), true - | `Sync (name, `Immediate) -> (fun () -> + | `Sync (name, `Immediate) -> (fun () -> reach eop; - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id st x); Proof_global.discard_all () ), `Yes, true @@ -2401,7 +2449,7 @@ let known_state ?(redefine_qed=false) ~cache id = if keep != VtKeepAsAxiom then reach view.next; let wall_clock2 = Unix.gettimeofday () in - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id ?proof st x); let wall_clock3 = Unix.gettimeofday () in Aux_file.record_in_aux_at ?loc:x.loc "proof_check_time" @@ -2419,7 +2467,7 @@ let known_state ?(redefine_qed=false) ~cache id = aux (collect_proof keep (view.next, x) brname brinfo eop) | `Sideff (ReplayCommand x,_) -> (fun () -> reach view.next; - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id st x); update_global_env () ), cache, true @@ -2429,7 +2477,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 !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; @@ -2460,6 +2508,7 @@ let doc_type_module_name (std : stm_doc_type) = *) let init_core () = + if !async_proofs_mode = APon then Control.enable_thread_delay := true; State.register_root_state () let new_doc { doc_type ; require_libs } = @@ -2478,12 +2527,16 @@ let new_doc { doc_type ; require_libs } = begin match doc_type with | Interactive ln -> + Safe_typing.allow_delayed_constants := true; Declaremods.start_library ln + | VoDoc ln -> let ldir = Flags.verbosely Library.start_library ln in VCS.set_ldir ldir; set_compilation_hints ln + | VioDoc ln -> + Safe_typing.allow_delayed_constants := true; let ldir = Flags.verbosely Library.start_library ln in VCS.set_ldir ldir; set_compilation_hints ln @@ -2494,10 +2547,10 @@ let new_doc { doc_type ; require_libs } = 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 () then begin stm_prerr_endline (fun () -> "Initializing workers"); Query.init (); - let opts = match !Flags.async_proofs_private_flags with + let opts = match !async_proofs_private_flags with | None -> [] | Some s -> Str.split_delim (Str.regexp ",") s in begin try @@ -2688,7 +2741,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) | VtQuery (false,route), VtNow -> let query_sid = VCS.cur_tip () in (try - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp ~route query_sid st x) with e -> let e = CErrors.push e in @@ -2696,7 +2749,7 @@ 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 !async_proofs_full then `QueryQueue (ref false) else if VCS.is_vio_doc () && VCS.((get_branch head).kind = `Master) && may_pierce_opaque x @@ -2762,7 +2815,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) (* Side effect on all branches *) | VtUnknown, _ when expr = VernacToplevelControl Drop -> - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp (VCS.get_branch_pos head) st x); `Ok @@ -2790,7 +2843,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) VCS.checkout VCS.Branch.master; let mid = VCS.get_branch_pos VCS.Branch.master in let _st' = Reach.known_state ~cache:(VCS.is_interactive ()) mid in - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id st x); (* Vernac x may or may not start a proof *) if not in_proof && Proof_global.there_are_pending_proofs () then @@ -2831,7 +2884,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) let get_ast ~doc id = match VCS.visit id with | { step = `Cmd { cast = { loc; expr } } } - | { step = `Fork (({ loc; expr }, _, _, _), _) } + | { step = `Fork (({ loc; expr }, _, _, _), _) } | { step = `Qed ({ qast = { loc; expr } }, _) } -> Some (Loc.tag ?loc expr) | _ -> None @@ -2861,7 +2914,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) ++ @@ -3020,7 +3073,7 @@ let edit_at ~doc id = VCS.delete_boxes_of id; VCS.gc (); VCS.print (); - if not !Flags.async_proofs_full then + if not !async_proofs_full then Reach.known_state ~cache:(VCS.is_interactive ()) id; VCS.checkout_shallowest_proof_branch (); `NewTip in @@ -3036,7 +3089,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 !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 31f4599d3..ef95be0e4 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -220,8 +220,35 @@ val forward_feedback_hook : (Feedback.feedback -> unit) Hook.t val get_doc : Feedback.doc_id -> doc val state_of_id : doc:doc -> - Stateid.t -> [ `Valid of Vernacentries.interp_state option | `Expired | `Error of exn ] + Stateid.t -> [ `Valid of Vernacstate.t option | `Expired | `Error of exn ] (* 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 + +(* Flags *) +module AsyncOpts : sig + + (* Defaults for worker creation *) + val async_proofs_n_workers : int ref + val async_proofs_n_tacworkers : int ref + + type async_proofs = APoff | APonLazy | APon + val async_proofs_mode : async_proofs ref + + type cache = Force + val async_proofs_cache : cache option ref + + val async_proofs_private_flags : string option ref + val async_proofs_full : bool ref + val async_proofs_never_reopen_branch : bool ref + + type tac_error_filter = [ `None | `Only of string list | `All ] + val async_proofs_tac_error_resilience : tac_error_filter ref + val async_proofs_cmd_error_resilience : bool ref + val async_proofs_delegation_threshold : float ref + +end diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 3aa2cd707..c5ae27a11 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -103,8 +103,7 @@ 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 _) -> + | VernacDefinition ((Decl_kinds.DoDischarge,_),((_,i),_),ProveBody _) -> VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity,[i]), VtLater | VernacDefinition (_,((_,i),_),ProveBody _) -> VtStartProof(default_proof_mode (),GuaranteesOpacity,[i]), VtLater @@ -113,19 +112,29 @@ let rec classify_vernac e = 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) -> + | VernacFixpoint (discharge,l) -> + let guarantee = + match discharge with + | Decl_kinds.NoDischarge -> GuaranteesOpacity + | Decl_kinds.DoDischarge -> Doesn'tGuaranteeOpacity + 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 = + match discharge with + | Decl_kinds.NoDischarge -> GuaranteesOpacity + | Decl_kinds.DoDischarge -> Doesn'tGuaranteeOpacity + 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) -> @@ -176,12 +185,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,7 +201,7 @@ 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 () diff --git a/stm/workerLoop.ml b/stm/workerLoop.ml index 64121eb3d..704119186 100644 --- a/stm/workerLoop.ml +++ b/stm/workerLoop.ml @@ -6,6 +6,10 @@ (* * 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 @@ -15,5 +19,5 @@ let loop init args = let args = parse 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 53f745935..da2e6fe0c 100644 --- a/stm/workerLoop.mli +++ b/stm/workerLoop.mli @@ -6,4 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Default priority *) +val async_proofs_worker_priority : CoqworkmgrApi.priority ref + val loop : (unit -> unit) -> string list -> string list |