From debbugs-submit-bounces@debbugs.gnu.org Wed Jun 21 15:46:15 2017 Received: (at submit) by debbugs.gnu.org; 21 Jun 2017 19:46:15 +0000 Received: from localhost ([127.0.0.1]:60265 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dNlZr-0002kg-E1 for submit@debbugs.gnu.org; Wed, 21 Jun 2017 15:46:15 -0400 Received: from eggs.gnu.org ([208.118.235.92]:33980) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dNlZp-0002kT-J9 for submit@debbugs.gnu.org; Wed, 21 Jun 2017 15:46:10 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1dNlZi-0006s5-I6 for submit@debbugs.gnu.org; Wed, 21 Jun 2017 15:46:04 -0400 X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on eggs.gnu.org X-Spam-Level: X-Spam-Status: No, score=0.8 required=5.0 tests=BAYES_50,T_DKIM_INVALID autolearn=disabled version=3.3.2 Received: from lists.gnu.org ([2001:4830:134:3::11]:55200) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1dNlZi-0006rz-E1 for submit@debbugs.gnu.org; Wed, 21 Jun 2017 15:46:02 -0400 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) DKIM-Signature: v=1; a=rsa-sha256; c=simple/simple; d=lepiller.eu; s=default; t=1498074350; bh=jrkyVVGY1kpZcSVt2Tc8xIRsX2lJi5PdGqgEUng0IWM=; h=Date:From:To:Subject:From; b=F4E0lYxoH3+2bh+Clrqta3xvpkrr1orgp2YtTqBICdGjNw9BcqWzMXDA9LY9iqK6z GDHW16taJrqY4JRCTsSgXurpbDcttn6ZRygd92hOv66198IyD5orTlPgvRyrHZDHAP DlNrx9qlWi2pWDltvGqtVHYK5N1uu2x2BUhBAHRvbQCzSjZeS1RPnYiwJOT63qqyWg b4kVR+LEeluKthzf8rMuz2G/T3X57koBMpjT9njxgaOqVjMBrJQVtim0zvPbWum+bY 2yQbzGgLxzzfTHoCK/Ndz6vjdCq72WIEe/Ph4zvIlyebPkHMCIt5g8q3lhwE/6tCvP Fr6bvApxE7OK4GWeAWV8yLtT7k9mWMhBd+RyW3saFjoxnc1PyuUm+4rVDkjUEuBrIg 0maYgMw6U51Ks9eulXmGFiiyfJKjKWZSFMBUIgKa3sOPmqBd06EEZzhDxqeDcYqTX+ Obs03FerDZQctNQQR7EGfwzPjaqjTa3LQhgMNGrjfhdBB+Asxj4SH6vR9mwmt3+74K vUrahF8ao3E3R1dowlELbWExUZXPe33nfw90J94JJCW6NoXClGlOyjtl046jd43Nxw 9NRvUIOapzEejVs3U059uMJO4nASbzKk8hzNJ9Bc5fdGLn72/U/zSlQXm/3/fUr+tw +pIuxP1uzZpLlFG6xNEzXq8w= X-Virus-Scanned: Debian amavisd-new at lepiller.eu 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) DKIM-Signature: v=1; a=rsa-sha256; c=simple/simple; d=lepiller.eu; s=default; t=1498074344; bh=jrkyVVGY1kpZcSVt2Tc8xIRsX2lJi5PdGqgEUng0IWM=; h=Date:From:To:Subject:From; b=n8IaSv5167ybIpkABEzuZP7xQ+lIUm8MLMx4zpKyN4tQHpd/bvsq48Yrg4Y/s+QCI oUF+Jp2VMKhONkjYi6v10DlqsgX4RFoeQXTop64MLwqt3hWDEnRidYj56U2XHEh/5v gLnvke3e0zk3IanETTXSuOY2VJ+OZzATUvxXl8DkY8AhSBr+rmm76CZNbbJXNarye4 C0UGc0yE+jVouMWQCdnKz8gJoqHv9rxpMpqxid+/feCp5+3w3CumXRPj9RyOakgIqG wE63ACcw9pv8DuL5M/BHobswwgQ7QL1N+zCWxZX7qakHeYzyxmb9IPzOqj1d7uM8qu Rou26Z/YFiUDGugU6b6g4NkymduoqMeucZAgt5HGh42s2hmc7hCyloh52/0VOuwsDw /cTxy5OIFhUpur/+oiP0bKpZBQpo2zBxE9IG1BRgKGqXe1JUVwxXimBbFQyZZlJMF8 RO1wOjtby+t13TUncYJhs90PEW1SaykmXH3X9kzzb5C2tDpTLyQ0FURdpX8ZIce/EP K8ugnN7jLLNTEridMdA8tZxar4cW0xvO6n1vc2TVcIkDwKaO4Y5LisCZHdIrcdckoD PKfu1yCirt9O4TNgvSLjSJHYI+TcJlLlN8iaugMrsCd6UottSciYXJ0JMNCqkygGut cP8PrRdGz+cKJi7kGJJ10pe4= Date: Wed, 21 Jun 2017 21:45:39 +0200 From: Julien Lepiller To: guix-patches@gnu.org Subject: coq libraries Message-ID: <20170621214539.756fd583@lepiller.eu> X-Mailer: Claws Mail 3.15.0-dirty (GTK+ 2.24.31; x86_64-unknown-linux-gnu) MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="MP_/bWso2dr_27xyNtbLRWvMris" X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] [fuzzy] X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.6.x X-Received-From: 2001:4830:134:3::11 X-Spam-Score: -5.0 (-----) X-Debbugs-Envelope-To: submit X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -5.0 (-----) --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-- From debbugs-submit-bounces@debbugs.gnu.org Thu Jun 22 15:39:23 2017 Received: (at 27444) by debbugs.gnu.org; 22 Jun 2017 19:39:23 +0000 Received: from localhost ([127.0.0.1]:33495 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dO7wp-0004i3-A5 for submit@debbugs.gnu.org; Thu, 22 Jun 2017 15:39:23 -0400 Received: from eggs.gnu.org ([208.118.235.92]:46468) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dO7wo-0004hq-0D for 27444@debbugs.gnu.org; Thu, 22 Jun 2017 15:39:22 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1dO7wf-00042R-I2 for 27444@debbugs.gnu.org; Thu, 22 Jun 2017 15:39:16 -0400 X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on eggs.gnu.org X-Spam-Level: X-Spam-Status: No, score=0.8 required=5.0 tests=BAYES_50,T_RP_MATCHES_RCVD autolearn=disabled version=3.3.2 Received: from fencepost.gnu.org ([2001:4830:134:3::e]:50252) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dO7wf-00042L-EH; Thu, 22 Jun 2017 15:39:13 -0400 Received: from reverse-83.fdn.fr ([80.67.176.83]:37494 helo=ribbon) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1dO7we-0004iT-MC; Thu, 22 Jun 2017 15:39:13 -0400 From: ludo@gnu.org (Ludovic =?utf-8?Q?Court=C3=A8s?=) To: Julien Lepiller Subject: Re: [bug#27444] coq libraries References: <20170621214539.756fd583@lepiller.eu> X-URL: http://www.fdn.fr/~lcourtes/ X-Revolutionary-Date: 4 Messidor an 225 de la =?utf-8?Q?R=C3=A9volution?= X-PGP-Key-ID: 0x090B11993D9AEBB5 X-PGP-Key: http://www.fdn.fr/~lcourtes/ludovic.asc X-PGP-Fingerprint: 3CE4 6455 8A84 FDC6 9DB4 0CFB 090B 1199 3D9A EBB5 X-OS: x86_64-unknown-linux-gnu Date: Thu, 22 Jun 2017 21:39:09 +0200 In-Reply-To: <20170621214539.756fd583@lepiller.eu> (Julien Lepiller's message of "Wed, 21 Jun 2017 21:45:39 +0200") Message-ID: <87mv8zrew2.fsf@gnu.org> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.2 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 2001:4830:134:3::e X-Spam-Score: -5.0 (-----) X-Debbugs-Envelope-To: 27444 Cc: 27444@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -5.0 (-----) Hi Julien, Julien Lepiller skribis: > 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. LGTM. > + `(#:configure-flags > + (list (string-append "--libdir=3D" (assoc-ref %outputs "out") > + "/lib/coq/user-contrib/Flocq")) Should we add a search path specification in Coq for =E2=80=9Clib/coq=E2=80= =9D? > 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. [...] > + (home-page "http://gappa.gforge.inria.fr/") > + (synopsis "Verify and formally prove properties on numerical program= s") > + (description "Gappa is a tool intended to help verifying and formall= y proving > +properties on numerical programs dealing with floating-point or fixed-po= int > +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 th= e Why3 > +software verification plateform or as an automatic tactic for the Coq pr= oof > +assistant.") > + (license (list license:gpl2 license:cecill)))) Please indicate if it=E2=80=99s a mixture of both licenses or a choice up t= o the user. Also, double-check whether it=E2=80=99s =E2=80=98gpl2=E2=80=99 and n= ot =E2=80=98gpl2+=E2=80=99. Otherwise LGTM. > 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. LGTM. > 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. LGTM. > 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. OK! Thank you, Ludo=E2=80=99. From debbugs-submit-bounces@debbugs.gnu.org Thu Jul 27 14:45:13 2017 Received: (at 27444) by debbugs.gnu.org; 27 Jul 2017 18:45:13 +0000 Received: from localhost ([127.0.0.1]:58911 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1danmb-0002qA-8Q for submit@debbugs.gnu.org; Thu, 27 Jul 2017 14:45:13 -0400 Received: from static-176-182-42-79.ncc.abo.bbox.fr ([176.182.42.79]:56580 helo=metebelis3) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1danmZ-0002pw-6s for 27444@debbugs.gnu.org; Thu, 27 Jul 2017 14:45:12 -0400 Received: from localhost (bbox.lan [192.168.1.254]); by metebelis3 (OpenSMTPD) with ESMTPSA id 23942fa4; TLS version=TLSv1/SSLv3 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NO; for <27444@debbugs.gnu.org>; Thu, 27 Jul 2017 18:45:03 +0000 (UTC) Date: Thu, 27 Jul 2017 20:44:27 +0200 From: Julien Lepiller To: 27444@debbugs.gnu.org Subject: Re: [bug#27444] coq libraries Message-ID: <20170727204427.5a2eaf3b@lepiller.eu> In-Reply-To: <87mv8zrew2.fsf@gnu.org> References: <20170621214539.756fd583@lepiller.eu> <87mv8zrew2.fsf@gnu.org> X-Mailer: Claws Mail 3.15.0-dirty (GTK+ 2.24.31; x86_64-unknown-linux-gnu) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable X-Spam-Score: 3.6 (+++) X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org", has NOT identified this incoming email as spam. The original message has been attached to this so you can view it or label similar future email. If you have any questions, see the administrator of that system for details. Content preview: Le Thu, 22 Jun 2017 21:39:09 +0200, ludo@gnu.org (Ludovic Courtès) a écrit : > Hi Julien, > > Julien Lepiller skribis: > > > 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. > > LGTM. > > > + `(#:configure-flags > > + (list (string-append "--libdir=" (assoc-ref %outputs "out") > > + "/lib/coq/user-contrib/Flocq")) > > Should we add a search path specification in Coq for “lib/coq”? [...] Content analysis details: (3.6 points, 10.0 required) pts rule name description ---- ---------------------- -------------------------------------------------- 0.0 FSL_HELO_NON_FQDN_1 No description available. 3.6 RCVD_IN_PBL RBL: Received via a relay in Spamhaus PBL [176.182.42.79 listed in zen.spamhaus.org] -0.0 SPF_PASS SPF: sender matches SPF record X-Debbugs-Envelope-To: 27444 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: 3.6 (+++) X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org", has NOT identified this incoming email as spam. The original message has been attached to this so you can view it or label similar future email. If you have any questions, see the administrator of that system for details. Content preview: Le Thu, 22 Jun 2017 21:39:09 +0200, ludo@gnu.org (Ludovic Courtès) a écrit : > Hi Julien, > > Julien Lepiller skribis: > > > 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. > > LGTM. > > > + `(#:configure-flags > > + (list (string-append "--libdir=" (assoc-ref %outputs "out") > > + "/lib/coq/user-contrib/Flocq")) > > Should we add a search path specification in Coq for “lib/coq”? [...] Content analysis details: (3.6 points, 10.0 required) pts rule name description ---- ---------------------- -------------------------------------------------- 3.6 RCVD_IN_PBL RBL: Received via a relay in Spamhaus PBL [176.182.42.79 listed in zen.spamhaus.org] 0.0 FSL_HELO_NON_FQDN_1 No description available. -0.0 SPF_PASS SPF: sender matches SPF record Le Thu, 22 Jun 2017 21:39:09 +0200, ludo@gnu.org (Ludovic Court=C3=A8s) a =C3=A9crit : > Hi Julien, >=20 > Julien Lepiller skribis: >=20 > > 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. =20 >=20 > LGTM. >=20 > > + `(#:configure-flags > > + (list (string-append "--libdir=3D" (assoc-ref %outputs "out") > > + "/lib/coq/user-contrib/Flocq")) =20 >=20 > Should we add a search path specification in Coq for =E2=80=9Clib/coq=E2= =80=9D? If I do that, coq doesn't work correctly anymore. >=20 > > 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. =20 >=20 > [...] >=20 > > + (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)))) =20 >=20 > Please indicate if it=E2=80=99s a mixture of both licenses or a choice up= to > the user. Also, double-check whether it=E2=80=99s =E2=80=98gpl2=E2=80=99= and not =E2=80=98gpl2+=E2=80=99. I'm not sure. The source says "under the terms of the GNU General Public License version." (including the dot). >=20 > Otherwise LGTM. >=20 > > 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. =20 >=20 > LGTM. >=20 > > 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. =20 >=20 > LGTM. >=20 > > 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. =20 >=20 > OK! >=20 > Thank you, > Ludo=E2=80=99. Thanks for the review and sorry for the very late reply. From debbugs-submit-bounces@debbugs.gnu.org Fri Jul 28 15:49:12 2017 Received: (at 27444) by debbugs.gnu.org; 28 Jul 2017 19:49:12 +0000 Received: from localhost ([127.0.0.1]:60323 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dbBG3-0005pl-T5 for submit@debbugs.gnu.org; Fri, 28 Jul 2017 15:49:12 -0400 Received: from eggs.gnu.org ([208.118.235.92]:40466) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dbBG2-0005pW-D7 for 27444@debbugs.gnu.org; Fri, 28 Jul 2017 15:49:10 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1dbBFs-0000nA-Ez for 27444@debbugs.gnu.org; Fri, 28 Jul 2017 15:49:05 -0400 X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on eggs.gnu.org X-Spam-Level: X-Spam-Status: No, score=-0.5 required=5.0 tests=BAYES_05,RP_MATCHES_RCVD autolearn=disabled version=3.3.2 Received: from fencepost.gnu.org ([2001:4830:134:3::e]:40703) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dbBFs-0000mv-Bc; Fri, 28 Jul 2017 15:49:00 -0400 Received: from reverse-83.fdn.fr ([80.67.176.83]:50518 helo=ribbon) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1dbBFr-0005MU-Rb; Fri, 28 Jul 2017 15:49:00 -0400 From: ludo@gnu.org (Ludovic =?utf-8?Q?Court=C3=A8s?=) To: Julien Lepiller Subject: Re: [bug#27444] coq libraries References: <20170621214539.756fd583@lepiller.eu> <87mv8zrew2.fsf@gnu.org> <20170727204427.5a2eaf3b@lepiller.eu> X-URL: http://www.fdn.fr/~lcourtes/ X-Revolutionary-Date: 10 Thermidor an 225 de la =?utf-8?Q?R=C3=A9volution?= X-PGP-Key-ID: 0x090B11993D9AEBB5 X-PGP-Key: http://www.fdn.fr/~lcourtes/ludovic.asc X-PGP-Fingerprint: 3CE4 6455 8A84 FDC6 9DB4 0CFB 090B 1199 3D9A EBB5 X-OS: x86_64-unknown-linux-gnu Date: Fri, 28 Jul 2017 21:48:58 +0200 In-Reply-To: <20170727204427.5a2eaf3b@lepiller.eu> (Julien Lepiller's message of "Thu, 27 Jul 2017 20:44:27 +0200") Message-ID: <87h8xwl4ut.fsf@gnu.org> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.2 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 2001:4830:134:3::e X-Spam-Score: -5.0 (-----) X-Debbugs-Envelope-To: 27444 Cc: 27444@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -5.0 (-----) Hello! Julien Lepiller skribis: > Le Thu, 22 Jun 2017 21:39:09 +0200, > ludo@gnu.org (Ludovic Court=C3=A8s) a =C3=A9crit : > >> Hi Julien, >>=20 >> Julien Lepiller skribis: >>=20 >> > 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.=20=20 >>=20 >> LGTM. >>=20 >> > + `(#:configure-flags >> > + (list (string-append "--libdir=3D" (assoc-ref %outputs "out") >> > + "/lib/coq/user-contrib/Flocq"))=20=20 >>=20 >> Should we add a search path specification in Coq for =E2=80=9Clib/coq=E2= =80=9D? > > If I do that, coq doesn't work correctly anymore. Would be nice to see why. Perhaps because it can=E2=80=99t find its own fi= les anymore or something like that? >> > + (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))))=20=20 >>=20 >> Please indicate if it=E2=80=99s a mixture of both licenses or a choice u= p to >> the user. Also, double-check whether it=E2=80=99s =E2=80=98gpl2=E2=80= =99 and not =E2=80=98gpl2+=E2=80=99. > > I'm not sure. The source says "under the terms of the GNU General > Public License version." (including the dot). Then it =E2=80=98gpl2+=E2=80=99 (assuming the =E2=80=98COPYING=E2=80=99 fil= e is that of v2.) Thanks, Ludo=E2=80=99. From debbugs-submit-bounces@debbugs.gnu.org Sun Jul 30 04:56:26 2017 Received: (at 27444-done) by debbugs.gnu.org; 30 Jul 2017 08:56:27 +0000 Received: from localhost ([127.0.0.1]:33571 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dbk1S-0002wG-Nw for submit@debbugs.gnu.org; Sun, 30 Jul 2017 04:56:26 -0400 Received: from static-176-182-42-79.ncc.abo.bbox.fr ([176.182.42.79]:57692 helo=metebelis3) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dbk1R-0002w2-5a for 27444-done@debbugs.gnu.org; Sun, 30 Jul 2017 04:56:25 -0400 Received: from localhost (bbox.lan [192.168.1.254]); by metebelis3 (OpenSMTPD) with ESMTPSA id 9e8ebd8e; TLS version=TLSv1/SSLv3 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NO; for <27444-done@debbugs.gnu.org>; Sun, 30 Jul 2017 08:56:18 +0000 (UTC) Date: Sun, 30 Jul 2017 10:55:46 +0200 From: Julien Lepiller To: 27444-done@debbugs.gnu.org Subject: Re: [bug#27444] coq libraries Message-ID: <20170730105546.7c069491@lepiller.eu> In-Reply-To: <87h8xwl4ut.fsf@gnu.org> References: <20170621214539.756fd583@lepiller.eu> <87mv8zrew2.fsf@gnu.org> <20170727204427.5a2eaf3b@lepiller.eu> <87h8xwl4ut.fsf@gnu.org> X-Mailer: Claws Mail 3.15.0-dirty (GTK+ 2.24.31; x86_64-unknown-linux-gnu) MIME-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit X-Spam-Score: 3.6 (+++) X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org", has NOT identified this incoming email as spam. The original message has been attached to this so you can view it or label similar future email. If you have any questions, see the administrator of that system for details. Content preview: Pushed as d163d97d92f3abea98f4b36d55ac3bb9db23d423 - 303690c405446d1eea231044f0bcb48b88b6508d [...] Content analysis details: (3.6 points, 10.0 required) pts rule name description ---- ---------------------- -------------------------------------------------- 3.6 RCVD_IN_PBL RBL: Received via a relay in Spamhaus PBL [176.182.42.79 listed in zen.spamhaus.org] 0.0 FSL_HELO_NON_FQDN_1 No description available. -0.0 SPF_PASS SPF: sender matches SPF record X-Debbugs-Envelope-To: 27444-done X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: 3.6 (+++) X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org", has NOT identified this incoming email as spam. The original message has been attached to this so you can view it or label similar future email. If you have any questions, see the administrator of that system for details. Content preview: Pushed as d163d97d92f3abea98f4b36d55ac3bb9db23d423 - 303690c405446d1eea231044f0bcb48b88b6508d [...] Content analysis details: (3.6 points, 10.0 required) pts rule name description ---- ---------------------- -------------------------------------------------- 3.6 RCVD_IN_PBL RBL: Received via a relay in Spamhaus PBL [176.182.42.79 listed in zen.spamhaus.org] 0.0 FSL_HELO_NON_FQDN_1 No description available. -0.0 SPF_PASS SPF: sender matches SPF record Pushed as d163d97d92f3abea98f4b36d55ac3bb9db23d423 - 303690c405446d1eea231044f0bcb48b88b6508d From unknown Wed Aug 20 03:37:39 2025 Received: (at fakecontrol) by fakecontrolmessage; To: internal_control@debbugs.gnu.org From: Debbugs Internal Request Subject: Internal Control Message-Id: bug archived. Date: Sun, 27 Aug 2017 11:24:04 +0000 User-Agent: Fakemail v42.6.9 # This is a fake control message. # # The action: # bug archived. thanks # This fakemail brought to you by your local debbugs # administrator