From fdb8555cf6bc21ea230141373920196b078bdd28 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 27 Nov 2023 13:48:46 +0100
Subject: Do not activate the sanity (invariant) checks by default

---
 compiler/Config.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'compiler/Config.ml')

diff --git a/compiler/Config.ml b/compiler/Config.ml
index fe110ee4..48ee0a06 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -35,11 +35,11 @@ let backend = ref FStar
 
 (** {1 Interpreter} *)
 
-(** Check that invariants are maintained whenever we execute a statement
-
-    TODO: rename to sanity_checks.
+(** Activate the sanity checks, and in particular the invariant checks
+    that are performed at every evaluation step. This is very expensive
+    (~100x slow down) but very efficient to catch mistakes early.
  *)
-let check_invariants = ref true
+let sanity_checks = ref false
 
 (** Expand all symbolic values containing borrows upon introduction - allows
     to use restrict ourselves to a simpler model for the projectors over
-- 
cgit v1.2.3


From 8a6c26355ef82de725ed643f4a3c40ed54d1b4c7 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 27 Nov 2023 14:19:12 +0100
Subject: Update a comment

---
 compiler/Config.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'compiler/Config.ml')

diff --git a/compiler/Config.ml b/compiler/Config.ml
index 48ee0a06..1a00656d 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -52,7 +52,8 @@ let greedy_expand_symbolics_with_borrows = true
 
 (** Experimental.
 
-    TODO: remove (always true now)
+    TODO: remove (always true now), but check that when we panic/call a function
+    there is no bottom below a borrow.
 
     We sometimes want to temporarily break the invariant that there is no
     bottom value below a borrow. If this value is true, we don't check
-- 
cgit v1.2.3


From 6f8f1213e056804eda4c521922cdf45f4e92a509 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 27 Nov 2023 15:57:55 +0100
Subject: Fix the issues with the cross-references for OCaml doc

---
 compiler/Config.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'compiler/Config.ml')

diff --git a/compiler/Config.ml b/compiler/Config.ml
index 1a00656d..364ef748 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -289,7 +289,7 @@ let unfold_monadic_let_bindings = ref false
     we later filter the useless *forward* calls in the micro-passes, where it is
     more natural to do.
 
-    See the comments for {!val:PureMicroPasses.expression_contains_child_call_in_all_paths}
+    See the comments for {!PureMicroPasses.expression_contains_child_call_in_all_paths}
     for additional explanations.
  *)
 let filter_useless_monadic_calls = ref true
-- 
cgit v1.2.3