From 8c0f9b63cb923a6cb6682124cd48db5da391075c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 24 Jan 2014 14:37:45 +0100 Subject: -schedule-vi-checking ported to spawn --- doc/refman/AsyncProofs.tex | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'doc/refman/AsyncProofs.tex') diff --git a/doc/refman/AsyncProofs.tex b/doc/refman/AsyncProofs.tex index 86bec7c21..3dcd762aa 100644 --- a/doc/refman/AsyncProofs.tex +++ b/doc/refman/AsyncProofs.tex @@ -124,8 +124,9 @@ The $coqtop -schedule-vi-checking 3 a b c$ command can be used to obtain a good scheduling for 3 workers to check all proof tasks of $a.vi$, $b.vi$ and $c.vi$. Auxiliary files are used to predict how long a proof task will take, assuming it will take the same amount of time it took last time. -The output of $coqtop -schedule-vi-checking$ is a list of commands one has -to execute in order to check all proof tasks. +If the $Makefile$ one uses was produced by $coq\_makefile$ the $checkproofs$ +target can be used to check all $.vi$ files. The variable $J$ should be +set to the number of workers, like in $make checkproofs J=3$. \subsubsection{Caveats} -- cgit v1.2.3