nixpkgs/pkgs/development/coq-modules/coqeal/default.nix

{ coq, mkCoqDerivation, mathcomp, bignums, paramcoq, multinomials,
  mathcomp-real-closed,
  lib, version ? null }:

(mkCoqDerivation {

  pname = "CoqEAL";

  inherit version;
  defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp.version ]  [
      { cases = [ (range "8.13" "8.16") (isGe "1.13.0") ]; out = "1.1.1"; }
      { cases = [ (range "8.10" "8.15") (isGe "1.12.0") ]; out = "1.1.0"; }
      { cases = [ (isGe "8.10") (range "1.11.0" "1.12.0") ]; out = "1.0.5"; }
      { cases = [ (isGe "8.7") "1.11.0" ]; out = "1.0.4"; }
      { cases = [ (isGe "8.7") "1.10.0" ]; out = "1.0.3"; }
    ] null;

  release."1.1.1".sha256 = "sha256-ExAdC3WuArNxS+Sa1r4x5aT7ylbCvP/BZXfkdQNAvZ8=";
  release."1.1.0".sha256 = "1vyhfna5frkkq2fl1fkg2mwzpg09k3sbzxxpyp14fjay81xajrxr";
  release."1.0.6".sha256 = "0lqkyfj4qbq8wr3yk8qgn7mclw582n3fjl9l19yp8cnchspzywx0";
  release."1.0.5".sha256 = "0cmvky8glb5z2dy3q62aln6qbav4lrf2q1589f6h1gn5bgjrbzkm";
  release."1.0.4".sha256 = "1g5m26lr2lwxh6ld2gykailhay4d0ayql4bfh0aiwqpmmczmxipk";
  release."1.0.3".sha256 = "0hc63ny7phzbihy8l7wxjvn3haxx8jfnhi91iw8hkq8n29i23v24";

  propagatedBuildInputs = [ mathcomp.algebra bignums paramcoq multinomials ];

  meta = {
    description = "CoqEAL - The Coq Effective Algebra Library";
    license = lib.licenses.mit;
  };
}).overrideAttrs (o: {
  propagatedBuildInputs = o.propagatedBuildInputs
  ++ lib.optional (lib.versions.isGe "1.1" o.version || o.version == "dev") mathcomp-real-closed;
})
coqPackages: refactor 2020-08-28 21:05:46 +00:00			`{ coq, mkCoqDerivation, mathcomp, bignums, paramcoq, multinomials,`
coqPackages.coqeal: master, add dependency In order to include matrix normal forms in CoqEAL (https://github.com/coq-community/coqeal/pull/54) we add a dependency to mathcomp-real-closed. 2021-10-25 13:20:28 +00:00			`mathcomp-real-closed,`
coqPackages: etc - put `findlib` in `buildInputs` of `mkCoqDerivation` to make sure `coq` packages find their ocaml plugin dependencies, - use `propagatedBuildInputs` to make sure ocaml plugin dependencies are in path, - updated `coqPackage.heq` (broken url), - fixed use of `DESTDIR` and `COQMF_COQLIB` in mkCoqDerivation, - adding `COQCORELIB` environement variable to put ocaml plugin files in the right place, - make `metaFetch` available from `coqPackages` 2021-02-19 18:34:30 +00:00			`lib, version ? null }:`
coqPackages: refactor 2020-08-28 21:05:46 +00:00
coqPackages.coqeal: master, add dependency In order to include matrix normal forms in CoqEAL (https://github.com/coq-community/coqeal/pull/54) we add a dependency to mathcomp-real-closed. 2021-10-25 13:20:28 +00:00			`(mkCoqDerivation {`
coqPackages: refactor 2020-08-28 21:05:46 +00:00
			`pname = "CoqEAL";`
coqPackages.mathcomp: 1.12.0 -> 1.13.0 2021-10-28 14:17:24 +00:00
coqPackages: refactor 2020-08-28 21:05:46 +00:00			`inherit version;`
treewide: remove global with lib; statements in pkgs/coq-modules 2023-01-21 22:19:48 +00:00			`defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp.version ] [`
coqPackages.coqeal: enable for Coq 8.16 2022-09-08 16:06:52 +00:00			`{ cases = [ (range "8.13" "8.16") (isGe "1.13.0") ]; out = "1.1.1"; }`
Adapt to Coq 8.15 and MathCOmp 1.14 2022-01-27 18:16:20 +00:00			`{ cases = [ (range "8.10" "8.15") (isGe "1.12.0") ]; out = "1.1.0"; }`
coqPackages.coqeal: 1.0.4 → 1.0.5 2021-04-29 06:24:35 +00:00			`{ cases = [ (isGe "8.10") (range "1.11.0" "1.12.0") ]; out = "1.0.5"; }`
coqPackages: refactor 2020-08-28 21:05:46 +00:00			`{ cases = [ (isGe "8.7") "1.11.0" ]; out = "1.0.4"; }`
			`{ cases = [ (isGe "8.7") "1.10.0" ]; out = "1.0.3"; }`
			`] null;`

coqPackages.coqeal: 1.1.0 → 1.1.1 2022-07-08 13:30:10 +00:00			`release."1.1.1".sha256 = "sha256-ExAdC3WuArNxS+Sa1r4x5aT7ylbCvP/BZXfkdQNAvZ8=";`
coqPackages.coqeal: 1.0.6 -> 1.1.0 2021-11-05 10:26:23 +00:00			`release."1.1.0".sha256 = "1vyhfna5frkkq2fl1fkg2mwzpg09k3sbzxxpyp14fjay81xajrxr";`
coqPackages.coqeal: 1.0.5 → 1.0.6 2021-08-06 09:42:07 +00:00			`release."1.0.6".sha256 = "0lqkyfj4qbq8wr3yk8qgn7mclw582n3fjl9l19yp8cnchspzywx0";`
coqPackages.coqeal: 1.0.4 → 1.0.5 2021-04-29 06:24:35 +00:00			`release."1.0.5".sha256 = "0cmvky8glb5z2dy3q62aln6qbav4lrf2q1589f6h1gn5bgjrbzkm";`
coqPackages: refactor 2020-08-28 21:05:46 +00:00			`release."1.0.4".sha256 = "1g5m26lr2lwxh6ld2gykailhay4d0ayql4bfh0aiwqpmmczmxipk";`
			`release."1.0.3".sha256 = "0hc63ny7phzbihy8l7wxjvn3haxx8jfnhi91iw8hkq8n29i23v24";`

			`propagatedBuildInputs = [ mathcomp.algebra bignums paramcoq multinomials ];`

			`meta = {`
			`description = "CoqEAL - The Coq Effective Algebra Library";`
treewide: remove global with lib; statements in pkgs/coq-modules 2023-01-21 22:19:48 +00:00			`license = lib.licenses.mit;`
coqPackages: refactor 2020-08-28 21:05:46 +00:00			`};`
coqPackages.coqeal: master, add dependency In order to include matrix normal forms in CoqEAL (https://github.com/coq-community/coqeal/pull/54) we add a dependency to mathcomp-real-closed. 2021-10-25 13:20:28 +00:00			`}).overrideAttrs (o: {`
			`propagatedBuildInputs = o.propagatedBuildInputs`
treewide: remove global with lib; statements in pkgs/coq-modules 2023-01-21 22:19:48 +00:00			`++ lib.optional (lib.versions.isGe "1.1" o.version \|\| o.version == "dev") mathcomp-real-closed;`
coqPackages.coqeal: master, add dependency In order to include matrix normal forms in CoqEAL (https://github.com/coq-community/coqeal/pull/54) we add a dependency to mathcomp-real-closed. 2021-10-25 13:20:28 +00:00			`})`