gnu/packages/coq.scm

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