The FreeBSD Ports Archive
FreeBSD math  : coq
Theorem prover based on lambda-C
From the website:
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.
Coq is distributed under the GNU Lesser General Public Licence
Version 2.1 (LGPL).
CoqIde is installed if the x11-toolkits/ocaml-lablgtk2 port is installed.
Author: Rene Ladan
http://coq.inria.fr/
|
coq history
v. 1.15
date: 2007/07/30 07:36:01; author: johans; state: Exp; lines: +5 -3
Update to 8.1.1 (bugfix release)
v. 1.14
date: 2007/05/19 20:14:52; author: flz; state: Exp; lines: +1 -0
- Welcome X.org 7.2 \o/.
- Set X11BASE to ${LOCALBASE} for recent ${OSVERSION}.
- Bump PORTREVISION for ports intalling files in ${X11BASE}.
v. 1.13
date: 2007/03/25 18:44:33; author: johans; state: Exp; lines: +6 -7
- Update to 8.1
- Grab maintainership
- Remove FreeBSD-specific workaround that shouldn't be needed anymore
v. 1.12
date: 2006/03/16 15:31:23; author: pav; state: Exp; lines: +6 -8
- Update to 8.0pl3
PR: ports/93954
Submitted by: Johan van Selst
v. 1.11
date: 2006/03/06 20:30:52; author: kris; state: Exp; lines: +2 -0
BROKEN: Does not build
Approved by: portmgr (implicit)
v. 1.10
date: 2005/12/07 15:59:14; author: vs; state: Exp; lines: +2 -0
Unbreak: Add vendor-patch for ocaml 3.09
v. 1.9
date: 2005/12/05 09:49:23; author: vs; state: Exp; lines: +1 -0
Bump PORTREVISION to regenerate the package with the newly enabled IDE on the cluster
Suggested by: kris
v. 1.8
date: 2005/12/05 09:16:08; author: vs; state: Exp; lines: +3 -3
Enable IDE by default.
v. 1.7
date: 2005/10/29 20:14:47; author: mnag; state: Exp; lines: +1 -1
Drop MAINTAINER
PR: 88197
Submitted by: Rene Ladan (maintainer)
v. 1.6
date: 2005/02/02 11:34:42; author: vs; state: Exp; lines: +3 -6
Update to 8.0p2
PR: ports/76977
Submitted by: Rene Laden (maintainer)
v. 1.5
date: 2005/01/18 16:44:23; author: vs; state: Exp; lines: +3 -1
Fix packaging
PR: ports/75787
Submitted by: maintainer
v. 1.4
date: 2004/12/20 21:37:52; author: sem; state: Exp; lines: +1 -2
- 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
v. 1.3
date: 2004/11/29 09:34:20; author: tobez; state: Exp; lines: +4 -0
Mark broken on ia64 and amd64.
PR: 74502
Submitted by: maintainer
v. 1.2
date: 2004/11/08 21:57:29; author: pav; state: Exp; lines: +16 -7
- Add optional CoqIde support (depends on lablgtk2)
- Correct PORTVERSION to match actual source version
- Cosmetics
PR: ports/73634
Submitted by: Rene Ladan (maintainer)
v. 1.1
date: 2004/10/16 00:55:32; author: pav; state: Exp;
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
=============================================================================
v. 1.15
date: 2007/07/30 07:36:01; author: johans; state: Exp; lines: +5 -3
Update to 8.1.1 (bugfix release)
v. 1.14
date: 2007/05/19 20:14:52; author: flz; state: Exp; lines: +1 -0
- Welcome X.org 7.2 \o/.
- Set X11BASE to ${LOCALBASE} for recent ${OSVERSION}.
- Bump PORTREVISION for ports intalling files in ${X11BASE}.
v. 1.13
date: 2007/03/25 18:44:33; author: johans; state: Exp; lines: +6 -7
- Update to 8.1
- Grab maintainership
- Remove FreeBSD-specific workaround that shouldn't be needed anymore
v. 1.12
date: 2006/03/16 15:31:23; author: pav; state: Exp; lines: +6 -8
- Update to 8.0pl3
PR: ports/93954
Submitted by: Johan van Selst
v. 1.11
date: 2006/03/06 20:30:52; author: kris; state: Exp; lines: +2 -0
BROKEN: Does not build
Approved by: portmgr (implicit)
v. 1.10
date: 2005/12/07 15:59:14; author: vs; state: Exp; lines: +2 -0
Unbreak: Add vendor-patch for ocaml 3.09
v. 1.9
date: 2005/12/05 09:49:23; author: vs; state: Exp; lines: +1 -0
Bump PORTREVISION to regenerate the package with the newly enabled IDE on the cluster
Suggested by: kris
v. 1.8
date: 2005/12/05 09:16:08; author: vs; state: Exp; lines: +3 -3
Enable IDE by default.
v. 1.7
date: 2005/10/29 20:14:47; author: mnag; state: Exp; lines: +1 -1
Drop MAINTAINER
PR: 88197
Submitted by: Rene Ladan (maintainer)
v. 1.6
date: 2005/02/02 11:34:42; author: vs; state: Exp; lines: +3 -6
Update to 8.0p2
PR: ports/76977
Submitted by: Rene Laden (maintainer)
v. 1.5
date: 2005/01/18 16:44:23; author: vs; state: Exp; lines: +3 -1
Fix packaging
PR: ports/75787
Submitted by: maintainer
v. 1.4
date: 2004/12/20 21:37:52; author: sem; state: Exp; lines: +1 -2
- 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
v. 1.3
date: 2004/11/29 09:34:20; author: tobez; state: Exp; lines: +4 -0
Mark broken on ia64 and amd64.
PR: 74502
Submitted by: maintainer
v. 1.2
date: 2004/11/08 21:57:29; author: pav; state: Exp; lines: +16 -7
- Add optional CoqIde support (depends on lablgtk2)
- Correct PORTVERSION to match actual source version
- Cosmetics
PR: ports/73634
Submitted by: Rene Ladan (maintainer)
v. 1.1
date: 2004/10/16 00:55:32; author: pav; state: Exp;
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
=============================================================================
v. 1.15
date: 2007/07/30 07:36:01; author: johans; state: Exp; lines: +5 -3
Update to 8.1.1 (bugfix release)
v. 1.14
date: 2007/05/19 20:14:52; author: flz; state: Exp; lines: +1 -0
- Welcome X.org 7.2 \o/.
- Set X11BASE to ${LOCALBASE} for recent ${OSVERSION}.
- Bump PORTREVISION for ports intalling files in ${X11BASE}.
v. 1.13
date: 2007/03/25 18:44:33; author: johans; state: Exp; lines: +6 -7
- Update to 8.1
- Grab maintainership
- Remove FreeBSD-specific workaround that shouldn't be needed anymore
v. 1.12
date: 2006/03/16 15:31:23; author: pav; state: Exp; lines: +6 -8
- Update to 8.0pl3
PR: ports/93954
Submitted by: Johan van Selst
v. 1.11
date: 2006/03/06 20:30:52; author: kris; state: Exp; lines: +2 -0
BROKEN: Does not build
Approved by: portmgr (implicit)
v. 1.10
date: 2005/12/07 15:59:14; author: vs; state: Exp; lines: +2 -0
Unbreak: Add vendor-patch for ocaml 3.09
v. 1.9
date: 2005/12/05 09:49:23; author: vs; state: Exp; lines: +1 -0
Bump PORTREVISION to regenerate the package with the newly enabled IDE on the cluster
Suggested by: kris
v. 1.8
date: 2005/12/05 09:16:08; author: vs; state: Exp; lines: +3 -3
Enable IDE by default.
v. 1.7
date: 2005/10/29 20:14:47; author: mnag; state: Exp; lines: +1 -1
Drop MAINTAINER
PR: 88197
Submitted by: Rene Ladan (maintainer)
v. 1.6
date: 2005/02/02 11:34:42; author: vs; state: Exp; lines: +3 -6
Update to 8.0p2
PR: ports/76977
Submitted by: Rene Laden (maintainer)
v. 1.5
date: 2005/01/18 16:44:23; author: vs; state: Exp; lines: +3 -1
Fix packaging
PR: ports/75787
Submitted by: maintainer
v. 1.4
date: 2004/12/20 21:37:52; author: sem; state: Exp; lines: +1 -2
- 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
v. 1.3
date: 2004/11/29 09:34:20; author: tobez; state: Exp; lines: +4 -0
Mark broken on ia64 and amd64.
PR: 74502
Submitted by: maintainer
v. 1.2
date: 2004/11/08 21:57:29; author: pav; state: Exp; lines: +16 -7
- Add optional CoqIde support (depends on lablgtk2)
- Correct PORTVERSION to match actual source version
- Cosmetics
PR: ports/73634
Submitted by: Rene Ladan (maintainer)
v. 1.1
date: 2004/10/16 00:55:32; author: pav; state: Exp;
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
=============================================================================
|
| |
|