From 85e5450775fd8cfaefa8962c9907941aa8154274 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 26 Dec 2013 11:23:31 +0100
Subject: 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.
---
 tools/coqc.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'tools')

diff --git a/tools/coqc.ml b/tools/coqc.ml
index 3b01f90c45..378f493adf 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -126,7 +126,8 @@ let parse_args () =
     | ("-outputstate"|"-inputstate"|"-is"|"-exclude-dir"
       |"-load-vernac-source"|"-l"|"-load-vernac-object"
       |"-load-ml-source"|"-require"|"-load-ml-object"
-      |"-init-file"|"-dump-glob"|"-compat"|"-coqlib" as o) :: rem ->
+      |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"
+      |"-check-vi-tasks" as o) :: rem ->
 	begin
 	  match rem with
 	    | s :: rem' -> parse (cfiles,s::o::args) rem'
-- 
cgit v1.2.3