GNU bug report logs - #52164
[PATCH] gnu: coq: Update to 8.14.0.

Please note: This is a static page, with minimal formatting, updated once a day.
Click here to see this page with the latest information and nicer formatting.

Package: guix-patches; Reported by: Julien Lepiller <julien@HIDDEN>; Keywords: patch; dated Sun, 28 Nov 2021 16:45:02 UTC; Maintainer for guix-patches is guix-patches@HIDDEN.

Message received at 52164 <at> debbugs.gnu.org:


Received: (at 52164) by debbugs.gnu.org; 29 Nov 2021 14:14:05 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Mon Nov 29 09:14:05 2021
Received: from localhost ([127.0.0.1]:37534 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1mrhPx-0003ku-5T
	for submit <at> debbugs.gnu.org; Mon, 29 Nov 2021 09:14:05 -0500
Received: from mail-il1-f179.google.com ([209.85.166.179]:33385)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <zimon.toutoune@HIDDEN>) id 1mrhPw-0003jv-3I
 for 52164 <at> debbugs.gnu.org; Mon, 29 Nov 2021 09:14:04 -0500
Received: by mail-il1-f179.google.com with SMTP id i6so17581926ila.0
 for <52164 <at> debbugs.gnu.org>; Mon, 29 Nov 2021 06:14:04 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112;
 h=mime-version:references:in-reply-to:from:date:message-id:subject:to
 :cc:content-transfer-encoding;
 bh=jHOgdM7kV4VGdRpYEV+2JmFyx2pLo8nKKHSeQu9fr38=;
 b=ZRP8pXZ28haBfaieY36pjOu0/cZP52zix6DMI2Q/5U+gdCgnVjBLBkRdkM9R4+0ESu
 b9fa7oi96FEeOZ9usDH5FT3PgWUnoTAXdz3ZJ/zmDj1GP4VPEp0sDkKEleBAMyqJhqo1
 41L+hvkBzV6sMRC7NiCGqfsgj9OaJoxXCI6O2cI4Z4386E3VyaxVScEsEb8o0L/AjcMO
 iNFQn8NFQXuBKvTEU2hRNqGqQtrzbZ+9D9RuA2Xjt+Fp/VDC/9dX9+4NsJYe0+9Y0c9U
 l2pt5B087edjy0PquzYVUElI1m9R+PfRHiM+a0dV5KDuk2PVUl5DO3zI5Xnalzpq411V
 wb5A==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
 d=1e100.net; s=20210112;
 h=x-gm-message-state:mime-version:references:in-reply-to:from:date
 :message-id:subject:to:cc:content-transfer-encoding;
 bh=jHOgdM7kV4VGdRpYEV+2JmFyx2pLo8nKKHSeQu9fr38=;
 b=sEnTvPK5eLo/idRX+94EtBfUKu/xY8OE6nYIdx4B8Bo8ytyVOJZ9rTLhHlqkhlxutC
 OhAqZSF1nKP4xjffIjW6BF66KxnqxgPRdFpfIOTpCFB+vvjSlPtUX+7SxfwXlmYn02R6
 Ea6ZmJnlUisyhriptKD33QBvIq551+rkor/Vxz3M8mOntZLFfIVOg0heT1YF6JsFWTy+
 P1mteOohqKJX28ZbewY1/cXfEQ84ZgqS0ZHpDPQfPhy6pCGefqq16L5pGP2U+5d+60kn
 Fhb4j/fGV+dizBQfjIzSYlp+fjYjfHUgON1NL4DzNaZBwZc+LeVA0zJfnmgxhZ9wyECV
 KPlg==
X-Gm-Message-State: AOAM531KAslTtGAKlI0mb0+W+Toeefpvc5VgzBzsbD4iD3VcFjD+JKMt
 XKzn0MlJYr/kR+jPlAS+V6nB9SYxH9j4udjNNBOMSHnO
X-Google-Smtp-Source: ABdhPJwFoGSIKrBME1XgA3ZwZ8YopzcaRzQbncm4EjevUlsfkMUQam5zyqBS7+Z1P3cxdvLMYUzZkIhgWbLosWPqWJU=
X-Received: by 2002:a05:6e02:1c2e:: with SMTP id
 m14mr57793438ilh.172.1638195238654; 
 Mon, 29 Nov 2021 06:13:58 -0800 (PST)
MIME-Version: 1.0
References: <20211128174408.747bccba@HIDDEN>
 <d62a5a234b89db4331c5bda48efa725fea18e97a.1638120398.git.julien@HIDDEN>
 <8635nfl2m6.fsf_-_@HIDDEN>
 <592223CF-588B-44EF-A35F-9E9FDB3E4865@HIDDEN>
 <CAJ3okZ23f-Vsm2fSJobjt3zLn+Wfy3YshfzKw4FtSLvQ2-YCzw@HIDDEN>
 <89F34741-9EFC-4C19-8167-3B990D90533F@HIDDEN>
In-Reply-To: <89F34741-9EFC-4C19-8167-3B990D90533F@HIDDEN>
From: zimoun <zimon.toutoune@HIDDEN>
Date: Mon, 29 Nov 2021 15:13:47 +0100
Message-ID: <CAJ3okZ31+VdRSe=z4nBcCQk7NXuwozK82Jnd2H-Nbk5p_-E=sg@HIDDEN>
Subject: Re: bug#52164: [PATCH] gnu: coq: Update to 8.14.0.
To: Julien Lepiller <julien@HIDDEN>
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
X-Spam-Score: 0.0 (/)
X-Debbugs-Envelope-To: 52164
Cc: 52164 <at> debbugs.gnu.org
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -1.0 (-)

Re,

On Mon, 29 Nov 2021 at 14:39, Julien Lepiller <julien@HIDDEN> wrote:

> I've always updated dependents first whenever possible (without breaking =
anything), then the compiler, then the rest that needs the new compiler. Ho=
wever, I've always been careful not to introduce breakage with a commit, ev=
en if it's inside a series. I think that's the policiy, but I'm not sure if=
 it overrides the one-change per commit policy.

Me neither. :-)
Anyway, all LGTM except wrong commit message for coq-semantics.

Cheers,
simon




Information forwarded to guix-patches@HIDDEN:
bug#52164; Package guix-patches. Full text available.

Message received at 52164 <at> debbugs.gnu.org:


Received: (at 52164) by debbugs.gnu.org; 29 Nov 2021 13:39:42 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Mon Nov 29 08:39:42 2021
Received: from localhost ([127.0.0.1]:37427 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1mrgsf-0002l5-Rs
	for submit <at> debbugs.gnu.org; Mon, 29 Nov 2021 08:39:42 -0500
Received: from lepiller.eu ([89.234.186.109]:42302)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <julien@HIDDEN>) id 1mrgsd-0002ks-HR
 for 52164 <at> debbugs.gnu.org; Mon, 29 Nov 2021 08:39:40 -0500
Received: from lepiller.eu (localhost [127.0.0.1])
 by lepiller.eu (OpenSMTPD) with ESMTP id 37ce504a;
 Mon, 29 Nov 2021 13:39:36 +0000 (UTC)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed; d=lepiller.eu; h=date:from
 :to:cc:subject:in-reply-to:references:message-id:mime-version
 :content-type:content-transfer-encoding; s=dkim; bh=cYTgx/It9svd
 g9CYMuhbKXtvZEmawTgENAOTtVWWYb0=; b=N5UTMsMGzvDRdiBxRkExWdLyDvjK
 gjEL1Dm/QYuuKEcZPg50rQ/OHr640HUGeMgIHejOXW7gPhcej8j+jeIyzl5d0k9m
 TCBUw+V4F/b+m7xhErtwX/OKg6bNzjOWiDgiv8HjNDJM8U+DNSFrtvSD9dDbKIL2
 xquvApPV7IrX+BB/+MZlqwe/en1b2yDpa+ryf1oGb7+va2zW+WaeHBn4SutIX1xO
 Ju61NRXLH3CvyvzCBwBITGbGhY9gxVK9CYrYZ/EZn+LTrDF7QY9Lr7053B4hp/lv
 dwse0I6Skof0Rbi+6P0PNayk2jJHwrdIhO+pbkVHUY9cabrpTiypan49fw==
Received: by lepiller.eu (OpenSMTPD) with ESMTPSA id c2415a3d
 (TLSv1.3:AEAD-AES256-GCM-SHA384:256:NO); 
 Mon, 29 Nov 2021 13:39:35 +0000 (UTC)
Date: Mon, 29 Nov 2021 08:39:23 -0500
From: Julien Lepiller <julien@HIDDEN>
To: zimoun <zimon.toutoune@HIDDEN>
Subject: Re: bug#52164: [PATCH] gnu: coq: Update to 8.14.0.
User-Agent: K-9 Mail for Android
In-Reply-To: <CAJ3okZ23f-Vsm2fSJobjt3zLn+Wfy3YshfzKw4FtSLvQ2-YCzw@HIDDEN>
References: <20211128174408.747bccba@HIDDEN>
 <d62a5a234b89db4331c5bda48efa725fea18e97a.1638120398.git.julien@HIDDEN>
 <8635nfl2m6.fsf_-_@HIDDEN>
 <592223CF-588B-44EF-A35F-9E9FDB3E4865@HIDDEN>
 <CAJ3okZ23f-Vsm2fSJobjt3zLn+Wfy3YshfzKw4FtSLvQ2-YCzw@HIDDEN>
Message-ID: <89F34741-9EFC-4C19-8167-3B990D90533F@HIDDEN>
MIME-Version: 1.0
Content-Type: text/plain;
 charset=utf-8
Content-Transfer-Encoding: quoted-printable
X-Spam-Score: -0.0 (/)
X-Debbugs-Envelope-To: 52164
Cc: 52164 <at> debbugs.gnu.org
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -1.0 (-)




