-
-
Notifications
You must be signed in to change notification settings - Fork 14.9k
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
2fe7c5c
commit 90b7ca2
Showing
54 changed files
with
1,364 additions
and
2,250 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,40 +1,77 @@ | ||
| # Coq {#sec-language-coq} | ||
| # Coq and coq packages {#sec-language-coq} | ||
|
|
||
| Coq libraries should be installed in `$(out)/lib/coq/${coq.coq-version}/user-contrib/`. Such directories are automatically added to the `$COQPATH` environment variable by the hook defined in the Coq derivation. | ||
| ## Coq derivation: `coq` | ||
|
|
||
| Some extensions (plugins) might require OCaml and sometimes other OCaml packages. The `coq.ocamlPackages` attribute can be used to depend on the same package set Coq was built against. | ||
| The Coq derivation is overridable through the `coq.override overrides`, where overrides is an attribute set which contains the arguments to override. We recommend overriding either of the following | ||
| + `version` (optional, defaults to the latest version of Coq selected for nixpkgs, see `pkgs/top-level/coq-packages` to witness this choice), which follows the conventions explained in the `coqPackages` section below, | ||
| + `customOCamlPackage` (optional, defaults to `null`, which lets Coq choose a version automatically), which can be set to any of the ocaml packages attribute of `ocaml-ng` (such as `ocaml-ng.ocamlPackages_4_10` which is the default for Coq 8.11 for example). | ||
| + `coq-version` (optional, defaults to the short version e.g. "8.10"), is a version number of the form "x.y" that indicates which Coq's version build behavior to mimic when using a source which is not a release. E.g. `coq.override { version = "d370a9d1328a4e1cdb9d02ee032f605a9d94ec7a"; coq-version = "8.10"; }`. | ||
|
|
||
| Coq libraries may be compatible with some specific versions of Coq only. The `compatibleCoqVersions` attribute is used to precisely select those versions of Coq that are compatible with this derivation. | ||
| ## Coq packages attribute sets: `coqPackages` | ||
|
|
||
| Here is a simple package example. It is a pure Coq library, thus it depends on Coq. It builds on the Mathematical Components library, thus it also takes `mathcomp` as `buildInputs`. Its `Makefile` has been generated using `coq_makefile` so we only have to set the `$COQLIB` variable at install time. | ||
| The recommended way of defining a derivation for a Coq library, is to use the `coqPackages.mkCoqDerivation` function, which is essentially a specialization of `mkDerivation` taking into account most of the specifics of Coq libraries. The following attributes are supported: | ||
| - `pname` (required) is the name of the package, | ||
| - `version` (optional, defaults to `null`), is the version to fetch and build, | ||
| this attribute is interpreted in several ways depending on its type and pattern: | ||
| + if it is a known released version string, i.e. from the `release` attribute below, the according release is picked, and the `version` attribute of the resulting derivation is set to this release string, | ||
| + if it is a majorMinor `"x.y"` prefix of a known released version (as defined above), then the latest `"x.y.z"` known released version is selected (for the ordering given by `versionAtLeast`), | ||
| + if it is a path or a string representing an absolute path (i.e. starting with `"/"`), the provided path is selected as a source, and the `version` attribute of the resulting derivation is set to `"dev"`, | ||
| + if it is a string of the form `owner:branch` then it tries to download the `branch` of owner `owner` for a project of the same name using the same vcs, and the `version` attribute of the resulting derivation is set to `"dev"`, additionally if the owner is not provided (i.e. if the `owner:` prefix is missing), it defaults to the original owner of the package (see below), | ||
| + if it is a string of the form `"#N"`, and the domain is github, then it tries to download the current head of the pull request `#N` from github, | ||
| - `defaultVersion` (optional). Coq libraries may be compatible with some specific versions of Coq only. The `defaultVersion` attribute is used when no `version` is provided (or if `version = null`) to select the version of the library to use by default, depending on the context. This selection will mainly depend on a `coq` version number but also possibly on other packages versions (e.g. `mathcomp`). If its value ends up to be `null`, the package is marked for removal in end-user `coqPackages` attribute set. | ||
| - `release` (optional, defaults to `{}`), lists all the known releases of the library and for each of them provides an attribute set with at least a `sha256` attribute (you may use the shell command `nix-prefetch-url --unpack <archive-url>` to find it, where `<archive-url>` is for example `https://github.com/owner/repo/archive/version.tar.gz`), each attribute set of the list of releases also takes optional overloading arguments for the fetcher as below (i.e.`domain`, `owner`, `repo`, `rev` assuming the default fetcher is used) and optional overrides for the result of the fetcher (i.e. `version` and `src`). | ||
| - `fetcher` (optional, default to a generic fetching mechanism supporting github or gitlab based infrastructures), is a function that takes at least an `owner`, a `repo`, a `rev`, and a `sha256` and returns an attribute set with a `version` and `src`. | ||
| - `repo` (optional, defaults to the value of `pname`), | ||
| - `owner` (optional, defaults to `"coq-community"`). | ||
| - `domain` (optional, defaults to `"github.com"`), domains including the strings `"github"` or `"gitlab"` in their names are automatically supported, otherwise, one must change the `fetcher` argument to support them (cf `pkgs/development/coq-modules/heq/default.nix` for an example), | ||
| - `releaseRev` (optional, defaults to `(v: v)`), provides a default mapping from release names to revision hashes/branch names/tags, | ||
| - `displayVersion` (optional), provides a way to alter the computation of `name` from `pname`, by explaining how to display version numbers, | ||
| - `namePrefix` (optional), provides a way to alter the computation of `name` from `pname`, by explaining which dependencies must occur in `name`, | ||
| - `extraBuildInputs` (optional), by default `buildInputs` just contains `coq`, this allows to add more build inputs, | ||
| - `mlPlugin` (optional, defaults to `false`). Some extensions (plugins) might require OCaml and sometimes other OCaml packages. Standard dependencies can be added by setting the current option to `true`. For a finer grain control, the `coq.ocamlPackages` attribute can be used in `extraBuildInputs` to depend on the same package set Coq was built against. | ||
| - `enableParallelBuilding` (optional, defaults to `true`), since it is activated by default, we provide a way to disable it. | ||
| - `extraInstallFlags` (optional), allows to extend `installFlags` which initializes the variable `COQMF_COQLIB` so as to install in the proper subdirectory. Indeed Coq libraries should be installed in `$(out)/lib/coq/${coq.coq-version}/user-contrib/`. Such directories are automatically added to the `$COQPATH` environment variable by the hook defined in the Coq derivation. | ||
| - `setCOQBIN` (optional, defaults to `true`), by default, the environment variable `$COQBIN` is set to the current Coq's binary, but one can disable this behavior by setting it to `false`, | ||
| - `useMelquiondRemake` (optional, default to `null`) is an attribute set, which, if given, overloads the `preConfigurePhases`, `configureFlags`, `buildPhase`, and `installPhase` attributes of the derivation for a specific use in libraries using `remake` as set up by Guillaume Melquiond for `flocq`, `gappalib`, `interval`, and `coquelicot` (see the corresponding derivation for concrete examples of use of this option). For backward compatibility, the attribute `useMelquiondRemake.logpath` must be set to the logical root of the library (otherwise, one can pass `useMelquiondRemake = {}` to activate this without backward compatibility). | ||
| - `dropAttrs`, `keepAttrs`, `dropDerivationAttrs` are all optional and allow to tune which attribute is added or removed from the final call to `mkDerivation`. | ||
|
|
||
| It also takes other standard `mkDerivation` attributes, they are added as such, except for `meta` which extends an automatically computed `meta` (where the `platform` is the same as `coq` and the homepage is automatically computed). | ||
|
|
||
| Here is a simple package example. It is a pure Coq library, thus it depends on Coq. It builds on the Mathematical Components library, thus it also takes some `mathcomp` derivations as `extraBuildInputs`. | ||
|
|
||
| ```nix | ||
| { stdenv, fetchFromGitHub, coq, mathcomp }: | ||
| stdenv.mkDerivation rec { | ||
| name = "coq${coq.coq-version}-multinomials-${version}"; | ||
| version = "1.0"; | ||
| src = fetchFromGitHub { | ||
| owner = "math-comp"; | ||
| repo = "multinomials"; | ||
| rev = version; | ||
| sha256 = "1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m"; | ||
| { coq, mkCoqDerivation, mathcomp, mathcomp-finmap, mathcomp-bigenough, | ||
| lib, version ? null }: | ||
| with lib; mkCoqDerivation { | ||
| /* namePrefix leads to e.g. `name = coq8.11-mathcomp1.11-multinomials-1.5.2` */ | ||
| namePrefix = [ "coq" "mathcomp" ]; | ||
| pname = "multinomials"; | ||
| owner = "math-comp"; | ||
| inherit version; | ||
| defaultVersion = with versions; switch [ coq.version mathcomp.version ] [ | ||
| { cases = [ (range "8.7" "8.12") "1.11.0" ]; out = "1.5.2"; } | ||
| { cases = [ (range "8.7" "8.11") (range "1.8" "1.10") ]; out = "1.5.0"; } | ||
| { cases = [ (range "8.7" "8.10") (range "1.8" "1.10") ]; out = "1.4"; } | ||
| { cases = [ "8.6" (range "1.6" "1.7") ]; out = "1.1"; } | ||
| ] null; | ||
| release = { | ||
| "1.5.2".sha256 = "15aspf3jfykp1xgsxf8knqkxv8aav2p39c2fyirw7pwsfbsv2c4s"; | ||
| "1.5.1".sha256 = "13nlfm2wqripaq671gakz5mn4r0xwm0646araxv0nh455p9ndjs3"; | ||
| "1.5.0".sha256 = "064rvc0x5g7y1a0nip6ic91vzmq52alf6in2bc2dmss6dmzv90hw"; | ||
| "1.5.0".rev = "1.5"; | ||
| "1.4".sha256 = "0vnkirs8iqsv8s59yx1fvg1nkwnzydl42z3scya1xp1b48qkgn0p"; | ||
| "1.3".sha256 = "0l3vi5n094nx3qmy66hsv867fnqm196r8v605kpk24gl0aa57wh4"; | ||
| "1.2".sha256 = "1mh1w339dslgv4f810xr1b8v2w7rpx6fgk9pz96q0fyq49fw2xcq"; | ||
| "1.1".sha256 = "1q8alsm89wkc0lhcvxlyn0pd8rbl2nnxg81zyrabpz610qqjqc3s"; | ||
| "1.0".sha256 = "1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m"; | ||
| }; | ||
| buildInputs = [ coq ]; | ||
| propagatedBuildInputs = [ mathcomp ]; | ||
| installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/"; | ||
| propagatedBuildInputs = | ||
| [ mathcomp.ssreflect mathcomp.algebra mathcomp-finmap mathcomp-bigenough ]; | ||
| meta = { | ||
| description = "A Coq/SSReflect Library for Monoidal Rings and Multinomials"; | ||
| inherit (src.meta) homepage; | ||
| license = stdenv.lib.licenses.cecill-b; | ||
| inherit (coq.meta) platforms; | ||
| }; | ||
| passthru = { | ||
| compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" ]; | ||
| license = licenses.cecill-c; | ||
| }; | ||
| } | ||
| ``` |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.