The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Sat, Oct 12, 2013 at 11:59:24PM +0200, Thomas Braibant wrote:
> Now for the questions/request for comments.
> 
> * What about camlp4/camlp5?
>   Some packages (ssreflect 1.5rc1) do not compile if Coq was not
>   compiled with camlp5.

No deep reason for not supporting camlp4, actually I was planning to
fix that for 1.5.

> I do not know of packages that require camlp4
>   specifically. Is there a good reason to handle both, or should
>   camlp5 be mandatory?

The situation is quite sad.  The two tools are almost identical but with
minor incompatibilities.  Camlp4 comes with OCaml, but is not
documented, camlp5 on the contrary is documented but is a separate
package, i.e. extra burdain for the user that compile things by hand.
I'm afraid this situation is not the result of a pragmatic decision...

I think the best we can do it make the compatibility layer Coq uses for
its own sources available to plugins.  There is already a Compat module,
but is not sufficient (in the ssr case, an extra token filter is
needed).  Ideally a couple of extra .cmo to camlpX should do the work.
This should be fixed on the coq_makefile side I guess.  I'll look into
that next week.

> To conclude this email, I think that building this list of packages and
> compilers that can be installed in an automatic manner is an important
> part of the job, and help is needed on that front. Then, there is the
> actual code of the package manager: it seems that OCamlPro is willing
> to help, and I would like personally to continue to work on it in my
> spare time [2]. But if you want to help, please let me know.

For ssreflect, I can maintain the almost-opam-package if you want.

But I've a more general remark.  I do swich Coq versions too, but
I don't think I qualify as a regular user.  IMO users should stick to
the stable version, unless they want to develop Coq or a plugin.

Still, I find your ideas relevant for plugins/contribs installation,
that live their own life/release cycle.

Ciao
-- 
Enrico Tassi