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