new option -q for replayer, prints only warnings

allows to show the warnings in the nightly bench

CHANGES

 * marks an incompatible change
 
+  o new warning: form exists x, P -> Q
+  o [replayer] new option -q
   o [Provers] support for Coq 8.4
   o New scheme for Coq realizations, using type classes
 

ROADMAP

@@ -132,14 +132,20 @@ scheduled on Sep 2012
 New features:
 
   o new API for programs
-  o type invariants ?
+  o type invariants
+
+  o transformations for induction
+
   o Support for Coq 8.4
   o dropped support for Coq 8.2
   o new scheme for Coq realizations using type classes
   o Support for PVS 6.0, including realizations
   o support for iProver and Zenon
+
   o a warning is emitted for unused bound logic variables in
     "forall", "exists" and "let"
+  o new warning: formulas of the form "exists x, P -> Q" 
+  o [replayer] new option -q
 
 Bug fixes:
 
@@ -190,6 +196,10 @@ Bug fixes:
 
 == TODOs ==
 
+
+* faire le menage dans les transformations d'induction : _int _ty
+  _ty_lex, et DOCUMENTER
+
 * Sortie PVS
 ** avec mecanisme de realization
 

doc/manpages.tex

@@ -528,6 +528,7 @@ option \verb|-force| described below.
 \item The exit code is 0 if no difference was detected, 1 if there
   was. Other exit codes mean some failure in running the replay.
 \item Option \verb|-s| suppresses the output of the final tree view.
+\item Option \verb|-q| runs quietly (no progress info)
 \item Option \texttt{-I \textsl{<path>}} adds \texttt{\textsl{<path>}} to the loadpath.
 \item Option \verb|-force| enforces saving the session, if all proof
   attempts replayed correctly, even if some goals are not proved.

examples/hoare_logic/blocking_semantics5.mlw

@@ -711,7 +711,7 @@ function wp (s:stmt) (q:fmla) : fmla =
   (** {3 main soundness result} *)
 
   lemma wp_soundness:
-    forall n :int, sigma sigma':env, pi pi':stack, s s':stmt,
+    forall n:int, sigma sigma':env, pi pi':stack, s s':stmt,
            sigmat: type_env, pit: type_stack, q:fmla.
       compatible_env sigma sigmat pi pit ->
       type_stmt sigmat pit s ->

examples/hoare_logic/blocking_semantics5/why3session.xml

@@ -2734,7 +2734,7 @@
      edited="blocking_semantics5_WP_wp_soundness_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.83"/>
+     <result status="valid" time="0.70"/>
     </proof>
    </goal>
   </theory>

examples/regtests.sh

@@ -32,7 +32,7 @@ run_dir () {
     for f in `ls $1/*/why3session.xml`; do
         d=`dirname $f`
 	echo -n "Replaying $d ... "
-        ../bin/why3replayer.opt $REPLAYOPT $2 $d 2> $TMPERR > $TMP
+        ../bin/why3replayer.opt -q $REPLAYOPT $2 $d 2> $TMPERR > $TMP
         ret=$?
 	if test "$ret" != "0"  ; then
 	    echo -n "FAILED (ret code=$ret):"
@@ -46,7 +46,7 @@ run_dir () {
 	    res=1
 	else
 	    echo -n "OK"
-	    cat $TMP
+	    cat $TMP $TMPERR
             success=`expr $success + 1`
 	fi
         total=`expr $total + 1`

src/ide/replay.ml

@@ -30,6 +30,7 @@ let opt_stats = ref true
 let opt_force = ref false
 let opt_obsolete_only = ref false
 let opt_bench = ref false
+let opt_verbose = ref true
 
 (** {2 Smoke detector} *)
 
@@ -83,6 +84,9 @@ let spec = Arg.align [
   ("-s",
    Arg.Clear opt_stats,
    " do not print statistics") ;
+  ("-q",
+   Arg.Clear opt_verbose,
+   " run quietly") ;
   ("-v",
    Arg.Set opt_version,
    " print version information") ;
@@ -301,7 +305,7 @@ let same_result r1 r2 =
 let add_to_check_no_smoke config found_obs env_session sched =
   let session = env_session.S.session in
   let callback report =
-    eprintf "@.";
+    if !opt_verbose then eprintf "@.";
     let files,n,m =
       S.PHstr.fold file_statistics
         session.S.session_files ([],0,0)
@@ -329,12 +333,12 @@ session NOT updated)@." n m
         else
           printf " %d/%d@." n m ;
         if !opt_stats && n<m then print_statistics files;
-        eprintf "Everything replayed OK.@.";
+        if !opt_verbose then eprintf "Everything replayed OK.@.";
         if found_obs && (n=m || !opt_force) then
           begin
-            eprintf "Saving session...@?";
+            if !opt_verbose then eprintf "Saving session...@?";
             S.save_session config session;
-            eprintf " done@."
+            if !opt_verbose then eprintf " done@."
           end;
         exit 0
       end
@@ -351,7 +355,7 @@ session NOT updated)@." n m
 
 let add_to_check_smoke env_session sched =
   let callback report =
-    eprintf "@.";
+    if !opt_verbose then eprintf "@.";
     let report =
       List.filter
         (function
@@ -362,7 +366,7 @@ let add_to_check_smoke env_session sched =
           | _ -> false) report
     in
     if report = [] then begin
-      eprintf "No smoke detected.@.";
+      if !opt_verbose then eprintf "No smoke detected.@.";
       exit 0
     end
     else begin
@@ -417,15 +421,16 @@ let run_as_bench env_session =
 
 let () =
   try
-    eprintf "Opening session...@?";
+    if !opt_verbose then eprintf "Opening session...@?";
+    O.verbose := !opt_verbose;
     let env_session,found_obs =
       let session = S.read_session project_dir in
       M.update_session ~allow_obsolete:true session env config
     in
-    eprintf " done.@.";
+    if !opt_verbose then eprintf " done.@.";
     if !opt_obsolete_only && not found_obs then
       begin
-        eprintf "Session is not obsolete, hence no replayed@.";
+        eprintf "Session is not obsolete, hence not replayed@.";
         printf "@.";
         exit 0
       end;

src/session/session_scheduler.ml

@@ -992,6 +992,8 @@ module Base_scheduler (X : sig end)  =
     let idle_handler = ref None
     let timeout_handler = ref None
 
+    let verbose = ref true
+
      let idle f =
        match !idle_handler with
          | None -> idle_handler := Some f;
@@ -1003,7 +1005,8 @@ module Base_scheduler (X : sig end)  =
          | Some _ -> failwith "Replay.timeout: already one handler installed"
 
      let notify_timer_state w s r =
-       Printf.eprintf "Progress: %d/%d/%d                       \r%!" w s r
+       if !verbose then
+         Printf.eprintf "Progress: %d/%d/%d                       \r%!" w s r
 
      let main_loop () =
        let last = ref (Unix.gettimeofday ()) in

src/session/session_scheduler.mli

@@ -265,6 +265,7 @@ module Base_scheduler (X : sig end) : sig
 
   val timeout: ms:int -> (unit -> bool) -> unit
   val idle: (unit -> bool) -> unit
+  val verbose : bool ref
   val notify_timer_state : int -> int -> int -> unit
   (** These functions have the properties required by OBSERVER *)