From 87d6f6c7c90bf7b427397d6bd2e2c70d610678e3 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 4 Jul 2023 14:57:51 +0200
Subject: Reorganize the Lean tests

---
 compiler/Config.ml | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'compiler/Config.ml')

diff --git a/compiler/Config.ml b/compiler/Config.ml
index ce9b0e0c..bfb9d161 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -162,6 +162,11 @@ let backward_no_state_update = ref false
  *)
 let split_files = ref true
 
+(** For Lean, controls whether we generate a lakefile or not.
+
+ *)
+let lean_gen_lakefile = ref false
+
 (** If true, treat the unit functions (function taking no inputs and returning
     no outputs) as unit tests: evaluate them with the interpreter and check that
     they don't panic.
-- 
cgit v1.2.3


From 0a0445c72e005c328b4764f5fb0f8f38e7a55d60 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jul 2023 14:52:23 +0200
Subject: Start using namespaces in the Lean backend

---
 compiler/Config.ml | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'compiler/Config.ml')

diff --git a/compiler/Config.ml b/compiler/Config.ml
index bfb9d161..f58ba89b 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -297,3 +297,10 @@ let filter_useless_monadic_calls = ref true
       dynamically check for that).
  *)
 let filter_useless_functions = ref true
+
+(** Obsolete. TODO: remove.
+
+    For Lean we used to parameterize the entire development by a section variable
+    called opaque_defs, of type OpaqueDefs.
+  *)
+let wrap_opaque_in_sig = ref false
-- 
cgit v1.2.3


From 36c3348bacf7127d3736f9aac16a430a30424020 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 6 Jul 2023 13:46:26 +0200
Subject: Use short names for the structure fields in Lean

---
 compiler/Config.ml | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'compiler/Config.ml')

diff --git a/compiler/Config.ml b/compiler/Config.ml
index f58ba89b..0475899c 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -304,3 +304,14 @@ let filter_useless_functions = ref true
     called opaque_defs, of type OpaqueDefs.
   *)
 let wrap_opaque_in_sig = ref false
+
+(** Use short names for the record fields.
+
+    Some backends can't disambiguate records when their field names have collisions.
+    When this happens, we use long names, by which we concatenate the record
+    names with the field names, and check whether there are name collisions.
+
+    For backends which can disambiguate records (typically by using the typing
+    information), we use short names (i.e., the original field names).
+ *)
+let record_fields_short_names = ref false
-- 
cgit v1.2.3