The Coq mailing list

[Gregory Malecha <gmalecha AT cs.harvard.edu>]

Hi, Thomas --

I think this would be great! (I've considered building such a system for a little while now, but never got around to it). I would like to add two things:

1) Is it possible to change the vo format to be indpendent of the coq version (where feasible)? Something like storing the ASTs as protocol buffers seems like it would work and alleviate some of the problems. Also note that, depending on the format, it might be possible to have packages compiled with an older version of Coq included in your development allowing you to avoid porting them.

I would be happy to work on this if someone would point me in the right direction, I've dug through the coq sources but never found the right place for this.

2) In my experience the recursive load feature is convenient but a little bit loose and makes some things difficult. For example, I've been working on consolidating a bunch of things that I find myself writing over and over again in coq-ext-lib (https://github.com/coq-ext-lib/coq-ext-lib) and it has files named, e.g. List, for type class instances and such related to lists. But this clashes with the standard library's List. I include it with "-R ... -as ExtLib" but I feel like sometimes it doesn't work the way I anticipate and have to write "Import Coq.Lists.List" in order to get List from the standard library.

While not directly related to a package manager, I feel like pulling in a lot of packages could exasperate this problem. As with before, I wouldn't mind doing some development if other people have experienced issues like this.

On Sat, Oct 12, 2013 at 5: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.
 

--

gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/