merge composed build

Author: andres-erbsen

.gitignore

@@ -1,3 +1,8 @@
+# make
+/o/
+/.coqdep.mk
+/src/_CoqProject
+
 # vim
 [._]*.s[a-v][a-z]
 [._]*.sw[a-p]

Makefile.composed

@@ -0,0 +1,28 @@
+COQFLAGS :=
+O:=.
+
+include rupicola/bedrock2/deps/coqutil/globalsettings.mk
+include rupicola/bedrock2/deps/coqutil/src/coqutil/BUILD.mk
+include rupicola/bedrock2/deps/coqutil/test/BUILD.mk
+include rupicola/bedrock2/bedrock2/src/bedrock2/BUILD.mk
+include rupicola/bedrock2/bedrock2/src/bedrock2Examples/BUILD.mk
+include rupicola/bedrock2/deps/riscv-coq/src/riscv/BUILD.mk
+include rupicola/bedrock2/compiler/src/compiler/BUILD.mk
+include rupicola/bedrock2/compiler/src/compilerExamples/BUILD.mk
+include rupicola/src/Rupicola/BUILD.mk
+include coqprime.BUILD.mk
+include rewriter.BUILD.mk
+include src/BUILD.mk
+
+VFILES := $(COQPRIME_VFILES) $(REWRITER_VFILES) $(COQUTIL_VFILES) $(COQUTIL_TEST_VFILES) $(BEDROCK_VFILES) $(BEDROCK_EXAMPLES_VFILES) $(RISCV_VFILES) $(BEDROCK_COMPILER_VFILES) $(BEDROCK_COMPILER_EXAMPLES_VFILES) $(RUPICOLA_VFILES) $(FIATCRYPTO_VFILES)
+COQDEPFLAGS := -w +default $(COQPRIME_COQDEPFLAGS) $(REWRITER_COQDEPFLAGS) $(COQUTIL_COQDEPFLAGS) $(BEDROCK_COQDEPFLAGS) $(BEDROCK_EXAMPLES_COQDEPFLAGS) $(RISCV_COQDEPFLAGS) $(BEDROCK_COMPILER_COQDEPFLAGS) $(BEDROCK_COMPILER_EXAMPLES_COQDEPFLAGS) $(RUPICOLA_COQDEPFLAGS) $(FIATCRYPTO_COQDEPFLAGS)
+include rupicola/bedrock2/deps/coqutil/vfiles_rules.mk
+
+.PHONY: all
+all: $(filter-out $(O)/$(FIATCRYPTO_DIR)/PerfTesting/% $(O)/$(FIATCRYPTO_DIR)/Rewriter/PerfTesting/% $(O)/$(FIATCRYPTO_DIR)/Extraction%,$(VOFILES)) \
+	$(COQUTIL_DIR)/_CoqProject $(COQUTIL_TEST_DIR)/_CoqProject $(BEDROCK_EXAMPLES_DIR)/_CoqProject $(RISCV_DIR)/_CoqProject $(BEDROCK_COMPILER_DIR)/_CoqProject $(BEDROCK_COMPILER_EXAMPLES_DIR)/_CoqProject $(RUPICOLA_DIR)/_CoqProject $(FIATCRYPTO_DIR)/_CoqProject
+.PHONY: check
+check: all
+.PHONY: clean
+clean: vfiles_clean
+	rm -f $(COQUTIL_DIR)/_CoqProject $(COQUTIL_TEST_DIR)/_CoqProject $(BEDROCK_EXAMPLES_DIR)/_CoqProject $(RISCV_DIR)/_CoqProject $(BEDROCK_COMPILER_DIR)/_CoqProject $(BEDROCK_COMPILER_EXAMPLES_DIR)/_CoqProject $(RUPICOLA_DIR)/_CoqProject $(FIATCRYPTO_DIR)/_CoqProject

coqprime.BUILD.mk

