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 <[EMAIL PROTECTED]>
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
+([EMAIL PROTECTED]); it was modified and submitted
+to the fink package submission tracker by Jesse Alama
+([EMAIL PROTECTED]).
--- 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
+([EMAIL PROTECTED]); it was modified and submitted
+to the fink package submission tracker by Jesse Alama
+([EMAIL PROTECTED]).
--- 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 <[EMAIL PROTECTED]>
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.
<<
-------------------------------------------------------------------------
Take Surveys. Earn Cash. Influence the Future of IT
Join SourceForge.net's Techsay panel and you'll get the chance to share your
opinions on IT & business topics through brief surveys -- and earn cash
http://www.techsay.com/default.php?page=join.php&p=sourceforge&CID=DEVDEV
_______________________________________________
Fink-commits mailing list
Fink-commits@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/fink-commits
