diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 61af30e96e..8f8349df89 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -54,4 +54,4 @@ jobs: - name: Don't 'import Lean', use precise imports if: always() run: | - ! (find . -name "*.lean" ! -path "./test/import_lean.lean" -type f -print0 | xargs -0 grep -E -n '^import Lean$') + ! (find . -name "*.lean" ! -path "./BatteriesTest/import_lean.lean" -type f -print0 | xargs -0 grep -E -n '^import Lean$') diff --git a/Batteries.lean b/Batteries.lean index 8f88944fea..7e5c73f5fd 100644 --- a/Batteries.lean +++ b/Batteries.lean @@ -94,9 +94,6 @@ import Batteries.Tactic.SqueezeScope import Batteries.Tactic.Trans import Batteries.Tactic.Unreachable import Batteries.Tactic.Where -import Batteries.Test.Internal.DummyLabelAttr -import Batteries.Test.Internal.DummyLibraryNote -import Batteries.Test.Internal.DummyLibraryNote2 import Batteries.Util.Cache import Batteries.Util.ExtendedBinder import Batteries.Util.LibraryNote diff --git a/Batteries/Test/Internal/DummyLabelAttr.lean b/BatteriesTest/Internal/DummyLabelAttr.lean similarity index 100% rename from Batteries/Test/Internal/DummyLabelAttr.lean rename to BatteriesTest/Internal/DummyLabelAttr.lean diff --git a/Batteries/Test/Internal/DummyLibraryNote.lean b/BatteriesTest/Internal/DummyLibraryNote.lean similarity index 100% rename from Batteries/Test/Internal/DummyLibraryNote.lean rename to BatteriesTest/Internal/DummyLibraryNote.lean diff --git a/Batteries/Test/Internal/DummyLibraryNote2.lean b/BatteriesTest/Internal/DummyLibraryNote2.lean similarity index 88% rename from Batteries/Test/Internal/DummyLibraryNote2.lean rename to BatteriesTest/Internal/DummyLibraryNote2.lean index 3a5bc35dc0..0676060219 100644 --- a/Batteries/Test/Internal/DummyLibraryNote2.lean +++ b/BatteriesTest/Internal/DummyLibraryNote2.lean @@ -1,4 +1,4 @@ -import Batteries.Test.Internal.DummyLibraryNote +import BatteriesTest.Internal.DummyLibraryNote library_note "test" /-- 3: this is a note in a different file importing the above testnotes, diff --git a/test/MLList.lean b/BatteriesTest/MLList.lean similarity index 100% rename from test/MLList.lean rename to BatteriesTest/MLList.lean diff --git a/test/absurd.lean b/BatteriesTest/absurd.lean similarity index 100% rename from test/absurd.lean rename to BatteriesTest/absurd.lean diff --git a/test/alias.lean b/BatteriesTest/alias.lean similarity index 100% rename from test/alias.lean rename to BatteriesTest/alias.lean diff --git a/test/array.lean b/BatteriesTest/array.lean similarity index 100% rename from test/array.lean rename to BatteriesTest/array.lean diff --git a/test/by_contra.lean b/BatteriesTest/by_contra.lean similarity index 100% rename from test/by_contra.lean rename to BatteriesTest/by_contra.lean diff --git a/test/case.lean b/BatteriesTest/case.lean similarity index 100% rename from test/case.lean rename to BatteriesTest/case.lean diff --git a/test/congr.lean b/BatteriesTest/congr.lean similarity index 100% rename from test/congr.lean rename to BatteriesTest/congr.lean diff --git a/test/conv_equals.lean b/BatteriesTest/conv_equals.lean similarity index 100% rename from test/conv_equals.lean rename to BatteriesTest/conv_equals.lean diff --git a/test/exfalso.lean b/BatteriesTest/exfalso.lean similarity index 100% rename from test/exfalso.lean rename to BatteriesTest/exfalso.lean diff --git a/test/float.lean b/BatteriesTest/float.lean similarity index 100% rename from test/float.lean rename to BatteriesTest/float.lean diff --git a/test/help_cmd.lean b/BatteriesTest/help_cmd.lean similarity index 100% rename from test/help_cmd.lean rename to BatteriesTest/help_cmd.lean diff --git a/test/import_lean.lean b/BatteriesTest/import_lean.lean similarity index 100% rename from test/import_lean.lean rename to BatteriesTest/import_lean.lean diff --git a/test/instances.lean b/BatteriesTest/instances.lean similarity index 100% rename from test/instances.lean rename to BatteriesTest/instances.lean diff --git a/test/isIndependentOf.lean b/BatteriesTest/isIndependentOf.lean similarity index 100% rename from test/isIndependentOf.lean rename to BatteriesTest/isIndependentOf.lean diff --git a/test/kmp_matcher.lean b/BatteriesTest/kmp_matcher.lean similarity index 100% rename from test/kmp_matcher.lean rename to BatteriesTest/kmp_matcher.lean diff --git a/test/lemma_cmd.lean b/BatteriesTest/lemma_cmd.lean similarity index 100% rename from test/lemma_cmd.lean rename to BatteriesTest/lemma_cmd.lean diff --git a/test/library_note.lean b/BatteriesTest/library_note.lean similarity index 96% rename from test/library_note.lean rename to BatteriesTest/library_note.lean index f7ac514cdc..7eadf44a44 100644 --- a/test/library_note.lean +++ b/BatteriesTest/library_note.lean @@ -1,5 +1,5 @@ import Batteries.Tactic.HelpCmd -import Batteries.Test.Internal.DummyLibraryNote2 +import BatteriesTest.Internal.DummyLibraryNote2 /-- error: Note not found diff --git a/test/lintTC.lean b/BatteriesTest/lintTC.lean similarity index 100% rename from test/lintTC.lean rename to BatteriesTest/lintTC.lean diff --git a/test/lint_docBlame.lean b/BatteriesTest/lint_docBlame.lean similarity index 100% rename from test/lint_docBlame.lean rename to BatteriesTest/lint_docBlame.lean diff --git a/test/lint_docBlameThm.lean b/BatteriesTest/lint_docBlameThm.lean similarity index 100% rename from test/lint_docBlameThm.lean rename to BatteriesTest/lint_docBlameThm.lean diff --git a/test/lint_dupNamespace.lean b/BatteriesTest/lint_dupNamespace.lean similarity index 100% rename from test/lint_dupNamespace.lean rename to BatteriesTest/lint_dupNamespace.lean diff --git a/test/lint_empty.lean b/BatteriesTest/lint_empty.lean similarity index 100% rename from test/lint_empty.lean rename to BatteriesTest/lint_empty.lean diff --git a/test/lint_lean.lean b/BatteriesTest/lint_lean.lean similarity index 100% rename from test/lint_lean.lean rename to BatteriesTest/lint_lean.lean diff --git a/test/lint_simpNF.lean b/BatteriesTest/lint_simpNF.lean similarity index 100% rename from test/lint_simpNF.lean rename to BatteriesTest/lint_simpNF.lean diff --git a/test/lint_unreachableTactic.lean b/BatteriesTest/lint_unreachableTactic.lean similarity index 100% rename from test/lint_unreachableTactic.lean rename to BatteriesTest/lint_unreachableTactic.lean diff --git a/test/lintsimp.lean b/BatteriesTest/lintsimp.lean similarity index 100% rename from test/lintsimp.lean rename to BatteriesTest/lintsimp.lean diff --git a/test/lintunused.lean b/BatteriesTest/lintunused.lean similarity index 100% rename from test/lintunused.lean rename to BatteriesTest/lintunused.lean diff --git a/test/list_sublists.lean b/BatteriesTest/list_sublists.lean similarity index 100% rename from test/list_sublists.lean rename to BatteriesTest/list_sublists.lean diff --git a/test/nondet.lean b/BatteriesTest/nondet.lean similarity index 100% rename from test/nondet.lean rename to BatteriesTest/nondet.lean diff --git a/test/norm_cast.lean b/BatteriesTest/norm_cast.lean similarity index 100% rename from test/norm_cast.lean rename to BatteriesTest/norm_cast.lean diff --git a/test/omega/benchmark.lean b/BatteriesTest/omega/benchmark.lean similarity index 100% rename from test/omega/benchmark.lean rename to BatteriesTest/omega/benchmark.lean diff --git a/test/on_goal.lean b/BatteriesTest/on_goal.lean similarity index 100% rename from test/on_goal.lean rename to BatteriesTest/on_goal.lean diff --git a/test/print_prefix.lean b/BatteriesTest/print_prefix.lean similarity index 100% rename from test/print_prefix.lean rename to BatteriesTest/print_prefix.lean diff --git a/test/proof_wanted.lean b/BatteriesTest/proof_wanted.lean similarity index 100% rename from test/proof_wanted.lean rename to BatteriesTest/proof_wanted.lean diff --git a/test/register_label_attr.lean b/BatteriesTest/register_label_attr.lean similarity index 92% rename from test/register_label_attr.lean rename to BatteriesTest/register_label_attr.lean index 9add2305c6..d1928052e8 100644 --- a/test/register_label_attr.lean +++ b/BatteriesTest/register_label_attr.lean @@ -1,4 +1,4 @@ -import Batteries.Test.Internal.DummyLabelAttr +import BatteriesTest.Internal.DummyLabelAttr import Lean.LabelAttribute set_option linter.missingDocs false diff --git a/test/rfl.lean b/BatteriesTest/rfl.lean similarity index 100% rename from test/rfl.lean rename to BatteriesTest/rfl.lean diff --git a/test/seq_focus.lean b/BatteriesTest/seq_focus.lean similarity index 100% rename from test/seq_focus.lean rename to BatteriesTest/seq_focus.lean diff --git a/test/show_term.lean b/BatteriesTest/show_term.lean similarity index 100% rename from test/show_term.lean rename to BatteriesTest/show_term.lean diff --git a/test/show_unused.lean b/BatteriesTest/show_unused.lean similarity index 100% rename from test/show_unused.lean rename to BatteriesTest/show_unused.lean diff --git a/test/simp_trace.lean b/BatteriesTest/simp_trace.lean similarity index 100% rename from test/simp_trace.lean rename to BatteriesTest/simp_trace.lean diff --git a/test/simpa.lean b/BatteriesTest/simpa.lean similarity index 100% rename from test/simpa.lean rename to BatteriesTest/simpa.lean diff --git a/test/solve_by_elim.lean b/BatteriesTest/solve_by_elim.lean similarity index 97% rename from test/solve_by_elim.lean rename to BatteriesTest/solve_by_elim.lean index 94baf49ea7..6bfe72bf02 100644 --- a/test/solve_by_elim.lean +++ b/BatteriesTest/solve_by_elim.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Scott Morrison -/ import Batteries.Tactic.PermuteGoals -import Batteries.Test.Internal.DummyLabelAttr +import BatteriesTest.Internal.DummyLabelAttr import Lean.Meta.Tactic.Constructor import Lean.Elab.SyntheticMVars import Lean.Elab.Tactic.SolveByElim -- FIXME we need to make SolveByElimConfig builtin diff --git a/test/trans.lean b/BatteriesTest/trans.lean similarity index 100% rename from test/trans.lean rename to BatteriesTest/trans.lean diff --git a/test/tryThis.lean b/BatteriesTest/tryThis.lean similarity index 100% rename from test/tryThis.lean rename to BatteriesTest/tryThis.lean diff --git a/test/vector.lean b/BatteriesTest/vector.lean similarity index 100% rename from test/vector.lean rename to BatteriesTest/vector.lean diff --git a/test/where.lean b/BatteriesTest/where.lean similarity index 100% rename from test/where.lean rename to BatteriesTest/where.lean diff --git a/lakefile.toml b/lakefile.toml index a8a658ef9f..18abb8a007 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -1,5 +1,5 @@ name = "batteries" -testDriver = "test" +testDriver = "BatteriesTest" lintDriver = "runLinter" defaultTargets = ["Batteries", "runLinter"] @@ -9,6 +9,11 @@ linter.missingDocs = true [[lean_lib]] name = "Batteries" +[[lean_lib]] +name = "BatteriesTest" +globs = ["BatteriesTest.+"] +leanOptions = {linter.missingDocs = false} + [[lean_exe]] name = "runLinter" srcDir = "scripts"