[bug#28925] [PATCH] Update coq and coq libraries.

[bug#28925] [PATCH] Update coq and coq libraries.

[Julien Lepiller]

Hi,

this patch series updates coq and its libraries.

[bug#28925] [PATCH 1/7] gnu: camlp5: install META file.

[julien]

From: Julien Lepiller <julien@lepiller.eu>

* gnu/packages/ocaml.scm (camlp5) [phases]: New install-meta phase.
---
 gnu/packages/ocaml.scm | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index aa2f00667..40d42a5d4 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -401,7 +401,12 @@ syntax of OCaml.")
                   (lambda _
                     (zero? (system* "make" "-j" (number->string
                                                  (parallel-job-count))
-                                    "world.opt")))))))
+                                    "world.opt"))))
+         ;; Required for findlib to find camlp5's libraries
+         (add-after 'install 'install-meta
+           (lambda* (#:key outputs #:allow-other-keys)
+             (install-file "etc/META" (string-append (assoc-ref outputs "out")
+                                                     "/lib/ocaml/camlp5/")))))))
     (home-page "http://camlp5.gforge.inria.fr/")
     (synopsis "Pre-processor Pretty Printer for OCaml")
     (description
-- 
2.14.2

[bug#28925] [PATCH] gnu: youtube-dl: Update to 2017.10.20.

[julien]

From: Tobias Geerinckx-Rice <me@tobias.gr>

* gnu/packages/video.scm (youtube-dl): Update to 2017.10.20.
---
 gnu/packages/ocaml.scm | 22 +++++++++++++++-------
 gnu/packages/video.scm |  4 ++--
 2 files changed, 17 insertions(+), 9 deletions(-)

diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index aa2f00667..8292ece2e 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -401,7 +401,11 @@ syntax of OCaml.")
                   (lambda _
                     (zero? (system* "make" "-j" (number->string
                                                  (parallel-job-count))
-                                    "world.opt")))))))
+                                    "world.opt"))))
+         (add-after 'install 'install-meta
+           (lambda* (#:key outputs #:allow-other-keys)
+             (install-file "etc/META" (string-append (assoc-ref outputs "out")
+                                                     "/lib/ocaml/camlp5/")))))))
     (home-page "http://camlp5.gforge.inria.fr/")
     (synopsis "Pre-processor Pretty Printer for OCaml")
     (description
@@ -445,26 +449,25 @@ written in Objective Caml.")
 (define-public coq
   (package
     (name "coq")
-    (version "8.5pl2")
+    (version "8.7.0")
     (source (origin
               (method url-fetch)
               (uri (string-append "https://coq.inria.fr/distrib/V" version
                                   "/files/" name "-" version ".tar.gz"))
               (sha256
                (base32
-                "0wyywia0darak2zmc5v0ra9rn0b9whwdfiahralm8v5za499s8w3"))))
+                "15wjngjd5pyfqdl5yw92rvdxvy15xcjlpx0rqlkzvcsis1z20xpk"))))
     (native-search-paths
      (list (search-path-specification
             (variable "COQPATH")
             (files (list "lib/coq/user-contrib")))))
-    (build-system gnu-build-system)
+    (build-system ocaml-build-system)
     (native-inputs
      `(("texlive" ,texlive)
-       ("findlib" ,ocaml-findlib)
        ("hevea" ,hevea)))
     (inputs
-     `(("ocaml" ,ocaml)
-       ("lablgtk" ,lablgtk)
+     `(("lablgtk" ,lablgtk)
+       ("python" ,python-2)
        ("camlp5" ,camlp5)))
     (arguments
      `(#:phases
@@ -488,6 +491,11 @@ written in Objective Caml.")
          (add-after 'install 'check
            (lambda _
              (with-directory-excursion "test-suite"
+               ;; These two tests fail.
+               ;; This one fails because the output is not formatted as expected.
+               (delete-file-recursively "coq-makefile/timing")
+               ;; This one fails because we didn't build coqtop.byte.
+               (delete-file-recursively "coq-makefile/findlib-package")
                (zero? (system* "make"))))))))
     (home-page "https://coq.inria.fr")
     (synopsis "Proof assistant for higher-order logic")
