aboutsummaryrefslogtreecommitdiff
path: root/infra/libkookie/nixpkgs/pkgs/applications/science/logic
diff options
context:
space:
mode:
Diffstat (limited to 'infra/libkookie/nixpkgs/pkgs/applications/science/logic')
-rw-r--r--infra/libkookie/nixpkgs/pkgs/applications/science/logic/abc/default.nix8
-rw-r--r--infra/libkookie/nixpkgs/pkgs/applications/science/logic/boolector/default.nix54
-rw-r--r--infra/libkookie/nixpkgs/pkgs/applications/science/logic/btor2tools/default.nix6
-rw-r--r--infra/libkookie/nixpkgs/pkgs/applications/science/logic/coq/default.nix1
-rw-r--r--infra/libkookie/nixpkgs/pkgs/applications/science/logic/coq2html/default.nix4
-rw-r--r--infra/libkookie/nixpkgs/pkgs/applications/science/logic/cryptoverif/default.nix4
-rw-r--r--infra/libkookie/nixpkgs/pkgs/applications/science/logic/key/default.nix74
-rw-r--r--infra/libkookie/nixpkgs/pkgs/applications/science/logic/lean/default.nix14
-rw-r--r--infra/libkookie/nixpkgs/pkgs/applications/science/logic/ott/default.nix2
-rw-r--r--infra/libkookie/nixpkgs/pkgs/applications/science/logic/potassco/clingcon.nix2
-rw-r--r--infra/libkookie/nixpkgs/pkgs/applications/science/logic/proverif/default.nix1
-rw-r--r--infra/libkookie/nixpkgs/pkgs/applications/science/logic/tlaplus/toolbox.nix4
-rw-r--r--infra/libkookie/nixpkgs/pkgs/applications/science/logic/workcraft/default.nix4
-rw-r--r--infra/libkookie/nixpkgs/pkgs/applications/science/logic/z3/4.4.0.nix2
-rw-r--r--infra/libkookie/nixpkgs/pkgs/applications/science/logic/z3/default.nix5
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 ];
};
}