>
>Hum, the breakage of coq-bignums or coq-equations is recent=2E  Because
>using 65234d0 from Nov=2E 2nd, they are substituable; using coq@8=2E13=2E=
2=2E
>Or do you mean that coq-binums@8=2E13 is broken with coq@8=2E14?

I meant to say bignums 8=2E13 is broken with coq 8=2E14, and bignums 8=2E1=
4 is broken with coq 8=2E13=2E

>
>In all cases, it appears to me clearer to have:
>
> 1=2E update coq
> 2=2E update coq-bignums
> 3=2E update coq-equations
>
>i=2Ee=2E, update the "compiler" and fix then the breakage introduced by
>this "compiler" upgrade, e=2Eg=2E, upgrade other packages=2E  We are alwa=
ys
>doing like that, no?

I've always updated dependents first whenever possible (without breaking a=
nything), then the compiler, then the rest that needs the new compiler=2E H=
owever, I've always been careful not to introduce breakage with a commit, e=
ven if it's inside a series=2E I think that's the policiy, but I'm not sure=
 if it overrides the one-change per commit policy=2E

>
>
>Cheers,
>simon




Information forwarded to guix-patches@HIDDEN:
bug#52164; Package guix-patches. Full text available.

Message received at 52164 <at> debbugs.gnu.org:


Received: (at 52164) by debbugs.gnu.org; 29 Nov 2021 13:21:38 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Mon Nov 29 08:21:38 2021
Received: from localhost ([127.0.0.1]:37403 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1mrgbB-0002EB-Oa
	for submit <at> debbugs.gnu.org; Mon, 29 Nov 2021 08:21:37 -0500
Received: from mail-io1-f54.google.com ([209.85.166.54]:34603)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <zimon.toutoune@HIDDEN>) id 1mrgb7-0002Dw-V2
 for 52164 <at> debbugs.gnu.org; Mon, 29 Nov 2021 08:21:36 -0500
Received: by mail-io1-f54.google.com with SMTP id w22so21463143ioa.1
 for <52164 <at> debbugs.gnu.org>; Mon, 29 Nov 2021 05:21:33 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112;
 h=mime-version:references:in-reply-to:from:date:message-id:subject:to
 :cc:content-transfer-encoding;
 bh=I8x8VTLrkiI0FdMzdrx67XifL9BAh6gJucYqaPKTu2Q=;
 b=ONtce3CyOfRvUO+1tGKhQ81G2F9OPaanMEvhUCPh5lWwZOXlhFKPWREA9jgJRLjFHE
 JYUDonYcWY8hePi4YfEwYoGeJ+5RqzOpqUvvU9dE7+o7iVv1FiP3TXiaPIryeSCPdz7v
 V06gOugkftAqzIFGlBuYEPAyn9poU/VBJyg2ONHaxyZcux33dxRKbxAmweJ+yckw8iF/
 dFPcw4m9ZZVohlQIfih4xxIUGuCBpGUJM48jd4VSdQt8DmS97xie8MkFrXscD77Qv8NZ
 Wfd1jJTCftQS85ZLIG/eXkcJ9LjCM17Fv84T5begBMPgfqGhho3LdUxXOpkPd4E+sQXX
 QTRA==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
 d=1e100.net; s=20210112;
 h=x-gm-message-state:mime-version:references:in-reply-to:from:date
 :message-id:subject:to:cc:content-transfer-encoding;
 bh=I8x8VTLrkiI0FdMzdrx67XifL9BAh6gJucYqaPKTu2Q=;
 b=YY5PePvlcqQc5MY4lOWDPzYWFOlPddk7D3oHXnMcCjoCMUSeIACQx+xfft3etpKz5r
 rgmShabZOtTY7DTVfZA2NiKGYOn3xou6Zn6qFXDdZWBoKIez/6w2Cw4t8H8km0o5eUex
 j8Ry5sX2YojxuA92QJX1cJ2ZM4bQiUyJyFsgg3H7J9qysxc8+SVPWaf79KnVBDHGq4WE
 im6xoeatPq65Ioiq0PHwW1pztBQctipT4CoHBu2Q3Qek7LsbAHEWKNfUw8DGtNYR0NAt
 Vv8/VFbWz1F2kHbukW3BwAOdrzBkvWtF2KAs7POxxjQ+mvm6GbHl6imwyKKT6fuRPSer
 ENvw==
X-Gm-Message-State: AOAM5314D23NSs+pdfeJB6V5zdW6j6xsqSYJywvE6vZPOPZlkV5ezk1w
 WzPryS6iHySPf5MlG094Y1zM0UsfuOzibxCVeTYncinZYdI=
X-Google-Smtp-Source: ABdhPJwdHhFZl9G09GfU9NBbiVmKc+0feAK1zjptv7Bu5xOudhjxffk0H3eq74oXm0k0SuKpudG+OGTDNUwzeEtGjFg=
X-Received: by 2002:a6b:7006:: with SMTP id l6mr1857290ioc.5.1638192088205;
 Mon, 29 Nov 2021 05:21:28 -0800 (PST)
MIME-Version: 1.0
References: <20211128174408.747bccba@HIDDEN>
 <d62a5a234b89db4331c5bda48efa725fea18e97a.1638120398.git.julien@HIDDEN>
 <8635nfl2m6.fsf_-_@HIDDEN>
 <592223CF-588B-44EF-A35F-9E9FDB3E4865@HIDDEN>
In-Reply-To: <592223CF-588B-44EF-A35F-9E9FDB3E4865@HIDDEN>
From: zimoun <zimon.toutoune@HIDDEN>
Date: Mon, 29 Nov 2021 14:21:16 +0100
Message-ID: <CAJ3okZ23f-Vsm2fSJobjt3zLn+Wfy3YshfzKw4FtSLvQ2-YCzw@HIDDEN>
Subject: Re: bug#52164: [PATCH] gnu: coq: Update to 8.14.0.
To: Julien Lepiller <julien@HIDDEN>
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
X-Spam-Score: 0.0 (/)
X-Debbugs-Envelope-To: 52164
Cc: 52164 <at> debbugs.gnu.org
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -1.0 (-)

Hi Julien,

On Mon, 29 Nov 2021 at 13:30, Julien Lepiller <julien@HIDDEN> wrote:

> >With this approach, 3 builds.  Is it required by kind-of Coq bootstrap?
>
> Coq now uses dune, and it is split into core, stdlib anl coq. I prefer to=
 build one dune package in each guix package, rather than everything, espec=
ially since we want to separate coq-ide.

Thanks for the explanations.  So LGTM. :-)


