From 64ed7e705d418aa34d8a14bf1e82f6627d9354a2 Mon Sep 17 00:00:00 2001
From: Michael Raskin <7c6f434c@mail.ru>
Date: Fri, 3 Dec 2010 11:26:34 +0000
Subject: [PATCH] Adding Satallax prover

svn path=/nixpkgs/trunk/; revision=24963
---
 .../science/logic/satallax/default.nix        | 72 +++++++++++++++++++
 .../builder-defs/template-auto-callable.nix   |  6 ++
 pkgs/top-level/all-packages.nix               |  2 +
 3 files changed, 80 insertions(+)
 create mode 100644 pkgs/applications/science/logic/satallax/default.nix

diff --git a/pkgs/applications/science/logic/satallax/default.nix b/pkgs/applications/science/logic/satallax/default.nix
new file mode 100644
index 00000000000..4bf6e53737e
--- /dev/null
+++ b/pkgs/applications/science/logic/satallax/default.nix
@@ -0,0 +1,72 @@
+x@{builderDefsPackage
+  , sbcl, zlib
+  , ...}:
+builderDefsPackage
+(a :  
+let 
+  helperArgNames = ["stdenv" "fetchurl" "builderDefsPackage"] ++ 
+    [];
+
+  buildInputs = map (n: builtins.getAttr n x)
+    (builtins.attrNames (builtins.removeAttrs x helperArgNames));
+  sourceInfo = rec {
+    baseName="satallax";
+    version="1.4";
+    name="${baseName}-${version}";
+    url="http://www.ps.uni-saarland.de/~cebrown/satallax/downloads/${name}.tar.gz";
+    hash="0l8dq4nyfw2bdsyqmgb4v6fjw3739p8nqv4bh2gh2924ibzrq5fc";
+  };
+in
+rec {
+  src = a.fetchurl {
+    url = sourceInfo.url;
+    sha256 = sourceInfo.hash;
+  };
+
+  inherit (sourceInfo) name version;
+  inherit buildInputs;
+
+  phaseNames = ["doDeployMinisat" "doDeploy"];
+
+  doDeployMinisat = a.fullDepEntry (''
+    (
+      cd minisat/simp
+      make
+    )
+
+    ensureDir "$out/bin"
+    cp minisat/simp/minisat "$out/bin"
+
+    echo "(setq *minisat-binary* \"$out/bin/minisat\")" > config.lisp
+
+  '') ["defEnsureDir" "minInit" "addInputs" "doUnpack"];
+  doDeploy = a.fullDepEntry (''
+    ensureDir "$out/share/satallax/build-dir"
+    cp -r * "$out/share/satallax/build-dir"
+    cd  "$out/share/satallax/build-dir"
+
+    sbcl --load make.lisp
+    ! ( ./test | grep ERROR )
+    
+    ensureDir "$out/bin"
+    cp bin/satallax "$out/bin"
+  '') ["defEnsureDir" "minInit" "addInputs" "doUnpack"];
+      
+  meta = {
+    description = "A higher-order logic prover";
+    maintainers = with a.lib.maintainers;
+    [
+      raskin
+    ];
+    platforms = with a.lib.platforms;
+      unix;
+    license = "free-noncopyleft";
+    homepage = "http://www.ps.uni-saarland.de/~cebrown/satallax/";
+  };
+  passthru = {
+    updateInfo = {
+      downloadPage = "http://www.ps.uni-saarland.de/~cebrown/satallax/";
+    };
+  };
+}) x
+
diff --git a/pkgs/build-support/builder-defs/template-auto-callable.nix b/pkgs/build-support/builder-defs/template-auto-callable.nix
index 769b9c1af76..1ff7ed0a96c 100644
--- a/pkgs/build-support/builder-defs/template-auto-callable.nix
+++ b/pkgs/build-support/builder-defs/template-auto-callable.nix
@@ -10,6 +10,11 @@ let
   buildInputs = map (n: builtins.getAttr n x)
     (builtins.attrNames (builtins.removeAttrs x helperArgNames));
   sourceInfo = rec {
+    baseName="${abort ''Specify package name''}";
+    version="";
+    name="${baseName}-${version}";
+    url="${name}";
+    hash="";
   };
 in
 rec {
@@ -32,6 +37,7 @@ rec {
     ];
     platforms = with a.lib.platforms;
       (abort "Specify platforms");
+    license = "${abort ''Specify license''}";
   };
   passthru = {
     updateInfo = {
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 1657cb1ae48..7fa7c5a6e82 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -6983,6 +6983,8 @@ let
 
   prover9 = callPackage ../applications/science/logic/prover9 { };
 
+  satallax = callPackage ../applications/science/logic/satallax {};
+
   ssreflect = callPackage ../applications/science/logic/ssreflect {
     camlp5 = camlp5_transitional;
   };