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


From 9c09789c26dd8142b8a29b42e250a685aa983e58 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 27 May 2024 11:22:37 +0200
Subject: runner: Support negative tests

---
 Makefile | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index bda88c74..38da9f7e 100644
--- a/Makefile
+++ b/Makefile
@@ -25,7 +25,7 @@ CHARON_OPTIONS ?=
 # The directory thta contains the rust source files for tests.
 INPUTS_DIR ?= tests/src
 # The directory where to look for the .llbc files.
-LLBC_DIR ?= $(PWD)/tests/llbc
+LLBC_DIR ?= tests/llbc
 
 # In CI, we enforce formatting and activate the (expensive) sanity checks.
 IN_CI ?=
@@ -157,6 +157,8 @@ verify:
 
 # List the files and directories in `INPUTS_DIR`
 INPUTS_LIST = $(wildcard $(INPUTS_DIR)/*)
+# Remove the committed output files
+INPUTS_LIST := $(filter-out %.out,$(INPUTS_LIST))
 # Remove the directory prefix, replace with `test-`
 INPUTS_LIST := $(subst $(INPUTS_DIR)/,test-,$(INPUTS_LIST))
 
-- 
cgit v1.2.3


From b5046454b47aba598a42d3d775d2ec54dc57c75a Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 28 May 2024 16:05:56 +0200
Subject: ci: Check correctness of the charon pinned commit

---
 Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 38da9f7e..b27fe0de 100644
--- a/Makefile
+++ b/Makefile
@@ -90,7 +90,7 @@ update-charon-pin:
 # Keep the commit revision in `./charon-pin` as well so that non-nix users can
 # know which commit to use.
 ./charon-pin: flake.lock
-	nix-shell -p jq --run './scripts/update-charon-pin.sh' >> ./charon-pin
+	./scripts/update-charon-pin.sh >> ./charon-pin
 
 # Checks that `./charon` contains a clone of charon at the required commit.
 # Also checks that `./charon/bin/charon` exists.
-- 
cgit v1.2.3


From 4195b9653b2d00b846edd3b74211f129192a8806 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 30 May 2024 15:36:08 +0200
Subject: Update charon pin to local commit when developing

---
 Makefile | 11 +++--------
 1 file changed, 3 insertions(+), 8 deletions(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index b27fe0de..1e832378 100644
--- a/Makefile
+++ b/Makefile
@@ -81,16 +81,11 @@ build-bin-dir: build-bin build-lib build-runner
 doc:
 	cd compiler && dune build @doc
 
-# Fetches the latest commit from charon and updates `flake.lock` accordingly.
+# Updates `flake.lock` and `charon-pin` with the latest commit from Charon. If
+# we're using a symlink, this takes the commit from our local charon.
 .PHONY: update-charon-pin
 update-charon-pin:
-	nix flake lock --update-input charon
-	$(MAKE) charon-pin
-
-# Keep the commit revision in `./charon-pin` as well so that non-nix users can
-# know which commit to use.
-./charon-pin: flake.lock
-	./scripts/update-charon-pin.sh >> ./charon-pin
+	./scripts/update-charon-pin.sh
 
 # Checks that `./charon` contains a clone of charon at the required commit.
 # Also checks that `./charon/bin/charon` exists.
-- 
cgit v1.2.3