diff options
| author | Enrico Tassi | 2013-12-26 11:23:31 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-01-05 16:55:36 +0100 |
| commit | 85e5450775fd8cfaefa8962c9907941aa8154274 (patch) | |
| tree | c3c15beff14b6e25227e480ddbd4d26cfe88a23d /toplevel/stm.mli | |
| parent | 3accba9b8569f4ff1752802a792a8157f97e8533 (diff) | |
coqtop: -check-vi-tasks and -schedule-vi-checking
The command `coqtop -check-vi-tasks 1,4,2 a` checks tasks 1 4 2,
in this precise order, stored in a.vi.
The command `coqtop -schedule-vi-checking 4 a b c` reads {a,b,c}.vi
and .{a,b,c}.aux and spits 4 command lines to check all the tasks in
{a,b,c}.vi trying to equally partition the job between the 4 workers,
that can indeed be run in parallel.
The aux file contains the time that it took to check the proofs stored
in the .vi files last time the file was fully checked.
This user interface is still very rough, it should probably run the
workers instead of just printing their command line.
Diffstat (limited to 'toplevel/stm.mli')
| -rw-r--r-- | toplevel/stm.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/toplevel/stm.mli b/toplevel/stm.mli index 4949845b58..89efdc718f 100644 --- a/toplevel/stm.mli +++ b/toplevel/stm.mli @@ -44,6 +44,9 @@ val join : unit -> unit type tasks val dump : unit -> tasks +val check_task : tasks -> int -> unit +val info_tasks : tasks -> (string * float * int) list + (* Id of the tip of the current branch *) val get_current_state : unit -> Stateid.t |