gnu/packages/coq.scm

   1 ;;; GNU Guix --- Functional package management for GNU
   2 ;;; Copyright © 2018 Julien Lepiller <julien@lepiller.eu>
   3 ;;; Copyright © 2018, 2019 Tobias Geerinckx-Rice <me@tobias.gr>
   4 ;;; Copyright © 2019 Dan Frumin <dfrumin@cs.ru.nl>
   5 ;;; Copyright © 2020 Brett Gilio <brettg@gnu.org>
   6 ;;; Copyright © 2020 Björn Höfling <bjoern.hoefling@bjoernhoefling.de>
   7 ;;; Copyright © 2020 raingloom <raingloom@riseup.net>
   8 ;;;
   9 ;;; This file is part of GNU Guix.
  10 ;;;
  11 ;;; GNU Guix is free software; you can redistribute it and/or modify it
  12 ;;; under the terms of the GNU General Public License as published by
  13 ;;; the Free Software Foundation; either version 3 of the License, or (at
  14 ;;; your option) any later version.
  15 ;;;
  16 ;;; GNU Guix is distributed in the hope that it will be useful, but
  17 ;;; WITHOUT ANY WARRANTY; without even the implied warranty of
  18 ;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  19 ;;; GNU General Public License for more details.
  20 ;;;
  21 ;;; You should have received a copy of the GNU General Public License
  22 ;;; along with GNU Guix.  If not, see <http://www.gnu.org/licenses/>.
  23
  24 (define-module (gnu packages coq)
  25   #:use-module (gnu packages)
  26   #:use-module (gnu packages autotools)
  27   #:use-module (gnu packages base)
  28   #:use-module (gnu packages bison)
  29   #:use-module (gnu packages boost)
  30   #:use-module (gnu packages emacs)
  31   #:use-module (gnu packages flex)
  32   #:use-module (gnu packages gawk)
  33   #:use-module (gnu packages multiprecision)
  34   #:use-module (gnu packages ocaml)
  35   #:use-module (gnu packages perl)
  36   #:use-module (gnu packages python)
  37   #:use-module (gnu packages texinfo)
  38   #:use-module (guix build-system gnu)
  39   #:use-module (guix build-system ocaml)
  40   #:use-module (guix download)
  41   #:use-module (guix git-download)
  42   #:use-module ((guix licenses) #:prefix license:)
  43   #:use-module (guix packages)
  44   #:use-module (guix utils)
  45   #:use-module ((srfi srfi-1) #:hide (zip)))
  46
  47 (define-public coq
  48   (package
  49     (name "coq")
  50     (version "8.10.2")
  51     (source
  52      (origin
  53        (method git-fetch)
  54        (uri (git-reference
  55              (url "https://github.com/coq/coq")
  56              (commit (string-append "V" version))))
  57        (file-name (git-file-name name version))
  58        (sha256
  59         (base32
  60          "0ji2rzd70b3hcwfw97qk7rv3m2977ylqnq82l1555dp3njr8nm3q"))))
  61     (native-search-paths
  62      (list (search-path-specification
  63             (variable "COQPATH")
  64             (files (list "lib/coq/user-contrib")))))
  65     (build-system ocaml-build-system)
  66     (outputs '("out" "ide"))
  67     (inputs
  68      `(("lablgtk" ,lablgtk3)
  69        ("python" ,python-2)
  70        ("camlp5" ,camlp5)
  71        ("ocaml-num" ,ocaml-num)))
  72     (native-inputs
  73      `(("ocaml-ounit" ,ocaml-ounit)))
  74     (arguments
  75      `(#:phases
  76        (modify-phases %standard-phases
  77          (add-after 'unpack 'make-git-checkout-writable
  78            (lambda _
  79              (for-each make-file-writable (find-files "."))
  80              #t))
  81          (replace 'configure
  82            (lambda* (#:key outputs #:allow-other-keys)
  83              (let* ((out (assoc-ref outputs "out"))
  84                     (mandir (string-append out "/share/man"))
  85                     (browser "icecat -remote \"OpenURL(%s,new-tab)\""))
  86                (invoke "./configure"
  87                        "-prefix" out
  88                        "-mandir" mandir
  89                        "-browser" browser
  90                        "-coqide" "opt"))))
  91          (replace 'build
  92            (lambda _
  93              (invoke "make"
  94                      "-j" (number->string (parallel-job-count))
  95                      "world")))
  96          (delete 'check)
  97          (add-after 'install 'remove-duplicate
  98            (lambda* (#:key outputs #:allow-other-keys)
  99              (let* ((out (assoc-ref outputs "out"))
 100                     (bin (string-append out "/bin"))
 101                     (coqtop (string-append bin "/coqtop"))
 102                     (coqidetop (string-append bin "/coqidetop"))
 103                     (coqtop.opt (string-append coqtop ".opt"))
 104                     (coqidetop.opt (string-append coqidetop ".opt")))
 105                ;; These files are exact copies without `.opt` extension.
 106                ;; Removing these saves 35 MiB in the resulting package.
 107                ;; Unfortunately, completely deleting them breaks coqide.
 108                (delete-file coqtop.opt)
 109                (delete-file coqidetop.opt)
 110                (symlink coqtop coqtop.opt)
 111                (symlink coqidetop coqidetop.opt))
 112              #t))
 113          (add-after 'install 'install-ide
 114            (lambda* (#:key outputs #:allow-other-keys)
 115              (let ((out (assoc-ref outputs "out"))
 116                    (ide (assoc-ref outputs "ide")))
 117                (mkdir-p (string-append ide "/bin"))
 118                (rename-file (string-append out "/bin/coqide")
 119                             (string-append ide "/bin/coqide")))
 120              #t))
 121          (add-after 'install 'check
 122            (lambda _
 123              (with-directory-excursion "test-suite"
 124                ;; These two tests fail.
 125                ;; Fails because the output is not formatted as expected.
 126                (delete-file-recursively "coq-makefile/timing")
 127                ;; Fails because we didn't build coqtop.byte.
 128                (delete-file-recursively "coq-makefile/findlib-package")
 129                (invoke "make")))))))
 130     (home-page "https://coq.inria.fr")
 131     (synopsis "Proof assistant for higher-order logic")
 132     (description
 133      "Coq is a proof assistant for higher-order logic, which allows the
 134 development of computer programs consistent with their formal specification.
 135 It is developed using Objective Caml and Camlp5.")
 136     ;; The source code is distributed under lgpl2.1.
 137     ;; Some of the documentation is distributed under opl1.0+.
 138     (license (list license:lgpl2.1 license:opl1.0+))))
 139
 140 (define-public proof-general
 141   (package
 142     (name "proof-general")
 143     (version "4.4")
 144     (source (origin
 145               (method git-fetch)
 146               (uri (git-reference
 147                     (url (string-append
 148                           "https://github.com/ProofGeneral/PG"))
 149                     (commit (string-append "v" version))))
 150               (file-name (git-file-name name version))
 151               (sha256
 152                (base32
 153                 "0bdfk91wf71z80mdfnl8hpinripndcjgdkz854zil6521r84nqk8"))))
 154     (build-system gnu-build-system)
 155     (native-inputs
 156      `(("which" ,which)
 157        ("emacs" ,emacs-minimal)
 158        ("texinfo" ,texinfo)))
 159     (inputs
 160      `(("host-emacs" ,emacs)
 161        ("perl" ,perl)
 162        ("coq" ,coq)))
 163     (arguments
 164      `(#:tests? #f  ; no check target
 165        #:make-flags (list (string-append "PREFIX=" %output)
 166                           (string-append "DEST_PREFIX=" %output))
 167        #:modules ((guix build gnu-build-system)
 168                   (guix build utils)
 169                   (guix build emacs-utils))
 170        #:imported-modules (,@%gnu-build-system-modules
 171                            (guix build emacs-utils))
 172        #:phases
 173        (modify-phases %standard-phases
 174          (delete 'configure)
 175          (add-after 'unpack 'disable-byte-compile-error-on-warn
 176                     (lambda _
 177                       (substitute* "Makefile"
 178                         (("\\(setq byte-compile-error-on-warn t\\)")
 179                          "(setq byte-compile-error-on-warn nil)"))
 180                       #t))
 181          (add-after 'unpack 'patch-hardcoded-paths
 182                     (lambda* (#:key inputs outputs #:allow-other-keys)
 183                       (let ((out   (assoc-ref outputs "out"))
 184                             (coq   (assoc-ref inputs "coq"))
 185                             (emacs (assoc-ref inputs "host-emacs")))
 186                         (define (coq-prog name)
 187                           (string-append coq "/bin/" name))
 188                         (substitute* "Makefile"
 189                           (("/sbin/install-info") "install-info"))
 190                         (substitute* "bin/proofgeneral"
 191                           (("^PGHOMEDEFAULT=.*" all)
 192                            (string-append all
 193                                           "PGHOME=$PGHOMEDEFAULT\n"
 194                                           "EMACS=" emacs "/bin/emacs")))
 195                         #t)))
 196          (add-after 'unpack 'clean
 197            (lambda _
 198              ;; Delete the pre-compiled elc files for Emacs 23.
 199              (invoke "make" "clean")))
 200          (add-after 'install 'install-doc
 201            (lambda* (#:key make-flags #:allow-other-keys)
 202              ;; XXX FIXME avoid building/installing pdf files,
 203              ;; due to unresolved errors building them.
 204              (substitute* "Makefile"
 205                ((" [^ ]*\\.pdf") ""))
 206              (apply invoke "make" "install-doc" make-flags))))))
 207     (home-page "https://proofgeneral.github.io/ ")
 208     (synopsis "Generic front-end for proof assistants based on Emacs")
 209     (description
 210      "Proof General is a major mode to turn Emacs into an interactive proof
 211 assistant to write formal mathematical proofs using a variety of theorem
 212 provers.")
 213     (license license:gpl2+)))
 214
 215 (define-public coq-flocq
 216   (package
 217     (name "coq-flocq")
 218     (version "3.2.0")
 219     (source
 220      (origin
 221        (method git-fetch)
 222        (uri (git-reference
 223              (url "https://gitlab.inria.fr/flocq/flocq.git")
 224              (commit (string-append "flocq-" version))))
 225        (file-name (git-file-name name version))
 226        (sha256
 227         (base32
 228          "15bi36x7zj0glsb3s2gwqd4wswhfzh36rbp7imbyff53a7nna95l"))))
 229     (build-system gnu-build-system)
 230     (native-inputs
 231      `(("autoconf" ,autoconf)
 232        ("automake" ,automake)
 233        ("ocaml" ,ocaml)
 234        ("which" ,which)
 235        ("coq" ,coq)))
 236     (arguments
 237      `(#:configure-flags
 238        (list (string-append "--libdir=" (assoc-ref %outputs "out")
 239                             "/lib/coq/user-contrib/Flocq"))
 240        #:phases
 241        (modify-phases %standard-phases
 242          (add-after 'unpack 'remove-failing-examples
 243            (lambda _
 244              (substitute* "Remakefile.in"
 245                ;; Fails on a union error.
 246                (("Double_rounding_odd_radix.v") ""))
 247              #t))
 248          (add-before 'configure 'fix-remake
 249            (lambda _
 250              (substitute* "remake.cpp"
 251                (("/bin/sh") (which "sh")))
 252              #t))
 253          (replace 'build
 254            (lambda _
 255              (invoke "./remake")))
 256          (replace 'check
 257            (lambda _
 258              (invoke "./remake" "check")))
 259              ;; TODO: requires coq-gappa and coq-interval.
 260              ;(invoke "./remake" "check-more")
 261          (replace 'install
 262            (lambda _
 263              (invoke "./remake" "install"))))))
 264     (home-page "https://flocq.gforge.inria.fr/")
 265     (synopsis "Floating-point formalization for the Coq system")
 266     (description "Flocq (Floats for Coq) is a floating-point formalization for
 267 the Coq system.  It provides a comprehensive library of theorems on a multi-radix
 268 multi-precision arithmetic.  It also supports efficient numerical computations
 269 inside Coq.")
 270     (license license:lgpl3+)))
 271
 272 (define-public coq-gappa
 273   (package
 274     (name "coq-gappa")
 275     (version "1.4.2")
 276     (source
 277      (origin
 278        (method git-fetch)
 279        (uri (git-reference
 280              (url "https://gitlab.inria.fr/gappa/coq.git")
 281              (commit (string-append "gappalib-coq-" version))))
 282        (file-name (git-file-name name version))
 283        (sha256
 284         (base32
 285          "0r7jwp5xssdfzivs2flp7mzrscqhgl63mryhhf1cvndpgzqwfk2f"))))
 286     (build-system gnu-build-system)
 287     (native-inputs
 288      `(("autoconf" ,autoconf)
 289        ("automake" ,automake)
 290        ("ocaml" ,ocaml)
 291        ("which" ,which)
 292        ("coq" ,coq)
 293        ("camlp5" ,camlp5)
 294        ("bison" ,bison)
 295        ("flex" ,flex)))
 296     (inputs
 297      `(("gmp" ,gmp)
 298        ("mpfr" ,mpfr)
 299        ("boost" ,boost)))
 300     (propagated-inputs
 301      `(("coq-flocq" ,coq-flocq)))
 302     (arguments
 303      `(#:configure-flags
 304        (list (string-append "--libdir=" (assoc-ref %outputs "out")
 305                             "/lib/coq/user-contrib/Gappa"))
 306        #:phases
 307        (modify-phases %standard-phases
 308          (add-before 'configure 'fix-remake
 309            (lambda _
 310              (substitute* "remake.cpp"
 311                (("/bin/sh") (which "sh")))
 312              #t))
 313          (replace 'build
 314            (lambda _ (invoke "./remake")))
 315          ;; FIXME: Figure out why failures occur, and re-enable check phase.
 316          (delete 'check)
 317          ;; (replace 'check
 318          ;;   (lambda _ (invoke "./remake" "check")))
 319          (replace 'install
 320            (lambda _ (invoke "./remake" "install"))))))
 321     (home-page "https://gappa.gforge.inria.fr/")
 322     (synopsis "Verify and formally prove properties on numerical programs")
 323     (description "Gappa is a tool intended to help verifying and formally proving
 324 properties on numerical programs dealing with floating-point or fixed-point
 325 arithmetic.  It has been used to write robust floating-point filters for CGAL
 326 and it is used to certify elementary functions in CRlibm.  While Gappa is
 327 intended to be used directly, it can also act as a backend prover for the Why3
 328 software verification plateform or as an automatic tactic for the Coq proof
 329 assistant.")
 330     (license (list license:gpl2+ license:cecill))));either gpl2+ or cecill
 331
 332 (define-public coq-mathcomp
 333   (package
 334     (name "coq-mathcomp")
 335     (version "1.10.0")
 336     (source
 337      (origin
 338        (method git-fetch)
 339        (uri (git-reference
 340              (url "https://github.com/math-comp/math-comp")
 341              (commit (string-append "mathcomp-" version))))
 342        (file-name (git-file-name name version))
 343        (sha256
 344         (base32 "1h5h1c2025r1ms5qryvwy6pikxmpmmjav6yl127xpzmqdi6w732d"))))
 345     (build-system gnu-build-system)
 346     (native-inputs
 347      `(("ocaml" ,ocaml)
 348        ("which" ,which)
 349        ("coq" ,coq)))
 350     (arguments
 351      `(#:tests? #f ; No tests.
 352        #:phases
 353        (modify-phases %standard-phases
 354          (delete 'configure)
 355          (add-before 'build 'chdir
 356            (lambda _ (chdir "mathcomp") #t))
 357          (replace 'install
 358            (lambda* (#:key outputs #:allow-other-keys)
 359              (invoke "make" "-f" "Makefile.coq"
 360                      (string-append "COQLIB=" (assoc-ref outputs "out")
 361                                     "/lib/coq/")
 362                      "install"))))))
 363     (home-page "https://math-comp.github.io/")
 364     (synopsis "Mathematical Components for Coq")
 365     (description "Mathematical Components for Coq has its origins in the formal
 366 proof of the Four Colour Theorem.  Since then it has grown to cover many areas
 367 of mathematics and has been used for large scale projects like the formal proof
 368 of the Odd Order Theorem.
 369
 370 The library is written using the Ssreflect proof language that is an integral
 371 part of the distribution.")
 372     (license license:cecill-b)))
 373
 374 (define-public coq-coquelicot
 375   (package
 376     (name "coq-coquelicot")
 377     (version "3.0.3")
 378     (source
 379      (origin
 380        (method git-fetch)
 381        (uri (git-reference
 382              (url "https://gitlab.inria.fr/coquelicot/coquelicot.git")
 383              (commit (string-append "coquelicot-" version))))
 384        (file-name (git-file-name name version))
 385        (sha256
 386         (base32
 387          "0m5wbr2s8lnf8b7cfwv15hyzsmbcaz6hgdn7aazcrkxnwr87vgkp"))))
 388     (build-system gnu-build-system)
 389     (native-inputs
 390      `(("autoconf" ,autoconf)
 391        ("automake" ,automake)
 392        ("ocaml" ,ocaml)
 393        ("which" ,which)
 394        ("coq" ,coq)))
 395     (propagated-inputs
 396      `(("mathcomp" ,coq-mathcomp)))
 397     (arguments
 398      `(#:configure-flags
 399        (list (string-append "--libdir=" (assoc-ref %outputs "out")
 400                             "/lib/coq/user-contrib/Coquelicot"))
 401        #:phases
 402        (modify-phases %standard-phases
 403          (add-before 'configure 'fix-remake
 404            (lambda _
 405              (substitute* "remake.cpp"
 406                (("/bin/sh") (which "sh")))
 407              #t))
 408          (replace 'build
 409            (lambda _ (invoke "./remake")))
 410          (replace 'check
 411            (lambda _ (invoke "./remake" "check")))
 412          (replace 'install
 413            (lambda _ (invoke "./remake" "install"))))))
 414     (home-page "http://coquelicot.saclay.inria.fr")
 415     (synopsis "Coq library for Reals")
 416     (description "Coquelicot is an easier way of writing formulas and theorem
 417 statements, achieved by relying on total functions in place of dependent types
 418 for limits, derivatives, integrals, power series, and so on.  To help with the
 419 proof process, the library comes with a comprehensive set of theorems that cover
 420 not only these notions, but also some extensions such as parametric integrals,
 421 two-dimensional differentiability, asymptotic behaviors.  It also offers some
 422 automations for performing differentiability proofs.  Moreover, Coquelicot is a
 423 conservative extension of Coq's standard library and provides correspondence
 424 theorems between the two libraries.")
 425     (license license:lgpl3+)))
 426
 427 (define-public coq-bignums
 428   (package
 429     (name "coq-bignums")
 430     (version "8.10.0")
 431     (source (origin
 432               (method git-fetch)
 433               (uri (git-reference
 434                      (url "https://github.com/coq/bignums")
 435                      (commit (string-append "V" version))))
 436               (file-name (git-file-name name version))
 437               (sha256
 438                (base32
 439                 "0bpb4flckn4nqxbs3wjiznyx1k7r8k93qdigp3qwmikp2lxvcbw5"))))
 440     (build-system gnu-build-system)
 441     (native-inputs
 442      `(("ocaml" ,ocaml)
 443        ("coq" ,coq)))
 444     (inputs
 445      `(("camlp5" ,camlp5)))
 446     (arguments
 447      `(#:tests? #f ; No test target.
 448        #:make-flags
 449        (list (string-append "COQLIBINSTALL=" (assoc-ref %outputs "out")
 450                             "/lib/coq/user-contrib"))
 451        #:phases
 452        (modify-phases %standard-phases
 453          (delete 'configure))))
 454     (home-page "https://github.com/coq/bignums")
 455     (synopsis "Coq library for arbitrary large numbers")
 456     (description "Bignums is a coq library of arbitrary large numbers.  It
 457 provides BigN, BigZ, BigQ that used to be part of Coq standard library.")
 458     (license license:lgpl2.1+)))
 459
 460 (define-public coq-interval
 461   (package
 462     (name "coq-interval")
 463     (version "3.4.1")
 464     (source
 465      (origin
 466        (method git-fetch)
 467        (uri (git-reference
 468              (url "https://gitlab.inria.fr/coqinterval/interval.git")
 469              (commit (string-append "interval-" version))))
 470        (file-name (git-file-name name version))
 471        (sha256
 472         (base32
 473          "03q3dfqi3r3f7aji5s06ig4aav9ajcwswwdzi5lrgr69z0m487k4"))))
 474     (build-system gnu-build-system)
 475     (native-inputs
 476      `(("autoconf" ,autoconf)
 477        ("automake" ,automake)
 478        ("ocaml" ,ocaml)
 479        ("which" ,which)
 480        ("coq" ,coq)))
 481     (propagated-inputs
 482      `(("flocq" ,coq-flocq)
 483        ("bignums" ,coq-bignums)
 484        ("coquelicot" ,coq-coquelicot)
 485        ("mathcomp" ,coq-mathcomp)))
 486     (arguments
 487      `(#:configure-flags
 488        (list (string-append "--libdir=" (assoc-ref %outputs "out")
 489                             "/lib/coq/user-contrib/Gappa"))
 490        #:phases
 491        (modify-phases %standard-phases
 492          (add-before 'configure 'fix-remake
 493            (lambda _
 494              (substitute* "remake.cpp"
 495                (("/bin/sh") (which "sh")))
 496              #t))
 497          (replace 'build
 498            (lambda _ (invoke "./remake")))
 499          (replace 'check
 500            (lambda _ (invoke "./remake" "check")))
 501          (replace 'install
 502            (lambda _ (invoke "./remake" "install"))))))
 503     (home-page "http://coq-interval.gforge.inria.fr/")
 504     (synopsis "Coq tactics to simplify inequality proofs")
 505     (description "Interval provides vernacular files containing tactics for
 506 simplifying the proofs of inequalities on expressions of real numbers for the
 507 Coq proof assistant.")
 508     (license license:cecill-c)))
 509
 510 (define-public coq-autosubst
 511   ;; Latest commit on that branch, where work on supporting coq 8.6 and
 512   ;; more recent versions of coq happen.
 513   (let ((branch "coq86-devel")
 514         (commit "fa6ef30664511ffa659cbcf3c962715cbee03572"))
 515     (package
 516       (name "coq-autosubst")
 517       (version (git-version "1" branch commit))
 518       (source (origin
 519                 (method git-fetch)
 520                 (uri (git-reference
 521                       (url "git://github.com/uds-psl/autosubst.git")
 522                       (commit commit)))
 523                 (file-name (git-file-name name version))
 524                 (sha256
 525                  (base32 "1cl0bp96bk6lplbl7n5c703vd3gvbs5mvf2qrf8q333kkqd7jqq4"))))
 526       (build-system gnu-build-system)
 527       (arguments
 528        `(#:tests? #f
 529          #:phases
 530          (modify-phases %standard-phases
 531            (delete 'configure)
 532            (replace 'install
 533              (lambda* (#:key outputs #:allow-other-keys)
 534                (setenv "COQLIB" (string-append (assoc-ref outputs "out") "/lib/coq/"))
 535                (invoke "make"
 536                        (string-append "COQLIB=" (assoc-ref outputs "out")
 537                                       "/lib/coq/")
 538                        "install"))))))
 539       (native-inputs
 540        `(("coq" ,coq)))
 541       (home-page "https://www.ps.uni-saarland.de/autosubst/")
 542       (synopsis "Coq library for parallel de Bruijn substitutions")
 543       (description "Formalizing syntactic theories with variable binders is
 544 not easy.  Autosubst is a library for the Coq proof assistant to
 545 automate this process.  Given an inductive definition of syntactic objects in
 546 de Bruijn representation augmented with binding annotations, Autosubst
 547 synthesizes the parallel substitution operation and automatically proves the
 548 basic lemmas about substitutions.  This library contains an automation
 549 tactic that solves equations involving terms and substitutions.  This makes the
 550 usage of substitution lemmas unnecessary.  The tactic is based on our current
 551 work on a decision procedure for the equational theory of an extension of the
 552 sigma-calculus by Abadi et al.  The library is completely written in Coq and
 553 uses Ltac to synthesize the substitution operation.")
 554       (license license:bsd-3))))
 555
 556 (define-public coq-equations
 557   (package
 558     (name "coq-equations")
 559     (version "1.2.1")
 560     (source (origin
 561               (method git-fetch)
 562               (uri (git-reference
 563                     (url "https://github.com/mattam82/Coq-Equations")
 564                     (commit (string-append "v" version "-8.10-2"))))
 565               (file-name (git-file-name name version))
 566               (sha256
 567                (base32
 568                 "0j3z4l5nrbyi9zbbyqkc6kassjanwld2188mwmrbqspaypm2ys68"))))
 569     (build-system gnu-build-system)
 570     (native-inputs
 571      `(("ocaml"  ,ocaml)
 572        ("coq"    ,coq)
 573        ("camlp5" ,camlp5)))
 574     (arguments
 575      `(#:test-target "test-suite"
 576        #:phases
 577        (modify-phases %standard-phases
 578          (replace 'configure
 579            (lambda* (#:key outputs #:allow-other-keys)
 580              (invoke "sh" "./configure.sh")))
 581          (replace 'install
 582            (lambda* (#:key outputs #:allow-other-keys)
 583              (invoke "make"
 584                      (string-append "COQLIB=" (assoc-ref outputs "out")
 585                                     "/lib/coq/")
 586                      "install"))))))
 587     (home-page "https://mattam82.github.io/Coq-Equations/")
 588     (synopsis "Function definition plugin for Coq")
 589     (description "Equations provides a notation for writing programs
 590 by dependent pattern-matching and (well-founded) recursion in Coq.  It
 591 compiles everything down to eliminators for inductive types, equality
 592 and accessibility, providing a definitional extension to the Coq
 593 kernel.")
 594     (license license:lgpl2.1)))
 595
 596 (define-public coq-stdpp
 597   (package
 598     (name "coq-stdpp")
 599     (version "1.4.0")
 600     (synopsis "Alternative Coq standard library std++")
 601     (source (origin
 602               (method git-fetch)
 603               (uri (git-reference
 604                     (url "https://gitlab.mpi-sws.org/iris/stdpp.git")
 605                     (commit (string-append "coq-stdpp-" version))))
 606               (file-name (git-file-name name version))
 607               (sha256
 608                (base32
 609                 "1m6c7ibwc99jd4cv14v3r327spnfvdf3x2mnq51f9rz99rffk68r"))))
 610     (build-system gnu-build-system)
 611     (inputs
 612      `(("coq" ,coq)))
 613     (arguments
 614      `(#:tests? #f ; Tests are executed during build phase.
 615        #:phases
 616        (modify-phases %standard-phases
 617          (delete 'configure)
 618          (replace 'install
 619            (lambda* (#:key outputs #:allow-other-keys)
 620              (invoke "make"
 621                      (string-append "COQLIB=" (assoc-ref outputs "out")
 622                                     "/lib/coq/")
 623                      "install"))))))
 624     (description "This project contains an extended \"Standard Library\" for
 625 Coq called coq-std++.  The key features are:
 626 @itemize
 627 @item Great number of definitions and lemmas for common data structures such
 628 as lists, finite maps, finite sets, and finite multisets.
 629
 630 @item Type classes for common notations (like ∅, ∪, and Haskell-style monad
 631 notations) so that these can be overloaded for different data structures.
 632
 633 @item It uses type classes to keep track of common properties of types, like
 634 it having decidable equality or being countable or finite.
 635
 636 @item Most data structures are represented in canonical ways so that Leibniz
 637 equality can be used as much as possible (for example, for maps we have m1 =
 638 m2 iff ∀ i, m1 !! i = m2 !! i).  On top of that, the library provides setoid
 639 instances for most types and operations.
 640
 641 @item Various tactics for common tasks, like an ssreflect inspired done tactic
 642 for finishing trivial goals, a simple breadth-first solver naive_solver, an
 643 equality simplifier simplify_eq, a solver solve_proper for proving
 644 compatibility of functions with respect to relations, and a solver set_solver
 645 for goals involving set operations.
 646
 647 @item The library is dependency- and axiom-free.
 648 @end itemize")
 649     (home-page "https://gitlab.mpi-sws.org/iris/stdpp")
 650     (license license:bsd-3)))