diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-01-24 14:37:45 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-01-26 14:20:52 +0100 |
| commit | 8c0f9b63cb923a6cb6682124cd48db5da391075c (patch) | |
| tree | c34f2972e3e336528648e5d0457de68b5e719e29 /toplevel/coqtop.ml | |
| parent | 3afdca3562b9dcadd9b16991bd8716f38a55f2c8 (diff) | |
-schedule-vi-checking ported to spawn
Diffstat (limited to 'toplevel/coqtop.ml')
| -rw-r--r-- | toplevel/coqtop.ml | 17 |
1 files changed, 14 insertions, 3 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 503e33cc5..74a94465e 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -254,7 +254,11 @@ let add_vi_task f = Flags.make_silent true; vi_tasks := f :: !vi_tasks -let check_vi_tasks () = List.iter Vi_checking.check_vi (List.rev !vi_tasks) +let check_vi_tasks () = + let rc = + List.fold_left (fun acc t -> Vi_checking.check_vi t && acc) + true (List.rev !vi_tasks) in + if not rc then exit 1 let vi_files = ref [] let vi_files_j = ref 0 @@ -263,7 +267,14 @@ let add_vi_file f = set_batch_mode (); Flags.make_silent true; vi_files := f :: !vi_files -let set_vi_checking_j j = vi_files_j := int_of_string j +let set_vi_checking_j opt j = + try vi_files_j := int_of_string j + with Failure _ -> + prerr_endline ("The first argument of " ^ opt ^ " must the number"); + prerr_endline "of concurrent workers to be used (a positive integer)."; + prerr_endline "Makefiles generated by coq_makefile should be called"; + prerr_endline "setting the J variable like in 'make checkproofs J=3'"; + exit 1 let is_not_dash_option = function | Some f when String.length f > 0 && f.[0] <> '-' -> true @@ -312,7 +323,7 @@ let parse_args arglist = let tfile = next () in add_vi_task (tno,tfile) |"-schedule-vi-checking" -> - set_vi_checking_j (next ()); + set_vi_checking_j opt (next ()); add_vi_file (next ()); while is_not_dash_option (peek_next ()) do add_vi_file (next ()); done |