From 944a46fe61018e2b4266f19297daa822b41cf9e7 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 3 Apr 2024 17:23:31 +0200
Subject: Improve the Makefile

---
 Makefile | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/Makefile b/Makefile
index 98172fda..3b44e0e6 100644
--- a/Makefile
+++ b/Makefile
@@ -20,6 +20,10 @@ REGEN_LLBC ?=
 # The path to Charon
 CHARON_HOME ?= ../charon
 
+ifeq (,$(wildcard $(CHARON_HOME)))
+  $(error The directory $$CHARON_HOME does not exist$(newline)(CHARON_HOME=$(CHARON_HOME)).)
+endif
+
 # The paths to the test directories in Charon (Aeneas will look for the .llbc
 # files in there).
 CHARON_TESTS_REGULAR_DIR ?= $(CHARON_HOME)/tests
@@ -89,7 +93,7 @@ clean:
 
 # Test the project by translating test files to F*
 .PHONY: test
-test: test-no_nested_borrows test-paper \
+test: build-dev test-no_nested_borrows test-paper \
 	test-hashmap test-hashmap_main \
 	test-external test-constants \
 	testp-polonius_list testp-betree_main \
-- 
cgit v1.2.3


From 3fdb4ca62155b6d913bceb7797ee9e10263cb087 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 3 Apr 2024 17:36:05 +0200
Subject: Remove the check for CHARON_HOME

---
 Makefile | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/Makefile b/Makefile
index 3b44e0e6..1266e631 100644
--- a/Makefile
+++ b/Makefile
@@ -20,10 +20,6 @@ REGEN_LLBC ?=
 # The path to Charon
 CHARON_HOME ?= ../charon
 
-ifeq (,$(wildcard $(CHARON_HOME)))
-  $(error The directory $$CHARON_HOME does not exist$(newline)(CHARON_HOME=$(CHARON_HOME)).)
-endif
-
 # The paths to the test directories in Charon (Aeneas will look for the .llbc
 # files in there).
 CHARON_TESTS_REGULAR_DIR ?= $(CHARON_HOME)/tests
-- 
cgit v1.2.3


From e9bbac75812ef556585f14b72239133619cf1748 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 3 Apr 2024 17:49:00 +0200
Subject: Update the initial configuration

---
 compiler/Config.ml | 2 +-
 compiler/Main.ml   | 3 ---
 2 files changed, 1 insertion(+), 4 deletions(-)

diff --git a/compiler/Config.ml b/compiler/Config.ml
index 099cdc8b..0b26e2ef 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -368,4 +368,4 @@ let backend_has_tuple_projectors () =
 let use_nested_tuple_projectors = ref false
 
 (** Generate name patterns for the external definitions we encounter *)
-let extract_external_name_patterns = ref false
+let extract_external_name_patterns = ref true
diff --git a/compiler/Main.ml b/compiler/Main.ml
index 64d8ae2b..db200f37 100644
--- a/compiler/Main.ml
+++ b/compiler/Main.ml
@@ -120,9 +120,6 @@ let () =
         Arg.Set use_nested_tuple_projectors,
         " Use nested projectors for tuples (e.g., (0, 1).snd.fst instead of \
          (0, 1).1)." );
-      ( "-ext-name-pats",
-        Arg.Set extract_external_name_patterns,
-        " Generate name patterns for the external definitions we find." );
     ]
   in
 
-- 
cgit v1.2.3