summary refs log tree commit diff
path: root/gnu/packages
diff options
context:
space:
mode:
authorJulien Lepiller <julien@lepiller.eu>2017-06-21 21:39:33 +0200
committerJulien Lepiller <julien@lepiller.eu>2017-07-29 15:18:59 +0200
commit380c65de949bbba0db3ff1679df723ddb50d9665 (patch)
tree15ea54a6648d52ed0b4204eb6f988f563ae8a188 /gnu/packages
parent88191acee23ce304c25da623efe56ff011831f3c (diff)
downloadguix-380c65de949bbba0db3ff1679df723ddb50d9665.tar.gz
gnu: Add coq-mathcomp.
* gnu/packages/ocaml.scm (coq-mathcomp): New variable.
Diffstat (limited to 'gnu/packages')
-rw-r--r--gnu/packages/ocaml.scm42
1 files changed, 42 insertions, 0 deletions
diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index 687b3d25fc..1ed0ffa76e 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -3253,3 +3253,45 @@ intended to be used directly, it can also act as a backend prover for the Why3
 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)))