From 3e0c054948a0b1fc015ad7e23bd8abd023d8e3ed Mon Sep 17 00:00:00 2001
From: Rob Sloan <varomodt@gmail.com>
Date: Thu, 28 Jan 2016 13:35:03 -0500
Subject: recursive-build coqprime

---
 coqprime/Makefile           | 43 +++++++++----------------------------------
 coqprime/PrimalityTest/Zp.v |  2 +-
 coqprime/num/Lucas.v        |  2 +-
 3 files changed, 11 insertions(+), 36 deletions(-)

(limited to 'coqprime')

diff --git a/coqprime/Makefile b/coqprime/Makefile
index 520cd9618..60497e777 100644
--- a/coqprime/Makefile
+++ b/coqprime/Makefile
@@ -39,18 +39,12 @@ $(call includecmdwithout@,$(COQBIN)coqtop -config)
 #                        #
 ##########################
 
-COQLIBS?= -R examples Coqprime\
-  -R num Coqprime\
-  -R elliptic Coqprime\
-  -R PrimalityTest Coqprime\
+COQLIBS?= -R PrimalityTest Coqprime\
   -R Z Coqprime\
   -R List Coqprime\
   -R N Coqprime\
   -R Tactic Coqprime
-COQDOCLIBS?=-R examples Coqprime\
-  -R num Coqprime\
-  -R elliptic Coqprime\
-  -R PrimalityTest Coqprime\
+COQDOCLIBS?= -R PrimalityTest Coqprime\
   -R Z Coqprime\
   -R List Coqprime\
   -R N Coqprime\
@@ -94,20 +88,11 @@ endif
 #                    #
 ######################
 
-VFILES:=examples/PocklingtonRefl.v\
-  examples/BasePrimes.v\
-  num/W.v\
-  num/montgomery.v\
-  num/Pock.v\
-  num/Mod_op.v\
-  num/MEll.v\
-  num/NEll.v\
-  num/Lucas.v\
-  num/Bits.v\
-  elliptic/ZEll.v\
-  elliptic/SMain.v\
-  elliptic/GZnZ.v\
-  PrimalityTest/Zp.v\
+# 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\
@@ -123,8 +108,6 @@ VFILES:=examples/PocklingtonRefl.v\
   PrimalityTest/Cyclic.v\
   Z/ZSum.v\
   Z/ZCmisc.v\
-  Z/Ppow.v\
-  Z/Zmod.v\
   Z/ZCAux.v\
   Z/Pmod.v\
   List/ZProgression.v\
@@ -139,8 +122,8 @@ VFILES:=examples/PocklingtonRefl.v\
 .SECONDARY: $(addsuffix .d,$(VFILES))
 
 VOFILES:=$(VFILES:.v=.vo)
-VOFILES1=$(patsubst examples/%,%,$(filter examples/%,$(VOFILES)))
-VOFILES2=$(patsubst num/%,%,$(filter num/%,$(VOFILES)))
+# 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)))
@@ -216,14 +199,6 @@ userinstall:
 	+$(MAKE) USERINSTALL=true install
 
 install:
-	cd "examples"; for i in $(VOFILES1); do \
-	 install -d "`dirname "$(DSTROOT)"$(COQLIBINSTALL)/Coqprime/$$i`"; \
-	 install -m 0644 $$i "$(DSTROOT)"$(COQLIBINSTALL)/Coqprime/$$i; \
-	done
-	cd "num"; for i in $(VOFILES2); do \
-	 install -d "`dirname "$(DSTROOT)"$(COQLIBINSTALL)/Coqprime/$$i`"; \
-	 install -m 0644 $$i "$(DSTROOT)"$(COQLIBINSTALL)/Coqprime/$$i; \
-	done
 	cd "elliptic"; for i in $(VOFILES3); do \
 	 install -d "`dirname "$(DSTROOT)"$(COQLIBINSTALL)/Coqprime/$$i`"; \
 	 install -m 0644 $$i "$(DSTROOT)"$(COQLIBINSTALL)/Coqprime/$$i; \
diff --git a/coqprime/PrimalityTest/Zp.v b/coqprime/PrimalityTest/Zp.v
index 1e5295191..9b99bef1d 100644
--- a/coqprime/PrimalityTest/Zp.v
+++ b/coqprime/PrimalityTest/Zp.v
@@ -15,7 +15,7 @@
     Definition: ZpGroup              
  **********************************************************************)
 Require Import ZArith Znumtheory Zpow_facts.
-Require Import Tactic.
+Require Import Coqprime.Tactic.
 Require Import Wf_nat.
 Require Import UList.
 Require Import FGroup.
diff --git a/coqprime/num/Lucas.v b/coqprime/num/Lucas.v
index f969dc106..dfd3e8142 100644
--- a/coqprime/num/Lucas.v
+++ b/coqprime/num/Lucas.v
@@ -14,7 +14,7 @@ Require Import ZCAux.
 Require Import W.
 Require Import Mod_op.
 Require Import LucasLehmer.
-Require Import Bits.
+Require Import Coqprime.Bits.
 Import CyclicAxioms DoubleType DoubleBase.
 
 Open Scope Z_scope. 
-- 
cgit v1.2.3