Home Explore Blog CI



nixpkgs

4th chunk of `doc/languages-frameworks/coq.section.md`
dc39cf30d9f562eb81bfef8ff52b38bf4d5fd99a2cae58bd0000000100000aa5
* `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
{
  lib,
  mkCoqDerivation,
  version ? null,
  coq,
  mathcomp,
  mathcomp-finmap,
  mathcomp-bigenough,
}:

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 lib.versions;
    lib.switch
      [ coq.version mathcomp.version ]
      [
        {
          cases = [
            (range "8.7" "8.12")
            (isEq "1.11")
          ];
          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 = [
            (isEq "8.6")
            (range "1.6" "1.7")
          ];
          out = "1.1";
        }
      ]
      null;
  release = {
    "1.5.2".hash = "sha256-mjCx9XKa38Nz9E6wNK7YSqHdJ7YTua5fD3d6J4e7WpU=";
    "1.5.1".hash = "sha256-Q8tm0y2FQAt2V1kZYkDlHWRia/lTvXAMVjdmzEV11I4=";
    "1.5.0".hash = "sha256-HIK0f21G69oEW8JG46gSBde/Q2LR3GiBCv680gHbmRg=";
    "1.5.0".rev = "1.5";
    "1.4".hash = "sha256-F9g3MSIr3B6UZ3p8QWjz3/Jpw9sudJ+KRlvjiHSO024=";
    "1.3".hash = "sha256-BPJTlAL0ETHvLMBslE0KFVt3DNoaGuMrHt2SBGyJe1A=";
    "1.2".hash = "sha256-mHXBXSLYO4BN+jfN50y/+XCx0Qq5g4Ac2Y/qlsbgAdY=";

Title: Advanced Coq Package Configuration and Example
Summary
This section covers advanced Coq package configurations, including using `useMelquiondRemake` for libraries using Guillaume Melquiond's `remake` system, tuning attributes with `dropAttrs`, `keepAttrs`, and `dropDerivationAttrs`, and leveraging standard `mkDerivation` attributes. It then presents a detailed example of a pure Coq library that depends on Coq and the Mathematical Components library, showcasing how to define version-specific attributes, hashes, and revisions using `mkCoqDerivation`.