From a47b49b11d17add5ca1ea5e650d2f344219b4f7e Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Fri, 5 Feb 2016 15:24:42 -0500
Subject: Update build process to use COQPATH & _CoqProject

Removed all of the files not built by default; they can be resurrected from git
history.  _CoqProject is the standard way to list the files in a project and to
give information to coq_makefile.  COQPATH is the standard way to make use of
not-yet-installed libraries that are not part of your project (i.e., you don't
want to remove them when you `make clean`, etc.).
---
 coqprime/examples/Makefile | 230 ---------------------------------------------
 1 file changed, 230 deletions(-)
 delete mode 100644 coqprime/examples/Makefile

(limited to 'coqprime/examples/Makefile')

diff --git a/coqprime/examples/Makefile b/coqprime/examples/Makefile
deleted file mode 100644
index eff7d0d99..000000000
--- a/coqprime/examples/Makefile
+++ /dev/null
@@ -1,230 +0,0 @@
-#############################################################################
-##  v      #                   The Coq Proof Assistant                     ##
-## <O___,, #                INRIA - CNRS - LIX - LRI - PPS                 ##
-##   \VV/  #                                                               ##
-##    //   #  Makefile automagically generated by coq_makefile V8.3pl1     ##
-#############################################################################
-
-# WARNING
-#
-# This Makefile has been automagically generated
-# Edit at your own risks !
-#
-# END OF WARNING
-
-#
-# This Makefile was generated by the command line :
-# coq_makefile -f Make -o Makefile 
-#
-
-# 
-# This Makefile may take 3 arguments passed as environment variables:
-#   - COQBIN to specify the directory where Coq binaries resides;
-#   - CAMLBIN and CAMLP4BIN to give the path for the OCaml and Camlp4/5 binaries.
-COQLIB:=$(shell $(COQBIN)coqtop -where | sed -e 's/\\/\\\\/g')
-CAMLP4:="$(shell $(COQBIN)coqtop -config | awk -F = '/CAMLP4=/{print $$2}')"
-ifndef CAMLP4BIN
-  CAMLP4BIN:=$(CAMLBIN)
-endif
-
-CAMLP4LIB:=$(shell $(CAMLP4BIN)$(CAMLP4) -where)
-
-##########################
-#                        #
-# Libraries definitions. #
-#                        #
-##########################
-
-OCAMLLIBS:=-I .\
-  -I ../Tactic\
-  -I ../N\
-  -I ../Z\
-  -I ../PrimalityTest\
-  -I ../List\
-  -I ../elliptic\
-  -I ../num
-COQSRCLIBS:=-I $(COQLIB)/kernel -I $(COQLIB)/lib \
-  -I $(COQLIB)/library -I $(COQLIB)/parsing \
-  -I $(COQLIB)/pretyping -I $(COQLIB)/interp \
-  -I $(COQLIB)/proofs -I $(COQLIB)/tactics \
-  -I $(COQLIB)/toplevel \
-  -I $(COQLIB)/plugins/cc \
-  -I $(COQLIB)/plugins/dp \
-  -I $(COQLIB)/plugins/extraction \
-  -I $(COQLIB)/plugins/field \
-  -I $(COQLIB)/plugins/firstorder \
-  -I $(COQLIB)/plugins/fourier \
-  -I $(COQLIB)/plugins/funind \
-  -I $(COQLIB)/plugins/groebner \
-  -I $(COQLIB)/plugins/interface \
-  -I $(COQLIB)/plugins/micromega \
-  -I $(COQLIB)/plugins/nsatz \
-  -I $(COQLIB)/plugins/omega \
-  -I $(COQLIB)/plugins/quote \
-  -I $(COQLIB)/plugins/ring \
-  -I $(COQLIB)/plugins/romega \
-  -I $(COQLIB)/plugins/rtauto \
-  -I $(COQLIB)/plugins/setoid_ring \
-  -I $(COQLIB)/plugins/subtac \
-  -I $(COQLIB)/plugins/subtac/test \
-  -I $(COQLIB)/plugins/syntax \
-  -I $(COQLIB)/plugins/xml
-COQLIBS:=-I .\
-  -I ../Tactic\
-  -I ../N\
-  -I ../Z\
-  -I ../PrimalityTest\
-  -I ../List\
-  -I ../elliptic\
-  -I ../num 
-COQDOCLIBS:=
-
-##########################
-#                        #
-# Variables definitions. #
-#                        #
-##########################
-
-ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)
-OPT:=
-COQFLAGS:=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML) -verbose
-ifdef CAMLBIN
-  COQMKTOPFLAGS:=-camlbin $(CAMLBIN) -camlp4bin $(CAMLP4BIN)
-endif
-COQC:=$(COQBIN)coqc
-COQDEP:=$(COQBIN)coqdep -c
-GALLINA:=$(COQBIN)gallina
-COQDOC:=$(COQBIN)coqdoc
-COQMKTOP:=$(COQBIN)coqmktop
-CAMLLIB:=$(shell $(CAMLBIN)ocamlc.opt -where)
-CAMLC:=$(CAMLBIN)ocamlc.opt -c -rectypes
-CAMLOPTC:=$(CAMLBIN)ocamlopt.opt -c -rectypes
-CAMLLINK:=$(CAMLBIN)ocamlc.opt -rectypes
-CAMLOPTLINK:=$(CAMLBIN)ocamlopt.opt -rectypes
-GRAMMARS:=grammar.cma
-CAMLP4EXTEND:=pa_extend.cmo pa_macro.cmo q_MLast.cmo
-CAMLP4OPTIONS:=
-PP:=-pp "$(CAMLP4BIN)$(CAMLP4)o -I $(CAMLLIB) -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl"
-
-###################################
-#                                 #
-# Definition of the "all" target. #
-#                                 #
-###################################
-
-VFILES:=BasePrimes.v\
-  PocklingtonRefl.v\
-  TestLucas.v\
-  prime216656403549020227250327256032933021325435259861468456540459488823774358486649614451547405419273433458932168893949521787.v\
-  prime329719147332060395689499.v\
-  russell1.v\
-  russell2.v
-VOFILES:=$(VFILES:.v=.vo)
-VOFILES0:=$(filter-out ,$(VOFILES))
-GLOBFILES:=$(VFILES:.v=.glob)
-VIFILES:=$(VFILES:.v=.vi)
-GFILES:=$(VFILES:.v=.g)
-HTMLFILES:=$(VFILES:.v=.html)
-GHTMLFILES:=$(VFILES:.v=.g.html)
-
-all: $(VOFILES) 
-spec: $(VIFILES)
-
-gallina: $(GFILES)
-
-html: $(GLOBFILES) $(VFILES)
-	- mkdir -p html
-	$(COQDOC) -toc -html $(COQDOCLIBS) -d html $(VFILES)
-
-gallinahtml: $(GLOBFILES) $(VFILES)
-	- mkdir -p html
-	$(COQDOC) -toc -html -g $(COQDOCLIBS) -d html $(VFILES)
-
-all.ps: $(VFILES)
-	$(COQDOC) -toc -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
-
-all-gal.ps: $(VFILES)
-	$(COQDOC) -toc -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
-
-all.pdf: $(VFILES)
-	$(COQDOC) -toc -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
-
-all-gal.pdf: $(VFILES)
-	$(COQDOC) -toc -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
-
-
-
-####################
-#                  #
-# Special targets. #
-#                  #
-####################
-
-.PHONY: all opt byte archclean clean install depend html
-
-%.vo %.glob: %.v
-	$(COQC) $(COQDEBUG) $(COQFLAGS) $*
-
-%.vi: %.v
-	$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*
-
-%.g: %.v
-	$(GALLINA) $<
-
-%.tex: %.v
-	$(COQDOC) -latex $< -o $@
-
-%.html: %.v %.glob
-	$(COQDOC) -html $< -o $@
-
-%.g.tex: %.v
-	$(COQDOC) -latex -g $< -o $@
-
-%.g.html: %.v %.glob
-	$(COQDOC) -html -g $< -o $@
-
-%.v.d: %.v
-	$(COQDEP) -slash $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
-
-byte:
-	$(MAKE) all "OPT:=-byte"
-
-opt:
-	$(MAKE) all "OPT:=-opt"
-
-install:
-	mkdir -p $(COQLIB)/user-contrib
-	(for i in $(VOFILES0); do \
-	 install -d `dirname $(COQLIB)/user-contrib/$(INSTALLDEFAULTROOT)/$$i`; \
-	 install $$i $(COQLIB)/user-contrib/$(INSTALLDEFAULTROOT)/$$i; \
-	 done)
-
-clean:
-	rm -f $(CMOFILES) $(CMIFILES) $(CMXFILES) $(CMXSFILES) $(OFILES) $(VOFILES) $(VIFILES) $(GFILES) $(MLFILES:.ml=.cmo) $(MLFILES:.ml=.cmx) *~
-	rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(HTMLFILES) $(GHTMLFILES) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) $(VFILES:.v=.v.d)
-	- rm -rf html
-
-archclean:
-	rm -f *.cmx *.o
-
-
-printenv: 
-	@echo CAMLC =	$(CAMLC)
-	@echo CAMLOPTC =	$(CAMLOPTC)
-	@echo CAMLP4LIB =	$(CAMLP4LIB)
-
-Makefile: Make
-	mv -f Makefile Makefile.bak
-	$(COQBIN)coq_makefile -f Make -o Makefile
-
-
--include $(VFILES:.v=.v.d)
-.SECONDARY: $(VFILES:.v=.v.d)
-
-# WARNING
-#
-# This Makefile has been automagically generated
-# Edit at your own risks !
-#
-# END OF WARNING
-
-- 
cgit v1.2.3