Packaged lambda-0.0.1

1 files changed, 38 insertions, 0 deletions

diff --git a/gnu/packages/rocq.scm b/gnu/packages/rocq.scm
new file mode 100644
index 0000000..d0837b4
--- /dev/null
+++ b/gnu/packages/rocq.scm
@@ -0,0 +1,38 @@
+(define-module (gnu packages rocq)
+  #:use-module (gnu packages autotools)
+  #:use-module (gnu packages base)  
+  #:use-module (gnu packages coq)
+  #:use-module (gnu packages gawk)
+  #:use-module (guix build-system gnu)
+  #:use-module (guix download)
+  #:use-module (guix gexp)
+  #:use-module (guix git-download)  
+  #:use-module (guix licenses)
+  #:use-module (guix packages))
+
+(define-public lambda
+  (package
+   (name "lambda")
+   (version "0.0.1")
+   (source (origin
+	     (method git-fetch)
+	     (uri (git-reference
+			(url "git://git.rostovtsev.org/lambda")
+			(commit "v0.0.1")))
+	    (sha256
+	     (base32 ;; nix32
+	      "0yk1shd3d6kz8pdbv11fg462kcvxvsw6lvmp7plqiiqicm4fbir4"))))
+   (build-system gnu-build-system)
+   (native-inputs (list coq
+			autoconf
+			automake ; alocal used here for some reason
+			which    ; used in autoconf step
+			gawk     ; used in autoconf step
+			))
+   (synopsis "Fundamental objects and results in the untyped lambda calculus.")
+   (description
+    (string-append
+     "A Rocq library for working with a weak call-by-value lambda calculus."
+     "Provides proofs of the Church-Rosser Properties and Uniform Confluence."))
+   (home-page "https://git.rostovtsev.org/lambda")
+   (license gpl3+)))