Skip to content

Replace coq_makefile with Makefile.composed #2330

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
andres-erbsen wants to merge 3 commits into
base: master
Choose a base branch
from
Draft

Replace coq_makefile with Makefile.composed #2330

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
4286517
build Everything.v in Makefile.composed, wrap rewriter
andres-erbsen May 12, 2026
55e33e9
replace Makefile.coq with Makefile.composed
andres-erbsen May 12, 2026
dd1e0fd
Merge branch 'master' into replace-coq-makefile
andres-erbsen May 13, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
75 changes: 20 additions & 55 deletions Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ SKIP_INCLUDE?=
SKIP_COQSCRIPTS_INCLUDE?=
ifneq ($(SKIP_INCLUDE),1)
# this include must be before all: and validate: which are overriden below
-include Makefile.coq
include Makefile.composed
ifneq ($(SKIP_COQSCRIPTS_INCLUDE),1)
include etc/coq-scripts/Makefile.vo_closure
endif
Expand Down Expand Up @@ -242,8 +242,6 @@ DEPFLAGS_NL :=
ifneq ($(EXTERNAL_REWRITER),1)
DEPFLAGS_NL:=-Q ${CURDIR_SAFE}/$(REWRITER_SRC)/$(REWRITER_NAME) $(REWRITER_NAME)\n-I ${CURDIR_SAFE}/$(REWRITER_SRC)/$(REWRITER_NAME)/Util/plugins\n$(DEPFLAGS_NL)
deps: rewriter
$(VOFILES): | rewriter
$(ALLDFILES): | rewriter
cleanall:: clean-rewriter
install: install-rewriter
endif
Expand All @@ -252,8 +250,6 @@ ifneq ($(SKIP_BEDROCK2),1)
ifneq ($(EXTERNAL_BEDROCK2),1)
DEPFLAGS_NL:=-Q ${CURDIR_SAFE}/$(RUPICOLA_SRC)/$(RUPICOLA_NAME) $(RUPICOLA_NAME) \n-Q ${CURDIR_SAFE}/$(BEDROCK2_SRC)/$(BEDROCK2_NAME) $(BEDROCK2_NAME)\n-Q ${CURDIR_SAFE}/$(BEDROCK2_EXAMPLES_SRC)/$(BEDROCK2_EXAMPLES_NAME) $(BEDROCK2_EXAMPLES_NAME)\n-Q ${CURDIR_SAFE}/$(BEDROCK2_COMPILER_SRC)/$(BEDROCK2_COMPILER_NAME) $(BEDROCK2_COMPILER_NAME)\n-Q ${CURDIR_SAFE}/$(RISCV_SRC)/$(RISCV_NAME) $(RISCV_NAME)\n$(DEPFLAGS_NL)
deps: bedrock2 bedrock2-compiler rupicola
$(VOFILES): | bedrock2 bedrock2-compiler rupicola
$(ALLDFILES): | bedrock2 bedrock2-compiler rupicola
cleanall:: clean-bedrock2 clean-bedrock2-compiler clean-rupicola
install: install-bedrock2 install-bedrock2-compiler install-rupicola
endif
Expand All @@ -262,85 +258,72 @@ endif
ifneq ($(EXTERNAL_COQUTIL),1)
DEPFLAGS_NL:=-Q ${CURDIR_SAFE}/$(COQUTIL_SRC)/$(COQUTIL_NAME) $(COQUTIL_NAME)\n$(DEPFLAGS_NL)
deps: coqutil
$(VOFILES): | coqutil
$(ALLDFILES): | coqutil
cleanall:: clean-coqutil
install: install-coqutil
endif

ifneq ($(EXTERNAL_COQPRIME),1)
DEPFLAGS_NL:=-Q ${CURDIR_SAFE}/$(COQPRIME_SRC)/$(COQPRIME_NAME) $(COQPRIME_NAME)\n$(DEPFLAGS_NL)
deps: coqprime
$(VOFILES): | coqprime
$(ALLDFILES): | coqprime
cleanall:: clean-coqprime
install: install-coqprime
endif

DEPFLAGS:=$(subst \n, ,$(DEPFLAGS_NL))

coqprime:
$(MAKE) --no-print-directory -C $(COQPRIME_FOLDER) src/Coqprime/PrimalityTest/Zp.vo src/Coqprime/PrimalityTest/PocklingtonCertificat.vo
coqprime: $(COQPRIME_VOFILES)

coqprime-all: coqprime
$(MAKE) --no-print-directory -C $(COQPRIME_FOLDER)

clean-coqprime:
$(MAKE) --no-print-directory -C $(COQPRIME_FOLDER) clean
rm -f $(COQPRIME_VOFILES) $(COQPRIME_VOFILES:.vo=.vos) $(COQPRIME_VOFILES:.vo=.vok) $(COQPRIME_VOFILES:.vo=.glob)

install-coqprime:
$(MAKE) --no-print-directory -C $(COQPRIME_FOLDER) install

