The Coq mailing list

[Valentin Robert <vrobert AT cs.ucsd.edu>]

Thanks Emilio, this looks extremely similar to what I am trying to achieve! (I need a serializer for constr_expr)

- Valentin

On Fri, May 6, 2016 at 4:17 PM Emilio Jesús Gallego Arias <e+coq-club AT x80.org> wrote:

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>