• 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.
session_scheduler.mli 11.4 KB