The Coq mailing list

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

Hi Clément,

Clément Pit--Claudel 
<clement.pit AT gmail.com>
 writes:

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

Well, indeed I am cheating here as even if I link to Coq, then I produce
"more or less" portable code.

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

Yeah a bit of my though in that sense is that you would ideally marshall
*automatically* the Ocaml API to whatever standard RPC you want, then
use such tools.

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

That sounds very cool, would you mind pointing me to a specific
reference?

Thanks!

Best regards,
Emilio