summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2024-06-17 07:25:00 +0200
committerSon Ho2024-06-17 07:25:00 +0200
commit48b425b3b190f1d40f60ccb4cb1fdf5521753fb9 (patch)
tree8d091974b5f77f73b3454c080ab663e43070c720
parent1021cdea98043dd935dbc8dbe633b90fda68047d (diff)
Deactivate some linter options for the generated Lean files
-rw-r--r--compiler/Translate.ml9
1 files changed, 9 insertions, 0 deletions
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 *)