The Coq mailing list

[e+coq-club AT x80.org (Emilio Jesús Gallego Arias)]

Hi Valentin,

Valentin Robert 
<vrobert AT cs.ucsd.edu>
 writes:

> I would like to know whether it is feasible to use ppx_deriving in a Coq
> plugin.

It is possible if you encapsulate all the logic in a ml file; mixing ml4
files and ppx is problematic, see the thread on coq-dev [1].

> I am currently building my plugin using a _CoqProject and coq_makefile. The
> generated Makefile.coq does not seem to use any of the fancy ocamlfind
> tooling, nor does it seem to cater for OCaml-specific flags (though maybe
> ZDEBUG/ZFLAGS could play that role).
>
> I would happily change this workflow if it meant I could use ppx_deriving.
>
> Does anyone have any experience with this?

jsCoq links with Coq and uses ppx to serialize data structures, see:

- https://github.com/ejgallego/jscoq/blob/master/coq-js/jssexp.ml
- https://github.com/ejgallego/jscoq/blob/master/coq-js/Makefile

I highly recommend you use ocamlfind.

I am indeed splitting serialization out of jsCoq to a plugin, I'll have
some code ready soon.

E.

[1] Message-ID: <20160226162505.GA23800@gargamel>