Skip to content

Commit 55e33e9

Browse files
andres-erbsenandres-erbsen
committed
replace Makefile.coq with Makefile.composed
1 parent 4286517 commit 55e33e9

2 files changed

Lines changed: 29 additions & 56 deletions

File tree

‎Makefile‎

Lines changed: 20 additions & 55 deletions
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ SKIP_INCLUDE?=
2222
SKIP_COQSCRIPTS_INCLUDE?=
2323
ifneq ($(SKIP_INCLUDE),1)
2424
# this include must be before all: and validate: which are overriden below
25-
-include Makefile.coq
25+
include Makefile.composed
2626
ifneq ($(SKIP_COQSCRIPTS_INCLUDE),1)
2727
include etc/coq-scripts/Makefile.vo_closure
2828
endif
@@ -242,8 +242,6 @@ DEPFLAGS_NL :=
242242
ifneq ($(EXTERNAL_REWRITER),1)
243243
DEPFLAGS_NL:=-Q ${CURDIR_SAFE}/$(REWRITER_SRC)/$(REWRITER_NAME) $(REWRITER_NAME)\n-I ${CURDIR_SAFE}/$(REWRITER_SRC)/$(REWRITER_NAME)/Util/plugins\n$(DEPFLAGS_NL)
244244
deps: rewriter
245-
$(VOFILES): | rewriter
246-
$(ALLDFILES): | rewriter
247245
cleanall:: clean-rewriter
248246
install: install-rewriter
249247
endif
@@ -252,8 +250,6 @@ ifneq ($(SKIP_BEDROCK2),1)
252250
ifneq ($(EXTERNAL_BEDROCK2),1)
253251
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)
254252
deps: bedrock2 bedrock2-compiler rupicola
255-
$(VOFILES): | bedrock2 bedrock2-compiler rupicola
256-
$(ALLDFILES): | bedrock2 bedrock2-compiler rupicola
257253
cleanall:: clean-bedrock2 clean-bedrock2-compiler clean-rupicola
258254
install: install-bedrock2 install-bedrock2-compiler install-rupicola
259255
endif
@@ -262,85 +258,72 @@ endif
262258
ifneq ($(EXTERNAL_COQUTIL),1)
263259
DEPFLAGS_NL:=-Q ${CURDIR_SAFE}/$(COQUTIL_SRC)/$(COQUTIL_NAME) $(COQUTIL_NAME)\n$(DEPFLAGS_NL)
264260
deps: coqutil
265-
$(VOFILES): | coqutil
266-
$(ALLDFILES): | coqutil
267261
cleanall:: clean-coqutil
268262
install: install-coqutil
269263
endif
270264

271265
ifneq ($(EXTERNAL_COQPRIME),1)
272266
DEPFLAGS_NL:=-Q ${CURDIR_SAFE}/$(COQPRIME_SRC)/$(COQPRIME_NAME) $(COQPRIME_NAME)\n$(DEPFLAGS_NL)
273267
deps: coqprime
274-
$(VOFILES): | coqprime
275-
$(ALLDFILES): | coqprime
276268
cleanall:: clean-coqprime
277269
install: install-coqprime
278270
endif
279271

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

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

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

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

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

294-
rewriter:
295-
$(MAKE) --no-print-directory -C $(REWRITER_FOLDER)
284+
rewriter: $(REWRITER_VOFILES)
296285

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

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

303-
coqutil:
304-
$(MAKE) --no-print-directory -C $(COQUTIL_FOLDER)
292+
coqutil: $(COQUTIL_VOFILES)
305293

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

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

312-
bedrock2: coqutil
313-
$(MAKE) --no-print-directory -C $(BEDROCK2_ROOT_FOLDER) bedrock2_ex
300+
bedrock2: coqutil $(BEDROCK_VOFILES) $(BEDROCK_EXAMPLES_VOFILES)
314301

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

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

321-
bedrock2-compiler: bedrock2
322-
$(MAKE) --no-print-directory -C $(BEDROCK2_ROOT_FOLDER) compiler_noex
309+
bedrock2-compiler: bedrock2 $(BEDROCK_COMPILER_VOFILES)
323310

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

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

331-
rupicola: bedrock2 | bedrock2-compiler
332-
$(MAKE) --no-print-directory -C $(RUPICOLA_FOLDER) all
317+
rupicola: bedrock2 bedrock2-compiler $(RUPICOLA_VOFILES)
333318

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

337322
install-rupicola:
338323
$(MAKE) --no-print-directory -C $(RUPICOLA_FOLDER) install_lib
339324
endif
340325

