-schedule-vi-checking ported to spawn

2 files changed, 9 insertions, 2 deletions

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index eefad34421..ab4a89ffbf 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -616,7 +616,8 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other
     end;
   if !some_vfile then
     begin
-      print "quick:\n\t$(MAKE) all VO=vi\n";
+      print "quick:\n\t$(MAKE) -f $(firstword $(MAKEFILE_LIST)) all VO=vi\n";
+      print "checkproofs:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vi-checking $(J) $(VOFILES:%.vo=%.vi)\n";
       print "gallina: $(GFILES)\n\n";
       print "html: $(GLOBFILES) $(VFILES)\n";
       print "\t- mkdir -p html\n";
diff --git a/tools/coqc.ml b/tools/coqc.ml
index 5e63322c5a..dbfdc40a2e 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -71,6 +71,7 @@ let usage () =
   exit 1
 
 (* parsing of the command line *)
+let extra_arg_needed = ref true
 
 let parse_args () =
   let rec parse (cfiles,args) = function
@@ -150,6 +151,11 @@ let parse_args () =
     | "-R" :: s :: "-as" :: t :: rem ->	parse (cfiles,t::"-as"::s::"-R"::args) rem
     | "-R" :: s :: "-as" :: [] -> usage ()
     | "-R" :: s :: t :: rem -> parse (cfiles,t::s::"-R"::args) rem
+    | ("-schedule-vi-checking" |"-check-vi-tasks" as o) :: s :: rem ->
+        let nodash, rem =
+          CList.split_when (fun x -> String.length x > 1 && x.[0] = '-') rem in
+        extra_arg_needed := false;
+        parse (cfiles, List.rev nodash @ s :: o :: args) rem
 
 (* Anything else is interpreted as a file *)
 
@@ -172,7 +178,7 @@ let parse_args () =
 
 let main () =
   let cfiles, args = parse_args () in
-    if cfiles = [] then begin
+    if cfiles = [] && !extra_arg_needed then begin
       prerr_endline "coqc: too few arguments" ;
       usage ()
     end;