diff options
author | Ben Siraphob <bensiraphob@gmail.com> | 2024-02-06 15:42:24 -0500 |
---|---|---|
committer | Ben Siraphob <bensiraphob@gmail.com> | 2024-02-12 15:40:25 -0500 |
commit | ea5f5df1c79b5f5e23fd98df25937acf4a11e0bf (patch) | |
tree | b71f99ac9b8cd78b1c24708b90f76a96d90e7183 /pkgs/development/coq-modules | |
parent | 04b99c67cae91c08670acf390cc5d2139b233ca5 (diff) |
coqPackages.smtcoq: expand to more supported versions
Diffstat (limited to 'pkgs/development/coq-modules')
-rw-r--r-- | pkgs/development/coq-modules/smtcoq/cvc4.nix | 50 | ||||
-rw-r--r-- | pkgs/development/coq-modules/smtcoq/default.nix | 25 | ||||
-rw-r--r-- | pkgs/development/coq-modules/smtcoq/minisat-fenv.patch | 65 |
3 files changed, 14 insertions, 126 deletions
diff --git a/pkgs/development/coq-modules/smtcoq/cvc4.nix b/pkgs/development/coq-modules/smtcoq/cvc4.nix deleted file mode 100644 index 220c24a2b8301..0000000000000 --- a/pkgs/development/coq-modules/smtcoq/cvc4.nix +++ /dev/null @@ -1,50 +0,0 @@ -{ lib, stdenv, cln, fetchurl, gmp, gnumake42, swig, pkg-config -, libantlr3c, boost, autoreconfHook -, python3 -}: - -let cln' = cln.override { gccStdenv = stdenv; }; in - -stdenv.mkDerivation rec { - pname = "cvc4"; - version = "1.6"; - - src = fetchurl { - url = "https://cvc4.cs.stanford.edu/downloads/builds/src/cvc4-${version}.tar.gz"; - sha256 = "1iw793zsi48q91lxpf8xl8lnvv0jsj4whdad79rakywkm1gbs62w"; - }; - - # Build fails with GNUmake 4.4 - nativeBuildInputs = [ autoreconfHook gnumake42 pkg-config ]; - buildInputs = [ gmp swig libantlr3c boost python3 ] - ++ lib.optionals stdenv.isLinux [ cln' ]; - - configureFlags = [ - "--enable-language-bindings=c" - "--enable-gpl" - "--with-boost=${boost.dev}" - ] ++ lib.optionals stdenv.isLinux [ "--with-cln" ]; - - prePatch = '' - patch -p1 -i ${./minisat-fenv.patch} -d src/prop/minisat - patch -p1 -i ${./minisat-fenv.patch} -d src/prop/bvminisat - ''; - - patches = [ - ../../../applications/science/logic/cvc4/cvc4-bash-patsub-replacement.patch - ]; - - preConfigure = '' - patchShebangs ./src/ - ''; - - enableParallelBuilding = true; - - meta = with lib; { - description = "A high-performance theorem prover and SMT solver"; - homepage = "http://cvc4.cs.stanford.edu/web/"; - license = licenses.gpl3; - platforms = platforms.unix; - maintainers = with maintainers; [ vbgl thoughtpolice gebner ]; - }; -} diff --git a/pkgs/development/coq-modules/smtcoq/default.nix b/pkgs/development/coq-modules/smtcoq/default.nix index 49c4348b9af57..f1ec4d0fed271 100644 --- a/pkgs/development/coq-modules/smtcoq/default.nix +++ b/pkgs/development/coq-modules/smtcoq/default.nix @@ -1,4 +1,4 @@ -{ lib, stdenv, gcc10StdenvCompat, pkgs, mkCoqDerivation, coq, trakt, veriT, zchaff, fetchurl, version ? null }: +{ lib, stdenv, pkgs, mkCoqDerivation, coq, trakt, veriT, zchaff, fetchurl, cvc5, version ? null }: let # version of veriT that works with SMTCoq @@ -9,32 +9,35 @@ let }; meta.broken = false; }); - cvc4 = pkgs.callPackage ./cvc4.nix { - stdenv = gcc10StdenvCompat; - }; in mkCoqDerivation { pname = "smtcoq"; owner = "smtcoq"; - release."2021-09-17".rev = "f36bf11e994cc269c2ec92b061b082e3516f472f"; - release."2021-09-17".sha256 = "sha256-bF7ES+tXraaAJwVEwAMx3CUESpNlAUerQjr4d2eaGJQ="; + release."SMTCoq-2.1+8.16".rev = "4996c00b455bfe98400e96c954839ceea93efdf7"; + release."SMTCoq-2.1+8.16".sha256 = "sha256-k53e+frUjwq+ZZKbbOKd/EfVC40QeAzB2nCsGkCKnHA="; + release."SMTCoq-2.1+8.14".rev = "e11d9b424b0113f32265bcef0ddc962361da4dae"; + release."SMTCoq-2.1+8.14".sha256 = "sha256-4a01/CRHUon2OfpagAnMaEVkBFipPX3MCVmSFS1Bnt4="; + release."SMTCoq-2.1+8.13".rev = "d02269c43739f4559d83873563ca00daad9faaf1"; + release."SMTCoq-2.1+8.13".sha256 = "sha256-VZetGghdr5uJWDwZWSlhYScoNEoRHIbwqwJKSQyfKKg="; inherit version; defaultVersion = with lib.versions; lib.switch coq.version [ - { case = isEq "8.13"; out = "2021-09-17"; } + { case = isEq "8.16"; out = "SMTCoq-2.1+8.16"; } + { case = isEq "8.14"; out = "SMTCoq-2.1+8.14"; } + { case = isEq "8.13"; out = "SMTCoq-2.1+8.13"; } ] null; - propagatedBuildInputs = [ trakt cvc4 veriT' zchaff ] ++ (with coq.ocamlPackages; [ num zarith ]); + propagatedBuildInputs = [ trakt cvc5 veriT' zchaff ] ++ (with coq.ocamlPackages; [ num zarith ]); mlPlugin = true; nativeBuildInputs = (with pkgs; [ gnumake42 ]) ++ (with coq.ocamlPackages; [ ocamlbuild ]); - # This is meant to ease future troubleshooting of cvc4 build failures - passthru = { inherit cvc4; }; + # This is meant to ease future troubleshooting of cvc5 build failures + passthru = { inherit cvc5; }; meta = with lib; { - description = "Communication between Coq and SAT/SMT solvers "; + description = "Communication between Coq and SAT/SMT solvers"; maintainers = with maintainers; [ siraben ]; license = licenses.cecill-b; platforms = platforms.unix; diff --git a/pkgs/development/coq-modules/smtcoq/minisat-fenv.patch b/pkgs/development/coq-modules/smtcoq/minisat-fenv.patch deleted file mode 100644 index 686d5a1c5b499..0000000000000 --- a/pkgs/development/coq-modules/smtcoq/minisat-fenv.patch +++ /dev/null @@ -1,65 +0,0 @@ -From 7f1016ceab9b0f57a935bd51ca6df3d18439b472 Mon Sep 17 00:00:00 2001 -From: Will Dietz <w@wdtz.org> -Date: Tue, 17 Oct 2017 22:57:02 -0500 -Subject: [PATCH] use fenv instead of non-standard fpu_control - ---- - core/Main.cc | 8 ++++++-- - simp/Main.cc | 8 ++++++-- - utils/System.h | 2 +- - 3 files changed, 13 insertions(+), 5 deletions(-) - -diff --git a/core/Main.cc b/core/Main.cc -index 2b0d97b..8ad95fb 100644 ---- a/core/Main.cc -+++ b/core/Main.cc -@@ -78,8 +78,12 @@ int main(int argc, char** argv) - // printf("This is MiniSat 2.0 beta\n"); - - #if defined(__linux__) -- fpu_control_t oldcw, newcw; -- _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw); -+ fenv_t fenv; -+ -+ fegetenv(&fenv); -+ fenv.__control_word &= ~0x300; /* _FPU_EXTENDED */ -+ fenv.__control_word |= 0x200; /* _FPU_DOUBLE */ -+ fesetenv(&fenv); - printf("WARNING: for repeatability, setting FPU to use double precision\n"); - #endif - // Extra options: -diff --git a/simp/Main.cc b/simp/Main.cc -index 2804d7f..39bfb71 100644 ---- a/simp/Main.cc -+++ b/simp/Main.cc -@@ -79,8 +79,12 @@ int main(int argc, char** argv) - // printf("This is MiniSat 2.0 beta\n"); - - #if defined(__linux__) -- fpu_control_t oldcw, newcw; -- _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw); -+ fenv_t fenv; -+ -+ fegetenv(&fenv); -+ fenv.__control_word &= ~0x300; /* _FPU_EXTENDED */ -+ fenv.__control_word |= 0x200; /* _FPU_DOUBLE */ -+ fesetenv(&fenv); - printf("WARNING: for repeatability, setting FPU to use double precision\n"); - #endif - // Extra options: -diff --git a/utils/System.h b/utils/System.h -index 1758192..c0ad13a 100644 ---- a/utils/System.h -+++ b/utils/System.h -@@ -22,7 +22,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA - #define Minisat_System_h - - #if defined(__linux__) --#include <fpu_control.h> -+#include <fenv.h> - #endif - - #include "mtl/IntTypes.h" --- -2.14.2 - |