The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

Hi Emilio and list,

On 07/01/2015 11:50 AM, Emilio Jesús Gallego Arias wrote:
> 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,

It's hard to tell without knowing the particular direction in which you are 
going, but I'm not sure about this fact. I'd like to build a tool that can 
run on anyone's machine provided Coq is installed, and independently of the 
OS, so ideally I'd like to avoid having to link against Coq.

> (...)
>> 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.

Indeed. Since a clearly defined protocol allows for easy interaction with a 
bunch of different IDEs, I hope the Coq team will commit to protocol 
stability instead of internal stability. Having both would be nice, but 
there's a high cost to doing that; the Coq team probably has much more 
exciting problems to look at :) Similarly, when protocol changes are needed, 
it seems reasonable to expect a detail description of the changes. On the 
other hand, one cannot expect a description and porting instructions for 
every internal change between releases.

> (...) - 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).

But with have many clients with many technologies: Emacs uses Elisp, IntelliJ 
uses Java, Vim uses strange magic invocations... I wouldn't want the Coq 
developers to feel committed to internal stability due to the risk of 
breaking IDEs that depend on internal details.

> (...) - 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).

I wasn't asking this question in the particular context of an IDE. However, 
in the context of PG and company-coq, I'd be afraid of incompatibilities if I 
relied on Coq's internals. One of the nice things about PG is that it makes 
very few assumptions about Coq; this allows it to still work today, despite 
very infrequent updates. I'd be afraid of taking a more tightly integrated 
route without finding a way to ensure that the project will be maintained in 
the long run. Plus, if you're IDE ends up being really cool, I'm sure plenty 
of people developing Coq plugins or hacking on Coq's source will want to look 
at it; being dependent on internals could open the door to quite a bunch of 
incompatibilities there.

Here is a concrete example: between 8.4 and 8.5, the pretty-printing 
interface changed significantly. Backporting some of my recent patches to use 
them on 8.4 took me almost as long as writing them in the first place.

> 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...)

Indeed, that's a tricky problem. The Rosilyn team at Microsoft has done great 
stuff in this domain with their free software .Net compiler; it could be 
interesting to look at that.

Cheers and thanks for the suggestions!
Clément.