diff options
| author | charguer | 2018-11-08 16:50:13 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-11-01 12:15:59 +0100 |
| commit | 72dc33fb0f99d403e8693db178a73c1e28096400 (patch) | |
| tree | 51d4f6808e26bfb5bf8d453fec7c7213c69245d2 /stm | |
| parent | e8ac44de70bc98d5393d7be655fd8ddc2eee5310 (diff) | |
Implementing support for vos/vok files.
A .vos file stores the result of compiling statements (defs, lemmas)
but not proofs.
A .vok file is an empty file that denotes successful compilation of
the full contents of a .v file.
Unlike a .vio file, a .vos file does not store suspended proofs,
so it is more lightweight. It cannot be completed into a .vo file.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 16 | ||||
| -rw-r--r-- | stm/stm.mli | 6 |
2 files changed, 16 insertions, 6 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 5c6df26cbb..c399b69a77 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2801,13 +2801,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 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 *) |