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/Makefile | 99 ++++++++++++++++---------------------------------------
 1 file changed, 29 insertions(+), 70 deletions(-)

(limited to 'coqprime/Makefile')

diff --git a/coqprime/Makefile b/coqprime/Makefile
index 60497e777..8fa838a1e 100644
--- a/coqprime/Makefile
+++ b/coqprime/Makefile
@@ -14,7 +14,7 @@
 
 #
 # This Makefile was generated by the command line :
-# coq_makefile -f Make 
+# coq_makefile -f _CoqProject -o Makefile 
 #
 
 .DEFAULT_GOAL := all
@@ -39,16 +39,8 @@ $(call includecmdwithout@,$(COQBIN)coqtop -config)
 #                        #
 ##########################
 
-COQLIBS?= -R PrimalityTest Coqprime\
-  -R Z Coqprime\
-  -R List Coqprime\
-  -R N Coqprime\
-  -R Tactic Coqprime
-COQDOCLIBS?= -R PrimalityTest Coqprime\
-  -R Z Coqprime\
-  -R List Coqprime\
-  -R N Coqprime\
-  -R Tactic Coqprime
+COQLIBS?= -R Coqprime Coqprime
+COQDOCLIBS?=-R Coqprime Coqprime
 
 ##########################
 #                        #
@@ -88,48 +80,35 @@ endif
 #                    #
 ######################
 
-# TODO (andres): 
-#   This repo is incomplete and can't build the things in num/
-#   or examples/ or elliptic/. Do we need those?
-
-VFILES := PrimalityTest/Zp.v\
-  PrimalityTest/Root.v\
-  PrimalityTest/Proth.v\
-  PrimalityTest/Pocklington.v\
-  PrimalityTest/PocklingtonCertificat.v\
-  PrimalityTest/PGroup.v\
-  PrimalityTest/Pepin.v\
-  PrimalityTest/LucasLehmer.v\
-  PrimalityTest/Lagrange.v\
-  PrimalityTest/IGroup.v\
-  PrimalityTest/FGroup.v\
-  PrimalityTest/Euler.v\
-  PrimalityTest/EGroup.v\
-  PrimalityTest/Cyclic.v\
-  Z/ZSum.v\
-  Z/ZCmisc.v\
-  Z/ZCAux.v\
-  Z/Pmod.v\
-  List/ZProgression.v\
-  List/UList.v\
-  List/Permutation.v\
-  List/ListAux.v\
-  List/Iterator.v\
-  N/NatAux.v\
-  Tactic/Tactic.v
+VFILES:=Coqprime/Zp.v\
+  Coqprime/ZSum.v\
+  Coqprime/ZProgression.v\
+  Coqprime/ZCmisc.v\
+  Coqprime/ZCAux.v\
+  Coqprime/UList.v\
+  Coqprime/Tactic.v\
+  Coqprime/Root.v\
+  Coqprime/PocklingtonCertificat.v\
+  Coqprime/Pocklington.v\
+  Coqprime/Pmod.v\
+  Coqprime/Permutation.v\
+  Coqprime/PGroup.v\
+  Coqprime/NatAux.v\
+  Coqprime/LucasLehmer.v\
+  Coqprime/ListAux.v\
+  Coqprime/Lagrange.v\
+  Coqprime/Iterator.v\
+  Coqprime/IGroup.v\
+  Coqprime/FGroup.v\
+  Coqprime/Euler.v\
+  Coqprime/EGroup.v\
+  Coqprime/Cyclic.v
 
 -include $(addsuffix .d,$(VFILES))
 .SECONDARY: $(addsuffix .d,$(VFILES))
 
 VOFILES:=$(VFILES:.v=.vo)
-# VOFILES1=$(patsubst examples/%,%,$(filter examples/%,$(VOFILES)))
-# VOFILES2=$(patsubst num/%,%,$(filter num/%,$(VOFILES)))
-VOFILES3=$(patsubst elliptic/%,%,$(filter elliptic/%,$(VOFILES)))
-VOFILES4=$(patsubst PrimalityTest/%,%,$(filter PrimalityTest/%,$(VOFILES)))
-VOFILES5=$(patsubst Z/%,%,$(filter Z/%,$(VOFILES)))
-VOFILES6=$(patsubst List/%,%,$(filter List/%,$(VOFILES)))
-VOFILES7=$(patsubst N/%,%,$(filter N/%,$(VOFILES)))
-VOFILES8=$(patsubst Tactic/%,%,$(filter Tactic/%,$(VOFILES)))
+VOFILES1=$(patsubst Coqprime/%,%,$(filter Coqprime/%,$(VOFILES)))
 GLOBFILES:=$(VFILES:.v=.glob)
 VIFILES:=$(VFILES:.v=.vi)
 GFILES:=$(VFILES:.v=.g)
@@ -199,27 +178,7 @@ userinstall:
 	+$(MAKE) USERINSTALL=true install
 
 install:
-	cd "elliptic"; for i in $(VOFILES3); do \
-	 install -d "`dirname "$(DSTROOT)"$(COQLIBINSTALL)/Coqprime/$$i`"; \
-	 install -m 0644 $$i "$(DSTROOT)"$(COQLIBINSTALL)/Coqprime/$$i; \
-	done
-	cd "PrimalityTest"; for i in $(VOFILES4); do \
-	 install -d "`dirname "$(DSTROOT)"$(COQLIBINSTALL)/Coqprime/$$i`"; \
-	 install -m 0644 $$i "$(DSTROOT)"$(COQLIBINSTALL)/Coqprime/$$i; \
-	done
-	cd "Z"; for i in $(VOFILES5); do \
-	 install -d "`dirname "$(DSTROOT)"$(COQLIBINSTALL)/Coqprime/$$i`"; \
-	 install -m 0644 $$i "$(DSTROOT)"$(COQLIBINSTALL)/Coqprime/$$i; \
-	done
-	cd "List"; for i in $(VOFILES6); do \
-	 install -d "`dirname "$(DSTROOT)"$(COQLIBINSTALL)/Coqprime/$$i`"; \
-	 install -m 0644 $$i "$(DSTROOT)"$(COQLIBINSTALL)/Coqprime/$$i; \
-	done
-	cd "N"; for i in $(VOFILES7); do \
-	 install -d "`dirname "$(DSTROOT)"$(COQLIBINSTALL)/Coqprime/$$i`"; \
-	 install -m 0644 $$i "$(DSTROOT)"$(COQLIBINSTALL)/Coqprime/$$i; \
-	done
-	cd "Tactic"; for i in $(VOFILES8); do \
+	cd "Coqprime"; for i in $(VOFILES1); do \
 	 install -d "`dirname "$(DSTROOT)"$(COQLIBINSTALL)/Coqprime/$$i`"; \
 	 install -m 0644 $$i "$(DSTROOT)"$(COQLIBINSTALL)/Coqprime/$$i; \
 	done
@@ -247,7 +206,7 @@ printenv:
 	@echo 'COQLIBINSTALL =	$(COQLIBINSTALL)'
 	@echo 'COQDOCINSTALL =	$(COQDOCINSTALL)'
 
-Makefile: Make
+Makefile: _CoqProject
 	mv -f $@ $@.bak
 	"$(COQBIN)coq_makefile" -f $< -o $@
 
-- 
cgit v1.2.3