NixOS · wegank · Jan 24, 2023 · Jan 21, 2023
diff --git a/pkgs/development/coq-modules/Cheerios/default.nix b/pkgs/development/coq-modules/Cheerios/default.nix
@@ -1,10 +1,10 @@
 { lib, mkCoqDerivation, coq, StructTact, version ? null }:
 
-with lib; mkCoqDerivation {
+mkCoqDerivation {
   pname   = "cheerios";
   owner   = "uwplse";
   inherit version;
-  defaultVersion = if versions.range "8.6" "8.16" coq.version then "20200201" else null;
+  defaultVersion = if lib.versions.range "8.6" "8.16" coq.version then "20200201" else null;
   release."20200201".rev    = "9c7f66e57b91f706d70afa8ed99d64ed98ab367d";
   release."20200201".sha256 = "1h55s6lk47bk0lv5ralh81z55h799jbl9mhizmqwqzy57y8wqgs1";
 

diff --git a/pkgs/development/coq-modules/CoLoR/default.nix b/pkgs/development/coq-modules/CoLoR/default.nix
@@ -1,10 +1,10 @@
 { lib, mkCoqDerivation, coq, bignums, version ? null }:
 
-with lib; mkCoqDerivation {
+mkCoqDerivation {
   pname = "color";
   owner = "fblanqui";
   inherit version;
-  defaultVersion = with versions; switch coq.version [
+  defaultVersion = with lib.versions; lib.switch coq.version [
     {case = range "8.12" "8.16"; out = "1.8.2"; }
     {case = range "8.10" "8.11"; out = "1.7.0"; }
     {case = range "8.8"  "8.9";  out = "1.6.0"; }
@@ -26,6 +26,6 @@ with lib; 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.";
-    maintainers = with maintainers; [ jpas jwiegley ];
+    maintainers = with lib.maintainers; [ jpas jwiegley ];
   };
 }
diff --git a/pkgs/development/coq-modules/HoTT/default.nix b/pkgs/development/coq-modules/HoTT/default.nix
@@ -1,11 +1,11 @@
 { lib, mkCoqDerivation, autoconf, automake, coq, version ? null }:
 
-with lib; mkCoqDerivation {
+mkCoqDerivation {
   pname = "HoTT";
   repo = "Coq-HoTT";
   owner = "HoTT";
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = range "8.14" "8.16"; out = coq.coq-version; }
   ] null;
   releaseRev = v: "V${v}";
@@ -20,6 +20,6 @@ with lib; mkCoqDerivation {
   meta = {
     homepage = "http://homotopytypetheory.org/";
     description = "Homotopy type theory";
-    maintainers = with maintainers; [ siddharthist ];
+    maintainers = with lib.maintainers; [ siddharthist ];
   };
 }
diff --git a/pkgs/development/coq-modules/ITree/default.nix b/pkgs/development/coq-modules/ITree/default.nix
@@ -1,17 +1,17 @@
 { lib, mkCoqDerivation, coq, version ? null , paco, coq-ext-lib }:
 
-with lib; mkCoqDerivation rec {
+mkCoqDerivation rec {
   pname = "InteractionTrees";
   owner = "DeepSpec";
   inherit version;
-  defaultVersion = with versions; switch coq.version [
+  defaultVersion = with lib.versions; lib.switch coq.version [
     { case = range "8.10" "8.16";  out = "4.0.0"; }
   ] null;
   release."4.0.0".sha256 = "0h5rhndl8syc24hxq1gch86kj7mpmgr89bxp2hmf28fd7028ijsm";
   releaseRev = v: "${v}";
   propagatedBuildInputs = [ coq-ext-lib paco ];
   meta = {
     description = "A Library for Representing Recursive and Impure Programs in Coq";
-    maintainers = with maintainers; [ larsr ];
+    maintainers = with lib.maintainers; [ larsr ];
   };
 }
diff --git a/pkgs/development/coq-modules/LibHyps/default.nix b/pkgs/development/coq-modules/LibHyps/default.nix
@@ -1,11 +1,10 @@
 { lib, mkCoqDerivation, coq, version ? null }:
 
-with lib;
 mkCoqDerivation {
   pname = "LibHyps";
   owner = "Matafou";
   inherit version;
-  defaultVersion = if (versions.range "8.11" "8.16") coq.version then "2.0.4.1" else null;
+  defaultVersion = if (lib.versions.range "8.11" "8.16") coq.version then "2.0.4.1" else null;
   release = {
     "2.0.4.1".sha256 = "09p89701zhrfdmqlpxw3mziw8yylj1w1skb4b0xpbdwd1vsn4k3h";
   };
@@ -16,6 +15,6 @@ mkCoqDerivation {
 
   meta = {
     description = "Hypotheses manipulation library";
-    license = licenses.mit;
+    license = lib.licenses.mit;
   };
 }
diff --git a/pkgs/development/coq-modules/StructTact/default.nix b/pkgs/development/coq-modules/StructTact/default.nix
@@ -1,10 +1,10 @@
 { lib, mkCoqDerivation, coq, version ? null }:
 
-with lib; mkCoqDerivation {
+mkCoqDerivation {
   pname = "StructTact";
   owner = "uwplse";
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = range "8.6" "8.16"; out = "20210328"; }
     { case = range "8.5" "8.13"; out = "20181102"; }
   ] null;

diff --git a/pkgs/development/coq-modules/VST/default.nix b/pkgs/development/coq-modules/VST/default.nix
@@ -1,7 +1,5 @@
 { lib, mkCoqDerivation, coq, compcert, ITree, version ? null }:
 
-with lib;
-
 # A few modules that are not built and installed by default
 #  but that may be useful to some users.
 # They depend on ITree.
@@ -11,7 +9,7 @@ let extra_floyd_files = [
   "powerlater.v"
   ]
   # floyd/printf.v is broken in VST 2.9
-  ++ optional (!versions.isGe "8.13" coq.coq-version) "printf.v"
+  ++ lib.optional (!lib.versions.isGe "8.13" coq.coq-version) "printf.v"
   ++ [
   "quickprogram.v"
   ];
@@ -24,7 +22,7 @@ mkCoqDerivation {
   owner = "PrincetonUniversity";
   repo = "VST";
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = range "8.15" "8.16"; out = "2.11.1"; }
     { case = range "8.14" "8.16"; out = "2.10"; }
     { case = range "8.13" "8.15"; out = "2.9"; }

diff --git a/pkgs/development/coq-modules/Velisarios/default.nix b/pkgs/development/coq-modules/Velisarios/default.nix
@@ -1,10 +1,10 @@
 { lib, mkCoqDerivation, coq, version ? null }:
 
-with lib; mkCoqDerivation {
+mkCoqDerivation {
   pname = "Velisarios";
   owner = "vrahli";
   inherit version;
-  defaultVersion = if versions.range "8.6" "8.8" coq.coq-version then "20180221" else null;
+  defaultVersion = if lib.versions.range "8.6" "8.8" coq.coq-version then "20180221" else null;
 
   release."20180221".rev    = "e1eee1f10d5d46331a560bd8565ac101229d0d6b";
   release."20180221".sha256 = "0l9885nxy0n955fj1gnijlxl55lyxiv9yjfmz8hmfrn9hl8vv1m2";

diff --git a/pkgs/development/coq-modules/Verdi/default.nix b/pkgs/development/coq-modules/Verdi/default.nix
@@ -1,11 +1,11 @@
 { lib, mkCoqDerivation, coq, Cheerios, InfSeqExt, ssreflect, version ? null }:
 
 
-with lib; mkCoqDerivation {
+mkCoqDerivation {
   pname = "verdi";
   owner = "uwplse";
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = range "8.7" "8.16"; out = "20211026"; }
     { case = range "8.7" "8.14"; out = "20210524"; }
     { case = range "8.7" "8.13"; out = "20200131"; }

diff --git a/pkgs/development/coq-modules/aac-tactics/default.nix b/pkgs/development/coq-modules/aac-tactics/default.nix
@@ -1,5 +1,4 @@
 { lib, mkCoqDerivation, coq, version ? null }:
-with lib;
 
 mkCoqDerivation {
   pname = "aac-tactics";
@@ -21,7 +20,7 @@ mkCoqDerivation {
   release."8.5.0".sha256 = "sha256-7yNxJn6CH5xS5w/zsXfcZYORa6e5/qS9v8PUq2o02h4=";
 
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = "8.16"; out = "8.16.0"; }
     { case = "8.15"; out = "8.15.1"; }
     { case = "8.14"; out = "8.14.1"; }
@@ -37,7 +36,7 @@ mkCoqDerivation {
 
   mlPlugin = true;
 
-  meta = {
+  meta = with lib; {
     description = "Coq plugin providing tactics for rewriting universally quantified equations";
     longDescription = ''
       This Coq plugin provides tactics for rewriting universally quantified

diff --git a/pkgs/development/coq-modules/addition-chains/default.nix b/pkgs/development/coq-modules/addition-chains/default.nix
@@ -1,6 +1,5 @@
 { lib, mkCoqDerivation, coq, mathcomp-ssreflect, mathcomp-algebra, mathcomp-fingroup, paramcoq
 , version ? null }:
-with lib;
 
 mkCoqDerivation {
   pname = "addition-chains";
@@ -12,7 +11,7 @@ mkCoqDerivation {
   releaseRev = (v: "v${v}");
 
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = range "8.13" "8.16"; out = "0.6"; }
     { case = range "8.11" "8.12"; out = "0.4"; }
   ] null;
@@ -21,7 +20,7 @@ mkCoqDerivation {
 
   useDune = true;
 
-  meta = {
+  meta = with lib; {
     description = "Exponentiation algorithms following addition chains";
     longDescription = ''
       Addition chains are algorithms for computations of the p-th

diff --git a/pkgs/development/coq-modules/autosubst/default.nix b/pkgs/development/coq-modules/autosubst/default.nix
@@ -1,5 +1,4 @@
 { lib, mkCoqDerivation, coq, mathcomp-ssreflect, version ? null }:
-with lib;
 
 mkCoqDerivation {
   pname = "autosubst";
@@ -8,13 +7,13 @@ mkCoqDerivation {
   release."1.7".sha256 = "sha256-qoyteQ5W2Noxf12uACOVeHhPLvgmTzrvEo6Ts+FKTGI=";
 
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = range "8.10" "8.16"; out = "1.7"; }
   ] null;
 
   propagatedBuildInputs = [ mathcomp-ssreflect ];
 
-  meta = {
+  meta = with lib; {
     homepage = "https://www.ps.uni-saarland.de/autosubst/";
     description = "Automation for de Bruijn syntax and substitution in Coq";
     maintainers = with maintainers; [ siraben jwiegley ];

diff --git a/pkgs/development/coq-modules/bignums/default.nix b/pkgs/development/coq-modules/bignums/default.nix
@@ -1,11 +1,11 @@
 { lib, mkCoqDerivation, coq, version ? null }:
 
-with lib; mkCoqDerivation {
+mkCoqDerivation {
   pname = "bignums";
   owner = "coq";
   displayVersion = { bignums = ""; };
   inherit version;
-  defaultVersion = if versions.isGe "8.6" coq.coq-version
+  defaultVersion = if lib.versions.isGe "8.6" coq.coq-version
     then "${coq.coq-version}.0" else null;
 
   release."8.17.0".sha256 = "sha256-MXYjqN86+3O4hT2ql62U83T5H03E/8ysH8erpvC/oyw=";
@@ -25,5 +25,5 @@ with lib; mkCoqDerivation {
 
   mlPlugin = true;
 
-  meta = { license = licenses.lgpl2; };
+  meta = { license = lib.licenses.lgpl2; };
 }
diff --git a/pkgs/development/coq-modules/category-theory/default.nix b/pkgs/development/coq-modules/category-theory/default.nix
@@ -1,6 +1,6 @@
 { lib, mkCoqDerivation, coq, ssreflect, equations, version ? null }:
 
-with lib; mkCoqDerivation {
+mkCoqDerivation {
 
   pname = "category-theory";
   owner = "jwiegley";
@@ -16,7 +16,7 @@ with lib; mkCoqDerivation {
   release."20180709".sha256 = "0f2nr8dgn1ab7hr7jrdmr1zla9g9h8216q4yf4wnff9qkln8sbbs";
 
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = range "8.14" "8.16"; out = "1.0.0"; }
     { case = range "8.10" "8.15"; out = "20211213"; }
     { case = range "8.8" "8.9"; out = "20190414"; }
@@ -28,6 +28,6 @@ with lib; mkCoqDerivation {
 
   meta = {
     description = "A formalization of category theory in Coq for personal study and practical work";
-    maintainers = with maintainers; [ jwiegley ];
+    maintainers = with lib.maintainers; [ jwiegley ];
   };
 }
diff --git a/pkgs/development/coq-modules/ceres/default.nix b/pkgs/development/coq-modules/ceres/default.nix
@@ -1,17 +1,16 @@
 { lib, mkCoqDerivation, coq, version ? null }:
 
-with lib;
 mkCoqDerivation {
 
   pname = "ceres";
   repo = "coq-ceres";
   owner = "Lysxia";
 
   inherit version;
-  defaultVersion = if versions.range "8.8" "8.16" coq.version then "0.4.0" else null;
+  defaultVersion = if lib.versions.range "8.8" "8.16" coq.version then "0.4.0" else null;
   release."0.4.0".sha256 = "sha256:0zwp3pn6fdj0qdig734zdczrls886al06mxqhhabms0jvvqijmbi";
 
-  meta = {
+  meta = with lib; {
     description = "Library for serialization to S-expressions";
     license = licenses.mit;
     maintainers = with maintainers; [ Zimmi48 ];

diff --git a/pkgs/development/coq-modules/compcert/default.nix b/pkgs/development/coq-modules/compcert/default.nix
@@ -5,8 +5,6 @@
 , version ? null
 }:
 
-with lib;
-
 let compcert = mkCoqDerivation rec {
 
   pname = "compcert";
@@ -15,7 +13,7 @@ let compcert = mkCoqDerivation rec {
   inherit version;
   releaseRev = v: "v${v}";
 
-  defaultVersion =  with versions; switch coq.version [
+  defaultVersion =  with lib.versions; lib.switch coq.version [
       { case = range "8.14" "8.16"; out = "3.11"; }
       { case = isEq "8.13"        ; out = "3.10"; }
       { case = isEq "8.12"       ; out = "3.9"; }
@@ -84,7 +82,7 @@ let compcert = mkCoqDerivation rec {
 }; in
 compcert.overrideAttrs (o:
   {
-    patches = with versions; switch [ coq.version o.version ] [
+    patches = with lib.versions; lib.switch [ coq.version o.version ] [
       { cases = [ (range "8.12.2" "8.13.2") "3.8" ];
         out = [
           # Support for Coq 8.12.2

diff --git a/pkgs/development/coq-modules/contribs/default.nix b/pkgs/development/coq-modules/contribs/default.nix
@@ -1,16 +1,16 @@
 { lib, mkCoqDerivation, coq, callPackage }:
 
-with lib; let mkContrib = pname: coqs: param:
+  let mkContrib = pname: coqs: param:
   let contribVersion = {version ? null}: mkCoqDerivation ({
       inherit pname version;
       owner = "coq-contribs";
       mlPlugin = true;
-    } // optionalAttrs (builtins.elem coq.coq-version coqs) ({
+    } // lib.optionalAttrs (builtins.elem coq.coq-version coqs) ({
       defaultVersion = param.version;
       release = { "${param.version}" = { inherit (param) rev sha256; }; };
     } // (removeAttrs param [ "version" "rev" "sha256" ]))
   ); in
-  makeOverridable contribVersion {} ; in
+  lib.makeOverridable contribVersion {} ; in
 {
   aac-tactics = mkContrib "aac-tactics" [ "8.7" "8.8" ] {
     "8.7" = {

diff --git a/pkgs/development/coq-modules/coq-bits/default.nix b/pkgs/development/coq-modules/coq-bits/default.nix
@@ -1,10 +1,10 @@
 { lib, mkCoqDerivation, coq, mathcomp-algebra, version ? null }:
 
-with lib; mkCoqDerivation {
+mkCoqDerivation {
   pname = "coq-bits";
   repo = "bits";
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = range "8.10" "8.16"; out = "1.1.0"; }
     { case = range "8.7"  "8.15"; out = "1.0.0"; }
   ] null;
@@ -14,7 +14,7 @@ with lib; mkCoqDerivation {
 
   propagatedBuildInputs = [ mathcomp-algebra ];
 
-  meta = {
+  meta = with lib; {
     description = "A formalization of bitset operations in Coq";
     license = licenses.asl20;
     maintainers = with maintainers; [ ptival ];

diff --git a/pkgs/development/coq-modules/coq-ext-lib/default.nix b/pkgs/development/coq-modules/coq-ext-lib/default.nix
@@ -1,10 +1,10 @@
 { lib, mkCoqDerivation, coq, version ? null }:
 
-with lib; mkCoqDerivation rec {
+mkCoqDerivation rec {
   pname = "coq-ext-lib";
   owner = "coq-ext-lib";
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = range "8.11" "8.16"; out = "0.11.7"; }
     { case = range "8.8" "8.16"; out = "0.11.6"; }
     { case = range "8.8" "8.14"; out = "0.11.4"; }
@@ -30,6 +30,6 @@ with lib; mkCoqDerivation rec {
 
   meta = {
     description = "A collection of theories and plugins that may be useful in other Coq developments";
-    maintainers = with maintainers; [ jwiegley ptival ];
+    maintainers = with lib.maintainers; [ jwiegley ptival ];
   };
 }