diff options
Diffstat (limited to 'pkgs/development/coq-modules')
43 files changed, 139 insertions, 113 deletions
diff --git a/pkgs/development/coq-modules/CoLoR/default.nix b/pkgs/development/coq-modules/CoLoR/default.nix index 618ba3fd0a46e..6e59dda15a6a4 100644 --- a/pkgs/development/coq-modules/CoLoR/default.nix +++ b/pkgs/development/coq-modules/CoLoR/default.nix @@ -29,7 +29,7 @@ mkCoqDerivation { meta = { homepage = "https://github.com/fblanqui/color"; - description = "CoLoR is a library of formal mathematical definitions and proofs of theorems on rewriting theory and termination whose correctness has been mechanically checked by the Coq proof assistant."; + description = "CoLoR is a library of formal mathematical definitions and proofs of theorems on rewriting theory and termination whose correctness has been mechanically checked by the Coq proof assistant"; maintainers = with lib.maintainers; [ jpas jwiegley ]; }; } diff --git a/pkgs/development/coq-modules/HoTT/default.nix b/pkgs/development/coq-modules/HoTT/default.nix index 426880940070b..6bc8ad9bb1804 100644 --- a/pkgs/development/coq-modules/HoTT/default.nix +++ b/pkgs/development/coq-modules/HoTT/default.nix @@ -27,7 +27,7 @@ mkCoqDerivation { meta = { homepage = "https://homotopytypetheory.org/"; - description = "The Homotopy Type Theory library"; + description = "Homotopy Type Theory library"; longDescription = '' Homotopy Type Theory is an interpretation of Martin-Löf’s intensional type theory into abstract homotopy theory. Propositional equality is diff --git a/pkgs/development/coq-modules/ITree/default.nix b/pkgs/development/coq-modules/ITree/default.nix index c886dfd149812..3eaa6eec67a49 100644 --- a/pkgs/development/coq-modules/ITree/default.nix +++ b/pkgs/development/coq-modules/ITree/default.nix @@ -15,7 +15,7 @@ mkCoqDerivation rec { releaseRev = v: "${v}"; propagatedBuildInputs = [ coq-ext-lib paco ]; meta = { - description = "A Library for Representing Recursive and Impure Programs in Coq"; + description = "Library for Representing Recursive and Impure Programs in Coq"; maintainers = with lib.maintainers; [ larsr ]; }; } diff --git a/pkgs/development/coq-modules/VST/default.nix b/pkgs/development/coq-modules/VST/default.nix index 706d117863540..8cfe5e9f764e9 100644 --- a/pkgs/development/coq-modules/VST/default.nix +++ b/pkgs/development/coq-modules/VST/default.nix @@ -43,7 +43,7 @@ mkCoqDerivation { preConfigure = '' patchShebangs util substituteInPlace Makefile \ - --replace 'COQVERSION= ' 'COQVERSION= 8.17.1 or-else 8.16.1 or-else 8.16.0 or-else 8.15.2 or-else 8.15.1 or-else '\ + --replace 'COQVERSION= ' 'COQVERSION= 8.19.2 or-else 8.17.1 or-else 8.16.1 or-else 8.16.0 or-else 8.15.2 or-else 8.15.1 or-else '\ --replace 'FLOYD_FILES=' 'FLOYD_FILES= ${toString extra_floyd_files}' ''; diff --git a/pkgs/development/coq-modules/VplTactic/default.nix b/pkgs/development/coq-modules/VplTactic/default.nix index e62499eb1ac82..b907a10498e72 100644 --- a/pkgs/development/coq-modules/VplTactic/default.nix +++ b/pkgs/development/coq-modules/VplTactic/default.nix @@ -13,6 +13,6 @@ mkCoqDerivation { mlPlugin = true; meta = Vpl.meta // { - description = "A Coq Tactic for Arithmetic (based on VPL)"; + description = "Coq Tactic for Arithmetic (based on VPL)"; }; } diff --git a/pkgs/development/coq-modules/aac-tactics/default.nix b/pkgs/development/coq-modules/aac-tactics/default.nix index 73d14282a3ab5..59a9c9ba11642 100644 --- a/pkgs/development/coq-modules/aac-tactics/default.nix +++ b/pkgs/development/coq-modules/aac-tactics/default.nix @@ -5,6 +5,7 @@ mkCoqDerivation { releaseRev = v: "v${v}"; + release."8.19.1".sha256 = "sha256-W/V57h+rjb3m0ktCG83PquMHfXiv6H1Nhvw9sVEPLqM="; release."8.19.0".sha256 = "sha256-IeCBd8gcu4bAXH5I/XIT7neQIILi+EWR6qqAA4GzQD0="; release."8.18.0".sha256 = "sha256-Vpe79qCyFLOdOtFFvLKR0N+MMpGD661Q01yx4gxRhZo="; release."8.17.0".sha256 = "sha256-c8DtD21QFDZEVyCQc7ScPZEMTmolxlT3+Db3gStofF8="; @@ -24,7 +25,7 @@ mkCoqDerivation { inherit version; defaultVersion = with lib.versions; lib.switch coq.coq-version [ - { case = "8.19"; out = "8.19.0"; } + { case = "8.19"; out = "8.19.1"; } { case = "8.18"; out = "8.18.0"; } { case = "8.17"; out = "8.17.0"; } { case = "8.16"; out = "8.16.0"; } diff --git a/pkgs/development/coq-modules/category-theory/default.nix b/pkgs/development/coq-modules/category-theory/default.nix index dc0bd6cfcadc3..568a7fa2e73b2 100644 --- a/pkgs/development/coq-modules/category-theory/default.nix +++ b/pkgs/development/coq-modules/category-theory/default.nix @@ -27,7 +27,7 @@ mkCoqDerivation { propagatedBuildInputs = [ ssreflect equations ]; meta = { - description = "A formalization of category theory in Coq for personal study and practical work"; + description = "Formalization of category theory in Coq for personal study and practical work"; maintainers = with lib.maintainers; [ jwiegley ]; }; } diff --git a/pkgs/development/coq-modules/compcert/default.nix b/pkgs/development/coq-modules/compcert/default.nix index 0557311c36507..59cfd680427b6 100644 --- a/pkgs/development/coq-modules/compcert/default.nix +++ b/pkgs/development/coq-modules/compcert/default.nix @@ -1,4 +1,4 @@ -{ lib, fetchzip, mkCoqDerivation +{ lib, mkCoqDerivation , coq, flocq, compcert , ocamlPackages, fetchpatch, makeWrapper, coq2html , stdenv, tools ? stdenv.cc @@ -193,6 +193,20 @@ compcert.overrideAttrs (o: url = "https://github.com/AbsInt/CompCert/commit/a2e4ed62fc558d565366845f9d135bd7db5e23c4.patch"; hash = "sha256-ufk0bokuayLfkSvK3cK4E9iXU5eZpp9d/ETSa/zCfMg="; }) + # Support for Coq 8.19.2 + (fetchpatch { + url = "https://github.com/AbsInt/CompCert/commit/8fcfb7d2a6e9ba44003ccab0dfcc894982779af1.patch"; + hash = "sha256-m/kcnDBBPWFriipuGvKZUqLQU8/W1uqw8j4qfCwnTZk="; + }) + ]; + } + { cases = [ (isEq "8.19") (isEq "3.14") ]; + out = [ + # Support for Coq 8.19.2 + (fetchpatch { + url = "https://github.com/AbsInt/CompCert/commit/8fcfb7d2a6e9ba44003ccab0dfcc894982779af1.patch"; + hash = "sha256-m/kcnDBBPWFriipuGvKZUqLQU8/W1uqw8j4qfCwnTZk="; + }) ]; } ] []; diff --git a/pkgs/development/coq-modules/coq-bits/default.nix b/pkgs/development/coq-modules/coq-bits/default.nix index ebc03a3a7306f..cadf18df73113 100644 --- a/pkgs/development/coq-modules/coq-bits/default.nix +++ b/pkgs/development/coq-modules/coq-bits/default.nix @@ -15,7 +15,7 @@ mkCoqDerivation { propagatedBuildInputs = [ mathcomp.algebra ]; meta = with lib; { - description = "A formalization of bitset operations in Coq"; + description = "Formalization of bitset operations in Coq"; license = licenses.asl20; maintainers = with maintainers; [ ptival ]; }; diff --git a/pkgs/development/coq-modules/coq-elpi/default.nix b/pkgs/development/coq-modules/coq-elpi/default.nix index db82458f4a20f..fe577a149d716 100644 --- a/pkgs/development/coq-modules/coq-elpi/default.nix +++ b/pkgs/development/coq-modules/coq-elpi/default.nix @@ -1,6 +1,6 @@ { lib, mkCoqDerivation, which, coq, version ? null }: -with builtins; with lib; let +let elpi = coq.ocamlPackages.elpi.override (lib.switch coq.coq-version [ { case = "8.11"; out = { version = "1.11.4"; };} { case = "8.12"; out = { version = "1.12.0"; };} @@ -70,8 +70,8 @@ in mkCoqDerivation { propagatedBuildInputs = [ coq.ocamlPackages.findlib elpi ]; meta = { - description = "Coq plugin embedding ELPI."; - maintainers = [ maintainers.cohencyril ]; - license = licenses.lgpl21Plus; + description = "Coq plugin embedding ELPI"; + maintainers = [ lib.maintainers.cohencyril ]; + license = lib.licenses.lgpl21Plus; }; } diff --git a/pkgs/development/coq-modules/coq-ext-lib/default.nix b/pkgs/development/coq-modules/coq-ext-lib/default.nix index 9eaebbb646d15..f4459ef29b784 100644 --- a/pkgs/development/coq-modules/coq-ext-lib/default.nix +++ b/pkgs/development/coq-modules/coq-ext-lib/default.nix @@ -31,7 +31,7 @@ mkCoqDerivation rec { releaseRev = v: "v${v}"; meta = { - description = "A collection of theories and plugins that may be useful in other Coq developments"; + description = "Collection of theories and plugins that may be useful in other Coq developments"; maintainers = with lib.maintainers; [ jwiegley ptival ]; }; } diff --git a/pkgs/development/coq-modules/coq-haskell/default.nix b/pkgs/development/coq-modules/coq-haskell/default.nix index 028b4c5025eb2..7ffc29e943bda 100644 --- a/pkgs/development/coq-modules/coq-haskell/default.nix +++ b/pkgs/development/coq-modules/coq-haskell/default.nix @@ -15,7 +15,7 @@ mkCoqDerivation { enableParallelBuilding = false; meta = { - description = "A library for formalizing Haskell types and functions in Coq"; + description = "Library for formalizing Haskell types and functions in Coq"; maintainers = with lib.maintainers; [ jwiegley ]; }; } diff --git a/pkgs/development/coq-modules/coq-lsp/default.nix b/pkgs/development/coq-modules/coq-lsp/default.nix index afa42728bb59c..8a031ba84d7af 100644 --- a/pkgs/development/coq-modules/coq-lsp/default.nix +++ b/pkgs/development/coq-modules/coq-lsp/default.nix @@ -8,16 +8,16 @@ mkCoqDerivation rec { useDune = true; release."0.1.8+8.16".sha256 = "sha256-dEEAK5IXGjHB8D/fYJRQG/oCotoXJuWLxXB0GQlY2eo="; - release."0.1.8+8.17".sha256 = "sha256-TmaE+osn/yAPU1Dyni/UTd5w/L2+qyPE3H/g6IWvHLQ="; - release."0.1.8+8.18".sha256 = "sha256-UYmiDdbax4wxp5dLia/1t1gFyK6UELtJJvDMd5Hd14s="; - release."0.1.8+8.19".sha256 = "sha256-aO3hUAWEqVxvCF7uJs+S4yrRxSMe/GaLKVfW/vawzNs="; + release."0.1.9+8.17".sha256 = "sha256-BCsVRKSE9txeKgDfTsu7hQ6MebC+dX2AAqDF9iL7bYE="; + release."0.1.9+8.18".sha256 = "sha256-elAXvkyqw/R/EziGn+QdPn42t5rqTVVW08BXGP3HimY="; + release."0.1.9+8.19".sha256 = "sha256-0bk0o25aYkrRf5zaWZnNJqqoBZ6u8nSV9QDIWCeFEco="; inherit version; defaultVersion = with lib.versions; lib.switch coq.coq-version [ { case = isEq "8.16"; out = "0.1.8+8.16"; } - { case = isEq "8.17"; out = "0.1.8+8.17"; } - { case = isEq "8.18"; out = "0.1.8+8.18"; } - { case = isEq "8.19"; out = "0.1.8+8.19"; } + { case = isEq "8.17"; out = "0.1.9+8.17"; } + { case = isEq "8.18"; out = "0.1.9+8.18"; } + { case = isEq "8.19"; out = "0.1.9+8.19"; } ] null; nativeBuildInputs = [ makeWrapper ]; diff --git a/pkgs/development/coq-modules/coq-record-update/default.nix b/pkgs/development/coq-modules/coq-record-update/default.nix index d65a486476a0a..b9a295617b8c2 100644 --- a/pkgs/development/coq-modules/coq-record-update/default.nix +++ b/pkgs/development/coq-modules/coq-record-update/default.nix @@ -5,8 +5,9 @@ owner = "tchajed"; inherit version; defaultVersion = with lib.versions; lib.switch coq.coq-version [ - { case = range "8.10" "8.19"; out = "0.3.3"; } + { case = range "8.10" "8.19"; out = "0.3.4"; } ] null; + release."0.3.4".sha256 = "sha256-AhEcugUiVIsgbq884Lur/bQIuGw8prk+3AlNkP1omcw="; release."0.3.3".sha256 = "sha256-HDIPeFHiC9EwhiOH7yMGJ9d2zJMhboTpRGf9kWcB9Io="; release."0.3.1".sha256 = "sha256-DyGxO2tqmYZZluXN6Oy5Tw6fuLMyuyxonj8CCToWKkk="; release."0.3.0".sha256 = "1ffr21dd6hy19gxnvcd4if2450iksvglvkd6q5713fajd72hmc0z"; diff --git a/pkgs/development/coq-modules/coqide/default.nix b/pkgs/development/coq-modules/coqide/default.nix index 449e81040dfa9..a4b85cdd7fbbe 100644 --- a/pkgs/development/coq-modules/coqide/default.nix +++ b/pkgs/development/coq-modules/coqide/default.nix @@ -54,7 +54,7 @@ mkCoqDerivation rec { meta = with lib; { homepage = "https://coq.inria.fr"; - description = "The CoqIDE user interface for the Coq proof assistant"; + description = "CoqIDE user interface for the Coq proof assistant"; mainProgram = "coqide"; license = licenses.lgpl21Plus; maintainers = [ maintainers.Zimmi48 ]; diff --git a/pkgs/development/coq-modules/coquelicot/default.nix b/pkgs/development/coq-modules/coquelicot/default.nix index 4ce063339f073..76fb985c2c017 100644 --- a/pkgs/development/coq-modules/coquelicot/default.nix +++ b/pkgs/development/coq-modules/coquelicot/default.nix @@ -29,7 +29,7 @@ mkCoqDerivation { meta = with lib; { homepage = "http://coquelicot.saclay.inria.fr/"; - description = "A Coq library for Reals"; + description = "Coq library for Reals"; license = licenses.lgpl3; maintainers = [ maintainers.vbgl ]; }; diff --git a/pkgs/development/coq-modules/corn/default.nix b/pkgs/development/coq-modules/corn/default.nix index 5e72d4a97e2a4..aee2f35d9e183 100644 --- a/pkgs/development/coq-modules/corn/default.nix +++ b/pkgs/development/coq-modules/corn/default.nix @@ -27,7 +27,7 @@ mkCoqDerivation rec { meta = with lib; { homepage = "http://c-corn.github.io/"; license = licenses.gpl2; - description = "A Coq library for constructive analysis"; + description = "Coq library for constructive analysis"; maintainers = [ maintainers.vbgl ]; }; } diff --git a/pkgs/development/coq-modules/equations/default.nix b/pkgs/development/coq-modules/equations/default.nix index 961b54f6a4dbd..83662720c7f72 100644 --- a/pkgs/development/coq-modules/equations/default.nix +++ b/pkgs/development/coq-modules/equations/default.nix @@ -68,7 +68,7 @@ meta = with lib; { homepage = "https://mattam82.github.io/Coq-Equations/"; - description = "A plugin for Coq to add dependent pattern-matching"; + description = "Plugin for Coq to add dependent pattern-matching"; maintainers = with maintainers; [ jwiegley ]; }; }).overrideAttrs (o: { diff --git a/pkgs/development/coq-modules/fiat/HEAD.nix b/pkgs/development/coq-modules/fiat/HEAD.nix index 0a6375907e899..63cc17fbbdd2f 100644 --- a/pkgs/development/coq-modules/fiat/HEAD.nix +++ b/pkgs/development/coq-modules/fiat/HEAD.nix @@ -28,7 +28,7 @@ mkCoqDerivation rec { meta = { homepage = "http://plv.csail.mit.edu/fiat/"; - description = "A library for the Coq proof assistant for synthesizing efficient correct-by-construction programs from declarative specifications"; + description = "Library for the Coq proof assistant for synthesizing efficient correct-by-construction programs from declarative specifications"; maintainers = with lib.maintainers; [ jwiegley ]; }; } diff --git a/pkgs/development/coq-modules/flocq/default.nix b/pkgs/development/coq-modules/flocq/default.nix index 8be0213a46eb4..34c79818642b0 100644 --- a/pkgs/development/coq-modules/flocq/default.nix +++ b/pkgs/development/coq-modules/flocq/default.nix @@ -29,7 +29,7 @@ mkCoqDerivation { useMelquiondRemake.logpath = "Flocq"; meta = with lib; { - description = "A floating-point formalization for the Coq system"; + description = "Floating-point formalization for the Coq system"; license = licenses.lgpl3; maintainers = with maintainers; [ jwiegley ]; }; diff --git a/pkgs/development/coq-modules/goedel/default.nix b/pkgs/development/coq-modules/goedel/default.nix index 1b16f8c3948a5..2dae5941197d1 100644 --- a/pkgs/development/coq-modules/goedel/default.nix +++ b/pkgs/development/coq-modules/goedel/default.nix @@ -17,7 +17,7 @@ mkCoqDerivation { propagatedBuildInputs = [ hydra-battles pocklington ]; meta = with lib; { - description = "The Gödel-Rosser 1st incompleteness theorem in Coq"; + description = "Gödel-Rosser 1st incompleteness theorem in Coq"; maintainers = with maintainers; [ siraben ]; license = licenses.mit; platforms = platforms.unix; diff --git a/pkgs/development/coq-modules/graph-theory/default.nix b/pkgs/development/coq-modules/graph-theory/default.nix index 0d28bbc0527f0..6554b811f4b95 100644 --- a/pkgs/development/coq-modules/graph-theory/default.nix +++ b/pkgs/development/coq-modules/graph-theory/default.nix @@ -8,12 +8,14 @@ mkCoqDerivation { release."0.9.1".sha256 = "sha256-lRRY+501x+DqNeItBnbwYIqWLDksinWIY4x/iojRNYU="; release."0.9.2".sha256 = "sha256-DPYCZS8CzkfgpR+lmYhV2v20ezMtyWp8hdWpuh0OOQU="; release."0.9.3".sha256 = "sha256-9WX3gsw+4btJLqcGg2W+7Qy+jaZtkfw7vCp8sXYmaWw="; + release."0.9.4".sha256 = "sha256-fXTAsRdPisNhg8Umaa7S7gZ1M8zuPGg426KP9fAkmXQ="; releaseRev = v: "v${v}"; inherit version; defaultVersion = with lib.versions; lib.switch [ coq.coq-version mathcomp.version ] [ - { cases = [ (isGe "8.16") (range "2.0.0" "2.1.0") ]; out = "0.9.3"; } + { cases = [ (isGe "8.16") (range "2.0.0" "2.2.0") ]; out = "0.9.4"; } + { cases = [ (range "8.16" "8.18") (range "2.0.0" "2.1.0" ) ]; out = "0.9.3"; } { cases = [ (range "8.14" "8.18") (range "1.13.0" "1.18.0") ]; out = "0.9.2"; } { cases = [ (range "8.14" "8.16") (range "1.13.0" "1.14.0") ]; out = "0.9.1"; } { cases = [ (range "8.12" "8.13") (range "1.12.0" "1.14.0") ]; out = "0.9"; } diff --git a/pkgs/development/coq-modules/iris/default.nix b/pkgs/development/coq-modules/iris/default.nix index ae6798243b6ac..a39e8a99509c3 100644 --- a/pkgs/development/coq-modules/iris/default.nix +++ b/pkgs/development/coq-modules/iris/default.nix @@ -31,7 +31,7 @@ mkCoqDerivation rec { ''; meta = with lib; { - description = "The Coq development of the Iris Project"; + description = "Coq development of the Iris Project"; license = licenses.bsd3; maintainers = [ maintainers.vbgl maintainers.ineol ]; }; diff --git a/pkgs/development/coq-modules/itauto/default.nix b/pkgs/development/coq-modules/itauto/default.nix index b0fba6868df83..63832a58caba5 100644 --- a/pkgs/development/coq-modules/itauto/default.nix +++ b/pkgs/development/coq-modules/itauto/default.nix @@ -30,7 +30,7 @@ passthru.tests.suite = callPackage ./test.nix {}; meta = with lib; { - description = "A reflexive SAT solver parameterised by a leaf tactic and Nelson-Oppen support"; + description = "Reflexive SAT solver parameterised by a leaf tactic and Nelson-Oppen support"; maintainers = with maintainers; [ siraben ]; license = licenses.gpl3Plus; }; diff --git a/pkgs/development/coq-modules/ltac2/default.nix b/pkgs/development/coq-modules/ltac2/default.nix index da28184296006..c9d6845aa9380 100644 --- a/pkgs/development/coq-modules/ltac2/default.nix +++ b/pkgs/development/coq-modules/ltac2/default.nix @@ -20,7 +20,7 @@ mkCoqDerivation { mlPlugin = true; meta = with lib; { - description = "A robust and expressive tactic language for Coq"; + description = "Robust and expressive tactic language for Coq"; maintainers = [ maintainers.vbgl ]; license = licenses.lgpl21; }; diff --git a/pkgs/development/coq-modules/math-classes/default.nix b/pkgs/development/coq-modules/math-classes/default.nix index 4630f14dea02f..102e52e59e167 100644 --- a/pkgs/development/coq-modules/math-classes/default.nix +++ b/pkgs/development/coq-modules/math-classes/default.nix @@ -21,7 +21,7 @@ mkCoqDerivation { meta = { homepage = "https://math-classes.github.io"; - description = "A library of abstract interfaces for mathematical structures in Coq."; + description = "Library of abstract interfaces for mathematical structures in Coq"; maintainers = with lib.maintainers; [ siddharthist jwiegley ]; }; } diff --git a/pkgs/development/coq-modules/mathcomp-analysis/default.nix b/pkgs/development/coq-modules/mathcomp-analysis/default.nix index 3703eee0e588d..97e8a7698a905 100644 --- a/pkgs/development/coq-modules/mathcomp-analysis/default.nix +++ b/pkgs/development/coq-modules/mathcomp-analysis/default.nix @@ -1,14 +1,16 @@ { lib, - mkCoqDerivation, recurseIntoAttrs, + mkCoqDerivation, mathcomp, mathcomp-finmap, mathcomp-bigenough, hierarchy-builder, single ? false, coqPackages, coq, version ? null }@args: -with builtins // lib; + let repo = "analysis"; owner = "math-comp"; + release."1.2.0".sha256 = "sha256-w6BivDM4dF4Iv4rUTy++2feweNtMAJxgGExPfYGhXxo="; + release."1.1.0".sha256 = "sha256-wl4kZf4mh9zbFfGcqaFEgWRyp0Bj511F505mYodpS6o="; release."1.0.0".sha256 = "sha256-KiXyaWB4zQ3NuXadq4BSWfoN1cIo1xiLVSN6nW03tC4="; release."0.7.0".sha256 = "sha256-JwkyetXrFsFHqz8KY3QBpHsrkhmEFnrCGuKztcoen60="; release."0.6.7".sha256 = "sha256-3i2PBMEwihwgwUmnS0cmrZ8s+aLPFVq/vo0aXMUaUyA="; @@ -28,20 +30,21 @@ let release."0.3.1".sha256 = "1iad288yvrjv8ahl9v18vfblgqb1l5z6ax644w49w9hwxs93f2k8"; release."0.2.3".sha256 = "0p9mr8g1qma6h10qf7014dv98ln90dfkwn76ynagpww7qap8s966"; - defaultVersion = with versions; lib.switch [ coq.version mathcomp.version ] [ - { cases = [ (range "8.17" "8.19") (range "2.0.0" "2.2.0") ]; out = "1.0.0"; } + defaultVersion = let inherit (lib.versions) range; in + lib.switch [ coq.version mathcomp.version ] [ + { cases = [ (range "8.17" "8.19") (range "2.0.0" "2.2.0") ]; out = "1.1.0"; } { cases = [ (range "8.17" "8.19") (range "1.17.0" "1.19.0") ]; out = "0.7.0"; } { cases = [ (range "8.17" "8.18") (range "1.15.0" "1.18.0") ]; out = "0.6.7"; } { cases = [ (range "8.17" "8.18") (range "1.15.0" "1.18.0") ]; out = "0.6.6"; } { cases = [ (range "8.14" "8.18") (range "1.15.0" "1.17.0") ]; out = "0.6.5"; } { cases = [ (range "8.14" "8.18") (range "1.13.0" "1.16.0") ]; out = "0.6.1"; } - { cases = [ (range "8.14" "8.18") (range "1.13" "1.15") ]; out = "0.5.2"; } - { cases = [ (range "8.13" "8.15") (range "1.13" "1.14") ]; out = "0.5.1"; } - { cases = [ (range "8.13" "8.15") (range "1.12" "1.14") ]; out = "0.3.13"; } - { cases = [ (range "8.11" "8.14") (range "1.12" "1.13") ]; out = "0.3.10"; } - { cases = [ (range "8.10" "8.12") "1.11.0" ]; out = "0.3.3"; } - { cases = [ (range "8.10" "8.11") "1.11.0" ]; out = "0.3.1"; } - { cases = [ (range "8.8" "8.11") (range "1.8" "1.10") ]; out = "0.2.3"; } + { cases = [ (range "8.14" "8.18") (range "1.13" "1.15") ]; out = "0.5.2"; } + { cases = [ (range "8.13" "8.15") (range "1.13" "1.14") ]; out = "0.5.1"; } + { cases = [ (range "8.13" "8.15") (range "1.12" "1.14") ]; out = "0.3.13"; } + { cases = [ (range "8.11" "8.14") (range "1.12" "1.13") ]; out = "0.3.10"; } + { cases = [ (range "8.10" "8.12") "1.11.0" ]; out = "0.3.3"; } + { cases = [ (range "8.10" "8.11") "1.11.0" ]; out = "0.3.1"; } + { cases = [ (range "8.8" "8.11") (range "1.8" "1.10") ]; out = "0.2.3"; } ] null; # list of analysis packages sorted by dependency order @@ -50,7 +53,7 @@ let mathcomp_ = package: let classical-deps = [ mathcomp.algebra mathcomp-finmap ]; analysis-deps = [ mathcomp.field mathcomp-bigenough ]; - intra-deps = lib.optionals (package != "single") (map mathcomp_ (head (splitList (lib.pred.equal package) packages))); + intra-deps = lib.optionals (package != "single") (map mathcomp_ (lib.head (lib.splitList (lib.pred.equal package) packages))); pkgpath = if package == "single" then "." else if package == "analysis" then "theories" else "${package}"; pname = if package == "single" then "mathcomp-analysis-single" @@ -62,8 +65,8 @@ let propagatedBuildInputs = intra-deps - ++ optionals (elem package [ "classical" "single" ]) classical-deps - ++ optionals (elem package [ "analysis" "single" ]) analysis-deps; + ++ lib.optionals (lib.elem package [ "classical" "single" ]) classical-deps + ++ lib.optionals (lib.elem package [ "analysis" "single" ]) analysis-deps; preBuild = '' cd ${pkgpath} @@ -71,26 +74,26 @@ let meta = { description = "Analysis library compatible with Mathematical Components"; - maintainers = [ maintainers.cohencyril ]; - license = licenses.cecill-c; + maintainers = [ lib.maintainers.cohencyril ]; + license = lib.licenses.cecill-c; }; - passthru = genAttrs packages mathcomp_; + passthru = lib.genAttrs packages mathcomp_; }); # split packages didn't exist before 0.6, so bulding nothing in that case patched-derivation1 = derivation.overrideAttrs (o: - optionalAttrs (o.pname != null && o.pname != "mathcomp-analysis" && - o.version != null && o.version != "dev" && versions.isLt "0.6" o.version) + 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: - optionalAttrs (o.pname != null && o.pname == "mathcomp-analysis" && - o.version != null && o.version != "dev" && versions.isLt "0.6" o.version) + lib.optionalAttrs (o.pname != null && o.pname == "mathcomp-analysis" && + o.version != null && o.version != "dev" && lib.versions.isLt "0.6" o.version) { preBuild = ""; } ); patched-derivation = patched-derivation2.overrideAttrs (o: - optionalAttrs (o.version != null - && (o.version == "dev" || versions.isGe "0.3.4" o.version)) + lib.optionalAttrs (o.version != null + && (o.version == "dev" || lib.versions.isGe "0.3.4" o.version)) { propagatedBuildInputs = o.propagatedBuildInputs ++ [ hierarchy-builder ]; } diff --git a/pkgs/development/coq-modules/mathcomp-apery/default.nix b/pkgs/development/coq-modules/mathcomp-apery/default.nix index 0b447909116ee..8e22a6c9aeb43 100644 --- a/pkgs/development/coq-modules/mathcomp-apery/default.nix +++ b/pkgs/development/coq-modules/mathcomp-apery/default.nix @@ -17,7 +17,7 @@ mkCoqDerivation { mathcomp-bigenough mathcomp-zify mathcomp-algebra-tactics ]; meta = { - description = "A formally verified proof in Coq, by computer algebra, that ζ(3) is irrational"; + description = "Formally verified proof in Coq, by computer algebra, that ζ(3) is irrational"; license = lib.licenses.cecill-c; }; } diff --git a/pkgs/development/coq-modules/mathcomp-bigenough/default.nix b/pkgs/development/coq-modules/mathcomp-bigenough/default.nix index df73d2111172c..35f8748f63c0b 100644 --- a/pkgs/development/coq-modules/mathcomp-bigenough/default.nix +++ b/pkgs/development/coq-modules/mathcomp-bigenough/default.nix @@ -19,7 +19,7 @@ mkCoqDerivation { propagatedBuildInputs = [ mathcomp.ssreflect ]; meta = { - description = "A small library to do epsilon - N reasonning"; + description = "Small library to do epsilon - N reasonning"; license = lib.licenses.cecill-b; }; } diff --git a/pkgs/development/coq-modules/mathcomp-finmap/default.nix b/pkgs/development/coq-modules/mathcomp-finmap/default.nix index c2f6ea02133cf..7120d9558566f 100644 --- a/pkgs/development/coq-modules/mathcomp-finmap/default.nix +++ b/pkgs/development/coq-modules/mathcomp-finmap/default.nix @@ -36,7 +36,7 @@ mkCoqDerivation { propagatedBuildInputs = [ mathcomp.ssreflect ]; meta = { - description = "A finset and finmap library"; + description = "Finset and finmap library"; license = lib.licenses.cecill-b; }; } diff --git a/pkgs/development/coq-modules/mathcomp-infotheo/default.nix b/pkgs/development/coq-modules/mathcomp-infotheo/default.nix index 6a14e67844c8d..cdd913f6d82b3 100644 --- a/pkgs/development/coq-modules/mathcomp-infotheo/default.nix +++ b/pkgs/development/coq-modules/mathcomp-infotheo/default.nix @@ -7,10 +7,12 @@ inherit version; defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp-analysis.version] [ + { cases = [ (isGe "8.17") (isGe "1.0") ]; out = "0.7.1"; } { cases = [ (isGe "8.17") (range "0.6.6" "0.7.0") ]; out = "0.6.1"; } { cases = [ (range "8.17" "8.18") (range "0.6.0" "0.6.7") ]; out = "0.5.2"; } { cases = [ (range "8.15" "8.16") (range "0.5.4" "0.6.5") ]; out = "0.5.1"; } ] null; + release."0.7.1".sha256 = "sha256-/4Elb35SmscG6EjEcHYDo+AmWrpBUlygZL0WhaD+fcY="; release."0.6.1".sha256 = "sha256-tFB5lrwRPIlHkP+ebgcJwu03Cc9yVaOINOAo8Bf2LT4="; release."0.5.1".sha256 = "sha256-yBBl5l+V+dggsg5KM59Yo9CULKog/xxE8vrW+ZRnX7Y="; release."0.5.2".sha256 = "sha256-8WAnAV53c0pMTdwj8XcUDUkLZbpUgIQbEOgOb63uHQA="; @@ -18,7 +20,7 @@ propagatedBuildInputs = [ mathcomp-analysis ]; meta = with lib; { - description = "A Coq formalization of information theory and linear error-correcting codes"; + description = "Coq formalization of information theory and linear error-correcting codes"; license = licenses.lgpl21Plus; }; }).overrideAttrs (o: { diff --git a/pkgs/development/coq-modules/mathcomp-word/default.nix b/pkgs/development/coq-modules/mathcomp-word/default.nix index 0183de9812269..98fdefa6d1176 100644 --- a/pkgs/development/coq-modules/mathcomp-word/default.nix +++ b/pkgs/development/coq-modules/mathcomp-word/default.nix @@ -18,8 +18,10 @@ mkCoqDerivation { releaseRev = v: "v${v}"; + release."3.2".sha256 = "sha256-4HOFFQzKbHIq+ktjJaS5b2Qr8WL1eQ26YxF4vt1FdWM="; release."3.1".sha256 = "sha256-qQHis6554sG7NpCpWhT2wvelnxsrbEPVNv3fpxwxHMU="; release."3.0".sha256 = "sha256-xEgx5HHDOimOJbNMtIVf/KG3XBemOS9XwoCoW6btyJ4="; + release."2.4".sha256 = "sha256-OG99PfjhtKikxM9aBKRsej1gTo1O/llAdXdiiyjZf2Q="; release."2.3".sha256 = "sha256-whU1yvFFuxpwQutW41B/WBg5DrVZJW/Do/GuHtzuI3U="; release."2.2".sha256 = "sha256-8BB6SToCrMZTtU78t2K+aExuxk9O1lCqVQaa8wabSm8="; release."2.1".sha256 = "sha256-895gZzwwX8hN9UUQRhcgRlphHANka9R0PRotfmSEelA="; @@ -27,8 +29,8 @@ mkCoqDerivation { inherit version; defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp.version ] [ - { cases = [ (range "8.16" "8.19") (isGe "2.0") ]; out = "3.1"; } - { cases = [ (range "8.12" "8.19") (range "1.12" "1.19") ]; out = "2.3"; } + { cases = [ (range "8.16" "8.19") (isGe "2.0") ]; out = "3.2"; } + { cases = [ (range "8.12" "8.19") (range "1.12" "1.19") ]; out = "2.4"; } ] null; propagatedBuildInputs = [ mathcomp.algebra mathcomp.ssreflect mathcomp.fingroup ]; diff --git a/pkgs/development/coq-modules/mathcomp/default.nix b/pkgs/development/coq-modules/mathcomp/default.nix index 50fc63de4cc49..7f132768ff88b 100644 --- a/pkgs/development/coq-modules/mathcomp/default.nix +++ b/pkgs/development/coq-modules/mathcomp/default.nix @@ -11,14 +11,15 @@ ############################################################################ { lib, ncurses, graphviz, lua, fetchzip, - mkCoqDerivation, recurseIntoAttrs, withDoc ? false, single ? false, + mkCoqDerivation, withDoc ? false, single ? false, coqPackages, coq, hierarchy-builder, version ? null }@args: -with builtins // lib; + let repo = "math-comp"; owner = "math-comp"; withDoc = single && (args.withDoc or false); - defaultVersion = with versions; lib.switch coq.coq-version [ + defaultVersion = let inherit (lib.versions) range; in + lib.switch coq.coq-version [ { case = range "8.19" "8.19"; out = "1.19.0"; } { case = range "8.17" "8.18"; out = "1.18.0"; } { case = range "8.15" "8.18"; out = "1.17.0"; } @@ -63,7 +64,7 @@ let packages = [ "ssreflect" "fingroup" "algebra" "solvable" "field" "character" "all" ]; mathcomp_ = package: let - mathcomp-deps = lib.optionals (package != "single") (map mathcomp_ (head (splitList (lib.pred.equal package) packages))); + mathcomp-deps = lib.optionals (package != "single") (map mathcomp_ (lib.head (lib.splitList (lib.pred.equal package) packages))); pkgpath = if package == "single" then "mathcomp" else "mathcomp/${package}"; pname = if package == "single" then "mathcomp" else "mathcomp-${package}"; pkgallMake = '' @@ -74,12 +75,12 @@ let derivation = mkCoqDerivation ({ inherit version pname defaultVersion release releaseRev repo owner; - mlPlugin = versions.isLe "8.6" coq.coq-version; - nativeBuildInputs = optionals withDoc [ graphviz lua ]; + mlPlugin = lib.versions.isLe "8.6" coq.coq-version; + nativeBuildInputs = lib.optionals withDoc [ graphviz lua ]; buildInputs = [ ncurses ]; propagatedBuildInputs = mathcomp-deps; - buildFlags = optional withDoc "doc"; + buildFlags = lib.optional withDoc "doc"; preBuild = '' if [[ -f etc/utils/ssrcoqdep ]] @@ -90,16 +91,16 @@ let fi '' + '' cd ${pkgpath} - '' + optionalString (package == "all") pkgallMake; + '' + lib.optionalString (package == "all") pkgallMake; meta = { homepage = "https://math-comp.github.io/"; - license = licenses.cecill-b; - maintainers = with maintainers; [ vbgl jwiegley cohencyril ]; + license = lib.licenses.cecill-b; + maintainers = with lib.maintainers; [ vbgl jwiegley cohencyril ]; }; - } // optionalAttrs (package != "single") - { passthru = genAttrs packages mathcomp_; } - // optionalAttrs withDoc { + } // lib.optionalAttrs (package != "single") + { passthru = lib.genAttrs packages mathcomp_; } + // lib.optionalAttrs withDoc { htmldoc_template = fetchzip { url = "https://github.com/math-comp/math-comp.github.io/archive/doc-1.12.0.zip"; @@ -111,7 +112,7 @@ let ''; postInstall = let tgt = "$out/share/coq/${coq.coq-version}/"; in - optionalString withDoc '' + lib.optionalString withDoc '' mkdir -p ${tgt} cp -r htmldoc ${tgt} cp -r $htmldoc_template/htmldoc_template/* ${tgt}/htmldoc/ @@ -120,20 +121,20 @@ let extraInstallFlags = [ "-f Makefile.coq" ]; }); patched-derivation1 = derivation.overrideAttrs (o: - optionalAttrs (o.pname != null && o.pname == "mathcomp-all" && - o.version != null && o.version != "dev" && versions.isLt "1.7" o.version) + 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: - optionalAttrs (versions.isLe "8.7" coq.coq-version || - (o.version != "dev" && versions.isLe "1.7" o.version)) + 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-derivation = patched-derivation2.overrideAttrs (o: - optionalAttrs (o.version != null - && (o.version == "dev" || versions.isGe "2.0.0" o.version)) + lib.optionalAttrs (o.version != null + && (o.version == "dev" || lib.versions.isGe "2.0.0" o.version)) { propagatedBuildInputs = o.propagatedBuildInputs ++ [ hierarchy-builder ]; } diff --git a/pkgs/development/coq-modules/metacoq/default.nix b/pkgs/development/coq-modules/metacoq/default.nix index 174f44b7702ae..bfd5baf97d4c4 100644 --- a/pkgs/development/coq-modules/metacoq/default.nix +++ b/pkgs/development/coq-modules/metacoq/default.nix @@ -1,11 +1,11 @@ { lib, fetchzip, - mkCoqDerivation, recurseIntoAttrs, single ? false, + mkCoqDerivation, single ? false, coqPackages, coq, equations, version ? null }@args: -with builtins // lib; + let repo = "metacoq"; owner = "MetaCoq"; - defaultVersion = with versions; switch coq.coq-version [ + defaultVersion = lib.switch coq.coq-version [ { case = "8.11"; out = "1.0-beta2-8.11"; } { case = "8.12"; out = "1.0-beta2-8.12"; } # Do not provide 8.13 because it does not compile with equations 1.3 provided by default (only 1.2.3) @@ -36,14 +36,14 @@ let releaseRev = v: "v${v}"; # list of core metacoq packages sorted by dependency order - packages = if versionAtLeast coq.coq-version "8.17" + packages = if lib.versionAtLeast coq.coq-version "8.17" then [ "utils" "common" "template-coq" "pcuic" "safechecker" "template-pcuic" "erasure" "quotation" "safechecker-plugin" "erasure-plugin" "all" ] else [ "template-coq" "pcuic" "safechecker" "erasure" "all" ]; template-coq = metacoq_ "template-coq"; metacoq_ = package: let - metacoq-deps = lib.optionals (package != "single") (map metacoq_ (head (splitList (lib.pred.equal package) packages))); + metacoq-deps = lib.optionals (package != "single") (map metacoq_ (lib.head (lib.splitList (lib.pred.equal package) packages))); pkgpath = if package == "single" then "./" else "./${package}"; pname = if package == "all" then "metacoq" else "metacoq-${package}"; pkgallMake = '' @@ -57,7 +57,7 @@ let mlPlugin = true; propagatedBuildInputs = [ equations coq.ocamlPackages.zarith ] ++ metacoq-deps; - patchPhase = if versionAtLeast coq.coq-version "8.17" then '' + patchPhase = if lib.versionAtLeast coq.coq-version "8.17" then '' patchShebangs ./configure.sh patchShebangs ./template-coq/update_plugin.sh patchShebangs ./template-coq/gen-src/to-lower.sh @@ -76,11 +76,11 @@ let sed -i -e 's/mv $i $newi;/mv $i tmp; mv tmp $newi;/' ./template-coq/gen-src/to-lower.sh ./pcuic/clean_extraction.sh ./safechecker/clean_extraction.sh ./erasure/clean_extraction.sh '' ; - configurePhase = optionalString (package == "all") pkgallMake + '' + configurePhase = lib.optionalString (package == "all") pkgallMake + '' touch ${pkgpath}/metacoq-config - '' + optionalString (elem package ["safechecker" "erasure" "template-pcuic" "quotation" "safechecker-plugin" "erasure-plugin"]) '' + '' + lib.optionalString (lib.elem package ["safechecker" "erasure" "template-pcuic" "quotation" "safechecker-plugin" "erasure-plugin"]) '' echo "-I ${template-coq}/lib/coq/${coq.coq-version}/user-contrib/MetaCoq/Template/" > ${pkgpath}/metacoq-config - '' + optionalString (package == "single") '' + '' + lib.optionalString (package == "single") '' ./configure.sh local ''; @@ -90,17 +90,17 @@ let meta = { homepage = "https://metacoq.github.io/"; - license = licenses.mit; - maintainers = with maintainers; [ cohencyril ]; + license = lib.licenses.mit; + maintainers = with lib.maintainers; [ cohencyril ]; }; - } // optionalAttrs (package != "single") - { passthru = genAttrs packages metacoq_; }) + } // lib.optionalAttrs (package != "single") + { passthru = lib.genAttrs packages metacoq_; }) ).overrideAttrs (o: - let requiresOcamlStdlibShims = versionAtLeast o.version "1.0-8.16" || - (o.version == "dev" && (versionAtLeast coq.coq-version "8.16" || coq.coq-version == "dev")) ; + let requiresOcamlStdlibShims = lib.versionAtLeast o.version "1.0-8.16" || + (o.version == "dev" && (lib.versionAtLeast coq.coq-version "8.16" || coq.coq-version == "dev")) ; in { - propagatedBuildInputs = o.propagatedBuildInputs ++ optional requiresOcamlStdlibShims coq.ocamlPackages.stdlib-shims; + propagatedBuildInputs = o.propagatedBuildInputs ++ lib.optional requiresOcamlStdlibShims coq.ocamlPackages.stdlib-shims; }); in derivation; in diff --git a/pkgs/development/coq-modules/multinomials/default.nix b/pkgs/development/coq-modules/multinomials/default.nix index 5547e22bc59fe..4326aa9ba2243 100644 --- a/pkgs/development/coq-modules/multinomials/default.nix +++ b/pkgs/development/coq-modules/multinomials/default.nix @@ -51,7 +51,7 @@ [ mathcomp.ssreflect mathcomp.algebra mathcomp-finmap mathcomp.fingroup mathcomp-bigenough ]; meta = { - description = "A Coq/SSReflect Library for Monoidal Rings and Multinomials"; + description = "Coq/SSReflect Library for Monoidal Rings and Multinomials"; license = lib.licenses.cecill-c; }; } diff --git a/pkgs/development/coq-modules/paco/default.nix b/pkgs/development/coq-modules/paco/default.nix index 717100ddfe259..afbcc6669bdb3 100644 --- a/pkgs/development/coq-modules/paco/default.nix +++ b/pkgs/development/coq-modules/paco/default.nix @@ -28,7 +28,7 @@ mkCoqDerivation { meta = { homepage = "https://plv.mpi-sws.org/paco/"; - description = "A Coq library implementing parameterized coinduction"; + description = "Coq library implementing parameterized coinduction"; maintainers = with lib.maintainers; [ jwiegley ptival ]; }; } diff --git a/pkgs/development/coq-modules/semantics/default.nix b/pkgs/development/coq-modules/semantics/default.nix index a715ff17a69bb..18e9171096d7b 100644 --- a/pkgs/development/coq-modules/semantics/default.nix +++ b/pkgs/development/coq-modules/semantics/default.nix @@ -34,7 +34,7 @@ mkCoqDerivation rec { ''; meta = with lib; { - description = "A survey of programming language semantics styles in Coq"; + description = "Survey of programming language semantics styles in Coq"; longDescription = '' A survey of semantics styles in Coq, from natural semantics through structural operational, axiomatic, and denotational semantics, to diff --git a/pkgs/development/coq-modules/serapi/default.nix b/pkgs/development/coq-modules/serapi/default.nix index f48cce55d4dc2..b7aa0ecff25e4 100644 --- a/pkgs/development/coq-modules/serapi/default.nix +++ b/pkgs/development/coq-modules/serapi/default.nix @@ -2,9 +2,9 @@ let release = { - "8.19.0+0.19.0".sha256 = "sha256-M9d0ne2veTjf8/mFIDwtWdHi64JXjwCPWupnO2Ztd/Y="; - "8.18.0+0.18.0".sha256 = "sha256-c+3yG9vcbek/uvQ27OOQGqqsIHU1VuQhQvNVOjfucbo="; - "8.17.0+0.17.0".sha256 = "sha256-I81qvaXpJfXcbFw8vyzYLzlnhPg1QD0lTqAFXhoZ0rI="; + "8.19.0+0.19.3".sha256 = "sha256-QWRXBTcjtAGskZBeLIuX7WDE95KfH6SxV8MJSMx8B2Q="; + "8.18.0+0.18.3".sha256 = "sha256-3JGZCyn62LYJVpfXiwnSMxvdA2vQNTL7li2ZBPcjF0M="; + "8.17.0+0.17.3".sha256 = "sha256-XolzpJd8zs4LLyJO4eWvCiAJ0HJSGBJTGVSBClQRGnw="; "8.16.0+0.16.3".sha256 = "sha256-22Kawp8jAsgyBTppwN5vmN7zEaB1QfPs0qKxd6x/7Uc="; "8.15.0+0.15.0".sha256 = "1vh99ya2dq6a8xl2jrilgs0rpj4j227qx8zvzd2v5xylx0p4bbrp"; "8.14.0+0.14.0".sha256 = "1kh80yb791yl771qbqkvwhbhydfii23a7lql0jgifvllm2k8hd8d"; @@ -21,9 +21,9 @@ in defaultVersion = with versions; lib.switch coq.version [ - { case = isEq "8.19"; out = "8.19.0+0.19.0"; } - { case = isEq "8.18"; out = "8.18.0+0.18.0"; } - { case = isEq "8.17"; out = "8.17.0+0.17.0"; } + { case = isEq "8.19"; out = "8.19.0+0.19.3"; } + { case = isEq "8.18"; out = "8.18.0+0.18.3"; } + { case = isEq "8.17"; out = "8.17.0+0.17.3"; } { case = isEq "8.16"; out = "8.16.0+0.16.3"; } { case = isEq "8.15"; out = "8.15.0+0.15.0"; } { case = isEq "8.14"; out = "8.14.0+0.14.0"; } diff --git a/pkgs/development/coq-modules/smpl/default.nix b/pkgs/development/coq-modules/smpl/default.nix index 2ba755dd42d02..147c04e0c3f33 100644 --- a/pkgs/development/coq-modules/smpl/default.nix +++ b/pkgs/development/coq-modules/smpl/default.nix @@ -23,7 +23,7 @@ mkCoqDerivation { mlPlugin = true; meta = with lib; { - description = "A Coq plugin providing an extensible tactic similar to first"; + description = "Coq plugin providing an extensible tactic similar to first"; maintainers = with maintainers; [ siraben ]; license = licenses.mit; platforms = platforms.unix; diff --git a/pkgs/development/coq-modules/stdpp/default.nix b/pkgs/development/coq-modules/stdpp/default.nix index 6eb8f77149cc3..1215acaed5a1c 100644 --- a/pkgs/development/coq-modules/stdpp/default.nix +++ b/pkgs/development/coq-modules/stdpp/default.nix @@ -29,7 +29,7 @@ mkCoqDerivation rec { ''; meta = with lib; { - description = "An extended “Standard Library” for Coq"; + description = "Extended “Standard Library” for Coq"; license = licenses.bsd3; maintainers = [ maintainers.vbgl maintainers.ineol ]; }; diff --git a/pkgs/development/coq-modules/tlc/default.nix b/pkgs/development/coq-modules/tlc/default.nix index 4fb67bede2379..00506bf0eea7d 100644 --- a/pkgs/development/coq-modules/tlc/default.nix +++ b/pkgs/development/coq-modules/tlc/default.nix @@ -18,7 +18,7 @@ meta = with lib; { homepage = "http://www.chargueraud.org/softs/tlc/"; - description = "A non-constructive library for Coq"; + description = "Non-constructive library for Coq"; license = licenses.free; maintainers = [ maintainers.vbgl ]; }; diff --git a/pkgs/development/coq-modules/trakt/default.nix b/pkgs/development/coq-modules/trakt/default.nix index e08d7b8d50ca5..e762a51880b24 100644 --- a/pkgs/development/coq-modules/trakt/default.nix +++ b/pkgs/development/coq-modules/trakt/default.nix @@ -19,7 +19,7 @@ mkCoqDerivation { propagatedBuildInputs = [ coq-elpi ]; meta = with lib; { - description = "A generic goal preprocessing tool for proof automation tactics in Coq"; + description = "Generic goal preprocessing tool for proof automation tactics in Coq"; maintainers = with maintainers; [ siraben ]; license = licenses.lgpl3Plus; platforms = platforms.unix; diff --git a/pkgs/development/coq-modules/vcfloat/default.nix b/pkgs/development/coq-modules/vcfloat/default.nix index 474ae171b77c1..cb1fa248fdc3d 100644 --- a/pkgs/development/coq-modules/vcfloat/default.nix +++ b/pkgs/development/coq-modules/vcfloat/default.nix @@ -19,7 +19,7 @@ let self = mkCoqDerivation { propagatedBuildInputs = [ interval compcert flocq bignums ]; meta = { - description = "A tool for Coq proofs about floating-point round-off error"; + description = "Tool for Coq proofs about floating-point round-off error"; maintainers = with lib.maintainers; [ quinn-dougherty ]; license = lib.licenses.lgpl3Plus; }; |