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