Skip to content

Commit

Permalink
fix makefile not to compile structures 3 times
Browse files Browse the repository at this point in the history
  • Loading branch information
gares committed May 18, 2020
1 parent b8d86c5 commit 1bf24d4
Showing 1 changed file with 36 additions and 10 deletions.
46 changes: 36 additions & 10 deletions Makefile.coq.local
Original file line number Diff line number Diff line change
Expand Up @@ -3,19 +3,45 @@ structures.vo : hb.elpi

#### generate many rules to generate demoN/test_HIERARCHY_USER.v ####
define MKRULE
demo$1/test_$2_$3.v: demo$1/user_$3.v structures.vo demo$1/hierarchy_$2.vo
cat demo$1/user_$3.v \
| sed 's?@@HIERARCHY@@?hierarchy_$2?' \
| sed 's?@@DEMO@@?HB.demo$1?' \
> demo$1/test_$2_$3.v
demo%/test_$1_$2.v: demo%/user_$2.v structures.vo demo%/hierarchy_$1.vo
cat demo$*/user_$2.v \
| sed 's?@@HIERARCHY@@?hierarchy_$1?' \
| sed 's?@@DEMO@@?HB.demo$*?' \
> demo$*/test_$1_$2.v
endef

$(foreach N,$(shell seq 0 10),\
$(foreach M,$(shell seq 0 10),\
$(foreach K,$(shell seq 0 10),\
$(eval $(call MKRULE,$(N),$(M),$(K))))))
# This makes make try to compile things more than onece :-/
#$(foreach N,$(shell seq 0 10),\
# $(foreach M,$(shell seq 0 10),\
# $(foreach K,$(shell seq 0 10),\
# $(eval $(call MKRULE,$(N),$(M),$(K))))))

#### add all the files we want to test ####
$(call MKRULE,0,0)
$(call MKRULE,0,1)
$(call MKRULE,0,2)
$(call MKRULE,0,3)
$(call MKRULE,1,0)
$(call MKRULE,1,1)
$(call MKRULE,1,2)
$(call MKRULE,1,3)
$(call MKRULE,2,0)
$(call MKRULE,2,1)
$(call MKRULE,2,2)
$(call MKRULE,2,3)
$(call MKRULE,3,0)
$(call MKRULE,3,1)
$(call MKRULE,3,2)
$(call MKRULE,3,3)
$(call MKRULE,4,0)
$(call MKRULE,4,1)
$(call MKRULE,4,2)
$(call MKRULE,4,3)
$(call MKRULE,5,0)
$(call MKRULE,5,1)
$(call MKRULE,5,2)
$(call MKRULE,5,3)

### add all the files we want to test ####

## demo1/

Expand Down

0 comments on commit 1bf24d4

Please sign in to comment.