diff options
| -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))) |