mirror of
https://github.com/NixOS/nixpkgs.git
synced 2026-08-25 17:55:21 +00:00
Merge coq-modules and rocq-modules derivations (#541797)
This commit is contained in:
Vincent Laporte
20
.github/labeler.yml
vendored
20
.github/labeler.yml
vendored
@@ -43,14 +43,6 @@
|
||||
- .github/**/*
|
||||
- ci/**/*.*
|
||||
|
||||
"6.topic: coq":
|
||||
- any:
|
||||
- changed-files:
|
||||
- any-glob-to-any-file:
|
||||
- pkgs/applications/science/logic/coq/**/*
|
||||
- pkgs/development/coq-modules/**/*
|
||||
- pkgs/top-level/coq-packages.nix
|
||||
|
||||
"6.topic: COSMIC":
|
||||
- any:
|
||||
- changed-files:
|
||||
@@ -466,6 +458,18 @@
|
||||
- any-glob-to-any-file:
|
||||
- pkgs/development/rocm-modules/**/*
|
||||
|
||||
"6.topic: rocq":
|
||||
- any:
|
||||
- changed-files:
|
||||
- any-glob-to-any-file:
|
||||
- pkgs/applications/science/logic/coq/**/*
|
||||
- pkgs/applications/science/logic/rocq-core/**/*
|
||||
- pkgs/build-support/coq/**/*
|
||||
- pkgs/build-support/rocq/**/*
|
||||
- pkgs/development/rocq-modules/**/*
|
||||
- pkgs/top-level/coq-packages.nix
|
||||
- pkgs/top-level/rocq-packages.nix
|
||||
|
||||
"6.topic: ruby":
|
||||
- any:
|
||||
- changed-files:
|
||||
|
||||
@@ -3,11 +3,12 @@
|
||||
Note that "The Rocq Prover" (Rocq for short) is the new name of the
|
||||
proof assistant formerly known as Coq. The `coq` and `coqPackages`
|
||||
derivations currently remain for both older versions of Coq, but also
|
||||
some versions of Rocq during the renaming transition. In the latter
|
||||
case, the `coq` derivation encompasses the compatibility binaries
|
||||
(`coqtop`, `coqc`, etc.) in addition to the `rocq` binary. The packages
|
||||
only in `coqPackages` are the ones which currently still depend on these
|
||||
compatibility binaries.
|
||||
as compatibility aliases for some versions of Rocq. In both cases, the
|
||||
`coq` and `rocq-core` attributes exist. In the case of Coq (< 9),
|
||||
`rocq-core` is just an alias for `coq`, while in the case of Rocq (>= 9),
|
||||
`rocq-core` is the main Rocq derivation, while `coq` provides
|
||||
compatibility binaries (`coqc`, `coqtop`, etc.) for packages that still
|
||||
depend on them.
|
||||
|
||||
## Rocq derivation: `rocq-core` {#rocq-derivation-rocq}
|
||||
|
||||
@@ -17,18 +18,18 @@ The Rocq derivation is overridable through the `rocq-core.override overrides`, w
|
||||
* `customOCamlPackages` (optional, defaults to `null`, which lets Rocq choose a version automatically), which can be set to any of the ocaml packages attribute of `ocaml-ng` (such as `ocaml-ng.ocamlPackages_4_14` which is the default for Rocq 9.1 for example).
|
||||
* `rocq-version` (optional, defaults to the short version e.g. "9.1"), is a version number of the form "x.y" that indicates which Rocq's version build behavior to mimic when using a source which is not a release. E.g. `rocq-core.override { version = "40be8435e132aab2231a79091f011ebc3e64a753"; rocq-version = "9.1"; }`.
|
||||
|
||||
## Creating custom Coq environments with `coq.withPackages` {#coq-withPackages}
|
||||
## Creating custom Coq environments with `rocq-core.withPackages` {#coq-withPackages}
|
||||
|
||||
The `coq.withPackages` function provides a convenient way to create a Coq environment that includes additional Coq packages. This is similar to how `python.withPackages` works for Python environments.
|
||||
The `rocq-core.withPackages` function provides a convenient way to create a Rocq environment that includes additional Rocq packages. This is similar to how `python.withPackages` works for Python environments.
|
||||
|
||||
The function takes a function that receives the Coq package set and returns a list of packages. It returns a wrapped Coq environment where all Coq binaries (`coqtop`, `coqc`, `coqdep`, `coqchk`, `coqide`, etc.) are configured with the appropriate environment variables to find the packages.
|
||||
The function takes a function that receives the Rocq package set and returns a list of packages. It returns a wrapped Rocq environment where the Rocq binaries (`rocq`, etc.) are configured with the appropriate environment variables to find the packages.
|
||||
|
||||
### Usage {#coq-withPackages-usage}
|
||||
|
||||
Here is an example of creating a Coq environment with specific packages.
|
||||
Here is an example of creating a Rocq environment with specific packages.
|
||||
|
||||
```nix
|
||||
coq.withPackages (
|
||||
rocq-core.withPackages (
|
||||
ps: with ps; [
|
||||
mathcomp
|
||||
bignums
|
||||
@@ -36,7 +37,9 @@ coq.withPackages (
|
||||
)
|
||||
```
|
||||
|
||||
If you install the `vsrocq-language-server` or `rocq-lsp` server, make sure to list them as part of the above `coq.withPackages` expression instead of installing them separately if you want them to find your Coq/Rocq packages.
|
||||
If you install the `vsrocq-language-server` or `rocq-lsp` server, make sure to list them as part of the above `rocq-core.withPackages` expression instead of installing them separately if you want them to find your Rocq packages.
|
||||
|
||||
For versions prior to Rocq 9.0, a similar `coq.withPackages` function is available.
|
||||
|
||||
## Rocq packages attribute sets: `rocqPackages` {#rocq-packages-attribute-sets-rocqpackages}
|
||||
|
||||
@@ -130,7 +133,7 @@ mkRocqDerivation {
|
||||
mathcomp.boot
|
||||
mathcomp.algebra
|
||||
mathcomp-finmap
|
||||
mathcomp.fingroup
|
||||
mathcomp.finite-group
|
||||
mathcomp-bigenough
|
||||
];
|
||||
|
||||
|
||||
@@ -100,6 +100,7 @@ let
|
||||
version = fetched.version;
|
||||
coq-version =
|
||||
args.coq-version or (if version != "dev" then lib.versions.majorMinor version else "dev");
|
||||
rocq-version = coq-version;
|
||||
coqAtLeast = v: coq-version == "dev" || lib.versionAtLeast coq-version v;
|
||||
buildIde = args.buildIde or (coqAtLeast "8.10" && !coqAtLeast "8.14");
|
||||
csdpPatch = lib.optionalString (csdp != null) ''
|
||||
@@ -161,6 +162,7 @@ let
|
||||
|
||||
passthru = {
|
||||
inherit coq-version;
|
||||
inherit rocq-version;
|
||||
inherit ocamlPackages ocamlNativeBuildInputs;
|
||||
inherit ocamlPropagatedBuildInputs;
|
||||
# For compatibility
|
||||
|
||||
@@ -11,7 +11,8 @@ packages:
|
||||
let
|
||||
# At version 9.0, Coq underwent a name change to Rocq.
|
||||
# A couple paths and environment variables need to change at this point.
|
||||
isRocq = lib.versionAtLeast coq.coq-version "9.0";
|
||||
isRocq = coq ? rocq-version && lib.versionAtLeast coq.rocq-version "9.0";
|
||||
rocq-version = if isRocq then coq.rocq-version else coq.coq-version;
|
||||
|
||||
collectPropagated =
|
||||
pkg:
|
||||
@@ -21,9 +22,9 @@ let
|
||||
|
||||
allPackages = lib.unique (lib.concatMap collectPropagated packages);
|
||||
|
||||
coqPath = lib.makeSearchPath "/lib/coq/${coq.coq-version}/user-contrib" allPackages;
|
||||
coqPath = lib.makeSearchPath "/lib/coq/${rocq-version}/user-contrib" allPackages;
|
||||
|
||||
ocamlPath = lib.makeSearchPath "/lib/ocaml/${coq.ocaml.version}/site-lib" (
|
||||
ocamlPath = lib.makeSearchPath "/lib/ocaml/${coq.ocamlPackages.ocaml.version}/site-lib" (
|
||||
[ coq.ocamlPackages.findlib ] ++ allPackages
|
||||
);
|
||||
|
||||
|
||||
@@ -213,6 +213,12 @@ stdenv.mkDerivation (
|
||||
}
|
||||
// (args.env or { });
|
||||
|
||||
preBuild =
|
||||
optionalString (useCoq && useDune && lib.versionAtLeast rocq-core.rocq-version "9.0") ''
|
||||
export COQPATH="$ROCQPATH"
|
||||
''
|
||||
+ (args.preBuild or "");
|
||||
|
||||
meta =
|
||||
(
|
||||
{
|
||||
|
||||
@@ -1,63 +0,0 @@
|
||||
{
|
||||
lib,
|
||||
mkCoqDerivation,
|
||||
coq,
|
||||
stdlib,
|
||||
version ? null,
|
||||
}:
|
||||
|
||||
let
|
||||
derivation = mkCoqDerivation {
|
||||
pname = "bignums";
|
||||
owner = "rocq-community";
|
||||
inherit version;
|
||||
defaultVersion =
|
||||
let
|
||||
case = case: out: { inherit case out; };
|
||||
in
|
||||
with lib.versions;
|
||||
lib.switch coq.coq-version [
|
||||
(case (range "8.13" "8.20") "9.0.0+coq${coq.coq-version}")
|
||||
(case (range "8.6" "8.17") "${coq.coq-version}.0")
|
||||
] null;
|
||||
|
||||
release."9.0.0+coq8.20".hash = "sha256-pkvyDaMXRalc6Uu1eBTuiqTpRauRrzu946c6TavyTKY=";
|
||||
release."9.0.0+coq8.19".hash = "sha256-02uL+qWbUveHe67zKfc8w3U0iN3X2DKBsvP3pKpW8KQ=";
|
||||
release."9.0.0+coq8.18".hash = "sha256-vLeJ0GNKl4M84Uj2tAwlrxJOSR6VZoJQvdlDhxJRge8=";
|
||||
release."9.0.0+coq8.17".hash = "sha256-Mn85LqxJKPDIfpxRef9Uh5POwOKlTQ7jsMVz1wnQwuY=";
|
||||
release."9.0.0+coq8.16".hash = "sha256-pwFTl4Unr2ZIirAB3HTtfhL2YN7G/Pg88RX9AhKWXbE=";
|
||||
release."9.0.0+coq8.15".hash = "sha256-2oGOANn3XULHNIlyqjZ5ppQTQa2QF1zzf3YjHAd/pjo=";
|
||||
release."9.0.0+coq8.14".hash = "sha256-qTU152Dz34W6nFZ0pPbja9ouUm/714ZrLQ/Z4N/HIC4=";
|
||||
release."9.0.0+coq8.13".hash = "sha256-zvAqV3VAB7cN+nlMhjSXzxuDkdd387ju2VSb2EUthI0=";
|
||||
release."8.17.0".hash = "sha256-MXYjqN86+3O4hT2ql62U83T5H03E/8ysH8erpvC/oyw=";
|
||||
release."8.16.0".hash = "sha256-DH3iWwatPlhhCVYVlgL2WLkvneSVzSXUiKo2e0+1zR4=";
|
||||
release."8.15.0".hash = "sha256:093klwlhclgyrba1iv18dyz1qp5f0lwiaa7y0qwvgmai8rll5fns";
|
||||
release."8.14.0".hash = "sha256:0jsgdvj0ddhkls32krprp34r64y1rb5mwxl34fgaxk2k4664yq06";
|
||||
release."8.13.0".hash = "sha256:1n66i7hd9222b2ks606mak7m4f0dgy02xgygjskmmav6h7g2sx7y";
|
||||
release."8.12.0".hash = "sha256:14ijb3qy2hin3g4djx437jmnswxxq7lkfh3dwh9qvrds9a015yg8";
|
||||
release."8.11.0".hash = "sha256:1xcd7c7qlvs0narfba6px34zq0mz8rffnhxw0kzhhg6i4iw115dp";
|
||||
release."8.10.0".hash = "sha256:0bpb4flckn4nqxbs3wjiznyx1k7r8k93qdigp3qwmikp2lxvcbw5";
|
||||
release."8.9.0".hash = "sha256:03qz1w2xb2j5p06liz5yyafl0fl9vprcqm6j0iwi7rxwghl00p01";
|
||||
release."8.8.0".hash = "sha256:1ymxyrvjygscxkfj3qkq66skl3vdjhb670rzvsvgmwrjkrakjnfg";
|
||||
release."8.7.0".hash = "sha256:11c4sdmpd3l6jjl4v6k213z9fhrmmm1xnly3zmzam1wrrdif4ghl";
|
||||
release."8.6.0".rev = "v8.6.0";
|
||||
release."8.6.0".hash = "sha256:0553pcsy21cyhmns6k9qggzb67az8kl31d0lwlnz08bsqswigzrj";
|
||||
releaseRev = v: "${if lib.versions.isGe "9.0" v then "v" else "V"}${v}";
|
||||
|
||||
mlPlugin = true;
|
||||
|
||||
propagatedBuildInputs = [ stdlib ];
|
||||
|
||||
meta = {
|
||||
license = lib.licenses.lgpl2;
|
||||
};
|
||||
};
|
||||
in
|
||||
# this is just a wrapper for rocqPackages.bignums for Rocq >= 9.0
|
||||
if coq.rocqPackages ? bignums then
|
||||
coq.rocqPackages.bignums.override {
|
||||
inherit version stdlib;
|
||||
inherit (coq.rocqPackages) rocq-core;
|
||||
}
|
||||
else
|
||||
derivation
|
||||
@@ -1,84 +0,0 @@
|
||||
{
|
||||
lib,
|
||||
mkCoqDerivation,
|
||||
coq,
|
||||
stdlib,
|
||||
coq-elpi,
|
||||
version ? null,
|
||||
}:
|
||||
|
||||
let
|
||||
hb = mkCoqDerivation {
|
||||
pname = "hierarchy-builder";
|
||||
owner = "math-comp";
|
||||
inherit version;
|
||||
defaultVersion =
|
||||
let
|
||||
case = case: out: { inherit case out; };
|
||||
in
|
||||
with lib.versions;
|
||||
lib.switch coq.coq-version [
|
||||
(case (range "8.20" "8.20") "1.9.1")
|
||||
(case (range "8.19" "8.20") "1.8.0")
|
||||
(case (range "8.18" "8.20") "1.7.1")
|
||||
(case (range "8.16" "8.18") "1.6.0")
|
||||
(case (range "8.15" "8.18") "1.5.0")
|
||||
(case (range "8.15" "8.17") "1.4.0")
|
||||
(case (range "8.13" "8.14") "1.2.0")
|
||||
(case (range "8.12" "8.13") "1.1.0")
|
||||
(case (isEq "8.11") "0.10.0")
|
||||
] null;
|
||||
release."1.9.1".hash = "sha256-AiS0ezMyfIYlXnuNsVLz1GlKQZzJX+ilkrKkbo0GrF0=";
|
||||
release."1.8.1".hash = "sha256-Z0WAHDyycqgL+Le/zNfEAoLWzFb7WIL+3G3vEBExlb4=";
|
||||
release."1.8.0".hash = "sha256-4s/4ZZKj5tiTtSHGIM8Op/Pak4Vp52WVOpd4l9m19fY=";
|
||||
release."1.7.1".hash = "sha256-MCmOzMh/SBTFAoPbbIQ7aqd3hMcSMpAKpiZI7dbRaGs=";
|
||||
release."1.7.0".hash = "sha256-WqSeuJhmqicJgXw/xGjGvbRzfyOK7rmkVRb6tPDTAZg=";
|
||||
release."1.6.0".hash = "sha256-E8s20veOuK96knVQ7rEDSt8VmbtYfPgItD0dTY/mckg=";
|
||||
release."1.5.0".hash = "sha256-Lia3o156Pbe8rDHOA1IniGYsG5/qzZkzDKdHecfmS+c=";
|
||||
release."1.4.0".hash = "sha256-tOed9UU3kMw6KWHJ5LVLUFEmzHx1ImutXQvZ0ldW9rw=";
|
||||
release."1.3.0".hash = "sha256:17k7rlxdx43qda6i1yafpgc64na8br285cb0mbxy5wryafcdrkrc";
|
||||
release."1.2.1".hash = "sha256-pQYZJ34YzvdlRSGLwsrYgPdz3p/l5f+KhJjkYT08Mj0=";
|
||||
release."1.2.0".hash = "sha256:0sk01rvvk652d86aibc8rik2m8iz7jn6mw9hh6xkbxlsvh50719d";
|
||||
release."1.1.0".hash = "sha256-spno5ty4kU4WWiOfzoqbXF8lWlNSlySWcRReR3zE/4Q=";
|
||||
release."1.0.0".hash = "sha256:0yykygs0z6fby6vkiaiv3azy1i9yx4rqg8xdlgkwnf2284hffzpp";
|
||||
release."0.10.0".hash = "sha256:1a3vry9nzavrlrdlq3cys3f8kpq3bz447q8c4c7lh2qal61wb32h";
|
||||
releaseRev = v: "v${v}";
|
||||
|
||||
propagatedBuildInputs = [ coq-elpi ];
|
||||
|
||||
mlPlugin = true;
|
||||
|
||||
meta = {
|
||||
description = "High level commands to declare a hierarchy based on packed classes";
|
||||
maintainers = with lib.maintainers; [
|
||||
cohencyril
|
||||
siraben
|
||||
];
|
||||
license = lib.licenses.mit;
|
||||
};
|
||||
};
|
||||
hb2 = hb.overrideAttrs (
|
||||
o:
|
||||
lib.optionalAttrs (lib.versions.isGe "1.2.0" o.version || o.version == "dev") {
|
||||
buildPhase = "make build";
|
||||
}
|
||||
// (
|
||||
if lib.versions.isGe "1.1.0" o.version || o.version == "dev" then
|
||||
{ installFlags = [ "DESTDIR=$(out)" ] ++ o.installFlags; }
|
||||
else
|
||||
{ installFlags = [ "VFILES=structures.v" ] ++ o.installFlags; }
|
||||
)
|
||||
// lib.optionalAttrs (o.version != null && o.version == "1.8.1") {
|
||||
propagatedBuildInputs = o.propagatedBuildInputs ++ [ stdlib ];
|
||||
}
|
||||
);
|
||||
in
|
||||
# this is just a wrapper for rocqPackages.hierarchy-builder for Rocq >= 9.0
|
||||
if coq.rocqPackages ? hierarchy-builder then
|
||||
coq.rocqPackages.hierarchy-builder.override {
|
||||
inherit version;
|
||||
inherit (coq.rocqPackages) rocq-core;
|
||||
rocq-elpi = coq-elpi;
|
||||
}
|
||||
else
|
||||
hb2
|
||||
@@ -1,65 +0,0 @@
|
||||
{
|
||||
lib,
|
||||
mkCoqDerivation,
|
||||
coq,
|
||||
stdpp,
|
||||
version ? null,
|
||||
}:
|
||||
|
||||
let
|
||||
derivation = mkCoqDerivation {
|
||||
pname = "iris";
|
||||
domain = "gitlab.mpi-sws.org";
|
||||
owner = "iris";
|
||||
inherit version;
|
||||
defaultVersion =
|
||||
let
|
||||
case = case: out: { inherit case out; };
|
||||
in
|
||||
with lib.versions;
|
||||
lib.switch coq.coq-version [
|
||||
(case (range "8.19" "9.1") "4.4.0")
|
||||
(case (range "8.18" "8.19") "4.2.0")
|
||||
(case (range "8.16" "8.18") "4.1.0")
|
||||
(case (range "8.13" "8.17") "4.0.0")
|
||||
(case (range "8.12" "8.14") "3.5.0")
|
||||
(case (range "8.11" "8.13") "3.4.0")
|
||||
(case (range "8.9" "8.10") "3.3.0")
|
||||
] null;
|
||||
release."4.4.0".hash = "sha256-zpuaIdH2ScOuZB0Vt1TEHAbsmcT1DyoDsJpftT1M7qw=";
|
||||
release."4.3.0".hash = "sha256-3qhjiFI+A3I3fD8rFfJL5Hek77wScfn/FNNbDyGqA1k=";
|
||||
release."4.2.0".hash = "sha256-HuiHIe+5letgr1NN1biZZFq0qlWUbFmoVI7Q91+UIfM=";
|
||||
release."4.1.0".hash = "sha256-nTZUeZOXiH7HsfGbMKDE7vGrNVCkbMaWxdMWUcTUNlo=";
|
||||
release."4.0.0".hash = "sha256-Jc9TmgGvkiDaz9IOoExyeryU1E+Q37GN24NIM397/Gg=";
|
||||
release."3.6.0".hash = "sha256:02vbq597fjxd5znzxdb54wfp36412wz2d4yash4q8yddgl1kakmj";
|
||||
release."3.5.0".hash = "sha256:0hh14m0anfcv65rxm982ps2vp95vk9fwrpv4br8bxd9vz0091d70";
|
||||
release."3.4.0".hash = "sha256:0vdc2mdqn5jjd6yz028c0c6blzrvpl0c7apx6xas7ll60136slrb";
|
||||
release."3.3.0".hash = "sha256:0az4gkp5m8sq0p73dlh0r7ckkzhk7zkg5bndw01bdsy5ywj0vilp";
|
||||
releaseRev = v: "iris-${v}";
|
||||
|
||||
propagatedBuildInputs = [ stdpp ];
|
||||
|
||||
preBuild = ''
|
||||
if [[ -f coq-lint.sh ]]
|
||||
then patchShebangs coq-lint.sh
|
||||
fi
|
||||
'';
|
||||
|
||||
meta = {
|
||||
description = "Coq development of the Iris Project";
|
||||
license = lib.licenses.bsd3;
|
||||
maintainers = [
|
||||
lib.maintainers.vbgl
|
||||
lib.maintainers.ineol
|
||||
];
|
||||
};
|
||||
};
|
||||
in
|
||||
# this is just a wrapper for rocqPackages.iris for Rocq >= 9.0
|
||||
if coq.rocqPackages ? iris then
|
||||
coq.rocqPackages.iris.override {
|
||||
inherit version stdpp;
|
||||
inherit (coq.rocqPackages) rocq-core;
|
||||
}
|
||||
else
|
||||
derivation
|
||||
@@ -1,255 +0,0 @@
|
||||
{
|
||||
lib,
|
||||
mkCoqDerivation,
|
||||
mathcomp,
|
||||
mathcomp-finmap,
|
||||
mathcomp-bigenough,
|
||||
hierarchy-builder,
|
||||
stdlib,
|
||||
single ? false,
|
||||
coq,
|
||||
version ? null,
|
||||
}@args:
|
||||
|
||||
let
|
||||
repo = "analysis";
|
||||
owner = "math-comp";
|
||||
|
||||
release."1.14.0".hash = "sha256-FFcfxnF1wtz2e9Rdqu4Wd0rtLW0DYoXswCTji//RSCQ=";
|
||||
release."1.13.0".hash = "sha256-nn2gl6cAO93QEdMvLGlB9WAPddQiOdeRtk1pLO+gxII=";
|
||||
release."1.12.0".hash = "sha256-PF10NlZ+aqP3PX7+UsZwgJT9PEaDwzvrS/ZGzjP64Wo=";
|
||||
release."1.11.0".hash = "sha256-1apbzBvaLNw/8ARLUhGGy89CyXW+/6O4ckdxKPraiVc=";
|
||||
release."1.9.0".hash = "sha256-zj7WSDUg8ISWxcipGpjEwvvnLp1g8nm23BZiib/15+g=";
|
||||
release."1.8.0".hash = "sha256-2ZafDmZAwGB7sxdUwNIE3xvwBRw1kFDk0m5Vz+onWZc=";
|
||||
release."1.7.0".hash = "sha256-GgsMIHqLkWsPm2VyOPeZdOulkN00IoBz++qA6yE9raQ=";
|
||||
release."1.5.0".hash = "sha256-EWogrkr5TC5F9HjQJwO3bl4P8mij8U7thUGJNNI+k88=";
|
||||
release."1.4.0".hash = "sha256-eDggeuEU0fMK7D5FbxvLkbAgpLw5lwL/Rl0eLXAnJeg=";
|
||||
release."1.2.0".hash = "sha256-w6BivDM4dF4Iv4rUTy++2feweNtMAJxgGExPfYGhXxo=";
|
||||
release."1.1.0".hash = "sha256-wl4kZf4mh9zbFfGcqaFEgWRyp0Bj511F505mYodpS6o=";
|
||||
release."1.0.0".hash = "sha256-KiXyaWB4zQ3NuXadq4BSWfoN1cIo1xiLVSN6nW03tC4=";
|
||||
release."0.7.0".hash = "sha256-JwkyetXrFsFHqz8KY3QBpHsrkhmEFnrCGuKztcoen60=";
|
||||
release."0.6.7".hash = "sha256-3i2PBMEwihwgwUmnS0cmrZ8s+aLPFVq/vo0aXMUaUyA=";
|
||||
release."0.6.6".hash = "sha256-tWtv6yeB5/vzwpKZINK9OQ0yQsvD8qu9zVSNHvLMX5Y=";
|
||||
release."0.6.5".hash = "sha256-oJk9/Jl1SWra2aFAXRAVfX7ZUaDfajqdDksYaW8dv8E=";
|
||||
release."0.6.1".hash = "sha256-1VyNXu11/pDMuH4DmFYSUF/qZ4Bo+/Zl3Y0JkyrH/r0=";
|
||||
release."0.6.0".hash = "sha256-0msICcIrK6jbOSiBu0gIVU3RHwoEEvB88CMQqW/06rg=";
|
||||
release."0.5.3".hash = "sha256-1NjFsi5TITF8ZWx1NyppRmi8g6YaoUtTdS9bU/sUe5k=";
|
||||
release."0.5.2".hash = "sha256:0yx5p9zyl8jv1vg7rgkyq8dqzkdnkqv969mi62whmhkvxbavgzbw";
|
||||
release."0.5.1".hash = "sha256:1hnzqb1gxf88wgj2n1b0f2xm6sxg9j0735zdsv6j12hlvx5lwk68";
|
||||
release."0.3.13".hash = "sha256-Yaztew79KWRC933kGFOAUIIoqukaZOdNOdw4XszR1Hg=";
|
||||
release."0.3.10".hash = "sha256-FBH2c8QRibq5Ycw/ieB8mZl0fDiPrYdIzZ6W/A3pIhI=";
|
||||
release."0.3.9".hash = "sha256-uUU9diBwUqBrNRLiDc0kz0CGkwTZCUmigPwLbpDOeg4=";
|
||||
release."0.3.6".hash = "sha256:0g2j7b2hca4byz62ssgg90bkbc8wwp7xkb2d3225bbvihi92b4c5";
|
||||
release."0.3.4".hash = "sha256:18mgycjgg829dbr7ps77z6lcj03h3dchjbj5iir0pybxby7gd45c";
|
||||
release."0.3.3".hash = "sha256:1m2mxcngj368vbdb8mlr91hsygl430spl7lgyn9qmn3jykack867";
|
||||
release."0.3.1".hash = "sha256:1iad288yvrjv8ahl9v18vfblgqb1l5z6ax644w49w9hwxs93f2k8";
|
||||
release."0.2.3".hash = "sha256:0p9mr8g1qma6h10qf7014dv98ln90dfkwn76ynagpww7qap8s966";
|
||||
|
||||
defaultVersion =
|
||||
let
|
||||
case = coq: mc: out: {
|
||||
cases = [
|
||||
coq
|
||||
mc
|
||||
];
|
||||
inherit out;
|
||||
};
|
||||
in
|
||||
with lib.versions;
|
||||
lib.switch
|
||||
[ coq.coq-version mathcomp.version ]
|
||||
[
|
||||
(case (range "8.20" "9.1") (range "2.4.0" "2.5.0") "1.14.0")
|
||||
(case (range "8.20" "9.1") (range "2.1.0" "2.4.0") "1.13.0")
|
||||
(case (range "8.20" "9.1") (range "2.1.0" "2.4.0") "1.12.0")
|
||||
(case (range "8.19" "8.20") (range "2.1.0" "2.3.0") "1.9.0")
|
||||
(case (range "8.17" "8.20") (range "2.0.0" "2.2.0") "1.1.0")
|
||||
(case (range "8.17" "8.19") (range "1.17.0" "1.19.0") "0.7.0")
|
||||
(case (range "8.17" "8.18") (range "1.15.0" "1.18.0") "0.6.7")
|
||||
(case (range "8.17" "8.18") (range "1.15.0" "1.18.0") "0.6.6")
|
||||
(case (range "8.14" "8.18") (range "1.15.0" "1.17.0") "0.6.5")
|
||||
(case (range "8.14" "8.18") (range "1.13.0" "1.16.0") "0.6.1")
|
||||
(case (range "8.14" "8.18") (range "1.13" "1.15") "0.5.2")
|
||||
(case (range "8.13" "8.15") (range "1.13" "1.14") "0.5.1")
|
||||
(case (range "8.13" "8.15") (range "1.12" "1.14") "0.3.13")
|
||||
(case (range "8.11" "8.14") (range "1.12" "1.13") "0.3.10")
|
||||
(case (range "8.10" "8.12") "1.11.0" "0.3.3")
|
||||
(case (range "8.10" "8.11") "1.11.0" "0.3.1")
|
||||
(case (range "8.8" "8.11") (range "1.8" "1.10") "0.2.3")
|
||||
]
|
||||
null;
|
||||
|
||||
# list of analysis packages sorted by dependency order
|
||||
packages = {
|
||||
"classical" = [ ];
|
||||
"reals" = [ "classical" ];
|
||||
"experimental-reals" = [ "reals" ];
|
||||
"analysis" = [ "reals" ];
|
||||
"reals-stdlib" = [ "reals" ];
|
||||
"analysis-stdlib" = [
|
||||
"analysis"
|
||||
"reals-stdlib"
|
||||
];
|
||||
};
|
||||
|
||||
mathcomp_ =
|
||||
package:
|
||||
let
|
||||
classical-deps = [
|
||||
mathcomp.ssreflect
|
||||
mathcomp.algebra
|
||||
mathcomp-finmap
|
||||
];
|
||||
experimental-reals-deps = [ mathcomp-bigenough ];
|
||||
analysis-deps = [
|
||||
mathcomp.field
|
||||
mathcomp-bigenough
|
||||
];
|
||||
intra-deps = lib.optionals (package != "single") (map mathcomp_ packages.${package});
|
||||
pkgpath = lib.switch package [
|
||||
{
|
||||
case = "single";
|
||||
out = ".";
|
||||
}
|
||||
{
|
||||
case = "analysis";
|
||||
out = "theories";
|
||||
}
|
||||
{
|
||||
case = "experimental-reals";
|
||||
out = "experimental_reals";
|
||||
}
|
||||
{
|
||||
case = "reals-stdlib";
|
||||
out = "reals_stdlib";
|
||||
}
|
||||
{
|
||||
case = "analysis-stdlib";
|
||||
out = "analysis_stdlib";
|
||||
}
|
||||
] package;
|
||||
pname = if package == "single" then "mathcomp-analysis-single" else "mathcomp-${package}";
|
||||
derivation = mkCoqDerivation {
|
||||
inherit
|
||||
version
|
||||
pname
|
||||
defaultVersion
|
||||
release
|
||||
repo
|
||||
owner
|
||||
;
|
||||
|
||||
namePrefix = [
|
||||
"coq"
|
||||
"mathcomp"
|
||||
];
|
||||
|
||||
propagatedBuildInputs =
|
||||
intra-deps
|
||||
++ lib.optionals (lib.elem package [
|
||||
"classical"
|
||||
"single"
|
||||
]) classical-deps
|
||||
++ lib.optionals (lib.elem package [
|
||||
"experimental-reals"
|
||||
"single"
|
||||
]) experimental-reals-deps
|
||||
++ lib.optionals (lib.elem package [
|
||||
"analysis"
|
||||
"single"
|
||||
]) analysis-deps
|
||||
++ lib.optional (lib.elem package [
|
||||
"reals-stdlib"
|
||||
"analysis-stdlib"
|
||||
"single"
|
||||
]) stdlib;
|
||||
|
||||
preBuild = ''
|
||||
cd ${pkgpath}
|
||||
'';
|
||||
|
||||
meta = {
|
||||
description = "Analysis library compatible with Mathematical Components";
|
||||
maintainers = [ lib.maintainers.cohencyril ];
|
||||
license = lib.licenses.cecill-c;
|
||||
};
|
||||
|
||||
passthru = lib.mapAttrs (package: deps: mathcomp_ package) packages;
|
||||
};
|
||||
# split packages didn't exist before 0.6, so building nothing in that case
|
||||
patched-derivation1 = derivation.overrideAttrs (
|
||||
o:
|
||||
lib.optionalAttrs
|
||||
(
|
||||
o.pname != null
|
||||
&& o.pname != "mathcomp-analysis"
|
||||
&& o.version != null
|
||||
&& o.version != "dev"
|
||||
&& lib.versions.isLt "0.6" o.version
|
||||
)
|
||||
{
|
||||
preBuild = "";
|
||||
buildPhase = "echo doing nothing";
|
||||
installPhase = "echo doing nothing";
|
||||
}
|
||||
);
|
||||
patched-derivation2 = patched-derivation1.overrideAttrs (
|
||||
o:
|
||||
lib.optionalAttrs (
|
||||
o.pname != null
|
||||
&& o.pname == "mathcomp-analysis"
|
||||
&& o.version != null
|
||||
&& o.version != "dev"
|
||||
&& lib.versions.isLt "0.6" o.version
|
||||
) { preBuild = ""; }
|
||||
);
|
||||
# only packages classical and analysis existed before 1.7, so building nothing in that case
|
||||
patched-derivation3 = patched-derivation2.overrideAttrs (
|
||||
o:
|
||||
lib.optionalAttrs
|
||||
(
|
||||
o.pname != null
|
||||
&& o.pname != "mathcomp-classical"
|
||||
&& o.pname != "mathcomp-analysis"
|
||||
&& o.version != null
|
||||
&& o.version != "dev"
|
||||
&& lib.versions.isLt "1.7" o.version
|
||||
)
|
||||
{
|
||||
preBuild = "";
|
||||
buildPhase = "echo doing nothing";
|
||||
installPhase = "echo doing nothing";
|
||||
}
|
||||
);
|
||||
patched-derivation = patched-derivation3.overrideAttrs (
|
||||
o:
|
||||
lib.optionalAttrs (o.version != null && (o.version == "dev" || lib.versions.isGe "0.3.4" o.version))
|
||||
{
|
||||
propagatedBuildInputs = o.propagatedBuildInputs ++ [ hierarchy-builder ];
|
||||
}
|
||||
);
|
||||
in
|
||||
patched-derivation;
|
||||
in
|
||||
# this is just a wrapper for rocqPackages.mathcomp-analysis for Rocq >= 9.0
|
||||
if
|
||||
coq.rocqPackages ? mathcomp-analysis
|
||||
&& !(lib.elem version [
|
||||
"1.12.0"
|
||||
"1.13.0"
|
||||
"1.14.0"
|
||||
"1.15.0"
|
||||
])
|
||||
then
|
||||
coq.rocqPackages.mathcomp-analysis.override {
|
||||
inherit version single;
|
||||
inherit
|
||||
mathcomp
|
||||
mathcomp-finmap
|
||||
mathcomp-bigenough
|
||||
stdlib
|
||||
;
|
||||
inherit (coq.rocqPackages) rocq-core;
|
||||
}
|
||||
else
|
||||
mathcomp_ (if single then "single" else "analysis")
|
||||
@@ -1,52 +0,0 @@
|
||||
{
|
||||
coq,
|
||||
mkCoqDerivation,
|
||||
mathcomp-boot,
|
||||
lib,
|
||||
version ? null,
|
||||
}:
|
||||
|
||||
let
|
||||
derivation = mkCoqDerivation {
|
||||
|
||||
namePrefix = [
|
||||
"coq"
|
||||
"mathcomp"
|
||||
];
|
||||
pname = "bigenough";
|
||||
owner = "math-comp";
|
||||
|
||||
release = {
|
||||
"1.0.0".hash = "sha256:10g0gp3hk7wri7lijkrqna263346wwf6a3hbd4qr9gn8hmsx70wg";
|
||||
"1.0.1".hash = "sha256:02f4dv4rz72liciwxb2k7acwx6lgqz4381mqyq5854p3nbyn06aw";
|
||||
"1.0.2".hash = "sha256-fJ/5xr91VtvpIoaFwb3PlnKl6UHG6GEeBRVGZrVLMU0=";
|
||||
"1.0.3".hash = "sha256-9ObUoaavnninL72r5iqkLz7lJBpcKXXi8LXKGhgx/N4=";
|
||||
};
|
||||
inherit version;
|
||||
defaultVersion =
|
||||
let
|
||||
case = case: out: { inherit case out; };
|
||||
in
|
||||
with lib.versions;
|
||||
lib.switch coq.coq-version [
|
||||
(case (range "8.10" "9.1") "1.0.3")
|
||||
(case (range "8.10" "9.1") "1.0.2")
|
||||
(case (range "8.5" "8.14") "1.0.0")
|
||||
] null;
|
||||
|
||||
propagatedBuildInputs = [ mathcomp-boot ];
|
||||
|
||||
meta = {
|
||||
description = "Small library to do epsilon - N reasonning";
|
||||
license = lib.licenses.cecill-b;
|
||||
};
|
||||
};
|
||||
in
|
||||
# this is just a wrapper for rocqPackages.mathcomp-bigenough for Rocq >= 9.0
|
||||
if coq.rocqPackages ? mathcomp-bigenough then
|
||||
coq.rocqPackages.mathcomp-bigenough.override {
|
||||
inherit version mathcomp-boot;
|
||||
inherit (coq.rocqPackages) rocq-core;
|
||||
}
|
||||
else
|
||||
derivation
|
||||
@@ -1,79 +0,0 @@
|
||||
{
|
||||
coq,
|
||||
mkCoqDerivation,
|
||||
mathcomp-boot,
|
||||
lib,
|
||||
version ? null,
|
||||
}:
|
||||
|
||||
let
|
||||
derivation = mkCoqDerivation {
|
||||
|
||||
namePrefix = [
|
||||
"coq"
|
||||
"mathcomp"
|
||||
];
|
||||
pname = "finmap";
|
||||
owner = "math-comp";
|
||||
inherit version;
|
||||
defaultVersion =
|
||||
let
|
||||
case = coq: mc: out: {
|
||||
cases = [
|
||||
coq
|
||||
mc
|
||||
];
|
||||
inherit out;
|
||||
};
|
||||
in
|
||||
with lib.versions;
|
||||
lib.switch
|
||||
[ coq.coq-version mathcomp-boot.version ]
|
||||
[
|
||||
(case (range "8.20" "9.1") (range "2.3" "2.5") "2.2.2")
|
||||
(case (range "8.20" "9.1") (range "2.3" "2.4") "2.2.0")
|
||||
(case (range "8.16" "9.0") (range "2.0" "2.3") "2.1.0")
|
||||
(case (range "8.16" "8.18") (range "2.0" "2.1") "2.0.0")
|
||||
(case (range "8.13" "8.20") (range "1.12" "1.19") "1.5.2")
|
||||
(case (isGe "8.10") (range "1.11" "1.17") "1.5.1")
|
||||
(case (range "8.7" "8.11") "1.11.0" "1.5.0")
|
||||
(case (isEq "8.11") (range "1.8" "1.10") "1.4.0+coq-8.11")
|
||||
(case (range "8.7" "8.11.0") (range "1.8" "1.10") "1.4.0")
|
||||
(case (range "8.7" "8.11.0") (range "1.8" "1.10") "1.3.4")
|
||||
(case (range "8.7" "8.9") "1.7.0" "1.1.0")
|
||||
(case (range "8.6" "8.7") (range "1.6.1" "1.7") "1.0.0")
|
||||
]
|
||||
null;
|
||||
release = {
|
||||
"2.2.2".hash = "sha256-G5fSdx4MhOXtQ2H8lpyK5FuIbWAZNc7vRL3hcYmGA2o=";
|
||||
"2.2.0".hash = "sha256-oDQEZOutrJxmN8FvzovUIhqw0mwc8Ej7thrieJrW8BY=";
|
||||
"2.1.0".hash = "sha256-gh0cnhdVDyo+D5zdtxLc10kGKQLQ3ITzHnMC45mCtpY=";
|
||||
"2.0.0".hash = "sha256-0Wr1ZUYVuZH74vawO4EZlZ+K3kq+s1xEz/BfzyKj+wk=";
|
||||
"1.5.2".hash = "sha256-0KmmSjc2AlUo6BKr9RZ4FjL9wlGISlTGU0X1Eu7l4sw=";
|
||||
"1.5.1".hash = "sha256:0ryfml4pf1dfya16d8ma80favasmrygvspvb923n06kfw9v986j7";
|
||||
"1.5.0".hash = "sha256:0vx9n1fi23592b3hv5p5ycy7mxc8qh1y5q05aksfwbzkk5zjkwnq";
|
||||
"1.4.1".hash = "sha256:0kx4nx24dml1igk0w0qijmw221r5bgxhwhl5qicnxp7ab3c35s8p";
|
||||
"1.4.0+coq-8.11".hash = "sha256:1fd00ihyx0kzq5fblh9vr8s5mr1kg7p6pk11c4gr8svl1n69ppmb";
|
||||
"1.4.0".hash = "sha256:0mp82mcmrs424ff1vj3cvd8353r9vcap027h3p0iprr1vkkwjbzd";
|
||||
"1.3.4".hash = "sha256:0f5a62ljhixy5d7gsnwd66gf054l26k3m79fb8nz40i2mgp6l9ii";
|
||||
"1.2.1".hash = "sha256:0jryb5dq8js3imbmwrxignlk5zh8gwfb1wr4b1s7jbwz410vp7zf";
|
||||
"1.1.0".hash = "sha256:05df59v3na8jhpsfp7hq3niam6asgcaipg2wngnzxzqnl86srp2a";
|
||||
"1.0.0".hash = "sha256:0sah7k9qm8sw17cgd02f0x84hki8vj8kdz7h15i7rmz08rj0whpa";
|
||||
};
|
||||
|
||||
propagatedBuildInputs = [ mathcomp-boot ];
|
||||
|
||||
meta = {
|
||||
description = "Finset and finmap library";
|
||||
license = lib.licenses.cecill-b;
|
||||
};
|
||||
};
|
||||
in
|
||||
# this is just a wrapper for rocqPackages.mathcomp-finmap for Rocq >= 9.0
|
||||
if coq.rocqPackages ? mathcomp-finmap then
|
||||
coq.rocqPackages.mathcomp-finmap.override {
|
||||
inherit version mathcomp-boot;
|
||||
inherit (coq.rocqPackages) rocq-core;
|
||||
}
|
||||
else
|
||||
derivation
|
||||
@@ -1,95 +0,0 @@
|
||||
{
|
||||
coq,
|
||||
mkCoqDerivation,
|
||||
mathcomp,
|
||||
mathcomp-bigenough,
|
||||
lib,
|
||||
version ? null,
|
||||
}:
|
||||
|
||||
let
|
||||
derivation = mkCoqDerivation {
|
||||
|
||||
namePrefix = [
|
||||
"coq"
|
||||
"mathcomp"
|
||||
];
|
||||
pname = "real-closed";
|
||||
owner = "math-comp";
|
||||
inherit version;
|
||||
release = {
|
||||
"2.0.3".hash = "sha256-heZ7aZ7TO9YNAESIvbAc1qqzO91xMyLAox8VKueIk/s=";
|
||||
"2.0.2".hash = "sha256-hBo9JMtmXDYBmf5ihKGksQLHv3c0+zDBnd8/aI2V/ao=";
|
||||
"2.0.1".hash = "sha256-tQTI3PCl0q1vWpps28oATlzOI8TpVQh1jhTwVmhaZic=";
|
||||
"2.0.0".hash = "sha256-sZvfiC5+5Lg4nRhfKKqyFzovCj2foAhqaq/w9F2bdU8=";
|
||||
"1.1.4".hash = "sha256-8Hs6XfowbpeRD8RhMRf4ZJe2xf8kE0e8m7bPUzR/IM4=";
|
||||
"1.1.3".hash = "sha256:1vwmmnzy8i4f203i2s60dn9i0kr27lsmwlqlyyzdpsghvbr8h5b7";
|
||||
"1.1.2".hash = "sha256:0907x4nf7nnvn764q3x9lx41g74rilvq5cki5ziwgpsdgb98pppn";
|
||||
"1.1.1".hash = "sha256:0ksjscrgq1i79vys4zrmgvzy2y4ylxa8wdsf4kih63apw6v5ws6b";
|
||||
"1.0.5".hash = "sha256:0q8nkxr9fba4naylr5xk7hfxsqzq2pvwlg1j0xxlhlgr3fmlavg2";
|
||||
"1.0.4".hash = "sha256:058v9dj973h9kfhqmvcy9a6xhhxzljr90cf99hdfcdx68fi2ha1b";
|
||||
"1.0.3".hash = "sha256:1xbzkzqgw5p42dx1liy6wy8lzdk39zwd6j14fwvv5735k660z7yb";
|
||||
"1.0.1".hash = "sha256:0j81gkjbza5vg89v4n9z598mfdbql416963rj4b8fzm7dp2r4rxg";
|
||||
};
|
||||
|
||||
defaultVersion =
|
||||
let
|
||||
case = coq: mc: out: {
|
||||
cases = [
|
||||
coq
|
||||
mc
|
||||
];
|
||||
inherit out;
|
||||
};
|
||||
in
|
||||
with lib.versions;
|
||||
lib.switch
|
||||
[ coq.version mathcomp.version ]
|
||||
[
|
||||
(case (range "8.18" "9.1") (isGe "2.2.0") "2.0.3")
|
||||
(case (range "8.17" "9.0") (range "2.1.0" "2.3.0") "2.0.2")
|
||||
(case (range "8.17" "8.20") (range "2.0.0" "2.2.0") "2.0.1")
|
||||
(case (range "8.16" "8.19") (range "2.0.0" "2.2.0") "2.0.0")
|
||||
(case (range "8.13" "8.19") (range "1.13.0" "1.19.0") "1.1.4")
|
||||
(case (isGe "8.13") (range "1.12.0" "1.18.0") "1.1.3")
|
||||
(case (isGe "8.10") (range "1.12.0" "1.18.0") "1.1.2")
|
||||
(case (isGe "8.7") "1.11.0" "1.1.1")
|
||||
(case (isGe "8.7") (range "1.9.0" "1.10.0") "1.0.4")
|
||||
(case (isGe "8.7") "1.8.0" "1.0.3")
|
||||
(case (isGe "8.7") "1.7.0" "1.0.1")
|
||||
]
|
||||
null;
|
||||
|
||||
propagatedBuildInputs = [
|
||||
mathcomp.ssreflect
|
||||
mathcomp.algebra
|
||||
mathcomp.field
|
||||
mathcomp.fingroup
|
||||
mathcomp.solvable
|
||||
mathcomp-bigenough
|
||||
];
|
||||
|
||||
meta = {
|
||||
description = "Mathematical Components Library on real closed fields";
|
||||
license = lib.licenses.cecill-c;
|
||||
};
|
||||
};
|
||||
in
|
||||
# this is just a wrapper for rocqPackages.mathcomp-real-closed for Rocq >= 9.0
|
||||
if
|
||||
coq.rocqPackages ? mathcomp-real-closed
|
||||
&& !(lib.elem version [
|
||||
"2.0.2"
|
||||
"2.0.3"
|
||||
])
|
||||
then
|
||||
coq.rocqPackages.mathcomp-real-closed.override {
|
||||
inherit version;
|
||||
inherit
|
||||
mathcomp
|
||||
mathcomp-bigenough
|
||||
;
|
||||
inherit (coq.rocqPackages) rocq-core;
|
||||
}
|
||||
else
|
||||
derivation
|
||||
@@ -1,285 +0,0 @@
|
||||
############################################################################
|
||||
# This file mainly provides the `mathcomp` derivation, which is #
|
||||
# essentially a meta-package containing all core mathcomp libraries #
|
||||
# (ssreflect fingroup algebra solvable field character). They can be #
|
||||
# accessed individually through the passthrough attributes of mathcomp #
|
||||
# bearing the same names (mathcomp.ssreflect, etc). #
|
||||
############################################################################
|
||||
# Compiling a custom version of mathcomp using `mathcomp.override`. #
|
||||
# This is the replacement for the former `mathcomp_ config` function. #
|
||||
# See the documentation at doc/languages-frameworks/coq.section.md. #
|
||||
############################################################################
|
||||
|
||||
{
|
||||
lib,
|
||||
ncurses,
|
||||
graphviz,
|
||||
lua,
|
||||
fetchzip,
|
||||
mkCoqDerivation,
|
||||
withDoc ? false,
|
||||
single ? false,
|
||||
coq,
|
||||
hierarchy-builder,
|
||||
stdlib,
|
||||
version ? null,
|
||||
}@args:
|
||||
|
||||
let
|
||||
repo = "math-comp";
|
||||
owner = "math-comp";
|
||||
withDoc = single && (args.withDoc or false);
|
||||
defaultVersion =
|
||||
let
|
||||
case = case: out: { inherit case out; };
|
||||
inherit (lib.versions) range;
|
||||
in
|
||||
lib.switch coq.coq-version [
|
||||
(case (range "8.20" "9.1") "2.5.0")
|
||||
(case (range "8.20" "9.1") "2.4.0")
|
||||
(case (range "8.19" "9.0") "2.3.0")
|
||||
(case (range "8.17" "8.20") "2.2.0")
|
||||
(case (range "8.17" "8.18") "2.1.0")
|
||||
(case (range "8.17" "8.18") "2.0.0")
|
||||
(case (range "8.19" "8.20") "1.19.0")
|
||||
(case (range "8.17" "8.18") "1.18.0")
|
||||
(case (range "8.15" "8.18") "1.17.0")
|
||||
(case (range "8.13" "8.18") "1.16.0")
|
||||
(case (range "8.14" "8.16") "1.15.0")
|
||||
(case (range "8.11" "8.15") "1.14.0")
|
||||
(case (range "8.11" "8.15") "1.13.0")
|
||||
(case (range "8.10" "8.13") "1.12.0")
|
||||
(case (range "8.7" "8.12") "1.11.0")
|
||||
(case (range "8.7" "8.11") "1.10.0")
|
||||
(case (range "8.7" "8.11") "1.9.0")
|
||||
(case (range "8.7" "8.9") "1.8.0")
|
||||
(case (range "8.6" "8.9") "1.7.0")
|
||||
(case (range "8.5" "8.7") "1.6.4")
|
||||
] null;
|
||||
release = {
|
||||
"2.5.0".hash = "sha256-M/6IP4WhTQ4j2Bc8nXBXjSjWO08QzNIYI+a2owfOh+8=";
|
||||
"2.4.0".hash = "sha256-A1XgLLwZRvKS8QyceCkSQa7ue6TYyf5fMft5gSx9NOs=";
|
||||
"2.3.0".hash = "sha256-wa6OBig8rhAT4iwupSylyCAMhO69rADa0MQIX5zzL+Q=";
|
||||
"2.2.0".hash = "sha256-SPyWSI5kIP5w7VpgnQ4vnK56yEuWnJylNQOT7M77yoQ=";
|
||||
"2.1.0".hash = "sha256-XDLx0BIkVRkSJ4sGCIE51j3rtkSGemNTs/cdVmTvxqo=";
|
||||
"2.0.0".hash = "sha256-dpOmrHYUXBBS9kmmz7puzufxlbNpIZofpcTvJFLG5DI=";
|
||||
"1.19.0".hash = "sha256-3kxS3qA+7WwQkXoFC/+kq3OEkv4kMEzQ/G3aXPsp1Q4=";
|
||||
"1.18.0".hash = "sha256-mJJ/zvM2WtmBZU3U4oid/zCMvDXei/93v5hwyyqwiiY=";
|
||||
"1.17.0".hash = "sha256-bUfoSTMiW/GzC1jKFay6DRqGzKPuLOSUsO6/wPSFwNg=";
|
||||
"1.16.0".hash = "sha256-gXTKhRgSGeRBUnwdDezMsMKbOvxdffT+kViZ9e1gEz0=";
|
||||
"1.15.0".hash = "sha256:1bp0jxl35ms54s0mdqky15w9af03f3i0n06qk12k4gw1xzvwqv21";
|
||||
"1.14.0".hash = "sha256:07yamlp1c0g5nahkd2gpfhammcca74ga2s6qr7a3wm6y6j5pivk9";
|
||||
"1.13.0".hash = "sha256:0j4cz2y1r1aw79snkcf1pmicgzf8swbaf9ippz0vg99a572zqzri";
|
||||
"1.12.0".hash = "sha256:1ccfny1vwgmdl91kz5xlmhq4wz078xm4z5wpd0jy5rn890dx03wp";
|
||||
"1.11.0".hash = "sha256:06a71d196wd5k4wg7khwqb7j7ifr7garhwkd54s86i0j7d6nhl3c";
|
||||
"1.10.0".hash = "sha256:1b9m6pwxxyivw7rgx82gn5kmgv2mfv3h3y0mmjcjfypi8ydkrlbv";
|
||||
"1.9.0".hash = "sha256:0lid9zaazdi3d38l8042lczb02pw5m9wq0yysiilx891hgq2p81r";
|
||||
"1.8.0".hash = "sha256:07l40is389ih8bi525gpqs3qp4yb2kl11r9c8ynk1ifpjzpnabwp";
|
||||
"1.7.0".hash = "sha256:0wnhj9nqpx2bw6n1l4i8jgrw3pjajvckvj3lr4vzjb3my2lbxdd1";
|
||||
"1.6.4".hash = "sha256:09ww48qbjsvpjmy1g9yhm0rrkq800ffq21p6fjkbwd34qvd82raz";
|
||||
"1.6.1".hash = "sha256:1ilw6vm4dlsdv9cd7kmf0vfrh2kkzr45wrqr8m37miy0byzr4p9i";
|
||||
};
|
||||
releaseRev = v: "mathcomp-${v}";
|
||||
|
||||
# list of core mathcomp packages sorted by dependency order
|
||||
packages = {
|
||||
"boot" = [ ];
|
||||
"order" = [ "boot" ];
|
||||
"fingroup" = [ "boot" ];
|
||||
"ssreflect" = [
|
||||
"boot"
|
||||
"order"
|
||||
];
|
||||
"algebra" = [
|
||||
"order"
|
||||
"fingroup"
|
||||
];
|
||||
"solvable" = [ "algebra" ];
|
||||
"field" = [ "solvable" ];
|
||||
"character" = [ "field" ];
|
||||
"all" = [ "character" ];
|
||||
};
|
||||
meta = {
|
||||
homepage = "https://math-comp.github.io/";
|
||||
license = lib.licenses.cecill-b;
|
||||
maintainers = with lib.maintainers; [
|
||||
vbgl
|
||||
jwiegley
|
||||
cohencyril
|
||||
];
|
||||
};
|
||||
|
||||
mathcomp_ =
|
||||
package:
|
||||
let
|
||||
mathcomp-deps = lib.optionals (package != "single") (map mathcomp_ packages.${package});
|
||||
pkgpath = if package == "single" then "." else package;
|
||||
pname = if package == "single" then "mathcomp" else "mathcomp-${package}";
|
||||
pkgallMake = ''
|
||||
echo "all.v" > Make
|
||||
echo "-I ." >> Make
|
||||
echo "-R . mathcomp.all" >> Make
|
||||
'';
|
||||
derivation = mkCoqDerivation (
|
||||
{
|
||||
inherit
|
||||
version
|
||||
pname
|
||||
defaultVersion
|
||||
release
|
||||
releaseRev
|
||||
repo
|
||||
owner
|
||||
meta
|
||||
;
|
||||
|
||||
mlPlugin = lib.versions.isLe "8.6" coq.coq-version;
|
||||
nativeBuildInputs = lib.optionals withDoc [
|
||||
graphviz
|
||||
lua
|
||||
];
|
||||
buildInputs = [ ncurses ];
|
||||
propagatedBuildInputs = mathcomp-deps;
|
||||
|
||||
buildFlags = lib.optional withDoc "doc";
|
||||
|
||||
preBuild = ''
|
||||
if [[ -f etc/utils/ssrcoqdep ]]
|
||||
then patchShebangs etc/utils/ssrcoqdep
|
||||
fi
|
||||
if [[ -f etc/buildlibgraph ]]
|
||||
then patchShebangs etc/buildlibgraph
|
||||
fi
|
||||
''
|
||||
+ ''
|
||||
# handle mathcomp < 2.4.0 which had an extra base mathcomp directory
|
||||
test -d mathcomp && cd mathcomp
|
||||
cd ${pkgpath} || cd ssreflect # before 2.5, boot didn't exist, make it behave as ssreflect
|
||||
''
|
||||
+ lib.optionalString (package == "all") pkgallMake;
|
||||
}
|
||||
// lib.optionalAttrs (package != "single") { passthru = lib.mapAttrs (p: _: mathcomp_ p) packages; }
|
||||
// lib.optionalAttrs withDoc {
|
||||
htmldoc_template = fetchzip {
|
||||
url = "https://github.com/math-comp/math-comp.github.io/archive/doc-1.12.0.zip";
|
||||
hash = "sha256:0y1352ha2yy6k2dl375sb1r68r1qi9dyyy7dyzj5lp9hxhhq69x8";
|
||||
};
|
||||
postBuild = ''
|
||||
cp -rf _build_doc/* .
|
||||
rm -r _build_doc
|
||||
'';
|
||||
postInstall =
|
||||
let
|
||||
tgt = "$out/share/coq/${coq.coq-version}/";
|
||||
in
|
||||
lib.optionalString withDoc ''
|
||||
mkdir -p ${tgt}
|
||||
cp -r htmldoc ${tgt}
|
||||
cp -r $htmldoc_template/htmldoc_template/* ${tgt}/htmldoc/
|
||||
'';
|
||||
buildTargets = "doc";
|
||||
extraInstallFlags = [ "-f Makefile.coq" ];
|
||||
}
|
||||
);
|
||||
patched-derivation1 = derivation.overrideAttrs (
|
||||
o:
|
||||
lib.optionalAttrs
|
||||
(
|
||||
o.pname != null
|
||||
&& o.pname == "mathcomp-all"
|
||||
&& o.version != null
|
||||
&& o.version != "dev"
|
||||
&& lib.versions.isLt "1.7" o.version
|
||||
)
|
||||
{
|
||||
preBuild = "";
|
||||
buildPhase = "";
|
||||
installPhase = "echo doing nothing";
|
||||
}
|
||||
);
|
||||
patched-derivation2 = patched-derivation1.overrideAttrs (
|
||||
o:
|
||||
lib.optionalAttrs
|
||||
(
|
||||
lib.versions.isLe "8.7" coq.coq-version || (o.version != "dev" && lib.versions.isLe "1.7" o.version)
|
||||
)
|
||||
{
|
||||
installFlags = o.installFlags ++ [ "-f Makefile.coq" ];
|
||||
}
|
||||
);
|
||||
patched-derivation3 = patched-derivation2.overrideAttrs (
|
||||
o:
|
||||
lib.optionalAttrs (o.version != null && (o.version == "dev" || lib.versions.isGe "2.0.0" o.version))
|
||||
{
|
||||
propagatedBuildInputs = o.propagatedBuildInputs ++ [ hierarchy-builder ];
|
||||
}
|
||||
);
|
||||
patched-derivation4 = patched-derivation3.overrideAttrs (
|
||||
o:
|
||||
lib.optionalAttrs (o.version != null && o.version == "2.3.0") {
|
||||
propagatedBuildInputs = o.propagatedBuildInputs ++ [ stdlib ];
|
||||
}
|
||||
);
|
||||
# boot and order packages didn't exist before 2.5,
|
||||
# so make boot behave as ssreflect then (c.f., above)
|
||||
# and building nothing in order and ssreflect
|
||||
patched-derivation5 = patched-derivation4.overrideAttrs (
|
||||
o:
|
||||
lib.optionalAttrs
|
||||
(
|
||||
lib.elem package [
|
||||
"order"
|
||||
"ssreflect"
|
||||
]
|
||||
&& o.version != null
|
||||
&& o.version != "dev"
|
||||
&& lib.versions.isLt "2.5" o.version
|
||||
)
|
||||
{
|
||||
preBuild = "";
|
||||
buildPhase = "echo doing nothing";
|
||||
installPhase = "echo doing nothing";
|
||||
}
|
||||
);
|
||||
in
|
||||
patched-derivation5;
|
||||
in
|
||||
# this is just a wrapper for rocqPackages.mathcomp for Rocq >= 9.0
|
||||
if coq.rocqPackages ? mathcomp && version != "2.3.0" && version != "2.4.0" then
|
||||
let
|
||||
mc = coq.rocqPackages.mathcomp.override {
|
||||
inherit version withDoc single;
|
||||
inherit
|
||||
ncurses
|
||||
graphviz
|
||||
lua
|
||||
fetchzip
|
||||
hierarchy-builder
|
||||
;
|
||||
inherit (coq.rocqPackages) rocq-core micromega-plugin;
|
||||
};
|
||||
in
|
||||
mc
|
||||
// {
|
||||
ssreflect = mkCoqDerivation {
|
||||
inherit
|
||||
version
|
||||
defaultVersion
|
||||
release
|
||||
releaseRev
|
||||
repo
|
||||
owner
|
||||
meta
|
||||
;
|
||||
pname = "mathcomp-ssreflect";
|
||||
propagatedBuildInputs = [
|
||||
mc.boot
|
||||
mc.order
|
||||
];
|
||||
preBuild = "cd ssreflect";
|
||||
};
|
||||
fingroup = mc.finite-group;
|
||||
character = mc.group-representation;
|
||||
}
|
||||
else
|
||||
mathcomp_ (if single then "single" else "all")
|
||||
@@ -1,41 +0,0 @@
|
||||
{
|
||||
lib,
|
||||
mkCoqDerivation,
|
||||
coq,
|
||||
version ? null,
|
||||
}:
|
||||
|
||||
let
|
||||
derivation = mkCoqDerivation {
|
||||
pname = "parseque";
|
||||
repo = "parseque";
|
||||
owner = "rocq-community";
|
||||
|
||||
inherit version;
|
||||
defaultVersion =
|
||||
let
|
||||
case = case: out: { inherit case out; };
|
||||
in
|
||||
lib.switch coq.coq-version [
|
||||
(case (lib.versions.range "8.16" "8.20") "0.2.2")
|
||||
] null;
|
||||
|
||||
release."0.2.2".hash = "sha256-O50Rs7Yf1H4wgwb7ltRxW+7IF0b04zpfs+mR83rxT+E=";
|
||||
|
||||
releaseRev = v: "v${v}";
|
||||
|
||||
meta = {
|
||||
description = "Total parser combinators in Coq/Rocq";
|
||||
maintainers = with lib.maintainers; [ womeier ];
|
||||
license = lib.licenses.mit;
|
||||
};
|
||||
};
|
||||
in
|
||||
# this is just a wrapper for rocqPackages.parseque for Rocq >= 9.0
|
||||
if coq.rocqPackages ? parseque then
|
||||
coq.rocqPackages.parseque.override {
|
||||
inherit version;
|
||||
inherit (coq.rocqPackages) rocq-core;
|
||||
}
|
||||
else
|
||||
derivation
|
||||
@@ -1,61 +0,0 @@
|
||||
{
|
||||
lib,
|
||||
mkCoqDerivation,
|
||||
coq,
|
||||
aac-tactics,
|
||||
mathcomp-boot,
|
||||
version ? null,
|
||||
}:
|
||||
|
||||
mkCoqDerivation {
|
||||
pname = "relation-algebra";
|
||||
owner = "damien-pous";
|
||||
|
||||
releaseRev = v: if lib.versions.range "1.7.6" "1.7.9" v then "v.${v}" else "v${v}";
|
||||
|
||||
release."1.7.11".hash = "sha256-ZOV0lUdduSabW9Qsz70clkO7QK/NK2STaHqBWcXb7nI=";
|
||||
release."1.7.10".hash = "sha256-h738L+dybhmWZwTSLJrhv+sB+cIbj0+62Zcy9BH5sVo=";
|
||||
release."1.7.9".hash = "sha256-1WzAZyj6q7s0u/9r7lahzxTl8612EA540l9wpm7TYEg=";
|
||||
release."1.7.8".hash = "sha256-RITFd3G5TjY+rFzW073Ao1AGU+u6OGQyQeGHVodAXnA=";
|
||||
release."1.7.7".hash = "sha256:1dff3id6nypl2alhk9rcifj3dab0j78dym05blc525lawsmc26l2";
|
||||
release."1.7.6".hash = "sha256:02gsj06zcy9zgd0h1ibqspwfiwm36pkkgg9cz37k4bxzcapxcr6w";
|
||||
release."1.7.5".hash = "sha256-XdO8agoJmNXPv8Ho+KTlLCB4oRlQsb0w06aM9M16ZBU=";
|
||||
release."1.7.4".hash = "sha256-o+v2CIAa2+9tJ/V8DneDTf4k31KMHycgMBLaQ+A4ufM=";
|
||||
release."1.7.3".hash = "sha256-4feSNfi7h4Yhwn5L+9KP9K1S7HCPvsvaVWwoQSTFvos=";
|
||||
release."1.7.2".hash = "sha256-f4oNjXspNMEz3AvhIeYO3avbUa1AThoC9DbcHMb5A2o=";
|
||||
release."1.7.1".hash = "sha256-WWVMcR6z8rT4wzZPb8SlaVWGe7NC8gScPqawd7bltQA=";
|
||||
|
||||
inherit version;
|
||||
defaultVersion =
|
||||
let
|
||||
case = case: out: { inherit case out; };
|
||||
in
|
||||
with lib.versions;
|
||||
lib.switch coq.coq-version [
|
||||
(case (isEq "8.20") "1.7.11")
|
||||
(case (range "8.18" "8.19") "1.7.10")
|
||||
(case (isEq "8.17") "1.7.9")
|
||||
(case (isEq "8.16") "1.7.8")
|
||||
(case (isEq "8.15") "1.7.7")
|
||||
(case (isEq "8.14") "1.7.6")
|
||||
(case (isEq "8.13") "1.7.5")
|
||||
(case (isEq "8.12") "1.7.4")
|
||||
(case (isEq "8.11") "1.7.3")
|
||||
(case (isEq "8.10") "1.7.2")
|
||||
(case (isEq "8.9") "1.7.1")
|
||||
] null;
|
||||
|
||||
mlPlugin = true;
|
||||
|
||||
propagatedBuildInputs = [
|
||||
aac-tactics
|
||||
mathcomp-boot
|
||||
];
|
||||
|
||||
meta = {
|
||||
description = "Relation algebra library for Coq";
|
||||
maintainers = with lib.maintainers; [ siraben ];
|
||||
license = lib.licenses.gpl3Plus;
|
||||
platforms = lib.platforms.unix;
|
||||
};
|
||||
}
|
||||
@@ -1,55 +0,0 @@
|
||||
{
|
||||
coq,
|
||||
mkCoqDerivation,
|
||||
lib,
|
||||
version ? null,
|
||||
}:
|
||||
|
||||
let
|
||||
derivation = mkCoqDerivation {
|
||||
|
||||
pname = "stdlib";
|
||||
repo = "stdlib";
|
||||
owner = "coq";
|
||||
opam-name = "coq-stdlib";
|
||||
|
||||
inherit version;
|
||||
defaultVersion =
|
||||
let
|
||||
case = case: out: { inherit case out; };
|
||||
in
|
||||
with lib.versions;
|
||||
lib.switch coq.coq-version [
|
||||
(case (isLe "9.1") "9.0.0")
|
||||
# the < 9.0 above is artificial as stdlib was included in Coq before
|
||||
] null;
|
||||
releaseRev = v: "V${v}";
|
||||
|
||||
release."9.0.0".hash = "sha256-2l7ak5Q/NbiNvUzIVXOniEneDXouBMNSSVFbD1Pf8cQ=";
|
||||
|
||||
configurePhase = ''
|
||||
echo no configuration
|
||||
'';
|
||||
buildPhase = ''
|
||||
echo building nothing
|
||||
'';
|
||||
installPhase = ''
|
||||
echo installing nothing
|
||||
# Make an output directory rather than a file, so this is more friendly to buildEnv
|
||||
mkdir $out
|
||||
'';
|
||||
|
||||
meta = {
|
||||
description = "Compatibility metapackage for Coq Stdlib library after the Rocq renaming";
|
||||
license = lib.licenses.lgpl21Only;
|
||||
};
|
||||
};
|
||||
in
|
||||
# this is just a wrapper for rocqPackages.stdlib for Rocq >= 9.0
|
||||
if coq.rocqPackages ? stdlib then
|
||||
coq.rocqPackages.stdlib.override {
|
||||
inherit version;
|
||||
inherit (coq.rocqPackages) rocq-core;
|
||||
}
|
||||
else
|
||||
derivation
|
||||
@@ -1,65 +0,0 @@
|
||||
{
|
||||
lib,
|
||||
mkCoqDerivation,
|
||||
coq,
|
||||
stdlib,
|
||||
version ? null,
|
||||
}:
|
||||
|
||||
let
|
||||
derivation = mkCoqDerivation {
|
||||
pname = "stdpp";
|
||||
inherit version;
|
||||
domain = "gitlab.mpi-sws.org";
|
||||
owner = "iris";
|
||||
defaultVersion =
|
||||
let
|
||||
case = case: out: { inherit case out; };
|
||||
in
|
||||
with lib.versions;
|
||||
lib.switch coq.coq-version [
|
||||
(case (range "8.19" "9.1") "1.12.0")
|
||||
(case (range "8.18" "8.19") "1.10.0")
|
||||
(case (range "8.16" "8.18") "1.9.0")
|
||||
(case (range "8.13" "8.17") "1.8.0")
|
||||
(case (range "8.12" "8.14") "1.6.0")
|
||||
(case (range "8.11" "8.13") "1.5.0")
|
||||
(case (range "8.8" "8.10") "1.4.0")
|
||||
] null;
|
||||
release."1.12.0".hash = "sha256-2o8YMkKbXrKHwtfpkdAovxl+2NZZk958GjSSd9wcEIU=";
|
||||
release."1.11.0".hash = "sha256-yqnkaA5gUdZBJZ3JnvPYh11vKQRl0BAnior1yGowG7k=";
|
||||
release."1.10.0".hash = "sha256-bfynevIKxAltvt76lsqVxBmifFkzEhyX8lRgTKxr21I=";
|
||||
release."1.9.0".hash = "sha256-OXeB+XhdyzWMp5Karsz8obp0rTeMKrtG7fu/tmc9aeI=";
|
||||
release."1.8.0".hash = "sha256-VkIGBPHevHeHCo/Q759Q7y9WyhSF/4SMht4cOPuAXHU=";
|
||||
release."1.7.0".hash = "sha256:0447wbzm23f9rl8byqf6vglasfn6c1wy6cxrrwagqjwsh3i5lx8y";
|
||||
release."1.6.0".hash = "sha256:1l1w6srzydjg0h3f4krrfgvz455h56shyy2lbcnwdbzjkahibl7v";
|
||||
release."1.5.0".hash = "sha256:1ym0fy620imah89p8b6rii8clx2vmnwcrbwxl3630h24k42092nf";
|
||||
release."1.4.0".hash = "sha256:1m6c7ibwc99jd4cv14v3r327spnfvdf3x2mnq51f9rz99rffk68r";
|
||||
releaseRev = v: "coq-stdpp-${v}";
|
||||
|
||||
propagatedBuildInputs = [ stdlib ];
|
||||
|
||||
preBuild = ''
|
||||
if [[ -f coq-lint.sh ]]
|
||||
then patchShebangs coq-lint.sh
|
||||
fi
|
||||
'';
|
||||
|
||||
meta = {
|
||||
description = "Extended “Standard Library” for Coq";
|
||||
license = lib.licenses.bsd3;
|
||||
maintainers = [
|
||||
lib.maintainers.vbgl
|
||||
lib.maintainers.ineol
|
||||
];
|
||||
};
|
||||
};
|
||||
in
|
||||
# this is just a wrapper for rocqPackages.stdpp for Rocq >= 9.0
|
||||
if coq.rocqPackages ? stdpp then
|
||||
coq.rocqPackages.stdpp.override {
|
||||
inherit version stdlib;
|
||||
inherit (coq.rocqPackages) rocq-core;
|
||||
}
|
||||
else
|
||||
derivation
|
||||
@@ -18,17 +18,42 @@ mkRocqDerivation {
|
||||
lib.switch rocq-core.rocq-version [
|
||||
(case (range "9.2" "9.3") "9.0.0+rocq9.2")
|
||||
(case (range "9.0" "9.1") "9.0.0+rocq${rocq-core.rocq-version}")
|
||||
(case (range "8.13" "8.20") "9.0.0+coq${rocq-core.rocq-version}")
|
||||
(case (range "8.6" "8.17") "${rocq-core.rocq-version}.0")
|
||||
] null;
|
||||
|
||||
release."9.0.0+rocq9.0".sha256 = "sha256-ctnwpyNVhryEUA5YEsAImrcJsNMhtBgDSOz+z5Z4R78=";
|
||||
release."9.0.0+rocq9.1".sha256 = "sha256-MSjlfJs3JOakuShOj+isNlus0bKlZ+rkvzRoKZQK5RQ=";
|
||||
release."9.0.0+rocq9.2".sha256 = "sha256-XQIx3MjmPgRsFMJiD1DR+FWkmO4J86tQ5fDuPHcjf+A=";
|
||||
releaseRev = v: "v${v}";
|
||||
release."9.0.0+coq8.20".hash = "sha256-pkvyDaMXRalc6Uu1eBTuiqTpRauRrzu946c6TavyTKY=";
|
||||
release."9.0.0+coq8.19".hash = "sha256-02uL+qWbUveHe67zKfc8w3U0iN3X2DKBsvP3pKpW8KQ=";
|
||||
release."9.0.0+coq8.18".hash = "sha256-vLeJ0GNKl4M84Uj2tAwlrxJOSR6VZoJQvdlDhxJRge8=";
|
||||
release."9.0.0+coq8.17".hash = "sha256-Mn85LqxJKPDIfpxRef9Uh5POwOKlTQ7jsMVz1wnQwuY=";
|
||||
release."9.0.0+coq8.16".hash = "sha256-pwFTl4Unr2ZIirAB3HTtfhL2YN7G/Pg88RX9AhKWXbE=";
|
||||
release."9.0.0+coq8.15".hash = "sha256-2oGOANn3XULHNIlyqjZ5ppQTQa2QF1zzf3YjHAd/pjo=";
|
||||
release."9.0.0+coq8.14".hash = "sha256-qTU152Dz34W6nFZ0pPbja9ouUm/714ZrLQ/Z4N/HIC4=";
|
||||
release."9.0.0+coq8.13".hash = "sha256-zvAqV3VAB7cN+nlMhjSXzxuDkdd387ju2VSb2EUthI0=";
|
||||
release."8.17.0".hash = "sha256-MXYjqN86+3O4hT2ql62U83T5H03E/8ysH8erpvC/oyw=";
|
||||
release."8.16.0".hash = "sha256-DH3iWwatPlhhCVYVlgL2WLkvneSVzSXUiKo2e0+1zR4=";
|
||||
release."8.15.0".hash = "sha256:093klwlhclgyrba1iv18dyz1qp5f0lwiaa7y0qwvgmai8rll5fns";
|
||||
release."8.14.0".hash = "sha256:0jsgdvj0ddhkls32krprp34r64y1rb5mwxl34fgaxk2k4664yq06";
|
||||
release."8.13.0".hash = "sha256:1n66i7hd9222b2ks606mak7m4f0dgy02xgygjskmmav6h7g2sx7y";
|
||||
release."8.12.0".hash = "sha256:14ijb3qy2hin3g4djx437jmnswxxq7lkfh3dwh9qvrds9a015yg8";
|
||||
release."8.11.0".hash = "sha256:1xcd7c7qlvs0narfba6px34zq0mz8rffnhxw0kzhhg6i4iw115dp";
|
||||
release."8.10.0".hash = "sha256:0bpb4flckn4nqxbs3wjiznyx1k7r8k93qdigp3qwmikp2lxvcbw5";
|
||||
release."8.9.0".hash = "sha256:03qz1w2xb2j5p06liz5yyafl0fl9vprcqm6j0iwi7rxwghl00p01";
|
||||
release."8.8.0".hash = "sha256:1ymxyrvjygscxkfj3qkq66skl3vdjhb670rzvsvgmwrjkrakjnfg";
|
||||
release."8.7.0".hash = "sha256:11c4sdmpd3l6jjl4v6k213z9fhrmmm1xnly3zmzam1wrrdif4ghl";
|
||||
release."8.6.0".rev = "v8.6.0";
|
||||
release."8.6.0".hash = "sha256:0553pcsy21cyhmns6k9qggzb67az8kl31d0lwlnz08bsqswigzrj";
|
||||
releaseRev = v: "${if lib.versions.isGe "9.0" v then "v" else "V"}${v}";
|
||||
|
||||
mlPlugin = true;
|
||||
|
||||
propagatedBuildInputs = [ stdlib ];
|
||||
|
||||
useCoqifVersion = v: v != null && v != "dev" && lib.versions.isLt "9.0.0+rocq" v;
|
||||
|
||||
meta = {
|
||||
license = lib.licenses.lgpl2;
|
||||
};
|
||||
|
||||
@@ -139,29 +139,21 @@ let
|
||||
propagatedBuildInputs = o.propagatedBuildInputs ++ [ stdlib ];
|
||||
}
|
||||
);
|
||||
patched-derivation4 = patched-derivation3.overrideAttrs (
|
||||
o:
|
||||
lib.optionalAttrs (o.version != null && (o.version == "dev" || lib.versions.isGe "2.5.0" o.version))
|
||||
{
|
||||
configurePhase = ''
|
||||
make dune-files || true
|
||||
'';
|
||||
buildPhase = ''
|
||||
dune build -p rocq-elpi @install ''${enableParallelBuilding:+-j $NIX_BUILD_CORES}
|
||||
'';
|
||||
installPhase = ''
|
||||
dune install --root . rocq-elpi --prefix=$out --libdir $OCAMLFIND_DESTDIR
|
||||
mkdir $out/lib/coq/
|
||||
mv $OCAMLFIND_DESTDIR/coq $out/lib/coq/${coq.coq-version}
|
||||
'';
|
||||
}
|
||||
);
|
||||
in
|
||||
# this is just a wrapper for rocqPackages.stdlib for Rocq >= 9.0
|
||||
if coq.rocqPackages ? rocq-elpi then
|
||||
coq.rocqPackages.rocq-elpi.override {
|
||||
inherit version elpi-version;
|
||||
inherit (coq.rocqPackages) rocq-core;
|
||||
}
|
||||
else
|
||||
patched-derivation4
|
||||
patched-derivation3.overrideAttrs (
|
||||
o:
|
||||
lib.optionalAttrs (o.version != null && (o.version == "dev" || lib.versions.isGe "2.5.0" o.version))
|
||||
{
|
||||
configurePhase = ''
|
||||
make dune-files || true
|
||||
'';
|
||||
buildPhase = ''
|
||||
dune build -p rocq-elpi @install ''${enableParallelBuilding:+-j $NIX_BUILD_CORES}
|
||||
'';
|
||||
installPhase = ''
|
||||
dune install --root . rocq-elpi --prefix=$out --libdir $OCAMLFIND_DESTDIR
|
||||
mkdir $out/lib/coq/
|
||||
mv $OCAMLFIND_DESTDIR/coq $out/lib/coq/${coq.coq-version}
|
||||
'';
|
||||
}
|
||||
)
|
||||
@@ -49,7 +49,7 @@ mkCoqDerivation {
|
||||
|
||||
propagatedBuildInputs = [
|
||||
mathcomp.boot
|
||||
mathcomp.fingroup
|
||||
mathcomp.finite-group
|
||||
mathcomp.algebra
|
||||
];
|
||||
|
||||
@@ -46,7 +46,7 @@ mkCoqDerivation {
|
||||
|
||||
propagatedBuildInputs = [
|
||||
mathcomp.boot
|
||||
mathcomp.fingroup
|
||||
mathcomp.finite-group
|
||||
mathcomp.algebra
|
||||
stdlib
|
||||
];
|
||||
@@ -51,7 +51,7 @@ mkCoqDerivation {
|
||||
propagatedBuildInputs = [
|
||||
mathcomp.algebra
|
||||
mathcomp-finmap
|
||||
mathcomp.fingroup
|
||||
mathcomp.finite-group
|
||||
fourcolor
|
||||
stdlib
|
||||
]
|
||||
@@ -20,16 +20,38 @@ let
|
||||
(case (range "9.0" "9.3") "1.10.3")
|
||||
(case (range "9.0" "9.1") "1.10.2")
|
||||
(case (range "9.0" "9.1") "1.10.0")
|
||||
(case (range "9.0" "9.1") "1.9.1")
|
||||
(case (range "8.20" "9.1") "1.9.1")
|
||||
(case (range "8.19" "8.20") "1.8.0")
|
||||
(case (range "8.18" "8.20") "1.7.1")
|
||||
(case (range "8.16" "8.18") "1.6.0")
|
||||
(case (range "8.15" "8.18") "1.5.0")
|
||||
(case (range "8.15" "8.17") "1.4.0")
|
||||
(case (range "8.13" "8.14") "1.2.0")
|
||||
(case (range "8.12" "8.13") "1.1.0")
|
||||
(case (isEq "8.11") "0.10.0")
|
||||
] null;
|
||||
release."1.10.3".hash = "sha256-y13KxzLulIu39Ci3aMc1cZG4tw3LL2ab7U9snI6jrXc=";
|
||||
release."1.10.2".sha256 = "sha256-Uzni9qrYQP45Tr+JkHs0BuRARwmWSMwA/iHhIzkolxc=";
|
||||
release."1.10.0".sha256 = "sha256-c52nS8I0tia7Q8lZTFJyHVPVabW9xv55m7w6B7y3+e8=";
|
||||
release."1.9.1".sha256 = "sha256-AiS0ezMyfIYlXnuNsVLz1GlKQZzJX+ilkrKkbo0GrF0=";
|
||||
release."1.8.0".hash = "sha256-4s/4ZZKj5tiTtSHGIM8Op/Pak4Vp52WVOpd4l9m19fY=";
|
||||
release."1.7.1".hash = "sha256-MCmOzMh/SBTFAoPbbIQ7aqd3hMcSMpAKpiZI7dbRaGs=";
|
||||
release."1.7.0".hash = "sha256-WqSeuJhmqicJgXw/xGjGvbRzfyOK7rmkVRb6tPDTAZg=";
|
||||
release."1.6.0".hash = "sha256-E8s20veOuK96knVQ7rEDSt8VmbtYfPgItD0dTY/mckg=";
|
||||
release."1.5.0".hash = "sha256-Lia3o156Pbe8rDHOA1IniGYsG5/qzZkzDKdHecfmS+c=";
|
||||
release."1.4.0".hash = "sha256-tOed9UU3kMw6KWHJ5LVLUFEmzHx1ImutXQvZ0ldW9rw=";
|
||||
release."1.3.0".hash = "sha256:17k7rlxdx43qda6i1yafpgc64na8br285cb0mbxy5wryafcdrkrc";
|
||||
release."1.2.1".hash = "sha256-pQYZJ34YzvdlRSGLwsrYgPdz3p/l5f+KhJjkYT08Mj0=";
|
||||
release."1.2.0".hash = "sha256:0sk01rvvk652d86aibc8rik2m8iz7jn6mw9hh6xkbxlsvh50719d";
|
||||
release."1.1.0".hash = "sha256-spno5ty4kU4WWiOfzoqbXF8lWlNSlySWcRReR3zE/4Q=";
|
||||
release."1.0.0".hash = "sha256:0yykygs0z6fby6vkiaiv3azy1i9yx4rqg8xdlgkwnf2284hffzpp";
|
||||
release."0.10.0".hash = "sha256:1a3vry9nzavrlrdlq3cys3f8kpq3bz447q8c4c7lh2qal61wb32h";
|
||||
releaseRev = v: "v${v}";
|
||||
|
||||
propagatedBuildInputs = [ rocq-elpi ];
|
||||
|
||||
useCoqifVersion = v: v != null && v != "dev" && lib.versions.isLe "1.9.1" v;
|
||||
|
||||
meta = {
|
||||
description = "High level commands to declare a hierarchy based on packed classes";
|
||||
maintainers = with lib.maintainers; [
|
||||
@@ -39,8 +61,19 @@ let
|
||||
license = lib.licenses.mit;
|
||||
};
|
||||
};
|
||||
hb2 = hb.overrideAttrs (
|
||||
o:
|
||||
lib.optionalAttrs (lib.versions.isGe "1.2.0" o.version || o.version == "dev") {
|
||||
buildPhase = "make build";
|
||||
}
|
||||
// (
|
||||
if lib.versions.range "1.1.0" "1.9.1" o.version then
|
||||
{ installFlags = [ "DESTDIR=$(out)" ] ++ o.installFlags; }
|
||||
else if lib.versions.range "0.10.0" "1.1.0" o.version then
|
||||
{ installFlags = [ "VFILES=structures.v" ] ++ o.installFlags; }
|
||||
else
|
||||
{ }
|
||||
)
|
||||
);
|
||||
in
|
||||
hb.overrideAttrs (
|
||||
o:
|
||||
lib.optionalAttrs (o.version == "1.9.1") { installFlags = [ "DESTDIR=$(out)" ] ++ o.installFlags; }
|
||||
)
|
||||
hb2
|
||||
|
||||
@@ -1,45 +1,62 @@
|
||||
{
|
||||
lib,
|
||||
mkRocqDerivation,
|
||||
stdlib,
|
||||
rocq-core,
|
||||
stdpp,
|
||||
version ? null,
|
||||
}:
|
||||
|
||||
mkRocqDerivation {
|
||||
pname = "iris";
|
||||
domain = "gitlab.mpi-sws.org";
|
||||
owner = "iris";
|
||||
inherit version;
|
||||
defaultVersion =
|
||||
let
|
||||
case = case: out: { inherit case out; };
|
||||
in
|
||||
with lib.versions;
|
||||
lib.switch rocq-core.rocq-version [
|
||||
(case (range "9.0" "9.3") "4.5.0")
|
||||
] null;
|
||||
release."4.5.0".sha256 = "sha256-oGqo+W1prLtAwRwo2U15VGhmrkDIPPE6uMbNrTa8iAQ=";
|
||||
releaseRev = v: "iris-${v}";
|
||||
let
|
||||
derivation = mkRocqDerivation {
|
||||
pname = "iris";
|
||||
domain = "gitlab.mpi-sws.org";
|
||||
owner = "iris";
|
||||
inherit version;
|
||||
defaultVersion =
|
||||
let
|
||||
case = case: out: { inherit case out; };
|
||||
in
|
||||
with lib.versions;
|
||||
lib.switch rocq-core.rocq-version [
|
||||
(case (range "9.0" "9.3") "4.5.0")
|
||||
(case (range "8.19" "9.1") "4.4.0")
|
||||
(case (range "8.18" "8.19") "4.2.0")
|
||||
(case (range "8.16" "8.18") "4.1.0")
|
||||
(case (range "8.13" "8.17") "4.0.0")
|
||||
(case (range "8.12" "8.14") "3.5.0")
|
||||
(case (range "8.11" "8.13") "3.4.0")
|
||||
(case (range "8.9" "8.10") "3.3.0")
|
||||
] null;
|
||||
release."4.5.0".sha256 = "sha256-oGqo+W1prLtAwRwo2U15VGhmrkDIPPE6uMbNrTa8iAQ=";
|
||||
release."4.4.0".hash = "sha256-zpuaIdH2ScOuZB0Vt1TEHAbsmcT1DyoDsJpftT1M7qw=";
|
||||
release."4.3.0".hash = "sha256-3qhjiFI+A3I3fD8rFfJL5Hek77wScfn/FNNbDyGqA1k=";
|
||||
release."4.2.0".hash = "sha256-HuiHIe+5letgr1NN1biZZFq0qlWUbFmoVI7Q91+UIfM=";
|
||||
release."4.1.0".hash = "sha256-nTZUeZOXiH7HsfGbMKDE7vGrNVCkbMaWxdMWUcTUNlo=";
|
||||
release."4.0.0".hash = "sha256-Jc9TmgGvkiDaz9IOoExyeryU1E+Q37GN24NIM397/Gg=";
|
||||
release."3.6.0".hash = "sha256:02vbq597fjxd5znzxdb54wfp36412wz2d4yash4q8yddgl1kakmj";
|
||||
release."3.5.0".hash = "sha256:0hh14m0anfcv65rxm982ps2vp95vk9fwrpv4br8bxd9vz0091d70";
|
||||
release."3.4.0".hash = "sha256:0vdc2mdqn5jjd6yz028c0c6blzrvpl0c7apx6xas7ll60136slrb";
|
||||
release."3.3.0".hash = "sha256:0az4gkp5m8sq0p73dlh0r7ckkzhk7zkg5bndw01bdsy5ywj0vilp";
|
||||
releaseRev = v: "iris-${v}";
|
||||
|
||||
propagatedBuildInputs = [
|
||||
stdlib
|
||||
stdpp
|
||||
];
|
||||
propagatedBuildInputs = [ stdpp ];
|
||||
|
||||
preBuild = ''
|
||||
if [[ -f coq-lint.sh ]]
|
||||
then patchShebangs coq-lint.sh
|
||||
fi
|
||||
'';
|
||||
preBuild = ''
|
||||
if [[ -f coq-lint.sh ]]
|
||||
then patchShebangs coq-lint.sh
|
||||
fi
|
||||
'';
|
||||
|
||||
meta = {
|
||||
description = "Rocq development of the Iris Project";
|
||||
license = lib.licenses.bsd3;
|
||||
maintainers = [
|
||||
lib.maintainers.vbgl
|
||||
lib.maintainers.ineol
|
||||
];
|
||||
useCoqifVersion = v: v != null && v != "dev" && lib.versions.isLe "4.4.0" v;
|
||||
|
||||
meta = {
|
||||
description = "Rocq development of the Iris Project";
|
||||
license = lib.licenses.bsd3;
|
||||
maintainers = [
|
||||
lib.maintainers.vbgl
|
||||
lib.maintainers.ineol
|
||||
];
|
||||
};
|
||||
};
|
||||
}
|
||||
in
|
||||
derivation
|
||||
|
||||
Some files were not shown because too many files have changed in this diff Show More
Reference in New Issue
Block a user