From 8b9b2210dc1a7e1ac63bd85df9e8d0c39c59a3f0 Mon Sep 17 00:00:00 2001 From: Tobias Geerinckx-Rice Date: Sun, 23 Dec 2018 11:06:13 +0100 Subject: gnu: coq: Don't use unstable tarball. * gnu/packages/coq.scm (coq)[source]: Use GIT-FETCH and GIT-FILE-NAME. [arguments]: Add 'make-git-checkout-writable' phase. --- gnu/packages/coq.scm | 22 ++++++++++++++-------- 1 file changed, 14 insertions(+), 8 deletions(-) (limited to 'gnu/packages/coq.scm') diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index e42f8af1ab..6cedb8363f 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -1,5 +1,6 @@ ;;; GNU Guix --- Functional package management for GNU ;;; Copyright © 2018 Julien Lepiller +;;; Copyright © 2018 Tobias Geerinckx-Rice ;;; Copyright © 2019 Dan Frumin ;;; ;;; This file is part of GNU Guix. @@ -42,14 +43,15 @@ (define-public coq (package (name "coq") (version "8.8.2") - (source (origin - (method url-fetch) - (uri (string-append "https://github.com/coq/coq/archive/V" - version ".tar.gz")) - (file-name (string-append name "-" version ".tar.gz")) - (sha256 - (base32 - "0i2hs0i6rp27cy8zd0mx7jscqw5cx2y0diw0pxgij66s3yr47y7r")))) + (source + (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/coq/coq.git") + (commit (string-append "V" version)))) + (file-name (git-file-name name version)) + (sha256 + (base32 "03v8b57mz3ivsijwxy51avzwiyhla5ijaf98a5a2q29yabdq8dkp")))) (native-search-paths (list (search-path-specification (variable "COQPATH") @@ -63,6 +65,10 @@ (define-public coq (arguments `(#:phases (modify-phases %standard-phases + (add-after 'unpack 'make-git-checkout-writable + (lambda _ + (for-each make-file-writable (find-files ".")) + #t)) (replace 'configure (lambda* (#:key outputs #:allow-other-keys) (let* ((out (assoc-ref outputs "out")) -- cgit v1.2.3 From aaa2add87111051b01159aa2e46dd7f55b28edb6 Mon Sep 17 00:00:00 2001 From: Tobias Geerinckx-Rice Date: Sun, 23 Dec 2018 11:11:33 +0100 Subject: gnu: coq-mathcomp: Don't use unstable tarball. * gnu/packages/coq.scm (coq-mathcomp)[source]: Use GIT-FETCH and GIT-FILE-NAME. --- gnu/packages/coq.scm | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) (limited to 'gnu/packages/coq.scm') diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index 6cedb8363f..fa02f85cdf 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -285,20 +285,22 @@ (define-public coq-mathcomp (package (name "coq-mathcomp") (version "1.7.0") - (source (origin - (method url-fetch) - (uri (string-append "https://github.com/math-comp/math-comp/archive/mathcomp-" - version ".tar.gz")) - (sha256 - (base32 - "05zgyi4wmasi1rcyn5jq42w0bi9713q9m8dl1fdgl66nmacixh39")))) + (source + (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/math-comp/math-comp.git") + (commit (string-append "mathcomp-" version)))) + (file-name (git-file-name name version)) + (sha256 + (base32 "1cdzi67jj440xkdpxm10aly80zpn56vjzj2ygb67iq3xpljlv95h")))) (build-system gnu-build-system) (native-inputs `(("ocaml" ,ocaml) ("which" ,which) ("coq" ,coq))) (arguments - `(#:tests? #f; No need to test formally-verified programs :) + `(#:tests? #f ; no need to test formally-verified programs :) #:phases (modify-phases %standard-phases (delete 'configure) -- cgit v1.2.3 From ec23bae682ab144179fad8d5ed6c2545d85384ad Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Wed, 13 Feb 2019 12:34:40 +0100 Subject: gnu: Add coq-equations. * gnu/packages/coq.scm (coq-equations): New variable. Signed-off-by: Julien Lepiller --- gnu/packages/coq.scm | 41 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 41 insertions(+) (limited to 'gnu/packages/coq.scm') 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 @@ (define-public coq-autosubst 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))) -- cgit v1.2.3