From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp1 ([2001:41d0:2:bcc0::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms0.migadu.com with LMTPS id OCZ1LIrUpGF8OQAAgWs5BA (envelope-from ) for ; Mon, 29 Nov 2021 14:24:26 +0100 Received: from aspmx1.migadu.com ([2001:41d0:2:bcc0::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp1 with LMTPS id aNcGKIrUpGF7WgAAbx9fmQ (envelope-from ) for ; Mon, 29 Nov 2021 13:24:26 +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 F2357DD26 for ; Mon, 29 Nov 2021 14:24:25 +0100 (CET) Received: from localhost ([::1]:53126 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1mrgdt-0007RE-2T for larch@yhetil.org; Mon, 29 Nov 2021 08:24:25 -0500 Received: from eggs.gnu.org ([209.51.188.92]:41350) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1mrgbb-0005Rw-7w for guix-patches@gnu.org; Mon, 29 Nov 2021 08:22:08 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:54090) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1mrgbZ-0006HS-SO for guix-patches@gnu.org; Mon, 29 Nov 2021 08:22:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1mrgbZ-0002Ep-Oy for guix-patches@gnu.org; Mon, 29 Nov 2021 08:22:01 -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 13:22:01 +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.16381920988571 (code B ref 52164); Mon, 29 Nov 2021 13:22:01 +0000 Received: (at 52164) by debbugs.gnu.org; 29 Nov 2021 13:21:38 +0000 Received: from localhost ([127.0.0.1]:37403 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mrgbB-0002EB-Oa for submit@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 ) id 1mrgb7-0002Dw-V2 for 52164@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@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@tachikoma.lepiller.eu> <8635nfl2m6.fsf_-_@gmail.com> <592223CF-588B-44EF-A35F-9E9FDB3E4865@lepiller.eu> In-Reply-To: <592223CF-588B-44EF-A35F-9E9FDB3E4865@lepiller.eu> From: zimoun Date: Mon, 29 Nov 2021 14:21:16 +0100 Message-ID: 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=1638192266; 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=I8x8VTLrkiI0FdMzdrx67XifL9BAh6gJucYqaPKTu2Q=; b=dtUIc9ycXErmcU5UopIrEB3TXKKTe/uByh8GGvbN1K8MpdOiWJi7LWQiFMi6pxi/eOvY3V /yXXgN+RNZEsdO4mmAxCIrHA3Ly0WK63XGwc+yBjb+PVqY+JEnXrDOLijYloT/jgyy2vz6 eBHb9Tu96ZuVSawnFI2vqhHbsOW8qPdBTv6AUo3RIAfmqyzz+wxbORLLcFmJrbQHexcsx7 tP2rEdeaRKfO2qBzBxJ/v0rnp45zq14LaprhRILCTU3bh+Gijchc8bwsQbSIA9MnzIrs5H qwTSD7eNokH4u+mB3cZcgG8Yy/5dEAit8PZLUGoZ/8vZ/dVSwxKTexumXkVq1Q== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1638192266; a=rsa-sha256; cv=none; b=PgP71+62pdlFuLyk1LV4xnM2gz7inqHryaxVlax9ZyaPYlb2QkU9Pj3WFQfCbaJ1qOk+hq N3tbpQIUl/ZuoxArBR+bw85xofBsaUG9o8yQc+jbm2DVQVYsu4tzb4Dr4/mBBmxdYlM0TA v9FZ2iyoDvxTHD57slH+dQeQMA/NSYfdFhPKfnqs6uZdrZ+fDBCyOQ8mruAobzccxQuJ3e Dvxjzr4FAY/DvoT/5PrnRB7fVS4YvZy8vkU/ZUCar1rt9809DK2sRYjeRpP+9cpieUfubO r6lbELMTKg99UJVRMQuza5A5DQ/gcVjzwnYofaZYxBYh3w6OjWotnCvq7DZHfw== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=gmail.com header.s=20210112 header.b=ONtce3Cy; 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=ONtce3Cy; 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: F2357DD26 X-Spam-Score: -1.81 X-Migadu-Scanner: scn0.migadu.com X-TUID: 6BZTH2yopgvn Hi Julien, On Mon, 29 Nov 2021 at 13:30, Julien Lepiller 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@8.13.2. Or do you mean that coq-binums@8.13 is broken with coq@8.14? 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