diff options
Diffstat (limited to 'pkgs/applications/science/logic')
7 files changed, 77 insertions, 25 deletions
diff --git a/pkgs/applications/science/logic/alt-ergo/default.nix b/pkgs/applications/science/logic/alt-ergo/default.nix index f83480cfbaf..e396f1c4a91 100644 --- a/pkgs/applications/science/logic/alt-ergo/default.nix +++ b/pkgs/applications/science/logic/alt-ergo/default.nix @@ -1,26 +1,47 @@ -{ fetchurl, stdenv, which, dune, ocamlPackages }: +{ fetchurl, lib, which, ocamlPackages }: -stdenv.mkDerivation rec { +let pname = "alt-ergo"; - version = "2.3.0"; + version = "2.3.2"; src = fetchurl { - url = "https://alt-ergo.ocamlpro.com/download_manager.php?target=${pname}-${version}.tar.gz"; - name = "${pname}-${version}.tar.gz"; - sha256 = "1ycr3ff0gacq1aqzs16n6swgfniwpim0m7rvhcam64kj0a80c6bz"; + url = "https://alt-ergo.ocamlpro.com/http/alt-ergo-${version}/alt-ergo-${version}.tar.gz"; + sha256 = "130hisjzkaslygipdaaqib92spzx9rapsd45dbh5ssczjn5qnhb9"; }; - buildInputs = [ dune which ] ++ (with ocamlPackages; [ - ocaml findlib camlzip lablgtk menhir num ocplib-simplex psmt2-frontend seq zarith - ]); - preConfigure = "patchShebangs ./configure"; + nativeBuildInputs = [ which ]; + +in + +let alt-ergo-lib = ocamlPackages.buildDunePackage rec { + pname = "alt-ergo-lib"; + inherit version src preConfigure nativeBuildInputs; + configureFlags = pname; + propagatedBuildInputs = with ocamlPackages; [ num ocplib-simplex stdlib-shims zarith ]; +}; in + +let alt-ergo-parsers = ocamlPackages.buildDunePackage rec { + pname = "alt-ergo-parsers"; + inherit version src preConfigure nativeBuildInputs; + configureFlags = pname; + buildInputs = with ocamlPackages; [ menhir ]; + propagatedBuildInputs = [ alt-ergo-lib ] ++ (with ocamlPackages; [ camlzip psmt2-frontend ]); +}; in + +ocamlPackages.buildDunePackage { + + inherit pname version src preConfigure nativeBuildInputs; + + configureFlags = pname; + + buildInputs = [ alt-ergo-parsers ocamlPackages.menhir ]; + meta = { description = "High-performance theorem prover and SMT solver"; homepage = "https://alt-ergo.ocamlpro.com/"; - license = stdenv.lib.licenses.ocamlpro_nc; - platforms = stdenv.lib.platforms.linux ++ stdenv.lib.platforms.darwin; - maintainers = [ stdenv.lib.maintainers.thoughtpolice ]; + license = lib.licenses.ocamlpro_nc; + maintainers = [ lib.maintainers.thoughtpolice ]; }; } diff --git a/pkgs/applications/science/logic/cadical/default.nix b/pkgs/applications/science/logic/cadical/default.nix new file mode 100644 index 00000000000..5e6c0d55b7d --- /dev/null +++ b/pkgs/applications/science/logic/cadical/default.nix @@ -0,0 +1,29 @@ +{ stdenv, fetchFromGitHub }: + +stdenv.mkDerivation rec { + pname = "cadical"; + version = "1.2.1"; + + src = fetchFromGitHub { + owner = "arminbiere"; + repo = "cadical"; + rev = "rel-${version}"; + hash = "sha256:1a66xkw42ad330fvw8i0sawrmg913m8wrq5c85lw5qandkwvxdi6"; + }; + + dontAddPrefix = true; + installPhase = '' + install -Dm0755 build/cadical "$out/bin/cadical" + install -Dm0755 build/mobical "$out/bin/mobical" + mkdir -p "$out/share/doc/${pname}-${version}/" + install -Dm0755 {LICEN?E,README*,VERSION} "$out/share/doc/${pname}-${version}/" + ''; + + meta = with stdenv.lib; { + description = "Simplified Satisfiability Solver"; + maintainers = with maintainers; [ shnarazk ]; + platforms = platforms.unix; + license = licenses.mit; + homepage = "http://fmv.jku.at/cadical"; + }; +} diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix index 85c5d23ffca..52a587ccb48 100644 --- a/pkgs/applications/science/logic/coq/default.nix +++ b/pkgs/applications/science/logic/coq/default.nix @@ -33,6 +33,7 @@ let "8.10.1" = "072v2zkjzf7gj48137wpr3c9j0hg9pdhlr5l8jrgrwynld8fp7i4"; "8.10.2" = "0znxmpy71bfw0p6x47i82jf5k7v41zbz9bdpn901ysn3ir8l3wrz"; "8.11.0" = "1rfdic6mp7acx2zfwz7ziqk12g95bl9nyj68z4n20a5bcjv2pxpn"; + "8.11.1" = "0qriy9dy36dajsv5qmli8gd6v55mah02ya334nw49ky19v7518m0"; }.${version}; coq-version = stdenv.lib.versions.majorMinor version; versionAtLeast = stdenv.lib.versionAtLeast coq-version; diff --git a/pkgs/applications/science/logic/lean/default.nix b/pkgs/applications/science/logic/lean/default.nix index cfd645a3c73..594f596b5ef 100644 --- a/pkgs/applications/science/logic/lean/default.nix +++ b/pkgs/applications/science/logic/lean/default.nix @@ -2,13 +2,13 @@ stdenv.mkDerivation rec { pname = "lean"; - version = "3.7.2"; + version = "3.8.0"; src = fetchFromGitHub { owner = "leanprover-community"; repo = "lean"; rev = "v${version}"; - sha256 = "0d9lz0mbxyaaykkvk2p8w2hcif9cx0ksihgh7qhxf417bz6msgc1"; + sha256 = "0frs2vhxlzdliyydb462c1886dn585zd7yp7hdxzsri2v6gdh89g"; }; nativeBuildInputs = [ cmake ]; diff --git a/pkgs/applications/science/logic/mcy/default.nix b/pkgs/applications/science/logic/mcy/default.nix index ec9af192631..a9366d56058 100644 --- a/pkgs/applications/science/logic/mcy/default.nix +++ b/pkgs/applications/science/logic/mcy/default.nix @@ -7,13 +7,13 @@ let in stdenv.mkDerivation { pname = "mcy"; - version = "2020.03.16"; + version = "2020.03.21"; src = fetchFromGitHub { owner = "YosysHQ"; repo = "mcy"; - rev = "562c02375067428bb657f57faa5131ee1ab44051"; - sha256 = "0q77v2hxnmv61zx5bl4lrqiavgvsiyb5qxdp9hnihimj1m30bc5h"; + rev = "bac92b8aad9bf24714fda70d3750bb50d6d96177"; + sha256 = "0mmg6zd5cbn8g0am9c3naamg0lq67yyy117fzn2ydigcyia7vmnp"; }; buildInputs = [ python ]; diff --git a/pkgs/applications/science/logic/poly/default.nix b/pkgs/applications/science/logic/poly/default.nix index c833b22e49b..ee50a2d8504 100644 --- a/pkgs/applications/science/logic/poly/default.nix +++ b/pkgs/applications/science/logic/poly/default.nix @@ -2,13 +2,14 @@ stdenv.mkDerivation rec { pname = "libpoly"; - version = "0.1.7"; + version = "0.1.8"; src = fetchFromGitHub { owner = "SRI-CSL"; repo = "libpoly"; - rev = "v${version}"; - sha256 = "0i5ar4lhs88glk0rvkmag656ii434i6i1q5dspx6d0kyg78fii64"; + # they've pushed to the release branch, use explicit tag + rev = "refs/tags/v${version}"; + sha256 = "1n3gijksnl2ybznq4lkwm2428f82423sxq18gnb2g1kiwqlzdaa3"; }; nativeBuildInputs = [ cmake ]; @@ -16,7 +17,7 @@ stdenv.mkDerivation rec { buildInputs = [ gmp python ]; meta = with stdenv.lib; { - homepage = https://github.com/SRI-CSL/libpoly; + homepage = "https://github.com/SRI-CSL/libpoly"; description = "C library for manipulating polynomials"; license = licenses.lgpl3; platforms = platforms.all; diff --git a/pkgs/applications/science/logic/symbiyosys/default.nix b/pkgs/applications/science/logic/symbiyosys/default.nix index 48c48836b06..b180cf307f0 100644 --- a/pkgs/applications/science/logic/symbiyosys/default.nix +++ b/pkgs/applications/science/logic/symbiyosys/default.nix @@ -5,13 +5,13 @@ stdenv.mkDerivation { pname = "symbiyosys"; - version = "2020.02.11"; + version = "2020.03.24"; src = fetchFromGitHub { owner = "YosysHQ"; repo = "SymbiYosys"; - rev = "0a7013017f9d583ef6cc8d10712f4bf11cf6e024"; - sha256 = "08xz8sgvs1qy7jxp8ma5yl49i6nl7k6bkhry4afdvwg3fvwis39c"; + rev = "8a62780b9df4d2584e41cdd42cab92fddcd75b31"; + sha256 = "0ss5mrzwff2dny8kfciqbrz67m6k52yvc1shd7gk3qb99x7g7fp8"; }; buildInputs = [ python3 ]; |