gnu: ocaml: Build reproducibly.
[jackhill/guix/guix.git] / gnu / packages / ocaml.scm
index 85b2dc8..f21c2b2 100644 (file)
@@ -5,10 +5,11 @@
 ;;; Copyright © 2015 David Hashe <david.hashe@dhashe.com>
 ;;; Copyright © 2016 Eric Bavier <bavier@member.fsf.org>
 ;;; Copyright © 2016 Jan Nieuwenhuizen <janneke@gnu.org>
-;;; Copyright © 2016 Efraim Flashner <efraim@flashner.co.il>
+;;; Copyright © 2016, 2018 Efraim Flashner <efraim@flashner.co.il>
 ;;; Copyright © 2016, 2017 Julien Lepiller <julien@lepiller.eu>
 ;;; Copyright © 2017 Ben Woodcroft <donttrustben@gmail.com>
 ;;; Copyright © 2017, 2018 Tobias Geerinckx-Rice <me@tobias.gr>
+;;; Copyright © 2018 Peter Kreye <kreyepr@gmail.com>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -42,6 +43,7 @@
   #:use-module (gnu packages gnome)
   #:use-module (gnu packages gtk)
   #:use-module (gnu packages libevent)
+  #:use-module (gnu packages libffi)
   #:use-module (gnu packages llvm)
   #:use-module (gnu packages m4)
   #:use-module (gnu packages multiprecision)
@@ -51,6 +53,7 @@
   #:use-module (gnu packages pkg-config)
   #:use-module (gnu packages protobuf)
   #:use-module (gnu packages python)
+  #:use-module (gnu packages sdl)
   #:use-module (gnu packages tex)
   #:use-module (gnu packages texinfo)
   #:use-module (gnu packages time)
                 ;; in OCaml's directory in the store, which is read-only.
                 (substitute* "Makefile"
                   (("--prefix")
-                   "--libdir $(LIBDIR) --prefix")))))))
+                   "--libdir $(LIBDIR) --prefix"))
+                #t)))))
 
 ;; They also require almost the same set of arguments
 (define janestreet-arguments
               (patches
                (search-patches
                 "ocaml-CVE-2015-8869.patch"
-                "ocaml-Add-a-.file-directive.patch"))))
+                "ocaml-Add-a-.file-directive.patch"
+                "ocaml-enable-ocamldoc-reproducibility.patch"))))
     (build-system gnu-build-system)
     (native-search-paths
      (list (search-path-specification
@@ -395,19 +400,20 @@ syntax of OCaml.")
                            (mandir (string-append out "/share/man")))
                       ;; Custom configure script doesn't recognize
                       ;; --prefix=<PREFIX> syntax (with equals sign).
-                      (zero? (system* "./configure"
-                                      "--prefix" out
-                                      "--mandir" mandir)))))
+                      (invoke "./configure"
+                              "--prefix" out
+                              "--mandir" mandir))))
          (replace 'build
                   (lambda _
-                    (zero? (system* "make" "-j" (number->string
-                                                 (parallel-job-count))
-                                    "world.opt"))))
+                    (invoke "make" "-j" (number->string
+                                         (parallel-job-count))
+                            "world.opt")))
          ;; Required for findlib to find camlp5's libraries
          (add-after 'install 'install-meta
            (lambda* (#:key outputs #:allow-other-keys)
              (install-file "etc/META" (string-append (assoc-ref outputs "out")
-                                                     "/lib/ocaml/camlp5/")))))))
+                                                     "/lib/ocaml/camlp5/"))
+             #t)))))
     (home-page "http://camlp5.gforge.inria.fr/")
     (synopsis "Pre-processor Pretty Printer for OCaml")
     (description
@@ -451,14 +457,15 @@ written in Objective Caml.")
 (define-public coq
   (package
     (name "coq")
-    (version "8.7.0")
+    (version "8.8.0")
     (source (origin
               (method url-fetch)
-              (uri (string-append "https://coq.inria.fr/distrib/V" version
-                                  "/files/" name "-" version ".tar.gz"))
+              (uri (string-append "https://github.com/coq/coq/archive/V"
+                                  version ".tar.gz"))
+              (file-name (string-append name "-" version ".tar.gz"))
               (sha256
                (base32
-                "15wjngjd5pyfqdl5yw92rvdxvy15xcjlpx0rqlkzvcsis1z20xpk"))))
+                "0g96k2x6lbddlmkmdaczvcpb2gwqi1ydbq9bv4gf9q38kv9w3xya"))))
     (native-search-paths
      (list (search-path-specification
             (variable "COQPATH")
@@ -778,7 +785,8 @@ libpanel, librsvg and quartz.")
             ;; Without the '-fix' argument, the html file produced does not
             ;; have functioning internal hyperlinks.
             (substitute* "doc/Makefile"
-              (("hevea unison") "hevea -fix unison"))))))
+              (("hevea unison") "hevea -fix unison"))
+            #t))))
     (build-system gnu-build-system)
     (outputs '("out"
                "doc"))                  ; 1.9 MiB of documentation
