cvs commit: ports/math Makefile ports/math/coq Makefile distinfo
pkg-descr pkg-plist
Pav Lucistnik
pav at FreeBSD.org
Fri Oct 15 17:55:33 PDT 2004
pav 2004-10-16 00:55:33 UTC
FreeBSD ports repository
Modified files:
math Makefile
Added files:
math/coq Makefile distinfo pkg-descr pkg-plist
Log:
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 at student.tue.nl>
Revision Changes Path
1.288 +1 -0 ports/math/Makefile
1.1 +46 -0 ports/math/coq/Makefile (new)
1.1 +4 -0 ports/math/coq/distinfo (new)
1.1 +23 -0 ports/math/coq/pkg-descr (new)
1.1 +524 -0 ports/math/coq/pkg-plist (new)
More information about the cvs-ports
mailing list