| CARVIEW |
Select Language
HTTP/2 200
expires: Thu, 19 Nov 1981 08:52:00 GMT
cache-control: no-store, no-cache, must-revalidate
pragma: no-cache
set-cookie: PHPSESSID=m6pghdau1q3umb7k44n0olbers; path=/
content-type: text/html; charset=UTF-8
date: Sat, 27 Dec 2025 22:18:58 GMT
server: Apache
pkgsrc.se | The NetBSD package collection
archivers
audio
benchmarks
biology
cad
chat
comms
converters
cross
crosspkgtools
databases
devel
doc
editors
emulators
filesystems
finance
fonts
games
geography
graphics
ham
inputmethod
lang
coq
mail
math
mbone
meta-pkgs
misc
multimedia
net
news
parallel
pkgtools
print
regress
security
shells
sysutils
textproc
time
wip
wm
www
x11
* = Virtual Category
Path to this page:
./lang/coq, Theorem prover which extracts programs from proofs
[
Branch: CURRENT, Version: 8.20.1nb4, Package name: coq-8.20.1nb4, Maintainer: dholland
From https://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.
Required to run:
[lang/ocaml] [x11/gtk3] [graphics/adwaita-icon-theme] [math/ocaml-num] [lang/python37] [x11/ocaml-lablgtk3]
Required to build:
[pkgtools/x11-links] [x11/xcb-proto] [x11/fixesproto4] [pkgtools/cwrappers] [x11/xorgproto]
Package options: coqide
Navigation:
-
Browse pkgsrc
(this page)
archivers
audio
benchmarks
biology
cad
chat
comms
converters
cross
crosspkgtools
databases
devel
doc
editors
emulators
filesystems
finance
fonts
games
geography
graphics
ham
inputmethod
lang coqmath
mbone
meta-pkgs
misc
multimedia
net
news
parallel
pkgtools
regress
security
shells
sysutils
textproc
time
wip
wm
www
x11
* = Virtual Category
New packages:Path to this page:
./lang/coq, Theorem prover which extracts programs from proofs
[ 
CVSweb ] [ 
Homepage ] [ 
RSS ] [ 
Required by ] [ 
Add to tracker ]
Branch: CURRENT, Version: 8.20.1nb4, Package name: coq-8.20.1nb4, Maintainer: dholland
From https://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.
Required to run:
[lang/ocaml] [x11/gtk3] [graphics/adwaita-icon-theme] [math/ocaml-num] [lang/python37] [x11/ocaml-lablgtk3]
Required to build:
[pkgtools/x11-links] [x11/xcb-proto] [x11/fixesproto4] [pkgtools/cwrappers] [x11/xorgproto]
Package options: coqide
Master sites:
Filesize: 7659.109 KBVersion history: (Expand)
- (2025-10-24) Updated to version: coq-8.20.1nb4
- (2025-08-31) Updated to version: coq-8.20.1nb3
- (2025-07-15) Package has been reborn
- (2025-07-15) Package deleted from pkgsrc
- (2025-04-24) Updated to version: coq-8.20.1nb2
- (2025-04-23) Updated to version: coq-8.20.1nb1
CVS history: (Expand)
| 2025-10-23 22:40:24 by Thomas Klausner | Files touched by this commit (2999) |
Log message: *: recursive bump for pcre2 Running an old binary against the new pcre doesn't work: /usr/pkg/lib/libpcre2-8.so.0: version PCRE2_10.47 required by \ /usr/pkg/lib/libglib-2.0.so.0 not defined |
| 2025-10-09 09:58:14 by Thomas Klausner | Files touched by this commit (442) |
Log message: *: remove reference to (removed) Python 3.9 |
| 2025-08-31 00:46:51 by Thomas Klausner | Files touched by this commit (1355) |
Log message: *: recursive bump for tiff growing lerc dependency |
| 2025-07-07 05:04:04 by David A. Holland | Files touched by this commit (1) |
Log message: lang/coq: typo in comment |
| 2025-04-24 16:16:37 by Thomas Klausner | Files touched by this commit (2412) |
Log message: *: recursive bump for jpeg -> libjpeg-turbo switch |
| 2025-04-17 23:53:13 by Thomas Klausner | Files touched by this commit (2449) |
Log message: *: recursive bump for icu 77 and libxml2 2.14 |
| 2025-03-03 10:29:21 by Thomas Klausner | Files touched by this commit (1) |
Log message: coq: remove REPLACE_* with no effect |
2025-02-24 04:41:03 by David A. Holland | Files touched by this commit (7) |  |
Log message:
lang/coq: update to 8.20.1
pkgsrc changes: g/c obsolete patches; update build mechanism.
*** Note:
***
*** Because of upstream build changes, the stdlib files have moved:
*** ${PREFIX}/lib/coq/theories
*** ==>
*** ${PREFIX}/lib/ocaml/site-lib/coq/theories
***
*** This package includes a symlink in the old location; future
*** versions might not.
Upstream changes since 8.15.2:
...way too many to paste here since it's been way too long since the
last update.
See https://coq.inria.fr/doc/v8.20/refman/changes.html.
|