diff options
Diffstat (limited to 'infra/libkookie/nixpkgs/pkgs/applications/science/logic')
97 files changed, 4340 insertions, 0 deletions
diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/abc/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/abc/default.nix new file mode 100644 index 000000000000..426c5a9df323 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/abc/default.nix @@ -0,0 +1,32 @@ +{ stdenv, fetchFromGitHub +, readline, cmake +}: + +stdenv.mkDerivation rec { + pname = "abc-verifier"; + version = "2020.11.24"; + + src = fetchFromGitHub { + owner = "yosyshq"; + repo = "abc"; + rev = "4f5f73d18b137930fb3048c0b385c82fa078db38"; + sha256 = "0z1kp223kix7i4r7mbj2bzawkdzc55nsgc41m85dmbajl9fsj1m0"; + }; + + nativeBuildInputs = [ cmake ]; + buildInputs = [ readline ]; + + enableParallelBuilding = true; + installPhase = "mkdir -p $out/bin && mv abc $out/bin"; + + # needed by yosys + passthru.rev = src.rev; + + meta = with stdenv.lib; { + description = "A tool for squential logic synthesis and formal verification"; + homepage = "https://people.eecs.berkeley.edu/~alanmi/abc"; + license = licenses.mit; + platforms = platforms.unix; + maintainers = with maintainers; [ thoughtpolice ]; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/abella/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/abella/default.nix new file mode 100644 index 000000000000..3d9a2e9bd67b --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/abella/default.nix @@ -0,0 +1,38 @@ +{ stdenv, fetchurl, rsync, ocamlPackages }: + +stdenv.mkDerivation rec { + pname = "abella"; + version = "2.0.6"; + + src = fetchurl { + url = "http://abella-prover.org/distributions/${pname}-${version}.tar.gz"; + sha256 = "164q9gngckg6q69k13lwx2pq3cnc9ckw1qi8dnpxqfjgwfqr7xyi"; + }; + + buildInputs = [ rsync ] ++ (with ocamlPackages; [ ocaml ocamlbuild findlib ]); + + installPhase = '' + mkdir -p $out/bin + rsync -av abella $out/bin/ + + mkdir -p $out/share/emacs/site-lisp/abella/ + rsync -av emacs/ $out/share/emacs/site-lisp/abella/ + + mkdir -p $out/share/abella/examples + rsync -av examples/ $out/share/abella/examples/ + ''; + + meta = { + description = "Interactive theorem prover"; + longDescription = '' + Abella is an interactive theorem prover based on lambda-tree syntax. + This means that Abella is well-suited for reasoning about the meta-theory + of programming languages and other logical systems which manipulate + objects with binding. + ''; + homepage = "http://abella-prover.org/"; + license = stdenv.lib.licenses.gpl3; + maintainers = with stdenv.lib.maintainers; [ bcdarwin ciil ]; + platforms = stdenv.lib.platforms.unix; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/acgtk/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/acgtk/default.nix new file mode 100644 index 000000000000..ccd080005076 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/acgtk/default.nix @@ -0,0 +1,28 @@ +{ stdenv, fetchurl, dune, ocamlPackages }: + +stdenv.mkDerivation { + + pname = "acgtk"; + version = "1.5.1"; + + src = fetchurl { + url = "https://acg.loria.fr/software/acg-1.5.1-20191113.tar.gz"; + sha256 = "17595qfwhzz5q091ak6i6bg5wlppbn8zfn58x3hmmmjvx2yfajn1"; + }; + + buildInputs = [ dune ] ++ (with ocamlPackages; [ + ocaml findlib ansiterminal cairo2 cmdliner fmt logs menhir mtime yojson + ]); + + buildPhase = "dune build"; + + inherit (dune) installPhase; + + meta = with stdenv.lib; { + homepage = "https://acg.loria.fr/"; + description = "A toolkit for developing ACG signatures and lexicon"; + license = licenses.cecill20; + inherit (ocamlPackages.ocaml.meta) platforms; + maintainers = [ maintainers.jirkamarsik ]; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/aiger/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/aiger/default.nix new file mode 100644 index 000000000000..aa5a59ed298a --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/aiger/default.nix @@ -0,0 +1,55 @@ +{ stdenv, fetchurl, picosat }: + +stdenv.mkDerivation rec { + pname = "aiger"; + version = "1.9.9"; + + src = fetchurl { + url = "http://fmv.jku.at/aiger/${pname}-${version}.tar.gz"; + sha256 = "1ish0dw0nf9gyghxsdhpy1jjiy5wp54c993swp85xp7m6vdx6l0y"; + }; + + enableParallelBuilding = true; + + configurePhase = '' + # Set up picosat, so we can build 'aigbmc' + mkdir ../picosat + ln -s ${picosat}/include/picosat/picosat.h ../picosat/picosat.h + ln -s ${picosat}/lib/picosat.o ../picosat/picosat.o + ln -s ${picosat}/share/picosat.version ../picosat/VERSION + ./configure.sh + ''; + + installPhase = '' + mkdir -p $out/bin $dev/include $lib/lib + + # Do the installation manually, as the Makefile has odd + # cyrillic characters, and this is easier than adding + # a whole .patch file. + BINS=( \ + aigand aigdd aigflip aigfuzz aiginfo aigjoin \ + aigmiter aigmove aignm aigor aigreset aigsim \ + aigsplit aigstrip aigtoaig aigtoblif aigtocnf \ + aigtodot aigtosmv aigunconstraint aigunroll \ + andtoaig bliftoaig smvtoaig soltostim wrapstim \ + aigbmc aigdep + ) + + for x in ''${BINS[*]}; do + install -m 755 -s $x $out/bin/$x + done + + cp -v aiger.o $lib/lib + cp -v aiger.h $dev/include + ''; + + outputs = [ "out" "dev" "lib" ]; + + meta = { + description = "And-Inverter Graph (AIG) utilities"; + homepage = "http://fmv.jku.at/aiger/"; + license = stdenv.lib.licenses.mit; + maintainers = with stdenv.lib.maintainers; [ thoughtpolice ]; + platforms = stdenv.lib.platforms.unix; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/alt-ergo/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/alt-ergo/default.nix new file mode 100644 index 000000000000..519b1f98138e --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/alt-ergo/default.nix @@ -0,0 +1,45 @@ +{ fetchurl, lib, which, ocamlPackages }: + +let + pname = "alt-ergo"; + version = "2.3.3"; + + src = fetchurl { + url = "https://alt-ergo.ocamlpro.com/http/alt-ergo-${version}/alt-ergo-${version}.tar.gz"; + sha256 = "124k2a4ikk4wdpmvgjpgl97x9skvr9qznk8m68dzsynzpv6yksaj"; + }; + + nativeBuildInputs = [ which ]; + +in + +let alt-ergo-lib = ocamlPackages.buildDunePackage rec { + pname = "alt-ergo-lib"; + inherit version src nativeBuildInputs; + configureFlags = pname; + propagatedBuildInputs = with ocamlPackages; [ num ocplib-simplex stdlib-shims zarith ]; +}; in + +let alt-ergo-parsers = ocamlPackages.buildDunePackage rec { + pname = "alt-ergo-parsers"; + inherit version src nativeBuildInputs; + configureFlags = pname; + buildInputs = with ocamlPackages; [ menhir ]; + propagatedBuildInputs = [ alt-ergo-lib ] ++ (with ocamlPackages; [ camlzip psmt2-frontend ]); +}; in + +ocamlPackages.buildDunePackage { + + inherit pname version src nativeBuildInputs; + + configureFlags = pname; + + buildInputs = [ alt-ergo-parsers ocamlPackages.menhir ]; + + meta = { + description = "High-performance theorem prover and SMT solver"; + homepage = "https://alt-ergo.ocamlpro.com/"; + license = lib.licenses.ocamlpro_nc; + maintainers = [ lib.maintainers.thoughtpolice ]; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/aspino/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/aspino/default.nix new file mode 100644 index 000000000000..c1cf9034c02a --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/aspino/default.nix @@ -0,0 +1,50 @@ +{ stdenv, fetchurl, fetchFromGitHub, zlib, boost }: + +let + glucose' = fetchurl { + url = "http://www.labri.fr/perso/lsimon/downloads/softwares/glucose-syrup.tgz"; + sha256 = "0bq5l2jabhdfhng002qfk0mcj4pfi1v5853x3c7igwfrgx0jmfld"; + }; +in + +stdenv.mkDerivation { + name = "aspino-unstable-2017-03-09"; + + src = fetchFromGitHub { + owner = "alviano"; + repo = "aspino"; + rev = "e31c3b4e5791a454e6602439cb26bd98d23c4e78"; + sha256 = "0annsjs2prqmv1lbs0lxr7yclfzh47xg9zyiq6mdxcc02rxsi14f"; + }; + + buildInputs = [ zlib boost ]; + + postPatch = '' + substituteInPlace Makefile \ + --replace "GCC = g++" "GCC = c++" + + patchShebangs . + ''; + + preBuild = '' + cp ${glucose'} patches/glucose-syrup.tgz + ./bootstrap.sh + ''; + + installPhase = '' + runHook preInstall + mkdir -p $out/bin + install -m0755 build/release/{aspino,fairino-{bs,ls,ps},maxino-2015-{k16,kdyn}} $out/bin + runHook postInstall + ''; + + meta = with stdenv.lib; { + description = "SAT/PseudoBoolean/MaxSat/ASP solver using glucose"; + maintainers = with maintainers; [ gebner ]; + platforms = platforms.unix; + license = licenses.asl20; + homepage = "https://alviano.net/software/maxino/"; + # See pkgs/applications/science/logic/glucose/default.nix + badPlatforms = [ "aarch64-linux" ]; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/avy/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/avy/default.nix new file mode 100644 index 000000000000..6b48c1e34488 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/avy/default.nix @@ -0,0 +1,49 @@ +{ stdenv, fetchgit, cmake, zlib, boost }: + +stdenv.mkDerivation rec { + pname = "avy"; + version = "2019.05.01"; # date of cav19 tag + + src = fetchgit { + url = "https://bitbucket.org/arieg/extavy"; + rev = "cav19"; + sha256 = "0qdzy9srxp5f38x4dbb3prnr9il6cy0kz80avrvd7fxqzy7wdlwy"; + fetchSubmodules = true; + }; + + buildInputs = [ cmake zlib boost.out boost.dev ]; + NIX_CFLAGS_COMPILE = toString ([ "-Wno-narrowing" ] + # Squelch endless stream of warnings on same few things + ++ stdenv.lib.optionals stdenv.cc.isClang [ + "-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} + ''; + + 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/infra/libkookie/nixpkgs/pkgs/applications/science/logic/avy/glucose-fenv.patch b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/avy/glucose-fenv.patch new file mode 100644 index 000000000000..dd19f7ec80e7 --- /dev/null +++ b/infra/libkookie/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/infra/libkookie/nixpkgs/pkgs/applications/science/logic/avy/minisat-fenv.patch b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/avy/minisat-fenv.patch new file mode 100644 index 000000000000..686d5a1c5b49 --- /dev/null +++ b/infra/libkookie/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/infra/libkookie/nixpkgs/pkgs/applications/science/logic/beluga/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/beluga/default.nix new file mode 100644 index 000000000000..44478a032b38 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/beluga/default.nix @@ -0,0 +1,40 @@ +{ lib, fetchFromGitHub, ocamlPackages, rsync }: + +ocamlPackages.buildDunePackage { + pname = "beluga"; + version = "unstable-2020-03-11"; + + src = fetchFromGitHub { + owner = "Beluga-lang"; + repo = "Beluga"; + rev = "6133b2f572219333f304bb4f77c177592324c55b"; + sha256 = "0sy6mi50z3mvs5z7dx38piydapk89all81rh038x3559b5fsk68q"; + }; + + useDune2 = true; + + buildInputs = with ocamlPackages; [ + gen sedlex_2 ocaml_extlib dune-build-info linenoise + ]; + + postPatch = '' + patchShebangs ./TEST ./run_harpoon_test.sh + ''; + + checkPhase = "./TEST"; + checkInputs = [ rsync ]; + doCheck = true; + + postInstall = '' + mkdir -p $out/share/emacs/site-lisp/beluga/ + cp -r tools/beluga-mode.el $out/share/emacs/site-lisp/beluga + ''; + + meta = with lib; { + description = "A functional language for reasoning about formal systems"; + homepage = "http://complogic.cs.mcgill.ca/beluga/"; + license = licenses.gpl3Plus; + maintainers = [ maintainers.bcdarwin ]; + platforms = platforms.unix; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/boolector/cmake-gtest.patch b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/boolector/cmake-gtest.patch new file mode 100644 index 000000000000..61a64d3abbbf --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/boolector/cmake-gtest.patch @@ -0,0 +1,16 @@ +diff --git a/cmake/googletest-download.cmake b/cmake/googletest-download.cmake +index 0ec4d558..d0910313 100644 +--- a/cmake/googletest-download.cmake ++++ b/cmake/googletest-download.cmake +@@ -9,10 +9,7 @@ ExternalProject_Add( + googletest + SOURCE_DIR "@GOOGLETEST_DOWNLOAD_ROOT@/googletest-src" + BINARY_DIR "@GOOGLETEST_DOWNLOAD_ROOT@/googletest-build" +- GIT_REPOSITORY +- https://github.com/google/googletest.git +- GIT_TAG +- release-1.10.0 ++ URL REPLACEME + CONFIGURE_COMMAND "" + BUILD_COMMAND "" + INSTALL_COMMAND "" diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/boolector/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/boolector/default.nix new file mode 100644 index 000000000000..0364a76639aa --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/boolector/default.nix @@ -0,0 +1,69 @@ +{ stdenv, fetchFromGitHub, fetchpatch, lib, python3 +, cmake, lingeling, btor2tools, gtest, gmp +}: + +stdenv.mkDerivation rec { + pname = "boolector"; + version = "3.2.1"; + + src = fetchFromGitHub { + owner = "boolector"; + repo = "boolector"; + rev = "refs/tags/${version}"; + sha256 = "0jkmaw678njqgkflzj9g374yk1mci8yqvsxkrqzlifn6bwhwb7ci"; + }; + + # excludes development artifacts from install, will be included in next release + patches = [ + (fetchpatch { + url = "https://github.com/Boolector/boolector/commit/4d240436e34e65096671099766344dd9126145b1.patch"; + sha256 = "1girsbvlhkkl1hldl2gsjynwc3m92jskn798qhx0ydg6whrfgcgw"; + }) + ]; + + postPatch = '' + sed s@REPLACEME@file://${gtest.src}@ ${./cmake-gtest.patch} | patch -p1 + ''; + + nativeBuildInputs = [ cmake ]; + buildInputs = [ lingeling btor2tools gmp ]; + + cmakeFlags = + [ "-DBUILD_SHARED_LIBS=ON" + "-DUSE_LINGELING=YES" + ] ++ (lib.optional (gmp != null) "-DUSE_GMP=YES"); + + checkInputs = [ python3 ]; + doCheck = true; + preCheck = + let var = if stdenv.isDarwin then "DYLD_LIBRARY_PATH" else "LD_LIBRARY_PATH"; + in + # tests modelgen and modelgensmt2 spawn boolector in another processes and + # macOS strips DYLD_LIBRARY_PATH, hardcode it for testing + stdenv.lib.optionalString stdenv.isDarwin '' + cp -r bin bin.back + install_name_tool -change libboolector.dylib $(pwd)/lib/libboolector.dylib bin/boolector + '' + '' + export ${var}=$(readlink -f lib) + patchShebangs .. + ''; + + postCheck = stdenv.lib.optionalString stdenv.isDarwin '' + rm -rf bin + mv bin.back bin + ''; + + # this is what haskellPackages.boolector expects + postInstall = '' + cp $out/include/boolector/boolector.h $out/include/boolector.h + cp $out/include/boolector/btortypes.h $out/include/btortypes.h + ''; + + meta = with stdenv.lib; { + description = "An extremely fast SMT solver for bit-vectors and arrays"; + homepage = "https://boolector.github.io"; + license = licenses.mit; + platforms = with platforms; linux ++ darwin; + maintainers = with maintainers; [ thoughtpolice ]; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/btor2tools/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/btor2tools/default.nix new file mode 100644 index 000000000000..7d2aed7596e8 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/btor2tools/default.nix @@ -0,0 +1,33 @@ +{ stdenv, cmake, fetchFromGitHub, fixDarwinDylibNames }: + +stdenv.mkDerivation rec { + pname = "btor2tools"; + version = "1.0.0-pre_${src.rev}"; + + src = fetchFromGitHub { + owner = "boolector"; + repo = "btor2tools"; + rev = "9831f9909fb283752a3d6d60d43613173bd8af42"; + sha256 = "0mfqmkgvyw8fa2c09kww107dmk180ch1hp98r5kv41vnc04iqb0s"; + }; + + nativeBuildInputs = [ cmake ] ++ stdenv.lib.optional stdenv.isDarwin fixDarwinDylibNames; + + installPhase = '' + mkdir -p $out $dev/include/btor2parser/ $lib/lib + + cp -vr bin $out + cp -v ../src/btor2parser/btor2parser.h $dev/include/btor2parser + cp -v lib/libbtor2parser.* $lib/lib + ''; + + outputs = [ "out" "dev" "lib" ]; + + meta = with stdenv.lib; { + description = "A generic parser and tool package for the BTOR2 format"; + homepage = "https://github.com/Boolector/btor2tools"; + license = licenses.mit; + platforms = platforms.unix; + maintainers = with maintainers; [ thoughtpolice ]; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/cadical/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/cadical/default.nix new file mode 100644 index 000000000000..e3707ff7dab1 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/cadical/default.nix @@ -0,0 +1,31 @@ +{ stdenv, fetchFromGitHub }: + +stdenv.mkDerivation rec { + pname = "cadical"; + version = "1.3.0"; + + src = fetchFromGitHub { + owner = "arminbiere"; + repo = "cadical"; + rev = "rel-${version}"; + sha256 = "05lvnvapjawgkky38xknb9lgaliiwan4kggmb9yggl4ifpjrh8qf"; + }; + + doCheck = true; + dontAddPrefix = true; + + installPhase = '' + install -Dm0755 build/cadical "$out/bin/cadical" + install -Dm0755 build/mobical "$out/bin/mobical" + mkdir -p "$out/share/doc/${pname}-${version}/" + install -Dm0755 {LICEN?E,README*,VERSION} "$out/share/doc/${pname}-${version}/" + ''; + + meta = with stdenv.lib; { + description = "Simplified Satisfiability Solver"; + maintainers = with maintainers; [ shnarazk ]; + platforms = platforms.unix; + license = licenses.mit; + homepage = "http://fmv.jku.at/cadical"; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/cedille/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/cedille/default.nix new file mode 100644 index 000000000000..2ac96df66a68 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/cedille/default.nix @@ -0,0 +1,52 @@ +{ stdenv +, lib +, fetchFromGitHub +, alex +, happy +, Agda +, buildPlatform +, buildPackages +, ghcWithPackages +}: + +stdenv.mkDerivation rec { + version = "1.1.1"; + pname = "cedille"; + + src = fetchFromGitHub { + owner = "cedille"; + repo = "cedille"; + rev = "v${version}"; + sha256 = "16pc72wz6kclq9yv2r8hx85mkp0s125h12snrhcjxkbl41xx2ynb"; + fetchSubmodules = true; + }; + + nativeBuildInputs = [ alex happy ]; + buildInputs = [ Agda (ghcWithPackages (ps: [ps.ieee])) ]; + + LANG = "en_US.UTF-8"; + LOCALE_ARCHIVE = + lib.optionalString (buildPlatform.libc == "glibc") + "${buildPackages.glibcLocales}/lib/locale/locale-archive"; + + postPatch = '' + patchShebangs create-libraries.sh + ''; + + installPhase = '' + install -Dm755 -t $out/bin/ cedille + install -Dm755 -t $out/bin/ core/cedille-core + install -Dm644 -t $out/share/info docs/info/cedille-info-main.info + + mkdir -p $out/lib/ + cp -r lib/ $out/lib/cedille/ + ''; + + meta = with stdenv.lib; { + description = "An interactive theorem-prover and dependently typed programming language, based on extrinsic (aka Curry-style) type theory"; + homepage = "https://cedille.github.io/"; + license = licenses.mit; + maintainers = with maintainers; [ marsam mpickering ]; + platforms = platforms.unix; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/celf/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/celf/default.nix new file mode 100644 index 000000000000..9dc20a61a4d2 --- /dev/null +++ b/infra/libkookie/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/infra/libkookie/nixpkgs/pkgs/applications/science/logic/clprover/clprover.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/clprover/clprover.nix new file mode 100644 index 000000000000..e53bbe688371 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/clprover/clprover.nix @@ -0,0 +1,27 @@ +{ stdenv, fetchzip }: + +stdenv.mkDerivation { + pname = "clprover"; + version = "1.0.3"; + + src = fetchzip { + url = "http://cgi.csc.liv.ac.uk/~ullrich/CLProver++/CLProver++-v1.0.3-18-04-2015.zip"; + sha256 = "10kmlg4m572qwfzi6hkyb0ypb643xw8sfb55xx7866lyh37w1q3s"; + stripRoot = false; + }; + + installPhase = '' + mkdir $out + cp -r bin $out/bin + mkdir -p $out/share/clprover + cp -r examples $out/share/clprover/examples + ''; + + meta = with stdenv.lib; { + description = "Resolution-based theorem prover for Coalition Logic implemented in C++"; + homepage = "http://cgi.csc.liv.ac.uk/~ullrich/CLProver++/"; + license = licenses.gpl3; # Note that while the website states that it is GPLv2 but the file in the zip as well as the comments in the source state it is GPLv3 + maintainers = with maintainers; [ mgttlinger ]; + platforms = [ "x86_64-linux" ]; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/coq/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/coq/default.nix new file mode 100644 index 000000000000..dc9e40912d53 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/coq/default.nix @@ -0,0 +1,175 @@ +# - 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, gnumake42 +, ocamlPackages, ncurses +, buildIde ? !(stdenv.isDarwin && stdenv.lib.versionAtLeast version "8.10") +, glib, gnome3, wrapGAppsHook +, csdp ? null +, version +}: + +let + sha256 = { + "8.5pl1" = "1976ki5xjg2r907xj9p7gs0kpdinywbwcqlgxqw75dgp0hkgi00n"; + "8.5pl2" = "109rrcrx7mz0fj7725kjjghfg5ydwb24hjsa5hspa27b4caah7rh"; + "8.5pl3" = "15c3rdk59nifzihsp97z4vjxis5xmsnrvpb86qiazj143z2fmdgw"; + "8.6" = "148mb48zpdax56c0blfi7v67lx014lnmrvxxasi28hsibyz2lvg4"; + "8.6.1" = "0llrxcxwy5j87vbbjnisw42rfw1n1pm5602ssx64xaxx3k176g6l"; + "8.7.0" = "1h18b7xpnx3ix9vsi5fx4zdcbxy7bhra7gd5c5yzxmk53cgf1p9m"; + "8.7.1" = "0gjn59jkbxwrihk8fx9d823wjyjh5m9gvj9l31nv6z6bcqhgdqi8"; + "8.7.2" = "0a0657xby8wdq4aqb2xsxp3n7pmc2w4yxjmrb2l4kccs1aqvaj4w"; + "8.8.0" = "13a4fka22hdxsjk11mgjb9ffzplfxyxp1sg5v1c8nk1grxlscgw8"; + "8.8.1" = "1hlf58gwazywbmfa48219amid38vqdl94yz21i11b4map6jfwhbk"; + "8.8.2" = "1lip3xja924dm6qblisk1bk0x8ai24s5xxqxphbdxj6djglj68fd"; + "8.9.0" = "1dkgdjc4n1m15m1p724hhi5cyxpqbjw6rxc5na6fl3v4qjjfnizh"; + "8.9.1" = "1xrq6mkhpq994bncmnijf8jwmwn961kkpl4mwwlv7j3dgnysrcv2"; + "8.10.0" = "138jw94wp4mg5dgjc2asn8ng09ayz1mxdznq342n0m469j803gzg"; + "8.10.1" = "072v2zkjzf7gj48137wpr3c9j0hg9pdhlr5l8jrgrwynld8fp7i4"; + "8.10.2" = "0znxmpy71bfw0p6x47i82jf5k7v41zbz9bdpn901ysn3ir8l3wrz"; + "8.11.0" = "1rfdic6mp7acx2zfwz7ziqk12g95bl9nyj68z4n20a5bcjv2pxpn"; + "8.11.1" = "0qriy9dy36dajsv5qmli8gd6v55mah02ya334nw49ky19v7518m0"; + "8.11.2" = "0f77ccyxdgbf1nrj5fa8qvrk1cyfy06fv8gj9kzfvlcgn0cf48sa"; + "8.12.0" = "18dc7k0piv6v064zgdadpw6mkkxk7j663hb3svgj5236fihjr0cz"; + "8.12.1" = "1rkcyjjrzcqw9xk93hsq0vvji4f8r5iq0f739mghk60bghkpnb7q"; + }.${version}; + coq-version = stdenv.lib.versions.majorMinor version; + versionAtLeast = stdenv.lib.versionAtLeast coq-version; + ideFlags = stdenv.lib.optionalString (buildIde && !versionAtLeast "8.10") + "-lablgtkdir ${ocamlPackages.lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt"; + csdpPatch = if csdp != null then '' + substituteInPlace plugins/micromega/sos.ml --replace "; csdp" "; ${csdp}/bin/csdp" + substituteInPlace plugins/micromega/coq_micromega.ml --replace "System.is_in_system_path \"csdp\"" "true" + '' else ""; +self = stdenv.mkDerivation { + pname = "coq"; + inherit version; + + passthru = { + inherit coq-version; + inherit ocamlPackages; + # For compatibility + inherit (ocamlPackages) ocaml camlp5 findlib num; + emacsBufferSetup = pkgs: '' + ; Propagate coq paths to children + (inherit-local-permanent coq-prog-name "${self}/bin/coqtop") + (inherit-local-permanent coq-dependency-analyzer "${self}/bin/coqdep") + (inherit-local-permanent coq-compiler "${self}/bin/coqc") + ; If the coq-library path was already set, re-set it based on our current coq + (when (fboundp 'get-coq-library-directory) + (inherit-local-permanent coq-library-directory (get-coq-library-directory)) + (coq-prog-args)) + (mapc (lambda (arg) + (when (file-directory-p (concat arg "/lib/coq/${coq-version}/user-contrib")) + (setenv "COQPATH" (concat (getenv "COQPATH") ":" arg "/lib/coq/${coq-version}/user-contrib")))) '(${stdenv.lib.concatStringsSep " " (map (pkg: "\"${pkg}\"") pkgs)})) + ; TODO Abstract this pattern from here and nixBufferBuilders.withPackages! + (defvar nixpkgs--coq-buffer-count 0) + (when (eq nixpkgs--coq-buffer-count 0) + (make-variable-buffer-local 'nixpkgs--is-nixpkgs-coq-buffer) + (defun nixpkgs--coq-inherit (buf) + (inherit-local-inherit-child buf) + (with-current-buffer buf + (setq nixpkgs--coq-buffer-count (1+ nixpkgs--coq-buffer-count)) + (add-hook 'kill-buffer-hook 'nixpkgs--decrement-coq-buffer-count nil t)) + buf) + ; When generating a scomint buffer, do inherit-local inheritance and make it a nixpkgs-coq buffer + (defun nixpkgs--around-scomint-make (orig &rest r) + (if nixpkgs--is-nixpkgs-coq-buffer + (progn + (advice-add 'get-buffer-create :filter-return #'nixpkgs--coq-inherit) + (apply orig r) + (advice-remove 'get-buffer-create #'nixpkgs--coq-inherit)) + (apply orig r))) + (advice-add 'scomint-make :around #'nixpkgs--around-scomint-make) + ; When we have no more coq buffers, tear down the buffer handling + (defun nixpkgs--decrement-coq-buffer-count () + (setq nixpkgs--coq-buffer-count (1- nixpkgs--coq-buffer-count)) + (when (eq nixpkgs--coq-buffer-count 0) + (advice-remove 'scomint-make #'nixpkgs--around-scomint-make) + (fmakunbound 'nixpkgs--around-scomint-make) + (fmakunbound 'nixpkgs--coq-inherit) + (fmakunbound 'nixpkgs--decrement-coq-buffer-count)))) + (setq nixpkgs--coq-buffer-count (1+ nixpkgs--coq-buffer-count)) + (add-hook 'kill-buffer-hook 'nixpkgs--decrement-coq-buffer-count nil t) + (setq nixpkgs--is-nixpkgs-coq-buffer t) + (inherit-local 'nixpkgs--is-nixpkgs-coq-buffer) + ''; + }; + + src = fetchFromGitHub { + owner = "coq"; + repo = "coq"; + rev = "V${version}"; + inherit sha256; + }; + + nativeBuildInputs = [ pkgconfig ] + ++ stdenv.lib.optional (!versionAtLeast "8.6") gnumake42 + ; + buildInputs = [ ncurses ocamlPackages.ocaml ocamlPackages.findlib ] + ++ stdenv.lib.optional (!versionAtLeast "8.10") ocamlPackages.camlp5 + ++ stdenv.lib.optional (!versionAtLeast "8.12") ocamlPackages.num + ++ stdenv.lib.optionals buildIde + (if versionAtLeast "8.10" + then [ ocamlPackages.lablgtk3-sourceview3 glib gnome3.defaultIconTheme wrapGAppsHook ] + else [ ocamlPackages.lablgtk ]); + + propagatedBuildInputs = stdenv.lib.optional (versionAtLeast "8.12") ocamlPackages.num; + + postPatch = '' + UNAME=$(type -tp uname) + RM=$(type -tp rm) + substituteInPlace configure --replace "/bin/uname" "$UNAME" + substituteInPlace tools/beautify-archive --replace "/bin/rm" "$RM" + substituteInPlace configure.ml --replace '"md5 -q"' '"md5sum"' + ${csdpPatch} + ''; + + setupHook = writeText "setupHook.sh" '' + addCoqPath () { + if test -d "''$1/lib/coq/${coq-version}/user-contrib"; then + export COQPATH="''${COQPATH-}''${COQPATH:+:}''$1/lib/coq/${coq-version}/user-contrib/" + fi + } + + addEnvHooks "$targetOffset" addCoqPath + ''; + + preConfigure = if versionAtLeast "8.10" then '' + patchShebangs dev/tools/ + '' else '' + configureFlagsArray=( + ${ideFlags} + ) + ''; + + prefixKey = "-prefix "; + + buildFlags = [ "revision" "coq" "coqide" "bin/votour" ]; + + createFindlibDestdir = true; + + postInstall = '' + cp bin/votour $out/bin/ + ln -s $out/lib/coq $OCAMLFIND_DESTDIR/coq + ''; + + meta = with stdenv.lib; { + description = "Coq proof assistant"; + longDescription = '' + Coq is a formal proof management system. It provides a formal language + to write mathematical definitions, executable algorithms and theorems + together with an environment for semi-interactive development of + machine-checked proofs. + ''; + homepage = "http://coq.inria.fr"; + license = licenses.lgpl21; + branch = coq-version; + maintainers = with maintainers; [ roconnor thoughtpolice vbgl Zimmi48 ]; + platforms = platforms.unix; + }; +}; in self diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/coq2html/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/coq2html/default.nix new file mode 100644 index 000000000000..e53e8e7392c0 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/coq2html/default.nix @@ -0,0 +1,39 @@ +{ stdenv, fetchgit, ocaml }: + +let + version = "20170720"; +in + +stdenv.mkDerivation { + pname = "coq2html"; + inherit version; + + src = fetchgit { + url = "https://github.com/xavierleroy/coq2html"; + rev = "e2b94093c6b9a877717f181765e30577de22439e"; + sha256 = "1x466j0pyjggyz0870pdllv9f5vpnfrgkd0w7ajvm9rkwyp3f610"; + }; + + buildInputs = [ ocaml ]; + + installPhase = '' + mkdir -p $out/bin + cp coq2html $out/bin + ''; + + meta = with stdenv.lib; { + description = "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/infra/libkookie/nixpkgs/pkgs/applications/science/logic/cryptominisat/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/cryptominisat/default.nix new file mode 100644 index 000000000000..ddbb140c9baa --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/cryptominisat/default.nix @@ -0,0 +1,32 @@ +{ stdenv, fetchFromGitHub, cmake, python3, xxd, boost, fetchpatch }: + +stdenv.mkDerivation rec { + pname = "cryptominisat"; + version = "5.8.0"; + + src = fetchFromGitHub { + owner = "msoos"; + repo = "cryptominisat"; + rev = version; + sha256 = "00hmxdlyhn7pwk9jlvc5g0l5z5xqfchjzf5jgn3pkj9xhl8yqq50"; + }; + + patches = [ + (fetchpatch { + # https://github.com/msoos/cryptominisat/pull/621 + url = "https://github.com/msoos/cryptominisat/commit/11a97003b0bfbfb61ed6c4e640212110d390c28c.patch"; + sha256 = "0hdy345bwcbxz0jl1jdxfa6mmfh77s2pz9rnncsr0jzk11b3j0cw"; + }) + ]; + + buildInputs = [ python3 boost ]; + nativeBuildInputs = [ cmake xxd ]; + + meta = with stdenv.lib; { + description = "An advanced SAT Solver"; + homepage = "https://github.com/msoos/cryptominisat"; + license = licenses.mit; + maintainers = with maintainers; [ mic92 ]; + platforms = platforms.unix; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/cryptoverif/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/cryptoverif/default.nix new file mode 100644 index 000000000000..28295ea28922 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/cryptoverif/default.nix @@ -0,0 +1,37 @@ +{ stdenv, fetchurl, ocaml }: + +stdenv.mkDerivation rec { + pname = "cryptoverif"; + version = "2.03pl1"; + + src = fetchurl { + url = "http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/cryptoverif${version}.tar.gz"; + sha256 = "0q7qa1qm7mbky3m36445gdmgmkb9mrhrdsk7mmwn8fzw0rfc6z00"; + }; + + buildInputs = [ ocaml ]; + + /* Fix up the frontend to load the 'default' cryptoverif library + ** from under $out/libexec. By default, it expects to find the files + ** in $CWD which doesn't work. */ + patchPhase = '' + substituteInPlace ./src/settings.ml \ + --replace \"default\" \"$out/libexec/default\" + ''; + + buildPhase = "./build"; + installPhase = '' + mkdir -p $out/bin $out/libexec + cp ./cryptoverif $out/bin + cp ./default.cvl $out/libexec + cp ./default.ocvl $out/libexec + ''; + + meta = { + description = "Cryptographic protocol verifier in the computational model"; + homepage = "https://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/"; + license = stdenv.lib.licenses.cecill-b; + platforms = stdenv.lib.platforms.unix; + maintainers = [ stdenv.lib.maintainers.thoughtpolice ]; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/cubicle/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/cubicle/default.nix new file mode 100644 index 000000000000..bfb6a57fb33a --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/cubicle/default.nix @@ -0,0 +1,24 @@ +{ stdenv, fetchurl, ocamlPackages }: + +stdenv.mkDerivation rec { + pname = "cubicle"; + version = "1.1.2"; + src = fetchurl { + url = "http://cubicle.lri.fr/cubicle-${version}.tar.gz"; + sha256 = "10kk80jdmpdvql88sdjsh7vqzlpaphd8vip2lp47aarxjkwjlz1q"; + }; + + postPatch = '' + substituteInPlace Makefile.in --replace "\\n" "" + ''; + + buildInputs = with ocamlPackages; [ ocaml findlib functory ]; + + meta = with stdenv.lib; { + description = "An open source model checker for verifying safety properties of array-based systems"; + homepage = "http://cubicle.lri.fr/"; + license = licenses.asl20; + platforms = platforms.unix; + maintainers = with maintainers; [ dwarfmaster ]; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/cvc3/cvc3-2.4.1-gccv6-fix.patch b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/cvc3/cvc3-2.4.1-gccv6-fix.patch new file mode 100644 index 000000000000..1fb3516b8c27 --- /dev/null +++ b/infra/libkookie/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/infra/libkookie/nixpkgs/pkgs/applications/science/logic/cvc3/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/cvc3/default.nix new file mode 100644 index 000000000000..be80565115fe --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/cvc3/default.nix @@ -0,0 +1,39 @@ +{ stdenv, fetchurl, flex, bison, gmp, perl }: + +stdenv.mkDerivation rec { + pname = "cvc3"; + version = "2.4.1"; + + src = fetchurl { + url = "http://www.cs.nyu.edu/acsys/cvc3/releases/${version}/${pname}-${version}.tar.gz"; + sha256 = "1xxcwhz3y6djrycw8sm6xz83wb4hb12rd1n0skvc7fng0rh1snym"; + }; + + buildInputs = [ gmp flex bison perl ]; + + patches = [ ./cvc3-2.4.1-gccv6-fix.patch ]; + + postPatch = '' + sed -e "s@ /bin/bash@bash@g" -i Makefile.std + find . -exec sed -e "s@/usr/bin/perl@${perl}/bin/perl@g" -i '{}' ';' + + # bison 3.7 workaround + for f in parsePL parseLisp parsesmtlib parsesmtlib2 ; do + ln -s ../parser/''${f}_defs.h src/include/''${f}.hpp + done + ''; + + meta = with stdenv.lib; { + description = "A prover for satisfiability modulo theory (SMT)"; + maintainers = with maintainers; + [ raskin ]; + platforms = platforms.unix; + 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/infra/libkookie/nixpkgs/pkgs/applications/science/logic/cvc4/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/cvc4/default.nix new file mode 100644 index 000000000000..54a2f0225518 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/cvc4/default.nix @@ -0,0 +1,48 @@ +{ stdenv, fetchFromGitHub, cmake, cln, gmp, git, swig, pkgconfig +, readline, libantlr3c, boost, jdk, python3, antlr3_4 +}: + +stdenv.mkDerivation rec { + pname = "cvc4"; + version = "1.8"; + + src = fetchFromGitHub { + owner = "cvc4"; + repo = "cvc4"; + rev = version; + sha256 = "1rhs4pvzaa1wk00czrczp58b2cxfghpsnq534m0l3snnya2958jp"; + }; + + nativeBuildInputs = [ pkgconfig cmake ]; + buildInputs = [ gmp git python3.pkgs.toml 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/ + ''; + cmakeFlags = [ + "-DCMAKE_BUILD_TYPE=Production" + ]; + + + 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/infra/libkookie/nixpkgs/pkgs/applications/science/logic/cvc4/minisat-fenv.patch b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/cvc4/minisat-fenv.patch new file mode 100644 index 000000000000..686d5a1c5b49 --- /dev/null +++ b/infra/libkookie/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/infra/libkookie/nixpkgs/pkgs/applications/science/logic/drat-trim/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/drat-trim/default.nix new file mode 100644 index 000000000000..81e20df33424 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/drat-trim/default.nix @@ -0,0 +1,45 @@ +{ stdenv, fetchFromGitHub }: + +stdenv.mkDerivation { + pname = "drat-trim-unstable"; + version = "2020-06-05"; + + src = fetchFromGitHub { + owner = "marijnheule"; + repo = "drat-trim"; + rev = "9afad0f7156a1e9c6ce19dce5d72cf1cb9a3ef27"; + sha256 = "1zq585igfaknwqbvv2cji744016zxadbvr0ifr5l6yq13m0vvn3b"; + }; + + postPatch = '' + substituteInPlace Makefile --replace gcc cc + ''; + + installPhase = '' + install -Dt $out/bin drat-trim lrat-check + ''; + + 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. + + This package also contains the related tool LRAT-check, which checks a + proof format called LRAT which extends DRAT with hint statements to speed + up the checking process. + ''; + homepage = "https://www.cs.utexas.edu/~marijn/drat-trim/"; + license = licenses.mit; + maintainers = with maintainers; [ kini ]; + platforms = platforms.all; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/ekrhyper/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/ekrhyper/default.nix new file mode 100644 index 000000000000..e1eb9a2dcc3b --- /dev/null +++ b/infra/libkookie/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/infra/libkookie/nixpkgs/pkgs/applications/science/logic/ekrhyper/default.upstream b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/ekrhyper/default.upstream new file mode 100644 index 000000000000..310e93ea53fd --- /dev/null +++ b/infra/libkookie/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/infra/libkookie/nixpkgs/pkgs/applications/science/logic/elan/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/elan/default.nix new file mode 100644 index 000000000000..7a7da2c5f5d2 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/elan/default.nix @@ -0,0 +1,44 @@ +{ lib, pkgconfig, curl, openssl, zlib, fetchFromGitHub, rustPlatform }: + +rustPlatform.buildRustPackage rec { + pname = "elan"; + version = "0.10.2"; + + src = fetchFromGitHub { + owner = "kha"; + repo = "elan"; + rev = "v${version}"; + sha256 = "0ycw1r364g5gwh8796dpv1israpg7zqwx8mcvnacv2lqj5iijmby"; + }; + + cargoSha256 = "0hcaiy046d2gnkp6sfpnkkprb3nd94i9q8dgqxxpwrc1j157x6z9"; + + 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 leanc leanmake; 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 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/infra/libkookie/nixpkgs/pkgs/applications/science/logic/eprover/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/eprover/default.nix new file mode 100644 index 000000000000..a3844dc3700b --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/eprover/default.nix @@ -0,0 +1,29 @@ +{ stdenv, fetchurl, which }: + +stdenv.mkDerivation rec { + pname = "eprover"; + version = "2.5"; + + src = fetchurl { + url = "https://wwwlehre.dhbw-stuttgart.de/~sschulz/WORK/E_DOWNLOAD/V_${version}/E.tgz"; + sha256 = "0jj0zkiqpcx9xp16spkskrv3jycprz7jg1g97i67j43c4yvxylwa"; + }; + + 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/infra/libkookie/nixpkgs/pkgs/applications/science/logic/fast-downward/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/fast-downward/default.nix new file mode 100644 index 000000000000..a46542095373 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/fast-downward/default.nix @@ -0,0 +1,62 @@ +{ stdenv, lib, fetchhg, cmake, which, python3, osi, cplex }: + +stdenv.mkDerivation { + version = "19.12"; + pname = "fast-downward"; + + src = fetchhg { + url = "http://hg.fast-downward.org/"; + rev = "41688a4f16b3"; + sha256 = "08m4k1mkx4sz7c2ab7xh7ip6b67zxv7kl68xrvwa83xw1yigqkna"; + }; + + nativeBuildInputs = [ cmake which ]; + buildInputs = [ python3 python3.pkgs.wrapPython osi ]; + + cmakeFlags = + lib.optional osi.withCplex [ "-DDOWNWARD_CPLEX_ROOT=${cplex}/cplex" ]; + + enableParallelBuilding = true; + + configurePhase = '' + python build.py release + ''; + + postPatch = '' + # Needed because the package tries to be too smart. + export CC="$(which $CC)" + export CXX="$(which $CXX)" + ''; + + installPhase = '' + install -Dm755 builds/release/bin/downward $out/libexec/fast-downward/downward + cp -r builds/release/bin/translate $out/libexec/fast-downward/ + install -Dm755 fast-downward.py $out/bin/fast-downward + mkdir -p $out/${python3.sitePackages} + cp -r driver $out/${python3.sitePackages} + + wrapPythonProgramsIn $out/bin "$out $pythonPath" + wrapPythonProgramsIn $out/libexec/fast-downward/translate "$out $pythonPath" + # Because fast-downward calls `python translate.py` we need to return wrapped scripts back. + for i in $out/libexec/fast-downward/translate/.*-wrapped; do + name="$(basename "$i")" + name1="''${name#.}" + name2="''${name1%-wrapped}" + dir="$(dirname "$i")" + dest="$dir/$name2" + echo "Moving $i to $dest" + mv "$i" "$dest" + done + + substituteInPlace $out/${python3.sitePackages}/driver/arguments.py \ + --replace 'args.build = "release"' "args.build = \"$out/libexec/fast-downward\"" + ''; + + meta = with stdenv.lib; { + description = "A domain-independent planning system"; + homepage = "http://www.fast-downward.org/"; + license = licenses.gpl3Plus; + platforms = with platforms; (linux ++ darwin); + maintainers = with maintainers; [ abbradar ]; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/gappa/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/gappa/default.nix new file mode 100644 index 000000000000..2ca1bcd30981 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/gappa/default.nix @@ -0,0 +1,23 @@ +{ stdenv, fetchurl, gmp, mpfr, boost }: + +stdenv.mkDerivation { + name = "gappa-1.3.5"; + + src = fetchurl { + url = "https://gforge.inria.fr/frs/download.php/file/38044/gappa-1.3.5.tar.gz"; + sha256 = "0q1wdiwqj6fsbifaayb1zkp20bz8a1my81sqjsail577jmzwi07w"; + }; + + buildInputs = [ gmp mpfr boost.dev ]; + + buildPhase = "./remake"; + installPhase = "./remake install"; + + meta = { + homepage = "http://gappa.gforge.inria.fr/"; + description = "Verifying and formally proving properties on numerical programs dealing with floating-point or fixed-point arithmetic"; + license = with stdenv.lib.licenses; [ cecill20 gpl2 ]; + maintainers = with stdenv.lib.maintainers; [ vbgl ]; + platforms = stdenv.lib.platforms.all; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/glucose/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/glucose/default.nix new file mode 100644 index 000000000000..0a8fad484da7 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/glucose/default.nix @@ -0,0 +1,29 @@ +{ stdenv, fetchurl, zlib }: +stdenv.mkDerivation rec { + pname = "glucose"; + version = "4.1"; + + src = fetchurl { + url = "http://www.labri.fr/perso/lsimon/downloads/softwares/glucose-syrup-${version}.tgz"; + sha256 = "0aahrkaq7n0z986fpqz66yz946nxardfi6dh8calzcfjpvqiraji"; + }; + + buildInputs = [ zlib ]; + + sourceRoot = "glucose-syrup-${version}/simp"; + makeFlags = [ "r" ]; + installPhase = '' + install -Dm0755 glucose_release $out/bin/glucose + mkdir -p "$out/share/doc/${pname}-${version}/" + install -Dm0755 ../{LICEN?E,README*,Changelog*} "$out/share/doc/${pname}-${version}/" + ''; + + meta = with stdenv.lib; { + description = "Modern, parallel SAT solver (sequential version)"; + license = licenses.mit; + platforms = platforms.unix; + maintainers = with maintainers; [ gebner ]; + # Build uses _FPU_EXTENDED macro + badPlatforms = [ "aarch64-linux" ]; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/glucose/syrup.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/glucose/syrup.nix new file mode 100644 index 000000000000..816f8504a52e --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/glucose/syrup.nix @@ -0,0 +1,24 @@ +{ stdenv, zlib, glucose }: +stdenv.mkDerivation rec { + pname = "glucose-syrup"; + version = glucose.version; + + src = glucose.src; + + buildInputs = [ zlib ]; + + sourceRoot = "glucose-syrup-${version}/parallel"; + makeFlags = [ "r" ]; + installPhase = '' + install -Dm0755 glucose-syrup_release $out/bin/glucose-syrup + mkdir -p "$out/share/doc/${pname}-${version}/" + install -Dm0755 ../{LICEN?E,README*,Changelog*} "$out/share/doc/${pname}-${version}/" + ''; + + meta = with stdenv.lib; { + description = "Modern, parallel SAT solver (parallel version)"; + license = licenses.unfreeRedistributable; + platforms = platforms.unix; + maintainers = with maintainers; [ gebner ]; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/hol/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/hol/default.nix new file mode 100644 index 000000000000..dbafee7d6000 --- /dev/null +++ b/infra/libkookie/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/infra/libkookie/nixpkgs/pkgs/applications/science/logic/hol_light/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/hol_light/default.nix new file mode 100644 index 000000000000..9c3030517e32 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/hol_light/default.nix @@ -0,0 +1,55 @@ +{ stdenv, runtimeShell, fetchFromGitHub, fetchpatch, ocaml, num, camlp5 }: + +let + load_num = + if num == null then "" else + '' + -I ${num}/lib/ocaml/${ocaml.version}/site-lib/num \ + -I ${num}/lib/ocaml/${ocaml.version}/site-lib/top-num \ + -I ${num}/lib/ocaml/${ocaml.version}/site-lib/stublibs \ + ''; + + start_script = + '' + #!${runtimeShell} + cd $out/lib/hol_light + exec ${ocaml}/bin/ocaml \ + -I \`${camlp5}/bin/camlp5 -where\` \ + ${load_num} \ + -init make.ml + ''; +in + +stdenv.mkDerivation { + name = "hol_light-2019-10-06"; + + src = fetchFromGitHub { + owner = "jrh13"; + repo = "hol-light"; + rev = "5c91b2ded8a66db571824ecfc18b4536c103b23e"; + sha256 = "0sxsk8z08ba0q5aixdyczcx5l29lb51ba4ip3d2fry7y604kjsx6"; + }; + + patches = [(fetchpatch { + url = "https://salsa.debian.org/ocaml-team/hol-light/-/raw/master/debian/patches/0004-Fix-compilation-with-camlp5-7.11.patch"; + sha256 = "180qmxbrk3vb1ix7j77hcs8vsar91rs11s5mm8ir5352rz7ylicr"; + })]; + + 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 maggesi vbgl ]; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/iprover/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/iprover/default.nix new file mode 100644 index 000000000000..310a95d7e7a6 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/iprover/default.nix @@ -0,0 +1,33 @@ +{ stdenv, fetchurl, ocaml, eprover, zlib }: + +stdenv.mkDerivation rec { + pname = "iprover"; + version = "3.1"; + + src = fetchurl { + url = "http://www.cs.man.ac.uk/~korovink/iprover/iprover-v${version}.tar.gz"; + sha256 = "0lik8p7ayhjwpkln1iwf0ri84ramhch74j5nj6z7ph6wfi92pgg8"; + }; + + buildInputs = [ ocaml eprover zlib ]; + + preConfigure = ''patchShebangs .''; + + installPhase = '' + mkdir -p "$out/bin" + cp iproveropt "$out/bin" + + mkdir -p "$out/share/${pname}-${version}" + cp *.p "$out/share/${pname}-${version}" + echo -e "#! ${stdenv.shell}\\n$out/bin/iproveropt --clausifier \"${eprover}/bin/eprover\" --clausifier_options \" --tstp-format --silent --cnf \" \"\$@\"" > "$out"/bin/iprover + chmod a+x "$out"/bin/iprover + ''; + + meta = with stdenv.lib; { + description = "An automated first-order logic theorem prover"; + homepage = "http://www.cs.man.ac.uk/~korovink/iprover/"; + maintainers = with maintainers; [ raskin gebner ]; + platforms = platforms.linux; + license = licenses.gpl3; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/isabelle/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/isabelle/default.nix new file mode 100644 index 000000000000..a12d75eabbe9 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/isabelle/default.nix @@ -0,0 +1,82 @@ +{ stdenv, fetchurl, perl, nettools, java, polyml, z3, rlwrap }: +# nettools needed for hostname + +stdenv.mkDerivation rec { + pname = "isabelle"; + version = "2020"; + + dirname = "Isabelle${version}"; + + src = if stdenv.isDarwin + then fetchurl { + url = "https://isabelle.in.tum.de/website-${dirname}/dist/${dirname}_macos.tar.gz"; + sha256 = "1sfr5filsaqj93g5y4p9n8g5652dhr4whj25x4lifdxr2pp560xx"; + } + else fetchurl { + url = "https://isabelle.in.tum.de/website-${dirname}/dist/${dirname}_linux.tar.gz"; + sha256 = "1bibabhlsvf6qsjjkgxcpq3cvl1z7r8yfcgqbhbvsiv69n3gyfk3"; + }; + + buildInputs = [ perl polyml z3 ] + ++ stdenv.lib.optionals (!stdenv.isDarwin) [ nettools java ]; + + sourceRoot = dirname; + + postPatch = '' + patchShebangs . + + cat >contrib/z3*/etc/settings <<EOF + Z3_HOME=${z3} + Z3_VERSION=${z3.version} + Z3_SOLVER=${z3}/bin/z3 + Z3_INSTALLED=yes + EOF + + cat >contrib/polyml-*/etc/settings <<EOF + ML_SYSTEM_64=true + ML_SYSTEM=${polyml.name} + ML_PLATFORM=${stdenv.system} + ML_HOME=${polyml}/bin + ML_OPTIONS="--minheap 1000" + POLYML_HOME="\$COMPONENT" + ML_SOURCES="\$POLYML_HOME/src" + EOF + + cat >contrib/jdk*/etc/settings <<EOF + ISABELLE_JAVA_PLATFORM=${stdenv.system} + ISABELLE_JDK_HOME=${java} + EOF + + echo ISABELLE_LINE_EDITOR=${rlwrap}/bin/rlwrap >>etc/settings + + for comp in contrib/jdk* contrib/polyml-* contrib/z3-*; do + rm -rf $comp/x86* + done + '' + (if ! stdenv.isLinux then "" else '' + arch=${if stdenv.hostPlatform.system == "x86_64-linux" then "x86_64-linux" else "x86-linux"} + for f in contrib/*/$arch/{bash_process,epclextract,eprover,nunchaku,SPASS}; do + patchelf --set-interpreter $(cat ${stdenv.cc}/nix-support/dynamic-linker) "$f" + done + ''); + + installPhase = '' + mkdir -p $out/bin + mv $TMP/$dirname $out + cd $out/$dirname + bin/isabelle install $out/bin + ''; + + meta = with stdenv.lib; { + 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 = "https://isabelle.in.tum.de/"; + license = licenses.bsd3; + maintainers = [ maintainers.jwiegley ]; + platforms = platforms.linux; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/jonprl/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/jonprl/default.nix new file mode 100644 index 000000000000..3ee05a478bc2 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/jonprl/default.nix @@ -0,0 +1,35 @@ +{ fetchgit, stdenv, smlnj, which }: + +stdenv.mkDerivation rec { + pname = "jonprl"; + version = "0.1.0"; + + src = fetchgit { + url = "https://github.com/jonsterling/JonPRL.git"; + deepClone = true; + rev = "refs/tags/v${version}"; + sha256 = "0czs13syvnw8fz24d075n4pmsyfs8rs8c7ksmvd7cgb3h55fvp4p"; + }; + + buildInputs = [ smlnj which ]; + + installPhase = '' + mkdir -p "$out/bin" + cp bin/.heapimg.* "$out/bin/" + build/mkexec.sh "${smlnj}/bin/sml" "$out" jonprl + ''; + + meta = { + description = "Proof Refinement Logic - Computational Type Theory"; + longDescription = '' + An proof refinement logic for computational type theory + based on Brouwer-realizability & meaning explanations. + Inspired by Nuprl + ''; + homepage = "https://github.com/jonsterling/JonPRL"; + license = stdenv.lib.licenses.mit; + maintainers = with stdenv.lib.maintainers; [ puffnfresh ]; + platforms = stdenv.lib.platforms.linux; + broken = true; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/key/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/key/default.nix new file mode 100644 index 000000000000..b08c4d84d1fc --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/key/default.nix @@ -0,0 +1,74 @@ +{ stdenv +, fetchurl +, unzip +, jdk +, ant +, jre +, makeWrapper +, runCommand +, key +}: + +# get this from the download URL when changing version +let gitRevision = "7d3deab0763c88edee4f7a08e604661e0dbdd450"; + +in stdenv.mkDerivation rec { + pname = "key"; + version = "2.6.3"; + + src = fetchurl { + url = "https://formal.iti.kit.edu/key/releases/${version}/key-src-${version}_${gitRevision}.zip"; + sha256 = "1dr5jmrqs0iy76wdsfiv5hx929i24yzm1xypzqqvx7afc7apyawy"; + }; + + sourceRoot = "key"; + + nativeBuildInputs = [ + unzip + jdk + ant + makeWrapper + ]; + + buildPhase = '' + ant -buildfile scripts/build.xml \ + -Dgit.revision=${gitRevision} \ + compileAll deployAll + ''; + + postCheck = '' + ant -buildfile scripts/build.xml \ + -Dgit.revision=${gitRevision} \ + compileAllTests runAllTests test-deploy-all + ''; + + installPhase = '' + mkdir -p $out/share/java + # Wrong version in the code. On next version change 2.5 to ${version}: + unzip deployment/key-2.5_${gitRevision}.zip -d $out/share/java + mkdir -p $out/bin + makeWrapper ${jre}/bin/java $out/bin/KeY \ + --add-flags "-cp $out/share/java/KeY.jar de.uka.ilkd.key.core.Main" + ''; + + passthru.tests.check-version = runCommand "key-help" {} '' + ${key}/bin/KeY --help | grep 2.5 # Wrong version in the code. On next version change to ${version} + touch $out + ''; + + meta = with stdenv.lib; { + description = "Java formal verification tool"; + homepage = "https://www.key-project.org"; # also https://formal.iti.kit.edu/key/ + longDescription = '' + The KeY System is a formal software development tool that aims to + integrate design, implementation, formal specification, and formal + verification of object-oriented software as seamlessly as possible. + At the core of the system is a novel theorem prover for the first-order + Dynamic Logic for Java with a user-friendly graphical interface. + ''; + license = licenses.gpl2; + maintainers = with maintainers; [ fgaz ]; + platforms = platforms.all; + }; +} + diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/lci/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/lci/default.nix new file mode 100644 index 000000000000..4775384a3ddc --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/lci/default.nix @@ -0,0 +1,16 @@ +{stdenv, fetchurl, readline}: +stdenv.mkDerivation rec { + version = "0.6"; + pname = "lci"; + src = fetchurl { + url = "mirror://sourceforge/lci/${pname}-${version}.tar.gz"; + sha256="204f1ca5e2f56247d71ab320246811c220ed511bf08c9cb7f305cf180a93948e"; + }; + buildInputs = [readline]; + meta = { + description = ''Lambda calculus interpreter''; + maintainers = with stdenv.lib.maintainers; [raskin]; + platforms = with stdenv.lib.platforms; linux; + license = stdenv.lib.licenses.gpl3; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/lean/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/lean/default.nix new file mode 100644 index 000000000000..88e1b4fbc0e1 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/lean/default.nix @@ -0,0 +1,40 @@ +{ stdenv, fetchFromGitHub, cmake, gmp, coreutils }: + +stdenv.mkDerivation rec { + pname = "lean"; + version = "3.23.0"; + + src = fetchFromGitHub { + owner = "leanprover-community"; + repo = "lean"; + rev = "v${version}"; + sha256 = "09mklc1p6ms1jayg2f89hqfmhca3h5744lli936l38ypn1d00sxx"; + }; + + nativeBuildInputs = [ cmake ]; + buildInputs = [ gmp ]; + enableParallelBuilding = true; + + cmakeDir = "../src"; + + # Running the tests is required to build the *.olean files for the core + # library. + doCheck = true; + + postPatch = "patchShebangs ."; + + postInstall = stdenv.lib.optionalString stdenv.isDarwin '' + substituteInPlace $out/bin/leanpkg \ + --replace "greadlink" "${coreutils}/bin/readlink" + ''; + + meta = with stdenv.lib; { + description = "Automatic and interactive theorem prover"; + homepage = "https://leanprover.github.io/"; + changelog = "https://github.com/leanprover-community/lean/blob/v${version}/doc/changes.md"; + license = licenses.asl20; + platforms = platforms.unix; + maintainers = with maintainers; [ thoughtpolice gebner ]; + }; +} + diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/lean2/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/lean2/default.nix new file mode 100644 index 000000000000..612c9d6f92a2 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/lean2/default.nix @@ -0,0 +1,37 @@ +{ stdenv, fetchFromGitHub, cmake, gmp, mpfr, python +, gperftools, ninja, makeWrapper }: + +stdenv.mkDerivation { + pname = "lean2"; + version = "2017-07-22"; + + src = fetchFromGitHub { + owner = "leanprover"; + repo = "lean2"; + rev = "34dbd6c3ae612186b8f0f80d12fbf5ae7a059ec9"; + sha256 = "1xv3j487zhh1zf2b4v19xzw63s2sgjhg8d62a0kxxyknfmdf3khl"; + }; + + buildInputs = [ gmp mpfr cmake python gperftools ninja makeWrapper ]; + enableParallelBuilding = true; + + preConfigure = '' + patchShebangs bin/leantags + cd src + ''; + + cmakeFlags = [ "-GNinja" ]; + + postInstall = '' + wrapProgram $out/bin/linja --prefix PATH : $out/bin:${ninja}/bin + ''; + + meta = with stdenv.lib; { + description = "Automatic and interactive theorem prover (version with HoTT support)"; + homepage = "http://leanprover.github.io"; + license = licenses.asl20; + platforms = platforms.unix; + maintainers = with maintainers; [ thoughtpolice gebner ]; + broken = true; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/leo2/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/leo2/default.nix new file mode 100644 index 000000000000..b43bfb801358 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/leo2/default.nix @@ -0,0 +1,37 @@ +{ stdenv, fetchurl, makeWrapper, eprover, ocaml, perl, zlib }: + +stdenv.mkDerivation rec { + pname = "leo2"; + version = "1.6.2"; + + src = fetchurl { + url = "https://page.mi.fu-berlin.de/cbenzmueller/leo/leo2_v${version}.tgz"; + sha256 = "1wjpmizb181iygnd18lx7p77fwaci2clgzs5ix5j51cc8f3pazmv"; + }; + + buildInputs = [ makeWrapper eprover ocaml perl zlib ]; + + sourceRoot = "leo2/src"; + + preConfigure = "patchShebangs configure"; + + buildFlags = [ "opt" ]; + + preInstall = "mkdir -p $out/bin"; + + postInstall = '' + mkdir -p "$out/etc" + echo -e "e = ${eprover}/bin/eprover\\nepclextract = ${eprover}/bin/epclextract" > "$out/etc/leoatprc" + + wrapProgram $out/bin/leo \ + --add-flags "--atprc $out/etc/leoatprc" + ''; + + meta = with stdenv.lib; { + description = "A high-performance typed higher order prover"; + maintainers = [ maintainers.raskin ]; + platforms = platforms.linux; + license = licenses.bsd3; + homepage = "http://www.leoprover.org/"; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/leo2/default.upstream b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/leo2/default.upstream new file mode 100644 index 000000000000..52b8ed1cdaa2 --- /dev/null +++ b/infra/libkookie/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/infra/libkookie/nixpkgs/pkgs/applications/science/logic/leo3/binary.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/leo3/binary.nix new file mode 100644 index 000000000000..29a9adf94c4b --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/leo3/binary.nix @@ -0,0 +1,29 @@ +{stdenv, fetchurl, openjdk, runtimeShell}: +stdenv.mkDerivation rec { + pname = "leo3"; + version = "1.2"; + + jar = fetchurl { + url = "https://github.com/leoprover/Leo-III/releases/download/v${version}/leo3.jar"; + sha256 = "1lgwxbr1rnk72rnvc8raq5i1q71ckhn998pwd9xk6zf27wlzijk7"; + }; + + phases=["installPhase" "fixupPhase"]; + + installPhase = '' + mkdir -p "$out"/{bin,lib/java/leo3} + cp "${jar}" "$out/lib/java/leo3/leo3.jar" + echo "#!${runtimeShell}" > "$out/bin/leo3" + echo "'${openjdk}/bin/java' -jar '$out/lib/java/leo3/leo3.jar' \"\$@\"" >> "$out/bin/leo3" + chmod a+x "$out/bin/leo3" + ''; + + meta = { + inherit version; + description = "An automated theorem prover for classical higher-order logic with choice"; + license = stdenv.lib.licenses.bsd3; + maintainers = [stdenv.lib.maintainers.raskin]; + platforms = stdenv.lib.platforms.linux; + homepage = "https://page.mi.fu-berlin.de/lex/leo3/"; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/lingeling/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/lingeling/default.nix new file mode 100644 index 000000000000..1805f6cdcc89 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/lingeling/default.nix @@ -0,0 +1,49 @@ +{ stdenv, fetchFromGitHub +, aiger +}: + +stdenv.mkDerivation { + pname = "lingeling"; + # This is the version used in satcomp2018, which was + # relicensed, and also known as version 'bcj' + version = "pre1_03b4860d"; + + src = fetchFromGitHub { + owner = "arminbiere"; + repo = "lingeling"; + rev = "03b4860d14016f42213ea271014f2f13d181f504"; + sha256 = "1lw1yfy219p7rrk88sbq4zl24b70040zapbjdrpv5a6i0jsblksx"; + }; + + configurePhase = '' + ./configure.sh + + # Rather than patch ./configure, just sneak in use of aiger here, since it + # doesn't handle real build products very well (it works on a build-time + # dir, not installed copy)... This is so we can build 'blimc' + substituteInPlace ./makefile \ + --replace 'targets: liblgl.a' 'targets: liblgl.a blimc' \ + --replace '$(AIGER)/aiger.o' '${aiger.lib}/lib/aiger.o' \ + --replace '$(AIGER)/aiger.h' '${aiger.dev}/include/aiger.h' \ + --replace '-I$(AIGER)' '-I${aiger.dev}/include' + ''; + + installPhase = '' + mkdir -p $out/bin $lib/lib $dev/include + + cp lglib.h $dev/include + cp liblgl.a $lib/lib + + cp lingeling plingeling treengeling ilingeling blimc $out/bin + ''; + + outputs = [ "out" "dev" "lib" ]; + + meta = with stdenv.lib; { + description = "Fast SAT solver"; + homepage = "http://fmv.jku.at/lingeling/"; + license = licenses.mit; + platforms = platforms.unix; + maintainers = with maintainers; [ thoughtpolice ]; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/logisim/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/logisim/default.nix new file mode 100644 index 000000000000..ce86b2523116 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/logisim/default.nix @@ -0,0 +1,29 @@ +{ stdenv, fetchurl, jre, makeWrapper }: + +let version = "2.7.1"; in + +stdenv.mkDerivation { + pname = "logisim"; + inherit version; + + src = fetchurl { + url = "mirror://sourceforge/project/circuit/2.7.x/${version}/logisim-generic-${version}.jar"; + sha256 = "1hkvc9zc7qmvjbl9579p84hw3n8wl3275246xlzj136i5b0phain"; + }; + + phases = [ "installPhase" ]; + + nativeBuildInputs = [makeWrapper]; + + installPhase = '' + mkdir -pv $out/bin + makeWrapper ${jre}/bin/java $out/bin/logisim --add-flags "-jar $src" + ''; + + meta = { + homepage = "http://ozark.hendrix.edu/~burch/logisim"; + description = "Educational tool for designing and simulating digital logic circuits"; + license = stdenv.lib.licenses.gpl2Plus; + platforms = stdenv.lib.platforms.unix; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/ltl2ba/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/ltl2ba/default.nix new file mode 100644 index 000000000000..b5d13db3b9a1 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/ltl2ba/default.nix @@ -0,0 +1,31 @@ +{ fetchurl, stdenv }: + +stdenv.mkDerivation rec { + pname = "ltl2ba"; + version = "1.3"; + + src = fetchurl { + url = "http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/${pname}-${version}.tar.gz"; + sha256 = "1bz9gjpvby4mnvny0nmxgd81rim26mqlcnjlznnxxk99575pfa4i"; + }; + + 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/infra/libkookie/nixpkgs/pkgs/applications/science/logic/mcrl2/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/mcrl2/default.nix new file mode 100644 index 000000000000..eb83eaf79c55 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/mcrl2/default.nix @@ -0,0 +1,29 @@ +{stdenv, fetchurl, cmake, libGLU, libGL, qt5, boost}: + +stdenv.mkDerivation rec { + version = "201707"; + build_nr = "1"; + pname = "mcrl2"; + + src = fetchurl { + url = "https://www.mcrl2.org/download/release/mcrl2-${version}.${build_nr}.tar.gz"; + sha256 = "1c8h94ja7271ph61zrcgnjgblxppld6v22f7f900prjgzbcfy14m"; + }; + + buildInputs = [ cmake libGLU libGL 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/infra/libkookie/nixpkgs/pkgs/applications/science/logic/mcy/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/mcy/default.nix new file mode 100644 index 000000000000..eba910e07eb1 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/mcy/default.nix @@ -0,0 +1,51 @@ +{ stdenv, fetchFromGitHub +, yosys, symbiyosys, python3 +}: + +let + python = python3.withPackages (p: with p; [ flask ]); +in +stdenv.mkDerivation { + pname = "mcy"; + version = "2020.08.03"; + + src = fetchFromGitHub { + owner = "YosysHQ"; + repo = "mcy"; + rev = "62048e69df13f8e03670424626755ae8ef4c36ff"; + sha256 = "15xxgzx1zxzx5kshqyrxnfx33cz6cjzxcdcn6z98jhs9bwyvf96f"; + }; + + buildInputs = [ python ]; + patchPhase = '' + chmod +x scripts/create_mutated.sh + patchShebangs . + + substituteInPlace mcy.py \ + --replace yosys '${yosys}/bin/yosys' \ + --replace 'os.execvp("mcy-dash"' "os.execvp(\"$out/bin/mcy-dash\"" + substituteInPlace mcy-dash.py \ + --replace 'app.run(debug=True)' 'app.run(host="0.0.0.0",debug=True)' \ + --replace 'subprocess.Popen(["mcy"' "subprocess.Popen([\"$out/bin/mcy\"" + substituteInPlace scripts/create_mutated.sh \ + --replace yosys '${yosys}/bin/yosys' + ''; + + # the build needs a bit of work... + buildPhase = "true"; + installPhase = '' + mkdir -p $out/bin $out/share/mcy/{dash,scripts} + install mcy.py $out/bin/mcy && chmod +x $out/bin/mcy + install mcy-dash.py $out/bin/mcy-dash && chmod +x $out/bin/mcy-dash + cp -r dash/. $out/share/mcy/dash/. + cp -r scripts/. $out/share/mcy/scripts/. + ''; + + meta = { + description = "Mutation-based coverage testing for hardware designs, with Yosys"; + homepage = "https://github.com/YosysHQ/mcy"; + license = stdenv.lib.licenses.isc; + maintainers = with stdenv.lib.maintainers; [ thoughtpolice ]; + platforms = stdenv.lib.platforms.all; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/metis-prover/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/metis-prover/default.nix new file mode 100644 index 000000000000..5755abfd9078 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/metis-prover/default.nix @@ -0,0 +1,32 @@ +{ stdenv, fetchFromGitHub, perl, mlton }: + +stdenv.mkDerivation { + pname = "metis-prover"; + version = "2.3.20160713"; + + src = fetchFromGitHub { + owner = "gilith"; + repo = "metis"; + rev = "f0b1a17cd57eb098077e963ab092477aee9fb340"; + sha256 = "1i7paax7b4byk8110f5zk4071mh5603r82bq7hbprqzljvsiipk7"; + }; + + nativeBuildInputs = [ perl ]; + buildInputs = [ mlton ]; + + patchPhase = "patchShebangs ."; + + buildPhase = "make mlton"; + + installPhase = '' + install -Dm0755 bin/mlton/metis $out/bin/metis + ''; + + meta = with stdenv.lib; { + description = "Automatic theorem prover for first-order logic with equality"; + homepage = "http://www.gilith.com/research/metis/"; + license = licenses.mit; + maintainers = with maintainers; [ gebner ]; + platforms = platforms.unix; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/minisat/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/minisat/default.nix new file mode 100644 index 000000000000..df1800e6c31b --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/minisat/default.nix @@ -0,0 +1,24 @@ +{ stdenv, fetchFromGitHub, cmake, zlib }: + +stdenv.mkDerivation rec { + pname = "minisat"; + version = "2.2.1"; + + src = fetchFromGitHub { + owner = "stp"; + repo = pname; + rev = "releases/${version}"; + sha256 = "14vcbjnlia00lpyv2fhbmw3wbc9bk9h7bln9zpyc3nwiz5cbjz4a"; + }; + + nativeBuildInputs = [ cmake ]; + buildInputs = [ zlib ]; + + 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/infra/libkookie/nixpkgs/pkgs/applications/science/logic/monosat/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/monosat/default.nix new file mode 100644 index 000000000000..63440213920c --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/monosat/default.nix @@ -0,0 +1,79 @@ +{ stdenv, fetchpatch, fetchFromGitHub, cmake, zlib, gmp, jdk8, + # The JDK we use on Darwin currenly makes extensive use of rpaths which are + # annoying and break the python library, so let's not bother for now + includeJava ? !stdenv.hostPlatform.isDarwin, includeGplCode ? true }: + +with stdenv.lib; + +let + boolToCmake = x: if x then "ON" else "OFF"; + + rev = "1.8.0"; + sha256 = "0q3a8x3iih25xkp2bm842sm2hxlb8hxlls4qmvj7vzwrh4lvsl7b"; + + pname = "monosat"; + version = rev; + + src = fetchFromGitHub { + owner = "sambayless"; + repo = pname; + inherit rev sha256; + }; + + patches = [ + # Python 3.8 compatibility + (fetchpatch { + url = "https://github.com/sambayless/monosat/commit/a5079711d0df0451f9840f3a41248e56dbb03967.patch"; + sha256 = "1p2y0jw8hb9c90nbffhn86k1dxd6f6hk5v70dfmpzka3y6g1ksal"; + }) + ]; + + core = stdenv.mkDerivation { + name = "${pname}-${version}"; + inherit src patches; + buildInputs = [ cmake zlib gmp jdk8 ]; + + cmakeFlags = [ + "-DBUILD_STATIC=OFF" + "-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"; + maintainers = [ maintainers.acairncross ]; + }; + }; + + python = { buildPythonPackage, cython }: buildPythonPackage { + inherit pname version src patches; + + propagatedBuildInputs = [ core cython ]; + + # This tells setup.py to use cython, which should produce faster bindings + MONOSAT_CYTHON = true; + + # After patching src, move to where the actually relevant source is. This could just be made + # the sourceRoot if it weren't for the patch. + postPatch = '' + cd src/monosat/api/python + '' + + # The relative paths here don't make sense for our Nix build + # 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... + '' + substituteInPlace setup.py \ + --replace 'library_dir = "../../../../"' 'library_dir = "${core}/lib/"' + ''; + }; +in core diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/open-wbo/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/open-wbo/default.nix new file mode 100644 index 000000000000..c314127e74bf --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/open-wbo/default.nix @@ -0,0 +1,27 @@ +{ stdenv, fetchFromGitHub, zlib, gmp }: + +stdenv.mkDerivation { + name = "open-wbo-2.0"; + + src = fetchFromGitHub { + owner = "sat-group"; + repo = "open-wbo"; + rev = "f193a3bd802551b13d6424bc1baba6ad35ec6ba6"; + sha256 = "1742i15qfsbf49c4r837wz35c1p7yafvz7ar6vmgcj6cmfwr8jb4"; + }; + + buildInputs = [ zlib gmp ]; + + makeFlags = [ "r" ]; + installPhase = '' + install -Dm0755 open-wbo_release $out/bin/open-wbo + ''; + + meta = with stdenv.lib; { + description = "State-of-the-art MaxSAT and Pseudo-Boolean solver"; + maintainers = with maintainers; [ gebner ]; + platforms = platforms.unix; + license = licenses.mit; + homepage = "http://sat.inesc-id.pt/open-wbo/"; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/opensmt/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/opensmt/default.nix new file mode 100644 index 000000000000..03b3ce4ff0b7 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/opensmt/default.nix @@ -0,0 +1,25 @@ +{ stdenv, fetchurl, automake, libtool, autoconf, intltool, perl +, gmpxx, flex, bison +}: + +stdenv.mkDerivation rec { + pname = "opensmt"; + version = "20101017"; + + src = fetchurl { + url = "http://opensmt.googlecode.com/files/opensmt_src_${version}.tgz"; + sha256 = "0xrky7ixjaby5x026v7hn72xh7d401w9jhccxjn0khhn1x87p2w1"; + }; + + buildInputs = [ automake libtool autoconf intltool perl gmpxx flex bison ]; + + meta = with stdenv.lib; { + description = "A satisfiability modulo theory (SMT) solver"; + maintainers = [ maintainers.raskin ]; + platforms = platforms.linux; + license = licenses.gpl3; + homepage = "http://code.google.com/p/opensmt/"; + broken = true; + downloadPage = "http://code.google.com/p/opensmt/downloads/list"; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/ott/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/ott/default.nix new file mode 100644 index 000000000000..48ad63eaa993 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/ott/default.nix @@ -0,0 +1,39 @@ +{ stdenv, fetchFromGitHub, pkgconfig, ocaml, opaline }: + +stdenv.mkDerivation rec { + pname = "ott"; + version = "0.31"; + + src = fetchFromGitHub { + owner = "ott-lang"; + repo = "ott"; + rev = version; + sha256 = "0l81126i2qkz11fs5yrjdgymnqgjcs5avb7f951h61yh1s68jpnn"; + }; + + nativeBuildInputs = [ pkgconfig opaline ]; + buildInputs = [ ocaml ]; + + installTargets = "ott.install"; + + postInstall = "opaline -prefix $out"; + + meta = { + description = "A 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/infra/libkookie/nixpkgs/pkgs/applications/science/logic/otter/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/otter/default.nix new file mode 100644 index 000000000000..a7eec20548c9 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/otter/default.nix @@ -0,0 +1,53 @@ +{stdenv, fetchurl, tcsh, libXaw, libXt, libX11}: +let + s = # Generated upstream information + rec { + version = "3.3f"; + name = "otter"; + url = "https://www.cs.unm.edu/~mccune/otter/otter-${version}.tar.gz"; + sha256 = "16mc1npl7sk9cmqhrf3ghfmvx29inijw76f1b1lsykllaxjqqb1r"; + }; + buildInputs = [ + tcsh libXaw libXt libX11 + ]; +in +stdenv.mkDerivation { + name = "${s.name}-${s.version}"; + inherit buildInputs; + src = fetchurl { + inherit (s) url sha256; + }; + + hardeningDisable = [ "format" ]; + + buildPhase = '' + find . -name Makefile | xargs sed -i -e "s@/bin/rm@$(type -P rm)@g" + find . -name Makefile | xargs sed -i -e "s@/bin/mv@$(type -P mv)@g" + find . -perm -0100 -type f | xargs sed -i -e "s@/bin/csh@$(type -P csh)@g" + find . -perm -0100 -type f | xargs sed -i -e "s@/bin/rm@$(type -P rm)@g" + find . -perm -0100 -type f | xargs sed -i -e "s@/bin/mv@$(type -P mv)@g" + + sed -i -e "s/^XLIBS *=.*/XLIBS=-lXaw -lXt -lX11/" source/formed/Makefile + + make all + make -C examples all + make -C examples-mace2 all + make -C source/formed realclean + make -C source/formed formed + ''; + + installPhase = '' + mkdir -p "$out"/{bin,share/otter} + cp bin/* source/formed/formed "$out/bin/" + cp -r examples examples-mace2 documents README* Legal Changelog Contents index.html "$out/share/otter/" + ''; + + meta = { + inherit (s) version; + description = "A reliable first-order theorem prover"; + license = stdenv.lib.licenses.publicDomain ; + maintainers = [stdenv.lib.maintainers.raskin]; + platforms = stdenv.lib.platforms.linux; + broken = true; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/petrinizer/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/petrinizer/default.nix new file mode 100644 index 000000000000..d277e0e1521a --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/petrinizer/default.nix @@ -0,0 +1,31 @@ +{ mkDerivation, callPackage, buildPackages +, async, base, bytestring, containers, fetchFromGitLab, mtl +, parallel-io, parsec, stdenv, stm, transformers +}: +let + z3 = callPackage ./z3.nix { gomp = null; z3 = buildPackages.z3; }; +in let + sbv = callPackage ./sbv-7.13.nix { inherit z3; }; +in +mkDerivation rec { + pname = "petrinizer"; + version = "0.9.1.1"; + + src = fetchFromGitLab { + domain = "gitlab.lrz.de"; + owner = "i7"; + repo = pname; + rev = version; + sha256 = "1n7fzm96gq5rxm2f8w8sr1yzm1zcxpf0b473c6xnhsgqsis5j4xw"; + }; + + isLibrary = false; + isExecutable = true; + executableHaskellDepends = [ + async base bytestring containers mtl parallel-io parsec sbv stm + transformers + ]; + description = "Safety and Liveness Analysis of Petri Nets with SMT solvers"; + license = stdenv.lib.licenses.gpl3; + maintainers = with stdenv.lib.maintainers; [ raskin ]; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/petrinizer/sbv-7.13.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/petrinizer/sbv-7.13.nix new file mode 100644 index 000000000000..ed10e9f3db19 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/petrinizer/sbv-7.13.nix @@ -0,0 +1,26 @@ +{ mkDerivation, array, async, base, bytestring, containers +, crackNum, deepseq, directory, doctest, filepath, generic-deriving +, ghc, Glob, hlint, mtl, pretty, process, QuickCheck, random +, stdenv, syb, tasty, tasty-golden, tasty-hunit, tasty-quickcheck +, template-haskell, time, z3 +}: +mkDerivation { + pname = "sbv"; + version = "7.13"; + sha256 = "0bk400swnb4s98c5p71ml1px6jndaiqhf5dj7zmnliyplqcgpfik"; + enableSeparateDataOutput = true; + libraryHaskellDepends = [ + array async base containers crackNum deepseq directory filepath + generic-deriving ghc mtl pretty process QuickCheck random syb + template-haskell time + ]; + testHaskellDepends = [ + base bytestring containers crackNum directory doctest filepath Glob + hlint mtl QuickCheck random syb tasty tasty-golden tasty-hunit + tasty-quickcheck template-haskell + ]; + testSystemDepends = [ z3 ]; + homepage = "http://leventerkok.github.com/sbv/"; + description = "SMT Based Verification: Symbolic Haskell theorem prover using SMT solving"; + license = stdenv.lib.licenses.bsd3; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/petrinizer/z3.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/petrinizer/z3.nix new file mode 100644 index 000000000000..4d868054c09b --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/petrinizer/z3.nix @@ -0,0 +1,24 @@ +{ mkDerivation, fetchpatch +, base, containers, gomp, hspec, QuickCheck, stdenv +, transformers, z3 +}: +mkDerivation { + pname = "z3"; + version = "408.0"; + sha256 = "13qkzy9wc17rm60i24fa9sx15ywbxq4a80g33w20887gvqyc0q53"; + isLibrary = true; + isExecutable = true; + libraryHaskellDepends = [ base containers transformers ]; + librarySystemDepends = [ gomp z3 ]; + testHaskellDepends = [ base hspec QuickCheck ]; + homepage = "https://github.com/IagoAbal/haskell-z3"; + description = "Bindings for the Z3 Theorem Prover"; + license = stdenv.lib.licenses.bsd3; + doCheck = false; + patches = [ + (fetchpatch { + url = "https://github.com/IagoAbal/haskell-z3/commit/b10e09b8a809fb5bbbb1ef86aeb62109ece99cae.patch"; + sha256 = "13fnrs27mg3985r3lwks8fxfxr5inrayy2cyx2867d92pnl3yry4"; + }) + ]; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/picosat/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/picosat/default.nix new file mode 100644 index 000000000000..b13d871580c5 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/picosat/default.nix @@ -0,0 +1,44 @@ +{ stdenv, fetchurl }: + +stdenv.mkDerivation rec { + pname = "picosat"; + version = "965"; + + src = fetchurl { + url = "http://fmv.jku.at/picosat/${pname}-${version}.tar.gz"; + sha256 = "0m578rpa5rdn08d10kr4lbsdwp4402hpavrz6n7n53xs517rn5hm"; + }; + + prePatch = '' + substituteInPlace picosat.c --replace "sys/unistd.h" "unistd.h" + + substituteInPlace makefile.in \ + --replace 'ar rc' '$(AR) rc' \ + --replace 'ranlib' '$(RANLIB)' + ''; + + configurePhase = "./configure.sh --shared --trace"; + + makeFlags = stdenv.lib.optional stdenv.isDarwin + "SONAME=-Wl,-install_name,$(out)/lib/libpicosat.so"; + + installPhase = '' + mkdir -p $out/bin $out/lib $out/share $out/include/picosat + cp picomus picomcs picosat picogcnf "$out"/bin + + cp VERSION "$out"/share/picosat.version + cp picosat.o "$out"/lib + cp libpicosat.a "$out"/lib + cp libpicosat.so "$out"/lib + + cp picosat.h "$out"/include/picosat + ''; + + meta = { + description = "SAT solver with proof and core support"; + homepage = "http://fmv.jku.at/picosat/"; + license = stdenv.lib.licenses.mit; + platforms = stdenv.lib.platforms.unix; + maintainers = with stdenv.lib.maintainers; [ roconnor thoughtpolice ]; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/poly/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/poly/default.nix new file mode 100644 index 000000000000..ee50a2d85040 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/poly/default.nix @@ -0,0 +1,25 @@ +{stdenv, fetchFromGitHub, gmp, cmake, python}: + +stdenv.mkDerivation rec { + pname = "libpoly"; + version = "0.1.8"; + + src = fetchFromGitHub { + owner = "SRI-CSL"; + repo = "libpoly"; + # they've pushed to the release branch, use explicit tag + rev = "refs/tags/v${version}"; + sha256 = "1n3gijksnl2ybznq4lkwm2428f82423sxq18gnb2g1kiwqlzdaa3"; + }; + + 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/infra/libkookie/nixpkgs/pkgs/applications/science/logic/potassco/clingcon.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/potassco/clingcon.nix new file mode 100644 index 000000000000..b74583ca1a2c --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/potassco/clingcon.nix @@ -0,0 +1,43 @@ +{ stdenv +, fetchFromGitHub +, cmake +, bison +, re2c +}: + +stdenv.mkDerivation rec { + pname = "clingcon"; + version = "3.3.0"; + + src = fetchFromGitHub { + owner = "potassco"; + repo = pname; + rev = "v${version}"; + fetchSubmodules = true; + sha256 = "1q7517h10jfvjdk2czq8d6y57r8kr1j1jj2k2ip2qxkpyfigk4rs"; + }; + + # deal with clingcon through git submodules recursively importing + # an outdated version of libpotassco which uses deprecated <xlocale.h> header in .cpp files + postPatch = '' + find ./ -type f -exec sed -i 's/<xlocale.h>/<locale.h>/g' {} \; + ''; + + nativeBuildInputs = [ cmake bison re2c ]; + + cmakeFlags = [ + "-DCLINGCON_MANAGE_RPATH=ON" + "-DCLINGO_BUILD_WITH_PYTHON=OFF" + "-DCLINGO_BUILD_WITH_LUA=OFF" + ]; + + meta = { + inherit version; + description = "Extension of clingo to handle constraints over integers"; + license = stdenv.lib.licenses.gpl3; # for now GPL3, next version MIT! + platforms = stdenv.lib.platforms.unix; + homepage = "https://potassco.org/"; + downloadPage = "https://github.com/potassco/clingcon/releases/"; + changelog = "https://github.com/potassco/clingcon/releases/tag/v${version}"; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/potassco/clingo.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/potassco/clingo.nix new file mode 100644 index 000000000000..7c1ee8099e2c --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/potassco/clingo.nix @@ -0,0 +1,25 @@ +{ stdenv, fetchzip, cmake }: + +stdenv.mkDerivation rec { + pname = "clingo"; + version = "5.4.0"; + + src = fetchzip { + url = "https://github.com/potassco/clingo/archive/v${version}.tar.gz"; + sha256 = "0gfqlgwg3qx042w6hdc9qpmr50n4vci3p0ddk28f3kqacf6q9q7m"; + }; + + 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/infra/libkookie/nixpkgs/pkgs/applications/science/logic/potassco/clingo.upstream b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/potassco/clingo.upstream new file mode 100644 index 000000000000..062577d1451b --- /dev/null +++ b/infra/libkookie/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/infra/libkookie/nixpkgs/pkgs/applications/science/logic/prooftree/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/prooftree/default.nix new file mode 100644 index 000000000000..98313e48cb27 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/prooftree/default.nix @@ -0,0 +1,43 @@ +{ stdenv, fetchurl, pkgconfig, ncurses, ocamlPackages }: + +stdenv.mkDerivation rec { + pname = "prooftree"; + version = "0.13"; + + src = fetchurl { + url = "https://askra.de/software/prooftree/releases/prooftree-${version}.tar.gz"; + sha256 = "0z1z4wqbqwgppkh2bm89fgy07a0y2m6g4lvcyzs09sm1ysklk2dh"; + }; + + nativeBuildInputs = [ pkgconfig ]; + buildInputs = [ ncurses ] ++ (with ocamlPackages; [ + ocaml findlib camlp5 lablgtk ]); + + dontAddPrefix = true; + configureFlags = [ "--prefix" "$(out)" ]; + + meta = with stdenv.lib; { + description = "A program for proof-tree visualization"; + longDescription = '' + Prooftree is a program for proof-tree visualization during interactive + proof development in a theorem prover. It is currently being developed + for Coq and Proof General. Prooftree helps against getting lost between + different subgoals in interactive proof development. It clearly shows + where the current subgoal comes from and thus helps in developing the + right plan for solving it. + + Prooftree uses different colors for the already proven subgoals, the + current branch in the proof and the still open subgoals. Sequent texts + are not displayed in the proof tree itself, but they are shown as a + tool-tip when the mouse rests over a sequent symbol. Long proof commands + are abbreviated in the tree display, but show up in full length as + tool-tip. Both, sequents and proof commands, can be shown in the display + below the tree (on single click) or in a separate window (on double or + shift-click). + ''; + homepage = "http://askra.de/software/prooftree"; + platforms = platforms.unix; + maintainers = [ maintainers.jwiegley ]; + license = licenses.gpl3; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/prover9/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/prover9/default.nix new file mode 100644 index 000000000000..fcdff8558483 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/prover9/default.nix @@ -0,0 +1,45 @@ +{stdenv, fetchurl}: + +stdenv.mkDerivation { + name = "prover9-2009-11a"; + + src = fetchurl { + url = "https://www.cs.unm.edu/~mccune/mace4/download/LADR-2009-11A.tar.gz"; + sha256 = "1l2i3d3h5z7nnbzilb6z92r0rbx0kh6yaxn2c5qhn3000xcfsay3"; + }; + + hardeningDisable = [ "format" ]; + + patchPhase = '' + RM=$(type -tp rm) + MV=$(type -tp mv) + CP=$(type -tp cp) + for f in Makefile */Makefile; do + substituteInPlace $f --replace "/bin/rm" "$RM" \ + --replace "/bin/mv" "$MV" \ + --replace "/bin/cp" "$CP"; + done + ''; + + buildFlags = [ "all" ]; + + checkPhase = "make test1"; + + installPhase = '' + mkdir -p $out/bin + cp bin/* $out/bin + ''; + + meta = { + homepage = "https://www.cs.unm.edu/~mccune/mace4/"; + license = "GPL"; + description = "Automated theorem prover for first-order and equational logic"; + longDescription = '' + Prover9 is a resolution/paramodulation automated theorem prover + for first-order and equational logic. Prover9 is a successor of + the Otter Prover. This is the LADR command-line version. + ''; + platforms = stdenv.lib.platforms.linux; + maintainers = []; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/proverif/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/proverif/default.nix new file mode 100644 index 000000000000..4242bb0599e9 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/proverif/default.nix @@ -0,0 +1,29 @@ +{ stdenv, fetchurl, ocamlPackages }: + +stdenv.mkDerivation rec { + pname = "proverif"; + version = "2.02pl1"; + + src = fetchurl { + url = "http://prosecco.gforge.inria.fr/personal/bblanche/proverif/proverif${version}.tar.gz"; + sha256 = "1jmzfpx0hdgfmkq0jp6i3k5av9xxgndjaj743wfy37svn0ga4jjx"; + }; + + buildInputs = with ocamlPackages; [ ocaml findlib lablgtk ]; + + buildPhase = "./build"; + installPhase = '' + mkdir -p $out/bin + cp ./proverif $out/bin + cp ./proveriftotex $out/bin + install -D -t $out/share/emacs/site-lisp/ emacs/proverif.el + ''; + + meta = { + description = "Cryptographic protocol verifier in the Dolev-Yao model"; + homepage = "https://prosecco.gforge.inria.fr/personal/bblanche/proverif/"; + license = stdenv.lib.licenses.gpl2; + platforms = stdenv.lib.platforms.unix; + maintainers = [ stdenv.lib.maintainers.thoughtpolice ]; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/redprl/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/redprl/default.nix new file mode 100644 index 000000000000..49245c73f2c4 --- /dev/null +++ b/infra/libkookie/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/infra/libkookie/nixpkgs/pkgs/applications/science/logic/sad/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/sad/default.nix new file mode 100644 index 000000000000..77613a135710 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/sad/default.nix @@ -0,0 +1,40 @@ +{ stdenv, fetchurl, haskell, spass }: + +stdenv.mkDerivation { + name = "system-for-automated-deduction-2.3.25"; + src = fetchurl { + url = "http://nevidal.org/download/sad-2.3-25.tar.gz"; + sha256 = "10jd93xgarik7xwys5lq7fx4vqp7c0yg1gfin9cqfch1k1v8ap4b"; + }; + buildInputs = [ haskell.compiler.ghc844 spass ]; + patches = [ + ./patch.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; + broken = true; # ghc-8.4.4 is gone from Nixpkgs + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/sad/monoid.patch b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/sad/monoid.patch new file mode 100644 index 000000000000..da9c21bcae91 --- /dev/null +++ b/infra/libkookie/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/infra/libkookie/nixpkgs/pkgs/applications/science/logic/sad/patch.patch b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/sad/patch.patch new file mode 100644 index 000000000000..a5b1d6177083 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/sad/patch.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/infra/libkookie/nixpkgs/pkgs/applications/science/logic/satallax/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/satallax/default.nix new file mode 100644 index 000000000000..6c2b03b5b37d --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/satallax/default.nix @@ -0,0 +1,71 @@ +{stdenv, fetchurl, ocaml, zlib, which, eprover, makeWrapper, coq}: +stdenv.mkDerivation rec { + pname = "satallax"; + version = "2.7"; + + buildInputs = [ocaml zlib which eprover makeWrapper coq]; + src = fetchurl { + url = "https://www.ps.uni-saarland.de/~cebrown/satallax/downloads/${pname}-${version}.tar.gz"; + sha256 = "1kvxn8mc35igk4vigi5cp7w3wpxk2z3bgwllfm4n3h2jfs0vkpib"; + }; + + patches = [ + # GCC9 doesn't allow default value in friend declaration. + ./fix-declaration-gcc9.patch + ]; + + 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/infra/libkookie/nixpkgs/pkgs/applications/science/logic/satallax/fix-declaration-gcc9.patch b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/satallax/fix-declaration-gcc9.patch new file mode 100644 index 000000000000..1933fc25c4da --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/satallax/fix-declaration-gcc9.patch @@ -0,0 +1,21 @@ +diff --git i/minisat/core/SolverTypes.h w/minisat/core/SolverTypes.h +--- i/minisat/core/SolverTypes.h ++++ w/minisat/core/SolverTypes.h +@@ -47,7 +47,7 @@ struct Lit { + int x; + + // Use this as a constructor: +- friend Lit mkLit(Var var, bool sign = false); ++ friend Lit mkLit(Var var, bool sign); + + bool operator == (Lit p) const { return x == p.x; } + bool operator != (Lit p) const { return x != p.x; } +@@ -55,7 +55,7 @@ struct Lit { + }; + + +-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 --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/saw-tools/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/saw-tools/default.nix new file mode 100644 index 000000000000..71b26f8023a2 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/saw-tools/default.nix @@ -0,0 +1,60 @@ +{ stdenv, fetchurl, gmp4, ncurses, zlib, clang }: + +let + libPath = stdenv.lib.makeLibraryPath + [ stdenv.cc.libc + stdenv.cc.cc + gmp4 + ncurses + zlib + ] + ":${stdenv.cc.cc.lib}/lib64"; + + url = "https://github.com/GaloisInc/saw-script/releases/download"; + + saw-bin = + if stdenv.hostPlatform.system == "i686-linux" + then fetchurl { + url = url + "/v0.1.1-dev/saw-0.1.1-dev-2015-07-31-CentOS6-32.tar.gz"; + sha256 = "126iag5nnvndi78c921z7vjrjfwcspn1hlxwwhzmqm4rvbhhr9v9"; + } + else fetchurl { + url = url + "/v0.1.1-dev/saw-0.1.1-dev-2015-07-31-CentOS6-64.tar.gz"; + sha256 = "07gyf319v6ama6n1aj96403as04bixi8mbisfy7f7va689zklflr"; + }; +in +stdenv.mkDerivation { + pname = "saw-tools"; + version = "0.1.1-20150731"; + + src = saw-bin; + + installPhase = '' + mkdir -p $out/lib $out/share + + mv bin $out/bin + mv doc $out/share + + ln -s ${ncurses.out}/lib/libtinfo.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}/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/infra/libkookie/nixpkgs/pkgs/applications/science/logic/spass/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/spass/default.nix new file mode 100644 index 000000000000..ece6f0b9f6a8 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/spass/default.nix @@ -0,0 +1,42 @@ +{ stdenv, fetchurl, bison, flex }: + +let + baseVersion="3"; + minorVersion="9"; + + extraTools = "FLOTTER prolog2dfg dfg2otter dfg2dimacs dfg2tptp" + + " dfg2ascii dfg2dfg tptp2dfg dimacs2dfg pgen rescmp"; +in + +stdenv.mkDerivation { + pname = "spass"; + version = "${baseVersion}.${minorVersion}"; + + src = fetchurl { + url = "http://www.spass-prover.org/download/sources/spass${baseVersion}${minorVersion}.tgz"; + sha256 = "11cyn3kcff4r79rsw2s0xm6rdb8bi0kpkazv2b48jhcms7xw75qp"; + }; + + sourceRoot = "."; + + nativeBuildInputs = [ bison flex ]; + + buildPhase = '' + make RM="rm -f" proparser.c ${extraTools} opt + ''; + installPhase = '' + mkdir -p $out/bin + install -m0755 SPASS ${extraTools} $out/bin/ + ''; + + meta = with stdenv.lib; { + description = "Automated theorem prover for first-order logic"; + maintainers = with maintainers; + [ + raskin + ]; + platforms = platforms.unix; + license = licenses.bsd2; + downloadPage = "http://www.spass-prover.org/download/index.html"; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/statverif/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/statverif/default.nix new file mode 100644 index 000000000000..e0efb28819d2 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/statverif/default.nix @@ -0,0 +1,34 @@ +{ stdenv, fetchurl, ocaml }: + +stdenv.mkDerivation rec { + pname = "statverif"; + version = "1.86pl4"; + + src = fetchurl { + url = "http://prosecco.gforge.inria.fr/personal/bblanche/proverif/proverif${version}.tar.gz"; + sha256 = "163vdcixs764jj8xa08w80qm4kcijf7xj911yp8jvz6pi1q5g13i"; + }; + + pf-patch = fetchurl { + url = "http://markryan.eu/research/statverif/files/proverif-${version}-statverif-2657ab4.patch"; + sha256 = "113jjhi1qkcggbsmbw8fa9ln8vs7vy2r288szks7rn0jjn0wxmbw"; + }; + + buildInputs = [ ocaml ]; + + patchPhase = "patch -p1 < ${pf-patch}"; + buildPhase = "./build"; + installPhase = '' + mkdir -p $out/bin + cp ./proverif $out/bin/statverif + cp ./proveriftotex $out/bin/statveriftotex + ''; + + meta = { + description = "Verification of stateful processes (via Proverif)"; + homepage = "https://markryan.eu/research/statverif/"; + license = stdenv.lib.licenses.gpl2; + platforms = stdenv.lib.platforms.unix; + maintainers = [ stdenv.lib.maintainers.thoughtpolice ]; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/stp/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/stp/default.nix new file mode 100644 index 000000000000..dd00eda1b571 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/stp/default.nix @@ -0,0 +1,36 @@ +{ stdenv, cmake, boost, bison, flex, fetchFromGitHub, perl +, python3, python3Packages, zlib, minisat, cryptominisat }: + +stdenv.mkDerivation rec { + pname = "stp"; + version = "2.3.3"; + + src = fetchFromGitHub { + owner = "stp"; + repo = "stp"; + rev = version; + sha256 = "1yg2v4wmswh1sigk47drwsxyayr472mf4i47lqmlcgn9hhbx1q87"; + }; + + buildInputs = [ boost zlib minisat cryptominisat python3 ]; + nativeBuildInputs = [ cmake bison flex perl ]; + preConfigure = '' + python_install_dir=$out/${python3Packages.python.sitePackages} + mkdir -p $python_install_dir + cmakeFlagsArray=( + $cmakeFlagsArray + "-DBUILD_SHARED_LIBS=ON" + "-DPYTHON_LIB_INSTALL_DIR=$python_install_dir" + ) + ''; + + # seems to build fine now, may revert if concurrency does become an issue + enableParallelBuilding = true; + + meta = with stdenv.lib; { + description = "Simple Theorem Prover"; + maintainers = with maintainers; [ ]; + platforms = platforms.linux; + license = licenses.mit; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/symbiyosys/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/symbiyosys/default.nix new file mode 100644 index 000000000000..9cf8b0845d43 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/symbiyosys/default.nix @@ -0,0 +1,58 @@ +{ stdenv, fetchFromGitHub +, bash, python3, yosys +, yices, boolector, z3, aiger +}: + +stdenv.mkDerivation { + pname = "symbiyosys"; + version = "2020.08.22"; + + src = fetchFromGitHub { + owner = "YosysHQ"; + repo = "SymbiYosys"; + rev = "33b0bb7d836fe2a73dc7b10587222f2a718beef4"; + sha256 = "03rbrbwsji1sqcp2yhgbc0fca04zsryv2g4izjhdzv64nqjzjyhn"; + }; + + buildInputs = [ ]; + patchPhase = '' + patchShebangs . + + # Fix up Yosys imports + substituteInPlace sbysrc/sby.py \ + --replace "##yosys-sys-path##" \ + "sys.path += [p + \"/share/yosys/python3/\" for p in [\"$out\", \"${yosys}\"]]" + + # Fix various executable references + substituteInPlace sbysrc/sby_core.py \ + --replace '"/usr/bin/env", "bash"' '"${bash}/bin/bash"' \ + --replace ', "btormc"' ', "${boolector}/bin/btormc"' \ + --replace ', "aigbmc"' ', "${aiger}/bin/aigbmc"' + + substituteInPlace sbysrc/sby_core.py \ + --replace '##yosys-program-prefix##' '"${yosys}/bin/"' + ''; + + 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 + ''; + + doCheck = false; # not all provers are yet packaged... + checkInputs = [ python3 yosys boolector yices z3 aiger ]; + checkPhase = "make test"; + + meta = { + description = "Tooling for Yosys-based verification flows"; + homepage = "https://symbiyosys.readthedocs.io/"; + license = stdenv.lib.licenses.isc; + maintainers = with stdenv.lib.maintainers; [ thoughtpolice emily ]; + platforms = stdenv.lib.platforms.all; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/tamarin-prover/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/tamarin-prover/default.nix new file mode 100644 index 000000000000..d217e2b9b505 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/tamarin-prover/default.nix @@ -0,0 +1,95 @@ +{ haskellPackages, mkDerivation, fetchFromGitHub, lib +# the following are non-haskell dependencies +, makeWrapper, which, maude, graphviz +}: + +let + version = "1.6.0"; + src = fetchFromGitHub { + owner = "tamarin-prover"; + repo = "tamarin-prover"; + rev = version; + sha256 = "1pl3kz7gyw9g6s4x5j90z4snd10vq6296g3ajlr8d4n53p3c9i3w"; + }; + + # tamarin has its own dependencies, but they're kept inside the repo, + # no submodules. this factors out the common metadata among all derivations + common = pname: src: { + inherit pname version src; + + license = lib.licenses.gpl3; + homepage = "https://tamarin-prover.github.io"; + description = "Security protocol verification in the symbolic model"; + maintainers = [ lib.maintainers.thoughtpolice ]; + }; + + # tamarin use symlinks to the LICENSE and Setup.hs files, so for these sublibraries + # we set the patchPhase to fix that. otherwise, cabal cries a lot. + replaceSymlinks = '' + cp --remove-destination ${src}/LICENSE .; + cp --remove-destination ${src}/Setup.hs .; + ''; + + tamarin-prover-utils = mkDerivation (common "tamarin-prover-utils" (src + "/lib/utils") // { + postPatch = replaceSymlinks; + libraryHaskellDepends = with haskellPackages; [ + base64-bytestring blaze-builder + dlist exceptions fclabels safe SHA syb + ]; + }); + + tamarin-prover-term = mkDerivation (common "tamarin-prover-term" (src + "/lib/term") // { + postPatch = replaceSymlinks; + libraryHaskellDepends = (with haskellPackages; [ + attoparsec HUnit + ]) ++ [ tamarin-prover-utils ]; + }); + + tamarin-prover-theory = mkDerivation (common "tamarin-prover-theory" (src + "/lib/theory") // { + postPatch = replaceSymlinks; + doHaddock = false; # broken + libraryHaskellDepends = (with haskellPackages; [ + aeson aeson-pretty parallel uniplate + ]) ++ [ tamarin-prover-utils tamarin-prover-term ]; + }); + + tamarin-prover-sapic = mkDerivation (common "tamarin-prover-sapic" (src + "/lib/sapic") // { + postPatch = "cp --remove-destination ${src}/LICENSE ."; + doHaddock = false; # broken + libraryHaskellDepends = (with haskellPackages; [ + raw-strings-qq + ]) ++ [ tamarin-prover-theory ]; + }); + +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"; + + # wrap the prover to be sure it can find maude, sapic, etc + executableToolDepends = [ makeWrapper which maude graphviz ]; + postInstall = '' + wrapProgram $out/bin/tamarin-prover \ + --prefix PATH : ${lib.makeBinPath [ which maude graphviz ]} + # so that the package can be used as a vim plugin to install syntax coloration + install -Dt $out/share/vim-plugins/tamarin-prover/syntax/ etc/syntax/spthy.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; [ + binary-instances binary-orphans blaze-html conduit file-embed + gitrev http-types lifted-base monad-control monad-unlift + resourcet shakespeare threads wai warp yesod-core yesod-static + ]) ++ [ tamarin-prover-utils + tamarin-prover-sapic + tamarin-prover-term + tamarin-prover-theory + ]; +}) diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/tlaplus/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/tlaplus/default.nix new file mode 100644 index 000000000000..14944f5e19b0 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/tlaplus/default.nix @@ -0,0 +1,40 @@ +{ stdenv, fetchFromGitHub, makeWrapper +, adoptopenjdk-bin, jre, ant +}: + +stdenv.mkDerivation rec { + pname = "tlaplus"; + version = "1.7.0"; + + src = fetchFromGitHub { + owner = "tlaplus"; + repo = "tlaplus"; + rev = "refs/tags/v${version}"; + sha256 = "1mm6r9bq79zks50yk0agcpdkw9yy994m38ibmgpb3bi3wkpq9891"; + }; + + buildInputs = [ makeWrapper adoptopenjdk-bin ant ]; + + buildPhase = "ant -f tlatools/org.lamport.tlatools/customBuild.xml compile dist"; + installPhase = '' + mkdir -p $out/share/java $out/bin + cp tlatools/org.lamport.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/infra/libkookie/nixpkgs/pkgs/applications/science/logic/tlaplus/tlaps.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/tlaplus/tlaps.nix new file mode 100644 index 000000000000..3872d3a9826b --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/tlaplus/tlaps.nix @@ -0,0 +1,54 @@ +{ fetchurl +, stdenv +, ocaml, isabelle, cvc3, perl, wget, which +}: + +stdenv.mkDerivation rec { + pname = "tlaps"; + version = "1.4.3"; + src = fetchurl { + url = "https://tla.msr-inria.inria.fr/tlaps/dist/current/tlaps-${version}.tar.gz"; + sha256 = "1w5z3ns5xxmhmp8r4x2kjmy3clqam935gmvx82imyxrr1bamx6gf"; + }; + + buildInputs = [ ocaml isabelle cvc3 perl wget which ]; + + phases = [ "unpackPhase" "installPhase" ]; + + installPhase = '' + mkdir -pv "$out" + export HOME="$out" + export PATH=$out/bin:$PATH + + pushd zenon + ./configure --prefix $out + make + make install + popd + + pushd isabelle + isabelle build -b Pure + popd + + pushd tlapm + ./configure --prefix $out + make all + make install + ''; + + meta = { + description = "Mechanically check TLA+ proofs"; + longDescription = '' + TLA+ is a general-purpose formal specification language that is + particularly useful for describing concurrent and distributed + systems. The TLA+ proof language is declarative, hierarchical, + and scalable to large system specifications. It provides a + consistent abstraction over the various “backend” verifiers. + ''; + homepage = "https://tla.msr-inria.inria.fr/tlaps/content/Home.html"; + license = stdenv.lib.licenses.bsd2; + platforms = stdenv.lib.platforms.unix; + maintainers = [ ]; + }; + +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/tlaplus/toolbox.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/tlaplus/toolbox.nix new file mode 100644 index 000000000000..c9e97375b6c7 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/tlaplus/toolbox.nix @@ -0,0 +1,81 @@ +{ lib, fetchzip, makeWrapper, makeDesktopItem, stdenv +, gtk, libXtst, glib, zlib +}: + +let + version = "1.7.0"; + arch = "x86_64"; + + desktopItem = makeDesktopItem rec { + name = "TLA+Toolbox"; + exec = "tla-toolbox"; + icon = "tla-toolbox"; + comment = "IDE for TLA+"; + desktopName = name; + genericName = comment; + categories = "Development"; + extraEntries = '' + StartupWMClass=TLA+ Toolbox + ''; + }; + + +in stdenv.mkDerivation { + pname = "tla-toolbox"; + inherit version; + src = fetchzip { + url = "https://tla.msr-inria.inria.fr/tlatoolbox/products/TLAToolbox-${version}-linux.gtk.${arch}.zip"; + sha256 = "0v15wscawair5bghr5ixb4i062kmh9by1m0hnz2r1sawlqyafz02"; + }; + + buildInputs = [ makeWrapper ]; + + phases = [ "installPhase" ]; + + installPhase = '' + mkdir -p "$out/bin" + cp -r "$src" "$out/toolbox" + chmod -R +w "$out/toolbox" + + patchelf \ + --set-interpreter $(cat $NIX_CC/nix-support/dynamic-linker) \ + "$out/toolbox/toolbox" + + patchelf \ + --set-interpreter $(cat $NIX_CC/nix-support/dynamic-linker) \ + "$(find "$out/toolbox" -name java)" + + makeWrapper $out/toolbox/toolbox $out/bin/tla-toolbox \ + --run "set -x; cd $out/toolbox" \ + --add-flags "-data ~/.tla-toolbox" \ + --prefix LD_LIBRARY_PATH : "${lib.makeLibraryPath [ gtk libXtst glib zlib ]}" + + echo -e "\nCreating TLA Toolbox icons..." + pushd "$src" + for icon_in in $(find . -path "./plugins/*/icons/full/etool16/tla_launch_check_wiz_*.png") + do + icon_size=$(echo $icon_in | grep -Po "wiz_\K[0-9]+") + icon_out="$out/share/icons/hicolor/$icon_size""x$icon_size/apps/tla-toolbox.png" + mkdir -p "$(dirname $icon_out)" + cp "$icon_in" "$icon_out" + done + popd + + echo -e "\nCreating TLA Toolbox desktop entry..." + cp -r "${desktopItem}/share/applications"* "$out/share/applications" + ''; + + meta = { + homepage = "http://research.microsoft.com/en-us/um/people/lamport/tla/toolbox.html"; + description = "IDE for the TLA+ tools"; + longDescription = '' + Integrated development environment for the TLA+ tools, based on Eclipse. You can use it + to create and edit your specs, run the PlusCal translator, view the pretty-printed + versions of your modules, run the TLC model checker, and run TLAPS, the TLA+ proof system. + ''; + # http://lamport.azurewebsites.net/tla/license.html + license = with lib.licenses; [ mit ]; + platforms = stdenv.lib.platforms.linux; + maintainers = [ ]; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/tptp/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/tptp/default.nix new file mode 100644 index 000000000000..4c63f8e72a36 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/tptp/default.nix @@ -0,0 +1,49 @@ +{ stdenv, fetchurl, yap, tcsh, perl, patchelf }: + +stdenv.mkDerivation rec { + pname = "TPTP"; + version = "7.2.0"; + + src = fetchurl { + urls = [ + "http://tptp.cs.miami.edu/TPTP/Distribution/TPTP-v${version}.tgz" + "http://tptp.cs.miami.edu/TPTP/Archive/TPTP-v${version}.tgz" + ]; + sha256 = "0yq8452b6mym4yscy46pshg0z2my8xi74b5bp2qlxd5bjwcrg6rl"; + }; + + nativeBuildInputs = [ patchelf ]; + buildInputs = [ tcsh yap perl ]; + + installPhase = '' + sharedir=$out/share/tptp + + mkdir -p $sharedir + cp -r ./ $sharedir + + export TPTP=$sharedir + + tcsh $sharedir/Scripts/tptp2T_install -default + + substituteInPlace $sharedir/TPTP2X/tptp2X_install --replace /bin/mv mv + tcsh $sharedir/TPTP2X/tptp2X_install -default + + patchelf --interpreter $(cat $NIX_CC/nix-support/dynamic-linker) $sharedir/Scripts/tptp4X + + mkdir -p $out/bin + ln -s $sharedir/TPTP2X/tptp2X $out/bin + ln -s $sharedir/Scripts/tptp2T $out/bin + ln -s $sharedir/Scripts/tptp4X $out/bin + ''; + + meta = with stdenv.lib; { + description = "Thousands of problems for theorem provers and tools"; + maintainers = with maintainers; [ raskin gebner ]; + # 6.3 GiB of data. Installation is unpacking and editing a few files. + # No sense in letting Hydra build it. + # Also, it is unclear what is covered by "verbatim" - we will edit configs + hydraPlatforms = []; + platforms = platforms.all; + license = licenses.unfreeRedistributable; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/twelf/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/twelf/default.nix new file mode 100644 index 000000000000..975b989bd94c --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/twelf/default.nix @@ -0,0 +1,51 @@ +{ stdenv, fetchurl, pkgconfig, smlnj, rsync }: + +stdenv.mkDerivation rec { + pname = "twelf"; + version = "1.7.1"; + + src = fetchurl { + url = "http://twelf.plparty.org/releases/twelf-src-${version}.tar.gz"; + sha256 = "0fi1kbs9hrdrm1x4k13angpjasxlyd1gc3ys8ah54i75qbcd9c4i"; + }; + + nativeBuildInputs = [ pkgconfig ]; + buildInputs = [ smlnj rsync ]; + + buildPhase = '' + export SMLNJ_HOME=${smlnj} + make smlnj + ''; + + installPhase = '' + mkdir -p $out/bin + rsync -av bin/{*,.heap} $out/bin/ + bin/.mkexec ${smlnj}/bin/sml $out/ twelf-server twelf-server + + substituteInPlace emacs/twelf-init.el \ + --replace '(concat twelf-root "emacs")' '(concat twelf-root "share/emacs/site-lisp/twelf")' + + mkdir -p $out/share/emacs/site-lisp/twelf/ + rsync -av emacs/ $out/share/emacs/site-lisp/twelf/ + + mkdir -p $out/share/twelf/examples + rsync -av examples/ $out/share/twelf/examples/ + mkdir -p $out/share/twelf/vim + rsync -av vim/ $out/share/twelf/vim/ + ''; + + meta = { + description = "Logic proof assistant"; + longDescription = '' + Twelf is a language used to specify, implement, and prove properties of + deductive systems such as programming languages and logics. Large + research projects using Twelf include the TALT typed assembly language, + a foundational proof-carrying-code system, and a type safety proof for + Standard ML. + ''; + homepage = "http://twelf.org/wiki/Main_Page"; + license = stdenv.lib.licenses.mit; + maintainers = with stdenv.lib.maintainers; [ jwiegley ]; + platforms = stdenv.lib.platforms.unix; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/vampire/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/vampire/default.nix new file mode 100644 index 000000000000..dca03823e9ea --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/vampire/default.nix @@ -0,0 +1,56 @@ +{ stdenv, fetchFromGitHub, fetchpatch, z3, zlib }: + +stdenv.mkDerivation rec { + pname = "vampire"; + version = "4.5.1"; + + src = fetchFromGitHub { + owner = "vprover"; + repo = "vampire"; + rev = version; + sha256 = "0q9gqyq96amdnhxgwjyv0r2sxakikp3jvmizgj2h0spfz643p8db"; + }; + + 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/infra/libkookie/nixpkgs/pkgs/applications/science/logic/verifast/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/verifast/default.nix new file mode 100644 index 000000000000..49618d2586b1 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/verifast/default.nix @@ -0,0 +1,50 @@ +{ stdenv, fetchurl, gtk2, gdk-pixbuf, atk, pango, glib, cairo, freetype +, fontconfig, libxml2, gnome2 }: + +let + + libPath = stdenv.lib.makeLibraryPath + [ stdenv.cc.libc stdenv.cc.cc gtk2 gdk-pixbuf atk pango glib cairo + freetype fontconfig libxml2 gnome2.gtksourceview + ] + ":${stdenv.cc.cc.lib}/lib64:$out/libexec"; + + patchExe = x: '' + patchelf --interpreter "$(cat $NIX_CC/nix-support/dynamic-linker)" \ + --set-rpath ${libPath} ${x} + ''; + + patchLib = x: '' + patchelf --set-rpath ${libPath} ${x} + ''; + +in +stdenv.mkDerivation rec { + pname = "verifast"; + version = "19.12"; + + src = fetchurl { + url = "https://github.com/verifast/verifast/releases/download/${version}/${pname}-${version}-linux.tar.gz"; + sha256 = "169kshjq4cf4i9v92azv0xaflrnik5686w7fwcgdhd6qkbzflzl6"; + }; + + 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.mit; + platforms = [ "x86_64-linux" ]; + maintainers = [ stdenv.lib.maintainers.thoughtpolice ]; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/verit/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/verit/default.nix new file mode 100644 index 000000000000..f20a83241571 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/verit/default.nix @@ -0,0 +1,31 @@ +{ stdenv, fetchurl, autoreconfHook, gmp, flex, bison }: + +stdenv.mkDerivation { + pname = "veriT"; + version = "2016"; + + src = fetchurl { + url = "http://www.verit-solver.org/distrib/veriT-stable2016.tar.gz"; + sha256 = "0gvp4diz0qjg0y5ry0p1z7dkdkxw8l7jb8cdhvcnhl06jx977v4b"; + }; + + nativeBuildInputs = [ autoreconfHook flex bison ]; + buildInputs = [ gmp ]; + + # --disable-static actually enables static linking here... + dontDisableStatic = true; + + makeFlags = [ "LEX=${flex}/bin/flex" ]; + + preInstall = '' + mkdir -p $out/bin + ''; + + meta = with stdenv.lib; { + description = "An open, trustable and efficient SMT-solver"; + homepage = "http://www.verit-solver.org/"; + license = licenses.bsd3; + platforms = platforms.unix; + maintainers = [ maintainers.gebner ]; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/why3/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/why3/default.nix new file mode 100644 index 000000000000..eacff32bdf62 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/why3/default.nix @@ -0,0 +1,49 @@ +{ callPackage, fetchurl, fetchpatch, stdenv +, ocamlPackages, coqPackages, rubber, hevea, emacs }: + +stdenv.mkDerivation { + pname = "why3"; + version = "1.3.3"; + + src = fetchurl { + url = "https://gforge.inria.fr/frs/download.php/file/38367/why3-1.3.3.tar.gz"; + sha256 = "1n0a2nn1gnk0zg339lh698g4wpk7m8m1vyi2yvifd5adqvk4milw"; + }; + + buildInputs = with ocamlPackages; [ + ocaml findlib ocamlgraph zarith menhir + # Compressed Sessions + # Emacs compilation of why3.el + emacs + # Documentation + rubber hevea + # GUI + lablgtk + # WebIDE + js_of_ocaml js_of_ocaml-ppx + # Coq Support + coqPackages.coq coqPackages.flocq ocamlPackages.camlp5 + ]; + + propagatedBuildInputs = with ocamlPackages; [ camlzip num ]; + + enableParallelBuilding = true; + + postPatch = '' + substituteInPlace Makefile.in --replace js_of_ocaml.ppx js_of_ocaml-ppx + ''; + + configureFlags = [ "--enable-verbose-make" ]; + + installTargets = [ "install" "install-lib" ]; + + passthru.withProvers = callPackage ./with-provers.nix {}; + + meta = with stdenv.lib; { + description = "A platform for deductive program verification"; + homepage = "http://why3.lri.fr/"; + license = licenses.lgpl21; + platforms = platforms.unix; + maintainers = with maintainers; [ thoughtpolice vbgl ]; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/why3/with-provers.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/why3/with-provers.nix new file mode 100644 index 000000000000..3528dbd3a647 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/why3/with-provers.nix @@ -0,0 +1,30 @@ +{ stdenv, makeWrapper, runCommand, symlinkJoin, why3 }: +provers: +let configAwkScript = runCommand "why3-conf.awk" { inherit provers; } + '' + for p in $provers; do + for b in $p/bin/*; do + BASENAME=$(basename $b) + echo "/^command =/{ gsub(\"$BASENAME\", \"$b\") }" >> $out + done + done + echo '{ print }' >> $out + ''; +in stdenv.mkDerivation { + name = "${why3.name}-with-provers"; + + phases = [ "buildPhase" "installPhase" ]; + + buildInputs = [ why3 makeWrapper ] ++ provers; + + buildPhase = '' + mkdir -p $out/share/why3/ + why3 config --detect-provers -C $out/share/why3/why3.conf + awk -i inplace -f ${configAwkScript} $out/share/why3/why3.conf + ''; + + installPhase = '' + mkdir -p $out/bin + makeWrapper ${why3}/bin/why3 $out/bin/why3 --add-flags "--extra-config $out/share/why3/why3.conf" + ''; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/workcraft/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/workcraft/default.nix new file mode 100644 index 000000000000..9ce6592d9989 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/workcraft/default.nix @@ -0,0 +1,33 @@ +{ stdenv, fetchurl, jre, makeWrapper }: + +stdenv.mkDerivation rec { + pname = "workcraft"; + version = "3.3.2"; + + src = fetchurl { + url = "https://github.com/workcraft/workcraft/releases/download/v${version}/workcraft-v${version}-linux.tar.gz"; + sha256 = "0v71x3fph2j3xrnysvkm7zsgnbxisfbdfgxzvzxxfdg59a6l3xid"; + }; + + 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/infra/libkookie/nixpkgs/pkgs/applications/science/logic/yices/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/yices/default.nix new file mode 100644 index 000000000000..b8dd528a11c1 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/yices/default.nix @@ -0,0 +1,44 @@ +{ stdenv, fetchFromGitHub, gmp-static, gperf, autoreconfHook, libpoly }: + +stdenv.mkDerivation rec { + pname = "yices"; + version = "2.6.1"; + + src = fetchFromGitHub { + owner = "SRI-CSL"; + repo = "yices2"; + rev = "Yices-${version}"; + sha256 = "04vf468spsh00jh7gj94cjnq8kjyfwy9l6r4z7l2pm0zgwkqgyhm"; + }; + + nativeBuildInputs = [ autoreconfHook ]; + buildInputs = [ gmp-static gperf libpoly ]; + configureFlags = + [ "--with-static-gmp=${gmp-static.out}/lib/libgmp.a" + "--with-static-gmp-include-dir=${gmp-static.dev}/include" + "--enable-mcsat" + ]; + + enableParallelBuilding = true; + doCheck = true; + + # Usual shenanigans + patchPhase = ''patchShebangs tests/regress/check.sh''; + + # Includes a fix for the embedded soname being libyices.so.2.5, but + # only installing the libyices.so.2.5.x file. + installPhase = let + ver_XdotY = stdenv.lib.versions.majorMinor version; + in '' + make install LDCONFIG=true + ln -sfr $out/lib/libyices.so.{${version},${ver_XdotY}} + ''; + + meta = with stdenv.lib; { + description = "A high-performance theorem prover and SMT solver"; + homepage = "http://yices.csl.sri.com"; + license = licenses.gpl3; + platforms = with platforms; linux ++ darwin; + maintainers = with maintainers; [ thoughtpolice ]; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/z3/4.4.0.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/z3/4.4.0.nix new file mode 100644 index 000000000000..a5388572db61 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/z3/4.4.0.nix @@ -0,0 +1,41 @@ +{ stdenv, fetchFromGitHub, python }: + +stdenv.mkDerivation rec { + name = "z3-${version}"; + version = "4.4.0"; + + src = fetchFromGitHub { + owner = "Z3Prover"; + repo = "z3"; + rev = "7f6ef0b6c0813f2e9e8f993d45722c0e5b99e152"; + sha256 = "1xllvq9fcj4cz34biq2a9dn2sj33bdgrzyzkj26hqw70wkzv1kzx"; + }; + + buildInputs = [ python ]; + enableParallelBuilding = true; + + configurePhase = "python scripts/mk_make.py --prefix=$out && cd build"; + + # z3's install phase is stupid because it tries to calculate the + # python package store location itself, meaning it'll attempt to + # write files into the nix store, and fail. + soext = if stdenv.system == "x86_64-darwin" then ".dylib" else ".so"; + installPhase = '' + mkdir -p $out/bin $out/lib/${python.libPrefix}/site-packages $out/include + cp ../src/api/z3*.h $out/include + cp ../src/api/c++/z3*.h $out/include + cp z3 $out/bin + cp libz3${soext} $out/lib + cp libz3${soext} $out/lib/${python.libPrefix}/site-packages + cp z3*.pyc $out/lib/${python.libPrefix}/site-packages + cp ../src/api/python/*.py $out/lib/${python.libPrefix}/site-packages + ''; + + meta = { + description = "A high-performance theorem prover and SMT solver"; + homepage = "https://github.com/Z3Prover/z3"; + license = stdenv.lib.licenses.mit; + platforms = stdenv.lib.platforms.x86_64; + maintainers = with stdenv.lib.maintainers; [ thoughtpolice ttuegel ]; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/z3/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/z3/default.nix new file mode 100644 index 000000000000..48512eff5300 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/z3/default.nix @@ -0,0 +1,66 @@ +{ stdenv, fetchFromGitHub, python, fixDarwinDylibNames +, javaBindings ? false +, ocamlBindings ? false +, pythonBindings ? true +, jdk ? null +, ocaml ? null, findlib ? null, zarith ? null +}: + +assert javaBindings -> jdk != null; +assert ocamlBindings -> ocaml != null && findlib != null && zarith != null; + +with stdenv.lib; + +stdenv.mkDerivation rec { + pname = "z3"; + version = "4.8.9"; + + src = fetchFromGitHub { + owner = "Z3Prover"; + repo = pname; + rev = "z3-${version}"; + sha256 = "1hnbzq10d23drd7ksm3c1n2611c3kd0q0yxgz8y78zaafwczvwxx"; + }; + + nativeBuildInputs = optional stdenv.hostPlatform.isDarwin fixDarwinDylibNames; + buildInputs = [ python ] + ++ optional javaBindings jdk + ++ optionals ocamlBindings [ ocaml findlib zarith ] + ; + propagatedBuildInputs = [ python.pkgs.setuptools ]; + enableParallelBuilding = true; + + postPatch = optionalString ocamlBindings '' + export OCAMLFIND_DESTDIR=$ocaml/lib/ocaml/${ocaml.version}/site-lib + mkdir -p $OCAMLFIND_DESTDIR/stublibs + ''; + + configurePhase = concatStringsSep " " ( + [ "${python.interpreter} scripts/mk_make.py --prefix=$out" ] + ++ optional javaBindings "--java" + ++ optional ocamlBindings "--ml" + ++ optional pythonBindings "--python --pypkgdir=$out/${python.sitePackages}" + ) + "\n" + "cd build"; + + postInstall = '' + mkdir -p $dev $lib + mv $out/lib $lib/lib + mv $out/include $dev/include + '' + optionalString pythonBindings '' + mkdir -p $python/lib + mv $lib/lib/python* $python/lib/ + ln -sf $lib/lib/libz3${stdenv.hostPlatform.extensions.sharedLibrary} $python/${python.sitePackages}/z3/lib/libz3${stdenv.hostPlatform.extensions.sharedLibrary} + ''; + + outputs = [ "out" "lib" "dev" "python" ] + ++ optional ocamlBindings "ocaml" + ; + + meta = { + description = "A high-performance theorem prover and SMT solver"; + homepage = "https://github.com/Z3Prover/z3"; + license = stdenv.lib.licenses.mit; + platforms = stdenv.lib.platforms.unix; + maintainers = with stdenv.lib.maintainers; [ thoughtpolice ttuegel ]; + }; +} diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/z3/tptp.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/z3/tptp.nix new file mode 100644 index 000000000000..34449542abb2 --- /dev/null +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/z3/tptp.nix @@ -0,0 +1,31 @@ +{stdenv, z3, cmake}: +stdenv.mkDerivation rec { + pname = "z3-tptp"; + version = z3.version; + + src = z3.src; + + sourceRoot = "source/examples/tptp"; + + nativeBuildInputs = [cmake]; + buildInputs = [z3]; + + preConfigure = '' + echo 'set(Z3_LIBRARIES "-lz3")' >> CMakeLists.new + cat CMakeLists.txt | grep -E 'add_executable|project|link_libraries' >> CMakeLists.new + mv CMakeLists.new CMakeLists.txt + ''; + + installPhase = '' + mkdir -p "$out/bin" + cp "z3_tptp5" "$out/bin/" + ln -s "z3_tptp5" "$out/bin/z3-tptp" + ''; + + meta = { + inherit version; + inherit (z3.meta) license homepage platforms; + description = ''TPTP wrapper for Z3 prover''; + maintainers = [stdenv.lib.maintainers.raskin]; + }; +} |