coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] About camlp5 and coq

From: Kakadu <Kakadu AT protonmail.ch>
To: coq-club AT inria.fr
Subject: [Coq-Club] About camlp5 and coq
Date: Fri, 04 Nov 2016 14:16:57 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=Kakadu AT protonmail.ch; spf=Pass smtp.mailfrom=Kakadu AT protonmail.ch; spf=Pass smtp.helo=postmaster AT mail4.protonmail.ch
Feedback-id: x4fwwyFgtRX3dSO51dMsbqWOEHlPiGfshOOS9J25YwI543bF7VeYg98tu93v-1yW4PsM4izyxQYM1xYUcvtBqg==:Ext:ProtonMail
Ironport-phdr: 9a23:uSZaTRWGuelGNdtK8vnPCplEiLPV8LGtZVwlr6E/grcLSJyIuqrYZhSDt8tkgFKBZ4jH8fUM07OQ6PG6HzxRqs/Z6DhCKMUKDEBVz51O3kQJO42sNw7SFLbSdSs0HcBPBhdO3kqQFgxrIvv4fEDYuXao7DQfSV3VPAtxIfnpSMaJ15zkn7P6x5qGaAJRwTG5fLlaLROsrAyXuNNFu4Z6LrcNzU7qq3hBd/kekUBhJlufgj7k/MCs+5hm+iVU/fkhoZ1uS6L/KocxTrVUEXxyEGk27cH2nQHZSheI4H4VU2FQmRoeUFuN1w3zQpqk6niyjeF6wiTPZcA=

Hello

I'm participating in a project that uses camlp5 and there are some camlp5-specific issues, most of them happens because pr_dump is buggy and we are forced to use pr_o. So, we lose some file locations in error messages and it is annoying.

I have fixed a few issues in pr_dump recently. A few are left. I hope I will manage to push patchesa to upstream.

AFAIU coq is the main user of camlp5 and there are rumors that lack of attributes in camlp5 forbids using PPX rewriters in Coq (but this feature is desired).

Can you somehow summarise how Coq lives with camlp5, which issues do you face because of it, etc?

Happy hacking,
Kakadu

[Coq-Club] About camlp5 and coq, Kakadu, 11/04/2016
- Re: [Coq-Club] About camlp5 and coq, Emilio Jesús Gallego Arias, 11/04/2016
  - Re: [Coq-Club] About camlp5 and coq, Kakadu, 11/08/2016
    - Re: [Coq-Club] About camlp5 and coq, Pierre-Marie Pédrot, 11/08/2016
    - Re: [Coq-Club] About camlp5 and coq, Emilio Jesús Gallego Arias, 11/08/2016