aboutsummaryrefslogtreecommitdiff
path: root/coqprime
diff options
context:
space:
mode:
authorGravatar Rob Sloan <varomodt@gmail.com>2016-01-28 13:35:03 -0500
committerGravatar Rob Sloan <varomodt@gmail.com>2016-01-28 13:35:03 -0500
commit3e0c054948a0b1fc015ad7e23bd8abd023d8e3ed (patch)
tree5d4351b816f3eecbafa7926ab53a2568eb0df9e5 /coqprime
parent75fd95e8948915328fc11033906b634768dd099e (diff)
recursive-build coqprime
Diffstat (limited to 'coqprime')
-rw-r--r--coqprime/Makefile43
-rw-r--r--coqprime/PrimalityTest/Zp.v2
-rw-r--r--coqprime/num/Lucas.v2
3 files changed, 11 insertions, 36 deletions
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.