diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/asyncTaskQueue.ml | 18 | ||||
| -rw-r--r-- | stm/coqworkmgrApi.ml | 4 | ||||
| -rw-r--r-- | stm/coqworkmgrApi.mli | 3 | ||||
| -rw-r--r-- | stm/proofBlockDelimiter.ml | 6 | ||||
| -rw-r--r-- | stm/proofBlockDelimiter.mli | 4 | ||||
| -rw-r--r-- | stm/proofworkertop.ml | 16 | ||||
| -rw-r--r-- | stm/proofworkertop.mllib | 1 | ||||
| -rw-r--r-- | stm/queryworkertop.ml | 16 | ||||
| -rw-r--r-- | stm/queryworkertop.mllib | 1 | ||||
| -rw-r--r-- | stm/stm.ml | 214 | ||||
| -rw-r--r-- | stm/stm.mli | 47 | ||||
| -rw-r--r-- | stm/stm.mllib | 1 | ||||
| -rw-r--r-- | stm/tacworkertop.ml | 16 | ||||
| -rw-r--r-- | stm/tacworkertop.mllib | 1 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 23 | ||||
| -rw-r--r-- | stm/vernac_classifier.mli | 1 | ||||
| -rw-r--r-- | stm/workerLoop.ml | 25 | ||||
| -rw-r--r-- | stm/workerLoop.mli | 4 |
18 files changed, 172 insertions, 229 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index b3e1500ae4..768d94d305 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -60,7 +60,7 @@ module Make(T : Task) () = struct type request = Request of T.request type more_data = - | MoreDataUnivLevel of Universes.universe_id list + | MoreDataUnivLevel of UnivGen.universe_id list let slave_respond (Request r) = let res = T.perform r in @@ -120,12 +120,11 @@ module Make(T : Task) () = struct let proc, ic, oc = let rec set_slave_opt = function | [] -> !async_proofs_flags_for_workers @ - ["-toploop"; !T.name^"top"; - "-worker-id"; name; + ["-worker-id"; name; "-async-proofs-worker-priority"; - CoqworkmgrApi.(string_of_priority !WorkerLoop.async_proofs_worker_priority)] - | ("-ideslave"|"-emacs"|"-emacs-U"|"-batch")::tl -> set_slave_opt tl - | ("-async-proofs" |"-toploop" |"-vio2vo" + CoqworkmgrApi.(string_of_priority !async_proofs_worker_priority)] + | ("-emacs"|"-emacs-U"|"-batch")::tl -> set_slave_opt tl + | ("-async-proofs" |"-vio2vo" |"-load-vernac-source" |"-l" |"-load-vernac-source-verbose" |"-lv" |"-compile" |"-compile-verbose" |"-async-proofs-worker-priority" |"-worker-id") :: _ :: tl -> @@ -134,7 +133,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 - Worker.spawn ~env Sys.argv.(0) 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) = @@ -171,7 +171,7 @@ module Make(T : Task) () = struct | Unix.WSIGNALED sno -> Printf.sprintf "signalled(%d)" sno | Unix.WSTOPPED sno -> Printf.sprintf "stopped(%d)" sno) in let more_univs n = - CList.init n (fun _ -> Universes.new_univ_id ()) in + CList.init n (fun _ -> UnivGen.new_univ_id ()) in let rec kill_if () = if not (Worker.is_alive proc) then () @@ -310,7 +310,7 @@ module Make(T : Task) () = struct Marshal.to_channel oc (RespFeedback (debug_with_pid fb)) []; flush oc in ignore (Feedback.add_feeder (fun x -> slave_feeder (Option.get !slave_oc) x)); (* We ask master to allocate universe identifiers *) - Universes.set_remote_new_univ_id (bufferize (fun () -> + UnivGen.set_remote_new_univ_id (bufferize (fun () -> marshal_response (Option.get !slave_oc) RespGetCounterNewUnivLevel; match unmarshal_more_data (Option.get !slave_ic) with | MoreDataUnivLevel l -> l)); diff --git a/stm/coqworkmgrApi.ml b/stm/coqworkmgrApi.ml index 36b5d18ab6..841cc08c07 100644 --- a/stm/coqworkmgrApi.ml +++ b/stm/coqworkmgrApi.ml @@ -11,6 +11,10 @@ let debug = false type priority = Low | High + +(* Default priority *) +let async_proofs_worker_priority = ref Low + let string_of_priority = function Low -> "low" | High -> "high" let priority_of_string = function | "low" -> Low diff --git a/stm/coqworkmgrApi.mli b/stm/coqworkmgrApi.mli index 2983b619db..be5b291776 100644 --- a/stm/coqworkmgrApi.mli +++ b/stm/coqworkmgrApi.mli @@ -14,6 +14,9 @@ type priority = Low | High val string_of_priority : priority -> string val priority_of_string : string -> priority +(* Default priority *) +val async_proofs_worker_priority : priority ref + (* Connects to a work manager if any. If no worker manager, then -async-proofs-j and -async-proofs-tac-j are used *) val init : priority -> unit diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index 23f976120a..b8af2bcd56 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -23,8 +23,8 @@ val crawl : static_block_declaration option val unit_val : Stm.DynBlockData.t -val of_bullet_val : Vernacexpr.bullet -> Stm.DynBlockData.t -val to_bullet_val : Stm.DynBlockData.t -> Vernacexpr.bullet +val of_bullet_val : Proof_bullet.t -> Stm.DynBlockData.t +val to_bullet_val : Stm.DynBlockData.t -> Proof_bullet.t val of_vernac_control_val : Vernacexpr.vernac_control -> Stm.DynBlockData.t val to_vernac_control_val : Stm.DynBlockData.t -> Vernacexpr.vernac_control @@ -41,7 +41,7 @@ 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 evi.evar_concl) && + 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)) && not (List.exists (Proofview.depends_on sigma g) gs) diff --git a/stm/proofBlockDelimiter.mli b/stm/proofBlockDelimiter.mli index 9784de1141..eacd3687ae 100644 --- a/stm/proofBlockDelimiter.mli +++ b/stm/proofBlockDelimiter.mli @@ -38,6 +38,6 @@ val crawl : val unit_val : Stm.DynBlockData.t (* Bullets *) -val of_bullet_val : Vernacexpr.bullet -> Stm.DynBlockData.t -val to_bullet_val : Stm.DynBlockData.t -> Vernacexpr.bullet +val of_bullet_val : Proof_bullet.t -> Stm.DynBlockData.t +val to_bullet_val : Stm.DynBlockData.t -> Proof_bullet.t diff --git a/stm/proofworkertop.ml b/stm/proofworkertop.ml deleted file mode 100644 index 4b85a05ac7..0000000000 --- a/stm/proofworkertop.ml +++ /dev/null @@ -1,16 +0,0 @@ -(************************************************************************) -(* * 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 *) -(* * (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 _ ~state:_ -> W.main_loop ()) - diff --git a/stm/proofworkertop.mllib b/stm/proofworkertop.mllib deleted file mode 100644 index f9f6c22d51..0000000000 --- a/stm/proofworkertop.mllib +++ /dev/null @@ -1 +0,0 @@ -Proofworkertop diff --git a/stm/queryworkertop.ml b/stm/queryworkertop.ml deleted file mode 100644 index aa00102aab..0000000000 --- a/stm/queryworkertop.ml +++ /dev/null @@ -1,16 +0,0 @@ -(************************************************************************) -(* * 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 *) -(* * (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 _ ~state:_ -> W.main_loop ()) - diff --git a/stm/queryworkertop.mllib b/stm/queryworkertop.mllib deleted file mode 100644 index c2f73089b3..0000000000 --- a/stm/queryworkertop.mllib +++ /dev/null @@ -1 +0,0 @@ -Queryworkertop diff --git a/stm/stm.ml b/stm/stm.ml index 4b49d1998d..c394be22e1 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -92,11 +92,11 @@ let execution_error ?loc state_id msg = module Hooks = struct let state_computed, state_computed_hook = Hook.make - ~default:(fun state_id ~in_cache -> + ~default:(fun ~doc:_ state_id ~in_cache -> feedback ~id:state_id Processed) () let state_ready, state_ready_hook = Hook.make - ~default:(fun state_id -> ()) () + ~default:(fun ~doc:_ state_id -> ()) () let forward_feedback, forward_feedback_hook = let m = Mutex.create () in @@ -106,7 +106,7 @@ let forward_feedback, forward_feedback_hook = with e -> Mutex.unlock m; raise e) () let unreachable_state, unreachable_state_hook = Hook.make - ~default:(fun _ _ -> ()) () + ~default:(fun ~doc:_ _ _ -> ()) () include Hook @@ -578,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 !cur_opt then Hooks.(call state_ready id) + if async_proofs_is_master !cur_opt then Hooks.(call state_ready ~doc:dummy_doc (* XXX should be taken in input *) id) let get_state id = (get_info id).state let reached id = let info = get_info id in @@ -770,6 +770,7 @@ module State : sig Warning: an optimization in installed_cached requires that state modifying functions are always executed using this wrapper. *) val define : + doc:doc -> ?safe_id:Stateid.t -> ?redefine:bool -> ?cache:Summary.marshallable -> ?feedback_processed:bool -> (unit -> unit) -> Stateid.t -> unit @@ -919,7 +920,7 @@ end = struct (* {{{ *) let e2 = Summary.project_from_summary s2 Global.global_env_summary_tag in e1 == e2 - let define ?safe_id ?(redefine=false) ?(cache=`No) ?(feedback_processed=true) + let define ~doc ?safe_id ?(redefine=false) ?(cache=`No) ?(feedback_processed=true) f id = feedback ~id:id (ProcessingIn !Flags.async_proofs_worker_id); @@ -938,7 +939,7 @@ end = struct (* {{{ *) stm_prerr_endline (fun () -> "setting cur id to "^str_id); cur_id := id; if feedback_processed then - Hooks.(call state_computed id ~in_cache:false); + Hooks.(call state_computed ~doc id ~in_cache:false); VCS.reached id; if Proof_global.there_are_pending_proofs () then VCS.goals id (Proof_global.get_open_goals ()) @@ -954,7 +955,7 @@ end = struct (* {{{ *) | Some _, None -> (e, info) | Some (_,at), Some id -> (e, Stateid.add info ~valid:id at) in if cache = `Yes || cache = `Shallow then freeze_invalid id ie; - Hooks.(call unreachable_state id ie); + Hooks.(call unreachable_state ~doc id ie); Exninfo.iraise ie let init_state = ref None @@ -1072,7 +1073,7 @@ let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacstate.t let is_filtered_command = function | VernacResetName _ | VernacResetInitial | VernacBack _ | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _ - | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true + | VernacAbortAll | VernacAbort _ -> true | _ -> false in let aux_interp st expr = @@ -1097,7 +1098,6 @@ let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacstate.t module Backtrack : sig val record : unit -> unit - val backto : Stateid.t -> unit (* we could navigate the dag, but this ways easy *) val branches_of : Stateid.t -> backup @@ -1122,14 +1122,6 @@ end = struct (* {{{ *) info.vcs_backup <- backup, branches) [VCS.current_branch (); VCS.Branch.master] - let backto oid = - let info = VCS.get_info oid in - match info.vcs_backup with - | None, _ -> - anomaly Pp.(str"Backtrack.backto "++str(Stateid.to_string oid)++ - str": a state with no vcs_backup.") - | Some vcs, _ -> VCS.restore vcs - let branches_of id = let info = VCS.get_info id in match info.vcs_backup with @@ -1220,7 +1212,6 @@ end = struct (* {{{ *) match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ()) () id in oid, VtLater - | VernacBacktrack (id,_,_) | VernacBackTo id -> Stateid.of_int id, VtNow | _ -> anomaly Pp.(str "incorrect VtMeta classification") @@ -1362,6 +1353,7 @@ module rec ProofTask : sig and type request := request val build_proof_here : + doc:doc -> ?loc:Loc.t -> drop_pt:bool -> Stateid.t * Stateid.t -> Stateid.t -> @@ -1476,11 +1468,12 @@ end = struct (* {{{ *) execution_error start (Pp.strbrk s); feedback (InProgress ~-1) - let build_proof_here ?loc ~drop_pt (id,valid) eop = + let build_proof_here ~doc ?loc ~drop_pt (id,valid) eop = Future.create (State.exn_on id ~valid) (fun () -> let wall_clock1 = Unix.gettimeofday () in - if VCS.is_interactive () = `No then Reach.known_state ~cache:`No eop - else Reach.known_state ~cache:`Shallow eop; + if VCS.is_interactive () = `No + then Reach.known_state ~doc ~cache:`No eop + else Reach.known_state ~doc ~cache:`Shallow eop; let wall_clock2 = Unix.gettimeofday () in Aux_file.record_in_aux_at ?loc "proof_build_time" (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1)); @@ -1494,7 +1487,7 @@ end = struct (* {{{ *) VCS.print (); let proof, future_proof, time = let wall_clock = Unix.gettimeofday () in - let fp = build_proof_here ?loc ~drop_pt:drop exn_info stop in + let fp = build_proof_here ~doc:dummy_doc (* XXX should be document *) ?loc ~drop_pt:drop exn_info stop in let proof = Future.force fp in proof, fp, Unix.gettimeofday () -. wall_clock in (* We typecheck the proof with the kernel (in the worker) to spot @@ -1518,7 +1511,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 (Proof_global.Opaque,None))) }) in ignore(Future.join checked_proof); end; (* STATE: Restore the state XXX: handle exn *) @@ -1587,7 +1580,7 @@ end = struct (* {{{ *) 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)); + t_assign(`Comp(build_proof_here ~doc:dummy_doc (* XXX should be stored in a closure, it is the same doc that was used to generate the task *) ?loc:t_loc ~drop_pt t_exn_info t_stop)); feedback (InProgress ~-1) end (* }}} *) @@ -1597,6 +1590,7 @@ and Slaves : sig (* (eventually) remote calls *) val build_proof : + doc:doc -> ?loc:Loc.t -> drop_pt:bool -> exn_info:(Stateid.t * Stateid.t) -> block_start:Stateid.t -> block_stop:Stateid.t -> name:string -> future_proof * AsyncTaskQueue.cancel_switch @@ -1644,7 +1638,7 @@ end = struct (* {{{ *) with VCS.Expired -> cur in aux stop in try - Reach.known_state ~cache:`No stop; + Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:`No stop; if drop then let _proof = Proof_global.return_proof ~allow_partial:true () in `OK_ADMITTED @@ -1657,7 +1651,7 @@ end = struct (* {{{ *) Proof_global.close_proof ~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 ~cache:`No start; + Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:`No start; (* STATE SPEC: * - start: First non-expired state! [This looks very fishy] * - end : start + qed @@ -1667,7 +1661,7 @@ 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 (Proof_global.Opaque,None))) }); `OK proof end with e -> @@ -1764,7 +1758,7 @@ end = struct (* {{{ *) BuildProof { t_states = s2 } -> overlap_rel s1 s2 | _ -> 0) - let build_proof ?loc ~drop_pt ~exn_info ~block_start ~block_stop ~name:pname = + let build_proof ~doc ?loc ~drop_pt ~exn_info ~block_start ~block_stop ~name:pname = let id, valid as t_exn_info = exn_info in let cancel_switch = ref false in if TaskQueue.n_workers (Option.get !queue) = 0 then @@ -1779,7 +1773,7 @@ end = struct (* {{{ *) TaskQueue.enqueue_task (Option.get !queue) task ~cancel_switch; f, cancel_switch end else - ProofTask.build_proof_here ?loc ~drop_pt t_exn_info block_stop, cancel_switch + ProofTask.build_proof_here ~doc ?loc ~drop_pt t_exn_info block_stop, cancel_switch else let f, t_assign = Future.create_delegate ~name:pname (State.exn_on id ~valid) in let t_uuid = Future.uuid f in @@ -1855,7 +1849,7 @@ end = struct (* {{{ *) | RespError of Pp.t | RespNoProgress - let name = ref "tacworker" + let name = ref "tacticworker" let extra_env () = [||] type competence = unit type worker_status = Fresh | Old of competence @@ -1902,11 +1896,11 @@ end = struct (* {{{ *) let perform { r_state = id; r_state_fb; r_document = vcs; r_ast; r_goal } = Option.iter VCS.restore vcs; try - Reach.known_state ~cache:`No id; + Reach.known_state ~doc:dummy_doc (* XXX should be vcs *) ~cache:`No id; stm_purify (fun () -> let _,_,_,_,sigma0 = Proof.proof (Proof_global.give_me_the_proof ()) in let g = Evd.find sigma0 r_goal in - let is_ground c = Evarutil.is_ground_term sigma0 (EConstr.of_constr c) in + let is_ground c = Evarutil.is_ground_term sigma0 c in if not ( is_ground Evd.(evar_concl g) && List.for_all (Context.Named.Declaration.for_all is_ground) @@ -1929,7 +1923,6 @@ end = struct (* {{{ *) match Evd.(evar_body (find sigma r_goal)) with | Evd.Evar_empty -> RespNoProgress | Evd.Evar_defined t -> - let t = EConstr.of_constr t in let t = Evarutil.nf_evar sigma t in if Evarutil.is_ground_term sigma t then let t = EConstr.Unsafe.to_constr t in @@ -2058,7 +2051,7 @@ end = struct (* {{{ *) let perform { r_where; r_doc; r_what; r_for } = VCS.restore r_doc; VCS.print (); - Reach.known_state ~cache:`No r_where; + Reach.known_state ~doc:dummy_doc (* XXX should be r_doc *) ~cache:`No r_where; (* STATE *) let st = Vernacstate.freeze_interp_state `No in try @@ -2103,7 +2096,8 @@ end (* }}} *) and Reach : sig val known_state : - ?redefine_qed:bool -> cache:Summary.marshallable -> Stateid.t -> unit + doc:doc -> ?redefine_qed:bool -> cache:Summary.marshallable -> + Stateid.t -> unit end = struct (* {{{ *) @@ -2119,12 +2113,6 @@ let delegate name = || VCS.is_vio_doc () || !cur_opt.async_proofs_full -let warn_deprecated_nested_proofs = - CWarnings.create ~name:"deprecated-nested-proofs" ~category:"deprecated" - (fun () -> - strbrk ("Nested proofs are deprecated and will "^ - "stop working in a future Coq version")) - let collect_proof keep cur hd brkind id = stm_prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id); let no_name = "" in @@ -2133,7 +2121,7 @@ let collect_proof keep cur hd brkind id = | id :: _ -> Names.Id.to_string id in let loc = (snd cur).loc in let is_defined_expr = function - | VernacEndProof (Proved (Transparent,_)) -> true + | VernacEndProof (Proved (Proof_global.Transparent,_)) -> true | _ -> false in let is_defined = function | _, { expr = e } -> is_defined_expr (Vernacprop.under_control e) @@ -2206,8 +2194,7 @@ let collect_proof keep cur hd brkind id = assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch); let name = name ids in `MaybeASync (parent last, accn, name, delegate name) - | `Sideff _ -> - warn_deprecated_nested_proofs (); + | `Sideff (CherryPickEnv,_) -> `Sync (no_name,`NestedProof) | _ -> `Sync (no_name,`Unknown) in let make_sync why = function @@ -2261,7 +2248,7 @@ let log_processing_sync id name reason = log_string Printf.(sprintf let wall_clock_last_fork = ref 0.0 -let known_state ?(redefine_qed=false) ~cache id = +let known_state ~doc ?(redefine_qed=false) ~cache id = let error_absorbing_tactic id blockname exn = (* We keep the static/dynamic part of block detection separate, since @@ -2294,7 +2281,7 @@ let known_state ?(redefine_qed=false) ~cache id = Proof_global.unfreeze proof; Proof_global.with_current_proof (fun _ p -> feedback ~id:id Feedback.AddedAxiom; - fst (Pfedit.solve Vernacexpr.SelectAll None tac p), ()); + fst (Pfedit.solve Goal_select.SelectAll None tac p), ()); (* STATE SPEC: * - start: Modifies the input state adding a proof. * - end : maybe after recovery command. @@ -2356,7 +2343,7 @@ let known_state ?(redefine_qed=false) ~cache id = and reach ?safe_id ?(redefine_qed=false) ?(cache=cache) id = stm_prerr_endline (fun () -> "reaching: " ^ Stateid.to_string id); if not redefine_qed && State.is_cached ~cache id then begin - Hooks.(call state_computed id ~in_cache:true); + Hooks.(call state_computed ~doc id ~in_cache:true); stm_prerr_endline (fun () -> "reached (cache)"); State.install_cached id end else @@ -2437,7 +2424,7 @@ let known_state ?(redefine_qed=false) ~cache id = ^" proof. Reprocess the command declaring " ^"the proof's statement to avoid that.")); let fp, cancel = - Slaves.build_proof + Slaves.build_proof ~doc ?loc ~drop_pt ~exn_info ~block_start ~block_stop ~name in Future.replace ofp fp; qed.fproof <- Some (fp, cancel); @@ -2449,10 +2436,10 @@ let known_state ?(redefine_qed=false) ~cache id = reach ~cache:`Shallow block_start; let fp, cancel = if delegate then - Slaves.build_proof + Slaves.build_proof ~doc ?loc ~drop_pt ~exn_info ~block_start ~block_stop ~name else - ProofTask.build_proof_here ?loc + ProofTask.build_proof_here ~doc ?loc ~drop_pt exn_info block_stop, ref false in qed.fproof <- Some (fp, cancel); @@ -2522,7 +2509,7 @@ let known_state ?(redefine_qed=false) ~cache id = let cache_step = if !cur_opt.async_proofs_cache = Some Force then `Yes else cache_step in - State.define ?safe_id + State.define ~doc ?safe_id ~cache:cache_step ~redefine:redefine_qed ~feedback_processed step id; stm_prerr_endline (fun () -> "reached: "^ Stateid.to_string id) in reach ~redefine_qed id @@ -2611,7 +2598,7 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = load_objs require_libs; (* We record the state at this point! *) - State.define ~cache:`Yes ~redefine:true (fun () -> ()) Stateid.initial; + State.define ~doc ~cache:`Yes ~redefine:true (fun () -> ()) Stateid.initial; Backtrack.record (); Slaves.init (); if async_proofs_is_master !cur_opt then begin @@ -2632,7 +2619,7 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = let observe ~doc id = let vcs = VCS.backup () in try - Reach.known_state ~cache:(VCS.is_interactive ()) id; + Reach.known_state ~doc ~cache:(VCS.is_interactive ()) id; VCS.print (); doc with e -> @@ -2725,7 +2712,7 @@ let merge_proof_branch ~valid ?id qast keep brname = VCS.rewrite_merge qed_id ~ours:(Qed (qed ofp)) ~at:master_id brname; VCS.delete_branch brname; VCS.gc (); - let _st = Reach.known_state ~redefine_qed:true ~cache:`No qed_id in + let _st : unit = Reach.known_state ~doc:dummy_doc (* XXX should be taken in input *) ~redefine_qed:true ~cache:`No qed_id in VCS.checkout VCS.Branch.master; `Unfocus qed_id | { VCS.kind = `Master } -> @@ -2757,9 +2744,7 @@ let snapshot_vio ~doc ldir long_f_dot_vo = let reset_task_queue = Slaves.reset_task_queue (* Document building *) -let process_back_meta_command ~part_of_script ~newtip ~head oid aast w = - match part_of_script, w with - | true, w -> +let process_back_meta_command ~newtip ~head oid aast w = let id = VCS.new_node ~id:newtip () in let { mine; others } = Backtrack.branches_of oid in let valid = VCS.get_branch_pos head in @@ -2779,16 +2764,15 @@ let process_back_meta_command ~part_of_script ~newtip ~head oid aast w = VCS.commit id (Alias (oid,aast)); Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok - | false, VtNow -> - stm_prerr_endline (fun () -> "undo to state " ^ Stateid.to_string oid); - Backtrack.backto oid; - VCS.checkout_shallowest_proof_branch (); - Reach.known_state ~cache:(VCS.is_interactive ()) oid; `Ok - - | false, VtLater -> - anomaly(str"undo classifier: VtMeta + VtLater must imply part_of_script.") +let allow_nested_proofs = ref false +let _ = Goptions.declare_bool_option + { Goptions.optdepr = false; + Goptions.optname = "Nested Proofs Allowed"; + Goptions.optkey = Vernac_classifier.stm_allow_nested_proofs_option_name; + Goptions.optread = (fun () -> !allow_nested_proofs); + Goptions.optwrite = (fun b -> allow_nested_proofs := b) } -let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) +let process_transaction ~doc ?(newtip=Stateid.fresh ()) ({ verbose; loc; expr } as x) c = stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x); let vcs = VCS.backup () in @@ -2802,22 +2786,10 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) (* Meta *) | VtMeta, _ -> let id, w = Backtrack.undo_vernac_classifier expr in - (* Special case Backtrack, as it is never part of a script. See #6240 *) - let part_of_script = begin match Vernacprop.under_control expr with - | VernacBacktrack _ -> false - | _ -> part_of_script - end in - process_back_meta_command ~part_of_script ~newtip ~head id x w + process_back_meta_command ~newtip ~head id x w + (* Query *) - | VtQuery (false,route), VtNow -> - let query_sid = VCS.cur_tip () in - (try - let st = Vernacstate.freeze_interp_state `No in - ignore(stm_vernac_interp ~route query_sid st x) - with e -> - let e = CErrors.push e in - Exninfo.iraise (State.exn_on ~valid:Stateid.dummy query_sid e)); `Ok - | VtQuery (true, route), w -> + | VtQuery, w -> let id = VCS.new_node ~id:newtip () in let queue = if !cur_opt.async_proofs_full then `QueryQueue (ref false) @@ -2829,11 +2801,17 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) VCS.commit id (mkTransCmd x [] false queue); Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok - | VtQuery (false,_), VtLater -> - anomaly(str"classifier: VtQuery + VtLater must imply part_of_script.") - (* Proof *) | VtStartProof (mode, guarantee, names), w -> + + if not !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 + |> Exninfo.iraise + else + let id = VCS.new_node ~id:newtip () in let bname = VCS.mk_branch_name x in VCS.checkout VCS.Branch.master; @@ -2884,18 +2862,22 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); rc - (* Side effect on all branches *) + (* Side effect in a (still open) proof is replayed on all branches*) | VtSideff l, w -> - let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in let id = VCS.new_node ~id:newtip () in - VCS.checkout VCS.Branch.master; - VCS.commit id (mkTransCmd x l in_proof `MainQueue); - (* We can't replay a Definition since universes may be differently - * inferred. This holds in Coq >= 8.5 *) - let action = match Vernacprop.under_control x.expr with - | VernacDefinition(_, _, DefineBody _) -> CherryPickEnv - | _ -> ReplayCommand x in - VCS.propagate_sideff ~action; + begin match (VCS.get_branch head).VCS.kind with + | `Edit _ -> VCS.commit id (mkTransCmd x l true `MainQueue); + | `Master -> VCS.commit id (mkTransCmd x l false `MainQueue); + | `Proof _ -> + VCS.checkout VCS.Branch.master; + 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 + | VernacDefinition(_, _, DefineBody _) -> CherryPickEnv + | _ -> ReplayCommand x in + VCS.propagate_sideff ~action; + end; VCS.checkout_shallowest_proof_branch (); Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok @@ -2904,11 +2886,11 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in let id = VCS.new_node ~id:newtip () in let head_id = VCS.get_branch_pos head in - let _st = Reach.known_state ~cache:`Yes head_id in (* ensure it is ok *) + let _st : unit = Reach.known_state ~doc ~cache:`Yes 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' = Reach.known_state ~cache:(VCS.is_interactive ()) mid in + let _st' : unit = Reach.known_state ~doc ~cache:(VCS.is_interactive ()) mid in let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id st x); (* Vernac x may or may not start a proof *) @@ -2924,12 +2906,17 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) VCS.branch bname (`Proof (proof_mode, VCS.proof_nesting () + 1)); Proof_global.activate_proof_mode proof_mode [@ocaml.warning "-3"]; end else begin - VCS.commit id (mkTransCmd x [] in_proof `MainQueue); - (* We hope it can be replayed, but we can't really know *) - VCS.propagate_sideff ~action:(ReplayCommand x); + 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 *) + VCS.propagate_sideff ~action:(ReplayCommand x); + end; VCS.checkout_shallowest_proof_branch (); end in - State.define ~safe_id:head_id ~cache:`Yes step id; + State.define ~doc ~safe_id:head_id ~cache:`Yes step id; Backtrack.record (); `Ok | VtUnknown, VtLater -> @@ -2989,7 +2976,7 @@ let parse_sentence ~doc sid pa = str "All is good if not parsing changes occur between the two states, however if they do, a problem might occur."); Flags.with_option Flags.we_are_parsing (fun () -> try - match Pcoq.Gram.entry_parse Pcoq.main_entry pa with + match Pcoq.Gram.entry_parse Pvernac.main_entry pa with | None -> raise End_of_input | Some (loc, cmd) -> CAst.make ~loc cmd with e when CErrors.noncritical e -> @@ -3040,11 +3027,10 @@ let add ~doc ~ontop ?newtip verb { CAst.loc; v=ast } = str ") than the tip: " ++ str (Stateid.to_string cur_tip) ++ str "." ++ fnl () ++ str "This is not supported yet, sorry."); let indentation, strlen = compute_indentation ?loc ontop in - CWarnings.set_current_loc loc; (* 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 - match process_transaction ?newtip aast clas with + match process_transaction ~doc ?newtip aast clas with | `Ok -> doc, VCS.cur_tip (), `NewTip | `Unfocus qed_id -> doc, qed_id, `Unfocus (VCS.cur_tip ()) @@ -3059,19 +3045,14 @@ type focus = { let query ~doc ~at ~route s = stm_purify (fun s -> if Stateid.equal at Stateid.dummy then ignore(finish ~doc:dummy_doc) - else Reach.known_state ~cache:`Yes at; + else Reach.known_state ~doc ~cache:`Yes at; try while true do let { CAst.loc; v=ast } = parse_sentence ~doc at s in let indentation, strlen = compute_indentation ?loc at in - CWarnings.set_current_loc loc; - let clas = Vernac_classifier.classify_vernac ast in + let st = State.get_cached at in let aast = { verbose = true; indentation; strlen; loc; expr = ast } in - match clas with - | VtMeta , _ -> (* TODO: can this still happen ? *) - ignore(process_transaction ~part_of_script:false aast (VtMeta,VtNow)) - | _ -> - ignore(process_transaction aast (VtQuery (false,route), VtNow)) + ignore(stm_vernac_interp ~route at st aast) done; with | End_of_input -> () @@ -3126,7 +3107,7 @@ let edit_at ~doc id = VCS.edit_branch (`Edit (mode, qed_id, master_id, keep, old_branch)); VCS.delete_boxes_of id; cancel_switch := true; - Reach.known_state ~cache:(VCS.is_interactive ()) id; + Reach.known_state ~doc ~cache:(VCS.is_interactive ()) id; VCS.checkout_shallowest_proof_branch (); `Focus { stop = qed_id; start = master_id; tip } in let no_edit = function @@ -3149,7 +3130,7 @@ let edit_at ~doc id = VCS.gc (); VCS.print (); if not !cur_opt.async_proofs_full then - Reach.known_state ~cache:(VCS.is_interactive ()) id; + Reach.known_state ~doc ~cache:(VCS.is_interactive ()) id; VCS.checkout_shallowest_proof_branch (); `NewTip in try @@ -3178,7 +3159,7 @@ let edit_at ~doc id = | true, None, _ -> if on_cur_branch id then begin VCS.reset_branch (VCS.current_branch ()) id; - Reach.known_state ~cache:(VCS.is_interactive ()) id; + Reach.known_state ~doc ~cache:(VCS.is_interactive ()) id; VCS.checkout_shallowest_proof_branch (); `NewTip end else if is_ancestor_of_cur_branch id then begin @@ -3241,4 +3222,9 @@ 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) +type document = VCS.vcs +let backup () = VCS.backup () +let restore d = VCS.restore d + + (* vim:set foldmethod=marker: *) diff --git a/stm/stm.mli b/stm/stm.mli index a8eb10fb33..aed7274d06 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -39,14 +39,25 @@ module AsyncOpts : sig end -(** The STM doc type determines some properties such as what - uncompleted proofs are allowed and recording of aux files. *) +(** The STM document type [stm_doc_type] determines some properties + such as what uncompleted proofs are allowed and what gets recorded + to aux files. *) type stm_doc_type = - | VoDoc of string - | VioDoc of string - | Interactive of DirPath.t + | VoDoc of string (* file path *) + | VioDoc of string (* file path *) + | Interactive of DirPath.t (* module path *) -(* Main initalization routine *) +(** Coq initalization options: + + - [doc_type]: Type of document being created. + + - [require_libs]: list of libraries/modules to be pre-loaded at + startup. A tuple [(modname,modfrom,import)] is equivalent to [From + modfrom Require modname]; [import] works similarly to + [Library.require_library_from_dirpath], [Some false] will import + the module, [Some true] will additionally export it. + +*) type stm_init_options = { (* The STM will set some internal flags differently depending on the specified [doc_type]. This distinction should dissappear at some @@ -72,12 +83,14 @@ type stm_init_options = { (** The type of a STM document *) type doc +(** [init_core] performs some low-level initalization; should go away + in future releases. *) val init_core : unit -> unit -(* Starts a new document *) +(** [new_doc opt] Creates a new document with options [opt] *) val new_doc : stm_init_options -> doc * Stateid.t -(* [parse_sentence sid pa] Reads a sentence from [pa] with parsing +(** [parse_sentence sid pa] Reads a sentence from [pa] with parsing state [sid] Returns [End_of_input] if the stream ends *) val parse_sentence : doc:doc -> Stateid.t -> Pcoq.Gram.coq_parsable -> Vernacexpr.vernac_control CAst.t @@ -115,14 +128,15 @@ val query : doc:doc -> type focus = { start : Stateid.t; stop : Stateid.t; tip : Stateid.t } val edit_at : doc:doc -> Stateid.t -> doc * [ `NewTip | `Focus of focus ] -(* Evaluates the tip of the current branch *) +(* [observe doc sid]] Check / execute span [sid] *) +val observe : doc:doc -> Stateid.t -> doc + +(* [finish doc] Fully checks a document up to the "current" tip. *) val finish : doc:doc -> doc (* Internal use (fake_ide) only, do not use *) val wait : doc:doc -> doc -val observe : doc:doc -> Stateid.t -> doc - val stop_worker : string -> unit (* Joins the entire document. Implies finish, but also checks proofs *) @@ -249,11 +263,12 @@ val register_proof_block_delimiter : * the alternative toploop for the worker can be selected by changing * the name of the Task(s) above) *) -val state_computed_hook : (Stateid.t -> in_cache:bool -> unit) Hook.t -val unreachable_state_hook : (Stateid.t -> Exninfo.iexn -> unit) Hook.t +val state_computed_hook : (doc:doc -> Stateid.t -> in_cache:bool -> unit) Hook.t +val unreachable_state_hook : + (doc:doc -> Stateid.t -> Exninfo.iexn -> unit) Hook.t (* ready means that master has it at hand *) -val state_ready_hook : (Stateid.t -> unit) Hook.t +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 @@ -269,3 +284,7 @@ val get_all_proof_names : doc:doc -> Id.t list (** Enable STM debugging *) val stm_debug : bool ref + +type document +val backup : unit -> document +val restore : document -> unit diff --git a/stm/stm.mllib b/stm/stm.mllib index 72b5380162..4b254e8113 100644 --- a/stm/stm.mllib +++ b/stm/stm.mllib @@ -5,7 +5,6 @@ TQueue WorkerPool Vernac_classifier CoqworkmgrApi -WorkerLoop AsyncTaskQueue Stm ProofBlockDelimiter diff --git a/stm/tacworkertop.ml b/stm/tacworkertop.ml deleted file mode 100644 index 3b91df86e0..0000000000 --- a/stm/tacworkertop.ml +++ /dev/null @@ -1,16 +0,0 @@ -(************************************************************************) -(* * 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 *) -(* * (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 _ ~state:_ -> W.main_loop ()) - diff --git a/stm/tacworkertop.mllib b/stm/tacworkertop.mllib deleted file mode 100644 index db38fde279..0000000000 --- a/stm/tacworkertop.mllib +++ /dev/null @@ -1 +0,0 @@ -Tacworkertop diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 9a8af3a58c..e01dcbcb6e 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -16,8 +16,6 @@ open Vernacexpr let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"] -let string_of_in_script b = if b then " (inside script)" else "" - let string_of_parallel = function | `Yes (solve,abs) -> "par" ^ if solve then "solve" else "" ^ if abs then "abs" else "" @@ -34,7 +32,7 @@ let string_of_vernac_type = function "ProofStep " ^ string_of_parallel parallel ^ Option.default "" proof_block_detection | VtProofMode s -> "ProofMode " ^ s - | VtQuery (b, route) -> "Query " ^ string_of_in_script b ^ " route " ^ string_of_int route + | VtQuery -> "Query" | VtMeta -> "Meta " let string_of_vernac_when = function @@ -56,13 +54,20 @@ let idents_of_name : Names.Name.t -> Names.Id.t list = | Names.Anonymous -> [] | Names.Name n -> [n] +let stm_allow_nested_proofs_option_name = ["Nested";"Proofs";"Allowed"] + +let options_affecting_stm_scheduling = + [ Vernacentries.universe_polymorphism_option_name; + stm_allow_nested_proofs_option_name ] + let classify_vernac e = let static_classifier ~poly e = match e with (* Univ poly compatibility: we run it now, so that we can just * look at Flags in stm.ml. Would be nicer to have the stm * look at the entire dag to detect this option. *) | ( VernacSetOption (_, l,_) | VernacUnsetOption (_, l)) - when CList.equal String.equal l Vernacentries.universe_polymorphism_option_name -> + when CList.exists (CList.equal String.equal l) + options_affecting_stm_scheduling -> VtSideff [], VtNow (* Qed *) | VernacAbort _ -> VtQed VtDrop, VtLater @@ -70,7 +75,7 @@ let classify_vernac e = | VernacEndProof _ | VernacExactProof _ -> VtQed VtKeep, VtLater (* Query *) | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _ - | VernacCheckMayEval _ -> VtQuery (true,Feedback.default_route), VtLater + | VernacCheckMayEval _ -> VtQuery, VtLater (* ProofStep *) | VernacProof _ | VernacFocus _ | VernacUnfocus @@ -145,7 +150,7 @@ let classify_vernac e = | VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _ | VernacChdir _ | VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _ - | VernacDeclareImplicits _ | VernacArguments _ | VernacArgumentsScope _ + | VernacArguments _ | VernacReserve _ | VernacGeneralizable _ | VernacSetOpacity _ | VernacSetStrategy _ @@ -183,7 +188,7 @@ let classify_vernac e = | VernacBack _ | VernacAbortAll | VernacUndoTo _ | VernacUndo _ | VernacResetName _ | VernacResetInitial - | VernacBacktrack _ | VernacBackTo _ | VernacRestart -> VtMeta, VtNow + | VernacBackTo _ | VernacRestart -> VtMeta, VtNow (* What are these? *) | VernacRestoreState _ | VernacWriteState _ -> VtSideff [], VtNow @@ -205,7 +210,7 @@ let classify_vernac e = static_control_classifier ~poly e | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) (match static_control_classifier ~poly e with - | ( VtQuery _ | VtProofStep _ | VtSideff _ + | ( VtQuery | VtProofStep _ | VtSideff _ | VtProofMode _ | VtMeta), _ as x -> x | VtQed _, _ -> VtProofStep { parallel = `No; proof_block_detection = None }, @@ -214,6 +219,6 @@ let classify_vernac e = in static_control_classifier ~poly:(Flags.is_universe_polymorphism ()) e -let classify_as_query = VtQuery (true,Feedback.default_route), VtLater +let classify_as_query = VtQuery, VtLater let classify_as_sideeff = VtSideff [], VtLater let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}, VtLater diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli index abbc04e895..45fbfb42af 100644 --- a/stm/vernac_classifier.mli +++ b/stm/vernac_classifier.mli @@ -25,3 +25,4 @@ val classify_as_query : vernac_classification val classify_as_sideeff : vernac_classification val classify_as_proofstep : vernac_classification +val stm_allow_nested_proofs_option_name : string list diff --git a/stm/workerLoop.ml b/stm/workerLoop.ml deleted file mode 100644 index 5445925b14..0000000000 --- a/stm/workerLoop.ml +++ /dev/null @@ -1,25 +0,0 @@ -(************************************************************************) -(* * 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 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(* Default priority *) -open CoqworkmgrApi -let async_proofs_worker_priority = ref Low - -let rec parse = function - | "--xml_format=Ppcmds" :: rest -> parse rest - | x :: rest -> x :: parse rest - | [] -> [] - -let loop init _coq_args extra_args = - let args = parse extra_args in - Flags.quiet := true; - init (); - CoqworkmgrApi.init !async_proofs_worker_priority; - args diff --git a/stm/workerLoop.mli b/stm/workerLoop.mli index f02edb9bba..37ec6dacca 100644 --- a/stm/workerLoop.mli +++ b/stm/workerLoop.mli @@ -11,4 +11,6 @@ (* Default priority *) val async_proofs_worker_priority : CoqworkmgrApi.priority ref -val loop : (unit -> unit) -> Coqargs.coq_cmdopts -> string list -> string list +val loop : + (unit -> unit) -> Coqargs.coq_cmdopts -> string list -> + Coqargs.coq_cmdopts * string list |