Commit | Line | Data |
---|---|---|
33af92dd JL |
1 | ;;; GNU Guix --- Functional package management for GNU |
2 | ;;; Copyright © 2018 Julien Lepiller <julien@lepiller.eu> | |
7d60df33 | 3 | ;;; Copyright © 2019 Dan Frumin <dfrumin@cs.ru.nl> |
33af92dd JL |
4 | ;;; |
5 | ;;; This file is part of GNU Guix. | |
6 | ;;; | |
7 | ;;; GNU Guix is free software; you can redistribute it and/or modify it | |
8 | ;;; under the terms of the GNU General Public License as published by | |
9 | ;;; the Free Software Foundation; either version 3 of the License, or (at | |
10 | ;;; your option) any later version. | |
11 | ;;; | |
12 | ;;; GNU Guix is distributed in the hope that it will be useful, but | |
13 | ;;; WITHOUT ANY WARRANTY; without even the implied warranty of | |
14 | ;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the | |
15 | ;;; GNU General Public License for more details. | |
16 | ;;; | |
17 | ;;; You should have received a copy of the GNU General Public License | |
18 | ;;; along with GNU Guix. If not, see <http://www.gnu.org/licenses/>. | |
19 | ||
20 | (define-module (gnu packages coq) | |
21 | #:use-module (gnu packages) | |
22 | #:use-module (gnu packages base) | |
23 | #:use-module (gnu packages bison) | |
24 | #:use-module (gnu packages boost) | |
25 | #:use-module (gnu packages emacs) | |
26 | #:use-module (gnu packages flex) | |
27 | #:use-module (gnu packages multiprecision) | |
28 | #:use-module (gnu packages ocaml) | |
29 | #:use-module (gnu packages perl) | |
30 | #:use-module (gnu packages python) | |
31 | #:use-module (gnu packages texinfo) | |
32 | #:use-module (guix build-system gnu) | |
33 | #:use-module (guix build-system ocaml) | |
34 | #:use-module (guix download) | |
7d60df33 | 35 | #:use-module (guix git-download) |
33af92dd JL |
36 | #:use-module ((guix licenses) #:prefix license:) |
37 | #:use-module (guix packages) | |
38 | #:use-module (guix utils) | |
39 | #:use-module ((srfi srfi-1) #:hide (zip))) | |
40 | ||
41 | (define-public coq | |
42 | (package | |
43 | (name "coq") | |
44 | (version "8.8.2") | |
45 | (source (origin | |
46 | (method url-fetch) | |
47 | (uri (string-append "https://github.com/coq/coq/archive/V" | |
48 | version ".tar.gz")) | |
49 | (file-name (string-append name "-" version ".tar.gz")) | |
50 | (sha256 | |
51 | (base32 | |
52 | "0i2hs0i6rp27cy8zd0mx7jscqw5cx2y0diw0pxgij66s3yr47y7r")))) | |
53 | (native-search-paths | |
54 | (list (search-path-specification | |
55 | (variable "COQPATH") | |
56 | (files (list "lib/coq/user-contrib"))))) | |
57 | (build-system ocaml-build-system) | |
58 | (inputs | |
59 | `(("lablgtk" ,lablgtk) | |
60 | ("python" ,python-2) | |
61 | ("camlp5" ,camlp5) | |
62 | ("ocaml-num" ,ocaml-num))) | |
63 | (arguments | |
64 | `(#:phases | |
65 | (modify-phases %standard-phases | |
66 | (replace 'configure | |
67 | (lambda* (#:key outputs #:allow-other-keys) | |
68 | (let* ((out (assoc-ref outputs "out")) | |
69 | (mandir (string-append out "/share/man")) | |
70 | (browser "icecat -remote \"OpenURL(%s,new-tab)\"")) | |
71 | (invoke "./configure" | |
72 | "-prefix" out | |
73 | "-mandir" mandir | |
74 | "-browser" browser | |
75 | "-coqide" "opt")))) | |
76 | (replace 'build | |
77 | (lambda _ | |
78 | (invoke "make" | |
79 | "-j" (number->string (parallel-job-count)) | |
80 | "world"))) | |
81 | (delete 'check) | |
82 | (add-after 'install 'check | |
83 | (lambda _ | |
84 | (with-directory-excursion "test-suite" | |
85 | ;; These two tests fail. | |
86 | ;; This one fails because the output is not formatted as expected. | |
87 | (delete-file-recursively "coq-makefile/timing") | |
88 | ;; This one fails because we didn't build coqtop.byte. | |
89 | (delete-file-recursively "coq-makefile/findlib-package") | |
90 | (invoke "make"))))))) | |
91 | (home-page "https://coq.inria.fr") | |
92 | (synopsis "Proof assistant for higher-order logic") | |
93 | (description | |
94 | "Coq is a proof assistant for higher-order logic, which allows the | |
95 | development of computer programs consistent with their formal specification. | |
96 | It is developed using Objective Caml and Camlp5.") | |
97 | ;; The code is distributed under lgpl2.1. | |
98 | ;; Some of the documentation is distributed under opl1.0+. | |
99 | (license (list license:lgpl2.1 license:opl1.0+)))) | |
100 | ||
101 | (define-public proof-general | |
102 | (package | |
103 | (name "proof-general") | |
104 | (version "4.2") | |
105 | (source (origin | |
106 | (method url-fetch) | |
107 | (uri (string-append | |
108 | "http://proofgeneral.inf.ed.ac.uk/releases/" | |
109 | "ProofGeneral-" version ".tgz")) | |
110 | (sha256 | |
111 | (base32 | |
112 | "09qb0myq66fw17v4ziz401ilsb5xlxz1nl2wsp69d0vrfy0bcrrm")))) | |
113 | (build-system gnu-build-system) | |
114 | (native-inputs | |
115 | `(("which" ,which) | |
116 | ("emacs" ,emacs-minimal) | |
117 | ("texinfo" ,texinfo))) | |
118 | (inputs | |
119 | `(("host-emacs" ,emacs) | |
120 | ("perl" ,perl) | |
121 | ("coq" ,coq))) | |
122 | (arguments | |
123 | `(#:tests? #f ; no check target | |
124 | #:make-flags (list (string-append "PREFIX=" %output) | |
125 | (string-append "DEST_PREFIX=" %output)) | |
126 | #:modules ((guix build gnu-build-system) | |
127 | (guix build utils) | |
128 | (guix build emacs-utils)) | |
129 | #:imported-modules (,@%gnu-build-system-modules | |
130 | (guix build emacs-utils)) | |
131 | #:phases | |
132 | (modify-phases %standard-phases | |
133 | (delete 'configure) | |
134 | (add-after 'unpack 'disable-byte-compile-error-on-warn | |
135 | (lambda _ | |
136 | (substitute* "Makefile" | |
137 | (("\\(setq byte-compile-error-on-warn t\\)") | |
138 | "(setq byte-compile-error-on-warn nil)")) | |
139 | #t)) | |
140 | (add-after 'unpack 'patch-hardcoded-paths | |
141 | (lambda* (#:key inputs outputs #:allow-other-keys) | |
142 | (let ((out (assoc-ref outputs "out")) | |
143 | (coq (assoc-ref inputs "coq")) | |
144 | (emacs (assoc-ref inputs "host-emacs"))) | |
145 | (define (coq-prog name) | |
146 | (string-append coq "/bin/" name)) | |
147 | (emacs-substitute-variables "coq/coq.el" | |
148 | ("coq-prog-name" (coq-prog "coqtop")) | |
149 | ("coq-compiler" (coq-prog "coqc")) | |
150 | ("coq-dependency-analyzer" (coq-prog "coqdep"))) | |
151 | (substitute* "Makefile" | |
152 | (("/sbin/install-info") "install-info")) | |
153 | (substitute* "bin/proofgeneral" | |
154 | (("^PGHOMEDEFAULT=.*" all) | |
155 | (string-append all | |
156 | "PGHOME=$PGHOMEDEFAULT\n" | |
157 | "EMACS=" emacs "/bin/emacs"))) | |
158 | #t))) | |
159 | (add-after 'unpack 'clean | |
a48d6acc RW |
160 | (lambda _ |
161 | ;; Delete the pre-compiled elc files for Emacs 23. | |
162 | (invoke "make" "clean"))) | |
33af92dd | 163 | (add-after 'install 'install-doc |
a48d6acc RW |
164 | (lambda* (#:key make-flags #:allow-other-keys) |
165 | ;; XXX FIXME avoid building/installing pdf files, | |
166 | ;; due to unresolved errors building them. | |
167 | (substitute* "Makefile" | |
168 | ((" [^ ]*\\.pdf") "")) | |
169 | (apply invoke "make" "install-doc" make-flags)))))) | |
33af92dd JL |
170 | (home-page "http://proofgeneral.inf.ed.ac.uk/") |
171 | (synopsis "Generic front-end for proof assistants based on Emacs") | |
172 | (description | |
173 | "Proof General is a major mode to turn Emacs into an interactive proof | |
174 | assistant to write formal mathematical proofs using a variety of theorem | |
175 | provers.") | |
176 | (license license:gpl2+))) | |
177 | ||
178 | (define-public coq-flocq | |
179 | (package | |
180 | (name "coq-flocq") | |
181 | (version "2.6.1") | |
182 | (source (origin | |
183 | (method url-fetch) | |
184 | ;; Use the ‘Latest version’ link for a stable URI across releases. | |
185 | (uri (string-append "https://gforge.inria.fr/frs/download.php/" | |
186 | "file/37454/flocq-" version ".tar.gz")) | |
187 | (sha256 | |
188 | (base32 | |
189 | "06msp1fwpqv6p98a3i1nnkj7ch9rcq3rm916yxq8dxf51lkghrin")))) | |
190 | (build-system gnu-build-system) | |
191 | (native-inputs | |
192 | `(("ocaml" ,ocaml) | |
193 | ("which" ,which) | |
194 | ("coq" ,coq))) | |
195 | (arguments | |
196 | `(#:configure-flags | |
197 | (list (string-append "--libdir=" (assoc-ref %outputs "out") | |
198 | "/lib/coq/user-contrib/Flocq")) | |
199 | #:phases | |
200 | (modify-phases %standard-phases | |
201 | (add-before 'configure 'fix-remake | |
202 | (lambda _ | |
203 | (substitute* "remake.cpp" | |
204 | (("/bin/sh") (which "sh"))) | |
205 | #t)) | |
206 | (replace 'build | |
207 | (lambda _ | |
208 | (invoke "./remake") | |
209 | #t)) | |
210 | (replace 'check | |
211 | (lambda _ | |
212 | (invoke "./remake" "check") | |
213 | #t)) | |
214 | ;; TODO: requires coq-gappa and coq-interval. | |
215 | ;(invoke "./remake" "check-more") | |
216 | (replace 'install | |
217 | (lambda _ | |
218 | (invoke "./remake" "install") | |
219 | #t))))) | |
220 | (home-page "http://flocq.gforge.inria.fr/") | |
221 | (synopsis "Floating-point formalization for the Coq system") | |
222 | (description "Flocq (Floats for Coq) is a floating-point formalization for | |
223 | the Coq system. It provides a comprehensive library of theorems on a multi-radix | |
224 | multi-precision arithmetic. It also supports efficient numerical computations | |
225 | inside Coq.") | |
226 | (license license:lgpl3+))) | |
227 | ||
228 | (define-public coq-gappa | |
229 | (package | |
230 | (name "coq-gappa") | |
231 | (version "1.3.2") | |
232 | (source (origin | |
233 | (method url-fetch) | |
234 | (uri (string-append "https://gforge.inria.fr/frs/download.php/file/36397/gappa-" | |
235 | version ".tar.gz")) | |
236 | (sha256 | |
237 | (base32 | |
238 | "19kg2zldaqs4smy7bv9hp650sqg46xbx1ss7jnyagpxdscwn9apd")))) | |
239 | (build-system gnu-build-system) | |
240 | (native-inputs | |
241 | `(("ocaml" ,ocaml) | |
242 | ("which" ,which) | |
243 | ("coq" ,coq) | |
244 | ("bison" ,bison) | |
245 | ("flex" ,flex))) | |
246 | (inputs | |
247 | `(("gmp" ,gmp) | |
248 | ("mpfr" ,mpfr) | |
249 | ("boost" ,boost))) | |
250 | (arguments | |
251 | `(#:configure-flags | |
252 | (list (string-append "--libdir=" (assoc-ref %outputs "out") | |
253 | "/lib/coq/user-contrib/Gappa")) | |
254 | #:phases | |
255 | (modify-phases %standard-phases | |
256 | (add-before 'configure 'fix-remake | |
257 | (lambda _ | |
258 | (substitute* "remake.cpp" | |
ace73a93 RW |
259 | (("/bin/sh") (which "sh"))) |
260 | #t)) | |
33af92dd | 261 | (replace 'build |
ace73a93 | 262 | (lambda _ (invoke "./remake"))) |
33af92dd | 263 | (replace 'check |
ace73a93 | 264 | (lambda _ (invoke "./remake" "check"))) |
33af92dd | 265 | (replace 'install |
ace73a93 | 266 | (lambda _ (invoke "./remake" "install")))))) |
33af92dd JL |
267 | (home-page "http://gappa.gforge.inria.fr/") |
268 | (synopsis "Verify and formally prove properties on numerical programs") | |
269 | (description "Gappa is a tool intended to help verifying and formally proving | |
270 | properties on numerical programs dealing with floating-point or fixed-point | |
271 | arithmetic. It has been used to write robust floating-point filters for CGAL | |
272 | and it is used to certify elementary functions in CRlibm. While Gappa is | |
273 | intended to be used directly, it can also act as a backend prover for the Why3 | |
274 | software verification plateform or as an automatic tactic for the Coq proof | |
275 | assistant.") | |
276 | (license (list license:gpl2+ license:cecill))));either gpl2+ or cecill | |
277 | ||
278 | (define-public coq-mathcomp | |
279 | (package | |
280 | (name "coq-mathcomp") | |
281 | (version "1.7.0") | |
282 | (source (origin | |
283 | (method url-fetch) | |
284 | (uri (string-append "https://github.com/math-comp/math-comp/archive/mathcomp-" | |
285 | version ".tar.gz")) | |
286 | (sha256 | |
287 | (base32 | |
288 | "05zgyi4wmasi1rcyn5jq42w0bi9713q9m8dl1fdgl66nmacixh39")))) | |
289 | (build-system gnu-build-system) | |
290 | (native-inputs | |
291 | `(("ocaml" ,ocaml) | |
292 | ("which" ,which) | |
293 | ("coq" ,coq))) | |
294 | (arguments | |
295 | `(#:tests? #f; No need to test formally-verified programs :) | |
296 | #:phases | |
297 | (modify-phases %standard-phases | |
298 | (delete 'configure) | |
299 | (add-before 'build 'chdir | |
492ee4f8 | 300 | (lambda _ (chdir "mathcomp") #t)) |
33af92dd JL |
301 | (replace 'install |
302 | (lambda* (#:key outputs #:allow-other-keys) | |
303 | (setenv "COQLIB" (string-append (assoc-ref outputs "out") "/lib/coq/")) | |
492ee4f8 RW |
304 | (invoke "make" "-f" "Makefile.coq" |
305 | (string-append "COQLIB=" (assoc-ref outputs "out") | |
306 | "/lib/coq/") | |
307 | "install")))))) | |
33af92dd JL |
308 | (home-page "https://math-comp.github.io/math-comp/") |
309 | (synopsis "Mathematical Components for Coq") | |
310 | (description "Mathematical Components for Coq has its origins in the formal | |
311 | proof of the Four Colour Theorem. Since then it has grown to cover many areas | |
312 | of mathematics and has been used for large scale projects like the formal proof | |
313 | of the Odd Order Theorem. | |
314 | ||
315 | The library is written using the Ssreflect proof language that is an integral | |
316 | part of the distribution.") | |
317 | (license license:cecill-b))) | |
318 | ||
319 | (define-public coq-coquelicot | |
320 | (package | |
321 | (name "coq-coquelicot") | |
322 | (version "3.0.1") | |
323 | (source (origin | |
324 | (method url-fetch) | |
325 | (uri (string-append "https://gforge.inria.fr/frs/download.php/" | |
326 | "file/37045/coquelicot-" version ".tar.gz")) | |
327 | (sha256 | |
328 | (base32 | |
329 | "0hsyhsy2lwqxxx2r8xgi5csmirss42lp9bkb9yy35mnya0w78c8r")))) | |
330 | (build-system gnu-build-system) | |
331 | (native-inputs | |
332 | `(("ocaml" ,ocaml) | |
333 | ("which" ,which) | |
334 | ("coq" ,coq))) | |
335 | (propagated-inputs | |
336 | `(("mathcomp" ,coq-mathcomp))) | |
337 | (arguments | |
338 | `(#:configure-flags | |
339 | (list (string-append "--libdir=" (assoc-ref %outputs "out") | |
340 | "/lib/coq/user-contrib/Coquelicot")) | |
341 | #:phases | |
342 | (modify-phases %standard-phases | |
343 | (add-before 'configure 'fix-coq8.8 | |
344 | (lambda _ | |
345 | ; appcontext has been removed from coq 8.8 | |
346 | (substitute* "theories/AutoDerive.v" | |
347 | (("appcontext") "context")) | |
348 | #t)) | |
349 | (add-before 'configure 'fix-remake | |
350 | (lambda _ | |
351 | (substitute* "remake.cpp" | |
e09e8388 RW |
352 | (("/bin/sh") (which "sh"))) |
353 | #t)) | |
33af92dd | 354 | (replace 'build |
e09e8388 | 355 | (lambda _ (invoke "./remake"))) |
33af92dd | 356 | (replace 'check |
e09e8388 | 357 | (lambda _ (invoke "./remake" "check"))) |
33af92dd | 358 | (replace 'install |
e09e8388 | 359 | (lambda _ (invoke "./remake" "install")))))) |
33af92dd JL |
360 | (home-page "http://coquelicot.saclay.inria.fr/index.html") |
361 | (synopsis "Coq library for Reals") | |
362 | (description "Coquelicot is an easier way of writing formulas and theorem | |
363 | statements, achieved by relying on total functions in place of dependent types | |
364 | for limits, derivatives, integrals, power series, and so on. To help with the | |
365 | proof process, the library comes with a comprehensive set of theorems that cover | |
366 | not only these notions, but also some extensions such as parametric integrals, | |
367 | two-dimensional differentiability, asymptotic behaviors. It also offers some | |
368 | automations for performing differentiability proofs. Moreover, Coquelicot is a | |
369 | conservative extension of Coq's standard library and provides correspondence | |
370 | theorems between the two libraries.") | |
371 | (license license:lgpl3+))) | |
372 | ||
373 | (define-public coq-bignums | |
374 | (package | |
375 | (name "coq-bignums") | |
376 | (version "8.8.0") | |
377 | (source (origin | |
378 | (method url-fetch) | |
379 | (uri (string-append "https://github.com/coq/bignums/archive/V" | |
380 | version ".tar.gz")) | |
381 | (file-name (string-append name "-" version ".tar.gz")) | |
382 | (sha256 | |
383 | (base32 | |
384 | "08m1cmq4hkaf4sb0vy978c11rgzvds71cphyadmr2iirpr5815r0")))) | |
385 | (build-system gnu-build-system) | |
386 | (native-inputs | |
387 | `(("ocaml" ,ocaml) | |
388 | ("coq" ,coq))) | |
389 | (inputs | |
390 | `(("camlp5" ,camlp5))) | |
391 | (arguments | |
392 | `(#:tests? #f; No test target | |
393 | #:make-flags | |
394 | (list (string-append "COQLIBINSTALL=" (assoc-ref %outputs "out") | |
395 | "/lib/coq/user-contrib")) | |
396 | #:phases | |
397 | (modify-phases %standard-phases | |
398 | (delete 'configure)))) | |
399 | (home-page "https://github.com/coq/bignums") | |
400 | (synopsis "Coq library for arbitrary large numbers") | |
401 | (description "Bignums is a coq library of arbitrary large numbers. It | |
402 | provides BigN, BigZ, BigQ that used to be part of Coq standard library.") | |
403 | (license license:lgpl2.1+))) | |
404 | ||
405 | (define-public coq-interval | |
406 | (package | |
407 | (name "coq-interval") | |
408 | (version "3.3.0") | |
409 | (source (origin | |
410 | (method url-fetch) | |
411 | (uri (string-append "https://gforge.inria.fr/frs/download.php/" | |
412 | "file/37077/interval-" version ".tar.gz")) | |
413 | (sha256 | |
414 | (base32 | |
415 | "08fdcf3hbwqphglvwprvqzgkg0qbimpyhnqsgv3gac4y1ap0f903")))) | |
416 | (build-system gnu-build-system) | |
417 | (native-inputs | |
418 | `(("ocaml" ,ocaml) | |
419 | ("which" ,which) | |
420 | ("coq" ,coq))) | |
421 | (propagated-inputs | |
422 | `(("flocq" ,coq-flocq) | |
423 | ("bignums" ,coq-bignums) | |
424 | ("coquelicot" ,coq-coquelicot) | |
425 | ("mathcomp" ,coq-mathcomp))) | |
426 | (arguments | |
427 | `(#:configure-flags | |
428 | (list (string-append "--libdir=" (assoc-ref %outputs "out") | |
429 | "/lib/coq/user-contrib/Gappa")) | |
430 | #:phases | |
431 | (modify-phases %standard-phases | |
432 | (add-before 'configure 'fix-remake | |
433 | (lambda _ | |
434 | (substitute* "remake.cpp" | |
7492af9b RW |
435 | (("/bin/sh") (which "sh"))) |
436 | #t)) | |
33af92dd | 437 | (replace 'build |
7492af9b | 438 | (lambda _ (invoke "./remake"))) |
33af92dd | 439 | (replace 'check |
7492af9b | 440 | (lambda _ (invoke "./remake" "check"))) |
33af92dd | 441 | (replace 'install |
7492af9b | 442 | (lambda _ (invoke "./remake" "install")))))) |
33af92dd JL |
443 | (home-page "http://coq-interval.gforge.inria.fr/") |
444 | (synopsis "Coq tactics to simplify inequality proofs") | |
445 | (description "Interval provides vernacular files containing tactics for | |
446 | simplifying the proofs of inequalities on expressions of real numbers for the | |
447 | Coq proof assistant.") | |
448 | (license license:cecill-c))) | |
7d60df33 DF |
449 | |
450 | (define-public coq-autosubst | |
451 | ;; Latest commit on that branch, where work on supporting coq 8.6 and | |
452 | ;; more recent versions of coq happen. | |
453 | (let ((branch "coq86-devel") | |
454 | (commit "d0d73557979796b3d4be7aac72135581c33f26f7")) | |
455 | (package | |
456 | (name "coq-autosubst") | |
457 | (version (git-version "1" branch commit)) | |
458 | (source (origin | |
459 | (method git-fetch) | |
460 | (uri (git-reference | |
461 | (url "git://github.com/uds-psl/autosubst.git") | |
462 | (commit commit))) | |
463 | (file-name (git-file-name name version)) | |
464 | (sha256 | |
465 | (base32 "1852xb5cwkjw3dlc0lp2sakwa40bjzw37qmwz4bn3vqazg1hnh6r")))) | |
466 | (build-system gnu-build-system) | |
467 | (arguments | |
468 | `(#:tests? #f | |
469 | #:phases | |
470 | (modify-phases %standard-phases | |
471 | (delete 'configure) | |
472 | (replace 'install | |
473 | (lambda* (#:key outputs #:allow-other-keys) | |
474 | (setenv "COQLIB" (string-append (assoc-ref outputs "out") "/lib/coq/")) | |
475 | (invoke "make" | |
476 | (string-append "COQLIB=" (assoc-ref outputs "out") | |
477 | "/lib/coq/") | |
478 | "install")))))) | |
479 | (native-inputs | |
480 | `(("coq" ,coq))) | |
481 | (home-page "https://www.ps.uni-saarland.de/autosubst/") | |
482 | (synopsis "Coq library for parallel de Bruijn substitutions") | |
483 | (description "Formalizing syntactic theories with variable binders is | |
484 | not easy. Autosubst is a library for the Coq proof assistant to | |
485 | automate this process. Given an inductive definition of syntactic objects in | |
486 | de Bruijn representation augmented with binding annotations, Autosubst | |
487 | synthesizes the parallel substitution operation and automatically proves the | |
488 | basic lemmas about substitutions. This library contains an automation | |
489 | tactic that solves equations involving terms and substitutions. This makes the | |
490 | usage of substitution lemmas unnecessary. The tactic is based on our current | |
491 | work on a decision procedure for the equational theory of an extension of the | |
492 | sigma-calculus by Abadi et al. The library is completely written in Coq and | |
493 | uses Ltac to synthesize the substitution operation.") | |
494 | (license license:bsd-3)))) |