From unknown Tue Aug 19 02:53:08 2025 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-Mailer: MIME-tools 5.509 (Entity 5.509) Content-Type: text/plain; charset=utf-8 From: bug#52164 <52164@debbugs.gnu.org> To: bug#52164 <52164@debbugs.gnu.org> Subject: Status: [PATCH] gnu: coq: Update to 8.14.0. Reply-To: bug#52164 <52164@debbugs.gnu.org> Date: Tue, 19 Aug 2025 09:53:08 +0000 retitle 52164 [PATCH] gnu: coq: Update to 8.14.0. reassign 52164 guix-patches submitter 52164 Julien Lepiller severity 52164 normal tag 52164 patch thanks From debbugs-submit-bounces@debbugs.gnu.org Sun Nov 28 11:44:47 2021 Received: (at submit) by debbugs.gnu.org; 28 Nov 2021 16:44:48 +0000 Received: from localhost ([127.0.0.1]:36241 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mrNIF-0003ys-Ow for submit@debbugs.gnu.org; Sun, 28 Nov 2021 11:44:47 -0500 Received: from lists.gnu.org ([209.51.188.17]:39422) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mrNID-0003yi-3C for submit@debbugs.gnu.org; Sun, 28 Nov 2021 11:44:45 -0500 Received: from eggs.gnu.org ([209.51.188.92]:51160) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1mrNIC-00085U-Rr for guix-patches@gnu.org; Sun, 28 Nov 2021 11:44:44 -0500 Received: from lepiller.eu ([89.234.186.109]:36668) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1mrNI9-0000Kb-9p for guix-patches@gnu.org; Sun, 28 Nov 2021 11:44:44 -0500 Received: from lepiller.eu (localhost [127.0.0.1]) by lepiller.eu (OpenSMTPD) with ESMTP id 540f5f0b for ; Sun, 28 Nov 2021 16:44:33 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed; d=lepiller.eu; h=date:from :to:subject:message-id:mime-version:content-type :content-transfer-encoding; s=dkim; bh=Dkqx/iqB0D2Tipv+gfcQW/pAQ W5BfCt4xMmNeRkhAno=; b=F+EjrOW9Mpn72EW9VKBzSLUigpoA4Hx7b6DXso1KP 1wtvHgVqVKOIJ7ttPFPa0xvZpW/YGWwbRMOalFakLYlC+/RYzAZuOOgw1ICW1ic+ NDPu/mcLFAKbKmrtExbCT0NiKIO/myYH9NdBdNLVNcAGDTLxG1FJZU6Fu3bc1EfD xY/BlsxsUh8SYdAQmqcfrGAqnhi8hqiVGX6wRvGkEhuuSYs2gnbv08oluK9aPVip utNKc07rEEsUXf7s/MYPaesvwDSA3qkSPTVk5rD1XVgbbdxsT9yagM48k1MghlBd g4cb0VZi1G7/3PCZjjZ6DoVI+o//xcp1vwbmBkFiZyLSw== Received: by lepiller.eu (OpenSMTPD) with ESMTPSA id 87246e35 (TLSv1.3:AEAD-AES256-GCM-SHA384:256:NO) for ; Sun, 28 Nov 2021 16:44:32 +0000 (UTC) Date: Sun, 28 Nov 2021 17:44:26 +0100 From: Julien Lepiller To: guix-patches@gnu.org Subject: [PATCH] gnu: coq: Update to 8.14.0. Message-ID: <20211128174408.747bccba@tachikoma.lepiller.eu> X-Mailer: Claws Mail 4.0.0 (GTK+ 3.24.24; x86_64-pc-linux-gnu) MIME-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Received-SPF: pass client-ip=89.234.186.109; envelope-from=julien@lepiller.eu; helo=lepiller.eu 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.3 (-) X-Debbugs-Envelope-To: submit 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 (--) Hi Guix! this small series updates coq to its latest version. From debbugs-submit-bounces@debbugs.gnu.org Sun Nov 28 12:27:24 2021 Received: (at 52164) by debbugs.gnu.org; 28 Nov 2021 17:27:24 +0000 Received: from localhost ([127.0.0.1]:36304 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mrNxU-0007Lj-4B for submit@debbugs.gnu.org; Sun, 28 Nov 2021 12:27:24 -0500 Received: from lepiller.eu ([89.234.186.109]:38862) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mrNxP-0007LS-8i for 52164@debbugs.gnu.org; Sun, 28 Nov 2021 12:27:22 -0500 Received: from lepiller.eu (localhost [127.0.0.1]) by lepiller.eu (OpenSMTPD) with ESMTP id 81c079cc for <52164@debbugs.gnu.org>; Sun, 28 Nov 2021 17:27:17 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed; d=lepiller.eu; h=from:to :subject:date:message-id:in-reply-to:references:mime-version :content-transfer-encoding; s=dkim; bh=LmiuDsE7ZXPdLCtp5qIvI5THL Abx6j6fmlrYKnuTOlg=; b=QUGOkat3IYgnVVn+yKIv2NxvpMGyslC9ONj+9LADk tieJwO4Pwv44dYYbIenUsQuH9AlRmobf/iKU/NLXGu9gzXc/ctwT4fyYw+1NC1cr 8al3NTwW2v5r+r+N0tH+jfUsZji7uUw+A5uETEdu9DH6ULXDCQqdbVr7ftd1sxvc 8SwT1m8PwFeSA4/30uVjghTPjvNFvmn0ch9WrjQ++3eCTDENwSw4DZtOqz+diVHN GEotS/TZZ6K2Zs0BCv61YKqWwH4SZokLq5GVN/Uh7m0jYWJgOstaS6Ywod9XMfL2 09HHhXzhjkwxXlQ47Rfu2kZX5svgWAzg3cjuLly7JCO0A== Received: by lepiller.eu (OpenSMTPD) with ESMTPSA id ac92b9c5 (TLSv1.3:AEAD-AES256-GCM-SHA384:256:NO) for <52164@debbugs.gnu.org>; Sun, 28 Nov 2021 17:27:17 +0000 (UTC) From: Julien Lepiller To: 52164@debbugs.gnu.org Subject: [PATCH 1/3] gnu: ocaml-semantics: Update to 8.14.0. Date: Sun, 28 Nov 2021 18:27:09 +0100 Message-Id: <854d751e7d512c66acb72225120168e5ee16d6a2.1638120398.git.julien@lepiller.eu> X-Mailer: git-send-email 2.34.0 In-Reply-To: <20211128174408.747bccba@tachikoma.lepiller.eu> References: <20211128174408.747bccba@tachikoma.lepiller.eu> MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Spam-Score: -0.0 (/) X-Debbugs-Envelope-To: 52164 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 | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index a27ec53ecb..e3c4190ac3 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -576,7 +576,7 @@ (define-public coq-equations (define-public coq-semantics (package (name "coq-semantics") - (version "8.13.0") + (version "8.14.0") (source (origin (method git-fetch) @@ -591,7 +591,7 @@ (define-public coq-semantics (file-name (git-file-name name version)) (sha256 (base32 - "0m5si9dsv96z92gy4xaqz8mzyz8zp7j1sp542l0wzsp5xgyfpc7i")))) + "0ldrp86bfcjpzsb08p45sgs3aczjzr1gksy5dsf7pxapg05pc7ac")))) (build-system gnu-build-system) (native-inputs `(("coq" ,coq) -- 2.33.1 From debbugs-submit-bounces@debbugs.gnu.org Sun Nov 28 12:27:27 2021 Received: (at 52164) by debbugs.gnu.org; 28 Nov 2021 17:27:27 +0000 Received: from localhost ([127.0.0.1]:36306 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mrNxX-0007Ly-DS for submit@debbugs.gnu.org; Sun, 28 Nov 2021 12:27:27 -0500 Received: from lepiller.eu ([89.234.186.109]:38862) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mrNxS-0007LS-IQ for 52164@debbugs.gnu.org; Sun, 28 Nov 2021 12:27:23 -0500 Received: from lepiller.eu (localhost [127.0.0.1]) by lepiller.eu (OpenSMTPD) with ESMTP id 7c811c7d for <52164@debbugs.gnu.org>; Sun, 28 Nov 2021 17:27:18 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed; d=lepiller.eu; h=from:to :subject:date:message-id:in-reply-to:references:mime-version :content-transfer-encoding; s=dkim; bh=c/Tr1jMIU4f18LwqyCQMkA0rP WcB0puNrW1dvR+26xc=; b=P85/C/x1kzGK9CBiLwVgkDygsxikOvOBH6ggwDeCH TzCatwUT0LLoFrDFzXiY4BHsLWu2kG5nGRmxtN0dWAaivMFgrZRQXRybOTJmWRzZ CtwtK2u7WLGVyN7jr+O7vYY5mM1dDIaQuaFgjZfCDmY4WNpS/uCtObkATMa7RKe+ qdEHlsn2wCw1DW/Uxe6D5G+kH5CHzZvZ60ydW7npgHTGzYFXGo0thPrA/zZ7K+zv Tluk/sjpfJQTeyVpkhmVKunHe6yfewWxpSOaWTfRCGxI7lDWGY5P933LMecwN0u9 27O7NOVWwBuNCGUMAPQ/wf2YHLhp4oSduivWn3z1/arcQ== Received: by lepiller.eu (OpenSMTPD) with ESMTPSA id 8577d61a (TLSv1.3:AEAD-AES256-GCM-SHA384:256:NO) for <52164@debbugs.gnu.org>; Sun, 28 Nov 2021 17:27:17 +0000 (UTC) From: Julien Lepiller To: 52164@debbugs.gnu.org Subject: [PATCH 2/3] gnu: proof-general: Update to latest commit. Date: Sun, 28 Nov 2021 18:27:10 +0100 Message-Id: <2e3b3fe2ed163577a854f10b9a1c8531eabcadf6.1638120398.git.julien@lepiller.eu> X-Mailer: git-send-email 2.34.0 In-Reply-To: <20211128174408.747bccba@tachikoma.lepiller.eu> References: <20211128174408.747bccba@tachikoma.lepiller.eu> MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Spam-Score: -0.0 (/) X-Debbugs-Envelope-To: 52164 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 (proof-general): Update to latest commit. --- gnu/packages/coq.scm | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index e3c4190ac3..2045901aed 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -119,9 +119,9 @@ (define-public coq-ide (define-public proof-general ;; The latest release is from 2016 and there has been more than 450 commits ;; since then. - ;; Commit from 2021-06-07. - (let ((commit "bc86736abb728ec0d28abc90ef0adae21d29a66a") - (revision "0")) + ;; Commit from 2021-11-25. + (let ((commit "1b1083e86e0cddc20ff2f1a6b25c7a7eee2edf02") + (revision "1")) (package (name "proof-general") (version (git-version "4.4" revision commit)) @@ -133,7 +133,7 @@ (define-public proof-general (file-name (git-file-name name version)) (sha256 (base32 - "00cga3n9nj2xa3ivb0fdkkdx3k11fp4879y188738631yd1x2lsa")))) + "1pnysczhscapgwmvf6ix7f31lf3hnh8h977bfll1m7jlxl9b9c0j")))) (build-system gnu-build-system) (native-inputs `(("emacs" ,emacs-minimal) -- 2.33.1 From debbugs-submit-bounces@debbugs.gnu.org Sun Nov 28 12:27:35 2021 Received: (at 52164) by debbugs.gnu.org; 28 Nov 2021 17:27:35 +0000 Received: from localhost ([127.0.0.1]:36308 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mrNxX-0007M0-PW for submit@debbugs.gnu.org; Sun, 28 Nov 2021 12:27:35 -0500 Received: from lepiller.eu ([89.234.186.109]:38862) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mrNxT-0007LS-FS for 52164@debbugs.gnu.org; Sun, 28 Nov 2021 12:27:24 -0500 Received: from lepiller.eu (localhost [127.0.0.1]) by lepiller.eu (OpenSMTPD) with ESMTP id d30ff2c9 for <52164@debbugs.gnu.org>; Sun, 28 Nov 2021 17:27:18 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed; d=lepiller.eu; h=from:to :subject:date:message-id:in-reply-to:references:mime-version :content-transfer-encoding; s=dkim; bh=680gNOFoHQqSlwNBKhvY2Y9hw 7SdJO0aaWHGCA98VMI=; b=cu3A/CvXYlq8+H6e4I6LoYbY61xyLV6mRqKnqhX9S bRWS3sDddXVG3ZlNCS/bKUg6zVf75OiVDr+kDw0hJOD6IbdV2AX+Vx6SKdvjZZFC M9BeAKJ2SNkgQX6yBtBDp6SP1TjTTFNw3VNPtoZwLkxIy9Ia0DpanrphmNI2pyJv eVEtxSE/elDefQCpW91cJO8uOGoTvLIAUoH4VLgIdto9CHX1Ztqp/PlUm/iOlcBo LbS1G8Bt1Y9OBSQjVf7sFxdNHuSe5NgUYy5veaV+nuLNTkVm5RKEabyxvYOObhq+ v6VJpEsgN/slNECTUnXZZVEQzY/Ias/ZSYVS8+wSkJrnQ== Received: by lepiller.eu (OpenSMTPD) with ESMTPSA id d187f1c7 (TLSv1.3:AEAD-AES256-GCM-SHA384:256:NO) for <52164@debbugs.gnu.org>; Sun, 28 Nov 2021 17:27:18 +0000 (UTC) From: Julien Lepiller To: 52164@debbugs.gnu.org Subject: [PATCH 3/3] gnu: coq: Update to 8.14.0. Date: Sun, 28 Nov 2021 18:27:11 +0100 Message-Id: X-Mailer: git-send-email 2.34.0 In-Reply-To: <20211128174408.747bccba@tachikoma.lepiller.eu> References: <20211128174408.747bccba@tachikoma.lepiller.eu> MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Spam-Score: -0.0 (/) X-Debbugs-Envelope-To: 52164 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.14.0. (coq-bignums): Update to 8.14.0. (coq-equations): Update to 1.3. * gnu/packages/patches/coq-fix-envvars.patch: New file. * gnu/local.mk (dist_patch_DATA): Add it. --- gnu/local.mk | 1 + gnu/packages/coq.scm | 65 +++++++--- gnu/packages/patches/coq-fix-envvars.patch | 139 +++++++++++++++++++++ 3 files changed, 188 insertions(+), 17 deletions(-) create mode 100644 gnu/packages/patches/coq-fix-envvars.patch diff --git a/gnu/local.mk b/gnu/local.mk index efe153faf2..b26907a211 100644 --- a/gnu/local.mk +++ b/gnu/local.mk @@ -951,6 +951,7 @@ dist_patch_DATA = \ %D%/packages/patches/collectd-5.11.0-noinstallvar.patch \ %D%/packages/patches/combinatorial-blas-awpm.patch \ %D%/packages/patches/combinatorial-blas-io-fix.patch \ + %D%/packages/patches/coq-fix-envvars.patch \ %D%/packages/patches/coreutils-ls.patch \ %D%/packages/patches/cpuinfo-system-libraries.patch \ %D%/packages/patches/crawl-upgrade-saves.patch \ diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index 2045901aed..b6a5ff357c 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -49,10 +49,10 @@ (define-module (gnu packages coq) #:use-module (guix utils) #:use-module ((srfi srfi-1) #:hide (zip))) -(define-public coq +(define-public coq-core (package - (name "coq") - (version "8.13.2") + (name "coq-core") + (version "8.14.0") (source (origin (method git-fetch) @@ -62,25 +62,31 @@ (define-public coq (file-name (git-file-name name version)) (sha256 (base32 - "15r0cm3p9dlsxbg0lf05njjp1xi1y74vxvq6drxjykax67x95l8a")))) + "0iachapmdwvwwlvkrb2yxhqqrgzs70zyr1c9v1jdb1awx3bp68hf")) + (patches (search-patches "coq-fix-envvars.patch")))) (native-search-paths (list (search-path-specification (variable "COQPATH") - (files (list "lib/coq/user-contrib"))) + (files (list "lib/ocaml/site-lib/coq/user-contrib" + "lib/coq/user-contrib"))) (search-path-specification - (variable "COQLIB") - (files (list "lib/ocaml/site-lib/coq")) + (variable "COQLIBPATH") + (files (list "lib/ocaml/site-lib/coq"))) + (search-path-specification + (variable "COQCORELIB") + (files (list "lib/ocaml/site-lib/coq-core")) (separator #f)))) (build-system dune-build-system) (inputs `(("gmp" ,gmp) ("ocaml-zarith" ,ocaml-zarith))) (native-inputs - `(("which" ,which))) + `(("ocaml-ounit2" ,ocaml-ounit2) + ("which" ,which))) (arguments - `(#:package "coq" - #:test-target "test-suite")) - (properties '((upstream-name . "coq"))) ; for inherited packages + `(#:package "coq-core" + #:test-target ".")) + (properties '((upstream-name . "coq"))) ; also for inherited packages (home-page "https://coq.inria.fr") (synopsis "Proof assistant for higher-order logic") (description @@ -91,6 +97,31 @@ (define-public coq ;; Some of the documentation is distributed under opl1.0+. (license (list license:lgpl2.1 license:opl1.0+)))) +(define-public coq-stdlib + (package + (inherit coq-core) + (name "coq-stdlib") + (arguments + `(#:package "coq-stdlib" + #:test-target ".")) + (inputs + `(("coq-core" ,coq-core) + ("gmp" ,gmp) + ("ocaml-zarith" ,ocaml-zarith))) + (native-inputs '()))) + +(define-public coq + (package + (inherit coq-core) + (name "coq") + (arguments + `(#:package "coq" + #:test-target ".")) + (propagated-inputs + `(("coq-core" ,coq-core) + ("coq-stdlib" ,coq-stdlib))) + (native-inputs '()))) + (define-public coq-ide-server (package (inherit coq) @@ -410,7 +441,7 @@ (define-public coq-coquelicot (define-public coq-bignums (package (name "coq-bignums") - (version "8.13.0") + (version "8.14.0") (source (origin (method git-fetch) (uri (git-reference @@ -419,7 +450,7 @@ (define-public coq-bignums (file-name (git-file-name name version)) (sha256 (base32 - "1n66i7hd9222b2ks606mak7m4f0dgy02xgygjskmmav6h7g2sx7y")))) + "0jsgdvj0ddhkls32krprp34r64y1rb5mwxl34fgaxk2k4664yq06")))) (build-system gnu-build-system) (native-inputs `(("ocaml" ,ocaml) @@ -471,7 +502,7 @@ (define-public coq-interval (arguments `(#:configure-flags (list (string-append "COQUSERCONTRIB=" (assoc-ref %outputs "out") - "/lib/coq/user-contrib")) + "/lib/ocaml/site-lib/coq/user-contrib")) #:phases (modify-phases %standard-phases (add-before 'configure 'fix-remake @@ -537,16 +568,16 @@ (define-public coq-autosubst (define-public coq-equations (package (name "coq-equations") - (version "1.2.4") + (version "1.3") (source (origin (method git-fetch) (uri (git-reference (url "https://github.com/mattam82/Coq-Equations") - (commit (string-append "v" version "-8.13")))) + (commit (string-append "v" version "-8.14")))) (file-name (git-file-name name version)) (sha256 (base32 - "0i014lshsdflzw6h0qxra9d2f0q82vffxv2f29awbb9ad0p4rq4q")))) + "19bj9nncd1r9g4273h5qx35gs3i4bw5z9bhjni24b413hyj55hkv")))) (build-system gnu-build-system) (native-inputs `(("ocaml" ,ocaml) diff --git a/gnu/packages/patches/coq-fix-envvars.patch b/gnu/packages/patches/coq-fix-envvars.patch new file mode 100644 index 0000000000..deecf5ce74 --- /dev/null +++ b/gnu/packages/patches/coq-fix-envvars.patch @@ -0,0 +1,139 @@ +From ebe09fcac72b21d17c4e8fe6edc1b6076a4ae97c Mon Sep 17 00:00:00 2001 +From: Julien Lepiller +Date: Sun, 21 Nov 2021 00:38:03 +0100 +Subject: [PATCH] Fix environment variable usage. + +--- + checker/checker.ml | 2 ++ + lib/envars.ml | 26 ++++++++++++++++---------- + sysinit/coqargs.ml | 3 ++- + sysinit/coqloadpath.ml | 3 ++- + sysinit/coqloadpath.mli | 2 +- + tools/coqdep.ml | 2 +- + 6 files changed, 24 insertions(+), 14 deletions(-) + +diff --git a/checker/checker.ml b/checker/checker.ml +index f55ed9e8d6..3b797729ed 100644 +--- a/checker/checker.ml ++++ b/checker/checker.ml +@@ -104,6 +104,7 @@ let set_include d p = + (* Initializes the LoadPath *) + let init_load_path () = + let coqlib = Envars.coqlib () in ++ let coqcorelib = Envars.coqcorelib () in + let user_contrib = coqlib/"user-contrib" in + let xdg_dirs = Envars.xdg_dirs in + let coqpath = Envars.coqpath in +@@ -111,6 +112,7 @@ let init_load_path () = + CPath.choose_existing + [ CPath.make [ coqlib ; "plugins" ] + ; CPath.make [ coqlib ; ".."; "coq-core"; "plugins" ] ++ ; CPath.make [ coqcorelib ; "plugins" ] + ] |> function + | None -> + CErrors.user_err (Pp.str "Cannot find plugins directory") +diff --git a/lib/envars.ml b/lib/envars.ml +index 750bd60e71..c7affbd437 100644 +--- a/lib/envars.ml ++++ b/lib/envars.ml +@@ -127,15 +127,21 @@ let check_file_else ~dir ~file oth = + let guess_coqlib fail = + getenv_else "COQLIB" (fun () -> + let prelude = "theories/Init/Prelude.vo" in +- check_file_else ~dir:Coq_config.coqlibsuffix ~file:prelude +- (fun () -> +- if Sys.file_exists (Coq_config.coqlib / prelude) +- then Coq_config.coqlib +- else +- fail "cannot guess a path for Coq libraries; please use -coqlib option \ +- or ensure you have installed the package containing Coq's stdlib (coq-stdlib in OPAM) \ +- If you intend to use Coq without a standard library, the -boot -noinit options must be used.") +- ) ++ let coqlibpath = getenv_else "COQLIBPATH" (fun () -> Coq_config.coqlibsuffix) in ++ let paths = path_to_list coqlibpath in ++ let valid_paths = ++ List.filter ++ (fun dir -> (check_file_else ~dir:dir ~file:prelude (fun () -> "")) <> "") ++ paths in ++ match valid_paths with ++ | [] -> ++ if Sys.file_exists (Coq_config.coqlib / prelude) ++ then Coq_config.coqlib ++ else ++ fail "cannot guess a path for Coq libraries; please use -coqlib option \ ++ or ensure you have installed the package containing Coq's stdlib (coq-stdlib in OPAM) \ ++ If you intend to use Coq without a standard library, the -boot -noinit options must be used." ++ | p::_ -> p) + + let coqlib_ref : string option ref = ref None + let set_user_coqlib path = coqlib_ref := Some path +@@ -208,7 +214,7 @@ let xdg_dirs ~warn = + let print_config ?(prefix_var_name="") f coq_src_subdirs = + let open Printf in + fprintf f "%sCOQLIB=%s/\n" prefix_var_name (coqlib ()); +- fprintf f "%sCOQCORELIB=%s/\n" prefix_var_name (coqlib () / "../coq-core/"); ++ fprintf f "%sCOQCORELIB=%s/\n" prefix_var_name (coqcorelib ()); + fprintf f "%sDOCDIR=%s/\n" prefix_var_name (docdir ()); + fprintf f "%sOCAMLFIND=%s\n" prefix_var_name (ocamlfind ()); + fprintf f "%sCAMLFLAGS=%s\n" prefix_var_name Coq_config.caml_flags; +diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml +index 00f70a5fea..8325623a63 100644 +--- a/sysinit/coqargs.ml ++++ b/sysinit/coqargs.ml +@@ -453,7 +453,8 @@ let build_load_path opts = + if opts.pre.boot then [],[] + else + let coqlib = Envars.coqlib () in +- Coqloadpath.init_load_path ~coqlib in ++ let coqcorelib = Envars.coqcorelib () in ++ Coqloadpath.init_load_path ~coqlib ~coqcorelib in + ml_path @ opts.pre.ml_includes , + vo_path @ opts.pre.vo_includes + +diff --git a/sysinit/coqloadpath.ml b/sysinit/coqloadpath.ml +index 95ae5da3de..a58cfe6928 100644 +--- a/sysinit/coqloadpath.ml ++++ b/sysinit/coqloadpath.ml +@@ -35,7 +35,7 @@ let build_userlib_path ~unix_path = + else [], [] + + (* LoadPath for Coq user libraries *) +-let init_load_path ~coqlib = ++let init_load_path ~coqlib ~coqcorelib = + + let open Loadpath in + let user_contrib = coqlib/"user-contrib" in +@@ -50,6 +50,7 @@ let init_load_path ~coqlib = + CPath.choose_existing + [ CPath.make [ coqlib ; "plugins" ] + ; CPath.make [ coqlib ; ".."; "coq-core"; "plugins" ] ++ ; CPath.make [ coqcorelib ; "plugins" ] + ] |> function + | None -> + CErrors.user_err (Pp.str "Cannot find plugins directory") +diff --git a/sysinit/coqloadpath.mli b/sysinit/coqloadpath.mli +index d853e9ea54..43c6dfa134 100644 +--- a/sysinit/coqloadpath.mli ++++ b/sysinit/coqloadpath.mli +@@ -12,5 +12,5 @@ + includes (in-order) Coq's standard library, Coq's [user-contrib] + folder, and directories specified in [COQPATH] and [XDG_DIRS] *) + val init_load_path +- : coqlib:CUnix.physical_path ++ : coqlib:CUnix.physical_path -> coqcorelib:CUnix.physical_path + -> CUnix.physical_path list * Loadpath.vo_path list +diff --git a/tools/coqdep.ml b/tools/coqdep.ml +index c1c87993e1..6c78e10866 100644 +--- a/tools/coqdep.ml ++++ b/tools/coqdep.ml +@@ -33,7 +33,7 @@ let coqdep () = + let coqlib = Envars.coqlib () in + let coq_plugins_dir = Filename.concat (Envars.coqcorelib ()) "plugins" in + if not (Sys.file_exists coq_plugins_dir) then +- CErrors.user_err Pp.(str "coqdep: cannot find plugins directory for coqlib: " ++ str coqlib ++ fnl ()); ++ CErrors.user_err Pp.(str "coqdep: cannot find plugins directory " ++ str coq_plugins_dir ++ str " for coqlib: " ++ str coqlib ++ fnl ()); + CD.add_rec_dir_import CD.add_coqlib_known (coqlib//"theories") ["Coq"]; + CD.add_rec_dir_import CD.add_coqlib_known (coq_plugins_dir) ["Coq"]; + let user = coqlib//"user-contrib" in +-- +2.33.1 -- 2.33.1 From debbugs-submit-bounces@debbugs.gnu.org Mon Nov 29 04:42:55 2021 Received: (at 52164) by debbugs.gnu.org; 29 Nov 2021 09:42:55 +0000 Received: from localhost ([127.0.0.1]:37078 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mrdBX-0002X8-8i for submit@debbugs.gnu.org; Mon, 29 Nov 2021 04:42:55 -0500 Received: from mail-wr1-f41.google.com ([209.85.221.41]:35591) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mrdBW-0002Wp-2W for 52164@debbugs.gnu.org; Mon, 29 Nov 2021 04:42:54 -0500 Received: by mail-wr1-f41.google.com with SMTP id i5so35352495wrb.2 for <52164@debbugs.gnu.org>; Mon, 29 Nov 2021 01:42:53 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=from:to:cc:subject:references:date:in-reply-to:message-id :user-agent:mime-version; bh=m5SY9D621E1Wkhb9Kj5Nk55OZiMSK8B23ecjrECRV3E=; b=LG4VAyVuXy3KE81xqEjKrI5NxrQumJhOj/BcIxIIRge7XdkEBq+10uQBs8dIfQXKm0 AzozSjicrNCQYTPMlelcg9fTCH0RJ35niFT2/UZnxp7Pz0rsAa/e9VEbQsg1k2VwNaSM X8IA3BhqINJhVIR8iUBj+Ql/Zi3jpcC3oTtQh2dDPxo/YnV+sNFio02DxqYDIZhKp3UQ zn1zwPJ1i/DX/xSCSizvitDTNyroixKCtGr4AaV5DSHgJ6J8dcfUSvxyYTitBf9QvgFT Bcgr4kpcaqpSE5wUEiq/Ho9TRPUqD0VEoqC+fHDCm3e+RUk2aHa26TLqpE9LngJf+wlH mhCQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:from:to:cc:subject:references:date:in-reply-to :message-id:user-agent:mime-version; bh=m5SY9D621E1Wkhb9Kj5Nk55OZiMSK8B23ecjrECRV3E=; b=sJSDobTHLUi6e9wTmzrqV9X95eYlVS69mdE7FK/48eUu5QPn8z26YyFtbdVEqj0Dx0 9g1hkT9RsKdK6jazU3L0+tq8Yy0CwSLSTm6xtM3u2n0SjrDjjpLLAPSV0+v/iB5R4IdD 8Z7dJuwW6j6+fu1uAtybC8G7hAAqxIyy5pP0RHW50l1YVuUaDffDtLNiW9MkG8gvFsmO 8JQP/HUvn/buDHUnowFG8dBX2IMiRZNUf3hsZNQE6L/7bNhOx0T+jEWcf5aJzXAENEhu gxb/ULnhCJYLTand/+arsScTQwv+709/RUCI9HK1QhPTd9J1DwXNT6nXUtklsbtJB+bo 2RKA== X-Gm-Message-State: AOAM532fTHI+E45oBejfb1i6AoXxS5IIIJt0na8qmH07Osy/M0uT6b8G OF+IFa4w0MgnDh8m2A04xnFuqvIrIVY= X-Google-Smtp-Source: ABdhPJzOxEQrae5TaSjrsVGNxn0Tymo8JadLvmvxD7azrAaryxALDkI4wYZzONRGHoN4NPZv5VncqQ== X-Received: by 2002:a5d:6d0c:: with SMTP id e12mr32173811wrq.94.1638178968192; Mon, 29 Nov 2021 01:42:48 -0800 (PST) Received: from jack-Precision-7820-Tower ([193.48.40.117]) by smtp.gmail.com with ESMTPSA id n32sm14734760wms.42.2021.11.29.01.42.47 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 29 Nov 2021 01:42:47 -0800 (PST) From: zimoun To: Julien Lepiller Subject: Re: bug#52164: [PATCH] gnu: coq: Update to 8.14.0. References: <20211128174408.747bccba@tachikoma.lepiller.eu> <2e3b3fe2ed163577a854f10b9a1c8531eabcadf6.1638120398.git.julien@lepiller.eu> Date: Mon, 29 Nov 2021 10:06:09 +0100 In-Reply-To: <2e3b3fe2ed163577a854f10b9a1c8531eabcadf6.1638120398.git.julien@lepiller.eu> (Julien Lepiller's message of "Sun, 28 Nov 2021 18:27:10 +0100") Message-ID: <865ysbl4am.fsf_-_@gmail.com> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/27.2 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 52164 Cc: 52164@debbugs.gnu.org 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 (-) On dim., 28 nov. 2021 at 18:27, Julien Lepiller wrote: > * gnu/packages/coq.scm (proof-general): Update to latest commit. > --- > gnu/packages/coq.scm | 8 ++++---- > 1 file changed, 4 insertions(+), 4 deletions(-) LGTM. Cheers, simon From debbugs-submit-bounces@debbugs.gnu.org Mon Nov 29 04:43:11 2021 Received: (at 52164) by debbugs.gnu.org; 29 Nov 2021 09:43:11 +0000 Received: from localhost ([127.0.0.1]:37080 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mrdBb-0002XV-QK for submit@debbugs.gnu.org; Mon, 29 Nov 2021 04:43:11 -0500 Received: from mail-wm1-f45.google.com ([209.85.128.45]:39602) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mrdBW-0002Wr-Om for 52164@debbugs.gnu.org; Mon, 29 Nov 2021 04:42:55 -0500 Received: by mail-wm1-f45.google.com with SMTP id n33-20020a05600c502100b0032fb900951eso16257793wmr.4 for <52164@debbugs.gnu.org>; Mon, 29 Nov 2021 01:42:54 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=from:to:cc:subject:references:date:in-reply-to:message-id :user-agent:mime-version:content-transfer-encoding; bh=lYjb2GeXr5FH2HEhI5b1hJF8OkGBX2QehXBiHlgJVZQ=; b=RGhzhh5lf4cQfiGnhSjSU6VLRQW2GLS/sy5CL+JwdX/SB+VAEr3NGtDMP+8/cKTKhc mEHC4k4iDGwOvVgdBGOUlf9BVlI3ble0Y4d+u+eKxxQMbN0bXbw8ZJxaZGjAaQkgbyNZ WCpwVZDK0SWYSLpqt44wzcjfD2Yd3CsaRlX3U1jY5d4wpqVuOXi+80xDZePZytZl1gam pjnQ7dPgkjQeJys94Rf3fH5dp1V/OWyxY96IMSqmSUMHOG8uHv0Z49k0Tt1nwSRGJJrY HSkZXXKdAwBwEWLWX1Uf31KZuD3UwzpeMelPWwKW33aduWMA0x9df5Y0kgGlt4sbzDlS 5E/Q== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:from:to:cc:subject:references:date:in-reply-to :message-id:user-agent:mime-version:content-transfer-encoding; bh=lYjb2GeXr5FH2HEhI5b1hJF8OkGBX2QehXBiHlgJVZQ=; b=c6B+f6AxxU78BkslUX23jph09namtkmrGzifMuW54YsTJGJg6RuM6mBpnDB4NEW0RG Bi3ssvUXu8Cz/77/No4ijtZFdSmtQipTah3KzFWCEJO6jl2LXE74JSZRFLS/eDeV68Lg FFzaIFf7pjW6IU6cN9b3EgpSlWJQrG68DyokxKftdrSJXDpJN2I5Qy7Dl9GZQEUPb+U7 QsOltAgGec/H0LvIx4d1QTyy7uxrQUNBfyBvs2Qg6/V47JsZKQGvMo9Rz+qwX0KMZPsV tz91eGSomBUiBK/FBtQt02FWjnP7RZ3fLqtuTfV72VbWQ5ymKd9VtWJeRrGmPKwvNRzA NBXg== X-Gm-Message-State: AOAM532jvYrf5L5AN36XzTYVDJ2aCI89pvqNRbViab2ZvuN6aoWOaxmr 1iR0VKUD4EKET0u8mCHSuBERxVND/fw= X-Google-Smtp-Source: ABdhPJwdk2vFh2MyRdEVVxFzfBZpQwy1nYw4R2xT8qdT87aQFX8b2JyGeJqo8/MnbezoFUaqL8gKZQ== X-Received: by 2002:a05:600c:1990:: with SMTP id t16mr34473543wmq.48.1638178969130; Mon, 29 Nov 2021 01:42:49 -0800 (PST) Received: from jack-Precision-7820-Tower ([193.48.40.117]) by smtp.gmail.com with ESMTPSA id m14sm17570928wrp.28.2021.11.29.01.42.48 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 29 Nov 2021 01:42:48 -0800 (PST) From: zimoun To: Julien Lepiller Subject: Re: bug#52164: [PATCH] gnu: coq: Update to 8.14.0. References: <20211128174408.747bccba@tachikoma.lepiller.eu> Date: Mon, 29 Nov 2021 10:42:25 +0100 In-Reply-To: (Julien Lepiller's message of "Sun, 28 Nov 2021 18:27:11 +0100") Message-ID: <8635nfl2m6.fsf_-_@gmail.com> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/27.2 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 52164 Cc: 52164@debbugs.gnu.org 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 (-) Hi, On dim., 28 nov. 2021 at 18:27, Julien Lepiller wrote: > * gnu/packages/coq.scm (coq): Update to 8.14.0. > (coq-bignums): Update to 8.14.0. > (coq-equations): Update to 1.3. > * gnu/packages/patches/coq-fix-envvars.patch: New file. > * gnu/local.mk (dist_patch_DATA): Add it. > --- > gnu/local.mk | 1 + > gnu/packages/coq.scm | 65 +++++++--- > gnu/packages/patches/coq-fix-envvars.patch | 139 +++++++++++++++++++++ > 3 files changed, 188 insertions(+), 17 deletions(-) > create mode 100644 gnu/packages/patches/coq-fix-envvars.patch [...] > -(define-public coq > +(define-public coq-core [...] > - `(("which" ,which))) > + `(("ocaml-ounit2" ,ocaml-ounit2) > + ("which" ,which))) This =E2=80=99which=E2=80=99 could be removed. :-) > +(define-public coq-stdlib > + (package > + (inherit coq-core) > + (name "coq-stdlib") > + (arguments > + `(#:package "coq-stdlib" > + #:test-target ".")) > + (inputs > + `(("coq-core" ,coq-core) > + ("gmp" ,gmp) > + ("ocaml-zarith" ,ocaml-zarith))) > + (native-inputs '()))) > + > +(define-public coq > + (package > + (inherit coq-core) > + (name "coq") > + (arguments > + `(#:package "coq" > + #:test-target ".")) > + (propagated-inputs > + `(("coq-core" ,coq-core) > + ("coq-stdlib" ,coq-stdlib))) > + (native-inputs '()))) With this approach, 3 builds. Is it required by kind-of Coq bootstrap? > (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. > diff --git a/gnu/packages/patches/coq-fix-envvars.patch b/gnu/packages/pa= tches/coq-fix-envvars.patch > new file mode 100644 > index 0000000000..deecf5ce74 > --- /dev/null > +++ b/gnu/packages/patches/coq-fix-envvars.patch > @@ -0,0 +1,139 @@ > +From ebe09fcac72b21d17c4e8fe6edc1b6076a4ae97c Mon Sep 17 00:00:00 2001 > +From: Julien Lepiller > +Date: Sun, 21 Nov 2021 00:38:03 +0100 > +Subject: [PATCH] Fix environment variable usage. > + > +--- > + checker/checker.ml | 2 ++ > + lib/envars.ml | 26 ++++++++++++++++---------- > + sysinit/coqargs.ml | 3 ++- > + sysinit/coqloadpath.ml | 3 ++- > + sysinit/coqloadpath.mli | 2 +- > + tools/coqdep.ml | 2 +- > + 6 files changed, 24 insertions(+), 14 deletions(-) This fix LGTM. Otherwise, LTGM. Cheers, simon From debbugs-submit-bounces@debbugs.gnu.org Mon Nov 29 04:43:11 2021 Received: (at 52164) by debbugs.gnu.org; 29 Nov 2021 09:43:11 +0000 Received: from localhost ([127.0.0.1]:37083 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mrdBn-0002Y7-5W for submit@debbugs.gnu.org; Mon, 29 Nov 2021 04:43:11 -0500 Received: from mail-wm1-f49.google.com ([209.85.128.49]:34645) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mrdBU-0002Wn-N2 for 52164@debbugs.gnu.org; Mon, 29 Nov 2021 04:42:55 -0500 Received: by mail-wm1-f49.google.com with SMTP id m25-20020a7bcb99000000b0033aa12cdd33so5556579wmi.1 for <52164@debbugs.gnu.org>; Mon, 29 Nov 2021 01:42:52 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=from:to:cc:subject:references:date:in-reply-to:message-id :user-agent:mime-version; bh=/JHom7vZwR408NFxs1CIoQtHsuRqIdhzpZ1nBXMdofk=; b=ZUXPAYlT0NiZrCheNzTO+5Q108Fe7PvTcPbVFyyP9EGR0OoB3HxooSOOyLdvI7Dig8 7jNqWRb8D+2iT7R6x4UDXakwPN2uSdKGdnYTkkIJZD8vlEx5gBwtu8nufCrSscE1SJ6V /F494JeFpyKPxE/Q+dEgt8HC3P069epLp71G9Mf8sJ9+84+wh5Lv66QXON6VFcd3IKKT VTMnjCAxMPeQrJOV2jh5S7VnUAO2qQ2metDklQJWjrpiBDn5OJ7HaAOw9VI3Qn8UpBGk p6QDmjDEXuXYp5PtAksYB0Xr1UoDY2i9FfF3j0raa7p6b16Bzx6nB/QEQPxdykrdM+hQ i0Jw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:from:to:cc:subject:references:date:in-reply-to :message-id:user-agent:mime-version; bh=/JHom7vZwR408NFxs1CIoQtHsuRqIdhzpZ1nBXMdofk=; b=7PMXGF06EvNncQm/nNpbAtL4oVJx582gejcMnFn88BJjX1wEbViDkbhd3Y/i8WRnLE OmRUzoEok36UJ2nn7IofBUgPvMn3NuBiuKV15SYgIvyLjXwHbxpi+qHt/gipZC3wgLIe GF7JOAGdl5C2GFB1YIXEjlKdDkzqTBbmrulYfqjLQB9GIUWxYL2alJFeGYEgLy7oq6BJ HFv4h/BJgD0+95rHcvLGpq5FWwGoonAdcM585HO9DL4KOZmplShtKaQjVtZgLVisEQ1j XOaX8X5+DfCLxqpnJI3+G2Pym2HixC6RSd0wlx+yrOD29cxACp47EwYlwNrV89aevOBj iAnQ== X-Gm-Message-State: AOAM532KNQZOzSiSex1nj4qtm+r/gAyTKyw2PvvKFzzWDD9BayENw+WA Nt6ki6yUUCkC+kakH5L6a3/llj2zvyY= X-Google-Smtp-Source: ABdhPJxhXxBx7hPOiJwHsnVDcRJTxSo6dKqG5m/HyenzbmitGT604UrgQo0+yBukG1IOS5jz8lH38A== X-Received: by 2002:a7b:cbd1:: with SMTP id n17mr35049308wmi.145.1638178966878; Mon, 29 Nov 2021 01:42:46 -0800 (PST) Received: from jack-Precision-7820-Tower ([193.48.40.117]) by smtp.gmail.com with ESMTPSA id s8sm13320028wro.19.2021.11.29.01.42.45 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 29 Nov 2021 01:42:46 -0800 (PST) From: zimoun To: Julien Lepiller Subject: [PATCH 1/3] gnu: ocaml-semantics: Update to 8.14.0. References: <20211128174408.747bccba@tachikoma.lepiller.eu> <854d751e7d512c66acb72225120168e5ee16d6a2.1638120398.git.julien@lepiller.eu> Date: Mon, 29 Nov 2021 10:05:39 +0100 In-Reply-To: <854d751e7d512c66acb72225120168e5ee16d6a2.1638120398.git.julien@lepiller.eu> (Julien Lepiller's message of "Sun, 28 Nov 2021 18:27:09 +0100") Message-ID: <868rx7l4bg.fsf_-_@gmail.com> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/27.2 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 52164 Cc: 52164@debbugs.gnu.org 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 (-) Hi Julien, Maybe something had been twisted. 1. Missing changelog. 2. Incorrect package name in commit oneline: coq-semantics and not ocaml-semantics. Cheers, simon On dim., 28 nov. 2021 at 18:27, Julien Lepiller wrote: > --- > gnu/packages/coq.scm | 4 ++-- > 1 file changed, 2 insertions(+), 2 deletions(-) > > diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm > index a27ec53ecb..e3c4190ac3 100644 > --- a/gnu/packages/coq.scm > +++ b/gnu/packages/coq.scm > @@ -576,7 +576,7 @@ (define-public coq-equations > (define-public coq-semantics > (package > (name "coq-semantics") > - (version "8.13.0") > + (version "8.14.0") > (source > (origin > (method git-fetch) > @@ -591,7 +591,7 @@ (define-public coq-semantics > (file-name (git-file-name name version)) > (sha256 > (base32 > - "0m5si9dsv96z92gy4xaqz8mzyz8zp7j1sp542l0wzsp5xgyfpc7i")))) > + "0ldrp86bfcjpzsb08p45sgs3aczjzr1gksy5dsf7pxapg05pc7ac")))) > (build-system gnu-build-system) > (native-inputs > `(("coq" ,coq) From debbugs-submit-bounces@debbugs.gnu.org Mon Nov 29 07:30:15 2021 Received: (at 52164) by debbugs.gnu.org; 29 Nov 2021 12:30:16 +0000 Received: from localhost ([127.0.0.1]:37308 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mrfnM-0007K6-Ep for submit@debbugs.gnu.org; Mon, 29 Nov 2021 07:30:15 -0500 Received: from lepiller.eu ([89.234.186.109]:42074) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mrfnK-0007ER-Qv for 52164@debbugs.gnu.org; Mon, 29 Nov 2021 07:30:07 -0500 Received: from lepiller.eu (localhost [127.0.0.1]) by lepiller.eu (OpenSMTPD) with ESMTP id e8be56e2; Mon, 29 Nov 2021 12:30:03 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed; d=lepiller.eu; h=date:from :to:cc:subject:in-reply-to:references:message-id:mime-version :content-type:content-transfer-encoding; s=dkim; bh=EVF/K18rrEB6 ZFAb5dvEfgHiEJrg+fjKL0eUa0XK1gg=; b=fR6y13NwtCDw31gcNphy/7TkAokU xXlRm+irfBZ+RnTaZP+WCHqPcQJ+DVU7SjCdNt5khgjbozjjj5MDt7q9WYxeK1h9 Ix3bN5o6eO18+SvpBLf4Mz8kiGls+LqlmdHPLdAqcYP+KYLmttfeMDFOITDBphGE /nGDhvtMn26WmX4uqPm+TH74shgrLlhurC3mNDBC4uuPJR/esAiF2/gyB2ajS59F mvROVkSlJ03JoLUhT2Ag+pWtdqIN4XhUAQZRGbR89XaYoqz6e2EheR9mbfV0Adkd xs8B7wzO4V8+OFek3LT5tIxUFRIUI30PHg3EDR/urzdgAJ8p8L7W+20hiQ== Received: by lepiller.eu (OpenSMTPD) with ESMTPSA id 3adeaeed (TLSv1.3:AEAD-AES256-GCM-SHA384:256:NO); Mon, 29 Nov 2021 12:30:02 +0000 (UTC) Date: Mon, 29 Nov 2021 07:29:51 -0500 From: Julien Lepiller To: zimoun Subject: Re: bug#52164: [PATCH] gnu: coq: Update to 8.14.0. User-Agent: K-9 Mail for Android In-Reply-To: <8635nfl2m6.fsf_-_@gmail.com> References: <20211128174408.747bccba@tachikoma.lepiller.eu> <8635nfl2m6.fsf_-_@gmail.com> Message-ID: <592223CF-588B-44EF-A35F-9E9FDB3E4865@lepiller.eu> MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-Spam-Score: -0.0 (/) X-Debbugs-Envelope-To: 52164 Cc: 52164@debbugs.gnu.org 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 (-) Le 29 novembre 2021 04:42:25 GMT-05:00, zimoun a =C3=A9crit=C2=A0: >Hi, > >On dim=2E, 28 nov=2E 2021 at 18:27, Julien Lepiller wrote: >> * gnu/packages/coq=2Escm (coq): Update to 8=2E14=2E0=2E >> (coq-bignums): Update to 8=2E14=2E0=2E >> (coq-equations): Update to 1=2E3=2E >> * gnu/packages/patches/coq-fix-envvars=2Epatch: New file=2E >> * gnu/local=2Emk (dist_patch_DATA): Add it=2E >> --- >> gnu/local=2Emk | 1 + >> gnu/packages/coq=2Escm | 65 +++++++--- >> gnu/packages/patches/coq-fix-envvars=2Epatch | 139 +++++++++++++++++++= ++ >> 3 files changed, 188 insertions(+), 17 deletions(-) >> create mode 100644 gnu/packages/patches/coq-fix-envvars=2Epatch > >[=2E=2E=2E] > >> -(define-public coq >> +(define-public coq-core > >[=2E=2E=2E] > >> - `(("which" ,which))) >> + `(("ocaml-ounit2" ,ocaml-ounit2) >> + ("which" ,which))) > >This =E2=80=99which=E2=80=99 could be removed=2E :-) > > >> +(define-public coq-stdlib >> + (package >> + (inherit coq-core) >> + (name "coq-stdlib") >> + (arguments >> + `(#:package "coq-stdlib" >> + #:test-target "=2E")) >> + (inputs >> + `(("coq-core" ,coq-core) >> + ("gmp" ,gmp) >> + ("ocaml-zarith" ,ocaml-zarith))) >> + (native-inputs '()))) >> + >> +(define-public coq >> + (package >> + (inherit coq-core) >> + (name "coq") >> + (arguments >> + `(#:package "coq" >> + #:test-target "=2E")) >> + (propagated-inputs >> + `(("coq-core" ,coq-core) >> + ("coq-stdlib" ,coq-stdlib))) >> + (native-inputs '()))) > >With this approach, 3 builds=2E Is it required by kind-of Coq bootstrap? Coq now uses dune, and it is split into core, stdlib anl coq=2E I prefer t= o build one dune package in each guix package, rather than everything, espe= cially since we want to separate coq-ide=2E > > >> (define-public coq-bignums >> (package >> (name "coq-bignums") >> - (version "8=2E13=2E0") >> + (version "8=2E14=2E0") > >This=E2=80=A6 > >> (define-public coq-equations >> (package >> (name "coq-equations") >> - (version "1=2E2=2E4") >> + (version "1=2E3") > >and this=E2=80=A6 Cannot they be upgraded by a separated commit? > >They will probably be broken with Coq 8=2E13 but if their upgrade is righ= t >after and pushed with the same batch, it is transparent and the >atomicity appears to me better=2E They're broken with coq 8=2E13, and the previous version is also broken wi= th coq 8=2E14=2E This is why I was able to update coq semantics independent= ly but not these two=2E > > >> diff --git a/gnu/packages/patches/coq-fix-envvars=2Epatch b/gnu/package= s/patches/coq-fix-envvars=2Epatch >> new file mode 100644 >> index 0000000000=2E=2Edeecf5ce74 >> --- /dev/null >> +++ b/gnu/packages/patches/coq-fix-envvars=2Epatch >> @@ -0,0 +1,139 @@ >> +From ebe09fcac72b21d17c4e8fe6edc1b6076a4ae97c Mon Sep 17 00:00:00 2001 >> +From: Julien Lepiller >> +Date: Sun, 21 Nov 2021 00:38:03 +0100 >> +Subject: [PATCH] Fix environment variable usage=2E >> + >> +--- >> + checker/checker=2Eml | 2 ++ >> + lib/envars=2Eml | 26 ++++++++++++++++---------- >> + sysinit/coqargs=2Eml | 3 ++- >> + sysinit/coqloadpath=2Eml | 3 ++- >> + sysinit/coqloadpath=2Emli | 2 +- >> + tools/coqdep=2Eml | 2 +- >> + 6 files changed, 24 insertions(+), 14 deletions(-) > >This fix LGTM=2E > > >Otherwise, LTGM=2E > > >Cheers, >simon From debbugs-submit-bounces@debbugs.gnu.org Mon Nov 29 08:21:38 2021 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: Subject: Re: bug#52164: [PATCH] gnu: coq: Update to 8.14.0. To: Julien Lepiller Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 52164 Cc: 52164@debbugs.gnu.org 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 (-) 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 From debbugs-submit-bounces@debbugs.gnu.org Mon Nov 29 08:39:42 2021 Received: (at 52164) by debbugs.gnu.org; 29 Nov 2021 13:39:42 +0000 Received: from localhost ([127.0.0.1]:37427 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mrgsf-0002l5-Rs for submit@debbugs.gnu.org; Mon, 29 Nov 2021 08:39:42 -0500 Received: from lepiller.eu ([89.234.186.109]:42302) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mrgsd-0002ks-HR for 52164@debbugs.gnu.org; Mon, 29 Nov 2021 08:39:40 -0500 Received: from lepiller.eu (localhost [127.0.0.1]) by lepiller.eu (OpenSMTPD) with ESMTP id 37ce504a; Mon, 29 Nov 2021 13:39:36 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed; d=lepiller.eu; h=date:from :to:cc:subject:in-reply-to:references:message-id:mime-version :content-type:content-transfer-encoding; s=dkim; bh=cYTgx/It9svd g9CYMuhbKXtvZEmawTgENAOTtVWWYb0=; b=N5UTMsMGzvDRdiBxRkExWdLyDvjK gjEL1Dm/QYuuKEcZPg50rQ/OHr640HUGeMgIHejOXW7gPhcej8j+jeIyzl5d0k9m TCBUw+V4F/b+m7xhErtwX/OKg6bNzjOWiDgiv8HjNDJM8U+DNSFrtvSD9dDbKIL2 xquvApPV7IrX+BB/+MZlqwe/en1b2yDpa+ryf1oGb7+va2zW+WaeHBn4SutIX1xO Ju61NRXLH3CvyvzCBwBITGbGhY9gxVK9CYrYZ/EZn+LTrDF7QY9Lr7053B4hp/lv dwse0I6Skof0Rbi+6P0PNayk2jJHwrdIhO+pbkVHUY9cabrpTiypan49fw== Received: by lepiller.eu (OpenSMTPD) with ESMTPSA id c2415a3d (TLSv1.3:AEAD-AES256-GCM-SHA384:256:NO); Mon, 29 Nov 2021 13:39:35 +0000 (UTC) Date: Mon, 29 Nov 2021 08:39:23 -0500 From: Julien Lepiller To: zimoun Subject: Re: bug#52164: [PATCH] gnu: coq: Update to 8.14.0. User-Agent: K-9 Mail for Android In-Reply-To: References: <20211128174408.747bccba@tachikoma.lepiller.eu> <8635nfl2m6.fsf_-_@gmail.com> <592223CF-588B-44EF-A35F-9E9FDB3E4865@lepiller.eu> Message-ID: <89F34741-9EFC-4C19-8167-3B990D90533F@lepiller.eu> MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-Spam-Score: -0.0 (/) X-Debbugs-Envelope-To: 52164 Cc: 52164@debbugs.gnu.org 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 (-) > >Hum, the breakage of coq-bignums or coq-equations is recent=2E Because >using 65234d0 from Nov=2E 2nd, they are substituable; using coq@8=2E13=2E= 2=2E >Or do you mean that coq-binums@8=2E13 is broken with coq@8=2E14? I meant to say bignums 8=2E13 is broken with coq 8=2E14, and bignums 8=2E1= 4 is broken with coq 8=2E13=2E > >In all cases, it appears to me clearer to have: > > 1=2E update coq > 2=2E update coq-bignums > 3=2E update coq-equations > >i=2Ee=2E, update the "compiler" and fix then the breakage introduced by >this "compiler" upgrade, e=2Eg=2E, upgrade other packages=2E We are alwa= ys >doing like that, no? I've always updated dependents first whenever possible (without breaking a= nything), then the compiler, then the rest that needs the new compiler=2E H= owever, I've always been careful not to introduce breakage with a commit, e= ven if it's inside a series=2E I think that's the policiy, but I'm not sure= if it overrides the one-change per commit policy=2E > > >Cheers, >simon From debbugs-submit-bounces@debbugs.gnu.org Mon Nov 29 09:14:05 2021 Received: (at 52164) by debbugs.gnu.org; 29 Nov 2021 14:14:05 +0000 Received: from localhost ([127.0.0.1]:37534 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mrhPx-0003ku-5T for submit@debbugs.gnu.org; Mon, 29 Nov 2021 09:14:05 -0500 Received: from mail-il1-f179.google.com ([209.85.166.179]:33385) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1mrhPw-0003jv-3I for 52164@debbugs.gnu.org; Mon, 29 Nov 2021 09:14:04 -0500 Received: by mail-il1-f179.google.com with SMTP id i6so17581926ila.0 for <52164@debbugs.gnu.org>; Mon, 29 Nov 2021 06:14:04 -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=jHOgdM7kV4VGdRpYEV+2JmFyx2pLo8nKKHSeQu9fr38=; b=ZRP8pXZ28haBfaieY36pjOu0/cZP52zix6DMI2Q/5U+gdCgnVjBLBkRdkM9R4+0ESu b9fa7oi96FEeOZ9usDH5FT3PgWUnoTAXdz3ZJ/zmDj1GP4VPEp0sDkKEleBAMyqJhqo1 41L+hvkBzV6sMRC7NiCGqfsgj9OaJoxXCI6O2cI4Z4386E3VyaxVScEsEb8o0L/AjcMO iNFQn8NFQXuBKvTEU2hRNqGqQtrzbZ+9D9RuA2Xjt+Fp/VDC/9dX9+4NsJYe0+9Y0c9U l2pt5B087edjy0PquzYVUElI1m9R+PfRHiM+a0dV5KDuk2PVUl5DO3zI5Xnalzpq411V wb5A== 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=jHOgdM7kV4VGdRpYEV+2JmFyx2pLo8nKKHSeQu9fr38=; b=sEnTvPK5eLo/idRX+94EtBfUKu/xY8OE6nYIdx4B8Bo8ytyVOJZ9rTLhHlqkhlxutC OhAqZSF1nKP4xjffIjW6BF66KxnqxgPRdFpfIOTpCFB+vvjSlPtUX+7SxfwXlmYn02R6 Ea6ZmJnlUisyhriptKD33QBvIq551+rkor/Vxz3M8mOntZLFfIVOg0heT1YF6JsFWTy+ P1mteOohqKJX28ZbewY1/cXfEQ84ZgqS0ZHpDPQfPhy6pCGefqq16L5pGP2U+5d+60kn Fhb4j/fGV+dizBQfjIzSYlp+fjYjfHUgON1NL4DzNaZBwZc+LeVA0zJfnmgxhZ9wyECV KPlg== X-Gm-Message-State: AOAM531KAslTtGAKlI0mb0+W+Toeefpvc5VgzBzsbD4iD3VcFjD+JKMt XKzn0MlJYr/kR+jPlAS+V6nB9SYxH9j4udjNNBOMSHnO X-Google-Smtp-Source: ABdhPJwFoGSIKrBME1XgA3ZwZ8YopzcaRzQbncm4EjevUlsfkMUQam5zyqBS7+Z1P3cxdvLMYUzZkIhgWbLosWPqWJU= X-Received: by 2002:a05:6e02:1c2e:: with SMTP id m14mr57793438ilh.172.1638195238654; Mon, 29 Nov 2021 06:13:58 -0800 (PST) MIME-Version: 1.0 References: <20211128174408.747bccba@tachikoma.lepiller.eu> <8635nfl2m6.fsf_-_@gmail.com> <592223CF-588B-44EF-A35F-9E9FDB3E4865@lepiller.eu> <89F34741-9EFC-4C19-8167-3B990D90533F@lepiller.eu> In-Reply-To: <89F34741-9EFC-4C19-8167-3B990D90533F@lepiller.eu> From: zimoun Date: Mon, 29 Nov 2021 15:13:47 +0100 Message-ID: Subject: Re: bug#52164: [PATCH] gnu: coq: Update to 8.14.0. To: Julien Lepiller Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 52164 Cc: 52164@debbugs.gnu.org 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 (-) Re, On Mon, 29 Nov 2021 at 14:39, Julien Lepiller wrote: > I've always updated dependents first whenever possible (without breaking = anything), then the compiler, then the rest that needs the new compiler. Ho= wever, I've always been careful not to introduce breakage with a commit, ev= en if it's inside a series. I think that's the policiy, but I'm not sure if= it overrides the one-change per commit policy. Me neither. :-) Anyway, all LGTM except wrong commit message for coq-semantics. Cheers, simon From debbugs-submit-bounces@debbugs.gnu.org Tue May 03 08:37:40 2022 Received: (at 52164-done) by debbugs.gnu.org; 3 May 2022 12:37:41 +0000 Received: from localhost ([127.0.0.1]:38924 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1nlrme-0006oL-O0 for submit@debbugs.gnu.org; Tue, 03 May 2022 08:37:40 -0400 Received: from mail-wr1-f51.google.com ([209.85.221.51]:39571) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1nlrma-0006o5-8g for 52164-done@debbugs.gnu.org; Tue, 03 May 2022 08:37:39 -0400 Received: by mail-wr1-f51.google.com with SMTP id d5so23177121wrb.6 for <52164-done@debbugs.gnu.org>; Tue, 03 May 2022 05:37:36 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=from:to:cc:subject:references:date:in-reply-to:message-id :user-agent:mime-version; bh=9Y75YwbvXHB5ZKbjmvS45BHeg4iLEBRP2ChNuW252LA=; b=ZZuIctdW6K5FHV0W9PyUfm9XPIYGHImkKwGT47sCX1xyQQ2azfDol7JGazn8kotENQ WfPfzOJbI33uv/PZcoLbtHT+p5Ug4V/85H71kjnxPvtvcebLwz0tos9PfYNKZiesEk2B COAcOxWF7IKXgTAWFCLFURfVfMWL6S7b8LpzYp0neq5mNhgnO2jrbm5hkxVjeIHvVWKZ x0WlYYal3+Bhd6cgxSDk2VzXNa2nrlQRCR3fMRNr0wCd+y9FfcupV/gt4gIC9A1Z765E LWyJKkbxxA7QBYtTRBzBeUGds1O5ntA9tTO6tg6GphhqwZM2u0sFJfSBOODDKIYUMBNX zEFQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:from:to:cc:subject:references:date:in-reply-to :message-id:user-agent:mime-version; bh=9Y75YwbvXHB5ZKbjmvS45BHeg4iLEBRP2ChNuW252LA=; b=aCM1D+DKd9q5qw6XpgBHrw80S2pNgwYdT/FSAJdbpkfAJ3LLmagf4cCiCurDPCVGEr tcj38gfrHmPQluXI2th9WGtDYiv46EUxTSf1aOcZRLJOIPuUZH95bvdc45pEE18kwFPd WEOusDsbDUdRwp2taVnd5CFF5xZipyY+GG8bMKUJs0/rpAKx6MSFwnVjduXlB38PoJoI wjzvGN4S/v74PUezuZLJNobWO4BaShaoOzw+SS932Jy8Q0aTDcTib9TEub/bN/GVmmXp 6e+sqByMN5Qo/tAxWOc9nindgdzfRdTXaLLwBvz1bVGFuMpVfu7VmJzuC4QBsH9W8bHZ IFIA== X-Gm-Message-State: AOAM530zbX3GvsKIX8KDN/BQyoMvFm914s9Z9ZWAFrYKIcK1car7+b/0 Y3ZQfMkmOqjC5favwLgiK5dAWI7SERg= X-Google-Smtp-Source: ABdhPJyypnssXjONfkJEmBixUbaYqeo21SuXWiz8KZFCLgAkoqLNvjT3hbCLr/pQ52kpvCUrC67kdQ== X-Received: by 2002:a05:6000:15c1:b0:20c:5825:f043 with SMTP id y1-20020a05600015c100b0020c5825f043mr11002622wry.261.1651581450194; Tue, 03 May 2022 05:37:30 -0700 (PDT) Received: from lili ([2a01:e0a:59b:9120:65d2:2476:f637:db1e]) by smtp.gmail.com with ESMTPSA id i14-20020a7bc94e000000b003942a244edcsm1564448wml.33.2022.05.03.05.37.29 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 03 May 2022 05:37:29 -0700 (PDT) From: zimoun To: Julien Lepiller Subject: Re: bug#52164: [PATCH] gnu: coq: Update to 8.14.0. References: <20211128174408.747bccba@tachikoma.lepiller.eu> Date: Tue, 03 May 2022 14:35:33 +0200 In-Reply-To: <20211128174408.747bccba@tachikoma.lepiller.eu> (Julien Lepiller's message of "Sun, 28 Nov 2021 17:44:26 +0100") Message-ID: <864k26iyju.fsf@gmail.com> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/27.2 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain X-Spam-Score: -0.0 (/) X-Debbugs-Envelope-To: 52164-done Cc: 52164-done@debbugs.gnu.org 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 (-) Hi Julien, On Sun, 28 Nov 2021 at 17:44, Julien Lepiller wrote: > this small series updates coq to its latest version. This series [1] updated Coq at 8.14 and the current Coq is 8.15. 1: So closing! Cheers, simon From unknown Tue Aug 19 02:53:08 2025 Received: (at fakecontrol) by fakecontrolmessage; To: internal_control@debbugs.gnu.org From: Debbugs Internal Request Subject: Internal Control Message-Id: bug archived. Date: Wed, 01 Jun 2022 11:24:06 +0000 User-Agent: Fakemail v42.6.9 # This is a fake control message. # # The action: # bug archived. thanks # This fakemail brought to you by your local debbugs # administrator