From bae17b767dc4b0f3574d2aaa1b1f90f1e4ac29dd Mon Sep 17 00:00:00 2001 From: Claude Marche Date: Wed, 10 Oct 2012 14:19:36 +0200 Subject: [PATCH] new option -q for replayer, prints only warnings allows to show the warnings in the nightly bench --- CHANGES | 2 ++ ROADMAP | 12 +++++++++- doc/manpages.tex | 1 + examples/hoare_logic/blocking_semantics5.mlw | 2 +- .../blocking_semantics5/why3session.xml | 2 +- examples/regtests.sh | 4 ++-- src/ide/replay.ml | 23 +++++++++++-------- src/session/session_scheduler.ml | 5 +++- src/session/session_scheduler.mli | 1 + 9 files changed, 37 insertions(+), 15 deletions(-) diff --git a/CHANGES b/CHANGES index 3ae49637c..243e70643 100644 --- a/CHANGES +++ b/CHANGES @@ -1,5 +1,7 @@ * 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 diff --git a/ROADMAP b/ROADMAP index 603801a4d..74d4b9504 100644 --- a/ROADMAP +++ b/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 diff --git a/doc/manpages.tex b/doc/manpages.tex index b947fd43a..5535f70f0 100644 --- a/doc/manpages.tex +++ b/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{}} adds \texttt{\textsl{}} to the loadpath. \item Option \verb|-force| enforces saving the session, if all proof attempts replayed correctly, even if some goals are not proved. diff --git a/examples/hoare_logic/blocking_semantics5.mlw b/examples/hoare_logic/blocking_semantics5.mlw index 9ea642e4d..07691d240 100644 --- a/examples/hoare_logic/blocking_semantics5.mlw +++ b/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 -> diff --git a/examples/hoare_logic/blocking_semantics5/why3session.xml b/examples/hoare_logic/blocking_semantics5/why3session.xml index 3ebc01508..03b635885 100644 --- a/examples/hoare_logic/blocking_semantics5/why3session.xml +++ b/examples/hoare_logic/blocking_semantics5/why3session.xml @@ -2734,7 +2734,7 @@ edited="blocking_semantics5_WP_wp_soundness_1.v" obsolete="false" archived="false"> - + diff --git a/examples/regtests.sh b/examples/regtests.sh index c45d9f822..b96a4b5ea 100755 --- a/examples/regtests.sh +++ b/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` diff --git a/src/ide/replay.ml b/src/ide/replay.ml index dc4cee45b..3541b86b0 100644 --- a/src/ide/replay.ml +++ b/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 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; diff --git a/src/session/session_scheduler.ml b/src/session/session_scheduler.ml index 6e376f732..9d3a92314 100644 --- a/src/session/session_scheduler.ml +++ b/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 diff --git a/src/session/session_scheduler.mli b/src/session/session_scheduler.mli index 57ba64aa2..d5cc90f06 100644 --- a/src/session/session_scheduler.mli +++ b/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 *) -- GitLab