GNU bug report logs - #43325
[PATCH] gnu: Update coq and its dependents

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 43325 in the body.
You can then email your comments to 43325 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: Robin Green <greenrd <at> greenrd.org>
To: guix-patches <at> gnu.org
Cc: Robin Green <greenrd <at> greenrd.org>
Subject: [PATCH] gnu: Update coq and its dependents
Date: Fri, 11 Sep 2020 08:30:27 +0100

* gnu/packages/coq.scm (coq): Update to 8.11.2
(coq-flocq): Update to 3.3.1
(coq-gappa): Update to 1.4.4
(coq-mathcomp): Update to 1.11.0
(coq-coquelicot): Update to 3.1.0
(coq-bignums): Update to 8.11.0
(coq-interval): Update to 4.0.0
(coq-equations): Update to 1.2.3
---
 gnu/packages/coq.scm | 45 +++++++++++++++++++++++---------------------
 1 file changed, 24 insertions(+), 21 deletions(-)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 3573518763..2d8dca8d46 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -34,6 +34,7 @@
   #:use-module (gnu packages ocaml)
   #:use-module (gnu packages perl)
   #:use-module (gnu packages python)
+  #:use-module (gnu packages rsync)
   #:use-module (gnu packages texinfo)
   #:use-module (guix build-system gnu)
   #:use-module (guix build-system ocaml)
