why3session_run.ml 12 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
MARCHE Claude's avatar
MARCHE Claude committed
4
(*  Copyright 2010-2017   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
9
(*                                                                  *)
10
(********************************************************************)
11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83

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_?

**)

(** 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),
84 85 86
   " 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\
87 88 89 90
     - 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),
91 92 93
   " set when modification of proofs are saved:\
     - all: apply all modifications\
     - obsolete: modify only the proofs that were obsolete or are new\
94 95 96 97 98
     - 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 \
99 100 101
     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)\
102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148
     - 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 -> ()

  let notify _any = ()


  let uninstalled_prover eS unknown =
    try
      Whyconf.get_prover_upgrade_policy eS.whyconf unknown
    with Not_found -> Whyconf.CPU_keep

  module Scheduler = Session_scheduler.Base_scheduler(struct end)

  include Scheduler

  let wait_level = 100
  let wait_margin = 10
  let must_wait = ref false

  let nb_file_todo = ref 0

  let notify_timer_state w s r =
    let level = w + s in
    if level > wait_level + wait_margin then must_wait := true
    else if level < wait_level - wait_margin then must_wait := false;
    if !opt_verbosity <> Vquiet then
      Printf.eprintf "Progress: %d/%d/%d/%d                       \r%!"
        !nb_file_todo w s r
end

module M = Session_scheduler.Make(O)

let print_proof_goal fmt pa =
149
  pp_print_string fmt (goal_name pa.proof_parent).Ident.id_string
150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169


let same_result r1 r2 =
  match r1.Call_provers.pr_answer, r2.Call_provers.pr_answer with
    | Call_provers.Valid, Call_provers.Valid
    | Call_provers.Invalid, Call_provers.Invalid
    | Call_provers.Timeout, Call_provers.Timeout
    | Call_provers.OutOfMemory, Call_provers.OutOfMemory
    | Call_provers.HighFailure, Call_provers.HighFailure -> true
    | Call_provers.Unknown u1, Call_provers.Unknown u2 -> u1 = u2
    | Call_provers.Failure f1, Call_provers.Failure f2 -> f1 = f2
    | _ -> false

let is_valid pr =
  match pr.Call_provers.pr_answer with
  | Call_provers.Valid -> true
  | _ -> false

let to_edit_queue = Queue.create ()

170
let is_successful env = (* means all goals proved*)
171 172 173 174
  try
    let rec iter = function
        | File f -> file_iter iter f
        | Theory th -> theory_iter iter th
175
        | Goal g -> if not (Opt.inhabited (goal_verified g)) then raise Exit
176 177 178 179 180 181 182
        | Proof_attempt _ | Transf _ | Metas _ -> assert false in
    session_iter iter env.session;
    true
  with Exit -> false


let run_one sched env config filters interactive_provers fname =
183
  let env_session, out_of_sync, missed =
184 185 186
    read_update_session ~allow_obsolete:(!opt_outofsync <> Outofsync_none)
      env config fname in
  if out_of_sync then
187 188 189
    dprintf verbose "@[From@ file@ %s: out of sync@]@." fname;
  if missed then
    dprintf verbose "@[From@ file@ %s: merge missed new goals@]@." fname;
