• Andrei Paskevich's avatar
    Prove_client: change the "standalone" logic · 39ed26b1
    Andrei Paskevich authored
    1. No default socket name is provided. If Why3 should connect to
       an external server, Prove_client.set_socket_name must be called
       first.
    
    2. If Prove_client.set_socket_name was never called, Why3 assumes
       to be in the stand-alone mode, and will start the server in the
       standard tmp directory (on Unix, $TMPDIR or /tmp, on Win, $TEMP or .).
       The socket name is set to be "why3server.<PID_of_Why3>.sock",
       to avoid clashes with other Why3 processes (fixes the Coq tactic).
    
    3. Global reference Prove_client.standalone is removed.
    
    4. Call_provers does not reexport Prove_client.set_socket_name.
    
    5. Prove_client.connect does nothing if the socket reference is set.
    39ed26b1
prove_client.ml 4.93 KB