add the command why3session run

	Just a proposition for a more controllable why3replayer

Makefile.in

@@ -611,7 +611,7 @@ install_local: bin/why3replayer
 
 SESSION_FILES = why3session_lib why3session_copy why3session_info	\
 		why3session_latex why3session_html why3session_rm	\
-		why3session_output why3session
+		why3session_output why3session_run why3session
 
 SESSIONMODULES = $(addprefix src/why3session/, $(SESSION_FILES))
 

src/printer/smtv2.ml

@@ -43,6 +43,8 @@ let ident_printer =
       "Array";"select";"store";"const";
        (** div and mod are builtin *)
       "div";"mod";
+      (** distinct is builtin in some provers *)
+      "distinct"
       ]
   in
   let san = sanitizer char_to_alpha char_to_alnumus in

src/session/session_scheduler.ml

@@ -17,6 +17,33 @@ let debug = register_info_flag "scheduler"
   ~desc:"Print@ debugging@ messages@ about@ scheduling@ of@ prover@ calls@ \
          and@ transformtion@ applications."
 
+module Todo = struct
+  type ('a,'b) todo =
+      {mutable todo : int;
+       mutable report : 'a;
+       push_report : 'a -> 'b -> 'a;
+       callback : 'a -> unit}
+
+  let create init push callback =
+    {todo = 0;  report = init; push_report = push; callback = callback}
+
+  let stop todo =
+    todo.todo <- todo.todo - 1;
+    if todo.todo=0 then todo.callback todo.report
+
+  let _done todo v =
+    todo.report <- todo.push_report todo.report v;
+    stop todo
+
+  let start todo =
+    todo.todo <- todo.todo + 1
+
+(** dead code
+  let print todo =
+    dprintf debug "[Sched] todo : %i@." todo.todo
+*)
+end
+
 (***************************)
 (*     main functor        *)
 (***************************)
@@ -201,12 +228,10 @@ let schedule_any_timeout t callback =
   t.running_proofs <- (Any_timeout callback) :: t.running_proofs;
   run_timeout_handler t
 
-(* dead code
-let add_a_check t callback =
+let schedule_check t callback =
   dprintf debug "[Sched] add a new check@.";
   t.running_check <- callback :: t.running_check;
   run_timeout_handler t
-*)
 
 (* idle handler *)
 
@@ -441,34 +466,27 @@ let fuzzy_proof_time nres ores =
     Done { res' with Call_provers.pr_time = told }
   | _, _ -> nres
 
-let run_external_proof_v2 eS eT a callback =
-  callback a a.proof_prover 0 None Starting;
+(** run_external_proof_v3 doesn't modify existing proof attempt, it can just
+    create new one by find_prover *)
+let run_external_proof_v3 eS eT a callback =
   match find_prover eS a with
   | None ->
+    callback a a.proof_prover 0 None Starting;
     (* nothing to do *)
     callback a a.proof_prover 0 None MissingProver
   | Some(ap,npc,a) ->
+    callback a ap 0 None Starting;
     if a.proof_edited_as = None &&
        npc.prover_config.Whyconf.interactive
     then begin
-      set_proof_state ~notify ~obsolete:false ~archived:false
-        Unedited a;
       callback a ap 0 None (MissingFile "unedited")
     end else begin
-      let previous_result,previous_obs = a.proof_state,a.proof_obsolete in
+      let previous_result = a.proof_state in
       let timelimit, memlimit = adapt_limits a in
       let inplace = npc.prover_config.Whyconf.in_place in
       let command = Whyconf.get_complete_command npc.prover_config in
       let cb result =
         let result = fuzzy_proof_time result previous_result in
-        begin match result with
-        | Interrupted ->
-          set_proof_state ~notify ~obsolete:previous_obs
-            ~archived:false previous_result a
-        | _ ->
-          set_proof_state ~notify ~obsolete:false
-            ~archived:false result a
-        end;
         callback a ap timelimit
           (match previous_result with Done res -> Some res | _ -> None)
           (StatusChange result) in
@@ -487,11 +505,33 @@ let run_external_proof_v2 eS eT a callback =
           eT
           (goal_task a.proof_parent)
       with NoFile f ->
-        set_proof_state ~notify ~obsolete:false ~archived:false
-          Unedited a;
         callback a ap 0 None (MissingFile f)
     end
 
+(** run_external_proof_v2 modify the session according to the current state *)
+let run_external_proof_v2 eS eT a callback =
+  let previous_res = ref (a.proof_state,a.proof_obsolete) in
+  let callback a ap timelimit previous state =
+    begin match state with
+    | Starting -> previous_res := (a.proof_state,a.proof_obsolete)
+    | MissingFile _ ->
+      set_proof_state ~notify ~obsolete:false ~archived:false
+        Unedited a
+    | StatusChange result ->
+      begin match result with
+      | Interrupted ->
+        let previous_result,obsolete = !previous_res in
+        set_proof_state ~notify ~obsolete
+          ~archived:false previous_result a
+      | _ ->
+        set_proof_state ~notify ~obsolete:false
+          ~archived:false result a
+      end
+    | _ -> ()
+    end;
+    callback a ap timelimit previous state in
+  run_external_proof_v3 eS eT a callback
+
 let run_external_proof_v2 eS eT a callback =
   (* Perhaps the test a.proof_archived should be done somewhere else *)
   if a.proof_archived || running a.proof_state then () else
@@ -643,45 +683,15 @@ type report =
   | Edited_file_absent of string
   | No_former_result of Call_provers.prover_result
 
-module Todo = struct
-  type ('a,'b) todo =
-      {mutable todo : int;
-       report : 'a;
-       push_report : 'a -> 'b -> unit}
-
-  let create init push =
-    {todo = 0;  report = init; push_report = push}
-
-  let _done todo v =
-    todo.todo <- todo.todo - 1;
-    todo.push_report todo.report v
-
-(* dead code
-  let stop todo =
-    todo.todo <- todo.todo - 1
-*)
-
-  let todo todo =
-    todo.todo <- todo.todo + 1
-
-  let _end todo =
-    if todo.todo<>0 then None else Some todo.report
-
-(* dead code
-  let print todo =
-    dprintf debug "[Sched] todo : %i@." todo.todo
-*)
-end
-
 let push_report report (g,p,t,r) =
-  report := (g.goal_name,p,t,r)::!report
+  (g.goal_name,p,t,r)::report
 
 let check_external_proof eS eT todo a =
   let callback a ap tl old s =
     let g = a.proof_parent in
     match s with
     | Starting ->
-      Todo.todo todo
+      Todo.start todo
     | MissingFile f ->
       Todo._done todo (g, ap, tl, Edited_file_absent f)
     | MissingProver ->
@@ -705,15 +715,11 @@ let check_goal_and_children eS eT todo g =
 
 let check_all eS eT ~callback =
   dprintf debug "[Sched] check all@.%a@." print_session eS.session;
-  let todo = Todo.create (ref []) push_report  in
+ let todo = Todo.create [] push_report callback in
+  Todo.start todo;
   session_iter_proof_attempt (check_external_proof eS eT todo)
     eS.session;
-  let timeout () =
-    match Todo._end todo with
-      | None -> true
-      | Some reports -> callback !reports;false
-  in
-  schedule_any_timeout eT timeout
+  Todo.stop todo
 
 
 (***********************************)
@@ -725,7 +731,7 @@ let rec play_on_goal_and_children eS eT ~timelimit ~memlimit todo l g =
     if not (running status) then Todo._done todo () in
   List.iter
     (fun p ->
-      Todo.todo todo;
+      Todo.start todo;
       (* eprintf "todo increased to %d@." todo.Todo.todo; *)
       (* eprintf "prover %a on goal %s@." *)
       (*   Whyconf.print_prover p g.goal_name.Ident.id_string; *)
@@ -743,7 +749,8 @@ let rec play_on_goal_and_children eS eT ~timelimit ~memlimit todo l g =
 
 
 let play_all eS eT ~callback ~timelimit ~memlimit l =
-  let todo = Todo.create (ref ()) (fun _ _ -> ())  in
+  let todo = Todo.create () (fun () _ -> ()) callback in
+  Todo.start todo;
   PHstr.iter
     (fun _ file ->
       List.iter
@@ -753,14 +760,7 @@ let play_all eS eT ~callback ~timelimit ~memlimit l =
             th.theory_goals)
         file.file_theories)
     eS.session.session_files;
-  let timeout () =
-    (* eprintf "Timeout handler@."; *)
-    match Todo._end todo with
-      | None ->  true
-      | Some _ -> callback (); false
-  in
-  schedule_any_timeout eT timeout
-
+  Todo.stop todo
 
 
 (** Transformation *)
@@ -814,20 +814,14 @@ let rec transform eS sched ~context_unproved_goals_only ?callback tr a =
 (* method: edit current goal *)
 (*****************************)
 
-let edit_proof eS sched ~default_editor a =
-  (* check that the state is not Scheduled or Running *)
-  if a.proof_archived || running a.proof_state then ()
-(*
-    info_window `ERROR "Edition already in progress"
-*)
-  else
-      match find_prover eS a with
-        | None ->
+let edit_proof_v3 eS sched ~default_editor callback a =
+  match find_prover eS a with
+  | None ->
           (* nothing to do
              TODO: report an non replayable proof if some option is set
           *)
-          ()
-        | Some(_,npc,a) ->
+    ()
+  | Some(_,npc,a) ->
 (*
     let ap = a.proof_prover in
     match find_loadable_prover eS a.proof_prover with
@@ -854,32 +848,51 @@ let edit_proof eS sched ~default_editor a =
           (** Now [a] is a proof_attempt of the lodable prover [nap] *)
 *)
 
-          let callback res =
-            match res with
-              | Done {Call_provers.pr_answer = Call_provers.Unknown ""} ->
-                set_proof_state ~notify ~obsolete:true ~archived:false
-                  JustEdited a
-              | _ ->
-                  set_proof_state ~notify ~obsolete:false ~archived:false
-                    res a
-          in
-          let editor =
-            match npc.prover_config.Whyconf.editor with
-            | "" -> default_editor
-            | s ->
-              try
-                let ed = Whyconf.editor_by_id eS.whyconf s in
-                String.concat " "(ed.Whyconf.editor_command ::
-                  ed.Whyconf.editor_options)
-              with Not_found -> default_editor
-          in
-          let file = update_edit_external_proof eS a in
-          dprintf debug "[Editing] goal %a with command '%s' on file %s@."
-            (fun fmt a -> pp_print_string fmt
-              (Task.task_goal (goal_task a.proof_parent))
-              . Decl.pr_name.Ident.id_string)
-            a editor file;
-          schedule_edition sched editor file callback
+    let editor =
+      match npc.prover_config.Whyconf.editor with
+      | "" -> default_editor
+      | s ->
+        try
+          let ed = Whyconf.editor_by_id eS.whyconf s in
+          String.concat " "(ed.Whyconf.editor_command ::
+                              ed.Whyconf.editor_options)
+        with Not_found -> default_editor
+    in
+    let file = update_edit_external_proof eS a in
+    dprintf debug "[Editing] goal %a with command '%s' on file %s@."
+      (fun fmt a -> pp_print_string fmt
+        (Task.task_goal (goal_task a.proof_parent))
+        . Decl.pr_name.Ident.id_string)
+      a editor file;
+    schedule_edition sched editor file (fun res -> callback a res)
+
+let edit_proof eS sched ~default_editor a =
+  (* check that the state is not Scheduled or Running *)
+  if a.proof_archived || running a.proof_state then ()
+(*
+    info_window `ERROR "Edition already in progress"
+*)
+  else
+    let callback a res =
+      match res with
+      | Done {Call_provers.pr_answer = Call_provers.Unknown ""} ->
+        set_proof_state ~notify ~obsolete:true ~archived:false
+          JustEdited a
+      | _ ->
+        set_proof_state ~notify ~obsolete:false ~archived:false
+          res a
+    in
+    edit_proof_v3 eS sched ~default_editor callback a
+
+let edit_proof_v3 eS sched ~default_editor ~callback a =
+  let callback a res =
+    match res with
+    | Done {Call_provers.pr_answer = Call_provers.Unknown ""} ->
+      callback a
+    | _ -> ()
+  in
+  edit_proof_v3 eS sched ~default_editor callback a
+
 
 (*************)
 (* removing  *)

src/session/session_scheduler.mli

@@ -9,6 +9,24 @@
 (*                                                                  *)
 (********************************************************************)
 
+(*** One module for calling callback when it's time to *)
+module Todo : sig
+  type ('a,'b) todo
+
+  val create : 'a -> ('a -> 'b -> 'a) -> ('a -> unit) -> ('a,'b) todo
+    (** create init step callback *)
+
+  val start : ('a,'b) todo -> unit
+  (** one task is started *)
+
+  val stop : ('a,'b) todo -> unit
+  (** one task is stopped without information *)
+
+  val _done : ('a,'b) todo -> 'b -> unit
+  (** one task is stopped with information *)
+
+end
+
 (** Proof sessions *)
 
 open Session
@@ -131,6 +149,25 @@ module Make(O: OBSERVER) : sig
   *)
 
 
+  type run_external_status =
+  | Starting
+  | MissingProver
+  | MissingFile of string
+  | StatusChange of proof_attempt_status
+
+  val run_external_proof_v3 :
+    O.key Session.env_session -> t -> O.key Session.proof_attempt ->
+    (O.key Session.proof_attempt -> Whyconf.prover ->
+     int -> Call_provers.prover_result option -> run_external_status -> unit) ->
+    unit
+  (** [run_external_proof_v3 env_session sched pa callback] the
+      callback is applied with [callback pa p timelimit old_result
+      status]. run_external_proof_v3 don't change the existing proof
+      attempt just can add new by O.uninstalled_prover. Be aware since
+      the session is not modified there is no test to see if the
+      proof_attempt had already be started *)
+
+
   val prover_on_goal :
     O.key env_session -> t ->
     ?callback:(O.key proof_attempt -> proof_attempt_status -> unit) ->
@@ -181,6 +218,15 @@ module Make(O: OBSERVER) : sig
     O.key proof_attempt -> unit
     (** edit the given proof attempt using the appropriate editor *)
 
+  val edit_proof_v3 :
+    O.key env_session -> t ->
+    default_editor:string ->
+    callback:(O.key Session.proof_attempt ->  unit) ->
+    O.key proof_attempt -> unit
+    (** edit the given proof attempt using the appropriate editor but don't
+        modify the session *)
+
+
   val cancel : O.key any -> unit
     (** [cancel a] marks all proofs under [a] as obsolete *)
 
@@ -247,6 +293,13 @@ module Make(O: OBSERVER) : sig
   val convert_unknown_prover : O.key env_session -> unit
     (** Same as {!Session_tools.convert_unknown_prover} *)
 
+  val schedule_check: t -> (unit -> bool) -> unit
+    (** test the check time to time, reschedule it if it returns true *)
+
+  val schedule_any_timeout: t -> (unit -> bool) -> unit
+    (** run it when an action slot/worker/cpu is available. Reschedule it if it
+        return true *)
+
 end
 
 

src/why3session/why3session.ml

@@ -23,6 +23,7 @@ let cmds =
     Why3session_copy.cmd_archive;
     Why3session_rm.cmd;
     Why3session_output.cmd;
+    Why3session_run.cmd;
   |]
 
 let exec_name = Sys.argv.(0)

src/why3session/why3session_lib.ml

@@ -237,3 +237,36 @@ let opt_force_obsolete = ref false
 let force_obsolete_spec =
   ["-F", Arg.Set opt_force_obsolete,
    " transform obsolete session"]
+
+
+
+let rec ask_yn () =
+  Format.printf "(y/n)@.";
+  let answer = read_line () in
+  match answer with
+    | "y" -> true
+    | "n" -> false
+    | _ -> ask_yn ()
+
+let rec ask_yn_nonblock ~callback =
+  let b = Buffer.create 3 in
+  let s = String.create 1 in
+  Format.printf "(y/n)@.";
+  fun () ->
+    match Unix.select [Unix.stdin] [] [] 0. with
+    | [],_,_ -> true
+    | _ ->
+      if Unix.read Unix.stdin s 1 0 = 0 then
+        begin (** EndOfFile*) callback false; false end
+      else begin
+        if s.[0] <> '\n'
+        then (Buffer.add_char b s.[0]; true)
+        else
+          match Buffer.contents b with
+          | "y" -> callback true; false
+          | "n" | "" -> callback false; false
+          | _ ->
+            Format.printf "(y/N)@.";
+            Buffer.clear b;
+            true
+      end

src/why3session/why3session_lib.mli

@@ -79,3 +79,11 @@ val set_filter_verified_goal : filter_three -> unit
 (** force obsolete *)
 val opt_force_obsolete : bool ref
 val force_obsolete_spec : spec_list
+
+
+(** ask yes/no question to the user *)
+val ask_yn : unit -> bool
+
+val ask_yn_nonblock : callback:(bool -> unit) -> (unit -> bool)
+(** call the callback when an answer have been given,
+    return true if it must be retried *)

src/why3session/why3session_run.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  Copyright (C) 2010-2012                                               *)
+(*    François Bobot                                                      *)
+(*    Jean-Christophe Filliâtre                                           *)
+(*    Claude Marché                                                       *)
+(*    Guillaume Melquiond                                                 *)
+(*    Andrei Paskevich                                                    *)
+(*                                                                        *)
+(*  This software is free software; you can redistribute it and/or        *)
+(*  modify it under the terms of the GNU Library General Public           *)
+(*  License version 2.1, with the special exception on linking            *)
+(*  described in file LICENSE.                                            *)
+(*                                                                        *)
+(*  This software is distributed in the hope that it will be useful,      *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Why3
+open Why3session_lib
+open Whyconf
+open Session
+open Format
+open Debug
+module Todo = Session_scheduler.Todo
+module C = Call_provers
+
+(**
+   TODO add_transformation,...
+
+   TODO:
+    filter_state
+    filter_time
+    filter_?
+
+**)
+
+let debug = register_info_flag "verbose"
+  ~desc:"Describe@ all@ the@ result@ compared@ to@ the@ previous."
+
+(** To prover *)
+
+type edit_mode =
+| Edit_all
+| Edit_diff
+| Edit_none
+
+let opt_edit = ref Edit_none
+
+let set_edit_opt = function
+  | "all"  -> opt_edit := Edit_all
+  | "diff" -> opt_edit := Edit_diff
+  | "none" -> opt_edit := Edit_none
+  | _ -> assert false
+
+type save_mode =
+| Save_all
+| Save_obsolete
+| Save_none
+
+let opt_save = ref Save_none
+
+let set_save_opt = function
+  | "all"  -> opt_save := Save_all
+  | "obsolete" -> opt_save := Save_obsolete
+  | "none" -> opt_save := Save_none
+  | _ -> assert false
+
+type outofsync_mode =
+| Outofsync_usual
+| Outofsync_success
+| Outofsync_none
+
+let opt_outofsync = ref Outofsync_success
+
+let set_outofsync_opt = function
+  | "usual"  -> opt_outofsync := Outofsync_usual
+  | "success" -> opt_outofsync := Outofsync_success
+  | "none" -> opt_outofsync := Outofsync_none
+  | _ -> assert false
+
+
+type verbosity =
+| Vnormal
+| Vquiet
+| Vverbose
+
+let opt_verbosity = ref Vnormal
+
+
+let spec =
+  [
+   "--edit", Arg.Symbol (["all";"diff";"none"],set_edit_opt),
+   " set when the user can edit an interactive proof:
+     - all: edit all the proofs not proved valid
+     - diff: edit all the proofs that have a different result
+     - none: never ask (default)";
+   "-e", Arg.Unit (fun () -> set_edit_opt "all"),
+   " same as --edit all";
+   "--modif", Arg.Symbol (["all";"obsolete";"none"],set_save_opt),
+   " set when modification of proofs are saved:
+     - all: apply all modifications
+     - obsolete: modify only the proofs that were obsolete or are new
+     - none: modify nothing (default)";
+   "-m", Arg.Unit (fun () -> set_save_opt "all"),
+   " same as --modif all";
+   "--out-of-sync", Arg.Symbol (["none";"success";"usual"],set_outofsync_opt),
+   " set what to do with sessions which are out-of-sync with the \
+     original file or with why3:
+     - none: don't open sessions which are out-of-sync
+     - success: save them only if all the goals are proved at the end (default)
+     - usual: don't consider them specially";
+   "--quiet",Arg.Unit (fun () -> opt_verbosity := Vquiet),
+   " remove the progression";
+  ]@
+    (force_obsolete_spec @ filter_spec @ common_options)
+
+module O = struct
+  type key = unit
+
+  let create ?parent:_ () = ()
+
+  let remove _row = ()
+
+  let reset () = ()
+
+  let init = fun _row _any -> ()
+