From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp10.migadu.com ([2001:41d0:2:4a6f::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms5.migadu.com with LMTPS id yMidNcmfE2NM/wAAbAwnHQ (envelope-from ) for ; Sat, 03 Sep 2022 20:41:14 +0200 Received: from aspmx1.migadu.com ([2001:41d0:2:4a6f::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp10.migadu.com with LMTPS id UAPcNMmfE2NVWAAAG6o9tA (envelope-from ) for ; Sat, 03 Sep 2022 20:41:13 +0200 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 93597B786 for ; Sat, 3 Sep 2022 20:41:13 +0200 (CEST) Received: from localhost ([::1]:57612 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1oUY4u-0007xb-QA for larch@yhetil.org; Sat, 03 Sep 2022 14:41:12 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:47486) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1oUY4l-0007xD-4O for guix-patches@gnu.org; Sat, 03 Sep 2022 14:41:03 -0400 Received: from debbugs.gnu.org ([209.51.188.43]:54325) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1oUY4k-0003Ng-QT for guix-patches@gnu.org; Sat, 03 Sep 2022 14:41:02 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1oUY4k-0007LK-9K for guix-patches@gnu.org; Sat, 03 Sep 2022 14:41:02 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#57540] [PATCH] Add ocaml-elpi (a dependency of coq-mathcomp-analysis) Resent-From: Julien Lepiller Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sat, 03 Sep 2022 18:41:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 57540 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Garek Dyszel Cc: 57540@debbugs.gnu.org Received: via spool by 57540-submit@debbugs.gnu.org id=B57540.166223044428196 (code B ref 57540); Sat, 03 Sep 2022 18:41:02 +0000 Received: (at 57540) by debbugs.gnu.org; 3 Sep 2022 18:40:44 +0000 Received: from localhost ([127.0.0.1]:43024 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1oUY4S-0007Kh-EG for submit@debbugs.gnu.org; Sat, 03 Sep 2022 14:40:44 -0400 Received: from lepiller.eu ([89.234.186.109]:53502) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1oUY4O-0007KX-KH for 57540@debbugs.gnu.org; Sat, 03 Sep 2022 14:40:43 -0400 Received: from lepiller.eu (localhost [127.0.0.1]) by lepiller.eu (OpenSMTPD) with ESMTP id d8fe000d; Sat, 3 Sep 2022 18:40:38 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed; d=lepiller.eu; h=date:from :to:cc:subject:message-id:in-reply-to:references:mime-version :content-type:content-transfer-encoding; s=dkim; bh=ox6TWUgPb88s kSOB7VAwSixZMt7C3pITidR8BjGCbeY=; b=Zre1ZZx7ohkYao4l+VOMA4l0i2cX wh2NBTR4frn8oSh1haS2r7Am2KtmAMK+IxAmCdX46V0JdSytMV+nw13g+yvIFIYA KQxJNEwP/ThJubjWeGBaTsvDaKVBr5c+mmfaTkfxNOrkR5O6ir9TpfHpKXZgPNYw HgVSJ85RUMZNar/UakdLMuUtoz94unZ8Nh8bpxQupf9DUxQrzriVr9qDuaptSNw4 WtG1TVeN3wxB/dC977yddmKDnI70vuSD6MOaOmn22o4C06nrGW2Z21dCYlGeZDYK LHDcMlum9a/3BJ0D0CE4hOr12z3ysxXD1jdEqp95jpf31yZUeTtmEPiE7A== Received: by lepiller.eu (OpenSMTPD) with ESMTPSA id 1ae6b595 (TLSv1.3:AEAD-AES256-GCM-SHA384:256:NO); Sat, 3 Sep 2022 18:40:37 +0000 (UTC) Date: Sat, 3 Sep 2022 20:40:35 +0200 From: Julien Lepiller Message-ID: <20220903204035.22e3b372@sybil.lepiller.eu> In-Reply-To: <79d544f7d8ba64b631a6f0f1d2ef0b08@disroot.org> References: <79d544f7d8ba64b631a6f0f1d2ef0b08@disroot.org> X-Mailer: Claws Mail 4.1.0 (GTK 3.24.30; x86_64-pc-linux-gnu) MIME-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit 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-To: larch@yhetil.org X-Migadu-Country: US ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=yhetil.org; s=key1; t=1662230473; 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=bFcVVW5XohwXfEHI2tbabjVJrbrW7do1woCdBRrKabs=; b=V+12cWgbJMxC7FCFfNqccRlMZkF9O4hftcgrWy42ojaEsaG5J5GVI/u9H9RJBgbl9m0AHZ p8KlXZzBnklItkLL0f+KVZ77AIihDiZU4fQDaJQhOTSdypfmuGUwwzq7omktxzcAC9lWwu VMDpYxmrQsrVwx9zkVFW8z9Dt9C82UikFG6BSaFoAQ0hQIYdgB9xDcchvd0vBJVRVixR9P ie8mOT8zeb6aZjoIBSIMIdJ5NBcdd8rPsiObEkohaOPtecd7iB3xcV1A36g1JFDEvGzrGr +Zdz8q7aG7OzQSOp1XhrgJQRhHw+Zk5NFjHNHtqutHv3Wt91drpV7PzXacL0NQ== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1662230473; a=rsa-sha256; cv=none; b=U6xHMm4Ww3FAfQk9IzMMPBLxuERJnSwfYOCXJ9JMdJ4G4ocVJtLIHU2g4lNCA1yBWnkkJS uBFNXMUcnxzjkc+piEd00zzUpgUhSZ6yG0loawCx0kmmAU3Xhrx4yQ9Ij2Cklhvm54bpfl /O2oZ4Jm+6bLgG66NKSzkwCJv61z9p1QIyt6yltjYZWx/rCKH3MBTAnePkZWurO63Gd9Bc 1K3UuzXsoaKr4+cxtszoj8jdZ0oXokVQAdpFg7zFJPrcDRIl4UGB/tDHQYyBQjPX5EACuv IfFrX/mLPuFXFWrUKRzSlX5GZRmHmVwmQOF+JUP7vJG3XMvSsMkqFP/ZhwHdUQ== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=lepiller.eu header.s=dkim header.b=Zre1ZZx7; 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: 5.93 Authentication-Results: aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=lepiller.eu header.s=dkim header.b=Zre1ZZx7; 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: 93597B786 X-Spam-Score: 5.93 X-Migadu-Scanner: scn0.migadu.com X-TUID: PbrD/gttRMne Hi Garek, thanks for the patches! As I understand it, these patches introduce 8 new packages, but I count only 7 (with this one which didn't make it as a part of the series). Could you split the last patch, so each new package has its own patch? Also, some points in your patches: For "Don't know about directory test", you can try with an argument: #:test-target "some-dir". This directory is the directory where tests are located. If there is no single directory, you can try #:test-target "." Descriptions should use our subset of texinfo. Basically, lists should look like: @itemize @item foo @item bar @end itemize and you can use @file, @code, etc as you see fit (to replace markdown's "`"). Whenever possible, we try not to rely on github tarballs, so it'd be best to use a git-reference in all your patches :) In coq-elpi: > + ;; Remove the useless line > + ;; "src/META.coq-elpi" > + ;; in file _CoqProject. > + ;; It does not affect > + ;; the success of compliation. should be "compilation". And then I wonder why you need that at all, if it doesn't change compilation result? > + #t)) Please don't use #t at the end of phases anymore. > + (replace 'check The gnu-build-system already runs "make test", doesn't it? Why do you need to replace this phase? In coq-mathcomp-hierarchy-builder: > + (replace 'check Instead of replacing this phase, maybe try #:test-target "test-suite" > + ;; Makefile.common has no references to tests at all > + ;; (yet). If that means that future versions will have tests (for instance if master has tests), maybe this should say it more explicitely. Once you fix all this, could you send a v2 series? Thank you!