• Andrei Paskevich's avatar
    Prove_client: API refactoring · c39eacf6
    Andrei Paskevich authored
    Do not store socket_name in a reference. Instead, provide two calls:
    [connect_external] that takes the socket name as an argument and
    [connect_internal] that starts a dedicated server on a fresh socket.
    If [Prove_client.send_request] is called when no connection is
    established, it calls [connect_internal].
    
    Rationale: the only reason to have a reference for socket_name is
    to delay the connection request (for example, until the first call
    to [Prove_client.send_request]). However, if the server is already
    running when we set [socket_name], it does not cost us anything to
    establish this connection right away. This is what [connect_external]
    is for. Otherwise, if the server is not running yet, the API client
    must ensure that it will be started before the first [send_request],
    or else the connection request fails. This requires synchronisation
    between the entity that starts the server and the Why3 process. In
    this case, the API client should just call [connect_external] once
    it knows that the server is up and running.
    
    TODO:
    - what is the semantics of [disconnect]? How should we handle the
      tasks in progress?
    - what is the semantics of [max_prover_running] when working with
      an external server?
    - how should we handle server-side disconnects (if at all)?
    c39eacf6
prove_client.ml 5.84 KB