BSD Portslang/coq 8.20.1nb10 NetBSD
Theorem prover which extracts programs from proofs
- System
- NetBSD
- Repository
- pkgsrc
- Maintainer
- [email protected]
- Last update
- Commit
7b5a3977f9- License
- gnu-lgpl-v2.1
- Categories
- lang, math
- Package size
- 169443.8 KiB, 726823.7 KiB installed
Description
From http://coq.inria.fr/doc/tutorial.html:
Coq is a Proof Assistant for a Logical Framework known as the
Calculus of Inductive Constructions. It allows the interactive
construction of formal proofs, and also the manipulation of
functional programs consistently with their specifications.
In the other systems
| System | Port | Version |
|---|---|---|
| NetBSD | lang/coq | 8.20.1nb10 |
| FreeBSD | math/coq | 8.20.1_3,3 |
| GhostBSD | math/coq | 8.20.1_3,3 |
Install
Binary package:
pkgin install coqFrom pkgsrc:
cd /usr/pkgsrc/lang/coq && make install cleanPackages
The version each package repository carries. “-” means the repository builds no package of it, “n/a” that there is no such repository.
| Repository | Version |
|---|---|
| NetBSD 10.1 x86_64 | 8.20.1nb10 |
| NetBSD 10.1 aarch64 | - |
| SmartOS / illumos x86_64 | - |
| macOS 15 arm64 | - |