aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorEnrico Tassi2013-12-26 11:23:31 +0100
committerEnrico Tassi2014-01-05 16:55:36 +0100
commit85e5450775fd8cfaefa8962c9907941aa8154274 (patch)
treec3c15beff14b6e25227e480ddbd4d26cfe88a23d /kernel
parent3accba9b8569f4ff1752802a792a8157f97e8533 (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 'kernel')
0 files changed, 0 insertions, 0 deletions