[bug#27444] coq libraries

[bug#27444] coq libraries

[Julien Lepiller]

[-- Attachment #1: Type: text/plain, Size: 30 bytes --]

Hi,

here are 5 coq libraries.

[-- Attachment #2: 0001-gnu-Add-coq-flocq.patch --]
[-- Type: text/x-patch, Size: 2557 bytes --]

From dc5475afb4cc2edde0a77a3211654ae835198441 Mon Sep 17 00:00:00 2001
From: Julien Lepiller <julien@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.
---
 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


[-- Attachment #3: 0002-gnu-Add-coq-gappa.patch --]
[-- Type: text/x-patch, Size: 2785 bytes --]

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


[-- Attachment #4: 0003-gnu-Add-coq-mathcomp.patch --]
[-- Type: text/x-patch, Size: 2520 bytes --]

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


[-- Attachment #5: 0004-gnu-Add-coq-coquelicot.patch --]
[-- Type: text/x-patch, Size: 2858 bytes --]

From 2ef53eb922f64b4f359704ef06a796339efc776f Mon Sep 17 00:00:00 2001
From: Julien Lepiller <julien@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.
---
 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


[-- Attachment #6: 0005-gnu-Add-coq-interval.patch --]
[-- Type: text/x-patch, Size: 2484 bytes --]

From a76224a176850d38ae2bc80a6d77493ab3fffa41 Mon Sep 17 00:00:00 2001
From: Julien Lepiller <julien@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.
---
 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

[bug#27444] coq libraries

[Ludovic Courtès]

Hi Julien,

Julien Lepiller <julien@lepiller.eu> skribis:

> From dc5475afb4cc2edde0a77a3211654ae835198441 Mon Sep 17 00:00:00 2001
> From: Julien Lepiller <julien@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@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@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@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@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’.

[bug#27444] coq libraries

[Julien Lepiller]

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

> Hi Julien,
> 
> Julien Lepiller <julien@lepiller.eu> skribis:
> 
> > From dc5475afb4cc2edde0a77a3211654ae835198441 Mon Sep 17 00:00:00
> > 2001 From: Julien Lepiller <julien@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@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@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@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@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.

[bug#27444] coq libraries

[Ludovic Courtès]

Hello!

Julien Lepiller <julien@lepiller.eu> skribis:

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

bug#27444: coq libraries

[Julien Lepiller]

Pushed as d163d97d92f3abea98f4b36d55ac3bb9db23d423 -
303690c405446d1eea231044f0bcb48b88b6508d