190 191 192
  let todo = Todo.create () (fun () _ -> ())
    (fun () ->
      if !opt_save <> Save_none &&
193
        (not (out_of_sync || missed)
194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210
         || !opt_outofsync = Outofsync_usual
           || (!opt_outofsync = Outofsync_success
              && is_successful env_session ))
      then save_session config env_session.session) in
  Todo.start todo;
  let stack = Stack.create () in
  session_iter_proof_attempt_by_filter filters
    (fun pr -> Stack.push pr stack) env_session.session;
  Stack.iter (fun pr ->
    Todo.start todo;
    let rec callback pa p _timelimit old_res status =
      match old_res, status with
      | _, M.Starting -> ()
      | _, M.StatusChange (Running|Scheduled) -> ()
      | _, M.StatusChange (Interrupted) -> Todo.stop todo
      | _, M.StatusChange (JustEdited|Unedited) -> assert false
      | _, M.MissingFile efname ->
211
        dprintf verbose
212 213 214 215 216
          "@[From@ file@ %s:@\nThe@ edited@ file@ %s@ for@ the@ proof@ of@ %a@ \
           is@ missing@]@."
          fname efname print_proof_goal pa;
        Todo.stop todo
      | _, M.MissingProver ->
217
        dprintf verbose
218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235
          "@[From@ file@ %s:@\nThe@ prover@ %a@ for@ the@ proof@ of@ %a@ is@ \
           not@ installed@]@."
          fname Whyconf.print_prover p
          print_proof_goal pa;
        Todo.stop todo
      | Some old_res, M.StatusChange (Done new_res)
          when !opt_edit = Edit_all
          && Sprover.mem pa.proof_prover interactive_provers
          && not (is_valid new_res) ->
        queue_proof pa old_res new_res
      | Some old_res, M.StatusChange (Done new_res)
          when !opt_edit = Edit_diff
          && Sprover.mem pa.proof_prover interactive_provers
          && not (is_valid new_res)
          && not (same_result old_res new_res) ->
        queue_proof pa old_res new_res
      | Some old_res, M.StatusChange (Done new_res)
        when same_result old_res new_res ->
236
        dprintf verbose
237 238 239 240 241 242 243 244 245 246
          "@[From@ file@ %s:@\nThe@ prover@ %a for@ the@ proof@ of@ \
           %a@ give@ the@ same@ result@ %a@ as@ before@ %a.@]@."
          fname print_prover pa.proof_prover print_proof_goal pa
          C.print_prover_result old_res
          C.print_prover_result new_res;
          if !opt_save = Save_all ||
            (pa.proof_obsolete && !opt_save = Save_obsolete) then
            set_proof_state ~obsolete:false ~archived:false (Done new_res) pa;
        Todo.stop todo
      | None, M.StatusChange (Done new_res) ->
247
        dprintf verbose
248 249 250 251 252 253 254 255
          "@[From@ file@ %s:@\nThe@ prover@ %a@ for@ the@ proof,@ previously@ \
           undone,@ of@ %a@ give@ the@ new@ result@ %a.@]@."
          fname print_prover pa.proof_prover
          print_proof_goal pa C.print_prover_result new_res;
        if !opt_save = Save_obsolete then
          set_proof_state ~obsolete:false ~archived:false (Done new_res) pa;
        Todo.stop todo
      | Some old_res, M.StatusChange (Done new_res) when pa.proof_obsolete ->
256
        dprintf verbose
257 258 259 260 261 262 263 264
          "@[From@ file@ %s:@\nThe@ prover@ %a@ for@ the@ proof@ of@ %a@ give@ \
           the@ result@ %a@ instead@ of@ the@ obsolete@ %a.@]@."
          fname print_prover pa.proof_prover print_proof_goal pa
          C.print_prover_result new_res C.print_prover_result old_res;
        if !opt_save = Save_obsolete || !opt_save = Save_all then
          set_proof_state ~obsolete:false ~archived:false (Done new_res) pa;
        Todo.stop todo
      | Some old_res, M.StatusChange (Done new_res) ->
265
        dprintf verbose
266 267 268 269 270 271 272 273
          "@[From@ file@ %s:@\nThe@ prover@ %a@ for@ the@ proof@ of@ %a@ give@ \
           the@ result@ %a@ instead@ of@ %a.@]@."
          fname print_prover pa.proof_prover print_proof_goal pa
          C.print_prover_result new_res C.print_prover_result old_res;
        if !opt_save = Save_all then
          set_proof_state ~obsolete:false ~archived:false (Done new_res) pa;
        Todo.stop todo
      | _, M.StatusChange (InternalFailure exn) ->
274
        dprintf verbose
275 276 277 278 279 280 281 282 283 284 285
          "@[From@ file@ %s:@\nThe@ prover@ %a@ for@ the@ proof@ of@ %a@ \
             failed@ with@ the@ error@ %a@]@."
          fname print_prover pa.proof_prover print_proof_goal pa
          Exn_printer.exn_printer exn;
        Todo.stop todo
    and queue_proof a old_res new_res =
      if not (Queue.is_empty to_edit_queue) then
        Queue.push (a,old_res,new_res) to_edit_queue
      else
        edit_proof a old_res new_res
    and edit_proof a old_res new_res =
286
      printf "@[<hov 2>From@ file@ %s:@\n\
287 288 289 290 291 292 293
           Do@ you@ want@ to@ edit@ %a@ that@ fail@ with@ the@ result@ \
           %a@\nPreviously@ %a.@]@."
        fname print_external_proof a C.print_prover_result new_res
        C.print_prover_result old_res;
      let checkyn = ask_yn_nonblock ~callback:(fun b ->
        if b then
          let callback_edit pa =
294 295
            M.run_external_proof_v3 ~use_steps:false
              env_session sched pa
David Hauzar's avatar
David Hauzar committed
296
	      callback in
297
          M.edit_proof_v3 env_session sched
298
	    ~cntexample:false
299
            ~default_editor:"" (* TODO? *)
300
            ~callback:callback_edit a
301 302 303 304 305 306 307 308
        else
          Todo.stop todo;
        if not (Queue.is_empty to_edit_queue) then
          let (a,old_res,new_res) = Queue.pop to_edit_queue in
          edit_proof a old_res new_res
      ) in
      O.timeout ~ms:100 checkyn
    in
309
    M.run_external_proof_v3 ~use_steps:false env_session sched pr callback
310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347
  ) stack;
  Todo.stop todo

let run () =
  let env,config,should_exit1 = read_env_spec () in
  let filters,should_exit2 = read_filter_spec config in
  if should_exit1 || should_exit2 then exit 1;
  let sched = M.init (Whyconf.running_provers_max (Whyconf.get_main config)) in
  let interactive_provers =
    if !opt_edit <> Edit_none then
      Mprover.map_filter
        (fun p -> if p.Whyconf.interactive then Some () else None)
        (Whyconf.get_provers config)
    else Sprover.empty
  in
  try
    let files = Queue.create () in
    iter_files (fun f -> incr O.nb_file_todo; Queue.add f files);
    let run_one_by_one () =
      !O.must_wait ||
        let f = Queue.pop files in
        begin try
                run_one sched env config filters interactive_provers f
          with e when not (Debug.test_flag Debug.stack_trace) ->
            eprintf "@[From@ file@ %s:@\n%a.@]@." f Exn_printer.exn_printer e
        end;
        decr O.nb_file_todo;
        not (Queue.is_empty files) in
    if not (Queue.is_empty files) then
      M.schedule_any_timeout sched run_one_by_one;
    O.main_loop ()
  with OutdatedSession as e ->
    eprintf "@.%a@ You@ can@ allow@ it@ with@ the@ option@ -F.@."
      Exn_printer.exn_printer e


let cmd =
  { cmd_spec     = spec;
348
    cmd_desc     = "run the proof attempt that corresponds to the filter";
349 350 351
    cmd_name     = "run";
    cmd_run      = run;
  }