From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp1 ([2001:41d0:2:bcc0::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms0.migadu.com with LMTPS id GAhiGc2C42CndAEAgWs5BA (envelope-from ) for ; Tue, 06 Jul 2021 00:08:13 +0200 Received: from aspmx1.migadu.com ([2001:41d0:2:bcc0::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp1 with LMTPS id aEnpFM2C42CgGwAAbx9fmQ (envelope-from ) for ; Mon, 05 Jul 2021 22:08:13 +0000 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by aspmx1.migadu.com (Postfix) with ESMTPS id 9A292164C5 for ; Tue, 6 Jul 2021 00:08:12 +0200 (CEST) Received: from localhost ([::1]:39108 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1m0Wl9-0006xG-Nc for larch@yhetil.org; Mon, 05 Jul 2021 18:08:11 -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 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-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+larch=yhetil.org@gnu.org Sender: "Guix-patches" X-Migadu-Flow: FLOW_IN ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=yhetil.org; s=key1; t=1625522892; h=from:from:sender:sender:reply-to:subject:subject:date:date: message-id:message-id:to:to:cc:mime-version:mime-version: content-type:content-type:resent-cc:resent-from:resent-sender: resent-message-id:list-id:list-help:list-unsubscribe:list-subscribe: list-post:dkim-signature; bh=TwHF4Ria2Hhlg9qQNkq/wFW7mB11IcP9CL1DfNSvOPs=; b=bNYh889Rxlj11X+tHhuW6C32pYM98rJ2aISMlLu2d9HGzvkaV2KgKnXu62Ob9XIhWwRTml xac3zyYX59CEklHTo+lC8KWmniBxBEEy48+d+Csc7kr01t6R+fixcZ6nbY3ScQO9cQxxFw K2BZ9PdMFHOEbz3wrtAj+jkk5ZeAwHBwdbej7F/vSWRNRtq0aT0oAE8Q6a9QTKyh9nli/X N3apS7tBEoPmJcljmeS6iFJK/gwKorhRmq+kCrsjFHKtM/2rfzF+YHotBtTHVDqQzdtG4n lNHsHJB/Qa5Re5fJ7IXgmFpRCI5DyWkILybl/CwPi+g3IBdA4+q6C5GkLDLGjA== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1625522892; a=rsa-sha256; cv=none; b=frp17Dcf8rNnbp+zzFuoi3YuiHhi3sQ2oBaKv3mogYsUfRsPvFFQVLmpfzU7Q0r9qrxJNv QOgfOcudYtjepdxXYRFb1XiD8nSdLHG2mxePTeG5tmKz42nYM0J4uvOpC38SOh2ERxIZ+K AwIu3Z3XdVzqkDt5/1fjPCxACna+nsk2/3sg9X+l/PSxiXZnPMOZwiu3Ng99nffJyUouYv kZSnulttEfaW3V80fp7qMJ09nZmD6/JaDH3D8IJ2NuKcf6INzsA5P0IIHszkXJy7d6aGhy TihjuPg24HEc0ibntBR89T8BsDe6RRifM6DjDaVPQDPrYUsOXtDe8ItqX0tKGA== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=lepiller.eu header.s=dkim header.b=MS8B8Hzo; spf=pass (aspmx1.migadu.com: domain of guix-patches-bounces@gnu.org designates 209.51.188.17 as permitted sender) smtp.mailfrom=guix-patches-bounces@gnu.org X-Migadu-Spam-Score: -1.31 Authentication-Results: aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=lepiller.eu header.s=dkim header.b=MS8B8Hzo; dmarc=fail reason="SPF not aligned (relaxed)" header.from=lepiller.eu (policy=none); spf=pass (aspmx1.migadu.com: domain of guix-patches-bounces@gnu.org designates 209.51.188.17 as permitted sender) smtp.mailfrom=guix-patches-bounces@gnu.org X-Migadu-Queue-Id: 9A292164C5 X-Spam-Score: -1.31 X-Migadu-Scanner: scn0.migadu.com X-TUID: yeVvyyTgVN53 --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--