Date: Sat, 16 Oct 2004 00:55:33 +0000 (UTC) From: Pav Lucistnik <pav@FreeBSD.org> To: ports-committers@FreeBSD.org, cvs-ports@FreeBSD.org, cvs-all@FreeBSD.org Subject: cvs commit: ports/math Makefile ports/math/coq Makefile distinfo pkg-descr pkg-plist Message-ID: <200410160055.i9G0tX09038494@repoman.freebsd.org>
next in thread | raw e-mail | index | archive | help
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@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)
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?200410160055.i9G0tX09038494>