@@ -47,7 +48,7 @@
 (define-public coq
   (package
     (name "coq")
-    (version "8.10.2")
+    (version "8.11.2")
     (source
      (origin
        (method git-fetch)
@@ -57,7 +58,7 @@
        (file-name (git-file-name name version))
        (sha256
         (base32
-         "0ji2rzd70b3hcwfw97qk7rv3m2977ylqnq82l1555dp3njr8nm3q"))))
+         "1gia82dkmzqspw2w3s4gjyh39ghbmw4i41i4hyzc91g7mza17nbz"))))
     (native-search-paths
      (list (search-path-specification
             (variable "COQPATH")
@@ -70,7 +71,8 @@
        ("camlp5" ,camlp5)
        ("ocaml-num" ,ocaml-num)))
     (native-inputs
-     `(("ocaml-ounit" ,ocaml-ounit)))
+     `(("ocaml-ounit" ,ocaml-ounit)
+       ("rsync" ,rsync)))
     (arguments
      `(#:phases
        (modify-phases %standard-phases
@@ -121,11 +123,12 @@
          (add-after 'install 'check
            (lambda _
              (with-directory-excursion "test-suite"
-               ;; These two tests fail.
+               ;; These three tests fail.
                ;; Fails because the output is not formatted as expected.
                (delete-file-recursively "coq-makefile/timing")
-               ;; Fails because we didn't build coqtop.byte.
-               (delete-file-recursively "coq-makefile/findlib-package")
+               ;; Fail because we didn't build coqtop.byte.
+               (delete-file-recursively "coq-makefile/findlib-package-unpacked")
+               (delete-file "misc/printers.sh")
                (invoke "make")))))))
     (home-page "https://coq.inria.fr")
     (synopsis "Proof assistant for higher-order logic")
@@ -215,7 +218,7 @@ provers.")
 (define-public coq-flocq
   (package
     (name "coq-flocq")
-    (version "3.2.0")
+    (version "3.3.1")
     (source
      (origin
        (method git-fetch)
@@ -225,7 +228,7 @@ provers.")
        (file-name (git-file-name name version))
        (sha256
         (base32
-         "15bi36x7zj0glsb3s2gwqd4wswhfzh36rbp7imbyff53a7nna95l"))))
+         "01gdykva0lcw6y3dm8j0djxayb87szfg9vn0mxd6z3pks644misl"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("autoconf" ,autoconf)
@@ -272,7 +275,7 @@ inside Coq.")
 (define-public coq-gappa
   (package
     (name "coq-gappa")
-    (version "1.4.2")
+    (version "1.4.4")
     (source
      (origin
        (method git-fetch)
@@ -282,7 +285,7 @@ inside Coq.")
        (file-name (git-file-name name version))
        (sha256
         (base32
-         "0r7jwp5xssdfzivs2flp7mzrscqhgl63mryhhf1cvndpgzqwfk2f"))))
+         "0f3g3wjkvfkm961l4jpckhsqd43jnvm7f5qqk78qc32zh1fg339n"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("autoconf" ,autoconf)
@@ -332,7 +335,7 @@ assistant.")
 (define-public coq-mathcomp
   (package
     (name "coq-mathcomp")
-    (version "1.10.0")
+    (version "1.11.0")
     (source
      (origin
        (method git-fetch)
@@ -341,7 +344,7 @@ assistant.")
              (commit (string-append "mathcomp-" version))))
        (file-name (git-file-name name version))
        (sha256
-        (base32 "1h5h1c2025r1ms5qryvwy6pikxmpmmjav6yl127xpzmqdi6w732d"))))
+        (base32 "1axywpa1jcpnidd86irpd1gdbbg2sfbwc652675xisq5wnmfmf6f"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("ocaml" ,ocaml)
@@ -374,7 +377,7 @@ part of the distribution.")
 (define-public coq-coquelicot
   (package
     (name "coq-coquelicot")
-    (version "3.0.3")
+    (version "3.1.0")
     (source
      (origin
        (method git-fetch)
@@ -384,7 +387,7 @@ part of the distribution.")
        (file-name (git-file-name name version))
        (sha256
         (base32
-         "0m5wbr2s8lnf8b7cfwv15hyzsmbcaz6hgdn7aazcrkxnwr87vgkp"))))
+         "0mz3pxan1237fr5fi79c66y7b9z7bmi0sc45kwrmkczsjm5462jm"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("autoconf" ,autoconf)
@@ -427,7 +430,7 @@ theorems between the two libraries.")
 (define-public coq-bignums
   (package
     (name "coq-bignums")
-    (version "8.10.0")
+    (version "8.11.0")
     (source (origin
               (method git-fetch)
               (uri (git-reference
@@ -436,7 +439,7 @@ theorems between the two libraries.")
               (file-name (git-file-name name version))
               (sha256
                (base32
-                "0bpb4flckn4nqxbs3wjiznyx1k7r8k93qdigp3qwmikp2lxvcbw5"))))
+                "1xcd7c7qlvs0narfba6px34zq0mz8rffnhxw0kzhhg6i4iw115dp"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("ocaml" ,ocaml)
@@ -460,7 +463,7 @@ provides BigN, BigZ, BigQ that used to be part of Coq standard library.")
 (define-public coq-interval
   (package
     (name "coq-interval")
-    (version "3.4.1")
+    (version "4.0.0")
     (source
      (origin
        (method git-fetch)
@@ -470,7 +473,7 @@ provides BigN, BigZ, BigQ that used to be part of Coq standard library.")
        (file-name (git-file-name name version))
        (sha256
         (base32
-         "03q3dfqi3r3f7aji5s06ig4aav9ajcwswwdzi5lrgr69z0m487k4"))))
+         "01iz6qmnsm6b9s1vmdjs79vjx9xgwzn5rwyjp6bvs8hg3zlmhpip"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("autoconf" ,autoconf)
@@ -556,16 +559,16 @@ uses Ltac to synthesize the substitution operation.")
 (define-public coq-equations
   (package
     (name "coq-equations")
-    (version "1.2.1")
+    (version "1.2.3")
     (source (origin
               (method git-fetch)
               (uri (git-reference
                     (url "https://github.com/mattam82/Coq-Equations")
-                    (commit (string-append "v" version "-8.10-2"))))
+                    (commit (string-append "v" version "-8.11"))))
               (file-name (git-file-name name version))
               (sha256
                (base32
-                "0j3z4l5nrbyi9zbbyqkc6kassjanwld2188mwmrbqspaypm2ys68"))))
+                "1srxz1rws8jsh7402g2x2vcqgjbbsr64dxxj5d2zs48pmhb20csf"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("ocaml"  ,ocaml)
-- 
2.28.0

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

From: Robin Green <greenrd <at> greenrd.org>
To: 43325 <at> debbugs.gnu.org
Subject: Re: [PATCH] gnu: Update coq and its dependents
Date: Sun, 13 Sep 2020 15:43:28 +0100

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

Updated patch, fixing a test that I mistakenly removed in the previous 
version.

[0001-gnu-Update-coq-and-its-dependents.patch (text/x-patch, attachment)]

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

From: Julien Lepiller <julien <at> lepiller.eu>
To: Robin Green <greenrd <at> greenrd.org>
Cc: 43325-done <at> debbugs.gnu.org
Subject: Re: [bug#43325] [PATCH] gnu: Update coq and its dependents
Date: Mon, 14 Sep 2020 02:29:43 +0200

Le Sun, 13 Sep 2020 15:43:28 +0100,
Robin Green <greenrd <at> greenrd.org> a écrit :

> Updated patch, fixing a test that I mistakenly removed in the
> previous version.
> 
> 

Pushed as 1042d269a723360a02b19a2baafef1e24a3bfc73, thank you!

Previous Next

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