diff options
26 files changed, 77 insertions, 2 deletions
diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean index 9748919e..bb97d5c4 100644 --- a/tests/lean/Arrays.lean +++ b/tests/lean/Arrays.lean @@ -2,6 +2,9 @@ -- [arrays] import Base open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false namespace arrays diff --git a/tests/lean/Betree/Funs.lean b/tests/lean/Betree/Funs.lean index 05341b31..4592e91c 100644 --- a/tests/lean/Betree/Funs.lean +++ b/tests/lean/Betree/Funs.lean @@ -4,6 +4,9 @@ import Base import Betree.Types import Betree.FunsExternal open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false namespace betree diff --git a/tests/lean/Betree/FunsExternal_Template.lean b/tests/lean/Betree/FunsExternal_Template.lean index 014f0d83..2fb40ebc 100644 --- a/tests/lean/Betree/FunsExternal_Template.lean +++ b/tests/lean/Betree/FunsExternal_Template.lean @@ -4,6 +4,9 @@ import Base import Betree.Types open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false open betree /- [betree::betree_utils::load_internal_node]: diff --git a/tests/lean/Betree/Types.lean b/tests/lean/Betree/Types.lean index 3b46c00c..9e7c505b 100644 --- a/tests/lean/Betree/Types.lean +++ b/tests/lean/Betree/Types.lean @@ -3,6 +3,9 @@ import Base import Betree.TypesExternal open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false namespace betree diff --git a/tests/lean/Betree/TypesExternal_Template.lean b/tests/lean/Betree/TypesExternal_Template.lean index 12fce657..f97517a6 100644 --- a/tests/lean/Betree/TypesExternal_Template.lean +++ b/tests/lean/Betree/TypesExternal_Template.lean @@ -3,6 +3,9 @@ -- This is a template file: rename it to "TypesExternal.lean" and fill the holes. import Base open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false /- The state type used in the state-error monad -/ axiom State : Type diff --git a/tests/lean/Bitwise.lean b/tests/lean/Bitwise.lean index 23ec66b4..7f347661 100644 --- a/tests/lean/Bitwise.lean +++ b/tests/lean/Bitwise.lean @@ -2,6 +2,9 @@ -- [bitwise] import Base open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false namespace bitwise diff --git a/tests/lean/Constants.lean b/tests/lean/Constants.lean index ecb91c16..fff74646 100644 --- a/tests/lean/Constants.lean +++ b/tests/lean/Constants.lean @@ -2,6 +2,9 @@ -- [constants] import Base open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false namespace constants diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean index 2bbc385d..a557cf73 100644 --- a/tests/lean/Demo/Demo.lean +++ b/tests/lean/Demo/Demo.lean @@ -2,6 +2,9 @@ -- [demo] import Base open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false namespace demo diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean index 1b1d5cdf..cd1883e5 100644 --- a/tests/lean/External/Funs.lean +++ b/tests/lean/External/Funs.lean @@ -4,6 +4,9 @@ import Base import External.Types import External.FunsExternal open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false namespace external diff --git a/tests/lean/External/FunsExternal_Template.lean b/tests/lean/External/FunsExternal_Template.lean index 870a79c0..51050b21 100644 --- a/tests/lean/External/FunsExternal_Template.lean +++ b/tests/lean/External/FunsExternal_Template.lean @@ -4,6 +4,9 @@ import Base import External.Types open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false open external /- [core::cell::{core::cell::Cell<T>#10}::get]: diff --git a/tests/lean/External/Types.lean b/tests/lean/External/Types.lean index 836ddff0..50446e1c 100644 --- a/tests/lean/External/Types.lean +++ b/tests/lean/External/Types.lean @@ -3,6 +3,9 @@ import Base import External.TypesExternal open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false namespace external diff --git a/tests/lean/External/TypesExternal_Template.lean b/tests/lean/External/TypesExternal_Template.lean index 24687d83..2cfbcc80 100644 --- a/tests/lean/External/TypesExternal_Template.lean +++ b/tests/lean/External/TypesExternal_Template.lean @@ -3,6 +3,9 @@ -- This is a template file: rename it to "TypesExternal.lean" and fill the holes. import Base open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false /- [core::cell::Cell] Source: '/rustc/65ea825f4021eaf77f1b25139969712d65b435a4/library/core/src/cell.rs', lines 294:0-294:26 diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean index f5d028db..7972b715 100644 --- a/tests/lean/Hashmap/Funs.lean +++ b/tests/lean/Hashmap/Funs.lean @@ -4,6 +4,9 @@ import Base import Hashmap.Types import Hashmap.FunsExternal open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false namespace hashmap diff --git a/tests/lean/Hashmap/FunsExternal_Template.lean b/tests/lean/Hashmap/FunsExternal_Template.lean index 80362a92..ea5ceed3 100644 --- a/tests/lean/Hashmap/FunsExternal_Template.lean +++ b/tests/lean/Hashmap/FunsExternal_Template.lean @@ -4,6 +4,9 @@ import Base import Hashmap.Types open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false open hashmap /- [hashmap::utils::deserialize]: diff --git a/tests/lean/Hashmap/Types.lean b/tests/lean/Hashmap/Types.lean index 93af883e..6f5d99a5 100644 --- a/tests/lean/Hashmap/Types.lean +++ b/tests/lean/Hashmap/Types.lean @@ -3,6 +3,9 @@ import Base import Hashmap.TypesExternal open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false namespace hashmap diff --git a/tests/lean/Hashmap/TypesExternal_Template.lean b/tests/lean/Hashmap/TypesExternal_Template.lean index 03c3d157..b6f24513 100644 --- a/tests/lean/Hashmap/TypesExternal_Template.lean +++ b/tests/lean/Hashmap/TypesExternal_Template.lean @@ -3,6 +3,9 @@ -- This is a template file: rename it to "TypesExternal.lean" and fill the holes. import Base open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false /- The state type used in the state-error monad -/ axiom State : Type diff --git a/tests/lean/InfiniteLoop.lean b/tests/lean/InfiniteLoop.lean index b8c2343e..b5986ed8 100644 --- a/tests/lean/InfiniteLoop.lean +++ b/tests/lean/InfiniteLoop.lean @@ -2,6 +2,9 @@ -- [infinite_loop] import Base open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false namespace infinite_loop diff --git a/tests/lean/Issue194RecursiveStructProjector.lean b/tests/lean/Issue194RecursiveStructProjector.lean index 4eb23934..730d1aa6 100644 --- a/tests/lean/Issue194RecursiveStructProjector.lean +++ b/tests/lean/Issue194RecursiveStructProjector.lean @@ -2,6 +2,9 @@ -- [issue_194_recursive_struct_projector] import Base open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false namespace issue_194_recursive_struct_projector diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean index a9e5a499..e676336e 100644 --- a/tests/lean/Loops.lean +++ b/tests/lean/Loops.lean @@ -2,6 +2,9 @@ -- [loops] import Base open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false namespace loops diff --git a/tests/lean/Matches.lean b/tests/lean/Matches.lean index 9233841b..8d592a85 100644 --- a/tests/lean/Matches.lean +++ b/tests/lean/Matches.lean @@ -2,6 +2,9 @@ -- [matches] import Base open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false namespace matches diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean index f0438050..090ca2b2 100644 --- a/tests/lean/NoNestedBorrows.lean +++ b/tests/lean/NoNestedBorrows.lean @@ -2,6 +2,9 @@ -- [no_nested_borrows] import Base open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false namespace no_nested_borrows diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean index 03b96903..b1aef703 100644 --- a/tests/lean/Paper.lean +++ b/tests/lean/Paper.lean @@ -2,6 +2,9 @@ -- [paper] import Base open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false namespace paper diff --git a/tests/lean/PoloniusList.lean b/tests/lean/PoloniusList.lean index ed279d58..489871ba 100644 --- a/tests/lean/PoloniusList.lean +++ b/tests/lean/PoloniusList.lean @@ -2,6 +2,9 @@ -- [polonius_list] import Base open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false namespace polonius_list diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean index 0dd692fe..51aba5bf 100644 --- a/tests/lean/Traits.lean +++ b/tests/lean/Traits.lean @@ -2,6 +2,9 @@ -- [traits] import Base open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false namespace traits diff --git a/tests/lean/misc/MutuallyRecursiveTraits.lean b/tests/lean/misc/MutuallyRecursiveTraits.lean index b0fcb9e9..05871009 100644 --- a/tests/lean/misc/MutuallyRecursiveTraits.lean +++ b/tests/lean/misc/MutuallyRecursiveTraits.lean @@ -2,5 +2,8 @@ -- [mutually_recursive_traits] import Base open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false namespace mutually_recursive_traits diff --git a/tests/src/mutually-recursive-traits.lean.out b/tests/src/mutually-recursive-traits.lean.out index e2ed3abc..9b3b0737 100644 --- a/tests/src/mutually-recursive-traits.lean.out +++ b/tests/src/mutually-recursive-traits.lean.out @@ -12,6 +12,6 @@ Uncaught exception: Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 46, characters 4-76 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 836, characters 2-52 -Called from Aeneas__Translate.extract_file in file "Translate.ml", line 954, characters 2-36 -Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1503, characters 5-42 +Called from Aeneas__Translate.extract_file in file "Translate.ml", line 963, characters 2-36 +Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1512, characters 5-42 Called from Dune__exe__Main in file "Main.ml", line 314, characters 14-66 |