341-
Makefile.coq: Makefile _CoqProject
342-
$(SHOW)'COQ_MAKEFILE -f _CoqProject > $@'
343-
$(HIDE)$(COQBIN)coq_makefile -f _CoqProject INSTALLDEFAULTROOT = $(INSTALLDEFAULTROOT) -o $@
326+
344327

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

341+
src/ExtractionOCaml/%.ml : private COQLIBS += $(FIATCRYPTO_COQFLAGS)
342+
src/ExtractionJsOfOCaml/%.ml : private COQLIBS += $(FIATCRYPTO_COQFLAGS)
343+
src/ExtractionHaskell/%.hs : private COQLIBS += $(FIATCRYPTO_COQFLAGS)
344+
358345
pre-standalone-extracted: $(STANDALONE_OCAML:%=src/ExtractionOCaml/%.ml) $(STANDALONE_JS_OF_OCAML:%=src/ExtractionJsOfOCaml/%.ml) $(STANDALONE_HASKELL:%=src/ExtractionHaskell/%.hs)
359346

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

494-
clean::
495-
rm -f Makefile.coq
481+
496482

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

539-
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)))))
540-
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)))))
541-
make_Everything_v_cmd_gen = { printf 'Require Import\n'; printf '%s\n' $(1); printf '.\n'; }
542-
make_Everything_v_cmd := $(call make_Everything_v_cmd_gen,$(REGULAR_EXCEPT_BEDROCK2_LIBS))
543-
make_Bedrock_Everything_v_cmd := $(call make_Everything_v_cmd_gen,$(REGULAR_WITH_BEDROCK2_LIBS))
544-
EXISTING_EVERYTHING_V_CONTENTS:=$(shell cat src/Everything.v 2>&1)
545-
EXISTING_BEDROCK_EVERYTHING_V_CONTENTS:=$(shell cat src/Bedrock/Everything.v 2>&1)
546-
NEW_EVERYTHING_V_CONTENTS:=$(shell $(make_Everything_v_cmd))
547-
NEW_BEDROCK_EVERYTHING_V_CONTENTS:=$(shell $(make_Bedrock_Everything_v_cmd))
548-
ifneq ($(EXISTING_EVERYTHING_V_CONTENTS),$(NEW_EVERYTHING_V_CONTENTS))
549-
.PHONY: src/Everything.v
550-
src/Everything.v:
551-
$(SHOW)'ECHO > $@'
552-
$(HIDE)$(make_Everything_v_cmd) > $@
553-
endif
554525

555-
ifneq ($(EXISTING_BEDROCK_EVERYTHING_V_CONTENTS),$(NEW_BEDROCK_EVERYTHING_V_CONTENTS))
556-
.PHONY: src/Bedrock/Everything.v
557-
src/Bedrock/Everything.v:
558-
$(SHOW)'ECHO > $@'
559-
$(HIDE)$(make_Bedrock_Everything_v_cmd) > $@
560-
endif

‎Makefile.composed‎

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,14 @@ include coqprime.BUILD.mk
1414
include rewriter.BUILD.mk
1515
include src/BUILD.mk
1616

17+
COQPRIME_VOFILES := $(patsubst %.v, $(O)/%.vo, $(COQPRIME_VFILES))
18+
REWRITER_VOFILES := $(patsubst %.v, $(O)/%.vo, $(REWRITER_VFILES))
19+
COQUTIL_VOFILES := $(patsubst %.v, $(O)/%.vo, $(COQUTIL_VFILES))
20+
BEDROCK_VOFILES := $(patsubst %.v, $(O)/%.vo, $(BEDROCK_VFILES))
21+
BEDROCK_EXAMPLES_VOFILES := $(patsubst %.v, $(O)/%.vo, $(BEDROCK_EXAMPLES_VFILES))
22+
BEDROCK_COMPILER_VOFILES := $(patsubst %.v, $(O)/%.vo, $(BEDROCK_COMPILER_VFILES))
23+
RUPICOLA_VOFILES := $(patsubst %.v, $(O)/%.vo, $(RUPICOLA_VFILES))
24+
1725
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)
1826
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)
1927
include rupicola/bedrock2/deps/coqutil/vfiles_rules.mk
@@ -24,5 +32,5 @@ all: $(filter-out $(O)/$(FIATCRYPTO_DIR)/PerfTesting/% $(O)/$(FIATCRYPTO_DIR)/Re
2432
.PHONY: check
2533
check: all
2634
.PHONY: clean
27-
clean: vfiles_clean
35+
clean:: vfiles_clean
2836
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

0 commit comments

Comments
 (0)