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              (invoke "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              (apply invoke "make" "install-doc" make-flags))))))
 168     (home-page "http://proofgeneral.inf.ed.ac.uk/")
 169     (synopsis "Generic front-end for proof assistants based on Emacs")
 170     (description
 171      "Proof General is a major mode to turn Emacs into an interactive proof
 172 assistant to write formal mathematical proofs using a variety of theorem
 173 provers.")
 174     (license license:gpl2+)))
 175
 176 (define-public coq-flocq
 177   (package
 178     (name "coq-flocq")
 179     (version "2.6.1")
 180     (source (origin
 181               (method url-fetch)
 182               ;; Use the ‘Latest version’ link for a stable URI across releases.
 183               (uri (string-append "https://gforge.inria.fr/frs/download.php/"
 184                                   "file/37454/flocq-" version ".tar.gz"))
 185               (sha256
 186                (base32
 187                 "06msp1fwpqv6p98a3i1nnkj7ch9rcq3rm916yxq8dxf51lkghrin"))))
 188     (build-system gnu-build-system)
 189     (native-inputs
 190      `(("ocaml" ,ocaml)
 191        ("which" ,which)
 192        ("coq" ,coq)))
 193     (arguments
 194      `(#:configure-flags
 195        (list (string-append "--libdir=" (assoc-ref %outputs "out")
 196                             "/lib/coq/user-contrib/Flocq"))
 197        #:phases
 198        (modify-phases %standard-phases
 199          (add-before 'configure 'fix-remake
 200            (lambda _
 201              (substitute* "remake.cpp"
 202                (("/bin/sh") (which "sh")))
 203              #t))
 204          (replace 'build
 205            (lambda _
 206              (invoke "./remake")
 207              #t))
 208          (replace 'check
 209            (lambda _
 210              (invoke "./remake" "check")
 211              #t))
 212              ;; TODO: requires coq-gappa and coq-interval.
 213              ;(invoke "./remake" "check-more")
 214          (replace 'install
 215            (lambda _
 216              (invoke "./remake" "install")
 217              #t)))))
 218     (home-page "http://flocq.gforge.inria.fr/")
 219     (synopsis "Floating-point formalization for the Coq system")
 220     (description "Flocq (Floats for Coq) is a floating-point formalization for
 221 the Coq system.  It provides a comprehensive library of theorems on a multi-radix
 222 multi-precision arithmetic.  It also supports efficient numerical computations
 223 inside Coq.")
 224     (license license:lgpl3+)))
 225
 226 (define-public coq-gappa
 227   (package
 228     (name "coq-gappa")
 229     (version "1.3.2")
 230     (source (origin
 231               (method url-fetch)
 232               (uri (string-append "https://gforge.inria.fr/frs/download.php/file/36397/gappa-"
 233                                   version ".tar.gz"))
 234               (sha256
 235                (base32
 236                 "19kg2zldaqs4smy7bv9hp650sqg46xbx1ss7jnyagpxdscwn9apd"))))
 237     (build-system gnu-build-system)
 238     (native-inputs
 239      `(("ocaml" ,ocaml)
 240        ("which" ,which)
 241        ("coq" ,coq)
 242        ("bison" ,bison)
 243        ("flex" ,flex)))
 244     (inputs
 245      `(("gmp" ,gmp)
 246        ("mpfr" ,mpfr)
 247        ("boost" ,boost)))
 248     (arguments
 249      `(#:configure-flags
 250        (list (string-append "--libdir=" (assoc-ref %outputs "out")
 251                             "/lib/coq/user-contrib/Gappa"))
 252        #:phases
 253        (modify-phases %standard-phases
 254          (add-before 'configure 'fix-remake
 255            (lambda _
 256              (substitute* "remake.cpp"
 257                (("/bin/sh") (which "sh")))
 258              #t))
 259          (replace 'build
 260            (lambda _ (invoke "./remake")))
 261          (replace 'check
 262            (lambda _ (invoke "./remake" "check")))
 263          (replace 'install
 264            (lambda _ (invoke "./remake" "install"))))))
 265     (home-page "http://gappa.gforge.inria.fr/")
 266     (synopsis "Verify and formally prove properties on numerical programs")
 267     (description "Gappa is a tool intended to help verifying and formally proving
 268 properties on numerical programs dealing with floating-point or fixed-point
 269 arithmetic.  It has been used to write robust floating-point filters for CGAL
 270 and it is used to certify elementary functions in CRlibm.  While Gappa is
 271 intended to be used directly, it can also act as a backend prover for the Why3
 272 software verification plateform or as an automatic tactic for the Coq proof
 273 assistant.")
 274     (license (list license:gpl2+ license:cecill))));either gpl2+ or cecill
 275
 276 (define-public coq-mathcomp
 277   (package
 278     (name "coq-mathcomp")
 279     (version "1.7.0")
 280     (source (origin
 281               (method url-fetch)
 282               (uri (string-append "https://github.com/math-comp/math-comp/archive/mathcomp-"
 283                                   version ".tar.gz"))
 284               (sha256
 285                (base32
 286                 "05zgyi4wmasi1rcyn5jq42w0bi9713q9m8dl1fdgl66nmacixh39"))))
 287     (build-system gnu-build-system)
 288     (native-inputs
 289      `(("ocaml" ,ocaml)
 290        ("which" ,which)
 291        ("coq" ,coq)))
 292     (arguments
 293      `(#:tests? #f; No need to test formally-verified programs :)
 294        #:phases
 295        (modify-phases %standard-phases
 296          (delete 'configure)
 297          (add-before 'build 'chdir
 298            (lambda _ (chdir "mathcomp") #t))
 299          (replace 'install
 300            (lambda* (#:key outputs #:allow-other-keys)
 301              (setenv "COQLIB" (string-append (assoc-ref outputs "out") "/lib/coq/"))
 302              (invoke "make" "-f" "Makefile.coq"
 303                      (string-append "COQLIB=" (assoc-ref outputs "out")
 304                                     "/lib/coq/")
 305                      "install"))))))
 306     (home-page "https://math-comp.github.io/math-comp/")
 307     (synopsis "Mathematical Components for Coq")
 308     (description "Mathematical Components for Coq has its origins in the formal
 309 proof of the Four Colour Theorem.  Since then it has grown to cover many areas
 310 of mathematics and has been used for large scale projects like the formal proof
 311 of the Odd Order Theorem.
 312
 313 The library is written using the Ssreflect proof language that is an integral
 314 part of the distribution.")
 315     (license license:cecill-b)))
 316
 317 (define-public coq-coquelicot
 318   (package
 319     (name "coq-coquelicot")
 320     (version "3.0.1")
 321     (source (origin
 322               (method url-fetch)
 323               (uri (string-append "https://gforge.inria.fr/frs/download.php/"
 324                                   "file/37045/coquelicot-" version ".tar.gz"))
 325               (sha256
 326                (base32
 327                 "0hsyhsy2lwqxxx2r8xgi5csmirss42lp9bkb9yy35mnya0w78c8r"))))
 328     (build-system gnu-build-system)
 329     (native-inputs
 330      `(("ocaml" ,ocaml)
 331        ("which" ,which)
 332        ("coq" ,coq)))
 333     (propagated-inputs
 334      `(("mathcomp" ,coq-mathcomp)))
 335     (arguments
 336      `(#:configure-flags
 337        (list (string-append "--libdir=" (assoc-ref %outputs "out")
 338                             "/lib/coq/user-contrib/Coquelicot"))
 339        #:phases
 340        (modify-phases %standard-phases
 341          (add-before 'configure 'fix-coq8.8
 342            (lambda _
 343              ; appcontext has been removed from coq 8.8
 344              (substitute* "theories/AutoDerive.v"
 345                (("appcontext") "context"))
 346              #t))
 347          (add-before 'configure 'fix-remake
 348            (lambda _
 349              (substitute* "remake.cpp"
 350                (("/bin/sh") (which "sh")))
 351              #t))
 352          (replace 'build
 353            (lambda _ (invoke "./remake")))
 354          (replace 'check
 355            (lambda _ (invoke "./remake" "check")))
 356          (replace 'install
 357            (lambda _ (invoke "./remake" "install"))))))
 358     (home-page "http://coquelicot.saclay.inria.fr/index.html")
 359     (synopsis "Coq library for Reals")
 360     (description "Coquelicot is an easier way of writing formulas and theorem
 361 statements, achieved by relying on total functions in place of dependent types
 362 for limits, derivatives, integrals, power series, and so on.  To help with the
 363 proof process, the library comes with a comprehensive set of theorems that cover
 364 not only these notions, but also some extensions such as parametric integrals,
 365 two-dimensional differentiability, asymptotic behaviors.  It also offers some
 366 automations for performing differentiability proofs.  Moreover, Coquelicot is a
 367 conservative extension of Coq's standard library and provides correspondence
 368 theorems between the two libraries.")
 369     (license license:lgpl3+)))
 370
 371 (define-public coq-bignums
 372   (package
 373     (name "coq-bignums")
 374     (version "8.8.0")
 375     (source (origin
 376               (method url-fetch)
 377               (uri (string-append "https://github.com/coq/bignums/archive/V"
 378                                   version ".tar.gz"))
 379               (file-name (string-append name "-" version ".tar.gz"))
 380               (sha256
 381                (base32
 382                 "08m1cmq4hkaf4sb0vy978c11rgzvds71cphyadmr2iirpr5815r0"))))
 383     (build-system gnu-build-system)
 384     (native-inputs
 385      `(("ocaml" ,ocaml)
 386        ("coq" ,coq)))
 387     (inputs
 388      `(("camlp5" ,camlp5)))
 389     (arguments
 390      `(#:tests? #f; No test target
 391        #:make-flags
 392        (list (string-append "COQLIBINSTALL=" (assoc-ref %outputs "out")
 393                             "/lib/coq/user-contrib"))
 394        #:phases
 395        (modify-phases %standard-phases
 396          (delete 'configure))))
 397     (home-page "https://github.com/coq/bignums")
 398     (synopsis "Coq library for arbitrary large numbers")
 399     (description "Bignums is a coq library of arbitrary large numbers.  It
 400 provides BigN, BigZ, BigQ that used to be part of Coq standard library.")
 401     (license license:lgpl2.1+)))
 402
 403 (define-public coq-interval
 404   (package
 405     (name "coq-interval")
 406     (version "3.3.0")
 407     (source (origin
 408               (method url-fetch)
 409               (uri (string-append "https://gforge.inria.fr/frs/download.php/"
 410                                   "file/37077/interval-" version ".tar.gz"))
 411               (sha256
 412                (base32
 413                 "08fdcf3hbwqphglvwprvqzgkg0qbimpyhnqsgv3gac4y1ap0f903"))))
 414     (build-system gnu-build-system)
 415     (native-inputs
 416      `(("ocaml" ,ocaml)
 417        ("which" ,which)
 418        ("coq" ,coq)))
 419     (propagated-inputs
 420      `(("flocq" ,coq-flocq)
 421        ("bignums" ,coq-bignums)
 422        ("coquelicot" ,coq-coquelicot)
 423        ("mathcomp" ,coq-mathcomp)))
 424     (arguments
 425      `(#:configure-flags
 426        (list (string-append "--libdir=" (assoc-ref %outputs "out")
 427                             "/lib/coq/user-contrib/Gappa"))
 428        #:phases
 429        (modify-phases %standard-phases
 430          (add-before 'configure 'fix-remake
 431            (lambda _
 432              (substitute* "remake.cpp"
 433                (("/bin/sh") (which "sh")))
 434              #t))
 435          (replace 'build
 436            (lambda _ (invoke "./remake")))
 437          (replace 'check
 438            (lambda _ (invoke "./remake" "check")))
 439          (replace 'install
 440            (lambda _ (invoke "./remake" "install"))))))
 441     (home-page "http://coq-interval.gforge.inria.fr/")
 442     (synopsis "Coq tactics to simplify inequality proofs")
 443     (description "Interval provides vernacular files containing tactics for
 444 simplifying the proofs of inequalities on expressions of real numbers for the
 445 Coq proof assistant.")
 446     (license license:cecill-c)))