From fa682c18c8ffc5fa7224d9e9d0e0dd94250ada57 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 3 Aug 2023 00:28:10 +0200
Subject: Make a minor formatting modification for Lean

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

(limited to 'compiler/Translate.ml')

diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index c5f7df92..17355dfd 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -855,7 +855,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
       (* Always open the Primitives namespace *)
       Printf.fprintf out "open Primitives\n";
       (* If we are inside the namespace: declare it, otherwise: open it *)
-      if fi.in_namespace then Printf.fprintf out "namespace %s\n" fi.namespace
+      if fi.in_namespace then Printf.fprintf out "\nnamespace %s\n" fi.namespace
       else Printf.fprintf out "open %s\n" fi.namespace
   | HOL4 ->
       Printf.fprintf out "open primitivesLib divDefLib\n";
-- 
cgit v1.2.3


From f1d171ce461e568410b6d6d3ee75aadae9bcb57b Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 4 Aug 2023 22:27:41 +0200
Subject: Fix issues with the extraction and extend the primitive libraries for
 Coq and F*

---
 compiler/Translate.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'compiler/Translate.ml')

diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 17355dfd..dfc97246 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -833,6 +833,8 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
       Printf.fprintf out "Require Import Primitives.\n";
       Printf.fprintf out "Import Primitives.\n";
       Printf.fprintf out "Require Import Coq.ZArith.ZArith.\n";
+      Printf.fprintf out "Require Import List.\n";
+      Printf.fprintf out "Import ListNotations.\n";
       Printf.fprintf out "Local Open Scope Primitives_scope.\n";
 
       (* Add the custom imports *)
-- 
cgit v1.2.3


From cb603d47be46a6957ec16b9bc68176694542e99a Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 4 Aug 2023 22:46:48 +0200
Subject: Add an option to not override Hashmap.lean

---
 compiler/Translate.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'compiler/Translate.ml')

diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index dfc97246..6c6435c5 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -1334,7 +1334,6 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
          custom_includes = [];
        }
      in
-     (* Add the extension for F* *)
      extract_file gen_config gen_ctx file_info);
 
   (* Generate the build file *)
@@ -1352,7 +1351,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
        * Generate the library entry point, if the crate is split between
        * different files.
        *)
-      if !Config.split_files then (
+      if !Config.split_files && !Config.generate_lib_entry_point then (
         let filename = Filename.concat dest_dir (crate_name ^ ".lean") in
         let out = open_out filename in
         (* Write *)
-- 
cgit v1.2.3