gnu/packages/coq.scm

   1 ;;; GNU Guix --- Functional package management for GNU
   2 ;;; Copyright © 2018 Julien Lepiller <julien@lepiller.eu>
   3 ;;;
   4 ;;; This file is part of GNU Guix.
   5 ;;;
   6 ;;; GNU Guix is free software; you can redistribute it and/or modify it
   7 ;;; under the terms of the GNU General Public License as published by
   8 ;;; the Free Software Foundation; either version 3 of the License, or (at
   9 ;;; your option) any later version.
  10 ;;;
  11 ;;; GNU Guix is distributed in the hope that it will be useful, but
  12 ;;; WITHOUT ANY WARRANTY; without even the implied warranty of
  13 ;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  14 ;;; GNU General Public License for more details.
  15 ;;;
  16 ;;; You should have received a copy of the GNU General Public License
  17 ;;; along with GNU Guix.  If not, see <http://www.gnu.org/licenses/>.
  18
  19 (define-module (gnu packages coq)
  20   #:use-module (gnu packages)
  21   #:use-module (gnu packages base)
  22   #:use-module (gnu packages bison)
  23   #:use-module (gnu packages boost)
  24   #:use-module (gnu packages emacs)
  25   #:use-module (gnu packages flex)
  26   #:use-module (gnu packages multiprecision)
  27   #:use-module (gnu packages ocaml)
  28   #:use-module (gnu packages perl)
  29   #:use-module (gnu packages python)
  30   #:use-module (gnu packages texinfo)
  31   #:use-module (guix build-system gnu)
  32   #:use-module (guix build-system ocaml)
  33   #:use-module (guix download)
  34   #:use-module ((guix licenses) #:prefix license:)
  35   #:use-module (guix packages)
  36   #:use-module (guix utils)
  37   #:use-module ((srfi srfi-1) #:hide (zip)))
  38
  39 (define-public coq
  40   (package
  41     (name "coq")
  42     (version "8.8.2")
  43     (source (origin
  44               (method url-fetch)
  45               (uri (string-append "https://github.com/coq/coq/archive/V"
  46                                   version ".tar.gz"))
  47               (file-name (string-append name "-" version ".tar.gz"))
  48               (sha256
  49                (base32
  50                 "0i2hs0i6rp27cy8zd0mx7jscqw5cx2y0diw0pxgij66s3yr47y7r"))))
  51     (native-search-paths
  52      (list (search-path-specification
  53             (variable "COQPATH")
  54             (files (list "lib/coq/user-contrib")))))
  55     (build-system ocaml-build-system)
  56     (inputs
  57      `(("lablgtk" ,lablgtk)
  58        ("python" ,python-2)
  59        ("camlp5" ,camlp5)
  60        ("ocaml-num" ,ocaml-num)))
  61     (arguments
  62      `(#:phases
  63        (modify-phases %standard-phases
  64          (replace 'configure
  65            (lambda* (#:key outputs #:allow-other-keys)
  66              (let* ((out (assoc-ref outputs "out"))
  67                     (mandir (string-append out "/share/man"))
  68                     (browser "icecat -remote \"OpenURL(%s,new-tab)\""))
  69                (invoke "./configure"
  70                        "-prefix" out
  71                        "-mandir" mandir
  72                        "-browser" browser
  73                        "-coqide" "opt"))))
  74          (replace 'build
  75            (lambda _
  76              (invoke "make"
  77                      "-j" (number->string (parallel-job-count))
  78                      "world")))
  79          (delete 'check)
  80          (add-after 'install 'check
  81            (lambda _
  82              (with-directory-excursion "test-suite"
  83                ;; These two tests fail.
  84                ;; This one fails because the output is not formatted as expected.
  85                (delete-file-recursively "coq-makefile/timing")
  86                ;; This one fails because we didn't build coqtop.byte.
  87                (delete-file-recursively "coq-makefile/findlib-package")
  88                (invoke "make")))))))
  89     (home-page "https://coq.inria.fr")
  90     (synopsis "Proof assistant for higher-order logic")
  91     (description
  92      "Coq is a proof assistant for higher-order logic, which allows the
  93 development of computer programs consistent with their formal specification.
  94 It is developed using Objective Caml and Camlp5.")
  95     ;; The code is distributed under lgpl2.1.
  96     ;; Some of the documentation is distributed under opl1.0+.
  97     (license (list license:lgpl2.1 license:opl1.0+))))
  98
  99 (define-public proof-general
 100   (package
 101     (name "proof-general")
 102     (version "4.2")
 103     (source (origin
 104               (method url-fetch)
 105               (uri (string-append
 106                     "http://proofgeneral.inf.ed.ac.uk/releases/"
 107                     "ProofGeneral-" version ".tgz"))
 108               (sha256
 109                (base32
 110                 "09qb0myq66fw17v4ziz401ilsb5xlxz1nl2wsp69d0vrfy0bcrrm"))))
 111     (build-system gnu-build-system)
 112     (native-inputs
 113      `(("which" ,which)
 114        ("emacs" ,emacs-minimal)
 115        ("texinfo" ,texinfo)))
 116     (inputs
 117      `(("host-emacs" ,emacs)
 118        ("perl" ,perl)
 119        ("coq" ,coq)))
 120     (arguments
 121      `(#:tests? #f  ; no check target
 122        #:make-flags (list (string-append "PREFIX=" %output)
 123                           (string-append "DEST_PREFIX=" %output))
 124        #:modules ((guix build gnu-build-system)
 125                   (guix build utils)
 126                   (guix build emacs-utils))
 127        #:imported-modules (,@%gnu-build-system-modules
 128                            (guix build emacs-utils))
 129        #:phases
 130        (modify-phases %standard-phases
 131          (delete 'configure)
 132          (add-after 'unpack 'disable-byte-compile-error-on-warn
 133                     (lambda _
 134                       (substitute* "Makefile"
 135                         (("\\(setq byte-compile-error-on-warn t\\)")
 136                          "(setq byte-compile-error-on-warn nil)"))
 137                       #t))
 138          (add-after 'unpack 'patch-hardcoded-paths
 139                     (lambda* (#:key inputs outputs #:allow-other-keys)
 140                       (let ((out   (assoc-ref outputs "out"))
 141                             (coq   (assoc-ref inputs "coq"))
 142                             (emacs (assoc-ref inputs "host-emacs")))
 143                         (define (coq-prog name)
 144                           (string-append coq "/bin/" name))
 145                         (emacs-substitute-variables "coq/coq.el"
 146                           ("coq-prog-name"           (coq-prog "coqtop"))
 147                           ("coq-compiler"            (coq-prog "coqc"))
 148                           ("coq-dependency-analyzer" (coq-prog "coqdep")))
 149                         (substitute* "Makefile"
 150                           (("/sbin/install-info") "install-info"))
 151                         (substitute* "bin/proofgeneral"
 152                           (("^PGHOMEDEFAULT=.*" all)
 153                            (string-append all
 154                                           "PGHOME=$PGHOMEDEFAULT\n"
 155                                           "EMACS=" emacs "/bin/emacs")))
 156                         #t)))
 157          (add-after 'unpack 'clean
 158                     (lambda _
 159                       ;; Delete the pre-compiled elc files for Emacs 23.
 160                       (zero? (system* "make" "clean"))))
 161          (add-after 'install 'install-doc
 162                     (lambda* (#:key make-flags #:allow-other-keys)
 163                       ;; XXX FIXME avoid building/installing pdf files,
 164                       ;; due to unresolved errors building them.
 165                       (substitute* "Makefile"
 166                         ((" [^ ]*\\.pdf") ""))
 167                       (zero? (apply system* "make" "install-doc"
 168                                     make-flags)))))))
 169     (home-page "http://proofgeneral.inf.ed.ac.uk/")
 170     (synopsis "Generic front-end for proof assistants based on Emacs")
 171     (description
 172      "Proof General is a major mode to turn Emacs into an interactive proof
 173 assistant to write formal mathematical proofs using a variety of theorem
 174 provers.")
 175     (license license:gpl2+)))
 176
 177 (define-public coq-flocq
 178   (package
 179     (name "coq-flocq")
 180     (version "2.6.1")
 181     (source (origin
 182               (method url-fetch)
 183               ;; Use the ‘Latest version’ link for a stable URI across releases.
 184               (uri (string-append "https://gforge.inria.fr/frs/download.php/"
 185                                   "file/37454/flocq-" version ".tar.gz"))
 186               (sha256
 187                (base32
 188                 "06msp1fwpqv6p98a3i1nnkj7ch9rcq3rm916yxq8dxf51lkghrin"))))
 189     (build-system gnu-build-system)
 190     (native-inputs
 191      `(("ocaml" ,ocaml)
 192        ("which" ,which)
 193        ("coq" ,coq)))
 194     (arguments
 195      `(#:configure-flags
 196        (list (string-append "--libdir=" (assoc-ref %outputs "out")
 197                             "/lib/coq/user-contrib/Flocq"))
 198        #:phases
 199        (modify-phases %standard-phases
 200          (add-before 'configure 'fix-remake
 201            (lambda _
 202              (substitute* "remake.cpp"
 203                (("/bin/sh") (which "sh")))
 204              #t))
 205          (replace 'build
 206            (lambda _
 207              (invoke "./remake")
 208              #t))
 209          (replace 'check
 210            (lambda _
 211              (invoke "./remake" "check")
 212              #t))
 213              ;; TODO: requires coq-gappa and coq-interval.
 214              ;(invoke "./remake" "check-more")
 215          (replace 'install
 216            (lambda _
 217              (invoke "./remake" "install")
 218              #t)))))
 219     (home-page "http://flocq.gforge.inria.fr/")
 220     (synopsis "Floating-point formalization for the Coq system")
 221     (description "Flocq (Floats for Coq) is a floating-point formalization for
 222 the Coq system.  It provides a comprehensive library of theorems on a multi-radix
 223 multi-precision arithmetic.  It also supports efficient numerical computations
 224 inside Coq.")
 225     (license license:lgpl3+)))
 226
 227 (define-public coq-gappa
 228   (package
 229     (name "coq-gappa")
 230     (version "1.3.2")
 231     (source (origin
 232               (method url-fetch)
 233               (uri (string-append "https://gforge.inria.fr/frs/download.php/file/36397/gappa-"
 234                                   version ".tar.gz"))
 235               (sha256
 236                (base32
 237                 "19kg2zldaqs4smy7bv9hp650sqg46xbx1ss7jnyagpxdscwn9apd"))))
 238     (build-system gnu-build-system)
 239     (native-inputs
 240      `(("ocaml" ,ocaml)
 241        ("which" ,which)
 242        ("coq" ,coq)
 243        ("bison" ,bison)
 244        ("flex" ,flex)))
 245     (inputs
 246      `(("gmp" ,gmp)
 247        ("mpfr" ,mpfr)
 248        ("boost" ,boost)))
 249     (arguments
 250      `(#:configure-flags
 251        (list (string-append "--libdir=" (assoc-ref %outputs "out")
 252                             "/lib/coq/user-contrib/Gappa"))
 253        #:phases
 254        (modify-phases %standard-phases
 255          (add-before 'configure 'fix-remake
 256            (lambda _
 257              (substitute* "remake.cpp"
 258                (("/bin/sh") (which "sh")))))
 259          (replace 'build
 260            (lambda _
 261              (zero? (system* "./remake"))))
 262          (replace 'check
 263            (lambda _
 264              (zero? (system* "./remake" "check"))))
 265          (replace 'install
 266            (lambda _
 267              (zero? (system* "./remake" "install")))))))
 268     (home-page "http://gappa.gforge.inria.fr/")
 269     (synopsis "Verify and formally prove properties on numerical programs")
 270     (description "Gappa is a tool intended to help verifying and formally proving
 271 properties on numerical programs dealing with floating-point or fixed-point
 272 arithmetic.  It has been used to write robust floating-point filters for CGAL
 273 and it is used to certify elementary functions in CRlibm.  While Gappa is
 274 intended to be used directly, it can also act as a backend prover for the Why3
 275 software verification plateform or as an automatic tactic for the Coq proof
 276 assistant.")
 277     (license (list license:gpl2+ license:cecill))));either gpl2+ or cecill
 278
 279 (define-public coq-mathcomp
 280   (package
 281     (name "coq-mathcomp")
 282     (version "1.7.0")
 283     (source (origin
 284               (method url-fetch)
 285               (uri (string-append "https://github.com/math-comp/math-comp/archive/mathcomp-"
 286                                   version ".tar.gz"))
 287               (sha256
 288                (base32
 289                 "05zgyi4wmasi1rcyn5jq42w0bi9713q9m8dl1fdgl66nmacixh39"))))
 290     (build-system gnu-build-system)
 291     (native-inputs
 292      `(("ocaml" ,ocaml)
 293        ("which" ,which)
 294        ("coq" ,coq)))
 295     (arguments
 296      `(#:tests? #f; No need to test formally-verified programs :)
 297        #:phases
 298        (modify-phases %standard-phases
 299          (delete 'configure)
 300          (add-before 'build 'chdir
 301            (lambda _
 302              (chdir "mathcomp")))
 303          (replace 'install
 304            (lambda* (#:key outputs #:allow-other-keys)
 305              (setenv "COQLIB" (string-append (assoc-ref outputs "out") "/lib/coq/"))
 306              (zero? (system* "make" "-f" "Makefile.coq"
 307                              (string-append "COQLIB=" (assoc-ref outputs "out")
 308                                             "/lib/coq/")
 309                              "install")))))))
 310     (home-page "https://math-comp.github.io/math-comp/")
 311     (synopsis "Mathematical Components for Coq")
 312     (description "Mathematical Components for Coq has its origins in the formal
 313 proof of the Four Colour Theorem.  Since then it has grown to cover many areas
 314 of mathematics and has been used for large scale projects like the formal proof
 315 of the Odd Order Theorem.
 316
 317 The library is written using the Ssreflect proof language that is an integral
 318 part of the distribution.")
 319     (license license:cecill-b)))
 320
 321 (define-public coq-coquelicot
 322   (package
 323     (name "coq-coquelicot")
 324     (version "3.0.1")
 325     (source (origin
 326               (method url-fetch)
 327               (uri (string-append "https://gforge.inria.fr/frs/download.php/"
 328                                   "file/37045/coquelicot-" version ".tar.gz"))
 329               (sha256
 330                (base32
 331                 "0hsyhsy2lwqxxx2r8xgi5csmirss42lp9bkb9yy35mnya0w78c8r"))))
 332     (build-system gnu-build-system)
 333     (native-inputs
 334      `(("ocaml" ,ocaml)
 335        ("which" ,which)
 336        ("coq" ,coq)))
 337     (propagated-inputs
 338      `(("mathcomp" ,coq-mathcomp)))
 339     (arguments
 340      `(#:configure-flags
 341        (list (string-append "--libdir=" (assoc-ref %outputs "out")
 342                             "/lib/coq/user-contrib/Coquelicot"))
 343        #:phases
 344        (modify-phases %standard-phases
 345          (add-before 'configure 'fix-coq8.8
 346            (lambda _
 347              ; appcontext has been removed from coq 8.8
 348              (substitute* "theories/AutoDerive.v"
 349                (("appcontext") "context"))
 350              #t))
 351          (add-before 'configure 'fix-remake
 352            (lambda _
 353              (substitute* "remake.cpp"
 354                (("/bin/sh") (which "sh")))))
 355          (replace 'build
 356            (lambda _
 357              (zero? (system* "./remake"))))
 358          (replace 'check
 359            (lambda _
 360              (zero? (system* "./remake" "check"))))
 361          (replace 'install
 362            (lambda _
 363              (zero? (system* "./remake" "install")))))))
 364     (home-page "http://coquelicot.saclay.inria.fr/index.html")
 365     (synopsis "Coq library for Reals")
 366     (description "Coquelicot is an easier way of writing formulas and theorem
 367 statements, achieved by relying on total functions in place of dependent types
 368 for limits, derivatives, integrals, power series, and so on.  To help with the
 369 proof process, the library comes with a comprehensive set of theorems that cover
 370 not only these notions, but also some extensions such as parametric integrals,
 371 two-dimensional differentiability, asymptotic behaviors.  It also offers some
 372 automations for performing differentiability proofs.  Moreover, Coquelicot is a
 373 conservative extension of Coq's standard library and provides correspondence
 374 theorems between the two libraries.")
 375     (license license:lgpl3+)))
 376
 377 (define-public coq-bignums
 378   (package
 379     (name "coq-bignums")
 380     (version "8.8.0")
 381     (source (origin
 382               (method url-fetch)
 383               (uri (string-append "https://github.com/coq/bignums/archive/V"
 384                                   version ".tar.gz"))
 385               (file-name (string-append name "-" version ".tar.gz"))
 386               (sha256
 387                (base32
 388                 "08m1cmq4hkaf4sb0vy978c11rgzvds71cphyadmr2iirpr5815r0"))))
 389     (build-system gnu-build-system)
 390     (native-inputs
 391      `(("ocaml" ,ocaml)
 392        ("coq" ,coq)))
 393     (inputs
 394      `(("camlp5" ,camlp5)))
 395     (arguments
 396      `(#:tests? #f; No test target
 397        #:make-flags
 398        (list (string-append "COQLIBINSTALL=" (assoc-ref %outputs "out")
 399                             "/lib/coq/user-contrib"))
 400        #:phases
 401        (modify-phases %standard-phases
 402          (delete 'configure))))
 403     (home-page "https://github.com/coq/bignums")
 404     (synopsis "Coq library for arbitrary large numbers")
 405     (description "Bignums is a coq library of arbitrary large numbers.  It
 406 provides BigN, BigZ, BigQ that used to be part of Coq standard library.")
 407     (license license:lgpl2.1+)))
 408
 409 (define-public coq-interval
 410   (package
 411     (name "coq-interval")
 412     (version "3.3.0")
 413     (source (origin
 414               (method url-fetch)
 415               (uri (string-append "https://gforge.inria.fr/frs/download.php/"
 416                                   "file/37077/interval-" version ".tar.gz"))
 417               (sha256
 418                (base32
 419                 "08fdcf3hbwqphglvwprvqzgkg0qbimpyhnqsgv3gac4y1ap0f903"))))
 420     (build-system gnu-build-system)
 421     (native-inputs
 422      `(("ocaml" ,ocaml)
 423        ("which" ,which)
 424        ("coq" ,coq)))
 425     (propagated-inputs
 426      `(("flocq" ,coq-flocq)
 427        ("bignums" ,coq-bignums)
 428        ("coquelicot" ,coq-coquelicot)
 429        ("mathcomp" ,coq-mathcomp)))
 430     (arguments
 431      `(#:configure-flags
 432        (list (string-append "--libdir=" (assoc-ref %outputs "out")
 433                             "/lib/coq/user-contrib/Gappa"))
 434        #:phases
 435        (modify-phases %standard-phases
 436          (add-before 'configure 'fix-remake
 437            (lambda _
 438              (substitute* "remake.cpp"
 439                (("/bin/sh") (which "sh")))))
 440          (replace 'build
 441            (lambda _
 442              (zero? (system* "./remake"))))
 443          (replace 'check
 444            (lambda _
 445              (zero? (system* "./remake" "check"))))
 446          (replace 'install
 447            (lambda _
 448              (zero? (system* "./remake" "install")))))))
 449     (home-page "http://coq-interval.gforge.inria.fr/")
 450     (synopsis "Coq tactics to simplify inequality proofs")
 451     (description "Interval provides vernacular files containing tactics for
 452 simplifying the proofs of inequalities on expressions of real numbers for the
 453 Coq proof assistant.")
 454     (license license:cecill-c)))