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

Previous Next

Full log

View this message in rfc822 format

From: help-debbugs <at> gnu.org (GNU bug Tracking System)
To: Z572 <zhengjunjie <at> iscas.ac.cn>
Cc: tracker <at> debbugs.gnu.org
Subject: bug#72730: closed ([PATCH 0/2] coq: Update to 8.18.0.)
Date: Thu, 12 Sep 2024 06:33:01 +0000

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

Your message dated Thu, 12 Sep 2024 14:32:29 +0800
with message-id <87wmjhcrgi.fsf <at> iscas.ac.cn>
and subject line Re: [bug#72730] [PATCH 2/2] gnu: coq: Update to 8.18.0.
has caused the debbugs.gnu.org bug report #72730,
regarding [PATCH 0/2] coq: Update to 8.18.0.
to be marked as done.

(If you believe you have received this mail in error, please contact
help-debbugs <at> 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: 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

[Message part 3 (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 4 (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)]

Previous Next

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