Received: (at 73237) by debbugs.gnu.org; 16 Sep 2024 15:31:59 +0000 From debbugs-submit-bounces <at> debbugs.gnu.org Mon Sep 16 11:31:59 2024 Received: from localhost ([127.0.0.1]:53076 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>) id 1sqDhm-0006xo-Hh for submit <at> debbugs.gnu.org; Mon, 16 Sep 2024 11:31:58 -0400 Received: from mail-ot1-f50.google.com ([209.85.210.50]:58434) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from <jean@HIDDEN>) id 1sqDhk-0006xa-L7 for 73237 <at> debbugs.gnu.org; Mon, 16 Sep 2024 11:31:57 -0400 Received: by mail-ot1-f50.google.com with SMTP id 46e09a7af769-710e14e2134so2202329a34.0 for <73237 <at> debbugs.gnu.org>; Mon, 16 Sep 2024 08:31:43 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=foundation.xyz; s=google; t=1726500638; x=1727105438; 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=PnwbGDI89gJpQpf9AC38REpI3qUvfdK48QsMaVplArM=; b=tTU3RF7ytvsqQlQtDC59k/0knEP+daDMjwMOCgsLACTjYkSR4nDP1rlS2LR4LVik+d bBP7O3KOyPoQ1oOvGhjAuYKBJLMgV8nXrhI3W7ujlJCNx5HYkxCHh/p3izgsQOSrJAWp zceEKv6bJGNVKgDwRdrjaxajpSSF7ZcvpN6gelEFY7ytgdcjzl9ALgPKxFWp/XOvuUxw 1c8XguUVyXUALwrWcwAsliqcWdD9RzcodJRZpxHZoNlg3gPWYgiEaqzs/qzgpGwHu3lZ EkD7DMqT44jTUPVAUTxf+XiBQP1W69VfqbOipQSakntu+cHvRaSidlqo/H69PnwK8iXs BHpA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1726500638; x=1727105438; 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=PnwbGDI89gJpQpf9AC38REpI3qUvfdK48QsMaVplArM=; b=b3sQ+NQOC4Y9UleDIMpPukyifyJ6MSKu8oIN3xg0knBOBzSYLs6FwNxj1gZsP6uPD4 0ck1AeEXwBWz7w/TWsm9UsqQDbw9X2yUAuIj7iErfAfVIb5/S09eR+yqVCwVOnR37VDd hbPV7R/Luf52xmCYnkW+ettLZ1AgPMn/cZtEB5JZYIog5MTnWDHcwtAhdqJlfwF+MfDN tYtopAo5eo5Vx/QthUMh7mir4bJ2HQyIE3k2L25OWXjkmDGPmUxvaIwIdl6MdXMVvcdC oMOtrW2fBJS7scUQyqmYtlPwfdfBL9hnOczndwZA/+rRnx71W/E2pqkSCRBgw6VYI0yl 5d/g== X-Gm-Message-State: AOJu0Yzb87244BMfLiSkDqVYr2U6aFXmvtaeNZgAeYHcX6iL3GiJk/yW EyLUv3aaTGBwmeeZpCf78SlX5Pa03o+ef/B0WF9qW5ZiS0BZRMJL1HeninZ/16ZL7AWD1oOdocD zQY/dNyUBYo/7iRW4uu6NkGozE/hU6u11D21QvHCluXLEtIez X-Google-Smtp-Source: AGHT+IHG2PnRzFlTbYJMzigugC+RAH3nNrCaaFdAgCXL9RCPk4/gmJ0s2NZGqf3nfIkNcgpcTwpZE2fWEpYZVkJKCNg= X-Received: by 2002:a05:6830:270e:b0:710:dec2:df70 with SMTP id 46e09a7af769-711094baecamr10486984a34.24.1726500637656; Mon, 16 Sep 2024 08:30:37 -0700 (PDT) MIME-Version: 1.0 References: <CAG1gdUpqdcc7Q1jMoHnCYEcZVw=V9WWB3RFZ2bJFgd3tPUcx=w@HIDDEN> <87o74nr5p6.fsf@HIDDEN> <CAG1gdUqp6u=2kuVBhCFsdFSODYR7+XjVdWatq8AUXgVNC3MnnA@HIDDEN> In-Reply-To: <CAG1gdUqp6u=2kuVBhCFsdFSODYR7+XjVdWatq8AUXgVNC3MnnA@HIDDEN> From: Jean-Pierre De Jesus Diaz <jean@HIDDEN> Date: Mon, 16 Sep 2024 15:30:27 +0000 Message-ID: <CAG1gdUrRDfpsDgqSEtkAU1+sYkdEJUHaSeLiZZDA-UmT=ikZRA@HIDDEN> Subject: Re: [PATCH] gnu: Add coq-ceres. To: Antero Mejr <mail@HIDDEN> Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Spam-Score: -0.0 (/) X-Debbugs-Envelope-To: 73237 Cc: 73237 <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 (-) >That's odd, it also propagates `which' when it shouldn't, only coq-mathcom= p >should be propagated. I've sent a few patches to fix this: <https://issues.guix.gnu.org/73298> On Mon, Sep 16, 2024 at 3:19=E2=80=AFPM Jean-Pierre De Jesus Diaz <jean@HIDDEN> wrote: > > >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-mathco= mp > should be propagated. > > On Mon, Sep 16, 2024 at 3:14=E2=80=AFPM Antero Mejr <mail@HIDDEN> wrote: > > > > Jean-Pierre De Jesus Diaz <jean@HIDDEN> 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 g= enerated > > > 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 thin= k > > those packages should be updated to have coq as a native-input as well.
guix-patches@HIDDEN:bug#73237; Package guix-patches.
Full text available.Received: (at 73237) by debbugs.gnu.org; 16 Sep 2024 15:21:04 +0000 From debbugs-submit-bounces <at> debbugs.gnu.org Mon Sep 16 11:21:04 2024 Received: from localhost ([127.0.0.1]:53048 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>) id 1sqDXE-0006Ll-FH for submit <at> 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 <jean@HIDDEN>) id 1sqDXA-0006L6-UB for 73237 <at> 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 <at> 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: <CAG1gdUpqdcc7Q1jMoHnCYEcZVw=V9WWB3RFZ2bJFgd3tPUcx=w@HIDDEN> <87o74nr5p6.fsf@HIDDEN> In-Reply-To: <87o74nr5p6.fsf@HIDDEN> From: Jean-Pierre De Jesus Diaz <jean@HIDDEN> Date: Mon, 16 Sep 2024 15:19:31 +0000 Message-ID: <CAG1gdUqp6u=2kuVBhCFsdFSODYR7+XjVdWatq8AUXgVNC3MnnA@HIDDEN> Subject: Re: [PATCH] gnu: Add coq-ceres. To: Antero Mejr <mail@HIDDEN> Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Spam-Score: -0.0 (/) X-Debbugs-Envelope-To: 73237 Cc: 73237 <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 (-) >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 <mail@HIDDEN> wrote: > > Jean-Pierre De Jesus Diaz <jean@HIDDEN> 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.
guix-patches@HIDDEN:bug#73237; Package guix-patches.
Full text available.Received: (at 73237) by debbugs.gnu.org; 16 Sep 2024 15:15:14 +0000 From debbugs-submit-bounces <at> debbugs.gnu.org Mon Sep 16 11:15:14 2024 Received: from localhost ([127.0.0.1]:53038 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>) id 1sqDRa-0005uZ-7M for submit <at> debbugs.gnu.org; Mon, 16 Sep 2024 11:15:14 -0400 Received: from smtp.forwardemail.net ([149.28.215.223]:8991) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from <SRS0=4762=QP=antr.me=mail@HIDDEN>) id 1sqDRX-0005u2-AW for 73237 <at> debbugs.gnu.org; Mon, 16 Sep 2024 11:15:12 -0400 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=antr.me; h=Content-Type: MIME-Version: Message-ID: Date: References: In-Reply-To: Subject: Cc: To: From; q=dns/txt; s=fe-d5cf982890; t=1726499690; bh=Uv76OqNpTfeK2xVkuajBPo9zW2jr1UFs/AxjA9XrKSo=; b=F3COaCQYlL9q1STA32E9nlmZSU+89j2nRkUjfdir82SBxXwTt3ol/jj7TR9qdXEsa637TGeQ/ 2MYfmOXIVd6liQhuK9I9drg485JHlrEb3VOsmc+/XgrsIReZHp6S8UkQ7do2pM1IBmijspKMjcu zbK6tV5GuX9CPkFxryyVar8= From: Antero Mejr <mail@HIDDEN> To: Jean-Pierre De Jesus Diaz <jean@HIDDEN> Subject: Re: [PATCH] gnu: Add coq-ceres. In-Reply-To: <CAG1gdUpqdcc7Q1jMoHnCYEcZVw=V9WWB3RFZ2bJFgd3tPUcx=w@HIDDEN> (Jean-Pierre De Jesus Diaz's message of "Mon, 16 Sep 2024 14:54:07 +0000") References: <CAG1gdUpqdcc7Q1jMoHnCYEcZVw=V9WWB3RFZ2bJFgd3tPUcx=w@HIDDEN> Date: Mon, 16 Sep 2024 15:14:45 +0000 Message-ID: <87o74nr5p6.fsf@HIDDEN> User-Agent: Gnus/5.13 (Gnus v5.13) MIME-Version: 1.0 Content-Type: text/plain X-Report-Abuse-To: abuse@HIDDEN X-Report-Abuse: abuse@HIDDEN X-Complaints-To: abuse@HIDDEN X-ForwardEmail-Version: 0.4.40 X-ForwardEmail-Sender: rfc822; mail@HIDDEN, smtp.forwardemail.net, 149.28.215.223 X-ForwardEmail-ID: 66e84b67d1181a3e5884d69b X-Spam-Score: -0.0 (/) X-Debbugs-Envelope-To: 73237 Cc: 73237 <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 (-) Jean-Pierre De Jesus Diaz <jean@HIDDEN> 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 generated > 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.
guix-patches@HIDDEN:bug#73237; Package guix-patches.
Full text available.
Received: (at 73237) by debbugs.gnu.org; 16 Sep 2024 14:55:39 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Mon Sep 16 10:55:39 2024
Received: from localhost ([127.0.0.1]:53023 helo=debbugs.gnu.org)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
id 1sqD8d-0004qC-0J
for submit <at> debbugs.gnu.org; Mon, 16 Sep 2024 10:55:39 -0400
Received: from mail-vs1-f54.google.com ([209.85.217.54]:53384)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <jean@HIDDEN>) id 1sqD8a-0004pr-TX
for 73237 <at> debbugs.gnu.org; Mon, 16 Sep 2024 10:55:37 -0400
Received: by mail-vs1-f54.google.com with SMTP id
ada2fe7eead31-49bd6c284bcso912746137.2
for <73237 <at> debbugs.gnu.org>; Mon, 16 Sep 2024 07:55:23 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
d=foundation.xyz; s=google; t=1726498458; x=1727103258; darn=debbugs.gnu.org;
h=cc:to:subject:message-id:date:from:mime-version:from:to:cc:subject
:date:message-id:reply-to;
bh=JLZ/q4QMBTFz3XAKG0PYYUbuEsJGs2+pbkF43vtzV0E=;
b=pjInmpbKmy72nC0IpKfaCSy8Jc5gr6STocjDCh7K7PkIrR0iWgtBTagJ7gcUCjUlaO
EGMNS8ihpcgIZfDkt4oYm+dJYd/PaFNebT/HSVxGsfNwHohIfTlh/3GEd4MoND/2QCUP
XSegdu7fnJcPE+QEAliz9UHC8briACxVPyqVtdBpU0ZtKdQPZm4agMP5XKcO1RY/rai2
nXI7+S0PJqii1Vuwss0jM/txqU/ydpCYbLMfQ0dvVjmB+rh1fVmYhTEUnk8SEcZGHF5/
TweaeitkPr2dZ/agwSH4RmfXU+BXpcGfcYOj99uOu7HhQ1Ew1tN4J83FG7oWUdDueMXu
ULpg==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
d=1e100.net; s=20230601; t=1726498458; x=1727103258;
h=cc:to:subject:message-id:date:from:mime-version:x-gm-message-state
:from:to:cc:subject:date:message-id:reply-to;
bh=JLZ/q4QMBTFz3XAKG0PYYUbuEsJGs2+pbkF43vtzV0E=;
b=sUuWDtymNzjnIVM1jKUXs3X1vcIOrl2Ob//g5gQETU69cVOCxibUQm18wod3kQXVd5
+rn20CXFUXatWX24Hcr2zxxAuhpIYcsgxYuNJfDySw9BzDxtvPAKAJq92yrxT/poAp64
x35i57iAfCEC2vDy6mPkNPd8oQxZ6byxNWJtqw57WjOjcFXgAbNi7Rfe6XtlzdhU/M7t
81zYeNTvQFps+H6wKg9u4D8V/K6X/WMMry/m2Kw5IgG7PwqUHW0Xa/VDj8O1owa3terH
oqI5hNEanSR9WhbkcYTtY4sjMhH74CxV2gtnziTUSox2cjXwwQOO2iBAMxKo63oQHKpE
Wbww==
X-Gm-Message-State: AOJu0YzRBbtjw67gB8WQWgg059HHgJZq4Qh0aSnQlY9H8Wq314xxOdYG
eE1tcX0b7/tfNYCMG1UGHifGr65pUMY2c1fp2AVblEAciSeLA+BC+R4aa4/aQ/kOtc1YkTITctj
wzyhjA13j3VNK17kFEzap2ANvIuzaQHxlG+Ozq2dc6fQ8t+8H
X-Google-Smtp-Source: AGHT+IFP7XRVLBNCnXdJAbROLRu0RfXzjfNON7cmiqibZ5SSWz9uDhHkxMPJ7S+UfkmqiAslh6654BKaRGxaYdwL4uc=
X-Received: by 2002:a05:6102:390b:b0:49b:e62d:b610 with SMTP id
ada2fe7eead31-49d4f612e9cmr7515765137.15.1726498457725; Mon, 16 Sep 2024
07:54:17 -0700 (PDT)
MIME-Version: 1.0
From: Jean-Pierre De Jesus Diaz <jean@HIDDEN>
Date: Mon, 16 Sep 2024 14:54:07 +0000
Message-ID: <CAG1gdUpqdcc7Q1jMoHnCYEcZVw=V9WWB3RFZ2bJFgd3tPUcx=w@HIDDEN>
Subject: Re: [PATCH] gnu: Add coq-ceres.
To: 73237 <at> debbugs.gnu.org
Content-Type: text/plain; charset="UTF-8"
X-Spam-Score: -0.0 (/)
X-Debbugs-Envelope-To: 73237
Cc: mail@HIDDEN
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 (-)
Hello,
I've also recently packaged coq-ceres for Guix in my personal channel,
it is a shorter version:
<https://github.com/jeandudey/guix-formal-verification/blob/25e9444861229f8345b7baea0a2251f5fd2c7fa8/formal-verification/packages/coq.scm#L46-L73>
I'd also adapt the install-doc to use the install-doc target of the generated
Makefile like this:
(arguments
(list #:test-target "test"
#:make-flags
#~(list (string-append "COQLIBINSTALL=" #$output
"/lib/coq/user-contrib")
(string-append "COQDOCINSTALL=" #$output
"/share/doc/" #$name "-" #$version))
#:phases
#~(modify-phases %standard-phases
(delete 'configure)
(add-after 'install 'install-documentation
(lambda* (#:key make-flags #:allow-other-keys)
(apply invoke "make" "install-doc" make-flags))))))
The license of the channel is GPL-3.0-or-later so feel free to take
inspiration from it to contribute to Guix.
>+ (propagated-inputs (list coq))
Coq does not need to be propagated, only needs to be a native-input.
guix-patches@HIDDEN:bug#73237; Package guix-patches.
Full text available.
Received: (at submit) by debbugs.gnu.org; 13 Sep 2024 20:55:50 +0000
From debbugs-submit-bounces <at> debbugs.gnu.org Fri Sep 13 16:55:50 2024
Received: from localhost ([127.0.0.1]:44342 helo=debbugs.gnu.org)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <debbugs-submit-bounces <at> debbugs.gnu.org>)
id 1spDKX-0000Ev-Je
for submit <at> debbugs.gnu.org; Fri, 13 Sep 2024 16:55:49 -0400
Received: from lists.gnu.org ([209.51.188.17]:52338)
by debbugs.gnu.org with esmtp (Exim 4.84_2)
(envelope-from <SRS0=0bc9=QM=antr.me=mail@HIDDEN>)
id 1spDKW-0000Em-3k
for submit <at> debbugs.gnu.org; Fri, 13 Sep 2024 16:55:48 -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 <SRS0=0bc9=QM=antr.me=mail@HIDDEN>)
id 1spDKM-0008Ly-3v
for guix-patches@HIDDEN; Fri, 13 Sep 2024 16:55:38 -0400
Received: from smtp.forwardemail.net ([207.246.76.47])
by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128)
(Exim 4.90_1)
(envelope-from <SRS0=0bc9=QM=antr.me=mail@HIDDEN>)
id 1spDKK-00042E-Aq
for guix-patches@HIDDEN; Fri, 13 Sep 2024 16:55:37 -0400
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=antr.me;
h=Content-Type: MIME-Version: Message-ID: Date: Subject: Cc: To: From;
q=dns/txt; s=fe-d5cf982890; t=1726260932;
bh=EURW1wpamsHy6ZzF6X2f+PVMEbNSYGo7EshhqQSKlus=;
b=oxaMWWZ+40hZoa3prv/IrQquMtkKVX4EDRsuc7OvGQtVq7hjG+8HeGmzCRbwvBohuwqGxFUwc
HNx9KTLLjaxbrCZKFzeEA6BzwniDuQegZ9Ws/JgMn1bI7VxBSo6ASyQ7KR+rA5vGhljP+ARBvxb
HldmpOWB3rKk15nZadF9Q/Y=
From: Antero Mejr <mail@HIDDEN>
To: guix-patches@HIDDEN
Subject: [PATCH] gnu: Add coq-ceres.
Date: Fri, 13 Sep 2024 20:55:28 +0000
Message-ID: <87zfob1dfj.fsf@HIDDEN>
User-Agent: Gnus/5.13 (Gnus v5.13)
MIME-Version: 1.0
Content-Type: text/plain
X-Report-Abuse-To: abuse@HIDDEN
X-Report-Abuse: abuse@HIDDEN
X-Complaints-To: abuse@HIDDEN
X-ForwardEmail-Version: 0.4.40
X-ForwardEmail-Sender: rfc822; mail@HIDDEN, smtp.forwardemail.net,
207.246.76.47
X-ForwardEmail-ID: 66e4a6c16c57d9a68975c7e2
Received-SPF: pass client-ip=207.246.76.47;
envelope-from=SRS0=0bc9=QM=antr.me=mail@HIDDEN;
helo=smtp.forwardemail.net
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.4 (-)
X-Debbugs-Envelope-To: submit
Cc: pukkamustard@HIDDEN, julien@HIDDEN
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.4 (--)
* gnu/packages/coq.scm (coq-ceres): New variable.
Change-Id: I366aa3ad38a25bbcbaa70874241a22fb45d41938
---
gnu/packages/coq.scm | 54 ++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 54 insertions(+)
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 31d1e8d51d..6417b3ea48 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -777,3 +777,57 @@ (define-public coq-mathcomp-bigenough
purposes as @code{bigenough} will be subsumed by the near tactics. The
formalization is based on the Mathematical Components library.")
(license license:cecill-b)))
+
+(define-public coq-ceres
+ (package
+ (name "coq-ceres")
+ (version "0.4.1")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/Lysxia/coq-ceres")
+ (commit version)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
+ "080nldsxmrxdan6gd0dvdgswn3gkwpy5hdqwra6wlmh8zzrs9z7n"))))
+ (build-system gnu-build-system)
+ (arguments
+ (list #:test-target "test"
+ #:make-flags #~(list "-f" "Makefile.coq"
+ (string-append "COQLIBINSTALL=" #$output
+ "/lib/coq/user-contrib")
+ "NO_TEST=1"
+ "COQTOP=coqtop")
+ #:phases #~(modify-phases %standard-phases
+ ;; Need to generate Makefile.coq
+ (replace 'configure
+ (lambda _
+ (invoke "coq_makefile" "-f" "_CoqProject.classic"
+ "-o" "Makefile.coq")))
+ (add-after 'build 'build-doc
+ (lambda* (#:key make-flags #:allow-other-keys)
+ (apply invoke "make" "html" make-flags)))
+ (replace 'check
+ (lambda* (#:key tests? test-target parallel-build?
+ make-flags #:allow-other-keys)
+ (when tests?
+ (apply invoke "make"
+ "-j" (number->string
+ (if parallel-build?
+ (parallel-job-count)
+ 1))
+ test-target make-flags))))
+ (add-after 'install 'install-doc
+ (lambda _
+ (let ((doc (string-append #$output
+ "/share/doc/ceres")))
+ (mkdir-p doc)
+ (copy-recursively "html" doc)))))))
+ (propagated-inputs (list coq))
+ (home-page "https://gitlab.mpi-sws.org/iris/actris")
+ (synopsis "Coq library for serialization to S-expressions")
+ (description
+ "This package provides a Coq library that allows for serialization and
+deserialization of S-expression data.")
+ (license license:bsd-3)))
base-commit: 0e0d9bc91f20ac6dda439ab09330f0163eb9bf42
--
2.46.0
Antero Mejr <mail@HIDDEN>:guix-patches@HIDDEN.
Full text available.guix-patches@HIDDEN:bug#73237; Package guix-patches.
Full text available.
GNU bug tracking system
Copyright (C) 1999 Darren O. Benham,
1997 nCipher Corporation Ltd,
1994-97 Ian Jackson.