[bug#27444] coq libraries

[Ludovic Courtès]

Hello!

Julien Lepiller <address@hidden> skribis:

> Le Thu, 22 Jun 2017 21:39:09 +0200,
> address@hidden (Ludovic Courtès) a écrit :
>
>> Hi Julien,
>> 
>> Julien Lepiller <address@hidden> skribis:
>> 
>> > From dc5475afb4cc2edde0a77a3211654ae835198441 Mon Sep 17 00:00:00
>> > 2001 From: Julien Lepiller <address@hidden>
>> > 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’.