summary refs log tree commit diff
path: root/pkgs/applications/science/logic
diff options
context:
space:
mode:
Diffstat (limited to 'pkgs/applications/science/logic')
-rw-r--r--pkgs/applications/science/logic/clprover/clprover.nix27
-rw-r--r--pkgs/applications/science/logic/hol_light/default.nix4
-rw-r--r--pkgs/applications/science/logic/leo3/binary.nix4
-rw-r--r--pkgs/applications/science/logic/why3/default.nix6
4 files changed, 34 insertions, 7 deletions
diff --git a/pkgs/applications/science/logic/clprover/clprover.nix b/pkgs/applications/science/logic/clprover/clprover.nix
new file mode 100644
index 00000000000..b6ebce68193
--- /dev/null
+++ b/pkgs/applications/science/logic/clprover/clprover.nix
@@ -0,0 +1,27 @@
+{ stdenv, pkgs, fetchzip }:
+
+stdenv.mkDerivation rec {
+  name = "clprover-${version}";
+  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/pkgs/applications/science/logic/hol_light/default.nix b/pkgs/applications/science/logic/hol_light/default.nix
index ffd25b6238b..099e2102c51 100644
--- a/pkgs/applications/science/logic/hol_light/default.nix
+++ b/pkgs/applications/science/logic/hol_light/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchFromGitHub, ocaml, num, camlp5 }:
+{ stdenv, runtimeShell, fetchFromGitHub, ocaml, num, camlp5 }:
 
 let
   load_num =
@@ -11,7 +11,7 @@ let
 
   start_script =
     ''
-      #!${stdenv.shell}
+      #!${runtimeShell}
       cd $out/lib/hol_light
       exec ${ocaml}/bin/ocaml \
         -I \`${camlp5}/bin/camlp5 -where\` \
diff --git a/pkgs/applications/science/logic/leo3/binary.nix b/pkgs/applications/science/logic/leo3/binary.nix
index a3834dc70b6..dcea9c27acb 100644
--- a/pkgs/applications/science/logic/leo3/binary.nix
+++ b/pkgs/applications/science/logic/leo3/binary.nix
@@ -1,4 +1,4 @@
-{stdenv, fetchurl, openjdk}:
+{stdenv, fetchurl, openjdk, runtimeShell}:
 stdenv.mkDerivation rec {
   pname = "leo3";
   version = "1.2";
@@ -13,7 +13,7 @@ stdenv.mkDerivation rec {
   installPhase = ''
     mkdir -p "$out"/{bin,lib/java/leo3}
     cp "${jar}" "$out/lib/java/leo3/leo3.jar"
-    echo "#!${stdenv.shell}" > "$out/bin/leo3"
+    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"
   '';
diff --git a/pkgs/applications/science/logic/why3/default.nix b/pkgs/applications/science/logic/why3/default.nix
index c22c15b3a4b..a3b369ad54a 100644
--- a/pkgs/applications/science/logic/why3/default.nix
+++ b/pkgs/applications/science/logic/why3/default.nix
@@ -2,11 +2,11 @@
 
 stdenv.mkDerivation rec {
   name    = "why3-${version}";
-  version = "1.1.1";
+  version = "1.2.0";
 
   src = fetchurl {
-    url = https://gforge.inria.fr/frs/download.php/file/37842/why3-1.1.1.tar.gz;
-    sha256 = "065ix1ill009bxg7w27s8wq47vn03vbr63hsaa79arv31d96izny";
+    url = https://gforge.inria.fr/frs/download.php/file/37903/why3-1.2.0.tar.gz;
+    sha256 = "0xz001jhi71ja8vqrjz27v63bidrzj4qvg1yqarq6p4dmpxhk348";
   };
 
   buildInputs = (with ocamlPackages; [