From c0a6916549b55fbae2226e4c34af45e500928645 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 24 May 2024 14:56:26 +0200 Subject: Fix running individual tests --- Makefile | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index b3dc9f2b..ca3bd66c 100644 --- a/Makefile +++ b/Makefile @@ -47,7 +47,12 @@ build-test-verify: build test verify # Build the project, without formatting the code .PHONY: build-dev +ifdef IN_CI +build-dev: + @true +else build-dev: build-bin build-lib build-bin-dir doc +endif .PHONY: build-bin build-bin: check-charon @@ -166,14 +171,13 @@ test-all: $(INPUTS_LIST) ifdef IN_CI # In CI we do extra sanity checks. test-%: AENEAS_OPTIONS += -checks -else -test-%: check-charon endif # Translate the given rust file to available backends. The test runner decides # which backends to use and sets test-specific options. +# Note: the tests have the fulle file name: `test-arrays.rs`, `test-loops.rs`, `test-betree`. .PHONY: test-% -test-%: +test-%: build-dev $(TEST_RUNNER_EXE) $(CHARON_EXE) $(AENEAS_EXE) $(LLBC_DIR) $(INPUTS_DIR)/"$*" $(AENEAS_OPTIONS) echo "# Test $* done" -- cgit v1.2.3 From 4d3778bea3112168645efc03308056ec341abb5f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 24 May 2024 15:47:20 +0200 Subject: runner: Pass options in special comments --- Makefile | 4 ---- 1 file changed, 4 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index ca3bd66c..bda88c74 100644 --- a/Makefile +++ b/Makefile @@ -159,10 +159,6 @@ verify: INPUTS_LIST = $(wildcard $(INPUTS_DIR)/*) # Remove the directory prefix, replace with `test-` INPUTS_LIST := $(subst $(INPUTS_DIR)/,test-,$(INPUTS_LIST)) -# Remove some tests we don't want to run. -# FIXME: move this information to the file itself -INPUTS_LIST := $(filter-out test-hashmap_utils.rs,$(INPUTS_LIST)) -INPUTS_LIST := $(filter-out test-nested_borrows.rs,$(INPUTS_LIST)) # Run all the tests we found. .PHONY: test-all -- cgit v1.2.3