JonPRL: init at 0.1.0

2015-09-09 21:23:48 +10:00
parent bd37676269
commit e9bdf0fc07
2 changed files with 40 additions and 0 deletions
@@ -0,0 +1,34 @@
+{ fetchgit, stdenv, smlnj, which }:
+
+stdenv.mkDerivation rec {
+  name = "JonPRL";
+  version = "v0.1.0";
+
+  src = fetchgit {
+    url = "https://github.com/jonsterling/JonPRL.git";
+    deepClone = true;
+    rev = "refs/tags/${version}";
+    sha256 = "1z0d8dq1nb4dycic58nnk617hbfgafz0vmwr8gkl0i6405gfg1zy";
+  };
+
+  buildInputs = [ smlnj which ];
+
+  installPhase = ''
+    mkdir -p "$out/bin"
+    cp bin/.heapimg.* "$out/bin/"
+    build/mkexec.sh "${smlnj}/bin/sml" "$out" jonprl
+  '';
+
+  meta = {
+    description = "Proof Refinement Logic - Computational Type Theory";
+    longDescription = ''
+      An proof refinement logic for computational type theory
+      based on Brouwer-realizability & meaning explanations.
+      Inspired by Nuprl
+    '';
+    homepage = http://www.jonprl.org/;
+    license = stdenv.lib.licenses.mit;
+    maintainers = with stdenv.lib.maintainers; [ puffnfresh ];
+    platforms = stdenv.lib.platforms.unix;
+  };
+}