diff --git a/gnu/packages/video.scm b/gnu/packages/video.scm
index 43e4fc2eb..63824f6c5 100644
--- a/gnu/packages/video.scm
+++ b/gnu/packages/video.scm
@@ -1116,7 +1116,7 @@ access to mpv's powerful playback capabilities.")
 (define-public youtube-dl
   (package
     (name "youtube-dl")
-    (version "2017.10.15.1")
+    (version "2017.10.20")
     (source (origin
               (method url-fetch)
               (uri (string-append "https://yt-dl.org/downloads/"
@@ -1124,7 +1124,7 @@ access to mpv's powerful playback capabilities.")
                                   version ".tar.gz"))
               (sha256
                (base32
-                "0zr9sx0nxk36si8xbvhlnazb69xzlygrhsxcyiydm0dy5y5ycsns"))))
+                "0npr8b1xg1dylz717kfllw433h1y16251npzch48lchq69bhm4iy"))))
     (build-system python-build-system)
     (arguments
      ;; The problem here is that the directory for the man page and completion
-- 
2.14.2

[bug#28925] [PATCH 2/7] gnu: Update coq to 8.7.0.

[julien]

From: Julien Lepiller <julien@lepiller.eu>

* gnu/packages/ocaml.scm (coq): Update to 8.7.0.
---
 gnu/packages/ocaml.scm | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index 40d42a5d4..bbdde2801 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -450,26 +450,25 @@ written in Objective Caml.")
 (define-public coq
   (package
     (name "coq")
-    (version "8.5pl2")
+    (version "8.7.0")
     (source (origin
               (method url-fetch)
               (uri (string-append "https://coq.inria.fr/distrib/V" version
                                   "/files/" name "-" version ".tar.gz"))
               (sha256
                (base32
-                "0wyywia0darak2zmc5v0ra9rn0b9whwdfiahralm8v5za499s8w3"))))
+                "15wjngjd5pyfqdl5yw92rvdxvy15xcjlpx0rqlkzvcsis1z20xpk"))))
     (native-search-paths
      (list (search-path-specification
             (variable "COQPATH")
             (files (list "lib/coq/user-contrib")))))
-    (build-system gnu-build-system)
+    (build-system ocaml-build-system)
     (native-inputs
      `(("texlive" ,texlive)
-       ("findlib" ,ocaml-findlib)
        ("hevea" ,hevea)))
     (inputs
-     `(("ocaml" ,ocaml)
-       ("lablgtk" ,lablgtk)
+     `(("lablgtk" ,lablgtk)
+       ("python" ,python-2)
        ("camlp5" ,camlp5)))
     (arguments
      `(#:phases
@@ -493,6 +492,11 @@ written in Objective Caml.")
          (add-after 'install 'check
            (lambda _
              (with-directory-excursion "test-suite"
+               ;; These two tests fail.
+               ;; This one fails because the output is not formatted as expected.
+               (delete-file-recursively "coq-makefile/timing")
+               ;; This one fails because we didn't build coqtop.byte.
+               (delete-file-recursively "coq-makefile/findlib-package")
                (zero? (system* "make"))))))))
     (home-page "https://coq.inria.fr")
     (synopsis "Proof assistant for higher-order logic")
-- 
2.14.2