@@ -848,15 +856,14 @@ to the other.")
 (define-public ocaml-findlib
   (package
     (name "ocaml-findlib")
-    (version "1.6.1")
+    (version "1.7.3")
     (source (origin
               (method url-fetch)
               (uri (string-append "http://download.camlcity.org/download/"
                                   "findlib" "-" version ".tar.gz"))
               (sha256
                (base32
-                "02abg1lsnwvjg3igdyb8qjgr5kv1nbwl4gaf8mdinzfii5p82721"))
-              (patches (search-patches "ocaml-findlib-make-install.patch"))))
+                "12xx8si1qv3xz90qsrpazjjk4lc1989fzm97rsmc4diwla7n15ni"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("camlp4" ,camlp4)
@@ -871,18 +878,25 @@ to the other.")
                    'configure
                    (lambda* (#:key inputs outputs #:allow-other-keys)
                      (let ((out (assoc-ref outputs "out")))
-                       (system*
+                       (invoke
                         "./configure"
                         "-bindir" (string-append out "/bin")
                         "-config" (string-append out "/etc/ocamfind.conf")
                         "-mandir" (string-append out "/share/man")
                         "-sitelib" (string-append out "/lib/ocaml/site-lib")
                         "-with-toolbox"))))
+                  (replace 'install
+                    (lambda* (#:key outputs #:allow-other-keys)
+                      (let ((out (assoc-ref outputs "out")))
+                        (invoke "make" "install"
+                                (string-append "OCAML_CORE_STDLIB="
+                                               out "/lib/ocaml/site-lib")))))
                   (add-after 'install 'remove-camlp4
                     (lambda* (#:key outputs #:allow-other-keys)
                       (let ((out (assoc-ref outputs "out")))
                         (delete-file-recursively
-                          (string-append out "/lib/ocaml/site-lib/camlp4"))))))))
+                         (string-append out "/lib/ocaml/site-lib/camlp4"))
+                        #t))))))
     (home-page "http://projects.camlcity.org/projects/findlib.html")
     (synopsis "Management tool for OCaml libraries")
     (description
@@ -898,28 +912,6 @@ compilation and linkage, there are new frontends of the various OCaml
 compilers that can directly deal with packages.")
     (license license:x11)))
 
