Merge branch 'master' into staging

1 files changed, 52 insertions, 39 deletions

diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index fc162759c2..864038fe99 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -100,7 +100,8 @@
                 ;; 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
@@ -398,19 +399,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
@@ -454,14 +456,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")
@@ -781,7 +784,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
@@ -873,7 +877,7 @@ 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")
@@ -883,14 +887,15 @@ to the other.")
                   (replace 'install
                     (lambda* (#:key outputs #:allow-other-keys)
                       (let ((out (assoc-ref outputs "out")))
-                        (zero? (system* "make" "install"
-                                        (string-append "OCAML_CORE_STDLIB="
-                                                       out "/lib/ocaml/site-lib"))))))
+                        (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
@@ -2196,17 +2201,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)
@@ -3868,15 +3875,15 @@ cross-platform SDL C library.")
 (define-public coq-flocq
   (package
     (name "coq-flocq")
-    (version "2.6.0")
+    (version "2.6.1")
     (source (origin
               (method url-fetch)
               ;; Use the ‘Latest version’ link for a stable URI across releases.
               (uri (string-append "https://gforge.inria.fr/frs/download.php/"
-                                  "latestfile/2228/flocq-" version ".tar.gz"))
+                                  "file/37454/flocq-" version ".tar.gz"))
               (sha256
                (base32
-                "13fv150dcwnjrk00d7zj2c5x9jwmxgrq0ay440gkr730l8mvk3l3"))))
+                "06msp1fwpqv6p98a3i1nnkj7ch9rcq3rm916yxq8dxf51lkghrin"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("ocaml" ,ocaml)
@@ -3918,14 +3925,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)
@@ -3970,14 +3977,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)
@@ -4033,6 +4040,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"
@@ -4062,7 +4075,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"
@@ -4070,7 +4083,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)