aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDan Frumin <dfrumin@cs.ru.nl>2019-02-13 12:34:40 +0100
committerJulien Lepiller <julien@lepiller.eu>2019-02-13 22:21:41 +0100
commitec23bae682ab144179fad8d5ed6c2545d85384ad (patch)
treef38b774eaef848b3996232615915786d045a8615
parent57e508d1c13cc95a37cf44ed429d1d0b97ef763d (diff)
downloadguix-ec23bae682ab144179fad8d5ed6c2545d85384ad.tar
guix-ec23bae682ab144179fad8d5ed6c2545d85384ad.tar.gz
gnu: Add coq-equations.
* gnu/packages/coq.scm (coq-equations): New variable. Signed-off-by: Julien Lepiller <julien@lepiller.eu>
-rw-r--r--gnu/packages/coq.scm41
1 files changed, 41 insertions, 0 deletions
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index fa02f85cdf..3cd8c4cb69 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)))