summary refs log tree commit diff
path: root/pkgs/applications/science/logic
diff options
context:
space:
mode:
authorProfpatsch <mail@profpatsch.de>2021-01-11 08:54:33 +0100
committerProfpatsch <mail@profpatsch.de>2021-01-11 10:38:22 +0100
commit4a7f99d55d299453a9c2397f90b33d1120669775 (patch)
tree9fca8e9c9970d0a00ce56dfe11b63ae76b00cf01 /pkgs/applications/science/logic
parente87aef06e00c42b26789321454d7bd609548cc12 (diff)
downloadnixpkgs-4a7f99d55d299453a9c2397f90b33d1120669775.tar
nixpkgs-4a7f99d55d299453a9c2397f90b33d1120669775.tar.gz
nixpkgs-4a7f99d55d299453a9c2397f90b33d1120669775.tar.bz2
nixpkgs-4a7f99d55d299453a9c2397f90b33d1120669775.tar.lz
nixpkgs-4a7f99d55d299453a9c2397f90b33d1120669775.tar.xz
nixpkgs-4a7f99d55d299453a9c2397f90b33d1120669775.tar.zst
nixpkgs-4a7f99d55d299453a9c2397f90b33d1120669775.zip
treewide: with stdenv.lib; in meta -> with lib;
Part of: https://github.com/NixOS/nixpkgs/issues/108938

meta = with stdenv.lib;

is a widely used pattern. We want to slowly remove
the `stdenv.lib` indirection and encourage people
to use `lib` directly. Thus let’s start with the meta
field.

This used a rewriting script to mostly automatically
replace all occurances of this pattern, and add the
`lib` argument to the package header if it doesn’t
exist yet.

The script in its current form is available at
https://cs.tvl.fyi/depot@2f807d7f141068d2d60676a89213eaa5353ca6e0/-/blob/users/Profpatsch/nixpkgs-rewriter/default.nix
Diffstat (limited to 'pkgs/applications/science/logic')
-rw-r--r--pkgs/applications/science/logic/abc/default.nix4
-rw-r--r--pkgs/applications/science/logic/acgtk/default.nix4
-rw-r--r--pkgs/applications/science/logic/aspino/default.nix4
-rw-r--r--pkgs/applications/science/logic/boolector/default.nix2
-rw-r--r--pkgs/applications/science/logic/btor2tools/default.nix4
-rw-r--r--pkgs/applications/science/logic/cadical/default.nix4
-rw-r--r--pkgs/applications/science/logic/cedille/default.nix2
-rw-r--r--pkgs/applications/science/logic/celf/default.nix4
-rw-r--r--pkgs/applications/science/logic/clprover/clprover.nix4
-rw-r--r--pkgs/applications/science/logic/coq/default.nix6
-rw-r--r--pkgs/applications/science/logic/coq2html/default.nix4
-rw-r--r--pkgs/applications/science/logic/cryptominisat/default.nix4
-rw-r--r--pkgs/applications/science/logic/cubicle/default.nix4
-rw-r--r--pkgs/applications/science/logic/cvc3/default.nix4
-rw-r--r--pkgs/applications/science/logic/cvc4/default.nix4
-rw-r--r--pkgs/applications/science/logic/drat-trim/default.nix4
-rw-r--r--pkgs/applications/science/logic/eprover/default.nix4
-rw-r--r--pkgs/applications/science/logic/fast-downward/default.nix2
-rw-r--r--pkgs/applications/science/logic/glucose/default.nix4
-rw-r--r--pkgs/applications/science/logic/glucose/syrup.nix4
-rw-r--r--pkgs/applications/science/logic/hol/default.nix4
-rw-r--r--pkgs/applications/science/logic/hol_light/default.nix4
-rw-r--r--pkgs/applications/science/logic/iprover/default.nix4
-rw-r--r--pkgs/applications/science/logic/isabelle/default.nix4
-rw-r--r--pkgs/applications/science/logic/key/default.nix4
-rw-r--r--pkgs/applications/science/logic/lean/default.nix4
-rw-r--r--pkgs/applications/science/logic/lean2/default.nix4
-rw-r--r--pkgs/applications/science/logic/leo2/default.nix4
-rw-r--r--pkgs/applications/science/logic/lingeling/default.nix4
-rw-r--r--pkgs/applications/science/logic/mcrl2/default.nix4
-rw-r--r--pkgs/applications/science/logic/metis-prover/default.nix4
-rw-r--r--pkgs/applications/science/logic/minisat/default.nix4
-rw-r--r--pkgs/applications/science/logic/open-wbo/default.nix4
-rw-r--r--pkgs/applications/science/logic/opensmt/default.nix4
-rw-r--r--pkgs/applications/science/logic/poly/default.nix4
-rw-r--r--pkgs/applications/science/logic/prooftree/default.nix4
-rw-r--r--pkgs/applications/science/logic/spass/default.nix4
-rw-r--r--pkgs/applications/science/logic/stp/default.nix4
-rw-r--r--pkgs/applications/science/logic/tptp/default.nix4
-rw-r--r--pkgs/applications/science/logic/vampire/default.nix4
-rw-r--r--pkgs/applications/science/logic/verit/default.nix4
-rw-r--r--pkgs/applications/science/logic/why3/default.nix4
-rw-r--r--pkgs/applications/science/logic/yices/default.nix4
43 files changed, 84 insertions, 84 deletions
diff --git a/pkgs/applications/science/logic/abc/default.nix b/pkgs/applications/science/logic/abc/default.nix
index 0e60122a598..cbcd452033c 100644
--- a/pkgs/applications/science/logic/abc/default.nix
+++ b/pkgs/applications/science/logic/abc/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchFromGitHub
+{ lib, stdenv, fetchFromGitHub
 , readline, cmake
 }:
 
