All opam repositories for Coq packages live here. Packages are organized according to the layout.
To activate the repositories:
-
all the released packages (recommended default):
opam repo add coq-released https://coq.inria.fr/opam/released
We welcome pull requests for all Coq-related packages that are compatible with a released version of Coq. Besides libraries of general interest, this also includes paper artifacts and other specialized formalizations that are not necessarily expected to be immediately reusable by others.
-
development versions:
opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
-
development versions of Coq:
opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev
To add new packages, look at this documentation. You can also look at existing pull requests to see how others are adding packages.
The scripts/archive2web.ml
program generates a JSON file
coq-packages.json
by looking at the opam
files.
In particular, it uses the tags
field of an opam
file as follows:
- strings beginning with
keyword:
are considered askeywords
- strings beginning with
category:
are considered ascategories
- a string beginning with
date:
is the date the software was last updated (not the package) - a string beginning with
logpath:
is considered the Coq logical path prefix
Example:
tags: [
"keyword:cool"
"keyword:stuff"
"category:Some/Category"
"date:1992-12-22"
"logpath:SomePrefix"
]
The homepage:
, author:
, maintainer:
, and doc:
fields are
also used to generate the package entry.
This JSON file is generated during continuous integration and copied to the website. Some JavaScript code on the website then loads it to dynamically generate the content of the webpage on client side.
See also CEP3 and the deployed website.
Incoming pull requests are tested on GitLab CI. @coqbot pushes any opened
or synchonized pull request to a branch named pr-<number>
on GitLab. It will
trigger a CI build. If the CI build runs for too long and times out, any
member of the Coq organization of GitLab can start it again using the "Run
Pipeline" green button at https://gitlab.com/coq/opam-coq-archive/pipelines.
This will then build only on runners without pre-set timeouts (the Coq Pyrolyse
server). It may still time out if the build takes longer than the GitLab
project's timeout setting (24 hours). To skip some packages the first PR
message can contain a line such as ci-skip: p1.v1 p2.v2
where p1
and p2
are package names, and v1
and v2
are versions.