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