The Coq mailing list

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

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.