diff options
Diffstat (limited to 'gnu/packages/coq.scm')
| -rw-r--r-- | gnu/packages/coq.scm | 446 |
1 files changed, 446 insertions, 0 deletions
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm new file mode 100644 index 0000000000..51dd5dedcf --- /dev/null +++ b/gnu/packages/coq.scm @@ -0,0 +1,446 @@ +;;; GNU Guix --- Functional package management for GNU +;;; Copyright © 2018 Julien Lepiller <julien@lepiller.eu> +;;; +;;; This file is part of GNU Guix. +;;; +;;; GNU Guix is free software; you can redistribute it and/or modify it +;;; under the terms of the GNU General Public License as published by +;;; the Free Software Foundation; either version 3 of the License, or (at +;;; your option) any later version. +;;; +;;; GNU Guix is distributed in the hope that it will be useful, but +;;; WITHOUT ANY WARRANTY; without even the implied warranty of +;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +;;; GNU General Public License for more details. +;;; +;;; You should have received a copy of the GNU General Public License +;;; along with GNU Guix. If not, see <http://www.gnu.org/licenses/>. + +(define-module (gnu packages coq) + #:use-module (gnu packages) + #:use-module (gnu packages base) + #:use-module (gnu packages bison) + #:use-module (gnu packages boost) + #:use-module (gnu packages emacs) + #:use-module (gnu packages flex) + #:use-module (gnu packages multiprecision) + #:use-module (gnu packages ocaml) + #:use-module (gnu packages perl) + #:use-module (gnu packages python) + #:use-module (gnu packages texinfo) + #:use-module (guix build-system gnu) + #:use-module (guix build-system ocaml) + #:use-module (guix download) + #:use-module ((guix licenses) #:prefix license:) + #:use-module (guix packages) + #:use-module (guix utils) + #:use-module ((srfi srfi-1) #:hide (zip))) + +(define-public coq + (package + (name "coq") + (version "8.8.2") + (source (origin + (method url-fetch) + (uri (string-append "https://github.com/coq/coq/archive/V" + version ".tar.gz")) + (file-name (string-append name "-" version ".tar.gz")) + (sha256 + (base32 + "0i2hs0i6rp27cy8zd0mx7jscqw5cx2y0diw0pxgij66s3yr47y7r")))) + (native-search-paths + (list (search-path-specification + (variable "COQPATH") + (files (list "lib/coq/user-contrib"))))) + (build-system ocaml-build-system) + (inputs + `(("lablgtk" ,lablgtk) + ("python" ,python-2) + ("camlp5" ,camlp5) + ("ocaml-num" ,ocaml-num))) + (arguments + `(#:phases + (modify-phases %standard-phases + (replace 'configure + (lambda* (#:key outputs #:allow-other-keys) + (let* ((out (assoc-ref outputs "out")) + (mandir (string-append out "/share/man")) + (browser "icecat -remote \"OpenURL(%s,new-tab)\"")) + (invoke "./configure" + "-prefix" out + "-mandir" mandir + "-browser" browser + "-coqide" "opt")))) + (replace 'build + (lambda _ + (invoke "make" + "-j" (number->string (parallel-job-count)) + "world"))) + (delete 'check) + (add-after 'install 'check + (lambda _ + (with-directory-excursion "test-suite" + ;; These two tests fail. + ;; This one fails because the output is not formatted as expected. + (delete-file-recursively "coq-makefile/timing") + ;; This one fails because we didn't build coqtop.byte. + (delete-file-recursively "coq-makefile/findlib-package") + (invoke "make"))))))) + (home-page "https://coq.inria.fr") + (synopsis "Proof assistant for higher-order logic") + (description + "Coq is a proof assistant for higher-order logic, which allows the +development of computer programs consistent with their formal specification. +It is developed using Objective Caml and Camlp5.") + ;; The code is distributed under lgpl2.1. + ;; Some of the documentation is distributed under opl1.0+. + (license (list license:lgpl2.1 license:opl1.0+)))) + +(define-public proof-general + (package + (name "proof-general") + (version "4.2") + (source (origin + (method url-fetch) + (uri (string-append + "http://proofgeneral.inf.ed.ac.uk/releases/" + "ProofGeneral-" version ".tgz")) + (sha256 + (base32 + "09qb0myq66fw17v4ziz401ilsb5xlxz1nl2wsp69d0vrfy0bcrrm")))) + (build-system gnu-build-system) + (native-inputs + `(("which" ,which) + ("emacs" ,emacs-minimal) + ("texinfo" ,texinfo))) + (inputs + `(("host-emacs" ,emacs) + ("perl" ,perl) + ("coq" ,coq))) + (arguments + `(#:tests? #f ; no check target + #:make-flags (list (string-append "PREFIX=" %output) + (string-append "DEST_PREFIX=" %output)) + #: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)")) + #t)) + (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"))) + (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" + (("^PGHOMEDEFAULT=.*" all) + (string-append all + "PGHOME=$PGHOMEDEFAULT\n" + "EMACS=" emacs "/bin/emacs"))) + #t))) + (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)))))) + (home-page "http://proofgeneral.inf.ed.ac.uk/") + (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+))) + +(define-public coq-flocq + (package + (name "coq-flocq") + (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/" + "file/37454/flocq-" version ".tar.gz")) + (sha256 + (base32 + "06msp1fwpqv6p98a3i1nnkj7ch9rcq3rm916yxq8dxf51lkghrin")))) + (build-system gnu-build-system) + (native-inputs + `(("ocaml" ,ocaml) + ("which" ,which) + ("coq" ,coq))) + (arguments + `(#:configure-flags + (list (string-append "--libdir=" (assoc-ref %outputs "out") + "/lib/coq/user-contrib/Flocq")) + #:phases + (modify-phases %standard-phases + (add-before 'configure 'fix-remake + (lambda _ + (substitute* "remake.cpp" + (("/bin/sh") (which "sh"))) + #t)) + (replace 'build + (lambda _ + (invoke "./remake") + #t)) + (replace 'check + (lambda _ + (invoke "./remake" "check") + #t)) + ;; TODO: requires coq-gappa and coq-interval. + ;(invoke "./remake" "check-more") + (replace 'install + (lambda _ + (invoke "./remake" "install") + #t))))) + (home-page "http://flocq.gforge.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 +multi-precision arithmetic. It also supports efficient numerical computations +inside Coq.") + (license license:lgpl3+))) + +(define-public coq-gappa + (package + (name "coq-gappa") + (version "1.3.2") + (source (origin + (method url-fetch) + (uri (string-append "https://gforge.inria.fr/frs/download.php/file/36397/gappa-" + version ".tar.gz")) + (sha256 + (base32 + "19kg2zldaqs4smy7bv9hp650sqg46xbx1ss7jnyagpxdscwn9apd")))) + (build-system gnu-build-system) + (native-inputs + `(("ocaml" ,ocaml) + ("which" ,which) + ("coq" ,coq) + ("bison" ,bison) + ("flex" ,flex))) + (inputs + `(("gmp" ,gmp) + ("mpfr" ,mpfr) + ("boost" ,boost))) + (arguments + `(#:configure-flags + (list (string-append "--libdir=" (assoc-ref %outputs "out") + "/lib/coq/user-contrib/Gappa")) + #:phases + (modify-phases %standard-phases + (add-before 'configure 'fix-remake + (lambda _ + (substitute* "remake.cpp" + (("/bin/sh") (which "sh"))) + #t)) + (replace 'build + (lambda _ (invoke "./remake"))) + (replace 'check + (lambda _ (invoke "./remake" "check"))) + (replace 'install + (lambda _ (invoke "./remake" "install")))))) + (home-page "http://gappa.gforge.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 +arithmetic. It has been used to write robust floating-point filters for CGAL +and it is used to certify elementary functions in CRlibm. While Gappa is +intended to be used directly, it can also act as a backend prover for the Why3 +software verification plateform or as an automatic tactic for the Coq proof +assistant.") + (license (list license:gpl2+ license:cecill))));either gpl2+ or cecill + +(define-public coq-mathcomp + (package + (name "coq-mathcomp") + (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 + "05zgyi4wmasi1rcyn5jq42w0bi9713q9m8dl1fdgl66nmacixh39")))) + (build-system gnu-build-system) + (native-inputs + `(("ocaml" ,ocaml) + ("which" ,which) + ("coq" ,coq))) + (arguments + `(#:tests? #f; No need to test formally-verified programs :) + #:phases + (modify-phases %standard-phases + (delete 'configure) + (add-before 'build 'chdir + (lambda _ (chdir "mathcomp") #t)) + (replace 'install + (lambda* (#:key outputs #:allow-other-keys) + (setenv "COQLIB" (string-append (assoc-ref outputs "out") "/lib/coq/")) + (invoke "make" "-f" "Makefile.coq" + (string-append "COQLIB=" (assoc-ref outputs "out") + "/lib/coq/") + "install")))))) + (home-page "https://math-comp.github.io/math-comp/") + (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 +of mathematics and has been used for large scale projects like the formal proof +of the Odd Order Theorem. + +The library is written using the Ssreflect proof language that is an integral +part of the distribution.") + (license license:cecill-b))) + +(define-public coq-coquelicot + (package + (name "coq-coquelicot") + (version "3.0.1") + (source (origin + (method url-fetch) + (uri (string-append "https://gforge.inria.fr/frs/download.php/" + "file/37045/coquelicot-" version ".tar.gz")) + (sha256 + (base32 + "0hsyhsy2lwqxxx2r8xgi5csmirss42lp9bkb9yy35mnya0w78c8r")))) + (build-system gnu-build-system) + (native-inputs + `(("ocaml" ,ocaml) + ("which" ,which) + ("coq" ,coq))) + (propagated-inputs + `(("mathcomp" ,coq-mathcomp))) + (arguments + `(#:configure-flags + (list (string-append "--libdir=" (assoc-ref %outputs "out") + "/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" + (("/bin/sh") (which "sh"))) + #t)) + (replace 'build + (lambda _ (invoke "./remake"))) + (replace 'check + (lambda _ (invoke "./remake" "check"))) + (replace 'install + (lambda _ (invoke "./remake" "install")))))) + (home-page "http://coquelicot.saclay.inria.fr/index.html") + (synopsis "Coq library for Reals") + (description "Coquelicot is an easier way of writing formulas and theorem +statements, achieved by relying on total functions in place of dependent types +for limits, derivatives, integrals, power series, and so on. To help with the +proof process, the library comes with a comprehensive set of theorems that cover +not only these notions, but also some extensions such as parametric integrals, +two-dimensional differentiability, asymptotic behaviors. It also offers some +automations for performing differentiability proofs. Moreover, Coquelicot is a +conservative extension of Coq's standard library and provides correspondence +theorems between the two libraries.") + (license license:lgpl3+))) + +(define-public coq-bignums + (package + (name "coq-bignums") + (version "8.8.0") + (source (origin + (method url-fetch) + (uri (string-append "https://github.com/coq/bignums/archive/V" + version ".tar.gz")) + (file-name (string-append name "-" version ".tar.gz")) + (sha256 + (base32 + "08m1cmq4hkaf4sb0vy978c11rgzvds71cphyadmr2iirpr5815r0")))) + (build-system gnu-build-system) + (native-inputs + `(("ocaml" ,ocaml) + ("coq" ,coq))) + (inputs + `(("camlp5" ,camlp5))) + (arguments + `(#:tests? #f; No test target + #: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/bignums") + (synopsis "Coq library for arbitrary large numbers") + (description "Bignums is a coq library of arbitrary large numbers. It +provides BigN, BigZ, BigQ that used to be part of Coq standard library.") + (license license:lgpl2.1+))) + +(define-public coq-interval + (package + (name "coq-interval") + (version "3.3.0") + (source (origin + (method url-fetch) + (uri (string-append "https://gforge.inria.fr/frs/download.php/" + "file/37077/interval-" version ".tar.gz")) + (sha256 + (base32 + "08fdcf3hbwqphglvwprvqzgkg0qbimpyhnqsgv3gac4y1ap0f903")))) + (build-system gnu-build-system) + (native-inputs + `(("ocaml" ,ocaml) + ("which" ,which) + ("coq" ,coq))) + (propagated-inputs + `(("flocq" ,coq-flocq) + ("bignums" ,coq-bignums) + ("coquelicot" ,coq-coquelicot) + ("mathcomp" ,coq-mathcomp))) + (arguments + `(#:configure-flags + (list (string-append "--libdir=" (assoc-ref %outputs "out") + "/lib/coq/user-contrib/Gappa")) + #:phases + (modify-phases %standard-phases + (add-before 'configure 'fix-remake + (lambda _ + (substitute* "remake.cpp" + (("/bin/sh") (which "sh"))) + #t)) + (replace 'build + (lambda _ (invoke "./remake"))) + (replace 'check + (lambda _ (invoke "./remake" "check"))) + (replace 'install + (lambda _ (invoke "./remake" "install")))))) + (home-page "http://coq-interval.gforge.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 +Coq proof assistant.") + (license license:cecill-c))) |