From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp2 ([2001:41d0:2:bcc0::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms0.migadu.com with LMTPS id oFRyNOigpGGf/AAAgWs5BA (envelope-from ) for ; Mon, 29 Nov 2021 10:44:08 +0100 Received: from aspmx1.migadu.com ([2001:41d0:2:bcc0::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp2 with LMTPS id yL0rMOigpGG1OwAAB5/wlQ (envelope-from ) for ; Mon, 29 Nov 2021 09:44:08 +0000 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by aspmx1.migadu.com (Postfix) with ESMTPS id 84C8236D77 for ; Mon, 29 Nov 2021 10:44:08 +0100 (CET) Received: from localhost ([::1]:35898 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1mrdCh-0001g4-No for larch@yhetil.org; Mon, 29 Nov 2021 04:44:07 -0500 Received: from eggs.gnu.org ([209.51.188.92]:58074) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1mrdCc-0001fU-LP for guix-patches@gnu.org; Mon, 29 Nov 2021 04:44:02 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:53771) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1mrdCc-0003Tf-DO for guix-patches@gnu.org; Mon, 29 Nov 2021 04:44:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1mrdCc-0002ZS-Be for guix-patches@gnu.org; Mon, 29 Nov 2021 04:44:02 -0500 X-Loop: help-debbugs@gnu.org Subject: [bug#52164] [PATCH] gnu: coq: Update to 8.14.0. Resent-From: zimoun Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Mon, 29 Nov 2021 09:44:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 52164 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Julien Lepiller Cc: 52164@debbugs.gnu.org Received: via spool by 52164-submit@debbugs.gnu.org id=B52164.16381789919806 (code B ref 52164); Mon, 29 Nov 2021 09:44:02 +0000 Received: (at 52164) by debbugs.gnu.org; 29 Nov 2021 09:43:11 +0000 Received: from localhost ([127.0.0.1]:37080 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mrdBb-0002XV-QK for submit@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 ) id 1mrdBW-0002Wr-Om for 52164@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@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 References: <20211128174408.747bccba@tachikoma.lepiller.eu> Date: Mon, 29 Nov 2021 10:42:25 +0100 In-Reply-To: (Julien Lepiller's message of "Sun, 28 Nov 2021 18:27:11 +0100") Message-ID: <8635nfl2m6.fsf_-_@gmail.com> 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-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+larch=yhetil.org@gnu.org Sender: "Guix-patches" X-Migadu-Flow: FLOW_IN X-Migadu-Country: US ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=yhetil.org; s=key1; t=1638179048; h=from:from:sender:sender:reply-to:subject:subject:date:date: message-id:message-id:to:to:cc:cc:mime-version:mime-version: content-type:content-type: content-transfer-encoding:content-transfer-encoding:resent-cc: resent-from:resent-sender:resent-message-id:in-reply-to:in-reply-to: references:references:list-id:list-help:list-unsubscribe: list-subscribe:list-post:dkim-signature; bh=lYjb2GeXr5FH2HEhI5b1hJF8OkGBX2QehXBiHlgJVZQ=; b=ooZBBUJLzDO+ZhkD7R4tmmoeX0QnmgDrCxb2SAbWqzXGSbQFQKM4BIBg5ufvMuvS7NyTdO sVuG/oRQwoz7UAdBimdzxlCM42lH2Q37v6sTt5ycWdQ9GlMRSnetd/95fohX68ItO+tUtQ V6gZHJsSS5Yln8G1EAhELWGuIjEnRlQ3cJ930nF2HU3nPsZFfuQy+L2FIjq3reVIX6K4/h 6bPmYi4eTOzXWE4cm+jv9SCEdf3dc9VKxXz3kXREqOg73NNe48U+0h0JX7PUW9NVete5Ek 9H/uuiOu+D6NkPIKXFZTN5vNcYIz550tDTGqq+Xpbk3pC5eVaHyZYo77oWOMrQ== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1638179048; a=rsa-sha256; cv=none; b=emox6i9GcdzLJaQCdWC1g1zNRvb/yKN+xYTwdE+EYuOCUB2uaeSa+QqaXB2RhBAekKgoiN V7nzi7oW7deQY9HkQ2PC9XZzhQWCX8oxmWz2oh8RaOn5Uo+cKhi2iOe3rGaj/zjpeGxwHo KlSx1xfcjZzeas9kdc9dSc1tQM/rIVPU0D8zJ3Ccp68ualiSlZq8NeiqIdF7KmGuZ36j4K wg/wQXmwEocBL3IbN6MfEQiHEewVpyPD3WnFvI81zaHIZeW90r4XfPNe+cbVbDow7FBCZr WVjkFkuuncDHk/TB1zWy05mYHdeFPGrjZ4untyw+2j+Jo5o1NplV1CrQWZWGOA== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=gmail.com header.s=20210112 header.b=RGhzhh5l; dmarc=fail reason="SPF not aligned (relaxed)" header.from=gmail.com (policy=none); spf=pass (aspmx1.migadu.com: domain of "guix-patches-bounces+larch=yhetil.org@gnu.org" designates 209.51.188.17 as permitted sender) smtp.mailfrom="guix-patches-bounces+larch=yhetil.org@gnu.org" X-Migadu-Spam-Score: -1.81 Authentication-Results: aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=gmail.com header.s=20210112 header.b=RGhzhh5l; dmarc=fail reason="SPF not aligned (relaxed)" header.from=gmail.com (policy=none); spf=pass (aspmx1.migadu.com: domain of "guix-patches-bounces+larch=yhetil.org@gnu.org" designates 209.51.188.17 as permitted sender) smtp.mailfrom="guix-patches-bounces+larch=yhetil.org@gnu.org" X-Migadu-Queue-Id: 84C8236D77 X-Spam-Score: -1.81 X-Migadu-Scanner: scn0.migadu.com X-TUID: 83lphvTdSIuK Hi, On dim., 28 nov. 2021 at 18:27, Julien Lepiller 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 > +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