From unknown Wed Jun 18 00:20:06 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#49423 <49423@debbugs.gnu.org> To: bug#49423 <49423@debbugs.gnu.org> Subject: Status: [PATCH] gnu: coq: Update to 8.13.2. Reply-To: bug#49423 <49423@debbugs.gnu.org> Date: Wed, 18 Jun 2025 07:20:06 +0000 retitle 49423 [PATCH] gnu: coq: Update to 8.13.2. reassign 49423 guix-patches submitter 49423 Julien Lepiller severity 49423 normal tag 49423 patch thanks From debbugs-submit-bounces@debbugs.gnu.org Mon Jul 05 18:07:05 2021 Received: (at submit) by debbugs.gnu.org; 5 Jul 2021 22:07:05 +0000 Received: from localhost ([127.0.0.1]:46787 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1m0Wjy-0001lq-02 for submit@debbugs.gnu.org; Mon, 05 Jul 2021 18:07:05 -0400 Received: from lists.gnu.org ([209.51.188.17]:54844) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1m0Wjv-0001lh-Ir for submit@debbugs.gnu.org; Mon, 05 Jul 2021 18:06:56 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:53622) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1m0Wjv-0006v1-Cd for guix-patches@gnu.org; Mon, 05 Jul 2021 18:06:55 -0400 Received: from lepiller.eu ([2a00:5884:8208::1]:38686) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1m0Wjr-0000Kn-5e for guix-patches@gnu.org; Mon, 05 Jul 2021 18:06:54 -0400 Received: from lepiller.eu (localhost [127.0.0.1]) by lepiller.eu (OpenSMTPD) with ESMTP id 4c909d06 for ; Mon, 5 Jul 2021 22:06:44 +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; s=dkim; bh=fhE 10fzac3PVbJUvfvMdyN9ksEFV0sY7pk5rSvn2Ij4=; b=MS8B8Hzo+y5W6rdmmdM Av+oLAy6Uri5mXIAjAFdCaoEZb9zxXgvL2JmkpGku+/vYXwJT3XL2Q4Tny2Vw40u zj290+fn1l+MyQiDBZNgN8JQ4obwQdjLvWRL3wmqkUBG0wE79qihC5ZBuLisWBUz DAC0XWP+a3XDQGXQuLF62eGXqfNszVzi6HB9zIOIaP+3bUUJT9Rl5KTuhmRl34t5 5503xIoL5vKj6/9nQHw/aACeWYpwfPS/tfga0ciLtHIyMMDQFnFL1ox8tTjAI3Wg /fEagYh3EyPeY+sMDeD+mjlvw0Mvcl3X/Z5AdbEptpy+XJ4Gi/ZKBc9ly3XReo/l eCQ== Received: by lepiller.eu (OpenSMTPD) with ESMTPSA id cbac0aa7 (TLSv1.2:ECDHE-RSA-AES256-GCM-SHA384:256:NO) for ; Mon, 5 Jul 2021 22:06:44 +0000 (UTC) Date: Tue, 6 Jul 2021 00:06:40 +0200 From: Julien Lepiller To: guix-patches@gnu.org Subject: [PATCH] gnu: coq: Update to 8.13.2. Message-ID: <20210706000640.4630e3bb@tachikoma.lepiller.eu> X-Mailer: Claws Mail 3.17.8 (GTK+ 2.24.32; x86_64-pc-linux-gnu) MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="MP_/jGUdlqUdtTBeoke1qO/tY2U" Received-SPF: pass client-ip=2a00:5884:8208::1; 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: -0.0 (/) --MP_/jGUdlqUdtTBeoke1qO/tY2U Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Content-Disposition: inline Hi guix! this small series updates coq to the latest version. I had to update zarith and a few dependencies (some of which cannot be updated independently of coq), and fix the installation of lablgtk. This version of coq uses dune, and I split the coq package into coq, coq-ide-server (contains coqidetop) and coq-ide (contains the graphical interface). This also simplifies the dependency graph for coq packages, as they no longer need the graphical stack. I tried building the documentation too, but it complains about missing coq package, even if I added it to the inputs of coq-doc, so it's not part of this series. --MP_/jGUdlqUdtTBeoke1qO/tY2U Content-Type: text/x-patch Content-Transfer-Encoding: 7bit Content-Disposition: attachment; filename=0001-gnu-ocaml-zarith-Update-to-1.12.patch >From 73fc06926c86e8dad8bbb61f6a1728343fd2a487 Mon Sep 17 00:00:00 2001 From: Julien Lepiller Date: Mon, 5 Jul 2021 17:31:10 +0200 Subject: [PATCH 1/4] gnu: ocaml-zarith: Update to 1.12. * gnu/packages/ocaml.scm (ocaml-zarith): Update to 1.12. --- gnu/packages/ocaml.scm | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm index cec6eb4f89..5f4ed3ae35 100644 --- a/gnu/packages/ocaml.scm +++ b/gnu/packages/ocaml.scm @@ -1428,7 +1428,7 @@ files in these formats.") (define-public ocaml-zarith (package (name "ocaml-zarith") - (version "1.9.1") + (version "1.12") (source (origin (method git-fetch) (uri (git-reference @@ -1437,7 +1437,7 @@ files in these formats.") (file-name (git-file-name name version)) (sha256 (base32 - "0hv5ywz1q2cgn8apfz490clwk5hcynr937g2v8i13x2ax4bnv0lz")))) + "1jslm1rv1j0ya818yh23wf3bb6hz7qqj9pn5fwl45y9mqyqa01s9")))) (build-system ocaml-build-system) (native-inputs `(("perl" ,perl))) @@ -1448,7 +1448,14 @@ files in these formats.") #:phases (modify-phases %standard-phases (replace 'configure - (lambda _ (invoke "./configure")))))) + (lambda _ (invoke "./configure"))) + (add-after 'install 'move-sublibs + (lambda* (#:key outputs #:allow-other-keys) + (let* ((out (assoc-ref outputs "out")) + (lib (string-append out "/lib/ocaml/site-lib"))) + (mkdir-p (string-append lib "/stublibs")) + (rename-file (string-append lib "/zarith/dllzarith.so") + (string-append lib "/stublibs/dllzarith.so")))))))) (home-page "https://forge.ocamlcore.org/projects/zarith/") (synopsis "Implements arbitrary-precision integers") (description "Implements arithmetic and logical operations over -- 2.32.0 --MP_/jGUdlqUdtTBeoke1qO/tY2U Content-Type: text/x-patch Content-Transfer-Encoding: 7bit Content-Disposition: attachment; filename=0002-gnu-lablgtk3-Install-with-version-information.patch >From 76a337769e67e84a32c5b85d80ab6bc160792aef Mon Sep 17 00:00:00 2001 From: Julien Lepiller Date: Mon, 5 Jul 2021 17:52:03 +0200 Subject: [PATCH 2/4] gnu: lablgtk3: Install with version information. This is required so recent versions of coq can check version requirements. * gnu/packages/ocaml.scm (lablgtk3)[arguments]: Ensure version is added to the META file. --- gnu/packages/ocaml.scm | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm index 5f4ed3ae35..4c8f04f29c 100644 --- a/gnu/packages/ocaml.scm +++ b/gnu/packages/ocaml.scm @@ -6902,6 +6902,12 @@ support for Mparser."))) (for-each (lambda (file) (chmod file #o644)) (find-files "." ".")) + #t)) + (add-before 'build 'set-version + (lambda _ + (substitute* "dune-project" + (("\\(name lablgtk3\\)") + (string-append "(name lablgtk3)\n(version " ,version ")"))) #t))))) (propagated-inputs `(("ocaml-cairo2" ,ocaml-cairo2))) -- 2.32.0 --MP_/jGUdlqUdtTBeoke1qO/tY2U Content-Type: text/x-patch Content-Transfer-Encoding: 7bit Content-Disposition: attachment; filename=0003-gnu-coq-stdpp-Update-to-1.5.0.patch >From 8f374c9e8001db83a12ef6feee8404cbef4daaab Mon Sep 17 00:00:00 2001 From: Julien Lepiller Date: Mon, 5 Jul 2021 23:41:16 +0200 Subject: [PATCH 3/4] gnu: coq-stdpp: Update to 1.5.0. * gnu/packages/coq.scm (coq-stdpp): Update to 1.5.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 fa1f4078b8..a18eddeb0f 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -598,7 +598,7 @@ kernel.") (define-public coq-stdpp (package (name "coq-stdpp") - (version "1.4.0") + (version "1.5.0") (synopsis "Alternative Coq standard library std++") (source (origin (method git-fetch) @@ -608,7 +608,7 @@ kernel.") (file-name (git-file-name name version)) (sha256 (base32 - "1m6c7ibwc99jd4cv14v3r327spnfvdf3x2mnq51f9rz99rffk68r")))) + "1ym0fy620imah89p8b6rii8clx2vmnwcrbwxl3630h24k42092nf")))) (build-system gnu-build-system) (inputs `(("coq" ,coq))) -- 2.32.0 --MP_/jGUdlqUdtTBeoke1qO/tY2U Content-Type: text/x-patch Content-Transfer-Encoding: quoted-printable Content-Disposition: attachment; filename=0004-gnu-coq-Update-to-8.13.2.patch =46rom 074a392bc2139309a39a06b03520af0573c844b1 Mon Sep 17 00:00:00 2001 From: Julien Lepiller Date: Mon, 5 Jul 2021 21:32:33 +0200 Subject: [PATCH 4/4] gnu: coq: Update to 8.13.2. * gnu/packages/coq.scm (coq): Update to 8.13.2. (coq-ide-server, coq-ide): New packages. (coq-gappa): Update to 1.4.6. (coq-bignums): Update to 8.13.0. (coq-interval): Update to 1.3.0. (coq-equations): Update to 1.2.4. --- gnu/packages/coq.scm | 147 ++++++++++++++++++------------------------- 1 file changed, 62 insertions(+), 85 deletions(-) diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index a18eddeb0f..4ad172c6b0 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -1,5 +1,5 @@ ;;; GNU Guix --- Functional package management for GNU -;;; Copyright =C2=A9 2018 Julien Lepiller +;;; Copyright =C2=A9 2018-2021 Julien Lepiller ;;; Copyright =C2=A9 2018, 2019 Tobias Geerinckx-Rice ;;; Copyright =C2=A9 2019 Dan Frumin ;;; Copyright =C2=A9 2020 Brett Gilio @@ -38,6 +38,7 @@ #:use-module (gnu packages python) #:use-module (gnu packages rsync) #:use-module (gnu packages texinfo) + #:use-module (guix build-system dune) #:use-module (guix build-system gnu) #:use-module (guix build-system ocaml) #:use-module (guix download) @@ -50,7 +51,7 @@ (define-public coq (package (name "coq") - (version "8.11.2") + (version "8.13.2") (source (origin (method git-fetch) @@ -60,78 +61,24 @@ (file-name (git-file-name name version)) (sha256 (base32 - "1gia82dkmzqspw2w3s4gjyh39ghbmw4i41i4hyzc91g7mza17nbz")))) + "15r0cm3p9dlsxbg0lf05njjp1xi1y74vxvq6drxjykax67x95l8a")))) (native-search-paths (list (search-path-specification (variable "COQPATH") - (files (list "lib/coq/user-contrib"))))) - (build-system ocaml-build-system) - (outputs '("out" "ide")) + (files (list "lib/coq/user-contrib"))) + (search-path-specification + (variable "COQLIB") + (files (list "lib/ocaml/site-lib/coq")) + (separator #f)))) + (build-system dune-build-system) (inputs - `(("lablgtk" ,lablgtk3) - ("python" ,python-2) - ("camlp5" ,camlp5) - ("ocaml-num" ,ocaml-num))) + `(("gmp" ,gmp) + ("ocaml-zarith" ,ocaml-zarith))) (native-inputs - `(("ocaml-ounit" ,ocaml-ounit) - ("rsync" ,rsync) - ("which" ,which))) + `(("which" ,which))) (arguments - `(#:phases - (modify-phases %standard-phases - (add-after 'unpack 'make-git-checkout-writable - (lambda _ - (for-each make-file-writable (find-files ".")) - #t)) - (replace 'configure - (lambda* (#:key outputs #:allow-other-keys) - (let* ((out (assoc-ref outputs "out")) - (mandir (string-append out "/share/man")) - (browser "icecat -remote \"OpenURL(%s,new-tab)\"")) - (invoke "./configure" - "-prefix" out - "-mandir" mandir - "-browser" browser - "-coqide" "opt")))) - (replace 'build - (lambda _ - (invoke "make" - "-j" (number->string (parallel-job-count)) - "world"))) - (delete 'check) - (add-after 'install 'remove-duplicate - (lambda* (#:key outputs #:allow-other-keys) - (let* ((out (assoc-ref outputs "out")) - (bin (string-append out "/bin")) - (coqtop (string-append bin "/coqtop")) - (coqidetop (string-append bin "/coqidetop")) - (coqtop.opt (string-append coqtop ".opt")) - (coqidetop.opt (string-append coqidetop ".opt"))) - ;; These files are exact copies without `.opt` extension. - ;; Removing these saves 35 MiB in the resulting package. - ;; Unfortunately, completely deleting them breaks coqide. - (delete-file coqtop.opt) - (delete-file coqidetop.opt) - (symlink coqtop coqtop.opt) - (symlink coqidetop coqidetop.opt)) - #t)) - (add-after 'install 'install-ide - (lambda* (#:key outputs #:allow-other-keys) - (let ((out (assoc-ref outputs "out")) - (ide (assoc-ref outputs "ide"))) - (mkdir-p (string-append ide "/bin")) - (rename-file (string-append out "/bin/coqide") - (string-append ide "/bin/coqide"))) - #t)) - (add-after 'install 'check - (lambda _ - (with-directory-excursion "test-suite" - ;; These two tests fail. - ;; Fails because the output is not formatted as expected. - (delete-file-recursively "coq-makefile/timing") - ;; Fails because we didn't build coqtop.byte. - (delete-file "misc/printers.sh") - (invoke "make"))))))) + `(#:package "coq" + #:test-target "test-suite")) (home-page "https://coq.inria.fr") (synopsis "Proof assistant for higher-order logic") (description @@ -142,6 +89,31 @@ It is developed using Objective Caml and Camlp5.") ;; Some of the documentation is distributed under opl1.0+. (license (list license:lgpl2.1 license:opl1.0+)))) =20 +(define-public coq-ide-server + (package + (inherit coq) + (name "coq-ide-server") + (arguments + `(#:tests? #f + #:package "coqide-server")) + (inputs + `(("coq" ,coq) + ("gmp" ,gmp) + ("ocaml-zarith" ,ocaml-zarith))))) + +(define-public coq-ide + (package + (inherit coq) + (name "coq-ide") + (arguments + `(#:tests? #f + #:package "coqide")) + (propagated-inputs + `(("coq" ,coq) + ("coq-ide-server" ,coq-ide-server))) + (inputs + `(("lablgtk3" ,lablgtk3))))) + (define-public proof-general ;; The latest release is from 2016 and there has been more than 450 comm= its ;; since then. @@ -274,7 +246,7 @@ inside Coq.") (define-public coq-gappa (package (name "coq-gappa") - (version "1.4.4") + (version "1.4.6") (source (origin (method git-fetch) @@ -284,7 +256,7 @@ inside Coq.") (file-name (git-file-name name version)) (sha256 (base32 - "0f3g3wjkvfkm961l4jpckhsqd43jnvm7f5qqk78qc32zh1fg339n")))) + "0492i0ksrz6dnc1d57jzsbmdlb9fp9hrh9ib5v8j0yqxpyi0x8f4")))) (build-system gnu-build-system) (native-inputs `(("autoconf" ,autoconf) @@ -298,13 +270,14 @@ inside Coq.") (inputs `(("gmp" ,gmp) ("mpfr" ,mpfr) + ("ocaml-zarith" ,ocaml-zarith) ("boost" ,boost))) (propagated-inputs `(("coq-flocq" ,coq-flocq))) (arguments `(#:configure-flags - (list (string-append "--libdir=3D" (assoc-ref %outputs "out") - "/lib/coq/user-contrib/Gappa")) + (list (string-append "COQUSERCONTRIB=3D" (assoc-ref %outputs "out") + "/lib/coq/user-contrib")) #:phases (modify-phases %standard-phases (add-before 'configure 'fix-remake @@ -334,7 +307,7 @@ assistant.") (define-public coq-mathcomp (package (name "coq-mathcomp") - (version "1.11.0") + (version "1.12.0") (source (origin (method git-fetch) @@ -343,7 +316,7 @@ assistant.") (commit (string-append "mathcomp-" version)))) (file-name (git-file-name name version)) (sha256 - (base32 "1axywpa1jcpnidd86irpd1gdbbg2sfbwc652675xisq5wnmfmf6f")))) + (base32 "12cgrmzlcjnp9kv9zxsk34fgf0qfa35jdb23cbf13kmg8dyfi3h5")))) (build-system gnu-build-system) (native-inputs `(("ocaml" ,ocaml) @@ -429,7 +402,7 @@ theorems between the two libraries.") (define-public coq-bignums (package (name "coq-bignums") - (version "8.11.0") + (version "8.13.0") (source (origin (method git-fetch) (uri (git-reference @@ -438,13 +411,14 @@ theorems between the two libraries.") (file-name (git-file-name name version)) (sha256 (base32 - "1xcd7c7qlvs0narfba6px34zq0mz8rffnhxw0kzhhg6i4iw115dp")))) + "1n66i7hd9222b2ks606mak7m4f0dgy02xgygjskmmav6h7g2sx7y")))) (build-system gnu-build-system) (native-inputs `(("ocaml" ,ocaml) ("coq" ,coq))) (inputs - `(("camlp5" ,camlp5))) + `(("camlp5" ,camlp5) + ("ocaml-zarith" ,ocaml-zarith))) (arguments `(#:tests? #f ; No test target. #:make-flags @@ -462,7 +436,7 @@ provides BigN, BigZ, BigQ that used to be part of Coq s= tandard library.") (define-public coq-interval (package (name "coq-interval") - (version "4.0.0") + (version "4.3.0") (source (origin (method git-fetch) @@ -472,7 +446,7 @@ provides BigN, BigZ, BigQ that used to be part of Coq s= tandard library.") (file-name (git-file-name name version)) (sha256 (base32 - "01iz6qmnsm6b9s1vmdjs79vjx9xgwzn5rwyjp6bvs8hg3zlmhpip")))) + "1jqvd17czhliscf40idhnxgrha620039ilrdyfahn71dg2jmzqnm")))) (build-system gnu-build-system) (native-inputs `(("autoconf" ,autoconf) @@ -484,11 +458,12 @@ provides BigN, BigZ, BigQ that used to be part of Coq= standard library.") `(("flocq" ,coq-flocq) ("bignums" ,coq-bignums) ("coquelicot" ,coq-coquelicot) - ("mathcomp" ,coq-mathcomp))) + ("mathcomp" ,coq-mathcomp) + ("ocaml-zarith" ,ocaml-zarith))) (arguments `(#:configure-flags - (list (string-append "--libdir=3D" (assoc-ref %outputs "out") - "/lib/coq/user-contrib/Gappa")) + (list (string-append "COQUSERCONTRIB=3D" (assoc-ref %outputs "out") + "/lib/coq/user-contrib")) #:phases (modify-phases %standard-phases (add-before 'configure 'fix-remake @@ -558,21 +533,23 @@ uses Ltac to synthesize the substitution operation.") (define-public coq-equations (package (name "coq-equations") - (version "1.2.3") + (version "1.2.4") (source (origin (method git-fetch) (uri (git-reference (url "https://github.com/mattam82/Coq-Equations") - (commit (string-append "v" version "-8.11")))) + (commit (string-append "v" version "-8.13")))) (file-name (git-file-name name version)) (sha256 (base32 - "1srxz1rws8jsh7402g2x2vcqgjbbsr64dxxj5d2zs48pmhb20csf")))) + "0i014lshsdflzw6h0qxra9d2f0q82vffxv2f29awbb9ad0p4rq4q")))) (build-system gnu-build-system) (native-inputs `(("ocaml" ,ocaml) ("coq" ,coq) ("camlp5" ,camlp5))) + (inputs + `(("ocaml-zarith" ,ocaml-zarith))) (arguments `(#:test-target "test-suite" #:phases --=20 2.32.0 --MP_/jGUdlqUdtTBeoke1qO/tY2U-- From debbugs-submit-bounces@debbugs.gnu.org Wed Jul 21 10:08:02 2021 Received: (at 49423) by debbugs.gnu.org; 21 Jul 2021 14:08:03 +0000 Received: from localhost ([127.0.0.1]:38166 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1m6CtG-00020Q-Ng for submit@debbugs.gnu.org; Wed, 21 Jul 2021 10:08:02 -0400 Received: from eggs.gnu.org ([209.51.188.92]:45268) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1m6CtF-0001zd-4U for 49423@debbugs.gnu.org; Wed, 21 Jul 2021 10:08:01 -0400 Received: from fencepost.gnu.org ([2001:470:142:3::e]:48834) by eggs.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1m6Ct9-0000vH-1w; Wed, 21 Jul 2021 10:07:55 -0400 Received: from [2a01:e0a:1d:7270:af76:b9b:ca24:c465] (port=45264 helo=ribbon) by fencepost.gnu.org with esmtpsa (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1m6Ct8-0000i0-Qh; Wed, 21 Jul 2021 10:07:55 -0400 From: =?utf-8?Q?Ludovic_Court=C3=A8s?= To: Julien Lepiller Subject: Re: bug#49423: [PATCH] gnu: coq: Update to 8.13.2. References: <20210706000640.4630e3bb@tachikoma.lepiller.eu> Date: Wed, 21 Jul 2021 16:07:53 +0200 In-Reply-To: <20210706000640.4630e3bb@tachikoma.lepiller.eu> (Julien Lepiller's message of "Tue, 6 Jul 2021 00:06:40 +0200") Message-ID: <87lf5zhi9y.fsf@gnu.org> 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: -2.3 (--) X-Debbugs-Envelope-To: 49423 Cc: 49423@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: -3.3 (---) Hi, Julien Lepiller skribis: > this small series updates coq to the latest version. I had to update > zarith and a few dependencies (some of which cannot be updated > independently of coq), and fix the installation of lablgtk. I haven=E2=80=99t tested it but the whole series LGTM! Thanks, Ludo=E2=80=99. From debbugs-submit-bounces@debbugs.gnu.org Sat Jul 24 09:17:41 2021 Received: (at 49423) by debbugs.gnu.org; 24 Jul 2021 13:17:41 +0000 Received: from localhost ([127.0.0.1]:45384 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1m7HXB-0007JS-3K for submit@debbugs.gnu.org; Sat, 24 Jul 2021 09:17:41 -0400 Received: from h87-96-130-155.cust.a3fiber.se ([87.96.130.155]:34060 helo=mail.yoctocell.xyz) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1m7HX6-0007JB-8c for 49423@debbugs.gnu.org; Sat, 24 Jul 2021 09:17:39 -0400 From: Xinglu Chen DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=yoctocell.xyz; s=mail; t=1627132646; bh=5g8Meysniokgr+/0y8Jhxz0NLb+Jn0DMdBmKJoByPQk=; h=From:To:Subject:In-Reply-To:References:Date; b=mxRwtm9THN52KFHx9sjriILhMbOelWWyjylnrrJSSzF5SAPtvUGx2tHdldWy9vqDw NcwQafCIEgVQh6EzNITS45yOXBLDvS3WlXELn65mwFN/2AW0QpvKqX/hXulVbliDEb RA2RSsKRMNpaiR8amatvHq0mXUoR+BLTy537I3Fk= To: Julien Lepiller , 49423@debbugs.gnu.org Subject: Re: [bug#49423] [PATCH] gnu: coq: Update to 8.13.2. In-Reply-To: <20210706000640.4630e3bb@tachikoma.lepiller.eu> References: <20210706000640.4630e3bb@tachikoma.lepiller.eu> Date: Sat, 24 Jul 2021 15:17:25 +0200 Message-ID: <87lf5v3l7e.fsf@yoctocell.xyz> MIME-Version: 1.0 Content-Type: multipart/signed; boundary="=-=-="; micalg=pgp-sha256; protocol="application/pgp-signature" X-Spam-Score: 2.9 (++) X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org", has NOT identified this incoming email as spam. The original message has been attached to this so you can view it or label similar future email. If you have any questions, see the administrator of that system for details. Content preview: On Tue, Jul 06 2021, Julien Lepiller wrote: > Hi guix! > > this small series updates coq to the latest version. I had to update > zarith and a few dependencies (some of which cannot be updated > independently of coq), and fix the installation o [...] Content analysis details: (2.9 points, 10.0 required) pts rule name description ---- ---------------------- -------------------------------------------------- -0.0 SPF_PASS SPF: sender matches SPF record 2.0 PDS_OTHER_BAD_TLD Untrustworthy TLDs [URI: yoctocell.xyz (xyz)] 0.0 SPF_HELO_NONE SPF: HELO does not publish an SPF Record 0.5 FROM_SUSPICIOUS_NTLD From abused NTLD 0.4 RDNS_DYNAMIC Delivered to internal network by host with dynamic-looking rDNS 0.0 PDS_RDNS_DYNAMIC_FP RDNS_DYNAMIC with FP steps X-Debbugs-Envelope-To: 49423 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.9 (++) X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org", has NOT identified this incoming email as spam. The original message has been attached to this so you can view it or label similar future email. If you have any questions, see the administrator of that system for details. Content preview: On Tue, Jul 06 2021, Julien Lepiller wrote: > Hi guix! > > this small series updates coq to the latest version. I had to update > zarith and a few dependencies (some of which cannot be updated > independently of coq), and fix the installation o [...] Content analysis details: (2.9 points, 10.0 required) pts rule name description ---- ---------------------- -------------------------------------------------- -0.0 SPF_PASS SPF: sender matches SPF record 2.0 PDS_OTHER_BAD_TLD Untrustworthy TLDs [URI: yoctocell.xyz (xyz)] 0.0 SPF_HELO_NONE SPF: HELO does not publish an SPF Record 0.5 FROM_SUSPICIOUS_NTLD From abused NTLD 0.4 RDNS_DYNAMIC Delivered to internal network by host with dynamic-looking rDNS 1.0 BULK_RE_SUSP_NTLD Precedence bulk and RE: from a suspicious TLD -1.0 MAILING_LIST_MULTI Multiple indicators imply a widely-seen list manager 0.0 PDS_RDNS_DYNAMIC_FP RDNS_DYNAMIC with FP steps --=-=-= Content-Type: text/plain Content-Transfer-Encoding: quoted-printable On Tue, Jul 06 2021, Julien Lepiller wrote: > Hi guix! > > this small series updates coq to the latest version. I had to update > zarith and a few dependencies (some of which cannot be updated > independently of coq), and fix the installation of lablgtk. > > This version of coq uses dune, and I split the coq package into coq, > coq-ide-server (contains coqidetop) and coq-ide (contains the graphical > interface). This also simplifies the dependency graph for coq packages, > as they no longer need the graphical stack. > > I tried building the documentation too, but it complains about missing > coq package, even if I added it to the inputs of coq-doc, so it's not > part of this series. > From 73fc06926c86e8dad8bbb61f6a1728343fd2a487 Mon Sep 17 00:00:00 2001 > From: Julien Lepiller > Date: Mon, 5 Jul 2021 17:31:10 +0200 > Subject: [PATCH 1/4] gnu: ocaml-zarith: Update to 1.12. > > * gnu/packages/ocaml.scm (ocaml-zarith): Update to 1.12. > --- > gnu/packages/ocaml.scm | 13 ++++++++++--- > 1 file changed, 10 insertions(+), 3 deletions(-) > > diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm > index cec6eb4f89..5f4ed3ae35 100644 > --- a/gnu/packages/ocaml.scm > +++ b/gnu/packages/ocaml.scm > @@ -1428,7 +1428,7 @@ files in these formats.") > (define-public ocaml-zarith > (package > (name "ocaml-zarith") > - (version "1.9.1") > + (version "1.12") > (source (origin > (method git-fetch) > (uri (git-reference > @@ -1437,7 +1437,7 @@ files in these formats.") > (file-name (git-file-name name version)) > (sha256 > (base32 > - "0hv5ywz1q2cgn8apfz490clwk5hcynr937g2v8i13x2ax4bnv0lz"))= )) > + "1jslm1rv1j0ya818yh23wf3bb6hz7qqj9pn5fwl45y9mqyqa01s9"))= )) > (build-system ocaml-build-system) > (native-inputs > `(("perl" ,perl))) > @@ -1448,7 +1448,14 @@ files in these formats.") > #:phases > (modify-phases %standard-phases > (replace 'configure > - (lambda _ (invoke "./configure")))))) > + (lambda _ (invoke "./configure"))) > + (add-after 'install 'move-sublibs > + (lambda* (#:key outputs #:allow-other-keys) > + (let* ((out (assoc-ref outputs "out")) > + (lib (string-append out "/lib/ocaml/site-lib"))) > + (mkdir-p (string-append lib "/stublibs")) > + (rename-file (string-append lib "/zarith/dllzarith.so") > + (string-append lib "/stublibs/dllzarith.so")= ))))))) > (home-page "https://forge.ocamlcore.org/projects/zarith/") > (synopsis "Implements arbitrary-precision integers") > (description "Implements arithmetic and logical operations over > --=20 > 2.32.0 > > From 76a337769e67e84a32c5b85d80ab6bc160792aef Mon Sep 17 00:00:00 2001 > From: Julien Lepiller > Date: Mon, 5 Jul 2021 17:52:03 +0200 > Subject: [PATCH 2/4] gnu: lablgtk3: Install with version information. > > This is required so recent versions of coq can check version > requirements. > > * gnu/packages/ocaml.scm (lablgtk3)[arguments]: Ensure version is added > to the META file. > --- > gnu/packages/ocaml.scm | 6 ++++++ > 1 file changed, 6 insertions(+) > > diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm > index 5f4ed3ae35..4c8f04f29c 100644 > --- a/gnu/packages/ocaml.scm > +++ b/gnu/packages/ocaml.scm > @@ -6902,6 +6902,12 @@ support for Mparser."))) > (for-each (lambda (file) > (chmod file #o644)) > (find-files "." ".")) > + #t)) Nit: no need to add a trailing #t. > + (add-before 'build 'set-version > + (lambda _ > + (substitute* "dune-project" > + (("\\(name lablgtk3\\)") > + (string-append "(name lablgtk3)\n(version " ,version ")"= ))) > #t))))) Likewise. Otherwise, looks good; everything builds fine. :) --=-=-= Content-Type: application/pgp-signature; name="signature.asc" -----BEGIN PGP SIGNATURE----- iQJJBAEBCAAzFiEEAVhh4yyK5+SEykIzrPUJmaL7XHkFAmD8EuUVHHB1YmxpY0B5 b2N0b2NlbGwueHl6AAoJEKz1CZmi+1x5eQoP/3iNFFmYkKxO0IlSYjzgElx/AhTl yXteOJSI6aV3YTJ8FbjwnYBEtYyEQ3CPCf3kGFpg0B3iXGheqkgtAy3SmnEPQygw dM5qu5HU/IAcK/hwWSvji04STwCtpRBj1Dhe06LM+5Mb3kQScHAIGkrfANRlG9qe QbCI7t87jVQaKCFJrInB04StAErEYMy4tTFI4xT33IOoWCx5b5n45LX72g5kmSRo xewKamw0cUkWJry4fKDs9Out1OzoCekqISkusELm5tqdBNgeUNFcduRgVas3pyaS 6B5HFbqE+6RIcEJVXG8qzi142wQH3bf+N/dawPXxPL1qSBwhLlp4FNR9+5Wx2Ad/ mH9HDohYiHh15wOjkKjwP+ZJCV3EdfK6DflsFToFJQQSNjQ1BzRdkLg9rMIWwvaR QkBSiG/o1XRWmcDtYHHvxncNz2S1TUfGrlR95BhesVDMxVy0I7wFY0zanrKvBue2 U7+lMVQP+/nZFF9AgrfB9lflx4EagTfT8yC+14Nj9s2IglqQIQCjAeiJ1l6mGVaZ fxzYjy15+LsRcAOLFlTA98CZpiAcvE20vFIRdmNDlOsigdvcbGSL6M3qBDrYeQkI X5m1BSJP1OtirhEzVBT8LZGdqw+NcfFZnOVB2ZRLp7EsvqQA9FTw7pOIklxSOQ1v CgZs7dAHUtYmJxkK =0CHK -----END PGP SIGNATURE----- --=-=-=-- From debbugs-submit-bounces@debbugs.gnu.org Sat Jul 31 17:07:43 2021 Received: (at 49423-done) by debbugs.gnu.org; 31 Jul 2021 21:07:43 +0000 Received: from localhost ([127.0.0.1]:34980 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1m9wCt-0007bE-FM for submit@debbugs.gnu.org; Sat, 31 Jul 2021 17:07:43 -0400 Received: from lepiller.eu ([89.234.186.109]:53680) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1m9wCr-0007b1-Oq for 49423-done@debbugs.gnu.org; Sat, 31 Jul 2021 17:07:42 -0400 Received: from lepiller.eu (localhost [127.0.0.1]) by lepiller.eu (OpenSMTPD) with ESMTP id 8dc2b770 for <49423-done@debbugs.gnu.org>; Sat, 31 Jul 2021 21:07:39 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed; d=lepiller.eu; h=date:from :to:subject:message-id:in-reply-to:references:mime-version :content-type:content-transfer-encoding; s=dkim; bh=hdlPsYuYI2mr WC3XG3RDSyYPmPFsHjYR3An4axmO6EE=; b=cyGkCNaS2XCA+wQ7LI77jJm//tfQ es/vJRPnTAMcEXuTR4jx+GxvG2bj1J6ROlrU5j4D0N5X6qbNfYlgxGo5mIMmY2S1 XnzKyKaXpw5sZY5YeTTbnE68Ver6KuIUKL9eqIVtUVryZ4Eo0ZwCdve58qZtOaSW WMC5vMPURcf6ATEFVUbTgqKGo6DNLCoYCjn/WfeIkzH8M8hu0At8QqlNEgKjbja+ SVeR0XOtWl4WO4+5bEWPD3paJeK2Qxj3UBDABYvZX7MLy5zvNeh4rP7x6r6QuSrt zNeQpePNxwPSOXFD4h9f778XVx/mTEz1FLO541wZZ71ySHIVTerAL90iDA== Received: by lepiller.eu (OpenSMTPD) with ESMTPSA id 09f9fd9a (TLSv1.3:AEAD-AES256-GCM-SHA384:256:NO) for <49423-done@debbugs.gnu.org>; Sat, 31 Jul 2021 21:07:38 +0000 (UTC) Date: Sat, 31 Jul 2021 23:07:31 +0200 From: Julien Lepiller To: 49423-done@debbugs.gnu.org Subject: Re: [bug#49423] [PATCH] gnu: coq: Update to 8.13.2. Message-ID: <20210731230731.5f7813ef@tachikoma.lepiller.eu> In-Reply-To: <20210706000640.4630e3bb@tachikoma.lepiller.eu> References: <20210706000640.4630e3bb@tachikoma.lepiller.eu> X-Mailer: Claws Mail 3.17.8 (GTK+ 2.24.32; x86_64-pc-linux-gnu) 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: 49423-done 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 Tue, 6 Jul 2021 00:06:40 +0200, Julien Lepiller a =C3=A9crit : > Hi guix! >=20 > this small series updates coq to the latest version. I had to update > zarith and a few dependencies (some of which cannot be updated > independently of coq), and fix the installation of lablgtk. >=20 > This version of coq uses dune, and I split the coq package into coq, > coq-ide-server (contains coqidetop) and coq-ide (contains the > graphical interface). This also simplifies the dependency graph for > coq packages, as they no longer need the graphical stack. >=20 > I tried building the documentation too, but it complains about missing > coq package, even if I added it to the inputs of coq-doc, so it's not > part of this series. Pushed to master as 96707d5a309d083b1a9bf1f0c8fc1251cf203337 to e38b4d5ceb344c9707917a7d32df50d0ced082b5, thanks! From unknown Wed Jun 18 00:20:06 2025 Received: (at fakecontrol) by fakecontrolmessage; To: internal_control@debbugs.gnu.org From: Debbugs Internal Request Subject: Internal Control Message-Id: bug archived. Date: Sun, 29 Aug 2021 11:24:05 +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