Add coq libraries

Julien LepillerThu Jun 01 18:17:40+0200 2017

05eb710

Add coq libraries

README.md

6363 
Gradle is partially written in groovy, which itself is partially written in
6464 
groovy. I currently am working on some dependencies, but I don't have a clear
6565 
plan for groovy.
66+
67+
OCaml and Coq packages
68+
----------------------
69+
70+
The more the better. They are being integrated.
more/packages/ocaml.scm
2525 
  #:use-module ((guix licenses) #:prefix license:)
2626 
  #:use-module (gnu packages)
2727 
  #:use-module (gnu packages base)
28+
  #:use-module (gnu packages bison)
29+
  #:use-module (gnu packages boost)
2830 
  #:use-module (gnu packages emacs)
31+
  #:use-module (gnu packages flex)
2932 
  #:use-module (gnu packages llvm)
3033 
  #:use-module (gnu packages multiprecision)
3134 
  #:use-module (gnu packages ocaml)
…
11661169 
    ;; actually the "INRIA Non-Commercial License Agreement"
11671170 
    ;; a non-free license.
11681171 
    (license (license:non-copyleft "file:///LICENSE"))))
1172+
1173+
;; yet another build system <3
1174+
;; In this one, the autoconf-generated configure script configures the build and
1175+
;; builds remake from source, a make-like system specific to this package.
1176+
(define-public coq-flocq
1177+
  (package
1178+
    (name "coq-flocq")
1179+
    (version "2.5.2")
1180+
    (source (origin
1181+
              (method url-fetch)
1182+
              (uri (string-append "https://gforge.inria.fr/frs/download.php/file/36199/flocq-"
1183+
                                  version ".tar.gz"))
1184+
              (sha256
1185+
               (base32
1186+
                "0h5mlasirfzc0wwn2isg4kahk384n73145akkpinrxq5jsn5d22h"))))
1187+
    (build-system gnu-build-system)
1188+
    (native-inputs
1189+
     `(("ocaml" ,ocaml)
1190+
       ("which" ,which)
1191+
       ("coq" ,coq)))
1192+
    (arguments
1193+
     `(#:configure-flags
1194+
       (list (string-append "--libdir=" (assoc-ref %outputs "out")
1195+
                            "/lib/coq/user-contrib/Flocq"))
1196+
       #:phases
1197+
       (modify-phases %standard-phases
1198+
         (add-before 'configure 'fix-remake
1199+
           (lambda _
1200+
             (substitute* "remake.cpp"
1201+
               (("/bin/sh") (which "sh")))))
1202+
         (replace 'build
1203+
           (lambda _
1204+
             (zero? (system* "./remake"))))
1205+
         (replace 'check
1206+
           (lambda _
1207+
             (zero? (system* "./remake" "check"))))
1208+
             ;; TODO: requires coq-gappa and coq-interval.
1209+
             ;(zero? (system* "./remake" "check-more"))))
1210+
         (replace 'install
1211+
           (lambda _
1212+
             (zero? (system* "./remake" "install")))))))
1213+
    (home-page "http://flocq.gforge.inria.fr/")
1214+
    (synopsis "Floating-point formalization for the Coq system")
1215+
    (description "Flocq (Floats for Coq) is a floating-point formalization for
1216+
the Coq system.  It provides a comprehensive library of theorems on a multi-radix
1217+
multi-precision arithmetic.  It also supports efficient numerical computations
1218+
inside Coq.")
1219+
    (license license:lgpl3+)))