rewriter:
$(MAKE) --no-print-directory -C $(REWRITER_FOLDER)
rewriter: $(REWRITER_VOFILES)

clean-rewriter:
$(MAKE) --no-print-directory -C $(REWRITER_FOLDER) clean
rm -f $(REWRITER_VOFILES) $(REWRITER_VOFILES:.vo=.vos) $(REWRITER_VOFILES:.vo=.vok) $(REWRITER_VOFILES:.vo=.glob)

install-rewriter:
$(MAKE) --no-print-directory -C $(REWRITER_FOLDER) install

coqutil:
$(MAKE) --no-print-directory -C $(COQUTIL_FOLDER)
coqutil: $(COQUTIL_VOFILES)

clean-coqutil:
$(MAKE) --no-print-directory -C $(COQUTIL_FOLDER) clean
rm -f $(COQUTIL_VOFILES) $(COQUTIL_VOFILES:.vo=.vos) $(COQUTIL_VOFILES:.vo=.vok) $(COQUTIL_VOFILES:.vo=.glob)

install-coqutil:
$(MAKE) --no-print-directory -C $(COQUTIL_FOLDER) install

bedrock2: coqutil
$(MAKE) --no-print-directory -C $(BEDROCK2_ROOT_FOLDER) bedrock2_ex
bedrock2: coqutil $(BEDROCK_VOFILES) $(BEDROCK_EXAMPLES_VOFILES)

clean-bedrock2:
$(MAKE) --no-print-directory -C $(BEDROCK2_ROOT_FOLDER) clean_bedrock2
rm -f $(BEDROCK_VOFILES) $(BEDROCK_VOFILES:.vo=.vos) $(BEDROCK_VOFILES:.vo=.vok) $(BEDROCK_VOFILES:.vo=.glob)
rm -f $(BEDROCK_EXAMPLES_VOFILES) $(BEDROCK_EXAMPLES_VOFILES:.vo=.vos) $(BEDROCK_EXAMPLES_VOFILES:.vo=.vok) $(BEDROCK_EXAMPLES_VOFILES:.vo=.glob)

install-bedrock2:
$(MAKE) --no-print-directory -C $(BEDROCK2_ROOT_FOLDER) install_bedrock2

bedrock2-compiler: bedrock2
$(MAKE) --no-print-directory -C $(BEDROCK2_ROOT_FOLDER) compiler_noex
bedrock2-compiler: bedrock2 $(BEDROCK_COMPILER_VOFILES)

clean-bedrock2-compiler:
$(MAKE) --no-print-directory -C $(BEDROCK2_ROOT_FOLDER) clean_deps
$(MAKE) --no-print-directory -C $(BEDROCK2_ROOT_FOLDER) clean_compiler
rm -f $(BEDROCK_COMPILER_VOFILES) $(BEDROCK_COMPILER_VOFILES:.vo=.vos) $(BEDROCK_COMPILER_VOFILES:.vo=.vok) $(BEDROCK_COMPILER_VOFILES:.vo=.glob)

install-bedrock2-compiler:
$(MAKE) --no-print-directory -C $(BEDROCK2_ROOT_FOLDER) install_compiler

rupicola: bedrock2 | bedrock2-compiler
$(MAKE) --no-print-directory -C $(RUPICOLA_FOLDER) all
rupicola: bedrock2 bedrock2-compiler $(RUPICOLA_VOFILES)

clean-rupicola:
$(MAKE) --no-print-directory -C $(RUPICOLA_FOLDER) clean
rm -f $(RUPICOLA_VOFILES) $(RUPICOLA_VOFILES:.vo=.vos) $(RUPICOLA_VOFILES:.vo=.vok) $(RUPICOLA_VOFILES:.vo=.glob)

install-rupicola:
$(MAKE) --no-print-directory -C $(RUPICOLA_FOLDER) install_lib
endif

Makefile.coq: Makefile _CoqProject
$(SHOW)'COQ_MAKEFILE -f _CoqProject > $@'
$(HIDE)$(COQBIN)coq_makefile -f _CoqProject INSTALLDEFAULTROOT = $(INSTALLDEFAULTROOT) -o $@


include Makefile.examples
include Makefile.standalone
Expand All @@ -355,6 +338,10 @@ $(STANDALONE_JS_OF_OCAML:%=src/ExtractionJsOfOCaml/%.ml): src/StandaloneJsOfOCam
$(BEDROCK2_STANDALONE_JS_OF_OCAML:%=src/ExtractionJsOfOCaml/%.ml): src/Bedrock/Standalone/StandaloneJsOfOCamlMain.vo
# $(PERF_STANDALONE:%=src/ExtractionHaskell/%.hs): src/Rewriter/PerfTesting/StandaloneHaskellMain.vo

src/ExtractionOCaml/%.ml : private COQLIBS += $(FIATCRYPTO_COQFLAGS)
src/ExtractionJsOfOCaml/%.ml : private COQLIBS += $(FIATCRYPTO_COQFLAGS)
src/ExtractionHaskell/%.hs : private COQLIBS += $(FIATCRYPTO_COQFLAGS)

