From 48b425b3b190f1d40f60ccb4cb1fdf5521753fb9 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 17 Jun 2024 07:25:00 +0200
Subject: Deactivate some linter options for the generated Lean files

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

diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 2bc9bb25..23c0782a 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -927,6 +927,15 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
       List.iter (fun m -> Printf.fprintf out "import %s\n" m) fi.custom_includes;
       (* Always open the Primitives namespace *)
       Printf.fprintf out "open Primitives\n";
+      (* It happens that we generate duplicated namespaces, like `betree.betree`.
+         We deactivate the linter for this, because otherwise it leads to too much
+         noise. *)
+      Printf.fprintf out "set_option linter.dupNamespace false\n";
+      (* The mathlib linter generates warnings when we use hash commands like `#assert`:
+         we deactivate this linter. *)
+      Printf.fprintf out "set_option linter.hashCommand false\n";
+      (* Definitions often contain unused variables: deactivate the corresponding linter *)
+      Printf.fprintf out "set_option linter.unusedVariables false\n";
       (* If we are inside the namespace: declare it *)
       if fi.in_namespace then Printf.fprintf out "\nnamespace %s\n" fi.namespace;
       (* We might need to open the namespace *)
-- 
cgit v1.2.3