The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

Hi Enrico,

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

I think that's nice on the one hand that you can make it work. But I
think it is really sad too to have to handle the discrepancies between
the two.

> > 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 there is a pragmatic decision coming: Xavier announced last
OCaml workshop that some part of the OCaml distribution can be split
off as separate projects, and camlp4  was earmarked as "soon" (not
"under discussion" but "soon").  At that point, there will be 2 almost
identical tools, not packaged, one of them being documented.


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

That would be nice, I will come back to you.

> 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.

Well, I think other have made the point that they do switch Coq
versions often. I develop plugins, but this is not my main reason to
change version. My main reason to change version is to have a look at
old developments, or when I do reviews, or to try out other people
libraries. I think this is part of the routine of many coq users, but
again, I would like to see numbers on this point too. I will make a
survey, with all these tiny questions that could help understand who
are the coq users, and what are their habits. (Not joking).

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

Many thanks for your support.
Thomas