1220+
1221+
(define-public coq-gappa
1222+
  (package
1223+
    (name "coq-gappa")
1224+
    (version "1.3.1")
1225+
    (source (origin
1226+
              (method url-fetch)
1227+
              (uri (string-append "https://gforge.inria.fr/frs/download.php/file/36351/gappa-"
1228+
                                  version ".tar.gz"))
1229+
              (sha256
1230+
               (base32
1231+
                "0924jr6f15fx22qfsvim5vc0qxqg30ivg9zxj34lf6slbgdl3j39"))))
1232+
    (build-system gnu-build-system)
1233+
    (native-inputs
1234+
     `(("ocaml" ,ocaml)
1235+
       ("which" ,which)
1236+
       ("coq" ,coq)
1237+
       ("bison" ,bison)
1238+
       ("flex" ,flex)))
1239+
    (inputs
1240+
     `(("gmp" ,gmp)
1241+
       ("mpfr" ,mpfr)
1242+
       ("boost" ,boost)))
1243+
    (arguments
1244+
     `(#:configure-flags
1245+
       (list (string-append "--libdir=" (assoc-ref %outputs "out")
1246+
                            "/lib/coq/user-contrib/Gappa"))
1247+
       #:phases
1248+
       (modify-phases %standard-phases
1249+
         (add-before 'configure 'fix-remake
1250+
           (lambda _
1251+
             (substitute* "remake.cpp"
1252+
               (("/bin/sh") (which "sh")))))
1253+
         (replace 'build
1254+
           (lambda _
1255+
             (zero? (system* "./remake"))))
1256+
         (replace 'check
1257+
           (lambda _
1258+
             (zero? (system* "./remake" "check"))))
1259+
         (replace 'install
1260+
           (lambda _
1261+
             (zero? (system* "./remake" "install")))))))
1262+
    (home-page "http://gappa.gforge.inria.fr/")
1263+
    (synopsis "Verify and formally prove properties on numerical programs")
1264+
    (description "Gappa is a tool intended to help verifying and formally proving
1265+
properties on numerical programs dealing with floating-point or fixed-point
1266+
arithmetic.  It has been used to write robust floating-point filters for CGAL
1267+
and it is used to certify elementary functions in CRlibm.  While Gappa is
1268+
intended to be used directly, it can also act as a backend prover for the Why3
1269+
software verification plateform or as an automatic tactic for the Coq proof
1270+
assistant.")
1271+
    (license (list license:gpl2 license:cecill))))
1272+
1273+
(define-public coq-mathcomp
1274+
  (package
1275+
    (name "coq-mathcomp")
1276+
    (version "1.6.1")
1277+
    (source (origin
1278+
              (method url-fetch)
1279+
              (uri (string-append "https://github.com/math-comp/math-comp/archive/mathcomp-"
1280+
                                  version ".tar.gz"))
1281+
              (sha256
1282+
               (base32
1283+
                "1j9ylggjzrxz1i2hdl2yhsvmvy5z6l4rprwx7604401080p5sgjw"))))
1284+
    (build-system gnu-build-system)
1285+
    (native-inputs
1286+
     `(("ocaml" ,ocaml)
1287+
       ("which" ,which)
1288+
       ("coq" ,coq)))
1289+
    (arguments
1290+
     `(#:tests? #f; No need to test formally-verified programs :)
1291+
       #:phases
1292+
       (modify-phases %standard-phases
1293+
         (delete 'configure)
1294+
         (add-before 'build 'chdir
1295+
           (lambda _
1296+
             (chdir "mathcomp")))
1297+
         (replace 'install
1298+
           (lambda* (#:key outputs #:allow-other-keys)
1299+
             (setenv "COQLIB" (string-append (assoc-ref outputs "out") "/lib/coq/"))
1300+
             (zero? (system* "make" "-f" "Makefile.coq"
1301+
                             (string-append "COQLIB=" (assoc-ref outputs "out")
1302+
                                            "/lib/coq/")
1303+
                             "install")))))))
1304+
    (home-page "https://math-comp.github.io/math-comp/")
1305+
    (synopsis "Mathematical Components for Coq")
1306+
    (description "Mathematical Components for Coq has its origins in the formal
1307+
proof of the Four Colour Theorem.  Since then it has grown to cover many areas
1308+
of mathematics and has been used for large scale projects like the formal proof
1309+
of the Odd Order Theorem.
1310+
1311+
The library is written using the Ssreflect proof language that is an integral
1312+
part of the distribution.")
1313+
    (license license:cecill-b)))
1314+
1315+
;; TODO: coquelicot
1316+
1317+
(define-public coq-interval
1318+
  (package
1319+
    (name "coq-interval")
1320+
    (version "3.2.0")
1321+
    (source (origin
1322+
              (method url-fetch)
1323+
              (uri (string-append "https://gforge.inria.fr/frs/download.php/"
1324+
                                  "file/36538/interval-" version ".tar.gz"))
1325+
              (sha256
1326+
               (base32
1327+
                "16ir7mizl18kwa1ls8fwjih6r87894bvc1r6lh85cd43la7nriq3"))))
1328+
    (build-system gnu-build-system)
1329+
    (native-inputs
1330+
     `(("ocaml" ,ocaml)
1331+
       ("which" ,which)
1332+
       ("coq" ,coq)))
1333+
    (propagated-inputs
1334+
     `(("flocq" ,coq-flocq)
1335+
       ("mathcomp" ,coq-mathcomp)))
1336+
    (arguments
1337+
     `(#:configure-flags
1338+
       (list (string-append "--libdir=" (assoc-ref %outputs "out")
1339+
                            "/lib/coq/user-contrib/Gappa"))
1340+
       #:phases
1341+
       (modify-phases %standard-phases
1342+
         (add-before 'configure 'fix-remake
1343+
           (lambda _
1344+
             (substitute* "remake.cpp"
1345+
               (("/bin/sh") (which "sh")))))
1346+
         (replace 'build
1347+
           (lambda _
1348+
             (zero? (system* "./remake"))))
1349+
         (replace 'check
1350+
           (lambda _
1351+
             (zero? (system* "./remake" "check"))))
1352+
         (replace 'install
1353+
           (lambda _
1354+
             (zero? (system* "./remake" "install")))))))
1355+
    (home-page "http://coq-interval.gforge.inria.fr/")
1356+
    (synopsis "Coq tactics to simplify inequality proofs")
1357+
    (description "Interval provides vernacular files containing tactics for
1358+
simplifying the proofs of inequalities on expressions of real numbers for the
1359+
Coq proof assistant.")
1360+
    (license license:cecill-c)))