diff options
Diffstat (limited to 'nixpkgs/pkgs/applications/science/logic')
96 files changed, 4116 insertions, 0 deletions
diff --git a/nixpkgs/pkgs/applications/science/logic/abc/default.nix b/nixpkgs/pkgs/applications/science/logic/abc/default.nix new file mode 100644 index 000000000000..c832d12627a0 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/abc/default.nix @@ -0,0 +1,31 @@ +{ fetchFromGitHub, stdenv, readline, cmake }: + +stdenv.mkDerivation { + pname = "abc-verifier"; + version = "2018-07-08"; + + src = fetchFromGitHub { + owner = "berkeley-abc"; + repo = "abc"; + rev = "24407e13db4b8ca16c3996049b2d33ec3722de39"; + sha256 = "1rckji7nk81n6v1yajz7daqwipxacv7zlafknvmbiwji30j47sq5"; + }; + + nativeBuildInputs = [ cmake ]; + buildInputs = [ readline ]; + + enableParallelBuilding = true; + + installPhase = '' + mkdir -p $out/bin + mv abc $out/bin + ''; + + meta = { + description = "A tool for squential logic synthesis and formal verification"; + homepage = https://people.eecs.berkeley.edu/~alanmi/abc; + license = stdenv.lib.licenses.mit; + platforms = stdenv.lib.platforms.unix; + maintainers = [ stdenv.lib.maintainers.thoughtpolice ]; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/abella/default.nix b/nixpkgs/pkgs/applications/science/logic/abella/default.nix new file mode 100644 index 000000000000..7078fd454a0a --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/abella/default.nix @@ -0,0 +1,38 @@ +{ stdenv, fetchurl, rsync, ocamlPackages }: + +stdenv.mkDerivation rec { + pname = "abella"; + version = "2.0.6"; + + src = fetchurl { + url = "http://abella-prover.org/distributions/${pname}-${version}.tar.gz"; + sha256 = "164q9gngckg6q69k13lwx2pq3cnc9ckw1qi8dnpxqfjgwfqr7xyi"; + }; + + buildInputs = [ rsync ] ++ (with ocamlPackages; [ ocaml ocamlbuild findlib ]); + + installPhase = '' + mkdir -p $out/bin + rsync -av abella $out/bin/ + + mkdir -p $out/share/emacs/site-lisp/abella/ + rsync -av emacs/ $out/share/emacs/site-lisp/abella/ + + mkdir -p $out/share/abella/examples + rsync -av examples/ $out/share/abella/examples/ + ''; + + meta = { + description = "Interactive theorem prover"; + longDescription = '' + Abella is an interactive theorem prover based on lambda-tree syntax. + This means that Abella is well-suited for reasoning about the meta-theory + of programming languages and other logical systems which manipulate + 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; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/acgtk/default.nix b/nixpkgs/pkgs/applications/science/logic/acgtk/default.nix new file mode 100644 index 000000000000..729aef4e21c2 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/acgtk/default.nix @@ -0,0 +1,27 @@ +{ stdenv, fetchurl, dune, ocamlPackages }: + +stdenv.mkDerivation { + + name = "acgtk-1.5.0"; + + src = fetchurl { + url = http://calligramme.loria.fr/acg/software/acg-1.5.0-20181019.tar.gz; + sha256 = "14n003gxzw5w79hlpw1ja4nq97jqf9zqyg00ihvpxw4bv9jlm8jm"; + }; + + buildInputs = [ dune ] ++ (with ocamlPackages; [ + ocaml findlib ansiterminal cairo2 fmt logs menhir mtime ocf + ]); + + buildPhase = "dune build"; + + inherit (dune) installPhase; + + meta = with stdenv.lib; { + homepage = http://calligramme.loria.fr/acg/; + description = "A toolkit for developing ACG signatures and lexicon"; + license = licenses.cecill20; + inherit (ocamlPackages.ocaml.meta) platforms; + maintainers = [ maintainers.jirkamarsik ]; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/aiger/default.nix b/nixpkgs/pkgs/applications/science/logic/aiger/default.nix new file mode 100644 index 000000000000..10d94e2bb8c7 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/aiger/default.nix @@ -0,0 +1,55 @@ +{ stdenv, fetchurl, picosat }: + +stdenv.mkDerivation rec { + pname = "aiger"; + version = "1.9.9"; + + src = fetchurl { + url = "http://fmv.jku.at/aiger/${pname}-${version}.tar.gz"; + sha256 = "1ish0dw0nf9gyghxsdhpy1jjiy5wp54c993swp85xp7m6vdx6l0y"; + }; + + enableParallelBuilding = true; + + configurePhase = '' + # Set up picosat, so we can build 'aigbmc' + mkdir ../picosat + ln -s ${picosat}/include/picosat/picosat.h ../picosat/picosat.h + ln -s ${picosat}/lib/picosat.o ../picosat/picosat.o + ln -s ${picosat}/share/picosat.version ../picosat/VERSION + ./configure.sh + ''; + + installPhase = '' + mkdir -p $out/bin $dev/include $lib/lib + + # Do the installation manually, as the Makefile has odd + # cyrillic characters, and this is easier than adding + # a whole .patch file. + BINS=( \ + aigand aigdd aigflip aigfuzz aiginfo aigjoin \ + aigmiter aigmove aignm aigor aigreset aigsim \ + aigsplit aigstrip aigtoaig aigtoblif aigtocnf \ + aigtodot aigtosmv aigunconstraint aigunroll \ + andtoaig bliftoaig smvtoaig soltostim wrapstim \ + aigbmc aigdep + ) + + for x in ''${BINS[*]}; do + install -m 755 -s $x $out/bin/$x + done + + cp -v aiger.o $lib/lib + cp -v aiger.h $dev/include + ''; + + outputs = [ "out" "dev" "lib" ]; + + 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.linux; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/alt-ergo/default.nix b/nixpkgs/pkgs/applications/science/logic/alt-ergo/default.nix new file mode 100644 index 000000000000..f83480cfbafc --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/alt-ergo/default.nix @@ -0,0 +1,26 @@ +{ fetchurl, stdenv, which, dune, ocamlPackages }: + +stdenv.mkDerivation rec { + pname = "alt-ergo"; + version = "2.3.0"; + + src = fetchurl { + url = "https://alt-ergo.ocamlpro.com/download_manager.php?target=${pname}-${version}.tar.gz"; + name = "${pname}-${version}.tar.gz"; + sha256 = "1ycr3ff0gacq1aqzs16n6swgfniwpim0m7rvhcam64kj0a80c6bz"; + }; + + buildInputs = [ dune which ] ++ (with ocamlPackages; [ + ocaml findlib camlzip lablgtk menhir num ocplib-simplex psmt2-frontend seq zarith + ]); + + preConfigure = "patchShebangs ./configure"; + + 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 ]; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/aspino/default.nix b/nixpkgs/pkgs/applications/science/logic/aspino/default.nix new file mode 100644 index 000000000000..d6190942efab --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/aspino/default.nix @@ -0,0 +1,50 @@ +{ stdenv, fetchurl, fetchFromGitHub, zlib, boost }: + +let + glucose' = fetchurl { + url = "http://www.labri.fr/perso/lsimon/downloads/softwares/glucose-syrup.tgz"; + sha256 = "0bq5l2jabhdfhng002qfk0mcj4pfi1v5853x3c7igwfrgx0jmfld"; + }; +in + +stdenv.mkDerivation { + name = "aspino-unstable-2017-03-09"; + + src = fetchFromGitHub { + owner = "alviano"; + repo = "aspino"; + rev = "e31c3b4e5791a454e6602439cb26bd98d23c4e78"; + sha256 = "0annsjs2prqmv1lbs0lxr7yclfzh47xg9zyiq6mdxcc02rxsi14f"; + }; + + buildInputs = [ zlib boost ]; + + postPatch = '' + substituteInPlace Makefile \ + --replace "GCC = g++" "GCC = c++" + + patchShebangs . + ''; + + preBuild = '' + cp ${glucose'} patches/glucose-syrup.tgz + ./bootstrap.sh + ''; + + installPhase = '' + runHook preInstall + mkdir -p $out/bin + install -m0755 build/release/{aspino,fairino-{bs,ls,ps},maxino-2015-{k16,kdyn}} $out/bin + runHook postInstall + ''; + + meta = with stdenv.lib; { + description = "SAT/PseudoBoolean/MaxSat/ASP solver using glucose"; + maintainers = with maintainers; [ gebner ma27 ]; + platforms = platforms.unix; + license = licenses.asl20; + homepage = http://alviano.net/software/maxino/; + # See pkgs/applications/science/logic/glucose/default.nix + badPlatforms = [ "aarch64-linux" ]; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/avy/0001-no-static-boost-libs.patch b/nixpkgs/pkgs/applications/science/logic/avy/0001-no-static-boost-libs.patch new file mode 100644 index 000000000000..a53142faba66 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/avy/0001-no-static-boost-libs.patch @@ -0,0 +1,12 @@ +diff --git a/avy/CMakeLists.txt b/avy/CMakeLists.txt +index 5913076..b0453b5 100644 +--- a/avy/CMakeLists.txt ++++ b/avy/CMakeLists.txt +@@ -23,7 +23,6 @@ if (CUSTOM_BOOST_ROOT) + set (Boost_NO_SYSTEM_PATHS "ON") + endif() + +-set (Boost_USE_STATIC_LIBS ON) + find_package (Boost 1.46.1 REQUIRED program_options) + IF (Boost_FOUND) + include_directories (${Boost_INCLUDE_DIRS}) diff --git a/nixpkgs/pkgs/applications/science/logic/avy/default.nix b/nixpkgs/pkgs/applications/science/logic/avy/default.nix new file mode 100644 index 000000000000..9b59828ddab7 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/avy/default.nix @@ -0,0 +1,53 @@ +{ stdenv, fetchgit, cmake, zlib, boost }: + +stdenv.mkDerivation { + pname = "avy"; + version = "2017.10.16"; + + src = fetchgit { + url = "https://bitbucket.org/arieg/extavy"; + rev = "c75c83379c38d6ea1046d0caee95aef77283ffe3"; + sha256 = "0zcycnypg4q5g710bnkjpycaawmibc092vmyhgfbixkgq9fb5lfh"; + fetchSubmodules = true; + }; + + buildInputs = [ cmake zlib boost.out boost.dev ]; + NIX_CFLAGS_COMPILE = [ "-Wno-narrowing" ] + # Squelch endless stream of warnings on same few things + ++ stdenv.lib.optionals stdenv.cc.isClang [ + "-Wno-empty-body" + "-Wno-tautological-compare" + "-Wc++11-compat-deprecated-writable-strings" + "-Wno-deprecated" + ]; + + prePatch = '' + sed -i -e '1i#include <stdint.h>' abc/src/bdd/dsd/dsd.h + substituteInPlace abc/src/bdd/dsd/dsd.h --replace \ + '((Child = Dsd_NodeReadDec(Node,Index))>=0);' \ + '((intptr_t)(Child = Dsd_NodeReadDec(Node,Index))>=0);' + + patch -p1 -d minisat -i ${./minisat-fenv.patch} + patch -p1 -d glucose -i ${./glucose-fenv.patch} + ''; + + patches = + [ ./0001-no-static-boost-libs.patch + ]; + + installPhase = '' + mkdir -p $out/bin + cp avy/src/{avy,avybmc} $out/bin/ + ''; + + 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; + # 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/avy/glucose-fenv.patch b/nixpkgs/pkgs/applications/science/logic/avy/glucose-fenv.patch new file mode 100644 index 000000000000..dd19f7ec80e7 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/avy/glucose-fenv.patch @@ -0,0 +1,65 @@ +From d6e0cb60270e8653bda3f339e3a07ce2cd2d6eb0 Mon Sep 17 00:00:00 2001 +From: Will Dietz <w@wdtz.org> +Date: Tue, 17 Oct 2017 23:01:36 -0500 +Subject: [PATCH] glucose: use fenv to set double precision + +--- + 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 c96aadd..994132b 100644 +--- a/core/Main.cc ++++ b/core/Main.cc +@@ -96,8 +96,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("c WARNING: for repeatability, setting FPU to use double precision\n"); + #endif + // Extra options: +diff --git a/simp/Main.cc b/simp/Main.cc +index 4f4772d..70c2e4b 100644 +--- a/simp/Main.cc ++++ b/simp/Main.cc +@@ -97,8 +97,12 @@ int main(int argc, char** argv) + + + #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 004d498..a768e99 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 Glucose_System_h + + #if defined(__linux__) +-#include <fpu_control.h> ++#include <fenv.h> + #endif + + #include "glucose/mtl/IntTypes.h" +-- +2.14.2 + diff --git a/nixpkgs/pkgs/applications/science/logic/avy/minisat-fenv.patch b/nixpkgs/pkgs/applications/science/logic/avy/minisat-fenv.patch new file mode 100644 index 000000000000..686d5a1c5b49 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/avy/minisat-fenv.patch @@ -0,0 +1,65 @@ +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 + diff --git a/nixpkgs/pkgs/applications/science/logic/beluga/default.nix b/nixpkgs/pkgs/applications/science/logic/beluga/default.nix new file mode 100644 index 000000000000..da0e9bf1c1dd --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/beluga/default.nix @@ -0,0 +1,34 @@ +{ stdenv, fetchFromGitHub, ocamlPackages, omake }: + +stdenv.mkDerivation { + name = "beluga-20180403"; + + src = fetchFromGitHub { + owner = "Beluga-lang"; + repo = "Beluga"; + rev = "046aa59f008be70a7c4700b723bed0214ea8b687"; + sha256 = "0m68y0r0wdw3mg2jks68bihaww7sg305zdfnic1rkndq2cxv0mld"; + }; + + nativeBuildInputs = with ocamlPackages; [ findlib ocamlbuild omake ]; + buildInputs = with ocamlPackages; [ ocaml ulex ocaml_extlib ]; + + installPhase = '' + mkdir -p $out + cp -r bin $out/ + + mkdir -p $out/share/beluga + cp -r tools/ examples/ $out/share/beluga + + mkdir -p $out/share/emacs/site-lisp/beluga/ + cp -r tools/beluga-mode.el $out/share/emacs/site-lisp/beluga + ''; + + meta = { + description = "A functional language for reasoning about formal systems"; + homepage = http://complogic.cs.mcgill.ca/beluga/; + license = stdenv.lib.licenses.gpl3Plus; + maintainers = [ stdenv.lib.maintainers.bcdarwin ]; + platforms = stdenv.lib.platforms.unix; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/boolector/default.nix b/nixpkgs/pkgs/applications/science/logic/boolector/default.nix new file mode 100644 index 000000000000..f1f74bcb5810 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/boolector/default.nix @@ -0,0 +1,50 @@ +{ stdenv, fetchFromGitHub +, cmake, lingeling, btor2tools +}: + +stdenv.mkDerivation rec { + pname = "boolector"; + version = "3.0.0"; + + src = fetchFromGitHub { + owner = "boolector"; + repo = "boolector"; + rev = "refs/tags/${version}"; + sha256 = "15i3ni5klss423m57wcy1gx0m5wfrjmglapwg85pm7fb3jj1y7sz"; + }; + + nativeBuildInputs = [ cmake ]; + buildInputs = [ lingeling btor2tools ]; + + cmakeFlags = + [ "-DSHARED=ON" + "-DUSE_LINGELING=YES" + "-DBTOR2_INCLUDE_DIR=${btor2tools.dev}/include" + "-DBTOR2_LIBRARIES=${btor2tools.lib}/lib/libbtor2parser.so" + "-DLINGELING_INCLUDE_DIR=${lingeling.dev}/include" + "-DLINGELING_LIBRARIES=${lingeling.lib}/lib/liblgl.a" + ]; + + installPhase = '' + mkdir -p $out/bin $lib/lib $dev/include + + cp -vr bin/* $out/bin + cp -vr lib/* $lib/lib + + rm -rf $out/bin/{examples,test} + + cd ../src + find . -iname '*.h' -exec cp --parents '{}' $dev/include \; + rm -rf $dev/include/tests + ''; + + outputs = [ "out" "dev" "lib" ]; + + meta = with stdenv.lib; { + description = "An extremely fast SMT solver for bit-vectors and arrays"; + homepage = https://boolector.github.io; + license = licenses.mit; + platforms = platforms.linux; + maintainers = with maintainers; [ thoughtpolice ]; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/btor2tools/default.nix b/nixpkgs/pkgs/applications/science/logic/btor2tools/default.nix new file mode 100644 index 000000000000..2d00e9f30464 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/btor2tools/default.nix @@ -0,0 +1,33 @@ +{ stdenv, fetchFromGitHub }: + +stdenv.mkDerivation { + pname = "btor2tools"; + version = "pre55_8c150b39"; + + src = fetchFromGitHub { + owner = "boolector"; + repo = "btor2tools"; + rev = "8c150b39cdbcdef4247344acf465d75ef642365d"; + sha256 = "1r5pid4x567nms02ajjrz3v0zj18k0fi5pansrmc2907rnx2acxx"; + }; + + configurePhase = "./configure.sh -shared"; + + installPhase = '' + mkdir -p $out $dev/include/btor2parser/ $lib/lib + + cp -vr bin $out + cp -v src/btor2parser/btor2parser.h $dev/include/btor2parser + cp -v build/libbtor2parser.* $lib/lib + ''; + + outputs = [ "out" "dev" "lib" ]; + + meta = with stdenv.lib; { + description = "Fast SAT solver"; + homepage = http://fmv.jku.at/lingeling/; + license = licenses.mit; + platforms = platforms.linux; + maintainers = with maintainers; [ thoughtpolice ]; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/cedille/default.nix b/nixpkgs/pkgs/applications/science/logic/cedille/default.nix new file mode 100644 index 000000000000..4cef49788c04 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/cedille/default.nix @@ -0,0 +1,52 @@ +{ stdenv +, lib +, fetchFromGitHub +, alex +, happy +, Agda +, buildPlatform +, buildPackages +, ghcWithPackages +}: + +stdenv.mkDerivation rec { + version = "1.1.1"; + pname = "cedille"; + + src = fetchFromGitHub { + owner = "cedille"; + repo = "cedille"; + rev = "v${version}"; + sha256 = "16pc72wz6kclq9yv2r8hx85mkp0s125h12snrhcjxkbl41xx2ynb"; + fetchSubmodules = true; + }; + + nativeBuildInputs = [ alex happy ]; + buildInputs = [ Agda (ghcWithPackages (ps: [ps.ieee])) ]; + + LANG = "en_US.UTF-8"; + LOCALE_ARCHIVE = + lib.optionalString (buildPlatform.libc == "glibc") + "${buildPackages.glibcLocales}/lib/locale/locale-archive"; + + postPatch = '' + patchShebangs create-libraries.sh + ''; + + installPhase = '' + install -Dm755 -t $out/bin/ cedille + install -Dm755 -t $out/bin/ core/cedille-core + install -Dm644 -t $out/share/info docs/info/cedille-info-main.info + + mkdir -p $out/lib/ + cp -r lib/ $out/lib/cedille/ + ''; + + meta = with stdenv.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; + maintainers = with maintainers; [ marsam mpickering ]; + platforms = platforms.unix; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/celf/default.nix b/nixpkgs/pkgs/applications/science/logic/celf/default.nix new file mode 100644 index 000000000000..708270f772fd --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/celf/default.nix @@ -0,0 +1,36 @@ +{ stdenv, fetchFromGitHub, smlnj }: + +stdenv.mkDerivation rec { + pname = "celf"; + pversion = "2013-07-25"; + name = "${pname}-${pversion}"; + + src = fetchFromGitHub { + owner = "clf"; + repo = pname; + rev = "d61d95900ab316468ae850fa34a2fe9488bc5b59"; + sha256 = "0slrwcxglp0sdbp6wr65cdkl5wcap2i0fqxbwqfi1q3cpb6ph6hq"; + }; + + buildInputs = [ smlnj ]; + + # (can also build with MLton) + buildPhase = '' + export SMLNJ_HOME=${smlnj} + sml < main-export.sml + ''; + + installPhase = '' + mkdir -p $out/bin + cp .heap* $out/bin/ + ./.mkexec ${smlnj}/bin/sml $out/bin celf + ''; + + meta = with stdenv.lib; { + description = "Linear logic programming system"; + homepage = https://github.com/clf/celf; + license = licenses.gpl3; + maintainers = with maintainers; [ bcdarwin ]; + platforms = platforms.unix; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/clprover/clprover.nix b/nixpkgs/pkgs/applications/science/logic/clprover/clprover.nix new file mode 100644 index 000000000000..0319069660ed --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/clprover/clprover.nix @@ -0,0 +1,27 @@ +{ stdenv, fetchzip }: + +stdenv.mkDerivation { + pname = "clprover"; + version = "1.0.3"; + + src = fetchzip { + url = "http://cgi.csc.liv.ac.uk/~ullrich/CLProver++/CLProver++-v1.0.3-18-04-2015.zip"; + sha256 = "10kmlg4m572qwfzi6hkyb0ypb643xw8sfb55xx7866lyh37w1q3s"; + stripRoot = false; + }; + + installPhase = '' + mkdir $out + cp -r bin $out/bin + mkdir -p $out/share/clprover + cp -r examples $out/share/clprover/examples + ''; + + meta = with stdenv.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 + maintainers = with maintainers; [ mgttlinger ]; + platforms = [ "x86_64-linux" ]; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/coq/default.nix b/nixpkgs/pkgs/applications/science/logic/coq/default.nix new file mode 100644 index 000000000000..a04ec0bb16ce --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/coq/default.nix @@ -0,0 +1,162 @@ +# - coqide compilation can be disabled by setting buildIde to false +# - The csdp program used for the Micromega tactic is statically referenced. +# However, coq can build without csdp by setting it to null. +# In this case some Micromega tactics will search the user's path for the csdp program and will fail if it is not found. +# - The exact version can be specified through the `version` argument to +# the derivation; it defaults to the latest stable version. + +{ stdenv, fetchFromGitHub, writeText, pkgconfig +, ocamlPackages, ncurses +, buildIde ? true +, glib, gnome3, wrapGAppsHook +, csdp ? null +, version +}: + +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+beta2" = "0jk7pwydhd17ab7ii69zvi4sgrr630q2lsxhckaj3sz55cpjlhal"; + }.${version}; + coq-version = stdenv.lib.versions.majorMinor version; + versionAtLeast = stdenv.lib.versionAtLeast coq-version; + ideFlags = stdenv.lib.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 ""; +self = stdenv.mkDerivation { + pname = "coq"; + inherit version; + + passthru = { + inherit coq-version; + inherit ocamlPackages; + # For compatibility + inherit (ocamlPackages) ocaml camlp5 findlib num; + emacsBufferSetup = pkgs: '' + ; Propagate coq paths to children + (inherit-local-permanent coq-prog-name "${self}/bin/coqtop") + (inherit-local-permanent coq-dependency-analyzer "${self}/bin/coqdep") + (inherit-local-permanent coq-compiler "${self}/bin/coqc") + ; If the coq-library path was already set, re-set it based on our current coq + (when (fboundp 'get-coq-library-directory) + (inherit-local-permanent coq-library-directory (get-coq-library-directory)) + (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)})) + ; TODO Abstract this pattern from here and nixBufferBuilders.withPackages! + (defvar nixpkgs--coq-buffer-count 0) + (when (eq nixpkgs--coq-buffer-count 0) + (make-variable-buffer-local 'nixpkgs--is-nixpkgs-coq-buffer) + (defun nixpkgs--coq-inherit (buf) + (inherit-local-inherit-child buf) + (with-current-buffer buf + (setq nixpkgs--coq-buffer-count (1+ nixpkgs--coq-buffer-count)) + (add-hook 'kill-buffer-hook 'nixpkgs--decrement-coq-buffer-count nil t)) + buf) + ; When generating a scomint buffer, do inherit-local inheritance and make it a nixpkgs-coq buffer + (defun nixpkgs--around-scomint-make (orig &rest r) + (if nixpkgs--is-nixpkgs-coq-buffer + (progn + (advice-add 'get-buffer-create :filter-return #'nixpkgs--coq-inherit) + (apply orig r) + (advice-remove 'get-buffer-create #'nixpkgs--coq-inherit)) + (apply orig r))) + (advice-add 'scomint-make :around #'nixpkgs--around-scomint-make) + ; When we have no more coq buffers, tear down the buffer handling + (defun nixpkgs--decrement-coq-buffer-count () + (setq nixpkgs--coq-buffer-count (1- nixpkgs--coq-buffer-count)) + (when (eq nixpkgs--coq-buffer-count 0) + (advice-remove 'scomint-make #'nixpkgs--around-scomint-make) + (fmakunbound 'nixpkgs--around-scomint-make) + (fmakunbound 'nixpkgs--coq-inherit) + (fmakunbound 'nixpkgs--decrement-coq-buffer-count)))) + (setq nixpkgs--coq-buffer-count (1+ nixpkgs--coq-buffer-count)) + (add-hook 'kill-buffer-hook 'nixpkgs--decrement-coq-buffer-count nil t) + (setq nixpkgs--is-nixpkgs-coq-buffer t) + (inherit-local 'nixpkgs--is-nixpkgs-coq-buffer) + ''; + }; + + src = fetchFromGitHub { + owner = "coq"; + repo = "coq"; + rev = "V${version}"; + inherit sha256; + }; + + nativeBuildInputs = [ pkgconfig ]; + buildInputs = [ ncurses ] ++ (with ocamlPackages; [ ocaml findlib camlp5 num ]) + ++ stdenv.lib.optionals buildIde + (if versionAtLeast "8.10" + then [ ocamlPackages.lablgtk3-sourceview3 glib gnome3.defaultIconTheme wrapGAppsHook ] + else [ ocamlPackages.lablgtk ]); + + postPatch = '' + UNAME=$(type -tp uname) + RM=$(type -tp rm) + substituteInPlace configure --replace "/bin/uname" "$UNAME" + substituteInPlace tools/beautify-archive --replace "/bin/rm" "$RM" + substituteInPlace configure.ml --replace '"md5 -q"' '"md5sum"' + ${csdpPatch} + ''; + + setupHook = writeText "setupHook.sh" '' + addCoqPath () { + if test -d "''$1/lib/coq/${coq-version}/user-contrib"; then + export COQPATH="''${COQPATH}''${COQPATH:+:}''$1/lib/coq/${coq-version}/user-contrib/" + fi + } + + addEnvHooks "$targetOffset" addCoqPath + ''; + + preConfigure = if versionAtLeast "8.10" then '' + patchShebangs dev/tools/ + '' else '' + configureFlagsArray=( + ${ideFlags} + ) + ''; + + prefixKey = "-prefix "; + + buildFlags = "revision coq coqide bin/votour"; + + createFindlibDestdir = true; + + postInstall = '' + cp bin/votour $out/bin/ + ln -s $out/lib/coq $OCAMLFIND_DESTDIR/coq + ''; + + meta = with stdenv.lib; { + description = "Coq proof assistant"; + longDescription = '' + Coq is a formal proof management system. It provides a formal language + to write mathematical definitions, executable algorithms and theorems + together with an environment for semi-interactive development of + machine-checked proofs. + ''; + homepage = http://coq.inria.fr; + license = licenses.lgpl21; + branch = coq-version; + maintainers = with maintainers; [ roconnor thoughtpolice vbgl Zimmi48 ]; + platforms = platforms.unix; + }; +}; in self diff --git a/nixpkgs/pkgs/applications/science/logic/coq2html/default.nix b/nixpkgs/pkgs/applications/science/logic/coq2html/default.nix new file mode 100644 index 000000000000..bebf81b030d6 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/coq2html/default.nix @@ -0,0 +1,39 @@ +{ stdenv, fetchgit, ocaml }: + +let + version = "20170720"; +in + +stdenv.mkDerivation { + pname = "coq2html"; + inherit version; + + src = fetchgit { + url = "https://github.com/xavierleroy/coq2html"; + rev = "e2b94093c6b9a877717f181765e30577de22439e"; + sha256 = "1x466j0pyjggyz0870pdllv9f5vpnfrgkd0w7ajvm9rkwyp3f610"; + }; + + buildInputs = [ ocaml ]; + + installPhase = '' + mkdir -p $out/bin + cp coq2html $out/bin + ''; + + meta = with stdenv.lib; { + description = "coq2html is an HTML documentation generator for Coq source files"; + longDescription = '' + coq2html is an HTML documentation generator for Coq source files. It is + an alternative to the standard coqdoc documentation generator + distributed along with Coq. The major feature of coq2html is its ability + to fold proof scripts: in the generated HTML, proof scripts are + initially hidden, but can be revealed one by one by clicking on the + "Proof" keyword. + ''; + homepage = https://github.com/xavierleroy/coq2html; + license = licenses.gpl2; + maintainers = with maintainers; [ jwiegley ]; + platforms = platforms.unix; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/cryptominisat/default.nix b/nixpkgs/pkgs/applications/science/logic/cryptominisat/default.nix new file mode 100644 index 000000000000..b4c4cb7c047d --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/cryptominisat/default.nix @@ -0,0 +1,24 @@ +{ stdenv, fetchFromGitHub, cmake, python3, xxd, boost }: + +stdenv.mkDerivation rec { + pname = "cryptominisat"; + version = "5.6.8"; + + src = fetchFromGitHub { + owner = "msoos"; + repo = "cryptominisat"; + rev = version; + sha256 = "0csimmy1nvkfcsxjra9bm4mlcyxa3ac8zarm88zfb7640ca0d0wv"; + }; + + buildInputs = [ python3 boost ]; + nativeBuildInputs = [ cmake xxd ]; + + meta = with stdenv.lib; { + description = "An advanced SAT Solver"; + homepage = https://github.com/msoos/cryptominisat; + license = licenses.mit; + maintainers = with maintainers; [ mic92 ]; + platforms = platforms.unix; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/cryptoverif/default.nix b/nixpkgs/pkgs/applications/science/logic/cryptoverif/default.nix new file mode 100644 index 000000000000..6877060d36d6 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/cryptoverif/default.nix @@ -0,0 +1,37 @@ +{ stdenv, fetchurl, ocaml }: + +stdenv.mkDerivation rec { + pname = "cryptoverif"; + version = "2.01pl1"; + + src = fetchurl { + url = "http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/cryptoverif${version}.tar.gz"; + sha256 = "1bkmrv3wsy8mwhrxd3z3br9zgv37c2w6443rm4s9jl0aphcgnbiw"; + }; + + buildInputs = [ ocaml ]; + + /* Fix up the frontend to load the 'default' cryptoverif library + ** from under $out/libexec. By default, it expects to find the files + ** in $CWD which doesn't work. */ + patchPhase = '' + substituteInPlace ./src/settings.ml \ + --replace \"default\" \"$out/libexec/default\" + ''; + + buildPhase = "./build"; + installPhase = '' + mkdir -p $out/bin $out/libexec + cp ./cryptoverif $out/bin + cp ./default.cvl $out/libexec + cp ./default.ocvl $out/libexec + ''; + + 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 ]; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/cubicle/default.nix b/nixpkgs/pkgs/applications/science/logic/cubicle/default.nix new file mode 100644 index 000000000000..cd41e1ca64b9 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/cubicle/default.nix @@ -0,0 +1,24 @@ +{ stdenv, fetchurl, ocamlPackages }: + +stdenv.mkDerivation rec { + pname = "cubicle"; + version = "1.1.2"; + src = fetchurl { + url = "http://cubicle.lri.fr/cubicle-${version}.tar.gz"; + sha256 = "10kk80jdmpdvql88sdjsh7vqzlpaphd8vip2lp47aarxjkwjlz1q"; + }; + + postPatch = '' + substituteInPlace Makefile.in --replace "\\n" "" + ''; + + buildInputs = with ocamlPackages; [ ocaml findlib functory ]; + + meta = with stdenv.lib; { + description = "An open source model checker for verifying safety properties of array-based systems"; + homepage = http://cubicle.lri.fr/; + license = licenses.asl20; + platforms = platforms.unix; + maintainers = with maintainers; [ lucas8 ]; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/cvc3/cvc3-2.4.1-gccv6-fix.patch b/nixpkgs/pkgs/applications/science/logic/cvc3/cvc3-2.4.1-gccv6-fix.patch new file mode 100644 index 000000000000..1fb3516b8c27 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/cvc3/cvc3-2.4.1-gccv6-fix.patch @@ -0,0 +1,76 @@ +commit 4eb28b907e89be05d92eb704115f821b9b848e60 +Author: Matthew Dawson <matthew@mjdsystems.ca> +Date: Sun Oct 16 22:06:03 2016 -0400 + + Fix gcc v6 compile failures. + + * Use std::hash<const char*> over std::hash<char *>, as throwing away the const is not allowed. + * Use Hash::hash by default in CDMap over std::hash, to get Hash::hash<CVC3::expr> + +diff --git a/src/expr/expr_value.cpp b/src/expr/expr_value.cpp +index 0c85ff6..e4dd251 100644 +--- a/src/expr/expr_value.cpp ++++ b/src/expr/expr_value.cpp +@@ -29,7 +29,7 @@ namespace CVC3 { + // Class ExprValue static members + //////////////////////////////////////////////////////////////////////// + +-std::hash<char*> ExprValue::s_charHash; ++std::hash<const char*> ExprValue::s_charHash; + std::hash<long int> ExprValue::s_intHash; + + //////////////////////////////////////////////////////////////////////// +diff --git a/src/include/cdmap.h b/src/include/cdmap.h +index faf682a..c3b094c 100644 +--- a/src/include/cdmap.h ++++ b/src/include/cdmap.h +@@ -43,9 +43,9 @@ namespace CVC3 { + // Auxiliary class: almost the same as CDO (see cdo.h), but on + // setNull() call it erases itself from the map. + +-template <class Key, class Data, class HashFcn = std::hash<Key> > class CDMap; ++template <class Key, class Data, class HashFcn = Hash::hash<Key> > class CDMap; + +-template <class Key, class Data, class HashFcn = std::hash<Key> > ++template <class Key, class Data, class HashFcn = Hash::hash<Key> > + class CDOmap :public ContextObj { + Key d_key; + Data d_data; +diff --git a/src/include/expr_hash.h b/src/include/expr_hash.h +index b2107d7..baa2eab 100644 +--- a/src/include/expr_hash.h ++++ b/src/include/expr_hash.h +@@ -20,7 +20,6 @@ + * hash_set over Expr class. + */ + /*****************************************************************************/ +- + #ifndef _cvc3__expr_h_ + #include "expr.h" + #endif +diff --git a/src/include/expr_value.h b/src/include/expr_value.h +index 95102b2..f53aa4d 100644 +--- a/src/include/expr_value.h ++++ b/src/include/expr_value.h +@@ -179,7 +179,7 @@ protected: + // Static hash functions. They don't depend on the context + // (ExprManager and such), so it is still thread-safe to have them + // static. +- static std::hash<char*> s_charHash; ++ static std::hash<const char*> s_charHash; + static std::hash<long int> s_intHash; + + static size_t pointerHash(void* p) { return s_intHash((long int)p); } +diff --git a/src/theory_core/theory_core.cpp b/src/theory_core/theory_core.cpp +index df5289f..37ccab9 100644 +--- a/src/theory_core/theory_core.cpp ++++ b/src/theory_core/theory_core.cpp +@@ -710,7 +710,7 @@ TheoryCore::TheoryCore(ContextManager* cm, + // d_termTheorems(cm->getCurrentContext()), + d_predicates(cm->getCurrentContext()), + d_solver(NULL), +- d_simplifyInPlace(false), ++ d_simplifyInPlace(NULL), + d_currentRecursiveSimplifier(NULL), + d_resourceLimit(0), + d_timeBase(0), diff --git a/nixpkgs/pkgs/applications/science/logic/cvc3/default.nix b/nixpkgs/pkgs/applications/science/logic/cvc3/default.nix new file mode 100644 index 000000000000..dfb04ad90e92 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/cvc3/default.nix @@ -0,0 +1,34 @@ +{ stdenv, fetchurl, flex, bison, gmp, perl }: + +stdenv.mkDerivation rec { + pname = "cvc3"; + version = "2.4.1"; + + src = fetchurl { + url = "http://www.cs.nyu.edu/acsys/cvc3/releases/${version}/${pname}-${version}.tar.gz"; + sha256 = "1xxcwhz3y6djrycw8sm6xz83wb4hb12rd1n0skvc7fng0rh1snym"; + }; + + buildInputs = [ gmp flex bison perl ]; + + patches = [ ./cvc3-2.4.1-gccv6-fix.patch ]; + + preConfigure = '' + sed -e "s@ /bin/bash@bash@g" -i Makefile.std + find . -exec sed -e "s@/usr/bin/perl@${perl}/bin/perl@g" -i '{}' ';' + ''; + + meta = with stdenv.lib; { + description = "A prover for satisfiability modulo theory (SMT)"; + maintainers = with maintainers; + [ raskin ]; + platforms = platforms.linux; + license = licenses.free; + homepage = http://www.cs.nyu.edu/acsys/cvc3/index.html; + }; + passthru = { + updateInfo = { + downloadPage = "http://www.cs.nyu.edu/acsys/cvc3/download.html"; + }; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/cvc4/default.nix b/nixpkgs/pkgs/applications/science/logic/cvc4/default.nix new file mode 100644 index 000000000000..c0c7a53ebd44 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/cvc4/default.nix @@ -0,0 +1,43 @@ +{ stdenv, fetchurl, cln, gmp, swig, pkgconfig +, readline, libantlr3c, boost, jdk, autoreconfHook +, python3, antlr3_4 +}: + +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"; + }; + + nativeBuildInputs = [ autoreconfHook pkgconfig ]; + buildInputs = [ gmp cln readline swig libantlr3c antlr3_4 boost jdk python3 ]; + configureFlags = [ + "--enable-language-bindings=c,c++,java" + "--enable-gpl" + "--with-cln" + "--with-readline" + "--with-boost=${boost.dev}" + ]; + + prePatch = '' + patch -p1 -i ${./minisat-fenv.patch} -d src/prop/minisat + patch -p1 -i ${./minisat-fenv.patch} -d src/prop/bvminisat + ''; + + preConfigure = '' + patchShebangs ./src/ + ''; + + enableParallelBuilding = true; + + meta = with stdenv.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/nixpkgs/pkgs/applications/science/logic/cvc4/minisat-fenv.patch b/nixpkgs/pkgs/applications/science/logic/cvc4/minisat-fenv.patch new file mode 100644 index 000000000000..686d5a1c5b49 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/cvc4/minisat-fenv.patch @@ -0,0 +1,65 @@ +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 + diff --git a/nixpkgs/pkgs/applications/science/logic/drat-trim/default.nix b/nixpkgs/pkgs/applications/science/logic/drat-trim/default.nix new file mode 100644 index 000000000000..4c4ea0f14ce1 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/drat-trim/default.nix @@ -0,0 +1,40 @@ +{ stdenv, fetchFromGitHub }: + +stdenv.mkDerivation { + name = "drat-trim-2017-08-31"; + + src = fetchFromGitHub { + owner = "marijnheule"; + repo = "drat-trim"; + rev = "37ac8f874826ffa3500a00698910e137498defac"; + sha256 = "1m9q47dfnvdli1z3kb1jvvbm0dgaw725k1aw6h9w00bggqb91bqh"; + }; + + postPatch = '' + substituteInPlace Makefile --replace gcc cc + ''; + + installPhase = '' + install -Dt $out/bin drat-trim + ''; + + meta = with stdenv.lib; { + description = "A proof checker for unSAT proofs"; + longDescription = '' + DRAT-trim is a satisfiability proof checking and trimming + utility designed to validate proofs for all known satisfiability + solving and preprocessing techniques. DRAT-trim can also emit + trimmed formulas, optimized proofs, and TraceCheck+ dependency + graphs. + + DRAT-trim has been used as part of the judging process in the + annual SAT Competition in recent years, in order to check + competing SAT solvers' work when they claim that a SAT instance + is unsatisfiable. + ''; + homepage = https://www.cs.utexas.edu/~marijn/drat-trim/; + license = licenses.mit; + maintainers = with maintainers; [ kini ]; + platforms = platforms.all; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/ekrhyper/default.nix b/nixpkgs/pkgs/applications/science/logic/ekrhyper/default.nix new file mode 100644 index 000000000000..e1eb9a2dcc3b --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/ekrhyper/default.nix @@ -0,0 +1,32 @@ +{stdenv, fetchurl, ocaml, perl}: +let + s = # Generated upstream information + rec { + baseName="ekrhyper"; + version="1_4_21022014"; + name="${baseName}-${version}"; + hash="14xaaxyvfli1nd4vd9fp4j1s8k76z2bhazxzzc7br3q6hc6b8ivw"; + url="http://userpages.uni-koblenz.de/~bpelzer/ekrhyper/ekrh_1_4_21022014.tar.gz"; + sha256="14xaaxyvfli1nd4vd9fp4j1s8k76z2bhazxzzc7br3q6hc6b8ivw"; + }; + buildInputs = [ + ocaml perl + ]; +in +stdenv.mkDerivation { + inherit (s) name version; + inherit buildInputs; + src = fetchurl { + inherit (s) url sha256; + }; + setSourceRoot = "export sourceRoot=$(echo */ekrh/src/)"; + preInstall = "export INSTALLDIR=$out"; + postInstall = ''for i in "$out/casc"/*; do ln -s "$i" "$out/bin/ekrh-casc-$(basename $i)"; done ''; + 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; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/ekrhyper/default.upstream b/nixpkgs/pkgs/applications/science/logic/ekrhyper/default.upstream new file mode 100644 index 000000000000..310e93ea53fd --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/ekrhyper/default.upstream @@ -0,0 +1,3 @@ +url http://userpages.uni-koblenz.de/~bpelzer/ekrhyper/ +ensure_choice +version '.*[^0-9]_([-0-9_]+)[.].*' '\1' diff --git a/nixpkgs/pkgs/applications/science/logic/elan/default.nix b/nixpkgs/pkgs/applications/science/logic/elan/default.nix new file mode 100644 index 000000000000..f9a911d82108 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/elan/default.nix @@ -0,0 +1,44 @@ +{ stdenv, pkgconfig, curl, openssl, zlib, fetchFromGitHub, rustPlatform }: + +rustPlatform.buildRustPackage rec { + pname = "elan"; + version = "0.7.5"; + + cargoSha256 = "0lc320m3vw76d6pa5wp6c9jblac6lmyf9qqnxmsnkn4ixdhnghsd"; + + src = fetchFromGitHub { + owner = "kha"; + repo = "elan"; + rev = "v${version}"; + sha256 = "1147f3lzr6lgvf580ppspn20bdwnf6l8idh1h5ana0p0lf5a0dn1"; + }; + + nativeBuildInputs = [ pkgconfig ]; + + buildInputs = [ curl zlib openssl ]; + + cargoBuildFlags = [ "--features no-self-update" ]; + + postInstall = '' + pushd $out/bin + mv elan-init elan + for link in lean leanpkg leanchecker; do + ln -s elan $link + done + popd + + # tries to create .elan + export HOME=$(mktemp -d) + mkdir -p "$out/share/"{bash-completion/completions,fish/vendor_completions.d,zsh/site-functions} + $out/bin/elan completions bash > "$out/share/bash-completion/completions/elan" + $out/bin/elan completions fish > "$out/share/fish/vendor_completions.d/elan.fish" + $out/bin/elan completions zsh > "$out/share/zsh/site-functions/_elan" + ''; + + meta = with stdenv.lib; { + description = "Small tool to manage your installations of the Lean theorem prover"; + homepage = "https://github.com/Kha/elan"; + license = with licenses; [ asl20 /* or */ mit ]; + maintainers = with maintainers; [ gebner ]; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/eprover/default.nix b/nixpkgs/pkgs/applications/science/logic/eprover/default.nix new file mode 100644 index 000000000000..1f6fced22335 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/eprover/default.nix @@ -0,0 +1,29 @@ +{ stdenv, fetchurl, which }: + +stdenv.mkDerivation rec { + pname = "eprover"; + version = "2.3"; + + src = fetchurl { + url = "https://wwwlehre.dhbw-stuttgart.de/~sschulz/WORK/E_DOWNLOAD/V_${version}/E.tgz"; + sha256 = "15pbmi195812a2pwrvfa4gwad0cy7117d5kaw98651g6fzgd4rjk"; + }; + + buildInputs = [ which ]; + + preConfigure = '' + sed -e 's/ *CC *= *gcc$//' -i Makefile.vars + ''; + configureFlags = [ + "--exec-prefix=$(out)" + "--man-prefix=$(out)/share/man" + ]; + + meta = with stdenv.lib; { + description = "Automated theorem prover for full first-order logic with equality"; + homepage = http://www.eprover.org/; + license = licenses.gpl2; + maintainers = with maintainers; [ raskin gebner ]; + platforms = platforms.all; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/fast-downward/default.nix b/nixpkgs/pkgs/applications/science/logic/fast-downward/default.nix new file mode 100644 index 000000000000..ed757e444b7c --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/fast-downward/default.nix @@ -0,0 +1,55 @@ +{ stdenv, lib, fetchhg, cmake, which, python3, osi, cplex }: + +stdenv.mkDerivation { + name = "fast-downward-2019-05-13"; + + src = fetchhg { + url = "http://hg.fast-downward.org/"; + rev = "090f5df5d84a"; + sha256 = "14pcjz0jfzx5269axg66iq8js7lm2w3cnqrrhhwmz833prjp945g"; + }; + + nativeBuildInputs = [ cmake which ]; + buildInputs = [ python3 python3.pkgs.wrapPython osi ]; + + cmakeFlags = + lib.optional osi.withCplex [ "-DDOWNWARD_CPLEX_ROOT=${cplex}/cplex" ]; + + enableParallelBuilding = true; + + postPatch = '' + cd src + # Needed because the package tries to be too smart. + export CC="$(which $CC)" + export CXX="$(which $CXX)" + ''; + + installPhase = '' + install -Dm755 bin/downward $out/libexec/fast-downward/downward + cp -r ../translate $out/libexec/fast-downward/ + install -Dm755 ../../fast-downward.py $out/bin/fast-downward + mkdir -p $out/${python3.sitePackages} + cp -r ../../driver $out/${python3.sitePackages} + + wrapPythonProgramsIn $out/bin "$out $pythonPath" + wrapPythonProgramsIn $out/libexec/fast-downward/translate "$out $pythonPath" + # Because fast-downward calls `python translate.py` we need to return wrapped scripts back. + for i in $out/libexec/fast-downward/translate/.*-wrapped; do + name="$(basename "$i")" + name1="''${name#.}" + name2="''${name1%-wrapped}" + dir="$(dirname "$i")" + dest="$dir/$name2" + echo "Moving $i to $dest" + mv "$i" "$dest" + done + ''; + + meta = with stdenv.lib; { + description = "A domain-independent planning system"; + homepage = "http://www.fast-downward.org/"; + license = licenses.gpl3Plus; + platforms = platforms.linux; + maintainers = with maintainers; [ abbradar ]; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/gappa/default.nix b/nixpkgs/pkgs/applications/science/logic/gappa/default.nix new file mode 100644 index 000000000000..7522eb4790ed --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/gappa/default.nix @@ -0,0 +1,23 @@ +{ stdenv, fetchurl, gmp, mpfr, boost }: + +stdenv.mkDerivation { + name = "gappa-1.3.5"; + + src = fetchurl { + url = https://gforge.inria.fr/frs/download.php/file/38044/gappa-1.3.5.tar.gz; + sha256 = "0q1wdiwqj6fsbifaayb1zkp20bz8a1my81sqjsail577jmzwi07w"; + }; + + buildInputs = [ gmp mpfr boost.dev ]; + + buildPhase = "./remake"; + installPhase = "./remake install"; + + 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; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/glucose/default.nix b/nixpkgs/pkgs/applications/science/logic/glucose/default.nix new file mode 100644 index 000000000000..0a8fad484da7 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/glucose/default.nix @@ -0,0 +1,29 @@ +{ stdenv, fetchurl, zlib }: +stdenv.mkDerivation rec { + pname = "glucose"; + version = "4.1"; + + src = fetchurl { + url = "http://www.labri.fr/perso/lsimon/downloads/softwares/glucose-syrup-${version}.tgz"; + sha256 = "0aahrkaq7n0z986fpqz66yz946nxardfi6dh8calzcfjpvqiraji"; + }; + + buildInputs = [ zlib ]; + + sourceRoot = "glucose-syrup-${version}/simp"; + makeFlags = [ "r" ]; + installPhase = '' + install -Dm0755 glucose_release $out/bin/glucose + mkdir -p "$out/share/doc/${pname}-${version}/" + install -Dm0755 ../{LICEN?E,README*,Changelog*} "$out/share/doc/${pname}-${version}/" + ''; + + meta = with stdenv.lib; { + description = "Modern, parallel SAT solver (sequential version)"; + license = licenses.mit; + platforms = platforms.unix; + maintainers = with maintainers; [ gebner ]; + # Build uses _FPU_EXTENDED macro + badPlatforms = [ "aarch64-linux" ]; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/glucose/syrup.nix b/nixpkgs/pkgs/applications/science/logic/glucose/syrup.nix new file mode 100644 index 000000000000..816f8504a52e --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/glucose/syrup.nix @@ -0,0 +1,24 @@ +{ stdenv, zlib, glucose }: +stdenv.mkDerivation rec { + pname = "glucose-syrup"; + version = glucose.version; + + src = glucose.src; + + buildInputs = [ zlib ]; + + sourceRoot = "glucose-syrup-${version}/parallel"; + makeFlags = [ "r" ]; + installPhase = '' + install -Dm0755 glucose-syrup_release $out/bin/glucose-syrup + mkdir -p "$out/share/doc/${pname}-${version}/" + install -Dm0755 ../{LICEN?E,README*,Changelog*} "$out/share/doc/${pname}-${version}/" + ''; + + meta = with stdenv.lib; { + description = "Modern, parallel SAT solver (parallel version)"; + license = licenses.unfreeRedistributable; + platforms = platforms.unix; + maintainers = with maintainers; [ gebner ]; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/hol/default.nix b/nixpkgs/pkgs/applications/science/logic/hol/default.nix new file mode 100644 index 000000000000..d6a1eb6cbf71 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/hol/default.nix @@ -0,0 +1,88 @@ +{stdenv, pkgs, fetchurl, graphviz, fontconfig, liberation_ttf, + experimentalKernel ? true}: + +let + pname = "hol4"; + vnum = "10"; +in + +let + version = "k.${vnum}"; + longVersion = "kananaskis-${vnum}"; + holsubdir = "hol-${longVersion}"; + kernelFlag = if experimentalKernel then "-expk" else "-stdknl"; +in + +let + polymlEnableShared = with pkgs; lib.overrideDerivation polyml (attrs: { + configureFlags = [ "--enable-shared" ]; + }); +in + +stdenv.mkDerivation { + name = "${pname}-${version}"; + + src = fetchurl { + url = "mirror://sourceforge/hol/hol/${longVersion}/${holsubdir}.tar.gz"; + sha256 = "0x2wxksr305h1lrbklf6p42lp09rbhb4rsh74g0l70sgapyiac9b"; + }; + + buildInputs = [polymlEnableShared graphviz fontconfig liberation_ttf]; + + buildCommand = '' + + mkdir chroot-fontconfig + cat ${fontconfig.out}/etc/fonts/fonts.conf > chroot-fontconfig/fonts.conf + sed -e 's@</fontconfig>@@' -i chroot-fontconfig/fonts.conf + echo "<dir>${liberation_ttf}</dir>" >> chroot-fontconfig/fonts.conf + echo "</fontconfig>" >> chroot-fontconfig/fonts.conf + + export FONTCONFIG_FILE=$(pwd)/chroot-fontconfig/fonts.conf + + mkdir -p "$out/src" + cd "$out/src" + + tar -xzf "$src" + cd ${holsubdir} + + substituteInPlace tools/Holmake/Holmake_types.sml \ + --replace "\"/bin/mv\"" "\"mv\"" \ + --replace "\"/bin/cp\"" "\"cp\"" + + for f in tools/buildutils.sml help/src-sml/DOT; + do + substituteInPlace $f --replace "\"/usr/bin/dot\"" "\"${graphviz}/bin/dot\"" + done + + #sed -ie "/compute/,999 d" tools/build-sequence # for testing + + poly < tools/smart-configure.sml + + bin/build ${kernelFlag} -symlink + + mkdir -p "$out/bin" + ln -st $out/bin $out/src/${holsubdir}/bin/* + # ln -s $out/src/hol4.${version}/bin $out/bin + ''; + + meta = with stdenv.lib; { + description = "Interactive theorem prover based on Higher-Order Logic"; + longDescription = '' + HOL4 is the latest version of the HOL interactive proof + assistant for higher order logic: a programming environment in + which theorems can be proved and proof tools + implemented. Built-in decision procedures and theorem provers + can automatically establish many simple theorems (users may have + to prove the hard theorems themselves!) An oracle mechanism + gives access to external programs such as SMT and BDD + engines. HOL4 is particularly suitable as a platform for + implementing combinations of deduction, execution and property + checking. + ''; + homepage = http://hol.sourceforge.net/; + license = licenses.bsd3; + maintainers = with maintainers; [ mudri ]; + platforms = with platforms; linux; + broken = true; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/hol_light/default.nix b/nixpkgs/pkgs/applications/science/logic/hol_light/default.nix new file mode 100644 index 000000000000..40b0115dc1b7 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/hol_light/default.nix @@ -0,0 +1,50 @@ +{ stdenv, runtimeShell, fetchFromGitHub, ocaml, num, camlp5 }: + +let + load_num = + if num == null then "" else + '' + -I ${num}/lib/ocaml/${ocaml.version}/site-lib/num \ + -I ${num}/lib/ocaml/${ocaml.version}/site-lib/top-num \ + -I ${num}/lib/ocaml/${ocaml.version}/site-lib/stublibs \ + ''; + + start_script = + '' + #!${runtimeShell} + cd $out/lib/hol_light + exec ${ocaml}/bin/ocaml \ + -I \`${camlp5}/bin/camlp5 -where\` \ + ${load_num} \ + -init make.ml + ''; +in + +stdenv.mkDerivation { + name = "hol_light-2019-03-27"; + + src = fetchFromGitHub { + owner = "jrh13"; + repo = "hol-light"; + rev = "a2b487b38d9da47350f1b4316e34a8fa4cf7a40a"; + sha256 = "1qlidl15qi8w4si8wxcmj8yg2srsb0q4k1ad9yd91sgx9h9aq8fk"; + }; + + buildInputs = [ ocaml camlp5 ]; + propagatedBuildInputs = [ num ]; + + installPhase = '' + mkdir -p "$out/lib/hol_light" "$out/bin" + cp -a . $out/lib/hol_light + echo "${start_script}" > "$out/bin/hol_light" + chmod a+x "$out/bin/hol_light" + ''; + + meta = with stdenv.lib; { + description = "Interactive theorem prover based on Higher-Order Logic"; + homepage = http://www.cl.cam.ac.uk/~jrh13/hol-light/; + license = licenses.bsd2; + platforms = platforms.unix; + maintainers = with maintainers; [ thoughtpolice z77z vbgl ]; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/iprover/default.nix b/nixpkgs/pkgs/applications/science/logic/iprover/default.nix new file mode 100644 index 000000000000..85fe52239ad9 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/iprover/default.nix @@ -0,0 +1,33 @@ +{ stdenv, fetchurl, ocaml, eprover, zlib }: + +stdenv.mkDerivation rec { + pname = "iprover"; + version = "2018_Jul_24_11h"; + + src = fetchurl { + url = "http://www.cs.man.ac.uk/~korovink/iprover/iprover_${version}.tar.gz"; + sha256 = "1iqim11flzm56aaysasl5whajcv1gq31hkidaqfr8ww7kwl1h06p"; + }; + + buildInputs = [ ocaml eprover zlib ]; + + preConfigure = ''patchShebangs .''; + + installPhase = '' + mkdir -p "$out/bin" + cp iproveropt "$out/bin" + + mkdir -p "$out/share/${pname}-${version}" + cp *.p "$out/share/${pname}-${version}" + echo -e "#! ${stdenv.shell}\\n$out/bin/iproveropt --clausifier \"${eprover}/bin/eprover\" --clausifier_options \" --tstp-format --silent --cnf \" \"\$@\"" > "$out"/bin/iprover + chmod a+x "$out"/bin/iprover + ''; + + meta = with stdenv.lib; { + description = "An automated first-order logic theorem prover"; + homepage = http://www.cs.man.ac.uk/~korovink/iprover/; + maintainers = with maintainers; [ raskin gebner ]; + platforms = platforms.linux; + license = licenses.gpl3; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/isabelle/default.nix b/nixpkgs/pkgs/applications/science/logic/isabelle/default.nix new file mode 100644 index 000000000000..024f2f4e8294 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/isabelle/default.nix @@ -0,0 +1,82 @@ +{ stdenv, fetchurl, perl, nettools, java, polyml, z3, rlwrap }: +# nettools needed for hostname + +stdenv.mkDerivation rec { + pname = "isabelle"; + version = "2018"; + + dirname = "Isabelle${version}"; + + src = if stdenv.isDarwin + then fetchurl { + url = "http://isabelle.in.tum.de/website-${dirname}/dist/${dirname}.dmg"; + sha256 = "0jwnvsf5whklq14ihaxs7b9nbic94mm56nvxljrdbvl6y628j9r5"; + } + else fetchurl { + url = "https://isabelle.in.tum.de/website-${dirname}/dist/${dirname}_linux.tar.gz"; + sha256 = "1928lwrw1v1p9s23kix30ncpqm8djmrnjixj82f3ni2a8sc3hrsp"; + }; + + buildInputs = [ perl polyml z3 ] + ++ stdenv.lib.optionals (!stdenv.isDarwin) [ nettools java ]; + + sourceRoot = dirname; + + postPatch = '' + patchShebangs . + + cat >contrib/z3*/etc/settings <<EOF + Z3_HOME=${z3} + Z3_VERSION=${z3.version} + Z3_SOLVER=${z3}/bin/z3 + Z3_INSTALLED=yes + EOF + + cat >contrib/polyml-*/etc/settings <<EOF + ML_SYSTEM_64=true + ML_SYSTEM=${polyml.name} + ML_PLATFORM=${stdenv.system} + ML_HOME=${polyml}/bin + ML_OPTIONS="--minheap 1000" + POLYML_HOME="\$COMPONENT" + ML_SOURCES="\$POLYML_HOME/src" + EOF + + cat >contrib/jdk/etc/settings <<EOF + ISABELLE_JAVA_PLATFORM=${stdenv.system} + ISABELLE_JDK_HOME=${java} + EOF + + echo ISABELLE_LINE_EDITOR=${rlwrap}/bin/rlwrap >>etc/settings + + for comp in contrib/jdk contrib/polyml-* contrib/z3-*; do + rm -rf $comp/x86* + done + '' + (if ! stdenv.isLinux then "" else '' + arch=${if stdenv.hostPlatform.system == "x86_64-linux" then "x86_64-linux" else "x86-linux"} + for f in contrib/*/$arch/{bash_process,epclextract,eprover,nunchaku,SPASS}; do + patchelf --set-interpreter $(cat ${stdenv.cc}/nix-support/dynamic-linker) "$f" + done + ''); + + installPhase = '' + mkdir -p $out/bin + mv $TMP/$dirname $out + cd $out/$dirname + bin/isabelle install $out/bin + ''; + + meta = { + description = "A generic proof assistant"; + + longDescription = '' + Isabelle is a generic proof assistant. It allows mathematical formulas + to be expressed in a formal language and provides tools for proving those + formulas in a logical calculus. + ''; + homepage = http://isabelle.in.tum.de/; + license = "LGPL"; + maintainers = [ stdenv.lib.maintainers.jwiegley ]; + platforms = stdenv.lib.platforms.linux; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/jonprl/default.nix b/nixpkgs/pkgs/applications/science/logic/jonprl/default.nix new file mode 100644 index 000000000000..61ca78d85ed1 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/jonprl/default.nix @@ -0,0 +1,34 @@ +{ fetchgit, stdenv, smlnj, which }: + +stdenv.mkDerivation rec { + pname = "jonprl"; + version = "0.1.0"; + + src = fetchgit { + url = "https://github.com/jonsterling/JonPRL.git"; + deepClone = true; + rev = "refs/tags/v${version}"; + sha256 = "0czs13syvnw8fz24d075n4pmsyfs8rs8c7ksmvd7cgb3h55fvp4p"; + }; + + buildInputs = [ smlnj which ]; + + installPhase = '' + mkdir -p "$out/bin" + cp bin/.heapimg.* "$out/bin/" + build/mkexec.sh "${smlnj}/bin/sml" "$out" jonprl + ''; + + meta = { + description = "Proof Refinement Logic - Computational Type Theory"; + longDescription = '' + An proof refinement logic for computational type theory + based on Brouwer-realizability & meaning explanations. + 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; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/lci/default.nix b/nixpkgs/pkgs/applications/science/logic/lci/default.nix new file mode 100644 index 000000000000..4775384a3ddc --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/lci/default.nix @@ -0,0 +1,16 @@ +{stdenv, fetchurl, readline}: +stdenv.mkDerivation rec { + version = "0.6"; + pname = "lci"; + src = fetchurl { + url = "mirror://sourceforge/lci/${pname}-${version}.tar.gz"; + sha256="204f1ca5e2f56247d71ab320246811c220ed511bf08c9cb7f305cf180a93948e"; + }; + buildInputs = [readline]; + meta = { + description = ''Lambda calculus interpreter''; + maintainers = with stdenv.lib.maintainers; [raskin]; + platforms = with stdenv.lib.platforms; linux; + license = stdenv.lib.licenses.gpl3; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/lean/default.nix b/nixpkgs/pkgs/applications/science/logic/lean/default.nix new file mode 100644 index 000000000000..9bf54a5f0940 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/lean/default.nix @@ -0,0 +1,29 @@ +{ stdenv, fetchFromGitHub, cmake, gmp }: + +stdenv.mkDerivation rec { + pname = "lean"; + version = "3.4.2"; + + src = fetchFromGitHub { + owner = "leanprover"; + repo = "lean"; + rev = "v${version}"; + sha256 = "0zpnfg6kyg120rrdr336i1lymmzz4xgcqpn96iavhzhlaanmx55l"; + }; + + nativeBuildInputs = [ cmake ]; + buildInputs = [ gmp ]; + enableParallelBuilding = true; + + preConfigure = '' + cd src + ''; + + meta = with stdenv.lib; { + description = "Automatic and interactive theorem prover"; + homepage = https://leanprover.github.io/; + license = licenses.asl20; + platforms = platforms.unix; + maintainers = with maintainers; [ thoughtpolice gebner ]; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/lean2/default.nix b/nixpkgs/pkgs/applications/science/logic/lean2/default.nix new file mode 100644 index 000000000000..8cc50bb5e295 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/lean2/default.nix @@ -0,0 +1,36 @@ +{ stdenv, fetchFromGitHub, cmake, gmp, mpfr, python +, gperftools, ninja, makeWrapper }: + +stdenv.mkDerivation { + pname = "lean2"; + version = "2017-07-22"; + + src = fetchFromGitHub { + owner = "leanprover"; + repo = "lean2"; + rev = "34dbd6c3ae612186b8f0f80d12fbf5ae7a059ec9"; + sha256 = "1xv3j487zhh1zf2b4v19xzw63s2sgjhg8d62a0kxxyknfmdf3khl"; + }; + + buildInputs = [ gmp mpfr cmake python gperftools ninja makeWrapper ]; + enableParallelBuilding = true; + + preConfigure = '' + patchShebangs bin/leantags + cd src + ''; + + cmakeFlags = [ "-GNinja" ]; + + postInstall = '' + wrapProgram $out/bin/linja --prefix PATH : $out/bin:${ninja}/bin + ''; + + meta = with stdenv.lib; { + description = "Automatic and interactive theorem prover (version with HoTT support)"; + homepage = "http://leanprover.github.io"; + license = licenses.asl20; + platforms = platforms.unix; + maintainers = with maintainers; [ thoughtpolice gebner ]; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/leo2/default.nix b/nixpkgs/pkgs/applications/science/logic/leo2/default.nix new file mode 100644 index 000000000000..b50848a18205 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/leo2/default.nix @@ -0,0 +1,37 @@ +{ stdenv, fetchurl, makeWrapper, eprover, ocaml, perl, zlib }: + +stdenv.mkDerivation rec { + pname = "leo2"; + version = "1.6.2"; + + src = fetchurl { + url = "https://page.mi.fu-berlin.de/cbenzmueller/leo/leo2_v${version}.tgz"; + sha256 = "1wjpmizb181iygnd18lx7p77fwaci2clgzs5ix5j51cc8f3pazmv"; + }; + + buildInputs = [ makeWrapper eprover ocaml perl zlib ]; + + sourceRoot = "leo2/src"; + + preConfigure = "patchShebangs configure"; + + buildFlags = [ "opt" ]; + + preInstall = "mkdir -p $out/bin"; + + postInstall = '' + mkdir -p "$out/etc" + echo -e "e = ${eprover}/bin/eprover\\nepclextract = ${eprover}/bin/epclextract" > "$out/etc/leoatprc" + + wrapProgram $out/bin/leo \ + --add-flags "--atprc $out/etc/leoatprc" + ''; + + meta = with stdenv.lib; { + description = "A high-performance typed higher order prover"; + maintainers = [ maintainers.raskin ]; + platforms = platforms.linux; + license = licenses.bsd3; + homepage = http://www.leoprover.org/; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/leo2/default.upstream b/nixpkgs/pkgs/applications/science/logic/leo2/default.upstream new file mode 100644 index 000000000000..52b8ed1cdaa2 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/leo2/default.upstream @@ -0,0 +1,6 @@ +url http://page.mi.fu-berlin.de/cbenzmueller/leo/download.html +version_link '[.]tgz' +version '.*_v([0-9.]+)[.][a-z0-9]+$' '\1' +do_overwrite () { + do_overwrite_just_version +} diff --git a/nixpkgs/pkgs/applications/science/logic/leo3/binary.nix b/nixpkgs/pkgs/applications/science/logic/leo3/binary.nix new file mode 100644 index 000000000000..dcea9c27acb4 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/leo3/binary.nix @@ -0,0 +1,29 @@ +{stdenv, fetchurl, openjdk, runtimeShell}: +stdenv.mkDerivation rec { + pname = "leo3"; + version = "1.2"; + + jar = fetchurl { + url = "https://github.com/leoprover/Leo-III/releases/download/v${version}/leo3.jar"; + sha256 = "1lgwxbr1rnk72rnvc8raq5i1q71ckhn998pwd9xk6zf27wlzijk7"; + }; + + phases=["installPhase" "fixupPhase"]; + + installPhase = '' + mkdir -p "$out"/{bin,lib/java/leo3} + cp "${jar}" "$out/lib/java/leo3/leo3.jar" + echo "#!${runtimeShell}" > "$out/bin/leo3" + echo "'${openjdk}/bin/java' -jar '$out/lib/java/leo3/leo3.jar' \"\$@\"" > "$out/bin/leo3" + chmod a+x "$out/bin/leo3" + ''; + + 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; + 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 new file mode 100644 index 000000000000..287dbd36eabf --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/lingeling/default.nix @@ -0,0 +1,49 @@ +{ stdenv, fetchFromGitHub +, aiger +}: + +stdenv.mkDerivation { + pname = "lingeling"; + # This is the version used in satcomp2018, which was + # relicensed, and also known as version 'bcj' + version = "pre1_03b4860d"; + + src = fetchFromGitHub { + owner = "arminbiere"; + repo = "lingeling"; + rev = "03b4860d14016f42213ea271014f2f13d181f504"; + sha256 = "1lw1yfy219p7rrk88sbq4zl24b70040zapbjdrpv5a6i0jsblksx"; + }; + + configurePhase = '' + ./configure.sh + + # Rather than patch ./configure, just sneak in use of aiger here, since it + # doesn't handle real build products very well (it works on a build-time + # dir, not installed copy)... This is so we can build 'blimc' + substituteInPlace ./makefile \ + --replace 'targets: liblgl.a' 'targets: liblgl.a blimc' \ + --replace '$(AIGER)/aiger.o' '${aiger.lib}/lib/aiger.o' \ + --replace '$(AIGER)/aiger.h' '${aiger.dev}/include/aiger.h' \ + --replace '-I$(AIGER)' '-I${aiger.dev}/include' + ''; + + installPhase = '' + mkdir -p $out/bin $lib/lib $dev/include + + cp lglib.h $dev/include + cp liblgl.a $lib/lib + + cp lingeling plingeling treengeling ilingeling blimc $out/bin + ''; + + outputs = [ "out" "dev" "lib" ]; + + meta = with stdenv.lib; { + description = "Fast SAT solver"; + homepage = http://fmv.jku.at/lingeling/; + license = licenses.mit; + platforms = platforms.linux; + maintainers = with maintainers; [ thoughtpolice ]; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/logisim/default.nix b/nixpkgs/pkgs/applications/science/logic/logisim/default.nix new file mode 100644 index 000000000000..d6a1207b5d60 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/logisim/default.nix @@ -0,0 +1,29 @@ +{ 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]; + + installPhase = '' + 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; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/ltl2ba/default.nix b/nixpkgs/pkgs/applications/science/logic/ltl2ba/default.nix new file mode 100644 index 000000000000..02e9844115ef --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/ltl2ba/default.nix @@ -0,0 +1,31 @@ +{ fetchurl, stdenv }: + +stdenv.mkDerivation rec { + pname = "ltl2ba"; + version = "1.2"; + + src = fetchurl { + url = "http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/${pname}-${version}.tar.gz"; + sha256 = "0vzv5g7v87r41cvdafxi6yqnk7glzxrzgavy8213k59f6v11dzlx"; + }; + + hardeningDisable = [ "format" ]; + + preConfigure = '' + substituteInPlace Makefile \ + --replace "CC=gcc" "" + ''; + + installPhase = '' + mkdir -p $out/bin + mv ltl2ba $out/bin + ''; + + 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 ]; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/mcrl2/default.nix b/nixpkgs/pkgs/applications/science/logic/mcrl2/default.nix new file mode 100644 index 000000000000..93212c5b8546 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/mcrl2/default.nix @@ -0,0 +1,29 @@ +{stdenv, fetchurl, cmake, libGLU_combined, qt5, boost}: + +stdenv.mkDerivation rec { + version = "201707"; + build_nr = "1"; + pname = "mcrl2"; + + src = fetchurl { + url = "https://www.mcrl2.org/download/release/mcrl2-${version}.${build_nr}.tar.gz"; + sha256 = "1c8h94ja7271ph61zrcgnjgblxppld6v22f7f900prjgzbcfy14m"; + }; + + buildInputs = [ cmake libGLU_combined qt5.qtbase boost ]; + + enableParallelBuilding = true; + + meta = with stdenv.lib; { + description = "A toolset for model-checking concurrent systems and protocols"; + longDescription = '' + A formal specification language with an associated toolset, + that can be used for modelling, validation and verification of + concurrent systems and protocols + ''; + homepage = https://www.mcrl2.org/; + license = licenses.boost; + maintainers = with maintainers; [ moretea ]; + platforms = platforms.unix; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/metis-prover/default.nix b/nixpkgs/pkgs/applications/science/logic/metis-prover/default.nix new file mode 100644 index 000000000000..ed1218c401b3 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/metis-prover/default.nix @@ -0,0 +1,32 @@ +{ stdenv, fetchFromGitHub, perl, mlton }: + +stdenv.mkDerivation { + pname = "metis-prover"; + version = "2.3.20160713"; + + src = fetchFromGitHub { + owner = "gilith"; + repo = "metis"; + rev = "f0b1a17cd57eb098077e963ab092477aee9fb340"; + sha256 = "1i7paax7b4byk8110f5zk4071mh5603r82bq7hbprqzljvsiipk7"; + }; + + nativeBuildInputs = [ perl ]; + buildInputs = [ mlton ]; + + patchPhase = "patchShebangs ."; + + buildPhase = "make mlton"; + + installPhase = '' + install -Dm0755 bin/mlton/metis $out/bin/metis + ''; + + meta = with stdenv.lib; { + description = "Automatic theorem prover for first-order logic with equality"; + homepage = http://www.gilith.com/research/metis/; + license = licenses.mit; + maintainers = with maintainers; [ gebner ]; + platforms = platforms.unix; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/minisat/clang.diff b/nixpkgs/pkgs/applications/science/logic/minisat/clang.diff new file mode 100644 index 000000000000..5b5072c71f3f --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/minisat/clang.diff @@ -0,0 +1,45 @@ +diff -aur minisat/core/SolverTypes.h minisat.clang/core/SolverTypes.h +--- minisat/core/SolverTypes.h 2010-07-10 18:07:36.000000000 +0200 ++++ minisat.clang/core/SolverTypes.h 2016-05-13 12:14:50.759671959 +0200 +@@ -47,7 +47,7 @@ + int x; + + // Use this as a constructor: +- friend Lit mkLit(Var var, bool sign = false); ++ //friend Lit mkLit(Var var, bool sign = false); + + bool operator == (Lit p) const { return x == p.x; } + bool operator != (Lit p) const { return x != p.x; } +@@ -55,7 +55,7 @@ + }; + + +-inline Lit mkLit (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; } ++inline Lit mkLit (Var var, bool sign = false) { Lit p; p.x = var + var + (int)sign; return p; } + inline Lit operator ~(Lit p) { Lit q; q.x = p.x ^ 1; return q; } + inline Lit operator ^(Lit p, bool b) { Lit q; q.x = p.x ^ (unsigned int)b; return q; } + inline bool sign (Lit p) { return p.x & 1; } +diff -aur minisat/utils/Options.h minisat.clang/utils/Options.h +--- minisat/utils/Options.h 2010-07-10 18:07:36.000000000 +0200 ++++ minisat.clang/utils/Options.h 2016-05-13 12:14:50.759671959 +0200 +@@ -282,15 +282,15 @@ + if (range.begin == INT64_MIN) + fprintf(stderr, "imin"); + else +- fprintf(stderr, "%4"PRIi64, range.begin); ++ fprintf(stderr, "%4" PRIi64, range.begin); + + fprintf(stderr, " .. "); + if (range.end == INT64_MAX) + fprintf(stderr, "imax"); + else +- fprintf(stderr, "%4"PRIi64, range.end); ++ fprintf(stderr, "%4" PRIi64, range.end); + +- fprintf(stderr, "] (default: %"PRIi64")\n", value); ++ fprintf(stderr, "] (default: %" PRIi64 ")\n", value); + if (verbose){ + fprintf(stderr, "\n %s\n", description); + fprintf(stderr, "\n"); +Only in minisat.clang/utils: Options.o +Only in minisat.clang/utils: System.o diff --git a/nixpkgs/pkgs/applications/science/logic/minisat/darwin.patch b/nixpkgs/pkgs/applications/science/logic/minisat/darwin.patch new file mode 100644 index 000000000000..f2b618d6bb3a --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/minisat/darwin.patch @@ -0,0 +1,26 @@ +https://github.com/fasterthanlime/homebrew-mingw/blob/master/Library/Formula/minisat.rb + +diff --git a/utils/System.cc b/utils/System.cc +index a7cf53f..feeaf3c 100644 +--- a/utils/System.cc ++++ b/utils/System.cc +@@ -78,16 +78,17 @@ double Minisat::memUsed(void) { + struct rusage ru; + getrusage(RUSAGE_SELF, &ru); + return (double)ru.ru_maxrss / 1024; } +-double MiniSat::memUsedPeak(void) { return memUsed(); } ++double Minisat::memUsedPeak(void) { return memUsed(); } + + + #elif defined(__APPLE__) + #include <malloc/malloc.h> + +-double Minisat::memUsed(void) { ++double Minisat::memUsed() { + malloc_statistics_t t; + malloc_zone_statistics(NULL, &t); + return (double)t.max_size_in_use / (1024*1024); } ++double Minisat::memUsedPeak() { return memUsed(); } + + #else + double Minisat::memUsed() { diff --git a/nixpkgs/pkgs/applications/science/logic/minisat/default.nix b/nixpkgs/pkgs/applications/science/logic/minisat/default.nix new file mode 100644 index 000000000000..34051a1da404 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/minisat/default.nix @@ -0,0 +1,32 @@ +{ stdenv, fetchurl, zlib }: + +stdenv.mkDerivation rec { + pname = "minisat"; + version = "2.2.0"; + + src = fetchurl { + url = "http://minisat.se/downloads/${pname}-${version}.tar.gz"; + sha256 = "023qdnsb6i18yrrawlhckm47q8x0sl7chpvvw3gssfyw3j2pv5cj"; + }; + + patches = + [ ./darwin.patch ] + ++ stdenv.lib.optionals stdenv.cc.isClang [ ./clang.diff ]; + + buildInputs = [ zlib ]; + + preBuild = "cd simp"; + makeFlags = [ "r" "MROOT=.." ]; + installPhase = '' + mkdir -p $out/bin + cp minisat_release $out/bin/minisat + ''; + + meta = with stdenv.lib; { + description = "Compact and readable SAT solver"; + maintainers = with maintainers; [ gebner raskin ]; + platforms = platforms.unix; + license = licenses.mit; + homepage = http://minisat.se/; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/minisat/unstable.nix b/nixpkgs/pkgs/applications/science/logic/minisat/unstable.nix new file mode 100644 index 000000000000..ef46c694acb7 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/minisat/unstable.nix @@ -0,0 +1,23 @@ +{ stdenv, fetchFromGitHub, zlib, cmake }: + +stdenv.mkDerivation { + name = "minisat-unstable-2013-09-25"; + + src = fetchFromGitHub { + owner = "niklasso"; + repo = "minisat"; + rev = "37dc6c67e2af26379d88ce349eb9c4c6160e8543"; + sha256 = "091hf3qkm197s5r7xcr3m07xsdwyz2rqk1hc9kj0hn13imz09irq"; + }; + + buildInputs = [ zlib ]; + nativeBuildInputs = [ cmake ]; + + meta = with stdenv.lib; { + description = "Compact and readable SAT solver"; + maintainers = with maintainers; [ mic92 ]; + platforms = platforms.unix; + license = licenses.mit; + homepage = http://minisat.se/; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/monosat/default.nix b/nixpkgs/pkgs/applications/science/logic/monosat/default.nix new file mode 100644 index 000000000000..30d47687a3eb --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/monosat/default.nix @@ -0,0 +1,67 @@ +{ stdenv, 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; + +let + boolToCmake = x: if x then "ON" else "OFF"; + + rev = "2deeadeff214e975c9f7508bc8a24fa05a1a0c32"; + sha256 = "09yhym2lxmn3xbhw5fcxawnmvms5jd9fw9m7x2wzil7yvy4vwdjn"; + + pname = "monosat"; + version = substring 0 7 sha256; + + src = fetchFromGitHub { + owner = "sambayless"; + repo = pname; + inherit rev sha256; + }; + + core = stdenv.mkDerivation { + name = "${pname}-${version}"; + inherit src; + buildInputs = [ cmake zlib gmp jdk8 ]; + + cmakeFlags = [ "-DJAVA=${boolToCmake includeJava}" "-DGPL=${boolToCmake includeGplCode}" ]; + + postInstall = optionalString includeJava '' + mkdir -p $out/share/java + cp monosat.jar $out/share/java + ''; + + passthru = { inherit python; }; + + meta = { + description = "SMT solver for Monotonic Theories"; + platforms = platforms.unix; + license = if includeGplCode then licenses.gpl2 else licenses.mit; + homepage = https://github.com/sambayless/monosat; + }; + }; + + python = { buildPythonPackage, cython }: buildPythonPackage { + inherit pname version src; + + # The top-level "source" is what fetchFromGitHub gives us. The rest is inside the repo + sourceRoot = "source/src/monosat/api/python/"; + + propagatedBuildInputs = [ core cython ]; + + # This tells setup.py to use cython + MONOSAT_CYTHON = true; + + # The relative paths here don't make sense for our Nix build + # Also, let's use cython since it should produce faster bindings + # TODO: do we want to just reference the core monosat library rather than copying the + # shared lib? The current setup.py copies the .dylib/.so... + postPatch = '' + + substituteInPlace setup.py \ + --replace '../../../../libmonosat.dylib' '${core}/lib/libmonosat.dylib' \ + --replace '../../../../libmonosat.so' '${core}/lib/libmonosat.so' + ''; + }; +in core \ No newline at end of file diff --git a/nixpkgs/pkgs/applications/science/logic/open-wbo/default.nix b/nixpkgs/pkgs/applications/science/logic/open-wbo/default.nix new file mode 100644 index 000000000000..32ce9fde0c31 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/open-wbo/default.nix @@ -0,0 +1,27 @@ +{ stdenv, fetchFromGitHub, zlib, gmp }: + +stdenv.mkDerivation { + name = "open-wbo-2.0"; + + src = fetchFromGitHub { + owner = "sat-group"; + repo = "open-wbo"; + rev = "f193a3bd802551b13d6424bc1baba6ad35ec6ba6"; + sha256 = "1742i15qfsbf49c4r837wz35c1p7yafvz7ar6vmgcj6cmfwr8jb4"; + }; + + buildInputs = [ zlib gmp ]; + + makeFlags = [ "r" ]; + installPhase = '' + install -Dm0755 open-wbo_release $out/bin/open-wbo + ''; + + meta = with stdenv.lib; { + description = "State-of-the-art MaxSAT and Pseudo-Boolean solver"; + maintainers = with maintainers; [ gebner ]; + platforms = platforms.unix; + license = licenses.mit; + homepage = http://sat.inesc-id.pt/open-wbo/; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/opensmt/default.nix b/nixpkgs/pkgs/applications/science/logic/opensmt/default.nix new file mode 100644 index 000000000000..9e5ebe008b8f --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/opensmt/default.nix @@ -0,0 +1,25 @@ +{ stdenv, fetchurl, automake, libtool, autoconf, intltool, perl +, gmpxx, flex, bison +}: + +stdenv.mkDerivation rec { + pname = "opensmt"; + version = "20101017"; + + src = fetchurl { + url = "http://opensmt.googlecode.com/files/opensmt_src_${version}.tgz"; + sha256 = "0xrky7ixjaby5x026v7hn72xh7d401w9jhccxjn0khhn1x87p2w1"; + }; + + buildInputs = [ automake libtool autoconf intltool perl gmpxx flex bison ]; + + meta = with stdenv.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"; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/ott/default.nix b/nixpkgs/pkgs/applications/science/logic/ott/default.nix new file mode 100644 index 000000000000..40c66dd699d8 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/ott/default.nix @@ -0,0 +1,44 @@ +{ stdenv, fetchFromGitHub, pkgconfig, ocaml }: + +stdenv.mkDerivation rec { + pname = "ott"; + version = "0.28"; + + src = fetchFromGitHub { + owner = "ott-lang"; + repo = "ott"; + rev = version; + sha256 = "0mzbrvqayqpns9zzg4m1scxx24dv9askhn51dawyb9pisvlyvai0"; + }; + + nativeBuildInputs = [ pkgconfig ]; + buildInputs = [ ocaml ]; + + installPhase = '' + mkdir -p $out/bin + cp src/ott.opt $out/bin + ln -s $out/bin/ott.opt $out/bin/ott + + mkdir -p $out/share/emacs/site-lisp + cp emacs/ott-mode.el $out/share/emacs/site-lisp + ''; + + meta = { + description = "Ott: tool for the working semanticist"; + longDescription = '' + Ott is a tool for writing definitions of programming languages and + calculi. It takes as input a definition of a language syntax and + semantics, in a concise and readable ASCII notation that is close to + what one would write in informal mathematics. It generates LaTeX to + build a typeset version of the definition, and Coq, HOL, and Isabelle + versions of the definition. Additionally, it can be run as a filter, + taking a LaTeX/Coq/Isabelle/HOL source file with embedded (symbolic) + terms of the defined language, parsing them and replacing them by + 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; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/otter/default.nix b/nixpkgs/pkgs/applications/science/logic/otter/default.nix new file mode 100644 index 000000000000..a7eec20548c9 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/otter/default.nix @@ -0,0 +1,53 @@ +{stdenv, fetchurl, tcsh, libXaw, libXt, libX11}: +let + s = # Generated upstream information + rec { + version = "3.3f"; + name = "otter"; + url = "https://www.cs.unm.edu/~mccune/otter/otter-${version}.tar.gz"; + sha256 = "16mc1npl7sk9cmqhrf3ghfmvx29inijw76f1b1lsykllaxjqqb1r"; + }; + buildInputs = [ + tcsh libXaw libXt libX11 + ]; +in +stdenv.mkDerivation { + name = "${s.name}-${s.version}"; + inherit buildInputs; + src = fetchurl { + inherit (s) url sha256; + }; + + hardeningDisable = [ "format" ]; + + buildPhase = '' + find . -name Makefile | xargs sed -i -e "s@/bin/rm@$(type -P rm)@g" + find . -name Makefile | xargs sed -i -e "s@/bin/mv@$(type -P mv)@g" + find . -perm -0100 -type f | xargs sed -i -e "s@/bin/csh@$(type -P csh)@g" + 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 + + make all + make -C examples all + make -C examples-mace2 all + make -C source/formed realclean + make -C source/formed formed + ''; + + installPhase = '' + mkdir -p "$out"/{bin,share/otter} + cp bin/* source/formed/formed "$out/bin/" + cp -r examples examples-mace2 documents README* Legal Changelog Contents index.html "$out/share/otter/" + ''; + + 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; + broken = true; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/petrinizer/default.nix b/nixpkgs/pkgs/applications/science/logic/petrinizer/default.nix new file mode 100644 index 000000000000..d277e0e1521a --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/petrinizer/default.nix @@ -0,0 +1,31 @@ +{ mkDerivation, callPackage, buildPackages +, async, base, bytestring, containers, fetchFromGitLab, mtl +, parallel-io, parsec, stdenv, stm, transformers +}: +let + z3 = callPackage ./z3.nix { gomp = null; z3 = buildPackages.z3; }; +in let + sbv = callPackage ./sbv-7.13.nix { inherit z3; }; +in +mkDerivation rec { + pname = "petrinizer"; + version = "0.9.1.1"; + + src = fetchFromGitLab { + domain = "gitlab.lrz.de"; + owner = "i7"; + repo = pname; + rev = version; + sha256 = "1n7fzm96gq5rxm2f8w8sr1yzm1zcxpf0b473c6xnhsgqsis5j4xw"; + }; + + isLibrary = false; + isExecutable = true; + executableHaskellDepends = [ + async base bytestring containers mtl parallel-io parsec sbv stm + transformers + ]; + description = "Safety and Liveness Analysis of Petri Nets with SMT solvers"; + license = stdenv.lib.licenses.gpl3; + maintainers = with stdenv.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 new file mode 100644 index 000000000000..ed10e9f3db19 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/petrinizer/sbv-7.13.nix @@ -0,0 +1,26 @@ +{ 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 +, template-haskell, time, z3 +}: +mkDerivation { + pname = "sbv"; + version = "7.13"; + sha256 = "0bk400swnb4s98c5p71ml1px6jndaiqhf5dj7zmnliyplqcgpfik"; + enableSeparateDataOutput = true; + libraryHaskellDepends = [ + array async base containers crackNum deepseq directory filepath + generic-deriving ghc mtl pretty process QuickCheck random syb + template-haskell time + ]; + testHaskellDepends = [ + base bytestring containers crackNum directory doctest filepath Glob + hlint mtl QuickCheck random syb tasty tasty-golden tasty-hunit + tasty-quickcheck template-haskell + ]; + testSystemDepends = [ z3 ]; + homepage = "http://leventerkok.github.com/sbv/"; + description = "SMT Based Verification: Symbolic Haskell theorem prover using SMT solving"; + license = stdenv.lib.licenses.bsd3; +} diff --git a/nixpkgs/pkgs/applications/science/logic/petrinizer/z3.nix b/nixpkgs/pkgs/applications/science/logic/petrinizer/z3.nix new file mode 100644 index 000000000000..4d868054c09b --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/petrinizer/z3.nix @@ -0,0 +1,24 @@ +{ mkDerivation, fetchpatch +, base, containers, gomp, hspec, QuickCheck, stdenv +, transformers, z3 +}: +mkDerivation { + pname = "z3"; + version = "408.0"; + sha256 = "13qkzy9wc17rm60i24fa9sx15ywbxq4a80g33w20887gvqyc0q53"; + isLibrary = true; + isExecutable = true; + libraryHaskellDepends = [ base containers transformers ]; + librarySystemDepends = [ gomp z3 ]; + testHaskellDepends = [ base hspec QuickCheck ]; + homepage = "https://github.com/IagoAbal/haskell-z3"; + description = "Bindings for the Z3 Theorem Prover"; + license = stdenv.lib.licenses.bsd3; + doCheck = false; + patches = [ + (fetchpatch { + url = "https://github.com/IagoAbal/haskell-z3/commit/b10e09b8a809fb5bbbb1ef86aeb62109ece99cae.patch"; + sha256 = "13fnrs27mg3985r3lwks8fxfxr5inrayy2cyx2867d92pnl3yry4"; + }) + ]; +} diff --git a/nixpkgs/pkgs/applications/science/logic/picosat/default.nix b/nixpkgs/pkgs/applications/science/logic/picosat/default.nix new file mode 100644 index 000000000000..547bd31e8b42 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/picosat/default.nix @@ -0,0 +1,44 @@ +{ stdenv, fetchurl }: + +stdenv.mkDerivation rec { + pname = "picosat"; + version = "965"; + + src = fetchurl { + url = "http://fmv.jku.at/picosat/${pname}-${version}.tar.gz"; + sha256 = "0m578rpa5rdn08d10kr4lbsdwp4402hpavrz6n7n53xs517rn5hm"; + }; + + prePatch = '' + substituteInPlace picosat.c --replace "sys/unistd.h" "unistd.h" + + substituteInPlace makefile.in \ + --replace 'ar rc' '$(AR) rc' \ + --replace 'ranlib' '$(RANLIB)' + ''; + + configurePhase = "./configure.sh --shared --trace"; + + makeFlags = stdenv.lib.optional stdenv.isDarwin + "SONAME=-Wl,-install_name,$(out)/lib/libpicosat.so"; + + installPhase = '' + mkdir -p $out/bin $out/lib $out/share $out/include/picosat + cp picomus picomcs picosat picogcnf "$out"/bin + + cp VERSION "$out"/share/picosat.version + cp picosat.o "$out"/lib + cp libpicosat.a "$out"/lib + cp libpicosat.so "$out"/lib + + cp picosat.h "$out"/include/picosat + ''; + + 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 ]; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/poly/default.nix b/nixpkgs/pkgs/applications/science/logic/poly/default.nix new file mode 100644 index 000000000000..c833b22e49b6 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/poly/default.nix @@ -0,0 +1,24 @@ +{stdenv, fetchFromGitHub, gmp, cmake, python}: + +stdenv.mkDerivation rec { + pname = "libpoly"; + version = "0.1.7"; + + src = fetchFromGitHub { + owner = "SRI-CSL"; + repo = "libpoly"; + rev = "v${version}"; + sha256 = "0i5ar4lhs88glk0rvkmag656ii434i6i1q5dspx6d0kyg78fii64"; + }; + + nativeBuildInputs = [ cmake ]; + + buildInputs = [ gmp python ]; + + meta = with stdenv.lib; { + homepage = https://github.com/SRI-CSL/libpoly; + description = "C library for manipulating polynomials"; + license = licenses.lgpl3; + platforms = platforms.all; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/potassco/clingo.nix b/nixpkgs/pkgs/applications/science/logic/potassco/clingo.nix new file mode 100644 index 000000000000..2b368a0e6730 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/potassco/clingo.nix @@ -0,0 +1,26 @@ +{ stdenv, fetchzip, cmake }: + +stdenv.mkDerivation rec { + pname = "clingo"; + version = "5.3.0"; + + src = fetchzip { + url = "https://github.com/potassco/clingo/archive/v${version}.tar.gz"; + sha256 = "01czx26p8gv81ahrh650x208hjhd8bx1kb688fmk1m4pw4yg5bfv"; + }; + + buildInputs = []; + nativeBuildInputs = [cmake]; + + cmakeFlags = [ "-DCLINGO_BUILD_WITH_PYTHON=OFF" ]; + + 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; + homepage = "https://potassco.org/"; + downloadPage = "https://github.com/potassco/clingo/releases/"; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/potassco/clingo.upstream b/nixpkgs/pkgs/applications/science/logic/potassco/clingo.upstream new file mode 100644 index 000000000000..062577d1451b --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/potassco/clingo.upstream @@ -0,0 +1,6 @@ +target clingo.nix +attribute_name clingo +url https://github.com/potassco/clingo/releases/ +ensure_choice +version '.*/v([0-9.]+)[.]tar[.].*' '\1' +minimize_overwrite diff --git a/nixpkgs/pkgs/applications/science/logic/prooftree/default.nix b/nixpkgs/pkgs/applications/science/logic/prooftree/default.nix new file mode 100644 index 000000000000..d4feb5c9e285 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/prooftree/default.nix @@ -0,0 +1,43 @@ +{ stdenv, fetchurl, pkgconfig, ncurses, ocamlPackages }: + +stdenv.mkDerivation rec { + pname = "prooftree"; + version = "0.13"; + + src = fetchurl { + url = "https://askra.de/software/prooftree/releases/prooftree-${version}.tar.gz"; + sha256 = "0z1z4wqbqwgppkh2bm89fgy07a0y2m6g4lvcyzs09sm1ysklk2dh"; + }; + + nativeBuildInputs = [ pkgconfig ]; + buildInputs = [ ncurses ] ++ (with ocamlPackages; [ + ocaml findlib camlp5 lablgtk ]); + + dontAddPrefix = true; + configureFlags = [ "--prefix" "$(out)" ]; + + meta = with stdenv.lib; { + description = "A program for proof-tree visualization"; + longDescription = '' + Prooftree is a program for proof-tree visualization during interactive + proof development in a theorem prover. It is currently being developed + for Coq and Proof General. Prooftree helps against getting lost between + different subgoals in interactive proof development. It clearly shows + where the current subgoal comes from and thus helps in developing the + right plan for solving it. + + Prooftree uses different colors for the already proven subgoals, the + current branch in the proof and the still open subgoals. Sequent texts + are not displayed in the proof tree itself, but they are shown as a + tool-tip when the mouse rests over a sequent symbol. Long proof commands + are abbreviated in the tree display, but show up in full length as + tool-tip. Both, sequents and proof commands, can be shown in the display + below the tree (on single click) or in a separate window (on double or + shift-click). + ''; + homepage = http://askra.de/software/prooftree; + platforms = platforms.unix; + maintainers = [ maintainers.jwiegley ]; + license = licenses.gpl3; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/prover9/default.nix b/nixpkgs/pkgs/applications/science/logic/prover9/default.nix new file mode 100644 index 000000000000..a4538e1070a3 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/prover9/default.nix @@ -0,0 +1,45 @@ +{stdenv, fetchurl}: + +stdenv.mkDerivation { + name = "prover9-2009-11a"; + + src = fetchurl { + url = https://www.cs.unm.edu/~mccune/mace4/download/LADR-2009-11A.tar.gz; + sha256 = "1l2i3d3h5z7nnbzilb6z92r0rbx0kh6yaxn2c5qhn3000xcfsay3"; + }; + + hardeningDisable = [ "format" ]; + + patchPhase = '' + RM=$(type -tp rm) + MV=$(type -tp mv) + CP=$(type -tp cp) + for f in Makefile */Makefile; do + substituteInPlace $f --replace "/bin/rm" "$RM" \ + --replace "/bin/mv" "$MV" \ + --replace "/bin/cp" "$CP"; + done + ''; + + buildFlags = "all"; + + checkPhase = "make test1"; + + installPhase = '' + mkdir -p $out/bin + cp bin/* $out/bin + ''; + + meta = { + homepage = https://www.cs.unm.edu/~mccune/mace4/; + license = "GPL"; + description = "Automated theorem prover for first-order and equational logic"; + longDescription = '' + Prover9 is a resolution/paramodulation automated theorem prover + 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; + maintainers = []; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/proverif/default.nix b/nixpkgs/pkgs/applications/science/logic/proverif/default.nix new file mode 100644 index 000000000000..931ad2fc4f39 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/proverif/default.nix @@ -0,0 +1,28 @@ +{ stdenv, fetchurl, ocamlPackages }: + +stdenv.mkDerivation rec { + pname = "proverif"; + version = "2.00"; + + src = fetchurl { + url = "http://prosecco.gforge.inria.fr/personal/bblanche/proverif/proverif${version}.tar.gz"; + sha256 = "0vjphj85ch9q39vc7sd6n4vxy5bplp017vlshk989yhfwb00r37y"; + }; + + buildInputs = with ocamlPackages; [ ocaml findlib lablgtk ]; + + buildPhase = "./build"; + installPhase = '' + mkdir -p $out/bin + cp ./proverif $out/bin + cp ./proveriftotex $out/bin + ''; + + 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 ]; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/redprl/default.nix b/nixpkgs/pkgs/applications/science/logic/redprl/default.nix new file mode 100644 index 000000000000..9da2647d1138 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/redprl/default.nix @@ -0,0 +1,28 @@ +{ stdenv, fetchgit, mlton }: +stdenv.mkDerivation { + name = "redprl-2017-03-28"; + src = fetchgit { + url = "https://github.com/RedPRL/sml-redprl.git"; + rev = "bdf027de732e4a8d10f9f954389dfff0c822f18b"; + sha256 = "0cihwnd78d3ksxp6mppifm7xpi3fsii5mixvicajy87ggw8z305c"; + fetchSubmodules = true; + }; + buildInputs = [ mlton ]; + patchPhase = '' + patchShebangs ./script/ + ''; + buildPhase = '' + ./script/mlton.sh + ''; + installPhase = '' + mkdir -p $out/bin + mv ./bin/redprl $out/bin + ''; + 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; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/sad/default.nix b/nixpkgs/pkgs/applications/science/logic/sad/default.nix new file mode 100644 index 000000000000..8e94356f376a --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/sad/default.nix @@ -0,0 +1,39 @@ +{ stdenv, fetchurl, haskell, spass }: + +stdenv.mkDerivation { + name = "system-for-automated-deduction-2.3.25"; + src = fetchurl { + url = "http://nevidal.org/download/sad-2.3-25.tar.gz"; + sha256 = "10jd93xgarik7xwys5lq7fx4vqp7c0yg1gfin9cqfch1k1v8ap4b"; + }; + buildInputs = [ haskell.compiler.ghc844 spass ]; + patches = [ + ./patch + # Since the LTS 12.0 update, <> is an operator in Prelude, colliding with + # the <> operator with a different meaning defined by this package + ./monoid.patch + ]; + postPatch = '' + substituteInPlace Alice/Main.hs --replace init.opt $out/init.opt + ''; + installPhase = '' + mkdir -p $out/{bin,provers} + install alice $out/bin + install provers/moses $out/provers + substituteAll provers/provers.dat $out/provers/provers.dat + substituteAll init.opt $out/init.opt + cp -r examples $out + ''; + inherit spass; + meta = { + description = "A program for automated proving of mathematical texts"; + longDescription = '' + 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 ]; + homepage = http://nevidal.org/sad.en.html; + platforms = stdenv.lib.platforms.linux; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/sad/monoid.patch b/nixpkgs/pkgs/applications/science/logic/sad/monoid.patch new file mode 100644 index 000000000000..da9c21bcae91 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/sad/monoid.patch @@ -0,0 +1,51 @@ +diff --git a/Alice/Core/Check.hs b/Alice/Core/Check.hs +index 0700fa0388f..69815864710 100644 +--- a/Alice/Core/Check.hs ++++ b/Alice/Core/Check.hs +@@ -18,8 +18,12 @@ + - along with this program. If not, see <http://www.gnu.org/licenses/>. + -} + ++{-# LANGUAGE NoImplicitPrelude #-} ++ + module Alice.Core.Check (fillDef) where + ++import Prelude hiding ((<>)) ++ + import Control.Monad + import Data.Maybe + +diff --git a/Alice/Core/Reason.hs b/Alice/Core/Reason.hs +index c361bcf220d..4e493d8c91b 100644 +--- a/Alice/Core/Reason.hs ++++ b/Alice/Core/Reason.hs +@@ -17,9 +17,12 @@ + - You should have received a copy of the GNU General Public License + - along with this program. If not, see <http://www.gnu.org/licenses/>. + -} ++{-# LANGUAGE NoImplicitPrelude #-} + + module Alice.Core.Reason where + ++import Prelude hiding ((<>)) ++ + import Control.Monad + + import Alice.Core.Base +diff --git a/Alice/Core/Verify.hs b/Alice/Core/Verify.hs +index 4f8550bdf11..0f59d135b16 100644 +--- a/Alice/Core/Verify.hs ++++ b/Alice/Core/Verify.hs +@@ -18,8 +18,12 @@ + - along with this program. If not, see <http://www.gnu.org/licenses/>. + -} + ++{-# LANGUAGE NoImplicitPrelude #-} ++ + module Alice.Core.Verify (verify) where + ++import Prelude hiding ((<>)) ++ + import Control.Monad + import Data.IORef + import Data.Maybe diff --git a/nixpkgs/pkgs/applications/science/logic/sad/patch b/nixpkgs/pkgs/applications/science/logic/sad/patch new file mode 100644 index 000000000000..a5b1d6177083 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/sad/patch @@ -0,0 +1,200 @@ +diff -aur serious/sad-2.3-25/Alice/Core/Base.hs sad-2.3-25/Alice/Core/Base.hs +--- serious/sad-2.3-25/Alice/Core/Base.hs 2008-03-29 18:24:12.000000000 +0000 ++++ sad-2.3-25/Alice/Core/Base.hs 2015-11-27 06:38:28.740840823 +0000 +@@ -21,6 +21,7 @@ + module Alice.Core.Base where + + import Control.Monad ++import Control.Applicative + import Data.IORef + import Data.List + import Data.Time +@@ -61,10 +62,21 @@ + type CRMC a b = IORef RState -> IO a -> (b -> IO a) -> IO a + newtype CRM b = CRM { runCRM :: forall a . CRMC a b } + ++instance Functor CRM where ++ fmap = liftM ++ ++instance Applicative CRM where ++ pure = return ++ (<*>) = ap ++ + instance Monad CRM where + return r = CRM $ \ _ _ k -> k r + m >>= n = CRM $ \ s z k -> runCRM m s z (\ r -> runCRM (n r) s z k) + ++instance Alternative CRM where ++ (<|>) = mplus ++ empty = mzero ++ + instance MonadPlus CRM where + mzero = CRM $ \ _ z _ -> z + mplus m n = CRM $ \ s z k -> runCRM m s (runCRM n s z k) k +diff -aur serious/sad-2.3-25/Alice/Core/Thesis.hs sad-2.3-25/Alice/Core/Thesis.hs +--- serious/sad-2.3-25/Alice/Core/Thesis.hs 2008-03-05 13:10:50.000000000 +0000 ++++ sad-2.3-25/Alice/Core/Thesis.hs 2015-11-27 06:35:08.311015166 +0000 +@@ -21,6 +21,7 @@ + module Alice.Core.Thesis (thesis) where + + import Control.Monad ++import Control.Applicative + import Data.List + import Data.Maybe + +@@ -126,11 +127,22 @@ + + newtype TM res = TM { runTM :: [String] -> [([String], res)] } + ++instance Functor TM where ++ fmap = liftM ++ ++instance Applicative TM where ++ pure = return ++ (<*>) = ap ++ + instance Monad TM where + return r = TM $ \ s -> [(s, r)] + m >>= k = TM $ \ s -> concatMap apply (runTM m s) + where apply (s, r) = runTM (k r) s + ++instance Alternative TM where ++ (<|>) = mplus ++ empty = mzero ++ + instance MonadPlus TM where + mzero = TM $ \ _ -> [] + mplus m k = TM $ \ s -> runTM m s ++ runTM k s +diff -aur serious/sad-2.3-25/Alice/Export/Base.hs sad-2.3-25/Alice/Export/Base.hs +--- serious/sad-2.3-25/Alice/Export/Base.hs 2008-03-09 09:36:39.000000000 +0000 ++++ sad-2.3-25/Alice/Export/Base.hs 2015-11-27 06:32:47.782738005 +0000 +@@ -39,7 +39,7 @@ + -- Database reader + + readPrDB :: String -> IO [Prover] +-readPrDB file = do inp <- catch (readFile file) $ die . ioeGetErrorString ++readPrDB file = do inp <- catchIOError (readFile file) $ die . ioeGetErrorString + + let dws = dropWhile isSpace + cln = reverse . dws . reverse . dws +diff -aur serious/sad-2.3-25/Alice/Export/Prover.hs sad-2.3-25/Alice/Export/Prover.hs +--- serious/sad-2.3-25/Alice/Export/Prover.hs 2008-03-09 09:36:39.000000000 +0000 ++++ sad-2.3-25/Alice/Export/Prover.hs 2015-11-27 06:36:47.632919161 +0000 +@@ -60,7 +60,7 @@ + when (askIB IBPdmp False ins) $ putStrLn tsk + + seq (length tsk) $ return $ +- do (wh,rh,eh,ph) <- catch run ++ do (wh,rh,eh,ph) <- catchIOError run + $ \ e -> die $ "run error: " ++ ioeGetErrorString e + + hPutStrLn wh tsk ; hClose wh +diff -aur serious/sad-2.3-25/Alice/ForTheL/Base.hs sad-2.3-25/Alice/ForTheL/Base.hs +--- serious/sad-2.3-25/Alice/ForTheL/Base.hs 2008-03-09 09:36:39.000000000 +0000 ++++ sad-2.3-25/Alice/ForTheL/Base.hs 2015-11-27 06:31:51.921230428 +0000 +@@ -226,7 +226,7 @@ + varlist = do vs <- chainEx (char ',') var + nodups vs ; return vs + +-nodups vs = unless (null $ dups vs) $ ++nodups vs = unless ((null :: [a] -> Bool) $ dups vs) $ + fail $ "duplicate names: " ++ show vs + + hidden = askPS psOffs >>= \ n -> return ('h':show n) +diff -aur serious/sad-2.3-25/Alice/Import/Reader.hs sad-2.3-25/Alice/Import/Reader.hs +--- serious/sad-2.3-25/Alice/Import/Reader.hs 2008-03-09 09:36:39.000000000 +0000 ++++ sad-2.3-25/Alice/Import/Reader.hs 2015-11-27 06:36:41.818866167 +0000 +@@ -24,7 +24,7 @@ + import Control.Monad + import System.IO + import System.IO.Error +-import System.Exit ++import System.Exit hiding (die) + + import Alice.Data.Text + import Alice.Data.Instr +@@ -44,7 +44,7 @@ + readInit "" = return [] + + readInit file = +- do input <- catch (readFile file) $ die file . ioeGetErrorString ++ do input <- catchIOError (readFile file) $ die file . ioeGetErrorString + let tkn = tokenize input ; ips = initPS () + inp = ips { psRest = tkn, psFile = file, psLang = "Init" } + liftM fst $ fireLPM instf inp +@@ -74,7 +74,7 @@ + reader lb fs (ps:ss) [TI (InStr ISfile file)] = + do let gfl = if null file then hGetContents stdin + else readFile file +- input <- catch gfl $ die file . ioeGetErrorString ++ input <- catchIOError gfl $ die file . ioeGetErrorString + let tkn = tokenize input + ips = initPS $ (psProp ps) { tvr_expr = [] } + sps = ips { psRest = tkn, psFile = file, psOffs = psOffs ps } +diff -aur serious/sad-2.3-25/Alice/Parser/Base.hs sad-2.3-25/Alice/Parser/Base.hs +--- serious/sad-2.3-25/Alice/Parser/Base.hs 2008-03-09 09:36:40.000000000 +0000 ++++ sad-2.3-25/Alice/Parser/Base.hs 2015-11-27 06:14:28.616734527 +0000 +@@ -20,6 +20,7 @@ + + module Alice.Parser.Base where + ++import Control.Applicative + import Control.Monad + import Data.List + +@@ -45,11 +46,22 @@ + type CPMC a b c = (c -> CPMS a b) -> (String -> CPMS a b) -> CPMS a b + newtype CPM a c = CPM { runCPM :: forall b . CPMC a b c } + ++instance Functor (CPM a) where ++ fmap = liftM ++ ++instance Applicative (CPM a) where ++ pure = return ++ (<*>) = ap ++ + instance Monad (CPM a) where + return r = CPM $ \ k _ -> k r + m >>= n = CPM $ \ k l -> runCPM m (\ b -> runCPM (n b) k l) l + fail e = CPM $ \ _ l -> l e + ++instance Alternative (CPM a) where ++ (<|>) = mplus ++ empty = mzero ++ + instance MonadPlus (CPM a) where + mzero = CPM $ \ _ _ _ z -> z + mplus m n = CPM $ \ k l s -> runCPM m k l s . runCPM n k l s +diff -aur serious/sad-2.3-25/init.opt sad-2.3-25/init.opt +--- serious/sad-2.3-25/init.opt 2007-10-11 15:25:45.000000000 +0000 ++++ sad-2.3-25/init.opt 2015-11-27 07:23:41.372816854 +0000 +@@ -1,6 +1,6 @@ + # Alice init options +-[library examples] +-[provers provers/provers.dat] ++[library @out@/examples] ++[provers @out@/provers/provers.dat] + [prover spass] + [timelimit 3] + [depthlimit 7] +diff -aur serious/sad-2.3-25/provers/provers.dat sad-2.3-25/provers/provers.dat +--- serious/sad-2.3-25/provers/provers.dat 2008-08-26 21:20:25.000000000 +0000 ++++ sad-2.3-25/provers/provers.dat 2015-11-27 07:24:18.878169702 +0000 +@@ -3,7 +3,7 @@ + Pmoses + LMoses + Fmoses +-Cprovers/moses ++C@out@/provers/moses + Yproved in + Nfound unprovable in + Utimeout in +@@ -12,7 +12,7 @@ + Pspass + LSPASS + Fdfg +-Cprovers/SPASS -CNFOptSkolem=0 -PProblem=0 -PGiven=0 -Stdin -TimeLimit=%d ++C@spass@/bin/SPASS -CNFOptSkolem=0 -PProblem=0 -PGiven=0 -Stdin -TimeLimit=%d + YSPASS beiseite: Proof found. + NSPASS beiseite: Completion found. + USPASS beiseite: Ran out of time. diff --git a/nixpkgs/pkgs/applications/science/logic/satallax/default.nix b/nixpkgs/pkgs/applications/science/logic/satallax/default.nix new file mode 100644 index 000000000000..7249eb991d38 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/satallax/default.nix @@ -0,0 +1,66 @@ +{stdenv, fetchurl, ocaml, zlib, which, eprover, makeWrapper, coq}: +stdenv.mkDerivation rec { + pname = "satallax"; + version = "2.7"; + + buildInputs = [ocaml zlib which eprover makeWrapper coq]; + src = fetchurl { + url = "https://www.ps.uni-saarland.de/~cebrown/satallax/downloads/${pname}-${version}.tar.gz"; + sha256 = "1kvxn8mc35igk4vigi5cp7w3wpxk2z3bgwllfm4n3h2jfs0vkpib"; + }; + + preConfigure = '' + mkdir fake-tools + echo "echo 'Nix-build-host.localdomain'" > fake-tools/hostname + chmod a+x fake-tools/hostname + export PATH="$PATH:$PWD/fake-tools" + + ( + cd picosat-* + ./configure + make + ) + export PATH="$PATH:$PWD/libexec/satallax" + + mkdir -p "$out/libexec/satallax" + cp picosat-*/picosat picosat-*/picomus "$out/libexec/satallax" + + ( + cd minisat + export MROOT=$PWD + cd core + make + cd ../simp + make + ) + ''; + + postBuild = "echo testing; ! (bash ./test | grep ERROR)"; + + installPhase = '' + 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" \ + --add-flags "-M" --add-flags "$out/lib/satallax/modes" + + cp LICENSE README "$out/share/doc/satallax" + + cp bin/*.so "$out/lib" + + cp -r modes "$out/lib/satallax/" + cp -r problems "$out/lib/satallax/" + cp -r coq* "$out/lib/satallax/" + ''; + + 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; + 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 new file mode 100644 index 000000000000..d357bef2c7a0 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/saw-tools/default.nix @@ -0,0 +1,61 @@ +{ stdenv, fetchurl, gmp4, ncurses, zlib, clang_35 }: + +let + libPath = stdenv.lib.makeLibraryPath + [ stdenv.cc.libc + stdenv.cc.cc + gmp4 + ncurses + zlib + ] + ":${stdenv.cc.cc.lib}/lib64"; + + url = "https://github.com/GaloisInc/saw-script/releases/download"; + + saw-bin = + if stdenv.hostPlatform.system == "i686-linux" + then fetchurl { + url = url + "/v0.1.1-dev/saw-0.1.1-dev-2015-07-31-CentOS6-32.tar.gz"; + sha256 = "126iag5nnvndi78c921z7vjrjfwcspn1hlxwwhzmqm4rvbhhr9v9"; + } + else fetchurl { + url = url + "/v0.1.1-dev/saw-0.1.1-dev-2015-07-31-CentOS6-64.tar.gz"; + sha256 = "07gyf319v6ama6n1aj96403as04bixi8mbisfy7f7va689zklflr"; + }; +in +stdenv.mkDerivation { + pname = "saw-tools"; + version = "0.1.1-20150731"; + + src = saw-bin; + + installPhase = '' + mkdir -p $out/lib $out/share + + mv bin $out/bin + mv doc $out/share + + # Hack around lack of libtinfo in NixOS + ln -s ${ncurses.out}/lib/libncursesw.so.5 $out/lib/libtinfo.so.5 + ln -s ${stdenv.cc.libc}/lib/libpthread.so.0 $out/lib/libpthread.so.0 + + # Add a clang symlink for easy building with a suitable compiler. + ln -s ${clang_35}/bin/clang $out/bin/saw-clang + ''; + + fixupPhase = '' + for x in bin/bcdump bin/extcore-info bin/jss bin/llvm-disasm bin/lss bin/saw; do + patchelf --interpreter "$(cat $NIX_CC/nix-support/dynamic-linker)" \ + --set-rpath "$out/lib:${libPath}" $out/$x; + done + ''; + + phases = "unpackPhase installPhase fixupPhase"; + + 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 ]; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/spass/default.nix b/nixpkgs/pkgs/applications/science/logic/spass/default.nix new file mode 100644 index 000000000000..ece6f0b9f6a8 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/spass/default.nix @@ -0,0 +1,42 @@ +{ stdenv, fetchurl, bison, flex }: + +let + baseVersion="3"; + minorVersion="9"; + + extraTools = "FLOTTER prolog2dfg dfg2otter dfg2dimacs dfg2tptp" + + " dfg2ascii dfg2dfg tptp2dfg dimacs2dfg pgen rescmp"; +in + +stdenv.mkDerivation { + pname = "spass"; + version = "${baseVersion}.${minorVersion}"; + + src = fetchurl { + url = "http://www.spass-prover.org/download/sources/spass${baseVersion}${minorVersion}.tgz"; + sha256 = "11cyn3kcff4r79rsw2s0xm6rdb8bi0kpkazv2b48jhcms7xw75qp"; + }; + + sourceRoot = "."; + + nativeBuildInputs = [ bison flex ]; + + buildPhase = '' + make RM="rm -f" proparser.c ${extraTools} opt + ''; + installPhase = '' + mkdir -p $out/bin + install -m0755 SPASS ${extraTools} $out/bin/ + ''; + + meta = with stdenv.lib; { + description = "Automated theorem prover for first-order logic"; + maintainers = with maintainers; + [ + raskin + ]; + platforms = platforms.unix; + license = licenses.bsd2; + downloadPage = "http://www.spass-prover.org/download/index.html"; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/statverif/default.nix b/nixpkgs/pkgs/applications/science/logic/statverif/default.nix new file mode 100644 index 000000000000..e0efb28819d2 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/statverif/default.nix @@ -0,0 +1,34 @@ +{ stdenv, fetchurl, ocaml }: + +stdenv.mkDerivation rec { + pname = "statverif"; + version = "1.86pl4"; + + src = fetchurl { + url = "http://prosecco.gforge.inria.fr/personal/bblanche/proverif/proverif${version}.tar.gz"; + sha256 = "163vdcixs764jj8xa08w80qm4kcijf7xj911yp8jvz6pi1q5g13i"; + }; + + pf-patch = fetchurl { + url = "http://markryan.eu/research/statverif/files/proverif-${version}-statverif-2657ab4.patch"; + sha256 = "113jjhi1qkcggbsmbw8fa9ln8vs7vy2r288szks7rn0jjn0wxmbw"; + }; + + buildInputs = [ ocaml ]; + + patchPhase = "patch -p1 < ${pf-patch}"; + buildPhase = "./build"; + installPhase = '' + mkdir -p $out/bin + cp ./proverif $out/bin/statverif + cp ./proveriftotex $out/bin/statveriftotex + ''; + + 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 ]; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/stp/default.nix b/nixpkgs/pkgs/applications/science/logic/stp/default.nix new file mode 100644 index 000000000000..0ea659d1927f --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/stp/default.nix @@ -0,0 +1,35 @@ +{ stdenv, cmake, boost, bison, flex, fetchFromGitHub, perl, python3, python3Packages, zlib, minisatUnstable, cryptominisat }: + +stdenv.mkDerivation rec { + pname = "stp"; + version = "2.3.3"; + + src = fetchFromGitHub { + owner = "stp"; + repo = "stp"; + rev = version; + sha256 = "1yg2v4wmswh1sigk47drwsxyayr472mf4i47lqmlcgn9hhbx1q87"; + }; + + buildInputs = [ boost zlib minisatUnstable cryptominisat python3 ]; + nativeBuildInputs = [ cmake bison flex perl ]; + preConfigure = '' + python_install_dir=$out/${python3Packages.python.sitePackages} + mkdir -p $python_install_dir + cmakeFlagsArray=( + $cmakeFlagsArray + "-DBUILD_SHARED_LIBS=ON" + "-DPYTHON_LIB_INSTALL_DIR=$python_install_dir" + ) + ''; + + # seems to build fine now, may revert if concurrency does become an issue + enableParallelBuilding = true; + + meta = with stdenv.lib; { + description = "Simple Theorem Prover"; + maintainers = with maintainers; [ ]; + platforms = platforms.linux; + license = licenses.mit; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/symbiyosys/default.nix b/nixpkgs/pkgs/applications/science/logic/symbiyosys/default.nix new file mode 100644 index 000000000000..ed66c77dcabf --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/symbiyosys/default.nix @@ -0,0 +1,39 @@ +{ stdenv, fetchFromGitHub, yosys, bash, python3 }: + +stdenv.mkDerivation { + pname = "symbiyosys"; + version = "2019.08.13"; + + src = fetchFromGitHub { + owner = "yosyshq"; + repo = "symbiyosys"; + rev = "9cb542ac7a310b3dfa626349db53bed6236b670c"; + sha256 = "0c7nz740738ybk33zzlfl00cq86n31wvra8pqqkpl4ygxnwca1d6"; + }; + + buildInputs = [ python3 yosys ]; + + buildPhase = "true"; + installPhase = '' + mkdir -p $out/bin $out/share/yosys/python3 + + cp sbysrc/sby_*.py $out/share/yosys/python3/ + cp sbysrc/sby.py $out/bin/sby + chmod +x $out/bin/sby + + # Fix up shebang and Yosys imports + patchShebangs $out/bin/sby + substituteInPlace $out/bin/sby \ + --replace "##yosys-sys-path##" \ + "sys.path += [p + \"/share/yosys/python3/\" for p in [\"$out\", \"${yosys}\"]]" + substituteInPlace $out/share/yosys/python3/sby_core.py \ + --replace '"/usr/bin/env", "bash"' '"${bash}/bin/bash"' + ''; + 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; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/tamarin-prover/default.nix b/nixpkgs/pkgs/applications/science/logic/tamarin-prover/default.nix new file mode 100644 index 000000000000..40378f8c04d5 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/tamarin-prover/default.nix @@ -0,0 +1,107 @@ +{ haskellPackages, mkDerivation, fetchFromGitHub, lib +# the following are non-haskell dependencies +, makeWrapper, which, maude, graphviz, ocaml +}: + +let + version = "1.4.1"; + src = fetchFromGitHub { + owner = "tamarin-prover"; + repo = "tamarin-prover"; + rev = "d2e1c57311ce4ed0ef46d0372c4995b8fdc25323"; + sha256 = "1bf2qvb646jg3qxd6jgp9ja3wlr888wchxi9mfr3kg7hfn63vxbq"; + }; + + # tamarin has its own dependencies, but they're kept inside the repo, + # no submodules. this factors out the common metadata among all derivations + common = pname: src: { + inherit pname version src; + + license = lib.licenses.gpl3; + homepage = https://tamarin-prover.github.io; + description = "Security protocol verification in the symbolic model"; + maintainers = [ lib.maintainers.thoughtpolice ]; + }; + + # tamarin use symlinks to the LICENSE and Setup.hs files, so for these sublibraries + # we set the patchPhase to fix that. otherwise, cabal cries a lot. + replaceSymlinks = '' + cp --remove-destination ${src}/LICENSE .; + cp --remove-destination ${src}/Setup.hs .; + ''; + + tamarin-prover-utils = mkDerivation (common "tamarin-prover-utils" (src + "/lib/utils") // { + postPatch = replaceSymlinks; + libraryHaskellDepends = with haskellPackages; [ + base base64-bytestring binary blaze-builder bytestring containers + deepseq dlist fclabels mtl pretty safe SHA syb time transformers + ]; + }); + + tamarin-prover-term = mkDerivation (common "tamarin-prover-term" (src + "/lib/term") // { + postPatch = replaceSymlinks; + libraryHaskellDepends = (with haskellPackages; [ + attoparsec base binary bytestring containers deepseq dlist HUnit + mtl process safe + ]) ++ [ tamarin-prover-utils ]; + }); + + tamarin-prover-theory = mkDerivation (common "tamarin-prover-theory" (src + "/lib/theory") // { + postPatch = replaceSymlinks; + doHaddock = false; # broken + libraryHaskellDepends = (with haskellPackages; [ + aeson aeson-pretty base binary bytestring containers deepseq dlist + fclabels mtl parallel parsec process safe text transformers uniplate + ]) ++ [ tamarin-prover-utils tamarin-prover-term ]; + }); + +in +mkDerivation (common "tamarin-prover" src // { + isLibrary = false; + isExecutable = true; + + # strip out unneeded deps manually + doHaddock = false; + enableSharedExecutables = false; + postFixup = "rm -rf $out/lib $out/nix-support $out/share/doc"; + + # Fix problem with MonadBaseControl not being found + patchPhase = '' + sed -ie 's,\(import *\)Control\.Monad$,&\ + \1Control.Monad.Trans.Control,' src/Web/Handler.hs + + sed -ie 's~\( *, \)mtl~&\ + \1monad-control~' tamarin-prover.cabal + + patch -p1 < ${./sapic-native.patch} + ''; + + postBuild = '' + cd plugins/sapic && make sapic && cd ../.. + ''; + + # wrap the prover to be sure it can find maude, sapic, etc + executableToolDepends = [ makeWrapper which maude graphviz ]; + postInstall = '' + wrapProgram $out/bin/tamarin-prover \ + --prefix PATH : ${lib.makeBinPath [ which maude graphviz ]} + # so that the package can be used as a vim plugin to install syntax coloration + install -Dt $out/share/vim-plugins/tamarin-prover/syntax/ etc/{spthy,sapic}.vim + install etc/filetype.vim -D $out/share/vim-plugins/tamarin-prover/ftdetect/tamarin.vim + install -m0755 ./plugins/sapic/sapic $out/bin/sapic + ''; + + checkPhase = "./dist/build/tamarin-prover/tamarin-prover test"; + + executableSystemDepends = [ ocaml ]; + executableHaskellDepends = (with haskellPackages; [ + base binary binary-orphans blaze-builder blaze-html bytestring + cmdargs conduit containers monad-control deepseq directory fclabels file-embed + filepath gitrev http-types HUnit lifted-base mtl monad-unlift parsec process + resourcet safe shakespeare tamarin-prover-term + template-haskell text threads time wai warp yesod-core yesod-static + ]) ++ [ tamarin-prover-utils + tamarin-prover-term + tamarin-prover-theory + ]; +}) diff --git a/nixpkgs/pkgs/applications/science/logic/tamarin-prover/sapic-native.patch b/nixpkgs/pkgs/applications/science/logic/tamarin-prover/sapic-native.patch new file mode 100644 index 000000000000..6ab7e4e7594f --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/tamarin-prover/sapic-native.patch @@ -0,0 +1,77 @@ +diff --git a/plugins/sapic/Makefile b/plugins/sapic/Makefile +index 8f1b1866..678accbe 100644 +--- a/plugins/sapic/Makefile ++++ b/plugins/sapic/Makefile +@@ -1,18 +1,18 @@ + TARGET = sapic +-OBJS= color.cmo exceptions.cmo btree.cmo position.cmo positionplusinit.cmo var.cmo term.cmo fact.cmo atomformulaaction.cmo action.cmo atom.cmo formula.cmo tamarin.cmo sapicterm.cmo sapicvar.cmo sapicaction.cmo lexer.cmo sapic.cmo annotatedsapicaction.cmo annotatedsapictree.cmo progressfunction.cmo restrictions.cmo annotatedrule.cmo translationhelper.cmo basetranslation.cmo firsttranslation.cmo main.cmo ++OBJS= color.cmx exceptions.cmx btree.cmx position.cmx positionplusinit.cmx var.cmx term.cmx fact.cmx atomformulaaction.cmx action.cmx atom.cmx formula.cmx tamarin.cmx sapicterm.cmx sapicvar.cmx sapicaction.cmx lexer.cmx sapic.cmx annotatedsapicaction.cmx annotatedsapictree.cmx progressfunction.cmx restrictions.cmx annotatedrule.cmx translationhelper.cmx basetranslation.cmx firsttranslation.cmx main.cmx + FLAGS=-g + +-OCAMLC := $(shell command -v ocamlc 2> /dev/null) ++OCAMLOPT := $(shell command -v ocamlopt 2> /dev/null) + OCAMLLEX := $(shell command -v ocamllex 2> /dev/null) + OCAMLYACC := $(shell command -v ocamlyacc 2> /dev/null) + OCAMLDEP := $(shell command -v ocamldep 2> /dev/null) +-OCAMLC_GTEQ_402 := $(shell expr `ocamlc -version | sed -e 's/\.\([0-9][0-9]\)/\1/g' -e 's/\.\([0-9]\)/0\1/g' -e 's/^[0-9]\{3,4\}$$/&00/'` \>= 40200) ++OCAMLC_GTEQ_402 := $(shell expr `ocamlopt -version | sed -e 's/\.\([0-9][0-9]\)/\1/g' -e 's/\.\([0-9]\)/0\1/g' -e 's/^[0-9]\{3,4\}$$/&00/'` \>= 40200) + + default: sapic + + sapic: +-ifdef OCAMLC +- @echo "Found ocamlc." ++ifdef OCAMLOPT ++ @echo "Found ocamlopt." + ifdef OCAMLLEX + @echo "Found ocamllex." + ifdef OCAMLYACC +@@ -22,9 +22,9 @@ ifdef OCAMLDEP + ifeq "$(OCAMLC_GTEQ_402)" "1" + @echo "Building SAPIC." + $(MAKE) $(OBJS) +- ocamlc $(FLAGS) -o $@ str.cma $(OBJS) +- @echo "Installing SAPIC into ~/.local/bin/" +- cp sapic ~/.local/bin ++ ocamlopt $(FLAGS) -o $@ str.cmxa $(OBJS) ++# @echo "Installing SAPIC into ~/.local/bin/" ++# cp sapic ~/.local/bin + else + @echo "Found OCAML version < 4.02. SAPIC will not be installed." + endif +@@ -38,7 +38,7 @@ else + @echo "ocamllex not found. SAPIC will not be installed." + endif + else +- @echo "ocamlc not found. SAPIC will not be installed." ++ @echo "ocamlopt not found. SAPIC will not be installed." + endif + + depend: +@@ -48,20 +48,20 @@ lexer.ml: sapic.cmi + + .PHONY: clean + clean: +- rm -rf *.cmi *.cmo $(TARGET) ++ rm -rf *.cmi **.cmx $(TARGET) + rm -rf sapic.ml sapic.mli lexer.ml lexer.mli + +-.SUFFIXES: .ml .mli .mll .mly .cmo .cmi ++.SUFFIXES: .ml .mli .mll .mly .cmx .cmi + +-.ml.cmo: +- ocamlc $(FLAGS) -c $< ++.ml.cmx: ++ ocamlopt $(FLAGS) -c $< + .mli.cmi: +- ocamlc $(FLAGS) -c $< ++ ocamlopt $(FLAGS) -c $< + .mll.ml: + ocamllex $< + .mly.ml: + ocamlyacc $< + .ml.mli: +- ocamlc -i $< > $@ ++ ocamlopt -i $< > $@ + + -include .depend diff --git a/nixpkgs/pkgs/applications/science/logic/tlaplus/default.nix b/nixpkgs/pkgs/applications/science/logic/tlaplus/default.nix new file mode 100644 index 000000000000..b1c72d7c5ee7 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/tlaplus/default.nix @@ -0,0 +1,40 @@ +{ stdenv, fetchFromGitHub, makeWrapper +, jdk, jre, ant +}: + +stdenv.mkDerivation rec { + pname = "tlaplus"; + version = "1.5.6"; + + src = fetchFromGitHub { + owner = "tlaplus"; + repo = "tlaplus"; + rev = "refs/tags/v${version}"; + sha256 = "0966mvgxamknj4hsp980qbxwda886w1dv309kn7isxn0420lfv4f"; + }; + + buildInputs = [ makeWrapper jdk ant ]; + + buildPhase = "ant -f tlatools/customBuild.xml compile dist"; + installPhase = '' + mkdir -p $out/share/java $out/bin + cp tlatools/dist/*.jar $out/share/java + + makeWrapper ${jre}/bin/java $out/bin/tlc2 \ + --add-flags "-cp $out/share/java/tla2tools.jar tlc2.TLC" + makeWrapper ${jre}/bin/java $out/bin/tla2sany \ + --add-flags "-cp $out/share/java/tla2tools.jar tla2sany.SANY" + makeWrapper ${jre}/bin/java $out/bin/pcal \ + --add-flags "-cp $out/share/java/tla2tools.jar pcal.trans" + makeWrapper ${jre}/bin/java $out/bin/tla2tex \ + --add-flags "-cp $out/share/java/tla2tools.jar tla2tex.TLA" + ''; + + 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 ]; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/tlaplus/tlaps.nix b/nixpkgs/pkgs/applications/science/logic/tlaplus/tlaps.nix new file mode 100644 index 000000000000..7c8389688d95 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/tlaplus/tlaps.nix @@ -0,0 +1,54 @@ +{ fetchurl +, stdenv +, ocaml, isabelle, cvc3, perl, wget, which +}: + +stdenv.mkDerivation rec { + pname = "tlaps"; + version = "1.4.3"; + src = fetchurl { + url = "https://tla.msr-inria.inria.fr/tlaps/dist/current/tlaps-${version}.tar.gz"; + sha256 = "1w5z3ns5xxmhmp8r4x2kjmy3clqam935gmvx82imyxrr1bamx6gf"; + }; + + buildInputs = [ ocaml isabelle cvc3 perl wget which ]; + + phases = [ "unpackPhase" "installPhase" ]; + + installPhase = '' + mkdir -pv "$out" + export HOME="$out" + export PATH=$out/bin:$PATH + + pushd zenon + ./configure --prefix $out + make + make install + popd + + pushd isabelle + isabelle build -b Pure + popd + + pushd tlapm + ./configure --prefix $out + make all + make install + ''; + + meta = { + description = "Mechanically check TLA+ proofs"; + longDescription = '' + TLA+ is a general-purpose formal specification language that is + particularly useful for describing concurrent and distributed + systems. The TLA+ proof language is declarative, hierarchical, + and scalable to large system specifications. It provides a + 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; + maintainers = [ stdenv.lib.maintainers.badi ]; + }; + +} diff --git a/nixpkgs/pkgs/applications/science/logic/tlaplus/toolbox.nix b/nixpkgs/pkgs/applications/science/logic/tlaplus/toolbox.nix new file mode 100644 index 000000000000..91666e85d923 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/tlaplus/toolbox.nix @@ -0,0 +1,81 @@ +{ lib, fetchzip, makeWrapper, makeDesktopItem, stdenv +, gtk, libXtst, glib, zlib +}: + +let + version = "1.6.0"; + arch = "x86_64"; + + desktopItem = makeDesktopItem rec { + name = "TLA+Toolbox"; + exec = "tla-toolbox"; + icon = "tla-toolbox"; + comment = "IDE for TLA+"; + desktopName = name; + genericName = comment; + categories = "Application;Development"; + extraEntries = '' + StartupWMClass=TLA+ Toolbox + ''; + }; + + +in stdenv.mkDerivation { + pname = "tla-toolbox"; + inherit version; + src = fetchzip { + url = "https://tla.msr-inria.inria.fr/tlatoolbox/products/TLAToolbox-${version}-linux.gtk.${arch}.zip"; + sha256 = "1mgx4p5qykf9q0p4cp6kcpc7fx8g5f2w1g40kdgas24hqwrgs3cm"; + }; + + buildInputs = [ makeWrapper ]; + + phases = [ "installPhase" ]; + + installPhase = '' + mkdir -p "$out/bin" + cp -r "$src" "$out/toolbox" + chmod -R +w "$out/toolbox" + + patchelf \ + --set-interpreter $(cat $NIX_CC/nix-support/dynamic-linker) \ + "$out/toolbox/toolbox" + + patchelf \ + --set-interpreter $(cat $NIX_CC/nix-support/dynamic-linker) \ + "$(find "$out/toolbox" -name java)" + + makeWrapper $out/toolbox/toolbox $out/bin/tla-toolbox \ + --run "set -x; cd $out/toolbox" \ + --add-flags "-data ~/.tla-toolbox" \ + --prefix LD_LIBRARY_PATH : "${lib.makeLibraryPath [ gtk libXtst glib zlib ]}" + + echo -e "\nCreating TLA Toolbox icons..." + pushd "$src" + for icon_in in $(find . -path "./plugins/*/icons/full/etool16/tla_launch_check_wiz_*.png") + do + icon_size=$(echo $icon_in | grep -Po "wiz_\K[0-9]+") + icon_out="$out/share/icons/hicolor/$icon_size""x$icon_size/apps/tla-toolbox.png" + mkdir -p "$(dirname $icon_out)" + cp "$icon_in" "$icon_out" + done + popd + + echo -e "\nCreating TLA Toolbox desktop entry..." + cp -r "${desktopItem}/share/applications"* "$out/share/applications" + ''; + + meta = { + homepage = http://research.microsoft.com/en-us/um/people/lamport/tla/toolbox.html; + description = "IDE for the TLA+ tools"; + longDescription = '' + Integrated development environment for the TLA+ tools, based on Eclipse. You can use it + to create and edit your specs, run the PlusCal translator, view the pretty-printed + versions of your modules, run the TLC model checker, and run TLAPS, the TLA+ proof system. + ''; + # http://lamport.azurewebsites.net/tla/license.html + license = with lib.licenses; [ mit ]; + platforms = stdenv.lib.platforms.linux; + maintainers = [ stdenv.lib.maintainers.badi ]; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/tptp/default.nix b/nixpkgs/pkgs/applications/science/logic/tptp/default.nix new file mode 100644 index 000000000000..4c63f8e72a36 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/tptp/default.nix @@ -0,0 +1,49 @@ +{ stdenv, fetchurl, yap, tcsh, perl, patchelf }: + +stdenv.mkDerivation rec { + pname = "TPTP"; + version = "7.2.0"; + + src = fetchurl { + urls = [ + "http://tptp.cs.miami.edu/TPTP/Distribution/TPTP-v${version}.tgz" + "http://tptp.cs.miami.edu/TPTP/Archive/TPTP-v${version}.tgz" + ]; + sha256 = "0yq8452b6mym4yscy46pshg0z2my8xi74b5bp2qlxd5bjwcrg6rl"; + }; + + nativeBuildInputs = [ patchelf ]; + buildInputs = [ tcsh yap perl ]; + + installPhase = '' + sharedir=$out/share/tptp + + mkdir -p $sharedir + cp -r ./ $sharedir + + export TPTP=$sharedir + + tcsh $sharedir/Scripts/tptp2T_install -default + + substituteInPlace $sharedir/TPTP2X/tptp2X_install --replace /bin/mv mv + tcsh $sharedir/TPTP2X/tptp2X_install -default + + patchelf --interpreter $(cat $NIX_CC/nix-support/dynamic-linker) $sharedir/Scripts/tptp4X + + mkdir -p $out/bin + ln -s $sharedir/TPTP2X/tptp2X $out/bin + ln -s $sharedir/Scripts/tptp2T $out/bin + ln -s $sharedir/Scripts/tptp4X $out/bin + ''; + + meta = with stdenv.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. + # No sense in letting Hydra build it. + # Also, it is unclear what is covered by "verbatim" - we will edit configs + hydraPlatforms = []; + platforms = platforms.all; + license = licenses.unfreeRedistributable; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/twelf/default.nix b/nixpkgs/pkgs/applications/science/logic/twelf/default.nix new file mode 100644 index 000000000000..161da6e4b235 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/twelf/default.nix @@ -0,0 +1,51 @@ +{ stdenv, fetchurl, pkgconfig, smlnj, rsync }: + +stdenv.mkDerivation rec { + pname = "twelf"; + version = "1.7.1"; + + src = fetchurl { + url = "http://twelf.plparty.org/releases/twelf-src-${version}.tar.gz"; + sha256 = "0fi1kbs9hrdrm1x4k13angpjasxlyd1gc3ys8ah54i75qbcd9c4i"; + }; + + nativeBuildInputs = [ pkgconfig ]; + buildInputs = [ smlnj rsync ]; + + buildPhase = '' + export SMLNJ_HOME=${smlnj} + make smlnj + ''; + + installPhase = '' + mkdir -p $out/bin + rsync -av bin/{*,.heap} $out/bin/ + bin/.mkexec ${smlnj}/bin/sml $out/ twelf-server twelf-server + + substituteInPlace emacs/twelf-init.el \ + --replace '(concat twelf-root "emacs")' '(concat twelf-root "share/emacs/site-lisp/twelf")' + + mkdir -p $out/share/emacs/site-lisp/twelf/ + rsync -av emacs/ $out/share/emacs/site-lisp/twelf/ + + mkdir -p $out/share/twelf/examples + rsync -av examples/ $out/share/twelf/examples/ + mkdir -p $out/share/twelf/vim + rsync -av vim/ $out/share/twelf/vim/ + ''; + + meta = { + description = "Logic proof assistant"; + longDescription = '' + Twelf is a language used to specify, implement, and prove properties of + deductive systems such as programming languages and logics. Large + research projects using Twelf include the TALT typed assembly language, + a foundational proof-carrying-code system, and a type safety proof for + 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; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/vampire/default.nix b/nixpkgs/pkgs/applications/science/logic/vampire/default.nix new file mode 100644 index 000000000000..42963fe5f9c6 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/vampire/default.nix @@ -0,0 +1,56 @@ +{ stdenv, fetchFromGitHub, fetchpatch, z3, zlib }: + +stdenv.mkDerivation rec { + pname = "vampire"; + version = "4.4"; + + src = fetchFromGitHub { + owner = "vprover"; + repo = "vampire"; + rev = version; + sha256 = "0v2fdfnk7l5xr5c4y54r25g1nbp4vi85zv29nbklh3r7aws3w9q1"; + }; + + buildInputs = [ z3 zlib ]; + + makeFlags = [ "vampire_z3_rel" "CC:=$(CC)" "CXX:=$(CXX)" ]; + + patches = [ + # https://github.com/vprover/vampire/pull/54 + (fetchpatch { + name = "fix-apple-cygwin-defines.patch"; + url = https://github.com/vprover/vampire/pull/54.patch; + sha256 = "0i6nrc50wlg1dqxq38lkpx4rmfb3lf7s8f95l4jkvqp0nxa20cza"; + }) + # https://github.com/vprover/vampire/pull/55 + (fetchpatch { + name = "fix-wait-any.patch"; + url = https://github.com/vprover/vampire/pull/55.patch; + sha256 = "1pwfpwpl23bqsgkmmvw6bnniyvp5j9v8l3z9s9pllfabnfcrcz9l"; + }) + # https://github.com/vprover/vampire/pull/56 + (fetchpatch { + name = "fenv.patch"; + url = https://github.com/vprover/vampire/pull/56.patch; + sha256 = "0xl3jcyqmk146mg3qj5hdd0pbja6wbq3250zmfhbxqrjh40mm40g"; + }) + ]; + + enableParallelBuilding = true; + + fixupPhase = '' + rm -rf z3 + ''; + + installPhase = '' + install -m0755 -D vampire_z3_rel* $out/bin/vampire + ''; + + meta = with stdenv.lib; { + homepage = "https://vprover.github.io/"; + description = "The Vampire Theorem Prover"; + platforms = platforms.unix; + license = licenses.unfree; + maintainers = with maintainers; [ gebner ]; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/verifast/default.nix b/nixpkgs/pkgs/applications/science/logic/verifast/default.nix new file mode 100644 index 000000000000..3e3e26708618 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/verifast/default.nix @@ -0,0 +1,50 @@ +{ stdenv, fetchurl, gtk2, gdk-pixbuf, atk, pango, glib, cairo, freetype +, fontconfig, libxml2, gnome2 }: + +let + + libPath = stdenv.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"; + + patchExe = x: '' + patchelf --interpreter "$(cat $NIX_CC/nix-support/dynamic-linker)" \ + --set-rpath ${libPath} ${x} + ''; + + patchLib = x: '' + patchelf --set-rpath ${libPath} ${x} + ''; + +in +stdenv.mkDerivation rec { + pname = "verifast"; + version = "18.02"; + + src = fetchurl { + url = "https://github.com/verifast/verifast/releases/download/${version}/${pname}-${version}-linux.tar.gz"; + sha256 = "19050be23b6d5e471690421fee59f84c58b29e38379fb86b8f3713a206a4423e"; + }; + + dontStrip = true; + phases = "unpackPhase installPhase"; + installPhase = '' + mkdir -p $out/bin + cp -R bin $out/libexec + + ${patchExe "$out/libexec/verifast"} + ${patchExe "$out/libexec/vfide"} + ${patchLib "$out/libexec/libz3.so"} + ln -s $out/libexec/verifast $out/bin/verifast + ln -s $out/libexec/vfide $out/bin/vfide + ''; + + meta = { + description = "Verification for C and Java programs via separation logic"; + homepage = "http://people.cs.kuleuven.be/~bart.jacobs/verifast/"; + license = stdenv.lib.licenses.msrla; + platforms = [ "x86_64-linux" ]; + maintainers = [ stdenv.lib.maintainers.thoughtpolice ]; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/verit/default.nix b/nixpkgs/pkgs/applications/science/logic/verit/default.nix new file mode 100644 index 000000000000..2c68191b800e --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/verit/default.nix @@ -0,0 +1,31 @@ +{ stdenv, fetchurl, autoreconfHook, gmp, flex, bison }: + +stdenv.mkDerivation { + pname = "veriT"; + version = "2016"; + + src = fetchurl { + url = "http://www.verit-solver.org/distrib/veriT-stable2016.tar.gz"; + sha256 = "0gvp4diz0qjg0y5ry0p1z7dkdkxw8l7jb8cdhvcnhl06jx977v4b"; + }; + + nativeBuildInputs = [ autoreconfHook flex bison ]; + buildInputs = [ gmp ]; + + # --disable-static actually enables static linking here... + dontDisableStatic = true; + + makeFlags = [ "LEX=${flex}/bin/flex" ]; + + preInstall = '' + mkdir -p $out/bin + ''; + + meta = with stdenv.lib; { + description = "An open, trustable and efficient SMT-solver"; + homepage = http://www.verit-solver.org/; + license = licenses.bsd3; + platforms = platforms.unix; + maintainers = [ maintainers.gebner ]; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/why3/configure.patch b/nixpkgs/pkgs/applications/science/logic/why3/configure.patch new file mode 100644 index 000000000000..3eebf3cf165d --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/why3/configure.patch @@ -0,0 +1,11 @@ +diff --git a/configure b/configure +--- a/configure ++++ b/configure +@@ -4029,7 +4029,6 @@ fi + + if test "$USEOCAMLFIND" = yes; then + OCAMLFINDLIB=$(ocamlfind printconf stdlib) +- OCAMLFIND=$(which ocamlfind) + if test "$OCAMLFINDLIB" != "$OCAMLLIB"; then + USEOCAMLFIND=no; + echo "but your ocamlfind is not compatible with your ocamlc:" diff --git a/nixpkgs/pkgs/applications/science/logic/why3/default.nix b/nixpkgs/pkgs/applications/science/logic/why3/default.nix new file mode 100644 index 000000000000..6f338f214783 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/why3/default.nix @@ -0,0 +1,48 @@ +{ callPackage, fetchurl, stdenv +, ocamlPackages, coqPackages, rubber, hevea, emacs }: + +stdenv.mkDerivation { + pname = "why3"; + version = "1.2.0"; + + src = fetchurl { + url = https://gforge.inria.fr/frs/download.php/file/37903/why3-1.2.0.tar.gz; + sha256 = "0xz001jhi71ja8vqrjz27v63bidrzj4qvg1yqarq6p4dmpxhk348"; + }; + + buildInputs = with ocamlPackages; [ + ocaml findlib ocamlgraph zarith menhir + # Compressed Sessions + # Emacs compilation of why3.el + emacs + # Documentation + rubber hevea + # GUI + lablgtk + # WebIDE + js_of_ocaml js_of_ocaml-ppx + # Coq Support + coqPackages.coq coqPackages.flocq ocamlPackages.camlp5 + ]; + + propagatedBuildInputs = with ocamlPackages; [ camlzip num ]; + + enableParallelBuilding = true; + + # Remove unnecessary call to which + patches = [ ./configure.patch ]; + + configureFlags = [ "--enable-verbose-make" ]; + + installTargets = [ "install" "install-lib" ]; + + passthru.withProvers = callPackage ./with-provers.nix {}; + + meta = with stdenv.lib; { + description = "A platform for deductive program verification"; + homepage = "http://why3.lri.fr/"; + license = licenses.lgpl21; + platforms = platforms.unix; + maintainers = with maintainers; [ thoughtpolice vbgl ]; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/why3/with-provers.nix b/nixpkgs/pkgs/applications/science/logic/why3/with-provers.nix new file mode 100644 index 000000000000..3528dbd3a647 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/why3/with-provers.nix @@ -0,0 +1,30 @@ +{ stdenv, makeWrapper, runCommand, symlinkJoin, why3 }: +provers: +let configAwkScript = runCommand "why3-conf.awk" { inherit provers; } + '' + for p in $provers; do + for b in $p/bin/*; do + BASENAME=$(basename $b) + echo "/^command =/{ gsub(\"$BASENAME\", \"$b\") }" >> $out + done + done + echo '{ print }' >> $out + ''; +in stdenv.mkDerivation { + name = "${why3.name}-with-provers"; + + phases = [ "buildPhase" "installPhase" ]; + + buildInputs = [ why3 makeWrapper ] ++ provers; + + buildPhase = '' + mkdir -p $out/share/why3/ + why3 config --detect-provers -C $out/share/why3/why3.conf + awk -i inplace -f ${configAwkScript} $out/share/why3/why3.conf + ''; + + installPhase = '' + mkdir -p $out/bin + makeWrapper ${why3}/bin/why3 $out/bin/why3 --add-flags "--extra-config $out/share/why3/why3.conf" + ''; +} diff --git a/nixpkgs/pkgs/applications/science/logic/workcraft/default.nix b/nixpkgs/pkgs/applications/science/logic/workcraft/default.nix new file mode 100644 index 000000000000..2f972c92b521 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/workcraft/default.nix @@ -0,0 +1,33 @@ +{ stdenv, fetchurl, jre, makeWrapper }: + +stdenv.mkDerivation rec { + pname = "workcraft"; + version = "3.1.9"; + + src = fetchurl { + url = "https://github.com/workcraft/workcraft/releases/download/v${version}/workcraft-v${version}-linux.tar.gz"; + sha256 = "0d1mi8jffwr7irp215j9rfpa3nmwxrx6mv13bh7vn0qf6i0aw0xi"; + }; + + buildInputs = [ makeWrapper ]; + + phases = [ "unpackPhase" "installPhase" "fixupPhase" ]; + + installPhase = '' + mkdir -p $out/share + cp -r * $out/share + mkdir $out/bin + makeWrapper $out/share/workcraft $out/bin/workcraft \ + --set JAVA_HOME "${jre}" \ + --set _JAVA_OPTIONS '-Dawt.useSystemAAFontSettings=gasp'; + ''; + + 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 ]; + inherit version; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/yices/default.nix b/nixpkgs/pkgs/applications/science/logic/yices/default.nix new file mode 100644 index 000000000000..76ed934fb39e --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/yices/default.nix @@ -0,0 +1,44 @@ +{ stdenv, fetchFromGitHub, gmp-static, gperf, autoreconfHook, libpoly }: + +stdenv.mkDerivation rec { + pname = "yices"; + version = "2.6.1"; + + src = fetchFromGitHub { + owner = "SRI-CSL"; + repo = "yices2"; + rev = "Yices-${version}"; + sha256 = "04vf468spsh00jh7gj94cjnq8kjyfwy9l6r4z7l2pm0zgwkqgyhm"; + }; + + nativeBuildInputs = [ autoreconfHook ]; + buildInputs = [ gmp-static gperf libpoly ]; + configureFlags = + [ "--with-static-gmp=${gmp-static.out}/lib/libgmp.a" + "--with-static-gmp-include-dir=${gmp-static.dev}/include" + "--enable-mcsat" + ]; + + enableParallelBuilding = true; + doCheck = true; + + # Usual shenanigans + 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 = builtins.concatStringsSep "." (stdenv.lib.take 2 (stdenv.lib.splitString "." version)); + in '' + make install LDCONFIG=true + ln -sfr $out/lib/libyices.so.{${version},${ver_XdotY}} + ''; + + meta = with stdenv.lib; { + description = "A high-performance theorem prover and SMT solver"; + homepage = "http://yices.csl.sri.com"; + license = licenses.gpl3; + platforms = with platforms; linux ++ darwin; + maintainers = with maintainers; [ thoughtpolice ]; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/z3/default.nix b/nixpkgs/pkgs/applications/science/logic/z3/default.nix new file mode 100644 index 000000000000..14f75fb68b5e --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/z3/default.nix @@ -0,0 +1,42 @@ +{ stdenv, fetchFromGitHub, python, fixDarwinDylibNames }: + +stdenv.mkDerivation rec { + pname = "z3"; + version = "4.8.5"; + + src = fetchFromGitHub { + owner = "Z3Prover"; + repo = pname; + rev = "Z3-${version}"; + sha256 = "11sy98clv7ln0a5vqxzvh6wwqbswsjbik2084hav5kfws4xvklfa"; + }; + + buildInputs = [ python fixDarwinDylibNames ]; + propagatedBuildInputs = [ python.pkgs.setuptools ]; + enableParallelBuilding = true; + + configurePhase = '' + ${python.interpreter} scripts/mk_make.py --prefix=$out --python --pypkgdir=$out/${python.sitePackages} + cd build + ''; + + postInstall = '' + mkdir -p $dev $lib $python/lib + + mv $out/lib/python* $python/lib/ + mv $out/lib $lib/lib + mv $out/include $dev/include + + ln -sf $lib/lib/libz3${stdenv.hostPlatform.extensions.sharedLibrary} $python/${python.sitePackages}/z3/lib/libz3${stdenv.hostPlatform.extensions.sharedLibrary} + ''; + + outputs = [ "out" "lib" "dev" "python" ]; + + 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 = [ stdenv.lib.maintainers.thoughtpolice ]; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/z3/tptp.nix b/nixpkgs/pkgs/applications/science/logic/z3/tptp.nix new file mode 100644 index 000000000000..34449542abb2 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/z3/tptp.nix @@ -0,0 +1,31 @@ +{stdenv, z3, cmake}: +stdenv.mkDerivation rec { + pname = "z3-tptp"; + version = z3.version; + + src = z3.src; + + sourceRoot = "source/examples/tptp"; + + nativeBuildInputs = [cmake]; + buildInputs = [z3]; + + preConfigure = '' + echo 'set(Z3_LIBRARIES "-lz3")' >> CMakeLists.new + cat CMakeLists.txt | grep -E 'add_executable|project|link_libraries' >> CMakeLists.new + mv CMakeLists.new CMakeLists.txt + ''; + + installPhase = '' + mkdir -p "$out/bin" + cp "z3_tptp5" "$out/bin/" + ln -s "z3_tptp5" "$out/bin/z3-tptp" + ''; + + meta = { + inherit version; + inherit (z3.meta) license homepage platforms; + description = ''TPTP wrapper for Z3 prover''; + maintainers = [stdenv.lib.maintainers.raskin]; + }; +} |