unofficial mirror of guix-patches@gnu.org 
 help / color / mirror / Atom feed
* [bug#43325] [PATCH] gnu: Update coq and its dependents
@ 2020-09-11  7:30 Robin Green
  2020-09-13 14:43 ` Robin Green
  0 siblings, 1 reply; 3+ messages in thread
From: Robin Green @ 2020-09-11  7:30 UTC (permalink / raw)
  To: 43325; +Cc: Robin Green

* 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





^ permalink raw reply	[flat|nested] 3+ messages in thread

* [bug#43325] [PATCH] gnu: Update coq and its dependents
  2020-09-11  7:30 [bug#43325] [PATCH] gnu: Update coq and its dependents Robin Green
@ 2020-09-13 14:43 ` Robin Green
  2020-09-14  0:29   ` bug#43325: " Julien Lepiller
  0 siblings, 1 reply; 3+ messages in thread
From: Robin Green @ 2020-09-13 14:43 UTC (permalink / raw)
  To: 43325

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

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



[-- Attachment #2: 0001-gnu-Update-coq-and-its-dependents.patch --]
[-- Type: text/x-patch, Size: 6719 bytes --]

From a435d45d5777e0a9d0350bc4871d700190cd817b Mon Sep 17 00:00:00 2001
From: Robin Green <greenrd@greenrd.org>
Date: Sun, 13 Sep 2020 15:12:18 +0100
Subject: [PATCH] gnu: Update coq and its dependents

* 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 | 41 ++++++++++++++++++++++-------------------
 1 file changed, 22 insertions(+), 19 deletions(-)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 3573518763..44317efd1c 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,9 @@
        ("camlp5" ,camlp5)
        ("ocaml-num" ,ocaml-num)))
     (native-inputs
-     `(("ocaml-ounit" ,ocaml-ounit)))
+     `(("ocaml-ounit" ,ocaml-ounit)
+       ("rsync" ,rsync)
+       ("which" ,which)))
     (arguments
      `(#:phases
        (modify-phases %standard-phases
@@ -125,7 +128,7 @@
                ;; 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")
+               (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


^ permalink raw reply	[flat|nested] 3+ messages in thread

* bug#43325: [PATCH] gnu: Update coq and its dependents
  2020-09-13 14:43 ` Robin Green
@ 2020-09-14  0:29   ` Julien Lepiller
  0 siblings, 0 replies; 3+ messages in thread
From: Julien Lepiller @ 2020-09-14  0:29 UTC (permalink / raw)
  To: Robin Green; +Cc: 43325-done

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

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

Pushed as 1042d269a723360a02b19a2baafef1e24a3bfc73, thank you!




^ permalink raw reply	[flat|nested] 3+ messages in thread

end of thread, other threads:[~2020-09-14  0:31 UTC | newest]

Thread overview: 3+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2020-09-11  7:30 [bug#43325] [PATCH] gnu: Update coq and its dependents Robin Green
2020-09-13 14:43 ` Robin Green
2020-09-14  0:29   ` bug#43325: " Julien Lepiller

unofficial mirror of guix-patches@gnu.org 

This inbox may be cloned and mirrored by anyone:

	git clone --mirror https://yhetil.org/guix-patches/1 guix-patches/git/1.git

	# If you have public-inbox 1.1+ installed, you may
	# initialize and index your mirror using the following commands:
	public-inbox-init -V2 guix-patches guix-patches/ https://yhetil.org/guix-patches \
		guix-patches@gnu.org
	public-inbox-index guix-patches

Example config snippet for mirrors.
Newsgroup available over NNTP:
	nntp://news.yhetil.org/yhetil.gnu.guix.patches


AGPL code for this site: git clone https://public-inbox.org/public-inbox.git