gnu: icecat: Update to 78.10.0-guix0-preview1 [security fixes].

[jackhill/guix/guix.git] / gnu / packages / coq.scm

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 3eba39e..fb6a899 100644 (file)
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -3,6 +3,9 @@
 ;;; Copyright © 2018, 2019 Tobias Geerinckx-Rice <me@tobias.gr>
 ;;; Copyright © 2019 Dan Frumin <dfrumin@cs.ru.nl>
 ;;; Copyright © 2020 Brett Gilio <brettg@gnu.org>
+;;; Copyright © 2020 Björn Höfling <bjoern.hoefling@bjoernhoefling.de>
+;;; Copyright © 2020 raingloom <raingloom@riseup.net>
+;;; Copyright © 2020 Robin Green <greenrd@greenrd.org>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -32,6 +35,7 @@
   #:use-module (gnu packages ocaml)
   #:use-module (gnu packages perl)
   #:use-module (gnu packages python)
+  #:use-module (gnu packages rsync)
   #:use-module (gnu packages texinfo)
   #:use-module (guix build-system gnu)
   #:use-module (guix build-system ocaml)
@@ -45,17 +49,17 @@
 (define-public coq
   (package
     (name "coq")
-    (version "8.10.2")
+    (version "8.11.2")
     (source
      (origin
        (method git-fetch)
        (uri (git-reference
-             (url "https://github.com/coq/coq.git")
+             (url "https://github.com/coq/coq")
              (commit (string-append "V" version))))
        (file-name (git-file-name name version))
        (sha256
         (base32
-         "0ji2rzd70b3hcwfw97qk7rv3m2977ylqnq82l1555dp3njr8nm3q"))))
+         "1gia82dkmzqspw2w3s4gjyh39ghbmw4i41i4hyzc91g7mza17nbz"))))
     (native-search-paths
      (list (search-path-specification
             (variable "COQPATH")
@@ -68,7 +72,9 @@
        ("camlp5" ,camlp5)
        ("ocaml-num" ,ocaml-num)))
     (native-inputs
-     `(("ocaml-ounit" ,ocaml-ounit)))
+     `(("ocaml-ounit" ,ocaml-ounit)
+       ("rsync" ,rsync)
+       ("which" ,which)))
     (arguments
      `(#:phases
        (modify-phases %standard-phases
@@ -95,11 +101,18 @@
          (add-after 'install 'remove-duplicate
            (lambda* (#:key outputs #:allow-other-keys)
              (let* ((out (assoc-ref outputs "out"))
-                    (bin (string-append out "/bin")))
+                    (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.
-               (delete-file (string-append bin "/coqtop.opt"))
-               (delete-file (string-append bin "/coqidetop.opt")))
+               ;; 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)
@@ -116,7 +129,7 @@
                ;; 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-recursively "coq-makefile/findlib-package")
+               (delete-file "misc/printers.sh")
                (invoke "make")))))))
     (home-page "https://coq.inria.fr")
     (synopsis "Proof assistant for higher-order logic")
@@ -131,15 +144,17 @@ It is developed using Objective Caml and Camlp5.")
 (define-public proof-general
   (package
     (name "proof-general")
-    (version "4.2")
+    (version "4.4")
     (source (origin
-              (method url-fetch)
-              (uri (string-append
-                    "http://proofgeneral.inf.ed.ac.uk/releases/"
-                    "ProofGeneral-" version ".tgz"))
+              (method git-fetch)
+              (uri (git-reference
+                    (url (string-append
+                          "https://github.com/ProofGeneral/PG"))
+                    (commit (string-append "v" version))))
+              (file-name (git-file-name name version))
               (sha256
                (base32
-                "09qb0myq66fw17v4ziz401ilsb5xlxz1nl2wsp69d0vrfy0bcrrm"))))
+                "0bdfk91wf71z80mdfnl8hpinripndcjgdkz854zil6521r84nqk8"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("which" ,which)
@@ -174,10 +189,6 @@ It is developed using Objective Caml and Camlp5.")
                             (emacs (assoc-ref inputs "host-emacs")))
                         (define (coq-prog name)
                           (string-append coq "/bin/" name))
-                        (emacs-substitute-variables "coq/coq.el"
-                          ("coq-prog-name"           (coq-prog "coqtop"))
-                          ("coq-compiler"            (coq-prog "coqc"))
-                          ("coq-dependency-analyzer" (coq-prog "coqdep")))
                         (substitute* "Makefile"
                           (("/sbin/install-info") "install-info"))
                         (substitute* "bin/proofgeneral"
@@ -197,7 +208,7 @@ It is developed using Objective Caml and Camlp5.")
              (substitute* "Makefile"
                ((" [^ ]*\\.pdf") ""))
              (apply invoke "make" "install-doc" make-flags))))))
-    (home-page "http://proofgeneral.inf.ed.ac.uk/")
+    (home-page "https://proofgeneral.github.io/ ")
     (synopsis "Generic front-end for proof assistants based on Emacs")
     (description
      "Proof General is a major mode to turn Emacs into an interactive proof
@@ -208,7 +219,7 @@ provers.")
 (define-public coq-flocq
   (package
     (name "coq-flocq")
-    (version "3.2.0")
+    (version "3.3.1")
     (source
      (origin
        (method git-fetch)
@@ -218,7 +229,7 @@ provers.")
        (file-name (git-file-name name version))
        (sha256
         (base32
-         "15bi36x7zj0glsb3s2gwqd4wswhfzh36rbp7imbyff53a7nna95l"))))
+         "01gdykva0lcw6y3dm8j0djxayb87szfg9vn0mxd6z3pks644misl"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("autoconf" ,autoconf)
@@ -265,7 +276,7 @@ inside Coq.")
 (define-public coq-gappa
   (package
     (name "coq-gappa")
-    (version "1.4.2")
+    (version "1.4.4")
     (source
      (origin
        (method git-fetch)
@@ -275,7 +286,7 @@ inside Coq.")
        (file-name (git-file-name name version))
        (sha256
         (base32
-         "0r7jwp5xssdfzivs2flp7mzrscqhgl63mryhhf1cvndpgzqwfk2f"))))
+         "0f3g3wjkvfkm961l4jpckhsqd43jnvm7f5qqk78qc32zh1fg339n"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("autoconf" ,autoconf)
@@ -325,16 +336,16 @@ assistant.")
 (define-public coq-mathcomp
   (package
     (name "coq-mathcomp")
-    (version "1.10.0")
+    (version "1.11.0")
     (source
      (origin
        (method git-fetch)
        (uri (git-reference
-             (url "https://github.com/math-comp/math-comp.git")
+             (url "https://github.com/math-comp/math-comp")
              (commit (string-append "mathcomp-" version))))
        (file-name (git-file-name name version))
        (sha256
-        (base32 "1h5h1c2025r1ms5qryvwy6pikxmpmmjav6yl127xpzmqdi6w732d"))))
+        (base32 "1axywpa1jcpnidd86irpd1gdbbg2sfbwc652675xisq5wnmfmf6f"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("ocaml" ,ocaml)
@@ -353,7 +364,7 @@ assistant.")
                      (string-append "COQLIB=" (assoc-ref outputs "out")
                                     "/lib/coq/")
                      "install"))))))
-    (home-page "https://math-comp.github.io/math-comp/")
+    (home-page "https://math-comp.github.io/")
     (synopsis "Mathematical Components for Coq")
     (description "Mathematical Components for Coq has its origins in the formal
 proof of the Four Colour Theorem.  Since then it has grown to cover many areas
@@ -367,7 +378,7 @@ part of the distribution.")
 (define-public coq-coquelicot
   (package
     (name "coq-coquelicot")
-    (version "3.0.3")
+    (version "3.1.0")
     (source
      (origin
        (method git-fetch)
@@ -377,7 +388,7 @@ part of the distribution.")
        (file-name (git-file-name name version))
        (sha256
         (base32
-         "0m5wbr2s8lnf8b7cfwv15hyzsmbcaz6hgdn7aazcrkxnwr87vgkp"))))
+         "0mz3pxan1237fr5fi79c66y7b9z7bmi0sc45kwrmkczsjm5462jm"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("autoconf" ,autoconf)
@@ -420,16 +431,16 @@ theorems between the two libraries.")
 (define-public coq-bignums
   (package
     (name "coq-bignums")
-    (version "8.10.0")
+    (version "8.11.0")
     (source (origin
               (method git-fetch)
               (uri (git-reference
-                     (url "https://github.com/coq/bignums.git")
+                     (url "https://github.com/coq/bignums")
                      (commit (string-append "V" version))))
               (file-name (git-file-name name version))
               (sha256
                (base32
-                "0bpb4flckn4nqxbs3wjiznyx1k7r8k93qdigp3qwmikp2lxvcbw5"))))
+                "1xcd7c7qlvs0narfba6px34zq0mz8rffnhxw0kzhhg6i4iw115dp"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("ocaml" ,ocaml)
@@ -453,7 +464,7 @@ provides BigN, BigZ, BigQ that used to be part of Coq standard library.")
 (define-public coq-interval
   (package
     (name "coq-interval")
-    (version "3.4.1")
+    (version "4.0.0")
     (source
      (origin
        (method git-fetch)
@@ -463,7 +474,7 @@ provides BigN, BigZ, BigQ that used to be part of Coq standard library.")
        (file-name (git-file-name name version))
        (sha256
         (base32
-         "03q3dfqi3r3f7aji5s06ig4aav9ajcwswwdzi5lrgr69z0m487k4"))))
+         "01iz6qmnsm6b9s1vmdjs79vjx9xgwzn5rwyjp6bvs8hg3zlmhpip"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("autoconf" ,autoconf)
@@ -511,7 +522,7 @@ Coq proof assistant.")
       (source (origin
                 (method git-fetch)
                 (uri (git-reference
-                      (url "git://github.com/uds-psl/autosubst.git")
+                      (url "git://github.com/uds-psl/autosubst")
                       (commit commit)))
                 (file-name (git-file-name name version))
                 (sha256
@@ -549,16 +560,16 @@ uses Ltac to synthesize the substitution operation.")
 (define-public coq-equations
   (package
     (name "coq-equations")
-    (version "1.2.1")
+    (version "1.2.3")
     (source (origin
               (method git-fetch)
               (uri (git-reference
-                    (url "https://github.com/mattam82/Coq-Equations.git")
-                    (commit (string-append "v" version "-8.10"))))
+                    (url "https://github.com/mattam82/Coq-Equations")
+                    (commit (string-append "v" version "-8.11"))))
               (file-name (git-file-name name version))
               (sha256
                (base32
-                "023q5dww3drw35dm9bi9p9d0wrj9k7vax7hfdsprf8l340pb4s0k"))))
+                "1srxz1rws8jsh7402g2x2vcqgjbbsr64dxxj5d2zs48pmhb20csf"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("ocaml"  ,ocaml)
@@ -589,7 +600,7 @@ kernel.")
 (define-public coq-stdpp
   (package
     (name "coq-stdpp")
-    (version "1.2.1")
+    (version "1.4.0")
     (synopsis "Alternative Coq standard library std++")
     (source (origin
               (method git-fetch)
@@ -599,7 +610,7 @@ kernel.")
               (file-name (git-file-name name version))
               (sha256
                (base32
-                "1lczybg1jq9drbi8nzrlb0k199x4n07aawjwfzrl3qqc0w8kmvdz"))))
+                "1m6c7ibwc99jd4cv14v3r327spnfvdf3x2mnq51f9rz99rffk68r"))))
     (build-system gnu-build-system)
     (inputs
      `(("coq" ,coq)))