GNU bug report logs - #27444
coq libraries

Previous Next

Full log

Message #8 received at 27444 <at> debbugs.gnu.org (full text, mbox):

From: ludo <at> gnu.org (Ludovic Courtès)
To: Julien Lepiller <julien <at> lepiller.eu>
Cc: 27444 <at> debbugs.gnu.org
Subject: Re: [bug#27444] coq libraries
Date: Thu, 22 Jun 2017 21:39:09 +0200

Hi Julien,

Julien Lepiller <julien <at> lepiller.eu> skribis:

> From dc5475afb4cc2edde0a77a3211654ae835198441 Mon Sep 17 00:00:00 2001
> From: Julien Lepiller <julien <at> lepiller.eu>
> 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”?

> From 2aa65616e6b478fb539e6a9a8bf00285e054e7f4 Mon Sep 17 00:00:00 2001
> From: Julien Lepiller <julien <at> lepiller.eu>
> 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 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))))

Please indicate if it’s a mixture of both licenses or a choice up to the
user.  Also, double-check whether it’s ‘gpl2’ and not ‘gpl2+’.

Otherwise LGTM.

> From 67fd96b375b25c83f4be5be82ce963ad1a3f651e Mon Sep 17 00:00:00 2001
> From: Julien Lepiller <julien <at> lepiller.eu>
> 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 <julien <at> lepiller.eu>
> 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 <julien <at> lepiller.eu>
> 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’.

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.