From d9d76f1a3a2959b014a5c1db99bf78ae17143311 Mon Sep 17 00:00:00 2001 From: Austin Seipp Date: Tue, 29 Apr 2014 17:50:20 -0500 Subject: [PATCH] cryptol: add 1.8.x expression This also includes support for the verification tools I'm using. Cryptol 2 is still the default obviously. Signed-off-by: Austin Seipp --- pkgs/development/compilers/cryptol/1.8.x.nix | 112 ++++++++++++++++++ .../cryptol/{default.nix => 2.0.x.nix} | 0 pkgs/top-level/all-packages.nix | 1 + pkgs/top-level/haskell-packages.nix | 2 +- 4 files changed, 114 insertions(+), 1 deletion(-) create mode 100644 pkgs/development/compilers/cryptol/1.8.x.nix rename pkgs/development/compilers/cryptol/{default.nix => 2.0.x.nix} (100%) diff --git a/pkgs/development/compilers/cryptol/1.8.x.nix b/pkgs/development/compilers/cryptol/1.8.x.nix new file mode 100644 index 00000000000..a2ca675a55f --- /dev/null +++ b/pkgs/development/compilers/cryptol/1.8.x.nix @@ -0,0 +1,112 @@ +{ stdenv, requireFile, gmp4, ncurses, zlib, makeWrapper }: + +let + name = "cryptol-${version}-${rev}"; + version = "1.8.27"; + rev = "1"; + lss-ver = "lss-0.2d"; + jss-ver = "jss-0.4"; + + libPath = stdenv.lib.makeLibraryPath + [ stdenv.gcc.libc + stdenv.gcc.gcc + gmp4 + ncurses + zlib + ] + ":${stdenv.gcc.gcc}/lib64"; + + cryptol-bin = + if stdenv.system == "i686-linux" + then requireFile { + url = "https://www.galois.com/cryptol"; + name = "${name}-i386-centos6-linux.tar.gz"; + sha256 = "131jkj3nh29rwwq5w5sfdf5jrb3c7ayjp4709v1zh84q4d6b35nf"; + } + else requireFile { + url = "https://www.galois.com/cryptol"; + name = "${name}-x86_64-centos6-linux.tar.gz"; + sha256 = "1dmkns8s6r2d6pvh176w8k3891frik6hmcr2ibghk4l6qr6gwarx"; + }; + + lss-bin = + if stdenv.system == "i686-linux" + then requireFile { + url = "https://www.galois.com/cryptol"; + name = "${lss-ver}-centos6-32.tar.gz"; + sha256 = "015ssw3v523wwzkma0qbpj3jnyzckab5q00ypdz0gr3kjcxn5rxg"; + } + else requireFile { + url = "https://www.galois.com/cryptol"; + name = "${lss-ver}-centos6-64.tar.gz"; + sha256 = "1zjy4xi8v3m6g8ydm9q6dgzg5xn0xc3a4zsll5plbhngprgwxcxm"; + }; + + jss-bin = + if stdenv.system == "i686-linux" + then requireFile { + url = "https://www.galois.com/cryptol"; + name = "${jss-ver}-centos5-32.tar.gz"; + sha256 = "1rlj14fbh9k3yvals8jsarczwl51fh6zjaic0pnhpc9s4p0pnjbr"; + } + else requireFile { + url = "https://www.galois.com/cryptol"; + name = "${jss-ver}-centos5-64.tar.gz"; + sha256 = "0smarm2pi3jz4c8jas9gwcbghc6vc375vrwxbdj1mqx4awlhnz1n"; + }; + +in +stdenv.mkDerivation rec { + inherit name version cryptol-bin jss-bin lss-bin; + + src = [ cryptol-bin lss-bin jss-bin ]; + buildInputs = [ makeWrapper ]; + + unpackPhase = '' + tar xf ${cryptol-bin} + tar xf ${lss-bin} + tar xf ${jss-bin} + ''; + + installPhase = '' + mkdir -p $out/share $out/libexec + + # Move Cryptol + mv cryptol-${version}/bin $out + mv cryptol-${version}/lib $out + mv cryptol-${version}/man $out/share + rm -f $out/bin/cryptol-2 + + # Move JSS + # Create a wrapper for jss to keep the .jar out of the way + mv ${jss-ver}/bin/jss $out/libexec + mv ${jss-ver}/bin/galois.jar $out/libexec + makeWrapper $out/libexec/jss $out/bin/jss --run "cd $out/libexec" + mv ${jss-ver}/doc/jss.1 $out/share/man/man1 + + # Move LSS + mv ${lss-ver}/bin/lss $out/bin + mv ${lss-ver}/sym-api $out/include + + # Hack around lack of libtinfo in NixOS + ln -s ${ncurses}/lib/libncursesw.so.5.9 $out/lib/libtinfo.so.5 + ln -s ${stdenv.gcc.libc}/lib/libpthread-2.19.so $out/lib/libpthread.so.0 + ''; + + fixupPhase = '' + for x in bin/cryptol bin/edif2verilog bin/copy-iverilog bin/symbolic_netlist bin/jaig bin/vvp-galois bin/lss libexec/jss; do + patchelf --interpreter "$(cat $NIX_GCC/nix-support/dynamic-linker)" \ + --set-rpath "$out/lib:${libPath}" $out/$x + patchelf --shrink-rpath $out/$x + done + ''; + + phases = "unpackPhase installPhase fixupPhase"; + + meta = { + description = "Cryptol: The Language of Cryptography"; + homepage = "https://cryptol.net"; + license = stdenv.lib.licenses.unfree; + platforms = stdenv.lib.platforms.linux; + maintainers = [ stdenv.lib.maintainers.thoughtpolice ]; + }; +} diff --git a/pkgs/development/compilers/cryptol/default.nix b/pkgs/development/compilers/cryptol/2.0.x.nix similarity index 100% rename from pkgs/development/compilers/cryptol/default.nix rename to pkgs/development/compilers/cryptol/2.0.x.nix diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index 20bf5027c1a..0d3d293bbb9 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -2461,6 +2461,7 @@ let cmucl_binary = callPackage ../development/compilers/cmucl/binary.nix { }; + cryptol1 = lowPrio (callPackage ../development/compilers/cryptol/1.8.x.nix {}); cryptol2 = haskellPackages.cryptol; cython = pythonPackages.cython; diff --git a/pkgs/top-level/haskell-packages.nix b/pkgs/top-level/haskell-packages.nix index 02e6472479d..dd7510e4c3f 100644 --- a/pkgs/top-level/haskell-packages.nix +++ b/pkgs/top-level/haskell-packages.nix @@ -3001,7 +3001,7 @@ let result = let callPackage = x : y : modifyPrio (newScope result.finalReturn x arbtt = callPackage ../applications/misc/arbtt {}; - cryptol = callPackage ../development/compilers/cryptol { + cryptol = callPackage ../development/compilers/cryptol/2.0.x.nix { QuickCheck = self.QuickCheck_2_7_3; text = self.text_1_1_0_1; cabalInstall = self.cabalInstall_1_18_0_3;