pre-standalone-extracted: $(STANDALONE_OCAML:%=src/ExtractionOCaml/%.ml) $(STANDALONE_JS_OF_OCAML:%=src/ExtractionJsOfOCaml/%.ml) $(STANDALONE_HASKELL:%=src/ExtractionHaskell/%.hs)

$(STANDALONE_OCAML:%=src/ExtractionOCaml/%.ml) : %.ml : %.v
Expand Down Expand Up @@ -491,8 +478,7 @@ $(ACCEPT_OUTPUTS) : accept-% :
$(SHOW)'ACCEPT $*.out'
$(HIDE)cp -f $*.out output-tests/$*.expected

clean::
rm -f Makefile.coq


cleanall:: clean
rm -rf src/Rewriter/PerfTesting/Specific/generated
Expand Down Expand Up @@ -536,25 +522,4 @@ printdeps::
printreversedeps::
$(HIDE)$(foreach vo,$(filter %.vo,$(MAKECMDGOALS)),echo '$(vo): $(call vo_reverse_closure,$(VOFILES),$(vo))'; )

REGULAR_WITH_BEDROCK2_LIBS := $(sort $(subst /,.,$(patsubst src/%.vo,Crypto/%,$(filter-out src/Bedrock/Everything.vo src/Everything.vo $(AFTER_EVERYTHING_VOFILES),$(REGULAR_WITH_BEDROCK2_VOFILES)))))
REGULAR_EXCEPT_BEDROCK2_LIBS := $(sort $(subst /,.,$(patsubst src/%.vo,Crypto/%,$(filter-out src/Bedrock/Everything.vo src/Everything.vo $(AFTER_EVERYTHING_VOFILES),$(REGULAR_EXCEPT_BEDROCK2_VOFILES)))))
make_Everything_v_cmd_gen = { printf 'Require Import\n'; printf '%s\n' $(1); printf '.\n'; }
make_Everything_v_cmd := $(call make_Everything_v_cmd_gen,$(REGULAR_EXCEPT_BEDROCK2_LIBS))
make_Bedrock_Everything_v_cmd := $(call make_Everything_v_cmd_gen,$(REGULAR_WITH_BEDROCK2_LIBS))
EXISTING_EVERYTHING_V_CONTENTS:=$(shell cat src/Everything.v 2>&1)
EXISTING_BEDROCK_EVERYTHING_V_CONTENTS:=$(shell cat src/Bedrock/Everything.v 2>&1)
NEW_EVERYTHING_V_CONTENTS:=$(shell $(make_Everything_v_cmd))
NEW_BEDROCK_EVERYTHING_V_CONTENTS:=$(shell $(make_Bedrock_Everything_v_cmd))
ifneq ($(EXISTING_EVERYTHING_V_CONTENTS),$(NEW_EVERYTHING_V_CONTENTS))
.PHONY: src/Everything.v
src/Everything.v:
$(SHOW)'ECHO > $@'
$(HIDE)$(make_Everything_v_cmd) > $@
endif

ifneq ($(EXISTING_BEDROCK_EVERYTHING_V_CONTENTS),$(NEW_BEDROCK_EVERYTHING_V_CONTENTS))
.PHONY: src/Bedrock/Everything.v
src/Bedrock/Everything.v:
$(SHOW)'ECHO > $@'
$(HIDE)$(make_Bedrock_Everything_v_cmd) > $@
endif
10 changes: 9 additions & 1 deletion Makefile.composed
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,14 @@ include coqprime.BUILD.mk
include rewriter.BUILD.mk
include src/BUILD.mk

COQPRIME_VOFILES := $(patsubst %.v, $(O)/%.vo, $(COQPRIME_VFILES))
REWRITER_VOFILES := $(patsubst %.v, $(O)/%.vo, $(REWRITER_VFILES))
COQUTIL_VOFILES := $(patsubst %.v, $(O)/%.vo, $(COQUTIL_VFILES))
BEDROCK_VOFILES := $(patsubst %.v, $(O)/%.vo, $(BEDROCK_VFILES))
BEDROCK_EXAMPLES_VOFILES := $(patsubst %.v, $(O)/%.vo, $(BEDROCK_EXAMPLES_VFILES))
BEDROCK_COMPILER_VOFILES := $(patsubst %.v, $(O)/%.vo, $(BEDROCK_COMPILER_VFILES))
RUPICOLA_VOFILES := $(patsubst %.v, $(O)/%.vo, $(RUPICOLA_VFILES))

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
Expand All @@ -24,5 +32,5 @@ all: $(filter-out $(O)/$(FIATCRYPTO_DIR)/PerfTesting/% $(O)/$(FIATCRYPTO_DIR)/Re
.PHONY: check
check: all
.PHONY: clean
clean: vfiles_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
Loading