diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/coqworkmgrApi.ml | 4 | ||||
| -rw-r--r-- | stm/dag.mli | 6 | ||||
| -rw-r--r-- | stm/proofBlockDelimiter.ml | 30 | ||||
| -rw-r--r-- | stm/stm.ml | 120 | ||||
| -rw-r--r-- | stm/stm.mli | 6 | ||||
| -rw-r--r-- | stm/vcs.ml | 14 | ||||
| -rw-r--r-- | stm/vcs.mli | 18 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 45 | ||||
| -rw-r--r-- | stm/vio_checking.ml | 9 | ||||
| -rw-r--r-- | stm/workerPool.ml | 2 | ||||
| -rw-r--r-- | stm/workerPool.mli | 2 |
11 files changed, 132 insertions, 124 deletions
diff --git a/stm/coqworkmgrApi.ml b/stm/coqworkmgrApi.ml index 92dc77172f..2b39a7a2aa 100644 --- a/stm/coqworkmgrApi.ml +++ b/stm/coqworkmgrApi.ml @@ -69,7 +69,7 @@ let parse_response s = let p = try int_of_string p with _ -> raise ParseError in Pong (n,m,p) | _ -> raise ParseError - + let print_request = function | Hello Low -> "HELLO LOW\n" | Hello High -> "HELLO HIGH\n" @@ -101,7 +101,7 @@ let option_map f = function None -> None | Some x -> Some (f x) let init p = try let sock = Sys.getenv "COQWORKMGR_SOCK" in - manager := option_map (fun s -> + manager := option_map (fun s -> let cout = Unix.out_channel_of_descr s in set_binary_mode_out cout true; let cin = Unix.in_channel_of_descr s in diff --git a/stm/dag.mli b/stm/dag.mli index 3a291c8d52..1cd593fdad 100644 --- a/stm/dag.mli +++ b/stm/dag.mli @@ -9,12 +9,12 @@ (************************************************************************) module type S = sig - + type node module NodeSet : Set.S with type elt = node type ('edge,'info,'cdata) t - + val empty : ('e,'i,'d) t val add_edge : ('e,'i,'d) t -> node -> 'e -> node -> ('e,'i,'d) t @@ -45,7 +45,7 @@ module type S = sig val property_of : ('e,'i,'d) t -> node -> 'd Property.t list val del_property : ('e,'i,'d) t -> 'd Property.t -> ('e,'i,'d) t - val iter : ('e,'i,'d) t -> + val iter : ('e,'i,'d) t -> (node -> 'd Property.t list -> 'i option -> (node * 'e) list -> unit) -> unit diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index 129444c3b3..0e8c463b19 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -77,17 +77,18 @@ include Util (* ****************** - foo - bar - baz *********************************** *) let static_bullet ({ entry_point; prev_node } as view) = + let open Vernacexpr in assert (not (Vernacprop.has_Fail entry_point.ast)); - match Vernacprop.under_control entry_point.ast with - | Vernacexpr.VernacBullet b -> + match entry_point.ast.CAst.v.expr with + | VernacBullet b -> let base = entry_point.indentation in let last_tac = prev_node entry_point in crawl view ~init:last_tac (fun prev node -> if node.indentation < base then `Stop else if node.indentation > base then `Cont node else if Vernacprop.has_Fail node.ast then `Stop - else match Vernacprop.under_control node.ast with - | Vernacexpr.VernacBullet b' when b = b' -> + else match node.ast.CAst.v.expr with + | VernacBullet b' when b = b' -> `Found { block_stop = entry_point.id; block_start = prev.id; dynamic_switch = node.id; carry_on_data = of_bullet_val b } | _ -> `Stop) entry_point @@ -99,7 +100,7 @@ let dynamic_bullet doc { dynamic_switch = id; carry_on_data = b } = `ValidBlock { base_state = id; goals_to_admit = focused; - recovery_command = Some (CAst.make @@ Vernacexpr.VernacExpr([], Vernacexpr.VernacBullet (to_bullet_val b))) + recovery_command = Some (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacBullet (to_bullet_val b)}) } | `Not -> `Leaks @@ -107,18 +108,19 @@ let () = register_proof_block_delimiter "bullet" static_bullet dynamic_bullet (* ******************** { block } ***************************************** *) - + let static_curly_brace ({ entry_point; prev_node } as view) = - assert(Vernacprop.under_control entry_point.ast = Vernacexpr.VernacEndSubproof); + let open Vernacexpr in + assert(entry_point.ast.CAst.v.expr = VernacEndSubproof); crawl view (fun (nesting,prev) node -> if Vernacprop.has_Fail node.ast then `Cont (nesting,node) - else match Vernacprop.under_control node.ast with - | Vernacexpr.VernacSubproof _ when nesting = 0 -> + else match node.ast.CAst.v.expr with + | VernacSubproof _ when nesting = 0 -> `Found { block_stop = entry_point.id; block_start = prev.id; dynamic_switch = node.id; carry_on_data = unit_val } - | Vernacexpr.VernacSubproof _ -> + | VernacSubproof _ -> `Cont (nesting - 1,node) - | Vernacexpr.VernacEndSubproof -> + | VernacEndSubproof -> `Cont (nesting + 1,node) | _ -> `Cont (nesting,node)) (-1, entry_point) @@ -128,7 +130,7 @@ let dynamic_curly_brace doc { dynamic_switch = id } = `ValidBlock { base_state = id; goals_to_admit = focused; - recovery_command = Some (CAst.make @@ Vernacexpr.VernacExpr ([], Vernacexpr.VernacEndSubproof)) + recovery_command = Some (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacEndSubproof }) } | `Not -> `Leaks @@ -167,7 +169,7 @@ let static_indent ({ entry_point; prev_node } as view) = else crawl view ~init:(Some last_tac) (fun prev node -> if node.indentation >= last_tac.indentation then `Cont node - else + else `Found { block_stop = entry_point.id; block_start = node.id; dynamic_switch = node.id; carry_on_data = of_vernac_control_val entry_point.ast } @@ -178,7 +180,7 @@ let dynamic_indent doc { dynamic_switch = id; carry_on_data = e } = match is_focused_goal_simple ~doc id with | `Simple [] -> `Leaks | `Simple focused -> - let but_last = List.tl (List.rev focused) in + let but_last = List.tl (List.rev focused) in `ValidBlock { base_state = id; goals_to_admit = but_last; diff --git a/stm/stm.ml b/stm/stm.ml index d5e6e6fd8b..eff2403eca 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -170,7 +170,7 @@ type fork_t = aast * Vcs_.Branch.t * opacity_guarantee * Names.Id.t list type qed_t = { qast : aast; keep : vernac_qed_type; - mutable fproof : (future_proof * AsyncTaskQueue.cancel_switch) option; + mutable fproof : (future_proof option * AsyncTaskQueue.cancel_switch) option; brname : Vcs_.Branch.t; brinfo : branch_type Vcs_.branch_info } @@ -571,7 +571,7 @@ end = struct (* {{{ *) vcs := rewrite_merge !vcs id ~ours ~theirs:Noop ~at branch let reachable id = reachable !vcs id let mk_branch_name { expr = x } = Branch.make - (match Vernacprop.under_control x with + (match x.CAst.v.Vernacexpr.expr with | VernacDefinition (_,({CAst.v=Name i},_),_) -> Id.to_string i | VernacStartTheoremProof (_,[({CAst.v=i},_),_]) -> Id.to_string i | VernacInstance (({CAst.v=Name i},_),_,_,_,_) -> Id.to_string i @@ -1054,9 +1054,9 @@ end = struct (* {{{ *) end (* }}} *) (* Wrapper for the proof-closing special path for Qed *) -let stm_qed_delay_proof ?route ~proof ~info ~id ~st ~loc pending : Vernacstate.t = +let stm_qed_delay_proof ?route ~proof ~info ~id ~st ~loc ~control pending : Vernacstate.t = set_id_for_feedback ?route dummy_doc id; - Vernacentries.interp_qed_delayed_proof ~proof ~info ~st ?loc:loc pending + Vernacinterp.interp_qed_delayed_proof ~proof ~info ~st ~control (CAst.make ?loc pending) (* Wrapper for Vernacentries.interp to set the feedback id *) (* It is currently called 19 times, this number should be certainly @@ -1073,17 +1073,17 @@ let stm_vernac_interp ?route id st { verbose; expr } : Vernacstate.t = *) let is_filtered_command = function | VernacResetName _ | VernacResetInitial | VernacBack _ - | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _ + | VernacRestart | VernacUndo _ | VernacUndoTo _ | VernacAbortAll | VernacAbort _ -> true | _ -> false in (* XXX unsupported attributes *) - let cmd = Vernacprop.under_control expr in + let cmd = expr.CAst.v.expr in if is_filtered_command cmd then (stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr); st) else begin stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr); - Vernacentries.interp ?verbosely:(Some verbose) ~st expr + Vernacinterp.interp ?verbosely:(Some verbose) ~st expr end (****************************** CRUFT *****************************************) @@ -1141,7 +1141,7 @@ end = struct (* {{{ *) | { step = `Fork ((_,_,_,l),_) } -> l, false,0 | { step = `Cmd { cids = l; ctac } } -> l, ctac,0 | { step = `Alias (_,{ expr }) } when not (Vernacprop.has_Fail expr) -> - begin match Vernacprop.under_control expr with + begin match expr.CAst.v.expr with | VernacUndo n -> [], false, n | _ -> [],false,0 end @@ -1171,7 +1171,7 @@ end = struct (* {{{ *) if not (VCS.is_interactive ()) && !cur_opt.async_proofs_cache <> Some Force then undo_costly_in_batch_mode v; try - match Vernacprop.under_control v with + match v.CAst.v.expr with | VernacResetInitial -> Stateid.initial | VernacResetName {CAst.v=name} -> @@ -1216,8 +1216,6 @@ end = struct (* {{{ *) match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ()) () id in oid - | VernacBackTo id -> - Stateid.of_int id | _ -> anomaly Pp.(str "incorrect VtMeta classification") with | Not_found -> @@ -1534,7 +1532,7 @@ end = struct (* {{{ *) let st = Vernacstate.freeze_interp_state ~marshallable:false in stm_qed_delay_proof ~st ~id:stop - ~proof:pobject ~info:(Lemmas.Info.make ()) ~loc (Proved (opaque,None))) in + ~proof:pobject ~info:(Lemmas.Info.make ()) ~loc ~control:[] (Proved (opaque,None))) in ignore(Future.join checked_proof); end; (* STATE: Restore the state XXX: handle exn *) @@ -1685,7 +1683,7 @@ end = struct (* {{{ *) *) (* STATE We use the state resulting from reaching start. *) let st = Vernacstate.freeze_interp_state ~marshallable:false in - ignore(stm_qed_delay_proof ~id:stop ~st ~proof ~info ~loc (Proved (opaque,None))); + ignore(stm_qed_delay_proof ~id:stop ~st ~proof ~info ~loc ~control:[] (Proved (opaque,None))); `OK proof end with e -> @@ -1745,9 +1743,9 @@ end = struct (* {{{ *) assert (Univ.ContextSet.is_empty uctx) in let pr = Constr.hcons pr in - let (ci, dummy) = p.(bucket) in + let dummy = p.(bucket) in let () = assert (Option.is_empty dummy) in - p.(bucket) <- ci, Some (pr, priv); + p.(bucket) <- Some (pr, priv); Univ.ContextSet.union cst uc, false let check_task name l i = @@ -1972,20 +1970,21 @@ end = struct (* {{{ *) let stm_fail ~st fail f = if fail then - Vernacentries.with_fail ~st f + Vernacinterp.with_fail ~st f else f () let vernac_interp ~solve ~abstract ~cancel_switch nworkers priority safe_id id { indentation; verbose; expr = e; strlen } : unit = - let e, time, batch, fail = - let rec find ~time ~batch ~fail v = CAst.with_loc_val (fun ?loc -> function - | VernacTime (batch,e) -> find ~time:true ~batch ~fail e - | VernacRedirect (_,e) -> find ~time ~batch ~fail e - | VernacFail e -> find ~time ~batch ~fail:true e - | e -> CAst.make ?loc e, time, batch, fail) v in - find ~time:false ~batch:false ~fail:false e in + let cl, time, batch, fail = + let rec find ~time ~batch ~fail cl = match cl with + | ControlTime batch :: cl -> find ~time:true ~batch ~fail cl + | ControlRedirect _ :: cl -> find ~time ~batch ~fail cl + | ControlFail :: cl -> find ~time ~batch ~fail:true cl + | cl -> cl, time, batch, fail in + find ~time:false ~batch:false ~fail:false e.CAst.v.control in + let e = CAst.map (fun cmd -> { cmd with control = cl }) e in let st = Vernacstate.freeze_interp_state ~marshallable:false in stm_fail ~st fail (fun () -> (if time then System.with_time ~batch ~header:(Pp.mt ()) else (fun x -> x)) (fun () -> @@ -2153,14 +2152,14 @@ let collect_proof keep cur hd brkind id = | VernacEndProof (Proved (Proof_global.Transparent,_)) -> true | _ -> false in let is_defined = function - | _, { expr = e } -> is_defined_expr (Vernacprop.under_control e) + | _, { expr = e } -> is_defined_expr e.CAst.v.expr && (not (Vernacprop.has_Fail e)) in let proof_using_ast = function | VernacProof(_,Some _) -> true | _ -> false in let proof_using_ast = function - | Some (_, v) when proof_using_ast (Vernacprop.under_control v.expr) + | Some (_, v) when proof_using_ast v.expr.CAst.v.expr && (not (Vernacprop.has_Fail v.expr)) -> Some v | _ -> None in let has_proof_using x = proof_using_ast x <> None in @@ -2169,14 +2168,14 @@ let collect_proof keep cur hd brkind id = | _ -> assert false in let proof_no_using = function - | Some (_, v) -> proof_no_using (Vernacprop.under_control v.expr), v + | Some (_, v) -> proof_no_using v.expr.CAst.v.expr, v | _ -> assert false in let has_proof_no_using = function | VernacProof(_,None) -> true | _ -> false in let has_proof_no_using = function - | Some (_, v) -> has_proof_no_using (Vernacprop.under_control v.expr) + | Some (_, v) -> has_proof_no_using v.expr.CAst.v.expr && (not (Vernacprop.has_Fail v.expr)) | _ -> false in let too_complex_to_delegate = function @@ -2193,7 +2192,7 @@ let collect_proof keep cur hd brkind id = let view = VCS.visit id in match view.step with | (`Sideff (ReplayCommand x,_) | `Cmd { cast = x }) - when too_complex_to_delegate (Vernacprop.under_control x.expr) -> + when too_complex_to_delegate x.expr.CAst.v.expr -> `Sync(no_name,`Print) | `Cmd { cast = x } -> collect (Some (id,x)) (id::accn) view.next | `Sideff (ReplayCommand x,_) -> collect (Some (id,x)) (id::accn) view.next @@ -2214,7 +2213,7 @@ let collect_proof keep cur hd brkind id = (try let name, hint = name ids, get_hint_ctx loc in let t, v = proof_no_using last in - v.expr <- CAst.map (fun _ -> VernacExpr([], VernacProof(t, Some hint))) v.expr; + v.expr <- CAst.map (fun _ -> { control = []; attrs = []; expr = VernacProof(t, Some hint)}) v.expr; `ASync (parent last,accn,name,delegate name) with Not_found -> let name = name ids in @@ -2237,7 +2236,7 @@ let collect_proof keep cur hd brkind id = | _ -> false in match cur, (VCS.visit id).step, brkind with - | (parent, x), `Fork _, _ when is_vernac_exact (Vernacprop.under_control x.expr) + | (parent, x), `Fork _, _ when is_vernac_exact x.expr.CAst.v.expr && (not (Vernacprop.has_Fail x.expr)) -> `Sync (no_name,`Immediate) | _, _, { VCS.kind = `Edit _ } -> check_policy (collect (Some cur) [] id) @@ -2352,8 +2351,8 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = term.` could also fail in this case, however that'd be a bug I do believe as proof injection shouldn't happen here. *) let extract_pe (x : aast) = - match Vernacprop.under_control x.expr with - | VernacEndProof pe -> pe + match x.expr.CAst.v.expr with + | VernacEndProof pe -> x.expr.CAst.v.control, pe | _ -> CErrors.anomaly Pp.(str "Non-qed command classified incorrectly") in (* ugly functions to process nested lemmas, i.e. hard to reproduce @@ -2461,8 +2460,8 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = let fp, cancel = Slaves.build_proof ~doc ?loc ~drop_pt ~exn_info ~block_start ~block_stop ~name in - Future.replace ofp fp; - qed.fproof <- Some (fp, cancel); + Future.replace (Option.get ofp) fp; + qed.fproof <- Some (Some fp, cancel); (* We don't generate a new state, but we still need * to install the right one *) State.install_cached id @@ -2477,7 +2476,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = ProofTask.build_proof_here ~doc ?loc ~drop_pt exn_info block_stop, ref false in - qed.fproof <- Some (fp, cancel); + qed.fproof <- Some (Some fp, cancel); let opaque = match keep' with | VtKeepAxiom | VtKeepOpaque -> Proof_global.Opaque (* Admitted -> Opaque should be OK. *) @@ -2488,7 +2487,8 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = if not delegate then ignore(Future.compute fp); reach view.next; let st = Vernacstate.freeze_interp_state ~marshallable:false in - ignore(stm_qed_delay_proof ~id ~st ~proof ~info ~loc (extract_pe x)); + let control, pe = extract_pe x in + ignore(stm_qed_delay_proof ~id ~st ~proof ~info ~loc ~control pe); feedback ~id:id Incomplete | { VCS.kind = `Master }, _ -> assert false end; @@ -2510,9 +2510,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = match keep with | VtDrop -> None | VtKeep VtKeepAxiom -> - let ctx = UState.empty in - let fp = Future.from_val ([],ctx) in - qed.fproof <- Some (fp, ref false); None + qed.fproof <- Some (None, ref false); None | VtKeep opaque -> let opaque = let open Proof_global in match opaque with | VtKeepOpaque -> Opaque | VtKeepDefined -> Transparent @@ -2528,7 +2526,8 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = let _st = match proof with | None -> stm_vernac_interp id st x | Some (proof, info) -> - stm_qed_delay_proof ~id ~st ~proof ~info ~loc (extract_pe x) + let control, pe = extract_pe x in + stm_qed_delay_proof ~id ~st ~proof ~info ~loc ~control pe in let wall_clock3 = Unix.gettimeofday () in Aux_file.record_in_aux_at ?loc:x.expr.CAst.loc "proof_check_time" @@ -2616,13 +2615,10 @@ let dirpath_of_file f = let new_doc { doc_type ; iload_path; require_libs; stm_options } = - let load_objs libs = - let rq_file (dir, from, exp) = - let mp = Libnames.qualid_of_string dir in - let mfrom = Option.map Libnames.qualid_of_string from in - Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] in - List.(iter rq_file (rev libs)) - in + let require_file (dir, from, exp) = + let mp = Libnames.qualid_of_string dir in + let mfrom = Option.map Libnames.qualid_of_string from in + Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] in (* Set the options from the new documents *) AsyncOpts.cur_opt := stm_options; @@ -2661,7 +2657,7 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = end; (* Import initial libraries. *) - load_objs require_libs; + List.iter require_file require_libs; (* We record the state at this point! *) State.define ~doc ~cache:true ~redefine:true (fun () -> ()) Stateid.initial; @@ -2711,7 +2707,7 @@ let rec join_admitted_proofs id = let view = VCS.visit id in match view.step with | `Qed ({ keep = VtKeep VtKeepAxiom; fproof = Some (fp,_) },_) -> - ignore(Future.force fp); + Option.iter (fun fp -> ignore(Future.force fp)) fp; join_admitted_proofs view.next | _ -> join_admitted_proofs view.next @@ -2803,13 +2799,21 @@ let handle_failure (e, info) vcs = VCS.print (); Exninfo.iraise (e, info) -let snapshot_vio ~doc ~output_native_objects ldir long_f_dot_vo = +let snapshot_vio ~create_vos ~doc ~output_native_objects ldir long_f_dot_vo = let doc = finish ~doc in if List.length (VCS.branches ()) > 1 then CErrors.user_err ~hdr:"stm" (str"Cannot dump a vio with open proofs"); - Library.save_library_to ~todo:(dump_snapshot ()) ~output_native_objects - ldir long_f_dot_vo - (Global.opaque_tables ()); + (* LATER: when create_vos is true, it could be more efficient to not allocate the futures; but for now it seems useful for synchronization of the workers, + below, [snapshot] gets computed even if [create_vos] is true. *) + let (tasks,counters) = dump_snapshot() in + let except = List.fold_left (fun e (r,_) -> + Future.UUIDSet.add r.Stateid.uuid e) Future.UUIDSet.empty tasks in + let todo_proofs = + if create_vos + then Library.ProofsTodoSomeEmpty except + else Library.ProofsTodoSome (except,tasks,counters) + in + Library.save_library_to todo_proofs ~output_native_objects ldir long_f_dot_vo (Global.opaque_tables ()); doc let reset_task_queue = Slaves.reset_task_queue @@ -2875,7 +2879,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) let queue = if VCS.is_vio_doc () && VCS.((get_branch head).kind = `Master) && - may_pierce_opaque (Vernacprop.under_control x.expr) + may_pierce_opaque x.expr.CAst.v.expr then `SkipQueue else `MainQueue in VCS.commit id (mkTransCmd x [] false queue); @@ -2886,14 +2890,14 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) | VtStartProof (guarantee, names) -> if not (get_allow_nested_proofs ()) && VCS.proof_nesting () > 0 then - "Nested proofs are not allowed unless you turn option Nested Proofs Allowed on." + "Nested proofs are not allowed unless you turn the Nested Proofs Allowed flag on." |> Pp.str |> (fun s -> (UserError (None, s), Exninfo.null)) |> State.exn_on ~valid:Stateid.dummy newtip |> Exninfo.iraise else - let proof_mode = Some (Vernacentries.get_default_proof_mode ()) in + let proof_mode = Some (Vernacinterp.get_default_proof_mode ()) in let id = VCS.new_node ~id:newtip proof_mode () in let bname = VCS.mk_branch_name x in VCS.checkout VCS.Branch.master; @@ -2941,7 +2945,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) VCS.commit id (mkTransCmd x l true `MainQueue); (* We can't replay a Definition since universes may be differently * inferred. This holds in Coq >= 8.5 *) - let action = match Vernacprop.under_control x.expr with + let action = match x.expr.CAst.v.expr with | VernacDefinition(_, _, DefineBody _) -> CherryPickEnv | _ -> ReplayCommand x in VCS.propagate_sideff ~action @@ -3108,7 +3112,7 @@ let edit_at ~doc id = (VCS.reachable (VCS.get_branch_pos (VCS.current_branch ()))) in let has_failed qed_id = match VCS.visit qed_id with - | { step = `Qed ({ fproof = Some (fp,_) }, _) } -> Future.is_exn fp + | { step = `Qed ({ fproof = Some (Some fp,_) }, _) } -> Future.is_exn fp | _ -> false in let rec master_for_br root tip = if Stateid.equal tip Stateid.initial then tip else diff --git a/stm/stm.mli b/stm/stm.mli index 29e4b02e3f..841adcf05b 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -159,8 +159,10 @@ val join : doc:doc -> doc - if the worker pool is empty, all tasks are saved - if the worker proof is not empty, then it waits until all workers are done with their current jobs and then dumps (or fails if one - of the completed tasks is a failure) *) -val snapshot_vio : doc:doc -> output_native_objects:bool -> DirPath.t -> string -> doc + of the completed tasks is a failure). + Note: the create_vos argument is used in the "-vos" mode, where the + proof tasks are not dumped into the output file. *) +val snapshot_vio : create_vos:bool -> doc:doc -> output_native_objects:bool -> DirPath.t -> string -> doc (* Empties the task queue, can be used only if the worker pool is empty (E.g. * after having built a .vio in batch mode *) diff --git a/stm/vcs.ml b/stm/vcs.ml index 78edeb53d3..26be9ae76f 100644 --- a/stm/vcs.ml +++ b/stm/vcs.ml @@ -24,20 +24,20 @@ module type S = sig end type id - + type ('kind) branch_info = { kind : [> `Master] as 'kind; root : id; pos : id; } - + type ('kind,'diff,'info,'property_data) t constraint 'kind = [> `Master ] - + val empty : id -> ('kind,'diff,'info,'property_data) t - + val current_branch : ('k,'e,'i,'c) t -> Branch.t val branches : ('k,'e,'i,'c) t -> Branch.t list - + val get_branch : ('k,'e,'i,'c) t -> Branch.t -> 'k branch_info val reset_branch : ('k,'e,'i,'c) t -> Branch.t -> id -> ('k,'e,'i,'c) t val branch : @@ -52,7 +52,7 @@ module type S = sig ('k,'diff,'i,'c) t -> id -> ours:'diff -> theirs:'diff -> at:id -> Branch.t -> ('k,'diff,'i,'c) t val checkout : ('k,'e,'i,'c) t -> Branch.t -> ('k,'e,'i,'c) t - + val set_info : ('k,'e,'info,'c) t -> id -> 'info -> ('k,'e,'info,'c) t val get_info : ('k,'e,'info,'c) t -> id -> 'info option @@ -62,7 +62,7 @@ module type S = sig val create_property : ('k,'e,'i,'c) t -> id list -> 'c -> ('k,'e,'i,'c) t val property_of : ('k,'e,'i,'c) t -> id -> 'c Dag.Property.t list - val delete_property : ('k,'e,'i,'c) t -> 'c Dag.Property.t -> ('k,'e,'i,'c) t + val delete_property : ('k,'e,'i,'c) t -> 'c Dag.Property.t -> ('k,'e,'i,'c) t (* Removes all unreachable nodes and returns them *) val gc : ('k,'e,'info,'c) t -> ('k,'e,'info,'c) t * Dag.NodeSet.t diff --git a/stm/vcs.mli b/stm/vcs.mli index f6ca81257b..584560f833 100644 --- a/stm/vcs.mli +++ b/stm/vcs.mli @@ -41,20 +41,20 @@ module type S = sig end type id - + type ('kind) branch_info = { kind : [> `Master] as 'kind; root : id; pos : id; } - + type ('kind,'diff,'info,'property_data) t constraint 'kind = [> `Master ] - + val empty : id -> ('kind,'diff,'info,'property_data) t - + val current_branch : ('k,'e,'i,'c) t -> Branch.t val branches : ('k,'e,'i,'c) t -> Branch.t list - + val get_branch : ('k,'e,'i,'c) t -> Branch.t -> 'k branch_info val reset_branch : ('k,'e,'i,'c) t -> Branch.t -> id -> ('k,'e,'i,'c) t val branch : @@ -69,25 +69,25 @@ module type S = sig ('k,'diff,'i,'c) t -> id -> ours:'diff -> theirs:'diff -> at:id -> Branch.t -> ('k,'diff,'i,'c) t val checkout : ('k,'e,'i,'c) t -> Branch.t -> ('k,'e,'i,'c) t - + val set_info : ('k,'e,'info,'c) t -> id -> 'info -> ('k,'e,'info,'c) t val get_info : ('k,'e,'info,'c) t -> id -> 'info option (* Read only dag *) module Dag : Dag.S with type node = id val dag : ('kind,'diff,'info,'cdata) t -> ('diff,'info,'cdata) Dag.t - + (* Properties are not a concept typical of a VCS, but a useful metadata * of a DAG (or graph). *) val create_property : ('k,'e,'i,'c) t -> id list -> 'c -> ('k,'e,'i,'c) t val property_of : ('k,'e,'i,'c) t -> id -> 'c Dag.Property.t list - val delete_property : ('k,'e,'i,'c) t -> 'c Dag.Property.t -> ('k,'e,'i,'c) t + val delete_property : ('k,'e,'i,'c) t -> 'c Dag.Property.t -> ('k,'e,'i,'c) t (* Removes all unreachable nodes and returns them *) val gc : ('k,'e,'info,'c) t -> ('k,'e,'info,'c) t * Dag.NodeSet.t val reachable : ('k,'e,'info,'c) t -> id -> Dag.NodeSet.t - + end module Make(OT : Map.OrderedType) : S diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 8750a64ccc..c5b3e0931b 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -51,7 +51,7 @@ let stm_allow_nested_proofs_option_name = ["Nested";"Proofs";"Allowed"] let options_affecting_stm_scheduling = [ Attributes.universe_polymorphism_option_name; stm_allow_nested_proofs_option_name; - Vernacentries.proof_mode_opt_name; + Vernacinterp.proof_mode_opt_name; Attributes.program_mode_option_name; Proof_using.proof_using_opt_name; ] @@ -74,7 +74,7 @@ let classify_vernac e = | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _ | VernacCheckMayEval _ -> VtQuery (* ProofStep *) - | VernacProof _ + | VernacProof _ | VernacFocus _ | VernacUnfocus | VernacSubproof _ | VernacCheckGuard @@ -83,7 +83,7 @@ let classify_vernac e = VtProofStep { parallel = `No; proof_block_detection = None } | VernacBullet _ -> VtProofStep { parallel = `No; proof_block_detection = Some "bullet" } - | VernacEndSubproof -> + | VernacEndSubproof -> VtProofStep { parallel = `No; proof_block_detection = Some "curly" } (* StartProof *) @@ -146,7 +146,7 @@ let classify_vernac e = | VernacUniverse _ | VernacConstraint _ | VernacCanonical _ | VernacCoercion _ | VernacIdentityCoercion _ | VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _ - | VernacChdir _ + | VernacChdir _ | VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _ | VernacArguments _ | VernacReserve _ @@ -183,17 +183,21 @@ let classify_vernac e = | VernacDeclareMLModule _ | VernacContext _ (* TASSI: unsure *) -> VtSideff ([], VtNow) | VernacProofMode pm -> VtProofMode pm - | VernacInstance ((name,_),_,_,None,_) when not (Attributes.parse_drop_extra Attributes.program atts) -> - let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in - let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in - VtStartProof (guarantee, idents_of_name name.CAst.v) - | VernacInstance ((name,_),_,_,_,_) -> - VtSideff (idents_of_name name.CAst.v, VtLater) + | VernacInstance ((name,_),_,_,props,_) -> + let program, refine = + Attributes.(parse_drop_extra Notations.(program ++ Classes.refine_att) atts) + in + if program || (props <> None && not refine) then + VtSideff (idents_of_name name.CAst.v, VtLater) + else + let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in + let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in + VtStartProof (guarantee, idents_of_name name.CAst.v) (* Stm will install a new classifier to handle these *) | VernacBack _ | VernacAbortAll | VernacUndoTo _ | VernacUndo _ | VernacResetName _ | VernacResetInitial - | VernacBackTo _ | VernacRestart -> VtMeta + | VernacRestart -> VtMeta (* What are these? *) | VernacRestoreState _ | VernacWriteState _ -> VtSideff ([], VtNow) @@ -202,18 +206,17 @@ let classify_vernac e = try Vernacextend.get_vernac_classifier s l with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".") in - let rec static_control_classifier v = v |> CAst.with_val (function - | VernacExpr (atts, e) -> - static_classifier ~atts e - | VernacTimeout (_,e) -> static_control_classifier e - | VernacTime (_,e) | VernacRedirect (_, e) -> - static_control_classifier e - | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) - (* XXX why is Fail not always Query? *) - (match static_control_classifier e with + let static_control_classifier ({ CAst.v ; _ } as cmd) = + (* Fail Qed or Fail Lemma must not join/fork the DAG *) + (* XXX why is Fail not always Query? *) + if Vernacprop.has_Fail cmd then + (match static_classifier ~atts:v.attrs v.expr with | VtQuery | VtProofStep _ | VtSideff _ | VtMeta as x -> x | VtQed _ -> VtProofStep { parallel = `No; proof_block_detection = None } - | VtStartProof _ | VtProofMode _ -> VtQuery)) + | VtStartProof _ | VtProofMode _ -> VtQuery) + else + static_classifier ~atts:v.attrs v.expr + in static_control_classifier e diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml index fab6767beb..837ba3d880 100644 --- a/stm/vio_checking.ml +++ b/stm/vio_checking.ml @@ -11,7 +11,6 @@ open Util let check_vio (ts,f_in) = - Dumpglob.noglob (); let _, _, _, tasks, _ = Library.load_library_todo f_in in Stm.set_compilation_hints f_in; List.fold_left (fun acc ids -> Stm.check_task f_in tasks ids && acc) true ts @@ -53,7 +52,7 @@ let schedule_vio_checking j fs = | ((f',id),_,_) :: tl when last = f' -> aux last (id::acc) tl | ((f',id),_,_) :: _ as l -> (last,acc) :: aux f' [] l in aux f [] l in - let prog = Sys.argv.(0) in + let prog = Sys.argv.(0) in let stdargs = filter_argv false (List.tl (Array.to_list Sys.argv)) in let make_job () = let cur = ref 0.0 in @@ -80,7 +79,7 @@ let schedule_vio_checking j fs = let cmp_job (f1,_,_) (f2,_,_) = compare f1 f2 in List.flatten (List.map (fun (f, tl) -> - "-check-vio-tasks" :: + "-check-vio-tasks" :: String.concat "," (List.map string_of_int tl) :: [f]) (pack (List.sort cmp_job !what))) in let rc = ref 0 in @@ -116,7 +115,7 @@ let schedule_vio_compilation j fs = | s :: rest when String.length s > 0 && s.[0] = '-' && b -> filter_argv false (s :: rest) | _ :: rest when b -> filter_argv b rest | s :: rest -> s :: filter_argv b rest in - let prog = Sys.argv.(0) in + let prog = Sys.argv.(0) in let stdargs = filter_argv false (List.tl (Array.to_list Sys.argv)) in let all_jobs = !jobs in let make_job () = @@ -142,5 +141,3 @@ let schedule_vio_compilation j fs = List.iter (fun (f,_) -> Unix.utimes (Filename.chop_extension f^".vo") t t) all_jobs; end; exit !rc - - diff --git a/stm/workerPool.ml b/stm/workerPool.ml index f77ced2f3a..d82741576e 100644 --- a/stm/workerPool.ml +++ b/stm/workerPool.ml @@ -88,7 +88,7 @@ let rec create_worker extra pool priority id = let cpanel = { exit; cancelled; extra } in let manager = CThread.create (Model.manager cpanel) worker in { name; cancel; manager; process } - + and cleanup x priority = locking x begin fun { workers; count; extra_arg } -> workers := List.map (function | { cancel } as w when !cancel = false -> w diff --git a/stm/workerPool.mli b/stm/workerPool.mli index 5468a24959..88175a788c 100644 --- a/stm/workerPool.mli +++ b/stm/workerPool.mli @@ -31,7 +31,7 @@ end module Make(Model : PoolModel) : sig type pool - + val create : Model.extra -> size:int -> CoqworkmgrApi.priority -> pool val is_empty : pool -> bool |