diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/asyncTaskQueue.ml | 22 | ||||
| -rw-r--r-- | stm/asyncTaskQueue.mli | 18 | ||||
| -rw-r--r-- | stm/coqworkmgrApi.ml | 5 | ||||
| -rw-r--r-- | stm/coqworkmgrApi.mli | 4 | ||||
| -rw-r--r-- | stm/dag.ml | 2 | ||||
| -rw-r--r-- | stm/dag.mli | 2 | ||||
| -rw-r--r-- | stm/proofBlockDelimiter.ml | 38 | ||||
| -rw-r--r-- | stm/proofBlockDelimiter.mli | 2 | ||||
| -rw-r--r-- | stm/spawned.ml | 2 | ||||
| -rw-r--r-- | stm/spawned.mli | 2 | ||||
| -rw-r--r-- | stm/stm.ml | 578 | ||||
| -rw-r--r-- | stm/stm.mli | 33 | ||||
| -rw-r--r-- | stm/tQueue.ml | 2 | ||||
| -rw-r--r-- | stm/tQueue.mli | 2 | ||||
| -rw-r--r-- | stm/vcs.ml | 2 | ||||
| -rw-r--r-- | stm/vcs.mli | 2 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 155 | ||||
| -rw-r--r-- | stm/vernac_classifier.mli | 2 | ||||
| -rw-r--r-- | stm/vio_checking.ml | 36 | ||||
| -rw-r--r-- | stm/vio_checking.mli | 2 | ||||
| -rw-r--r-- | stm/workerPool.ml | 18 | ||||
| -rw-r--r-- | stm/workerPool.mli | 7 |
22 files changed, 409 insertions, 527 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index d1bd3692ab..909804d0c9 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -115,7 +115,7 @@ module Make(T : Task) () = struct type process = Worker.process type extra = (T.task * cancel_switch) TQueue.t - let spawn id = + let spawn id priority = let name = Printf.sprintf "%s:%d" !T.name id in let proc, ic, oc = (* Filter arguments for slaves. *) @@ -123,9 +123,9 @@ module Make(T : Task) () = struct | [] -> !async_proofs_flags_for_workers @ ["-worker-id"; name; "-async-proofs-worker-priority"; - CoqworkmgrApi.(string_of_priority !async_proofs_worker_priority)] + CoqworkmgrApi.(string_of_priority priority)] (* Options to discard: 0 arguments *) - | ("-emacs"|"-emacs-U"|"-batch")::tl -> + | "-emacs"::tl -> set_slave_opt tl (* Options to discard: 1 argument *) | ( "-async-proofs" | "-vio2vo" | "-o" @@ -139,7 +139,7 @@ module Make(T : Task) () = struct (* We need to pass some options with one argument *) | ( "-I" | "-include" | "-top" | "-topfile" | "-coqlib" | "-exclude-dir" | "-compat" | "-load-ml-object" | "-load-ml-source" | "-require" | "-w" | "-color" | "-init-file" - | "-profile-ltac-cutoff" | "-main-channel" | "-control-channel" | "-mangle-names" + | "-profile-ltac-cutoff" | "-main-channel" | "-control-channel" | "-mangle-names" | "-set" | "-unset" | "-diffs" | "-mangle-name" | "-dump-glob" | "-bytecode-compiler" | "-native-compiler" as x) :: a :: tl -> x :: a :: set_slave_opt tl (* We need to pass some options with two arguments *) @@ -155,8 +155,8 @@ module Make(T : Task) () = struct let args = Array.of_list (set_slave_opt (List.tl (Array.to_list Sys.argv))) in let env = Array.append (T.extra_env ()) (Unix.environment ()) in - let worker_name = System.get_toplevel_path ("coq" ^ !T.name) in - Worker.spawn ~env worker_name args in + let worker_name = System.get_toplevel_path ("coq" ^ !T.name) in + Worker.spawn ~env worker_name args in name, proc, CThread.prepare_in_channel_for_thread_friendly_io ic, oc let manager cpanel (id, proc, ic, oc) = @@ -262,7 +262,7 @@ module Make(T : Task) () = struct cleaner : Thread.t option; } - let create size = + let create size priority = let cleaner queue = while true do try ignore(TQueue.pop ~picky:(fun (_,cancelled) -> !cancelled) queue) @@ -270,7 +270,7 @@ module Make(T : Task) () = struct done in let queue = TQueue.create () in { - active = Pool.create queue ~size; + active = Pool.create queue ~size priority; queue; cleaner = if size > 0 then Some (CThread.create cleaner queue) else None; } @@ -369,8 +369,8 @@ module Make(T : Task) () = struct (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 with_n_workers n priority f = + let q = create n priority 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 067ea5df0c..e6cf6343c8 100644 --- a/stm/asyncTaskQueue.mli +++ b/stm/asyncTaskQueue.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -68,10 +68,10 @@ module type Task = sig type request type response - (** UID of the task kind, for -toploop *) + (** UID of the task kind *) val name : string ref - (** Extra arguments of the task kind, for -toploop *) + (** Extra arguments of the task kind *) val extra_env : unit -> string array (** {5 Master API, it is run by the master, on a thread} *) @@ -144,10 +144,10 @@ module MakeQueue(T : Task) () : sig (** [queue] is the abstract queue type. *) type queue - (** [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 + (** [create n pri] will initialize the queue with [n] workers having + priority [pri]. 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 -> CoqworkmgrApi.priority -> queue (** [destroy q] Deallocates [q], cancelling all pending tasks. *) val destroy : queue -> unit @@ -203,9 +203,9 @@ module MakeQueue(T : Task) () : sig (** [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 + (** [with_n_workers n pri f] creates a queue, runs the function, destroys the queue. The user should call join *) - val with_n_workers : int -> (queue -> 'a) -> 'a + val with_n_workers : int -> CoqworkmgrApi.priority -> (queue -> 'a) -> 'a end diff --git a/stm/coqworkmgrApi.ml b/stm/coqworkmgrApi.ml index 841cc08c07..92dc77172f 100644 --- a/stm/coqworkmgrApi.ml +++ b/stm/coqworkmgrApi.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -13,7 +13,8 @@ let debug = false type priority = Low | High (* Default priority *) -let async_proofs_worker_priority = ref Low + +let default_async_proofs_worker_priority = Low let string_of_priority = function Low -> "low" | High -> "high" let priority_of_string = function diff --git a/stm/coqworkmgrApi.mli b/stm/coqworkmgrApi.mli index be5b291776..29eba5bc91 100644 --- a/stm/coqworkmgrApi.mli +++ b/stm/coqworkmgrApi.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -15,7 +15,7 @@ val string_of_priority : priority -> string val priority_of_string : string -> priority (* Default priority *) -val async_proofs_worker_priority : priority ref +val default_async_proofs_worker_priority : priority (* Connects to a work manager if any. If no worker manager, then -async-proofs-j and -async-proofs-tac-j are used *) diff --git a/stm/dag.ml b/stm/dag.ml index eb5063bf0c..4504de681b 100644 --- a/stm/dag.ml +++ b/stm/dag.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/stm/dag.mli b/stm/dag.mli index cae4fccc73..3a291c8d52 100644 --- a/stm/dag.mli +++ b/stm/dag.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index d13763cdec..a487799b74 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -41,21 +41,21 @@ let simple_goal sigma g gs = let open Evd in let open Evarutil in let evi = Evd.find sigma g in - Set.is_empty (evars_of_term (EConstr.Unsafe.to_constr evi.evar_concl)) && - Set.is_empty (evars_of_filtered_evar_info (nf_evar_info sigma evi)) && + Set.is_empty (evars_of_term sigma evi.evar_concl) && + Set.is_empty (evars_of_filtered_evar_info sigma (nf_evar_info sigma evi)) && not (List.exists (Proofview.depends_on sigma g) gs) let is_focused_goal_simple ~doc id = match state_of_id ~doc id with | `Expired | `Error _ | `Valid None -> `Not - | `Valid (Some { Vernacstate.proof }) -> - Option.cata (fun proof -> - let proof = Proof_global.give_me_the_proof proof in + | `Valid (Some { Vernacstate.lemmas }) -> + Option.cata (Vernacstate.LemmaStack.with_top_pstate ~f:(fun proof -> + let proof = Proof_global.get_proof proof in let Proof.{ goals=focused; stack=r1; shelf=r2; given_up=r3; sigma } = Proof.data proof in let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in if List.for_all (fun x -> simple_goal sigma x rest) focused then `Simple focused - else `Not) `Not proof + else `Not)) `Not lemmas type 'a until = [ `Stop | `Found of static_block_declaration | `Cont of 'a ] @@ -77,17 +77,18 @@ include Util (* ****************** - foo - bar - baz *********************************** *) let static_bullet ({ entry_point; prev_node } as view) = + let open Vernacexpr in assert (not (Vernacprop.has_Fail entry_point.ast)); - match Vernacprop.under_control entry_point.ast with - | Vernacexpr.VernacBullet b -> + match entry_point.ast.CAst.v.expr with + | 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 if Vernacprop.has_Fail node.ast then `Stop - else match Vernacprop.under_control node.ast with - | Vernacexpr.VernacBullet b' when b = b' -> + else match node.ast.CAst.v.expr with + | 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 } | _ -> `Stop) entry_point @@ -99,7 +100,7 @@ let dynamic_bullet doc { dynamic_switch = id; carry_on_data = b } = `ValidBlock { base_state = id; goals_to_admit = focused; - recovery_command = Some (Vernacexpr.VernacExpr([], Vernacexpr.VernacBullet (to_bullet_val b))) + recovery_command = Some (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacBullet (to_bullet_val b)}) } | `Not -> `Leaks @@ -109,16 +110,17 @@ let () = register_proof_block_delimiter (* ******************** { block } ***************************************** *) let static_curly_brace ({ entry_point; prev_node } as view) = - assert(Vernacprop.under_control entry_point.ast = Vernacexpr.VernacEndSubproof); + let open Vernacexpr in + assert(entry_point.ast.CAst.v.expr = VernacEndSubproof); crawl view (fun (nesting,prev) node -> if Vernacprop.has_Fail node.ast then `Cont (nesting,node) - else match Vernacprop.under_control node.ast with - | Vernacexpr.VernacSubproof _ when nesting = 0 -> + else match node.ast.CAst.v.expr with + | VernacSubproof _ when nesting = 0 -> `Found { block_stop = entry_point.id; block_start = prev.id; dynamic_switch = node.id; carry_on_data = unit_val } - | Vernacexpr.VernacSubproof _ -> + | VernacSubproof _ -> `Cont (nesting - 1,node) - | Vernacexpr.VernacEndSubproof -> + | VernacEndSubproof -> `Cont (nesting + 1,node) | _ -> `Cont (nesting,node)) (-1, entry_point) @@ -128,7 +130,7 @@ let dynamic_curly_brace doc { dynamic_switch = id } = `ValidBlock { base_state = id; goals_to_admit = focused; - recovery_command = Some (Vernacexpr.VernacExpr ([], Vernacexpr.VernacEndSubproof)) + recovery_command = Some (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacEndSubproof }) } | `Not -> `Leaks diff --git a/stm/proofBlockDelimiter.mli b/stm/proofBlockDelimiter.mli index eacd3687ae..e45f489a38 100644 --- a/stm/proofBlockDelimiter.mli +++ b/stm/proofBlockDelimiter.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/stm/spawned.ml b/stm/spawned.ml index bd772d825d..916139884b 100644 --- a/stm/spawned.ml +++ b/stm/spawned.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/stm/spawned.mli b/stm/spawned.mli index df4e725953..36612b1450 100644 --- a/stm/spawned.mli +++ b/stm/spawned.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/stm/stm.ml b/stm/stm.ml index d54a5fdf43..1042061021 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -27,6 +27,8 @@ open Feedback open Vernacexpr open Vernacextend +module PG_compat = Vernacstate.Proof_global [@@ocaml.warning "-3"] + let is_vtkeep = function VtKeep _ -> true | _ -> false let get_vtkeep = function VtKeep x -> x | _ -> assert false @@ -49,6 +51,8 @@ module AsyncOpts = struct async_proofs_tac_error_resilience : tac_error_filter; async_proofs_cmd_error_resilience : bool; async_proofs_delegation_threshold : float; + + async_proofs_worker_priority : CoqworkmgrApi.priority; } let default_opts = { @@ -65,6 +69,8 @@ module AsyncOpts = struct async_proofs_tac_error_resilience = `Only [ "curly" ]; async_proofs_cmd_error_resilience = true; async_proofs_delegation_threshold = 0.03; + + async_proofs_worker_priority = CoqworkmgrApi.Low; } let cur_opt = ref default_opts @@ -98,28 +104,26 @@ let forward_feedback, forward_feedback_hook = let unreachable_state, unreachable_state_hook = Hook.make ~default:(fun ~doc:_ _ _ -> ()) () +let document_add, document_add_hook = Hook.make + ~default:(fun _ _ -> ()) () + +let document_edit, document_edit_hook = Hook.make + ~default:(fun _ -> ()) () + +let sentence_exec, sentence_exec_hook = Hook.make + ~default:(fun _ -> ()) () + include Hook (* enables: Hooks.(call foo args) *) let call = get -let call_process_error_once = - let processed : unit Exninfo.t = Exninfo.make () in - fun (_, info as ei) -> - match Exninfo.get info processed with - | Some _ -> ei - | None -> - let e, info = ExplainErr.process_vernac_interp_error ei in - let info = Exninfo.add info processed () in - e, info - end let async_proofs_workers_extra_env = ref [||] type aast = { verbose : bool; - loc : Loc.t option; indentation : int; strlen : int; mutable expr : vernac_control; (* mutable: Proof using hinted by aux file *) @@ -139,8 +143,8 @@ let may_pierce_opaque = function | _ -> false let update_global_env () = - if Vernacstate.Proof_global.there_are_pending_proofs () then - Vernacstate.Proof_global.update_global_env () + if PG_compat.there_are_pending_proofs () then + PG_compat.update_global_env () module Vcs_ = Vcs.Make(Stateid.Self) type future_proof = Proof_global.closed_proof_output Future.computation @@ -198,7 +202,7 @@ let mkTransCmd cast cids ceff cqueue = (* Parts of the system state that are morally part of the proof state *) let summary_pstate = Evarutil.meta_counter_summary_tag, Evd.evar_counter_summary_tag, - Obligations.program_tcc_summary_tag + DeclareObl.program_tcc_summary_tag type cached_state = | EmptyState @@ -363,7 +367,6 @@ module VCS : sig val set_parsing_state : id -> Vernacstate.Parser.state -> unit val get_parsing_state : id -> Vernacstate.Parser.state option val get_proof_mode : id -> Pvernac.proof_mode option - val set_proof_mode : id -> Pvernac.proof_mode option -> unit (* cuts from start -> stop, raising Expired if some nodes are not there *) val slice : block_start:id -> block_stop:id -> vcs @@ -568,9 +571,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 - (match Vernacprop.under_control x with + (match x.CAst.v.Vernacexpr.expr with | VernacDefinition (_,({CAst.v=Name i},_),_) -> Id.to_string i | VernacStartTheoremProof (_,[({CAst.v=i},_),_]) -> Id.to_string i + | VernacInstance (({CAst.v=Name 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 @@ -610,7 +614,6 @@ end = struct (* {{{ *) info.state <- new_state let get_proof_mode id = (get_info id).proof_mode - let set_proof_mode id pm = (get_info id).proof_mode <- pm let reached id = let info = get_info id in @@ -872,18 +875,18 @@ end = struct (* {{{ *) let invalidate_cur_state () = cur_id := Stateid.dummy type proof_part = - Proof_global.t option * + Vernacstate.LemmaStack.t option * int * (* Evarutil.meta_counter_summary_tag *) int * (* Evd.evar_counter_summary_tag *) - Obligations.program_info Names.Id.Map.t (* Obligations.program_tcc_summary_tag *) + DeclareObl.program_info CEphemeron.key 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 proof_part_of_frozen { Vernacstate.lemmas; system } = let st = States.summary_of_state system in - proof, + lemmas, 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) @@ -947,17 +950,17 @@ end = struct (* {{{ *) try let prev = (VCS.visit id).next in if is_cached_and_valid prev - then { s with proof = - Vernacstate.Proof_global.copy_terminators - ~src:((get_cached prev).proof) ~tgt:s.proof } + then { s with lemmas = + PG_compat.copy_terminators + ~src:((get_cached prev).lemmas) ~tgt:s.lemmas } else s with VCS.Expired -> s in VCS.set_state id (FullState s) | `ProofOnly(ontop,(pstate,c1,c2,c3)) -> if is_cached_and_valid ontop then let s = get_cached ontop in - let s = { s with proof = - Vernacstate.Proof_global.copy_terminators ~src:s.proof ~tgt:pstate } in + let s = { s with lemmas = + PG_compat.copy_terminators ~src:s.lemmas ~tgt:pstate } in let s = { s with system = States.replace_summary s.system begin @@ -976,7 +979,6 @@ end = struct (* {{{ *) | Some _ -> (e, info) | None -> let loc = Loc.get_loc info in - let (e, info) = Hooks.(call_process_error_once (e, info)) in execution_error ?loc id (iprint (e, info)); (e, Stateid.add info ~valid id) @@ -1009,8 +1011,8 @@ end = struct (* {{{ *) if feedback_processed then Hooks.(call state_computed ~doc id ~in_cache:false); VCS.reached id; - if Vernacstate.Proof_global.there_are_pending_proofs () then - VCS.goals id (Vernacstate.Proof_global.get_open_goals ()) + if PG_compat.there_are_pending_proofs () then + VCS.goals id (PG_compat.get_open_goals ()) with e -> let (e, info) = CErrors.push e in let good_id = !cur_id in @@ -1051,133 +1053,38 @@ end = struct (* {{{ *) end (* }}} *) -(* indentation code for Show Script, initially contributed - * by D. de Rauglaudre. Should be moved away. - *) - -module ShowScript = struct - -let indent_script_item ((ng1,ngl1),nl,beginend,ppl) (cmd,ng) = - (* ng1 : number of goals remaining at the current level (before cmd) - ngl1 : stack of previous levels with their remaining goals - ng : number of goals after the execution of cmd - beginend : special indentation stack for { } *) - let ngprev = List.fold_left (+) ng1 ngl1 in - let new_ngl = - if ng > ngprev then - (* We've branched *) - (ng - ngprev + 1, ng1 - 1 :: ngl1) - else if ng < ngprev then - (* A subgoal have been solved. Let's compute the new current level - by discarding all levels with 0 remaining goals. *) - let rec loop = function - | (0, ng2::ngl2) -> loop (ng2,ngl2) - | p -> p - in loop (ng1-1, ngl1) - else - (* Standard case, same goal number as before *) - (ng1, ngl1) - in - (* When a subgoal have been solved, separate this block by an empty line *) - let new_nl = (ng < ngprev) - in - (* Indentation depth *) - let ind = List.length ngl1 - 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 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 - | _ -> ind, nl, beginend - in - let pp = Pp.( - (if nl then fnl () else mt ()) ++ - (hov (ind+1) (str (String.make ind ' ') ++ Ppvernac.pr_vernac cmd))) - in - (new_ngl, new_nl, new_beginend, pp :: ppl) - -let get_script prf = - let branch, test = - match prf with - | None -> VCS.Branch.master, fun _ -> true - | Some name -> VCS.current_branch (),fun nl -> nl=[] || List.mem name nl in - let rec find acc id = - if Stateid.equal id Stateid.initial || - Stateid.equal id Stateid.dummy then acc else - let view = VCS.visit id in - match view.step with - | `Fork((_,_,_,ns), _) when test ns -> acc - | `Qed (qed, proof) -> find [qed.qast.expr, (VCS.get_info id).n_goals] proof - | `Sideff (ReplayCommand x,_) -> - 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 - | `Cmd _ -> find acc view.next - | `Alias (id,_) -> find acc id - | `Fork _ -> find acc view.next - in - find [] (VCS.get_branch_pos branch) - -let warn_show_script_deprecated = - CWarnings.create ~name:"deprecated-show-script" ~category:"deprecated" - (fun () -> Pp.str "The “Show Script” command is deprecated.") - -let show_script ?proof () = - warn_show_script_deprecated (); - try - let prf = - try match proof with - | None -> Some (Vernacstate.Proof_global.get_current_proof_name ()) - | Some (p,_) -> Some (p.Proof_global.id) - with Vernacstate.Proof_global.NoCurrentProof -> None - in - let cmds = get_script prf in - let _,_,_,indented_cmds = - List.fold_left indent_script_item ((1,[]),false,[],[]) cmds - in - let indented_cmds = List.rev (indented_cmds) in - msg_notice Pp.(v 0 (prlist_with_sep fnl (fun x -> x) indented_cmds)) - with Vcs_aux.Expired -> () - -end +(* Wrapper for the proof-closing special path for Qed *) +let stm_qed_delay_proof ?route ~proof ~info ~id ~st ~loc ~control pending : Vernacstate.t = + set_id_for_feedback ?route dummy_doc id; + Vernacentries.interp_qed_delayed_proof ~proof ~info ~st ~control (CAst.make ?loc pending) (* 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 } : Vernacstate.t = +let stm_vernac_interp ?route id st { verbose; 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 *) set_id_for_feedback ?route dummy_doc id; - Aux_file.record_in_aux_set_at ?loc (); + Aux_file.record_in_aux_set_at ?loc:expr.CAst.loc (); (* 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 is_filtered_command = function | VernacResetName _ | VernacResetInitial | VernacBack _ - | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _ + | VernacRestart | VernacUndo _ | VernacUndoTo _ | VernacAbortAll | VernacAbort _ -> true | _ -> false in - let aux_interp st expr = - (* XXX unsupported attributes *) - 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 (CAst.make ?loc expr) - with e -> - let e = CErrors.push e in - Exninfo.iraise Hooks.(call_process_error_once e) - in aux_interp st expr + (* XXX unsupported attributes *) + let cmd = expr.CAst.v.expr in + if is_filtered_command cmd then + (stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr); st) + else begin + stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr); + Vernacentries.interp ?verbosely:(Some verbose) ~st expr + end (****************************** CRUFT *****************************************) (******************************************************************************) @@ -1193,6 +1100,7 @@ module Backtrack : sig (* Returns the state that the command should backtract to *) val undo_vernac_classifier : vernac_control -> doc:doc -> Stateid.t val get_prev_proof : doc:doc -> Stateid.t -> Proof.t option + val get_proof : doc:doc -> Stateid.t -> Proof.t option end = struct (* {{{ *) @@ -1233,7 +1141,7 @@ end = struct (* {{{ *) | { step = `Fork ((_,_,_,l),_) } -> l, false,0 | { step = `Cmd { cids = l; ctac } } -> l, ctac,0 | { step = `Alias (_,{ expr }) } when not (Vernacprop.has_Fail expr) -> - begin match Vernacprop.under_control expr with + begin match expr.CAst.v.expr with | VernacUndo n -> [], false, n | _ -> [],false,0 end @@ -1256,14 +1164,14 @@ end = struct (* {{{ *) let get_proof ~doc id = match state_of_id ~doc id with - | `Valid (Some vstate) -> Option.map Proof_global.give_me_the_proof vstate.Vernacstate.proof + | `Valid (Some vstate) -> Option.map (Vernacstate.LemmaStack.with_top_pstate ~f:Proof_global.get_proof) vstate.Vernacstate.lemmas | _ -> None let undo_vernac_classifier v ~doc = if not (VCS.is_interactive ()) && !cur_opt.async_proofs_cache <> Some Force then undo_costly_in_batch_mode v; try - match Vernacprop.under_control v with + match v.CAst.v.expr with | VernacResetInitial -> Stateid.initial | VernacResetName {CAst.v=name} -> @@ -1295,7 +1203,7 @@ end = struct (* {{{ *) | Some vcs, _ -> vcs in let cb, _ = try Vcs_aux.find_proof_at_depth vcs (Vcs_aux.proof_nesting vcs) - with Failure _ -> raise Vernacstate.Proof_global.NoCurrentProof in + with Failure _ -> raise PG_compat.NoCurrentProof in let n = fold_until (fun n (_,vcs,_,_,_) -> if List.mem cb (Vcs_.branches vcs) then `Cont (n+1) else `Stop n) 0 id in @@ -1308,8 +1216,6 @@ end = struct (* {{{ *) match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ()) () id in oid - | VernacBackTo id -> - Stateid.of_int id | _ -> anomaly Pp.(str "incorrect VtMeta classification") with | Not_found -> @@ -1333,11 +1239,12 @@ end = struct (* {{{ *) | None -> true done; !rv - with Not_found | Vernacstate.Proof_global.NoCurrentProof -> None + with Not_found | PG_compat.NoCurrentProof -> None end (* }}} *) let get_prev_proof = Backtrack.get_prev_proof +let get_proof = Backtrack.get_proof let hints = ref Aux_file.empty_aux_file let set_compilation_hints file = @@ -1594,7 +1501,7 @@ end = struct (* {{{ *) let wall_clock2 = Unix.gettimeofday () in Aux_file.record_in_aux_at ?loc "proof_build_time" (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1)); - let p = Vernacstate.Proof_global.return_proof ~allow_partial:drop_pt () in + let p = PG_compat.return_proof ~allow_partial:drop_pt () in if drop_pt then feedback ~id Complete; p) @@ -1620,16 +1527,12 @@ end = struct (* {{{ *) (* Unfortunately close_future_proof and friends are not pure so we need to set the state manually here *) State.unfreeze st; - let pobject, _ = - Vernacstate.Proof_global.close_future_proof ~opaque ~feedback_id:stop (Future.from_val ~fix_exn p) in - let terminator = (* The one sent by master is an InvalidKey *) - Lemmas.(standard_proof_terminator []) in + let pobject, _info = + PG_compat.close_future_proof ~opaque ~feedback_id:stop (Future.from_val ~fix_exn p) in let st = Vernacstate.freeze_interp_state ~marshallable:false in - stm_vernac_interp stop - ~proof:(pobject, terminator) st - { verbose = false; loc; indentation = 0; strlen = 0; - expr = VernacExpr ([], VernacEndProof (Proved (opaque,None))) }) in + stm_qed_delay_proof ~st ~id:stop + ~proof:pobject ~info:(Lemmas.Info.make ()) ~loc ~control:[] (Proved (opaque,None))) in ignore(Future.join checked_proof); end; (* STATE: Restore the state XXX: handle exn *) @@ -1651,7 +1554,7 @@ end = struct (* {{{ *) let perform_states query = if query = [] then [] else let is_tac e = match Vernac_classifier.classify_vernac e with - | VtProofStep _, _ -> true + | VtProofStep _ -> true | _ -> false in let initial = @@ -1717,7 +1620,7 @@ and Slaves : sig val wait_all_done : unit -> unit (* initialize the whole machinery (optional) *) - val init : unit -> unit + val init : CoqworkmgrApi.priority -> unit type 'a tasks = (('a,VCS.vcs) Stateid.request * bool) list val dump_snapshot : unit -> Future.UUID.t tasks @@ -1725,7 +1628,7 @@ and Slaves : sig val info_tasks : 'a tasks -> (string * float * int) list val finish_task : string -> - Library.seg_univ -> Library.seg_discharge -> Library.seg_proofs -> + Library.seg_univ -> Library.seg_proofs -> int tasks -> int -> Library.seg_univ val cancel_worker : WorkerPool.worker_id -> unit @@ -1739,11 +1642,11 @@ end = struct (* {{{ *) module TaskQueue = AsyncTaskQueue.MakeQueue(ProofTask) () let queue = ref None - let init () = + let init priority = if async_proofs_is_master !cur_opt then - queue := Some (TaskQueue.create !cur_opt.async_proofs_n_workers) + queue := Some (TaskQueue.create !cur_opt.async_proofs_n_workers priority) else - queue := Some (TaskQueue.create 0) + queue := Some (TaskQueue.create 0 priority) let check_task_aux extra name l i = let { Stateid.stop; document; loc; name = r_name }, drop = List.nth l i in @@ -1758,17 +1661,20 @@ end = struct (* {{{ *) try Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:false stop; if drop then - let _proof = Vernacstate.Proof_global.return_proof ~allow_partial:true () in + let _proof = PG_compat.return_proof ~allow_partial:true () in `OK_ADMITTED else begin + let opaque = Proof_global.Opaque in + (* The original terminator, a hook, has not been saved in the .vio*) - Vernacstate.Proof_global.set_terminator (Lemmas.standard_proof_terminator []); + let proof, _info = + PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in + + let info = Lemmas.Info.make () in - let opaque = Proof_global.Opaque in - let proof = - Vernacstate.Proof_global.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in (* We jump at the beginning since the kernel handles side effects by also * looking at the ones that happen to be present in the current env *) + Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:false start; (* STATE SPEC: * - start: First non-expired state! [This looks very fishy] @@ -1777,9 +1683,7 @@ end = struct (* {{{ *) *) (* STATE We use the state resulting from reaching start. *) let st = Vernacstate.freeze_interp_state ~marshallable:false in - ignore(stm_vernac_interp stop ~proof st - { verbose = false; loc; indentation = 0; strlen = 0; - expr = VernacExpr ([], VernacEndProof (Proved (opaque,None))) }); + ignore(stm_qed_delay_proof ~id:stop ~st ~proof ~info ~loc ~control:[] (Proved (opaque,None))); `OK proof end with e -> @@ -1791,10 +1695,11 @@ end = struct (* {{{ *) spc () ++ iprint (e, info)) | Some (_, cur) -> match VCS.visit cur with - | { step = `Cmd { cast = { loc } } } - | { step = `Fork (( { loc }, _, _, _), _) } - | { step = `Qed ( { qast = { loc } }, _) } - | { step = `Sideff (ReplayCommand { loc }, _) } -> + | { step = `Cmd { cast } } + | { step = `Fork (( cast, _, _, _), _) } + | { step = `Qed ( { qast = cast }, _) } + | { step = `Sideff (ReplayCommand cast, _) } -> + let loc = cast.expr.CAst.loc in let start, stop = Option.cata Loc.unloc (0,0) loc in msg_warning Pp.( str"File " ++ str name ++ str ": proof of " ++ str r_name ++ @@ -1809,40 +1714,39 @@ end = struct (* {{{ *) str (Printexc.to_string e))); if drop then `ERROR_ADMITTED else `ERROR - let finish_task name (u,cst,_) d p l i = + let finish_task name (cst,_) p l i = let { Stateid.uuid = bucket }, drop = List.nth l i in let bucket_name = if bucket < 0 then (assert drop; ", no bucket") else Printf.sprintf ", bucket %d" bucket in match check_task_aux bucket_name name l i with | `ERROR -> exit 1 - | `ERROR_ADMITTED -> u, cst, false - | `OK_ADMITTED -> u, cst, false - | `OK (po,_) -> - let discharge c = List.fold_right Cooking.cook_constr d.(bucket) c in - let con = - Nametab.locate_constant - (Libnames.qualid_of_ident po.Proof_global.id) in + | `ERROR_ADMITTED -> cst, false + | `OK_ADMITTED -> cst, false + | `OK { Proof_global.name } -> + let con = Nametab.locate_constant (Libnames.qualid_of_ident name) in let c = Global.lookup_constant con in let o = match c.Declarations.const_body with | Declarations.OpaqueDef o -> o | _ -> assert false in - let uc = - Option.get - (Opaqueproof.get_constraints (Global.opaque_tables ()) o) in + (* No need to delay the computation, the future has been forced by + the call to [check_task_aux] above. *) + let uc = Opaqueproof.force_constraints Library.indirect_accessor (Global.opaque_tables ()) o in + let uc = Univ.hcons_universe_context_set uc in + let (pr, priv, ctx) = Option.get (Global.body_of_constant_body Library.indirect_accessor c) in (* We only manipulate monomorphic terms here. *) - let map (c, ctx) = assert (Univ.AUContext.is_empty ctx); c in - let pr = - Future.from_val (map (Option.get (Global.body_of_constant_body c))) in - let uc = - Future.chain uc Univ.hcons_universe_context_set in - let pr = Future.chain pr discharge in - let pr = Future.chain pr Constr.hcons in - Future.sink pr; - let extra = Future.join uc in - u.(bucket) <- uc; - p.(bucket) <- pr; - u, Univ.ContextSet.union cst extra, false + let () = assert (Univ.AUContext.is_empty ctx) in + let () = match priv with + | Opaqueproof.PrivateMonomorphic () -> () + | Opaqueproof.PrivatePolymorphic (univs, uctx) -> + let () = assert (Int.equal (Univ.AUContext.size ctx) univs) in + assert (Univ.ContextSet.is_empty uctx) + in + let pr = Constr.hcons pr in + let (ci, dummy) = p.(bucket) in + let () = assert (Option.is_empty dummy) in + p.(bucket) <- ci, Some (pr, priv); + Univ.ContextSet.union cst uc, false let check_task name l i = match check_task_aux "" name l i with @@ -2016,7 +1920,7 @@ end = struct (* {{{ *) try Reach.known_state ~doc:dummy_doc (* XXX should be vcs *) ~cache:false id; State.purify (fun () -> - let Proof.{sigma=sigma0} = Proof.data (Vernacstate.Proof_global.give_me_the_proof ()) in + let Proof.{sigma=sigma0} = Proof.data (PG_compat.give_me_the_proof ()) in let g = Evd.find sigma0 r_goal in let is_ground c = Evarutil.is_ground_term sigma0 c in if not ( @@ -2028,7 +1932,7 @@ end = struct (* {{{ *) "goals only")) else begin let (i, ast) = r_ast in - Vernacstate.Proof_global.simple_with_current_proof (fun _ p -> Proof.focus focus_cond () i p); + PG_compat.map_proof (fun p -> Proof.focus focus_cond () i p); (* STATE SPEC: * - start : id * - return: id @@ -2037,7 +1941,7 @@ end = struct (* {{{ *) *) let st = Vernacstate.freeze_interp_state ~marshallable:false in ignore(stm_vernac_interp r_state_fb st ast); - let Proof.{sigma} = Proof.data (Vernacstate.Proof_global.give_me_the_proof ()) in + let Proof.{sigma} = Proof.data (PG_compat.give_me_the_proof ()) in match Evd.(evar_body (find sigma r_goal)) with | Evd.Evar_empty -> RespNoProgress | Evd.Evar_defined t -> @@ -2058,7 +1962,7 @@ and Partac : sig val vernac_interp : solve:bool -> abstract:bool -> cancel_switch:AsyncTaskQueue.cancel_switch -> - int -> Stateid.t -> Stateid.t -> aast -> unit + int -> CoqworkmgrApi.priority -> Stateid.t -> Stateid.t -> aast -> unit end = struct (* {{{ *) @@ -2070,21 +1974,22 @@ end = struct (* {{{ *) else f () - let vernac_interp ~solve ~abstract ~cancel_switch nworkers safe_id id - { indentation; verbose; loc; expr = e; strlen } : unit + let vernac_interp ~solve ~abstract ~cancel_switch nworkers priority safe_id id + { indentation; verbose; expr = e; strlen } : unit = - let e, time, batch, fail = - let rec find ~time ~batch ~fail = function - | VernacTime (batch,{CAst.v=e}) -> find ~time:true ~batch ~fail e - | VernacRedirect (_,{CAst.v=e}) -> find ~time ~batch ~fail e - | VernacFail {CAst.v=e} -> find ~time ~batch ~fail:true e - | e -> e, time, batch, fail in - find ~time:false ~batch:false ~fail:false e in + let cl, time, batch, fail = + let rec find ~time ~batch ~fail cl = match cl with + | ControlTime batch :: cl -> find ~time:true ~batch ~fail cl + | ControlRedirect _ :: cl -> find ~time ~batch ~fail cl + | ControlFail :: cl -> find ~time ~batch ~fail:true cl + | cl -> cl, time, batch, fail in + find ~time:false ~batch:false ~fail:false e.CAst.v.control in + let e = CAst.map (fun cmd -> { cmd with control = cl }) e in let st = Vernacstate.freeze_interp_state ~marshallable:false in stm_fail ~st fail (fun () -> (if time then System.with_time ~batch ~header:(Pp.mt ()) else (fun x -> x)) (fun () -> - ignore(TaskQueue.with_n_workers nworkers (fun queue -> - Vernacstate.Proof_global.with_current_proof (fun _ p -> + TaskQueue.with_n_workers nworkers priority (fun queue -> + PG_compat.map_proof (fun p -> let Proof.{goals} = Proof.data p in let open TacTask in let res = CList.map_i (fun i g -> @@ -2092,7 +1997,7 @@ end = struct (* {{{ *) Future.create_delegate ~name:(Printf.sprintf "subgoal %d" i) (State.exn_on id ~valid:safe_id) in - let t_ast = (i, { indentation; verbose; loc; expr = e; strlen }) in + let t_ast = (i, { indentation; verbose; expr = e; strlen }) in let t_name = Goal.uid g in TaskQueue.enqueue_task queue { t_state = safe_id; t_state_fb = id; @@ -2117,7 +2022,7 @@ end = struct (* {{{ *) let open Notations in match Future.join f with | Some (pt, uc) -> - let sigma, env = Vernacstate.Proof_global.get_current_context () in + let sigma, env = PG_compat.get_current_context () in stm_pperr_endline (fun () -> hov 0 ( str"g=" ++ int (Evar.repr gid) ++ spc () ++ str"t=" ++ (Printer.pr_constr_env env sigma pt) ++ spc () ++ @@ -2129,7 +2034,8 @@ end = struct (* {{{ *) if solve then Tacticals.New.tclSOLVE [] else tclUNIT () end) in - Proof.run_tactic (Global.env()) assign_tac p)))) ()) + let p,_,() = Proof.run_tactic (Global.env()) assign_tac p in + p))) ()) end (* }}} *) @@ -2197,7 +2103,7 @@ end (* }}} *) and Query : sig - val init : unit -> unit + val init : CoqworkmgrApi.priority -> unit val vernac_interp : cancel_switch:AsyncTaskQueue.cancel_switch -> Stateid.t -> Stateid.t -> aast -> unit end = struct (* {{{ *) @@ -2211,7 +2117,7 @@ end = struct (* {{{ *) TaskQueue.enqueue_task (Option.get !queue) QueryTask.({ t_where = prev; t_for = id; t_what = q }) ~cancel_switch - let init () = queue := Some (TaskQueue.create 0) + let init priority = queue := Some (TaskQueue.create 0 priority) end (* }}} *) @@ -2241,19 +2147,19 @@ let collect_proof keep cur hd brkind id = let name = function | [] -> no_name | id :: _ -> Names.Id.to_string id in - let loc = (snd cur).loc in + let loc = (snd cur).expr.CAst.loc in let is_defined_expr = function | VernacEndProof (Proved (Proof_global.Transparent,_)) -> true | _ -> false in let is_defined = function - | _, { expr = e } -> is_defined_expr (Vernacprop.under_control e) + | _, { expr = e } -> is_defined_expr e.CAst.v.expr && (not (Vernacprop.has_Fail e)) in let proof_using_ast = function | VernacProof(_,Some _) -> true | _ -> false in let proof_using_ast = function - | Some (_, v) when proof_using_ast (Vernacprop.under_control v.expr) + | Some (_, v) when proof_using_ast v.expr.CAst.v.expr && (not (Vernacprop.has_Fail v.expr)) -> Some v | _ -> None in let has_proof_using x = proof_using_ast x <> None in @@ -2262,14 +2168,14 @@ let collect_proof keep cur hd brkind id = | _ -> assert false in let proof_no_using = function - | Some (_, v) -> proof_no_using (Vernacprop.under_control v.expr), v + | Some (_, v) -> proof_no_using v.expr.CAst.v.expr, v | _ -> assert false in let has_proof_no_using = function | VernacProof(_,None) -> true | _ -> false in let has_proof_no_using = function - | Some (_, v) -> has_proof_no_using (Vernacprop.under_control v.expr) + | Some (_, v) -> has_proof_no_using v.expr.CAst.v.expr && (not (Vernacprop.has_Fail v.expr)) | _ -> false in let too_complex_to_delegate = function @@ -2286,7 +2192,7 @@ 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 (Vernacprop.under_control x.expr) -> + when too_complex_to_delegate x.expr.CAst.v.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 @@ -2307,7 +2213,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 <- VernacExpr([], VernacProof(t, Some hint)); + v.expr <- CAst.map (fun _ -> { control = []; attrs = []; expr = VernacProof(t, Some hint)}) v.expr; `ASync (parent last,accn,name,delegate name) with Not_found -> let name = name ids in @@ -2330,7 +2236,7 @@ let collect_proof keep cur hd brkind id = | _ -> false in match cur, (VCS.visit id).step, brkind with - | (parent, x), `Fork _, _ when is_vernac_exact (Vernacprop.under_control x.expr) + | (parent, x), `Fork _, _ when is_vernac_exact x.expr.CAst.v.expr && (not (Vernacprop.has_Fail x.expr)) -> `Sync (no_name,`Immediate) | _, _, { VCS.kind = `Edit _ } -> check_policy (collect (Some cur) [] id) @@ -2398,9 +2304,9 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = Proofview.give_up else Proofview.tclUNIT () end in match (VCS.get_info base_state).state with - | FullState { Vernacstate.proof } -> - Option.iter Vernacstate.Proof_global.unfreeze proof; - Vernacstate.Proof_global.with_current_proof (fun _ p -> + | FullState { Vernacstate.lemmas } -> + Option.iter PG_compat.unfreeze lemmas; + PG_compat.with_current_proof (fun _ p -> feedback ~id:id Feedback.AddedAxiom; fst (Pfedit.solve Goal_select.SelectAll None tac p), ()); (* STATE SPEC: @@ -2410,7 +2316,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = (* STATE: We use an updated state with proof *) let st = Vernacstate.freeze_interp_state ~marshallable:false in Option.iter (fun expr -> ignore(stm_vernac_interp id st { - verbose = true; loc = None; expr; indentation = 0; + verbose = true; expr; indentation = 0; strlen = 0 } )) recovery_command | _ -> assert false @@ -2441,6 +2347,14 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = try f x with e when CErrors.noncritical e -> () in + (* extract proof_ending in qed case, note that `Abort` and `Proof + term.` could also fail in this case, however that'd be a bug I do + believe as proof injection shouldn't happen here. *) + let extract_pe (x : aast) = + match x.expr.CAst.v.expr with + | VernacEndProof pe -> x.expr.CAst.v.control, pe + | _ -> CErrors.anomaly Pp.(str "Non-qed command classified incorrectly") in + (* ugly functions to process nested lemmas, i.e. hard to reproduce * side effects *) let cherry_pick_non_pstate () = @@ -2481,7 +2395,8 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = resilient_tactic id cblock (fun () -> reach ~cache:true view.next; Partac.vernac_interp ~solve ~abstract ~cancel_switch - !cur_opt.async_proofs_n_tacworkers view.next id x) + !cur_opt.async_proofs_n_tacworkers + !cur_opt.async_proofs_worker_priority view.next id x) ), cache, true | `Cmd { cast = x; cqueue = `QueryQueue cancel_switch } when async_proofs_is_master !cur_opt -> (fun () -> @@ -2494,8 +2409,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = (* State resulting from reach *) let st = Vernacstate.freeze_interp_state ~marshallable:false in ignore(stm_vernac_interp id st x) - ); - if eff then update_global_env () + ) ), eff || cache, true | `Cmd { cast = x; ceff = eff } -> (fun () -> (match !cur_opt.async_proofs_mode with @@ -2503,8 +2417,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = resilient_command reach view.next | APoff -> reach view.next); let st = Vernacstate.freeze_interp_state ~marshallable:false in - ignore(stm_vernac_interp id st x); - if eff then update_global_env () + ignore(stm_vernac_interp id st x) ), eff || cache, true | `Fork ((x,_,_,_), None) -> (fun () -> resilient_command reach view.next; @@ -2530,7 +2443,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = | `ASync (block_start, nodes, name, delegate) -> (fun () -> let keep' = get_vtkeep keep in let drop_pt = keep' == VtKeepAxiom in - let block_stop, exn_info, loc = eop, (id, eop), x.loc in + let block_stop, exn_info, loc = eop, (id, eop), x.expr.CAst.loc in log_processing_async id name; VCS.create_proof_task_box nodes ~qed:id ~block_start; begin match brinfo, qed.fproof with @@ -2569,28 +2482,30 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = Proof_global.Opaque (* Admitted -> Opaque should be OK. *) | VtKeepDefined -> Proof_global.Transparent in - let proof = - Vernacstate.Proof_global.close_future_proof ~opaque ~feedback_id:id fp in + let proof, info = + PG_compat.close_future_proof ~opaque ~feedback_id:id fp in if not delegate then ignore(Future.compute fp); reach view.next; let st = Vernacstate.freeze_interp_state ~marshallable:false in - ignore(stm_vernac_interp id ~proof st x); + let control, pe = extract_pe x in + ignore(stm_qed_delay_proof ~id ~st ~proof ~info ~loc ~control pe); feedback ~id:id Incomplete | { VCS.kind = `Master }, _ -> assert false end; - Vernacstate.Proof_global.discard_all () + PG_compat.discard_all () ), not redefine_qed, true | `Sync (name, `Immediate) -> (fun () -> reach eop; let st = Vernacstate.freeze_interp_state ~marshallable:false in ignore(stm_vernac_interp id st x); - Vernacstate.Proof_global.discard_all () + PG_compat.discard_all () ), true, true | `Sync (name, reason) -> (fun () -> log_processing_sync id name reason; reach eop; let wall_clock = Unix.gettimeofday () in - record_pb_time name ?loc:x.loc (wall_clock -. !wall_clock_last_fork); + let loc = x.expr.CAst.loc in + record_pb_time name ?loc (wall_clock -. !wall_clock_last_fork); let proof = match keep with | VtDrop -> None @@ -2603,18 +2518,23 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = | VtKeepOpaque -> Opaque | VtKeepDefined -> Transparent | VtKeepAxiom -> assert false in - Some(Vernacstate.Proof_global.close_proof ~opaque + Some(PG_compat.close_proof ~opaque ~keep_body_ucst_separate:false (State.exn_on id ~valid:eop)) in if keep <> VtKeep VtKeepAxiom then reach view.next; let wall_clock2 = Unix.gettimeofday () in let st = Vernacstate.freeze_interp_state ~marshallable:false in - ignore(stm_vernac_interp id ?proof st x); + let _st = match proof with + | None -> stm_vernac_interp id st x + | Some (proof, info) -> + let control, pe = extract_pe x in + stm_qed_delay_proof ~id ~st ~proof ~info ~loc ~control pe + in let wall_clock3 = Unix.gettimeofday () in - Aux_file.record_in_aux_at ?loc:x.loc "proof_check_time" + Aux_file.record_in_aux_at ?loc:x.expr.CAst.loc "proof_check_time" (Printf.sprintf "%.3f" (wall_clock3 -. wall_clock2)); - Vernacstate.Proof_global.discard_all () + PG_compat.discard_all () ), true, true | `MaybeASync (start, nodes, name, delegate) -> (fun () -> reach ~cache:true start; @@ -2628,8 +2548,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = | `Sideff (ReplayCommand x,_) -> (fun () -> reach view.next; let st = Vernacstate.freeze_interp_state ~marshallable:false in - ignore(stm_vernac_interp id st x); - update_global_env () + ignore(stm_vernac_interp id st x) ), cache, true | `Sideff (CherryPickEnv, origin) -> (fun () -> reach view.next; @@ -2650,16 +2569,16 @@ end (* }}} *) (********************************* STM API ************************************) (******************************************************************************) -(* Main initalization routine *) +(* Main initialization 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 + specified [doc_type]. This distinction should disappear 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; + iload_path : Loadpath.coq_path list; (* Require [require_libs] before the initial state is ready. Parameters follow [Library], that is to say, @@ -2691,20 +2610,17 @@ let dirpath_of_file f = Loadpath.logical lp with Not_found -> Libnames.default_root_prefix in - let file = Filename.chop_extension (Filename.basename f) in - let id = Id.of_string file in + let f = try Filename.chop_extension (Filename.basename f) with Invalid_argument _ -> f in + let id = Id.of_string f in let ldir = Libnames.add_dirpath_suffix ldir0 id in ldir 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_of_string dir in - let mfrom = Option.map Libnames.qualid_of_string from in - Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] in - List.(iter rq_file (rev libs)) - in + let require_file (dir, from, exp) = + let mp = Libnames.qualid_of_string dir in + let mfrom = Option.map Libnames.qualid_of_string from in + Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] in (* Set the options from the new documents *) AsyncOpts.cur_opt := stm_options; @@ -2717,7 +2633,7 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = (* 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; + List.iter Loadpath.add_coq_path iload_path; Safe_typing.allow_delayed_constants := !cur_opt.async_proofs_mode <> APoff; @@ -2743,15 +2659,15 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = end; (* Import initial libraries. *) - load_objs require_libs; + List.iter require_file require_libs; (* We record the state at this point! *) State.define ~doc ~cache:true ~redefine:true (fun () -> ()) Stateid.initial; Backtrack.record (); - Slaves.init (); + Slaves.init stm_options.async_proofs_worker_priority; if async_proofs_is_master !cur_opt then begin stm_prerr_endline (fun () -> "Initializing workers"); - Query.init (); + Query.init stm_options.async_proofs_worker_priority; let opts = match !cur_opt.async_proofs_private_flags with | None -> [] | Some s -> Str.split_delim (Str.regexp ",") s in @@ -2765,6 +2681,7 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = doc, VCS.cur_tip () let observe ~doc id = + Hooks.(call sentence_exec id); let vcs = VCS.backup () in try Reach.known_state ~doc ~cache:(VCS.is_interactive ()) id; @@ -2835,16 +2752,16 @@ let check_task name (tasks,rcbackup) i = with e when CErrors.noncritical e -> VCS.restore vcs; false let info_tasks (tasks,_) = Slaves.info_tasks tasks -let finish_tasks name u d p (t,rcbackup as tasks) = +let finish_tasks name u p (t,rcbackup as tasks) = RemoteCounter.restore rcbackup; let finish_task u (_,_,i) = let vcs = VCS.backup () in - let u = State.purify (Slaves.finish_task name u d p t) i in + let u = State.purify (Slaves.finish_task name u p t) i in VCS.restore vcs; u in try - let u, a, _ = List.fold_left finish_task u (info_tasks tasks) in - (u,a,true), p + let a, _ = List.fold_left finish_task u (info_tasks tasks) in + (a,true), p with e -> let e = CErrors.push e in msg_warning (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e); @@ -2875,7 +2792,7 @@ let merge_proof_branch ~valid ?id qast keep brname = VCS.checkout VCS.Branch.master; `Unfocus qed_id | { VCS.kind = `Master } -> - Exninfo.iraise (State.exn_on ~valid Stateid.dummy (Vernacstate.Proof_global.NoCurrentProof, Exninfo.null)) + Exninfo.iraise (State.exn_on ~valid Stateid.dummy (PG_compat.NoCurrentProof, Exninfo.null)) (* When tty is true, this code also does some of the job of the user interface: jump back to a state that is valid *) @@ -2932,7 +2849,7 @@ let get_allow_nested_proofs = (** [process_transaction] adds a node in the document *) let process_transaction ~doc ?(newtip=Stateid.fresh ()) - ({ verbose; loc; expr } as x) c = + ({ verbose; expr } as x) c = stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x); let vcs = VCS.backup () in try @@ -2946,31 +2863,31 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) " classified as: " ^ Vernac_classifier.string_of_vernac_classification c); match c with (* Meta *) - | VtMeta, _ -> + | VtMeta -> let id = Backtrack.undo_vernac_classifier expr ~doc in process_back_meta_command ~newtip ~head id x (* Query *) - | VtQuery, w -> + | VtQuery -> let id = VCS.new_node ~id:newtip proof_mode () in let queue = if VCS.is_vio_doc () && VCS.((get_branch head).kind = `Master) && - may_pierce_opaque (Vernacprop.under_control x.expr) + may_pierce_opaque x.expr.CAst.v.expr then `SkipQueue else `MainQueue in VCS.commit id (mkTransCmd x [] false queue); VCS.set_parsing_state id head_parsing; - Backtrack.record (); assert (w == VtLater); `Ok + Backtrack.record (); `Ok (* Proof *) - | VtStartProof (guarantee, names), w -> + | VtStartProof (guarantee, names) -> if not (get_allow_nested_proofs ()) && VCS.proof_nesting () > 0 then "Nested proofs are not allowed unless you turn option Nested Proofs Allowed on." |> Pp.str |> (fun s -> (UserError (None, s), Exninfo.null)) - |> State.exn_on ~valid:Stateid.dummy Stateid.dummy + |> State.exn_on ~valid:Stateid.dummy newtip |> Exninfo.iraise else @@ -2986,9 +2903,9 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) VCS.merge id ~ours:(Fork (x, bname, guarantee, names)) head end; VCS.set_parsing_state id head_parsing; - Backtrack.record (); assert (w == VtLater); `Ok + Backtrack.record (); `Ok - | VtProofStep { parallel; proof_block_detection = cblock }, w -> + | VtProofStep { parallel; proof_block_detection = cblock } -> let id = VCS.new_node ~id:newtip proof_mode () in let queue = match parallel with @@ -3000,18 +2917,18 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) detection should occur here. detect_proof_block id cblock; *) VCS.set_parsing_state id head_parsing; - Backtrack.record (); assert (w == VtLater); `Ok + Backtrack.record (); `Ok - | VtQed keep, w -> + | VtQed keep -> let valid = VCS.get_branch_pos head in let rc = merge_proof_branch ~valid ~id:newtip x keep head in VCS.checkout_shallowest_proof_branch (); - Backtrack.record (); assert (w == VtLater); + Backtrack.record (); rc (* Side effect in a (still open) proof is replayed on all branches*) - | VtSideff l, w -> + | VtSideff (l, w) -> let id = VCS.new_node ~id:newtip proof_mode () in let new_ids = match (VCS.get_branch head).VCS.kind with @@ -3022,7 +2939,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) VCS.commit id (mkTransCmd x l true `MainQueue); (* We can't replay a Definition since universes may be differently * inferred. This holds in Coq >= 8.5 *) - let action = match Vernacprop.under_control x.expr with + let action = match x.expr.CAst.v.expr with | VernacDefinition(_, _, DefineBody _) -> CherryPickEnv | _ -> ReplayCommand x in VCS.propagate_sideff ~action @@ -3047,63 +2964,13 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) VCS.set_parsing_state id parsing_state) new_ids; `Ok - (* Unknown: we execute it, check for open goals and propagate sideeff *) - | VtUnknown, VtNow -> - let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in - if not (get_allow_nested_proofs ()) && in_proof then - "Commands which may open proofs are not allowed in a proof unless you turn option Nested Proofs Allowed on." - |> Pp.str - |> (fun s -> (UserError (None, s), Exninfo.null)) - |> State.exn_on ~valid:Stateid.dummy Stateid.dummy - |> Exninfo.iraise - else - let id = VCS.new_node ~id:newtip proof_mode () in - let head_id = VCS.get_branch_pos head in - let _st : unit = Reach.known_state ~doc ~cache:true head_id in (* ensure it is ok *) - let step () = - VCS.checkout VCS.Branch.master; - let mid = VCS.get_branch_pos VCS.Branch.master in - let _st' : unit = Reach.known_state ~doc ~cache:(VCS.is_interactive ()) mid in - let st = Vernacstate.freeze_interp_state ~marshallable:false in - ignore(stm_vernac_interp id st x); - (* Vernac x may or may not start a proof *) - if not in_proof && Vernacstate.Proof_global.there_are_pending_proofs () then - begin - let bname = VCS.mk_branch_name x in - let opacity_of_produced_term = function - (* This AST is ambiguous, hence we check it dynamically *) - | VernacInstance (_,_ , None, _) -> GuaranteesOpacity - | _ -> Doesn'tGuaranteeOpacity in - VCS.commit id (Fork (x,bname,opacity_of_produced_term (Vernacprop.under_control x.expr),[])); - VCS.set_proof_mode id (Some (Vernacentries.get_default_proof_mode ())); - VCS.branch bname (`Proof (VCS.proof_nesting () + 1)); - end else begin - begin match (VCS.get_branch head).VCS.kind with - | `Edit _ -> VCS.commit id (mkTransCmd x [] in_proof `MainQueue); - | `Master -> VCS.commit id (mkTransCmd x [] in_proof `MainQueue); - | `Proof _ -> - VCS.commit id (mkTransCmd x [] in_proof `MainQueue); - (* We hope it can be replayed, but we can't really know *) - ignore(VCS.propagate_sideff ~action:(ReplayCommand x)); - end; - VCS.checkout_shallowest_proof_branch (); - end in - State.define ~doc ~safe_id:head_id ~cache:true step id; - Backtrack.record (); `Ok - - | VtUnknown, VtLater -> - anomaly(str"classifier: VtUnknown must imply VtNow.") - - | VtProofMode pm, VtNow -> + | VtProofMode pm -> let proof_mode = Pvernac.lookup_proof_mode pm in let id = VCS.new_node ~id:newtip proof_mode () in VCS.commit id (mkTransCmd x [] false `MainQueue); VCS.set_parsing_state id head_parsing; Backtrack.record (); `Ok - | VtProofMode _, VtLater -> - anomaly(str"classifier: VtProofMode must imply VtNow.") - end in let pr_rc rc = match rc with | `Ok -> Pp.(seq [str "newtip ("; str (Stateid.to_string (VCS.cur_tip ())); str ")"]) @@ -3118,11 +2985,11 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) let get_ast ~doc id = match VCS.visit id with - | { step = `Cmd { cast = { loc; expr } } } - | { step = `Fork (({ loc; expr }, _, _, _), _) } - | { step = `Sideff ((ReplayCommand {loc; expr}) , _) } - | { step = `Qed ({ qast = { loc; expr } }, _) } -> - Some (Loc.tag ?loc expr) + | { step = `Cmd { cast = { expr } } } + | { step = `Fork (({ expr }, _, _, _), _) } + | { step = `Sideff ((ReplayCommand { expr }) , _) } + | { step = `Qed ({ qast = { expr } }, _) } -> + Some expr | _ -> None let stop_worker n = Slaves.cancel_worker n @@ -3139,8 +3006,8 @@ let parse_sentence ~doc sid ~entry pa = let ind_len_loc_of_id sid = if Stateid.equal sid Stateid.initial then None else match (VCS.visit sid).step with - | `Cmd { ctac = true; cast = { indentation; strlen; loc } } -> - Some (indentation, strlen, loc) + | `Cmd { ctac = true; cast = { indentation; strlen; expr } } -> + Some (indentation, strlen, expr.CAst.loc) | _ -> None (* the indentation logic works like this: if the beginning of the @@ -3153,7 +3020,7 @@ let ind_len_loc_of_id sid = let compute_indentation ?loc sid = Option.cata (fun loc -> let open Loc in - (* The effective lenght is the lenght on the last line *) + (* The effective length is the length on the last line *) let len = loc.ep - loc.bp in let prev_indent = match ind_len_loc_of_id sid with | None -> 0 @@ -3167,7 +3034,9 @@ let compute_indentation ?loc sid = Option.cata (fun loc -> eff_indent, len ) (0, 0) loc -let add ~doc ~ontop ?newtip verb { CAst.loc; v=ast } = +let add ~doc ~ontop ?newtip verb ast = + Hooks.(call document_add ast ontop); + let loc = ast.CAst.loc in let cur_tip = VCS.cur_tip () in if not (Stateid.equal ontop cur_tip) then user_err ?loc ~hdr:"Stm.add" @@ -3177,7 +3046,7 @@ let add ~doc ~ontop ?newtip verb { CAst.loc; v=ast } = let indentation, strlen = compute_indentation ?loc ontop in (* XXX: Classifiy vernac should be moved inside process transaction *) let clas = Vernac_classifier.classify_vernac ast in - let aast = { verbose = verb; indentation; strlen; loc; expr = ast } in + let aast = { verbose = verb; indentation; strlen; expr = ast } in match process_transaction ~doc ?newtip aast clas with | `Ok -> doc, VCS.cur_tip (), `NewTip | `Unfocus qed_id -> doc, qed_id, `Unfocus (VCS.cur_tip ()) @@ -3197,20 +3066,22 @@ let query ~doc ~at ~route s = let rec loop () = match parse_sentence ~doc at ~entry:Pvernac.main_entry s with | None -> () - | Some {CAst.loc; v=ast} -> - let indentation, strlen = compute_indentation ?loc at in - let st = State.get_cached at in - let aast = { - verbose = true; indentation; strlen; - loc; expr = ast } in - ignore(stm_vernac_interp ~route at st aast); - loop () + | Some ast -> + let loc = ast.CAst.loc in + let indentation, strlen = compute_indentation ?loc at in + let st = State.get_cached at in + let aast = { + verbose = true; indentation; strlen; + expr = ast } in + ignore(stm_vernac_interp ~route at st aast); + loop () in loop () ) s let edit_at ~doc id = + Hooks.(call document_edit id); if Stateid.equal id Stateid.dummy then anomaly(str"edit_at dummy.") else let vcs = VCS.backup () in let on_cur_branch id = @@ -3366,7 +3237,10 @@ let state_computed_hook = Hooks.state_computed_hook let state_ready_hook = Hooks.state_ready_hook let forward_feedback_hook = Hooks.forward_feedback_hook let unreachable_state_hook = Hooks.unreachable_state_hook -let () = Hook.set Obligations.stm_get_fix_exn (fun () -> !State.fix_exn_ref) +let document_add_hook = Hooks.document_add_hook +let document_edit_hook = Hooks.document_edit_hook +let sentence_exec_hook = Hooks.sentence_exec_hook +let () = Hook.set DeclareObl.stm_get_fix_exn (fun () -> !State.fix_exn_ref) type document = VCS.vcs let backup () = VCS.backup () diff --git a/stm/stm.mli b/stm/stm.mli index 91651e3534..29e4b02e3f 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -34,6 +34,8 @@ module AsyncOpts : sig async_proofs_tac_error_resilience : tac_error_filter; async_proofs_cmd_error_resilience : bool; async_proofs_delegation_threshold : float; + + async_proofs_worker_priority : CoqworkmgrApi.priority; } val default_opts : stm_opt @@ -50,7 +52,7 @@ type stm_doc_type = | VioDoc of string (* file path *) | Interactive of interactive_top (* module path *) -(** Coq initalization options: +(** Coq initialization options: - [doc_type]: Type of document being created. @@ -63,13 +65,13 @@ type stm_doc_type = *) type stm_init_options = { (* The STM will set some internal flags differently depending on the - specified [doc_type]. This distinction should dissappear at some + specified [doc_type]. This distinction should disappear 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; + iload_path : Loadpath.coq_path list; (* Require [require_libs] before the initial state is ready. Parameters follow [Library], that is to say, @@ -86,7 +88,7 @@ type stm_init_options = { (** The type of a STM document *) type doc -(** [init_core] performs some low-level initalization; should go away +(** [init_core] performs some low-level initialization; should go away in future releases. *) val init_core : unit -> unit @@ -111,7 +113,7 @@ val parse_sentence : 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_control CAst.t -> + bool -> Vernacexpr.vernac_control -> doc * Stateid.t * [ `NewTip | `Unfocus of Stateid.t ] (* Returns the proof state before the last tactic that was applied at or before @@ -119,6 +121,8 @@ the specified state AND that has differences in the underlying proof (i.e., ignoring proofview-only changes). Used to compute proof diffs. *) val get_prev_proof : doc:doc -> Stateid.t -> Proof.t option +val get_proof : doc:doc -> Stateid.t -> Proof.t option + (* [query at ?report_with cmd] Executes [cmd] at a given state [at], throwing away side effects except messages. Feedback will be sent with [report_with], which defaults to the dummy state id *) @@ -167,7 +171,7 @@ type tasks val check_task : string -> tasks -> int -> bool val info_tasks : tasks -> (string * float * int) list val finish_tasks : string -> - Library.seg_univ -> Library.seg_discharge -> Library.seg_proofs -> + Library.seg_univ -> Library.seg_proofs -> tasks -> Library.seg_univ * Library.seg_proofs (* Id of the tip of the current branch *) @@ -175,7 +179,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_control Loc.located) option +val get_ast : doc:doc -> Stateid.t -> Vernacexpr.vernac_control option (* Filename *) val set_compilation_hints : string -> unit @@ -282,6 +286,19 @@ val state_ready_hook : (doc:doc -> Stateid.t -> unit) Hook.t (* Messages from the workers to the master *) val forward_feedback_hook : (Feedback.feedback -> unit) Hook.t +(* + * Hooks into the UI for plugins (not for general use) + *) + +(** User adds a sentence to the document (after parsing) *) +val document_add_hook : (Vernacexpr.vernac_control -> Stateid.t -> unit) Hook.t + +(** User edits a sentence in the document *) +val document_edit_hook : (Stateid.t -> unit) Hook.t + +(** User requests evaluation of a sentence *) +val sentence_exec_hook : (Stateid.t -> unit) Hook.t + val get_doc : Feedback.doc_id -> doc val state_of_id : doc:doc -> diff --git a/stm/tQueue.ml b/stm/tQueue.ml index 33744e7323..72a40a2a9c 100644 --- a/stm/tQueue.ml +++ b/stm/tQueue.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/stm/tQueue.mli b/stm/tQueue.mli index e098c37f2a..c8c592e42f 100644 --- a/stm/tQueue.mli +++ b/stm/tQueue.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/stm/vcs.ml b/stm/vcs.ml index 4bd46286bd..78edeb53d3 100644 --- a/stm/vcs.ml +++ b/stm/vcs.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/stm/vcs.mli b/stm/vcs.mli index 47622ef6f1..f6ca81257b 100644 --- a/stm/vcs.mli +++ b/stm/vcs.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 58fe923f9e..8d600c2859 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -20,10 +20,13 @@ let string_of_parallel = function "par" ^ if solve then "solve" else "" ^ if abs then "abs" else "" | `No -> "" -let string_of_vernac_type = function - | VtUnknown -> "Unknown" +let string_of_vernac_when = function + | VtLater -> "Later" + | VtNow -> "Now" + +let string_of_vernac_classification = function | VtStartProof _ -> "StartProof" - | VtSideff _ -> "Sideff" + | VtSideff (_,w) -> "Sideff"^" "^(string_of_vernac_when w) | VtQed (VtKeep VtKeepAxiom) -> "Qed(admitted)" | VtQed (VtKeep (VtKeepOpaque | VtKeepDefined)) -> "Qed(keep)" | VtQed VtDrop -> "Qed(drop)" @@ -34,13 +37,6 @@ let string_of_vernac_type = function | VtMeta -> "Meta " | VtProofMode _ -> "Proof Mode" -let string_of_vernac_when = function - | VtLater -> "Later" - | VtNow -> "Now" - -let string_of_vernac_classification (t,w) = - string_of_vernac_type t ^ " " ^ string_of_vernac_when w - let vtkeep_of_opaque = let open Proof_global in function | Opaque -> VtKeepOpaque | Transparent -> VtKeepDefined @@ -57,25 +53,26 @@ let options_affecting_stm_scheduling = stm_allow_nested_proofs_option_name; Vernacentries.proof_mode_opt_name; Attributes.program_mode_option_name; + Proof_using.proof_using_opt_name; ] let classify_vernac e = - let static_classifier ~poly e = match e with + let static_classifier ~atts 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 (_, l,_) | VernacUnsetOption (_, l)) + | VernacSetOption (_, l,_) when CList.exists (CList.equal String.equal l) options_affecting_stm_scheduling -> - VtSideff [], VtNow + VtSideff ([], VtNow) (* Qed *) - | VernacAbort _ -> VtQed VtDrop, VtLater - | VernacEndProof Admitted -> VtQed (VtKeep VtKeepAxiom), VtLater - | VernacEndProof (Proved (opaque,_)) -> VtQed (VtKeep (vtkeep_of_opaque opaque)), VtLater - | VernacExactProof _ -> VtQed (VtKeep VtKeepOpaque), VtLater + | VernacAbort _ -> VtQed VtDrop + | VernacEndProof Admitted -> VtQed (VtKeep VtKeepAxiom) + | VernacEndProof (Proved (opaque,_)) -> VtQed (VtKeep (vtkeep_of_opaque opaque)) + | VernacExactProof _ -> VtQed (VtKeep VtKeepOpaque) (* Query *) | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _ - | VernacCheckMayEval _ -> VtQuery, VtLater + | VernacCheckMayEval _ -> VtQuery (* ProofStep *) | VernacProof _ | VernacFocus _ | VernacUnfocus @@ -83,70 +80,69 @@ let classify_vernac e = | VernacCheckGuard | VernacUnfocused | VernacSolveExistential _ -> - VtProofStep { parallel = `No; proof_block_detection = None }, VtLater + VtProofStep { parallel = `No; proof_block_detection = None } | VernacBullet _ -> - VtProofStep { parallel = `No; proof_block_detection = Some "bullet" }, - VtLater + VtProofStep { parallel = `No; proof_block_detection = Some "bullet" } | VernacEndSubproof -> VtProofStep { parallel = `No; - proof_block_detection = Some "curly" }, - VtLater - (* Options changing parser *) - | VernacUnsetOption (_, ["Default";"Proof";"Using"]) - | VernacSetOption (_, ["Default";"Proof";"Using"],_) -> VtSideff [], VtNow + proof_block_detection = Some "curly" } (* StartProof *) - | VernacDefinition ((Decl_kinds.DoDischarge,_),({v=i},_),ProveBody _) -> - VtStartProof(Doesn'tGuaranteeOpacity, idents_of_name i), VtLater + | VernacDefinition ((DoDischarge,_),({v=i},_),ProveBody _) -> + VtStartProof(Doesn'tGuaranteeOpacity, idents_of_name i) | VernacDefinition (_,({v=i},_),ProveBody _) -> - let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in - VtStartProof(guarantee, idents_of_name i), VtLater + let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in + let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in + VtStartProof(guarantee, idents_of_name i) | VernacStartTheoremProof (_,l) -> - let ids = List.map (fun (({v=i}, _), _) -> i) l in - let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in - VtStartProof (guarantee,ids), VtLater + let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in + let ids = List.map (fun (({v=i}, _), _) -> i) l in + let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in + VtStartProof (guarantee,ids) | VernacFixpoint (discharge,l) -> + let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in let guarantee = - if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity + if discharge = DoDischarge || polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in let ids, open_proof = - List.fold_left (fun (l,b) ((({v=id},_),_,_,_,p),_) -> - id::l, b || p = None) ([],false) l in + List.fold_left (fun (l,b) {Vernacexpr.fname={CAst.v=id}; body_def} -> + id::l, b || body_def = None) ([],false) l in if open_proof - then VtStartProof (guarantee,ids), VtLater - else VtSideff ids, VtLater + then VtStartProof (guarantee,ids) + else VtSideff (ids, VtLater) | VernacCoFixpoint (discharge,l) -> + let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in let guarantee = - if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity + if discharge = DoDischarge || polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in let ids, open_proof = - List.fold_left (fun (l,b) ((({v=id},_),_,_,p),_) -> - id::l, b || p = None) ([],false) l in + List.fold_left (fun (l,b) { Vernacexpr.fname={CAst.v=id}; body_def } -> + id::l, b || body_def = None) ([],false) l in if open_proof - then VtStartProof (guarantee,ids), VtLater - else VtSideff ids, VtLater + then VtStartProof (guarantee,ids) + 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, _) -> id.v) l) l) in - VtSideff ids, VtLater + VtSideff (ids, VtLater) | VernacPrimitive (id,_,_) -> - VtSideff [id.CAst.v], VtLater - | VernacDefinition (_,({v=id},_),DefineBody _) -> VtSideff (idents_of_name id), VtLater + VtSideff ([id.CAst.v], VtLater) + | VernacDefinition (_,({v=id},_),DefineBody _) -> VtSideff (idents_of_name id, VtLater) | VernacInductive (_, _,_,l) -> let ids = List.map (fun (((_,({v=id},_)),_,_,_,cl),_) -> id :: match cl with | Constructors l -> List.map (fun (_,({v=id},_)) -> id) l | RecordDecl (oid,l) -> (match oid with Some {v=x} -> [x] | _ -> []) @ CList.map_filter (function - | ((_,AssumExpr({v=Names.Name n},_)),_),_ -> Some n + | AssumExpr({v=Names.Name n},_), _ -> Some n | _ -> None) l) l in - VtSideff (List.flatten ids), VtLater + VtSideff (List.flatten ids, VtLater) | VernacScheme l -> let ids = List.map (fun {v}->v) (CList.map_filter (fun (x,_) -> x) l) in - VtSideff ids, VtLater - | VernacCombinedScheme ({v=id},_) -> VtSideff [id], VtLater - | VernacBeginSection {v=id} -> VtSideff [id], VtLater + VtSideff (ids, VtLater) + | VernacCombinedScheme ({v=id},_) -> VtSideff ([id], VtLater) + | VernacBeginSection {v=id} -> VtSideff ([id], VtLater) | VernacUniverse _ | VernacConstraint _ | VernacCanonical _ | VernacCoercion _ | VernacIdentityCoercion _ | VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _ @@ -156,7 +152,7 @@ let classify_vernac e = | VernacReserve _ | VernacGeneralizable _ | VernacSetOpacity _ | VernacSetStrategy _ - | VernacUnsetOption _ | VernacSetOption _ + | VernacSetOption _ | VernacAddOption _ | VernacRemoveOption _ | VernacMemOption _ | VernacPrintOption _ | VernacGlobalCheck _ @@ -165,17 +161,17 @@ let classify_vernac e = | VernacRegister _ | VernacNameSectionHypSet _ | VernacComments _ - | VernacDeclareInstance _ -> VtSideff [], VtLater + | VernacDeclareInstance _ -> VtSideff ([], VtLater) (* Who knows *) - | VernacLoad _ -> VtSideff [], VtNow + | VernacLoad _ -> VtSideff ([], VtNow) (* (Local) Notations have to disappear *) - | VernacEndSegment _ -> VtSideff [], VtNow + | VernacEndSegment _ -> VtSideff ([], VtNow) (* Modules with parameters have to be executed: can import notations *) | VernacDeclareModule (exp,{v=id},bl,_) | VernacDefineModule (exp,{v=id},bl,_,_) -> - VtSideff [id], if bl = [] && exp = None then VtLater else VtNow + VtSideff ([id], if bl = [] && exp = None then VtLater else VtNow) | VernacDeclareModuleType ({v=id},bl,_,_) -> - VtSideff [id], if bl = [] then VtLater else VtNow + VtSideff ([id], if bl = [] then VtLater else VtNow) (* These commands alter the parser *) | VernacDeclareCustomEntry _ | VernacOpenCloseScope _ | VernacDeclareScope _ @@ -185,37 +181,38 @@ let classify_vernac e = | VernacSyntacticDefinition _ | VernacRequire _ | VernacImport _ | VernacInclude _ | VernacDeclareMLModule _ - | VernacContext _ (* TASSI: unsure *) -> VtSideff [], VtNow - | VernacProofMode pm -> VtProofMode pm, VtNow - (* These are ambiguous *) - | VernacInstance _ -> VtUnknown, VtNow + | VernacContext _ (* TASSI: unsure *) -> VtSideff ([], VtNow) + | VernacProofMode pm -> VtProofMode pm + | VernacInstance ((name,_),_,_,None,_) when not (Attributes.parse_drop_extra Attributes.program atts) -> + let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in + let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in + VtStartProof (guarantee, idents_of_name name.CAst.v) + | VernacInstance ((name,_),_,_,_,_) -> + VtSideff (idents_of_name name.CAst.v, VtLater) (* Stm will install a new classifier to handle these *) | VernacBack _ | VernacAbortAll | VernacUndoTo _ | VernacUndo _ | VernacResetName _ | VernacResetInitial - | VernacBackTo _ | VernacRestart -> VtMeta, VtNow + | VernacRestart -> VtMeta (* What are these? *) | VernacRestoreState _ - | VernacWriteState _ -> VtSideff [], VtNow + | VernacWriteState _ -> VtSideff ([], VtNow) (* Plugins should classify their commands *) | VernacExtend (s,l) -> try Vernacextend.get_vernac_classifier s l with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".") in - let rec static_control_classifier = function - | VernacExpr (f, e) -> - let poly = Attributes.(parse_drop_extra polymorphic_nowarn f) in - static_classifier ~poly e - | VernacTimeout (_,{v=e}) -> static_control_classifier e - | VernacTime (_,{v=e}) | VernacRedirect (_, {v=e}) -> - static_control_classifier e - | VernacFail {v=e} -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) - (match static_control_classifier e with - | ( VtQuery | VtProofStep _ | VtSideff _ - | VtMeta), _ as x -> x - | VtQed _, _ -> - VtProofStep { parallel = `No; proof_block_detection = None }, - VtLater - | (VtStartProof _ | VtUnknown | VtProofMode _), _ -> VtQuery, VtLater) + let static_control_classifier ({ CAst.v ; _ } as cmd) = + (* Fail Qed or Fail Lemma must not join/fork the DAG *) + (* XXX why is Fail not always Query? *) + if Vernacprop.has_Fail cmd then + (match static_classifier ~atts:v.attrs v.expr with + | VtQuery | VtProofStep _ | VtSideff _ + | VtMeta as x -> x + | VtQed _ -> VtProofStep { parallel = `No; proof_block_detection = None } + | VtStartProof _ | VtProofMode _ -> VtQuery) + else + static_classifier ~atts:v.attrs v.expr + in static_control_classifier e diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli index 9d93ad1f39..77994fac2e 100644 --- a/stm/vernac_classifier.mli +++ b/stm/vernac_classifier.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml index 69c1d9bd23..baa7b3570c 100644 --- a/stm/vio_checking.ml +++ b/stm/vio_checking.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -10,11 +10,10 @@ open Util -let check_vio (ts,f) = - Dumpglob.noglob (); - let long_f_dot_v, _, _, _, _, tasks, _ = Library.load_library_todo f in - Stm.set_compilation_hints long_f_dot_v; - List.fold_left (fun acc ids -> Stm.check_task f tasks ids && acc) true ts +let check_vio (ts,f_in) = + let _, _, _, tasks, _ = Library.load_library_todo f_in in + Stm.set_compilation_hints f_in; + List.fold_left (fun acc ids -> Stm.check_task f_in tasks ids && acc) true ts module Worker = Spawn.Sync () @@ -28,15 +27,12 @@ module Pool = Map.Make(IntOT) let schedule_vio_checking j fs = if j < 1 then CErrors.user_err Pp.(str "The number of workers must be bigger than 0"); let jobs = ref [] in - List.iter (fun f -> - let f = - if Filename.check_suffix f ".vio" then Filename.chop_extension f - else f in - let long_f_dot_v, _,_,_,_, tasks, _ = Library.load_library_todo f in - Stm.set_compilation_hints long_f_dot_v; + List.iter (fun long_f_dot_vio -> + let _,_,_, tasks, _ = Library.load_library_todo long_f_dot_vio in + Stm.set_compilation_hints long_f_dot_vio; let infos = Stm.info_tasks tasks in let eta = List.fold_left (fun a (_,t,_) -> a +. t) 0.0 infos in - if infos <> [] then jobs := (f, eta, infos) :: !jobs) + if infos <> [] then jobs := (long_f_dot_vio, eta, infos) :: !jobs) fs; let cmp_job (_,t1,_) (_,t2,_) = compare t2 t1 in jobs := List.sort cmp_job !jobs; @@ -103,16 +99,12 @@ let schedule_vio_checking j fs = let schedule_vio_compilation j fs = if j < 1 then CErrors.user_err Pp.(str "The number of workers must be bigger than 0"); let jobs = ref [] in - List.iter (fun f -> - let f = - if Filename.check_suffix f ".vio" then Filename.chop_extension f - else f in - let long_f_dot_v = Loadpath.locate_file (f^".v") in - let aux = Aux_file.load_aux_file_for long_f_dot_v in + List.iter (fun long_f_dot_vio -> + let aux = Aux_file.load_aux_file_for long_f_dot_vio in let eta = try float_of_string (Aux_file.get aux "vo_compile_time") with Not_found -> 0.0 in - jobs := (f, eta) :: !jobs) + jobs := (long_f_dot_vio, eta) :: !jobs) fs; let cmp_job (_,t1) (_,t2) = compare t2 t1 in jobs := List.sort cmp_job !jobs; @@ -146,8 +138,6 @@ let schedule_vio_compilation j fs = (* set the access and last modification time of all files to the same t * not to confuse make into thinking that some of them are outdated *) let t = Unix.gettimeofday () in - List.iter (fun (f,_) -> Unix.utimes (f^".vo") t t) all_jobs; + List.iter (fun (f,_) -> Unix.utimes (Filename.chop_extension f^".vo") t t) all_jobs; end; exit !rc - - diff --git a/stm/vio_checking.mli b/stm/vio_checking.mli index 177b3b2d06..0f139921ef 100644 --- a/stm/vio_checking.mli +++ b/stm/vio_checking.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/stm/workerPool.ml b/stm/workerPool.ml index 2432e72c8a..f77ced2f3a 100644 --- a/stm/workerPool.ml +++ b/stm/workerPool.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -19,7 +19,7 @@ type 'a cpanel = { module type PoolModel = sig (* this shall come from a Spawn.* model *) type process - val spawn : int -> worker_id * process * CThread.thread_ic * out_channel + val spawn : int -> CoqworkmgrApi.priority -> worker_id * process * CThread.thread_ic * out_channel (* this defines the main loop of the manager *) type extra @@ -79,20 +79,20 @@ let locking { lock; pool = p } f = x with e -> Mutex.unlock lock; raise e -let rec create_worker extra pool id = +let rec create_worker extra pool priority id = let cancel = ref false in - let name, process, ic, oc as worker = Model.spawn id in + let name, process, ic, oc as worker = Model.spawn id priority in master_handshake name ic oc; - let exit () = cancel := true; cleanup pool; Thread.exit () in + let exit () = cancel := true; cleanup pool priority; Thread.exit () in let cancelled () = !cancel in let cpanel = { exit; cancelled; extra } in let manager = CThread.create (Model.manager cpanel) worker in { name; cancel; manager; process } -and cleanup x = locking x begin fun { workers; count; extra_arg } -> +and cleanup x priority = locking x begin fun { workers; count; extra_arg } -> workers := List.map (function | { cancel } as w when !cancel = false -> w - | _ -> let n = !count in incr count; create_worker extra_arg x n) + | _ -> let n = !count in incr count; create_worker extra_arg x priority n) !workers end @@ -102,7 +102,7 @@ end let is_empty x = locking x begin fun { workers } -> !workers = [] end -let create extra_arg ~size = let x = { +let create extra_arg ~size priority = let x = { lock = Mutex.create (); pool = { extra_arg; @@ -110,7 +110,7 @@ let create extra_arg ~size = let x = { count = ref size; }} in locking x begin fun { workers } -> - workers := CList.init size (create_worker extra_arg x) + workers := CList.init size (create_worker extra_arg x priority) end; x diff --git a/stm/workerPool.mli b/stm/workerPool.mli index 0f1237b584..5468a24959 100644 --- a/stm/workerPool.mli +++ b/stm/workerPool.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -19,7 +19,8 @@ type 'a cpanel = { module type PoolModel = sig (* this shall come from a Spawn.* model *) type process - val spawn : int -> worker_id * process * CThread.thread_ic * out_channel + val spawn : int -> CoqworkmgrApi.priority -> + worker_id * process * CThread.thread_ic * out_channel (* this defines the main loop of the manager *) type extra @@ -31,7 +32,7 @@ module Make(Model : PoolModel) : sig type pool - val create : Model.extra -> size:int -> pool + val create : Model.extra -> size:int -> CoqworkmgrApi.priority -> pool val is_empty : pool -> bool val n_workers : pool -> int |