-(define-public ocaml-findlib-1.7.3
-  (package
-    (inherit ocaml-findlib)
-    (version "1.7.3")
-    (source (origin
-              (method url-fetch)
-              (uri (string-append "http://download.camlcity.org/download/"
-                                  "findlib" "-" version ".tar.gz"))
-              (sha256
-               (base32
-                "12xx8si1qv3xz90qsrpazjjk4lc1989fzm97rsmc4diwla7n15ni"))))
-    (arguments
-     (substitute-keyword-arguments (package-arguments ocaml-findlib)
-       ((#:phases phases)
-        `(modify-phases ,phases
-           (replace 'install
-             (lambda* (#:key outputs #:allow-other-keys)
-               (let ((out (assoc-ref outputs "out")))
-                 (zero? (system* "make" "install"
-                                 (string-append "OCAML_CORE_STDLIB="
-                                                out))))))))))))
-
 (define-public ocaml4.01-findlib
   (package
     (inherit ocaml-findlib)
@@ -1137,14 +1129,15 @@ instances and printing them.")
 (define-public ocaml-qtest
   (package
     (name "ocaml-qtest")
-    (version "2.5")
+    (version "2.8")
     (source (origin
               (method url-fetch)
-              (uri (string-append "https://github.com/vincent-hugot/iTeML/"
-                                  "archive/v" version ".tar.gz"))
+              (uri (string-append "https://github.com/vincent-hugot/qtest/"
+                                  "archive/" version ".tar.gz"))
+              (file-name (string-append name "-" version ".tar.gz"))
               (sha256
                (base32
-                "1hw3jqir7w79payy4knc38fa3nxcvl7ap6y6hnqavrhpi8zqb59j"))))
+                "1ff4if64mc9c7wmhjdgnlnh6k6a713piqzr4043zzj4s5pw7smxk"))))
     (build-system ocaml-build-system)
     (native-inputs
      `(("findlib" ,ocaml-findlib)))
@@ -1158,7 +1151,7 @@ instances and printing them.")
        #:phases
        (modify-phases %standard-phases
          (delete 'configure))))
-    (home-page "https://github.com/vincent-hugot/iTeML")
+    (home-page "https://github.com/vincent-hugot/qtest")
     (synopsis "Inline (Unit) Tests for OCaml")
     (description "Qtest extracts inline unit tests written using a special
 syntax in comments.  Those tests are then run using the oUnit framework and the
@@ -1177,6 +1170,7 @@ to use -- to sophisticated random generation of test cases.")
               (method url-fetch)
               (uri (string-append "https://github.com/rgrinberg/stringext"
                                   "/archive/v" version ".tar.gz"))
+              (file-name (string-append name "-" version ".tar.gz"))
               (sha256
                (base32
                 "19g6lfn03iki9f8h91hi0yiqn0b3wkxyq08b3y23wgv6jw6mssfh"))))
@@ -1256,6 +1250,7 @@ coverage information.")
               (method url-fetch)
               (uri (string-append "https://github.com/xguerin/bitstring"
                                   "/archive/v" version ".tar.gz"))
+              (file-name (string-append name "-" version ".tar.gz"))
               (sha256
                (base32
                 "0vy8ibrxccii1jbsk5q6yh1kxjigqvi7lhhcmizvd5gfhf7mfyc8"))
@@ -1321,6 +1316,7 @@ powerful.")
               (method url-fetch)
               (uri (string-append "https://github.com/janestreet/result"
                                   "/archive/" version ".tar.gz"))
+              (file-name (string-append name "-" version ".tar.gz"))
               (sha256
                (base32
                 "1pgpfsgvhxnh0i37fkvp9j8nadns9hz9iqgabj4dr519j2gr1xvw"))))
@@ -1658,6 +1654,7 @@ lets the client choose the concrete timeline.")
         (method url-fetch)
         (uri (string-append "https://github.com/savonet/ocaml-ssl/archive/"
                             version ".tar.gz"))
+        (file-name (string-append name "-" version ".tar.gz"))
         (sha256 (base32
                   "15p7652cvzdrlqxc1af11mg07wasxr1fsaj44gcmmh6bmav7wfzq"))))
     (build-system ocaml-build-system)
@@ -1692,6 +1689,7 @@ through Transport Layer Security (@dfn{TLS}) encrypted connections.")
         (method url-fetch)
         (uri (string-append "https://github.com/ocsigen/lwt/archive/" version
                             ".tar.gz"))
+        (file-name (string-append name "-" version ".tar.gz"))
         (sha256 (base32
                   "1gbw0g8a5a4b16diqrmlhc8ilnikrm4w3jjm1zq310maqg8z0zxz"))))
     (build-system ocaml-build-system)
