summaryrefslogtreecommitdiff
path: root/math
diff options
context:
space:
mode:
authorkristerw <kristerw>2003-03-22 18:20:54 +0000
committerkristerw <kristerw>2003-03-22 18:20:54 +0000
commit458e3eedfe06e889eb62a5f920ea01b1f552ea9c (patch)
tree6e06481b76fc91b4d5840599d50e2ce601a828cf /math
parentc9ac4bc042a08db1eaaaeabcdc61ff537a03211d (diff)
downloadpkgsrc-458e3eedfe06e889eb62a5f920ea01b1f552ea9c.tar.gz
Import coq 7.4. From Christopher Richards in PR 20669.
Coq is a Proof Assistant for a Logical Framework known as the Calculus of Inductive Constructions. It allows the interactive construction of formal proofs, and also the manipulation of functional programs consistently with their specifications.
Diffstat (limited to 'math')
-rw-r--r--math/coq/DESCR6
-rw-r--r--math/coq/MESSAGE14
-rw-r--r--math/coq/Makefile27
-rw-r--r--math/coq/PLIST268
-rw-r--r--math/coq/PLIST.opt6
-rw-r--r--math/coq/distinfo5
-rw-r--r--math/coq/patches/patch-aa31
7 files changed, 357 insertions, 0 deletions
diff --git a/math/coq/DESCR b/math/coq/DESCR
new file mode 100644
index 00000000000..43b67beaebc
--- /dev/null
+++ b/math/coq/DESCR
@@ -0,0 +1,6 @@
+From http://coq.inria.fr/doc/tutorial.html:
+
+ Coq is a Proof Assistant for a Logical Framework known as the
+ Calculus of Inductive Constructions. It allows the interactive
+ construction of formal proofs, and also the manipulation of
+ functional programs consistently with their specifications.
diff --git a/math/coq/MESSAGE b/math/coq/MESSAGE
new file mode 100644
index 00000000000..2f30deced83
--- /dev/null
+++ b/math/coq/MESSAGE
@@ -0,0 +1,14 @@
+===========================================================================
+$NetBSD: MESSAGE,v 1.1.1.1 2003/03/22 18:20:55 kristerw Exp $
+
+You may wish to add the following to your ~/.emacs:
+
+ (add-to-list 'auto-mode-alist '("\\.v$" . coq-mode))
+ (autoload 'coq-mode "coq" "Major mode for editing Coq vernacular." t)
+ (autoload 'run-coq "coq-inferior" "Run an inferior Coq process." t)
+ (autoload 'run-coq-other-window "coq-inferior"
+ "Run an inferior Coq process in a new window." t)
+ (autoload 'run-coq-other-frame "coq-inferior"
+ "Run an inferior Coq process in a new frame." t)
+
+===========================================================================
diff --git a/math/coq/Makefile b/math/coq/Makefile
new file mode 100644
index 00000000000..cd0a2b0cee7
--- /dev/null
+++ b/math/coq/Makefile
@@ -0,0 +1,27 @@
+# $NetBSD: Makefile,v 1.1.1.1 2003/03/22 18:20:54 kristerw Exp $
+#
+
+DISTNAME= coq-7.4
+CATEGORIES= math lang
+MASTER_SITES= ftp://ftp.inria.fr/INRIA/coq/V7.4/
+
+MAINTAINER= richards+netbsd@CS.Princeton.EDU
+HOMEPAGE= http://coq.inria.fr/
+COMMENT= Theorem prover which extracts programs from proofs
+
+USE_GMAKE= YES
+USE_BUILDLINK2= YES
+HAS_CONFIGURE= YES
+CONFIGURE_ARGS+= -prefix ${PREFIX}
+CONFIGURE_ARGS+= -emacslib ${PREFIX}/share/emacs/site-lisp
+CONFIGURE_ARGS+= -reals all
+ALL_TARGET= world
+
+.include "../../mk/bsd.prefs.mk"
+
+.if (${MACHINE_ARCH} == "i386")
+PLIST_SRC= ${PKGDIR}/PLIST.opt ${PKGDIR}/PLIST
+.endif
+
+.include "../../lang/ocaml/buildlink2.mk"
+.include "../../mk/bsd.pkg.mk"
diff --git a/math/coq/PLIST b/math/coq/PLIST
new file mode 100644
index 00000000000..72d7e03b6c9
--- /dev/null
+++ b/math/coq/PLIST
@@ -0,0 +1,268 @@
+@comment $NetBSD: PLIST,v 1.1.1.1 2003/03/22 18:20:55 kristerw Exp $
+bin/coq-interface
+bin/coq-tex
+bin/coq_makefile
+bin/coq_vo2xml
+bin/coqc
+bin/coqdep
+bin/coqmktop
+bin/coqtop
+bin/coqtop.byte
+bin/gallina
+lib/coq/contrib/cc/CC.vo
+lib/coq/contrib/correctness/ArrayPermut.vo
+lib/coq/contrib/correctness/Arrays.vo
+lib/coq/contrib/correctness/Correctness.vo
+lib/coq/contrib/correctness/Exchange.vo
+lib/coq/contrib/correctness/ProgBool.vo
+lib/coq/contrib/correctness/ProgInt.vo
+lib/coq/contrib/correctness/Sorted.vo
+lib/coq/contrib/correctness/Tuples.vo
+lib/coq/contrib/field/Field.vo
+lib/coq/contrib/field/Field_Compl.vo
+lib/coq/contrib/field/Field_Tactic.vo
+lib/coq/contrib/field/Field_Theory.vo
+lib/coq/contrib/fourier/Fourier.vo
+lib/coq/contrib/fourier/Fourier_util.vo
+lib/coq/contrib/interface/Centaur.vo
+lib/coq/contrib/omega/Omega.vo
+lib/coq/contrib/ring/ArithRing.vo
+lib/coq/contrib/ring/Quote.vo
+lib/coq/contrib/ring/Ring.vo
+lib/coq/contrib/ring/Ring_abstract.vo
+lib/coq/contrib/ring/Ring_normalize.vo
+lib/coq/contrib/ring/Ring_theory.vo
+lib/coq/contrib/ring/Setoid_ring.vo
+lib/coq/contrib/ring/Setoid_ring_normalize.vo
+lib/coq/contrib/ring/Setoid_ring_theory.vo
+lib/coq/contrib/ring/ZArithRing.vo
+lib/coq/contrib/romega/ROmega.vo
+lib/coq/contrib/romega/ReflOmegaCore.vo
+lib/coq/states/barestate.coq
+lib/coq/states/initial.coq
+lib/coq/theories/Arith/Arith.vo
+lib/coq/theories/Arith/Between.vo
+lib/coq/theories/Arith/Bool_nat.vo
+lib/coq/theories/Arith/Compare.vo
+lib/coq/theories/Arith/Compare_dec.vo
+lib/coq/theories/Arith/Div2.vo
+lib/coq/theories/Arith/EqNat.vo
+lib/coq/theories/Arith/Euclid.vo
+lib/coq/theories/Arith/Even.vo
+lib/coq/theories/Arith/Gt.vo
+lib/coq/theories/Arith/Le.vo
+lib/coq/theories/Arith/Lt.vo
+lib/coq/theories/Arith/Max.vo
+lib/coq/theories/Arith/Min.vo
+lib/coq/theories/Arith/Minus.vo
+lib/coq/theories/Arith/Mult.vo
+lib/coq/theories/Arith/Peano_dec.vo
+lib/coq/theories/Arith/Plus.vo
+lib/coq/theories/Arith/Wf_nat.vo
+lib/coq/theories/Bool/Bool.vo
+lib/coq/theories/Bool/BoolEq.vo
+lib/coq/theories/Bool/Bvector.vo
+lib/coq/theories/Bool/DecBool.vo
+lib/coq/theories/Bool/IfProp.vo
+lib/coq/theories/Bool/Sumbool.vo
+lib/coq/theories/Bool/Zerob.vo
+lib/coq/theories/Init/Datatypes.vo
+lib/coq/theories/Init/DatatypesSyntax.vo
+lib/coq/theories/Init/Logic.vo
+lib/coq/theories/Init/LogicSyntax.vo
+lib/coq/theories/Init/Logic_Type.vo
+lib/coq/theories/Init/Logic_TypeSyntax.vo
+lib/coq/theories/Init/Peano.vo
+lib/coq/theories/Init/PeanoSyntax.vo
+lib/coq/theories/Init/Prelude.vo
+lib/coq/theories/Init/Specif.vo
+lib/coq/theories/Init/SpecifSyntax.vo
+lib/coq/theories/Init/Wf.vo
+lib/coq/theories/IntMap/Adalloc.vo
+lib/coq/theories/IntMap/Addec.vo
+lib/coq/theories/IntMap/Addr.vo
+lib/coq/theories/IntMap/Adist.vo
+lib/coq/theories/IntMap/Allmaps.vo
+lib/coq/theories/IntMap/Fset.vo
+lib/coq/theories/IntMap/Lsort.vo
+lib/coq/theories/IntMap/Map.vo
+lib/coq/theories/IntMap/Mapaxioms.vo
+lib/coq/theories/IntMap/Mapc.vo
+lib/coq/theories/IntMap/Mapcanon.vo
+lib/coq/theories/IntMap/Mapcard.vo
+lib/coq/theories/IntMap/Mapfold.vo
+lib/coq/theories/IntMap/Mapiter.vo
+lib/coq/theories/IntMap/Maplists.vo
+lib/coq/theories/IntMap/Mapsubset.vo
+lib/coq/theories/Lists/List.vo
+lib/coq/theories/Lists/ListSet.vo
+lib/coq/theories/Lists/PolyList.vo
+lib/coq/theories/Lists/PolyListSyntax.vo
+lib/coq/theories/Lists/Streams.vo
+lib/coq/theories/Lists/TheoryList.vo
+lib/coq/theories/Logic/Berardi.vo
+lib/coq/theories/Logic/Classical.vo
+lib/coq/theories/Logic/ClassicalFacts.vo
+lib/coq/theories/Logic/Classical_Pred_Set.vo
+lib/coq/theories/Logic/Classical_Pred_Type.vo
+lib/coq/theories/Logic/Classical_Prop.vo
+lib/coq/theories/Logic/Classical_Type.vo
+lib/coq/theories/Logic/Decidable.vo
+lib/coq/theories/Logic/Eqdep.vo
+lib/coq/theories/Logic/Eqdep_dec.vo
+lib/coq/theories/Logic/Hurkens.vo
+lib/coq/theories/Logic/JMeq.vo
+lib/coq/theories/Logic/ProofIrrelevance.vo
+lib/coq/theories/Reals/Alembert.vo
+lib/coq/theories/Reals/AltSeries.vo
+lib/coq/theories/Reals/ArithProp.vo
+lib/coq/theories/Reals/Binomial.vo
+lib/coq/theories/Reals/Cauchy_prod.vo
+lib/coq/theories/Reals/Cos_plus.vo
+lib/coq/theories/Reals/Cos_rel.vo
+lib/coq/theories/Reals/DiscrR.vo
+lib/coq/theories/Reals/Exp_prop.vo
+lib/coq/theories/Reals/Integration.vo
+lib/coq/theories/Reals/MVT.vo
+lib/coq/theories/Reals/NewtonInt.vo
+lib/coq/theories/Reals/PSeries_reg.vo
+lib/coq/theories/Reals/PartSum.vo
+lib/coq/theories/Reals/RIneq.vo
+lib/coq/theories/Reals/RList.vo
+lib/coq/theories/Reals/R_Ifp.vo
+lib/coq/theories/Reals/R_sqr.vo
+lib/coq/theories/Reals/R_sqrt.vo
+lib/coq/theories/Reals/Ranalysis.vo
+lib/coq/theories/Reals/Ranalysis1.vo
+lib/coq/theories/Reals/Ranalysis2.vo
+lib/coq/theories/Reals/Ranalysis3.vo
+lib/coq/theories/Reals/Ranalysis4.vo
+lib/coq/theories/Reals/Raxioms.vo
+lib/coq/theories/Reals/Rbase.vo
+lib/coq/theories/Reals/Rbasic_fun.vo
+lib/coq/theories/Reals/Rcomplete.vo
+lib/coq/theories/Reals/Rdefinitions.vo
+lib/coq/theories/Reals/Rderiv.vo
+lib/coq/theories/Reals/Reals.vo
+lib/coq/theories/Reals/Rfunctions.vo
+lib/coq/theories/Reals/Rgeom.vo
+lib/coq/theories/Reals/RiemannInt.vo
+lib/coq/theories/Reals/RiemannInt_SF.vo
+lib/coq/theories/Reals/Rlimit.vo
+lib/coq/theories/Reals/Rpower.vo
+lib/coq/theories/Reals/Rprod.vo
+lib/coq/theories/Reals/Rseries.vo
+lib/coq/theories/Reals/Rsigma.vo
+lib/coq/theories/Reals/Rsqrt_def.vo
+lib/coq/theories/Reals/Rsyntax.vo
+lib/coq/theories/Reals/Rtopology.vo
+lib/coq/theories/Reals/Rtrigo.vo
+lib/coq/theories/Reals/Rtrigo_alt.vo
+lib/coq/theories/Reals/Rtrigo_calc.vo
+lib/coq/theories/Reals/Rtrigo_def.vo
+lib/coq/theories/Reals/Rtrigo_fun.vo
+lib/coq/theories/Reals/Rtrigo_reg.vo
+lib/coq/theories/Reals/SeqProp.vo
+lib/coq/theories/Reals/SeqSeries.vo
+lib/coq/theories/Reals/SplitAbsolu.vo
+lib/coq/theories/Reals/SplitRmult.vo
+lib/coq/theories/Reals/Sqrt_reg.vo
+lib/coq/theories/Reals/TypeSyntax.vo
+lib/coq/theories/Relations/Newman.vo
+lib/coq/theories/Relations/Operators_Properties.vo
+lib/coq/theories/Relations/Relation_Definitions.vo
+lib/coq/theories/Relations/Relation_Operators.vo
+lib/coq/theories/Relations/Relations.vo
+lib/coq/theories/Relations/Rstar.vo
+lib/coq/theories/Setoids/Setoid.vo
+lib/coq/theories/Sets/Classical_sets.vo
+lib/coq/theories/Sets/Constructive_sets.vo
+lib/coq/theories/Sets/Cpo.vo
+lib/coq/theories/Sets/Ensembles.vo
+lib/coq/theories/Sets/Finite_sets.vo
+lib/coq/theories/Sets/Finite_sets_facts.vo
+lib/coq/theories/Sets/Image.vo
+lib/coq/theories/Sets/Infinite_sets.vo
+lib/coq/theories/Sets/Integers.vo
+lib/coq/theories/Sets/Multiset.vo
+lib/coq/theories/Sets/Partial_Order.vo
+lib/coq/theories/Sets/Permut.vo
+lib/coq/theories/Sets/Powerset.vo
+lib/coq/theories/Sets/Powerset_Classical_facts.vo
+lib/coq/theories/Sets/Powerset_facts.vo
+lib/coq/theories/Sets/Relations_1.vo
+lib/coq/theories/Sets/Relations_1_facts.vo
+lib/coq/theories/Sets/Relations_2.vo
+lib/coq/theories/Sets/Relations_2_facts.vo
+lib/coq/theories/Sets/Relations_3.vo
+lib/coq/theories/Sets/Relations_3_facts.vo
+lib/coq/theories/Sets/Uniset.vo
+lib/coq/theories/Sorting/Heap.vo
+lib/coq/theories/Sorting/Permutation.vo
+lib/coq/theories/Sorting/Sorting.vo
+lib/coq/theories/Wellfounded/Disjoint_Union.vo
+lib/coq/theories/Wellfounded/Inclusion.vo
+lib/coq/theories/Wellfounded/Inverse_Image.vo
+lib/coq/theories/Wellfounded/Lexicographic_Exponentiation.vo
+lib/coq/theories/Wellfounded/Lexicographic_Product.vo
+lib/coq/theories/Wellfounded/Transitive_Closure.vo
+lib/coq/theories/Wellfounded/Union.vo
+lib/coq/theories/Wellfounded/Well_Ordering.vo
+lib/coq/theories/Wellfounded/Wellfounded.vo
+lib/coq/theories/ZArith/Wf_Z.vo
+lib/coq/theories/ZArith/ZArith.vo
+lib/coq/theories/ZArith/ZArith_base.vo
+lib/coq/theories/ZArith/ZArith_dec.vo
+lib/coq/theories/ZArith/Zbinary.vo
+lib/coq/theories/ZArith/Zbool.vo
+lib/coq/theories/ZArith/Zcomplements.vo
+lib/coq/theories/ZArith/Zdiv.vo
+lib/coq/theories/ZArith/Zhints.vo
+lib/coq/theories/ZArith/Zlogarithm.vo
+lib/coq/theories/ZArith/Zmisc.vo
+lib/coq/theories/ZArith/Zpower.vo
+lib/coq/theories/ZArith/Zsqrt.vo
+lib/coq/theories/ZArith/Zsyntax.vo
+lib/coq/theories/ZArith/Zwf.vo
+lib/coq/theories/ZArith/auxiliary.vo
+lib/coq/theories/ZArith/fast_integer.vo
+lib/coq/theories/ZArith/zarith_aux.vo
+man/man1/coq-interface.1
+man/man1/coq-tex.1
+man/man1/coq_makefile.1
+man/man1/coq_vo2xml.1
+man/man1/coqc.1
+man/man1/coqdep.1
+man/man1/coqmktop.1
+man/man1/coqtop.1
+man/man1/coqtop.byte.1
+man/man1/gallina.1
+share/emacs/site-lisp/coq-inferior.el
+share/emacs/site-lisp/coq.el
+@dirrm lib/coq/theories/ZArith
+@dirrm lib/coq/theories/Wellfounded
+@dirrm lib/coq/theories/Sorting
+@dirrm lib/coq/theories/Sets
+@dirrm lib/coq/theories/Setoids
+@dirrm lib/coq/theories/Relations
+@dirrm lib/coq/theories/Reals
+@dirrm lib/coq/theories/Logic
+@dirrm lib/coq/theories/Lists
+@dirrm lib/coq/theories/IntMap
+@dirrm lib/coq/theories/Init
+@dirrm lib/coq/theories/Bool
+@dirrm lib/coq/theories/Arith
+@dirrm lib/coq/theories
+@exec ${MKDIR} %D/lib/coq/tactics
+@dirrm lib/coq/tactics
+@dirrm lib/coq/states
+@dirrm lib/coq/contrib/romega
+@dirrm lib/coq/contrib/ring
+@dirrm lib/coq/contrib/omega
+@dirrm lib/coq/contrib/interface
+@dirrm lib/coq/contrib/fourier
+@dirrm lib/coq/contrib/field
+@dirrm lib/coq/contrib/correctness
+@dirrm lib/coq/contrib/cc
+@dirrm lib/coq/contrib
+@dirrm lib/coq
diff --git a/math/coq/PLIST.opt b/math/coq/PLIST.opt
new file mode 100644
index 00000000000..5a86c6a545a
--- /dev/null
+++ b/math/coq/PLIST.opt
@@ -0,0 +1,6 @@
+@comment $NetBSD: PLIST.opt,v 1.1.1.1 2003/03/22 18:20:55 kristerw Exp $
+bin/coq-interface.opt
+bin/coqtop.opt
+bin/parser
+man/man1/coqtop.opt.1
+man/man1/parser.1
diff --git a/math/coq/distinfo b/math/coq/distinfo
new file mode 100644
index 00000000000..8db97608089
--- /dev/null
+++ b/math/coq/distinfo
@@ -0,0 +1,5 @@
+$NetBSD: distinfo,v 1.1.1.1 2003/03/22 18:20:55 kristerw Exp $
+
+SHA1 (coq-7.4.tar.gz) = 82fe0094cde8a766e3ba0a77c731b4ef2345a41b
+Size (coq-7.4.tar.gz) = 1537547 bytes
+SHA1 (patch-aa) = ce59dda44ac5f81834f9f60a7f87524c90f6cb6e
diff --git a/math/coq/patches/patch-aa b/math/coq/patches/patch-aa
new file mode 100644
index 00000000000..b6676d97565
--- /dev/null
+++ b/math/coq/patches/patch-aa
@@ -0,0 +1,31 @@
+$NetBSD: patch-aa,v 1.1.1.1 2003/03/22 18:20:55 kristerw Exp $
+
+--- Makefile.orig Mon Feb 3 05:11:32 2003
++++ Makefile
+@@ -368,7 +368,10 @@ COQTOPBYTE=bin/coqtop.byte$(EXE)
+ COQTOPOPT=bin/coqtop.opt$(EXE)
+ BESTCOQTOP=bin/coqtop.$(BEST)$(EXE)
+ COQTOP=bin/coqtop$(EXE)
+-COQINTERFACE=bin/coq-interface$(EXE) bin/coq-interface.opt$(EXE) bin/parser$(EXE)
++COQINTERFACE=bin/coq-interface$(EXE)
++ifeq ($(BEST),opt)
++COQINTERFACE+=bin/coq-interface.opt$(EXE) bin/parser$(EXE)
++endif
+
+ COQBINARIES= $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(BESTCOQTOP) $(COQTOP) \
+ $(COQINTERFACE)
+@@ -877,9 +880,12 @@ install-library-light:
+ cp tools/coq.el tools/coq-inferior.el $(FULLEMACSLIB)
+
+ MANPAGES=man/coq-tex.1 man/coqdep.1 man/gallina.1 \
+- man/coqc.1 man/coqtop.1 man/coqtop.byte.1 man/coqtop.opt.1 \
++ man/coqc.1 man/coqtop.1 man/coqtop.byte.1 \
+ man/coq_makefile.1 man/coqmktop.1 \
+- man/coq-interface.1 man/parser.1 man/coq_vo2xml.1
++ man/coq-interface.1 man/coq_vo2xml.1
++ifeq ($(BEST),opt)
++MANPAGES+=man/coqtop.opt.1 man/parser.1
++endif
+
+ install-manpages:
+ $(MKDIR) $(FULLMANDIR)/man1