@@ -0,0 +1,10 @@
+COQPRIME_DIR := $(patsubst %/,%,$(dir $(lastword $(MAKEFILE_LIST))))/coqprime/src/Coqprime
+COQPRIME_VFILES := $(filter-out $(COQPRIME_DIR)/examples/% $(COQPRIME_DIR)/num/%,$(call rwildcard,$(COQPRIME_DIR),*.v))
+COQPRIME_COQDEPFLAGS := -Q $(COQPRIME_DIR) $(notdir $(COQPRIME_DIR))
+COQPRIME_REQUIREFLAGS := -Q $(O)/$(COQPRIME_DIR) $(notdir $(COQPRIME_DIR))
+
+COQPRIME_COQFLAGS := $(COQPRIME_REQUIREFLAGS)
+$(O)/$(COQPRIME_DIR)/%.vo: private COQFLAGS += $(COQPRIME_COQFLAGS)
+$(O)/$(COQPRIME_DIR)/%.vos: private COQFLAGS += $(COQPRIME_COQFLAGS)
+$(O)/$(COQPRIME_DIR)/%.vok: private COQFLAGS += $(COQPRIME_COQFLAGS)
+# $(COQPRIME_DIR)/_CoqProject: private COQFLAGS += $(COQPRIME_COQFLAGS)

rewriter.BUILD.mk

@@ -0,0 +1,17 @@
+REWRITER_DIR := $(patsubst %/,%,$(dir $(lastword $(MAKEFILE_LIST))))/rewriter/src/Rewriter
+REWRITER_VFILES := $(call rwildcard,$(REWRITER_DIR),*.v)
+REWRITER_COQDEPFLAGS := -I $(REWRITER_DIR)/Util/plugins -Q $(REWRITER_DIR) $(notdir $(REWRITER_DIR))
+REWRITER_REQUIREFLAGS := -I $(REWRITER_DIR)/Util/plugins -Q $(O)/$(REWRITER_DIR) $(notdir $(REWRITER_DIR))
+
+REWRITER_COQFLAGS := $(REWRITER_REQUIREFLAGS)
+$(O)/$(REWRITER_DIR)/%.vo: private COQFLAGS += $(REWRITER_COQFLAGS)
+$(O)/$(REWRITER_DIR)/%.vos: private COQFLAGS += $(REWRITER_COQFLAGS)
+$(O)/$(REWRITER_DIR)/%.vok: private COQFLAGS += $(REWRITER_COQFLAGS)
+$(O)/$(REWRITER_DIR)/Util/plugins/%.vo: rewriterplugin
+$(O)/$(REWRITER_DIR)/Util/plugins/%.vos: rewriterplugin
+$(O)/$(REWRITER_DIR)/Util/plugins/%.vok: rewriterplugin
+# .PHONY: rewriterplugin
+# rewriterplugin: private MAKEFLAGS := --silent
+# rewriterplugin:
+# 	$(MAKE) -C $(REWRITER_DIR)/../.. optfiles
+# $(O)/.coqdep.mk: | rewriterplugin

rupicola

@@ -0,0 +1,10 @@
+FIATCRYPTO_DIR := $(patsubst %/,%,$(dir $(lastword $(MAKEFILE_LIST))))
+FIATCRYPTO_VFILES := $(call rwildcard,$(FIATCRYPTO_DIR),*.v)
+FIATCRYPTO_COQDEPFLAGS := -R $(FIATCRYPTO_DIR) Crypto
+FIATCRYPTO_REQUIREFLAGS := -Q $(O)/$(FIATCRYPTO_DIR) Crypto
+
+FIATCRYPTO_COQFLAGS := $(COQPRIME_REQUIREFLAGS) $(REWRITER_REQUIREFLAGS) $(COQUTIL_REQUIREFLAGS) $(BEDROCK_REQUIREFLAGS) $(BEDROCK_EXAMPLES_REQUIREFLAGS) $(RISCV_REQUIREFLAGS) $(BEDROCK_COMPILER_REQUIREFLAGS) $(BEDROCK_COMPILER_EXAMPLES_REQUIREFLAGS) $(RUPICOLA_REQUIREFLAGS) -R $(O)/$(FIATCRYPTO_DIR) Crypto -w -deprecated-from-Coq,-deprecated-since-9.0,-deprecated-since-8.20
+$(O)/$(FIATCRYPTO_DIR)/%.vo: private COQFLAGS += $(FIATCRYPTO_COQFLAGS)
+$(O)/$(FIATCRYPTO_DIR)/%.vos: private COQFLAGS += $(FIATCRYPTO_COQFLAGS)
+$(O)/$(FIATCRYPTO_DIR)/%.vok: private COQFLAGS += $(FIATCRYPTO_COQFLAGS)
+$(FIATCRYPTO_DIR)/_CoqProject: private COQFLAGS += $(FIATCRYPTO_COQFLAGS)