Small change in the effect of the -force option of the replayer

doc/manpages.tex

@@ -430,7 +430,7 @@ the new run are shown.
 
 Nothing is shown when there is no change in the results, whether the
 considered goal is proved or not. When all the proof
-
+are done, a summary of what is proved or not is displayed using a
 tree-shape pretty print, similar to the IDE tree view after doing
 ``Collapse proved goals''. In other words, when a goal, a theory, or a
 file is fully proved, the subtree is not shown.
@@ -438,9 +438,15 @@ file is fully proved, the subtree is not shown.
 \paragraph{Obsolete proofs}
 
 When some proofs stored in the session file are obsolete, the replay is
-run anyway, as with the replay button in the IDE. Then, if all the
-replayed proofs went OK, the session file is updated. Otherwise you have
-to use the IDE to update it.
+run anyway, as with the replay button in the IDE. Then, the session
+file will be updated if both 
+\begin{itemize}
+\item all the replayed proof attempts give the same result as what
+  is stored in the session
+\item every goals are proved.
+\end{itemize}
+In other cases, you can use the IDE to update the session, or use the
+option \verb|-force| described below.
 
 \paragraph{Exit code and options}
 
@@ -449,8 +455,8 @@ to use the IDE to update it.
   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 \texttt{-I \textsl{<path>}} adds \texttt{\textsl{<path>}} to the loadpath.
-\item Option \verb|-force| writes a new session file even if
-  some proofs did not replay correctly.
+\item Option \verb|-force| enforces saving the session, if all proof
+  attempts replayed correctly, even if some goals are not proved.
 \item Option \texttt{-smoke-detector \{none|top|deep\}} tries to detect
   if the context is self-contradicting.
 \end{itemize}

src/ide/replay.ml

@@ -28,7 +28,9 @@ let file = ref None
 let opt_version = ref false
 let opt_stats = ref true
 let opt_force = ref false
+(*
 let opt_convert_unknown_provers = ref false
+*)
 let opt_bench = ref false
 
 (** {2 Smoke detector} *)
@@ -69,20 +71,24 @@ let spec = Arg.align [
    "<file> Read additional configuration from <file>") ;
   ("-force",
    Arg.Set opt_force,
-   " enforce saving of session even if replay failed") ;
+   " enforce saving the session after replay") ;
   ("-smoke-detector",
    Arg.Symbol (["none";"top";"deep"],set_opt_smoke),
    " try to detect if the context is self-contradicting") ;
+(*
   ("-bench",
    Arg.Set opt_bench, " run as bench (experimental)");
+*)
   ("-s",
    Arg.Clear opt_stats,
    " do not print statistics") ;
   ("-v",
    Arg.Set opt_version,
    " print version information") ;
+(*
   "--convert-unknown-provers", Arg.Set opt_convert_unknown_provers,
   " try to find compatible provers for all unknown provers";
+*)
   Debug.Opt.desc_debug_list;
   Debug.Opt.desc_shortcut "parse_only" "--parse-only" " Stop after parsing";
   Debug.Opt.desc_shortcut
@@ -321,24 +327,23 @@ let add_to_check_no_smoke config found_obs env_session sched =
             report
         in
         if report = [] then begin
+          if !opt_force then
+            printf " %d/%d (replay OK, session going to be saved since -force was given)@." n m
+          else
             if found_obs then
               if n=m then
                 printf " %d/%d (replay OK, all proved: obsolete session \
 updated)@." n m
               else
-                if !opt_force then
-                  printf " %d/%d (replay OK, but not all proved: obsolete \
-session updated since -force was given)@." n m
-                else
-                  printf " %d/%d (replay OK, but not all proved: obsolete \
+                printf " %d/%d (replay OK, but not all proved: obsolete \
 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 found_obs && (n=m || !opt_force) then
+            if (found_obs && n=m) || !opt_force then
               begin
-                eprintf "Updating obsolete session...@?";
+                eprintf "Saving session...@?";
                 S.save_session config session;
                 eprintf " done@."
               end;
@@ -430,7 +435,9 @@ let () =
     eprintf " done.@.";
     if !opt_bench then run_as_bench env_session;
     transform_smoke env_session;
+(*
     if !opt_convert_unknown_provers then M.convert_unknown_prover env_session;
+*)
     let sched =
       M.init (Whyconf.running_provers_max (Whyconf.get_main config)) in
     if found_obs then begin