GNU bug report logs - #72730
[PATCH 0/2] coq: Update to 8.18.0.

Previous Next

Package: guix-patches;

Reported by: Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>

Date: Tue, 20 Aug 2024 10:30:02 UTC

Severity: normal

Tags: patch

Done: Z572 <zhengjunjie <at> iscas.ac.cn>

Bug is archived. No further changes may be made.

Full log


View this message in rfc822 format

From: help-debbugs <at> gnu.org (GNU bug Tracking System)
To: Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>
Subject: bug#72730: closed (Re: [bug#72730] [PATCH 2/2] gnu: coq: Update
 to 8.18.0.)
Date: Thu, 12 Sep 2024 06:33:01 +0000
[Message part 1 (text/plain, inline)]
Your bug report

#72730: [PATCH 0/2] coq: Update to 8.18.0.

which was filed against the guix-patches package, has been closed.

The explanation is attached below, along with your original report.
If you require more details, please reply to 72730 <at> debbugs.gnu.org.

-- 
72730: https://debbugs.gnu.org/cgi/bugreport.cgi?bug=72730
GNU Bug Tracking System
Contact help-debbugs <at> gnu.org with problems
[Message part 2 (message/rfc822, inline)]
From: Z572 <zhengjunjie <at> iscas.ac.cn>
To: Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>
Cc: 72730-done <at> debbugs.gnu.org, pukkamustard <pukkamustard <at> posteo.net>,
 Julien Lepiller <julien <at> lepiller.eu>
Subject: Re: [bug#72730] [PATCH 2/2] gnu: coq: Update to 8.18.0.
Date: Thu, 12 Sep 2024 14:32:29 +0800
[Message part 3 (text/plain, inline)]
Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz> writes:

> * gnu/packages/coq.scm (coq): Update to 8.18.0.
> (coq-bignums): Update to 9.0.0+coq8.18.
> (coq-equations): Update to 1.3-8.18.

i split to 3 patch. and make coq-bignums coq-equations use g-expression.

>
> Change-Id: I644a4538538a23d736fca2fab541c2cd2fb1f472
> ---
>  gnu/packages/coq.scm | 14 +++++++-------
>  1 file changed, 7 insertions(+), 7 deletions(-)
>
> diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
> index be95d16991..02d2600546 100644
> --- a/gnu/packages/coq.scm
> +++ b/gnu/packages/coq.scm
> @@ -56,7 +56,7 @@ (define-module (gnu packages coq)
>  (define-public coq
>    (package
>      (name "coq")
> -    (version "8.17.1")
> +    (version "8.18.0")
>      (source
>       (origin
>         (method git-fetch)
> @@ -66,7 +66,7 @@ (define-public coq
>         (file-name (git-file-name name version))
>         (sha256
>          (base32
> -         "0gg6hizq0i08lk741b579cbswhy6qvkh6inc3d3i5a2af98psq63"))))
> +         "1qy71gdr4s2l6847b4nwns6akib2f7l725zb01m7zc26n6mrrh1m"))))
>      (native-search-paths
>       (list (search-path-specification
>              (variable "COQPATH")
> @@ -445,16 +445,16 @@ (define-public coq-coquelicot
>  (define-public coq-bignums
>    (package
>      (name "coq-bignums")
> -    (version "8.16.0")
> +    (version "9.0.0+coq8.18")
>      (source (origin
>                (method git-fetch)
>                (uri (git-reference
>                       (url "https://github.com/coq/bignums")
> -                     (commit (string-append "V" version))))
> +                     (commit (string-append "v" version))))
>                (file-name (git-file-name name version))
>                (sha256
>                 (base32
> -                "07ndnm7pndmai3a2bkcmwjfjzfaqyq19c5an15hmhgmd0rdy4z8c"))))
> +                "1vw1a498fhyrpm884rlm3r4lw4mg4l6b9xj8w4y875sacg88kdxw"))))
>      (build-system gnu-build-system)
>      (native-inputs
>       (list ocaml coq))
> @@ -567,7 +567,7 @@ (define-public coq-autosubst
>  (define-public coq-equations
>    (package
>      (name "coq-equations")
> -    (version "1.3-8.17")
> +    (version "1.3-8.18")
>      (source (origin
>                (method git-fetch)
>                (uri (git-reference
> @@ -576,7 +576,7 @@ (define-public coq-equations
>                (file-name (git-file-name name version))
>                (sha256
>                 (base32
> -                "0g68h4c1ijpphixvl9wkd7sibds38v4236dpvvh194j5ii42vnn8"))))
> +                "1akxf2vafwyz6fi1djlc3g8mwxrjv0a99x4b08jwrbwxypv4xiph"))))
>      (build-system gnu-build-system)
>      (native-inputs
>       (list ocaml coq camlp5))

push, close.
[signature.asc (application/pgp-signature, inline)]
[Message part 5 (message/rfc822, inline)]
From: Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>
To: guix-patches <at> gnu.org
Cc: Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>
Subject: [PATCH 0/2] coq: Update to 8.18.0.
Date: Tue, 20 Aug 2024 12:28:55 +0200
This updates Coq to 8.18.0 and some Coq plugins to build on the newer
version.  Updated to this one as 8.17 is already showing its age, Coq
8.19 still breaks Why 3, so that's the reason for 8.18, Why 3 already
has some fixes for 8.19 so when released we can update to 8.19 (or 8.20
that is soon to be released).

Jean-Pierre De Jesus DIAZ (2):
  gnu: coq: Propagate ocaml-zarith.
  gnu: coq: Update to 8.18.0.

 gnu/packages/coq.scm | 29 ++++++++++++++---------------
 1 file changed, 14 insertions(+), 15 deletions(-)


base-commit: 91b69f154db218834de002dcd013a8f47170e684
-- 
2.45.2




This bug report was last modified 250 days ago.

Previous Next


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