GNU bug report logs - #27444
coq libraries

Previous Next

To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 27444 in the body.
You can then email your comments to 27444 AT debbugs.gnu.org in the normal way.

Toggle the display of automated, internal messages from the tracker.

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

From: Julien Lepiller <julien <at> lepiller.eu>
To: guix-patches <at> gnu.org
Subject: coq libraries
Date: Wed, 21 Jun 2017 21:45:39 +0200

[Message part 1 (text/plain, inline)]

Hi,

here are 5 coq libraries.

[0001-gnu-Add-coq-flocq.patch (text/x-patch, attachment)]

[0002-gnu-Add-coq-gappa.patch (text/x-patch, attachment)]

[0003-gnu-Add-coq-mathcomp.patch (text/x-patch, attachment)]

[0004-gnu-Add-coq-coquelicot.patch (text/x-patch, attachment)]

[0005-gnu-Add-coq-interval.patch (text/x-patch, attachment)]

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’.

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

From: Julien Lepiller <julien <at> lepiller.eu>
To: 27444 <at> debbugs.gnu.org
Subject: Re: [bug#27444] coq libraries
Date: Thu, 27 Jul 2017 20:44:27 +0200

Le Thu, 22 Jun 2017 21:39:09 +0200,
ludo <at> gnu.org (Ludovic Courtès) a écrit :

> 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”?

If I do that, coq doesn't work correctly anymore.

> 
> > 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+’.

I'm not sure. The source says "under the terms of the GNU General
Public License version." (including the dot).

> 
> 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’.

Thanks for the review and sorry for the very late reply.

Message #14 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: Fri, 28 Jul 2017 21:48:58 +0200

Hello!

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

> Le Thu, 22 Jun 2017 21:39:09 +0200,
> ludo <at> gnu.org (Ludovic Courtès) a écrit :
>
>> 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”?
>
> If I do that, coq doesn't work correctly anymore.

Would be nice to see why.  Perhaps because it can’t find its own files
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))))  
>> 
>> 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+’.
>
> I'm not sure. The source says "under the terms of the GNU General
> Public License version." (including the dot).

Then it ‘gpl2+’ (assuming the ‘COPYING’ file is that of v2.)

Thanks,
Ludo’.

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

From: Julien Lepiller <julien <at> lepiller.eu>
To: 27444-done <at> debbugs.gnu.org
Subject: Re: [bug#27444] coq libraries
Date: Sun, 30 Jul 2017 10:55:46 +0200

Pushed as d163d97d92f3abea98f4b36d55ac3bb9db23d423 -
303690c405446d1eea231044f0bcb48b88b6508d

Previous Next

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