diff options
Diffstat (limited to 'gnu/packages/rocq.scm')
| -rw-r--r-- | gnu/packages/rocq.scm | 38 |
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+))) |