• 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
why3tac.ml4 49.9 KB