1. 20 Apr, 2016 6 commits
    • Andrei Paskevich's avatar
      headers on the added files · 99b6e736
      Andrei Paskevich authored
    • Andrei Paskevich's avatar
    • Andrei Paskevich's avatar
      Session_scheduler: rework the scheduler environment type · 52580155
      Andrei Paskevich authored
      - drop the "running_check" queue, unused and unusable.
      - drop the "running_proofs" list, maintained in the proof server now.
      - send a proof task to the server as soon as it is added to
        "proof_attempts_queue" (still limited by 3 * maximum_running_proofs).
      - process "proof_attempts_queue" in the timeout_handler.
      - do not clear proof_attempts_queue on cancel_scheduled_proofs,
        since every task in it is already sent to the server, and we
        have no means at the moment to pass cancellation events to it.
        TODO: this probably should be supported: it is quite frustrating
        to have thirty proof tasks in proof_attempts_queue and not be able
        to stop those that have not started yet. To do this, we should
        decide whether we want cancel tasks one by one, or all at once,
        or both. A server should send a single answer for every task,
        which may be "ProverFinished" (if the cancellation request arrived
        too late), or "ProverInterrupted" (if we want to extend the
        "prover_update" type), or "ProverFinished (Unknown (Interrupted))"
        (if we want to extend the "reason_unknown" type).
      IMPORTANT: schedule_any_timeout behaves differently now: all
      such callbacks are immediately added to proof_attempts_queue,
      and thus are executed on every timeout event, without being
      limited by "maximum_running_proofs". This function is only
      used in why3session_run, with a comment saying that it should
      not be used there, so maybe we should drop this completely.
    • Andrei Paskevich's avatar
      Call_provers: simplify API · 8159c0d7
      Andrei Paskevich authored
      - 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.
    • Andrei Paskevich's avatar
    • Andrei Paskevich's avatar
      Merge branch 'why3server' · aef3d093
      Andrei Paskevich authored
  2. 19 Apr, 2016 5 commits
  3. 18 Apr, 2016 29 commits