diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/asyncTaskQueue.ml | 10 | ||||
| -rw-r--r-- | stm/asyncTaskQueue.mli | 16 | ||||
| -rw-r--r-- | stm/coqworkmgrApi.ml | 10 | ||||
| -rw-r--r-- | stm/coqworkmgrApi.mli | 10 | ||||
| -rw-r--r-- | stm/dag.ml | 10 | ||||
| -rw-r--r-- | stm/dag.mli | 10 | ||||
| -rw-r--r-- | stm/proofBlockDelimiter.ml | 14 | ||||
| -rw-r--r-- | stm/proofBlockDelimiter.mli | 10 | ||||
| -rw-r--r-- | stm/proofworkertop.ml | 12 | ||||
| -rw-r--r-- | stm/queryworkertop.ml | 12 | ||||
| -rw-r--r-- | stm/spawned.ml | 10 | ||||
| -rw-r--r-- | stm/spawned.mli | 10 | ||||
| -rw-r--r-- | stm/stm.ml | 223 | ||||
| -rw-r--r-- | stm/stm.mli | 83 | ||||
| -rw-r--r-- | stm/tQueue.ml | 10 | ||||
| -rw-r--r-- | stm/tQueue.mli | 10 | ||||
| -rw-r--r-- | stm/tacworkertop.ml | 12 | ||||
| -rw-r--r-- | stm/vcs.ml | 10 | ||||
| -rw-r--r-- | stm/vcs.mli | 10 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 79 | ||||
| -rw-r--r-- | stm/vernac_classifier.mli | 10 | ||||
| -rw-r--r-- | stm/vio_checking.ml | 10 | ||||
| -rw-r--r-- | stm/vio_checking.mli | 10 | ||||
| -rw-r--r-- | stm/workerLoop.ml | 14 | ||||
| -rw-r--r-- | stm/workerLoop.mli | 12 | ||||
| -rw-r--r-- | stm/workerPool.ml | 10 | ||||
| -rw-r--r-- | stm/workerPool.mli | 10 |
27 files changed, 382 insertions, 265 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 26aef53552..b3e1500ae4 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open CErrors diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli index 07689389ff..6e6827c73f 100644 --- a/stm/asyncTaskQueue.mli +++ b/stm/asyncTaskQueue.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Default flags for workers *) @@ -71,7 +73,7 @@ module type Task = sig (** Extra arguments of the task kind, for -toploop *) val extra_env : unit -> string array - (** {5} Master API, it is run by the master, on a thread *) + (** {5 Master API, it is run by the master, on a thread} *) (** [request_of_task status t] takes the [status] of the worker and a task [t] and creates the corresponding [Some request] to be @@ -116,8 +118,8 @@ module type Task = sig (** [forward_feedback fb] sends fb to all the workers. *) val forward_feedback : Feedback.feedback -> unit - (** {5} Worker API, it is run by worker, on a different fresh - process *) + (** {5 Worker API, it is run by worker, on a different fresh + process} *) (** [perform in] synchronously processes a request [in] *) val perform : request -> response diff --git a/stm/coqworkmgrApi.ml b/stm/coqworkmgrApi.ml index 14fd97a6d5..36b5d18ab6 100644 --- a/stm/coqworkmgrApi.ml +++ b/stm/coqworkmgrApi.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) let debug = false diff --git a/stm/coqworkmgrApi.mli b/stm/coqworkmgrApi.mli index 953903810e..2983b619db 100644 --- a/stm/coqworkmgrApi.mli +++ b/stm/coqworkmgrApi.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* High level api for clients of the service (like coqtop) *) diff --git a/stm/dag.ml b/stm/dag.ml index bdd71c50bd..eb5063bf0c 100644 --- a/stm/dag.ml +++ b/stm/dag.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) module type S = sig diff --git a/stm/dag.mli b/stm/dag.mli index 049286df31..cae4fccc73 100644 --- a/stm/dag.mli +++ b/stm/dag.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) module type S = sig diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index 01b5b9a016..23f976120a 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Stm @@ -96,7 +98,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 (Vernacexpr.VernacExpr([], Vernacexpr.VernacBullet (to_bullet_val b))) } | `Not -> `Leaks @@ -125,7 +127,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 (Vernacexpr.VernacExpr ([], Vernacexpr.VernacEndSubproof)) } | `Not -> `Leaks diff --git a/stm/proofBlockDelimiter.mli b/stm/proofBlockDelimiter.mli index 5cff0a8a72..9784de1141 100644 --- a/stm/proofBlockDelimiter.mli +++ b/stm/proofBlockDelimiter.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* This file implements proof block detection for: diff --git a/stm/proofworkertop.ml b/stm/proofworkertop.ml index 10b42f7e91..4b85a05ac7 100644 --- a/stm/proofworkertop.ml +++ b/stm/proofworkertop.ml @@ -1,14 +1,16 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) module W = AsyncTaskQueue.MakeWorker(Stm.ProofTask) () let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout -let () = Coqtop.toploop_run := (fun _ -> W.main_loop ()) +let () = Coqtop.toploop_run := (fun _ ~state:_ -> W.main_loop ()) diff --git a/stm/queryworkertop.ml b/stm/queryworkertop.ml index a1fe50c63e..aa00102aab 100644 --- a/stm/queryworkertop.ml +++ b/stm/queryworkertop.ml @@ -1,14 +1,16 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) module W = AsyncTaskQueue.MakeWorker(Stm.QueryTask) () let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout -let () = Coqtop.toploop_run := (fun _ -> W.main_loop ()) +let () = Coqtop.toploop_run := (fun _ ~state:_ -> W.main_loop ()) diff --git a/stm/spawned.ml b/stm/spawned.ml index fb5708f3a3..3833c8026e 100644 --- a/stm/spawned.ml +++ b/stm/spawned.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Spawn diff --git a/stm/spawned.mli b/stm/spawned.mli index 7f463c6a6e..df4e725953 100644 --- a/stm/spawned.mli +++ b/stm/spawned.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* To link this file, threads are needed *) diff --git a/stm/stm.ml b/stm/stm.ml index afb6fabcb1..b3da97c6e0 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* enable in case of stm problems *) @@ -26,31 +28,50 @@ 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 + type tac_error_filter = [ `None | `Only of string list | `All ] - let async_proofs_private_flags = ref None - let async_proofs_full = ref false - let async_proofs_never_reopen_branch = ref false + type stm_opt = { + async_proofs_n_workers : int; + async_proofs_n_tacworkers : int; - 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 + async_proofs_cache : cache option; + async_proofs_mode : async_proofs; + + async_proofs_private_flags : string option; + async_proofs_full : bool; + async_proofs_never_reopen_branch : bool; - let async_proofs_delegation_threshold = ref 0.03 + async_proofs_tac_error_resilience : tac_error_filter; + async_proofs_cmd_error_resilience : bool; + async_proofs_delegation_threshold : float; + } + let default_opts = { + async_proofs_n_workers = 1; + async_proofs_n_tacworkers = 2; + + async_proofs_cache = None; + + async_proofs_mode = APoff; + + async_proofs_private_flags = None; + async_proofs_full = false; + async_proofs_never_reopen_branch = false; + + async_proofs_tac_error_resilience = `Only [ "curly" ]; + async_proofs_cmd_error_resilience = true; + async_proofs_delegation_threshold = 0.03; + } + + let cur_opt = ref default_opts end open AsyncOpts -let async_proofs_is_master () = - !async_proofs_mode = APon && +let async_proofs_is_master opt = + opt.async_proofs_mode = APon && !Flags.async_proofs_worker_id = "master" (* Protect against state changes *) @@ -66,8 +87,7 @@ let stm_purify f x = Exninfo.iraise e let execution_error ?loc state_id msg = - feedback ~id:state_id - (Message (Error, loc, msg)) + feedback ~id:state_id (Message (Error, loc, msg)) module Hooks = struct @@ -547,8 +567,8 @@ end = struct (* {{{ *) let reachable id = reachable !vcs id let mk_branch_name { expr = x } = Branch.make (match Vernacprop.under_control x with - | VernacDefinition (_,((_,i),_),_) -> Id.to_string i - | VernacStartTheoremProof (_,[Some ((_,i),_),_]) -> Id.to_string i + | VernacDefinition (_,({CAst.v=Name i},_),_) -> Id.to_string i + | VernacStartTheoremProof (_,[({CAst.v=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 @@ -558,7 +578,7 @@ end = struct (* {{{ *) | None -> raise Vcs_aux.Expired let set_state id s = (get_info id).state <- s; - if async_proofs_is_master () then Hooks.(call state_ready id) + if async_proofs_is_master !cur_opt then Hooks.(call state_ready id) let get_state id = (get_info id).state let reached id = let info = get_info id in @@ -1150,13 +1170,13 @@ end = struct (* {{{ *) " the \"-async-proofs-cache force\" option to Coq.")) let undo_vernac_classifier v = - if VCS.is_interactive () = `No && !async_proofs_cache <> Some Force + if VCS.is_interactive () = `No && !cur_opt.async_proofs_cache <> Some Force then undo_costly_in_batch_mode v; try match Vernacprop.under_control v with | VernacResetInitial -> Stateid.initial, VtNow - | VernacResetName (_,name) -> + | VernacResetName {CAst.v=name} -> let id = VCS.get_branch_pos (VCS.current_branch ()) in (try let oid = @@ -1218,7 +1238,7 @@ let set_compilation_hints file = let get_hint_ctx loc = let s = Aux_file.get ?loc !hints "context_used" in let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") s) in - let ids = List.map (fun id -> Loc.tag id) ids in + let ids = List.map (fun id -> CAst.make id) ids in match ids with | [] -> SsEmpty | x :: xs -> @@ -1286,7 +1306,7 @@ let prev_node { id } = let cur_node id = mk_doc_node id (VCS.visit id) let is_block_name_enabled name = - match !async_proofs_tac_error_resilience with + match !cur_opt.async_proofs_tac_error_resilience with | `None -> false | `All -> true | `Only l -> List.mem name l @@ -1294,7 +1314,7 @@ let is_block_name_enabled name = let detect_proof_block id name = let name = match name with None -> "indent" | Some x -> x in if is_block_name_enabled name && - (async_proofs_is_master () || Flags.async_proofs_is_worker ()) + (async_proofs_is_master !cur_opt || Flags.async_proofs_is_worker ()) then ( match cur_node id with | None -> () @@ -1396,7 +1416,7 @@ end = struct (* {{{ *) let task_match age t = match age, t with | Fresh, BuildProof { t_states } -> - not !async_proofs_full || + not !cur_opt.async_proofs_full || List.exists (fun x -> CList.mem_f Stateid.equal x !perspective) t_states | Old my_states, States l -> List.for_all (fun x -> CList.mem_f Stateid.equal x my_states) l @@ -1433,7 +1453,7 @@ end = struct (* {{{ *) feedback (InProgress ~-1); t_assign (`Val pl); record_pb_time ?loc:t_loc t_name time; - if !async_proofs_full || t_drop + if !cur_opt.async_proofs_full || t_drop then `Stay(t_states,[States t_states]) else `End | Fresh, BuildProof { t_assign; t_loc; t_name; t_states }, @@ -1498,7 +1518,7 @@ end = struct (* {{{ *) stm_vernac_interp stop ~proof:(pobject, terminator) st { verbose = false; loc; indentation = 0; strlen = 0; - expr = VernacExpr (VernacEndProof (Proved (Opaque,None))) }) in + expr = VernacExpr ([], VernacEndProof (Proved (Opaque,None))) }) in ignore(Future.join checked_proof); end; (* STATE: Restore the state XXX: handle exn *) @@ -1560,12 +1580,13 @@ end = struct (* {{{ *) | ReqStates sl -> RespStates (perform_states sl) let on_marshal_error s = function - | States _ -> msg_error(Pp.strbrk("Marshalling error: "^s^". "^ - "The system state could not be sent to the master process.")) + | States _ -> + msg_warning Pp.(strbrk("Marshalling error: "^s^". "^ + "The system state could not be sent to the master process.")) | BuildProof { t_exn_info; t_stop; t_assign; t_loc; t_drop = drop_pt } -> - msg_error(Pp.strbrk("Marshalling error: "^s^". "^ - "The system state could not be sent to the worker process. "^ - "Falling back to local, lazy, evaluation.")); + msg_warning Pp.(strbrk("Marshalling error: "^s^". "^ + "The system state could not be sent to the worker process. "^ + "Falling back to local, lazy, evaluation.")); t_assign(`Comp(build_proof_here ?loc:t_loc ~drop_pt t_exn_info t_stop)); feedback (InProgress ~-1) @@ -1607,8 +1628,8 @@ end = struct (* {{{ *) let queue = ref None let init () = - if async_proofs_is_master () then - queue := Some (TaskQueue.create !async_proofs_n_workers) + if async_proofs_is_master !cur_opt then + queue := Some (TaskQueue.create !cur_opt.async_proofs_n_workers) else queue := Some (TaskQueue.create 0) @@ -1646,14 +1667,14 @@ end = struct (* {{{ *) let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp stop ~proof st { verbose = false; loc; indentation = 0; strlen = 0; - expr = VernacExpr (VernacEndProof (Proved (Opaque,None))) }); + expr = VernacExpr ([], VernacEndProof (Proved (Opaque,None))) }); `OK proof end with e -> let (e, info) = CErrors.push e in (try match Stateid.get info with | None -> - msg_error Pp.( + msg_warning Pp.( str"File " ++ str name ++ str ": proof of " ++ str r_name ++ spc () ++ iprint (e, info)) | Some (_, cur) -> @@ -1663,17 +1684,17 @@ end = struct (* {{{ *) | { step = `Qed ( { qast = { loc } }, _) } | { step = `Sideff (ReplayCommand { loc }, _) } -> let start, stop = Option.cata Loc.unloc (0,0) loc in - msg_error Pp.( + msg_warning Pp.( str"File " ++ str name ++ str ": proof of " ++ str r_name ++ str ": chars " ++ int start ++ str "-" ++ int stop ++ spc () ++ iprint (e, info)) | _ -> - msg_error Pp.( + msg_warning Pp.( str"File " ++ str name ++ str ": proof of " ++ str r_name ++ spc () ++ iprint (e, info)) with e -> - msg_error Pp.(str"unable to print error message: " ++ - str (Printexc.to_string e))); + msg_warning Pp.(str"unable to print error message: " ++ + str (Printexc.to_string e))); if drop then `ERROR_ADMITTED else `ERROR let finish_task name (u,cst,_) d p l i = @@ -1935,15 +1956,16 @@ end = struct (* {{{ *) let vernac_interp ~solve ~abstract ~cancel_switch nworkers safe_id id { indentation; verbose; loc; expr = e; strlen } = - let e, time, fail = - let rec find ~time ~fail = function - | VernacTime (_,e) -> find ~time:true ~fail e - | VernacRedirect (_,(_,e)) -> find ~time ~fail e - | VernacFail e -> find ~time ~fail:true e - | e -> e, time, fail in find ~time:false ~fail:false e in + let e, time, batch, fail = + let rec find ~time ~batch ~fail = function + | VernacTime (batch,{CAst.v=e}) -> find ~time:true ~batch ~fail e + | VernacRedirect (_,{CAst.v=e}) -> find ~time ~batch ~fail e + | VernacFail e -> find ~time ~batch ~fail:true e + | e -> e, time, batch, fail in + find ~time:false ~batch:false ~fail:false e in let st = Vernacstate.freeze_interp_state `No in Vernacentries.with_fail st fail (fun () -> - (if time then System.with_time !Flags.time else (fun x -> x)) (fun () -> + (if time then System.with_time ~batch else (fun x -> x)) (fun () -> ignore(TaskQueue.with_n_workers nworkers (fun queue -> Proof_global.with_current_proof (fun _ p -> let goals, _, _, _, _ = Proof.proof p in @@ -2073,7 +2095,7 @@ end = struct (* {{{ *) QueryTask.({ t_where = prev; t_for = id; t_what = q }) ~cancel_switch let init () = queue := Some (TaskQueue.create - (if !async_proofs_full then 1 else 0)) + (if !cur_opt.async_proofs_full then 1 else 0)) end (* }}} *) @@ -2086,17 +2108,16 @@ and Reach : sig end = struct (* {{{ *) let async_policy () = - let open Flags in - if is_universe_polymorphism () then false + if Flags.is_universe_polymorphism () then false else if VCS.is_interactive () = `Yes then - (async_proofs_is_master () || !async_proofs_mode = APonLazy) + (async_proofs_is_master !cur_opt || !cur_opt.async_proofs_mode = APonLazy) else - (VCS.is_vio_doc () || !async_proofs_mode <> APoff) + (VCS.is_vio_doc () || !cur_opt.async_proofs_mode <> APoff) let delegate name = - get_hint_bp_time name >= !async_proofs_delegation_threshold + get_hint_bp_time name >= !cur_opt.async_proofs_delegation_threshold || VCS.is_vio_doc () - || !async_proofs_full + || !cur_opt.async_proofs_full let warn_deprecated_nested_proofs = CWarnings.create ~name:"deprecated-nested-proofs" ~category:"deprecated" @@ -2176,7 +2197,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 <- VernacExpr([], VernacProof(t, Some hint)); `ASync (parent last,accn,name,delegate name) with Not_found -> let name = name ids in @@ -2211,7 +2232,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) || !async_proofs_full) + (not(State.is_cached_and_valid id) || !cur_opt.async_proofs_full) then check_policy rc else make_sync `AlreadyEvaluated rc @@ -2293,9 +2314,9 @@ let known_state ?(redefine_qed=false) ~cache id = (* Absorb tactic errors from f () *) let resilient_tactic id blockname f = - if !async_proofs_tac_error_resilience = `None || - (async_proofs_is_master () && - !async_proofs_mode = APoff) + if !cur_opt.async_proofs_tac_error_resilience = `None || + (async_proofs_is_master !cur_opt && + !cur_opt.async_proofs_mode = APoff) then f () else try f () @@ -2304,9 +2325,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 !async_proofs_cmd_error_resilience || - (async_proofs_is_master () && - !async_proofs_mode = APoff) + if not !cur_opt.async_proofs_cmd_error_resilience || + (async_proofs_is_master !cur_opt && + !cur_opt.async_proofs_mode = APoff) then f x else try f x @@ -2352,10 +2373,10 @@ let known_state ?(redefine_qed=false) ~cache id = resilient_tactic id cblock (fun () -> reach ~cache:`Shallow view.next; Partac.vernac_interp ~solve ~abstract ~cancel_switch - !async_proofs_n_tacworkers view.next id x) + !cur_opt.async_proofs_n_tacworkers view.next id x) ), cache, true | `Cmd { cast = x; cqueue = `QueryQueue cancel_switch } - when async_proofs_is_master () -> (fun () -> + when async_proofs_is_master !cur_opt -> (fun () -> reach view.next; Query.vernac_interp ~cancel_switch view.next id x ), cache, false @@ -2369,7 +2390,7 @@ let known_state ?(redefine_qed=false) ~cache id = if eff then update_global_env () ), (if eff then `Yes else cache), true | `Cmd { cast = x; ceff = eff } -> (fun () -> - (match !async_proofs_mode with + (match !cur_opt.async_proofs_mode with | APon | APonLazy -> resilient_command reach view.next | APoff -> reach view.next); @@ -2409,7 +2430,7 @@ let known_state ?(redefine_qed=false) ~cache id = | { VCS.kind = `Edit (_,_,_, okeep, _) }, Some (ofp, cancel) -> assert(redefine_qed = true); if okeep != keep then - msg_error(strbrk("The command closing the proof changed. " + msg_warning(strbrk("The command closing the proof changed. " ^"The kernel cannot take this into account and will " ^(if keep == VtKeep then "not check " else "reject ") ^"the "^(if keep == VtKeep then "new" else "incomplete") @@ -2461,7 +2482,7 @@ let known_state ?(redefine_qed=false) ~cache id = match keep with | VtDrop -> None | VtKeepAsAxiom -> - let ctx = Evd.empty_evar_universe_context in + let ctx = UState.empty in let fp = Future.from_val ([],ctx) in qed.fproof <- Some (fp, ref false); None | VtKeep -> @@ -2499,7 +2520,7 @@ let known_state ?(redefine_qed=false) ~cache id = ), cache, true in let cache_step = - if !async_proofs_cache = Some Force then `Yes + if !cur_opt.async_proofs_cache = Some Force then `Yes else cache_step in State.define ?safe_id ~cache:cache_step ~redefine:redefine_qed ~feedback_processed step id; @@ -2512,15 +2533,28 @@ end (* }}} *) (********************************* STM API ************************************) (******************************************************************************) +(* Main initalization routine *) type stm_init_options = { + (* The STM will set some internal flags differently depending on the + specified [doc_type]. This distinction should dissappear at some + some point. *) doc_type : stm_doc_type; + + (* Initial load path in scope for the document. Usually extracted + from -R options / _CoqProject *) + iload_path : Mltop.coq_path list; + + (* Require [require_libs] before the initial state is + ready. Parameters follow [Library], that is to say, + [lib,prefix,import_export] means require library [lib] from + optional [prefix] and [import_export] if [Some false/Some true] + is used. *) require_libs : (string * string option * bool option) list; -(* - fb_handler : Feedback.feedback -> unit; - iload_path : (string list * string * bool) list; - implicit_std : bool; -*) + + (* STM options that apply to the current document. *) + stm_options : AsyncOpts.stm_opt; } +(* fb_handler : Feedback.feedback -> unit; *) (* let doc_type_module_name (std : stm_doc_type) = @@ -2530,10 +2564,11 @@ let doc_type_module_name (std : stm_doc_type) = *) let init_core () = - if !async_proofs_mode = APon then Control.enable_thread_delay := true; + if !cur_opt.async_proofs_mode = APon then Control.enable_thread_delay := true; State.register_root_state () -let new_doc { doc_type ; require_libs } = +let new_doc { doc_type ; iload_path; require_libs; stm_options } = + let load_objs libs = let rq_file (dir, from, exp) = let mp = Libnames.(Qualid (Loc.tag @@ qualid_of_string dir)) in @@ -2542,11 +2577,19 @@ let new_doc { doc_type ; require_libs } = List.(iter rq_file (rev libs)) in + (* Set the options from the new documents *) + AsyncOpts.cur_opt := stm_options; + (* We must reset the whole state before creating a document! *) State.restore_root_state (); let doc = VCS.init doc_type Stateid.initial in + (* Set load path; important, this has to happen before we declare + the library below as [Declaremods/Library] will infer the module + name by looking at the load path! *) + List.iter Mltop.add_coq_path iload_path; + begin match doc_type with | Interactive ln -> Safe_typing.allow_delayed_constants := true; @@ -2563,16 +2606,18 @@ let new_doc { doc_type ; require_libs } = VCS.set_ldir ldir; set_compilation_hints ln end; + + (* Import initial libraries. *) load_objs require_libs; - (* We record the state here! *) + (* We record the state at this point! *) State.define ~cache:`Yes ~redefine:true (fun () -> ()) Stateid.initial; Backtrack.record (); Slaves.init (); - if async_proofs_is_master () then begin + if async_proofs_is_master !cur_opt then begin stm_prerr_endline (fun () -> "Initializing workers"); Query.init (); - let opts = match !async_proofs_private_flags with + let opts = match !cur_opt.async_proofs_private_flags with | None -> [] | Some s -> Str.split_delim (Str.regexp ",") s in begin try @@ -2658,7 +2703,7 @@ let finish_tasks name u d p (t,rcbackup as tasks) = (u,a,true), p with e -> let e = CErrors.push e in - msg_error (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e); + msg_warning (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e); exit 1 let merge_proof_branch ~valid ?id qast keep brname = @@ -2771,7 +2816,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 !async_proofs_full then `QueryQueue (ref false) + if !cur_opt.async_proofs_full then `QueryQueue (ref false) else if VCS.is_vio_doc () && VCS.((get_branch head).kind = `Master) && may_pierce_opaque (Vernacprop.under_control x.expr) @@ -2871,10 +2916,9 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) if not in_proof && Proof_global.there_are_pending_proofs () then begin let bname = VCS.mk_branch_name x in - let rec opacity_of_produced_term = function + let opacity_of_produced_term = function (* This AST is ambiguous, hence we check it dynamically *) | VernacInstance (false, _,_ , None, _) -> GuaranteesOpacity - | VernacLocal (_,e) -> opacity_of_produced_term e | _ -> Doesn'tGuaranteeOpacity in VCS.commit id (Fork (x,bname,opacity_of_produced_term (Vernacprop.under_control x.expr),[])); let proof_mode = default_proof_mode () in @@ -2907,6 +2951,7 @@ 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) | _ -> None @@ -3104,7 +3149,7 @@ let edit_at ~doc id = VCS.delete_boxes_of id; VCS.gc (); VCS.print (); - if not !async_proofs_full then + if not !cur_opt.async_proofs_full then Reach.known_state ~cache:(VCS.is_interactive ()) id; VCS.checkout_shallowest_proof_branch (); `NewTip in @@ -3120,7 +3165,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 !async_proofs_never_reopen_branch + if has_failed qed_id && is_pure qed_id && not !cur_opt.async_proofs_never_reopen_branch then reopen_branch start id mode qed_id tip bn else backto id (Some bn) | true, Some { qed = qed_id }, Some(mode,bn) -> diff --git a/stm/stm.mli b/stm/stm.mli index 587b756422..f967c98159 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -1,15 +1,44 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names (** state-transaction-machine interface *) +(* Flags *) +module AsyncOpts : sig + + type cache = Force + type async_proofs = APoff | APonLazy | APon + type tac_error_filter = [ `None | `Only of string list | `All ] + + type stm_opt = { + async_proofs_n_workers : int; + async_proofs_n_tacworkers : int; + + async_proofs_cache : cache option; + async_proofs_mode : async_proofs; + + async_proofs_private_flags : string option; + async_proofs_full : bool; + async_proofs_never_reopen_branch : bool; + + async_proofs_tac_error_resilience : tac_error_filter; + async_proofs_cmd_error_resilience : bool; + async_proofs_delegation_threshold : float; + } + + val default_opts : stm_opt + +end + (** The STM doc type determines some properties such as what uncompleted proofs are allowed and recording of aux files. *) type stm_doc_type = @@ -19,14 +48,26 @@ type stm_doc_type = (* Main initalization routine *) type stm_init_options = { + (* The STM will set some internal flags differently depending on the + specified [doc_type]. This distinction should dissappear at some + some point. *) doc_type : stm_doc_type; + + (* Initial load path in scope for the document. Usually extracted + from -R options / _CoqProject *) + iload_path : Mltop.coq_path list; + + (* Require [require_libs] before the initial state is + ready. Parameters follow [Library], that is to say, + [lib,prefix,import_export] means require library [lib] from + optional [prefix] and [import_export] if [Some false/Some true] + is used. *) require_libs : (string * string option * bool option) list; -(* - fb_handler : Feedback.feedback -> unit; - iload_path : (string list * string * bool) list; - implicit_std : bool; -*) + + (* STM options that apply to the current document. *) + stm_options : AsyncOpts.stm_opt; } +(* fb_handler : Feedback.feedback -> unit; *) (** The type of a STM document *) type doc @@ -228,27 +269,3 @@ 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/tQueue.ml b/stm/tQueue.ml index 56e8c41acd..33744e7323 100644 --- a/stm/tQueue.ml +++ b/stm/tQueue.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) module PriorityQueue : sig diff --git a/stm/tQueue.mli b/stm/tQueue.mli index f005b58ad1..e098c37f2a 100644 --- a/stm/tQueue.mli +++ b/stm/tQueue.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Thread safe queue with some extras *) diff --git a/stm/tacworkertop.ml b/stm/tacworkertop.ml index 17f90b7b15..3b91df86e0 100644 --- a/stm/tacworkertop.ml +++ b/stm/tacworkertop.ml @@ -1,14 +1,16 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) module W = AsyncTaskQueue.MakeWorker(Stm.TacTask) () let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout -let () = Coqtop.toploop_run := (fun _ -> W.main_loop ()) +let () = Coqtop.toploop_run := (fun _ ~state:_ -> W.main_loop ()) diff --git a/stm/vcs.ml b/stm/vcs.ml index 5d4a812fac..4bd46286bd 100644 --- a/stm/vcs.ml +++ b/stm/vcs.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp diff --git a/stm/vcs.mli b/stm/vcs.mli index 6148335676..47622ef6f1 100644 --- a/stm/vcs.mli +++ b/stm/vcs.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* This module builds a VCS like interface on top of Dag, used to build diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 1291b76426..48ccb8f4ce 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -1,15 +1,18 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Vernacexpr open CErrors open Util open Pp +open CAst +open Vernacexpr let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"] @@ -48,18 +51,19 @@ let declare_vernac_classifier = classifiers := !classifiers @ [s,f] +let idents_of_name : Names.Name.t -> Names.Id.t list = + function + | Names.Anonymous -> [] + | Names.Name n -> [n] + let classify_vernac e = - let rec static_classifier ~poly e = match e with + let static_classifier ~poly e = match e with (* Univ poly compatibility: we run it now, so that we can just * look at Flags in stm.ml. Would be nicer to have the stm * look at the entire dag to detect this option. *) | ( VernacSetOption (l,_) | VernacUnsetOption l) when CList.equal String.equal l Vernacentries.universe_polymorphism_option_name -> VtSideff [], VtNow - (* Nested vernac exprs *) - | VernacProgram e -> static_classifier ~poly e - | VernacLocal (_,e) -> static_classifier ~poly e - | VernacPolymorphic (b, e) -> static_classifier ~poly:b e (* Qed *) | VernacAbort _ -> VtQed VtDrop, VtLater | VernacEndProof Admitted -> VtQed VtKeepAsAxiom, VtLater @@ -86,26 +90,23 @@ let classify_vernac e = | VernacUnsetOption (["Default";"Proof";"Using"]) | VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow (* StartProof *) - | VernacDefinition ((Decl_kinds.DoDischarge,_),((_,i),_),ProveBody _) -> - VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity,[i]), VtLater - | VernacDefinition (_,((_,i),_),ProveBody _) -> + | VernacDefinition ((Decl_kinds.DoDischarge,_),({v=i},_),ProveBody _) -> + VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity, idents_of_name i), VtLater + + | VernacDefinition (_,({v=i},_),ProveBody _) -> let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in - VtStartProof(default_proof_mode (),guarantee,[i]), VtLater + VtStartProof(default_proof_mode (),guarantee, idents_of_name i), VtLater | VernacStartTheoremProof (_,l) -> - let ids = - CList.map_filter (function (Some ((_,i),pl), _) -> Some i | _ -> None) l in + let ids = List.map (fun (({v=i}, _), _) -> i) l in let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in VtStartProof (default_proof_mode (),guarantee,ids), VtLater - | VernacGoal _ -> - let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in - VtStartProof (default_proof_mode (),guarantee,[]), VtLater | VernacFixpoint (discharge,l) -> let guarantee = if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in let ids, open_proof = - List.fold_left (fun (l,b) ((((_,id),_),_,_,_,p),_) -> + List.fold_left (fun (l,b) ((({v=id},_),_,_,_,p),_) -> id::l, b || p = None) ([],false) l in if open_proof then VtStartProof (default_proof_mode (),guarantee,ids), VtLater @@ -116,29 +117,29 @@ let classify_vernac e = else GuaranteesOpacity in let ids, open_proof = - List.fold_left (fun (l,b) ((((_,id),_),_,_,p),_) -> + List.fold_left (fun (l,b) ((({v=id},_),_,_,p),_) -> id::l, b || p = None) ([],false) l in if open_proof then VtStartProof (default_proof_mode (),guarantee,ids), VtLater else VtSideff ids, VtLater (* Sideff: apply to all open branches. usually run on master only *) | VernacAssumption (_,_,l) -> - let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map (fun (id, _) -> snd id) l) l) in - VtSideff ids, VtLater - | VernacDefinition (_,((_,id),_),DefineBody _) -> VtSideff [id], VtLater + let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map (fun (id, _) -> id.v) l) l) in + VtSideff ids, VtLater + | VernacDefinition (_,({v=id},_),DefineBody _) -> VtSideff (idents_of_name id), VtLater | VernacInductive (_, _,_,l) -> - let ids = List.map (fun (((_,((_,id),_)),_,_,_,cl),_) -> id :: match cl with - | Constructors l -> List.map (fun (_,((_,id),_)) -> id) l - | RecordDecl (oid,l) -> (match oid with Some (_,x) -> [x] | _ -> []) @ + 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((_,Names.Name n),_)),_),_ -> Some n + | ((_,AssumExpr({v=Names.Name n},_)),_),_ -> Some n | _ -> None) l) l in VtSideff (List.flatten ids), VtLater | VernacScheme l -> - let ids = List.map snd (CList.map_filter (fun (x,_) -> x) l) in + let ids = List.map (fun {v}->v) (CList.map_filter (fun (x,_) -> x) l) in VtSideff ids, VtLater - | VernacCombinedScheme ((_,id),_) -> VtSideff [id], VtLater - | VernacBeginSection (_,id) -> VtSideff [id], VtLater + | VernacCombinedScheme ({v=id},_) -> VtSideff [id], VtLater + | VernacBeginSection {v=id} -> VtSideff [id], VtLater | VernacUniverse _ | VernacConstraint _ | VernacCanonical _ | VernacCoercion _ | VernacIdentityCoercion _ | VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _ @@ -162,10 +163,10 @@ let classify_vernac e = (* (Local) Notations have to disappear *) | VernacEndSegment _ -> VtSideff [], VtNow (* Modules with parameters have to be executed: can import notations *) - | VernacDeclareModule (exp,(_,id),bl,_) - | VernacDefineModule (exp,(_,id),bl,_,_) -> + | VernacDeclareModule (exp,{v=id},bl,_) + | VernacDefineModule (exp,{v=id},bl,_,_) -> VtSideff [id], if bl = [] && exp = None then VtLater else VtNow - | VernacDeclareModuleType ((_,id),bl,_,_) -> + | VernacDeclareModuleType ({v=id},bl,_,_) -> VtSideff [id], if bl = [] then VtLater else VtNow (* These commands alter the parser *) | VernacOpenCloseScope _ | VernacDelimiters _ | VernacBindScope _ @@ -193,9 +194,15 @@ let classify_vernac e = with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".") in let rec static_control_classifier ~poly = function - | VernacExpr e -> static_classifier ~poly e + | VernacExpr (f, e) -> + let poly = List.fold_left (fun poly f -> + match f with + | VernacPolymorphic b -> b + | (VernacProgram | VernacLocal _) -> poly + ) poly f in + static_classifier ~poly e | VernacTimeout (_,e) -> static_control_classifier ~poly e - | VernacTime (_,e) | VernacRedirect (_, (_,e)) -> + | VernacTime (_,{v=e}) | VernacRedirect (_, {v=e}) -> static_control_classifier ~poly e | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) (match static_control_classifier ~poly e with diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli index c0571c1d6f..abbc04e895 100644 --- a/stm/vernac_classifier.mli +++ b/stm/vernac_classifier.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Vernacexpr diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml index da6a095ab7..64f19e1fd9 100644 --- a/stm/vio_checking.ml +++ b/stm/vio_checking.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util diff --git a/stm/vio_checking.mli b/stm/vio_checking.mli index e05f11cb4e..177b3b2d06 100644 --- a/stm/vio_checking.mli +++ b/stm/vio_checking.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* [check_vio tasks file] checks the [tasks] stored in [file] *) diff --git a/stm/workerLoop.ml b/stm/workerLoop.ml index 7041191869..5445925b14 100644 --- a/stm/workerLoop.ml +++ b/stm/workerLoop.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Default priority *) @@ -15,8 +17,8 @@ let rec parse = function | x :: rest -> x :: parse rest | [] -> [] -let loop init args = - let args = parse args in +let loop init _coq_args extra_args = + let args = parse extra_args in Flags.quiet := true; init (); CoqworkmgrApi.init !async_proofs_worker_priority; diff --git a/stm/workerLoop.mli b/stm/workerLoop.mli index da2e6fe0cc..f02edb9bba 100644 --- a/stm/workerLoop.mli +++ b/stm/workerLoop.mli @@ -1,12 +1,14 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Default priority *) val async_proofs_worker_priority : CoqworkmgrApi.priority ref -val loop : (unit -> unit) -> string list -> string list +val loop : (unit -> unit) -> Coqargs.coq_cmdopts -> string list -> string list diff --git a/stm/workerPool.ml b/stm/workerPool.ml index ff4dc5c35e..0ff66686e4 100644 --- a/stm/workerPool.ml +++ b/stm/workerPool.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) type worker_id = string diff --git a/stm/workerPool.mli b/stm/workerPool.mli index de396d85b0..0f1237b584 100644 --- a/stm/workerPool.mli +++ b/stm/workerPool.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) type worker_id = string |