diff options
| -rw-r--r-- | gnu/packages/coq.scm | 41 |
1 files changed, 41 insertions, 0 deletions
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index 0ce96d4fd7..60937af750 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -44,6 +44,7 @@ #:use-module (guix build-system gnu) #:use-module (guix build-system ocaml) #:use-module (guix download) + #:use-module (guix gexp) #:use-module (guix git-download) #:use-module ((guix licenses) #:prefix license:) #:use-module (guix packages) @@ -730,3 +731,43 @@ contains a generic order and set libary, which will eventually be used to subsume notations for finite sets.") (home-page "https://math-comp.github.io/") (license license:cecill-b))) + +(define-public coq-mathcomp-bigenough + (package + (name "coq-mathcomp-bigenough") + (version "1.0.1") + (source (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/math-comp/bigenough") + (commit version))) + (file-name (git-file-name name version)) + (sha256 + (base32 + "02f4dv4rz72liciwxb2k7acwx6lgqz4381mqyq5854p3nbyn06aw")))) + (build-system gnu-build-system) + (arguments + `(;; No references to tests in Makefile.common. + ;; It doesn't appear as though tests will be included + ;; by the packaged project in the future. + #:tests? #f + #:make-flags ,#~(list (string-append "COQBIN=" + #$(this-package-input "coq-core") + "/bin/") + (string-append "COQMF_COQLIB=" + (assoc-ref %outputs "out") + "/lib/ocaml/site-lib/coq") + (string-append "COQLIBINSTALL=" + (assoc-ref %outputs "out") + "/lib/coq/user-contrib")) + #:phases (modify-phases %standard-phases + (delete 'configure)))) + (propagated-inputs (list coq coq-core coq-mathcomp which)) + (home-page "https://math-comp.github.io/") + (synopsis "Small library to do epsilon - N reasoning") + (description + "The package is used for reasoning with big enough objects (mostly +natural numbers). This package is essentially for backward compatibility +purposes as @code{bigenough} will be subsumed by the near tactics. The +formalization is based on the Mathematical Components library.") + (license license:cecill-b))) |