cryptol v2.0.0

This comes with several extra libraries, including GraphSCC, monadLib,
presburger, process and smtLib, all required as build dependencies. But
otherwise totally automated via cabal2nix.

Next up is CVC4 (a total pain in the ass to package) for proving/SAT
support.

I have another WIP branch for the unfree 1.x series which I may (or may
not) add later as it has external verification tech at the moment.

Signed-off-by: Austin Seipp <aseipp@pobox.com>

pkgs/development/compilers/cryptol/default.nix

@@ -0,0 +1,31 @@
+{ cabal, cabalInstall, Cabal, alex, ansiTerminal, deepseq, executablePath
+, filepath, graphSCC, happy, haskeline, monadLib, mtl, presburger, QuickCheck
+, random, smtLib, syb, text, transformers, utf8String, process, fetchgit
+}:
+
+cabal.mkDerivation (self: {
+  pname = "cryptol";
+  version = "2.0.0";
+  src = fetchgit {
+    url    = "https://github.com/GaloisInc/cryptol.git";
+    rev    = "refs/tags/v2.0.0";
+    sha256 = "6af3499d7c6f034446f6665660f7a66dd592e81281e34b0cee3e55bc03597e6b";
+  };
+  isLibrary = true;
+  isExecutable = true;
+
+  patches = [ ./fix-gitrev.patch ];
+  buildDepends = [
+    ansiTerminal deepseq executablePath filepath graphSCC haskeline
+    monadLib mtl presburger QuickCheck random smtLib syb text
+    transformers utf8String process Cabal
+  ];
+  buildTools = [ alex happy cabalInstall ];
+  meta = {
+    description = "Cryptol: The Language of Cryptography";
+    homepage    = "https://cryptol.net";
+    license     = self.stdenv.lib.licenses.bsd3;
+    platforms   = self.ghc.meta.platforms;
+    maintainers = [ self.stdenv.lib.maintainers.thoughtpolice ];
+  };
+})

pkgs/development/compilers/cryptol/fix-gitrev.patch

@@ -0,0 +1,44 @@
+From 3ceec293f8e68314d872909b7de1d4a2c3ecba49 Mon Sep 17 00:00:00 2001
+From: Austin Seipp <aseipp@pobox.com>
+Date: Fri, 25 Apr 2014 00:24:39 -0500
+Subject: [PATCH] Add GitRev.hs to signify v2.0.0 release
+
+Signed-off-by: Austin Seipp <aseipp@pobox.com>
+---
+ cryptol.cabal |  2 +-
+ src/GitRev.hs | 10 ++++++++++
+ 2 files changed, 11 insertions(+), 1 deletion(-)
+ create mode 100644 src/GitRev.hs
+
+diff --git a/cryptol.cabal b/cryptol.cabal
+index 2ba6e56..9acd1ef 100644
+--- a/cryptol.cabal
++++ b/cryptol.cabal
+@@ -6,7 +6,7 @@ Author:              Galois, Inc.
+ Maintainer:          cryptol@galois.com
+ Copyright:           2013-2014 Galois Inc.
+ Category:            Language
+-Build-type:          Configure
++Build-type:          Simple
+ Cabal-version:       >= 1.18
+ 
+ data-files:          lib/Cryptol.cry
+diff --git a/src/GitRev.hs b/src/GitRev.hs
+new file mode 100644
+index 0000000..1c767dc
+--- /dev/null
++++ b/src/GitRev.hs
+@@ -0,0 +1,10 @@
++module GitRev (hash, branch, dirty) where
++
++hash :: String
++hash = "bd578915eaba8c56fadc29fe30f5dcd212c63374"
++
++branch :: String
++branch = "Unknown"
++
++dirty :: Bool
++dirty = False
+-- 
+1.8.3.2
+

pkgs/development/libraries/haskell/graphscc/default.nix

@@ -0,0 +1,13 @@
+{ cabal }:
+
+cabal.mkDerivation (self: {
+  pname = "GraphSCC";
+  version = "1.0.4";
+  sha256 = "1wbcx3wb02adb7l4nchxla3laliz0h5q074vfw4z0ic833k977bq";
+  meta = {
+    description = "Tarjan's algorithm for computing the strongly connected components of a graph";
+    license = self.stdenv.lib.licenses.bsd3;
+    platforms = self.ghc.meta.platforms;
+    maintainers = [ self.stdenv.lib.maintainers.thoughtpolice ];
+  };
+})

pkgs/development/libraries/haskell/monadlib/default.nix

@@ -0,0 +1,14 @@
+{ cabal }:
+
+cabal.mkDerivation (self: {
+  pname = "monadLib";
+  version = "3.7.2";
+  sha256 = "01s7jfwzr4jmwz1k4bkxi38q8v364vg6fnn77n5v8zpbimcv3rds";
+  meta = {
+    homepage = "http://wiki.github.com/yav/monadlib";
+    description = "A collection of monad transformers";
+    license = self.stdenv.lib.licenses.bsd3;
+    platforms = self.ghc.meta.platforms;
+    maintainers = [ self.stdenv.lib.maintainers.thoughtpolice ];
+  };
+})

