build Everything.v in Makefile.composed, wrap rewriter (#2329)

Author: andres-erbsen

rewriter.BUILD.mk

@@ -1,17 +1,22 @@
 REWRITER_DIR := $(patsubst %/,%,$(dir $(lastword $(MAKEFILE_LIST))))/rewriter/src/Rewriter
-REWRITER_VFILES := $(call rwildcard,$(REWRITER_DIR),*.v)
+OCAMLPATH ?=
+export OCAMLPATH := $(REWRITER_DIR)/Util/plugins$(if $(OCAMLPATH),:$(OCAMLPATH))
+
+include rewriter/Makefile.local.common
+REWRITER_COMPAT_VFILES := $(addprefix rewriter/,$(filter %.v,$(COMPATIBILITY_FILES)))
+REWRITER_VFILES := $(sort $(call rwildcard,$(REWRITER_DIR),*.v) $(REWRITER_COMPAT_VFILES))
 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_COMPAT_VFILES): | recursive-make-rewriter-plugin
+$(O)/.coqdep.mk: | recursive-make-rewriter-plugin
+
+.PHONY: recursive-make-rewriter-optfiles
+recursive-make-rewriter-plugin: private MAKEFLAGS := --silent
+recursive-make-rewriter-plugin: | recursive-make-rewriter-plugin
+	$(MAKE) -C $(REWRITER_DIR)/../.. optfiles
+
 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

src/BUILD.mk

@@ -1,5 +1,5 @@
 FIATCRYPTO_DIR := $(patsubst %/,%,$(dir $(lastword $(MAKEFILE_LIST))))
-FIATCRYPTO_VFILES := $(call rwildcard,$(FIATCRYPTO_DIR),*.v)
+FIATCRYPTO_VFILES := $(call rwildcard,$(FIATCRYPTO_DIR),*.v) $(FIATCRYPTO_DIR)/Everything.v 
 FIATCRYPTO_COQDEPFLAGS := -R $(FIATCRYPTO_DIR) Crypto
 FIATCRYPTO_REQUIREFLAGS := -Q $(O)/$(FIATCRYPTO_DIR) Crypto
 
@@ -8,3 +8,5 @@ $(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)
+
+include $(FIATCRYPTO_DIR)/Everything.v.mk

src/Everything.v.mk

@@ -0,0 +1,25 @@
+FIATCRYPTO_EVERYTHING_VFILES := $(filter-out $(FIATCRYPTO_DIR)/Everything.v $(FIATCRYPTO_DIR)/Bedrock/Everything.v $(FIATCRYPTO_DIR)/Extraction% $(FIATCRYPTO_DIR)/PerfTesting/% $(FIATCRYPTO_DIR)/Rewriter/PerfTesting/%,$(FIATCRYPTO_VFILES))
+#
+# PerfTesting targets depend on Everything.vo
+FIATCRYPTO_COQDEPFLAGS += -R $(O)/$(FIATCRYPTO_DIR) Crypto
+
+empty :=
+space := $(empty) $(empty)
+define newline
+
+
+endef
+
+eq = $(and $(findstring $(1),$(2)),$(findstring $(2),$(1)))
+
+
+FIATCRYPTO_EVERYTHING_CONTENTS := Require Import$(newline)$(subst $(space),$(newline),$(sort $(subst /,.,$(patsubst $(FIATCRYPTO_DIR)/%.v,Crypto/%,$(FIATCRYPTO_EVERYTHING_VFILES)))))$(newline).
+
+$(O)/$(FIATCRYPTO_DIR):
+	@mkdir -p $@
+
+$(O)/$(FIATCRYPTO_DIR)/Everything.v: $(FIATCRYPTO_EVERYTHING_VFILES) | $(O)/$(FIATCRYPTO_DIR)
+	$(if $(call eq,$(file <$@),$(FIATCRYPTO_EVERYTHING_CONTENTS)),,\
+		$(file >$@,$(FIATCRYPTO_EVERYTHING_CONTENTS)$(newline)))
+
+$(O)/.coqdep.mk: | $(O)/$(FIATCRYPTO_DIR)/Everything.v