The Coq mailing list

[Bas Spitters <spitters AT cs.ru.nl>]

I once did the following back-of-the-envelope computation:

http://qa.debian.org/popcon.php?package=coq
1210 installations
http://popcon.ubuntu.com/by_inst
5697 installations!

To complete the statistics you would need to have a distribution of
operating systems.
http://distrowatch.com/

There should be more than 20,000 *linux* installations of Coq!

Maybe 50,000 installations in total ????

I am sure someone will correct these numbers.

On Mon, Oct 14, 2013 at 4:00 PM, Thomas Braibant
<thomas.braibant AT gmail.com>
 wrote:
> Hi,
>
> I am not sure at all about that, because the space of installed packaged may
> become quite big (if you consider one image per possible subset of installed
> packages).
>
> Yet I still find the suggestion very interesting in a slightly different
> context: Coq is widely [1] used in academia. It might be very nice to
> package a given Coq version, with a given set of package as a Dockerfile
> script, and provide that for students. It would be a nice and easy way to
> get everyone use the same setup, when giving a Coq class. (BTW, this rings a
> bell, so maybe it already exists).
>
> [1] This is a personal opinion, on which I would love to get precise numbers
>
> Thomas
>
>
> On Sun, Oct 13, 2013 at 2:34 AM, t x 
> <txrev319 AT gmail.com>
>  wrote:
>>
>> One thing possibly worth considering might be docker.io -- they use copy
>> on write file systems, so one can create a base ubuntu + ocaml image, and
>> the various Coq installations are "diffs" against the base image.
>>
>> Each "package" then becomes a Dockerfile script which builds the variant
>> of Coq.
>>
>>
>> On Sat, Oct 12, 2013 at 2:59 PM, Thomas Braibant
>> <thomas.braibant AT gmail.com>
>>  wrote:
>>>
>>> Hi list,
>>>
>>> Last summer, I have been playing around a prototype package manager
>>> for Coq. It is really a prototype and not ready for public consumption,
>>> but it raised some interesting questions that need feedback.
>>>
>>> The main ideas behind this prototype are 1) to be able to "switch"
>>> between various versions of Coq, without having to
>>> recompile/reinstall/handle symlinks by hand in any way; 2) to have a
>>> unified way to find out what packages (that is, libraries, plugins,
>>> fancy developments) are available for a given version of Coq; 3) to
>>> get this prototype working with as little work as possible.
>>>
>>> My solution to 1), 2) and 3) was to hack opam, the OCaml package
>>> manager, to use it to handle Coq installations rather than OCaml
>>> installations. Many thanks to ocamlpro for the brilliant tool that
>>> opam is.
>>>
>>> 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. I do not know of packages that require camlp4
>>>   specifically. Is there a good reason to handle both, or should
>>>   camlp5 be mandatory?
>>>
>>> * Build systems
>>>   All packages I know of either use hand-written makefiles, or
>>>   coq_makefile generated one. Do you use something fancier?
>>>
>>> * Installation of packages
>>>   Some packages are meant to be installed "locally". That is, they ask
>>>   the user to add a few cryptic commands to files, like:
>>>
>>>   Add Rec LoadPath "<dir>" as FooBar.
>>>
>>>   The problem with that is that it makes for non-portable
>>>   developments. It seems a rather fragile way to mark dependencies on
>>>   packages, and prone to break if one distribute files: there is no
>>>   reason that the <dir> path I use will be valid on someone else's
>>>   computer.
>>>
>>>   Then, coq_makefile generates Makefiles with an "install target" that
>>>   copy required files (plugins and .vo) to coq/user-contrib/foobar/
>>>   (where foobar is the name of the package). This seems portable,
>>>   since coqtop will look there upon "Require".
>>>
>>>   Is there any reason not to make this mandatory for packages? It
>>>   would make for an easy uninstall procedure, since it suffices to
>>>   remove the foobar directory to remove the foobar package. (I am not
>>>   speaking of dependencies between packages here, because this is
>>>   nicely handled by the prototype).
>>>
>>> * Coq contribs, and packages in the wild
>>>   Coq contributions housed at http://coq.inria.fr/pylons/contribs made
>>>   for a mixed experience when I tried to package some of them. Some
>>>   work out of the box, once you figure what are the INSTALL steps.
>>>   Some are harder to handle. For instance, the ergo contrib has its
>>>   dependencies over other contribs built in its makefile, which
>>>   requires some work (it is not an "out-of-the-box" experience).
>>>
>>>   Then, there are some outstanding works that are not present there at
>>>   all, or that are old versions of things. I spent some time trying to
>>>   find out packages in the wild, but this is a place where help is
>>>   needed. If you have a package, and you think it could be cool to add
>>>   it to this prototype package manager, please, send me an email.
>>>
>>> * (Simplifying) design decisions.
>>>   First, if you would be happy with recompiling everything
>>>   anytime you switch from compilers to compilers, there is no need for
>>>   a dedicated package manager, you can use opam readily for that, with
>>>   the right list of packages. Yet, I really think that we want some
>>>   "persistent" coq switches: switching from coq vA to coq vB makes it
>>>   possible to install packages for vB, and come back to your coq vA
>>>   installation without having to recompile coq vA. (Personally, I used
>>>   to think that I would only ever use the latest Coq version, but it
>>>   is not the case anymore: sometimes, I use trunk, sometimes I use Coq
>>>   patched with mtac, sometimes, I use 8.4pl2 and so on.) So am I right
>>>   that we (the coq community) want some persistent switches?
>>>
>>>   Second, changing the underlying OCaml version will force the user to
>>>   recompile his Coq installations and packages. There may be a spot
>>>   for discussion here, because I think that vo's magic number depends
>>>   on the ocaml version, which may be too stringent. Yet, it is no big
>>>   deal, is it?
>>>
>>>   Third, after discussion with OCamlPro people, it seems that it could
>>>   be possible to enhance opam to be our Coq package manager (Coq
>>>   packages would get a special treatment). Would people be happy with
>>>   that kind of workflow? Or would you rather have a separate package
>>>   manager, maybe a fork of opam (which is what my prototype is)?
>>>
>>> * compilers and packages.
>>>   So far, my list of packages and compilers are as follows.
>>>
>>>   aac_tactics.0.4  containers.2010  ergo.2010        mathcomp.1.5
>>>   color.09.09.2013 counting.2010    flocq.2.2.0      ssreflect.1.5
>>>   compcert.2.0     cybelle.1.2      interval.0.16.1
>>>
>>>   8.4.dev 8.4.pl1-mtac 8.4.pl2-mtac 8.4.pl2 trunk
>>>
>>>   If you have a package/a coq version that you would like to see on
>>>   this list, please let me know privately. Note that this list is the
>>>   product of a random process, and that some packages (some of my own
>>> even)
>>>   are not part of it yet. I think we really need to be
>>>   "consumer-driven" here [1].
>>>
>>>   (There might be a naming issue, because some packages are not
>>>   versioned officialy, and/or I mangled names. I think it is
>>>   not really important at this point, isn't it?)
>>>
>>> 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.
>>>
>>> Thomas
>>>
>>> [1] For instance, on my todo list are the various libraries about
>>> separation logic
>>> that I know of.
>>> [2] Even if my spare time is a dwindling quantity recently.
>>>
>>>
>>>
>>
>