* [bug#49423] [PATCH] gnu: coq: Update to 8.13.2.
@ 2021-07-05 22:06 Julien Lepiller
2021-07-21 14:07 ` Ludovic Courtès
` (2 more replies)
0 siblings, 3 replies; 4+ messages in thread
From: Julien Lepiller @ 2021-07-05 22:06 UTC (permalink / raw)
To: 49423
[-- Attachment #1: Type: text/plain, Size: 623 bytes --]
Hi guix!
this small series updates coq to the latest version. I had to update
zarith and a few dependencies (some of which cannot be updated
independently of coq), and fix the installation of lablgtk.
This version of coq uses dune, and I split the coq package into coq,
coq-ide-server (contains coqidetop) and coq-ide (contains the graphical
interface). This also simplifies the dependency graph for coq packages,
as they no longer need the graphical stack.
I tried building the documentation too, but it complains about missing
coq package, even if I added it to the inputs of coq-doc, so it's not
part of this series.
[-- Attachment #2: 0001-gnu-ocaml-zarith-Update-to-1.12.patch --]
[-- Type: text/x-patch, Size: 2026 bytes --]
From 73fc06926c86e8dad8bbb61f6a1728343fd2a487 Mon Sep 17 00:00:00 2001
From: Julien Lepiller <julien@lepiller.eu>
Date: Mon, 5 Jul 2021 17:31:10 +0200
Subject: [PATCH 1/4] gnu: ocaml-zarith: Update to 1.12.
* gnu/packages/ocaml.scm (ocaml-zarith): Update to 1.12.
---
gnu/packages/ocaml.scm | 13 ++++++++++---
1 file changed, 10 insertions(+), 3 deletions(-)
diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index cec6eb4f89..5f4ed3ae35 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -1428,7 +1428,7 @@ files in these formats.")
(define-public ocaml-zarith
(package
(name "ocaml-zarith")
- (version "1.9.1")
+ (version "1.12")
(source (origin
(method git-fetch)
(uri (git-reference
@@ -1437,7 +1437,7 @@ files in these formats.")
(file-name (git-file-name name version))
(sha256
(base32
- "0hv5ywz1q2cgn8apfz490clwk5hcynr937g2v8i13x2ax4bnv0lz"))))
+ "1jslm1rv1j0ya818yh23wf3bb6hz7qqj9pn5fwl45y9mqyqa01s9"))))
(build-system ocaml-build-system)
(native-inputs
`(("perl" ,perl)))
@@ -1448,7 +1448,14 @@ files in these formats.")
#:phases
(modify-phases %standard-phases
(replace 'configure
- (lambda _ (invoke "./configure"))))))
+ (lambda _ (invoke "./configure")))
+ (add-after 'install 'move-sublibs
+ (lambda* (#:key outputs #:allow-other-keys)
+ (let* ((out (assoc-ref outputs "out"))
+ (lib (string-append out "/lib/ocaml/site-lib")))
+ (mkdir-p (string-append lib "/stublibs"))
+ (rename-file (string-append lib "/zarith/dllzarith.so")
+ (string-append lib "/stublibs/dllzarith.so"))))))))
(home-page "https://forge.ocamlcore.org/projects/zarith/")
(synopsis "Implements arbitrary-precision integers")
(description "Implements arithmetic and logical operations over
--
2.32.0
[-- Attachment #3: 0002-gnu-lablgtk3-Install-with-version-information.patch --]
[-- Type: text/x-patch, Size: 1137 bytes --]
From 76a337769e67e84a32c5b85d80ab6bc160792aef Mon Sep 17 00:00:00 2001
From: Julien Lepiller <julien@lepiller.eu>
Date: Mon, 5 Jul 2021 17:52:03 +0200
Subject: [PATCH 2/4] gnu: lablgtk3: Install with version information.
This is required so recent versions of coq can check version
requirements.
* gnu/packages/ocaml.scm (lablgtk3)[arguments]: Ensure version is added
to the META file.
---
gnu/packages/ocaml.scm | 6 ++++++
1 file changed, 6 insertions(+)
diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index 5f4ed3ae35..4c8f04f29c 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -6902,6 +6902,12 @@ support for Mparser.")))
(for-each (lambda (file)
(chmod file #o644))
(find-files "." "."))
+ #t))
+ (add-before 'build 'set-version
+ (lambda _
+ (substitute* "dune-project"
+ (("\\(name lablgtk3\\)")
+ (string-append "(name lablgtk3)\n(version " ,version ")")))
#t)))))
(propagated-inputs
`(("ocaml-cairo2" ,ocaml-cairo2)))
--
2.32.0
[-- Attachment #4: 0003-gnu-coq-stdpp-Update-to-1.5.0.patch --]
[-- Type: text/x-patch, Size: 1111 bytes --]
From 8f374c9e8001db83a12ef6feee8404cbef4daaab Mon Sep 17 00:00:00 2001
From: Julien Lepiller <julien@lepiller.eu>
Date: Mon, 5 Jul 2021 23:41:16 +0200
Subject: [PATCH 3/4] gnu: coq-stdpp: Update to 1.5.0.
* gnu/packages/coq.scm (coq-stdpp): Update to 1.5.0.
---
gnu/packages/coq.scm | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index fa1f4078b8..a18eddeb0f 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -598,7 +598,7 @@ kernel.")
(define-public coq-stdpp
(package
(name "coq-stdpp")
- (version "1.4.0")
+ (version "1.5.0")
(synopsis "Alternative Coq standard library std++")
(source (origin
(method git-fetch)
@@ -608,7 +608,7 @@ kernel.")
(file-name (git-file-name name version))
(sha256
(base32
- "1m6c7ibwc99jd4cv14v3r327spnfvdf3x2mnq51f9rz99rffk68r"))))
+ "1ym0fy620imah89p8b6rii8clx2vmnwcrbwxl3630h24k42092nf"))))
(build-system gnu-build-system)
(inputs
`(("coq" ,coq)))
--
2.32.0
[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #5: 0004-gnu-coq-Update-to-8.13.2.patch --]
[-- Type: text/x-patch, Size: 11569 bytes --]
From 074a392bc2139309a39a06b03520af0573c844b1 Mon Sep 17 00:00:00 2001
From: Julien Lepiller <julien@lepiller.eu>
Date: Mon, 5 Jul 2021 21:32:33 +0200
Subject: [PATCH 4/4] gnu: coq: Update to 8.13.2.
* gnu/packages/coq.scm (coq): Update to 8.13.2.
(coq-ide-server, coq-ide): New packages.
(coq-gappa): Update to 1.4.6.
(coq-bignums): Update to 8.13.0.
(coq-interval): Update to 1.3.0.
(coq-equations): Update to 1.2.4.
---
gnu/packages/coq.scm | 147 ++++++++++++++++++-------------------------
1 file changed, 62 insertions(+), 85 deletions(-)
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index a18eddeb0f..4ad172c6b0 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -1,5 +1,5 @@
;;; GNU Guix --- Functional package management for GNU
-;;; Copyright © 2018 Julien Lepiller <julien@lepiller.eu>
+;;; Copyright © 2018-2021 Julien Lepiller <julien@lepiller.eu>
;;; Copyright © 2018, 2019 Tobias Geerinckx-Rice <me@tobias.gr>
;;; Copyright © 2019 Dan Frumin <dfrumin@cs.ru.nl>
;;; Copyright © 2020 Brett Gilio <brettg@gnu.org>
@@ -38,6 +38,7 @@
#:use-module (gnu packages python)
#:use-module (gnu packages rsync)
#:use-module (gnu packages texinfo)
+ #:use-module (guix build-system dune)
#:use-module (guix build-system gnu)
#:use-module (guix build-system ocaml)
#:use-module (guix download)
@@ -50,7 +51,7 @@
(define-public coq
(package
(name "coq")
- (version "8.11.2")
+ (version "8.13.2")
(source
(origin
(method git-fetch)
@@ -60,78 +61,24 @@
(file-name (git-file-name name version))
(sha256
(base32
- "1gia82dkmzqspw2w3s4gjyh39ghbmw4i41i4hyzc91g7mza17nbz"))))
+ "15r0cm3p9dlsxbg0lf05njjp1xi1y74vxvq6drxjykax67x95l8a"))))
(native-search-paths
(list (search-path-specification
(variable "COQPATH")
- (files (list "lib/coq/user-contrib")))))
- (build-system ocaml-build-system)
- (outputs '("out" "ide"))
+ (files (list "lib/coq/user-contrib")))
+ (search-path-specification
+ (variable "COQLIB")
+ (files (list "lib/ocaml/site-lib/coq"))
+ (separator #f))))
+ (build-system dune-build-system)
(inputs
- `(("lablgtk" ,lablgtk3)
- ("python" ,python-2)
- ("camlp5" ,camlp5)
- ("ocaml-num" ,ocaml-num)))
+ `(("gmp" ,gmp)
+ ("ocaml-zarith" ,ocaml-zarith)))
(native-inputs
- `(("ocaml-ounit" ,ocaml-ounit)
- ("rsync" ,rsync)
- ("which" ,which)))
+ `(("which" ,which)))
(arguments
- `(#:phases
- (modify-phases %standard-phases
- (add-after 'unpack 'make-git-checkout-writable
- (lambda _
- (for-each make-file-writable (find-files "."))
- #t))
- (replace 'configure
- (lambda* (#:key outputs #:allow-other-keys)
- (let* ((out (assoc-ref outputs "out"))
- (mandir (string-append out "/share/man"))
- (browser "icecat -remote \"OpenURL(%s,new-tab)\""))
- (invoke "./configure"
- "-prefix" out
- "-mandir" mandir
- "-browser" browser
- "-coqide" "opt"))))
- (replace 'build
- (lambda _
- (invoke "make"
- "-j" (number->string (parallel-job-count))
- "world")))
- (delete 'check)
- (add-after 'install 'remove-duplicate
- (lambda* (#:key outputs #:allow-other-keys)
- (let* ((out (assoc-ref outputs "out"))
- (bin (string-append out "/bin"))
- (coqtop (string-append bin "/coqtop"))
- (coqidetop (string-append bin "/coqidetop"))
- (coqtop.opt (string-append coqtop ".opt"))
- (coqidetop.opt (string-append coqidetop ".opt")))
- ;; These files are exact copies without `.opt` extension.
- ;; Removing these saves 35 MiB in the resulting package.
- ;; Unfortunately, completely deleting them breaks coqide.
- (delete-file coqtop.opt)
- (delete-file coqidetop.opt)
- (symlink coqtop coqtop.opt)
- (symlink coqidetop coqidetop.opt))
- #t))
- (add-after 'install 'install-ide
- (lambda* (#:key outputs #:allow-other-keys)
- (let ((out (assoc-ref outputs "out"))
- (ide (assoc-ref outputs "ide")))
- (mkdir-p (string-append ide "/bin"))
- (rename-file (string-append out "/bin/coqide")
- (string-append ide "/bin/coqide")))
- #t))
- (add-after 'install 'check
- (lambda _
- (with-directory-excursion "test-suite"
- ;; These two 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 "misc/printers.sh")
- (invoke "make")))))))
+ `(#:package "coq"
+ #:test-target "test-suite"))
(home-page "https://coq.inria.fr")
(synopsis "Proof assistant for higher-order logic")
(description
@@ -142,6 +89,31 @@ It is developed using Objective Caml and Camlp5.")
;; Some of the documentation is distributed under opl1.0+.
(license (list license:lgpl2.1 license:opl1.0+))))
+(define-public coq-ide-server
+ (package
+ (inherit coq)
+ (name "coq-ide-server")
+ (arguments
+ `(#:tests? #f
+ #:package "coqide-server"))
+ (inputs
+ `(("coq" ,coq)
+ ("gmp" ,gmp)
+ ("ocaml-zarith" ,ocaml-zarith)))))
+
+(define-public coq-ide
+ (package
+ (inherit coq)
+ (name "coq-ide")
+ (arguments
+ `(#:tests? #f
+ #:package "coqide"))
+ (propagated-inputs
+ `(("coq" ,coq)
+ ("coq-ide-server" ,coq-ide-server)))
+ (inputs
+ `(("lablgtk3" ,lablgtk3)))))
+
(define-public proof-general
;; The latest release is from 2016 and there has been more than 450 commits
;; since then.
@@ -274,7 +246,7 @@ inside Coq.")
(define-public coq-gappa
(package
(name "coq-gappa")
- (version "1.4.4")
+ (version "1.4.6")
(source
(origin
(method git-fetch)
@@ -284,7 +256,7 @@ inside Coq.")
(file-name (git-file-name name version))
(sha256
(base32
- "0f3g3wjkvfkm961l4jpckhsqd43jnvm7f5qqk78qc32zh1fg339n"))))
+ "0492i0ksrz6dnc1d57jzsbmdlb9fp9hrh9ib5v8j0yqxpyi0x8f4"))))
(build-system gnu-build-system)
(native-inputs
`(("autoconf" ,autoconf)
@@ -298,13 +270,14 @@ inside Coq.")
(inputs
`(("gmp" ,gmp)
("mpfr" ,mpfr)
+ ("ocaml-zarith" ,ocaml-zarith)
("boost" ,boost)))
(propagated-inputs
`(("coq-flocq" ,coq-flocq)))
(arguments
`(#:configure-flags
- (list (string-append "--libdir=" (assoc-ref %outputs "out")
- "/lib/coq/user-contrib/Gappa"))
+ (list (string-append "COQUSERCONTRIB=" (assoc-ref %outputs "out")
+ "/lib/coq/user-contrib"))
#:phases
(modify-phases %standard-phases
(add-before 'configure 'fix-remake
@@ -334,7 +307,7 @@ assistant.")
(define-public coq-mathcomp
(package
(name "coq-mathcomp")
- (version "1.11.0")
+ (version "1.12.0")
(source
(origin
(method git-fetch)
@@ -343,7 +316,7 @@ assistant.")
(commit (string-append "mathcomp-" version))))
(file-name (git-file-name name version))
(sha256
- (base32 "1axywpa1jcpnidd86irpd1gdbbg2sfbwc652675xisq5wnmfmf6f"))))
+ (base32 "12cgrmzlcjnp9kv9zxsk34fgf0qfa35jdb23cbf13kmg8dyfi3h5"))))
(build-system gnu-build-system)
(native-inputs
`(("ocaml" ,ocaml)
@@ -429,7 +402,7 @@ theorems between the two libraries.")
(define-public coq-bignums
(package
(name "coq-bignums")
- (version "8.11.0")
+ (version "8.13.0")
(source (origin
(method git-fetch)
(uri (git-reference
@@ -438,13 +411,14 @@ theorems between the two libraries.")
(file-name (git-file-name name version))
(sha256
(base32
- "1xcd7c7qlvs0narfba6px34zq0mz8rffnhxw0kzhhg6i4iw115dp"))))
+ "1n66i7hd9222b2ks606mak7m4f0dgy02xgygjskmmav6h7g2sx7y"))))
(build-system gnu-build-system)
(native-inputs
`(("ocaml" ,ocaml)
("coq" ,coq)))
(inputs
- `(("camlp5" ,camlp5)))
+ `(("camlp5" ,camlp5)
+ ("ocaml-zarith" ,ocaml-zarith)))
(arguments
`(#:tests? #f ; No test target.
#:make-flags
@@ -462,7 +436,7 @@ provides BigN, BigZ, BigQ that used to be part of Coq standard library.")
(define-public coq-interval
(package
(name "coq-interval")
- (version "4.0.0")
+ (version "4.3.0")
(source
(origin
(method git-fetch)
@@ -472,7 +446,7 @@ provides BigN, BigZ, BigQ that used to be part of Coq standard library.")
(file-name (git-file-name name version))
(sha256
(base32
- "01iz6qmnsm6b9s1vmdjs79vjx9xgwzn5rwyjp6bvs8hg3zlmhpip"))))
+ "1jqvd17czhliscf40idhnxgrha620039ilrdyfahn71dg2jmzqnm"))))
(build-system gnu-build-system)
(native-inputs
`(("autoconf" ,autoconf)
@@ -484,11 +458,12 @@ provides BigN, BigZ, BigQ that used to be part of Coq standard library.")
`(("flocq" ,coq-flocq)
("bignums" ,coq-bignums)
("coquelicot" ,coq-coquelicot)
- ("mathcomp" ,coq-mathcomp)))
+ ("mathcomp" ,coq-mathcomp)
+ ("ocaml-zarith" ,ocaml-zarith)))
(arguments
`(#:configure-flags
- (list (string-append "--libdir=" (assoc-ref %outputs "out")
- "/lib/coq/user-contrib/Gappa"))
+ (list (string-append "COQUSERCONTRIB=" (assoc-ref %outputs "out")
+ "/lib/coq/user-contrib"))
#:phases
(modify-phases %standard-phases
(add-before 'configure 'fix-remake
@@ -558,21 +533,23 @@ uses Ltac to synthesize the substitution operation.")
(define-public coq-equations
(package
(name "coq-equations")
- (version "1.2.3")
+ (version "1.2.4")
(source (origin
(method git-fetch)
(uri (git-reference
(url "https://github.com/mattam82/Coq-Equations")
- (commit (string-append "v" version "-8.11"))))
+ (commit (string-append "v" version "-8.13"))))
(file-name (git-file-name name version))
(sha256
(base32
- "1srxz1rws8jsh7402g2x2vcqgjbbsr64dxxj5d2zs48pmhb20csf"))))
+ "0i014lshsdflzw6h0qxra9d2f0q82vffxv2f29awbb9ad0p4rq4q"))))
(build-system gnu-build-system)
(native-inputs
`(("ocaml" ,ocaml)
("coq" ,coq)
("camlp5" ,camlp5)))
+ (inputs
+ `(("ocaml-zarith" ,ocaml-zarith)))
(arguments
`(#:test-target "test-suite"
#:phases
--
2.32.0
^ permalink raw reply related [flat|nested] 4+ messages in thread
* [bug#49423] [PATCH] gnu: coq: Update to 8.13.2.
2021-07-05 22:06 [bug#49423] [PATCH] gnu: coq: Update to 8.13.2 Julien Lepiller
@ 2021-07-21 14:07 ` Ludovic Courtès
2021-07-24 13:17 ` Xinglu Chen
2021-07-31 21:07 ` bug#49423: " Julien Lepiller
2 siblings, 0 replies; 4+ messages in thread
From: Ludovic Courtès @ 2021-07-21 14:07 UTC (permalink / raw)
To: Julien Lepiller; +Cc: 49423
Hi,
Julien Lepiller <julien@lepiller.eu> skribis:
> this small series updates coq to the latest version. I had to update
> zarith and a few dependencies (some of which cannot be updated
> independently of coq), and fix the installation of lablgtk.
I haven’t tested it but the whole series LGTM!
Thanks,
Ludo’.
^ permalink raw reply [flat|nested] 4+ messages in thread
* [bug#49423] [PATCH] gnu: coq: Update to 8.13.2.
2021-07-05 22:06 [bug#49423] [PATCH] gnu: coq: Update to 8.13.2 Julien Lepiller
2021-07-21 14:07 ` Ludovic Courtès
@ 2021-07-24 13:17 ` Xinglu Chen
2021-07-31 21:07 ` bug#49423: " Julien Lepiller
2 siblings, 0 replies; 4+ messages in thread
From: Xinglu Chen @ 2021-07-24 13:17 UTC (permalink / raw)
To: Julien Lepiller, 49423
[-- Attachment #1: Type: text/plain, Size: 4136 bytes --]
On Tue, Jul 06 2021, Julien Lepiller wrote:
> Hi guix!
>
> this small series updates coq to the latest version. I had to update
> zarith and a few dependencies (some of which cannot be updated
> independently of coq), and fix the installation of lablgtk.
>
> This version of coq uses dune, and I split the coq package into coq,
> coq-ide-server (contains coqidetop) and coq-ide (contains the graphical
> interface). This also simplifies the dependency graph for coq packages,
> as they no longer need the graphical stack.
>
> I tried building the documentation too, but it complains about missing
> coq package, even if I added it to the inputs of coq-doc, so it's not
> part of this series.
> From 73fc06926c86e8dad8bbb61f6a1728343fd2a487 Mon Sep 17 00:00:00 2001
> From: Julien Lepiller <julien@lepiller.eu>
> Date: Mon, 5 Jul 2021 17:31:10 +0200
> Subject: [PATCH 1/4] gnu: ocaml-zarith: Update to 1.12.
>
> * gnu/packages/ocaml.scm (ocaml-zarith): Update to 1.12.
> ---
> gnu/packages/ocaml.scm | 13 ++++++++++---
> 1 file changed, 10 insertions(+), 3 deletions(-)
>
> diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
> index cec6eb4f89..5f4ed3ae35 100644
> --- a/gnu/packages/ocaml.scm
> +++ b/gnu/packages/ocaml.scm
> @@ -1428,7 +1428,7 @@ files in these formats.")
> (define-public ocaml-zarith
> (package
> (name "ocaml-zarith")
> - (version "1.9.1")
> + (version "1.12")
> (source (origin
> (method git-fetch)
> (uri (git-reference
> @@ -1437,7 +1437,7 @@ files in these formats.")
> (file-name (git-file-name name version))
> (sha256
> (base32
> - "0hv5ywz1q2cgn8apfz490clwk5hcynr937g2v8i13x2ax4bnv0lz"))))
> + "1jslm1rv1j0ya818yh23wf3bb6hz7qqj9pn5fwl45y9mqyqa01s9"))))
> (build-system ocaml-build-system)
> (native-inputs
> `(("perl" ,perl)))
> @@ -1448,7 +1448,14 @@ files in these formats.")
> #:phases
> (modify-phases %standard-phases
> (replace 'configure
> - (lambda _ (invoke "./configure"))))))
> + (lambda _ (invoke "./configure")))
> + (add-after 'install 'move-sublibs
> + (lambda* (#:key outputs #:allow-other-keys)
> + (let* ((out (assoc-ref outputs "out"))
> + (lib (string-append out "/lib/ocaml/site-lib")))
> + (mkdir-p (string-append lib "/stublibs"))
> + (rename-file (string-append lib "/zarith/dllzarith.so")
> + (string-append lib "/stublibs/dllzarith.so"))))))))
> (home-page "https://forge.ocamlcore.org/projects/zarith/")
> (synopsis "Implements arbitrary-precision integers")
> (description "Implements arithmetic and logical operations over
> --
> 2.32.0
>
> From 76a337769e67e84a32c5b85d80ab6bc160792aef Mon Sep 17 00:00:00 2001
> From: Julien Lepiller <julien@lepiller.eu>
> Date: Mon, 5 Jul 2021 17:52:03 +0200
> Subject: [PATCH 2/4] gnu: lablgtk3: Install with version information.
>
> This is required so recent versions of coq can check version
> requirements.
>
> * gnu/packages/ocaml.scm (lablgtk3)[arguments]: Ensure version is added
> to the META file.
> ---
> gnu/packages/ocaml.scm | 6 ++++++
> 1 file changed, 6 insertions(+)
>
> diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
> index 5f4ed3ae35..4c8f04f29c 100644
> --- a/gnu/packages/ocaml.scm
> +++ b/gnu/packages/ocaml.scm
> @@ -6902,6 +6902,12 @@ support for Mparser.")))
> (for-each (lambda (file)
> (chmod file #o644))
> (find-files "." "."))
> + #t))
Nit: no need to add a trailing #t.
> + (add-before 'build 'set-version
> + (lambda _
> + (substitute* "dune-project"
> + (("\\(name lablgtk3\\)")
> + (string-append "(name lablgtk3)\n(version " ,version ")")))
> #t)))))
Likewise.
Otherwise, looks good; everything builds fine. :)
[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 861 bytes --]
^ permalink raw reply [flat|nested] 4+ messages in thread
* bug#49423: [PATCH] gnu: coq: Update to 8.13.2.
2021-07-05 22:06 [bug#49423] [PATCH] gnu: coq: Update to 8.13.2 Julien Lepiller
2021-07-21 14:07 ` Ludovic Courtès
2021-07-24 13:17 ` Xinglu Chen
@ 2021-07-31 21:07 ` Julien Lepiller
2 siblings, 0 replies; 4+ messages in thread
From: Julien Lepiller @ 2021-07-31 21:07 UTC (permalink / raw)
To: 49423-done
Le Tue, 6 Jul 2021 00:06:40 +0200,
Julien Lepiller <julien@lepiller.eu> a écrit :
> Hi guix!
>
> this small series updates coq to the latest version. I had to update
> zarith and a few dependencies (some of which cannot be updated
> independently of coq), and fix the installation of lablgtk.
>
> This version of coq uses dune, and I split the coq package into coq,
> coq-ide-server (contains coqidetop) and coq-ide (contains the
> graphical interface). This also simplifies the dependency graph for
> coq packages, as they no longer need the graphical stack.
>
> I tried building the documentation too, but it complains about missing
> coq package, even if I added it to the inputs of coq-doc, so it's not
> part of this series.
Pushed to master as 96707d5a309d083b1a9bf1f0c8fc1251cf203337 to
e38b4d5ceb344c9707917a7d32df50d0ced082b5, thanks!
^ permalink raw reply [flat|nested] 4+ messages in thread
end of thread, other threads:[~2021-07-31 21:08 UTC | newest]
Thread overview: 4+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2021-07-05 22:06 [bug#49423] [PATCH] gnu: coq: Update to 8.13.2 Julien Lepiller
2021-07-21 14:07 ` Ludovic Courtès
2021-07-24 13:17 ` Xinglu Chen
2021-07-31 21:07 ` bug#49423: " Julien Lepiller
Code repositories for project(s) associated with this public inbox
https://git.savannah.gnu.org/cgit/guix.git
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).