| Port details |
- coq Theorem prover based on lambda-C
- 8.20.1_3,3 math
 =1      8.20.1_3,3Version of this port present on the latest quarterly branch. - There is no maintainer for this port.
- Any concerns regarding this port should be directed to the FreeBSD Ports mailing list via ports@FreeBSD.org
- Port Added: 2004-10-16 01:04:52
- Last Update: 2026-03-26 01:07:07
- Commit Hash: dbcf335
- People watching this port, also watch:: ocaml-lwt, osslsigncode
- License: LGPL21
- WWW:
- https://coq.inria.fr/
- Description:
- Developed in the LogiCal project, the Coq tool is a formal proof
management system: a proof done with Coq is mechanically checked
by the machine.
In particular, Coq allows:
* the definition of functions or predicates,
* to state mathematical theorems and software specifications,
* to develop interactively formal proofs of these theorems,
* to check these proofs by a small certification "kernel".
Coq is based on a logical framework called "Calculus of Inductive
Constructions" extended by a modular development system for
theories.
CoqIde is installed if the x11-toolkits/ocaml-lablgtk2 port is installed.
  ¦  ¦  ¦  ¦ 
- Manual pages:
-
- pkg-plist: as obtained via:
make generate-plist - USE_RC_SUBR (Service Scripts)
- no SUBR information found for this port
- Dependency lines:
-
- Conflicts:
- CONFLICTS_INSTALL:
- To install the port:
- cd /usr/ports/math/coq/ && make install clean
- To add the package, run one of these commands:
- pkg install math/coq
- pkg install coq
NOTE: If this package has multiple flavors (see below), then use one of them instead of the name specified above.- PKGNAME: coq
- Flavors: there is no flavor information for this port.
- distinfo:
- TIMESTAMP = 1739496231
SHA256 (coq-coq-V8.20.1_GH0.tar.gz) = 09ad238cc7930d59564b032be2a8a1fd10d6ef845364d739072d04090a6d3cc2
SIZE (coq-coq-V8.20.1_GH0.tar.gz) = 7842928
Packages (timestamps in pop-ups are UTC):
- Dependencies
- NOTE: FreshPorts displays only information on required and default dependencies. Optional dependencies are not covered.
- Build dependencies:
-
- META : math/ocaml-num
- META : math/ocaml-zarith
- bash : shells/bash
- camlp5 : devel/ocaml-camlp5
- META : x11-toolkits/ocaml-lablgtk3
- gettext-runtime>=0.26 : devel/gettext-runtime
- gmake>=4.4.1 : devel/gmake
- ocaml-dune>=3.7.1_2 : devel/ocaml-dune
- ocamlc : lang/ocaml
- camlp4 : devel/ocaml-camlp4
- Runtime dependencies:
-
- META : math/ocaml-num
- META : math/ocaml-zarith
- META : x11-toolkits/ocaml-lablgtk3
- ocamlc : lang/ocaml
- Library dependencies:
-
- libfontconfig.so : x11-fonts/fontconfig
- libfreetype.so : print/freetype2
- libgmp.so : math/gmp
- libharfbuzz.so : print/harfbuzz
- libintl.so : devel/gettext-runtime
- libatk-1.0.so : accessibility/at-spi2-core
- libcairo.so : graphics/cairo
- libgdk_pixbuf-2.0.so : graphics/gdk-pixbuf2
- libglib-2.0.so : devel/glib20
- libintl.so : devel/gettext-runtime
- libgtk-3.so : x11-toolkits/gtk30
- libgtksourceview-3.0.so : x11-toolkits/gtksourceview3
- libxml2.so : textproc/libxml2
- libharfbuzz.so : print/harfbuzz
- libpango-1.0.so : x11-toolkits/pango
- Patch dependencies:
-
- ocamlc : lang/ocaml
-
- There are no ports dependent upon this port
Configuration Options:- ===> The following configuration options are available for coq-8.20.1_3,3:
DOCS=on: Build and/or install documentation
IDE=on: Include desktop environment (coqide)
===> Use 'make config' to modify these settings
- Options name:
- math_coq
- USES:
- gettext-runtime gmake gnome ocaml:camlp4,dune,ldconfig python:env shebangfix tex
- FreshPorts was unable to extract/find any pkg message
- Master Sites:
|
| Notes from UPDATING |
- These upgrade notes are taken from /usr/ports/UPDATING
- 2026-03-25
Affects: users of math/coq Author: jrm@FreeBSD.org Reason:
Upstream no longer installs Emacs lisp, so the Emacs flavors have been
removed. In order for a `pkg upgrade` to install new versions of coq,
any installed package for a non-default flavor must be renamed. Do
this by running the commands below under /bin/sh with superuser
privileges:
on=$(pkg query -g %n coq-emacs_*)
nn=$(pkg query -g %n g coq-emacs_* | sed -e 's/-emacs_[a-z_]*//')
pkg set -n "$on":"$nn"
|
Number of commits found: 107 (showing only 7 on this page)
| Commit History - (may be incomplete: for full details, see links to repositories near top of page) |
| Commit | Credits | Log message |
|---|
8.0p2
29 Oct 2005 20:14:47
  |
mnag |
Drop MAINTAINER
PR: 88197
Submitted by: Rene Ladan <r.c.ladan@student.tue.nl> (maintainer) |
8.0p2
02 Feb 2005 11:34:42
|
vs |
Update to 8.0p2
PR: ports/76977
Submitted by: Rene Laden (maintainer) |
8.0p1
18 Jan 2005 16:44:23
|
vs |
Fix packaging
PR: ports/75787
Submitted by: maintainer |
8.0p1
20 Dec 2004 21:37:52
|
sem |
- Unbreak on amd64
(Johan van Selst succesfully ran the test-suite
on an amd64 running 6-CURRENT and ocaml-3.08.2)
PR: ports/75334
Submitted by: maintainer |
8.0p1
29 Nov 2004 09:34:20
|
tobez |
Mark broken on ia64 and amd64.
PR: 74502
Submitted by: maintainer |
8.0p1
08 Nov 2004 21:57:29
|
pav |
- Add optional CoqIde support (depends on lablgtk2)
- Correct PORTVERSION to match actual source version
- Cosmetics
PR: ports/73634
Submitted by: Rene Ladan <r.c.ladan@student.tue.nl> (maintainer) |
8.0
16 Oct 2004 00:55:33
|
pav |
Add coq, a formal proof management system: a proof done with Coq is
mechanically checked by the machine.
In particular, Coq allows:
* the definition of functions or predicates,
* to state mathematical theorems and software specifications,
* to develop interactively formal proofs of these theorems,
* to check these proofs by a small certification "kernel".
PR: ports/72718
Submitted by: Rene Ladan <r.c.ladan@student.tue.nl> |
Number of commits found: 107 (showing only 7 on this page)
|
As an Amazon Associate I earn from qualifying purchases.