ryan77627/guix
1
0
Fork 0
mirror of https://git.in.rschanz.org/ryan77627/guix.git synced 2024-12-27 06:42:14 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

gnu: Add coq-mathcomp.

Browse source 
* gnu/packages/ocaml.scm (coq-mathcomp): New variable.
This commit is contained in:
Julien Lepiller 2017-06-21 21:39:33 +02:00
parent 88191acee2
commit 380c65de94
No known key found for this signature in database
GPG key ID: 43111F4520086A0C
1 changed files with 42 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

42
gnu/packages/ocaml.scm
View file

@ -3253,3 +3253,45 @@ (define-public coq-gappa
software verification plateform or as an automatic tactic for the Coq proof
assistant.")
(license (list license:gpl2+ license:cecill))));either gpl2+ or cecill
(define-public coq-mathcomp
(package
(name "coq-mathcomp")
(version "1.6.1")
(source (origin
(method url-fetch)
(uri (string-append "https://github.com/math-comp/math-comp/archive/mathcomp-"
version ".tar.gz"))
(sha256
(base32
"1j9ylggjzrxz1i2hdl2yhsvmvy5z6l4rprwx7604401080p5sgjw"))))
(build-system gnu-build-system)
(native-inputs
`(("ocaml" ,ocaml)
("which" ,which)
("coq" ,coq)))
(arguments
`(#:tests? #f; No need to test formally-verified programs :)
#:phases
(modify-phases %standard-phases
(delete 'configure)
(add-before 'build 'chdir
(lambda _
(chdir "mathcomp")))
(replace 'install
(lambda* (#:key outputs #:allow-other-keys)
(setenv "COQLIB" (string-append (assoc-ref outputs "out") "/lib/coq/"))
(zero? (system* "make" "-f" "Makefile.coq"
(string-append "COQLIB=" (assoc-ref outputs "out")
"/lib/coq/")
"install")))))))
(home-page "https://math-comp.github.io/math-comp/")
(synopsis "Mathematical Components for Coq")
(description "Mathematical Components for Coq has its origins in the formal
proof of the Four Colour Theorem. Since then it has grown to cover many areas
of mathematics and has been used for large scale projects like the formal proof
of the Odd Order Theorem.
The library is written using the Ssreflect proof language that is an integral
part of the distribution.")
(license license:cecill-b)))