From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from eggs.gnu.org ([2001:4830:134:3::10]:37514) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dO7xW-0006Me-DK for guix-patches@gnu.org; Thu, 22 Jun 2017 15:40:07 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1dO7xT-0004uv-1e for guix-patches@gnu.org; Thu, 22 Jun 2017 15:40:06 -0400 Received: from debbugs.gnu.org ([208.118.235.43]:59051) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1dO7xS-0004uj-V2 for guix-patches@gnu.org; Thu, 22 Jun 2017 15:40:02 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1dO7xS-0004ix-M4 for guix-patches@gnu.org; Thu, 22 Jun 2017 15:40:02 -0400 Subject: [bug#27444] coq libraries Resent-Message-ID: From: ludo@gnu.org (Ludovic =?UTF-8?Q?Court=C3=A8s?=) References: <20170621214539.756fd583@lepiller.eu> 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> MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable 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: Julien Lepiller Cc: 27444@debbugs.gnu.org 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.