Commit | Line | Data |
---|---|---|
33af92dd JL |
1 | ;;; GNU Guix --- Functional package management for GNU |
2 | ;;; Copyright © 2018 Julien Lepiller <julien@lepiller.eu> | |
b92660af | 3 | ;;; Copyright © 2018, 2019 Tobias Geerinckx-Rice <me@tobias.gr> |
7d60df33 | 4 | ;;; Copyright © 2019 Dan Frumin <dfrumin@cs.ru.nl> |
641981d3 | 5 | ;;; Copyright © 2020 Brett Gilio <brettg@gnu.org> |
6656123d | 6 | ;;; Copyright © 2020 Björn Höfling <bjoern.hoefling@bjoernhoefling.de> |
13947652 | 7 | ;;; Copyright © 2020 raingloom <raingloom@riseup.net> |
1042d269 | 8 | ;;; Copyright © 2020 Robin Green <greenrd@greenrd.org> |
33af92dd JL |
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) | |
34682557 | 27 | #:use-module (gnu packages autotools) |
33af92dd JL |
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) | |
66fbffde | 33 | #:use-module (gnu packages gawk) |
33af92dd JL |
34 | #:use-module (gnu packages multiprecision) |
35 | #:use-module (gnu packages ocaml) | |
36 | #:use-module (gnu packages perl) | |
37 | #:use-module (gnu packages python) | |
1042d269 | 38 | #:use-module (gnu packages rsync) |
33af92dd JL |
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) | |
7d60df33 | 43 | #:use-module (guix git-download) |
33af92dd JL |
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") | |
1042d269 | 52 | (version "8.11.2") |
8b9b2210 TGR |
53 | (source |
54 | (origin | |
55 | (method git-fetch) | |
56 | (uri (git-reference | |
b0e7b699 | 57 | (url "https://github.com/coq/coq") |
8b9b2210 TGR |
58 | (commit (string-append "V" version)))) |
59 | (file-name (git-file-name name version)) | |
60 | (sha256 | |
1ac40045 | 61 | (base32 |
1042d269 | 62 | "1gia82dkmzqspw2w3s4gjyh39ghbmw4i41i4hyzc91g7mza17nbz")))) |
33af92dd JL |
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) | |
4d6d88bb | 68 | (outputs '("out" "ide")) |
33af92dd | 69 | (inputs |
1ac40045 | 70 | `(("lablgtk" ,lablgtk3) |
33af92dd JL |
71 | ("python" ,python-2) |
72 | ("camlp5" ,camlp5) | |
73 | ("ocaml-num" ,ocaml-num))) | |
e03e1b55 | 74 | (native-inputs |
1042d269 RG |
75 | `(("ocaml-ounit" ,ocaml-ounit) |
76 | ("rsync" ,rsync) | |
77 | ("which" ,which))) | |
33af92dd JL |
78 | (arguments |
79 | `(#:phases | |
80 | (modify-phases %standard-phases | |
8b9b2210 TGR |
81 | (add-after 'unpack 'make-git-checkout-writable |
82 | (lambda _ | |
83 | (for-each make-file-writable (find-files ".")) | |
84 | #t)) | |
33af92dd JL |
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) | |
4d6d88bb JL |
101 | (add-after 'install 'remove-duplicate |
102 | (lambda* (#:key outputs #:allow-other-keys) | |
103 | (let* ((out (assoc-ref outputs "out")) | |
13947652 | 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"))) | |
a5727da9 BG |
109 | ;; These files are exact copies without `.opt` extension. |
110 | ;; Removing these saves 35 MiB in the resulting package. | |
13947652 | 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)) | |
4d6d88bb JL |
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)) | |
33af92dd JL |
125 | (add-after 'install 'check |
126 | (lambda _ | |
127 | (with-directory-excursion "test-suite" | |
128 | ;; These two tests fail. | |
a5727da9 | 129 | ;; Fails because the output is not formatted as expected. |
33af92dd | 130 | (delete-file-recursively "coq-makefile/timing") |
a5727da9 | 131 | ;; Fails because we didn't build coqtop.byte. |
1042d269 | 132 | (delete-file "misc/printers.sh") |
33af92dd JL |
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.") | |
a5727da9 | 140 | ;; The source code is distributed under lgpl2.1. |
33af92dd JL |
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") | |
5bd5d6ef | 147 | (version "4.4") |
33af92dd | 148 | (source (origin |
5bd5d6ef JS |
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)) | |
33af92dd JL |
155 | (sha256 |
156 | (base32 | |
5bd5d6ef | 157 | "0bdfk91wf71z80mdfnl8hpinripndcjgdkz854zil6521r84nqk8")))) |
33af92dd JL |
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)) | |
33af92dd JL |
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 | |
a48d6acc RW |
201 | (lambda _ |
202 | ;; Delete the pre-compiled elc files for Emacs 23. | |
203 | (invoke "make" "clean"))) | |
33af92dd | 204 | (add-after 'install 'install-doc |
a48d6acc RW |
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)))))) | |
53eaf69d | 211 | (home-page "https://proofgeneral.github.io/ ") |
33af92dd JL |
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") | |
1042d269 | 222 | (version "3.3.1") |
34682557 BG |
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 | |
1042d269 | 232 | "01gdykva0lcw6y3dm8j0djxayb87szfg9vn0mxd6z3pks644misl")))) |
33af92dd JL |
233 | (build-system gnu-build-system) |
234 | (native-inputs | |
34682557 BG |
235 | `(("autoconf" ,autoconf) |
236 | ("automake" ,automake) | |
237 | ("ocaml" ,ocaml) | |
33af92dd JL |
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 | |
34682557 BG |
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)) | |
33af92dd JL |
252 | (add-before 'configure 'fix-remake |
253 | (lambda _ | |
254 | (substitute* "remake.cpp" | |
255 | (("/bin/sh") (which "sh"))) | |
256 | #t)) | |
257 | (replace 'build | |
258 | (lambda _ | |
718d358a | 259 | (invoke "./remake"))) |
33af92dd JL |
260 | (replace 'check |
261 | (lambda _ | |
718d358a | 262 | (invoke "./remake" "check"))) |
33af92dd JL |
263 | ;; TODO: requires coq-gappa and coq-interval. |
264 | ;(invoke "./remake" "check-more") | |
265 | (replace 'install | |
266 | (lambda _ | |
718d358a | 267 | (invoke "./remake" "install")))))) |
59265e5f | 268 | (home-page "https://flocq.gforge.inria.fr/") |
33af92dd JL |
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") | |
1042d269 | 279 | (version "1.4.4") |
f24dc271 BG |
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 | |
1042d269 | 289 | "0f3g3wjkvfkm961l4jpckhsqd43jnvm7f5qqk78qc32zh1fg339n")))) |
33af92dd JL |
290 | (build-system gnu-build-system) |
291 | (native-inputs | |
f24dc271 BG |
292 | `(("autoconf" ,autoconf) |
293 | ("automake" ,automake) | |
294 | ("ocaml" ,ocaml) | |
33af92dd JL |
295 | ("which" ,which) |
296 | ("coq" ,coq) | |
f24dc271 | 297 | ("camlp5" ,camlp5) |
33af92dd JL |
298 | ("bison" ,bison) |
299 | ("flex" ,flex))) | |
300 | (inputs | |
301 | `(("gmp" ,gmp) | |
302 | ("mpfr" ,mpfr) | |
303 | ("boost" ,boost))) | |
f24dc271 BG |
304 | (propagated-inputs |
305 | `(("coq-flocq" ,coq-flocq))) | |
33af92dd JL |
306 | (arguments |
307 | `(#:configure-flags | |
308 | (list (string-append "--libdir=" (assoc-ref %outputs "out") | |
0fe041bd | 309 | "/lib/coq/user-contrib/Gappa")) |
33af92dd JL |
310 | #:phases |
311 | (modify-phases %standard-phases | |
312 | (add-before 'configure 'fix-remake | |
313 | (lambda _ | |
314 | (substitute* "remake.cpp" | |
ace73a93 RW |
315 | (("/bin/sh") (which "sh"))) |
316 | #t)) | |
33af92dd | 317 | (replace 'build |
ace73a93 | 318 | (lambda _ (invoke "./remake"))) |
f24dc271 BG |
319 | ;; FIXME: Figure out why failures occur, and re-enable check phase. |
320 | (delete 'check) | |
321 | ;; (replace 'check | |
322 | ;; (lambda _ (invoke "./remake" "check"))) | |
33af92dd | 323 | (replace 'install |
ace73a93 | 324 | (lambda _ (invoke "./remake" "install")))))) |
a61fe4c0 | 325 | (home-page "https://gappa.gforge.inria.fr/") |
33af92dd JL |
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") | |
1042d269 | 339 | (version "1.11.0") |
aaa2add8 TGR |
340 | (source |
341 | (origin | |
342 | (method git-fetch) | |
343 | (uri (git-reference | |
b0e7b699 | 344 | (url "https://github.com/math-comp/math-comp") |
aaa2add8 TGR |
345 | (commit (string-append "mathcomp-" version)))) |
346 | (file-name (git-file-name name version)) | |
347 | (sha256 | |
1042d269 | 348 | (base32 "1axywpa1jcpnidd86irpd1gdbbg2sfbwc652675xisq5wnmfmf6f")))) |
33af92dd JL |
349 | (build-system gnu-build-system) |
350 | (native-inputs | |
351 | `(("ocaml" ,ocaml) | |
352 | ("which" ,which) | |
353 | ("coq" ,coq))) | |
354 | (arguments | |
641981d3 | 355 | `(#:tests? #f ; No tests. |
33af92dd JL |
356 | #:phases |
357 | (modify-phases %standard-phases | |
358 | (delete 'configure) | |
359 | (add-before 'build 'chdir | |
492ee4f8 | 360 | (lambda _ (chdir "mathcomp") #t)) |
33af92dd JL |
361 | (replace 'install |
362 | (lambda* (#:key outputs #:allow-other-keys) | |
492ee4f8 RW |
363 | (invoke "make" "-f" "Makefile.coq" |
364 | (string-append "COQLIB=" (assoc-ref outputs "out") | |
365 | "/lib/coq/") | |
366 | "install")))))) | |
6656123d | 367 | (home-page "https://math-comp.github.io/") |
33af92dd JL |
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") | |
1042d269 | 381 | (version "3.1.0") |
d481db8b BG |
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 | |
1042d269 | 391 | "0mz3pxan1237fr5fi79c66y7b9z7bmi0sc45kwrmkczsjm5462jm")))) |
33af92dd JL |
392 | (build-system gnu-build-system) |
393 | (native-inputs | |
d481db8b BG |
394 | `(("autoconf" ,autoconf) |
395 | ("automake" ,automake) | |
396 | ("ocaml" ,ocaml) | |
33af92dd JL |
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 | |
33af92dd JL |
407 | (add-before 'configure 'fix-remake |
408 | (lambda _ | |
409 | (substitute* "remake.cpp" | |
e09e8388 RW |
410 | (("/bin/sh") (which "sh"))) |
411 | #t)) | |
33af92dd | 412 | (replace 'build |
e09e8388 | 413 | (lambda _ (invoke "./remake"))) |
33af92dd | 414 | (replace 'check |
e09e8388 | 415 | (lambda _ (invoke "./remake" "check"))) |
33af92dd | 416 | (replace 'install |
e09e8388 | 417 | (lambda _ (invoke "./remake" "install")))))) |
c0228096 | 418 | (home-page "http://coquelicot.saclay.inria.fr") |
33af92dd JL |
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") | |
1042d269 | 434 | (version "8.11.0") |
33af92dd | 435 | (source (origin |
775373b8 EF |
436 | (method git-fetch) |
437 | (uri (git-reference | |
b0e7b699 | 438 | (url "https://github.com/coq/bignums") |
775373b8 EF |
439 | (commit (string-append "V" version)))) |
440 | (file-name (git-file-name name version)) | |
33af92dd JL |
441 | (sha256 |
442 | (base32 | |
1042d269 | 443 | "1xcd7c7qlvs0narfba6px34zq0mz8rffnhxw0kzhhg6i4iw115dp")))) |
33af92dd JL |
444 | (build-system gnu-build-system) |
445 | (native-inputs | |
446 | `(("ocaml" ,ocaml) | |
447 | ("coq" ,coq))) | |
448 | (inputs | |
449 | `(("camlp5" ,camlp5))) | |
450 | (arguments | |
14af514b | 451 | `(#:tests? #f ; No test target. |
33af92dd JL |
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") | |
1042d269 | 467 | (version "4.0.0") |
8f121655 BG |
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 | |
1042d269 | 477 | "01iz6qmnsm6b9s1vmdjs79vjx9xgwzn5rwyjp6bvs8hg3zlmhpip")))) |
33af92dd JL |
478 | (build-system gnu-build-system) |
479 | (native-inputs | |
8f121655 BG |
480 | `(("autoconf" ,autoconf) |
481 | ("automake" ,automake) | |
482 | ("ocaml" ,ocaml) | |
33af92dd JL |
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" | |
7492af9b RW |
499 | (("/bin/sh") (which "sh"))) |
500 | #t)) | |
33af92dd | 501 | (replace 'build |
7492af9b | 502 | (lambda _ (invoke "./remake"))) |
33af92dd | 503 | (replace 'check |
7492af9b | 504 | (lambda _ (invoke "./remake" "check"))) |
33af92dd | 505 | (replace 'install |
7492af9b | 506 | (lambda _ (invoke "./remake" "install")))))) |
33af92dd JL |
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))) | |
7d60df33 DF |
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") | |
e03e1b55 | 518 | (commit "fa6ef30664511ffa659cbcf3c962715cbee03572")) |
7d60df33 DF |
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.git") | |
526 | (commit commit))) | |
527 | (file-name (git-file-name name version)) | |
528 | (sha256 | |
e03e1b55 | 529 | (base32 "1cl0bp96bk6lplbl7n5c703vd3gvbs5mvf2qrf8q333kkqd7jqq4")))) |
7d60df33 DF |
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)))) | |
ec23bae6 DF |
559 | |
560 | (define-public coq-equations | |
561 | (package | |
562 | (name "coq-equations") | |
1042d269 | 563 | (version "1.2.3") |
ec23bae6 DF |
564 | (source (origin |
565 | (method git-fetch) | |
566 | (uri (git-reference | |
b0e7b699 | 567 | (url "https://github.com/mattam82/Coq-Equations") |
1042d269 | 568 | (commit (string-append "v" version "-8.11")))) |
ec23bae6 DF |
569 | (file-name (git-file-name name version)) |
570 | (sha256 | |
571 | (base32 | |
1042d269 | 572 | "1srxz1rws8jsh7402g2x2vcqgjbbsr64dxxj5d2zs48pmhb20csf")))) |
ec23bae6 DF |
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) | |
cd5406ef | 584 | (invoke "sh" "./configure.sh"))) |
ec23bae6 DF |
585 | (replace 'install |
586 | (lambda* (#:key outputs #:allow-other-keys) | |
ec23bae6 DF |
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))) | |
66fbffde DF |
599 | |
600 | (define-public coq-stdpp | |
601 | (package | |
602 | (name "coq-stdpp") | |
599f8d98 | 603 | (version "1.4.0") |
66fbffde DF |
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 | |
d2884b7f | 612 | (base32 |
599f8d98 | 613 | "1m6c7ibwc99jd4cv14v3r327spnfvdf3x2mnq51f9rz99rffk68r")))) |
66fbffde DF |
614 | (build-system gnu-build-system) |
615 | (inputs | |
616 | `(("coq" ,coq))) | |
617 | (arguments | |
3c9e86ae | 618 | `(#:tests? #f ; Tests are executed during build phase. |
66fbffde DF |
619 | #:phases |
620 | (modify-phases %standard-phases | |
621 | (delete 'configure) | |
622 | (replace 'install | |
623 | (lambda* (#:key outputs #:allow-other-keys) | |
66fbffde DF |
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))) |