coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Using ppx_deriving in a Coq plugin

From: Valentin Robert <vrobert AT cs.ucsd.edu>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Using ppx_deriving in a Coq plugin
Date: Fri, 06 May 2016 21:31:22 +0000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=vrobert AT cs.ucsd.edu; spf=Pass smtp.mailfrom=valentin.robert.42 AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw0-f178.google.com
Ironport-phdr: 9a23:XjSd1hIwmDel0HhqLNmcpTZWNBhigK39O0sv0rFitYgULPzxwZ3uMQTl6Ol3ixeRBMOAu6MC07Wd6/uocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWM5DIfUi/yKRBybrysXNWC3oLviKvqoNX6WEZhunmUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD86Fpy8kVG679ZuEzSaFSJDUgKWE8osPx/1GXRgyWo3AYT28+kxxSAgGD4gusDbnrtS6viON51S+GPMu+d7c+VC6+p/N1UhjihT0bHzUitnzckcA2ga5G9kHy7ydjypLZNdnGfMF1ebnQKIsX

Hello club,

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

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?

Best regards,

- Valentin

[Coq-Club] Using ppx_deriving in a Coq plugin, Valentin Robert, 05/06/2016
- Re: [Coq-Club] Using ppx_deriving in a Coq plugin, Emilio Jesús Gallego Arias, 05/07/2016
  - Re: [Coq-Club] Using ppx_deriving in a Coq plugin, Valentin Robert, 05/07/2016