pkgs/development/libraries/haskell/presburger/default.nix

@@ -0,0 +1,14 @@
+{ cabal }:
+
+cabal.mkDerivation (self: {
+  pname = "presburger";
+  version = "1.1";
+  sha256 = "0pb0rabhhzrrrsr8260lgjpp168pm8ldqwfqbc2i1wy95n7wxk7c";
+  meta = {
+    homepage = "http://github.com/yav/presburger";
+    description = "A decision procedure for quantifier-free linear arithmetic";
+    license = self.stdenv.lib.licenses.bsd3;
+    platforms = self.ghc.meta.platforms;
+    maintainers = [ self.stdenv.lib.maintainers.thoughtpolice ];
+  };
+})

pkgs/development/libraries/haskell/process/default.nix

@@ -0,0 +1,14 @@
+{ cabal, deepseq, filepath }:
+
+cabal.mkDerivation (self: {
+  pname = "process";
+  version = "1.2.0.0";
+  sha256 = "02il5pxibf0q9b46v0lgdxyc2wlk5kg1v8223ry6brg41zpcj71q";
+  buildDepends = [ deepseq filepath ];
+  meta = {
+    description = "Process libraries";
+    license = self.stdenv.lib.licenses.bsd3;
+    platforms = self.ghc.meta.platforms;
+    maintainers = [ self.stdenv.lib.maintainers.thoughtpolice ];
+  };
+})

pkgs/development/libraries/haskell/smtLib/default.nix

@@ -0,0 +1,13 @@
+{ cabal }:
+
+cabal.mkDerivation (self: {
+  pname = "smtLib";
+  version = "1.0.7";
+  sha256 = "1jn2790x7g7n6jm5cfgd692n3l6iafyv0zyz40hx8ykcs4jh2rkf";
+  meta = {
+    description = "A library for working with the SMTLIB format";
+    license = self.stdenv.lib.licenses.bsd3;
+    platforms = self.ghc.meta.platforms;
+    maintainers = [ self.stdenv.lib.maintainers.thoughtpolice ];
+  };
+})

pkgs/top-level/haskell-packages.nix

@@ -1283,6 +1283,8 @@ let result = let callPackage = x : y : modifyPrio (newScope result.finalReturn x
 
   graphviz = callPackage ../development/libraries/haskell/graphviz {};
 
+  graphSCC = callPackage ../development/libraries/haskell/graphscc {};
+
   graphWrapper = callPackage ../development/libraries/haskell/graph-wrapper {};
 
   groups = callPackage ../development/libraries/haskell/groups {};
@@ -1770,6 +1772,8 @@ let result = let callPackage = x : y : modifyPrio (newScope result.finalReturn x
 
   monadExtras = callPackage ../development/libraries/haskell/monad-extras {};
 
+  monadLib = callPackage ../development/libraries/haskell/monadlib {};
+
   monadloc = callPackage ../development/libraries/haskell/monadloc {};
 
   monadLoops = callPackage ../development/libraries/haskell/monad-loops {};
@@ -2061,12 +2065,16 @@ let result = let callPackage = x : y : modifyPrio (newScope result.finalReturn x
 
   pqueue = callPackage ../development/libraries/haskell/pqueue {};
 
+  process = callPackage ../development/libraries/haskell/process {};
+
   preprocessorTools_0_1_3 = callPackage ../development/libraries/haskell/preprocessor-tools/0.1.3.nix {};
 
   preprocessorTools_1_0_1 = callPackage ../development/libraries/haskell/preprocessor-tools/1.0.1.nix {};
 
   preprocessorTools = self.preprocessorTools_1_0_1;
 
+  presburger = callPackage ../development/libraries/haskell/presburger {};
+
   prettyclass = callPackage ../development/libraries/haskell/prettyclass {};
 
   prettyShow_1_2 = callPackage ../development/libraries/haskell/pretty-show/1.2.nix {};
@@ -2275,6 +2283,8 @@ let result = let callPackage = x : y : modifyPrio (newScope result.finalReturn x
 
   smallcheck = callPackage ../development/libraries/haskell/smallcheck {};
 
+  smtLib = callPackage ../development/libraries/haskell/smtLib {};
+
   smtpMail = callPackage ../development/libraries/haskell/smtp-mail {};
 
   smtpsGmail = callPackage ../development/libraries/haskell/smtps-gmail {};
@@ -2973,6 +2983,13 @@ let result = let callPackage = x : y : modifyPrio (newScope result.finalReturn x
 
   arbtt = callPackage ../applications/misc/arbtt {};
 
+  cryptol = callPackage ../development/compilers/cryptol {
+    QuickCheck   = self.QuickCheck_2_7_3;
+    text         = self.text_1_1_0_1;
+    cabalInstall = self.cabalInstall_1_18_0_3;
+    Cabal        = self.Cabal_1_18_1_3;
+  };
+
   darcs = callPackage ../applications/version-management/darcs {};
 
   idris_plain = callPackage ../development/compilers/idris {