diff options
Diffstat (limited to 'gnu/packages/coq.scm')
| -rw-r--r-- | gnu/packages/coq.scm | 371 |
1 files changed, 209 insertions, 162 deletions
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index 4ad172c6b0..b523ccb065 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -7,6 +7,7 @@ ;;; Copyright © 2020 raingloom <[email protected]> ;;; Copyright © 2020 Robin Green <[email protected]> ;;; Copyright © 2021 Xinglu Chen <[email protected]> +;;; Copyright © 2021 Simon Tournier <[email protected]> ;;; ;;; This file is part of GNU Guix. ;;; @@ -48,10 +49,10 @@ #:use-module (guix utils) #:use-module ((srfi srfi-1) #:hide (zip))) -(define-public coq +(define-public coq-core (package - (name "coq") - (version "8.13.2") + (name "coq-core") + (version "8.14.1") (source (origin (method git-fetch) @@ -61,24 +62,29 @@ (file-name (git-file-name name version)) (sha256 (base32 - "15r0cm3p9dlsxbg0lf05njjp1xi1y74vxvq6drxjykax67x95l8a")))) + "0q634fmrh5ivpxy7ammdiqdh9xp72ji2726vcz1bd55ln0d08z40")) + (patches (search-patches "coq-fix-envvars.patch")))) (native-search-paths (list (search-path-specification (variable "COQPATH") - (files (list "lib/coq/user-contrib"))) + (files (list "lib/ocaml/site-lib/coq/user-contrib" + "lib/coq/user-contrib"))) (search-path-specification - (variable "COQLIB") - (files (list "lib/ocaml/site-lib/coq")) + (variable "COQLIBPATH") + (files (list "lib/ocaml/site-lib/coq"))) + (search-path-specification + (variable "COQCORELIB") + (files (list "lib/ocaml/site-lib/coq-core")) (separator #f)))) (build-system dune-build-system) (inputs - `(("gmp" ,gmp) - ("ocaml-zarith" ,ocaml-zarith))) + (list gmp ocaml-zarith)) (native-inputs - `(("which" ,which))) + (list ocaml-ounit2 which)) (arguments - `(#:package "coq" - #:test-target "test-suite")) + `(#:package "coq-core" + #:test-target ".")) + (properties '((upstream-name . "coq"))) ; also for inherited packages (home-page "https://coq.inria.fr") (synopsis "Proof assistant for higher-order logic") (description @@ -89,6 +95,28 @@ 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-stdlib + (package + (inherit coq-core) + (name "coq-stdlib") + (arguments + `(#:package "coq-stdlib" + #:test-target ".")) + (inputs + (list coq-core gmp ocaml-zarith)) + (native-inputs '()))) + +(define-public coq + (package + (inherit coq-core) + (name "coq") + (arguments + `(#:package "coq" + #:test-target ".")) + (propagated-inputs + (list coq-core coq-stdlib)) + (native-inputs '()))) + (define-public coq-ide-server (package (inherit coq) @@ -97,9 +125,7 @@ It is developed using Objective Caml and Camlp5.") `(#:tests? #f #:package "coqide-server")) (inputs - `(("coq" ,coq) - ("gmp" ,gmp) - ("ocaml-zarith" ,ocaml-zarith))))) + (list coq gmp ocaml-zarith)))) (define-public coq-ide (package @@ -109,17 +135,16 @@ It is developed using Objective Caml and Camlp5.") `(#:tests? #f #:package "coqide")) (propagated-inputs - `(("coq" ,coq) - ("coq-ide-server" ,coq-ide-server))) + (list coq 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. - ;; Commit from 2021-06-07. - (let ((commit "bc86736abb728ec0d28abc90ef0adae21d29a66a") - (revision "0")) + ;; Commit from 2021-11-25. + (let ((commit "1b1083e86e0cddc20ff2f1a6b25c7a7eee2edf02") + (revision "1")) (package (name "proof-general") (version (git-version "4.4" revision commit)) @@ -131,65 +156,80 @@ It is developed using Objective Caml and Camlp5.") (file-name (git-file-name name version)) (sha256 (base32 - "00cga3n9nj2xa3ivb0fdkkdx3k11fp4879y188738631yd1x2lsa")))) + "1pnysczhscapgwmvf6ix7f31lf3hnh8h977bfll1m7jlxl9b9c0j")))) (build-system gnu-build-system) (native-inputs - `(("which" ,which) - ("emacs" ,emacs-minimal) + `(("emacs" ,emacs-minimal) ("texinfo" ,texinfo))) (inputs - `(("host-emacs" ,emacs) - ("perl" ,perl) - ("coq" ,coq))) + (list perl)) (arguments - `(#:tests? #f ; no check target - #:make-flags (list (string-append "PREFIX=" %output) - (string-append "DEST_PREFIX=" %output) - (string-append "ELISP_START=" %output - "/share/emacs/site-lisp/ProofGeneral")) - #:modules ((guix build gnu-build-system) - (guix build utils) - (guix build emacs-utils)) - #:imported-modules (,@%gnu-build-system-modules - (guix build emacs-utils)) - #:phases - (modify-phases %standard-phases - (delete 'configure) - (add-after 'unpack 'disable-byte-compile-error-on-warn - (lambda _ - (substitute* "Makefile" - (("\\(setq byte-compile-error-on-warn t\\)") - "(setq byte-compile-error-on-warn nil)")))) - (add-after 'unpack 'patch-hardcoded-paths - (lambda* (#:key inputs outputs #:allow-other-keys) - (let ((out (assoc-ref outputs "out")) - (coq (assoc-ref inputs "coq")) - (emacs (assoc-ref inputs "host-emacs"))) + (let ((base-directory "/share/emacs/site-lisp/ProofGeneral")) + `(#:tests? #f ; no check target + #:make-flags (list (string-append "PREFIX=" %output) + (string-append "EMACS=" (assoc-ref %build-inputs "emacs") + "/bin/emacs") + (string-append "DEST_PREFIX=" %output) + (string-append "ELISP=" %output ,base-directory) + (string-append "DEST_ELISP=" %output ,base-directory) + (string-append "ELISP_START=" %output ,base-directory)) + #:phases + (modify-phases %standard-phases + (delete 'configure) + (add-after 'unpack 'disable-byte-compile-error-on-warn + (lambda _ + (substitute* "Makefile" + (("\\(setq byte-compile-error-on-warn t\\)") + "(setq byte-compile-error-on-warn nil)")))) + (add-after 'unpack 'patch-hardcoded-paths + (lambda _ (substitute* "Makefile" - (("/sbin/install-info") "install-info"))))) - (add-after 'unpack 'clean - (lambda _ - ;; Delete the pre-compiled elc files for Emacs 23. - (invoke "make" "clean"))) - (add-after 'install 'install-doc - (lambda* (#:key make-flags #:allow-other-keys) - ;; XXX FIXME avoid building/installing pdf files, - ;; due to unresolved errors building them. - (substitute* "Makefile" - ((" [^ ]*\\.pdf") "")) - (apply invoke "make" "install-doc" make-flags)))))) + (("/sbin/install-info") "install-info")))) + (add-after 'unpack 'remove-which + (lambda _ + (substitute* "Makefile" + (("`which perl`") "perl") + (("`which bash`") "bash")))) + (add-after 'unpack 'clean + (lambda _ + ;; Delete the pre-compiled elc files for Emacs 23. + (invoke "make" "clean"))) + (add-after 'install 'install-doc + (lambda* (#:key make-flags #:allow-other-keys) + ;; XXX FIXME avoid building/installing pdf files, + ;; due to unresolved errors building them. + (substitute* "Makefile" + ((" [^ ]*\\.pdf") "")) + (apply invoke "make" "install-doc" make-flags))) + (add-after 'install 'allow-subfolders-autoloads + ;; Autoload cookies are present in sub-directories. A friendly + ;; wrapper proof-general.el around generic/proof-site.el is + ;; provided for execution on Emacs start-up. It serves two + ;; purposes: + ;; + ;; * Setting up the load path when byte-compiling pg. + ;; * Loading a minimal PG setup on startup (not all of Proof + ;; General, of course; mostly mode hooks and autoloads). + ;; + ;; The renaming to proof-general-autoloads.el is Guix + ;; specific. + (lambda* (#:key outputs #:allow-other-keys) + (let ((out (assoc-ref outputs "out"))) + (copy-file "proof-general.el" + (string-append out ,base-directory + "/proof-general-autoloads.el"))))))))) (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 assistant to write formal mathematical proofs using a variety of theorem provers.") - (license license:gpl2+)))) + (license license:gpl3+)))) (define-public coq-flocq (package (name "coq-flocq") - (version "3.3.1") + (version "3.4.2") (source (origin (method git-fetch) @@ -199,26 +239,16 @@ provers.") (file-name (git-file-name name version)) (sha256 (base32 - "01gdykva0lcw6y3dm8j0djxayb87szfg9vn0mxd6z3pks644misl")))) + "0j7vq7ifqcdaj2x881aha2rl51l2p72y1cn7r2xya0fjgsssfigy")))) (build-system gnu-build-system) (native-inputs - `(("autoconf" ,autoconf) - ("automake" ,automake) - ("ocaml" ,ocaml) - ("which" ,which) - ("coq" ,coq))) + (list autoconf automake ocaml which coq)) (arguments `(#:configure-flags - (list (string-append "--libdir=" (assoc-ref %outputs "out") - "/lib/coq/user-contrib/Flocq")) + (list (string-append "COQUSERCONTRIB=" (assoc-ref %outputs "out") + "/lib/coq/user-contrib")) #:phases (modify-phases %standard-phases - (add-after 'unpack 'remove-failing-examples - (lambda _ - (substitute* "Remakefile.in" - ;; Fails on a union error. - (("Double_rounding_odd_radix.v") "")) - #t)) (add-before 'configure 'fix-remake (lambda _ (substitute* "remake.cpp" @@ -235,7 +265,7 @@ provers.") (replace 'install (lambda _ (invoke "./remake" "install")))))) - (home-page "https://flocq.gforge.inria.fr/") + (home-page "https://flocq.gitlabpages.inria.fr") (synopsis "Floating-point formalization for the Coq system") (description "Flocq (Floats for Coq) is a floating-point formalization for the Coq system. It provides a comprehensive library of theorems on a multi-radix @@ -246,7 +276,7 @@ inside Coq.") (define-public coq-gappa (package (name "coq-gappa") - (version "1.4.6") + (version "1.5.0") (source (origin (method git-fetch) @@ -256,24 +286,21 @@ inside Coq.") (file-name (git-file-name name version)) (sha256 (base32 - "0492i0ksrz6dnc1d57jzsbmdlb9fp9hrh9ib5v8j0yqxpyi0x8f4")))) + "1ivh8xm1c8191rm4riamjzya2x6ls96qax5byir1fywf9hbxr1vg")))) (build-system gnu-build-system) (native-inputs - `(("autoconf" ,autoconf) - ("automake" ,automake) - ("ocaml" ,ocaml) - ("which" ,which) - ("coq" ,coq) - ("camlp5" ,camlp5) - ("bison" ,bison) - ("flex" ,flex))) + (list autoconf + automake + ocaml + which + coq + camlp5 + bison + flex)) (inputs - `(("gmp" ,gmp) - ("mpfr" ,mpfr) - ("ocaml-zarith" ,ocaml-zarith) - ("boost" ,boost))) + (list gmp mpfr ocaml-zarith boost)) (propagated-inputs - `(("coq-flocq" ,coq-flocq))) + (list coq-flocq)) (arguments `(#:configure-flags (list (string-append "COQUSERCONTRIB=" (assoc-ref %outputs "out") @@ -293,7 +320,7 @@ inside Coq.") ;; (lambda _ (invoke "./remake" "check"))) (replace 'install (lambda _ (invoke "./remake" "install")))))) - (home-page "https://gappa.gforge.inria.fr/") + (home-page "https://gappa.gitlabpages.inria.fr/") (synopsis "Verify and formally prove properties on numerical programs") (description "Gappa is a tool intended to help verifying and formally proving properties on numerical programs dealing with floating-point or fixed-point @@ -307,7 +334,7 @@ assistant.") (define-public coq-mathcomp (package (name "coq-mathcomp") - (version "1.12.0") + (version "1.13.0") (source (origin (method git-fetch) @@ -316,25 +343,20 @@ assistant.") (commit (string-append "mathcomp-" version)))) (file-name (git-file-name name version)) (sha256 - (base32 "12cgrmzlcjnp9kv9zxsk34fgf0qfa35jdb23cbf13kmg8dyfi3h5")))) + (base32 "0aj8hsdzzds5w0p1858s2b6k9zssjcxa6kgpi0q1nvaml4zfpkcc")))) (build-system gnu-build-system) (native-inputs - `(("ocaml" ,ocaml) - ("which" ,which) - ("coq" ,coq))) + (list ocaml which coq)) (arguments `(#:tests? #f ; No tests. + #:make-flags (list (string-append "COQLIBINSTALL=" + (assoc-ref %outputs "out") + "/lib/coq/user-contrib")) #:phases (modify-phases %standard-phases (delete 'configure) (add-before 'build 'chdir - (lambda _ (chdir "mathcomp") #t)) - (replace 'install - (lambda* (#:key outputs #:allow-other-keys) - (invoke "make" "-f" "Makefile.coq" - (string-append "COQLIB=" (assoc-ref outputs "out") - "/lib/coq/") - "install")))))) + (lambda _ (chdir "mathcomp") #t))))) (home-page "https://math-comp.github.io/") (synopsis "Mathematical Components for Coq") (description "Mathematical Components for Coq has its origins in the formal @@ -349,7 +371,7 @@ part of the distribution.") (define-public coq-coquelicot (package (name "coq-coquelicot") - (version "3.1.0") + (version "3.2.0") (source (origin (method git-fetch) @@ -359,20 +381,16 @@ part of the distribution.") (file-name (git-file-name name version)) (sha256 (base32 - "0mz3pxan1237fr5fi79c66y7b9z7bmi0sc45kwrmkczsjm5462jm")))) + "146s5y2xsc7wb43m1pq1n4p14hw99gqbzx0ic3a4naxq16v7cv4w")))) (build-system gnu-build-system) (native-inputs - `(("autoconf" ,autoconf) - ("automake" ,automake) - ("ocaml" ,ocaml) - ("which" ,which) - ("coq" ,coq))) + (list autoconf automake ocaml which coq)) (propagated-inputs `(("mathcomp" ,coq-mathcomp))) (arguments `(#:configure-flags - (list (string-append "--libdir=" (assoc-ref %outputs "out") - "/lib/coq/user-contrib/Coquelicot")) + (list (string-append "COQUSERCONTRIB=" (assoc-ref %outputs "out") + "/lib/coq/user-contrib")) #:phases (modify-phases %standard-phases (add-before 'configure 'fix-remake @@ -402,7 +420,7 @@ theorems between the two libraries.") (define-public coq-bignums (package (name "coq-bignums") - (version "8.13.0") + (version "8.14.0") (source (origin (method git-fetch) (uri (git-reference @@ -411,14 +429,12 @@ theorems between the two libraries.") (file-name (git-file-name name version)) (sha256 (base32 - "1n66i7hd9222b2ks606mak7m4f0dgy02xgygjskmmav6h7g2sx7y")))) + "0jsgdvj0ddhkls32krprp34r64y1rb5mwxl34fgaxk2k4664yq06")))) (build-system gnu-build-system) (native-inputs - `(("ocaml" ,ocaml) - ("coq" ,coq))) + (list ocaml coq)) (inputs - `(("camlp5" ,camlp5) - ("ocaml-zarith" ,ocaml-zarith))) + (list camlp5 ocaml-zarith)) (arguments `(#:tests? #f ; No test target. #:make-flags @@ -436,7 +452,7 @@ provides BigN, BigZ, BigQ that used to be part of Coq standard library.") (define-public coq-interval (package (name "coq-interval") - (version "4.3.0") + (version "4.3.1") (source (origin (method git-fetch) @@ -446,14 +462,10 @@ provides BigN, BigZ, BigQ that used to be part of Coq standard library.") (file-name (git-file-name name version)) (sha256 (base32 - "1jqvd17czhliscf40idhnxgrha620039ilrdyfahn71dg2jmzqnm")))) + "0sr9psildc0sda07r2r47rfgyry49yklk38bg04yyvry5j5pryb6")))) (build-system gnu-build-system) (native-inputs - `(("autoconf" ,autoconf) - ("automake" ,automake) - ("ocaml" ,ocaml) - ("which" ,which) - ("coq" ,coq))) + (list autoconf automake ocaml which coq)) (propagated-inputs `(("flocq" ,coq-flocq) ("bignums" ,coq-bignums) @@ -477,7 +489,7 @@ provides BigN, BigZ, BigQ that used to be part of Coq standard library.") (lambda _ (invoke "./remake" "check"))) (replace 'install (lambda _ (invoke "./remake" "install")))))) - (home-page "http://coq-interval.gforge.inria.fr/") + (home-page "https://coqinterval.gitlabpages.inria.fr/") (synopsis "Coq tactics to simplify inequality proofs") (description "Interval provides vernacular files containing tactics for simplifying the proofs of inequalities on expressions of real numbers for the @@ -503,18 +515,14 @@ Coq proof assistant.") (build-system gnu-build-system) (arguments `(#:tests? #f + #:make-flags (list (string-append "COQLIBINSTALL=" + (assoc-ref %outputs "out") + "/lib/coq/user-contrib")) #:phases (modify-phases %standard-phases - (delete 'configure) - (replace 'install - (lambda* (#:key outputs #:allow-other-keys) - (setenv "COQLIB" (string-append (assoc-ref outputs "out") "/lib/coq/")) - (invoke "make" - (string-append "COQLIB=" (assoc-ref outputs "out") - "/lib/coq/") - "install")))))) + (delete 'configure)))) (native-inputs - `(("coq" ,coq))) + (list coq)) (home-page "https://www.ps.uni-saarland.de/autosubst/") (synopsis "Coq library for parallel de Bruijn substitutions") (description "Formalizing syntactic theories with variable binders is @@ -533,36 +541,31 @@ uses Ltac to synthesize the substitution operation.") (define-public coq-equations (package (name "coq-equations") - (version "1.2.4") + (version "1.3") (source (origin (method git-fetch) (uri (git-reference (url "https://github.com/mattam82/Coq-Equations") - (commit (string-append "v" version "-8.13")))) + (commit (string-append "v" version "-8.14")))) (file-name (git-file-name name version)) (sha256 (base32 - "0i014lshsdflzw6h0qxra9d2f0q82vffxv2f29awbb9ad0p4rq4q")))) + "19bj9nncd1r9g4273h5qx35gs3i4bw5z9bhjni24b413hyj55hkv")))) (build-system gnu-build-system) (native-inputs - `(("ocaml" ,ocaml) - ("coq" ,coq) - ("camlp5" ,camlp5))) + (list ocaml coq camlp5)) (inputs - `(("ocaml-zarith" ,ocaml-zarith))) + (list ocaml-zarith)) (arguments `(#:test-target "test-suite" + #:make-flags (list (string-append "COQLIBINSTALL=" + (assoc-ref %outputs "out") + "/lib/coq/user-contrib")) #:phases (modify-phases %standard-phases (replace 'configure (lambda* (#:key outputs #:allow-other-keys) - (invoke "sh" "./configure.sh"))) - (replace 'install - (lambda* (#:key outputs #:allow-other-keys) - (invoke "make" - (string-append "COQLIB=" (assoc-ref outputs "out") - "/lib/coq/") - "install")))))) + (invoke "sh" "./configure.sh")))))) (home-page "https://mattam82.github.io/Coq-Equations/") (synopsis "Function definition plugin for Coq") (description "Equations provides a notation for writing programs @@ -572,10 +575,57 @@ and accessibility, providing a definitional extension to the Coq kernel.") (license license:lgpl2.1))) +(define-public coq-semantics + (package + (name "coq-semantics") + (version "8.14.0") + (source + (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/coq-community/semantics") + (commit (string-append "v" version)))) + (modules '((guix build utils))) + (snippet + '(substitute* "Makefile.coq.local" + ;; Num was part of OCaml and now external + (("-libs nums") "-use-ocamlfind -pkg num -libs num"))) + (file-name (git-file-name name version)) + (sha256 + (base32 + "0ldrp86bfcjpzsb08p45sgs3aczjzr1gksy5dsf7pxapg05pc7ac")))) + (build-system gnu-build-system) + (native-inputs + (list coq ocaml ocamlbuild ocaml-findlib)) + (inputs + (list ocaml-num)) + (arguments + `(#:tests? #f ;included in Makefile + #:make-flags (list (string-append "COQLIBINSTALL=" + (assoc-ref %outputs "out") + "/lib/coq/user-contrib")) + #:phases + (modify-phases %standard-phases + (delete 'configure)))) + (home-page "https://github.com/coq-community/semantics") + (synopsis "Survey of semantics styles") + (description + "This package provides a survey of programming language semantics styles, +from natural semantics through structural operational, axiomatic, and +denotational semantics, for a miniature example of an imperative programming +language. Their encoding, the proofs of equivalence of different styles, +abstract interpretation, and the proof of soundess obtained from axiomatic +semantics or abstract interpretation is done in Coq. The tools can be run +inside Coq, thus making them available for proof by reflection. Code can also +be extracted and connected to a yacc-based parser, thanks to the use of a +functor parameterized by a module type of strings. A hand-written parser is +also provided in Coq, without associated proofs.") + (license license:expat))) + (define-public coq-stdpp (package (name "coq-stdpp") - (version "1.5.0") + (version "1.6.0") (synopsis "Alternative Coq standard library std++") (source (origin (method git-fetch) @@ -585,21 +635,18 @@ kernel.") (file-name (git-file-name name version)) (sha256 (base32 - "1ym0fy620imah89p8b6rii8clx2vmnwcrbwxl3630h24k42092nf")))) + "1l1w6srzydjg0h3f4krrfgvz455h56shyy2lbcnwdbzjkahibl7v")))) (build-system gnu-build-system) (inputs - `(("coq" ,coq))) + (list coq)) (arguments `(#:tests? #f ; Tests are executed during build phase. + #:make-flags (list (string-append "COQLIBINSTALL=" + (assoc-ref %outputs "out") + "/lib/coq/user-contrib")) #:phases (modify-phases %standard-phases - (delete 'configure) - (replace 'install - (lambda* (#:key outputs #:allow-other-keys) - (invoke "make" - (string-append "COQLIB=" (assoc-ref outputs "out") - "/lib/coq/") - "install")))))) + (delete 'configure)))) (description "This project contains an extended \"Standard Library\" for Coq called coq-std++. The key features are: @itemize |