Lean: ignore unused variables (#1013)

This reduces the number of warnings+errors from 3021 to 1562 on the RISC-V spec. This closes #1011. Co-authored-by: Léo Stefanesco <[email protected]>
rems-project · Feb 16, 2025 · ecfe107 · ecfe107
1 parent 6ae1f3d
commit ecfe107
Show file tree

Hide file tree

Showing 29 changed files with 115 additions and 0 deletions.
diff --git a/src/sail_lean_backend/sail_plugin_lean.ml b/src/sail_lean_backend/sail_plugin_lean.ml
@@ -193,6 +193,9 @@ let start_lean_output (out_name : string) default_sail_dir =
   let main_file = open_out (Filename.concat project_dir (out_name_camel ^ ".lean")) in
   output_string main_file ("import " ^ out_name_camel ^ ".Sail.Sail\n");
   output_string main_file ("import " ^ out_name_camel ^ ".Sail.BitVec\n\n");
+  output_string main_file "set_option maxHeartbeats 1_000_000_000\n";
+  output_string main_file "set_option maxRecDepth 10_000\n";
+  output_string main_file "set_option linter.unusedVariables false\n\n";
   output_string main_file "open Sail\n\n";
   let lakefile = open_out (Filename.concat project_dir "lakefile.toml") in
   { out_name; out_name_camel; sail_dir; main_file; lakefile }

diff --git a/test/lean/SailTinyArm.expected.lean b/test/lean/SailTinyArm.expected.lean
@@ -1,6 +1,10 @@
 import Out.Sail.Sail
 import Out.Sail.BitVec
 
+set_option maxHeartbeats 1_000_000_000
+set_option maxRecDepth 10_000
+set_option linter.unusedVariables false
+
 open Sail
 
 abbrev bits k_n := (BitVec k_n)

diff --git a/test/lean/atom_bool.expected.lean b/test/lean/atom_bool.expected.lean
@@ -1,6 +1,10 @@
 import Out.Sail.Sail
 import Out.Sail.BitVec
 
+set_option maxHeartbeats 1_000_000_000
+set_option maxRecDepth 10_000
+set_option linter.unusedVariables false
+
 open Sail
 
 abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource Unit

diff --git a/test/lean/bitfield.expected.lean b/test/lean/bitfield.expected.lean
@@ -1,6 +1,10 @@
 import Out.Sail.Sail
 import Out.Sail.BitVec
 
+set_option maxHeartbeats 1_000_000_000
+set_option maxRecDepth 10_000
+set_option linter.unusedVariables false
+
 open Sail
 
 abbrev bits k_n := (BitVec k_n)

diff --git a/test/lean/bitvec_operation.expected.lean b/test/lean/bitvec_operation.expected.lean
@@ -1,6 +1,10 @@
 import Out.Sail.Sail
 import Out.Sail.BitVec
 
+set_option maxHeartbeats 1_000_000_000
+set_option maxRecDepth 10_000
+set_option linter.unusedVariables false
+
 open Sail
 
 abbrev bits k_n := (BitVec k_n)

diff --git a/test/lean/enum.expected.lean b/test/lean/enum.expected.lean
@@ -1,6 +1,10 @@
 import Out.Sail.Sail
 import Out.Sail.BitVec
 
+set_option maxHeartbeats 1_000_000_000
+set_option maxRecDepth 10_000
+set_option linter.unusedVariables false
+
 open Sail
 
 abbrev bits k_n := (BitVec k_n)

diff --git a/test/lean/errors.expected.lean b/test/lean/errors.expected.lean
@@ -1,6 +1,10 @@
 import Out.Sail.Sail
 import Out.Sail.BitVec
 
+set_option maxHeartbeats 1_000_000_000
+set_option maxRecDepth 10_000
+set_option linter.unusedVariables false
+
 open Sail
 
 abbrev bits k_n := (BitVec k_n)

diff --git a/test/lean/extern.expected.lean b/test/lean/extern.expected.lean
@@ -1,6 +1,10 @@
 import Out.Sail.Sail
 import Out.Sail.BitVec
 
+set_option maxHeartbeats 1_000_000_000
+set_option maxRecDepth 10_000
+set_option linter.unusedVariables false
+
 open Sail
 
 abbrev bits k_n := (BitVec k_n)

diff --git a/test/lean/extern_bitvec.expected.lean b/test/lean/extern_bitvec.expected.lean
@@ -1,6 +1,10 @@
 import Out.Sail.Sail
 import Out.Sail.BitVec
 
+set_option maxHeartbeats 1_000_000_000
+set_option maxRecDepth 10_000
+set_option linter.unusedVariables false
+
 open Sail
 
 abbrev bits k_n := (BitVec k_n)

diff --git a/test/lean/implicit.expected.lean b/test/lean/implicit.expected.lean
@@ -1,6 +1,10 @@
 import Out.Sail.Sail
 import Out.Sail.BitVec
 
+set_option maxHeartbeats 1_000_000_000
+set_option maxRecDepth 10_000
+set_option linter.unusedVariables false
+
 open Sail
 
 abbrev bits k_n := (BitVec k_n)

diff --git a/test/lean/ite.expected.lean b/test/lean/ite.expected.lean
@@ -1,6 +1,10 @@
 import Out.Sail.Sail
 import Out.Sail.BitVec
 
+set_option maxHeartbeats 1_000_000_000
+set_option maxRecDepth 10_000
+set_option linter.unusedVariables false
+
 open Sail
 
 abbrev bits k_n := (BitVec k_n)

diff --git a/test/lean/let.expected.lean b/test/lean/let.expected.lean
@@ -1,6 +1,10 @@
 import Out.Sail.Sail
 import Out.Sail.BitVec
 
+set_option maxHeartbeats 1_000_000_000
+set_option maxRecDepth 10_000
+set_option linter.unusedVariables false
+
 open Sail
 
 abbrev bits k_n := (BitVec k_n)

diff --git a/test/lean/loop.expected.lean b/test/lean/loop.expected.lean
@@ -1,6 +1,10 @@
 import Out.Sail.Sail
 import Out.Sail.BitVec
 
+set_option maxHeartbeats 1_000_000_000
+set_option maxRecDepth 10_000
+set_option linter.unusedVariables false
+
 open Sail
 
 abbrev bits k_n := (BitVec k_n)

diff --git a/test/lean/mapping.expected.lean b/test/lean/mapping.expected.lean
@@ -1,6 +1,10 @@
 import Out.Sail.Sail
 import Out.Sail.BitVec
 
+set_option maxHeartbeats 1_000_000_000
+set_option maxRecDepth 10_000
+set_option linter.unusedVariables false
+
 open Sail
 
 abbrev bits k_n := (BitVec k_n)

diff --git a/test/lean/match.expected.lean b/test/lean/match.expected.lean
@@ -1,6 +1,10 @@
 import Out.Sail.Sail
 import Out.Sail.BitVec
 
+set_option maxHeartbeats 1_000_000_000
+set_option maxRecDepth 10_000
+set_option linter.unusedVariables false
+
 open Sail
 
 abbrev bits k_n := (BitVec k_n)

diff --git a/test/lean/match_bv.expected.lean b/test/lean/match_bv.expected.lean
@@ -1,6 +1,10 @@
 import Out.Sail.Sail
 import Out.Sail.BitVec
 
+set_option maxHeartbeats 1_000_000_000
+set_option maxRecDepth 10_000
+set_option linter.unusedVariables false
+
 open Sail
 
 abbrev bits k_n := (BitVec k_n)

diff --git a/test/lean/option.expected.lean b/test/lean/option.expected.lean
@@ -1,6 +1,10 @@
 import Out.Sail.Sail
 import Out.Sail.BitVec
 
+set_option maxHeartbeats 1_000_000_000
+set_option maxRecDepth 10_000
+set_option linter.unusedVariables false
+
 open Sail
 
 abbrev bits k_n := (BitVec k_n)

diff --git a/test/lean/range.expected.lean b/test/lean/range.expected.lean
@@ -1,6 +1,10 @@
 import Out.Sail.Sail
 import Out.Sail.BitVec
 
+set_option maxHeartbeats 1_000_000_000
+set_option maxRecDepth 10_000
+set_option linter.unusedVariables false
+
 open Sail
 
 abbrev bits k_n := (BitVec k_n)

diff --git a/test/lean/register_vector.expected.lean b/test/lean/register_vector.expected.lean
@@ -1,6 +1,10 @@
 import Out.Sail.Sail
 import Out.Sail.BitVec
 
+set_option maxHeartbeats 1_000_000_000
+set_option maxRecDepth 10_000
+set_option linter.unusedVariables false
+
 open Sail
 
 abbrev bits k_n := (BitVec k_n)

diff --git a/test/lean/registers.expected.lean b/test/lean/registers.expected.lean
@@ -1,6 +1,10 @@
 import Out.Sail.Sail
 import Out.Sail.BitVec
 
+set_option maxHeartbeats 1_000_000_000
+set_option maxRecDepth 10_000
+set_option linter.unusedVariables false
+
 open Sail
 
 abbrev bits k_n := (BitVec k_n)

diff --git a/test/lean/struct.expected.lean b/test/lean/struct.expected.lean
@@ -1,6 +1,10 @@
 import Out.Sail.Sail
 import Out.Sail.BitVec
 
+set_option maxHeartbeats 1_000_000_000
+set_option maxRecDepth 10_000
+set_option linter.unusedVariables false
+
 open Sail
 
 abbrev bits k_n := (BitVec k_n)

diff --git a/test/lean/struct_of_enum.expected.lean b/test/lean/struct_of_enum.expected.lean
@@ -1,6 +1,10 @@
 import Out.Sail.Sail
 import Out.Sail.BitVec
 
+set_option maxHeartbeats 1_000_000_000
+set_option maxRecDepth 10_000
+set_option linter.unusedVariables false
+
 open Sail
 
 abbrev bits k_n := (BitVec k_n)

diff --git a/test/lean/trivial.expected.lean b/test/lean/trivial.expected.lean
@@ -1,6 +1,10 @@
 import Out.Sail.Sail
 import Out.Sail.BitVec
 
+set_option maxHeartbeats 1_000_000_000
+set_option maxRecDepth 10_000
+set_option linter.unusedVariables false
+
 open Sail
 
 abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource Unit

diff --git a/test/lean/tuples.expected.lean b/test/lean/tuples.expected.lean
@@ -1,6 +1,10 @@
 import Out.Sail.Sail
 import Out.Sail.BitVec
 
+set_option maxHeartbeats 1_000_000_000
+set_option maxRecDepth 10_000
+set_option linter.unusedVariables false
+
 open Sail
 
 abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource Unit

diff --git a/test/lean/type_kid.expected.lean b/test/lean/type_kid.expected.lean
@@ -1,6 +1,10 @@
 import Out.Sail.Sail
 import Out.Sail.BitVec
 
+set_option maxHeartbeats 1_000_000_000
+set_option maxRecDepth 10_000
+set_option linter.unusedVariables false
+
 open Sail
 
 abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource Unit

diff --git a/test/lean/typedef.expected.lean b/test/lean/typedef.expected.lean
@@ -1,6 +1,10 @@
 import Out.Sail.Sail
 import Out.Sail.BitVec
 
+set_option maxHeartbeats 1_000_000_000
+set_option maxRecDepth 10_000
+set_option linter.unusedVariables false
+
 open Sail
 
 abbrev bits k_n := (BitVec k_n)

diff --git a/test/lean/typquant.expected.lean b/test/lean/typquant.expected.lean
@@ -1,6 +1,10 @@
 import Out.Sail.Sail
 import Out.Sail.BitVec
 
+set_option maxHeartbeats 1_000_000_000
+set_option maxRecDepth 10_000
+set_option linter.unusedVariables false
+
 open Sail
 
 abbrev bits k_n := (BitVec k_n)

diff --git a/test/lean/undefined.expected.lean b/test/lean/undefined.expected.lean
@@ -1,6 +1,10 @@
 import Out.Sail.Sail
 import Out.Sail.BitVec
 
+set_option maxHeartbeats 1_000_000_000
+set_option maxRecDepth 10_000
+set_option linter.unusedVariables false
+
 open Sail
 
 abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource Unit

diff --git a/test/lean/union.expected.lean b/test/lean/union.expected.lean
@@ -1,6 +1,10 @@
 import Out.Sail.Sail
 import Out.Sail.BitVec
 
+set_option maxHeartbeats 1_000_000_000
+set_option maxRecDepth 10_000
+set_option linter.unusedVariables false
+
 open Sail