coq 8.1.3_2 math =1

Theorem prover based on lambda-C
Maintained by: johans@stack.nl
Port Added: 16 Oct 2004 02:04:52

---

---

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 <r.c.ladan@student.tue.nl>
WWW:    http://coq.inria.fr/

CVSWeb : Sources : Main Web Site : Distfiles Availability : PortsMon

---

Required To Build: devel/ocaml-camlp5, lang/ocaml, x11-toolkits/ocaml-lablgtk2, devel/gmake
Required To Run: lang/ocaml, devel/ocaml-camlp5, lang/ocaml, x11-toolkits/ocaml-lablgtk2, devel/gmake

---

To install the port: cd /usr/ports/math/coq/ && make install clean
To add the package: pkg_add -r coq

---

Configuration Options

     No options to configure

---

Master Sites:

http://coq.inria.fr/V8.1pl3/files/

ftp://ftp.stack.nl/pub/users/johans/coq/

ftp://ftp.FreeBSD.org/pub/FreeBSD/ports/distfiles/

Bump portrevision due to upgrade of devel/gettext.

The affected ports are the ones with gettext as a run-dependency
according to ports/INDEX-7 (5007 of them) and the ones with USE_GETTEXT
in Makefile (29 of them).

PR:             ports/124340
Submitted by:   edwin@
Approved by:    portmgr (pav)

- Due to depency updates, camlp5 (fresh port) is now required as well:
  Include this dependency and bump portrevision

- Update to 8.1pl3
- Take advantage of USE_OCAML
- Update MASTER_SITES

Update to 8.1.1  (bugfix release)

- Welcome X.org 7.2 \o/.
- Set X11BASE to ${LOCALBASE} for recent ${OSVERSION}.
- Bump PORTREVISION for ports intalling files in ${X11BASE}.

- Update to 8.1
- Grab maintainership
- Remove FreeBSD-specific workaround that shouldn't be needed anymore

- Update to 8.0pl3

PR:             ports/93954
Submitted by:   Johan van Selst <johans@stack.nl>

BROKEN: Does not build

Approved by:    portmgr (implicit)

Replace ugly "@unexec rmdir %D... 2>/dev/null || true" with @dirrmtry

Approved by:    krion@
PR:             ports/88711 (related)

Unbreak: Add vendor-patch for ocaml 3.09

Bump PORTREVISION to regenerate the package with the newly enabled IDE on the
cluster

Suggested by: kris

Enable IDE by default.

- Add SHA256

Drop MAINTAINER

PR:             88197
Submitted by:   Rene Ladan <r.c.ladan@student.tue.nl> (maintainer)

Update to 8.0p2

PR:             ports/76977
Submitted by:   Rene Laden (maintainer)

Fix packaging

PR:             ports/75787
Submitted by:   maintainer

- 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

Mark broken on ia64 and amd64.

PR:             74502
Submitted by:   maintainer

- 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)

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>

3 vulnerabilities affecting 4 ports have been reported in the past 14 days

^* - modified, not new

All vulnerabilities