@@ -2204,17 +2202,19 @@ file (POSIX like) and filename.")
                 "1ln7vc7ip6s5xbi20mhnn087xi4a2m5vqawx0703qqnfkzhmslqy"))
             (modules '((guix build utils)))
             (snippet
-             '(substitute* "test/test-main/Test.ml"
-                ;; most of these tests fail because ld cannot find crti.o, but according
-                ;; to the log file, the environment variables {LD_,}LIBRARY_PATH
-                ;; are set correctly whene LD_LIBRARY_PATH is defined beforhand.
-                (("TestBaseCompat.tests;") "")
-                (("TestExamples.tests;") "")
-                (("TestFull.tests;") "")
-                (("TestPluginDevFiles.tests;") "")
-                (("TestPluginInternal.tests;") "")
-                (("TestPluginOCamlbuild.tests;") "")
-                (("TestPluginOMake.tests;") "")))))
+             '(begin
+                (substitute* "test/test-main/Test.ml"
+                  ;; most of these tests fail because ld cannot find crti.o, but according
+                  ;; to the log file, the environment variables {LD_,}LIBRARY_PATH
+                  ;; are set correctly whene LD_LIBRARY_PATH is defined beforhand.
+                  (("TestBaseCompat.tests;") "")
+                  (("TestExamples.tests;") "")
+                  (("TestFull.tests;") "")
+                  (("TestPluginDevFiles.tests;") "")
+                  (("TestPluginInternal.tests;") "")
+                  (("TestPluginOCamlbuild.tests;") "")
+                  (("TestPluginOMake.tests;") ""))
+                #t))))
     (build-system ocaml-build-system)
     (native-inputs
      `(("ocamlify" ,ocamlify)
@@ -3462,6 +3462,7 @@ and 4 (random based) according to RFC 4122.")
               (method url-fetch)
               (uri (string-append "https://github.com/alavrik/piqi-ocaml/"
                                   "archive/v" version ".tar.gz"))
+              (file-name (string-append name "-" version ".tar.gz"))
               (sha256
                (base32
                 "0ngz6y8i98i5v2ma8nk6mc83pdsmf2z0ks7m3xi6clfg3zqbddrv"))))
@@ -3501,13 +3502,13 @@ XML and Protocol Buffers formats.")
    (build-system ocaml-build-system)
    (native-inputs
     `(("oasis" ,ocaml-oasis)
-      ("clang" ,clang)
+      ("clang" ,clang-3.8)
       ("ounit" ,ocaml-ounit)))
    (propagated-inputs
     `(("core-kernel" ,ocaml-core-kernel)
       ("ppx-driver" ,ocaml-ppx-driver)
       ("uri" ,ocaml-uri)
-      ("llvm" ,llvm)
+      ("llvm" ,llvm-3.8)
       ("gmp" ,gmp)
       ("clang-runtime" ,clang-runtime)
       ("fileutils" ,ocaml-fileutils)
@@ -3523,7 +3524,7 @@ XML and Protocol Buffers formats.")
       ("bitstring" ,ocaml-bitstring)
       ("ppx-jane" ,ocaml-ppx-jane)
       ("re" ,ocaml-re)))
-   (inputs `(("llvm" ,llvm)))
+   (inputs `(("llvm" ,llvm-3.8)))
    (arguments
     `(#:use-make? #t
       #:phases
@@ -3726,7 +3727,7 @@ instead of bindings to a C library.")
        ("cppo" ,ocaml-cppo)
        ("jbuilder" ,ocaml-jbuilder)))
     (propagated-inputs
-     `(("findlib" ,ocaml-findlib-1.7.3)
+     `(("ocaml-findlib" ,ocaml-findlib)
        ("lambda-term" ,ocaml-lambda-term)
        ("lwt" ,ocaml-lwt)
        ("react" ,ocaml-react)
@@ -3739,17 +3740,151 @@ terminal or in Emacs.  It supports line editing, history, real-time and context
 sensitive completion, colors, and more.")
     (license license:bsd-3)))
 
