Emilio Jesús Gallego Arias

Very cool, thanks for the info.

I plan to use https://github.com/janestreet/ppx_hash for this; ideally we'd get this in Coq 8.11 by the way.

I mean, once Dune is the main build system of Coq, we can vendor ppx painlessly. So for example we could remove from `serlib` big chunks of `[@@deriving sexp]`.

Ok, basic support added, see a build is available at: https://github.com/ejgallego/jscoq-builds/tree/serapi an emulator is at: https://x80.org/rhino-hawk/

It should not be a lot of work and in fact I was looking forward to try it soon. I am not sure the `json` serializer will be able to...

Hi folks, indeed the current licensing situation is not good, thanks for bringing the issue into my attention. I can't think about this today, but added to my todo list.

c.f. https://github.com/coq-community/apery/issues/10

@SnarkBoojum I will first most of the issues, I think at this point I only have one question. LGPL2.1 does allow you to also pick GPL2.1 and GPL3+ , by...

In fact you can combine or even relicense the whole of Coq to GPL 3 if you want, if I read the clause correctly.

What version of SerAPI are you using? There is actually some bugs in Coq such as https://github.com/coq/coq/issues/6884 so indeed if you cannot provide a test-case I'm afraid we are going...