diff options
Diffstat (limited to 'gnu/packages/coq.scm')
| -rw-r--r-- | gnu/packages/coq.scm | 60 |
1 files changed, 36 insertions, 24 deletions
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index 166e66c09e..e57e40c2ad 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -4,6 +4,8 @@ ;;; 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. ;;; @@ -33,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) @@ -46,7 +49,7 @@ (define-public coq (package (name "coq") - (version "8.10.2") + (version "8.11.2") (source (origin (method git-fetch) @@ -56,7 +59,7 @@ (file-name (git-file-name name version)) (sha256 (base32 - "0ji2rzd70b3hcwfw97qk7rv3m2977ylqnq82l1555dp3njr8nm3q")))) + "1gia82dkmzqspw2w3s4gjyh39ghbmw4i41i4hyzc91g7mza17nbz")))) (native-search-paths (list (search-path-specification (variable "COQPATH") @@ -69,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 @@ -96,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) @@ -117,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") @@ -207,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) @@ -217,7 +229,7 @@ provers.") (file-name (git-file-name name version)) (sha256 (base32 - "15bi36x7zj0glsb3s2gwqd4wswhfzh36rbp7imbyff53a7nna95l")))) + "01gdykva0lcw6y3dm8j0djxayb87szfg9vn0mxd6z3pks644misl")))) (build-system gnu-build-system) (native-inputs `(("autoconf" ,autoconf) @@ -264,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) @@ -274,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) @@ -324,7 +336,7 @@ assistant.") (define-public coq-mathcomp (package (name "coq-mathcomp") - (version "1.10.0") + (version "1.11.0") (source (origin (method git-fetch) @@ -333,7 +345,7 @@ assistant.") (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) @@ -366,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) @@ -376,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) @@ -419,7 +431,7 @@ 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 @@ -428,7 +440,7 @@ theorems between the two libraries.") (file-name (git-file-name name version)) (sha256 (base32 - "0bpb4flckn4nqxbs3wjiznyx1k7r8k93qdigp3qwmikp2lxvcbw5")))) + "1xcd7c7qlvs0narfba6px34zq0mz8rffnhxw0kzhhg6i4iw115dp")))) (build-system gnu-build-system) (native-inputs `(("ocaml" ,ocaml) @@ -452,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) @@ -462,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) @@ -548,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") - (commit (string-append "v" version "-8.10")))) + (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) @@ -588,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) @@ -598,7 +610,7 @@ kernel.") (file-name (git-file-name name version)) (sha256 (base32 - "1lczybg1jq9drbi8nzrlb0k199x4n07aawjwfzrl3qqc0w8kmvdz")))) + "1m6c7ibwc99jd4cv14v3r327spnfvdf3x2mnq51f9rz99rffk68r")))) (build-system gnu-build-system) (inputs `(("coq" ,coq))) |