Commit eb9dd8b3 authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen
Browse files

Hopefully fix for older versions of Coq

parent f5b806e9
Pipeline #10561 failed with stage
in 2 minutes and 4 seconds
*.vo
*.glob
.*.aux
*.v.d
.coqdeps.d
_CoqProject
CoqMakefile
CoqMakefile.conf
SRC_DIRS := 'src' $(shell test -d 'vendor' && echo 'vendor')
ALL_VFILES := $(shell find $(SRC_DIRS) -name "*.v")
TEST_VFILES := $(shell find 'src' -name "*Tests.v")
PROJ_VFILES := $(shell find 'src' -name "*.v")
VFILES := $(filter-out $(TEST_VFILES),$(PROJ_VFILES))
COQARGS :=
default: $(VFILES:.v=.vo)
test: $(TEST_VFILES:.v=.vo) $(VFILES:.v=.vo)
_CoqProject: libname $(wildcard vendor/*)
@echo "-R src $$(cat libname)" > $@
@for libdir in $(wildcard vendor/*); do \
libname=$$(cat $$libdir/libname); \
if [ $$? -ne 0 ]; then \
echo "Do you need to run git submodule update --init --recursive?" 1>&2; \
exit 1; \
fi; \
echo "-R $$libdir/src $$(cat $$libdir/libname)" >> $@; \
done
@echo "_CoqProject:"
@cat $@
.coqdeps.d: $(ALL_VFILES) _CoqProject
@echo "COQDEP $@"
@coqdep -f _CoqProject $(ALL_VFILES) > $@
ifneq ($(MAKECMDGOALS), clean)
-include .coqdeps.d
endif
%.vo: %.v _CoqProject
@echo "COQC $<"
@coqc $(COQARGS) $(shell cat '_CoqProject') $< -o $@
clean:
@echo "CLEAN vo glob aux"
@rm -f $(ALL_VFILES:.v=.vo) $(ALL_VFILES:.v=.glob)
@find $(SRC_DIRS) -name ".*.aux" -exec rm {} \;
rm -f _CoqProject .coqdeps.d
.PHONY: default test clean
.DELETE_ON_ERROR:
# Based on makefile from Iris.
# Forward most targets to Coq makefile (with some trick to make this phony)
%: CoqMakefile phony
+@make -f CoqMakefile $@
all: CoqMakefile
+@make -f CoqMakefile all
.PHONY: all
clean: CoqMakefile
+@make -f CoqMakefile clean
rm -f Makefile.coq
.PHONY: clean
# Create Coq Makefile.
CoqMakefile: _CoqProject Makefile
"$(COQBIN)coq_makefile" -f _CoqProject -o CoqMakefile
# Some files that do *not* need to be forwarded to Makefile.coq
Makefile: ;
_CoqProject: ;
opam: ;
# Phony wildcard targets
phony: ;
.PHONY: phony
-R src SmartContracts
src/Blockchain.v
src/Congress.v
-R vendor/record-update/src RecordUpdate
vendor/record-update/src/ReadmeExampleTests.v
vendor/record-update/src/RecordSetTests.v
vendor/record-update/src/RecordSet.v
vendor/record-update/src/RecordUpdate.v
vendor/record-update/src/RegressionTests.v
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment