diff options
author | Son HO | 2024-06-18 08:33:09 +0200 |
---|---|---|
committer | GitHub | 2024-06-18 08:33:09 +0200 |
commit | 43a9fb0fa5a1c03a7cce575a052f0d4201189d1d (patch) | |
tree | c967637249ea1c9001983e09e1f04f17b8e0a1d4 /compiler/Translate.ml | |
parent | 76ab141814644a94bffc8497e5845436d86b1083 (diff) | |
parent | 878be6d051f2f920fdc6c90add8423fa6f489492 (diff) |
Merge pull request #246 from AeneasVerif/son/cleanup
Do some cleanup in the test files and the Lean backend
Diffstat (limited to 'compiler/Translate.ml')
-rw-r--r-- | compiler/Translate.ml | 9 |
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 *) |