From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp1 ([2001:41d0:8:6d80::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms0.migadu.com with LMTPS id GGPHFxDIpGH3DwAAgWs5BA (envelope-from ) for ; Mon, 29 Nov 2021 13:31:12 +0100 Received: from aspmx1.migadu.com ([2001:41d0:8:6d80::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp1 with LMTPS id qBp/ExDIpGHjNwAAbx9fmQ (envelope-from ) for ; Mon, 29 Nov 2021 12:31:12 +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 EED7F1CD10 for ; Mon, 29 Nov 2021 13:31:11 +0100 (CET) Received: from localhost ([::1]:37438 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1mrfoN-0008W7-1V for larch@yhetil.org; Mon, 29 Nov 2021 07:31:11 -0500 Received: from eggs.gnu.org ([209.51.188.92]:51232) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1mrfoE-0008TB-TU for guix-patches@gnu.org; Mon, 29 Nov 2021 07:31:02 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:53995) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1mrfoE-0005AO-KB for guix-patches@gnu.org; Mon, 29 Nov 2021 07:31:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1mrfoE-0008AR-B8 for guix-patches@gnu.org; Mon, 29 Nov 2021 07:31:02 -0500 X-Loop: help-debbugs@gnu.org Subject: [bug#52164] [PATCH] gnu: coq: Update to 8.14.0. Resent-From: Julien Lepiller Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Mon, 29 Nov 2021 12:31: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: zimoun Cc: 52164@debbugs.gnu.org Received: via spool by 52164-submit@debbugs.gnu.org id=B52164.163818901628740 (code B ref 52164); Mon, 29 Nov 2021 12:31:02 +0000 Received: (at 52164) by debbugs.gnu.org; 29 Nov 2021 12:30:16 +0000 Received: from localhost ([127.0.0.1]:37308 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mrfnM-0007K6-Ep for submit@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 ) id 1mrfnK-0007ER-Qv for 52164@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 User-Agent: K-9 Mail for Android In-Reply-To: <8635nfl2m6.fsf_-_@gmail.com> References: <20211128174408.747bccba@tachikoma.lepiller.eu> <8635nfl2m6.fsf_-_@gmail.com> Message-ID: <592223CF-588B-44EF-A35F-9E9FDB3E4865@lepiller.eu> 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=1638189072; 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=qCDgoCbuPbJBj0Gbjvj33SBemebVErPuCHXqPiV2YKw=; b=RqocmqguJ6jZFpfxKOu+Glxtj5SMUsSxfeQDlGBhwRdig3XsmV9ypV2pB61Jn6PbUMGtnY qte8QqB0eCmHhb70I6iSqRGwQBFPppAP3ityNEKc/7LpA59/d9nj3Pm3nIx2rnikOAM56X ++rITLBsHjpX1GpJEPmAYGl6ZD8AT++aQLiov+UHee0+qcjS830K9yqbpg6DSPTWaXUIHa FkOkQkRZ9vYdArFSxIviBmMOYotQTcJ0R6Tfa+R8fgFaE7/W8xpvmwFW2pYTSBIhX/uagP DdNjcm3nspGheikHhRtMbkoq6jAc6BG6k9UNfSj25Iq7cuqCbV5464VEQw71ZQ== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1638189072; a=rsa-sha256; cv=none; b=iCel0jGF0y/LRfX3JH8vqUrMLyDrUP9E7UrTkvKhW+kEgBEQpj/Rz+Pe/KwklaLbqscARj mFDnDe0WSDT40IPNQfN/XdlYYZJYjOPc9/cj00eZdBc2yWuAFokz09MtLRuVdVFW9POYzR VBV56NR4GmalshxQm1YS1TEZm8vEC4OzIYTK1B2Dh7du2mICQumA02sjBRon0DQFW7iDHV I4cJykh9ZZQ6JBEqtXHaAmD+96m8GzY+E9MUFw3rsKYQQDVruEbyXPB0CeE2MErbH+Zxw2 5gZ9cx0kPvXuS2r4J2AImFdoCkVHe4+7Fnl9WKMkssVfRw3xxgN7H+nyZfP5+g== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=lepiller.eu header.s=dkim header.b=fR6y13Nw; dmarc=fail reason="SPF not aligned (relaxed)" header.from=lepiller.eu (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=lepiller.eu header.s=dkim header.b=fR6y13Nw; dmarc=fail reason="SPF not aligned (relaxed)" header.from=lepiller.eu (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: EED7F1CD10 X-Spam-Score: -1.81 X-Migadu-Scanner: scn0.migadu.com X-TUID: Cc8wAXM0cgQQ Le 29 novembre 2021 04:42:25 GMT-05:00, zimoun a =C3=A9crit=C2=A0: >Hi, > >On dim=2E, 28 nov=2E 2021 at 18:27, Julien Lepiller 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 >> +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