From patchwork Mon Jul 5 22:06:40 2021 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Patchwork-Submitter: Julien Lepiller X-Patchwork-Id: 31184 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id AF3D527BC78; Mon, 5 Jul 2021 23:08:15 +0100 (BST) X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-2.8 required=5.0 tests=BAYES_00,DKIM_SIGNED, MAILING_LIST_MULTI,SPF_HELO_PASS,T_DKIM_INVALID,URIBL_BLOCKED autolearn=unavailable autolearn_force=no version=3.4.2 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTPS id 378E927BC81 for ; Mon, 5 Jul 2021 23:08:14 +0100 (BST) Received: from localhost ([::1]:39108 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1m0WlB-0006xG-B6 for patchwork@mira.cbaines.net; Mon, 05 Jul 2021 18:08:13 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:53772) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1m0Wl1-0006x5-0x for guix-patches@gnu.org; Mon, 05 Jul 2021 18:08:03 -0400 Received: from debbugs.gnu.org ([209.51.188.43]:35241) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1m0Wl0-0000zx-PR for guix-patches@gnu.org; Mon, 05 Jul 2021 18:08:02 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1m0Wl0-0001nP-EE for guix-patches@gnu.org; Mon, 05 Jul 2021 18:08:02 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#49423] [PATCH] gnu: coq: Update to 8.13.2. Resent-From: Julien Lepiller Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Mon, 05 Jul 2021 22:08:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: report 49423 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 49423@debbugs.gnu.org X-Debbugs-Original-To: guix-patches@gnu.org Received: via spool by submit@debbugs.gnu.org id=B.16255228256838 (code B ref -1); Mon, 05 Jul 2021 22:08:02 +0000 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 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 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-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: "Guix-patches" X-getmail-retrieved-from-mailbox: Patches 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 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 © 2018 Julien Lepiller +;;; Copyright © 2018-2021 Julien Lepiller ;;; Copyright © 2018, 2019 Tobias Geerinckx-Rice ;;; Copyright © 2019 Dan Frumin ;;; Copyright © 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+)))) +(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 commits ;; 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=" (assoc-ref %outputs "out") - "/lib/coq/user-contrib/Gappa")) + (list (string-append "COQUSERCONTRIB=" (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 standard 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 standard 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=" (assoc-ref %outputs "out") - "/lib/coq/user-contrib/Gappa")) + (list (string-append "COQUSERCONTRIB=" (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 -- 2.32.0