From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from eggs.gnu.org ([2001:4830:134:3::10]:53367) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dNlak-0004RP-97 for guix-patches@gnu.org; Wed, 21 Jun 2017 15:47:08 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1dNlag-000710-AA for guix-patches@gnu.org; Wed, 21 Jun 2017 15:47:06 -0400 Received: from debbugs.gnu.org ([208.118.235.43]:57588) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1dNlag-00070w-5Z for guix-patches@gnu.org; Wed, 21 Jun 2017 15:47:02 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1dNlaf-0002ll-T6 for guix-patches@gnu.org; Wed, 21 Jun 2017 15:47:01 -0400 Subject: [bug#27444] coq libraries Resent-Message-ID: Received: from eggs.gnu.org ([2001:4830:134:3::10]:53149) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dNlZf-0004Hw-Pg for guix-patches@gnu.org; Wed, 21 Jun 2017 15:46:02 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1dNlZb-0006qF-TM for guix-patches@gnu.org; Wed, 21 Jun 2017 15:45:59 -0400 Received: from 89-92-10-219.hfc.dyn.abo.bbox.fr ([89.92.10.219]:36058 helo=skaro.lepiller.eu) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1dNlZb-0006pY-8g for guix-patches@gnu.org; Wed, 21 Jun 2017 15:45:55 -0400 Received: from localhost (localhost [127.0.0.1]) by skaro.lepiller.eu (Postfix) with ESMTP id 3E862815A6 for ; Wed, 21 Jun 2017 21:45:50 +0200 (CEST) Received: from skaro.lepiller.eu ([127.0.0.1]) by localhost (lepiller.eu [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id LVU8GV_vzdKv for ; Wed, 21 Jun 2017 21:45:44 +0200 (CEST) Received: from localhost (bbox.lan [192.168.1.254]) by skaro.lepiller.eu (Postfix) with ESMTPSA id 2D72C80B9F for ; Wed, 21 Jun 2017 21:45:44 +0200 (CEST) Date: Wed, 21 Jun 2017 21:45:39 +0200 From: Julien Lepiller Message-ID: <20170621214539.756fd583@lepiller.eu> MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="MP_/bWso2dr_27xyNtbLRWvMris" List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+kyle=kyleam.com@gnu.org Sender: "Guix-patches" To: 27444@debbugs.gnu.org --MP_/bWso2dr_27xyNtbLRWvMris Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Content-Disposition: inline Hi, here are 5 coq libraries. --MP_/bWso2dr_27xyNtbLRWvMris Content-Type: text/x-patch Content-Transfer-Encoding: 7bit Content-Disposition: attachment; filename=0001-gnu-Add-coq-flocq.patch >From dc5475afb4cc2edde0a77a3211654ae835198441 Mon Sep 17 00:00:00 2001 From: Julien Lepiller Date: Thu, 8 Jun 2017 18:25:32 +0200 Subject: [PATCH 1/5] gnu: Add coq-flocq. * gnu/packages/ocaml.scm (coq-flocq): New variable. --- gnu/packages/ocaml.scm | 45 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 45 insertions(+) diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm index 68619019f..82da0bf1d 100644 --- a/gnu/packages/ocaml.scm +++ b/gnu/packages/ocaml.scm @@ -3153,3 +3153,48 @@ writing to these structures, and they are accessed via the Bigarray module.") (synopsis "Minimal library providing hexadecimal converters") (description "Hex is a minimal library providing hexadecimal converters.") (license license:isc))) + +(define-public coq-flocq + (package + (name "coq-flocq") + (version "2.5.2") + (source (origin + (method url-fetch) + (uri (string-append "https://gforge.inria.fr/frs/download.php/file" + "/36199/flocq-" version ".tar.gz")) + (sha256 + (base32 + "0h5mlasirfzc0wwn2isg4kahk384n73145akkpinrxq5jsn5d22h")))) + (build-system gnu-build-system) + (native-inputs + `(("ocaml" ,ocaml) + ("which" ,which) + ("coq" ,coq))) + (arguments + `(#:configure-flags + (list (string-append "--libdir=" (assoc-ref %outputs "out") + "/lib/coq/user-contrib/Flocq")) + #:phases + (modify-phases %standard-phases + (add-before 'configure 'fix-remake + (lambda _ + (substitute* "remake.cpp" + (("/bin/sh") (which "sh"))))) + (replace 'build + (lambda _ + (zero? (system* "./remake")))) + (replace 'check + (lambda _ + (zero? (system* "./remake" "check")))) + ;; TODO: requires coq-gappa and coq-interval. + ;(zero? (system* "./remake" "check-more")))) + (replace 'install + (lambda _ + (zero? (system* "./remake" "install"))))))) + (home-page "http://flocq.gforge.inria.fr/") + (synopsis "Floating-point formalization for the Coq system") + (description "Flocq (Floats for Coq) is a floating-point formalization for +the Coq system. It provides a comprehensive library of theorems on a multi-radix +multi-precision arithmetic. It also supports efficient numerical computations +inside Coq.") + (license license:lgpl3+))) -- 2.13.1 --MP_/bWso2dr_27xyNtbLRWvMris Content-Type: text/x-patch Content-Transfer-Encoding: 7bit Content-Disposition: attachment; filename=0002-gnu-Add-coq-gappa.patch >From 2aa65616e6b478fb539e6a9a8bf00285e054e7f4 Mon Sep 17 00:00:00 2001 From: Julien Lepiller Date: Wed, 21 Jun 2017 21:38:42 +0200 Subject: [PATCH 2/5] gnu: Add coq-gappa. * gnu/packages/ocaml.scm (coq-gappa): New variable. --- gnu/packages/ocaml.scm | 52 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 52 insertions(+) diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm index 82da0bf1d..21e4a7d72 100644 --- a/gnu/packages/ocaml.scm +++ b/gnu/packages/ocaml.scm @@ -3198,3 +3198,55 @@ the Coq system. It provides a comprehensive library of theorems on a multi-radi multi-precision arithmetic. It also supports efficient numerical computations inside Coq.") (license license:lgpl3+))) + +(define-public coq-gappa + (package + (name "coq-gappa") + (version "1.3.1") + (source (origin + (method url-fetch) + (uri (string-append "https://gforge.inria.fr/frs/download.php/file/36351/gappa-" + version ".tar.gz")) + (sha256 + (base32 + "0924jr6f15fx22qfsvim5vc0qxqg30ivg9zxj34lf6slbgdl3j39")))) + (build-system gnu-build-system) + (native-inputs + `(("ocaml" ,ocaml) + ("which" ,which) + ("coq" ,coq) + ("bison" ,bison) + ("flex" ,flex))) + (inputs + `(("gmp" ,gmp) + ("mpfr" ,mpfr) + ("boost" ,boost))) + (arguments + `(#:configure-flags + (list (string-append "--libdir=" (assoc-ref %outputs "out") + "/lib/coq/user-contrib/Gappa")) + #:phases + (modify-phases %standard-phases + (add-before 'configure 'fix-remake + (lambda _ + (substitute* "remake.cpp" + (("/bin/sh") (which "sh"))))) + (replace 'build + (lambda _ + (zero? (system* "./remake")))) + (replace 'check + (lambda _ + (zero? (system* "./remake" "check")))) + (replace 'install + (lambda _ + (zero? (system* "./remake" "install"))))))) + (home-page "http://gappa.gforge.inria.fr/") + (synopsis "Verify and formally prove properties on numerical programs") + (description "Gappa is a tool intended to help verifying and formally proving +properties on numerical programs dealing with floating-point or fixed-point +arithmetic. It has been used to write robust floating-point filters for CGAL +and it is used to certify elementary functions in CRlibm. While Gappa is +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)))) -- 2.13.1 --MP_/bWso2dr_27xyNtbLRWvMris Content-Type: text/x-patch Content-Transfer-Encoding: 7bit Content-Disposition: attachment; filename=0003-gnu-Add-coq-mathcomp.patch >From 67fd96b375b25c83f4be5be82ce963ad1a3f651e Mon Sep 17 00:00:00 2001 From: Julien Lepiller Date: Wed, 21 Jun 2017 21:39:33 +0200 Subject: [PATCH 3/5] gnu: Add coq-mathcomp. * gnu/packages/ocaml.scm (coq-mathcomp): New variable. --- gnu/packages/ocaml.scm | 42 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 42 insertions(+) diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm index 21e4a7d72..51530399c 100644 --- a/gnu/packages/ocaml.scm +++ b/gnu/packages/ocaml.scm @@ -3250,3 +3250,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)))) + +(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))) -- 2.13.1 --MP_/bWso2dr_27xyNtbLRWvMris Content-Type: text/x-patch Content-Transfer-Encoding: 7bit Content-Disposition: attachment; filename=0004-gnu-Add-coq-coquelicot.patch >From 2ef53eb922f64b4f359704ef06a796339efc776f Mon Sep 17 00:00:00 2001 From: Julien Lepiller Date: Wed, 21 Jun 2017 21:40:23 +0200 Subject: [PATCH 4/5] gnu: Add coq-coquelicot. * gnu/packages/ocaml.scm (coq-coquelicot): New variable. --- gnu/packages/ocaml.scm | 50 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 50 insertions(+) diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm index 51530399c..86c6e135f 100644 --- a/gnu/packages/ocaml.scm +++ b/gnu/packages/ocaml.scm @@ -3292,3 +3292,53 @@ 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))) + +(define-public coq-coquelicot + (package + (name "coq-coquelicot") + (version "3.0.0") + (source (origin + (method url-fetch) + (uri (string-append "https://gforge.inria.fr/frs/download.php/" + "file/36537/coquelicot-" version ".tar.gz")) + (sha256 + (base32 + "0fx99bvsbdizj00gx2im8939y4wwl05f4qhw184j90kcx5vjxxv9")))) + (build-system gnu-build-system) + (native-inputs + `(("ocaml" ,ocaml) + ("which" ,which) + ("coq" ,coq))) + (propagated-inputs + `(("mathcomp" ,coq-mathcomp))) + (arguments + `(#:configure-flags + (list (string-append "--libdir=" (assoc-ref %outputs "out") + "/lib/coq/user-contrib/Coquelicot")) + #:phases + (modify-phases %standard-phases + (add-before 'configure 'fix-remake + (lambda _ + (substitute* "remake.cpp" + (("/bin/sh") (which "sh"))))) + (replace 'build + (lambda _ + (zero? (system* "./remake")))) + (replace 'check + (lambda _ + (zero? (system* "./remake" "check")))) + (replace 'install + (lambda _ + (zero? (system* "./remake" "install"))))))) + (home-page "http://coquelicot.saclay.inria.fr/index.html") + (synopsis "Coq library for Reals") + (description "Coquelicot is an easier way of writing formulas and theorem +statements, achieved by relying on total functions in place of dependent types +for limits, derivatives, integrals, power series, and so on. To help with the +proof process, the library comes with a comprehensive set of theorems that cover +not only these notions, but also some extensions such as parametric integrals, +two-dimensional differentiability, asymptotic behaviors. It also offers some +automations for performing differentiability proofs. Moreover, Coquelicot is a +conservative extension of Coq's standard library and provides correspondence +theorems between the two libraries.") + (license license:lgpl3+))) -- 2.13.1 --MP_/bWso2dr_27xyNtbLRWvMris Content-Type: text/x-patch Content-Transfer-Encoding: 7bit Content-Disposition: attachment; filename=0005-gnu-Add-coq-interval.patch >From a76224a176850d38ae2bc80a6d77493ab3fffa41 Mon Sep 17 00:00:00 2001 From: Julien Lepiller Date: Wed, 21 Jun 2017 21:41:36 +0200 Subject: [PATCH 5/5] gnu: Add coq-interval. * gnu/packages/ocaml.scm (coq-interval): New variable. --- gnu/packages/ocaml.scm | 46 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 46 insertions(+) diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm index 86c6e135f..a4249fc55 100644 --- a/gnu/packages/ocaml.scm +++ b/gnu/packages/ocaml.scm @@ -3342,3 +3342,49 @@ automations for performing differentiability proofs. Moreover, Coquelicot is a conservative extension of Coq's standard library and provides correspondence theorems between the two libraries.") (license license:lgpl3+))) + +(define-public coq-interval + (package + (name "coq-interval") + (version "3.2.0") + (source (origin + (method url-fetch) + (uri (string-append "https://gforge.inria.fr/frs/download.php/" + "file/36538/interval-" version ".tar.gz")) + (sha256 + (base32 + "16ir7mizl18kwa1ls8fwjih6r87894bvc1r6lh85cd43la7nriq3")))) + (build-system gnu-build-system) + (native-inputs + `(("ocaml" ,ocaml) + ("which" ,which) + ("coq" ,coq))) + (propagated-inputs + `(("flocq" ,coq-flocq) + ("coquelicot" ,coq-coquelicot) + ("mathcomp" ,coq-mathcomp))) + (arguments + `(#:configure-flags + (list (string-append "--libdir=" (assoc-ref %outputs "out") + "/lib/coq/user-contrib/Gappa")) + #:phases + (modify-phases %standard-phases + (add-before 'configure 'fix-remake + (lambda _ + (substitute* "remake.cpp" + (("/bin/sh") (which "sh"))))) + (replace 'build + (lambda _ + (zero? (system* "./remake")))) + (replace 'check + (lambda _ + (zero? (system* "./remake" "check")))) + (replace 'install + (lambda _ + (zero? (system* "./remake" "install"))))))) + (home-page "http://coq-interval.gforge.inria.fr/") + (synopsis "Coq tactics to simplify inequality proofs") + (description "Interval provides vernacular files containing tactics for +simplifying the proofs of inequalities on expressions of real numbers for the +Coq proof assistant.") + (license license:cecill-c))) -- 2.13.1 --MP_/bWso2dr_27xyNtbLRWvMris--