The Coq mailing list

[gallego AT cri.ensmp.fr (Emilio Jesús Gallego Arias)]

Hi Pierre,

Pierre Courtieu 
<pierre.courtieu AT gmail.com>
 writes:

> Hi Emilio, Could you please be more precise?

Of course! I'll actually rehash some of the discussion we had at the Coq
Coding Sprint, my apologies to those that have to hear me again.

> The coq team just spent some time in the last two years making an xml
> protocol in order to de-correlate coq from its ide. The idea being that

Indeed having a protocol is great for a lot of uses cases.

My use case is very particular, this is why I prefer linking, and indeed
it seems that Clément is moving in similar directions than ours, so this
is why I commented about the linking possibility.

> 1) ide can run in a different thread, ide can even talk with different
>    forks (workers) of the same coq.

I don't see why this cannot work when linking too.

> 2) the codes are well separated and a bug in coq leaves the interface
>    alive

Given how much state we have in a typical Coq session I'm not sure that
would be useful.

I am using Coq as library from my IDE, so the code is IMHVO reasonably
separated.

> 3) protocols are essentially APIs that one cannot easily shunt, so it
> forces good practice.

I think the argument works both ways, commitment to API stability or
protocol stability is a human choice.

IMVHO good practice cannot be forced through technical means.

As we have witnessed, many vendors over the years have made changes
to protocols, creating countless problems.

> So any argument in favor of going back to a linked interface should be
> looked at very carefully. I think a lot of things can be done via a well
> designed protocol.

Sure, however, I don't see why both cannot coexist, people linking to
Coq shouldn't harm the protocol users, indeed, it could even make the
protocol better by exposing new uses cases.

Why do I prefer linking to the protocol?

- IMVHO a "protocol" would make more sense if we had several clients *and
  _servers_* which are implemented using different technologies.

  In this case, we have only one server and one technology (OCaml).

  Would my IDE have to talk to a Java version of Coq in addition to the
  Ocaml one I would run into more trouble for sure.

- I don't have to spend time marshalling/unmarshalling things back.

  The size, complexity, and duplication of my code base are
  significantly reduced. Performance is better.

  In addition, I don't have to maintain my own data structures as I
  reuse Coq's.

- I don't have to care about state or asynchronous communication so much.

- Error handling is easier.

- A coq session is extremely stateful, this may be very hard to handle
  correctly with a protocol.

- And the true dealbreaker for me, I'm not bound to what the protocol
  specifies.

  Indeed, my IDE wants to interact with the pretyper, with the matching
  algorithm, implement different printing routines (as in Clément's).

  So basically, I'd have to either limit my IDE to more traditional
  features or I'd have to marshal half of Coq internal structures
  through XML. (Good luck with marshalling Ocaml refs, etc...)

Best regards,
E.