1. 28 Mar, 2018 1 commit
  2. 27 Mar, 2018 1 commit
    • Sylvain Dailler's avatar
      Add debug keep_vcs: allow to use a given filename to save prover files. · 979cf05c
      Sylvain Dailler authored
      It is now possible to give an optional argument to schedule_proof_attempt
      so that (when in debug mode) the file given is used to store the generated
      input file of the prover. In non debug mode, the file given to
      schedule_proof_attempt is used but removed after the call to the prover.
      
      Currently, no file is ever given to schedule_proof_attempt but this can be
      used by people using Why3 as a backend.
      979cf05c
  3. 26 Mar, 2018 1 commit
  4. 16 Mar, 2018 1 commit
  5. 11 Jan, 2018 1 commit
  6. 06 Nov, 2017 3 commits
  7. 01 Nov, 2017 1 commit
  8. 20 Sep, 2017 1 commit
  9. 14 Sep, 2017 1 commit
  10. 13 Sep, 2017 1 commit
    • Sylvain Dailler's avatar
      Using new forward_result to get new results from why3server. · d1c876ec
      Sylvain Dailler authored
      Changing the structure of timeout_handler which now uses one hashtable
      with the prover calls information and one queue which has the editor call
      information.
      The loop in timeout_handler is now done on the result given by why3server
      not on a queue of prover task. This is more efficient and the code should
      be the same even when blocking = true.
      d1c876ec
  11. 10 May, 2017 1 commit
  12. 12 Apr, 2017 1 commit
  13. 04 Nov, 2016 1 commit
    • Sylvain Dailler's avatar
      Added replay. To be checked/tested. · c80328b7
      Sylvain Dailler authored
      * call_provers.ml
      (prover_update): Adding unimplemented errors that reflects the cases of
      proof_attempt_status. Otherwise, proof_attempt_status is a list of cases
      that are never reached.
      * controller_itp.ml
      (proof_attempt_status): Added Uninstalled case in proof_attempt_status.
      Launched in replay when asked to replay something not installed.
      (print_trans_status): Adding a ! when proof is valid for debugging
      reasons.
      (report): Added a report type for replay reporting of differences.
      (print_report): printing function for report.
      (replay_print): callback used with replay to print the report at the end.
      (replay): Function that replays all proof attempts of the session.
      
      * session_itp.ml
      (session_iter_proof_attempt): Added the proofNodeID the fold function
      for convenience.
      * why3shell.ml
      (test_replay): Added to test replay.
      c80328b7
  14. 11 Oct, 2016 1 commit
    • Johannes Kanig's avatar
      P909-002 allow for large exit codes · 883af7f6
      Johannes Kanig authored
      Sometimes the windows syscall GetExitCodeProcess returns a large result,
      larger than the ocaml [int] type. This is expected and not an error. For
      example the constant STATUS_QUOTA_EXCEEDED, which is 0xC0000044, may be
      a valid exit code. Such large values trip up the [int_of_string] parsing
      in the client.
      
      This patch implements the following solution to this problem:
      * the server doesn't care and sends the large value;
      * (the server now recognizes this value, though, to set the timeout flag
        more often)
      * the client uses an Int64 value to parse that big constant;
      * when converting to the internal Unix.process_status type, we simply
        convert to [int], because such large values don't have any special
        meaning for Why3 anyway.
      
      * call_provers.ml
      (parse_prover_run): now directly take the exit status as argument, and
      convert it to int;
      (handle_answer): don't wrap argument to parse_prover_run into unix type
      * prove_client.ml
      (read_answer): read Int64 type now
      * server-win.c
      (handle_child_event): set timeout boolean also when exitcode is equal to
         constant STATUS_QUOTA_EXCEEDED
      
      Change-Id: I1163a6f1adf1bdbfe1f53269ce0ae57dc8bd0287
      883af7f6
  15. 26 Sep, 2016 1 commit
    • MARCHE Claude's avatar
      Yet another attempt to fix unstability of prover answers · 32c8a24c
      MARCHE Claude authored
      - Call_provers.parse_prover_run does not attempt fixing answer anymore,
        except in the case where the answer is HighFailure and time is close
        to time limit (which is considered as Timeout)
      
      - Session_scheduler.fuzzy_proof_time is now more liberal, accepts
        that two answers Unknown or Timeout of OutOfMemory with less than
        10% difference in time are equivalent, and thus should not be
        reported as a significant change
      32c8a24c
  16. 17 Aug, 2016 1 commit
  17. 01 Jul, 2016 1 commit
  18. 10 May, 2016 1 commit
    • Johannes Kanig's avatar
      P509-017 fix incorrect time limits · 34f472e9
      Johannes Kanig authored
      The adaptation of time limits was incorrect, and could transform "0" (no
      time limit) to "1" (second).
      
      * call_provers.ml
      (adapt_limit): do nothing when no time limit was present
      34f472e9
  19. 20 Apr, 2016 1 commit
    • Andrei Paskevich's avatar
      Call_provers: simplify API · 8159c0d7
      Andrei Paskevich authored
      Call_provers:
      
      - drop closures "pre_prover_call" and "post_prover_call". They were
        intended to be used for synchronous interaction with provers from
        multiple threads. This is now responsibility of the proof server:
        (a) any Call_prover.call_on_[file|buffer] submits the proof task
            immediately to the server;
        (b) all proof results are handled in the working Why3 thread.
      
      - Call_provers.query_call returns a tri-state "prover_update" type
        which can be one of: "ProverStarted" (returned after the proof
        server informs Why3 that a prover was started), "ProverFinished"
        (returned after the proof server returns the prover result), and
        "NoUpdates" (returned when the proof server has not sent any new
        updates concerning the proof task in question).
      
          IMPORTANT: query_call does not maintain the state of a given
        prover call. In a normal use case, "ProverFinished" is returned
        _exactly_ once, and "ProverStarted" _at_most_ once (never for
        an editor call or when rapidly overwritten by "ProverFinished").
      
          TODO: extend the proof server protocol and implementation to
        send "ProverStarted" events back to Why3.
      8159c0d7
  20. 15 Apr, 2016 2 commits
  21. 14 Apr, 2016 6 commits
  22. 12 Apr, 2016 2 commits
  23. 11 Apr, 2016 1 commit
  24. 10 Apr, 2016 1 commit
  25. 05 Apr, 2016 1 commit
  26. 25 Mar, 2016 1 commit
    • Johannes Kanig's avatar
      replace prover spawning by connection to why3server · 69b8ed31
      Johannes Kanig authored
      * previous implementations of call_on_file and call_on_buffer are
        removed, and now directly use the prove_file_server function
      * now, both blocking and nonblocking reading is supported on the socket
      * wait_on_call and query_call are implemented by blocking and
        nonblocking read, together with a result buffer, if results for other
        prover runs are returned
      * logging of the server is now optional
      69b8ed31
  27. 19 Mar, 2016 1 commit
  28. 17 Mar, 2016 2 commits
  29. 15 Mar, 2016 2 commits