the Fink project is an effort to port
popular Unix programs to Mac OS X
Package: coqide
Version: 8.0pl3
Revision: 3
Source: ftp://ftp.inria.fr/INRIA/coq/V%v/coq-%v.tar.gz
Source-MD5: c98d4cefd119accb1ecdeebb41128822
Maintainer: Jesse Alama
HomePage: http://coq.inria.fr/
License: LGPL
DocFiles: CHANGES COPYRIGHT CREDITS LICENSE README README.fink
Description: Interactive development environment for Coq
BuildDepends: glitz, expat1, libpng3, cairo (>= 1.6-1), fontconfig2-dev (>= 2.4.1-1), freetype219 (>= 2.3.5-1), xft2-dev, ocaml (>=3.09), lablgtk2 (>=2.4.0), gtk+2-dev (>= 2.12.0-1), pango1-xft2-ft219-dev (>= 1.18.4-4), pixman (>= 0.10.0-1), x11-dev, atk1 (>= 1.20.0-1), glib2-dev (>= 2.14.0-1), libgettext3-dev, libiconv-dev, pkgconfig (>= 0.21-1)
Depends: coq, gtk+2-shlibs (>= 2.12.0-1), pango1-xft2-ft219-shlibs (>= 1.18.4-4), x11-shlibs, atk1-shlibs (>= 1.20.0-1), glib2-shlibs (>= 2.14.0-1), libgettext3-shlibs, libiconv, x11
Patch: %n.patch
CompileScript: <<
#!/bin/sh -ev
export PKG_CONFIG_PATH="%p/lib/pango-ft219/lib/pkgconfig:%p/lib/fontconfig2/lib/pkgconfig:%p/lib/freetype219/lib/pkgconfig:$PKG_CONFIG_PATH" FREETYPE_CONFIG=%p/lib/freetype219/bin/freetype-config
./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.
<<