Curious, why did you not use coq serapi by Emilio?

[brando90]

I've been working on a pycoq interface:

• https://github.com/brando90/pycoq
• https://github.com/ejgallego/pycoq and I'm trying to understand the trade offs of how to build it. You didn't choose to use serapi, so I am curious, why is that?

[EugeneLoy]

Hi, sorry for late reply.

You didn't choose to use serapi, so I am curious, why is that?

I'd say that the main reason that I wanted to introduce as little extra dependencies as possible. As it is kernel already have dependencies on things from 2-3 different ecosystems (Python/OCaml/OS packages). Using Coq SerAPI would (likely) add more config hassle for end user and more moving parts to break.

The next big reason is that idetop (at the time of starting) was part of Coq itself, IDE worked with it and looked like more stable/reliable (in terms of community support) protocol to rely upon (esp. comparing with Coq SerAPI that has proof of concept status and now in maintenance mode).