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