Skip to content
This repository has been archived by the owner on Oct 11, 2018. It is now read-only.

Home

Jump to bottom
Thomas Braibant edited this page Dec 4, 2013 · 5 revisions

Basic requirements for Coq packages

For now, all Coq packages must have an install target, that copies .vo files and cmo/cmxs files in Coq's user-contrib directory.

Using suitable invocations for coq_makefile (in particular, using the right -R parameters), each library will be copied in a different sub-directory of `$coq/user-contribs

I do not want to use coq_makefile, how do I know the location of user-contribs

The location of this directory can be found doing coqtop -where. For instance, on my machine, I get

$ coqtop -where
/home/braibant/.opam/system--coq.8.4.2/lib/coq

(Note that I must catenate the /user-contrib part myself)

Where does opam build the packages?

It uses a subdirectory of `$opam/$switch/build/. But this is a temporary build location, and you should not rely on this information, e.g., to decide where to copy your files.

My library contains examples (.v files). What should I do?

Good question. My opinion right now is that you should copy these .v files in a subdirectory of $opam/$switch/$lib. To know more about this, please refer to the documentation of opam config --help to know more about OPAM's configuration variables or send me a mail.

I do not want to create/maintain the package myself, what should I do?

  1. Please, put a tarball of your code somewhere that correspond to a tagged release of your library. Version numbers are neat tags (e.g. foobar.1.2.2.tar.gz). Date of release are kind of ok as tags (e.g. foobar.20131206.tar.gz). Strings are bad (e.g. foobar.stable.tar.gz).
  2. Please make sure that these tarball are persistent (for instance, that new versions of your library will not erase older ones).
  3. Please make sure that you have at least an install target that meets the aforementioned requirements
  4. Then, either send me an email, or open an issue.

Ideas

I think there could be some value in "meta-packages" that install together a given version of Coq, a version of CoqIde, and some packages (e.g., ssreflect). Each university, or each course could have its own meta-package, making installing Coq a breeze for students.

Clone this wiki locally