[bug#28925] [PATCH 3/7] gnu: Update coq-flocq to 2.6.0.

[julien]

From: Julien Lepiller <julien@lepiller.eu>

* gnu/packages/ocaml.scm (coq-flocq): Update to 2.6.0.
---
 gnu/packages/ocaml.scm | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index bbdde2801..f2b06d065 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -3560,14 +3560,14 @@ library is currently designed for Unicode Standard 3.2.")
 (define-public coq-flocq
   (package
     (name "coq-flocq")
-    (version "2.5.2")
+    (version "2.6.0")
     (source (origin
               (method url-fetch)
               (uri (string-append "https://gforge.inria.fr/frs/download.php/file"
-                                  "/36199/flocq-" version ".tar.gz"))
+                                  "/37054/flocq-" version ".tar.gz"))
               (sha256
                (base32
-                "0h5mlasirfzc0wwn2isg4kahk384n73145akkpinrxq5jsn5d22h"))))
+                "13fv150dcwnjrk00d7zj2c5x9jwmxgrq0ay440gkr730l8mvk3l3"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("ocaml" ,ocaml)
-- 
2.14.2

[bug#28925] [PATCH 4/7] gnu: Update coq-mathcomp to 1.6.2.

[julien]

From: Julien Lepiller <julien@lepiller.eu>

* gnu/packages/ocaml.scm (coq-mathcomp): Update to 1..6.2.
---
 gnu/packages/ocaml.scm | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index f2b06d065..beb73a2d0 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -3657,14 +3657,14 @@ assistant.")
 (define-public coq-mathcomp
   (package
     (name "coq-mathcomp")
-    (version "1.6.1")
+    (version "1.6.2")
     (source (origin
               (method url-fetch)
               (uri (string-append "https://github.com/math-comp/math-comp/archive/mathcomp-"
                                   version ".tar.gz"))
               (sha256
                (base32
-                "1j9ylggjzrxz1i2hdl2yhsvmvy5z6l4rprwx7604401080p5sgjw"))))
+                "0lg5ncr7p4y8qqq6pfw6brqc6a9xzlfa0drprwfdn0rnyaq5nca6"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("ocaml" ,ocaml)
-- 
2.14.2

[bug#28925] [PATCH 5/7] gnu: Update coq-coquelicot to 3.0.1.

[julien]

From: Julien Lepiller <julien@lepiller.eu>

* gnu/packages/ocaml.scm (coq-coquelicot): Update to 3.0.1.
---
 gnu/packages/ocaml.scm | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index beb73a2d0..6cf92689a 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -3699,14 +3699,14 @@ part of the distribution.")
 (define-public coq-coquelicot
   (package
     (name "coq-coquelicot")
-    (version "3.0.0")
+    (version "3.0.1")
     (source (origin
               (method url-fetch)
               (uri (string-append "https://gforge.inria.fr/frs/download.php/"
-                                  "file/36537/coquelicot-" version ".tar.gz"))
+                                  "file/37045/coquelicot-" version ".tar.gz"))
               (sha256
                (base32
-                "0fx99bvsbdizj00gx2im8939y4wwl05f4qhw184j90kcx5vjxxv9"))))
+                "0hsyhsy2lwqxxx2r8xgi5csmirss42lp9bkb9yy35mnya0w78c8r"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("ocaml" ,ocaml)
-- 
2.14.2

[bug#28925] [PATCH 6/7] gnu: Add coq-bignums.

[julien]

From: Julien Lepiller <julien@lepiller.eu>

* gnu/packages/ocaml.scm (coq-bignums): New variable.
---
 gnu/packages/ocaml.scm | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)

diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index 6cf92689a..addcdba5a 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -3746,6 +3746,38 @@ conservative extension of Coq's standard library and provides correspondence
 theorems between the two libraries.")
     (license license:lgpl3+)))
 
+(define-public coq-bignums
+  (package
+    (name "coq-bignums")
+    (version "8.7.0")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append "https://github.com/coq/bignums/archive/V"
+                                  version ".tar.gz"))
+              (file-name (string-append name "-" version ".tar.gz"))
+              (sha256
+               (base32
+                "03iw9jiwq9jx45gsvp315y3lxr8m9ksppmcjvxs5c23qnky6zqjx"))))
+    (build-system gnu-build-system)
+    (native-inputs
+     `(("ocaml" ,ocaml)
+       ("coq" ,coq)))
+    (inputs
+     `(("camlp5" ,camlp5)))
+    (arguments
+     `(#:tests? #f; No test target
+       #:make-flags
+       (list (string-append "COQLIBINSTALL=" (assoc-ref %outputs "out")
+                            "/lib/coq/user-contrib"))
+       #:phases
+       (modify-phases %standard-phases
+         (delete 'configure))))
+    (home-page "https://github.com/coq/bignums")
+    (synopsis "Coq library for arbitrary large numbers")
+    (description "Bignums is a coq library of arbitrary large numbers.  It
+provides BigN, BigZ, BigQ that used to be part of Coq standard library.")
+    (license license:lgpl2.1+)))
+
 (define-public coq-interval
   (package
     (name "coq-interval")
-- 
2.14.2

[bug#28925] [PATCH 7/7] gnu: Update coq-interval to 3.3.0.

[julien]

From: Julien Lepiller <julien@lepiller.eu>

* gnu/packages/ocaml.scm (coq-interval): Update to 3.3.0.
---
 gnu/packages/ocaml.scm | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index addcdba5a..b13168c7d 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -3781,14 +3781,14 @@ provides BigN, BigZ, BigQ that used to be part of Coq standard library.")
 (define-public coq-interval
   (package
     (name "coq-interval")
-    (version "3.2.0")
+    (version "3.3.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"))))
+                "08fdcf3hbwqphglvwprvqzgkg0qbimpyhnqsgv3gac4y1ap0f903"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("ocaml" ,ocaml)
@@ -3796,6 +3796,7 @@ provides BigN, BigZ, BigQ that used to be part of Coq standard library.")
        ("coq" ,coq)))
     (propagated-inputs
      `(("flocq" ,coq-flocq)
+       ("bignums" ,coq-bignums)
        ("coquelicot" ,coq-coquelicot)
        ("mathcomp" ,coq-mathcomp)))
     (arguments
-- 
2.14.2

[bug#28925] [PATCH] gnu: youtube-dl: Update to 2017.10.20.

[Julien Lepiller]

Le Sat, 21 Oct 2017 18:20:52 +0200,
julien@lepiller.eu a écrit :

> From: Tobias Geerinckx-Rice <me@tobias.gr>
> 
> [...]

Whoops, this is not in the patch series, it's a mistake. The rest is
correct.

[bug#28925] [PATCH 2/7] gnu: Update coq to 8.7.0.

[Marius Bakke]

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

julien@lepiller.eu writes:

> From: Julien Lepiller <julien@lepiller.eu>
>
> * gnu/packages/ocaml.scm (coq): Update to 8.7.0.

Please also mention the changes to inputs and build-system here.  The
same goes for the other patches.  This series LGTM apart from that.

[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 487 bytes --]

bug#28925: [PATCH 2/7] gnu: Update coq to 8.7.0.

[Julien Lepiller]

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

Le Sun, 22 Oct 2017 00:18:43 +0200,
Marius Bakke <mbakke@fastmail.com> a écrit :

> julien@lepiller.eu writes:
> 
> > From: Julien Lepiller <julien@lepiller.eu>
> >
> > * gnu/packages/ocaml.scm (coq): Update to 8.7.0.  
> 
> Please also mention the changes to inputs and build-system here.  The
> same goes for the other patches.  This series LGTM apart from that.

Thank you for the review, pushed as
07b4cd3a48022a472c90ec46f2e8b08d9cc8fc3e
- 6efc99967800183daa74ba2ebff6185dfcf1b33d.

[-- Attachment #2: Signature digitale OpenPGP --]
[-- Type: application/pgp-signature, Size: 833 bytes --]

[bug#28925] [PATCH 1/7] gnu: camlp5: install META file.

[Ludovic Courtès]

julien@lepiller.eu skribis:

> From: Julien Lepiller <julien@lepiller.eu>
>
> * gnu/packages/ocaml.scm (camlp5) [phases]: New install-meta phase.
> ---
>  gnu/packages/ocaml.scm | 7 ++++++-
>  1 file changed, 6 insertions(+), 1 deletion(-)
>
> diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
> index aa2f00667..40d42a5d4 100644
> --- a/gnu/packages/ocaml.scm
> +++ b/gnu/packages/ocaml.scm
> @@ -401,7 +401,12 @@ syntax of OCaml.")
>                    (lambda _
>                      (zero? (system* "make" "-j" (number->string
>                                                   (parallel-job-count))
> -                                    "world.opt")))))))
> +                                    "world.opt"))))
> +         ;; Required for findlib to find camlp5's libraries
> +         (add-after 'install 'install-meta
> +           (lambda* (#:key outputs #:allow-other-keys)
> +             (install-file "etc/META" (string-append (assoc-ref outputs "out")
> +                                                     "/lib/ocaml/camlp5/")))))))

Return #t, but otherwise LGTM!

Ludo'.