The Coq mailing list

[Guillaume Claret <guillaume AT claret.me>]

Hi,

I agree a package manager is a need for Coq and thanks for proposing 
this idea. OPAM seems the most pragmatic approach since it exists and 
handles OCaml code (many plugins contain OCaml files or even depend on 
other OCaml projects).

An easy switching system could also help testing and continuous 
integration of packages on various Coq versions. We could probably reuse 
tools like https://github.com/ocamllabs/ocamlot .

To me it is OK to recompile all the packages when someone switches to a 
new Coq version, as long as we use a cache for previously compiled files 
for the current version (as it is done for OPAM with OCaml compilers). I 
would say that, since packages can contains .v and .ml files, a "current 
compiler" is actually a couple ("current OCaml compiler", "current Coq 
version (+ compilation flags like camlp4/5))". This makes a lot of 
combinations but it prevents any unexpected collisions and disk usage 
should not be a problem today.

The implementation may be a patch to OPAM or a separated project using 
OPAM as a back-end library. In this case, could "coq-egg" be a good 
command-line name?

We should also have a separated repository hosted on 
http://coq.inria.fr/ . Contribs are a good base to start with (more than 
100 packages). I have started to make a script to import them. We could 
also generate a nice web front-end using 
https://github.com/OCamlPro/opam2web .

Cheers,
Guillaume

Le 15/10/2013 12:16, Enrico Tassi a écrit :> On Mon, Oct 14, 2013 at 
09:55:45PM +0200, Thomas Braibant wrote:
>> Hi,
>>
>>> I also expect to see more and more Coq developments relying on existing
>>> plugins (ssreflect, mtac,...) or combinations thereof, so the idea you
>>> mentioned of having persistent packages is probably worth exploring.
>>
>> Yes, I have the same feeling. Note though that mtac is a patch of Coq,
>> not a plugin (even if it may change in the future, afaik), and
>> therefore, lives in its own switch. I would really like to know if
>> there are other packages like ssreflect 1) that takes a long time to
>> compile, 2) people often switch from version to version.
>
> Just for the records, from version 1.5 ssreflect and the mathematical
> components library will split.  Ssreflect will contain "only" the files
> up to and including fintype.  This takes way less time to compile than
> the whole math comp library.
>
> Still there are users of the whole library ;-)
>
> Ciao
>