coq 8.3.2_1,1 math =1

Theorem prover based on lambda-C
Maintained by: johans@FreeBSD.org
Port Added: 16 Oct 2004 01:04:52
License: not specified in port

---

---

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

---

NOTE: FreshPorts displays only required dependencies information. Optional dependencies are not covered.
Required To Build: devel/ocaml-camlp5, textproc/hevea, print/teTeX, print/latex-ucs, lang/ocaml, x11-toolkits/ocaml-lablgtk2, devel/gmake
Required To Run: lang/ocaml, devel/ocaml-camlp5, textproc/hevea, print/teTeX, print/latex-ucs, lang/ocaml, x11-toolkits/ocaml-lablgtk2, devel/gmake
There are no ports dependent upon this port

---

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/distrib/V8.3pl2/files/

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

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

Mark as broken on powerpc: fails to link.

Hat:            portmgr
Feature safe:   yes

Bump PORTREVISION after open-mofit update

Update coq to 8.3.2

Correct PORTVERSION: pl (patch level) releases follow a main release

Reported by:            erwin

- Update coq to 8.3pl1
- Remove obsoleted patch (fixed in dist)

Fix build with new ocaml preprocessor (patch from upstream)

Reported by:    pointyhat via pav

- Update coq to 8.3
- Add a patch to fix threading issues

Submitted by:   AUGER Cedric <Cedric.Auger@lri.fr>

- Update to version 8.2pl1
- Bump EPOCH due to different versioning style
- Build and install documentation

PR:             ports/148034
Submitted by:   Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>
Feature safe:   yes

- update to 1.4.1
Reviewed by:    exp8 run on pointyhat
Supported by:   miwi

Update my mail address to @FreeBSD.org

Feature safe:   yes

- update to jpeg-8

- bump all port that indirectly depends on libjpeg and have not yet been bumped
or updated
Requested by:   edwin

Fix pkg-plist

Reported by:    QAT

Update to 8.2.1

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>

17 vulnerabilities affecting 41 ports have been reported in the past 14 days

^* - modified, not new

All vulnerabilities