Makefile: Do not automatically rebuild backend

Automatically rebuilding the backend makes it impossible to test an out-of-tree
build with the Makefile.

Author: ttuegel

README.md

@@ -60,6 +60,7 @@ Use `docker.sh` to run commands inside the container:
 
 ``` sh
 ./docker/build.sh  # run once when dependencies change
+./docker/run.sh make  # build the backend
 ./docker/run.sh make test  # run all tests
 ./docker/run.sh make -C test/imp test  # run all tests in test/imp
 ```

include.mk

@@ -48,11 +48,11 @@ KORE_REPL_OPTS = --no-bug-report
 export KORE_REPL
 export KORE_REPL_OPTS
 
-$(KORE_EXEC):
+$(BUILD_DIR)/kore/bin/kore-exec:
 	$(STACK) $(STACK_BUILD) $(STACK_NO_PROFILE) --copy-bins kore:exe:kore-exec
 
-$(KORE_REPL):
+$(BUILD_DIR)/kore/bin/kore-repl:
 	$(STACK) $(STACK_BUILD) $(STACK_NO_PROFILE) --copy-bins kore:exe:kore-repl
 
-$(KORE_PARSER):
+$(BUILD_DIR)/kore/bin/kore-parser:
 	$(STACK) $(STACK_BUILD) $(STACK_NO_PROFILE) --copy-bins kore:exe:kore-parser

test/include.mk

@@ -19,7 +19,7 @@ KOMPILED := $(TEST_DIR)/$(DEF)-kompiled
 export KOMPILED
 DEF_KORE_DEFAULT = $(KOMPILED)/definition.kore
 DEF_KORE ?= $(DEF_KORE_DEFAULT)
-TEST_DEPS = $(K) $(KORE_PARSER) $(DEF_KORE) $(KORE_EXEC)
+TEST_DEPS = $(K) $(DEF_KORE)
 
 TESTS = \
 	$(wildcard $(DEF_DIR)/*.verify) \
@@ -44,7 +44,7 @@ KORE_EXEC_OPTS += \
 KPROVE_REPL_OPTS += -d $(DEF_DIR) -m $(KPROVE_MODULE)
 KPROVE_SPEC = $<
 
-$(DEF_KORE_DEFAULT): $(DEF_DIR)/$(DEF).k $(K) $(KORE_PARSER)
+$(DEF_KORE_DEFAULT): $(DEF_DIR)/$(DEF).k $(K)
 	@echo ">>>" $(CURDIR) "kompile" $<
 	rm -fr $(KOMPILED)
 	$(KOMPILE) $(KOMPILE_OPTS) $<
@@ -112,10 +112,10 @@ PATTERN_OPTS = --pattern "$$(cat $*.k)"
 %.save-proofs.kore: %.out
 	[ -f $@ ]
 
-%-spec.k.repl: $(TEST_DIR)/%-spec.k $(KORE_REPL) $(TEST_DEPS)
+%-spec.k.repl: $(TEST_DIR)/%-spec.k $(TEST_DEPS)
 	$(KPROVE) $(KPROVE_REPL_OPTS) $<
 
-%-spec.k.run-repl-script: $(TEST_DIR)/%-spec.k $(KORE_REPL) $(TEST_DEPS)
+%-spec.k.run-repl-script: $(TEST_DIR)/%-spec.k $(TEST_DEPS)
 	$(KPROVE) $(KPROVE_REPL_OPTS) $<
 %-spec.k.run-repl-script: KORE_REPL_OPTS= -r --repl-script $@
 
@@ -133,15 +133,15 @@ PATTERN_OPTS = --pattern "$$(cat $*.k)"
 
 ### MERGE
 
-%.merge.out: $(TEST_DIR)/%.merge $(DEF_KORE) $(KORE_EXEC)
+%.merge.out: $(TEST_DIR)/%.merge $(DEF_KORE)
 	@echo ">>>" $(CURDIR) "kore-exec --merge-rules" $<
 	rm -f $@
 	$(KORE_EXEC) $(DEF_KORE) --module $(KORE_MODULE) --merge-rules $< --output $@
 	$(DIFF) $@.golden $@ || $(FAILED)
 
 ### SCRIPTS
 
-test-%.sh.out: $(KORE_EXEC) $(TEST_DIR)/test-%.sh
+test-%.sh.out: $(TEST_DIR)/test-%.sh
 	@echo ">>>" $(CURDIR) $(@:.out=)
 	rm -f $@
 	$(TEST_DIR)/$(@:.out=) > $@ || true

test/no-injection-into-hooked/Makefile

@@ -17,7 +17,7 @@ clean:
 
 .PHONY: test-k test golden clean
 
-test-kompiled/definition.kore: test.k $(K) $(KORE_PARSER)
+test-kompiled/definition.kore: test.k $(K)
 	@echo ">>>" $(CURDIR) "kompile" $<
 	rm -fr $(KOMPILED)
 	$(KOMPILE) $(KOMPILE_OPTS) $<; if [ $$? -eq 0 ]; then exit 1; fi

test/parser/Makefile

@@ -13,7 +13,7 @@ TESTS = $(wildcard *.kore)
 OUTS += $(foreach TEST, $(TESTS), $(TEST).out)
 GOLDEN += $(foreach TEST, $(TESTS), $(TEST).golden)
 
-%.kore.out : %.kore $(KORE_PARSER)
+%.kore.out : %.kore
 	$(KORE_PARSER) --no-print-definition $< 2>$@ || true
 	$(DIFF) $*.kore.golden $@ || $(FAILED)