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>
10 ;;; This file is part of GNU Guix.
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.
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.
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/>.
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)))
57 (url "https://github.com/coq/coq")
58 (commit (string-append "V" version))))
59 (file-name (git-file-name name version))
62 "1gia82dkmzqspw2w3s4gjyh39ghbmw4i41i4hyzc91g7mza17nbz"))))
64 (list (search-path-specification
66 (files (list "lib/coq/user-contrib")))))
67 (build-system ocaml-build-system)
68 (outputs '("out" "ide"))
70 `(("lablgtk" ,lablgtk3)
73 ("ocaml-num" ,ocaml-num)))
75 `(("ocaml-ounit" ,ocaml-ounit)
80 (modify-phases %standard-phases
81 (add-after 'unpack 'make-git-checkout-writable
83 (for-each make-file-writable (find-files "."))
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)\""))
98 "-j" (number->string (parallel-job-count))
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))
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")))
125 (add-after 'install 'check
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")
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+))))
144 (define-public proof-general
146 (name "proof-general")
152 "https://github.com/ProofGeneral/PG"))
153 (commit (string-append "v" version))))
154 (file-name (git-file-name name version))
157 "0bdfk91wf71z80mdfnl8hpinripndcjgdkz854zil6521r84nqk8"))))
158 (build-system gnu-build-system)
161 ("emacs" ,emacs-minimal)
162 ("texinfo" ,texinfo)))
164 `(("host-emacs" ,emacs)
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)
173 (guix build emacs-utils))
174 #:imported-modules (,@%gnu-build-system-modules
175 (guix build emacs-utils))
177 (modify-phases %standard-phases
179 (add-after 'unpack 'disable-byte-compile-error-on-warn
181 (substitute* "Makefile"
182 (("\\(setq byte-compile-error-on-warn t\\)")
183 "(setq byte-compile-error-on-warn nil)"))
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)
197 "PGHOME=$PGHOMEDEFAULT\n"
198 "EMACS=" emacs "/bin/emacs")))
200 (add-after 'unpack 'clean
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")
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
217 (license license:gpl2+)))
219 (define-public coq-flocq
227 (url "https://gitlab.inria.fr/flocq/flocq.git")
228 (commit (string-append "flocq-" version))))
229 (file-name (git-file-name name version))
232 "01gdykva0lcw6y3dm8j0djxayb87szfg9vn0mxd6z3pks644misl"))))
233 (build-system gnu-build-system)
235 `(("autoconf" ,autoconf)
236 ("automake" ,automake)
242 (list (string-append "--libdir=" (assoc-ref %outputs "out")
243 "/lib/coq/user-contrib/Flocq"))
245 (modify-phases %standard-phases
246 (add-after 'unpack 'remove-failing-examples
248 (substitute* "Remakefile.in"
249 ;; Fails on a union error.
250 (("Double_rounding_odd_radix.v") ""))
252 (add-before 'configure 'fix-remake
254 (substitute* "remake.cpp"
255 (("/bin/sh") (which "sh")))
259 (invoke "./remake")))
262 (invoke "./remake" "check")))
263 ;; TODO: requires coq-gappa and coq-interval.
264 ;(invoke "./remake" "check-more")
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
274 (license license:lgpl3+)))
276 (define-public coq-gappa
284 (url "https://gitlab.inria.fr/gappa/coq.git")
285 (commit (string-append "gappalib-coq-" version))))
286 (file-name (git-file-name name version))
289 "0f3g3wjkvfkm961l4jpckhsqd43jnvm7f5qqk78qc32zh1fg339n"))))
290 (build-system gnu-build-system)
292 `(("autoconf" ,autoconf)
293 ("automake" ,automake)
305 `(("coq-flocq" ,coq-flocq)))
308 (list (string-append "--libdir=" (assoc-ref %outputs "out")
309 "/lib/coq/user-contrib/Gappa"))
311 (modify-phases %standard-phases
312 (add-before 'configure 'fix-remake
314 (substitute* "remake.cpp"
315 (("/bin/sh") (which "sh")))
318 (lambda _ (invoke "./remake")))
319 ;; FIXME: Figure out why failures occur, and re-enable check phase.
322 ;; (lambda _ (invoke "./remake" "check")))
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
334 (license (list license:gpl2+ license:cecill))));either gpl2+ or cecill
336 (define-public coq-mathcomp
338 (name "coq-mathcomp")
344 (url "https://github.com/math-comp/math-comp")
345 (commit (string-append "mathcomp-" version))))
346 (file-name (git-file-name name version))
348 (base32 "1axywpa1jcpnidd86irpd1gdbbg2sfbwc652675xisq5wnmfmf6f"))))
349 (build-system gnu-build-system)
355 `(#:tests? #f ; No tests.
357 (modify-phases %standard-phases
359 (add-before 'build 'chdir
360 (lambda _ (chdir "mathcomp") #t))
362 (lambda* (#:key outputs #:allow-other-keys)
363 (invoke "make" "-f" "Makefile.coq"
364 (string-append "COQLIB=" (assoc-ref outputs "out")
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.
374 The library is written using the Ssreflect proof language that is an integral
375 part of the distribution.")
376 (license license:cecill-b)))
378 (define-public coq-coquelicot
380 (name "coq-coquelicot")
386 (url "https://gitlab.inria.fr/coquelicot/coquelicot.git")
387 (commit (string-append "coquelicot-" version))))
388 (file-name (git-file-name name version))
391 "0mz3pxan1237fr5fi79c66y7b9z7bmi0sc45kwrmkczsjm5462jm"))))
392 (build-system gnu-build-system)
394 `(("autoconf" ,autoconf)
395 ("automake" ,automake)
400 `(("mathcomp" ,coq-mathcomp)))
403 (list (string-append "--libdir=" (assoc-ref %outputs "out")
404 "/lib/coq/user-contrib/Coquelicot"))
406 (modify-phases %standard-phases
407 (add-before 'configure 'fix-remake
409 (substitute* "remake.cpp"
410 (("/bin/sh") (which "sh")))
413 (lambda _ (invoke "./remake")))
415 (lambda _ (invoke "./remake" "check")))
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+)))
431 (define-public coq-bignums
438 (url "https://github.com/coq/bignums")
439 (commit (string-append "V" version))))
440 (file-name (git-file-name name version))
443 "1xcd7c7qlvs0narfba6px34zq0mz8rffnhxw0kzhhg6i4iw115dp"))))
444 (build-system gnu-build-system)
449 `(("camlp5" ,camlp5)))
451 `(#:tests? #f ; No test target.
453 (list (string-append "COQLIBINSTALL=" (assoc-ref %outputs "out")
454 "/lib/coq/user-contrib"))
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+)))
464 (define-public coq-interval
466 (name "coq-interval")
472 (url "https://gitlab.inria.fr/coqinterval/interval.git")
473 (commit (string-append "interval-" version))))
474 (file-name (git-file-name name version))
477 "01iz6qmnsm6b9s1vmdjs79vjx9xgwzn5rwyjp6bvs8hg3zlmhpip"))))
478 (build-system gnu-build-system)
480 `(("autoconf" ,autoconf)
481 ("automake" ,automake)
486 `(("flocq" ,coq-flocq)
487 ("bignums" ,coq-bignums)
488 ("coquelicot" ,coq-coquelicot)
489 ("mathcomp" ,coq-mathcomp)))
492 (list (string-append "--libdir=" (assoc-ref %outputs "out")
493 "/lib/coq/user-contrib/Gappa"))
495 (modify-phases %standard-phases
496 (add-before 'configure 'fix-remake
498 (substitute* "remake.cpp"
499 (("/bin/sh") (which "sh")))
502 (lambda _ (invoke "./remake")))
504 (lambda _ (invoke "./remake" "check")))
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)))
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"))
520 (name "coq-autosubst")
521 (version (git-version "1" branch commit))
525 (url "git://github.com/uds-psl/autosubst")
527 (file-name (git-file-name name version))
529 (base32 "1cl0bp96bk6lplbl7n5c703vd3gvbs5mvf2qrf8q333kkqd7jqq4"))))
530 (build-system gnu-build-system)
534 (modify-phases %standard-phases
537 (lambda* (#:key outputs #:allow-other-keys)
538 (setenv "COQLIB" (string-append (assoc-ref outputs "out") "/lib/coq/"))
540 (string-append "COQLIB=" (assoc-ref outputs "out")
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))))
560 (define-public coq-equations
562 (name "coq-equations")
567 (url "https://github.com/mattam82/Coq-Equations")
568 (commit (string-append "v" version "-8.11"))))
569 (file-name (git-file-name name version))
572 "1srxz1rws8jsh7402g2x2vcqgjbbsr64dxxj5d2zs48pmhb20csf"))))
573 (build-system gnu-build-system)
579 `(#:test-target "test-suite"
581 (modify-phases %standard-phases
583 (lambda* (#:key outputs #:allow-other-keys)
584 (invoke "sh" "./configure.sh")))
586 (lambda* (#:key outputs #:allow-other-keys)
588 (string-append "COQLIB=" (assoc-ref outputs "out")
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
598 (license license:lgpl2.1)))
600 (define-public coq-stdpp
604 (synopsis "Alternative Coq standard library std++")
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))
613 "1m6c7ibwc99jd4cv14v3r327spnfvdf3x2mnq51f9rz99rffk68r"))))
614 (build-system gnu-build-system)
618 `(#:tests? #f ; Tests are executed during build phase.
620 (modify-phases %standard-phases
623 (lambda* (#:key outputs #:allow-other-keys)
625 (string-append "COQLIB=" (assoc-ref outputs "out")
628 (description "This project contains an extended \"Standard Library\" for
629 Coq called coq-std++. The key features are:
631 @item Great number of definitions and lemmas for common data structures such
632 as lists, finite maps, finite sets, and finite multisets.
634 @item Type classes for common notations (like ∅, ∪, and Haskell-style monad
635 notations) so that these can be overloaded for different data structures.
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.
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.
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.
651 @item The library is dependency- and axiom-free.
653 (home-page "https://gitlab.mpi-sws.org/iris/stdpp")
654 (license license:bsd-3)))