all messages for Guix-related lists mirrored at yhetil.org
 help / color / mirror / code / Atom feed
* [bug#49423] [PATCH] gnu: coq: Update to 8.13.2.
@ 2021-07-05 22:06 Julien Lepiller
  2021-07-21 14:07 ` Ludovic Courtès
                   ` (2 more replies)
  0 siblings, 3 replies; 4+ messages in thread
From: Julien Lepiller @ 2021-07-05 22:06 UTC (permalink / raw)
  To: 49423

[-- Attachment #1: Type: text/plain, Size: 623 bytes --]

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.

[-- Attachment #2: 0001-gnu-ocaml-zarith-Update-to-1.12.patch --]
[-- Type: text/x-patch, Size: 2026 bytes --]

From 73fc06926c86e8dad8bbb61f6a1728343fd2a487 Mon Sep 17 00:00:00 2001
From: Julien Lepiller <julien@lepiller.eu>
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


[-- Attachment #3: 0002-gnu-lablgtk3-Install-with-version-information.patch --]
[-- Type: text/x-patch, Size: 1137 bytes --]

From 76a337769e67e84a32c5b85d80ab6bc160792aef Mon Sep 17 00:00:00 2001
From: Julien Lepiller <julien@lepiller.eu>
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


[-- Attachment #4: 0003-gnu-coq-stdpp-Update-to-1.5.0.patch --]
[-- Type: text/x-patch, Size: 1111 bytes --]

From 8f374c9e8001db83a12ef6feee8404cbef4daaab Mon Sep 17 00:00:00 2001
From: Julien Lepiller <julien@lepiller.eu>
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


[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #5: 0004-gnu-coq-Update-to-8.13.2.patch --]
[-- Type: text/x-patch, Size: 11569 bytes --]

From 074a392bc2139309a39a06b03520af0573c844b1 Mon Sep 17 00:00:00 2001
From: Julien Lepiller <julien@lepiller.eu>
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 <julien@lepiller.eu>
+;;; Copyright © 2018-2021 Julien Lepiller <julien@lepiller.eu>
 ;;; Copyright © 2018, 2019 Tobias Geerinckx-Rice <me@tobias.gr>
 ;;; Copyright © 2019 Dan Frumin <dfrumin@cs.ru.nl>
 ;;; Copyright © 2020 Brett Gilio <brettg@gnu.org>
@@ -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


^ permalink raw reply related	[flat|nested] 4+ messages in thread
end of thread, other threads:[~2021-07-31 21:08 UTC | newest]

Thread overview: 4+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2021-07-05 22:06 [bug#49423] [PATCH] gnu: coq: Update to 8.13.2 Julien Lepiller
2021-07-21 14:07 ` Ludovic Courtès
2021-07-24 13:17 ` Xinglu Chen
2021-07-31 21:07 ` bug#49423: " Julien Lepiller

Code repositories for project(s) associated with this external index

	https://git.savannah.gnu.org/cgit/guix.git

This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.