From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp2.migadu.com ([2001:41d0:403:58f0::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms13.migadu.com with LMTPS id CC8MOhtN6GYtHQAAe85BDQ:P1 (envelope-from ) for ; Mon, 16 Sep 2024 15:22:04 +0000 Received: from aspmx1.migadu.com ([2001:41d0:403:58f0::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp2.migadu.com with LMTPS id CC8MOhtN6GYtHQAAe85BDQ (envelope-from ) for ; Mon, 16 Sep 2024 17:22:04 +0200 X-Envelope-To: larch@yhetil.org Authentication-Results: aspmx1.migadu.com; dkim=pass header.d=debbugs.gnu.org header.s=debbugs-gnu-org header.b=FYgLbi+2; dkim=fail ("headers rsa verify failed") header.d=foundation.xyz header.s=google header.b=tIGrmV1K; 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"; dmarc=fail reason="SPF not aligned (relaxed), DKIM not aligned (relaxed)" header.from=foundation.xyz (policy=none) ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=yhetil.org; s=key1; t=1726500123; 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=g7W0y6q76+r9IeJoh8fBK0gBkZQ6JoaEvTqhSK8fc1M=; b=LDVbC/ls7r0WEVOpJ3wTgHXgzidMotTXtGkElx2wpBMxMC5Ebf4f6/Yzea69uLxUTKvSTt b45d41cqxkcB/fTpK9dWT2jRnO2yN1Wma6MmMcxWoBg75FUXi06hDENEqvWQeto04kb+jZ asmnOTA1pRAMiQEPpjAxcUTIep0vz+ChuOPhxMhtZM1lFznx63Jw8gVDYKfz/wR5UWe93q gpdNfPfZ0VJkkPJbjA+dFJWqdTVWzYDg6A+FSRp2RrbdsFlaxodDtaletKLTZXU3tNDbjc kupCugGXSlkAH0B3C81iCHU8BOsOOTlsI45W0Tejf30g/hcj8HLraCYBYv2ebA== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=pass header.d=debbugs.gnu.org header.s=debbugs-gnu-org header.b=FYgLbi+2; dkim=fail ("headers rsa verify failed") header.d=foundation.xyz header.s=google header.b=tIGrmV1K; 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"; dmarc=fail reason="SPF not aligned (relaxed), DKIM not aligned (relaxed)" header.from=foundation.xyz (policy=none) ARC-Seal: i=1; s=key1; d=yhetil.org; t=1726500123; a=rsa-sha256; cv=none; b=PmNA4GP75waTjCT5m0C0IFb7Gg9ftldEiyg4ZR2WYXcNp7gE6NnStFr2f9+JvQKoBdxsxd dpeleenRdtfIMapvmk063dnQ6ExpblDhgKjGntIxoUlC+02tf0FcmgzOsFYXDNq5WS4j9f GOP5BiO3V/8CT8fLup2NUO3ZAgs3vn/Nb9yADwOWfMcYPrBOLeKA4E53dLQaFluqVgWAOj 0eT0chGQVSujUt+4Tqf81+V4eSSJfDj2MYI9bksBETV+oxTLh1CcF9b3kynycctmVjFM9A J0Mlg7oaulDtZyqe/X+87sCgYqWbDRDQMSNQXaH8NkpK7G72M7T4ainLGVDxEA== 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 A82DF86891 for ; Mon, 16 Sep 2024 17:22:03 +0200 (CEST) Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1sqDXz-0004Ux-E6; Mon, 16 Sep 2024 11:21:51 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1sqDXx-0004UY-B3 for guix-patches@gnu.org; Mon, 16 Sep 2024 11:21:49 -0400 Received: from debbugs.gnu.org ([2001:470:142:5::43]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1sqDXx-0005nE-1I for guix-patches@gnu.org; Mon, 16 Sep 2024 11:21:49 -0400 DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=debbugs.gnu.org; s=debbugs-gnu-org; h=Date:From:In-Reply-To:References:MIME-Version:To:Subject; bh=g7W0y6q76+r9IeJoh8fBK0gBkZQ6JoaEvTqhSK8fc1M=; b=FYgLbi+2NKFRA0mCTL1cD+yS2NAr+jwMiZ2aaUQMEgamPLqpSZOQvJTQHN4Bt6dZihsPeD88w01hsE9c/nxXcH8G28P0+iLhEdITnte4ojo7AxSXETf5UCmY3iwGC3RcMHoKxikCdhHUNYi1b5fIHQkXaF65U0NC6IxOCUFiHOo1Nx2/OQUKy0oGGotS68/nPWgKQ6pcWxDIMpuu34tUT9geWjPMAtdx+NocrP8r7mCavFyz9WJGNa5Vy8vD7W+UJjV4AilG7Q9khbPbR0SpgBEtvFm1AuewyULiJ+aeoxL9GX6x+uw+picA2INLs/fKQYPoHKbIj6W+Dnkv/YCo6A==; Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1sqDYA-0006NR-Cs for guix-patches@gnu.org; Mon, 16 Sep 2024 11:22:02 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#73237] [PATCH] gnu: Add coq-ceres. Resent-From: Jean-Pierre De Jesus Diaz Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Mon, 16 Sep 2024 15:22:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 73237 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Antero Mejr Cc: 73237@debbugs.gnu.org Received: via spool by 73237-submit@debbugs.gnu.org id=B73237.172650006424419 (code B ref 73237); Mon, 16 Sep 2024 15:22:02 +0000 Received: (at 73237) by debbugs.gnu.org; 16 Sep 2024 15:21:04 +0000 Received: from localhost ([127.0.0.1]:53048 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1sqDXE-0006Ll-FH for submit@debbugs.gnu.org; Mon, 16 Sep 2024 11:21:04 -0400 Received: from mail-ot1-f52.google.com ([209.85.210.52]:61634) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1sqDXA-0006L6-UB for 73237@debbugs.gnu.org; Mon, 16 Sep 2024 11:21:03 -0400 Received: by mail-ot1-f52.google.com with SMTP id 46e09a7af769-710e910dd7dso2779027a34.2 for <73237@debbugs.gnu.org>; Mon, 16 Sep 2024 08:20:47 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=foundation.xyz; s=google; t=1726499982; x=1727104782; darn=debbugs.gnu.org; h=content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:from:to:cc:subject:date :message-id:reply-to; bh=g7W0y6q76+r9IeJoh8fBK0gBkZQ6JoaEvTqhSK8fc1M=; b=tIGrmV1KOAA5M8UgAJsmGXbpftZw7E3gfpSR3gow5a4EmWTxP7I2zGqCo0z9OTW479 0WRtNp1bBBeSYOTYfbG6Df9HvD3XqPE7ty+cRs54lSrcSYn2AUM0fCKuAo3CMZi+cSZP UGhF6bpD233oJWCQiOEpeKzxjR/AI+1lOUWvRf5d7OJ4WsgSFPXohsf+xiw8w7BCbwHu T9o2rX+nYVXId39oeQ8GRd+Pgb9BjBBfcwqAsMX4nL44z6ql5yV1MF4nBqb0un6lFPr+ ukdY99ocWZVrMFLqzOcSVkkJUqBBo7YXypb3ywBSgtDEdYOQreIx9PmCOmbbQjQpZK// 6XwQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1726499982; x=1727104782; h=content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:x-gm-message-state:from:to:cc :subject:date:message-id:reply-to; bh=g7W0y6q76+r9IeJoh8fBK0gBkZQ6JoaEvTqhSK8fc1M=; b=BwRoWFIzQ9iaBC0I/5IM9Ob8nT6h/W2+totR3Lf5XknE8EZrfs3YxU5Hgh4R4jtlzu GHxjEIKtpEGyGvxo0Uo3xATR/06JsndAmGLPcpp1RDH6O8+5JkvmbG6WHoXfKTp0pKNz gycspQmlSuweGZ/D1CCBHHmgdUVV8EAFm+p5qqVT2ggj07Jyp8A/UmrKvKtqeDgxZk0q WYpim+r60ynp2tQ9KRCIm+PeVBc5tiNRH3qIYRL5/YjPgEKdUTGmYhJ94yqSo5BScmgp nh39l9rBwSH406Xvud+FTXwuyuHHtxGhX/ztTUt7PS6y9SgIeTeT3fkyd4e7Y6EDmn/G njkg== X-Gm-Message-State: AOJu0Yx5359+LVKIQzIj4rnzfxzxxCJNAqZ4P+TB4R9LQEPITB8WMaVy vrdBNauKqVqEaDsZjAg3YB25gezHBPaUNF8K98OKgpegzNfSZLcXDlZeRjF1tk6lnDjc8F+d5CY BSsQVPBiZRd/wHcSdW0yhPhYuA7Vd4lfcgC4rTw== X-Google-Smtp-Source: AGHT+IFsMAMu7C9RhWzZvsrItmCr3S10EYeQL/y+gFRRNfrCxJdIj7uPf00oG6sG4GlgEBF+G+w5693tfVU7741K9vI= X-Received: by 2002:a05:6808:17a9:b0:3e0:51f9:996b with SMTP id 5614622812f47-3e071a7a6bamr11016998b6e.9.1726499981745; Mon, 16 Sep 2024 08:19:41 -0700 (PDT) MIME-Version: 1.0 References: <87o74nr5p6.fsf@antr.me> In-Reply-To: <87o74nr5p6.fsf@antr.me> From: Jean-Pierre De Jesus Diaz Date: Mon, 16 Sep 2024 15:19:31 +0000 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-bounces+larch=yhetil.org@gnu.org X-Migadu-Flow: FLOW_IN X-Migadu-Country: US X-Migadu-Queue-Id: A82DF86891 X-Migadu-Scanner: mx11.migadu.com X-Spam-Score: -10.44 X-Migadu-Spam-Score: -10.44 X-TUID: NHL1HOt7jEk/ >Yes. For some reason, the coq-mathcomp-bigenough package propagates coq, >and coq-stdpp has it in inputs, so I was unsure where to put it. I think >those packages should be updated to have coq as a native-input as well. That's odd, it also propagates `which' when it shouldn't, only coq-mathcomp should be propagated. On Mon, Sep 16, 2024 at 3:14=E2=80=AFPM Antero Mejr wrote: > > Jean-Pierre De Jesus Diaz writes: > > > I've also recently packaged coq-ceres for Guix in my personal channel, > > it is a shorter version: > > There's a lot of useful stuff there, it would be great to get it > upstreamed. Unfortunately I do not have commit access. > > > I'd also adapt the install-doc to use the install-doc target of the gen= erated > > Makefile like this: > > That sounds good, I will update the patch. > > > Coq does not need to be propagated, only needs to be a native-input. > > Yes. For some reason, the coq-mathcomp-bigenough package propagates coq, > and coq-stdpp has it in inputs, so I was unsure where to put it. I think > those packages should be updated to have coq as a native-input as well.