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.

1 files changed, 12 insertions, 0 deletions

diff --git a/library/library.ml b/library/library.ml
index 8b390832f..1088bcb16 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -394,6 +394,18 @@ let intern_from_file f =
   close_in ch;
   library
 
+let load_library_todo f =
+  let paths = Loadpath.get_paths () in
+  let _, longf =
+    System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in
+  let f = longf^"i" in
+  let ch = System.with_magic_number_check raw_intern_library f in
+  let _ = System.skip_in_segment f ch in
+  let tasks, _, _ = System.marshal_in_segment f ch in
+  match tasks with
+  | Some a -> a, longf
+  | None -> errorlabstrm "load_library_todo" (str"not a .vi file")
+
 let rec intern_library needed (dir, f) =
   (* Look if in the current logical environment *)
   try find_library dir, needed