diff options
Diffstat (limited to 'gnu/packages/coq.scm')
| -rw-r--r-- | gnu/packages/coq.scm | 235 |
1 files changed, 141 insertions, 94 deletions
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index dccb9bea4c..a27ec53ecb 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -7,6 +7,7 @@ ;;; Copyright © 2020 raingloom <raingloom@riseup.net> ;;; Copyright © 2020 Robin Green <greenrd@greenrd.org> ;;; Copyright © 2021 Xinglu Chen <public@yoctocell.xyz> +;;; Copyright © 2021 Simon Tournier <zimon.toutoune@gmail.com> ;;; ;;; This file is part of GNU Guix. ;;; @@ -135,50 +136,65 @@ It is developed using Objective Caml and Camlp5.") "00cga3n9nj2xa3ivb0fdkkdx3k11fp4879y188738631yd1x2lsa")))) (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))) + `(("perl" ,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 '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" - (("/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)))))) + ((" [^ ]*\\.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 @@ -190,7 +206,7 @@ provers.") (define-public coq-flocq (package (name "coq-flocq") - (version "3.3.1") + (version "3.4.2") (source (origin (method git-fetch) @@ -200,7 +216,7 @@ provers.") (file-name (git-file-name name version)) (sha256 (base32 - "01gdykva0lcw6y3dm8j0djxayb87szfg9vn0mxd6z3pks644misl")))) + "0j7vq7ifqcdaj2x881aha2rl51l2p72y1cn7r2xya0fjgsssfigy")))) (build-system gnu-build-system) (native-inputs `(("autoconf" ,autoconf) @@ -210,16 +226,10 @@ provers.") ("coq" ,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" @@ -236,7 +246,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 @@ -247,7 +257,7 @@ inside Coq.") (define-public coq-gappa (package (name "coq-gappa") - (version "1.4.6") + (version "1.5.0") (source (origin (method git-fetch) @@ -257,7 +267,7 @@ inside Coq.") (file-name (git-file-name name version)) (sha256 (base32 - "0492i0ksrz6dnc1d57jzsbmdlb9fp9hrh9ib5v8j0yqxpyi0x8f4")))) + "1ivh8xm1c8191rm4riamjzya2x6ls96qax5byir1fywf9hbxr1vg")))) (build-system gnu-build-system) (native-inputs `(("autoconf" ,autoconf) @@ -294,7 +304,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 @@ -308,7 +318,7 @@ assistant.") (define-public coq-mathcomp (package (name "coq-mathcomp") - (version "1.12.0") + (version "1.13.0") (source (origin (method git-fetch) @@ -317,7 +327,7 @@ 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) @@ -325,17 +335,14 @@ assistant.") ("coq" ,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 @@ -350,7 +357,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) @@ -360,7 +367,7 @@ part of the distribution.") (file-name (git-file-name name version)) (sha256 (base32 - "0mz3pxan1237fr5fi79c66y7b9z7bmi0sc45kwrmkczsjm5462jm")))) + "146s5y2xsc7wb43m1pq1n4p14hw99gqbzx0ic3a4naxq16v7cv4w")))) (build-system gnu-build-system) (native-inputs `(("autoconf" ,autoconf) @@ -372,8 +379,8 @@ part of the distribution.") `(("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 @@ -437,7 +444,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) @@ -447,7 +454,7 @@ 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) @@ -478,7 +485,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 @@ -504,16 +511,12 @@ 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))) (home-page "https://www.ps.uni-saarland.de/autosubst/") @@ -553,17 +556,14 @@ uses Ltac to synthesize the substitution operation.") `(("ocaml-zarith" ,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 @@ -573,10 +573,60 @@ and accessibility, providing a definitional extension to the Coq kernel.") (license license:lgpl2.1))) +(define-public coq-semantics + (package + (name "coq-semantics") + (version "8.13.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 + "0m5si9dsv96z92gy4xaqz8mzyz8zp7j1sp542l0wzsp5xgyfpc7i")))) + (build-system gnu-build-system) + (native-inputs + `(("coq" ,coq) + ("ocaml" ,ocaml) + ("ocamlbuild" ,ocamlbuild) + ("ocaml-findlib" ,ocaml-findlib))) + (inputs + `(("ocaml-num" ,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) @@ -586,21 +636,18 @@ kernel.") (file-name (git-file-name name version)) (sha256 (base32 - "1ym0fy620imah89p8b6rii8clx2vmnwcrbwxl3630h24k42092nf")))) + "1l1w6srzydjg0h3f4krrfgvz455h56shyy2lbcnwdbzjkahibl7v")))) (build-system gnu-build-system) (inputs `(("coq" ,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 |