diff options
| author | Garek Dyszel <garekdyszel@disroot.org> | 2022-09-07 14:33:39 -0400 |
|---|---|---|
| committer | Julien Lepiller <julien@lepiller.eu> | 2022-09-24 20:24:45 +0200 |
| commit | 17098178c1869fb86a3b29c79cdf39ba1f4820e7 (patch) | |
| tree | 98fd08775857568f7a6daa9959569c020dfad4ac /gnu/packages/coq.scm | |
| parent | 8371ad64083970f68c8e1dd5f04b1f10d9cf029d (diff) | |
| download | guix-17098178c1869fb86a3b29c79cdf39ba1f4820e7.tar guix-17098178c1869fb86a3b29c79cdf39ba1f4820e7.tar.gz | |
gnu: Add coq-mathcomp-finmap.
* gnu/packages/coq.scm (coq-mathcomp-finmap): New variable.
Signed-off-by: Julien Lepiller <julien@lepiller.eu>
Diffstat (limited to 'gnu/packages/coq.scm')
| -rw-r--r-- | gnu/packages/coq.scm | 36 |
1 files changed, 36 insertions, 0 deletions
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index 09e04d9f7e..0ce96d4fd7 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -8,6 +8,7 @@ ;;; Copyright © 2020 Robin Green <greenrd@greenrd.org> ;;; Copyright © 2021 Xinglu Chen <public@yoctocell.xyz> ;;; Copyright © 2021 Simon Tournier <zimon.toutoune@gmail.com> +;;; Copyright © 2022 Garek Dyszel <garekdyszel@disroot.org> ;;; ;;; This file is part of GNU Guix. ;;; @@ -694,3 +695,38 @@ for goals involving set operations. @end itemize") (home-page "https://gitlab.mpi-sws.org/iris/stdpp") (license license:bsd-3))) + +(define-public coq-mathcomp-finmap + (package + (name "coq-mathcomp-finmap") + (version "1.5.2") + (source (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/math-comp/finmap") + (commit version))) + (file-name (git-file-name name version)) + (sha256 + (base32 + "1k72wpp15xa5ag358jl8a71gschng0bgbaqjx0l5a0in6x5adafh")))) + (build-system gnu-build-system) + (arguments + `(;; No tests supplied in Makefile.common. + ;; The project doesn't appear to have plans to include tests in + ;; the future. + #:tests? #f + #:make-flags (list (string-append "COQLIBINSTALL=" + (assoc-ref %outputs "out") + "/lib/coq/user-contrib")) + #:phases (modify-phases %standard-phases + (delete 'configure)))) + (inputs (list coq coq-stdlib coq-mathcomp which)) + (synopsis "Finite sets and finite types for coq-mathcomp") + (description + "This library is an extension of coq-mathcomp which supports finite sets +and finite maps on choicetypes (rather than finite types). This includes +support for functions with finite support and multisets. The library also +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))) |