From e692a9535cecc8a19fea9d0ebf2b470a09cf4541 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 13 Oct 2022 17:42:11 +0200
Subject: Make minor modifications to the Makefile

---
 Makefile | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index e92b2b9b..f75d00be 100644
--- a/Makefile
+++ b/Makefile
@@ -3,7 +3,7 @@ ifeq (3.81,$(MAKE_VERSION))
     install make, then invoke gmake instead of make)
 endif
 
-all: build-test-verify
+all: build-tests-verify
 
 CHARON_HOME = ../charon
 CHARON_EXEC = $(CHARON_HOME)/charon
@@ -25,7 +25,7 @@ SUBDIR :=
 
 # Build the project, test it and verify the generated files
 .PHONY: build-test-verify
-build-test-verify: build test verify
+build-tests-verify: build tests verify
 
 # Build the project
 .PHONY: build
@@ -33,15 +33,15 @@ build:
 	dune build src/main.exe
 
 # Test the project by translating test files to F*
-.PHONY: test
-test: build trans-no_nested_borrows trans-paper \
+.PHONY: tests
+tests: build trans-no_nested_borrows trans-paper \
 	trans-hashmap trans-hashmap_main \
 	trans-external trans-constants \
 	trans-nll-betree_nll trans-nll-betree_main
 
 # Verify the F* files generated by the translation
 .PHONY: verify
-verify: build test
+verify: build tests
 	cd tests && $(MAKE) all
 
 # Reformat the project
-- 
cgit v1.2.3


From e7b4aba11391bede785799237a73ef7bd16d0372 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 13 Oct 2022 18:04:31 +0200
Subject: Use "polonius" in the names instead of "nll"

---
 Makefile | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index f75d00be..93ff7431 100644
--- a/Makefile
+++ b/Makefile
@@ -37,7 +37,7 @@ build:
 tests: build trans-no_nested_borrows trans-paper \
 	trans-hashmap trans-hashmap_main \
 	trans-external trans-constants \
-	trans-nll-betree_nll trans-nll-betree_main
+	trans-polonius-betree_polonius trans-polonius-betree_main
 
 # Verify the F* files generated by the translation
 .PHONY: verify
@@ -60,8 +60,8 @@ trans-hashmap: SUBDIR:=hashmap
 trans-hashmap_main: TRANS_OPTIONS += -template-clauses
 trans-hashmap_main: SUBDIR:=hashmap_on_disk
 
-trans-nll-betree_nll: TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses
-trans-nll-betree_nll: SUBDIR:=misc
+trans-polonius-betree_polonius: TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses
+trans-polonius-betree_polonius: SUBDIR:=misc
 
 trans-constants: TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses
 trans-constants: SUBDIR:=misc
@@ -69,8 +69,8 @@ trans-constants: SUBDIR:=misc
 trans-external: TRANS_OPTIONS +=
 trans-external: SUBDIR:=misc
 
-trans-nll-betree_main: TRANS_OPTIONS += -template-clauses
-trans-nll-betree_main: SUBDIR:=betree
+trans-polonius-betree_main: TRANS_OPTIONS += -template-clauses
+trans-polonius-betree_main: SUBDIR:=betree
 
 # Generic rules to extract the LLBC from a rust file
 # We use the rules in Charon's Makefile to generate the .llbc files: the options
@@ -80,15 +80,16 @@ gen-llbc-%: build
 	cd $(CHARON_HOME) && $(MAKE) test-$*
 
 # Generic rule to test the translation of an LLBC file.
-# Note that the non-linear lifetime files are generated in the tests-nll subdirectory.
+# Note that the files requiring the Polonius borrow-checker are generated
+# in the tests-polonius subdirectory.
 .PHONY: trans-%
 trans-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests/llbc
-trans-nll-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests-nll/llbc
+trans-polonius-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests-polonius/llbc
 
 trans-%: gen-llbc-%
 	dune exec -- src/main.exe $(CHARON_TESTS_DIR)/$*.llbc -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS)
 
-trans-nll-%: gen-llbc-nll-%
+trans-polonius-%: gen-llbc-polonius-%
 	dune exec -- src/main.exe $(CHARON_TESTS_DIR)/$*.llbc -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS)
 
 .PHONY: doc
-- 
cgit v1.2.3


From 5e1e4f11dc2f75f20728ea1022b29a67c87bc07c Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 18 Oct 2022 22:39:45 +0200
Subject: Update the Makefile

---
 Makefile | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 93ff7431..c59aec01 100644
--- a/Makefile
+++ b/Makefile
@@ -75,9 +75,13 @@ trans-polonius-betree_main: SUBDIR:=betree
 # Generic rules to extract the LLBC from a rust file
 # We use the rules in Charon's Makefile to generate the .llbc files: the options
 # vary with the test files.
+.PHONY: gen-llbc-polonius-%
+gen-llbc-polonius-%: build
+	cd $(CHARON_HOME)/tests-polonius && $(MAKE) test-$*
+
 .PHONY: gen-llbc-%
 gen-llbc-%: build
-	cd $(CHARON_HOME) && $(MAKE) test-$*
+	cd $(CHARON_HOME)/tests && $(MAKE) test-$*
 
 # Generic rule to test the translation of an LLBC file.
 # Note that the files requiring the Polonius borrow-checker are generated
@@ -86,10 +90,10 @@ gen-llbc-%: build
 trans-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests/llbc
 trans-polonius-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests-polonius/llbc
 
-trans-%: gen-llbc-%
+trans-polonius-%: gen-llbc-polonius-%
 	dune exec -- src/main.exe $(CHARON_TESTS_DIR)/$*.llbc -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS)
 
-trans-polonius-%: gen-llbc-polonius-%
+trans-%: gen-llbc-%
 	dune exec -- src/main.exe $(CHARON_TESTS_DIR)/$*.llbc -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS)
 
 .PHONY: doc
-- 
cgit v1.2.3