From unknown Sun Jun 22 00:59:42 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#72730] [PATCH 0/2] coq: Update to 8.18.0. Resent-From: Jean-Pierre De Jesus DIAZ Original-Sender: "Debbugs-submit" Resent-CC: julien@lepiller.eu, pukkamustard@posteo.net, guix-patches@gnu.org Resent-Date: Tue, 20 Aug 2024 10:30:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: report 72730 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 72730@debbugs.gnu.org Cc: Jean-Pierre De Jesus DIAZ , Julien Lepiller , pukkamustard X-Debbugs-Original-To: guix-patches@gnu.org X-Debbugs-Original-Xcc: Julien Lepiller , pukkamustard Received: via spool by submit@debbugs.gnu.org id=B.172414978821357 (code B ref -1); Tue, 20 Aug 2024 10:30:02 +0000 Received: (at submit) by debbugs.gnu.org; 20 Aug 2024 10:29:48 +0000 Received: from localhost ([127.0.0.1]:59922 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1sgM7Y-0005YP-4y for submit@debbugs.gnu.org; Tue, 20 Aug 2024 06:29:48 -0400 Received: from lists.gnu.org ([209.51.188.17]:44258) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1sgM7V-0005YG-LA for submit@debbugs.gnu.org; Tue, 20 Aug 2024 06:29:46 -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 1sgM6o-0004OH-Co for guix-patches@gnu.org; Tue, 20 Aug 2024 06:29:02 -0400 Received: from mail-wm1-x32d.google.com ([2a00:1450:4864:20::32d]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1sgM6m-0004ER-QG for guix-patches@gnu.org; Tue, 20 Aug 2024 06:29:02 -0400 Received: by mail-wm1-x32d.google.com with SMTP id 5b1f17b1804b1-428119da952so42815685e9.0 for ; Tue, 20 Aug 2024 03:28:59 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=foundation.xyz; s=google; t=1724149738; x=1724754538; darn=gnu.org; h=content-transfer-encoding:mime-version:message-id:date:subject:cc :to:from:from:to:cc:subject:date:message-id:reply-to; bh=XoSere6M7Ku9MAKY1jptLpeneDv23NmGppM5OqBX/Bo=; b=dzqK7XjVknpnJi4PO7QIc6gh7B+F/L4FCZ7oktS89ROV5gqfZpHWWkLPcuttX43ksT i7Gng/qN03CEXktxDT0aDqg1GFsQIhIdzUinLiRS3EFHgQ5eHH5CoeVndcAh3LXaYJpv wK7FUt17WKN8hFX6bv3GGVk4msT1aOsCV37wU7/YSIS6gfrxuL4feDJ0BUnKqfXDcc+1 GR4HibqHYOjbBdTGCzW2wYg8KhkfUskJ3sihmnMDVZ8Ls6mFxdjJ8fLEgauiyLT4DXSp Oen8dyAzd30p93gy37mb8XhG7EEwrUiGBycUcRWTDNTEZjILEn+dRviDwzQQMlj1Jrrc y3xg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1724149738; x=1724754538; h=content-transfer-encoding:mime-version:message-id:date:subject:cc :to:from:x-gm-message-state:from:to:cc:subject:date:message-id :reply-to; bh=XoSere6M7Ku9MAKY1jptLpeneDv23NmGppM5OqBX/Bo=; b=xQTgNBEyZImE8Wrk0YcRG7/Tx+pN4SvTIQjrawjptYIY3G/EC0YQs+oNMOZVh4FOZu 6xOttahj5/5YjvSkz4wIjpAES0OI9WbfPlhdR8HCbLr4FiGMQdcDtQEyejVtXvWAyMeq 9bz++fSB7HwuD7uePYIcHJOw+FY0Acr8TIcqmUU4qvkI0WXRt31lolj8RJFyhq6ms2Av RzMl6D7oK8i+dFGWfUiky8NFgtHpfIHtY8kfVm5X4C/51pDq5IdPt6JwBFV4s33gZ13T 4/ccu4NYaNoF5Wh4jLnhCVlYoPnu54AGtXw8uGE12UjUgNyH2N7aS0dWehNILJmEMw20 ACvQ== X-Gm-Message-State: AOJu0YyZufvWTCUYV+MtYx1j0HtCP1XILJeEOH59Q2m0YwBJ7SIHoUcD qlfdmAEQ0hjOS9XfCCvhP+25MJvQ0zeg3UkntjGz6Ao4Ds6DMdwxCRtVajJubSmU2EZYbNI29A/ i X-Google-Smtp-Source: AGHT+IGpHleGJq6hDYGnznDHD6Ex69uvXDtRlCW9Zh6ipdMwJSQLEloBMQZdtxfrK1EcogKOkm3mtg== X-Received: by 2002:a05:600c:46cf:b0:426:64f4:7793 with SMTP id 5b1f17b1804b1-429ed7af3d8mr105248735e9.22.1724149738200; Tue, 20 Aug 2024 03:28:58 -0700 (PDT) Received: from jeandudey.home ([89.131.29.87]) by smtp.gmail.com with ESMTPSA id 5b1f17b1804b1-429ded36f55sm191248245e9.26.2024.08.20.03.28.57 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 20 Aug 2024 03:28:57 -0700 (PDT) From: Jean-Pierre De Jesus DIAZ Date: Tue, 20 Aug 2024 12:28:55 +0200 Message-ID: X-Mailer: git-send-email 2.45.2 MIME-Version: 1.0 Content-Transfer-Encoding: 8bit Received-SPF: pass client-ip=2a00:1450:4864:20::32d; envelope-from=jean@foundation.xyz; helo=mail-wm1-x32d.google.com 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, RCVD_IN_DNSWL_NONE=-0.0001, SPF_HELO_NONE=0.001, SPF_PASS=-0.001, T_SCC_BODY_TEXT_LINE=-0.01 autolearn=ham autolearn_force=no X-Spam_action: no action X-Spam-Score: -1.3 (-) X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -2.3 (--) This updates Coq to 8.18.0 and some Coq plugins to build on the newer version. Updated to this one as 8.17 is already showing its age, Coq 8.19 still breaks Why 3, so that's the reason for 8.18, Why 3 already has some fixes for 8.19 so when released we can update to 8.19 (or 8.20 that is soon to be released). Jean-Pierre De Jesus DIAZ (2): gnu: coq: Propagate ocaml-zarith. gnu: coq: Update to 8.18.0. gnu/packages/coq.scm | 29 ++++++++++++++--------------- 1 file changed, 14 insertions(+), 15 deletions(-) base-commit: 91b69f154db218834de002dcd013a8f47170e684 -- 2.45.2 From unknown Sun Jun 22 00:59:42 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#72730] [PATCH 1/2] gnu: coq: Propagate ocaml-zarith. Resent-From: Jean-Pierre De Jesus DIAZ Original-Sender: "Debbugs-submit" Resent-CC: julien@lepiller.eu, pukkamustard@posteo.net, guix-patches@gnu.org Resent-Date: Tue, 20 Aug 2024 10:34:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 72730 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 72730@debbugs.gnu.org Cc: Jean-Pierre De Jesus DIAZ , Julien Lepiller , pukkamustard X-Debbugs-Original-Xcc: Julien Lepiller , pukkamustard Received: via spool by 72730-submit@debbugs.gnu.org id=B72730.172414999721841 (code B ref 72730); Tue, 20 Aug 2024 10:34:01 +0000 Received: (at 72730) by debbugs.gnu.org; 20 Aug 2024 10:33:17 +0000 Received: from localhost ([127.0.0.1]:59930 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1sgMAu-0005gB-T7 for submit@debbugs.gnu.org; Tue, 20 Aug 2024 06:33:17 -0400 Received: from mail-wm1-f45.google.com ([209.85.128.45]:55360) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1sgMAs-0005fq-Hx for 72730@debbugs.gnu.org; Tue, 20 Aug 2024 06:33:15 -0400 Received: by mail-wm1-f45.google.com with SMTP id 5b1f17b1804b1-428141be2ddso41441755e9.2 for <72730@debbugs.gnu.org>; Tue, 20 Aug 2024 03:32:31 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=foundation.xyz; s=google; t=1724149884; x=1724754684; darn=debbugs.gnu.org; h=content-transfer-encoding:mime-version:references:in-reply-to :message-id:date:subject:cc:to:from:from:to:cc:subject:date :message-id:reply-to; bh=xWF+TseV8tOqncxo+fLjJtfiCuR9tPZjg/eaQOIQWWs=; b=r4xBPLbsyx1staduqKyoMx2+ZGI+g6XaJmhJR1GaGdVBRVnEYp5HeJeXYckjJCc4nl AcQosyzracHvYlQGIvn46mucBXV+EngsbEMupHI1gmwDA1ZP8Rv9IopEF3XAd3+UyGcT XEt3UyoC0TWwvAYTmF+D980a+/YAzeviSEG/eCdQWzx6wxcvGoapVMBWewiFK3ujxoBk ncJhwnJvxTis+7apmuTBskEHzPooQCQr7nhdS5V9O1ZmHb0471ZBQ5/P/fnRDo8AVjxF seHd1etFo3fObxEdUn3I7XOZH3yTpbebC0CIsyGQp5pNuUOabpYt342FLast7zLt3xLQ yavQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1724149884; x=1724754684; h=content-transfer-encoding:mime-version:references:in-reply-to :message-id:date:subject:cc:to:from:x-gm-message-state:from:to:cc :subject:date:message-id:reply-to; bh=xWF+TseV8tOqncxo+fLjJtfiCuR9tPZjg/eaQOIQWWs=; b=F9qbVA+m8Qlbsg77uzZfXF/dYsCA+JM0xXXNyRWjEMlpffcXWbJm6k9zEEzJOEAFAs MuGi50x6Ao9jdhqH30XooWj8apRYxeLv7mtyV9EZZKaU7+HgIzg4i0a1SBEt1bx3sxZz yj4spDUBed5yoMWc+f+MvQxrYKIL6yTWCtmQxWJXSvFWYG5cF8m7KBtjmg2XH2eTcYAk zpgXFJnxf8FePhnB0ZBpSq9MVw9UVqq1bz+tGN6WsVP9yOMkrWpS24YYhJuQjxx0GVDg SJw2L+RIgWW45eV+b8UBN/RTi8GETY74KF5bKs6KFV6Nz7X2/dp2pKpNZNWHU1L0p5v1 HpRw== X-Gm-Message-State: AOJu0YyWSnoKD9M318bazkj0hBJkdMjUfd06VNYuMvoVpVwols1yt24J oxhueSGa5ibwkCRZNoKxJ5Cpt91fov09XwiRUPqKmLoruarnkIM5tRi4smoGldpjjCFAvKXE5uJ R X-Google-Smtp-Source: AGHT+IFjKAQl3tcg2etWRvS5haYZRlmoRckbHLVjKBcILe+WLbDb14zfChQ8iQ1gytQbFUWX1SedDg== X-Received: by 2002:adf:9790:0:b0:371:913a:3533 with SMTP id ffacd0b85a97d-3719454bd5emr9150107f8f.22.1724149884320; Tue, 20 Aug 2024 03:31:24 -0700 (PDT) Received: from jeandudey.home ([89.131.29.87]) by smtp.gmail.com with ESMTPSA id 5b1f17b1804b1-42aa6736e5esm121397595e9.38.2024.08.20.03.31.23 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 20 Aug 2024 03:31:24 -0700 (PDT) From: Jean-Pierre De Jesus DIAZ Date: Tue, 20 Aug 2024 12:31:18 +0200 Message-ID: X-Mailer: git-send-email 2.45.2 In-Reply-To: References: MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Spam-Score: -0.0 (/) X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) Otherwise each Coq plugin needs to specify it. * gnu/packages/coq.scm (coq) : Move ocaml-zarith from here... : ... to here. (coq-gappa) : Remove ocaml-zarith. (coq-bignums) : Likewise. (coq-interval) : Likewise. (coq-equations) : Likewise. Change-Id: I63cab11032cc6d4673efc9fdcf14be2929bda05e --- gnu/packages/coq.scm | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index 4857426613..be95d16991 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -91,8 +91,10 @@ (define-public coq (libdir (string-append out "/lib/ocaml/site-lib"))) (invoke "dune" "install" "--prefix" out "--libdir" libdir "coq" "coq-core" "coq-stdlib"))))))) + (propagated-inputs + (list ocaml-zarith)) (inputs - (list gmp ocaml-zarith)) + (list gmp)) (native-inputs (list ocaml-ounit2 which)) (properties '((upstream-name . "coq"))) ; also for inherited packages @@ -114,7 +116,7 @@ (define-public coq-ide-server `(#:tests? #f #:package "coqide-server")) (inputs - (list coq gmp ocaml-zarith)))) + (list coq gmp)))) (define-public coq-ide (package @@ -319,7 +321,7 @@ (define-public coq-gappa bison flex)) (inputs - (list gmp mpfr ocaml-zarith boost)) + (list gmp mpfr boost)) (propagated-inputs (list coq-flocq)) (arguments @@ -457,7 +459,7 @@ (define-public coq-bignums (native-inputs (list ocaml coq)) (inputs - (list camlp5 ocaml-zarith)) + (list camlp5)) (arguments `(#:tests? #f ; No test target. #:make-flags @@ -495,8 +497,7 @@ (define-public coq-interval `(("flocq" ,coq-flocq) ("bignums" ,coq-bignums) ("coquelicot" ,coq-coquelicot) - ("mathcomp" ,coq-mathcomp) - ("ocaml-zarith" ,ocaml-zarith))) + ("mathcomp" ,coq-mathcomp))) (arguments `(#:configure-flags (list (string-append "COQUSERCONTRIB=" (assoc-ref %outputs "out") @@ -579,8 +580,6 @@ (define-public coq-equations (build-system gnu-build-system) (native-inputs (list ocaml coq camlp5)) - (inputs - (list ocaml-zarith)) (arguments `(#:test-target "test-suite" #:make-flags (list (string-append "COQLIBINSTALL=" -- 2.45.2 From unknown Sun Jun 22 00:59:42 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#72730] [PATCH 2/2] gnu: coq: Update to 8.18.0. Resent-From: Jean-Pierre De Jesus DIAZ Original-Sender: "Debbugs-submit" Resent-CC: julien@lepiller.eu, pukkamustard@posteo.net, guix-patches@gnu.org Resent-Date: Tue, 20 Aug 2024 10:34:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 72730 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 72730@debbugs.gnu.org Cc: Jean-Pierre De Jesus DIAZ , Julien Lepiller , pukkamustard X-Debbugs-Original-Xcc: Julien Lepiller , pukkamustard Received: via spool by 72730-submit@debbugs.gnu.org id=B72730.172414999721847 (code B ref 72730); Tue, 20 Aug 2024 10:34:02 +0000 Received: (at 72730) by debbugs.gnu.org; 20 Aug 2024 10:33:17 +0000 Received: from localhost ([127.0.0.1]:59932 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1sgMAv-0005gE-9h for submit@debbugs.gnu.org; Tue, 20 Aug 2024 06:33:17 -0400 Received: from mail-wr1-f44.google.com ([209.85.221.44]:57668) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1sgMAt-0005fu-Ek for 72730@debbugs.gnu.org; Tue, 20 Aug 2024 06:33:15 -0400 Received: by mail-wr1-f44.google.com with SMTP id ffacd0b85a97d-371a92d8c90so1697701f8f.3 for <72730@debbugs.gnu.org>; Tue, 20 Aug 2024 03:32:32 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=foundation.xyz; s=google; t=1724149886; x=1724754686; darn=debbugs.gnu.org; h=content-transfer-encoding:mime-version:references:in-reply-to :message-id:date:subject:cc:to:from:from:to:cc:subject:date :message-id:reply-to; bh=xH6OatA45Pf62iDmq+8h42CV07u3EgW2cCnRjM+/7l8=; b=Pm3PRkFCyaVep9eYlf9IMc58gi+coFs9x9STjqnuQIr5QTZpegEz8dCe2NZkIiSnwa 9Y8qapc52kt7LOIOpPYHA4PXefjqkHqo51iZXel2QMQLlXQg1FK+wK7/V91r0E8eMFC4 vy+2rJbJdH3y2Iv1mG2L1k9ANVdf/k368g4DvhBfTKhvSajAFChwHjI7clA+YaRDC6KM +ffZBKJBGsi1yQVyYDm3sKv1vOONUaHURZ0rI997HYDPIBbzhufl3qWFQp1QOVQEECLj Cuq0hjB1KDD4R9WQEBhFsC/3KH3oICAYkNCTn/nZeP1UzD/HLJHgRP+Xp8qfLKAmseU2 okpw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1724149886; x=1724754686; h=content-transfer-encoding:mime-version:references:in-reply-to :message-id:date:subject:cc:to:from:x-gm-message-state:from:to:cc :subject:date:message-id:reply-to; bh=xH6OatA45Pf62iDmq+8h42CV07u3EgW2cCnRjM+/7l8=; b=QEW2rl4/JOybGcqQYe0L9Q6kZCscJOXz2uKsFI7OLatWRG5Ba9YB2jcgppAswr6Ij+ arkVkkyHXsowKIDa8sW6CSg/XbQy1+gj8WGhq9D9/oN0yOPIB6C+btyv3855bRtUbEch oNDSrjxzn+m+iwJ/k+1jYM40r10B4GYnxpVlyy7GZNB+xTsvIu6/76HYs4KvN6ri9QYi +0gW6JqtdEsoqAEMHfwFKHhjWbAjV7FuuDQk6ToznAKyi/x4PIRidglCUvRl2SziKeZk O+LeMaou4xbFc9epIQIDYhKUk56zh/2oEkj/QRjEYfvGx3S35dQfiEJMcq6gbGLXlHIV 7gSw== X-Gm-Message-State: AOJu0YywWLGL/E0284TOvO3AiuxtDhKi8pLBrRcvR347M5FqG18p5Ijv 579SWqZKG7eXq9sC8+Z0QlEoss31MpBWdK6tfjJsG+N5fSatrWITkQDHQfqxhEseo89yKeiBjcY Q X-Google-Smtp-Source: AGHT+IEeGBD5VV2Zu/eB/Q3drJJ0swMCsfsrRVPkLksm6VRq36dKh7mvdRRb+8F8nOusJSAGYEPRxA== X-Received: by 2002:a05:6000:e81:b0:371:8a74:4170 with SMTP id ffacd0b85a97d-3719464ee2bmr8520136f8f.24.1724149886483; Tue, 20 Aug 2024 03:31:26 -0700 (PDT) Received: from jeandudey.home ([89.131.29.87]) by smtp.gmail.com with ESMTPSA id 5b1f17b1804b1-42aa6736e5esm121397595e9.38.2024.08.20.03.31.25 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 20 Aug 2024 03:31:26 -0700 (PDT) From: Jean-Pierre De Jesus DIAZ Date: Tue, 20 Aug 2024 12:31:19 +0200 Message-ID: X-Mailer: git-send-email 2.45.2 In-Reply-To: References: MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Spam-Score: -0.0 (/) X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) * gnu/packages/coq.scm (coq): Update to 8.18.0. (coq-bignums): Update to 9.0.0+coq8.18. (coq-equations): Update to 1.3-8.18. Change-Id: I644a4538538a23d736fca2fab541c2cd2fb1f472 --- gnu/packages/coq.scm | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index be95d16991..02d2600546 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -56,7 +56,7 @@ (define-module (gnu packages coq) (define-public coq (package (name "coq") - (version "8.17.1") + (version "8.18.0") (source (origin (method git-fetch) @@ -66,7 +66,7 @@ (define-public coq (file-name (git-file-name name version)) (sha256 (base32 - "0gg6hizq0i08lk741b579cbswhy6qvkh6inc3d3i5a2af98psq63")))) + "1qy71gdr4s2l6847b4nwns6akib2f7l725zb01m7zc26n6mrrh1m")))) (native-search-paths (list (search-path-specification (variable "COQPATH") @@ -445,16 +445,16 @@ (define-public coq-coquelicot (define-public coq-bignums (package (name "coq-bignums") - (version "8.16.0") + (version "9.0.0+coq8.18") (source (origin (method git-fetch) (uri (git-reference (url "https://github.com/coq/bignums") - (commit (string-append "V" version)))) + (commit (string-append "v" version)))) (file-name (git-file-name name version)) (sha256 (base32 - "07ndnm7pndmai3a2bkcmwjfjzfaqyq19c5an15hmhgmd0rdy4z8c")))) + "1vw1a498fhyrpm884rlm3r4lw4mg4l6b9xj8w4y875sacg88kdxw")))) (build-system gnu-build-system) (native-inputs (list ocaml coq)) @@ -567,7 +567,7 @@ (define-public coq-autosubst (define-public coq-equations (package (name "coq-equations") - (version "1.3-8.17") + (version "1.3-8.18") (source (origin (method git-fetch) (uri (git-reference @@ -576,7 +576,7 @@ (define-public coq-equations (file-name (git-file-name name version)) (sha256 (base32 - "0g68h4c1ijpphixvl9wkd7sibds38v4236dpvvh194j5ii42vnn8")))) + "1akxf2vafwyz6fi1djlc3g8mwxrjv0a99x4b08jwrbwxypv4xiph")))) (build-system gnu-build-system) (native-inputs (list ocaml coq camlp5)) -- 2.45.2 From unknown Sun Jun 22 00:59:42 2025 MIME-Version: 1.0 X-Mailer: MIME-tools 5.505 (Entity 5.505) X-Loop: help-debbugs@gnu.org From: help-debbugs@gnu.org (GNU bug Tracking System) To: Jean-Pierre De Jesus DIAZ Subject: bug#72730: closed (Re: [bug#72730] [PATCH 2/2] gnu: coq: Update to 8.18.0.) Message-ID: References: <87wmjhcrgi.fsf@iscas.ac.cn> X-Gnu-PR-Message: they-closed 72730 X-Gnu-PR-Package: guix-patches X-Gnu-PR-Keywords: patch Reply-To: 72730@debbugs.gnu.org Date: Thu, 12 Sep 2024 06:33:01 +0000 Content-Type: multipart/mixed; boundary="----------=_1726122781-19427-1" This is a multi-part message in MIME format... ------------=_1726122781-19427-1 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" Your bug report #72730: [PATCH 0/2] coq: Update to 8.18.0. which was filed against the guix-patches package, has been closed. The explanation is attached below, along with your original report. If you require more details, please reply to 72730@debbugs.gnu.org. --=20 72730: https://debbugs.gnu.org/cgi/bugreport.cgi?bug=3D72730 GNU Bug Tracking System Contact help-debbugs@gnu.org with problems ------------=_1726122781-19427-1 Content-Type: message/rfc822 Content-Disposition: inline Content-Transfer-Encoding: 7bit Received: (at 72730-done) by debbugs.gnu.org; 12 Sep 2024 06:33:00 +0000 Received: from localhost ([127.0.0.1]:39931 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1sodNz-000538-Oi for submit@debbugs.gnu.org; Thu, 12 Sep 2024 02:33:00 -0400 Received: from smtp81.cstnet.cn ([159.226.251.81]:53504 helo=cstnet.cn) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1sodNw-00052o-EW for 72730-done@debbugs.gnu.org; Thu, 12 Sep 2024 02:32:59 -0400 Received: from m (unknown [107.174.64.25]) by APP-03 (Coremail) with SMTP id rQCowACHXI__iuJmvKv4Ag--.13626S2; Thu, 12 Sep 2024 14:32:36 +0800 (CST) From: Z572 To: Jean-Pierre De Jesus DIAZ Subject: Re: [bug#72730] [PATCH 2/2] gnu: coq: Update to 8.18.0. In-Reply-To: (Jean-Pierre De Jesus DIAZ's message of "Tue, 20 Aug 2024 12:31:19 +0200") References: Date: Thu, 12 Sep 2024 14:32:29 +0800 Message-ID: <87wmjhcrgi.fsf@iscas.ac.cn> MIME-Version: 1.0 Content-Type: multipart/signed; boundary="=-=-="; micalg=pgp-sha512; protocol="application/pgp-signature" X-CM-TRANSID: rQCowACHXI__iuJmvKv4Ag--.13626S2 X-Coremail-Antispam: 1UD129KBjvJXoW7CF47CF1rKFW7JryDCFWktFb_yoW8Kw1Up3 yfZa4F9F10k34Utwn5uF12kF15urWxGF10kw4UZws7KwnIqrWxXrWUta95CF17Aw18Cw4Y vw40v3WrXrW5GaDanT9S1TB71UUUUU7qnTZGkaVYY2UrUUUUjbIjqfuFe4nvWSU5nxnvy2 9KBjDU0xBIdaVrnRJUUUvlb7Iv0xC_Kw4lb4IE77IF4wAFF20E14v26r1j6r4UM7CY07I2 0VC2zVCF04k26cxKx2IYs7xG6rWj6s0DM7CIcVAFz4kK6r1j6r18M28lY4IEw2IIxxk0rw A2F7IY1VAKz4vEj48ve4kI8wA2z4x0Y4vE2Ix0cI8IcVAFwI0_Xr0_Ar1l84ACjcxK6xII jxv20xvEc7CjxVAFwI0_Gr0_Cr1l84ACjcxK6I8E87Iv67AKxVW8Jr0_Cr1UM28EF7xvwV C2z280aVCY1x0267AKxVW0oVCq3wAa7VASzI0EjI02j7AqF2xKxVCjxxvEa2IrM2AIxVAI cxkEcVAq07x20xvEncxIr21le4C267I2x7xF54xIwI1l5I8CrVACY4xI64kE6c02F40Ex7 xfMcIj6xIIjxv20xvE14v26r1j6r18McIj6I8E87Iv67AKxVWUJVW8JwAm72CE4IkC6x0Y z7v_Jr0_Gr1lF7xvr2IY64vIr41l42xK82IYc2Ij64vIr41l4I8I3I0E4IkC6x0Yz7v_Jr 0_Gr1lx2IqxVAqx4xG67AKxVWUJVWUGwC20s026x8GjcxK67AKxVWUGVWUWwC2zVAF1VAY 17CE14v26r126r1DMIIYrxkI7VAKI48JMIIF0xvE2Ix0cI8IcVAFwI0_Jr0_JF4lIxAIcV C0I7IYx2IY6xkF7I0E14v26r1j6r4UMIIF0xvE42xK8VAvwI8IcIk0rVWUJVWUCwCI42IY 6I8E87Iv67AKxVWUJVW8JwCI42IY6I8E87Iv6xkF7I0E14v26r1j6r4UYxBIdaVFxhVjvj DU0xZFpf9x07jEOJOUUUUU= X-Originating-IP: [107.174.64.25] X-CM-SenderInfo: x2kh0wxmxqyx3h6l2u1dvotugofq/ X-Spam-Score: -0.0 (/) X-Debbugs-Envelope-To: 72730-done Cc: 72730-done@debbugs.gnu.org, pukkamustard , Julien Lepiller X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) --=-=-= Content-Type: text/plain Jean-Pierre De Jesus DIAZ writes: > * gnu/packages/coq.scm (coq): Update to 8.18.0. > (coq-bignums): Update to 9.0.0+coq8.18. > (coq-equations): Update to 1.3-8.18. i split to 3 patch. and make coq-bignums coq-equations use g-expression. > > Change-Id: I644a4538538a23d736fca2fab541c2cd2fb1f472 > --- > gnu/packages/coq.scm | 14 +++++++------- > 1 file changed, 7 insertions(+), 7 deletions(-) > > diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm > index be95d16991..02d2600546 100644 > --- a/gnu/packages/coq.scm > +++ b/gnu/packages/coq.scm > @@ -56,7 +56,7 @@ (define-module (gnu packages coq) > (define-public coq > (package > (name "coq") > - (version "8.17.1") > + (version "8.18.0") > (source > (origin > (method git-fetch) > @@ -66,7 +66,7 @@ (define-public coq > (file-name (git-file-name name version)) > (sha256 > (base32 > - "0gg6hizq0i08lk741b579cbswhy6qvkh6inc3d3i5a2af98psq63")))) > + "1qy71gdr4s2l6847b4nwns6akib2f7l725zb01m7zc26n6mrrh1m")))) > (native-search-paths > (list (search-path-specification > (variable "COQPATH") > @@ -445,16 +445,16 @@ (define-public coq-coquelicot > (define-public coq-bignums > (package > (name "coq-bignums") > - (version "8.16.0") > + (version "9.0.0+coq8.18") > (source (origin > (method git-fetch) > (uri (git-reference > (url "https://github.com/coq/bignums") > - (commit (string-append "V" version)))) > + (commit (string-append "v" version)))) > (file-name (git-file-name name version)) > (sha256 > (base32 > - "07ndnm7pndmai3a2bkcmwjfjzfaqyq19c5an15hmhgmd0rdy4z8c")))) > + "1vw1a498fhyrpm884rlm3r4lw4mg4l6b9xj8w4y875sacg88kdxw")))) > (build-system gnu-build-system) > (native-inputs > (list ocaml coq)) > @@ -567,7 +567,7 @@ (define-public coq-autosubst > (define-public coq-equations > (package > (name "coq-equations") > - (version "1.3-8.17") > + (version "1.3-8.18") > (source (origin > (method git-fetch) > (uri (git-reference > @@ -576,7 +576,7 @@ (define-public coq-equations > (file-name (git-file-name name version)) > (sha256 > (base32 > - "0g68h4c1ijpphixvl9wkd7sibds38v4236dpvvh194j5ii42vnn8")))) > + "1akxf2vafwyz6fi1djlc3g8mwxrjv0a99x4b08jwrbwxypv4xiph")))) > (build-system gnu-build-system) > (native-inputs > (list ocaml coq camlp5)) push, close. --=-=-= Content-Type: application/pgp-signature; name="signature.asc" -----BEGIN PGP SIGNATURE----- iQIzBAEBCgAdFiEEfr6klGDOXiwIdX/bO1qpk+Gi3/AFAmbiiv0ACgkQO1qpk+Gi 3/BcYg/+MY2X+Zvr2zADULU8osxx4SlwV2UuFJ4Nb2gjpMRHR00C0wtLn2bPt6pO iuyiucpd7diGWqyWTUph/ql8CXgkq0sCCDat0soBCzcSeFEtS6ANuDRamK2ruty1 /uBN674dbd64symRLnS04HYaKJlhmPjCVfGh/baPi5P6GDYe1HqLEMzmMJcMZeiW dZ5wZPW6h+GgXhm01q10VEQ0zvohCqfYlMliE0UC7eQ0wtzgvorL49dKv3pm/4P0 KFTP7rHpZ6+LVPAzPnBPK6cgYjbKy9bqcVNenlmZWlJio8Jgwqkcu2mxbsFPSttY iSiPpfeXOpJzb1rHPsZKvOKDBJg2pdsFrto5u7CYe0DuuKt77HeMl/r6/m1YDZfc TtgAqVFoXIi3D6UZHRJx9vxfKdE2LMunckdKCa1kLJejfywhoRYkm3yQGwBriPyD dOT5xEKTfQ0hSR9P0XFzoPu5URGnrY23NAlK9F0IWB73aYF4AwMFgBFQTFQvoGC9 Y7aGJoCBsCecYiAbxS8gGPORGGScUBgmx28lYnTcNLj5EKelZdDRkpFvpMpsIEbU +lE956/jYky6BHmO+uskwXKOdRohdQSvhd53Vwz0KczmKmkn35pYDYjwOZcF/+9L l6ZGoEoJdlHgy11x1kYP79uSK02L6QkxqyqFp4KwLZvpSPUI4u0= =8pXE -----END PGP SIGNATURE----- --=-=-=-- ------------=_1726122781-19427-1 Content-Type: message/rfc822 Content-Disposition: inline Content-Transfer-Encoding: 7bit Received: (at submit) by debbugs.gnu.org; 20 Aug 2024 10:29:48 +0000 Received: from localhost ([127.0.0.1]:59922 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1sgM7Y-0005YP-4y for submit@debbugs.gnu.org; Tue, 20 Aug 2024 06:29:48 -0400 Received: from lists.gnu.org ([209.51.188.17]:44258) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1sgM7V-0005YG-LA for submit@debbugs.gnu.org; Tue, 20 Aug 2024 06:29:46 -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 1sgM6o-0004OH-Co for guix-patches@gnu.org; Tue, 20 Aug 2024 06:29:02 -0400 Received: from mail-wm1-x32d.google.com ([2a00:1450:4864:20::32d]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1sgM6m-0004ER-QG for guix-patches@gnu.org; Tue, 20 Aug 2024 06:29:02 -0400 Received: by mail-wm1-x32d.google.com with SMTP id 5b1f17b1804b1-428119da952so42815685e9.0 for ; Tue, 20 Aug 2024 03:28:59 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=foundation.xyz; s=google; t=1724149738; x=1724754538; darn=gnu.org; h=content-transfer-encoding:mime-version:message-id:date:subject:cc :to:from:from:to:cc:subject:date:message-id:reply-to; bh=XoSere6M7Ku9MAKY1jptLpeneDv23NmGppM5OqBX/Bo=; b=dzqK7XjVknpnJi4PO7QIc6gh7B+F/L4FCZ7oktS89ROV5gqfZpHWWkLPcuttX43ksT i7Gng/qN03CEXktxDT0aDqg1GFsQIhIdzUinLiRS3EFHgQ5eHH5CoeVndcAh3LXaYJpv wK7FUt17WKN8hFX6bv3GGVk4msT1aOsCV37wU7/YSIS6gfrxuL4feDJ0BUnKqfXDcc+1 GR4HibqHYOjbBdTGCzW2wYg8KhkfUskJ3sihmnMDVZ8Ls6mFxdjJ8fLEgauiyLT4DXSp Oen8dyAzd30p93gy37mb8XhG7EEwrUiGBycUcRWTDNTEZjILEn+dRviDwzQQMlj1Jrrc y3xg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1724149738; x=1724754538; h=content-transfer-encoding:mime-version:message-id:date:subject:cc :to:from:x-gm-message-state:from:to:cc:subject:date:message-id :reply-to; bh=XoSere6M7Ku9MAKY1jptLpeneDv23NmGppM5OqBX/Bo=; b=xQTgNBEyZImE8Wrk0YcRG7/Tx+pN4SvTIQjrawjptYIY3G/EC0YQs+oNMOZVh4FOZu 6xOttahj5/5YjvSkz4wIjpAES0OI9WbfPlhdR8HCbLr4FiGMQdcDtQEyejVtXvWAyMeq 9bz++fSB7HwuD7uePYIcHJOw+FY0Acr8TIcqmUU4qvkI0WXRt31lolj8RJFyhq6ms2Av RzMl6D7oK8i+dFGWfUiky8NFgtHpfIHtY8kfVm5X4C/51pDq5IdPt6JwBFV4s33gZ13T 4/ccu4NYaNoF5Wh4jLnhCVlYoPnu54AGtXw8uGE12UjUgNyH2N7aS0dWehNILJmEMw20 ACvQ== X-Gm-Message-State: AOJu0YyZufvWTCUYV+MtYx1j0HtCP1XILJeEOH59Q2m0YwBJ7SIHoUcD qlfdmAEQ0hjOS9XfCCvhP+25MJvQ0zeg3UkntjGz6Ao4Ds6DMdwxCRtVajJubSmU2EZYbNI29A/ i X-Google-Smtp-Source: AGHT+IGpHleGJq6hDYGnznDHD6Ex69uvXDtRlCW9Zh6ipdMwJSQLEloBMQZdtxfrK1EcogKOkm3mtg== X-Received: by 2002:a05:600c:46cf:b0:426:64f4:7793 with SMTP id 5b1f17b1804b1-429ed7af3d8mr105248735e9.22.1724149738200; Tue, 20 Aug 2024 03:28:58 -0700 (PDT) Received: from jeandudey.home ([89.131.29.87]) by smtp.gmail.com with ESMTPSA id 5b1f17b1804b1-429ded36f55sm191248245e9.26.2024.08.20.03.28.57 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 20 Aug 2024 03:28:57 -0700 (PDT) From: Jean-Pierre De Jesus DIAZ To: guix-patches@gnu.org Subject: [PATCH 0/2] coq: Update to 8.18.0. Date: Tue, 20 Aug 2024 12:28:55 +0200 Message-ID: X-Mailer: git-send-email 2.45.2 MIME-Version: 1.0 X-Debbugs-Cc: Julien Lepiller , pukkamustard Content-Transfer-Encoding: 8bit Received-SPF: pass client-ip=2a00:1450:4864:20::32d; envelope-from=jean@foundation.xyz; helo=mail-wm1-x32d.google.com 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, RCVD_IN_DNSWL_NONE=-0.0001, SPF_HELO_NONE=0.001, SPF_PASS=-0.001, T_SCC_BODY_TEXT_LINE=-0.01 autolearn=ham autolearn_force=no X-Spam_action: no action X-Spam-Score: -1.3 (-) X-Debbugs-Envelope-To: submit Cc: Jean-Pierre De Jesus DIAZ X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -2.3 (--) This updates Coq to 8.18.0 and some Coq plugins to build on the newer version. Updated to this one as 8.17 is already showing its age, Coq 8.19 still breaks Why 3, so that's the reason for 8.18, Why 3 already has some fixes for 8.19 so when released we can update to 8.19 (or 8.20 that is soon to be released). Jean-Pierre De Jesus DIAZ (2): gnu: coq: Propagate ocaml-zarith. gnu: coq: Update to 8.18.0. gnu/packages/coq.scm | 29 ++++++++++++++--------------- 1 file changed, 14 insertions(+), 15 deletions(-) base-commit: 91b69f154db218834de002dcd013a8f47170e684 -- 2.45.2 ------------=_1726122781-19427-1-- From unknown Sun Jun 22 00:59:42 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#72730] [PATCH 1/2] gnu: coq: Propagate ocaml-zarith. Resent-From: Z572 Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Thu, 12 Sep 2024 06:35:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 72730 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Jean-Pierre De Jesus DIAZ Cc: 72730@debbugs.gnu.org, pukkamustard , Julien Lepiller Received: via spool by 72730-submit@debbugs.gnu.org id=B72730.172612287419647 (code B ref 72730); Thu, 12 Sep 2024 06:35:02 +0000 Received: (at 72730) by debbugs.gnu.org; 12 Sep 2024 06:34:34 +0000 Received: from localhost ([127.0.0.1]:39951 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1sodPV-00056o-NX for submit@debbugs.gnu.org; Thu, 12 Sep 2024 02:34:34 -0400 Received: from smtp81.cstnet.cn ([159.226.251.81]:53864 helo=cstnet.cn) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1sodPT-00056b-Ck for 72730@debbugs.gnu.org; Thu, 12 Sep 2024 02:34:32 -0400 Received: from m (unknown [107.174.64.25]) by APP-03 (Coremail) with SMTP id rQCowADn7X1ji+JmAcf4Ag--.849S2; Thu, 12 Sep 2024 14:34:15 +0800 (CST) From: Z572 In-Reply-To: (Jean-Pierre De Jesus DIAZ's message of "Tue, 20 Aug 2024 12:31:18 +0200") References: Date: Thu, 12 Sep 2024 14:34:09 +0800 Message-ID: <87seu5crdq.fsf@iscas.ac.cn> MIME-Version: 1.0 Content-Type: multipart/signed; boundary="=-=-="; micalg=pgp-sha512; protocol="application/pgp-signature" X-CM-TRANSID: rQCowADn7X1ji+JmAcf4Ag--.849S2 X-Coremail-Antispam: 1UD129KBjvJXoWxXFykXF4rKF45Cr1kKrW3ZFb_yoW5XrWUpa yfAayjkr1xCrWrtw12gF4akFn8uF4rJr1Ykw18A3W5G345ta95Wry7Kayfu3sxCw1xW34U K3y8ta1vv3yrCFJanT9S1TB71UUUUU7qnTZGkaVYY2UrUUUUjbIjqfuFe4nvWSU5nxnvy2 9KBjDU0xBIdaVrnRJUUUvlb7Iv0xC_Kw4lb4IE77IF4wAFF20E14v26r1j6r4UM7CY07I2 0VC2zVCF04k26cxKx2IYs7xG6rWj6s0DM7CIcVAFz4kK6r1j6r18M28lY4IEw2IIxxk0rw A2F7IY1VAKz4vEj48ve4kI8wA2z4x0Y4vE2Ix0cI8IcVAFwI0_Gr0_Xr1l84ACjcxK6xII jxv20xvEc7CjxVAFwI0_Gr0_Cr1l84ACjcxK6I8E87Iv67AKxVW8Jr0_Cr1UM28EF7xvwV C2z280aVCY1x0267AKxVW0oVCq3wAa7VASzI0EjI02j7AqF2xKxVCjxxvEa2IrM2AIxVAI cxkEcVAq07x20xvEncxIr21le4C267I2x7xF54xIwI1l5I8CrVACY4xI64kE6c02F40Ex7 xfMcIj6xIIjxv20xvE14v26r106r15McIj6I8E87Iv67AKxVWUJVW8JwAm72CE4IkC6x0Y z7v_Jr0_Gr1lF7xvr2IY64vIr41l42xK82IYc2Ij64vIr41l4I8I3I0E4IkC6x0Yz7v_Jr 0_Gr1lx2IqxVAqx4xG67AKxVWUJVWUGwC20s026x8GjcxK67AKxVWUGVWUWwC2zVAF1VAY 17CE14v26r126r1DMIIYrxkI7VAKI48JMIIF0xvE2Ix0cI8IcVAFwI0_Jr0_JF4lIxAIcV C0I7IYx2IY6xkF7I0E14v26r1j6r4UMIIF0xvE42xK8VAvwI8IcIk0rVWUJVWUCwCI42IY 6I8E87Iv67AKxVWUJVW8JwCI42IY6I8E87Iv6xkF7I0E14v26r1j6r4UYxBIdaVFxhVjvj DU0xZFpf9x07jt4SwUUUUU= X-Originating-IP: [107.174.64.25] X-CM-SenderInfo: x2kh0wxmxqyx3h6l2u1dvotugofq/ X-Spam-Score: -0.0 (/) X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) --=-=-= Content-Type: text/plain Content-Transfer-Encoding: quoted-printable Jean-Pierre De Jesus DIAZ writes: > Otherwise each Coq plugin needs to specify it. > > * gnu/packages/coq.scm (coq) : Move ocaml-zarith from here... > : ... to here. > (coq-gappa) : Remove ocaml-zarith. > (coq-bignums) : Likewise. > (coq-interval) : Likewise. > (coq-equations) : Likewise. adjust to * gnu/packages/coq.scm (coq)[inputs]: Move ocaml-zarith from here... [propagated-inptus]: ... to here. (coq-gappa)[inputs]: Remove ocaml-zarith. (coq-bignums)[inputs]: Likewise. (coq-interval)[inputs]: Likewise. (coq-equations)[inputs]: Likewise. > > Change-Id: I63cab11032cc6d4673efc9fdcf14be2929bda05e > --- > gnu/packages/coq.scm | 15 +++++++-------- > 1 file changed, 7 insertions(+), 8 deletions(-) > > diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm > index 4857426613..be95d16991 100644 > --- a/gnu/packages/coq.scm > +++ b/gnu/packages/coq.scm > @@ -91,8 +91,10 @@ (define-public coq > (libdir (string-append out "/lib/ocaml/site-lib"))) > (invoke "dune" "install" "--prefix" out > "--libdir" libdir "coq" "coq-core" "coq-stdlib")= )))))) > + (propagated-inputs > + (list ocaml-zarith)) > (inputs > - (list gmp ocaml-zarith)) > + (list gmp)) > (native-inputs > (list ocaml-ounit2 which)) > (properties '((upstream-name . "coq"))) ; also for inherited packages > @@ -114,7 +116,7 @@ (define-public coq-ide-server > `(#:tests? #f > #:package "coqide-server")) > (inputs > - (list coq gmp ocaml-zarith)))) > + (list coq gmp)))) >=20=20 > (define-public coq-ide > (package > @@ -319,7 +321,7 @@ (define-public coq-gappa > bison > flex)) > (inputs > - (list gmp mpfr ocaml-zarith boost)) > + (list gmp mpfr boost)) > (propagated-inputs > (list coq-flocq)) > (arguments > @@ -457,7 +459,7 @@ (define-public coq-bignums > (native-inputs > (list ocaml coq)) > (inputs > - (list camlp5 ocaml-zarith)) > + (list camlp5)) > (arguments > `(#:tests? #f ; No test target. > #:make-flags > @@ -495,8 +497,7 @@ (define-public coq-interval > `(("flocq" ,coq-flocq) > ("bignums" ,coq-bignums) > ("coquelicot" ,coq-coquelicot) > - ("mathcomp" ,coq-mathcomp) > - ("ocaml-zarith" ,ocaml-zarith))) > + ("mathcomp" ,coq-mathcomp))) > (arguments > `(#:configure-flags > (list (string-append "COQUSERCONTRIB=3D" (assoc-ref %outputs "out= ") > @@ -579,8 +580,6 @@ (define-public coq-equations > (build-system gnu-build-system) > (native-inputs > (list ocaml coq camlp5)) > - (inputs > - (list ocaml-zarith)) > (arguments > `(#:test-target "test-suite" > #:make-flags (list (string-append "COQLIBINSTALL=3D" --=-=-= Content-Type: application/pgp-signature; name="signature.asc" -----BEGIN PGP SIGNATURE----- iQIzBAEBCgAdFiEEfr6klGDOXiwIdX/bO1qpk+Gi3/AFAmbii2EACgkQO1qpk+Gi 3/Cw9RAArET/mMF/CK2ewH3CpBLnwjH+2UmlWs07k8oQElL/EzbvojwHPTQGMMuS Nr3GiZ+1KCRG/Q6xrWyXiGSvBvAILdGdYj7PbDkUZMJT2wWkG7S31i9IedwZ3did krLIzo4JSauOZ4fiG2yq6HxVrllJG//RuH8NAS33hFI2aSs1fLcaM/eosboraND/ dROf/2Sjr8FzDHqbFJsT6GirWhLIEggfOOAYCu0vGLWJ2jQaRcBNm2s5rZo5unUr zjR2hkSIcC1mrhUcW6YBXWn7im7yPhSfAxh4COZhPycG4ss22MBIj0f5TeX+Oht3 BwWW94aQkwszQqnqb2S5a2+JMVIpuME+8f59xBchv/+vGRD4PTZ1/OhIlSNotB2H AC+gIkn9sofSilNh64Sj08rulyv3Z/7POUZgjMbhjIFqFRX4PrUEi99bYpIrbdUJ yHWA+uqk9JlwA9+8YGWfJB4IISQ/g9xYesWG9hxPC9QmJWiGTPYIzXeFs2BplIAx kcTU7mYH1R0hZeuu1QKvXVWkw3JcAuatsqPUYrSEGbZVOv3xgNw8/fk9BxdR+MHG I6NklryhWzS9N3v2G1X244wuB/DDQ3UqneC+xE02IW1I0qopRYj10CWlxeJ7l88v pEFyDi+knbRhyIFryWBG3CzGXA7PztYYgWqfZuukjFbVIwj0Fhw= =iJq0 -----END PGP SIGNATURE----- --=-=-=--