diff options
Diffstat (limited to 'nixpkgs/pkgs/applications/science/logic')
82 files changed, 353 insertions, 337 deletions
diff --git a/nixpkgs/pkgs/applications/science/logic/abc/default.nix b/nixpkgs/pkgs/applications/science/logic/abc/default.nix index 426c5a9df323..cbcd452033ca 100644 --- a/nixpkgs/pkgs/applications/science/logic/abc/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/abc/default.nix @@ -1,4 +1,4 @@ -{ stdenv, fetchFromGitHub +{ lib, stdenv, fetchFromGitHub , readline, cmake }: @@ -16,13 +16,12 @@ stdenv.mkDerivation rec { nativeBuildInputs = [ cmake ]; buildInputs = [ readline ]; - enableParallelBuilding = true; installPhase = "mkdir -p $out/bin && mv abc $out/bin"; # 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/nixpkgs/pkgs/applications/science/logic/abella/default.nix b/nixpkgs/pkgs/applications/science/logic/abella/default.nix index 3d9a2e9bd67b..14ceb53f9bb0 100644 --- a/nixpkgs/pkgs/applications/science/logic/abella/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/abella/default.nix @@ -1,4 +1,4 @@ -{ stdenv, fetchurl, rsync, ocamlPackages }: +{ lib, stdenv, fetchurl, rsync, ocamlPackages }: stdenv.mkDerivation rec { pname = "abella"; @@ -31,8 +31,8 @@ stdenv.mkDerivation rec { objects with binding. ''; homepage = "http://abella-prover.org/"; - license = stdenv.lib.licenses.gpl3; - maintainers = with stdenv.lib.maintainers; [ bcdarwin ciil ]; - platforms = stdenv.lib.platforms.unix; + license = lib.licenses.gpl3; + maintainers = with lib.maintainers; [ bcdarwin ciil ]; + platforms = lib.platforms.unix; }; } diff --git a/nixpkgs/pkgs/applications/science/logic/acgtk/default.nix b/nixpkgs/pkgs/applications/science/logic/acgtk/default.nix index ccd080005076..13364beed5cb 100644 --- a/nixpkgs/pkgs/applications/science/logic/acgtk/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/acgtk/default.nix @@ -1,4 +1,4 @@ -{ stdenv, fetchurl, dune, ocamlPackages }: +{ lib, stdenv, fetchurl, dune, ocamlPackages }: stdenv.mkDerivation { @@ -16,9 +16,11 @@ stdenv.mkDerivation { buildPhase = "dune build"; - inherit (dune) installPhase; + installPhase = '' + dune install --prefix $out --libdir $OCAMLFIND_DESTDIR + ''; - 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/nixpkgs/pkgs/applications/science/logic/aiger/default.nix b/nixpkgs/pkgs/applications/science/logic/aiger/default.nix index aa5a59ed298a..15c45466b132 100644 --- a/nixpkgs/pkgs/applications/science/logic/aiger/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/aiger/default.nix @@ -1,4 +1,4 @@ -{ stdenv, fetchurl, picosat }: +{ lib, stdenv, fetchurl, picosat }: stdenv.mkDerivation rec { pname = "aiger"; @@ -48,8 +48,8 @@ stdenv.mkDerivation rec { meta = { description = "And-Inverter Graph (AIG) utilities"; homepage = "http://fmv.jku.at/aiger/"; - license = stdenv.lib.licenses.mit; - maintainers = with stdenv.lib.maintainers; [ thoughtpolice ]; - platforms = stdenv.lib.platforms.unix; + license = lib.licenses.mit; + maintainers = with lib.maintainers; [ thoughtpolice ]; + platforms = lib.platforms.unix; }; } diff --git a/nixpkgs/pkgs/applications/science/logic/aspino/default.nix b/nixpkgs/pkgs/applications/science/logic/aspino/default.nix index c1cf9034c02a..f9cc97893da8 100644 --- a/nixpkgs/pkgs/applications/science/logic/aspino/default.nix +++ b/nixpkgs/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/nixpkgs/pkgs/applications/science/logic/avy/default.nix b/nixpkgs/pkgs/applications/science/logic/avy/default.nix index 6b48c1e34488..fe2f30a55a33 100644 --- a/nixpkgs/pkgs/applications/science/logic/avy/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/avy/default.nix @@ -1,4 +1,4 @@ -{ stdenv, fetchgit, cmake, zlib, boost }: +{ lib, stdenv, fetchgit, cmake, zlib, boost }: stdenv.mkDerivation rec { pname = "avy"; @@ -11,10 +11,11 @@ stdenv.mkDerivation rec { fetchSubmodules = true; }; - buildInputs = [ cmake zlib boost.out boost.dev ]; + nativeBuildInputs = [ cmake ]; + buildInputs = [ zlib boost.out boost.dev ]; NIX_CFLAGS_COMPILE = toString ([ "-Wno-narrowing" ] # Squelch endless stream of warnings on same few things - ++ stdenv.lib.optionals stdenv.cc.isClang [ + ++ lib.optionals stdenv.cc.isClang [ "-Wno-empty-body" "-Wno-tautological-compare" "-Wc++11-compat-deprecated-writable-strings" @@ -39,9 +40,9 @@ stdenv.mkDerivation rec { meta = { description = "AIGER model checking for Property Directed Reachability"; homepage = "https://arieg.bitbucket.io/avy/"; - license = stdenv.lib.licenses.mit; - maintainers = with stdenv.lib.maintainers; [ thoughtpolice ]; - platforms = stdenv.lib.platforms.linux; + license = lib.licenses.mit; + maintainers = with lib.maintainers; [ thoughtpolice ]; + platforms = lib.platforms.linux; # See pkgs/applications/science/logic/glucose/default.nix # (The error is different due to glucose-fenv.patch, but the same) badPlatforms = [ "aarch64-linux" ]; diff --git a/nixpkgs/pkgs/applications/science/logic/boolector/default.nix b/nixpkgs/pkgs/applications/science/logic/boolector/default.nix index 0364a76639aa..6916379bdea6 100644 --- a/nixpkgs/pkgs/applications/science/logic/boolector/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/boolector/default.nix @@ -40,7 +40,7 @@ stdenv.mkDerivation rec { in # tests modelgen and modelgensmt2 spawn boolector in another processes and # macOS strips DYLD_LIBRARY_PATH, hardcode it for testing - stdenv.lib.optionalString stdenv.isDarwin '' + lib.optionalString stdenv.isDarwin '' cp -r bin bin.back install_name_tool -change libboolector.dylib $(pwd)/lib/libboolector.dylib bin/boolector '' + '' @@ -48,7 +48,7 @@ stdenv.mkDerivation rec { patchShebangs .. ''; - postCheck = stdenv.lib.optionalString stdenv.isDarwin '' + postCheck = lib.optionalString stdenv.isDarwin '' rm -rf bin mv bin.back bin ''; @@ -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/nixpkgs/pkgs/applications/science/logic/btor2tools/default.nix b/nixpkgs/pkgs/applications/science/logic/btor2tools/default.nix index 7d2aed7596e8..992d8b1de58f 100644 --- a/nixpkgs/pkgs/applications/science/logic/btor2tools/default.nix +++ b/nixpkgs/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"; @@ -11,7 +11,7 @@ stdenv.mkDerivation rec { sha256 = "0mfqmkgvyw8fa2c09kww107dmk180ch1hp98r5kv41vnc04iqb0s"; }; - nativeBuildInputs = [ cmake ] ++ stdenv.lib.optional stdenv.isDarwin fixDarwinDylibNames; + nativeBuildInputs = [ cmake ] ++ lib.optional stdenv.isDarwin fixDarwinDylibNames; installPhase = '' mkdir -p $out $dev/include/btor2parser/ $lib/lib @@ -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/nixpkgs/pkgs/applications/science/logic/cadical/default.nix b/nixpkgs/pkgs/applications/science/logic/cadical/default.nix index e3707ff7dab1..ca5e6b5c4195 100644 --- a/nixpkgs/pkgs/applications/science/logic/cadical/default.nix +++ b/nixpkgs/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/nixpkgs/pkgs/applications/science/logic/cedille/default.nix b/nixpkgs/pkgs/applications/science/logic/cedille/default.nix index 7b181790f140..2b099e7664a6 100644 --- a/nixpkgs/pkgs/applications/science/logic/cedille/default.nix +++ b/nixpkgs/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/nixpkgs/pkgs/applications/science/logic/celf/default.nix b/nixpkgs/pkgs/applications/science/logic/celf/default.nix index 9dc20a61a4d2..044a6f3ca1c4 100644 --- a/nixpkgs/pkgs/applications/science/logic/celf/default.nix +++ b/nixpkgs/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/nixpkgs/pkgs/applications/science/logic/clprover/clprover.nix b/nixpkgs/pkgs/applications/science/logic/clprover/clprover.nix index e53bbe688371..f3049a659d11 100644 --- a/nixpkgs/pkgs/applications/science/logic/clprover/clprover.nix +++ b/nixpkgs/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/nixpkgs/pkgs/applications/science/logic/coq/default.nix b/nixpkgs/pkgs/applications/science/logic/coq/default.nix index 2ebe75d3bc50..a2ff8382947b 100644 --- a/nixpkgs/pkgs/applications/science/logic/coq/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/coq/default.nix @@ -5,57 +5,76 @@ # - The exact version can be specified through the `version` argument to # the derivation; it defaults to the latest stable version. -{ stdenv, fetchFromGitHub, writeText, pkgconfig, gnumake42 -, ocamlPackages, ncurses -, buildIde ? !(stdenv.isDarwin && stdenv.lib.versionAtLeast version "8.10") +{ lib, stdenv, fetchzip, writeText, pkg-config, gnumake42 +, customOCamlPackages ? null +, ocamlPackages_4_05, ocamlPackages_4_09, ocamlPackages_4_10, ncurses +, buildIde ? !(stdenv.isDarwin && lib.versionAtLeast version "8.10") , glib, gnome3, wrapGAppsHook , csdp ? null -, version -}: - +, version, coq-version ? null, +}@args: +let lib = import ../../../../build-support/coq/extra-lib.nix {inherit (stdenv) lib;}; in +with builtins; with lib; let - sha256 = { - "8.5pl1" = "1976ki5xjg2r907xj9p7gs0kpdinywbwcqlgxqw75dgp0hkgi00n"; - "8.5pl2" = "109rrcrx7mz0fj7725kjjghfg5ydwb24hjsa5hspa27b4caah7rh"; - "8.5pl3" = "15c3rdk59nifzihsp97z4vjxis5xmsnrvpb86qiazj143z2fmdgw"; - "8.6" = "148mb48zpdax56c0blfi7v67lx014lnmrvxxasi28hsibyz2lvg4"; - "8.6.1" = "0llrxcxwy5j87vbbjnisw42rfw1n1pm5602ssx64xaxx3k176g6l"; - "8.7.0" = "1h18b7xpnx3ix9vsi5fx4zdcbxy7bhra7gd5c5yzxmk53cgf1p9m"; - "8.7.1" = "0gjn59jkbxwrihk8fx9d823wjyjh5m9gvj9l31nv6z6bcqhgdqi8"; - "8.7.2" = "0a0657xby8wdq4aqb2xsxp3n7pmc2w4yxjmrb2l4kccs1aqvaj4w"; - "8.8.0" = "13a4fka22hdxsjk11mgjb9ffzplfxyxp1sg5v1c8nk1grxlscgw8"; - "8.8.1" = "1hlf58gwazywbmfa48219amid38vqdl94yz21i11b4map6jfwhbk"; - "8.8.2" = "1lip3xja924dm6qblisk1bk0x8ai24s5xxqxphbdxj6djglj68fd"; - "8.9.0" = "1dkgdjc4n1m15m1p724hhi5cyxpqbjw6rxc5na6fl3v4qjjfnizh"; - "8.9.1" = "1xrq6mkhpq994bncmnijf8jwmwn961kkpl4mwwlv7j3dgnysrcv2"; - "8.10.0" = "138jw94wp4mg5dgjc2asn8ng09ayz1mxdznq342n0m469j803gzg"; - "8.10.1" = "072v2zkjzf7gj48137wpr3c9j0hg9pdhlr5l8jrgrwynld8fp7i4"; - "8.10.2" = "0znxmpy71bfw0p6x47i82jf5k7v41zbz9bdpn901ysn3ir8l3wrz"; - "8.11.0" = "1rfdic6mp7acx2zfwz7ziqk12g95bl9nyj68z4n20a5bcjv2pxpn"; - "8.11.1" = "0qriy9dy36dajsv5qmli8gd6v55mah02ya334nw49ky19v7518m0"; - "8.11.2" = "0f77ccyxdgbf1nrj5fa8qvrk1cyfy06fv8gj9kzfvlcgn0cf48sa"; - "8.12.0" = "18dc7k0piv6v064zgdadpw6mkkxk7j663hb3svgj5236fihjr0cz"; - "8.12.1" = "1rkcyjjrzcqw9xk93hsq0vvji4f8r5iq0f739mghk60bghkpnb7q"; - "8.12.2" = "18gscfm039pqhq4msq01nraig5dm9ab98bjca94zldf8jvdv0x2n"; - "8.13+beta1" = "1v4a6dpj41flspa4ihcr7m5ahqz10kbn62fmrldmv7gzq6jsyfyq"; - }.${version}; - coq-version = stdenv.lib.versions.majorMinor version; - versionAtLeast = stdenv.lib.versionAtLeast coq-version; - ideFlags = stdenv.lib.optionalString (buildIde && !versionAtLeast "8.10") + release = { + "8.5pl1".sha256 = "1976ki5xjg2r907xj9p7gs0kpdinywbwcqlgxqw75dgp0hkgi00n"; + "8.5pl2".sha256 = "109rrcrx7mz0fj7725kjjghfg5ydwb24hjsa5hspa27b4caah7rh"; + "8.5pl3".sha256 = "15c3rdk59nifzihsp97z4vjxis5xmsnrvpb86qiazj143z2fmdgw"; + "8.6.0".sha256 = "148mb48zpdax56c0blfi7v67lx014lnmrvxxasi28hsibyz2lvg4"; + "8.6.0".rev = "V8.6"; + "8.6.1".sha256 = "0llrxcxwy5j87vbbjnisw42rfw1n1pm5602ssx64xaxx3k176g6l"; + "8.7.0".sha256 = "1h18b7xpnx3ix9vsi5fx4zdcbxy7bhra7gd5c5yzxmk53cgf1p9m"; + "8.7.1".sha256 = "0gjn59jkbxwrihk8fx9d823wjyjh5m9gvj9l31nv6z6bcqhgdqi8"; + "8.7.2".sha256 = "0a0657xby8wdq4aqb2xsxp3n7pmc2w4yxjmrb2l4kccs1aqvaj4w"; + "8.8.0".sha256 = "13a4fka22hdxsjk11mgjb9ffzplfxyxp1sg5v1c8nk1grxlscgw8"; + "8.8.1".sha256 = "1hlf58gwazywbmfa48219amid38vqdl94yz21i11b4map6jfwhbk"; + "8.8.2".sha256 = "1lip3xja924dm6qblisk1bk0x8ai24s5xxqxphbdxj6djglj68fd"; + "8.9.0".sha256 = "1dkgdjc4n1m15m1p724hhi5cyxpqbjw6rxc5na6fl3v4qjjfnizh"; + "8.9.1".sha256 = "1xrq6mkhpq994bncmnijf8jwmwn961kkpl4mwwlv7j3dgnysrcv2"; + "8.10.0".sha256 = "138jw94wp4mg5dgjc2asn8ng09ayz1mxdznq342n0m469j803gzg"; + "8.10.1".sha256 = "072v2zkjzf7gj48137wpr3c9j0hg9pdhlr5l8jrgrwynld8fp7i4"; + "8.10.2".sha256 = "0znxmpy71bfw0p6x47i82jf5k7v41zbz9bdpn901ysn3ir8l3wrz"; + "8.11.0".sha256 = "1rfdic6mp7acx2zfwz7ziqk12g95bl9nyj68z4n20a5bcjv2pxpn"; + "8.11.1".sha256 = "0qriy9dy36dajsv5qmli8gd6v55mah02ya334nw49ky19v7518m0"; + "8.11.2".sha256 = "0f77ccyxdgbf1nrj5fa8qvrk1cyfy06fv8gj9kzfvlcgn0cf48sa"; + "8.12.0".sha256 = "18dc7k0piv6v064zgdadpw6mkkxk7j663hb3svgj5236fihjr0cz"; + "8.12.1".sha256 = "1rkcyjjrzcqw9xk93hsq0vvji4f8r5iq0f739mghk60bghkpnb7q"; + "8.12.2".sha256 = "18gscfm039pqhq4msq01nraig5dm9ab98bjca94zldf8jvdv0x2n"; + "8.13+beta1".sha256 = "1v4a6dpj41flspa4ihcr7m5ahqz10kbn62fmrldmv7gzq6jsyfyq"; + }; + releaseRev = v: "V${v}"; + fetched = import ../../../../build-support/coq/meta-fetch/default.nix + { inherit stdenv fetchzip; } + { inherit release releaseRev; location = { owner = "coq"; repo = "coq";}; } + args.version; + version = fetched.version; + coq-version = args.coq-version or (if version != "dev" then versions.majorMinor version else "dev"); + versionAtLeast = v: (coq-version == "dev") || (lib.versionAtLeast coq-version v); + ideFlags = optionalString (buildIde && !versionAtLeast "8.10") "-lablgtkdir ${ocamlPackages.lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt"; csdpPatch = if csdp != null then '' substituteInPlace plugins/micromega/sos.ml --replace "; csdp" "; ${csdp}/bin/csdp" substituteInPlace plugins/micromega/coq_micromega.ml --replace "System.is_in_system_path \"csdp\"" "true" '' else ""; + ocamlPackages = if !isNull customOCamlPackages then customOCamlPackages + else with versions; switch coq-version [ + { case = range "8.11" "8.13"; out = ocamlPackages_4_10; } + { case = range "8.7" "8.10"; out = ocamlPackages_4_09; } + { case = range "8.5" "8.6"; out = ocamlPackages_4_05; } + ] ocamlPackages_4_10; + ocamlBuildInputs = [ ocamlPackages.ocaml ocamlPackages.findlib ] + ++ optional (!versionAtLeast "8.10") ocamlPackages.camlp5 + ++ optional (!versionAtLeast "8.13") ocamlPackages.num + ++ optional (versionAtLeast "8.13") ocamlPackages.zarith; self = stdenv.mkDerivation { pname = "coq"; - inherit version; + inherit (fetched) version src; passthru = { inherit coq-version; - inherit ocamlPackages; + inherit ocamlPackages ocamlBuildInputs; # For compatibility - inherit (ocamlPackages) ocaml camlp5 findlib num; + inherit (ocamlPackages) ocaml camlp5 findlib num ; emacsBufferSetup = pkgs: '' ; Propagate coq paths to children (inherit-local-permanent coq-prog-name "${self}/bin/coqtop") @@ -67,7 +86,7 @@ self = stdenv.mkDerivation { (coq-prog-args)) (mapc (lambda (arg) (when (file-directory-p (concat arg "/lib/coq/${coq-version}/user-contrib")) - (setenv "COQPATH" (concat (getenv "COQPATH") ":" arg "/lib/coq/${coq-version}/user-contrib")))) '(${stdenv.lib.concatStringsSep " " (map (pkg: "\"${pkg}\"") pkgs)})) + (setenv "COQPATH" (concat (getenv "COQPATH") ":" arg "/lib/coq/${coq-version}/user-contrib")))) '(${concatStringsSep " " (map (pkg: "\"${pkg}\"") pkgs)})) ; TODO Abstract this pattern from here and nixBufferBuilders.withPackages! (defvar nixpkgs--coq-buffer-count 0) (when (eq nixpkgs--coq-buffer-count 0) @@ -102,27 +121,12 @@ self = stdenv.mkDerivation { ''; }; - src = fetchFromGitHub { - owner = "coq"; - repo = "coq"; - rev = "V${version}"; - inherit sha256; - }; - - nativeBuildInputs = [ pkgconfig ] - ++ stdenv.lib.optional (!versionAtLeast "8.6") gnumake42 - ; - buildInputs = [ ncurses ocamlPackages.ocaml ocamlPackages.findlib ] - ++ stdenv.lib.optional (!versionAtLeast "8.10") ocamlPackages.camlp5 - ++ stdenv.lib.optional (!versionAtLeast "8.12") ocamlPackages.num - ++ stdenv.lib.optionals buildIde - (if versionAtLeast "8.10" - then [ ocamlPackages.lablgtk3-sourceview3 glib gnome3.defaultIconTheme wrapGAppsHook ] - else [ ocamlPackages.lablgtk ]); - - propagatedBuildInputs = - stdenv.lib.optional (versionAtLeast "8.13") ocamlPackages.zarith - ++ stdenv.lib.optional (coq-version == "8.12") ocamlPackages.num; + nativeBuildInputs = [ pkg-config ] ++ optional (!versionAtLeast "8.6") gnumake42; + buildInputs = [ ncurses ] ++ ocamlBuildInputs + ++ optionals buildIde + (if versionAtLeast "8.10" + then [ ocamlPackages.lablgtk3-sourceview3 glib gnome3.defaultIconTheme wrapGAppsHook ] + else [ ocamlPackages.lablgtk ]); postPatch = '' UNAME=$(type -tp uname) @@ -162,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/nixpkgs/pkgs/applications/science/logic/coq2html/default.nix b/nixpkgs/pkgs/applications/science/logic/coq2html/default.nix index e53e8e7392c0..46f2ebd775bf 100644 --- a/nixpkgs/pkgs/applications/science/logic/coq2html/default.nix +++ b/nixpkgs/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/nixpkgs/pkgs/applications/science/logic/cryptominisat/default.nix b/nixpkgs/pkgs/applications/science/logic/cryptominisat/default.nix index ddbb140c9baa..33de2d27dc90 100644 --- a/nixpkgs/pkgs/applications/science/logic/cryptominisat/default.nix +++ b/nixpkgs/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"; @@ -11,7 +11,7 @@ stdenv.mkDerivation rec { sha256 = "00hmxdlyhn7pwk9jlvc5g0l5z5xqfchjzf5jgn3pkj9xhl8yqq50"; }; - patches = [ + patches = [ (fetchpatch { # https://github.com/msoos/cryptominisat/pull/621 url = "https://github.com/msoos/cryptominisat/commit/11a97003b0bfbfb61ed6c4e640212110d390c28c.patch"; @@ -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/nixpkgs/pkgs/applications/science/logic/cryptoverif/default.nix b/nixpkgs/pkgs/applications/science/logic/cryptoverif/default.nix index 78861786defa..4c9ce3e95959 100644 --- a/nixpkgs/pkgs/applications/science/logic/cryptoverif/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/cryptoverif/default.nix @@ -1,4 +1,4 @@ -{ stdenv, fetchurl, ocaml }: +{ lib, stdenv, fetchurl, ocaml }: stdenv.mkDerivation rec { pname = "cryptoverif"; @@ -30,8 +30,8 @@ stdenv.mkDerivation rec { meta = { description = "Cryptographic protocol verifier in the computational model"; homepage = "https://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/"; - license = stdenv.lib.licenses.cecill-b; - platforms = stdenv.lib.platforms.unix; - maintainers = [ stdenv.lib.maintainers.thoughtpolice ]; + license = lib.licenses.cecill-b; + platforms = lib.platforms.unix; + maintainers = [ lib.maintainers.thoughtpolice ]; }; } diff --git a/nixpkgs/pkgs/applications/science/logic/cubicle/default.nix b/nixpkgs/pkgs/applications/science/logic/cubicle/default.nix index bfb6a57fb33a..aa3fba635ffc 100644 --- a/nixpkgs/pkgs/applications/science/logic/cubicle/default.nix +++ b/nixpkgs/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/nixpkgs/pkgs/applications/science/logic/cvc3/default.nix b/nixpkgs/pkgs/applications/science/logic/cvc3/default.nix index be80565115fe..63efe0a2d05b 100644 --- a/nixpkgs/pkgs/applications/science/logic/cvc3/default.nix +++ b/nixpkgs/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/nixpkgs/pkgs/applications/science/logic/cvc4/default.nix b/nixpkgs/pkgs/applications/science/logic/cvc4/default.nix index 54a2f0225518..b0b3e5e610e6 100644 --- a/nixpkgs/pkgs/applications/science/logic/cvc4/default.nix +++ b/nixpkgs/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, pkg-config , readline, libantlr3c, boost, jdk, python3, antlr3_4 }: @@ -13,7 +13,7 @@ stdenv.mkDerivation rec { sha256 = "1rhs4pvzaa1wk00czrczp58b2cxfghpsnq534m0l3snnya2958jp"; }; - nativeBuildInputs = [ pkgconfig cmake ]; + nativeBuildInputs = [ pkg-config cmake ]; buildInputs = [ gmp git python3.pkgs.toml cln readline swig libantlr3c antlr3_4 boost jdk python3 ]; configureFlags = [ "--enable-language-bindings=c,c++,java" @@ -35,10 +35,7 @@ stdenv.mkDerivation rec { "-DCMAKE_BUILD_TYPE=Production" ]; - - enableParallelBuilding = true; - - 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/nixpkgs/pkgs/applications/science/logic/drat-trim/default.nix b/nixpkgs/pkgs/applications/science/logic/drat-trim/default.nix index 81e20df33424..c58a29dc2894 100644 --- a/nixpkgs/pkgs/applications/science/logic/drat-trim/default.nix +++ b/nixpkgs/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/nixpkgs/pkgs/applications/science/logic/ekrhyper/default.nix b/nixpkgs/pkgs/applications/science/logic/ekrhyper/default.nix index e1eb9a2dcc3b..38cc0f06088d 100644 --- a/nixpkgs/pkgs/applications/science/logic/ekrhyper/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/ekrhyper/default.nix @@ -1,4 +1,4 @@ -{stdenv, fetchurl, ocaml, perl}: +{lib, stdenv, fetchurl, ocaml, perl}: let s = # Generated upstream information rec { @@ -25,8 +25,8 @@ stdenv.mkDerivation { meta = { inherit (s) version; description = "Automated first-order theorem prover"; - license = stdenv.lib.licenses.gpl2 ; - maintainers = [stdenv.lib.maintainers.raskin]; - platforms = stdenv.lib.platforms.linux; + license = lib.licenses.gpl2 ; + maintainers = [lib.maintainers.raskin]; + platforms = lib.platforms.linux; }; } diff --git a/nixpkgs/pkgs/applications/science/logic/elan/default.nix b/nixpkgs/pkgs/applications/science/logic/elan/default.nix index 7a7da2c5f5d2..bb10998b2f45 100644 --- a/nixpkgs/pkgs/applications/science/logic/elan/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/elan/default.nix @@ -1,19 +1,19 @@ -{ lib, pkgconfig, curl, openssl, zlib, fetchFromGitHub, rustPlatform }: +{ lib, pkg-config, curl, openssl, zlib, fetchFromGitHub, rustPlatform }: rustPlatform.buildRustPackage rec { pname = "elan"; - version = "0.10.2"; + version = "0.10.3"; src = fetchFromGitHub { owner = "kha"; repo = "elan"; rev = "v${version}"; - sha256 = "0ycw1r364g5gwh8796dpv1israpg7zqwx8mcvnacv2lqj5iijmby"; + sha256 = "sha256-YkGfuqtvVfPcxJ8UqD5QidcNEy5brTWGEK4fR64Yz70="; }; - cargoSha256 = "0hcaiy046d2gnkp6sfpnkkprb3nd94i9q8dgqxxpwrc1j157x6z9"; + cargoSha256 = "sha256-2fYicpoEERwD4OjdpseKQOkDvZlb7NnOZcb6Tu+rQdA="; - nativeBuildInputs = [ pkgconfig ]; + nativeBuildInputs = [ pkg-config ]; buildInputs = [ curl zlib openssl ]; diff --git a/nixpkgs/pkgs/applications/science/logic/eprover/default.nix b/nixpkgs/pkgs/applications/science/logic/eprover/default.nix index a3844dc3700b..14c46f88b27c 100644 --- a/nixpkgs/pkgs/applications/science/logic/eprover/default.nix +++ b/nixpkgs/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/nixpkgs/pkgs/applications/science/logic/fast-downward/default.nix b/nixpkgs/pkgs/applications/science/logic/fast-downward/default.nix index a46542095373..bc825703ee3a 100644 --- a/nixpkgs/pkgs/applications/science/logic/fast-downward/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/fast-downward/default.nix @@ -16,8 +16,6 @@ stdenv.mkDerivation { cmakeFlags = lib.optional osi.withCplex [ "-DDOWNWARD_CPLEX_ROOT=${cplex}/cplex" ]; - enableParallelBuilding = true; - configurePhase = '' python build.py release ''; @@ -52,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/nixpkgs/pkgs/applications/science/logic/gappa/default.nix b/nixpkgs/pkgs/applications/science/logic/gappa/default.nix index 2ca1bcd30981..73f34f60fc47 100644 --- a/nixpkgs/pkgs/applications/science/logic/gappa/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/gappa/default.nix @@ -1,4 +1,4 @@ -{ stdenv, fetchurl, gmp, mpfr, boost }: +{ lib, stdenv, fetchurl, gmp, mpfr, boost }: stdenv.mkDerivation { name = "gappa-1.3.5"; @@ -16,8 +16,8 @@ stdenv.mkDerivation { meta = { homepage = "http://gappa.gforge.inria.fr/"; description = "Verifying and formally proving properties on numerical programs dealing with floating-point or fixed-point arithmetic"; - license = with stdenv.lib.licenses; [ cecill20 gpl2 ]; - maintainers = with stdenv.lib.maintainers; [ vbgl ]; - platforms = stdenv.lib.platforms.all; + license = with lib.licenses; [ cecill20 gpl2 ]; + maintainers = with lib.maintainers; [ vbgl ]; + platforms = lib.platforms.all; }; } diff --git a/nixpkgs/pkgs/applications/science/logic/glucose/default.nix b/nixpkgs/pkgs/applications/science/logic/glucose/default.nix index 0a8fad484da7..5ba8208d6e18 100644 --- a/nixpkgs/pkgs/applications/science/logic/glucose/default.nix +++ b/nixpkgs/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/nixpkgs/pkgs/applications/science/logic/glucose/syrup.nix b/nixpkgs/pkgs/applications/science/logic/glucose/syrup.nix index 816f8504a52e..17342858fb8f 100644 --- a/nixpkgs/pkgs/applications/science/logic/glucose/syrup.nix +++ b/nixpkgs/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/nixpkgs/pkgs/applications/science/logic/hol/default.nix b/nixpkgs/pkgs/applications/science/logic/hol/default.nix index dbafee7d6000..6fc7286154ae 100644 --- a/nixpkgs/pkgs/applications/science/logic/hol/default.nix +++ b/nixpkgs/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/nixpkgs/pkgs/applications/science/logic/hol_light/default.nix b/nixpkgs/pkgs/applications/science/logic/hol_light/default.nix index 9c3030517e32..24faa98f777b 100644 --- a/nixpkgs/pkgs/applications/science/logic/hol_light/default.nix +++ b/nixpkgs/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/nixpkgs/pkgs/applications/science/logic/iprover/default.nix b/nixpkgs/pkgs/applications/science/logic/iprover/default.nix index 310a95d7e7a6..ff88586e0353 100644 --- a/nixpkgs/pkgs/applications/science/logic/iprover/default.nix +++ b/nixpkgs/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"; @@ -11,7 +11,7 @@ stdenv.mkDerivation rec { buildInputs = [ ocaml eprover zlib ]; - preConfigure = ''patchShebangs .''; + preConfigure = "patchShebangs ."; installPhase = '' mkdir -p "$out/bin" @@ -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/nixpkgs/pkgs/applications/science/logic/isabelle/default.nix b/nixpkgs/pkgs/applications/science/logic/isabelle/default.nix index a12d75eabbe9..6c22c949483f 100644 --- a/nixpkgs/pkgs/applications/science/logic/isabelle/default.nix +++ b/nixpkgs/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 { @@ -18,7 +18,7 @@ stdenv.mkDerivation rec { }; buildInputs = [ perl polyml z3 ] - ++ stdenv.lib.optionals (!stdenv.isDarwin) [ nettools java ]; + ++ lib.optionals (!stdenv.isDarwin) [ nettools java ]; sourceRoot = dirname; @@ -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/nixpkgs/pkgs/applications/science/logic/jonprl/default.nix b/nixpkgs/pkgs/applications/science/logic/jonprl/default.nix index 3ee05a478bc2..379a9a483540 100644 --- a/nixpkgs/pkgs/applications/science/logic/jonprl/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/jonprl/default.nix @@ -1,4 +1,4 @@ -{ fetchgit, stdenv, smlnj, which }: +{ fetchgit, lib, stdenv, smlnj, which }: stdenv.mkDerivation rec { pname = "jonprl"; @@ -27,9 +27,9 @@ stdenv.mkDerivation rec { Inspired by Nuprl ''; homepage = "https://github.com/jonsterling/JonPRL"; - license = stdenv.lib.licenses.mit; - maintainers = with stdenv.lib.maintainers; [ puffnfresh ]; - platforms = stdenv.lib.platforms.linux; + license = lib.licenses.mit; + maintainers = with lib.maintainers; [ puffnfresh ]; + platforms = lib.platforms.linux; broken = true; }; } diff --git a/nixpkgs/pkgs/applications/science/logic/key/default.nix b/nixpkgs/pkgs/applications/science/logic/key/default.nix index b08c4d84d1fc..531081beafaf 100644 --- a/nixpkgs/pkgs/applications/science/logic/key/default.nix +++ b/nixpkgs/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/nixpkgs/pkgs/applications/science/logic/lci/default.nix b/nixpkgs/pkgs/applications/science/logic/lci/default.nix index 4775384a3ddc..593b2c54c5cf 100644 --- a/nixpkgs/pkgs/applications/science/logic/lci/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/lci/default.nix @@ -1,4 +1,4 @@ -{stdenv, fetchurl, readline}: +{lib, stdenv, fetchurl, readline}: stdenv.mkDerivation rec { version = "0.6"; pname = "lci"; @@ -8,9 +8,9 @@ stdenv.mkDerivation rec { }; buildInputs = [readline]; meta = { - description = ''Lambda calculus interpreter''; - maintainers = with stdenv.lib.maintainers; [raskin]; - platforms = with stdenv.lib.platforms; linux; - license = stdenv.lib.licenses.gpl3; + description = "Lambda calculus interpreter"; + maintainers = with lib.maintainers; [raskin]; + platforms = with lib.platforms; linux; + license = lib.licenses.gpl3; }; } diff --git a/nixpkgs/pkgs/applications/science/logic/lean/default.nix b/nixpkgs/pkgs/applications/science/logic/lean/default.nix index 88e1b4fbc0e1..1f3f7afa9d1b 100644 --- a/nixpkgs/pkgs/applications/science/logic/lean/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/lean/default.nix @@ -1,19 +1,18 @@ -{ stdenv, fetchFromGitHub, cmake, gmp, coreutils }: +{ lib, stdenv, fetchFromGitHub, cmake, gmp, coreutils }: stdenv.mkDerivation rec { pname = "lean"; - version = "3.23.0"; + version = "3.25.0"; src = fetchFromGitHub { owner = "leanprover-community"; repo = "lean"; rev = "v${version}"; - sha256 = "09mklc1p6ms1jayg2f89hqfmhca3h5744lli936l38ypn1d00sxx"; + sha256 = "sha256-/TlVoqgTGhRfC8d70kXc+VsEkURUksKNGRjYcww+F8g="; }; nativeBuildInputs = [ cmake ]; buildInputs = [ gmp ]; - enableParallelBuilding = true; cmakeDir = "../src"; @@ -23,12 +22,12 @@ stdenv.mkDerivation rec { postPatch = "patchShebangs ."; - postInstall = stdenv.lib.optionalString stdenv.isDarwin '' + postInstall = lib.optionalString stdenv.isDarwin '' substituteInPlace $out/bin/leanpkg \ --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/nixpkgs/pkgs/applications/science/logic/lean2/default.nix b/nixpkgs/pkgs/applications/science/logic/lean2/default.nix index 612c9d6f92a2..b3c6a51d440a 100644 --- a/nixpkgs/pkgs/applications/science/logic/lean2/default.nix +++ b/nixpkgs/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 { @@ -12,8 +12,8 @@ stdenv.mkDerivation { sha256 = "1xv3j487zhh1zf2b4v19xzw63s2sgjhg8d62a0kxxyknfmdf3khl"; }; - buildInputs = [ gmp mpfr cmake python gperftools ninja makeWrapper ]; - enableParallelBuilding = true; + nativeBuildInputs = [ cmake makeWrapper ninja ]; + buildInputs = [ gmp mpfr python gperftools ]; preConfigure = '' patchShebangs bin/leantags @@ -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/nixpkgs/pkgs/applications/science/logic/leo2/default.nix b/nixpkgs/pkgs/applications/science/logic/leo2/default.nix index b43bfb801358..520c47d7500b 100644 --- a/nixpkgs/pkgs/applications/science/logic/leo2/default.nix +++ b/nixpkgs/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/nixpkgs/pkgs/applications/science/logic/leo3/binary.nix b/nixpkgs/pkgs/applications/science/logic/leo3/binary.nix index 29a9adf94c4b..dda18c49b720 100644 --- a/nixpkgs/pkgs/applications/science/logic/leo3/binary.nix +++ b/nixpkgs/pkgs/applications/science/logic/leo3/binary.nix @@ -1,4 +1,4 @@ -{stdenv, fetchurl, openjdk, runtimeShell}: +{lib, stdenv, fetchurl, openjdk, runtimeShell}: stdenv.mkDerivation rec { pname = "leo3"; version = "1.2"; @@ -21,9 +21,9 @@ stdenv.mkDerivation rec { meta = { inherit version; description = "An automated theorem prover for classical higher-order logic with choice"; - license = stdenv.lib.licenses.bsd3; - maintainers = [stdenv.lib.maintainers.raskin]; - platforms = stdenv.lib.platforms.linux; + license = lib.licenses.bsd3; + maintainers = [lib.maintainers.raskin]; + platforms = lib.platforms.linux; homepage = "https://page.mi.fu-berlin.de/lex/leo3/"; }; } diff --git a/nixpkgs/pkgs/applications/science/logic/lingeling/default.nix b/nixpkgs/pkgs/applications/science/logic/lingeling/default.nix index 1805f6cdcc89..08bd0e4d6375 100644 --- a/nixpkgs/pkgs/applications/science/logic/lingeling/default.nix +++ b/nixpkgs/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/nixpkgs/pkgs/applications/science/logic/logisim/default.nix b/nixpkgs/pkgs/applications/science/logic/logisim/default.nix index ce86b2523116..1ca22cf769c6 100644 --- a/nixpkgs/pkgs/applications/science/logic/logisim/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/logisim/default.nix @@ -1,16 +1,16 @@ -{ stdenv, fetchurl, jre, makeWrapper }: +{ lib, stdenv, fetchurl, jre, makeWrapper }: let version = "2.7.1"; in stdenv.mkDerivation { pname = "logisim"; inherit version; - + src = fetchurl { url = "mirror://sourceforge/project/circuit/2.7.x/${version}/logisim-generic-${version}.jar"; sha256 = "1hkvc9zc7qmvjbl9579p84hw3n8wl3275246xlzj136i5b0phain"; }; - + phases = [ "installPhase" ]; nativeBuildInputs = [makeWrapper]; @@ -19,11 +19,11 @@ stdenv.mkDerivation { mkdir -pv $out/bin makeWrapper ${jre}/bin/java $out/bin/logisim --add-flags "-jar $src" ''; - + meta = { homepage = "http://ozark.hendrix.edu/~burch/logisim"; description = "Educational tool for designing and simulating digital logic circuits"; - license = stdenv.lib.licenses.gpl2Plus; - platforms = stdenv.lib.platforms.unix; + license = lib.licenses.gpl2Plus; + platforms = lib.platforms.unix; }; } diff --git a/nixpkgs/pkgs/applications/science/logic/ltl2ba/default.nix b/nixpkgs/pkgs/applications/science/logic/ltl2ba/default.nix index b5d13db3b9a1..30c13c6036f9 100644 --- a/nixpkgs/pkgs/applications/science/logic/ltl2ba/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/ltl2ba/default.nix @@ -1,4 +1,4 @@ -{ fetchurl, stdenv }: +{ fetchurl, lib, stdenv }: stdenv.mkDerivation rec { pname = "ltl2ba"; @@ -24,8 +24,8 @@ stdenv.mkDerivation rec { meta = { description = "Fast translation from LTL formulae to Buchi automata"; homepage = "http://www.lsv.ens-cachan.fr/~gastin/ltl2ba"; - license = stdenv.lib.licenses.gpl2Plus; - platforms = stdenv.lib.platforms.darwin ++ stdenv.lib.platforms.linux; - maintainers = [ stdenv.lib.maintainers.thoughtpolice ]; + license = lib.licenses.gpl2Plus; + platforms = lib.platforms.darwin ++ lib.platforms.linux; + maintainers = [ lib.maintainers.thoughtpolice ]; }; } diff --git a/nixpkgs/pkgs/applications/science/logic/mcrl2/default.nix b/nixpkgs/pkgs/applications/science/logic/mcrl2/default.nix index eb83eaf79c55..56898f163b99 100644 --- a/nixpkgs/pkgs/applications/science/logic/mcrl2/default.nix +++ b/nixpkgs/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"; @@ -10,11 +10,10 @@ stdenv.mkDerivation rec { sha256 = "1c8h94ja7271ph61zrcgnjgblxppld6v22f7f900prjgzbcfy14m"; }; - buildInputs = [ cmake libGLU libGL qt5.qtbase boost ]; + nativeBuildInputs = [ cmake ]; + buildInputs = [ libGLU libGL qt5.qtbase boost ]; - enableParallelBuilding = true; - - 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/nixpkgs/pkgs/applications/science/logic/mcy/default.nix b/nixpkgs/pkgs/applications/science/logic/mcy/default.nix index eba910e07eb1..dc1094f3e27d 100644 --- a/nixpkgs/pkgs/applications/science/logic/mcy/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/mcy/default.nix @@ -1,4 +1,4 @@ -{ stdenv, fetchFromGitHub +{ lib, stdenv, fetchFromGitHub , yosys, symbiyosys, python3 }: @@ -44,8 +44,8 @@ stdenv.mkDerivation { meta = { description = "Mutation-based coverage testing for hardware designs, with Yosys"; homepage = "https://github.com/YosysHQ/mcy"; - license = stdenv.lib.licenses.isc; - maintainers = with stdenv.lib.maintainers; [ thoughtpolice ]; - platforms = stdenv.lib.platforms.all; + license = lib.licenses.isc; + maintainers = with lib.maintainers; [ thoughtpolice ]; + platforms = lib.platforms.all; }; } diff --git a/nixpkgs/pkgs/applications/science/logic/metis-prover/default.nix b/nixpkgs/pkgs/applications/science/logic/metis-prover/default.nix index 5755abfd9078..e30a897e5659 100644 --- a/nixpkgs/pkgs/applications/science/logic/metis-prover/default.nix +++ b/nixpkgs/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/nixpkgs/pkgs/applications/science/logic/minisat/default.nix b/nixpkgs/pkgs/applications/science/logic/minisat/default.nix index df1800e6c31b..10d380882744 100644 --- a/nixpkgs/pkgs/applications/science/logic/minisat/default.nix +++ b/nixpkgs/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/nixpkgs/pkgs/applications/science/logic/monosat/default.nix b/nixpkgs/pkgs/applications/science/logic/monosat/default.nix index 63440213920c..259cdcea4432 100644 --- a/nixpkgs/pkgs/applications/science/logic/monosat/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/monosat/default.nix @@ -1,9 +1,9 @@ -{ stdenv, fetchpatch, fetchFromGitHub, cmake, zlib, gmp, jdk8, +{ lib, stdenv, fetchpatch, fetchFromGitHub, cmake, zlib, gmp, jdk8, # The JDK we use on Darwin currenly makes extensive use of rpaths which are # annoying and break the python library, so let's not bother for now includeJava ? !stdenv.hostPlatform.isDarwin, includeGplCode ? true }: -with stdenv.lib; +with lib; let boolToCmake = x: if x then "ON" else "OFF"; @@ -31,7 +31,8 @@ let core = stdenv.mkDerivation { name = "${pname}-${version}"; inherit src patches; - buildInputs = [ cmake zlib gmp jdk8 ]; + nativeBuildInputs = [ cmake ]; + buildInputs = [ zlib gmp jdk8 ]; cmakeFlags = [ "-DBUILD_STATIC=OFF" diff --git a/nixpkgs/pkgs/applications/science/logic/open-wbo/default.nix b/nixpkgs/pkgs/applications/science/logic/open-wbo/default.nix index c314127e74bf..77db8ae3384d 100644 --- a/nixpkgs/pkgs/applications/science/logic/open-wbo/default.nix +++ b/nixpkgs/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/nixpkgs/pkgs/applications/science/logic/opensmt/default.nix b/nixpkgs/pkgs/applications/science/logic/opensmt/default.nix index 03b3ce4ff0b7..1681d4545904 100644 --- a/nixpkgs/pkgs/applications/science/logic/opensmt/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/opensmt/default.nix @@ -1,25 +1,38 @@ -{ stdenv, fetchurl, automake, libtool, autoconf, intltool, perl -, gmpxx, flex, bison +{ stdenv, lib, fetchFromGitHub +, cmake, libedit, gmpxx, bison, flex +, enableReadline ? false, readline +, gtest }: stdenv.mkDerivation rec { pname = "opensmt"; - version = "20101017"; + version = "2.0.1"; - src = fetchurl { - url = "http://opensmt.googlecode.com/files/opensmt_src_${version}.tgz"; - sha256 = "0xrky7ixjaby5x026v7hn72xh7d401w9jhccxjn0khhn1x87p2w1"; + src = fetchFromGitHub { + owner = "usi-verification-and-security"; + repo = "opensmt"; + rev = "v${version}"; + sha256 = "uoIcXWsxxRsIuFsou3RcN9e48lc7cWMgRPVJLFVslDE="; }; - buildInputs = [ automake libtool autoconf intltool perl gmpxx flex bison ]; + nativeBuildInputs = [ cmake bison flex ]; + buildInputs = [ libedit gmpxx ] + ++ lib.optional enableReadline readline; - meta = with stdenv.lib; { + preConfigure = '' + substituteInPlace test/CMakeLists.txt \ + --replace 'FetchContent_Populate' '#FetchContent_Populate' + ''; + cmakeFlags = [ + "-Dgoogletest_SOURCE_DIR=${gtest.src}" + "-Dgoogletest_BINARY_DIR=./gtest-build" + ]; + + meta = with lib; { description = "A satisfiability modulo theory (SMT) solver"; maintainers = [ maintainers.raskin ]; platforms = platforms.linux; - license = licenses.gpl3; - homepage = "http://code.google.com/p/opensmt/"; - broken = true; - downloadPage = "http://code.google.com/p/opensmt/downloads/list"; + license = if enableReadline then licenses.gpl2Plus else licenses.mit; + homepage = "https://github.com/usi-verification-and-security/opensmt"; }; } diff --git a/nixpkgs/pkgs/applications/science/logic/ott/default.nix b/nixpkgs/pkgs/applications/science/logic/ott/default.nix index 48ad63eaa993..8752c4ef59d4 100644 --- a/nixpkgs/pkgs/applications/science/logic/ott/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/ott/default.nix @@ -1,4 +1,4 @@ -{ stdenv, fetchFromGitHub, pkgconfig, ocaml, opaline }: +{ lib, stdenv, fetchFromGitHub, pkg-config, ocaml, opaline }: stdenv.mkDerivation rec { pname = "ott"; @@ -11,12 +11,18 @@ stdenv.mkDerivation rec { sha256 = "0l81126i2qkz11fs5yrjdgymnqgjcs5avb7f951h61yh1s68jpnn"; }; - nativeBuildInputs = [ pkgconfig opaline ]; + nativeBuildInputs = [ pkg-config opaline ]; buildInputs = [ ocaml ]; installTargets = "ott.install"; - postInstall = "opaline -prefix $out"; + postInstall = '' + opaline -prefix $out + '' + # There is `emacsPackages.ott-mode` for this now. + + '' + rm -r $out/share/emacs + ''; meta = { description = "A tool for the working semanticist"; @@ -32,8 +38,8 @@ stdenv.mkDerivation rec { target-system terms. ''; homepage = "http://www.cl.cam.ac.uk/~pes20/ott"; - license = stdenv.lib.licenses.bsd3; - maintainers = with stdenv.lib.maintainers; [ jwiegley ]; - platforms = stdenv.lib.platforms.unix; + license = lib.licenses.bsd3; + maintainers = with lib.maintainers; [ jwiegley ]; + platforms = lib.platforms.unix; }; } diff --git a/nixpkgs/pkgs/applications/science/logic/otter/default.nix b/nixpkgs/pkgs/applications/science/logic/otter/default.nix index a7eec20548c9..2ad066e53f74 100644 --- a/nixpkgs/pkgs/applications/science/logic/otter/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/otter/default.nix @@ -1,4 +1,4 @@ -{stdenv, fetchurl, tcsh, libXaw, libXt, libX11}: +{lib, stdenv, fetchurl, tcsh, libXaw, libXt, libX11}: let s = # Generated upstream information rec { @@ -27,7 +27,7 @@ stdenv.mkDerivation { find . -perm -0100 -type f | xargs sed -i -e "s@/bin/rm@$(type -P rm)@g" find . -perm -0100 -type f | xargs sed -i -e "s@/bin/mv@$(type -P mv)@g" - sed -i -e "s/^XLIBS *=.*/XLIBS=-lXaw -lXt -lX11/" source/formed/Makefile + sed -i -e "s/^XLIBS *=.*/XLIBS=-lXaw -lXt -lX11/" source/formed/Makefile make all make -C examples all @@ -45,9 +45,9 @@ stdenv.mkDerivation { meta = { inherit (s) version; description = "A reliable first-order theorem prover"; - license = stdenv.lib.licenses.publicDomain ; - maintainers = [stdenv.lib.maintainers.raskin]; - platforms = stdenv.lib.platforms.linux; + license = lib.licenses.publicDomain ; + maintainers = [lib.maintainers.raskin]; + platforms = lib.platforms.linux; broken = true; }; } diff --git a/nixpkgs/pkgs/applications/science/logic/petrinizer/default.nix b/nixpkgs/pkgs/applications/science/logic/petrinizer/default.nix index d277e0e1521a..5118795978d1 100644 --- a/nixpkgs/pkgs/applications/science/logic/petrinizer/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/petrinizer/default.nix @@ -1,6 +1,6 @@ { mkDerivation, callPackage, buildPackages , async, base, bytestring, containers, fetchFromGitLab, mtl -, parallel-io, parsec, stdenv, stm, transformers +, parallel-io, parsec, lib, stdenv, stm, transformers }: let z3 = callPackage ./z3.nix { gomp = null; z3 = buildPackages.z3; }; @@ -26,6 +26,6 @@ mkDerivation rec { transformers ]; description = "Safety and Liveness Analysis of Petri Nets with SMT solvers"; - license = stdenv.lib.licenses.gpl3; - maintainers = with stdenv.lib.maintainers; [ raskin ]; + license = lib.licenses.gpl3; + maintainers = with lib.maintainers; [ raskin ]; } diff --git a/nixpkgs/pkgs/applications/science/logic/petrinizer/sbv-7.13.nix b/nixpkgs/pkgs/applications/science/logic/petrinizer/sbv-7.13.nix index ed10e9f3db19..96e216417df1 100644 --- a/nixpkgs/pkgs/applications/science/logic/petrinizer/sbv-7.13.nix +++ b/nixpkgs/pkgs/applications/science/logic/petrinizer/sbv-7.13.nix @@ -1,7 +1,7 @@ { mkDerivation, array, async, base, bytestring, containers , crackNum, deepseq, directory, doctest, filepath, generic-deriving , ghc, Glob, hlint, mtl, pretty, process, QuickCheck, random -, stdenv, syb, tasty, tasty-golden, tasty-hunit, tasty-quickcheck +, lib, stdenv, syb, tasty, tasty-golden, tasty-hunit, tasty-quickcheck , template-haskell, time, z3 }: mkDerivation { @@ -22,5 +22,5 @@ mkDerivation { testSystemDepends = [ z3 ]; homepage = "http://leventerkok.github.com/sbv/"; description = "SMT Based Verification: Symbolic Haskell theorem prover using SMT solving"; - license = stdenv.lib.licenses.bsd3; + license = lib.licenses.bsd3; } diff --git a/nixpkgs/pkgs/applications/science/logic/petrinizer/z3.nix b/nixpkgs/pkgs/applications/science/logic/petrinizer/z3.nix index 4d868054c09b..3574954c376c 100644 --- a/nixpkgs/pkgs/applications/science/logic/petrinizer/z3.nix +++ b/nixpkgs/pkgs/applications/science/logic/petrinizer/z3.nix @@ -1,5 +1,5 @@ { mkDerivation, fetchpatch -, base, containers, gomp, hspec, QuickCheck, stdenv +, base, containers, gomp, hspec, QuickCheck, lib, stdenv , transformers, z3 }: mkDerivation { @@ -13,7 +13,7 @@ mkDerivation { testHaskellDepends = [ base hspec QuickCheck ]; homepage = "https://github.com/IagoAbal/haskell-z3"; description = "Bindings for the Z3 Theorem Prover"; - license = stdenv.lib.licenses.bsd3; + license = lib.licenses.bsd3; doCheck = false; patches = [ (fetchpatch { diff --git a/nixpkgs/pkgs/applications/science/logic/picosat/default.nix b/nixpkgs/pkgs/applications/science/logic/picosat/default.nix index b13d871580c5..48def5fc2e4d 100644 --- a/nixpkgs/pkgs/applications/science/logic/picosat/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/picosat/default.nix @@ -1,4 +1,4 @@ -{ stdenv, fetchurl }: +{ lib, stdenv, fetchurl }: stdenv.mkDerivation rec { pname = "picosat"; @@ -19,7 +19,7 @@ stdenv.mkDerivation rec { configurePhase = "./configure.sh --shared --trace"; - makeFlags = stdenv.lib.optional stdenv.isDarwin + makeFlags = lib.optional stdenv.isDarwin "SONAME=-Wl,-install_name,$(out)/lib/libpicosat.so"; installPhase = '' @@ -37,8 +37,8 @@ stdenv.mkDerivation rec { meta = { description = "SAT solver with proof and core support"; homepage = "http://fmv.jku.at/picosat/"; - license = stdenv.lib.licenses.mit; - platforms = stdenv.lib.platforms.unix; - maintainers = with stdenv.lib.maintainers; [ roconnor thoughtpolice ]; + license = lib.licenses.mit; + platforms = lib.platforms.unix; + maintainers = with lib.maintainers; [ roconnor thoughtpolice ]; }; } diff --git a/nixpkgs/pkgs/applications/science/logic/poly/default.nix b/nixpkgs/pkgs/applications/science/logic/poly/default.nix index ee50a2d85040..db124c379cad 100644 --- a/nixpkgs/pkgs/applications/science/logic/poly/default.nix +++ b/nixpkgs/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/nixpkgs/pkgs/applications/science/logic/potassco/clingcon.nix b/nixpkgs/pkgs/applications/science/logic/potassco/clingcon.nix index b74583ca1a2c..4d64a813e621 100644 --- a/nixpkgs/pkgs/applications/science/logic/potassco/clingcon.nix +++ b/nixpkgs/pkgs/applications/science/logic/potassco/clingcon.nix @@ -1,4 +1,4 @@ -{ stdenv +{ lib, stdenv , fetchFromGitHub , cmake , bison @@ -34,8 +34,8 @@ stdenv.mkDerivation rec { meta = { inherit version; description = "Extension of clingo to handle constraints over integers"; - license = stdenv.lib.licenses.gpl3; # for now GPL3, next version MIT! - platforms = stdenv.lib.platforms.unix; + license = lib.licenses.gpl3; # for now GPL3, next version MIT! + platforms = lib.platforms.unix; homepage = "https://potassco.org/"; downloadPage = "https://github.com/potassco/clingcon/releases/"; changelog = "https://github.com/potassco/clingcon/releases/tag/v${version}"; diff --git a/nixpkgs/pkgs/applications/science/logic/potassco/clingo.nix b/nixpkgs/pkgs/applications/science/logic/potassco/clingo.nix index fd6b2c8d14cd..f473c4f5366e 100644 --- a/nixpkgs/pkgs/applications/science/logic/potassco/clingo.nix +++ b/nixpkgs/pkgs/applications/science/logic/potassco/clingo.nix @@ -1,4 +1,4 @@ -{ stdenv, fetchzip, cmake }: +{ lib, stdenv, fetchzip, cmake }: stdenv.mkDerivation rec { pname = "clingo"; @@ -16,9 +16,9 @@ stdenv.mkDerivation rec { meta = { inherit version; description = "ASP system to ground and solve logic programs"; - license = stdenv.lib.licenses.mit; - maintainers = [stdenv.lib.maintainers.raskin]; - platforms = stdenv.lib.platforms.unix; + license = lib.licenses.mit; + maintainers = [lib.maintainers.raskin]; + platforms = lib.platforms.unix; homepage = "https://potassco.org/"; downloadPage = "https://github.com/potassco/clingo/releases/"; }; diff --git a/nixpkgs/pkgs/applications/science/logic/prooftree/default.nix b/nixpkgs/pkgs/applications/science/logic/prooftree/default.nix index 98313e48cb27..2606b94f4bbb 100644 --- a/nixpkgs/pkgs/applications/science/logic/prooftree/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/prooftree/default.nix @@ -1,4 +1,4 @@ -{ stdenv, fetchurl, pkgconfig, ncurses, ocamlPackages }: +{ lib, stdenv, fetchurl, pkg-config, ncurses, ocamlPackages }: stdenv.mkDerivation rec { pname = "prooftree"; @@ -9,14 +9,14 @@ stdenv.mkDerivation rec { sha256 = "0z1z4wqbqwgppkh2bm89fgy07a0y2m6g4lvcyzs09sm1ysklk2dh"; }; - nativeBuildInputs = [ pkgconfig ]; + nativeBuildInputs = [ pkg-config ]; buildInputs = [ ncurses ] ++ (with ocamlPackages; [ ocaml findlib camlp5 lablgtk ]); 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/nixpkgs/pkgs/applications/science/logic/prover9/default.nix b/nixpkgs/pkgs/applications/science/logic/prover9/default.nix index fcdff8558483..7fedca72b698 100644 --- a/nixpkgs/pkgs/applications/science/logic/prover9/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/prover9/default.nix @@ -1,4 +1,4 @@ -{stdenv, fetchurl}: +{lib, stdenv, fetchurl}: stdenv.mkDerivation { name = "prover9-2009-11a"; @@ -39,7 +39,7 @@ stdenv.mkDerivation { for first-order and equational logic. Prover9 is a successor of the Otter Prover. This is the LADR command-line version. ''; - platforms = stdenv.lib.platforms.linux; + platforms = lib.platforms.linux; maintainers = []; }; } diff --git a/nixpkgs/pkgs/applications/science/logic/proverif/default.nix b/nixpkgs/pkgs/applications/science/logic/proverif/default.nix index 4242bb0599e9..ba46d87581e0 100644 --- a/nixpkgs/pkgs/applications/science/logic/proverif/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/proverif/default.nix @@ -1,4 +1,4 @@ -{ stdenv, fetchurl, ocamlPackages }: +{ lib, stdenv, fetchurl, ocamlPackages }: stdenv.mkDerivation rec { pname = "proverif"; @@ -22,8 +22,8 @@ stdenv.mkDerivation rec { meta = { description = "Cryptographic protocol verifier in the Dolev-Yao model"; homepage = "https://prosecco.gforge.inria.fr/personal/bblanche/proverif/"; - license = stdenv.lib.licenses.gpl2; - platforms = stdenv.lib.platforms.unix; - maintainers = [ stdenv.lib.maintainers.thoughtpolice ]; + license = lib.licenses.gpl2; + platforms = lib.platforms.unix; + maintainers = [ lib.maintainers.thoughtpolice ]; }; } diff --git a/nixpkgs/pkgs/applications/science/logic/redprl/default.nix b/nixpkgs/pkgs/applications/science/logic/redprl/default.nix index 49245c73f2c4..43a2ec7e97e2 100644 --- a/nixpkgs/pkgs/applications/science/logic/redprl/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/redprl/default.nix @@ -1,4 +1,4 @@ -{ stdenv, fetchgit, mlton }: +{ lib, stdenv, fetchgit, mlton }: stdenv.mkDerivation { name = "redprl-2017-03-28"; src = fetchgit { @@ -21,8 +21,8 @@ stdenv.mkDerivation { meta = { description = "A proof assistant for Nominal Computational Type Theory"; homepage = "http://www.redprl.org/"; - license = stdenv.lib.licenses.mit; - maintainers = [ stdenv.lib.maintainers.acowley ]; - platforms = stdenv.lib.platforms.unix; + license = lib.licenses.mit; + maintainers = [ lib.maintainers.acowley ]; + platforms = lib.platforms.unix; }; } diff --git a/nixpkgs/pkgs/applications/science/logic/sad/default.nix b/nixpkgs/pkgs/applications/science/logic/sad/default.nix index 77613a135710..8e4d19973ef7 100644 --- a/nixpkgs/pkgs/applications/science/logic/sad/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/sad/default.nix @@ -31,10 +31,10 @@ stdenv.mkDerivation { The system for automated deduction is intended for automated processing of formal mathematical texts written in a special language called ForTheL (FORmal THEory Language) or in a traditional first-order language ''; - license = stdenv.lib.licenses.gpl3Plus; - maintainers = [ stdenv.lib.maintainers.schmitthenner ]; + license = lib.licenses.gpl3Plus; + maintainers = [ lib.maintainers.schmitthenner ]; homepage = "http://nevidal.org/sad.en.html"; - platforms = stdenv.lib.platforms.linux; + platforms = lib.platforms.linux; broken = true; # ghc-8.4.4 is gone from Nixpkgs }; } diff --git a/nixpkgs/pkgs/applications/science/logic/satallax/default.nix b/nixpkgs/pkgs/applications/science/logic/satallax/default.nix index 6c2b03b5b37d..dffb66b2fcf5 100644 --- a/nixpkgs/pkgs/applications/science/logic/satallax/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/satallax/default.nix @@ -1,4 +1,4 @@ -{stdenv, fetchurl, ocaml, zlib, which, eprover, makeWrapper, coq}: +{lib, stdenv, fetchurl, ocaml, zlib, which, eprover, makeWrapper, coq}: stdenv.mkDerivation rec { pname = "satallax"; version = "2.7"; @@ -30,7 +30,7 @@ stdenv.mkDerivation rec { mkdir -p "$out/libexec/satallax" cp picosat-*/picosat picosat-*/picomus "$out/libexec/satallax" - ( + ( cd minisat export MROOT=$PWD cd core @@ -46,7 +46,7 @@ stdenv.mkDerivation rec { mkdir -p "$out/share/doc/satallax" "$out/bin" "$out/lib" "$out/lib/satallax" cp bin/satallax.opt "$out/bin/satallax" wrapProgram "$out/bin/satallax" \ - --suffix PATH : "${stdenv.lib.makeBinPath [ coq eprover ]}:$out/libexec/satallax" \ + --suffix PATH : "${lib.makeBinPath [ coq eprover ]}:$out/libexec/satallax" \ --add-flags "-M" --add-flags "$out/lib/satallax/modes" cp LICENSE README "$out/share/doc/satallax" @@ -60,10 +60,10 @@ stdenv.mkDerivation rec { meta = { inherit version; - description = ''Automated theorem prover for higher-order logic''; - license = stdenv.lib.licenses.mit ; - maintainers = [stdenv.lib.maintainers.raskin]; - platforms = stdenv.lib.platforms.linux; + description = "Automated theorem prover for higher-order logic"; + license = lib.licenses.mit ; + maintainers = [lib.maintainers.raskin]; + platforms = lib.platforms.linux; downloadPage = "http://www.ps.uni-saarland.de/~cebrown/satallax/downloads.php"; homepage = "http://www.ps.uni-saarland.de/~cebrown/satallax/index.php"; updateWalker = true; diff --git a/nixpkgs/pkgs/applications/science/logic/saw-tools/default.nix b/nixpkgs/pkgs/applications/science/logic/saw-tools/default.nix index 71b26f8023a2..1dd6dc1cfc89 100644 --- a/nixpkgs/pkgs/applications/science/logic/saw-tools/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/saw-tools/default.nix @@ -1,7 +1,7 @@ -{ stdenv, fetchurl, gmp4, ncurses, zlib, clang }: +{ lib, stdenv, fetchurl, gmp4, ncurses, zlib, clang }: let - libPath = stdenv.lib.makeLibraryPath + libPath = lib.makeLibraryPath [ stdenv.cc.libc stdenv.cc.cc gmp4 @@ -53,8 +53,8 @@ stdenv.mkDerivation { meta = { description = "Tools for software verification and analysis"; homepage = "https://saw.galois.com"; - license = stdenv.lib.licenses.unfreeRedistributable; - platforms = stdenv.lib.platforms.linux; - maintainers = [ stdenv.lib.maintainers.thoughtpolice ]; + license = lib.licenses.unfreeRedistributable; + platforms = lib.platforms.linux; + maintainers = [ lib.maintainers.thoughtpolice ]; }; } diff --git a/nixpkgs/pkgs/applications/science/logic/spass/default.nix b/nixpkgs/pkgs/applications/science/logic/spass/default.nix index ece6f0b9f6a8..77b297b4fbbb 100644 --- a/nixpkgs/pkgs/applications/science/logic/spass/default.nix +++ b/nixpkgs/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/nixpkgs/pkgs/applications/science/logic/statverif/default.nix b/nixpkgs/pkgs/applications/science/logic/statverif/default.nix index e0efb28819d2..07365eef33fa 100644 --- a/nixpkgs/pkgs/applications/science/logic/statverif/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/statverif/default.nix @@ -1,4 +1,4 @@ -{ stdenv, fetchurl, ocaml }: +{ lib, stdenv, fetchurl, ocaml }: stdenv.mkDerivation rec { pname = "statverif"; @@ -27,8 +27,8 @@ stdenv.mkDerivation rec { meta = { description = "Verification of stateful processes (via Proverif)"; homepage = "https://markryan.eu/research/statverif/"; - license = stdenv.lib.licenses.gpl2; - platforms = stdenv.lib.platforms.unix; - maintainers = [ stdenv.lib.maintainers.thoughtpolice ]; + license = lib.licenses.gpl2; + platforms = lib.platforms.unix; + maintainers = [ lib.maintainers.thoughtpolice ]; }; } diff --git a/nixpkgs/pkgs/applications/science/logic/stp/default.nix b/nixpkgs/pkgs/applications/science/logic/stp/default.nix index dd00eda1b571..42926a870816 100644 --- a/nixpkgs/pkgs/applications/science/logic/stp/default.nix +++ b/nixpkgs/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,10 +24,7 @@ stdenv.mkDerivation rec { ) ''; - # seems to build fine now, may revert if concurrency does become an issue - enableParallelBuilding = true; - - meta = with stdenv.lib; { + meta = with lib; { description = "Simple Theorem Prover"; maintainers = with maintainers; [ ]; platforms = platforms.linux; diff --git a/nixpkgs/pkgs/applications/science/logic/symbiyosys/default.nix b/nixpkgs/pkgs/applications/science/logic/symbiyosys/default.nix index 9cf8b0845d43..1f2ad4634de2 100644 --- a/nixpkgs/pkgs/applications/science/logic/symbiyosys/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/symbiyosys/default.nix @@ -1,4 +1,4 @@ -{ stdenv, fetchFromGitHub +{ lib, stdenv, fetchFromGitHub , bash, python3, yosys , yices, boolector, z3, aiger }: @@ -51,8 +51,8 @@ stdenv.mkDerivation { meta = { description = "Tooling for Yosys-based verification flows"; homepage = "https://symbiyosys.readthedocs.io/"; - license = stdenv.lib.licenses.isc; - maintainers = with stdenv.lib.maintainers; [ thoughtpolice emily ]; - platforms = stdenv.lib.platforms.all; + license = lib.licenses.isc; + maintainers = with lib.maintainers; [ thoughtpolice emily ]; + platforms = lib.platforms.all; }; } diff --git a/nixpkgs/pkgs/applications/science/logic/tlaplus/default.nix b/nixpkgs/pkgs/applications/science/logic/tlaplus/default.nix index 14944f5e19b0..c4ba334b85ff 100644 --- a/nixpkgs/pkgs/applications/science/logic/tlaplus/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/tlaplus/default.nix @@ -1,4 +1,4 @@ -{ stdenv, fetchFromGitHub, makeWrapper +{ lib, stdenv, fetchFromGitHub, makeWrapper , adoptopenjdk-bin, jre, ant }: @@ -33,8 +33,8 @@ stdenv.mkDerivation rec { meta = { description = "An algorithm specification language with model checking tools"; homepage = "http://lamport.azurewebsites.net/tla/tla.html"; - license = stdenv.lib.licenses.mit; - platforms = stdenv.lib.platforms.unix; - maintainers = [ stdenv.lib.maintainers.thoughtpolice ]; + license = lib.licenses.mit; + platforms = lib.platforms.unix; + maintainers = [ lib.maintainers.thoughtpolice ]; }; } diff --git a/nixpkgs/pkgs/applications/science/logic/tlaplus/tlaps.nix b/nixpkgs/pkgs/applications/science/logic/tlaplus/tlaps.nix index 3872d3a9826b..89bdd979fea0 100644 --- a/nixpkgs/pkgs/applications/science/logic/tlaplus/tlaps.nix +++ b/nixpkgs/pkgs/applications/science/logic/tlaplus/tlaps.nix @@ -1,5 +1,5 @@ { fetchurl -, stdenv +, lib, stdenv , ocaml, isabelle, cvc3, perl, wget, which }: @@ -46,8 +46,8 @@ stdenv.mkDerivation rec { consistent abstraction over the various “backend” verifiers. ''; homepage = "https://tla.msr-inria.inria.fr/tlaps/content/Home.html"; - license = stdenv.lib.licenses.bsd2; - platforms = stdenv.lib.platforms.unix; + license = lib.licenses.bsd2; + platforms = lib.platforms.unix; maintainers = [ ]; }; diff --git a/nixpkgs/pkgs/applications/science/logic/tlaplus/toolbox.nix b/nixpkgs/pkgs/applications/science/logic/tlaplus/toolbox.nix index c9e97375b6c7..1c33d923289f 100644 --- a/nixpkgs/pkgs/applications/science/logic/tlaplus/toolbox.nix +++ b/nixpkgs/pkgs/applications/science/logic/tlaplus/toolbox.nix @@ -75,7 +75,7 @@ in stdenv.mkDerivation { ''; # http://lamport.azurewebsites.net/tla/license.html license = with lib.licenses; [ mit ]; - platforms = stdenv.lib.platforms.linux; + platforms = lib.platforms.linux; maintainers = [ ]; }; } diff --git a/nixpkgs/pkgs/applications/science/logic/tptp/default.nix b/nixpkgs/pkgs/applications/science/logic/tptp/default.nix index 4c63f8e72a36..9c91eaddfc47 100644 --- a/nixpkgs/pkgs/applications/science/logic/tptp/default.nix +++ b/nixpkgs/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/nixpkgs/pkgs/applications/science/logic/twelf/default.nix b/nixpkgs/pkgs/applications/science/logic/twelf/default.nix index 975b989bd94c..67779b2b5722 100644 --- a/nixpkgs/pkgs/applications/science/logic/twelf/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/twelf/default.nix @@ -1,4 +1,4 @@ -{ stdenv, fetchurl, pkgconfig, smlnj, rsync }: +{ lib, stdenv, fetchurl, pkg-config, smlnj, rsync }: stdenv.mkDerivation rec { pname = "twelf"; @@ -9,7 +9,7 @@ stdenv.mkDerivation rec { sha256 = "0fi1kbs9hrdrm1x4k13angpjasxlyd1gc3ys8ah54i75qbcd9c4i"; }; - nativeBuildInputs = [ pkgconfig ]; + nativeBuildInputs = [ pkg-config ]; buildInputs = [ smlnj rsync ]; buildPhase = '' @@ -44,8 +44,8 @@ stdenv.mkDerivation rec { Standard ML. ''; homepage = "http://twelf.org/wiki/Main_Page"; - license = stdenv.lib.licenses.mit; - maintainers = with stdenv.lib.maintainers; [ jwiegley ]; - platforms = stdenv.lib.platforms.unix; + license = lib.licenses.mit; + maintainers = with lib.maintainers; [ jwiegley ]; + platforms = lib.platforms.unix; }; } diff --git a/nixpkgs/pkgs/applications/science/logic/vampire/default.nix b/nixpkgs/pkgs/applications/science/logic/vampire/default.nix index dca03823e9ea..b88544544462 100644 --- a/nixpkgs/pkgs/applications/science/logic/vampire/default.nix +++ b/nixpkgs/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/nixpkgs/pkgs/applications/science/logic/verifast/default.nix b/nixpkgs/pkgs/applications/science/logic/verifast/default.nix index 49618d2586b1..2d625a1c1b29 100644 --- a/nixpkgs/pkgs/applications/science/logic/verifast/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/verifast/default.nix @@ -1,9 +1,9 @@ -{ stdenv, fetchurl, gtk2, gdk-pixbuf, atk, pango, glib, cairo, freetype +{ lib, stdenv, fetchurl, gtk2, gdk-pixbuf, atk, pango, glib, cairo, freetype , fontconfig, libxml2, gnome2 }: let - libPath = stdenv.lib.makeLibraryPath + libPath = lib.makeLibraryPath [ stdenv.cc.libc stdenv.cc.cc gtk2 gdk-pixbuf atk pango glib cairo freetype fontconfig libxml2 gnome2.gtksourceview ] + ":${stdenv.cc.cc.lib}/lib64:$out/libexec"; @@ -43,8 +43,8 @@ stdenv.mkDerivation rec { meta = { description = "Verification for C and Java programs via separation logic"; homepage = "http://people.cs.kuleuven.be/~bart.jacobs/verifast/"; - license = stdenv.lib.licenses.mit; + license = lib.licenses.mit; platforms = [ "x86_64-linux" ]; - maintainers = [ stdenv.lib.maintainers.thoughtpolice ]; + maintainers = [ lib.maintainers.thoughtpolice ]; }; } diff --git a/nixpkgs/pkgs/applications/science/logic/verit/default.nix b/nixpkgs/pkgs/applications/science/logic/verit/default.nix index f20a83241571..81acbe4f2d0b 100644 --- a/nixpkgs/pkgs/applications/science/logic/verit/default.nix +++ b/nixpkgs/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/nixpkgs/pkgs/applications/science/logic/why3/default.nix b/nixpkgs/pkgs/applications/science/logic/why3/default.nix index eacff32bdf62..deb40c742847 100644 --- a/nixpkgs/pkgs/applications/science/logic/why3/default.nix +++ b/nixpkgs/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/nixpkgs/pkgs/applications/science/logic/workcraft/default.nix b/nixpkgs/pkgs/applications/science/logic/workcraft/default.nix index 9ce6592d9989..cb0d668f5365 100644 --- a/nixpkgs/pkgs/applications/science/logic/workcraft/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/workcraft/default.nix @@ -1,4 +1,4 @@ -{ stdenv, fetchurl, jre, makeWrapper }: +{ lib, stdenv, fetchurl, jre, makeWrapper }: stdenv.mkDerivation rec { pname = "workcraft"; @@ -25,9 +25,9 @@ stdenv.mkDerivation rec { meta = { homepage = "https://workcraft.org/"; description = "Framework for interpreted graph modeling, verification and synthesis"; - platforms = stdenv.lib.platforms.linux; - license = stdenv.lib.licenses.mit; - maintainers = with stdenv.lib.maintainers; [ timor ]; + platforms = lib.platforms.linux; + license = lib.licenses.mit; + maintainers = with lib.maintainers; [ timor ]; inherit version; }; } diff --git a/nixpkgs/pkgs/applications/science/logic/yices/default.nix b/nixpkgs/pkgs/applications/science/logic/yices/default.nix index b8dd528a11c1..c26504bf7bdc 100644 --- a/nixpkgs/pkgs/applications/science/logic/yices/default.nix +++ b/nixpkgs/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"; @@ -23,18 +23,18 @@ stdenv.mkDerivation rec { doCheck = true; # Usual shenanigans - patchPhase = ''patchShebangs tests/regress/check.sh''; + patchPhase = "patchShebangs tests/regress/check.sh"; # Includes a fix for the embedded soname being libyices.so.2.5, but # only installing the libyices.so.2.5.x file. installPhase = let - ver_XdotY = stdenv.lib.versions.majorMinor version; + ver_XdotY = lib.versions.majorMinor version; in '' make install LDCONFIG=true 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; diff --git a/nixpkgs/pkgs/applications/science/logic/z3/4.4.0.nix b/nixpkgs/pkgs/applications/science/logic/z3/4.4.0.nix index a5388572db61..9b7dabeb7200 100644 --- a/nixpkgs/pkgs/applications/science/logic/z3/4.4.0.nix +++ b/nixpkgs/pkgs/applications/science/logic/z3/4.4.0.nix @@ -1,4 +1,4 @@ -{ stdenv, fetchFromGitHub, python }: +{ lib, stdenv, fetchFromGitHub, python }: stdenv.mkDerivation rec { name = "z3-${version}"; @@ -34,8 +34,8 @@ stdenv.mkDerivation rec { meta = { description = "A high-performance theorem prover and SMT solver"; homepage = "https://github.com/Z3Prover/z3"; - license = stdenv.lib.licenses.mit; - platforms = stdenv.lib.platforms.x86_64; - maintainers = with stdenv.lib.maintainers; [ thoughtpolice ttuegel ]; + license = lib.licenses.mit; + platforms = lib.platforms.x86_64; + maintainers = with lib.maintainers; [ thoughtpolice ttuegel ]; }; } diff --git a/nixpkgs/pkgs/applications/science/logic/z3/default.nix b/nixpkgs/pkgs/applications/science/logic/z3/default.nix index 48512eff5300..cd58740186fe 100644 --- a/nixpkgs/pkgs/applications/science/logic/z3/default.nix +++ b/nixpkgs/pkgs/applications/science/logic/z3/default.nix @@ -1,4 +1,4 @@ -{ stdenv, fetchFromGitHub, python, fixDarwinDylibNames +{ lib, stdenv, fetchFromGitHub, python, fixDarwinDylibNames , javaBindings ? false , ocamlBindings ? false , pythonBindings ? true @@ -9,7 +9,7 @@ assert javaBindings -> jdk != null; assert ocamlBindings -> ocaml != null && findlib != null && zarith != null; -with stdenv.lib; +with lib; stdenv.mkDerivation rec { pname = "z3"; @@ -59,8 +59,8 @@ stdenv.mkDerivation rec { meta = { description = "A high-performance theorem prover and SMT solver"; homepage = "https://github.com/Z3Prover/z3"; - license = stdenv.lib.licenses.mit; - platforms = stdenv.lib.platforms.unix; - maintainers = with stdenv.lib.maintainers; [ thoughtpolice ttuegel ]; + license = lib.licenses.mit; + platforms = lib.platforms.unix; + maintainers = with lib.maintainers; [ thoughtpolice ttuegel ]; }; } diff --git a/nixpkgs/pkgs/applications/science/logic/z3/tptp.nix b/nixpkgs/pkgs/applications/science/logic/z3/tptp.nix index 34449542abb2..bb912742b7c5 100644 --- a/nixpkgs/pkgs/applications/science/logic/z3/tptp.nix +++ b/nixpkgs/pkgs/applications/science/logic/z3/tptp.nix @@ -1,4 +1,4 @@ -{stdenv, z3, cmake}: +{lib, stdenv, z3, cmake}: stdenv.mkDerivation rec { pname = "z3-tptp"; version = z3.version; @@ -25,7 +25,7 @@ stdenv.mkDerivation rec { meta = { inherit version; inherit (z3.meta) license homepage platforms; - description = ''TPTP wrapper for Z3 prover''; - maintainers = [stdenv.lib.maintainers.raskin]; + description = "TPTP wrapper for Z3 prover"; + maintainers = [lib.maintainers.raskin]; }; } |