diff options
| author | pav <pav@FreeBSD.org> | 2004-10-16 08:55:32 +0800 |
|---|---|---|
| committer | pav <pav@FreeBSD.org> | 2004-10-16 08:55:32 +0800 |
| commit | 1acd43444f510aae364a8325c935b699be30b2bc (patch) | |
| tree | f67e449ba94b3220182190280ad8a13df718774b /math/coq/Makefile | |
| parent | 196c9f155c78071ee434ac871e748fcafcd9f6a3 (diff) | |
| download | freebsd-ports-gnome-1acd43444f510aae364a8325c935b699be30b2bc.tar.gz freebsd-ports-gnome-1acd43444f510aae364a8325c935b699be30b2bc.tar.zst freebsd-ports-gnome-1acd43444f510aae364a8325c935b699be30b2bc.zip | |
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>
Diffstat (limited to 'math/coq/Makefile')
| -rw-r--r-- | math/coq/Makefile | 46 |
1 files changed, 46 insertions, 0 deletions
diff --git a/math/coq/Makefile b/math/coq/Makefile new file mode 100644 index 000000000000..4219e9197363 --- /dev/null +++ b/math/coq/Makefile @@ -0,0 +1,46 @@ +# New ports collection makefile for: coq +# Date created: 2004-10-11 +# Whom: Rene Ladan <r.c.ladan@student.tue.nl> +# +# $FreeBSD$ +# + +PORTNAME= coq +PORTVERSION= 8.0 +CATEGORIES= math +MASTER_SITES= ftp://ftp.inria.fr/INRIA/coq/V8.0pl1/ +DISTNAME= coq-8.0pl1 + +PATCH_SITES= ${MASTER_SITES} +#Ports has Ocaml 3.08.1 : +PATCHFILES= patch-coq-8.0pl1-ocaml-3.08.1 + +MAINTAINER= r.c.ladan@student.tue.nl +COMMENT= Theorem prover based on lambda-C + +BUILD_DEPENDS= ocamlc:${PORTSDIR}/lang/ocaml + +USE_GMAKE= yes + +HAS_CONFIGURE= yes +CONFIGURE_ARGS= --prefix ${PREFIX} +CONFIGURE_ARGS+= --emacslib ${PREFIX}/share/emacs/site-lisp +CONFIGURE_ARGS+= --reals all +CONFIGURE_ARGS+= --opt + +ALL_TARGET= world +#no lablgl2 in ports yet + +MAN1= coq-interface.1 coq-tex.1 coq_makefile.1 coqc.1 coqdep.1 \ + coqdoc.1 coqmktop.1 coqtop.1 coqtop.byte.1 coqtop.opt.1 \ + coqwc.1 parser.1 gallina.1 + +post-install: +.if !defined(NOPORTDOCS) + -@${MKDIR} ${DOCSDIR} +.for i in CHANGES COPYRIGHT CREDITS INSTALL LICENSE README + @${INSTALL_DATA} ${WRKSRC}/${i} ${DOCSDIR} +.endfor +.endif + +.include <bsd.port.mk> |