diff options
Diffstat (limited to 'infra/libkookie/nixpkgs/pkgs/applications/science/logic')
15 files changed, 137 insertions, 48 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 index 29d727d988e7..426c5a9df323 100644 --- a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/abc/default.nix +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/abc/default.nix @@ -4,13 +4,13 @@ stdenv.mkDerivation rec { pname = "abc-verifier"; - version = "2020.06.22"; + version = "2020.11.24"; src = fetchFromGitHub { - owner = "berkeley-abc"; + owner = "yosyshq"; repo = "abc"; - rev = "341db25668f3054c87aa3372c794e180f629af5d"; - sha256 = "14cgv34vz5ljkcms6nrv19vqws2hs8bgjgffk5q03cbxnm2jxv5s"; + rev = "4f5f73d18b137930fb3048c0b385c82fa078db38"; + sha256 = "0z1kp223kix7i4r7mbj2bzawkdzc55nsgc41m85dmbajl9fsj1m0"; }; nativeBuildInputs = [ cmake ]; diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/boolector/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/boolector/default.nix index aedc8e3484a9..0364a76639aa 100644 --- a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/boolector/default.nix +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/boolector/default.nix @@ -1,4 +1,4 @@ -{ stdenv, fetchFromGitHub, lib, python3 +{ stdenv, fetchFromGitHub, fetchpatch, lib, python3 , cmake, lingeling, btor2tools, gtest, gmp }: @@ -13,6 +13,14 @@ stdenv.mkDerivation rec { 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 ''; @@ -23,39 +31,39 @@ stdenv.mkDerivation rec { cmakeFlags = [ "-DBUILD_SHARED_LIBS=ON" "-DUSE_LINGELING=YES" - "-DBtor2Tools_INCLUDE_DIR=${btor2tools.dev}/include" - "-DBtor2Tools_LIBRARIES=${btor2tools.lib}/lib/libbtor2parser.so" ] ++ (lib.optional (gmp != null) "-DUSE_GMP=YES"); - installPhase = '' - mkdir -p $out/bin $lib/lib $dev/include - - cp -vr bin/* $out/bin - cp -vr lib/* $lib/lib - - rm -rf $out/bin/{examples,tests} - # we don't care about gtest related libs - rm -rf $lib/lib/libg* - - cd ../src - find . -iname '*.h' -exec cp --parents '{}' $dev/include \; - rm -rf $dev/include/tests - ''; - checkInputs = [ python3 ]; doCheck = true; - preCheck = '' - export LD_LIBRARY_PATH=$(readlink -f lib) - patchShebangs .. + 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 ''; - outputs = [ "out" "dev" "lib" ]; + # 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 = platforms.linux; + 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 index 714ab49524b0..7d2aed7596e8 100644 --- a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/btor2tools/default.nix +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/btor2tools/default.nix @@ -1,4 +1,4 @@ -{ stdenv, cmake, fetchFromGitHub }: +{ stdenv, cmake, fetchFromGitHub, fixDarwinDylibNames }: stdenv.mkDerivation rec { pname = "btor2tools"; @@ -11,7 +11,7 @@ stdenv.mkDerivation rec { sha256 = "0mfqmkgvyw8fa2c09kww107dmk180ch1hp98r5kv41vnc04iqb0s"; }; - nativeBuildInputs = [ cmake ]; + nativeBuildInputs = [ cmake ] ++ stdenv.lib.optional stdenv.isDarwin fixDarwinDylibNames; installPhase = '' mkdir -p $out $dev/include/btor2parser/ $lib/lib @@ -27,7 +27,7 @@ stdenv.mkDerivation rec { description = "A generic parser and tool package for the BTOR2 format"; homepage = "https://github.com/Boolector/btor2tools"; license = licenses.mit; - platforms = platforms.linux; + platforms = platforms.unix; maintainers = with maintainers; [ thoughtpolice ]; }; } diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/coq/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/coq/default.nix index 946cba41b143..dc9e40912d53 100644 --- a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/coq/default.nix +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/coq/default.nix @@ -35,6 +35,7 @@ let "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; diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/coq2html/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/coq2html/default.nix index 2e56eda893e9..e53e8e7392c0 100644 --- a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/coq2html/default.nix +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/coq2html/default.nix @@ -1,6 +1,6 @@ { stdenv, fetchgit, ocaml }: -let +let version = "20170720"; in @@ -22,7 +22,7 @@ stdenv.mkDerivation { ''; meta = with stdenv.lib; { - description = "coq2html is an HTML documentation generator for Coq source files"; + 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 diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/cryptoverif/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/cryptoverif/default.nix index 6877060d36d6..28295ea28922 100644 --- a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/cryptoverif/default.nix +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/cryptoverif/default.nix @@ -2,11 +2,11 @@ stdenv.mkDerivation rec { pname = "cryptoverif"; - version = "2.01pl1"; + version = "2.03pl1"; src = fetchurl { url = "http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/cryptoverif${version}.tar.gz"; - sha256 = "1bkmrv3wsy8mwhrxd3z3br9zgv37c2w6443rm4s9jl0aphcgnbiw"; + sha256 = "0q7qa1qm7mbky3m36445gdmgmkb9mrhrdsk7mmwn8fzw0rfc6z00"; }; buildInputs = [ ocaml ]; 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/lean/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/lean/default.nix index 32a75cabc13f..88e1b4fbc0e1 100644 --- a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/lean/default.nix +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/lean/default.nix @@ -2,22 +2,26 @@ stdenv.mkDerivation rec { pname = "lean"; - version = "3.19.0"; + version = "3.23.0"; src = fetchFromGitHub { owner = "leanprover-community"; repo = "lean"; rev = "v${version}"; - sha256 = "1dybq6104vc62x620izgblfd8dqc4ynaiw8ml07km78lq38anm6v"; + sha256 = "09mklc1p6ms1jayg2f89hqfmhca3h5744lli936l38ypn1d00sxx"; }; nativeBuildInputs = [ cmake ]; buildInputs = [ gmp ]; enableParallelBuilding = true; - preConfigure = '' - cd src - ''; + 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 \ diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/ott/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/ott/default.nix index ecc253a64d98..48ad63eaa993 100644 --- a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/ott/default.nix +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/ott/default.nix @@ -19,7 +19,7 @@ stdenv.mkDerivation rec { postInstall = "opaline -prefix $out"; meta = { - description = "Ott: tool for the working semanticist"; + 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 diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/potassco/clingcon.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/potassco/clingcon.nix index 1203822d86e9..b74583ca1a2c 100644 --- a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/potassco/clingcon.nix +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/potassco/clingcon.nix @@ -11,7 +11,7 @@ stdenv.mkDerivation rec { src = fetchFromGitHub { owner = "potassco"; - repo = "${pname}"; + repo = pname; rev = "v${version}"; fetchSubmodules = true; sha256 = "1q7517h10jfvjdk2czq8d6y57r8kr1j1jj2k2ip2qxkpyfigk4rs"; diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/proverif/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/proverif/default.nix index 6acae2bcb766..4242bb0599e9 100644 --- a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/proverif/default.nix +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/proverif/default.nix @@ -16,6 +16,7 @@ stdenv.mkDerivation rec { mkdir -p $out/bin cp ./proverif $out/bin cp ./proveriftotex $out/bin + install -D -t $out/share/emacs/site-lisp/ emacs/proverif.el ''; meta = { diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/tlaplus/toolbox.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/tlaplus/toolbox.nix index 5c445459a36a..c9e97375b6c7 100644 --- a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/tlaplus/toolbox.nix +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/tlaplus/toolbox.nix @@ -3,7 +3,7 @@ }: let - version = "1.6.0"; + version = "1.7.0"; arch = "x86_64"; desktopItem = makeDesktopItem rec { @@ -25,7 +25,7 @@ in stdenv.mkDerivation { inherit version; src = fetchzip { url = "https://tla.msr-inria.inria.fr/tlatoolbox/products/TLAToolbox-${version}-linux.gtk.${arch}.zip"; - sha256 = "1mgx4p5qykf9q0p4cp6kcpc7fx8g5f2w1g40kdgas24hqwrgs3cm"; + sha256 = "0v15wscawair5bghr5ixb4i062kmh9by1m0hnz2r1sawlqyafz02"; }; buildInputs = [ makeWrapper ]; diff --git a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/workcraft/default.nix b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/workcraft/default.nix index 4038db17f938..9ce6592d9989 100644 --- a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/workcraft/default.nix +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/workcraft/default.nix @@ -2,11 +2,11 @@ stdenv.mkDerivation rec { pname = "workcraft"; - version = "3.3.0"; + version = "3.3.2"; src = fetchurl { url = "https://github.com/workcraft/workcraft/releases/download/v${version}/workcraft-v${version}-linux.tar.gz"; - sha256 = "072i7kan2c9f4s9jxwqr4ccsi9979c12xhwr385sbq06rwyrna85"; + sha256 = "0v71x3fph2j3xrnysvkm7zsgnbxisfbdfgxzvzxxfdg59a6l3xid"; }; buildInputs = [ makeWrapper ]; 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 index 1e3bcea42ef7..a5388572db61 100644 --- 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 @@ -33,7 +33,7 @@ stdenv.mkDerivation rec { meta = { description = "A high-performance theorem prover and SMT solver"; - homepage = "http://github.com/Z3Prover/z3"; + 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 index 88aafcdae222..48512eff5300 100644 --- a/infra/libkookie/nixpkgs/pkgs/applications/science/logic/z3/default.nix +++ b/infra/libkookie/nixpkgs/pkgs/applications/science/logic/z3/default.nix @@ -22,7 +22,8 @@ stdenv.mkDerivation rec { sha256 = "1hnbzq10d23drd7ksm3c1n2611c3kd0q0yxgz8y78zaafwczvwxx"; }; - buildInputs = [ python fixDarwinDylibNames ] + nativeBuildInputs = optional stdenv.hostPlatform.isDarwin fixDarwinDylibNames; + buildInputs = [ python ] ++ optional javaBindings jdk ++ optionals ocamlBindings [ ocaml findlib zarith ] ; @@ -59,7 +60,7 @@ stdenv.mkDerivation rec { 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; + platforms = stdenv.lib.platforms.unix; maintainers = with stdenv.lib.maintainers; [ thoughtpolice ttuegel ]; }; } |