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