Menu
▾
▴
[cvs] dists/10.4/unstable/main/finkinfo/sci coq.info, NONE, 1.1 coq.patch, NONE, 1.1 coqide.info, NONE, 1.1 coqide.patch, NONE, 1.1
|
From: Alexander H. <ale...@us...> - 2006-09-18 20:16:06
|
Update of /cvsroot/fink/dists/10.4/unstable/main/finkinfo/sci In directory sc8-pr-cvs5.sourceforge.net:/tmp/cvs-serv2656 Added Files: coq.info coq.patch coqide.info coqide.patch Log Message: New from tracker (#'s 1504487 and 1504488) --- NEW FILE: coqide.info --- Package: coqide Version: 8.0pl3 Revision: 1 Source: ftp://ftp.inria.fr/INRIA/coq/V%v/coq-%v.tar.gz Source-MD5: c98d4cefd119accb1ecdeebb41128822 Maintainer: Jesse Alama <al...@st...> HomePage: http://coq.inria.fr/ License: LGPL DocFiles: CHANGES COPYRIGHT CREDITS LICENSE README README.fink Description: Interactive development environment for Coq BuildDepends: ocaml (>=3.09), lablgtk2 (>=2.4.0), gtk+2-dev, pango1-xft2-dev, x11-dev, atk1, glib2-dev, libgettext3-dev, libiconv-dev Depends: coq, gtk+2-shlibs, pango1-xft2-shlibs, x11-shlibs, atk1-shlibs, glib2-shlibs, libgettext3-shlibs, libiconv, x11 Patch: %n.patch CompileScript: << ./configure -prefix %p -coqdocdir %p/share/doc/coq -mandir %p/share/man -emacslib %p/share/emacs/site-lisp/coq -opt -reals all make coqide << InstallScript: make install-coqide COQINSTALLPREFIX=%d DescDetail: << Developed in the LogiCal project (http://logical.inria.fr), the Coq tool is a formal proof management system: a proof done with Coq is mechanically checked by the machine. In particular, Coq allows one: * to define functions and 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 also includes * a mecanism for automatically generating certified programs * proofs of the specifications of these programs * a documentation tool (coqdoc) * dependecy and makefile generation tools for Coq * a preprocessor for TeX files that include Coq commands (coq-tex) This package provides a graphical user interface (GTK+2) for Coq. << --- NEW FILE: coq.patch --- diff -Naur --exclude='*~' coq-8.0pl3/README.fink coq-8.0pl3.fink/README.fink --- coq-8.0pl3/README.fink 1969-12-31 16:00:00.000000000 -0800 +++ coq-8.0pl3.fink/README.fink 2006-06-11 13:13:05.000000000 -0700 @@ -0,0 +1,4 @@ +This package was originally finkified by Roland Zumkeller +(rol...@po...); it was modified and submitted +to the fink package submission tracker by Jesse Alama +(al...@st...). --- NEW FILE: coqide.patch --- diff -Naur --exclude='*~' coq-8.0pl3/README.fink coq-8.0pl3.fink/README.fink --- coq-8.0pl3/README.fink 1969-12-31 16:00:00.000000000 -0800 +++ coq-8.0pl3.fink/README.fink 2006-06-11 13:13:05.000000000 -0700 @@ -0,0 +1,4 @@ +This package was originally finkified by Roland Zumkeller +(rol...@po...); it was modified and submitted +to the fink package submission tracker by Jesse Alama +(al...@st...). --- NEW FILE: coq.info --- Package: coq Version: 8.0pl3 Revision: 1 Source: ftp://ftp.inria.fr/INRIA/coq/V%v/coq-%v.tar.gz Source-MD5: c98d4cefd119accb1ecdeebb41128822 Maintainer: Jesse Alama <al...@st...> HomePage: http://coq.inria.fr/ License: LGPL Description: The Coq interactive proof assistant BuildDepends: ocaml (>=3.09) DocFiles: CHANGES COPYRIGHT CREDITS LICENSE README README.fink Patch: %n.patch CompileScript: << ./configure -prefix %p -coqdocdir %p/share/doc/coq -mandir %p/share/man -emacslib %p/share/emacs/site-lisp/coq -opt -reals all make coq << InstallScript: make install-coq COQINSTALLPREFIX=%d DescDetail: << Developed in the LogiCal project (http://logical.inria.fr), the Coq tool is a formal proof management system: a proof done with Coq is mechanically checked by the machine. In particular, Coq allows one: * to define functions and 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 also includes * a mecanism to automatically generate certified programs * proofs of the specifications of these programs * a documentation tool (coqdoc) * dependecy and makefile generation tools for Coq * a preprocessor for TeX files that include Coq commands (coq-tex) This package provides the core of the coq package; a graphical user environment is contained in the `coqide' package. << |