[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
01/01: gnu: Add coq-equations.
From: |
guix-commits |
Subject: |
01/01: gnu: Add coq-equations. |
Date: |
Wed, 13 Feb 2019 16:22:26 -0500 (EST) |
roptat pushed a commit to branch master
in repository guix.
commit ec23bae682ab144179fad8d5ed6c2545d85384ad
Author: Dan Frumin <address@hidden>
Date: Wed Feb 13 12:34:40 2019 +0100
gnu: Add coq-equations.
* gnu/packages/coq.scm (coq-equations): New variable.
Signed-off-by: Julien Lepiller <address@hidden>
---
gnu/packages/coq.scm | 41 +++++++++++++++++++++++++++++++++++++++++
1 file changed, 41 insertions(+)
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index fa02f85..3cd8c4c 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -500,3 +500,44 @@ work on a decision procedure for the equational theory of
an extension of the
sigma-calculus by Abadi et al. The library is completely written in Coq and
uses Ltac to synthesize the substitution operation.")
(license license:bsd-3))))
+
+(define-public coq-equations
+ (package
+ (name "coq-equations")
+ (version "1.1")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/mattam82/Coq-Equations.git")
+ (commit (string-append "v" version "-8.8"))))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "129rxsdsf88vjcw0xhm74yax1hmnk6f8n9ksg0hcyyjq1ijddiwa"))))
+ (build-system gnu-build-system)
+ (native-inputs
+ `(("ocaml" ,ocaml)
+ ("coq" ,coq)
+ ("camlp5" ,camlp5)))
+ (arguments
+ `(#:test-target "test-suite"
+ #:phases
+ (modify-phases %standard-phases
+ (replace 'configure
+ (lambda* (#:key outputs #:allow-other-keys)
+ (invoke "coq_makefile" "-f" "_CoqProject" "-o" "Makefile")))
+ (replace 'install
+ (lambda* (#:key outputs #:allow-other-keys)
+ (setenv "COQLIB" (string-append (assoc-ref outputs "out")
"/lib/coq/"))
+ (invoke "make"
+ (string-append "COQLIB=" (assoc-ref outputs "out")
+ "/lib/coq/")
+ "install"))))))
+ (home-page "https://mattam82.github.io/Coq-Equations/")
+ (synopsis "Function definition plugin for Coq")
+ (description "Equations provides a notation for writing programs
+by dependent pattern-matching and (well-founded) recursion in Coq. It
+compiles everything down to eliminators for inductive types, equality
+and accessibility, providing a definitional extension to the Coq
+kernel.")
+ (license license:lgpl2.1)))