@@ -21,7 +21,7 @@ stdenv.mkDerivation rec {
   # needed by yosys
   passthru.rev = src.rev;
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "A tool for squential logic synthesis and formal verification";
     homepage    = "https://people.eecs.berkeley.edu/~alanmi/abc";
     license     = licenses.mit;
diff --git a/pkgs/applications/science/logic/acgtk/default.nix b/pkgs/applications/science/logic/acgtk/default.nix
index ccd08000507..48563248773 100644
--- a/pkgs/applications/science/logic/acgtk/default.nix
+++ b/pkgs/applications/science/logic/acgtk/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchurl, dune, ocamlPackages }:
+{ lib, stdenv, fetchurl, dune, ocamlPackages }:
 
 stdenv.mkDerivation {
 
@@ -18,7 +18,7 @@ stdenv.mkDerivation {
 
   inherit (dune) installPhase;
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     homepage = "https://acg.loria.fr/";
     description = "A toolkit for developing ACG signatures and lexicon";
     license = licenses.cecill20;
diff --git a/pkgs/applications/science/logic/aspino/default.nix b/pkgs/applications/science/logic/aspino/default.nix
index c1cf9034c02..f9cc97893da 100644
--- a/pkgs/applications/science/logic/aspino/default.nix
+++ b/pkgs/applications/science/logic/aspino/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchurl, fetchFromGitHub, zlib, boost }:
+{ lib, stdenv, fetchurl, fetchFromGitHub, zlib, boost }:
 
 let
   glucose' = fetchurl {
@@ -38,7 +38,7 @@ stdenv.mkDerivation {
     runHook postInstall
   '';
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "SAT/PseudoBoolean/MaxSat/ASP solver using glucose";
     maintainers = with maintainers; [ gebner ];
     platforms = platforms.unix;
diff --git a/pkgs/applications/science/logic/boolector/default.nix b/pkgs/applications/science/logic/boolector/default.nix
index 0364a76639a..2898ce4e1f6 100644
--- a/pkgs/applications/science/logic/boolector/default.nix
+++ b/pkgs/applications/science/logic/boolector/default.nix
@@ -59,7 +59,7 @@ stdenv.mkDerivation rec {
     cp $out/include/boolector/btortypes.h $out/include/btortypes.h
   '';
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "An extremely fast SMT solver for bit-vectors and arrays";
     homepage    = "https://boolector.github.io";
     license     = licenses.mit;
diff --git a/pkgs/applications/science/logic/btor2tools/default.nix b/pkgs/applications/science/logic/btor2tools/default.nix
index 7d2aed7596e..355274d1e1c 100644
--- a/pkgs/applications/science/logic/btor2tools/default.nix
+++ b/pkgs/applications/science/logic/btor2tools/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, cmake, fetchFromGitHub, fixDarwinDylibNames }:
+{ lib, stdenv, cmake, fetchFromGitHub, fixDarwinDylibNames }:
 
 stdenv.mkDerivation rec {
   pname = "btor2tools";
@@ -23,7 +23,7 @@ stdenv.mkDerivation rec {
 
   outputs = [ "out" "dev" "lib" ];
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "A generic parser and tool package for the BTOR2 format";
     homepage    = "https://github.com/Boolector/btor2tools";
     license     = licenses.mit;
diff --git a/pkgs/applications/science/logic/cadical/default.nix b/pkgs/applications/science/logic/cadical/default.nix
index e3707ff7dab..ca5e6b5c419 100644
--- a/pkgs/applications/science/logic/cadical/default.nix
+++ b/pkgs/applications/science/logic/cadical/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchFromGitHub }:
+{ lib, stdenv, fetchFromGitHub }:
 
 stdenv.mkDerivation rec {
   pname = "cadical";
@@ -21,7 +21,7 @@ stdenv.mkDerivation rec {
     install -Dm0755 {LICEN?E,README*,VERSION} "$out/share/doc/${pname}-${version}/"
   '';
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "Simplified Satisfiability Solver";
     maintainers = with maintainers; [ shnarazk ];
     platforms = platforms.unix;
diff --git a/pkgs/applications/science/logic/cedille/default.nix b/pkgs/applications/science/logic/cedille/default.nix
index 7b181790f14..2b099e7664a 100644
--- a/pkgs/applications/science/logic/cedille/default.nix
+++ b/pkgs/applications/science/logic/cedille/default.nix
@@ -46,7 +46,7 @@ stdenv.mkDerivation rec {
     cp -r lib/ $out/lib/cedille/
   '';
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "An interactive theorem-prover and dependently typed programming language, based on extrinsic (aka Curry-style) type theory";
     homepage = "https://cedille.github.io/";
     license = licenses.mit;
diff --git a/pkgs/applications/science/logic/celf/default.nix b/pkgs/applications/science/logic/celf/default.nix
index 9dc20a61a4d..044a6f3ca1c 100644
--- a/pkgs/applications/science/logic/celf/default.nix
+++ b/pkgs/applications/science/logic/celf/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchFromGitHub, smlnj }:
+{ lib, stdenv, fetchFromGitHub, smlnj }:
 
 stdenv.mkDerivation rec {
   pname = "celf";
@@ -26,7 +26,7 @@ stdenv.mkDerivation rec {
     ./.mkexec ${smlnj}/bin/sml $out/bin celf
   '';
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "Linear logic programming system";
     homepage = "https://github.com/clf/celf";
     license = licenses.gpl3;
diff --git a/pkgs/applications/science/logic/clprover/clprover.nix b/pkgs/applications/science/logic/clprover/clprover.nix
index e53bbe68837..f3049a659d1 100644
--- a/pkgs/applications/science/logic/clprover/clprover.nix
+++ b/pkgs/applications/science/logic/clprover/clprover.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchzip }:
+{ lib, stdenv, fetchzip }:
 
 stdenv.mkDerivation {
   pname = "clprover";
@@ -17,7 +17,7 @@ stdenv.mkDerivation {
     cp -r examples $out/share/clprover/examples
   '';
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "Resolution-based theorem prover for Coalition Logic implemented in C++";
     homepage = "http://cgi.csc.liv.ac.uk/~ullrich/CLProver++/";
     license = licenses.gpl3; # Note that while the website states that it is GPLv2 but the file in the zip as well as the comments in the source state it is GPLv3
diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix
index 9d0876d8d05..fae17a5e09f 100644
--- a/pkgs/applications/science/logic/coq/default.nix
+++ b/pkgs/applications/science/logic/coq/default.nix
@@ -5,10 +5,10 @@
 # - The exact version can be specified through the `version` argument to
 #   the derivation; it defaults to the latest stable version.
 
-{ stdenv, fetchzip, writeText, pkgconfig, gnumake42
+{ lib, stdenv, fetchzip, writeText, pkgconfig, gnumake42
 , customOCamlPackages ? null
 , ocamlPackages_4_05, ocamlPackages_4_09, ocamlPackages_4_10, ncurses
-, buildIde ? !(stdenv.isDarwin && stdenv.lib.versionAtLeast version "8.10")
+, buildIde ? !(stdenv.isDarwin && lib.versionAtLeast version "8.10")
 , glib, gnome3, wrapGAppsHook
 , csdp ? null
 , version, coq-version ? null,
@@ -166,7 +166,7 @@ self = stdenv.mkDerivation {
     ln -s $out/lib/coq $OCAMLFIND_DESTDIR/coq
   '';
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "Coq proof assistant";
     longDescription = ''
       Coq is a formal proof management system.  It provides a formal language
diff --git a/pkgs/applications/science/logic/coq2html/default.nix b/pkgs/applications/science/logic/coq2html/default.nix
index e53e8e7392c..46f2ebd775b 100644
--- a/pkgs/applications/science/logic/coq2html/default.nix
+++ b/pkgs/applications/science/logic/coq2html/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchgit, ocaml }:
+{ lib, stdenv, fetchgit, ocaml }:
 
 let
   version = "20170720";
@@ -21,7 +21,7 @@ stdenv.mkDerivation {
     cp coq2html $out/bin
   '';
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "HTML documentation generator for Coq source files";
     longDescription = ''
       coq2html is an HTML documentation generator for Coq source files. It is
diff --git a/pkgs/applications/science/logic/cryptominisat/default.nix b/pkgs/applications/science/logic/cryptominisat/default.nix
index ddbb140c9ba..042a4b23566 100644
--- a/pkgs/applications/science/logic/cryptominisat/default.nix
+++ b/pkgs/applications/science/logic/cryptominisat/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchFromGitHub, cmake, python3, xxd, boost, fetchpatch }:
+{ lib, stdenv, fetchFromGitHub, cmake, python3, xxd, boost, fetchpatch }:
 
 stdenv.mkDerivation rec {
   pname = "cryptominisat";
@@ -22,7 +22,7 @@ stdenv.mkDerivation rec {
   buildInputs = [ python3 boost ];
   nativeBuildInputs = [ cmake xxd ];
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "An advanced SAT Solver";
     homepage    = "https://github.com/msoos/cryptominisat";
     license     = licenses.mit;
diff --git a/pkgs/applications/science/logic/cubicle/default.nix b/pkgs/applications/science/logic/cubicle/default.nix
index bfb6a57fb33..aa3fba635ff 100644
--- a/pkgs/applications/science/logic/cubicle/default.nix
+++ b/pkgs/applications/science/logic/cubicle/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchurl, ocamlPackages }:
+{ lib, stdenv, fetchurl, ocamlPackages }:
 
 stdenv.mkDerivation rec {
   pname = "cubicle";
@@ -14,7 +14,7 @@ stdenv.mkDerivation rec {
 
   buildInputs = with ocamlPackages; [ ocaml findlib functory ];
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "An open source model checker for verifying safety properties of array-based systems";
     homepage = "http://cubicle.lri.fr/";
     license = licenses.asl20;
diff --git a/pkgs/applications/science/logic/cvc3/default.nix b/pkgs/applications/science/logic/cvc3/default.nix
index be80565115f..63efe0a2d05 100644
--- a/pkgs/applications/science/logic/cvc3/default.nix
+++ b/pkgs/applications/science/logic/cvc3/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchurl, flex, bison, gmp, perl }:
+{ lib, stdenv, fetchurl, flex, bison, gmp, perl }:
 
 stdenv.mkDerivation rec {
     pname = "cvc3";
@@ -23,7 +23,7 @@ stdenv.mkDerivation rec {
     done
   '';
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "A prover for satisfiability modulo theory (SMT)";
     maintainers = with maintainers;
       [ raskin ];
diff --git a/pkgs/applications/science/logic/cvc4/default.nix b/pkgs/applications/science/logic/cvc4/default.nix
index 1a92247c54d..fd31a5732e3 100644
--- a/pkgs/applications/science/logic/cvc4/default.nix
+++ b/pkgs/applications/science/logic/cvc4/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchFromGitHub, cmake, cln, gmp, git, swig, pkgconfig
+{ lib, stdenv, fetchFromGitHub, cmake, cln, gmp, git, swig, pkgconfig
 , readline, libantlr3c, boost, jdk, python3, antlr3_4
 }:
 
@@ -35,7 +35,7 @@ stdenv.mkDerivation rec {
     "-DCMAKE_BUILD_TYPE=Production"
   ];
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "A high-performance theorem prover and SMT solver";
     homepage    = "http://cvc4.cs.stanford.edu/web/";
     license     = licenses.gpl3;
diff --git a/pkgs/applications/science/logic/drat-trim/default.nix b/pkgs/applications/science/logic/drat-trim/default.nix
index 81e20df3342..c58a29dc289 100644
--- a/pkgs/applications/science/logic/drat-trim/default.nix
+++ b/pkgs/applications/science/logic/drat-trim/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchFromGitHub }:
+{ lib, stdenv, fetchFromGitHub }:
 
 stdenv.mkDerivation {
   pname = "drat-trim-unstable";
@@ -19,7 +19,7 @@ stdenv.mkDerivation {
     install -Dt $out/bin drat-trim lrat-check
   '';
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "A proof checker for unSAT proofs";
     longDescription = ''
       DRAT-trim is a satisfiability proof checking and trimming
diff --git a/pkgs/applications/science/logic/eprover/default.nix b/pkgs/applications/science/logic/eprover/default.nix
index a3844dc3700..14c46f88b27 100644
--- a/pkgs/applications/science/logic/eprover/default.nix
+++ b/pkgs/applications/science/logic/eprover/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchurl, which }:
+{ lib, stdenv, fetchurl, which }:
 
 stdenv.mkDerivation rec {
   pname = "eprover";
@@ -19,7 +19,7 @@ stdenv.mkDerivation rec {
     "--man-prefix=$(out)/share/man"
   ];
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "Automated theorem prover for full first-order logic with equality";
     homepage = "http://www.eprover.org/";
     license = licenses.gpl2;
diff --git a/pkgs/applications/science/logic/fast-downward/default.nix b/pkgs/applications/science/logic/fast-downward/default.nix
index cc14fd7706a..bc825703ee3 100644
--- a/pkgs/applications/science/logic/fast-downward/default.nix
+++ b/pkgs/applications/science/logic/fast-downward/default.nix
@@ -50,7 +50,7 @@ stdenv.mkDerivation {
       --replace 'args.build = "release"' "args.build = \"$out/libexec/fast-downward\""
   '';
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "A domain-independent planning system";
     homepage = "http://www.fast-downward.org/";
     license = licenses.gpl3Plus;
diff --git a/pkgs/applications/science/logic/glucose/default.nix b/pkgs/applications/science/logic/glucose/default.nix
index 0a8fad484da..5ba8208d6e1 100644
--- a/pkgs/applications/science/logic/glucose/default.nix
+++ b/pkgs/applications/science/logic/glucose/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchurl, zlib }:
+{ lib, stdenv, fetchurl, zlib }:
 stdenv.mkDerivation rec {
   pname = "glucose";
   version = "4.1";
@@ -18,7 +18,7 @@ stdenv.mkDerivation rec {
     install -Dm0755 ../{LICEN?E,README*,Changelog*} "$out/share/doc/${pname}-${version}/"
   '';
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "Modern, parallel SAT solver (sequential version)";
     license = licenses.mit;
     platforms = platforms.unix;
diff --git a/pkgs/applications/science/logic/glucose/syrup.nix b/pkgs/applications/science/logic/glucose/syrup.nix
index 816f8504a52..17342858fb8 100644
--- a/pkgs/applications/science/logic/glucose/syrup.nix
+++ b/pkgs/applications/science/logic/glucose/syrup.nix
@@ -1,4 +1,4 @@
-{ stdenv, zlib, glucose }:
+{ lib, stdenv, zlib, glucose }:
 stdenv.mkDerivation rec {
   pname = "glucose-syrup";
   version = glucose.version;
@@ -15,7 +15,7 @@ stdenv.mkDerivation rec {
     install -Dm0755 ../{LICEN?E,README*,Changelog*} "$out/share/doc/${pname}-${version}/"
   '';
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "Modern, parallel SAT solver (parallel version)";
     license = licenses.unfreeRedistributable;
     platforms = platforms.unix;
diff --git a/pkgs/applications/science/logic/hol/default.nix b/pkgs/applications/science/logic/hol/default.nix
index dbafee7d600..6fc7286154a 100644
--- a/pkgs/applications/science/logic/hol/default.nix
+++ b/pkgs/applications/science/logic/hol/default.nix
@@ -1,4 +1,4 @@
-{stdenv, pkgs, fetchurl, graphviz, fontconfig, liberation_ttf,
+{lib, stdenv, pkgs, fetchurl, graphviz, fontconfig, liberation_ttf,
  experimentalKernel ? true}:
 
 let
@@ -65,7 +65,7 @@ stdenv.mkDerivation {
     # ln -s $out/src/hol4.${version}/bin $out/bin
   '';
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "Interactive theorem prover based on Higher-Order Logic";
     longDescription = ''
       HOL4 is the latest version of the HOL interactive proof
diff --git a/pkgs/applications/science/logic/hol_light/default.nix b/pkgs/applications/science/logic/hol_light/default.nix
index 9c3030517e3..24faa98f777 100644
--- a/pkgs/applications/science/logic/hol_light/default.nix
+++ b/pkgs/applications/science/logic/hol_light/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, runtimeShell, fetchFromGitHub, fetchpatch, ocaml, num, camlp5 }:
+{ lib, stdenv, runtimeShell, fetchFromGitHub, fetchpatch, ocaml, num, camlp5 }:
 
 let
   load_num =
@@ -45,7 +45,7 @@ stdenv.mkDerivation {
     chmod a+x "$out/bin/hol_light"
   '';
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "Interactive theorem prover based on Higher-Order Logic";
     homepage    = "http://www.cl.cam.ac.uk/~jrh13/hol-light/";
     license     = licenses.bsd2;
diff --git a/pkgs/applications/science/logic/iprover/default.nix b/pkgs/applications/science/logic/iprover/default.nix
index 310a95d7e7a..1f02d30cf25 100644
--- a/pkgs/applications/science/logic/iprover/default.nix
+++ b/pkgs/applications/science/logic/iprover/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchurl, ocaml, eprover, zlib }:
+{ lib, stdenv, fetchurl, ocaml, eprover, zlib }:
 
 stdenv.mkDerivation rec {
   pname = "iprover";
@@ -23,7 +23,7 @@ stdenv.mkDerivation rec {
     chmod a+x  "$out"/bin/iprover
   '';
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "An automated first-order logic theorem prover";
     homepage = "http://www.cs.man.ac.uk/~korovink/iprover/";
     maintainers = with maintainers; [ raskin gebner ];
diff --git a/pkgs/applications/science/logic/isabelle/default.nix b/pkgs/applications/science/logic/isabelle/default.nix
index a12d75eabbe..9472d4b9b29 100644
--- a/pkgs/applications/science/logic/isabelle/default.nix
+++ b/pkgs/applications/science/logic/isabelle/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchurl, perl, nettools, java, polyml, z3, rlwrap }:
+{ lib, stdenv, fetchurl, perl, nettools, java, polyml, z3, rlwrap }:
 # nettools needed for hostname
 
 stdenv.mkDerivation rec {
@@ -66,7 +66,7 @@ stdenv.mkDerivation rec {
     bin/isabelle install $out/bin
   '';
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "A generic proof assistant";
 
     longDescription = ''
diff --git a/pkgs/applications/science/logic/key/default.nix b/pkgs/applications/science/logic/key/default.nix
index b08c4d84d1f..531081beafa 100644
--- a/pkgs/applications/science/logic/key/default.nix
+++ b/pkgs/applications/science/logic/key/default.nix
@@ -1,4 +1,4 @@
-{ stdenv
+{ lib, stdenv
 , fetchurl
 , unzip
 , jdk
@@ -56,7 +56,7 @@ in stdenv.mkDerivation rec {
     touch $out
   '';
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "Java formal verification tool";
     homepage = "https://www.key-project.org"; # also https://formal.iti.kit.edu/key/
     longDescription = ''
diff --git a/pkgs/applications/science/logic/lean/default.nix b/pkgs/applications/science/logic/lean/default.nix
index f5b7ccd76b1..5bf33a8a359 100644
--- a/pkgs/applications/science/logic/lean/default.nix
+++ b/pkgs/applications/science/logic/lean/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchFromGitHub, cmake, gmp, coreutils }:
+{ lib, stdenv, fetchFromGitHub, cmake, gmp, coreutils }:
 
 stdenv.mkDerivation rec {
   pname = "lean";
@@ -27,7 +27,7 @@ stdenv.mkDerivation rec {
       --replace "greadlink" "${coreutils}/bin/readlink"
   '';
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "Automatic and interactive theorem prover";
     homepage    = "https://leanprover.github.io/";
     changelog   = "https://github.com/leanprover-community/lean/blob/v${version}/doc/changes.md";
diff --git a/pkgs/applications/science/logic/lean2/default.nix b/pkgs/applications/science/logic/lean2/default.nix
index 9ac4f2a6c6b..b3c6a51d440 100644
--- a/pkgs/applications/science/logic/lean2/default.nix
+++ b/pkgs/applications/science/logic/lean2/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchFromGitHub, cmake, gmp, mpfr, python
+{ lib, stdenv, fetchFromGitHub, cmake, gmp, mpfr, python
 , gperftools, ninja, makeWrapper }:
 
 stdenv.mkDerivation {
@@ -26,7 +26,7 @@ stdenv.mkDerivation {
     wrapProgram $out/bin/linja --prefix PATH : $out/bin:${ninja}/bin
   '';
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "Automatic and interactive theorem prover (version with HoTT support)";
     homepage    = "http://leanprover.github.io";
     license     = licenses.asl20;
diff --git a/pkgs/applications/science/logic/leo2/default.nix b/pkgs/applications/science/logic/leo2/default.nix
index b43bfb80135..520c47d7500 100644
--- a/pkgs/applications/science/logic/leo2/default.nix
+++ b/pkgs/applications/science/logic/leo2/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchurl, makeWrapper, eprover, ocaml, perl, zlib }:
+{ lib, stdenv, fetchurl, makeWrapper, eprover, ocaml, perl, zlib }:
 
 stdenv.mkDerivation rec {
   pname = "leo2";
@@ -27,7 +27,7 @@ stdenv.mkDerivation rec {
       --add-flags "--atprc $out/etc/leoatprc"
   '';
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "A high-performance typed higher order prover";
     maintainers = [ maintainers.raskin ];
     platforms = platforms.linux;
diff --git a/pkgs/applications/science/logic/lingeling/default.nix b/pkgs/applications/science/logic/lingeling/default.nix
index 1805f6cdcc8..08bd0e4d637 100644
--- a/pkgs/applications/science/logic/lingeling/default.nix
+++ b/pkgs/applications/science/logic/lingeling/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchFromGitHub
+{ lib, stdenv, fetchFromGitHub
 , aiger
 }:
 
@@ -39,7 +39,7 @@ stdenv.mkDerivation {
 
   outputs = [ "out" "dev" "lib" ];
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "Fast SAT solver";
     homepage    = "http://fmv.jku.at/lingeling/";
     license     = licenses.mit;
diff --git a/pkgs/applications/science/logic/mcrl2/default.nix b/pkgs/applications/science/logic/mcrl2/default.nix
index 584988f2b40..56898f163b9 100644
--- a/pkgs/applications/science/logic/mcrl2/default.nix
+++ b/pkgs/applications/science/logic/mcrl2/default.nix
@@ -1,4 +1,4 @@
-{stdenv, fetchurl, cmake, libGLU, libGL, qt5, boost}:
+{lib, stdenv, fetchurl, cmake, libGLU, libGL, qt5, boost}:
 
 stdenv.mkDerivation rec {
   version = "201707";
@@ -13,7 +13,7 @@ stdenv.mkDerivation rec {
   nativeBuildInputs = [ cmake ];
   buildInputs = [ libGLU libGL qt5.qtbase boost ];
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "A toolset for model-checking concurrent systems and protocols";
     longDescription = ''
       A formal specification language with an associated toolset,
diff --git a/pkgs/applications/science/logic/metis-prover/default.nix b/pkgs/applications/science/logic/metis-prover/default.nix
index 5755abfd907..e30a897e565 100644
--- a/pkgs/applications/science/logic/metis-prover/default.nix
+++ b/pkgs/applications/science/logic/metis-prover/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchFromGitHub, perl, mlton }:
+{ lib, stdenv, fetchFromGitHub, perl, mlton }:
 
 stdenv.mkDerivation {
   pname = "metis-prover";
@@ -22,7 +22,7 @@ stdenv.mkDerivation {
     install -Dm0755 bin/mlton/metis $out/bin/metis
   '';
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "Automatic theorem prover for first-order logic with equality";
     homepage = "http://www.gilith.com/research/metis/";
     license = licenses.mit;
diff --git a/pkgs/applications/science/logic/minisat/default.nix b/pkgs/applications/science/logic/minisat/default.nix
index df1800e6c31..10d38088274 100644
--- a/pkgs/applications/science/logic/minisat/default.nix
+++ b/pkgs/applications/science/logic/minisat/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchFromGitHub, cmake, zlib }:
+{ lib, stdenv, fetchFromGitHub, cmake, zlib }:
 
 stdenv.mkDerivation rec {
   pname = "minisat";
@@ -14,7 +14,7 @@ stdenv.mkDerivation rec {
   nativeBuildInputs = [ cmake ];
   buildInputs = [ zlib ];
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "Compact and readable SAT solver";
     maintainers = with maintainers; [ gebner raskin ];
     platforms = platforms.unix;
diff --git a/pkgs/applications/science/logic/open-wbo/default.nix b/pkgs/applications/science/logic/open-wbo/default.nix
index c314127e74b..77db8ae3384 100644
--- a/pkgs/applications/science/logic/open-wbo/default.nix
+++ b/pkgs/applications/science/logic/open-wbo/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchFromGitHub, zlib, gmp }:
+{ lib, stdenv, fetchFromGitHub, zlib, gmp }:
 
 stdenv.mkDerivation {
   name = "open-wbo-2.0";
@@ -17,7 +17,7 @@ stdenv.mkDerivation {
     install -Dm0755 open-wbo_release $out/bin/open-wbo
   '';
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "State-of-the-art MaxSAT and Pseudo-Boolean solver";
     maintainers = with maintainers; [ gebner ];
     platforms = platforms.unix;
diff --git a/pkgs/applications/science/logic/opensmt/default.nix b/pkgs/applications/science/logic/opensmt/default.nix
index 03b3ce4ff0b..3b4dd20931c 100644
--- a/pkgs/applications/science/logic/opensmt/default.nix
+++ b/pkgs/applications/science/logic/opensmt/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchurl, automake, libtool, autoconf, intltool, perl
+{ lib, stdenv, fetchurl, automake, libtool, autoconf, intltool, perl
 , gmpxx, flex, bison
 }:
 
@@ -13,7 +13,7 @@ stdenv.mkDerivation rec {
 
   buildInputs = [ automake libtool autoconf intltool perl gmpxx flex bison ];
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "A satisfiability modulo theory (SMT) solver";
     maintainers = [ maintainers.raskin ];
     platforms = platforms.linux;
diff --git a/pkgs/applications/science/logic/poly/default.nix b/pkgs/applications/science/logic/poly/default.nix
index ee50a2d8504..db124c379ca 100644
--- a/pkgs/applications/science/logic/poly/default.nix
+++ b/pkgs/applications/science/logic/poly/default.nix
@@ -1,4 +1,4 @@
-{stdenv, fetchFromGitHub, gmp, cmake, python}:
+{lib, stdenv, fetchFromGitHub, gmp, cmake, python}:
 
 stdenv.mkDerivation rec {
   pname = "libpoly";
@@ -16,7 +16,7 @@ stdenv.mkDerivation rec {
 
   buildInputs = [ gmp python ];
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     homepage = "https://github.com/SRI-CSL/libpoly";
     description = "C library for manipulating polynomials";
     license = licenses.lgpl3;
diff --git a/pkgs/applications/science/logic/prooftree/default.nix b/pkgs/applications/science/logic/prooftree/default.nix
index 98313e48cb2..4db3c333e97 100644
--- a/pkgs/applications/science/logic/prooftree/default.nix
+++ b/pkgs/applications/science/logic/prooftree/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchurl, pkgconfig, ncurses, ocamlPackages }:
+{ lib, stdenv, fetchurl, pkgconfig, ncurses, ocamlPackages }:
 
 stdenv.mkDerivation rec {
   pname = "prooftree";
@@ -16,7 +16,7 @@ stdenv.mkDerivation rec {
   dontAddPrefix = true;
   configureFlags = [ "--prefix" "$(out)" ];
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "A program for proof-tree visualization";
     longDescription = ''
       Prooftree is a program for proof-tree visualization during interactive
diff --git a/pkgs/applications/science/logic/spass/default.nix b/pkgs/applications/science/logic/spass/default.nix
index ece6f0b9f6a..77b297b4fbb 100644
--- a/pkgs/applications/science/logic/spass/default.nix
+++ b/pkgs/applications/science/logic/spass/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchurl, bison, flex }:
+{ lib, stdenv, fetchurl, bison, flex }:
 
 let
   baseVersion="3";
@@ -29,7 +29,7 @@ stdenv.mkDerivation {
     install -m0755 SPASS ${extraTools} $out/bin/
   '';
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "Automated theorem prover for first-order logic";
     maintainers = with maintainers;
     [
diff --git a/pkgs/applications/science/logic/stp/default.nix b/pkgs/applications/science/logic/stp/default.nix
index fcffc239b48..42926a87081 100644
--- a/pkgs/applications/science/logic/stp/default.nix
+++ b/pkgs/applications/science/logic/stp/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, cmake, boost, bison, flex, fetchFromGitHub, perl
+{ lib, stdenv, cmake, boost, bison, flex, fetchFromGitHub, perl
 , python3, python3Packages, zlib, minisat, cryptominisat }:
 
 stdenv.mkDerivation rec {
@@ -24,7 +24,7 @@ stdenv.mkDerivation rec {
     )
   '';
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "Simple Theorem Prover";
     maintainers = with maintainers; [ ];
     platforms = platforms.linux;
diff --git a/pkgs/applications/science/logic/tptp/default.nix b/pkgs/applications/science/logic/tptp/default.nix
index 4c63f8e72a3..9c91eaddfc4 100644
--- a/pkgs/applications/science/logic/tptp/default.nix
+++ b/pkgs/applications/science/logic/tptp/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchurl, yap, tcsh, perl, patchelf }:
+{ lib, stdenv, fetchurl, yap, tcsh, perl, patchelf }:
 
 stdenv.mkDerivation rec {
   pname = "TPTP";
@@ -36,7 +36,7 @@ stdenv.mkDerivation rec {
     ln -s $sharedir/Scripts/tptp4X $out/bin
   '';
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "Thousands of problems for theorem provers and tools";
     maintainers = with maintainers; [ raskin gebner ];
     # 6.3 GiB of data. Installation is unpacking and editing a few files.
diff --git a/pkgs/applications/science/logic/vampire/default.nix b/pkgs/applications/science/logic/vampire/default.nix
index dca03823e9e..b8854454446 100644
--- a/pkgs/applications/science/logic/vampire/default.nix
+++ b/pkgs/applications/science/logic/vampire/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchFromGitHub, fetchpatch, z3, zlib }:
+{ lib, stdenv, fetchFromGitHub, fetchpatch, z3, zlib }:
 
 stdenv.mkDerivation rec {
   pname = "vampire";
@@ -46,7 +46,7 @@ stdenv.mkDerivation rec {
     install -m0755 -D vampire_z3_rel* $out/bin/vampire
   '';
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     homepage = "https://vprover.github.io/";
     description = "The Vampire Theorem Prover";
     platforms = platforms.unix;
diff --git a/pkgs/applications/science/logic/verit/default.nix b/pkgs/applications/science/logic/verit/default.nix
index f20a8324157..81acbe4f2d0 100644
--- a/pkgs/applications/science/logic/verit/default.nix
+++ b/pkgs/applications/science/logic/verit/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchurl, autoreconfHook, gmp, flex, bison }:
+{ lib, stdenv, fetchurl, autoreconfHook, gmp, flex, bison }:
 
 stdenv.mkDerivation {
   pname = "veriT";
@@ -21,7 +21,7 @@ stdenv.mkDerivation {
     mkdir -p $out/bin
   '';
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "An open, trustable and efficient SMT-solver";
     homepage = "http://www.verit-solver.org/";
     license = licenses.bsd3;
diff --git a/pkgs/applications/science/logic/why3/default.nix b/pkgs/applications/science/logic/why3/default.nix
index eacff32bdf6..deb40c74284 100644
--- a/pkgs/applications/science/logic/why3/default.nix
+++ b/pkgs/applications/science/logic/why3/default.nix
@@ -1,4 +1,4 @@
-{ callPackage, fetchurl, fetchpatch, stdenv
+{ callPackage, fetchurl, fetchpatch, lib, stdenv
 , ocamlPackages, coqPackages, rubber, hevea, emacs }:
 
 stdenv.mkDerivation {
@@ -39,7 +39,7 @@ stdenv.mkDerivation {
 
   passthru.withProvers = callPackage ./with-provers.nix {};
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "A platform for deductive program verification";
     homepage    = "http://why3.lri.fr/";
     license     = licenses.lgpl21;
diff --git a/pkgs/applications/science/logic/yices/default.nix b/pkgs/applications/science/logic/yices/default.nix
index b8dd528a11c..a01a07b8954 100644
--- a/pkgs/applications/science/logic/yices/default.nix
+++ b/pkgs/applications/science/logic/yices/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchFromGitHub, gmp-static, gperf, autoreconfHook, libpoly }:
+{ lib, stdenv, fetchFromGitHub, gmp-static, gperf, autoreconfHook, libpoly }:
 
 stdenv.mkDerivation rec {
   pname = "yices";
@@ -34,7 +34,7 @@ stdenv.mkDerivation rec {
       ln -sfr $out/lib/libyices.so.{${version},${ver_XdotY}}
   '';
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "A high-performance theorem prover and SMT solver";
     homepage    = "http://yices.csl.sri.com";
     license     = licenses.gpl3;