diff options
Diffstat (limited to 'nixpkgs/pkgs/applications/science/logic')
91 files changed, 4176 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..6e7a3cfc88ac --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/abc/default.nix @@ -0,0 +1,31 @@ +{ fetchFromGitHub, stdenv, readline, cmake }: + +stdenv.mkDerivation rec { + name = "abc-verifier-${version}"; + 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..7d71a56fa23e --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/abella/default.nix @@ -0,0 +1,38 @@ +{ stdenv, fetchurl, rsync, ocamlPackages }: + +stdenv.mkDerivation rec { + name = "abella-${version}"; + version = "2.0.5"; + + src = fetchurl { + url = "http://abella-prover.org/distributions/${name}.tar.gz"; + sha256 = "0bry4pj6p9y7sg79ygdksynml4rdsjhqi959vnnwwsbaysa3bci0"; + }; + + 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..03524fc6b222 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/aiger/default.nix @@ -0,0 +1,55 @@ +{ stdenv, fetchurl, picosat }: + +stdenv.mkDerivation rec { + name = "aiger-${version}"; + version = "1.9.9"; + + src = fetchurl { + url = "http://fmv.jku.at/aiger/${name}.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..794430ebbe84 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/alt-ergo/default.nix @@ -0,0 +1,23 @@ +{ fetchurl, stdenv, ocamlPackages }: + +stdenv.mkDerivation rec { + name = "alt-ergo-${version}"; + version = "2.2.0"; + + src = fetchurl { + url = "https://alt-ergo.ocamlpro.com/download_manager.php?target=${name}.tar.gz"; + name = "${name}.tar.gz"; + sha256 = "106zfgisq6qxr7dlk8z7gi68ly7qff4frn8wab2g8z2nkkwla92w"; + }; + + buildInputs = with ocamlPackages; + [ ocaml findlib camlzip ocamlgraph zarith lablgtk ocplib-simplex psmt2-frontend menhir num ]; + + 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..bf8d3cf03b83 --- /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 rec { + 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..6c2d2f0a062f --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/avy/default.nix @@ -0,0 +1,53 @@ +{ stdenv, fetchgit, cmake, zlib, boost }: + +stdenv.mkDerivation rec { + name = "avy-${version}"; + 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..8e0ad22bba18 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/boolector/default.nix @@ -0,0 +1,50 @@ +{ stdenv, fetchFromGitHub +, cmake, lingeling, btor2tools +}: + +stdenv.mkDerivation rec { + name = "boolector-${version}"; + 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..ed3d9e638121 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/btor2tools/default.nix @@ -0,0 +1,33 @@ +{ stdenv, fetchFromGitHub }: + +stdenv.mkDerivation rec { + name = "btor2tools-${version}"; + 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..0817ebe0654b --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/cedille/default.nix @@ -0,0 +1,50 @@ +{ stdenv, lib, fetchFromGitHub, alex, happy, Agda, agdaIowaStdlib, + buildPlatform, buildPackages, ghcWithPackages, fetchpatch }: +let + options-patch = + fetchpatch { + url = https://github.com/cedille/cedille/commit/ee62b0fabde6c4f7299a3778868519255cc4a64f.patch; + name = "options.patch"; + sha256 = "19xzn9sqpfnfqikqy1x9lb9mb6722kbgvrapl6cf8ckcw8cfj8cz"; + }; +in +stdenv.mkDerivation rec { + version = "1.0.0"; + name = "cedille-${version}"; + src = fetchFromGitHub { + owner = "cedille"; + repo = "cedille"; + rev = "v${version}"; + sha256 = "08c2vgg8i6l3ws7hd5gsj89mki36lxm7x7s8hi1qa5gllq04a832"; + }; + buildInputs = [ alex happy Agda (ghcWithPackages (ps: [ps.ieee])) ]; + + patches = [options-patch]; + + LANG = "en_US.UTF-8"; + LOCALE_ARCHIVE = + lib.optionalString (buildPlatform.libc == "glibc") + "${buildPackages.glibcLocales}/lib/locale/locale-archive"; + + postPatch = '' + patchShebangs create-libraries.sh + cp -r ${agdaIowaStdlib.src} ial + chmod -R 755 ial + ''; + + outputs = ["out" "lib"]; + + installPhase = '' + mkdir -p $out/bin + mv cedille $out/bin/cedille + mv lib $lib + ''; + + meta = { + description = "An interactive theorem-prover and dependently typed programming language, based on extrinsic (aka Curry-style) type theory."; + homepage = https://cedille.github.io/; + license = stdenv.lib.licenses.mit; + maintainers = [ stdenv.lib.maintainers.mpickering ]; + platforms = stdenv.lib.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/coq/default.nix b/nixpkgs/pkgs/applications/science/logic/coq/default.nix new file mode 100644 index 000000000000..5fab9788a94a --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/coq/default.nix @@ -0,0 +1,151 @@ +# - 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 +, 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+beta1" = "1yxv2klqal3mh6symi3gc6gv3xm684zlld2c0b6ijhjmp865cin8"; + }."${version}"; + coq-version = builtins.substring 0 3 version; + ideFlags = if buildIde then "-lablgtkdir ${ocamlPackages.lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt" else ""; + 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 { + name = "coq-${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.optional buildIde 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 = '' + 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..d76462ca9380 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/coq2html/default.nix @@ -0,0 +1,38 @@ +{ stdenv, fetchgit, ocaml }: + +let + version = "20170720"; +in + +stdenv.mkDerivation { + name = "coq2html-${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..4d96339149af --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/cryptominisat/default.nix @@ -0,0 +1,30 @@ +{ stdenv, fetchFromGitHub, fetchpatch, cmake, python, xxd }: + +stdenv.mkDerivation rec { + name = "cryptominisat-${version}"; + version = "5.0.1"; + + src = fetchFromGitHub { + owner = "msoos"; + repo = "cryptominisat"; + rev = version; + sha256 = "0cpw5d9vplxvv3aaplhnga55gz1hy29p7s4pkw1306knkbhlzvkb"; + }; + + buildInputs = [ python xxd ]; + nativeBuildInputs = [ cmake ]; + + patches = [(fetchpatch rec { + name = "fix-exported-library-name.patch"; + url = "https://github.com/msoos/cryptominisat/commit/7a47795cbe5ad5a899731102d297f234bcade077.patch"; + sha256 = "11hf3cfqs4cykn7rlgjglq29lzqfxvlm0f20qasi0kdrz01cr30f"; + })]; + + 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..df9e58af08bb --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/cryptoverif/default.nix @@ -0,0 +1,37 @@ +{ stdenv, fetchurl, ocaml }: + +stdenv.mkDerivation rec { + name = "cryptoverif-${version}"; + version = "2.00"; + + src = fetchurl { + url = "http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/cryptoverif${version}.tar.gz"; + sha256 = "0g8pkj58b48zk4c0sgpln0qhbj82v75mz3w6cl3w5bvmxsbkwvy1"; + }; + + 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 = "http://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..91eaaeeb0e40 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/cubicle/default.nix @@ -0,0 +1,24 @@ +{ stdenv, fetchurl, ocamlPackages }: + +stdenv.mkDerivation rec { + name = "cubicle-${version}"; + 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..703ce6fd5086 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/cvc3/default.nix @@ -0,0 +1,34 @@ +{ stdenv, fetchurl, flex, bison, gmp, perl }: + +stdenv.mkDerivation rec { + name = "cvc3-${version}"; + version = "2.4.1"; + + src = fetchurl { + url = "http://www.cs.nyu.edu/acsys/cvc3/releases/${version}/${name}.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..cddcbef7a035 --- /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 { + name = "cvc4-${version}"; + 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..50454847baf1 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/drat-trim/default.nix @@ -0,0 +1,40 @@ +{ stdenv, fetchFromGitHub }: + +stdenv.mkDerivation rec { + 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..f0b912c57fc5 --- /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 { + name = "elan-${version}"; + version = "0.7.1"; + + cargoSha256 = "0vv7kr7rc3lvas7ngp5dp99ajjd5v8k5937ish7zqz1k4970q2f1"; + + src = fetchFromGitHub { + owner = "kha"; + repo = "elan"; + rev = "v${version}"; + sha256 = "0x5s1wm78yx5ci63wrmlkzm6k3281p33gn4dzw25k5s4vx0p9n24"; + }; + + 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..4d8e7b17b2bc --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/eprover/default.nix @@ -0,0 +1,29 @@ +{ stdenv, fetchurl, which }: + +stdenv.mkDerivation rec { + name = "eprover-${version}"; + version = "2.2"; + + src = fetchurl { + url = "https://wwwlehre.dhbw-stuttgart.de/~sschulz/WORK/E_DOWNLOAD/V_${version}/E.tgz"; + sha256 = "08ihpwgkz0l7skr42iw8lm202kqr51i792bs61qsbnk9gsjlab1c"; + }; + + 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/gappa/default.nix b/nixpkgs/pkgs/applications/science/logic/gappa/default.nix new file mode 100644 index 000000000000..71114d2f9e12 --- /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.2"; + + src = fetchurl { + url = https://gforge.inria.fr/frs/download.php/file/34787/gappa-1.2.0.tar.gz; + sha256 = "03hfzmaf5jm54sjpbks20q7qixpmagrfbnyyc276vgmiyslk4dkh"; + }; + + 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..bc8d372ce42c --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/glucose/default.nix @@ -0,0 +1,29 @@ +{ stdenv, fetchurl, zlib }: +stdenv.mkDerivation rec { + name = "glucose-${version}"; + 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/${name}/" + install -Dm0755 ../{LICEN?E,README*,Changelog*} "$out/share/doc/${name}/" + ''; + + 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..30af3216737c --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/glucose/syrup.nix @@ -0,0 +1,24 @@ +{ stdenv, zlib, glucose }: +stdenv.mkDerivation rec { + name = "glucose-syrup-${version}"; + 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/${name}/" + install -Dm0755 ../{LICEN?E,README*,Changelog*} "$out/share/doc/${name}/" + ''; + + 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..91be7dca1173 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/hol_light/default.nix @@ -0,0 +1,50 @@ +{ stdenv, 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 = + '' + #!/bin/sh + 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-2018-09-30"; + + src = fetchFromGitHub { + owner = "jrh13"; + repo = "hol-light"; + rev = "27e09dd27834de46e917057710e9d8ded51a4c9f"; + sha256 = "1p0rm08wnc2lsrh3xzhlq3zdhzqcv1lbqnkwx3aybrqhbg1ixc1d"; + }; + + 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..d3950349711b --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/iprover/default.nix @@ -0,0 +1,33 @@ +{ stdenv, fetchurl, ocaml, eprover, zlib }: + +stdenv.mkDerivation rec { + name = "iprover-${version}"; + 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/${name}" + cp *.p "$out/share/${name}" + echo -e "#! /bin/sh\\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..ffe508569553 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/isabelle/default.nix @@ -0,0 +1,77 @@ +{ stdenv, fetchurl, perl, nettools, java, polyml, z3 }: +# nettools needed for hostname + +let + dirname = "Isabelle2017"; +in + +stdenv.mkDerivation { + name = "isabelle-2017"; + inherit dirname; + + src = if stdenv.isDarwin + then fetchurl { + url = "http://isabelle.in.tum.de/website-${dirname}/dist/${dirname}.dmg"; + sha256 = "1awgg39i72pivwfijdwffvil3glnpimjz2x04qbl5la2j6la48nb"; + } + else fetchurl { + url = "https://isabelle.in.tum.de/website-${dirname}/dist/${dirname}_linux.tar.gz"; + sha256 = "01v1zrajyfamjq5b8v18qr3ffivjckifsvvx2vs13di6wsnmm9gw"; + }; + + buildInputs = [ perl polyml z3 ] + ++ stdenv.lib.optionals (!stdenv.isDarwin) [ nettools java ]; + + sourceRoot = dirname; + + postPatch = '' + ENV=$(type -p env) + patchShebangs "." + substituteInPlace lib/Tools/env \ + --replace /usr/bin/env $ENV + substituteInPlace lib/Tools/install \ + --replace /usr/bin/env $ENV + sed -i 's|isabelle_java java|${java}/bin/java|g' lib/Tools/java + substituteInPlace etc/settings \ + --subst-var-by ML_HOME "${polyml}/bin" + substituteInPlace contrib/jdk/etc/settings \ + --replace ISABELLE_JDK_HOME= '#ISABELLE_JDK_HOME=' + substituteInPlace contrib/polyml-*/etc/settings \ + --replace '$POLYML_HOME/$ML_PLATFORM' ${polyml}/bin \ + --replace '$POLYML_HOME/$PLATFORM/polyml' ${polyml}/bin/poly + substituteInPlace lib/scripts/run-polyml* lib/scripts/polyml-version \ + --replace '$ML_HOME/poly' ${polyml}/bin/poly + substituteInPlace contrib/z3*/etc/settings \ + --replace '$Z3_HOME/z3' '${z3}/bin/z3' + + for comp in contrib/jdk contrib/polyml*; 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..a95d1201cbd6 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/jonprl/default.nix @@ -0,0 +1,34 @@ +{ fetchgit, stdenv, smlnj, which }: + +stdenv.mkDerivation rec { + name = "jonprl-${version}"; + 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..d7f047b84e0f --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/lci/default.nix @@ -0,0 +1,16 @@ +{stdenv, fetchurl, readline}: +stdenv.mkDerivation rec { + version = "0.6"; + name = "lci-${version}"; + src = fetchurl { + url = "mirror://sourceforge/lci/${name}.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..16fdab59ea02 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/lean/default.nix @@ -0,0 +1,29 @@ +{ stdenv, fetchFromGitHub, cmake, gmp }: + +stdenv.mkDerivation rec { + name = "lean-${version}"; + version = "3.4.1"; + + src = fetchFromGitHub { + owner = "leanprover"; + repo = "lean"; + rev = "v${version}"; + sha256 = "0ww8azlyy3xikhd7nh96f507sg23r53zvayij1mwv5513vmblhhw"; + }; + + nativeBuildInputs = [ cmake ]; + buildInputs = [ gmp ]; + enableParallelBuilding = true; + + preConfigure = '' + cd src + ''; + + meta = with stdenv.lib; { + description = "Automatic and interactive theorem prover"; + homepage = "http://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..4e1415d3961d --- /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 rec { + name = "lean2-${version}"; + 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..be337a1c258e --- /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 { + name = "leo2-${version}"; + 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/lingeling/default.nix b/nixpkgs/pkgs/applications/science/logic/lingeling/default.nix new file mode 100644 index 000000000000..000587a22e67 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/lingeling/default.nix @@ -0,0 +1,49 @@ +{ stdenv, fetchFromGitHub +, aiger +}: + +stdenv.mkDerivation rec { + name = "lingeling-${version}"; + # 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..db784237ea91 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/logisim/default.nix @@ -0,0 +1,28 @@ +{ stdenv, fetchurl, jre, makeWrapper }: + +let version = "2.7.1"; in + +stdenv.mkDerivation { + name = "logisim-${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..c77e0327fb6b --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/ltl2ba/default.nix @@ -0,0 +1,31 @@ +{ fetchurl, stdenv }: + +stdenv.mkDerivation rec { + name = "ltl2ba-${version}"; + version = "1.2"; + + src = fetchurl { + url = "http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/${name}.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..dc32e84279a8 --- /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"; + name = "mcrl2-${version}"; + + 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..1601a74e1899 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/metis-prover/default.nix @@ -0,0 +1,32 @@ +{ stdenv, fetchFromGitHub, perl, mlton }: + +stdenv.mkDerivation rec { + name = "metis-prover-${version}"; + 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..4b2116680d50 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/minisat/default.nix @@ -0,0 +1,32 @@ +{ stdenv, fetchurl, zlib }: + +stdenv.mkDerivation rec { + name = "minisat-${version}"; + version = "2.2.0"; + + src = fetchurl { + url = "http://minisat.se/downloads/${name}.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..f1a42f8215e3 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/minisat/unstable.nix @@ -0,0 +1,23 @@ +{ stdenv, fetchFromGitHub, zlib, cmake }: + +stdenv.mkDerivation rec { + 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..54bedc7c5e97 --- /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 rec { + 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..48546a86112b --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/open-wbo/default.nix @@ -0,0 +1,27 @@ +{ stdenv, fetchFromGitHub, zlib, gmp }: + +stdenv.mkDerivation rec { + 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..f9f021b15f07 --- /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 { + name = "opensmt-${version}"; + 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..d21487ef92fa --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/ott/default.nix @@ -0,0 +1,44 @@ +{ stdenv, fetchFromGitHub, pkgconfig, ocaml }: + +stdenv.mkDerivation rec { + name = "ott-${version}"; + 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..b19650eb8630 --- /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 = "http://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/picosat/default.nix b/nixpkgs/pkgs/applications/science/logic/picosat/default.nix new file mode 100644 index 000000000000..638996e853b8 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/picosat/default.nix @@ -0,0 +1,44 @@ +{ stdenv, fetchurl }: + +stdenv.mkDerivation rec { + name = "picosat-${version}"; + version = "965"; + + src = fetchurl { + url = "http://fmv.jku.at/picosat/${name}.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..2f765572f9ad --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/poly/default.nix @@ -0,0 +1,25 @@ +{stdenv, fetchFromGitHub, gmp, cmake, python}: + +stdenv.mkDerivation rec { + name = "${pname}-${version}"; + 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..4abfdf9162c0 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/potassco/clingo.nix @@ -0,0 +1,27 @@ +{ stdenv, fetchzip, cmake }: + +stdenv.mkDerivation rec { + name = "${pname}-${version}"; + 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..1f6620a2872d --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/prooftree/default.nix @@ -0,0 +1,43 @@ +{ stdenv, fetchurl, pkgconfig, ncurses, ocamlPackages }: + +stdenv.mkDerivation rec { + name = "prooftree-${version}"; + 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..f96532b7038b --- /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 = http://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..c70ee610199f --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/proverif/default.nix @@ -0,0 +1,28 @@ +{ stdenv, fetchurl, ocamlPackages }: + +stdenv.mkDerivation rec { + name = "proverif-${version}"; + 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 = "http://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..426f1928938c --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/sad/default.nix @@ -0,0 +1,39 @@ +{ stdenv, fetchurl, ghc, 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 = [ ghc 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/sapic/default.nix b/nixpkgs/pkgs/applications/science/logic/sapic/default.nix new file mode 100644 index 000000000000..27efe865a9d9 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/sapic/default.nix @@ -0,0 +1,28 @@ +{ stdenv, fetchurl, unzip, ocaml }: + +stdenv.mkDerivation rec { + name = "sapic-${version}"; + version = "0.9"; + + src = fetchurl { + url = "http://sapic.gforge.inria.fr/${name}.zip"; + sha256 = "1ckl090lpyfh90mkjhnpcys5grs3nrl9wlbn9nfkxxnaivn2yx9y"; + }; + + nativeBuildInputs = [ unzip ]; + buildInputs = [ ocaml ]; + patches = [ ./native.patch ]; # create a native binary, not a bytecode one + + buildPhase = "make depend && make"; + installPhase = '' + mkdir -p $out/bin + cp ./sapic $out/bin + ''; + + meta = { + description = "Stateful applied Pi Calculus for protocol verification"; + homepage = http://sapic.gforge.inria.fr/; + platforms = stdenv.lib.platforms.unix; + maintainers = [ stdenv.lib.maintainers.thoughtpolice ]; + }; +} diff --git a/nixpkgs/pkgs/applications/science/logic/sapic/native.patch b/nixpkgs/pkgs/applications/science/logic/sapic/native.patch new file mode 100644 index 000000000000..6e0b98113df2 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/sapic/native.patch @@ -0,0 +1,38 @@ +diff --git a/Makefile b/Makefile +index a1de94d..f9e2eb8 100644 +--- a/Makefile ++++ b/Makefile +@@ -1,8 +1,8 @@ + TARGET = sapic +-OBJS=lexer.cmo apip.cmo firsttranslation.cmo main.cmo #secondtranslation.cmo thirdtranslation.cmo main.cmo ++OBJS=lexer.cmx apip.cmx firsttranslation.cmx main.cmx + + sapic: $(OBJS) +- ocamlc -o $@ $(OBJS) ++ ocamlopt.opt -o $@ $(OBJS) + + depend: + ocamldep *.ml *.mli > .depend +@@ -13,17 +13,17 @@ clean: + rm -rf *.cmi *.cmo $(TARGET) + rm -rf apip.ml apip.mli lexer.ml lexer.mli + +-.SUFFIXES: .ml .mli .mll .mly .cmo .cmi ++.SUFFIXES: .ml .mli .mll .mly .cmo .cmi .cmx + +-.ml.cmo: +- ocamlc -c $< ++.ml.cmx: ++ ocamlopt.opt -c $< + .mli.cmi: +- ocamlc -c $< ++ ocamlopt.opt -c $< + .mll.ml: + ocamllex $< + .mly.ml: + ocamlyacc $< + .ml.mli: +- ocamlc -i $< > $@ ++ ocamlopt.opt -i $< > $@ + + -include .depend 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..b9dd90f601f5 --- /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 { + name = "satallax-${version}"; + version = "2.7"; + + buildInputs = [ocaml zlib which eprover makeWrapper coq]; + src = fetchurl { + url = "https://www.ps.uni-saarland.de/~cebrown/satallax/downloads/${name}.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..32ebdad51d94 --- /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 rec { + name = "saw-tools-${version}"; + 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..2bb2b911d491 --- /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 rec { + name = "spass-${version}"; + 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..9e51849a93b9 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/statverif/default.nix @@ -0,0 +1,34 @@ +{ stdenv, fetchurl, ocaml }: + +stdenv.mkDerivation rec { + name = "statverif-${version}"; + 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 = "http://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..081dc788163b --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/stp/default.nix @@ -0,0 +1,36 @@ +{ stdenv, cmake, boost, bison, flex, fetchFromGitHub, perl, python3, python3Packages, zlib, minisatUnstable, cryptominisat }: + +stdenv.mkDerivation rec { + version = "2.2.0"; + name = "stp-${version}"; + + src = fetchFromGitHub { + owner = "stp"; + repo = "stp"; + rev = "stp-${version}"; + sha256 = "1jh23wjm62nnqfx447g2y53bbangq04hjrvqc35v9xxpcjgj3i49"; + }; + + 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" + ) + ''; + + # `make -f lib/Interface/CMakeFiles/cppinterface.dir/build.make lib/Interface/CMakeFiles/cppinterface.dir/cpp_interface.cpp.o`: + # include/stp/AST/UsefulDefs.h:41:29: fatal error: stp/AST/ASTKind.h: No such file or directory + enableParallelBuilding = false; + + 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..e21c274370c8 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/symbiyosys/default.nix @@ -0,0 +1,37 @@ +{ stdenv, fetchFromGitHub, yosys, python3 }: + +stdenv.mkDerivation rec { + name = "symbiyosys-${version}"; + version = "2018.09.12"; + + src = fetchFromGitHub { + owner = "yosyshq"; + repo = "symbiyosys"; + rev = "e90bcb588e97118af0cdba23fae562fb0efbf294"; + sha256 = "16nlimpdc3g6lghwqpyirgrr1d9mgk4wg3c06fvglzaicvjixnfr"; + }; + + 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}\"]]" + ''; + meta = { + description = "Tooling for Yosys-based verification flows"; + homepage = https://symbiyosys.readthedocs.io/; + license = stdenv.lib.licenses.mit; + maintainers = with stdenv.lib.maintainers; [ thoughtpolice ]; + platforms = stdenv.lib.platforms.unix; + }; +} 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..9056eab71ea3 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/tamarin-prover/default.nix @@ -0,0 +1,102 @@ +{ haskellPackages, mkDerivation, fetchFromGitHub, lib +# the following are non-haskell dependencies +, makeWrapper, which, maude, graphviz, sapic +}: + +let + version = "1.4.0"; + src = fetchFromGitHub { + owner = "tamarin-prover"; + repo = "tamarin-prover"; + rev = "7ced07a69f8e93178f9a95797479277a736ae572"; + sha256 = "02pyw22h90228g6qybjpdvpcm9d5lh96f5qwmy2hv2bylz05z3nn"; + }; + + # 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; + patches = [ ./ghc-8.4-support-utils.patch ]; + 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; + patches = [ ./ghc-8.4-support-term.patch ]; + 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; + patches = [ ./ghc-8.4-support-theory.patch ]; + 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 + ''; + + # wrap the prover to be sure it can find maude, sapic, etc + executableToolDepends = [ makeWrapper which maude graphviz sapic ]; + postInstall = '' + wrapProgram $out/bin/tamarin-prover \ + --prefix PATH : ${lib.makeBinPath [ which maude graphviz sapic ]} + # 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 + ''; + + checkPhase = "./dist/build/tamarin-prover/tamarin-prover test"; + + 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/ghc-8.4-support-term.patch b/nixpkgs/pkgs/applications/science/logic/tamarin-prover/ghc-8.4-support-term.patch new file mode 100644 index 000000000000..f93919faf54e --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/tamarin-prover/ghc-8.4-support-term.patch @@ -0,0 +1,109 @@ +From a08f6e400772899b9b0fc16befc50391cd70696b Mon Sep 17 00:00:00 2001 +From: Felix Yan <felixonmars@archlinux.org> +Date: Fri, 18 May 2018 16:24:41 +0800 +Subject: [PATCH] GHC 8.4 support + +--- + src/Term/Maude/Signature.hs | 8 ++-- + src/Term/Rewriting/Definitions.hs | 23 ++++++---- + src/Term/Unification.hs | 4 +- + 11 files changed, 79 insertions(+), 48 deletions(-) + +diff --git a/src/Term/Maude/Signature.hs b/src/Term/Maude/Signature.hs +index 98c25d9f..1a4ce82f 100644 +--- a/src/Term/Maude/Signature.hs ++++ b/src/Term/Maude/Signature.hs +@@ -104,9 +104,9 @@ maudeSig msig@(MaudeSig {enableDH,enableBP,enableMSet,enableXor,enableDiff=_,stF + `S.union` dhReducibleFunSig `S.union` bpReducibleFunSig `S.union` xorReducibleFunSig + + -- | A monoid instance to combine maude signatures. +-instance Monoid MaudeSig where +- (MaudeSig dh1 bp1 mset1 xor1 diff1 stFunSyms1 stRules1 _ _) `mappend` +- (MaudeSig dh2 bp2 mset2 xor2 diff2 stFunSyms2 stRules2 _ _) = ++instance Semigroup MaudeSig where ++ MaudeSig dh1 bp1 mset1 xor1 diff1 stFunSyms1 stRules1 _ _ <> ++ MaudeSig dh2 bp2 mset2 xor2 diff2 stFunSyms2 stRules2 _ _ = + maudeSig (mempty {enableDH=dh1||dh2 + ,enableBP=bp1||bp2 + ,enableMSet=mset1||mset2 +@@ -114,6 +114,8 @@ instance Monoid MaudeSig where + ,enableDiff=diff1||diff2 + ,stFunSyms=S.union stFunSyms1 stFunSyms2 + ,stRules=S.union stRules1 stRules2}) ++ ++instance Monoid MaudeSig where + mempty = MaudeSig False False False False False S.empty S.empty S.empty S.empty + + -- | Non-AC function symbols. +diff --git a/src/Term/Rewriting/Definitions.hs b/src/Term/Rewriting/Definitions.hs +index bd942b6a..18562e4e 100644 +--- a/src/Term/Rewriting/Definitions.hs ++++ b/src/Term/Rewriting/Definitions.hs +@@ -44,10 +44,12 @@ evalEqual (Equal l r) = l == r + instance Functor Equal where + fmap f (Equal lhs rhs) = Equal (f lhs) (f rhs) + ++instance Semigroup a => Semigroup (Equal a) where ++ (Equal l1 r1) <> (Equal l2 r2) = ++ Equal (l1 <> l2) (r1 <> r2) ++ + instance Monoid a => Monoid (Equal a) where + mempty = Equal mempty mempty +- (Equal l1 r1) `mappend` (Equal l2 r2) = +- Equal (l1 `mappend` l2) (r1 `mappend` r2) + + instance Foldable Equal where + foldMap f (Equal l r) = f l `mappend` f r +@@ -104,14 +106,15 @@ instance Functor Match where + fmap _ NoMatch = NoMatch + fmap f (DelayedMatches ms) = DelayedMatches (fmap (f *** f) ms) + ++instance Semigroup (Match a) where ++ NoMatch <> _ = NoMatch ++ _ <> NoMatch = NoMatch ++ DelayedMatches ms1 <> DelayedMatches ms2 = ++ DelayedMatches (ms1 <> ms2) ++ + instance Monoid (Match a) where + mempty = DelayedMatches [] + +- NoMatch `mappend` _ = NoMatch +- _ `mappend` NoMatch = NoMatch +- DelayedMatches ms1 `mappend` DelayedMatches ms2 = +- DelayedMatches (ms1 `mappend` ms2) +- + + instance Foldable Match where + foldMap _ NoMatch = mempty +@@ -136,10 +139,12 @@ data RRule a = RRule a a + instance Functor RRule where + fmap f (RRule lhs rhs) = RRule (f lhs) (f rhs) + ++instance Monoid a => Semigroup (RRule a) where ++ (RRule l1 r1) <> (RRule l2 r2) = ++ RRule (l1 <> l2) (r1 <> r2) ++ + instance Monoid a => Monoid (RRule a) where + mempty = RRule mempty mempty +- (RRule l1 r1) `mappend` (RRule l2 r2) = +- RRule (l1 `mappend` l2) (r1 `mappend` r2) + + instance Foldable RRule where + foldMap f (RRule l r) = f l `mappend` f r +diff --git a/src/Term/Unification.hs b/src/Term/Unification.hs +index e1de0163..7ce6bb41 100644 +--- a/src/Term/Unification.hs ++++ b/src/Term/Unification.hs +@@ -265,9 +265,11 @@ unifyRaw l0 r0 = do + + data MatchFailure = NoMatcher | ACProblem + ++instance Semigroup MatchFailure where ++ _ <> _ = NoMatcher ++ + instance Monoid MatchFailure where + mempty = NoMatcher +- mappend _ _ = NoMatcher + + -- | Ensure that the computed substitution @sigma@ satisfies + -- @t ==_AC apply sigma p@ after the delayed equations are solved. diff --git a/nixpkgs/pkgs/applications/science/logic/tamarin-prover/ghc-8.4-support-theory.patch b/nixpkgs/pkgs/applications/science/logic/tamarin-prover/ghc-8.4-support-theory.patch new file mode 100644 index 000000000000..f7393e37f1b2 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/tamarin-prover/ghc-8.4-support-theory.patch @@ -0,0 +1,130 @@ +From a08f6e400772899b9b0fc16befc50391cd70696b Mon Sep 17 00:00:00 2001 +From: Felix Yan <felixonmars@archlinux.org> +Date: Fri, 18 May 2018 16:24:41 +0800 +Subject: [PATCH] GHC 8.4 support + +--- + src/Theory/Proof.hs | 43 +++++++++++-------- + 11 files changed, 79 insertions(+), 48 deletions(-) + +diff --git a/src/Theory/Constraint/Solver/Reduction.hs b/src/Theory/Constraint/Solver/Reduction.hs +index ddbc965a..6daadd0d 100644 +--- a/src/Theory/Constraint/Solver/Reduction.hs ++++ b/src/Theory/Constraint/Solver/Reduction.hs +@@ -139,13 +139,14 @@ execReduction m ctxt se fs = + data ChangeIndicator = Unchanged | Changed + deriving( Eq, Ord, Show ) + ++instance Semigroup ChangeIndicator where ++ Changed <> _ = Changed ++ _ <> Changed = Changed ++ Unchanged <> Unchanged = Unchanged ++ + instance Monoid ChangeIndicator where + mempty = Unchanged + +- Changed `mappend` _ = Changed +- _ `mappend` Changed = Changed +- Unchanged `mappend` Unchanged = Unchanged +- + -- | Return 'True' iff there was a change. + wasChanged :: ChangeIndicator -> Bool + wasChanged Changed = True +diff --git a/src/Theory/Constraint/System/Guarded.hs b/src/Theory/Constraint/System/Guarded.hs +index f98fc7c2..2aac8ce2 100644 +--- a/src/Theory/Constraint/System/Guarded.hs ++++ b/src/Theory/Constraint/System/Guarded.hs +@@ -435,7 +435,7 @@ gall ss atos gf = GGuarded All ss atos gf + + -- | Local newtype to avoid orphan instance. + newtype ErrorDoc d = ErrorDoc { unErrorDoc :: d } +- deriving( Monoid, NFData, Document, HighlightDocument ) ++ deriving( Monoid, Semigroup, NFData, Document, HighlightDocument ) + + -- | @formulaToGuarded fm@ returns a guarded formula @gf@ that is + -- equivalent to @fm@ under the assumption that this is possible. +diff --git a/src/Theory/Proof.hs b/src/Theory/Proof.hs +index 74fb77b1..7971b9fc 100644 +--- a/src/Theory/Proof.hs ++++ b/src/Theory/Proof.hs +@@ -388,17 +388,19 @@ data ProofStatus = + | TraceFound -- ^ There is an annotated solved step + deriving ( Show, Generic, NFData, Binary ) + ++instance Semigroup ProofStatus where ++ TraceFound <> _ = TraceFound ++ _ <> TraceFound = TraceFound ++ IncompleteProof <> _ = IncompleteProof ++ _ <> IncompleteProof = IncompleteProof ++ _ <> CompleteProof = CompleteProof ++ CompleteProof <> _ = CompleteProof ++ UndeterminedProof <> UndeterminedProof = UndeterminedProof ++ ++ + instance Monoid ProofStatus where + mempty = CompleteProof + +- mappend TraceFound _ = TraceFound +- mappend _ TraceFound = TraceFound +- mappend IncompleteProof _ = IncompleteProof +- mappend _ IncompleteProof = IncompleteProof +- mappend _ CompleteProof = CompleteProof +- mappend CompleteProof _ = CompleteProof +- mappend UndeterminedProof UndeterminedProof = UndeterminedProof +- + -- | The status of a 'ProofStep'. + proofStepStatus :: ProofStep (Maybe a) -> ProofStatus + proofStepStatus (ProofStep _ Nothing ) = UndeterminedProof +@@ -560,10 +562,12 @@ newtype Prover = Prover + -> Maybe IncrementalProof -- resulting proof + } + ++instance Semigroup Prover where ++ p1 <> p2 = Prover $ \ctxt d se -> ++ runProver p1 ctxt d se >=> runProver p2 ctxt d se ++ + instance Monoid Prover where + mempty = Prover $ \_ _ _ -> Just +- p1 `mappend` p2 = Prover $ \ctxt d se -> +- runProver p1 ctxt d se >=> runProver p2 ctxt d se + + -- | Provers whose sequencing is handled via the 'Monoid' instance. + -- +@@ -579,10 +583,12 @@ newtype DiffProver = DiffProver + -> Maybe IncrementalDiffProof -- resulting proof + } + ++instance Semigroup DiffProver where ++ p1 <> p2 = DiffProver $ \ctxt d se -> ++ runDiffProver p1 ctxt d se >=> runDiffProver p2 ctxt d se ++ + instance Monoid DiffProver where + mempty = DiffProver $ \_ _ _ -> Just +- p1 `mappend` p2 = DiffProver $ \ctxt d se -> +- runDiffProver p1 ctxt d se >=> runDiffProver p2 ctxt d se + + -- | Map the proof generated by the prover. + mapProverProof :: (IncrementalProof -> IncrementalProof) -> Prover -> Prover +@@ -784,15 +790,16 @@ runAutoDiffProver (AutoProver heuristic bound cut) = + -- | The result of one pass of iterative deepening. + data IterDeepRes = NoSolution | MaybeNoSolution | Solution ProofPath + ++instance Semigroup IterDeepRes where ++ x@(Solution _) <> _ = x ++ _ <> y@(Solution _) = y ++ MaybeNoSolution <> _ = MaybeNoSolution ++ _ <> MaybeNoSolution = MaybeNoSolution ++ NoSolution <> NoSolution = NoSolution ++ + instance Monoid IterDeepRes where + mempty = NoSolution + +- x@(Solution _) `mappend` _ = x +- _ `mappend` y@(Solution _) = y +- MaybeNoSolution `mappend` _ = MaybeNoSolution +- _ `mappend` MaybeNoSolution = MaybeNoSolution +- NoSolution `mappend` NoSolution = NoSolution +- + -- | @cutOnSolvedDFS prf@ removes all other cases if an attack is found. The + -- attack search is performed using a parallel DFS traversal with iterative + -- deepening. diff --git a/nixpkgs/pkgs/applications/science/logic/tamarin-prover/ghc-8.4-support-utils.patch b/nixpkgs/pkgs/applications/science/logic/tamarin-prover/ghc-8.4-support-utils.patch new file mode 100644 index 000000000000..d6cd6d73f99e --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/tamarin-prover/ghc-8.4-support-utils.patch @@ -0,0 +1,140 @@ +From a08f6e400772899b9b0fc16befc50391cd70696b Mon Sep 17 00:00:00 2001 +From: Felix Yan <felixonmars@archlinux.org> +Date: Fri, 18 May 2018 16:24:41 +0800 +Subject: [PATCH] GHC 8.4 support + +--- + src/Extension/Data/Bounded.hs | 10 ++++- + src/Extension/Data/Monoid.hs | 14 +++--- + src/Logic/Connectives.hs | 4 +- + src/Text/PrettyPrint/Class.hs | 4 +- + src/Text/PrettyPrint/Html.hs | 6 ++- + 11 files changed, 79 insertions(+), 48 deletions(-) + + +diff --git a/src/Extension/Data/Bounded.hs b/src/Extension/Data/Bounded.hs +index 5f166006..f416a44c 100644 +--- a/src/Extension/Data/Bounded.hs ++++ b/src/Extension/Data/Bounded.hs +@@ -11,19 +11,25 @@ module Extension.Data.Bounded ( + ) where + + -- import Data.Monoid ++import Data.Semigroup + + -- | A newtype wrapper for a monoid of the maximum of a bounded type. + newtype BoundedMax a = BoundedMax {getBoundedMax :: a} + deriving( Eq, Ord, Show ) + ++instance (Ord a, Bounded a) => Semigroup (BoundedMax a) where ++ BoundedMax x <> BoundedMax y = BoundedMax (max x y) ++ + instance (Ord a, Bounded a) => Monoid (BoundedMax a) where + mempty = BoundedMax minBound +- (BoundedMax x) `mappend` (BoundedMax y) = BoundedMax (max x y) ++ mappend = (<>) + + -- | A newtype wrapper for a monoid of the minimum of a bounded type. + newtype BoundedMin a = BoundedMin {getBoundedMin :: a} + deriving( Eq, Ord, Show ) + ++instance (Ord a, Bounded a) => Semigroup (BoundedMin a) where ++ BoundedMin x <> BoundedMin y = BoundedMin (min x y) ++ + instance (Ord a, Bounded a) => Monoid (BoundedMin a) where + mempty = BoundedMin maxBound +- (BoundedMin x) `mappend` (BoundedMin y) = BoundedMin (min x y) +\ No newline at end of file +diff --git a/src/Extension/Data/Monoid.hs b/src/Extension/Data/Monoid.hs +index 83655c34..9ce2f91b 100644 +--- a/src/Extension/Data/Monoid.hs ++++ b/src/Extension/Data/Monoid.hs +@@ -18,6 +18,7 @@ module Extension.Data.Monoid ( + ) where + + import Data.Monoid ++import Data.Semigroup + + #if __GLASGOW_HASKELL__ < 704 + +@@ -38,10 +39,13 @@ newtype MinMax a = MinMax { getMinMax :: Maybe (a, a) } + minMaxSingleton :: a -> MinMax a + minMaxSingleton x = MinMax (Just (x, x)) + ++instance Ord a => Semigroup (MinMax a) where ++ MinMax Nothing <> y = y ++ x <> MinMax Nothing = x ++ MinMax (Just (xMin, xMax)) <> MinMax (Just (yMin, yMax)) = ++ MinMax (Just (min xMin yMin, max xMax yMax)) ++ ++ + instance Ord a => Monoid (MinMax a) where + mempty = MinMax Nothing +- +- MinMax Nothing `mappend` y = y +- x `mappend` MinMax Nothing = x +- MinMax (Just (xMin, xMax)) `mappend` MinMax (Just (yMin, yMax)) = +- MinMax (Just (min xMin yMin, max xMax yMax)) ++ mappend = (<>) +diff --git a/src/Logic/Connectives.hs b/src/Logic/Connectives.hs +index 2e441172..7206cc2c 100644 +--- a/src/Logic/Connectives.hs ++++ b/src/Logic/Connectives.hs +@@ -23,12 +23,12 @@ import Control.DeepSeq + + -- | A conjunction of atoms of type a. + newtype Conj a = Conj { getConj :: [a] } +- deriving (Monoid, Foldable, Traversable, Eq, Ord, Show, Binary, ++ deriving (Monoid, Semigroup, Foldable, Traversable, Eq, Ord, Show, Binary, + Functor, Applicative, Monad, Alternative, MonadPlus, Typeable, Data, NFData) + + -- | A disjunction of atoms of type a. + newtype Disj a = Disj { getDisj :: [a] } +- deriving (Monoid, Foldable, Traversable, Eq, Ord, Show, Binary, ++ deriving (Monoid, Semigroup, Foldable, Traversable, Eq, Ord, Show, Binary, + Functor, Applicative, Monad, Alternative, MonadPlus, Typeable, Data, NFData) + + instance MonadDisj Disj where +diff --git a/src/Text/PrettyPrint/Class.hs b/src/Text/PrettyPrint/Class.hs +index f5eb42fe..13be6515 100644 +--- a/src/Text/PrettyPrint/Class.hs ++++ b/src/Text/PrettyPrint/Class.hs +@@ -187,9 +187,11 @@ instance Document Doc where + nest i (Doc d) = Doc $ P.nest i d + caseEmptyDoc yes no (Doc d) = if P.isEmpty d then yes else no + ++instance Semigroup Doc where ++ Doc d1 <> Doc d2 = Doc $ (P.<>) d1 d2 ++ + instance Monoid Doc where + mempty = Doc $ P.empty +- mappend (Doc d1) (Doc d2) = Doc $ (P.<>) d1 d2 + + ------------------------------------------------------------------------------ + -- Additional combinators +diff --git a/src/Text/PrettyPrint/Html.hs b/src/Text/PrettyPrint/Html.hs +index 3de5e307..10103eb7 100644 +--- a/src/Text/PrettyPrint/Html.hs ++++ b/src/Text/PrettyPrint/Html.hs +@@ -90,7 +90,7 @@ attribute (key,value) = " " ++ key ++ "=\"" ++ escapeHtmlEntities value ++ "\"" + + -- | A 'Document' transformer that adds proper HTML escaping. + newtype HtmlDoc d = HtmlDoc { getHtmlDoc :: d } +- deriving( Monoid ) ++ deriving( Monoid, Semigroup ) + + -- | Wrap a document such that HTML markup can be added without disturbing the + -- layout. +@@ -182,9 +182,11 @@ getNoHtmlDoc = runIdentity . unNoHtmlDoc + instance NFData d => NFData (NoHtmlDoc d) where + rnf = rnf . getNoHtmlDoc + ++instance Semigroup d => Semigroup (NoHtmlDoc d) where ++ (<>) = liftA2 (<>) ++ + instance Monoid d => Monoid (NoHtmlDoc d) where + mempty = pure mempty +- mappend = liftA2 mappend + + instance Document d => Document (NoHtmlDoc d) where + char = pure . char 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..b1eb171b20b1 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/tlaplus/default.nix @@ -0,0 +1,40 @@ +{ stdenv, fetchFromGitHub, makeWrapper +, jdk, jre, ant +}: + +stdenv.mkDerivation rec { + name = "tlaplus-${version}"; + 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..7d35f5f91df3 --- /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 { + name = "tlaps-${version}"; + 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..f1116a27c0be --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/tlaplus/toolbox.nix @@ -0,0 +1,77 @@ +{ lib, fetchzip, makeWrapper, makeDesktopItem, stdenv +, jre, swt, gtk, libXtst, glib +}: + +let + version = "1.5.7"; + 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 { + name = "tla-toolbox-${version}"; + src = fetchzip { + url = "https://tla.msr-inria.inria.fr/tlatoolbox/products/TLAToolbox-${version}-linux.gtk.${arch}.zip"; + sha256 = "0lg9sizpw5mkcnwwvmgqigkizjyz2lf1wrg48h7mg7wcv3macy4q"; + }; + + buildInputs = [ makeWrapper ]; + + phases = [ "installPhase" ]; + + installPhase = '' + mkdir -p "$out/bin" + cp -r "$src" "$out/toolbox" + chmod +w "$out/toolbox" "$out/toolbox/toolbox" + + patchelf \ + --set-interpreter $(cat $NIX_CC/nix-support/dynamic-linker) \ + "$out/toolbox/toolbox" + + makeWrapper $out/toolbox/toolbox $out/bin/tla-toolbox \ + --run "set -x; cd $out/toolbox" \ + --add-flags "-data ~/.tla-toolbox" \ + --prefix PATH : "${jre}/bin" \ + --prefix LD_LIBRARY_PATH : "${lib.makeLibraryPath [ swt gtk libXtst glib ]}" + + 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..24971b500d3f --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/tptp/default.nix @@ -0,0 +1,49 @@ +{ stdenv, fetchurl, yap, tcsh, perl, patchelf }: + +stdenv.mkDerivation rec { + name = "TPTP-${version}"; + version = "7.2.0"; + + src = fetchurl { + urls = [ + "http://www.cs.miami.edu/~tptp/TPTP/Distribution/TPTP-v${version}.tgz" + "http://www.cs.miami.edu/~tptp/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..74f8875fcebe --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/twelf/default.nix @@ -0,0 +1,51 @@ +{ stdenv, fetchurl, pkgconfig, smlnj, rsync }: + +stdenv.mkDerivation rec { + name = "twelf-${version}"; + 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..8ad70531d543 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/vampire/default.nix @@ -0,0 +1,59 @@ +{ stdenv, fetchFromGitHub, fetchpatch, z3, zlib, git }: + +stdenv.mkDerivation rec { + version = "4.2.2"; + name = "vampire-${version}"; + + src = fetchFromGitHub { + owner = "vprover"; + repo = "vampire"; + rev = version; + sha256 = "0d1klprlgqrcn8r5ywgvsahr4qz96ayl67ry5jks946v0k94m1k1"; + fetchSubmodules = true; + leaveDotGit = true; + }; + + nativeBuildInputs = [ git ]; + 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..22eb5d07f1c1 --- /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 { + name = "verifast-${version}"; + version = "18.02"; + + src = fetchurl { + url = "https://github.com/verifast/verifast/releases/download/${version}/${name}-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..ca3673d7bf97 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/verit/default.nix @@ -0,0 +1,31 @@ +{ stdenv, fetchurl, autoreconfHook, gmp, flex, bison }: + +stdenv.mkDerivation rec { + name = "veriT-${version}"; + 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/default.nix b/nixpkgs/pkgs/applications/science/logic/why3/default.nix new file mode 100644 index 000000000000..58609e856c3b --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/why3/default.nix @@ -0,0 +1,27 @@ +{ fetchurl, stdenv, ocamlPackages, coq }: + +stdenv.mkDerivation rec { + name = "why3-${version}"; + version = "1.1.0"; + + src = fetchurl { + url = https://gforge.inria.fr/frs/download.php/file/37767/why3-1.1.0.tar.gz; + sha256 = "199ziq8mv3r24y3dd1n2r8k2gy09p7kdyyhkg9qn1vzfd2fxwzc1"; + }; + + buildInputs = (with ocamlPackages; [ + ocaml findlib num lablgtk ocamlgraph zarith menhir ]) ++ + stdenv.lib.optionals (ocamlPackages.ocaml == coq.ocaml ) [ + coq coq.camlp5 + ]; + + installTargets = [ "install" "install-lib" ]; + + 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/workcraft/default.nix b/nixpkgs/pkgs/applications/science/logic/workcraft/default.nix new file mode 100644 index 000000000000..313fe5a9f1dd --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/workcraft/default.nix @@ -0,0 +1,33 @@ +{ stdenv, fetchurl, jre, makeWrapper }: + +stdenv.mkDerivation rec { + name = "workcraft-${version}"; + 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..0ab08db67465 --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/yices/default.nix @@ -0,0 +1,43 @@ +{ stdenv, fetchurl, gmp-static, gperf, autoreconfHook, libpoly }: + +stdenv.mkDerivation rec { + name = "yices-${version}"; + version = "2.6.1"; + + src = fetchurl { + url = "https://github.com/SRI-CSL/yices2/archive/Yices-${version}.tar.gz"; + name = "${name}-src.tar.gz"; + sha256 = "14xvflv14qn8ssm8rklvckp6l1q94vn49qz2snz73j40nwzshaww"; + }; + + 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 = [ 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..28a7e783ff3f --- /dev/null +++ b/nixpkgs/pkgs/applications/science/logic/z3/default.nix @@ -0,0 +1,42 @@ +{ stdenv, fetchFromGitHub, python, fixDarwinDylibNames }: + +stdenv.mkDerivation rec { + name = "z3-${version}"; + version = "4.8.3"; + + src = fetchFromGitHub { + owner = "Z3Prover"; + repo = "z3"; + rev = name; + sha256 = "0p5gdmhd32x6zwmx7j5cgwh4jyfxa9yapym95nlmyfaqzak92qar"; + }; + + 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 ]; + }; +} |