diff options
Diffstat (limited to 'coqprime/Makefile')
| -rw-r--r-- | coqprime/Makefile | 99 |
1 files changed, 29 insertions, 70 deletions
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 $@ |