aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar Andres Erbsen <andreser@mit.edu>2016-02-28 16:31:08 -0500
committerGravatar Robert Sloan <varomodt@gmail.com>2016-06-22 13:42:14 -0400
commit93ffda26d4b9caf243a9e71a18d6e2e254a960e9 (patch)
treee2e7302e7156efff883817b21166d92e50f29c9c /Makefile
parentf566b025ae84efb7e740eb89632988b305c8f1ee (diff)
Makefile: single-quotes for shell globbing
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile23
1 files changed, 12 insertions, 11 deletions
diff --git a/Makefile b/Makefile
index 37e659dc2..890d2384e 100644
--- a/Makefile
+++ b/Makefile
@@ -1,11 +1,13 @@
-COQ_ARGS := -R coqprime/Tactic Coqprime -R coqprime/N Coqprime -R coqprime/Z Coqprime -R coqprime/List Coqprime -R coqprime/PrimalityTest Coqprime
MOD_NAME := Crypto
SRC_DIR := src
-MODULES := Curves Galois Rep Specific Tactics Util
-VS := $(MODULES:%=src/%/*.v)
-.PHONY: coq clean install coqprime
-.DEFAULT_GOAL: coq
+.PHONY: coq clean install coqprime update-_CoqProject
+.DEFAULT_GOAL := coq
+
+SORT_COQPROJECT = sed 's,[^/]*/,~&,g' | env LC_COLLATE=C sort | sed 's,~,,g'
+
+update-_CoqProject::
+ (echo '-R $(SRC_DIR) $(MOD_NAME)'; (git ls-files 'src/*.v' | $(SORT_COQPROJECT))) > _CoqProject
coq: coqprime Makefile.coq
$(MAKE) -f Makefile.coq
@@ -13,14 +15,13 @@ coq: coqprime Makefile.coq
coqprime:
$(MAKE) -C coqprime
-Makefile.coq: Makefile $(VS)
- coq_makefile -R $(SRC_DIR) $(MOD_NAME) $(COQ_ARGS) $(VS) -o Makefile.coq
+Makefile.coq: Makefile _CoqProject
+ coq_makefile -f _CoqProject -o Makefile.coq
clean: Makefile.coq
$(MAKE) -f Makefile.coq clean
rm -f Makefile.coq
-install: coq
- ln -sfL $(shell pwd)/src $(shell coqtop -where)/user-contrib/Crypto
- ln -sfL $(shell pwd)/bedrock/Bedrock $(shell coqtop -where)/user-contrib/Bedrock
-
+install: coq Makefile.coq
+ $(MAKE) -f Makefile.coq install
+ $(MAKE) -C coqprime install