+(define-public ocaml-integers
+  (package
+    (name "ocaml-integers")
+    (version "0.2.2")
+    (home-page "https://github.com/ocamllabs/ocaml-integers")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append home-page
+                                  "/releases/download/v0.2.2/integers-"
+                                  version ".tbz"))
+              (file-name (string-append name "-" version ".tbz"))
+              (sha256
+               (base32
+                "08b1ljw88ny3l0mdq6xmffjk8anfc77igryva5jz1p6f4f746ywk"))))
+    (build-system ocaml-build-system)
+    (arguments
+     `(#:tests? #f; no tests
+       #:build-flags (list "build")
+       #:phases
+       (modify-phases %standard-phases
+         (delete 'configure))))
+    (inputs
+     `(("topkg" ,ocaml-topkg)
+       ("opam" ,opam)))
+    (synopsis "Various signed and unsigned integer types for OCaml")
+    (description "The ocaml-integers library provides a number of 8-, 16-, 32-
+and 64-bit signed and unsigned integer types, together with aliases such as
+long and size_t whose sizes depend on the host platform.")
+    (license license:expat)))
+
+(define-public ocaml-ctypes
+  (package
+   (name "ocaml-ctypes")
+   (version "0.13.1")
+   (home-page "https://github.com/ocamllabs/ocaml-ctypes")
+   (source (origin
+             (method url-fetch)
+             (uri (string-append home-page "/archive/" version ".tar.gz"))
+             (file-name (string-append name "-" version ".tar.gz"))
+             (sha256
+              (base32
+               "17w0pr5k0zjcjns4y9n36rjpfl35zhvp3h8ggqs9lz12qhshdk2m"))))
+   (build-system ocaml-build-system)
+   (arguments
+    `(#:make-flags
+      (list (string-append "INSTALL_HEADERS = $(wildcard $($(PROJECT).dir)/*.h)"))
+      #:phases
+      (modify-phases %standard-phases
+        (delete 'configure))))
+   (native-inputs
+    `(("pkg-config" ,pkg-config)))
+   (inputs
+    `(("libffi" ,libffi)
+      ("ounit" ,ocaml-ounit)
+      ("integers" ,ocaml-integers)
+      ("lwt" ,ocaml-lwt)
+      ("topkg" ,ocaml-topkg)
+      ("opam" ,opam)))
+   (synopsis "Library for binding to C libraries using pure OCaml")
+   (description "Ctypes is a library for binding to C libraries using pure
+OCaml.  The primary aim is to make writing C extensions as straightforward as
+possible.  The core of ctypes is a set of combinators for describing the
+structure of C types -- numeric types, arrays, pointers, structs, unions and
+functions.  You can use these combinators to describe the types of the
+functions that you want to call, then bind directly to those functions -- all
+without writing or generating any C!")
+   (license license:expat)))
+
+(define-public ocaml-ocb-stubblr
+  (package
+   (name "ocaml-ocb-stubblr")
+   (version "0.1.1")
+   (home-page "https://github.com/pqwy/ocb-stubblr")
+   (source (origin
+             (method url-fetch)
+             (uri (string-append
+                   home-page "/releases/download/v0.1.1/ocb-stubblr-"
+                   version ".tbz"))
+             (file-name (string-append name "-" version ".tbz"))
+             (sha256
+              (base32
+               "167b7x1j21mkviq8dbaa0nmk4rps2ilvzwx02igsc2706784z72f"))))
+   (build-system ocaml-build-system)
+   (arguments
+    `(#:build-flags (list "build" "--tests" "true")
+      #:phases
+      (modify-phases %standard-phases
+        (delete 'configure))))
+   (inputs
+    `(("topkg" ,ocaml-topkg)
+      ("opam" ,opam)))
+   (native-inputs
+    `(("astring" ,ocaml-astring)))
+   (synopsis "OCamlbuild plugin for C stubs")
+   (description "Ocb-stubblr is about ten lines of code that you need to
+repeat over, over, over and over again if you are using ocamlbuild to build
+OCaml projects that contain C stubs.")
+   (license license:isc)))
+
+(define-public ocaml-tsdl
+  (package
+    (name "ocaml-tsdl")
+    (version "0.9.1")
+    (home-page "http://erratique.ch/software/tsdl")
+    (source (origin
+              (method url-fetch)
+              (uri (string-append home-page "/releases/tsdl-"
+                                  version ".tbz"))
+              (file-name (string-append name "-" version ".tar.gz"))
+              (sha256
+               (base32
+                "08bb97fhvz829fb0sgjn2p20mp7b04v98zy2qxpk2w390a6c4b34"))))
+    (build-system ocaml-build-system)
+    (arguments
+     `(#:build-flags '("build")
+       #:tests? #f; tests require a display device
+       #:phases
+       (modify-phases %standard-phases
+         (delete 'configure))))
+    (native-inputs
+     `(("opam" ,opam)
+       ("pkg-config" ,pkg-config)))
+    (inputs
+     `(("topkg" ,ocaml-topkg)
+       ("result" ,ocaml-result)
+       ("sdl2" ,sdl2)
+       ("integers" ,ocaml-integers)
+       ("ctypes" ,ocaml-ctypes)))
+    (synopsis "Thin bindings to SDL for OCaml")
+    (description "Tsdl is an OCaml library providing thin bindings to the
+cross-platform SDL C library.")
+    (license license:isc)))
+
 (define-public coq-flocq
   (package
     (name "coq-flocq")
-    (version "2.6.0")
+    (version "2.6.1")
     (source (origin
               (method url-fetch)
-              (uri (string-append "https://gforge.inria.fr/frs/download.php/file"
-                                  "/37054/flocq-" version ".tar.gz"))
+              ;; Use the ‘Latest version’ link for a stable URI across releases.
+              (uri (string-append "https://gforge.inria.fr/frs/download.php/"
+                                  "file/37454/flocq-" version ".tar.gz"))
               (sha256
                (base32
-                "13fv150dcwnjrk00d7zj2c5x9jwmxgrq0ay440gkr730l8mvk3l3"))))
+                "06msp1fwpqv6p98a3i1nnkj7ch9rcq3rm916yxq8dxf51lkghrin"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("ocaml" ,ocaml)
@@ -3764,18 +3899,22 @@ sensitive completion, colors, and more.")
          (add-before 'configure 'fix-remake
            (lambda _
              (substitute* "remake.cpp"
-               (("/bin/sh") (which "sh")))))
+               (("/bin/sh") (which "sh")))
+             #t))
          (replace 'build
            (lambda _
-             (zero? (system* "./remake"))))
+             (invoke "./remake")
+             #t))
          (replace 'check
            (lambda _
-             (zero? (system* "./remake" "check"))))
+             (invoke "./remake" "check")
+             #t))
              ;; TODO: requires coq-gappa and coq-interval.
-             ;(zero? (system* "./remake" "check-more"))))
+             ;(invoke "./remake" "check-more")
          (replace 'install
            (lambda _
-             (zero? (system* "./remake" "install")))))))
+             (invoke "./remake" "install")
+             #t)))))
     (home-page "http://flocq.gforge.inria.fr/")
     (synopsis "Floating-point formalization for the Coq system")
     (description "Flocq (Floats for Coq) is a floating-point formalization for
@@ -3787,14 +3926,14 @@ inside Coq.")
 (define-public coq-gappa
   (package
     (name "coq-gappa")
-    (version "1.3.1")
+    (version "1.3.2")
     (source (origin
               (method url-fetch)
-              (uri (string-append "https://gforge.inria.fr/frs/download.php/file/36351/gappa-"
+              (uri (string-append "https://gforge.inria.fr/frs/download.php/file/36397/gappa-"
                                   version ".tar.gz"))
               (sha256
                (base32
-                "0924jr6f15fx22qfsvim5vc0qxqg30ivg9zxj34lf6slbgdl3j39"))))
+                "19kg2zldaqs4smy7bv9hp650sqg46xbx1ss7jnyagpxdscwn9apd"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("ocaml" ,ocaml)
@@ -3839,14 +3978,14 @@ assistant.")
 (define-public coq-mathcomp
   (package
     (name "coq-mathcomp")
-    (version "1.6.2")
+    (version "1.7.0")
     (source (origin
               (method url-fetch)
               (uri (string-append "https://github.com/math-comp/math-comp/archive/mathcomp-"
                                   version ".tar.gz"))
               (sha256
                (base32
-                "0lg5ncr7p4y8qqq6pfw6brqc6a9xzlfa0drprwfdn0rnyaq5nca6"))))
+                "05zgyi4wmasi1rcyn5jq42w0bi9713q9m8dl1fdgl66nmacixh39"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("ocaml" ,ocaml)
@@ -3902,6 +4041,12 @@ part of the distribution.")
                             "/lib/coq/user-contrib/Coquelicot"))
        #:phases
        (modify-phases %standard-phases
+         (add-before 'configure 'fix-coq8.8
+           (lambda _
+             ; appcontext has been removed from coq 8.8
+             (substitute* "theories/AutoDerive.v"
+               (("appcontext") "context"))
+             #t))
          (add-before 'configure 'fix-remake
            (lambda _
              (substitute* "remake.cpp"
@@ -3931,7 +4076,7 @@ theorems between the two libraries.")
 (define-public coq-bignums
   (package
     (name "coq-bignums")
-    (version "8.7.0")
+    (version "8.8.0")
     (source (origin
               (method url-fetch)
               (uri (string-append "https://github.com/coq/bignums/archive/V"
@@ -3939,7 +4084,7 @@ theorems between the two libraries.")
               (file-name (string-append name "-" version ".tar.gz"))
               (sha256
                (base32
-                "03iw9jiwq9jx45gsvp315y3lxr8m9ksppmcjvxs5c23qnky6zqjx"))))
+                "08m1cmq4hkaf4sb0vy978c11rgzvds71cphyadmr2iirpr5815r0"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("ocaml" ,ocaml)