> >>  (define-public coq-bignums
> >>    (package
> >>      (name "coq-bignums")
> >> -    (version "8.13.0")
> >> +    (version "8.14.0")
> >
> >This=E2=80=A6
> >
> >>  (define-public coq-equations
> >>    (package
> >>      (name "coq-equations")
> >> -    (version "1.2.4")
> >> +    (version "1.3")
> >
> >and this=E2=80=A6 Cannot they be upgraded by a separated commit?
> >
> >They will probably be broken with Coq 8.13 but if their upgrade is right
> >after and pushed with the same batch, it is transparent and the
> >atomicity appears to me better.
>
> They're broken with coq 8.13, and the previous version is also broken wit=
h coq 8.14. This is why I was able to update coq semantics independently bu=
t not these two.

Hum, the breakage of coq-bignums or coq-equations is recent.  Because
using 65234d0 from Nov. 2nd, they are substituable; using coq@HIDDEN
Or do you mean that coq-binums@HIDDEN is broken with coq@HIDDEN?

In all cases, it appears to me clearer to have:

 1. update coq
 2. update coq-bignums
 3. update coq-equations

i.e., update the "compiler" and fix then the breakage introduced by
this "compiler" upgrade, e.g., upgrade other packages.  We are always
doing like that, no?


Cheers,
simon




Information forwarded to guix-patches@HIDDEN:
bug#52164; Package guix-patches. Full text available.

Message received at 52164 <at> debbugs.gnu.org:


Received: (at 52164) by debbugs.gnu.org; 29 Nov 2021 12:30:16 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Mon Nov 29 07:30:15 2021
Received: from localhost ([127.0.0.1]:37308 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1mrfnM-0007K6-Ep
	for submit <at> debbugs.gnu.org; Mon, 29 Nov 2021 07:30:15 -0500
Received: from lepiller.eu ([89.234.186.109]:42074)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <julien@HIDDEN>) id 1mrfnK-0007ER-Qv
 for 52164 <at> debbugs.gnu.org; Mon, 29 Nov 2021 07:30:07 -0500
Received: from lepiller.eu (localhost [127.0.0.1])
 by lepiller.eu (OpenSMTPD) with ESMTP id e8be56e2;
 Mon, 29 Nov 2021 12:30:03 +0000 (UTC)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed; d=lepiller.eu; h=date:from
 :to:cc:subject:in-reply-to:references:message-id:mime-version
 :content-type:content-transfer-encoding; s=dkim; bh=EVF/K18rrEB6
 ZFAb5dvEfgHiEJrg+fjKL0eUa0XK1gg=; b=fR6y13NwtCDw31gcNphy/7TkAokU
 xXlRm+irfBZ+RnTaZP+WCHqPcQJ+DVU7SjCdNt5khgjbozjjj5MDt7q9WYxeK1h9
 Ix3bN5o6eO18+SvpBLf4Mz8kiGls+LqlmdHPLdAqcYP+KYLmttfeMDFOITDBphGE
 /nGDhvtMn26WmX4uqPm+TH74shgrLlhurC3mNDBC4uuPJR/esAiF2/gyB2ajS59F
 mvROVkSlJ03JoLUhT2Ag+pWtdqIN4XhUAQZRGbR89XaYoqz6e2EheR9mbfV0Adkd
 xs8B7wzO4V8+OFek3LT5tIxUFRIUI30PHg3EDR/urzdgAJ8p8L7W+20hiQ==
Received: by lepiller.eu (OpenSMTPD) with ESMTPSA id 3adeaeed
 (TLSv1.3:AEAD-AES256-GCM-SHA384:256:NO); 
 Mon, 29 Nov 2021 12:30:02 +0000 (UTC)
Date: Mon, 29 Nov 2021 07:29:51 -0500
From: Julien Lepiller <julien@HIDDEN>
To: zimoun <zimon.toutoune@HIDDEN>
Subject: Re: bug#52164: [PATCH] gnu: coq: Update to 8.14.0.
User-Agent: K-9 Mail for Android
In-Reply-To: <8635nfl2m6.fsf_-_@HIDDEN>
References: <20211128174408.747bccba@HIDDEN>
 <d62a5a234b89db4331c5bda48efa725fea18e97a.1638120398.git.julien@HIDDEN>
 <8635nfl2m6.fsf_-_@HIDDEN>
Message-ID: <592223CF-588B-44EF-A35F-9E9FDB3E4865@HIDDEN>
MIME-Version: 1.0
Content-Type: text/plain;
 charset=utf-8
Content-Transfer-Encoding: quoted-printable
X-Spam-Score: -0.0 (/)
X-Debbugs-Envelope-To: 52164
Cc: 52164 <at> debbugs.gnu.org
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -1.0 (-)



Le 29 novembre 2021 04:42:25 GMT-05:00, zimoun <zimon=2Etoutoune@gmail=2Ec=
om> a =C3=A9crit=C2=A0:
>Hi,
>
>On dim=2E, 28 nov=2E 2021 at 18:27, Julien Lepiller <julien@lepiller=2Eeu=
> wrote:
>> * gnu/packages/coq=2Escm (coq): Update to 8=2E14=2E0=2E
>> (coq-bignums): Update to 8=2E14=2E0=2E
>> (coq-equations): Update to 1=2E3=2E
>> * gnu/packages/patches/coq-fix-envvars=2Epatch: New file=2E
>> * gnu/local=2Emk (dist_patch_DATA): Add it=2E
>> ---
>>  gnu/local=2Emk                               |   1 +
>>  gnu/packages/coq=2Escm                       |  65 +++++++---
>>  gnu/packages/patches/coq-fix-envvars=2Epatch | 139 +++++++++++++++++++=
++
>>  3 files changed, 188 insertions(+), 17 deletions(-)
>>  create mode 100644 gnu/packages/patches/coq-fix-envvars=2Epatch
>
>[=2E=2E=2E]
>
>> -(define-public coq
>> +(define-public coq-core
>
>[=2E=2E=2E]
>
>> -     `(("which" ,which)))
>> +     `(("ocaml-ounit2" ,ocaml-ounit2)
>> +       ("which" ,which)))
>
>This =E2=80=99which=E2=80=99 could be removed=2E :-)
>
>
>> +(define-public coq-stdlib
>> +  (package
>> +    (inherit coq-core)
>> +    (name "coq-stdlib")
>> +    (arguments
>> +     `(#:package "coq-stdlib"
>> +       #:test-target "=2E"))
>> +    (inputs
>> +     `(("coq-core" ,coq-core)
>> +       ("gmp" ,gmp)
>> +       ("ocaml-zarith" ,ocaml-zarith)))
>> +    (native-inputs '())))
>> +
>> +(define-public coq
>> +  (package
>> +    (inherit coq-core)
>> +    (name "coq")
>> +    (arguments
>> +     `(#:package "coq"
>> +       #:test-target "=2E"))
>> +    (propagated-inputs
>> +     `(("coq-core" ,coq-core)
>> +       ("coq-stdlib" ,coq-stdlib)))
>> +    (native-inputs '())))
>
>With this approach, 3 builds=2E  Is it required by kind-of Coq bootstrap?

Coq now uses dune, and it is split into core, stdlib anl coq=2E I prefer t=
o build one dune package in each guix package, rather than everything, espe=
cially since we want to separate coq-ide=2E

>
>
>>  (define-public coq-bignums
>>    (package
>>      (name "coq-bignums")
>> -    (version "8=2E13=2E0")
>> +    (version "8=2E14=2E0")
>
>This=E2=80=A6
>
>>  (define-public coq-equations
>>    (package
>>      (name "coq-equations")
>> -    (version "1=2E2=2E4")
>> +    (version "1=2E3")
>
>and this=E2=80=A6 Cannot they be upgraded by a separated commit?
>
>They will probably be broken with Coq 8=2E13 but if their upgrade is righ=
t
>after and pushed with the same batch, it is transparent and the
>atomicity appears to me better=2E

They're broken with coq 8=2E13, and the previous version is also broken wi=
th coq 8=2E14=2E This is why I was able to update coq semantics independent=
ly but not these two=2E

>
>
>> diff --git a/gnu/packages/patches/coq-fix-envvars=2Epatch b/gnu/package=
s/patches/coq-fix-envvars=2Epatch
>> new file mode 100644
>> index 0000000000=2E=2Edeecf5ce74
>> --- /dev/null
>> +++ b/gnu/packages/patches/coq-fix-envvars=2Epatch
>> @@ -0,0 +1,139 @@
>> +From ebe09fcac72b21d17c4e8fe6edc1b6076a4ae97c Mon Sep 17 00:00:00 2001
>> +From: Julien Lepiller <julien@lepiller=2Eeu>
>> +Date: Sun, 21 Nov 2021 00:38:03 +0100
>> +Subject: [PATCH] Fix environment variable usage=2E
>> +
>> +---
>> + checker/checker=2Eml      |  2 ++
>> + lib/envars=2Eml           | 26 ++++++++++++++++----------
>> + sysinit/coqargs=2Eml      |  3 ++-
>> + sysinit/coqloadpath=2Eml  |  3 ++-
>> + sysinit/coqloadpath=2Emli |  2 +-
>> + tools/coqdep=2Eml         |  2 +-
>> + 6 files changed, 24 insertions(+), 14 deletions(-)
>
>This fix LGTM=2E
>
>
>Otherwise, LTGM=2E
>
>
>Cheers,
>simon




Information forwarded to guix-patches@HIDDEN:
bug#52164; Package guix-patches. Full text available.

Message received at 52164 <at> debbugs.gnu.org:


Received: (at 52164) by debbugs.gnu.org; 29 Nov 2021 09:43:11 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Mon Nov 29 04:43:11 2021
Received: from localhost ([127.0.0.1]:37083 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1mrdBn-0002Y7-5W
	for submit <at> debbugs.gnu.org; Mon, 29 Nov 2021 04:43:11 -0500
Received: from mail-wm1-f49.google.com ([209.85.128.49]:34645)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <zimon.toutoune@HIDDEN>) id 1mrdBU-0002Wn-N2
 for 52164 <at> debbugs.gnu.org; Mon, 29 Nov 2021 04:42:55 -0500
Received: by mail-wm1-f49.google.com with SMTP id
 m25-20020a7bcb99000000b0033aa12cdd33so5556579wmi.1
 for <52164 <at> debbugs.gnu.org>; Mon, 29 Nov 2021 01:42:52 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112;
 h=from:to:cc:subject:references:date:in-reply-to:message-id
 :user-agent:mime-version;
 bh=/JHom7vZwR408NFxs1CIoQtHsuRqIdhzpZ1nBXMdofk=;
 b=ZUXPAYlT0NiZrCheNzTO+5Q108Fe7PvTcPbVFyyP9EGR0OoB3HxooSOOyLdvI7Dig8
 7jNqWRb8D+2iT7R6x4UDXakwPN2uSdKGdnYTkkIJZD8vlEx5gBwtu8nufCrSscE1SJ6V
 /F494JeFpyKPxE/Q+dEgt8HC3P069epLp71G9Mf8sJ9+84+wh5Lv66QXON6VFcd3IKKT
 VTMnjCAxMPeQrJOV2jh5S7VnUAO2qQ2metDklQJWjrpiBDn5OJ7HaAOw9VI3Qn8UpBGk
 p6QDmjDEXuXYp5PtAksYB0Xr1UoDY2i9FfF3j0raa7p6b16Bzx6nB/QEQPxdykrdM+hQ
 i0Jw==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
 d=1e100.net; s=20210112;
 h=x-gm-message-state:from:to:cc:subject:references:date:in-reply-to
 :message-id:user-agent:mime-version;
 bh=/JHom7vZwR408NFxs1CIoQtHsuRqIdhzpZ1nBXMdofk=;
 b=7PMXGF06EvNncQm/nNpbAtL4oVJx582gejcMnFn88BJjX1wEbViDkbhd3Y/i8WRnLE
 OmRUzoEok36UJ2nn7IofBUgPvMn3NuBiuKV15SYgIvyLjXwHbxpi+qHt/gipZC3wgLIe
 GF7JOAGdl5C2GFB1YIXEjlKdDkzqTBbmrulYfqjLQB9GIUWxYL2alJFeGYEgLy7oq6BJ
 HFv4h/BJgD0+95rHcvLGpq5FWwGoonAdcM585HO9DL4KOZmplShtKaQjVtZgLVisEQ1j
 XOaX8X5+DfCLxqpnJI3+G2Pym2HixC6RSd0wlx+yrOD29cxACp47EwYlwNrV89aevOBj
 iAnQ==
X-Gm-Message-State: AOAM532KNQZOzSiSex1nj4qtm+r/gAyTKyw2PvvKFzzWDD9BayENw+WA
 Nt6ki6yUUCkC+kakH5L6a3/llj2zvyY=
X-Google-Smtp-Source: ABdhPJxhXxBx7hPOiJwHsnVDcRJTxSo6dKqG5m/HyenzbmitGT604UrgQo0+yBukG1IOS5jz8lH38A==
X-Received: by 2002:a7b:cbd1:: with SMTP id n17mr35049308wmi.145.1638178966878; 
 Mon, 29 Nov 2021 01:42:46 -0800 (PST)
Received: from jack-Precision-7820-Tower ([193.48.40.117])
 by smtp.gmail.com with ESMTPSA id s8sm13320028wro.19.2021.11.29.01.42.45
 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256);
 Mon, 29 Nov 2021 01:42:46 -0800 (PST)
From: zimoun <zimon.toutoune@HIDDEN>
To: Julien Lepiller <julien@HIDDEN>
Subject: [PATCH 1/3] gnu: ocaml-semantics: Update to 8.14.0.
References: <20211128174408.747bccba@HIDDEN>
 <854d751e7d512c66acb72225120168e5ee16d6a2.1638120398.git.julien@HIDDEN>
Date: Mon, 29 Nov 2021 10:05:39 +0100
In-Reply-To: <854d751e7d512c66acb72225120168e5ee16d6a2.1638120398.git.julien@HIDDEN>
 (Julien Lepiller's message of "Sun, 28 Nov 2021 18:27:09 +0100")
Message-ID: <868rx7l4bg.fsf_-_@HIDDEN>
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/27.2 (gnu/linux)
MIME-Version: 1.0
Content-Type: text/plain
X-Spam-Score: 0.0 (/)
X-Debbugs-Envelope-To: 52164
Cc: 52164 <at> debbugs.gnu.org
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -1.0 (-)

Hi Julien,

Maybe something had been twisted.

 1. Missing changelog.

 2. Incorrect package name in commit oneline: coq-semantics and not
    ocaml-semantics.

Cheers,
simon


On dim., 28 nov. 2021 at 18:27, Julien Lepiller <julien@HIDDEN> wrote:
> ---
>  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 a27ec53ecb..e3c4190ac3 100644
> --- a/gnu/packages/coq.scm
> +++ b/gnu/packages/coq.scm
> @@ -576,7 +576,7 @@ (define-public coq-equations
>  (define-public coq-semantics
>    (package
>      (name "coq-semantics")
> -    (version "8.13.0")
> +    (version "8.14.0")
>      (source
>        (origin
>          (method git-fetch)
> @@ -591,7 +591,7 @@ (define-public coq-semantics
>          (file-name (git-file-name name version))
>          (sha256
>           (base32
> -          "0m5si9dsv96z92gy4xaqz8mzyz8zp7j1sp542l0wzsp5xgyfpc7i"))))
> +          "0ldrp86bfcjpzsb08p45sgs3aczjzr1gksy5dsf7pxapg05pc7ac"))))
>      (build-system gnu-build-system)
>      (native-inputs
>       `(("coq" ,coq)




Information forwarded to guix-patches@HIDDEN:
bug#52164; Package guix-patches. Full text available.

Message received at 52164 <at> debbugs.gnu.org:


Received: (at 52164) by debbugs.gnu.org; 29 Nov 2021 09:43:11 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Mon Nov 29 04:43:11 2021
Received: from localhost ([127.0.0.1]:37080 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1mrdBb-0002XV-QK
	for submit <at> debbugs.gnu.org; Mon, 29 Nov 2021 04:43:11 -0500
Received: from mail-wm1-f45.google.com ([209.85.128.45]:39602)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <zimon.toutoune@HIDDEN>) id 1mrdBW-0002Wr-Om
 for 52164 <at> debbugs.gnu.org; Mon, 29 Nov 2021 04:42:55 -0500
Received: by mail-wm1-f45.google.com with SMTP id
 n33-20020a05600c502100b0032fb900951eso16257793wmr.4
 for <52164 <at> debbugs.gnu.org>; Mon, 29 Nov 2021 01:42:54 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112;
 h=from:to:cc:subject:references:date:in-reply-to:message-id
 :user-agent:mime-version:content-transfer-encoding;
 bh=lYjb2GeXr5FH2HEhI5b1hJF8OkGBX2QehXBiHlgJVZQ=;
 b=RGhzhh5lf4cQfiGnhSjSU6VLRQW2GLS/sy5CL+JwdX/SB+VAEr3NGtDMP+8/cKTKhc
 mEHC4k4iDGwOvVgdBGOUlf9BVlI3ble0Y4d+u+eKxxQMbN0bXbw8ZJxaZGjAaQkgbyNZ
 WCpwVZDK0SWYSLpqt44wzcjfD2Yd3CsaRlX3U1jY5d4wpqVuOXi+80xDZePZytZl1gam
 pjnQ7dPgkjQeJys94Rf3fH5dp1V/OWyxY96IMSqmSUMHOG8uHv0Z49k0Tt1nwSRGJJrY
 HSkZXXKdAwBwEWLWX1Uf31KZuD3UwzpeMelPWwKW33aduWMA0x9df5Y0kgGlt4sbzDlS
 5E/Q==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
 d=1e100.net; s=20210112;
 h=x-gm-message-state:from:to:cc:subject:references:date:in-reply-to
 :message-id:user-agent:mime-version:content-transfer-encoding;
 bh=lYjb2GeXr5FH2HEhI5b1hJF8OkGBX2QehXBiHlgJVZQ=;
 b=c6B+f6AxxU78BkslUX23jph09namtkmrGzifMuW54YsTJGJg6RuM6mBpnDB4NEW0RG
 Bi3ssvUXu8Cz/77/No4ijtZFdSmtQipTah3KzFWCEJO6jl2LXE74JSZRFLS/eDeV68Lg
 FFzaIFf7pjW6IU6cN9b3EgpSlWJQrG68DyokxKftdrSJXDpJN2I5Qy7Dl9GZQEUPb+U7
 QsOltAgGec/H0LvIx4d1QTyy7uxrQUNBfyBvs2Qg6/V47JsZKQGvMo9Rz+qwX0KMZPsV
 tz91eGSomBUiBK/FBtQt02FWjnP7RZ3fLqtuTfV72VbWQ5ymKd9VtWJeRrGmPKwvNRzA
 NBXg==
X-Gm-Message-State: AOAM532jvYrf5L5AN36XzTYVDJ2aCI89pvqNRbViab2ZvuN6aoWOaxmr
 1iR0VKUD4EKET0u8mCHSuBERxVND/fw=
X-Google-Smtp-Source: ABdhPJwdk2vFh2MyRdEVVxFzfBZpQwy1nYw4R2xT8qdT87aQFX8b2JyGeJqo8/MnbezoFUaqL8gKZQ==
X-Received: by 2002:a05:600c:1990:: with SMTP id
 t16mr34473543wmq.48.1638178969130; 
 Mon, 29 Nov 2021 01:42:49 -0800 (PST)
Received: from jack-Precision-7820-Tower ([193.48.40.117])
 by smtp.gmail.com with ESMTPSA id m14sm17570928wrp.28.2021.11.29.01.42.48
 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256);
 Mon, 29 Nov 2021 01:42:48 -0800 (PST)
From: zimoun <zimon.toutoune@HIDDEN>
To: Julien Lepiller <julien@HIDDEN>
Subject: Re: bug#52164: [PATCH] gnu: coq: Update to 8.14.0.
References: <20211128174408.747bccba@HIDDEN>
 <d62a5a234b89db4331c5bda48efa725fea18e97a.1638120398.git.julien@HIDDEN>
Date: Mon, 29 Nov 2021 10:42:25 +0100
In-Reply-To: <d62a5a234b89db4331c5bda48efa725fea18e97a.1638120398.git.julien@HIDDEN>
 (Julien Lepiller's message of "Sun, 28 Nov 2021 18:27:11 +0100")
Message-ID: <8635nfl2m6.fsf_-_@HIDDEN>
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/27.2 (gnu/linux)
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: quoted-printable
X-Spam-Score: 0.0 (/)
X-Debbugs-Envelope-To: 52164
Cc: 52164 <at> debbugs.gnu.org
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -1.0 (-)

Hi,

On dim., 28 nov. 2021 at 18:27, Julien Lepiller <julien@HIDDEN> wrote:
> * gnu/packages/coq.scm (coq): Update to 8.14.0.
> (coq-bignums): Update to 8.14.0.
> (coq-equations): Update to 1.3.
> * gnu/packages/patches/coq-fix-envvars.patch: New file.
> * gnu/local.mk (dist_patch_DATA): Add it.
> ---
>  gnu/local.mk                               |   1 +
>  gnu/packages/coq.scm                       |  65 +++++++---
>  gnu/packages/patches/coq-fix-envvars.patch | 139 +++++++++++++++++++++
>  3 files changed, 188 insertions(+), 17 deletions(-)
>  create mode 100644 gnu/packages/patches/coq-fix-envvars.patch

[...]

> -(define-public coq
> +(define-public coq-core

[...]

> -     `(("which" ,which)))
> +     `(("ocaml-ounit2" ,ocaml-ounit2)
> +       ("which" ,which)))

This =E2=80=99which=E2=80=99 could be removed. :-)


> +(define-public coq-stdlib
> +  (package
> +    (inherit coq-core)
> +    (name "coq-stdlib")
> +    (arguments
> +     `(#:package "coq-stdlib"
> +       #:test-target "."))
> +    (inputs
> +     `(("coq-core" ,coq-core)
> +       ("gmp" ,gmp)
> +       ("ocaml-zarith" ,ocaml-zarith)))
> +    (native-inputs '())))
> +
> +(define-public coq
> +  (package
> +    (inherit coq-core)
> +    (name "coq")
> +    (arguments
> +     `(#:package "coq"
> +       #:test-target "."))
> +    (propagated-inputs
> +     `(("coq-core" ,coq-core)
> +       ("coq-stdlib" ,coq-stdlib)))
> +    (native-inputs '())))

With this approach, 3 builds.  Is it required by kind-of Coq bootstrap?


>  (define-public coq-bignums
>    (package
>      (name "coq-bignums")
> -    (version "8.13.0")
> +    (version "8.14.0")

This=E2=80=A6

>  (define-public coq-equations
>    (package
>      (name "coq-equations")
> -    (version "1.2.4")
> +    (version "1.3")

and this=E2=80=A6 Cannot they be upgraded by a separated commit?

They will probably be broken with Coq 8.13 but if their upgrade is right
after and pushed with the same batch, it is transparent and the
atomicity appears to me better.


> diff --git a/gnu/packages/patches/coq-fix-envvars.patch b/gnu/packages/pa=
tches/coq-fix-envvars.patch
> new file mode 100644
> index 0000000000..deecf5ce74
> --- /dev/null
> +++ b/gnu/packages/patches/coq-fix-envvars.patch
> @@ -0,0 +1,139 @@
> +From ebe09fcac72b21d17c4e8fe6edc1b6076a4ae97c Mon Sep 17 00:00:00 2001
> +From: Julien Lepiller <julien@HIDDEN>
> +Date: Sun, 21 Nov 2021 00:38:03 +0100
> +Subject: [PATCH] Fix environment variable usage.
> +
> +---
> + checker/checker.ml      |  2 ++
> + lib/envars.ml           | 26 ++++++++++++++++----------
> + sysinit/coqargs.ml      |  3 ++-
> + sysinit/coqloadpath.ml  |  3 ++-
> + sysinit/coqloadpath.mli |  2 +-
> + tools/coqdep.ml         |  2 +-
> + 6 files changed, 24 insertions(+), 14 deletions(-)

This fix LGTM.


Otherwise, LTGM.


Cheers,
simon




Information forwarded to guix-patches@HIDDEN:
bug#52164; Package guix-patches. Full text available.

Message received at 52164 <at> debbugs.gnu.org:


Received: (at 52164) by debbugs.gnu.org; 29 Nov 2021 09:42:55 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Mon Nov 29 04:42:55 2021
Received: from localhost ([127.0.0.1]:37078 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1mrdBX-0002X8-8i
	for submit <at> debbugs.gnu.org; Mon, 29 Nov 2021 04:42:55 -0500
Received: from mail-wr1-f41.google.com ([209.85.221.41]:35591)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <zimon.toutoune@HIDDEN>) id 1mrdBW-0002Wp-2W
 for 52164 <at> debbugs.gnu.org; Mon, 29 Nov 2021 04:42:54 -0500
Received: by mail-wr1-f41.google.com with SMTP id i5so35352495wrb.2
 for <52164 <at> debbugs.gnu.org>; Mon, 29 Nov 2021 01:42:53 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112;
 h=from:to:cc:subject:references:date:in-reply-to:message-id
 :user-agent:mime-version;
 bh=m5SY9D621E1Wkhb9Kj5Nk55OZiMSK8B23ecjrECRV3E=;
 b=LG4VAyVuXy3KE81xqEjKrI5NxrQumJhOj/BcIxIIRge7XdkEBq+10uQBs8dIfQXKm0
 AzozSjicrNCQYTPMlelcg9fTCH0RJ35niFT2/UZnxp7Pz0rsAa/e9VEbQsg1k2VwNaSM
 X8IA3BhqINJhVIR8iUBj+Ql/Zi3jpcC3oTtQh2dDPxo/YnV+sNFio02DxqYDIZhKp3UQ
 zn1zwPJ1i/DX/xSCSizvitDTNyroixKCtGr4AaV5DSHgJ6J8dcfUSvxyYTitBf9QvgFT
 Bcgr4kpcaqpSE5wUEiq/Ho9TRPUqD0VEoqC+fHDCm3e+RUk2aHa26TLqpE9LngJf+wlH
 mhCQ==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
 d=1e100.net; s=20210112;
 h=x-gm-message-state:from:to:cc:subject:references:date:in-reply-to
 :message-id:user-agent:mime-version;
 bh=m5SY9D621E1Wkhb9Kj5Nk55OZiMSK8B23ecjrECRV3E=;
 b=sJSDobTHLUi6e9wTmzrqV9X95eYlVS69mdE7FK/48eUu5QPn8z26YyFtbdVEqj0Dx0
 9g1hkT9RsKdK6jazU3L0+tq8Yy0CwSLSTm6xtM3u2n0SjrDjjpLLAPSV0+v/iB5R4IdD
 8Z7dJuwW6j6+fu1uAtybC8G7hAAqxIyy5pP0RHW50l1YVuUaDffDtLNiW9MkG8gvFsmO
 8JQP/HUvn/buDHUnowFG8dBX2IMiRZNUf3hsZNQE6L/7bNhOx0T+jEWcf5aJzXAENEhu
 gxb/ULnhCJYLTand/+arsScTQwv+709/RUCI9HK1QhPTd9J1DwXNT6nXUtklsbtJB+bo
 2RKA==
X-Gm-Message-State: AOAM532fTHI+E45oBejfb1i6AoXxS5IIIJt0na8qmH07Osy/M0uT6b8G
 OF+IFa4w0MgnDh8m2A04xnFuqvIrIVY=
X-Google-Smtp-Source: ABdhPJzOxEQrae5TaSjrsVGNxn0Tymo8JadLvmvxD7azrAaryxALDkI4wYZzONRGHoN4NPZv5VncqQ==
X-Received: by 2002:a5d:6d0c:: with SMTP id e12mr32173811wrq.94.1638178968192; 
 Mon, 29 Nov 2021 01:42:48 -0800 (PST)
Received: from jack-Precision-7820-Tower ([193.48.40.117])
 by smtp.gmail.com with ESMTPSA id n32sm14734760wms.42.2021.11.29.01.42.47
 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256);
 Mon, 29 Nov 2021 01:42:47 -0800 (PST)
From: zimoun <zimon.toutoune@HIDDEN>
To: Julien Lepiller <julien@HIDDEN>
Subject: Re: bug#52164: [PATCH] gnu: coq: Update to 8.14.0.
References: <20211128174408.747bccba@HIDDEN>
 <2e3b3fe2ed163577a854f10b9a1c8531eabcadf6.1638120398.git.julien@HIDDEN>
Date: Mon, 29 Nov 2021 10:06:09 +0100
In-Reply-To: <2e3b3fe2ed163577a854f10b9a1c8531eabcadf6.1638120398.git.julien@HIDDEN>
 (Julien Lepiller's message of "Sun, 28 Nov 2021 18:27:10 +0100")
Message-ID: <865ysbl4am.fsf_-_@HIDDEN>
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/27.2 (gnu/linux)
MIME-Version: 1.0
Content-Type: text/plain
X-Spam-Score: 0.0 (/)
X-Debbugs-Envelope-To: 52164
Cc: 52164 <at> debbugs.gnu.org
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -1.0 (-)


On dim., 28 nov. 2021 at 18:27, Julien Lepiller <julien@HIDDEN> wrote:
> * gnu/packages/coq.scm (proof-general): Update to latest commit.
> ---
>  gnu/packages/coq.scm | 8 ++++----
>  1 file changed, 4 insertions(+), 4 deletions(-)

LGTM.

Cheers,
simon




Information forwarded to guix-patches@HIDDEN:
bug#52164; Package guix-patches. Full text available.

Message received at 52164 <at> debbugs.gnu.org:


Received: (at 52164) by debbugs.gnu.org; 28 Nov 2021 17:27:35 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Sun Nov 28 12:27:35 2021
Received: from localhost ([127.0.0.1]:36308 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1mrNxX-0007M0-PW
	for submit <at> debbugs.gnu.org; Sun, 28 Nov 2021 12:27:35 -0500
Received: from lepiller.eu ([89.234.186.109]:38862)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <julien@HIDDEN>) id 1mrNxT-0007LS-FS
 for 52164 <at> debbugs.gnu.org; Sun, 28 Nov 2021 12:27:24 -0500
Received: from lepiller.eu (localhost [127.0.0.1])
 by lepiller.eu (OpenSMTPD) with ESMTP id d30ff2c9
 for <52164 <at> debbugs.gnu.org>; Sun, 28 Nov 2021 17:27:18 +0000 (UTC)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed; d=lepiller.eu; h=from:to
 :subject:date:message-id:in-reply-to:references:mime-version
 :content-transfer-encoding; s=dkim; bh=680gNOFoHQqSlwNBKhvY2Y9hw
 7SdJO0aaWHGCA98VMI=; b=cu3A/CvXYlq8+H6e4I6LoYbY61xyLV6mRqKnqhX9S
 bRWS3sDddXVG3ZlNCS/bKUg6zVf75OiVDr+kDw0hJOD6IbdV2AX+Vx6SKdvjZZFC
 M9BeAKJ2SNkgQX6yBtBDp6SP1TjTTFNw3VNPtoZwLkxIy9Ia0DpanrphmNI2pyJv
 eVEtxSE/elDefQCpW91cJO8uOGoTvLIAUoH4VLgIdto9CHX1Ztqp/PlUm/iOlcBo
 LbS1G8Bt1Y9OBSQjVf7sFxdNHuSe5NgUYy5veaV+nuLNTkVm5RKEabyxvYOObhq+
 v6VJpEsgN/slNECTUnXZZVEQzY/Ias/ZSYVS8+wSkJrnQ==
Received: by lepiller.eu (OpenSMTPD) with ESMTPSA id d187f1c7
 (TLSv1.3:AEAD-AES256-GCM-SHA384:256:NO) for <52164 <at> debbugs.gnu.org>;
 Sun, 28 Nov 2021 17:27:18 +0000 (UTC)
From: Julien Lepiller <julien@HIDDEN>
To: 52164 <at> debbugs.gnu.org
Subject: [PATCH 3/3] gnu: coq: Update to 8.14.0.
Date: Sun, 28 Nov 2021 18:27:11 +0100
Message-Id: <d62a5a234b89db4331c5bda48efa725fea18e97a.1638120398.git.julien@HIDDEN>
X-Mailer: git-send-email 2.34.0
In-Reply-To: <20211128174408.747bccba@HIDDEN>
References: <20211128174408.747bccba@HIDDEN>
MIME-Version: 1.0
Content-Transfer-Encoding: 8bit
X-Spam-Score: -0.0 (/)
X-Debbugs-Envelope-To: 52164
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -1.0 (-)

* gnu/packages/coq.scm (coq): Update to 8.14.0.
(coq-bignums): Update to 8.14.0.
(coq-equations): Update to 1.3.
* gnu/packages/patches/coq-fix-envvars.patch: New file.
* gnu/local.mk (dist_patch_DATA): Add it.
---
 gnu/local.mk                               |   1 +
 gnu/packages/coq.scm                       |  65 +++++++---
 gnu/packages/patches/coq-fix-envvars.patch | 139 +++++++++++++++++++++
 3 files changed, 188 insertions(+), 17 deletions(-)
 create mode 100644 gnu/packages/patches/coq-fix-envvars.patch

diff --git a/gnu/local.mk b/gnu/local.mk
index efe153faf2..b26907a211 100644
--- a/gnu/local.mk
+++ b/gnu/local.mk
@@ -951,6 +951,7 @@ dist_patch_DATA =						\
   %D%/packages/patches/collectd-5.11.0-noinstallvar.patch		\
   %D%/packages/patches/combinatorial-blas-awpm.patch		\
   %D%/packages/patches/combinatorial-blas-io-fix.patch		\
+  %D%/packages/patches/coq-fix-envvars.patch			\
   %D%/packages/patches/coreutils-ls.patch			\
   %D%/packages/patches/cpuinfo-system-libraries.patch		\
   %D%/packages/patches/crawl-upgrade-saves.patch		\
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 2045901aed..b6a5ff357c 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -49,10 +49,10 @@ (define-module (gnu packages coq)
   #:use-module (guix utils)
   #:use-module ((srfi srfi-1) #:hide (zip)))
 
-(define-public coq
+(define-public coq-core
   (package
-    (name "coq")
-    (version "8.13.2")
+    (name "coq-core")
+    (version "8.14.0")
     (source
      (origin
        (method git-fetch)
@@ -62,25 +62,31 @@ (define-public coq
        (file-name (git-file-name name version))
        (sha256
         (base32
-         "15r0cm3p9dlsxbg0lf05njjp1xi1y74vxvq6drxjykax67x95l8a"))))
+         "0iachapmdwvwwlvkrb2yxhqqrgzs70zyr1c9v1jdb1awx3bp68hf"))
+       (patches (search-patches "coq-fix-envvars.patch"))))
     (native-search-paths
      (list (search-path-specification
             (variable "COQPATH")
-            (files (list "lib/coq/user-contrib")))
+            (files (list "lib/ocaml/site-lib/coq/user-contrib"
+                         "lib/coq/user-contrib")))
            (search-path-specification
-            (variable "COQLIB")
-            (files (list "lib/ocaml/site-lib/coq"))
+            (variable "COQLIBPATH")
+            (files (list "lib/ocaml/site-lib/coq")))
+           (search-path-specification
+            (variable "COQCORELIB")
+            (files (list "lib/ocaml/site-lib/coq-core"))
             (separator #f))))
     (build-system dune-build-system)
     (inputs
      `(("gmp" ,gmp)
        ("ocaml-zarith" ,ocaml-zarith)))
     (native-inputs
-     `(("which" ,which)))
+     `(("ocaml-ounit2" ,ocaml-ounit2)
+       ("which" ,which)))
     (arguments
-     `(#:package "coq"
-       #:test-target "test-suite"))
-    (properties '((upstream-name . "coq"))) ; for inherited packages
+     `(#:package "coq-core"
+       #:test-target "."))
+    (properties '((upstream-name . "coq"))) ; also for inherited packages
     (home-page "https://coq.inria.fr")
     (synopsis "Proof assistant for higher-order logic")
     (description
@@ -91,6 +97,31 @@ (define-public coq
     ;; Some of the documentation is distributed under opl1.0+.
     (license (list license:lgpl2.1 license:opl1.0+))))
 
+(define-public coq-stdlib
+  (package
+    (inherit coq-core)
+    (name "coq-stdlib")
+    (arguments
+     `(#:package "coq-stdlib"
+       #:test-target "."))
+    (inputs
+     `(("coq-core" ,coq-core)
+       ("gmp" ,gmp)
+       ("ocaml-zarith" ,ocaml-zarith)))
+    (native-inputs '())))
+
+(define-public coq
+  (package
+    (inherit coq-core)
+    (name "coq")
+    (arguments
+     `(#:package "coq"
+       #:test-target "."))
+    (propagated-inputs
+     `(("coq-core" ,coq-core)
+       ("coq-stdlib" ,coq-stdlib)))
+    (native-inputs '())))
+
 (define-public coq-ide-server
   (package
     (inherit coq)
@@ -410,7 +441,7 @@ (define-public coq-coquelicot
 (define-public coq-bignums
   (package
     (name "coq-bignums")
-    (version "8.13.0")
+    (version "8.14.0")
     (source (origin
               (method git-fetch)
               (uri (git-reference
@@ -419,7 +450,7 @@ (define-public coq-bignums
               (file-name (git-file-name name version))
               (sha256
                (base32
-                "1n66i7hd9222b2ks606mak7m4f0dgy02xgygjskmmav6h7g2sx7y"))))
+                "0jsgdvj0ddhkls32krprp34r64y1rb5mwxl34fgaxk2k4664yq06"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("ocaml" ,ocaml)
@@ -471,7 +502,7 @@ (define-public coq-interval
     (arguments
      `(#:configure-flags
        (list (string-append "COQUSERCONTRIB=" (assoc-ref %outputs "out")
-                            "/lib/coq/user-contrib"))
+                            "/lib/ocaml/site-lib/coq/user-contrib"))
        #:phases
        (modify-phases %standard-phases
          (add-before 'configure 'fix-remake
@@ -537,16 +568,16 @@ (define-public coq-autosubst
 (define-public coq-equations
   (package
     (name "coq-equations")
-    (version "1.2.4")
+    (version "1.3")
     (source (origin
               (method git-fetch)
               (uri (git-reference
                     (url "https://github.com/mattam82/Coq-Equations")
-                    (commit (string-append "v" version "-8.13"))))
+                    (commit (string-append "v" version "-8.14"))))
               (file-name (git-file-name name version))
               (sha256
                (base32
-                "0i014lshsdflzw6h0qxra9d2f0q82vffxv2f29awbb9ad0p4rq4q"))))
+                "19bj9nncd1r9g4273h5qx35gs3i4bw5z9bhjni24b413hyj55hkv"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("ocaml"  ,ocaml)
diff --git a/gnu/packages/patches/coq-fix-envvars.patch b/gnu/packages/patches/coq-fix-envvars.patch
new file mode 100644
index 0000000000..deecf5ce74
--- /dev/null
+++ b/gnu/packages/patches/coq-fix-envvars.patch
@@ -0,0 +1,139 @@
+From ebe09fcac72b21d17c4e8fe6edc1b6076a4ae97c Mon Sep 17 00:00:00 2001
+From: Julien Lepiller <julien@HIDDEN>
+Date: Sun, 21 Nov 2021 00:38:03 +0100
+Subject: [PATCH] Fix environment variable usage.
+
+---
+ checker/checker.ml      |  2 ++
+ lib/envars.ml           | 26 ++++++++++++++++----------
+ sysinit/coqargs.ml      |  3 ++-
+ sysinit/coqloadpath.ml  |  3 ++-
+ sysinit/coqloadpath.mli |  2 +-
+ tools/coqdep.ml         |  2 +-
+ 6 files changed, 24 insertions(+), 14 deletions(-)
+
+diff --git a/checker/checker.ml b/checker/checker.ml
+index f55ed9e8d6..3b797729ed 100644
+--- a/checker/checker.ml
++++ b/checker/checker.ml
+@@ -104,6 +104,7 @@ let set_include d p =
+ (* Initializes the LoadPath *)
+ let init_load_path () =
+   let coqlib = Envars.coqlib () in
++  let coqcorelib = Envars.coqcorelib () in
+   let user_contrib = coqlib/"user-contrib" in
+   let xdg_dirs = Envars.xdg_dirs in
+   let coqpath = Envars.coqpath in
+@@ -111,6 +112,7 @@ let init_load_path () =
+     CPath.choose_existing
+       [ CPath.make [ coqlib ; "plugins" ]
+       ; CPath.make [ coqlib ; ".."; "coq-core"; "plugins" ]
++      ; CPath.make [ coqcorelib ; "plugins" ]
+       ] |> function
+     | None ->
+       CErrors.user_err (Pp.str "Cannot find plugins directory")
+diff --git a/lib/envars.ml b/lib/envars.ml
+index 750bd60e71..c7affbd437 100644
+--- a/lib/envars.ml
++++ b/lib/envars.ml
+@@ -127,15 +127,21 @@ let check_file_else ~dir ~file oth =
+ let guess_coqlib fail =
+   getenv_else "COQLIB" (fun () ->
+   let prelude = "theories/Init/Prelude.vo" in
+-  check_file_else ~dir:Coq_config.coqlibsuffix ~file:prelude
+-    (fun () ->
+-      if Sys.file_exists (Coq_config.coqlib / prelude)
+-      then Coq_config.coqlib
+-      else
+-        fail "cannot guess a path for Coq libraries; please use -coqlib option \
+-              or ensure you have installed the package containing Coq's stdlib (coq-stdlib in OPAM) \
+-              If you intend to use Coq without a standard library, the -boot -noinit options must be used.")
+-  )
++  let coqlibpath = getenv_else "COQLIBPATH" (fun () -> Coq_config.coqlibsuffix) in
++  let paths = path_to_list coqlibpath in
++  let valid_paths =
++    List.filter
++      (fun dir -> (check_file_else ~dir:dir ~file:prelude (fun () -> "")) <> "")
++      paths in
++  match valid_paths with
++  | [] ->
++    if Sys.file_exists (Coq_config.coqlib / prelude)
++    then Coq_config.coqlib
++    else
++      fail "cannot guess a path for Coq libraries; please use -coqlib option \
++            or ensure you have installed the package containing Coq's stdlib (coq-stdlib in OPAM) \
++            If you intend to use Coq without a standard library, the -boot -noinit options must be used."
++  | p::_ -> p)
+ 
+ let coqlib_ref : string option ref = ref None
+ let set_user_coqlib path = coqlib_ref := Some path
+@@ -208,7 +214,7 @@ let xdg_dirs ~warn =
+ let print_config ?(prefix_var_name="") f coq_src_subdirs =
+   let open Printf in
+   fprintf f "%sCOQLIB=%s/\n" prefix_var_name (coqlib ());
+-  fprintf f "%sCOQCORELIB=%s/\n" prefix_var_name (coqlib () / "../coq-core/");
++  fprintf f "%sCOQCORELIB=%s/\n" prefix_var_name (coqcorelib ());
+   fprintf f "%sDOCDIR=%s/\n" prefix_var_name (docdir ());
+   fprintf f "%sOCAMLFIND=%s\n" prefix_var_name (ocamlfind ());
+   fprintf f "%sCAMLFLAGS=%s\n" prefix_var_name Coq_config.caml_flags;
+diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml
+index 00f70a5fea..8325623a63 100644
+--- a/sysinit/coqargs.ml
++++ b/sysinit/coqargs.ml
+@@ -453,7 +453,8 @@ let build_load_path opts =
+     if opts.pre.boot then [],[]
+     else
+       let coqlib = Envars.coqlib () in
+-      Coqloadpath.init_load_path ~coqlib in
++      let coqcorelib = Envars.coqcorelib () in
++      Coqloadpath.init_load_path ~coqlib ~coqcorelib in
+   ml_path @ opts.pre.ml_includes ,
+   vo_path @ opts.pre.vo_includes
+ 
+diff --git a/sysinit/coqloadpath.ml b/sysinit/coqloadpath.ml
+index 95ae5da3de..a58cfe6928 100644
+--- a/sysinit/coqloadpath.ml
++++ b/sysinit/coqloadpath.ml
+@@ -35,7 +35,7 @@ let build_userlib_path ~unix_path =
+   else [], []
+ 
+ (* LoadPath for Coq user libraries *)
+-let init_load_path ~coqlib =
++let init_load_path ~coqlib ~coqcorelib =
+ 
+   let open Loadpath in
+   let user_contrib = coqlib/"user-contrib" in
+@@ -50,6 +50,7 @@ let init_load_path ~coqlib =
+     CPath.choose_existing
+       [ CPath.make [ coqlib ; "plugins" ]
+       ; CPath.make [ coqlib ; ".."; "coq-core"; "plugins" ]
++      ; CPath.make [ coqcorelib ; "plugins" ]
+       ] |> function
+     | None ->
+       CErrors.user_err (Pp.str "Cannot find plugins directory")
+diff --git a/sysinit/coqloadpath.mli b/sysinit/coqloadpath.mli
+index d853e9ea54..43c6dfa134 100644
+--- a/sysinit/coqloadpath.mli
++++ b/sysinit/coqloadpath.mli
+@@ -12,5 +12,5 @@
+    includes (in-order) Coq's standard library, Coq's [user-contrib]
+    folder, and directories specified in [COQPATH] and [XDG_DIRS] *)
+ val init_load_path
+-  : coqlib:CUnix.physical_path
++  : coqlib:CUnix.physical_path -> coqcorelib:CUnix.physical_path
+   -> CUnix.physical_path list * Loadpath.vo_path list
+diff --git a/tools/coqdep.ml b/tools/coqdep.ml
+index c1c87993e1..6c78e10866 100644
+--- a/tools/coqdep.ml
++++ b/tools/coqdep.ml
+@@ -33,7 +33,7 @@ let coqdep () =
+     let coqlib = Envars.coqlib () in
+     let coq_plugins_dir = Filename.concat (Envars.coqcorelib ()) "plugins" in
+     if not (Sys.file_exists coq_plugins_dir) then
+-      CErrors.user_err Pp.(str "coqdep: cannot find plugins directory for coqlib: " ++ str coqlib ++ fnl ());
++      CErrors.user_err Pp.(str "coqdep: cannot find plugins directory " ++ str coq_plugins_dir ++ str " for coqlib: " ++ str coqlib ++ fnl ());
+     CD.add_rec_dir_import CD.add_coqlib_known (coqlib//"theories") ["Coq"];
+     CD.add_rec_dir_import CD.add_coqlib_known (coq_plugins_dir) ["Coq"];
+     let user = coqlib//"user-contrib" in
+-- 
+2.33.1
-- 
2.33.1





Information forwarded to guix-patches@HIDDEN:
bug#52164; Package guix-patches. Full text available.

Message received at 52164 <at> debbugs.gnu.org:


Received: (at 52164) by debbugs.gnu.org; 28 Nov 2021 17:27:27 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Sun Nov 28 12:27:27 2021
Received: from localhost ([127.0.0.1]:36306 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1mrNxX-0007Ly-DS
	for submit <at> debbugs.gnu.org; Sun, 28 Nov 2021 12:27:27 -0500
Received: from lepiller.eu ([89.234.186.109]:38862)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <julien@HIDDEN>) id 1mrNxS-0007LS-IQ
 for 52164 <at> debbugs.gnu.org; Sun, 28 Nov 2021 12:27:23 -0500
Received: from lepiller.eu (localhost [127.0.0.1])
 by lepiller.eu (OpenSMTPD) with ESMTP id 7c811c7d
 for <52164 <at> debbugs.gnu.org>; Sun, 28 Nov 2021 17:27:18 +0000 (UTC)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed; d=lepiller.eu; h=from:to
 :subject:date:message-id:in-reply-to:references:mime-version
 :content-transfer-encoding; s=dkim; bh=c/Tr1jMIU4f18LwqyCQMkA0rP
 WcB0puNrW1dvR+26xc=; b=P85/C/x1kzGK9CBiLwVgkDygsxikOvOBH6ggwDeCH
 TzCatwUT0LLoFrDFzXiY4BHsLWu2kG5nGRmxtN0dWAaivMFgrZRQXRybOTJmWRzZ
 CtwtK2u7WLGVyN7jr+O7vYY5mM1dDIaQuaFgjZfCDmY4WNpS/uCtObkATMa7RKe+
 qdEHlsn2wCw1DW/Uxe6D5G+kH5CHzZvZ60ydW7npgHTGzYFXGo0thPrA/zZ7K+zv
 Tluk/sjpfJQTeyVpkhmVKunHe6yfewWxpSOaWTfRCGxI7lDWGY5P933LMecwN0u9
 27O7NOVWwBuNCGUMAPQ/wf2YHLhp4oSduivWn3z1/arcQ==
Received: by lepiller.eu (OpenSMTPD) with ESMTPSA id 8577d61a
 (TLSv1.3:AEAD-AES256-GCM-SHA384:256:NO) for <52164 <at> debbugs.gnu.org>;
 Sun, 28 Nov 2021 17:27:17 +0000 (UTC)
From: Julien Lepiller <julien@HIDDEN>
To: 52164 <at> debbugs.gnu.org
Subject: [PATCH 2/3] gnu: proof-general: Update to latest commit.
Date: Sun, 28 Nov 2021 18:27:10 +0100
Message-Id: <2e3b3fe2ed163577a854f10b9a1c8531eabcadf6.1638120398.git.julien@HIDDEN>
X-Mailer: git-send-email 2.34.0
In-Reply-To: <20211128174408.747bccba@HIDDEN>
References: <20211128174408.747bccba@HIDDEN>
MIME-Version: 1.0
Content-Transfer-Encoding: 8bit
X-Spam-Score: -0.0 (/)
X-Debbugs-Envelope-To: 52164
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -1.0 (-)

* gnu/packages/coq.scm (proof-general): Update to latest commit.
---
 gnu/packages/coq.scm | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index e3c4190ac3..2045901aed 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -119,9 +119,9 @@ (define-public coq-ide
 (define-public proof-general
   ;; The latest release is from 2016 and there has been more than 450 commits
   ;; since then.
-  ;; Commit from 2021-06-07.
-  (let ((commit "bc86736abb728ec0d28abc90ef0adae21d29a66a")
-        (revision "0"))
+  ;; Commit from 2021-11-25.
+  (let ((commit "1b1083e86e0cddc20ff2f1a6b25c7a7eee2edf02")
+        (revision "1"))
     (package
       (name "proof-general")
       (version (git-version "4.4" revision commit))
@@ -133,7 +133,7 @@ (define-public proof-general
                 (file-name (git-file-name name version))
                 (sha256
                  (base32
-                  "00cga3n9nj2xa3ivb0fdkkdx3k11fp4879y188738631yd1x2lsa"))))
+                  "1pnysczhscapgwmvf6ix7f31lf3hnh8h977bfll1m7jlxl9b9c0j"))))
       (build-system gnu-build-system)
       (native-inputs
        `(("emacs" ,emacs-minimal)
-- 
2.33.1





Information forwarded to guix-patches@HIDDEN:
bug#52164; Package guix-patches. Full text available.

Message received at 52164 <at> debbugs.gnu.org:


Received: (at 52164) by debbugs.gnu.org; 28 Nov 2021 17:27:24 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Sun Nov 28 12:27:24 2021
Received: from localhost ([127.0.0.1]:36304 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1mrNxU-0007Lj-4B
	for submit <at> debbugs.gnu.org; Sun, 28 Nov 2021 12:27:24 -0500
Received: from lepiller.eu ([89.234.186.109]:38862)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <julien@HIDDEN>) id 1mrNxP-0007LS-8i
 for 52164 <at> debbugs.gnu.org; Sun, 28 Nov 2021 12:27:22 -0500
Received: from lepiller.eu (localhost [127.0.0.1])
 by lepiller.eu (OpenSMTPD) with ESMTP id 81c079cc
 for <52164 <at> debbugs.gnu.org>; Sun, 28 Nov 2021 17:27:17 +0000 (UTC)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed; d=lepiller.eu; h=from:to
 :subject:date:message-id:in-reply-to:references:mime-version
 :content-transfer-encoding; s=dkim; bh=LmiuDsE7ZXPdLCtp5qIvI5THL
 Abx6j6fmlrYKnuTOlg=; b=QUGOkat3IYgnVVn+yKIv2NxvpMGyslC9ONj+9LADk
 tieJwO4Pwv44dYYbIenUsQuH9AlRmobf/iKU/NLXGu9gzXc/ctwT4fyYw+1NC1cr
 8al3NTwW2v5r+r+N0tH+jfUsZji7uUw+A5uETEdu9DH6ULXDCQqdbVr7ftd1sxvc
 8SwT1m8PwFeSA4/30uVjghTPjvNFvmn0ch9WrjQ++3eCTDENwSw4DZtOqz+diVHN
 GEotS/TZZ6K2Zs0BCv61YKqWwH4SZokLq5GVN/Uh7m0jYWJgOstaS6Ywod9XMfL2
 09HHhXzhjkwxXlQ47Rfu2kZX5svgWAzg3cjuLly7JCO0A==
Received: by lepiller.eu (OpenSMTPD) with ESMTPSA id ac92b9c5
 (TLSv1.3:AEAD-AES256-GCM-SHA384:256:NO) for <52164 <at> debbugs.gnu.org>;
 Sun, 28 Nov 2021 17:27:17 +0000 (UTC)
From: Julien Lepiller <julien@HIDDEN>
To: 52164 <at> debbugs.gnu.org
Subject: [PATCH 1/3] gnu: ocaml-semantics: Update to 8.14.0.
Date: Sun, 28 Nov 2021 18:27:09 +0100
Message-Id: <854d751e7d512c66acb72225120168e5ee16d6a2.1638120398.git.julien@HIDDEN>
X-Mailer: git-send-email 2.34.0
In-Reply-To: <20211128174408.747bccba@HIDDEN>
References: <20211128174408.747bccba@HIDDEN>
MIME-Version: 1.0
Content-Transfer-Encoding: 8bit
X-Spam-Score: -0.0 (/)
X-Debbugs-Envelope-To: 52164
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -1.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 a27ec53ecb..e3c4190ac3 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -576,7 +576,7 @@ (define-public coq-equations
 (define-public coq-semantics
   (package
     (name "coq-semantics")
-    (version "8.13.0")
+    (version "8.14.0")
     (source
       (origin
         (method git-fetch)
@@ -591,7 +591,7 @@ (define-public coq-semantics
         (file-name (git-file-name name version))
         (sha256
          (base32
-          "0m5si9dsv96z92gy4xaqz8mzyz8zp7j1sp542l0wzsp5xgyfpc7i"))))
+          "0ldrp86bfcjpzsb08p45sgs3aczjzr1gksy5dsf7pxapg05pc7ac"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("coq" ,coq)
-- 
2.33.1





Information forwarded to guix-patches@HIDDEN:
bug#52164; Package guix-patches. Full text available.

Message received at submit <at> debbugs.gnu.org:


Received: (at submit) by debbugs.gnu.org; 28 Nov 2021 16:44:48 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Sun Nov 28 11:44:47 2021
Received: from localhost ([127.0.0.1]:36241 helo=debbugs.gnu.org)
	by debbugs.gnu.org with esmtp (Exim 4.84_2)
	(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
	id 1mrNIF-0003ys-Ow
	for submit <at> debbugs.gnu.org; Sun, 28 Nov 2021 11:44:47 -0500
Received: from lists.gnu.org ([209.51.188.17]:39422)
 by debbugs.gnu.org with esmtp (Exim 4.84_2)
 (envelope-from <julien@HIDDEN>) id 1mrNID-0003yi-3C
 for submit <at> debbugs.gnu.org; Sun, 28 Nov 2021 11:44:45 -0500
Received: from eggs.gnu.org ([209.51.188.92]:51160)
 by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
 (Exim 4.90_1) (envelope-from <julien@HIDDEN>)
 id 1mrNIC-00085U-Rr
 for guix-patches@HIDDEN; Sun, 28 Nov 2021 11:44:44 -0500
Received: from lepiller.eu ([89.234.186.109]:36668)
 by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
 (Exim 4.90_1) (envelope-from <julien@HIDDEN>)
 id 1mrNI9-0000Kb-9p
 for guix-patches@HIDDEN; Sun, 28 Nov 2021 11:44:44 -0500
Received: from lepiller.eu (localhost [127.0.0.1])
 by lepiller.eu (OpenSMTPD) with ESMTP id 540f5f0b
 for <guix-patches@HIDDEN>; Sun, 28 Nov 2021 16:44:33 +0000 (UTC)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed; d=lepiller.eu; h=date:from
 :to:subject:message-id:mime-version:content-type
 :content-transfer-encoding; s=dkim; bh=Dkqx/iqB0D2Tipv+gfcQW/pAQ
 W5BfCt4xMmNeRkhAno=; b=F+EjrOW9Mpn72EW9VKBzSLUigpoA4Hx7b6DXso1KP
 1wtvHgVqVKOIJ7ttPFPa0xvZpW/YGWwbRMOalFakLYlC+/RYzAZuOOgw1ICW1ic+
 NDPu/mcLFAKbKmrtExbCT0NiKIO/myYH9NdBdNLVNcAGDTLxG1FJZU6Fu3bc1EfD
 xY/BlsxsUh8SYdAQmqcfrGAqnhi8hqiVGX6wRvGkEhuuSYs2gnbv08oluK9aPVip
 utNKc07rEEsUXf7s/MYPaesvwDSA3qkSPTVk5rD1XVgbbdxsT9yagM48k1MghlBd
 g4cb0VZi1G7/3PCZjjZ6DoVI+o//xcp1vwbmBkFiZyLSw==
Received: by lepiller.eu (OpenSMTPD) with ESMTPSA id 87246e35
 (TLSv1.3:AEAD-AES256-GCM-SHA384:256:NO) for <guix-patches@HIDDEN>;
 Sun, 28 Nov 2021 16:44:32 +0000 (UTC)
Date: Sun, 28 Nov 2021 17:44:26 +0100
From: Julien Lepiller <julien@HIDDEN>
To: guix-patches@HIDDEN
Subject: [PATCH] gnu: coq: Update to 8.14.0.
Message-ID: <20211128174408.747bccba@HIDDEN>
X-Mailer: Claws Mail 4.0.0 (GTK+ 3.24.24; x86_64-pc-linux-gnu)
MIME-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Received-SPF: pass client-ip=89.234.186.109; envelope-from=julien@HIDDEN;
 helo=lepiller.eu
X-Spam_score_int: -20
X-Spam_score: -2.1
X-Spam_bar: --
X-Spam_report: (-2.1 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1,
 DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, SPF_HELO_PASS=-0.001,
 SPF_PASS=-0.001 autolearn=ham autolearn_force=no
X-Spam_action: no action
X-Spam-Score: -1.3 (-)
X-Debbugs-Envelope-To: submit
X-BeenThere: debbugs-submit <at> debbugs.gnu.org
X-Mailman-Version: 2.1.18
Precedence: list
List-Id: <debbugs-submit.debbugs.gnu.org>
List-Unsubscribe: <https://debbugs.gnu.org/cgi-bin/mailman/options/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=unsubscribe>
List-Archive: <https://debbugs.gnu.org/cgi-bin/mailman/private/debbugs-submit/>
List-Post: <mailto:debbugs-submit <at> debbugs.gnu.org>
List-Help: <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=help>
List-Subscribe: <https://debbugs.gnu.org/cgi-bin/mailman/listinfo/debbugs-submit>, 
 <mailto:debbugs-submit-request <at> debbugs.gnu.org?subject=subscribe>
Errors-To: debbugs-submit-bounces <at> debbugs.gnu.org
Sender: "Debbugs-submit" <debbugs-submit-bounces <at> debbugs.gnu.org>
X-Spam-Score: -2.3 (--)

Hi Guix!

this small series updates coq to its latest version.




Acknowledgement sent to Julien Lepiller <julien@HIDDEN>:
New bug report received and forwarded. Copy sent to guix-patches@HIDDEN. Full text available.
Report forwarded to guix-patches@HIDDEN:
bug#52164; Package guix-patches. Full text available.
Please note: This is a static page, with minimal formatting, updated once a day.
Click here to see this page with the latest information and nicer formatting.
Last modified: Mon, 29 Nov 2021 14:30:02 UTC

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