projects/guix·blob java-team · refs

759 lines · 30.3 KiB

1;;; GNU Guix --- Functional package management for GNU
2;;; Copyright © 2018-2021 Julien Lepiller <[email protected]>
3;;; Copyright © 2018, 2019 Tobias Geerinckx-Rice <[email protected]>
4;;; Copyright © 2019 Dan Frumin <[email protected]>
5;;; Copyright © 2020 Brett Gilio <[email protected]>
6;;; Copyright © 2020 Björn Höfling <[email protected]>
7;;; Copyright © 2020 raingloom <[email protected]>
8;;; Copyright © 2020 Robin Green <[email protected]>
9;;; Copyright © 2021 Xinglu Chen <[email protected]>
10;;; Copyright © 2021 Simon Tournier <[email protected]>
11;;; Copyright © 2022 Garek Dyszel <[email protected]>
12;;; Copyright © 2024 Foundation Devices, Inc. <[email protected]>
13;;; Copyright © 2024 Zheng Junjie <[email protected]>
14;;;
15;;; This file is part of GNU Guix.
16;;;
17;;; GNU Guix is free software; you can redistribute it and/or modify it
18;;; under the terms of the GNU General Public License as published by
19;;; the Free Software Foundation; either version 3 of the License, or (at
20;;; your option) any later version.
21;;;
22;;; GNU Guix is distributed in the hope that it will be useful, but
23;;; WITHOUT ANY WARRANTY; without even the implied warranty of
24;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
25;;; GNU General Public License for more details.
26;;;
27;;; You should have received a copy of the GNU General Public License
28;;; along with GNU Guix. If not, see <http://www.gnu.org/licenses/>.
29
30(define-module (gnu packages coq)
31 #:use-module (gnu packages)
32 #:use-module (gnu packages autotools)
33 #:use-module (gnu packages base)
34 #:use-module (gnu packages bison)
35 #:use-module (gnu packages boost)
36 #:use-module (gnu packages compression)
37 #:use-module (gnu packages emacs)
38 #:use-module (gnu packages compiler-tools)
39 #:use-module (gnu packages gawk)
40 #:use-module (gnu packages multiprecision)
41 #:use-module (gnu packages ocaml)
42 #:use-module (gnu packages perl)
43 #:use-module (gnu packages python)
44 #:use-module (gnu packages rsync)
45 #:use-module (gnu packages texinfo)
46 #:use-module (guix build-system dune)
47 #:use-module (guix build-system gnu)
48 #:use-module (guix build-system trivial)
49 #:use-module (guix download)
50 #:use-module (guix gexp)
51 #:use-module (guix git-download)
52 #:use-module ((guix licenses) #:prefix license:)
53 #:use-module (guix packages)
54 #:use-module (guix utils)
55 #:use-module ((srfi srfi-1) #:hide (zip)))
56
57(define-public coq
58 (package
59 (name "coq")
60 (version "8.18.0")
61 (source
62 (origin
63 (method git-fetch)
64 (uri (git-reference
65 (url "https://github.com/coq/coq")
66 (commit (string-append "V" version))))
67 (file-name (git-file-name name version))
68 (sha256
69 (base32
70 "1qy71gdr4s2l6847b4nwns6akib2f7l725zb01m7zc26n6mrrh1m"))))
71 (native-search-paths
72 (list (search-path-specification
73 (variable "COQPATH")
74 (files (list "lib/coq/user-contrib")))))
75 (build-system dune-build-system)
76 (arguments
77 (list
78 #:package "coq-core,coq-stdlib,coq"
79 #:phases
80 #~(modify-phases %standard-phases
81 (add-before 'build 'configure
82 (lambda* (#:key outputs #:allow-other-keys)
83 (let* ((out (assoc-ref outputs "out"))
84 (coqlib (string-append out "/lib/ocaml/site-lib/coq/")))
85 (invoke "./configure" "-prefix" out
86 "-libdir" coqlib))))
87 (add-before 'build 'make-dunestrap
88 (lambda _ (invoke "make" "dunestrap")))
89 (replace 'install
90 (lambda* (#:key outputs #:allow-other-keys)
91 (let* ((out (assoc-ref outputs "out"))
92 (libdir (string-append out "/lib/ocaml/site-lib")))
93 (invoke "dune" "install" "--prefix" out
94 "--libdir" libdir "coq" "coq-core" "coq-stdlib")))))))
95 (propagated-inputs
96 (list ocaml-zarith))
97 (inputs
98 (list gmp))
99 (native-inputs
100 (list ocaml-ounit2 which))
101 (properties '((upstream-name . "coq"))) ; also for inherited packages
102 (home-page "https://coq.inria.fr")
103 (synopsis "Proof assistant for higher-order logic")
104 (description
105 "Coq is a proof assistant for higher-order logic, which allows the
106development of computer programs consistent with their formal specification.
107It is developed using Objective Caml and Camlp5.")
108 ;; The source code is distributed under lgpl2.1.
109 ;; Some of the documentation is distributed under opl1.0+.
110 (license (list license:lgpl2.1 license:opl1.0+))))
111
112(define-public coq-ide-server
113 (package
114 (inherit coq)
115 (name "coq-ide-server")
116 (arguments
117 `(#:tests? #f
118 #:package "coqide-server"))
119 (inputs
120 (list coq gmp))))
121
122(define-public coq-ide
123 (package
124 (inherit coq)
125 (name "coq-ide")
126 (arguments
127 `(#:tests? #f
128 #:package "coqide"))
129 (propagated-inputs
130 (list coq coq-ide-server zlib))
131 (inputs
132 (list lablgtk3 ocaml-lablgtk3-sourceview3))))
133
134(define-public proof-general
135 ;; The latest release is from 2022 and there has been more than 100 commits
136 ;; since then.
137 ;; Commit from 2024-04-29.
138 (let ((commit "d6689469298b4140dc1f0f8b0ff7e8f937041ffe")
139 (revision "2"))
140 (package
141 (name "proof-general")
142 (version (git-version "4.5" revision commit))
143 (source (origin
144 (method git-fetch)
145 (uri (git-reference
146 (url "https://github.com/ProofGeneral/PG")
147 (commit commit)))
148 (file-name (git-file-name name version))
149 (sha256
150 (base32
151 "1d12z41rn5nh15qj4sf0w8xrbd9djxlrz0r6g38fiq63i7krbm4x"))))
152 (build-system gnu-build-system)
153 (native-inputs
154 `(("emacs" ,emacs-minimal)
155 ("texinfo" ,texinfo)))
156 (inputs
157 (list perl))
158 (arguments
159 (let ((base-directory "/share/emacs/site-lisp/ProofGeneral"))
160 `(#:tests? #f ; no check target
161 #:make-flags (list (string-append "PREFIX=" %output)
162 (string-append "EMACS=" (assoc-ref %build-inputs "emacs")
163 "/bin/emacs")
164 (string-append "DEST_PREFIX=" %output)
165 (string-append "ELISP=" %output ,base-directory)
166 (string-append "DEST_ELISP=" %output ,base-directory)
167 (string-append "ELISP_START=" %output ,base-directory))
168 #:phases
169 (modify-phases %standard-phases
170 (delete 'configure)
171 (add-after 'unpack 'patch-hardcoded-paths
172 (lambda _
173 (substitute* "Makefile"
174 (("/sbin/install-info") "install-info"))))
175 (add-after 'unpack 'do-not-patch-script-shebangs
176 (lambda _
177 (substitute* "Makefile"
178 (("install-bin: scripts") "install-bin:"))))
179 (add-after 'install 'install-doc
180 (lambda* (#:key make-flags #:allow-other-keys)
181 ;; XXX FIXME avoid building/installing pdf files,
182 ;; due to unresolved errors building them.
183 (substitute* "Makefile"
184 ((" [^ ]*\\.pdf") ""))
185 (apply invoke "make" "install-doc" make-flags)))
186 (add-after 'install 'allow-subfolders-autoloads
187 ;; Autoload cookies are present in sub-directories. A friendly
188 ;; wrapper proof-general.el around generic/proof-site.el is
189 ;; provided for execution on Emacs start-up. It serves two
190 ;; purposes:
191 ;;
192 ;; * Setting up the load path when byte-compiling pg.
193 ;; * Loading a minimal PG setup on startup (not all of Proof
194 ;; General, of course; mostly mode hooks and autoloads).
195 ;;
196 ;; The renaming to proof-general-autoloads.el is Guix
197 ;; specific.
198 (lambda* (#:key outputs #:allow-other-keys)
199 (let ((out (assoc-ref outputs "out")))
200 (copy-file "proof-general.el"
201 (string-append out ,base-directory
202 "/proof-general-autoloads.el")))))))))
203 (home-page "https://proofgeneral.github.io/")
204 (synopsis "Generic front-end for proof assistants based on Emacs")
205 (description
206 "Proof General is a major mode to turn Emacs into an interactive proof
207assistant to write formal mathematical proofs using a variety of theorem
208provers.")
209 (license license:gpl3+))))
210
211(define-public coq-flocq
212 (package
213 (name "coq-flocq")
214 (version "4.1.4")
215 (source
216 (origin
217 (method git-fetch)
218 (uri (git-reference
219 (url "https://gitlab.inria.fr/flocq/flocq.git")
220 (commit (string-append "flocq-" version))))
221 (file-name (git-file-name name version))
222 (sha256
223 (base32
224 "08vrh0h909vmam1b4gfrvcmamnhmr5g0x79zx98hn7cx0vdwysh7"))))
225 (build-system gnu-build-system)
226 (native-inputs
227 (list autoconf automake ocaml which coq))
228 (arguments
229 `(#:configure-flags
230 (list (string-append "COQUSERCONTRIB=" (assoc-ref %outputs "out")
231 "/lib/coq/user-contrib"))
232 #:phases
233 (modify-phases %standard-phases
234 (add-before 'configure 'fix-remake
235 (lambda _
236 (substitute* "remake.cpp"
237 (("/bin/sh") (which "sh")))
238 #t))
239 (replace 'build
240 (lambda _
241 (invoke "./remake")))
242 (replace 'check
243 (lambda _
244 (invoke "./remake" "check")))
245 ;; TODO: requires coq-gappa and coq-interval.
246 ;(invoke "./remake" "check-more")
247 (replace 'install
248 (lambda _
249 (invoke "./remake" "install"))))))
250 (home-page "https://flocq.gitlabpages.inria.fr")
251 (synopsis "Floating-point formalization for the Coq system")
252 (description "Flocq (Floats for Coq) is a floating-point formalization for
253the Coq system. It provides a comprehensive library of theorems on a multi-radix
254multi-precision arithmetic. It also supports efficient numerical computations
255inside Coq.")
256 (license license:lgpl3+)))
257
258;; Union of coq and coq-ide-server as vim-coqtail expects coqc and coqidetop
259;; to be in the same bin folder, when vim-coqtail is installed coqc and
260;; coqidetop will be in the "same" bin folder in the profile, so this is only
261;; required for testing the package.
262;;
263;; This is deeply ingrained in the internals of vim-coqtail so this is why
264;; it's necessary.
265(define-public coq-for-coqtail
266 (hidden-package
267 (package
268 (inherit coq)
269 (name "coq-for-coqtail")
270 (source #f)
271 (build-system trivial-build-system)
272 (arguments
273 '(#:modules ((guix build union))
274 #:builder
275 (begin
276 (use-modules (ice-9 match)
277 (guix build union))
278 (match %build-inputs
279 (((names . directories) ...)
280 (union-build (assoc-ref %outputs "out")
281 directories))))))
282 (inputs (list coq coq-ide-server)))))
283
284(define-public coq-gappa
285 (package
286 (name "coq-gappa")
287 (version "1.5.5")
288 (source
289 (origin
290 (method git-fetch)
291 (uri (git-reference
292 (url "https://gitlab.inria.fr/gappa/coq.git")
293 (commit (string-append "gappalib-coq-" version))))
294 (file-name (git-file-name name version))
295 (sha256
296 (base32
297 "0w780wk10khzfx6d633dyzx9q0hvqgimqbzc3irjzvsbpvb0zm5c"))))
298 (build-system gnu-build-system)
299 (native-inputs
300 (list autoconf
301 automake
302 ocaml
303 which
304 coq
305 camlp5
306 bison
307 flex))
308 (inputs
309 (list gmp mpfr boost))
310 (propagated-inputs
311 (list coq-flocq))
312 (arguments
313 `(#:configure-flags
314 (list (string-append "COQUSERCONTRIB=" (assoc-ref %outputs "out")
315 "/lib/coq/user-contrib")
316 (string-append "OCAMLFIND_DESTDIR=" (assoc-ref %outputs "out")
317 "/lib/ocaml/site-lib"))
318 #:phases
319 (modify-phases %standard-phases
320 (add-before 'configure 'fix-remake
321 (lambda _
322 (substitute* "remake.cpp"
323 (("/bin/sh") (which "sh")))
324 #t))
325 (replace 'build
326 (lambda _ (invoke "./remake")))
327 ;; FIXME: Figure out why failures occur, and re-enable check phase.
328 (delete 'check)
329 ;; (replace 'check
330 ;; (lambda _ (invoke "./remake" "check")))
331 (replace 'install
332 (lambda _ (invoke "./remake" "install"))))))
333 (home-page "https://gappa.gitlabpages.inria.fr/")
334 (synopsis "Verify and formally prove properties on numerical programs")
335 (description "Gappa is a tool intended to help verifying and formally proving
336properties on numerical programs dealing with floating-point or fixed-point
337arithmetic. It has been used to write robust floating-point filters for CGAL
338and it is used to certify elementary functions in CRlibm. While Gappa is
339intended to be used directly, it can also act as a backend prover for the Why3
340software verification plateform or as an automatic tactic for the Coq proof
341assistant.")
342 (license (list license:gpl2+ license:cecill))));either gpl2+ or cecill
343
344(define-public coq-mathcomp
345 (package
346 (name "coq-mathcomp")
347 (version "1.19.0")
348 (source
349 (origin
350 (method git-fetch)
351 (uri (git-reference
352 (url "https://github.com/math-comp/math-comp")
353 (commit (string-append "mathcomp-" version))))
354 (file-name (git-file-name name version))
355 (sha256
356 (base32 "0dij9zl2ag083dzgrv2j16ks2kkn2xxwnk1wr5956zw1y7ynrzb3"))))
357 (build-system gnu-build-system)
358 (native-inputs
359 (list ocaml which coq))
360 (arguments
361 `(#:tests? #f ; No tests.
362 #:make-flags (list (string-append "COQLIBINSTALL="
363 (assoc-ref %outputs "out")
364 "/lib/coq/user-contrib"))
365 #:phases
366 (modify-phases %standard-phases
367 (delete 'configure)
368 (add-before 'build 'chdir
369 (lambda _ (chdir "mathcomp") #t)))))
370 (home-page "https://math-comp.github.io/")
371 (synopsis "Mathematical Components for Coq")
372 (description "Mathematical Components for Coq has its origins in the formal
373proof of the Four Colour Theorem. Since then it has grown to cover many areas
374of mathematics and has been used for large scale projects like the formal proof
375of the Odd Order Theorem.
376
377The library is written using the Ssreflect proof language that is an integral
378part of the distribution.")
379 (license license:cecill-b)))
380
381(define-public coq-coquelicot
382 (package
383 (name "coq-coquelicot")
384 (version "3.4.1")
385 (source
386 (origin
387 (method git-fetch)
388 (uri (git-reference
389 (url "https://gitlab.inria.fr/coquelicot/coquelicot.git")
390 (commit (string-append "coquelicot-" version))))
391 (file-name (git-file-name name version))
392 (sha256
393 (base32
394 "1y22dqdklh3c8rbhar0d7mzaj84q6zyfik7namx5q4ma76s2rx73"))))
395 (build-system gnu-build-system)
396 (native-inputs
397 (list autoconf automake ocaml which coq))
398 (propagated-inputs
399 `(("mathcomp" ,coq-mathcomp)))
400 (arguments
401 `(#:configure-flags
402 (list (string-append "COQUSERCONTRIB=" (assoc-ref %outputs "out")
403 "/lib/coq/user-contrib"))
404 #:phases
405 (modify-phases %standard-phases
406 (add-before 'configure 'fix-remake
407 (lambda _
408 (substitute* "remake.cpp"
409 (("/bin/sh") (which "sh")))
410 #t))
411 (replace 'build
412 (lambda _ (invoke "./remake")))
413 (replace 'check
414 (lambda _ (invoke "./remake" "check")))
415 (replace 'install
416 (lambda _ (invoke "./remake" "install"))))))
417 (home-page "http://coquelicot.saclay.inria.fr")
418 (synopsis "Coq library for Reals")
419 (description "Coquelicot is an easier way of writing formulas and theorem
420statements, achieved by relying on total functions in place of dependent types
421for limits, derivatives, integrals, power series, and so on. To help with the
422proof process, the library comes with a comprehensive set of theorems that cover
423not only these notions, but also some extensions such as parametric integrals,
424two-dimensional differentiability, asymptotic behaviors. It also offers some
425automations for performing differentiability proofs. Moreover, Coquelicot is a
426conservative extension of Coq's standard library and provides correspondence
427theorems between the two libraries.")
428 (license license:lgpl3+)))
429
430(define-public coq-bignums
431 (package
432 (name "coq-bignums")
433 (version "9.0.0+coq8.18")
434 (source (origin
435 (method git-fetch)
436 (uri (git-reference
437 (url "https://github.com/coq/bignums")
438 (commit (string-append "v" version))))
439 (file-name (git-file-name name version))
440 (sha256
441 (base32
442 "1vw1a498fhyrpm884rlm3r4lw4mg4l6b9xj8w4y875sacg88kdxw"))))
443 (build-system gnu-build-system)
444 (native-inputs
445 (list ocaml coq))
446 (inputs
447 (list camlp5))
448 (arguments
449 (list #:tests? #f ; No test target.
450 #:make-flags
451 #~(list (string-append "COQLIBINSTALL=" #$output
452 "/lib/coq/user-contrib")
453 (string-append "COQPLUGININSTALL=" #$output
454 "/lib/ocaml/site-lib/"))
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
461provides BigN, BigZ, BigQ that used to be part of Coq standard library.")
462 (license license:lgpl2.1+)))
463
464(define-public coq-interval
465 (package
466 (name "coq-interval")
467 (version "4.10.0")
468 (source
469 (origin
470 (method git-fetch)
471 (uri (git-reference
472 (url "https://gitlab.inria.fr/coqinterval/interval.git")
473 (commit (string-append "interval-" version))))
474 (file-name (git-file-name name version))
475 (sha256
476 (base32
477 "039c29hc8mzp2is6zh9fps36k03hlvx6zz08h03vj6dhjgr7njz8"))))
478 (build-system gnu-build-system)
479 (native-inputs
480 (list autoconf automake ocaml which coq))
481 (propagated-inputs
482 `(("flocq" ,coq-flocq)
483 ("bignums" ,coq-bignums)
484 ("coquelicot" ,coq-coquelicot)
485 ("mathcomp" ,coq-mathcomp)))
486 (arguments
487 `(#:configure-flags
488 (list (string-append "COQUSERCONTRIB=" (assoc-ref %outputs "out")
489 "/lib/coq/user-contrib")
490 (string-append "OCAMLFIND_DESTDIR=" (assoc-ref %outputs "out")
491 "/lib/ocaml/site-lib"))
492 #:phases
493 (modify-phases %standard-phases
494 (add-before 'configure 'fix-remake
495 (lambda _
496 (substitute* "remake.cpp"
497 (("/bin/sh") (which "sh")))
498 #t))
499 (replace 'build
500 (lambda _ (invoke "./remake")))
501 (replace 'check
502 (lambda _ (invoke "./remake" "check")))
503 (replace 'install
504 (lambda _ (invoke "./remake" "install"))))))
505 (home-page "https://coqinterval.gitlabpages.inria.fr/")
506 (synopsis "Coq tactics to simplify inequality proofs")
507 (description "Interval provides vernacular files containing tactics for
508simplifying the proofs of inequalities on expressions of real numbers for the
509Coq proof assistant.")
510 (license license:cecill-c)))
511
512(define-public coq-autosubst
513 (package
514 (name "coq-autosubst")
515 (version "1.8")
516 (source (origin
517 (method git-fetch)
518 (uri (git-reference
519 (url "https://github.com/coq-community/autosubst")
520 (commit (string-append "v" version))))
521 (file-name (git-file-name name version))
522 (sha256
523 (base32 "0qk72r6cqxwhqqkl2kmryhw365w3l2016qii1q1sk3md7zq46jcz"))
524 (patches
525 (search-patches "coq-autosubst-1.8-remove-deprecated-files.patch"))))
526 (build-system gnu-build-system)
527 (arguments
528 `(#:tests? #f
529 #:make-flags (list (string-append "COQLIBINSTALL="
530 (assoc-ref %outputs "out")
531 "/lib/coq/user-contrib"))
532 #:phases
533 (modify-phases %standard-phases
534 (delete 'configure))))
535 (native-inputs
536 (list coq))
537 (home-page "https://www.ps.uni-saarland.de/autosubst/")
538 (synopsis "Coq library for parallel de Bruijn substitutions")
539 (description "Formalizing syntactic theories with variable binders is
540not easy. Autosubst is a library for the Coq proof assistant to
541automate this process. Given an inductive definition of syntactic objects in
542de Bruijn representation augmented with binding annotations, Autosubst
543synthesizes the parallel substitution operation and automatically proves the
544basic lemmas about substitutions. This library contains an automation
545tactic that solves equations involving terms and substitutions. This makes the
546usage of substitution lemmas unnecessary. The tactic is based on our current
547work on a decision procedure for the equational theory of an extension of the
548sigma-calculus by Abadi et al. The library is completely written in Coq and
549uses Ltac to synthesize the substitution operation.")
550 (license license:bsd-3)))
551
552(define-public coq-equations
553 (package
554 (name "coq-equations")
555 (version "1.3-8.18")
556 (source (origin
557 (method git-fetch)
558 (uri (git-reference
559 (url "https://github.com/mattam82/Coq-Equations")
560 (commit (string-append "v" version))))
561 (file-name (git-file-name name version))
562 (sha256
563 (base32
564 "1akxf2vafwyz6fi1djlc3g8mwxrjv0a99x4b08jwrbwxypv4xiph"))))
565 (build-system gnu-build-system)
566 (native-inputs
567 (list ocaml coq camlp5))
568 (arguments
569 (list #:test-target "test-suite"
570 #:make-flags #~(list (string-append "COQLIBINSTALL="
571 #$output
572 "/lib/coq/user-contrib")
573 (string-append "COQPLUGININSTALL="
574 #$output
575 "/lib/ocaml/site-lib/"))
576 #:phases
577 #~(modify-phases %standard-phases
578 (replace 'configure
579 (lambda* (#:key outputs #:allow-other-keys)
580 (invoke "sh" "./configure.sh"))))))
581 (home-page "https://mattam82.github.io/Coq-Equations/")
582 (synopsis "Function definition plugin for Coq")
583 (description "Equations provides a notation for writing programs
584by dependent pattern-matching and (well-founded) recursion in Coq. It
585compiles everything down to eliminators for inductive types, equality
586and accessibility, providing a definitional extension to the Coq
587kernel.")
588 (license license:lgpl2.1)))
589
590(define-public coq-semantics
591 (package
592 (name "coq-semantics")
593 (version "8.14.0")
594 (source
595 (origin
596 (method git-fetch)
597 (uri (git-reference
598 (url "https://github.com/coq-community/semantics")
599 (commit (string-append "v" version))))
600 (modules '((guix build utils)))
601 (snippet
602 '(substitute* "Makefile.coq.local"
603 ;; Num was part of OCaml and now external
604 (("-libs nums") "-use-ocamlfind -pkg num -libs num")))
605 (file-name (git-file-name name version))
606 (sha256
607 (base32
608 "0ldrp86bfcjpzsb08p45sgs3aczjzr1gksy5dsf7pxapg05pc7ac"))))
609 (build-system gnu-build-system)
610 (native-inputs
611 (list coq ocaml ocamlbuild ocaml-findlib))
612 (inputs
613 (list ocaml-num))
614 (arguments
615 `(#:tests? #f ;included in Makefile
616 #:make-flags (list (string-append "COQLIBINSTALL="
617 (assoc-ref %outputs "out")
618 "/lib/coq/user-contrib"))
619 #:phases
620 (modify-phases %standard-phases
621 (delete 'configure))))
622 (home-page "https://github.com/coq-community/semantics")
623 (synopsis "Survey of semantics styles")
624 (description
625 "This package provides a survey of programming language semantics styles,
626from natural semantics through structural operational, axiomatic, and
627denotational semantics, for a miniature example of an imperative programming
628language. Their encoding, the proofs of equivalence of different styles,
629abstract interpretation, and the proof of soundess obtained from axiomatic
630semantics or abstract interpretation is done in Coq. The tools can be run
631inside Coq, thus making them available for proof by reflection. Code can also
632be extracted and connected to a yacc-based parser, thanks to the use of a
633functor parameterized by a module type of strings. A hand-written parser is
634also provided in Coq, without associated proofs.")
635 (license license:expat)))
636
637(define-public coq-stdpp
638 (package
639 (name "coq-stdpp")
640 (version "1.10.0")
641 (synopsis "Alternative Coq standard library std++")
642 (source (origin
643 (method git-fetch)
644 (uri (git-reference
645 (url "https://gitlab.mpi-sws.org/iris/stdpp.git")
646 (commit (string-append "coq-stdpp-" version))))
647 (file-name (git-file-name name version))
648 (sha256
649 (base32
650 "0lnvdfn4qq2lyabiq4ikb5ya46f4jp59dynyprnhki0ay9xagz3d"))))
651 (build-system gnu-build-system)
652 (inputs
653 (list coq))
654 (arguments
655 `(#:tests? #f ; Tests are executed during build phase.
656 #:make-flags (list (string-append "COQLIBINSTALL="
657 (assoc-ref %outputs "out")
658 "/lib/coq/user-contrib"))
659 #:phases
660 (modify-phases %standard-phases
661 (delete 'configure))))
662 (description "This project contains an extended \"Standard Library\" for
663Coq called coq-std++. The key features are:
664@itemize
665@item Great number of definitions and lemmas for common data structures such
666as lists, finite maps, finite sets, and finite multisets.
667
668@item Type classes for common notations (like ∅, ∪, and Haskell-style monad
669notations) so that these can be overloaded for different data structures.
670
671@item It uses type classes to keep track of common properties of types, like
672it having decidable equality or being countable or finite.
673
674@item Most data structures are represented in canonical ways so that Leibniz
675equality can be used as much as possible (for example, for maps we have m1 =
676m2 iff ∀ i, m1 !! i = m2 !! i). On top of that, the library provides setoid
677instances for most types and operations.
678
679@item Various tactics for common tasks, like an ssreflect inspired done tactic
680for finishing trivial goals, a simple breadth-first solver naive_solver, an
681equality simplifier simplify_eq, a solver solve_proper for proving
682compatibility of functions with respect to relations, and a solver set_solver
683for goals involving set operations.
684
685@item The library is dependency- and axiom-free.
686@end itemize")
687 (home-page "https://gitlab.mpi-sws.org/iris/stdpp")
688 (license license:bsd-3)))
689
690(define-public coq-mathcomp-finmap
691 (package
692 (name "coq-mathcomp-finmap")
693 (version "1.5.2")
694 (source (origin
695 (method git-fetch)
696 (uri (git-reference
697 (url "https://github.com/math-comp/finmap")
698 (commit version)))
699 (file-name (git-file-name name version))
700 (sha256
701 (base32
702 "1k72wpp15xa5ag358jl8a71gschng0bgbaqjx0l5a0in6x5adafh"))))
703 (build-system gnu-build-system)
704 (arguments
705 `(;; No tests supplied in Makefile.common.
706 ;; The project doesn't appear to have plans to include tests in
707 ;; the future.
708 #:tests? #f
709 #:make-flags (list (string-append "COQLIBINSTALL="
710 (assoc-ref %outputs "out")
711 "/lib/coq/user-contrib"))
712 #:phases (modify-phases %standard-phases
713 (delete 'configure))))
714 (inputs (list coq coq coq-mathcomp which))
715 (synopsis "Finite sets and finite types for coq-mathcomp")
716 (description
717 "This library is an extension of coq-mathcomp which supports finite sets
718and finite maps on choicetypes (rather than finite types). This includes
719support for functions with finite support and multisets. The library also
720contains a generic order and set library, which will eventually be used to
721subsume notations for finite sets.")
722 (home-page "https://math-comp.github.io/")
723 (license license:cecill-b)))
724
725(define-public coq-mathcomp-bigenough
726 (package
727 (name "coq-mathcomp-bigenough")
728 (version "1.0.1")
729 (source (origin
730 (method git-fetch)
731 (uri (git-reference
732 (url "https://github.com/math-comp/bigenough")
733 (commit version)))
734 (file-name (git-file-name name version))
735 (sha256
736 (base32
737 "02f4dv4rz72liciwxb2k7acwx6lgqz4381mqyq5854p3nbyn06aw"))))
738 (build-system gnu-build-system)
739 (arguments
740 (list ;; No references to tests in Makefile.common.
741 ;; It doesn't appear as though tests will be included
742 ;; by the packaged project in the future.
743 #:tests? #f
744 #:make-flags
745 #~(list (string-append "COQLIBINSTALL=" #$output
746 "/lib/coq/user-contrib"))
747 #:phases
748 #~(modify-phases %standard-phases
749 (delete 'configure))))
750 (native-inputs (list coq which))
751 (propagated-inputs (list coq-mathcomp))
752 (home-page "https://math-comp.github.io/")
753 (synopsis "Small library to do epsilon - N reasoning")
754 (description
755 "The package is used for reasoning with big enough objects (mostly
756natural numbers). This package is essentially for backward compatibility
757purposes as @code{bigenough} will be subsumed by the near tactics. The
758formalization is based on the Mathematical Components library.")
759 (license license:cecill-b)))