From 5401849e3a0e175d3cf1a6fcf52bc1ffa8f5e299 Mon Sep 17 00:00:00 2001 From: Austin Seipp Date: Thu, 24 Apr 2014 23:15:50 -0500 Subject: [PATCH] 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 --- .../development/compilers/cryptol/default.nix | 31 +++++++++++++ .../compilers/cryptol/fix-gitrev.patch | 44 +++++++++++++++++++ .../libraries/haskell/graphscc/default.nix | 13 ++++++ .../libraries/haskell/monadlib/default.nix | 14 ++++++ .../libraries/haskell/presburger/default.nix | 14 ++++++ .../libraries/haskell/process/default.nix | 14 ++++++ .../libraries/haskell/smtLib/default.nix | 13 ++++++ pkgs/top-level/haskell-packages.nix | 17 +++++++ 8 files changed, 160 insertions(+) create mode 100644 pkgs/development/compilers/cryptol/default.nix create mode 100644 pkgs/development/compilers/cryptol/fix-gitrev.patch create mode 100644 pkgs/development/libraries/haskell/graphscc/default.nix create mode 100644 pkgs/development/libraries/haskell/monadlib/default.nix create mode 100644 pkgs/development/libraries/haskell/presburger/default.nix create mode 100644 pkgs/development/libraries/haskell/process/default.nix create mode 100644 pkgs/development/libraries/haskell/smtLib/default.nix diff --git a/pkgs/development/compilers/cryptol/default.nix b/pkgs/development/compilers/cryptol/default.nix new file mode 100644 index 000000000000..753dfb4f318a --- /dev/null +++ b/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 ]; + }; +}) diff --git a/pkgs/development/compilers/cryptol/fix-gitrev.patch b/pkgs/development/compilers/cryptol/fix-gitrev.patch new file mode 100644 index 000000000000..ab9a789baf2b --- /dev/null +++ b/pkgs/development/compilers/cryptol/fix-gitrev.patch @@ -0,0 +1,44 @@ +From 3ceec293f8e68314d872909b7de1d4a2c3ecba49 Mon Sep 17 00:00:00 2001 +From: Austin Seipp +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 +--- + 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 + diff --git a/pkgs/development/libraries/haskell/graphscc/default.nix b/pkgs/development/libraries/haskell/graphscc/default.nix new file mode 100644 index 000000000000..3f04e668a8f5 --- /dev/null +++ b/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 ]; + }; +}) diff --git a/pkgs/development/libraries/haskell/monadlib/default.nix b/pkgs/development/libraries/haskell/monadlib/default.nix new file mode 100644 index 000000000000..361e177aa01c --- /dev/null +++ b/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 ]; + }; +}) diff --git a/pkgs/development/libraries/haskell/presburger/default.nix b/pkgs/development/libraries/haskell/presburger/default.nix new file mode 100644 index 000000000000..f266cf6cdab0 --- /dev/null +++ b/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 ]; + }; +}) diff --git a/pkgs/development/libraries/haskell/process/default.nix b/pkgs/development/libraries/haskell/process/default.nix new file mode 100644 index 000000000000..f3ae03da7c41 --- /dev/null +++ b/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 ]; + }; +}) diff --git a/pkgs/development/libraries/haskell/smtLib/default.nix b/pkgs/development/libraries/haskell/smtLib/default.nix new file mode 100644 index 000000000000..e1363d9063ac --- /dev/null +++ b/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 ]; + }; +}) diff --git a/pkgs/top-level/haskell-packages.nix b/pkgs/top-level/haskell-packages.nix index 3e4d410a154a..05a459fb1613 100644 --- a/pkgs/top-level/haskell-packages.nix +++ b/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 {