Merge branch 'main' into cleanup-vector-basic

leanprover-community · Nov 5, 2024 · 621656e · 621656e
2 parents 27db89a + af73110
commit 621656e
Show file tree

Hide file tree

Showing 52 changed files with 11 additions and 9 deletions.
diff --git 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
@@ -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 → BatteriesTest/Internal/DummyLabelAttr.lean b/Batteries/Test/Internal/DummyLabelAttr.lean → BatteriesTest/Internal/DummyLabelAttr.lean
diff --git a/...eries/Test/Internal/DummyLibraryNote.lean → BatteriesTest/Internal/DummyLibraryNote.lean b/...eries/Test/Internal/DummyLibraryNote.lean → BatteriesTest/Internal/DummyLibraryNote.lean
diff --git a/...ries/Test/Internal/DummyLibraryNote2.lean → ...eriesTest/Internal/DummyLibraryNote2.lean b/...ries/Test/Internal/DummyLibraryNote2.lean → ...eriesTest/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 → BatteriesTest/MLList.lean b/test/MLList.lean → BatteriesTest/MLList.lean
diff --git a/test/absurd.lean → BatteriesTest/absurd.lean b/test/absurd.lean → BatteriesTest/absurd.lean
diff --git a/test/alias.lean → BatteriesTest/alias.lean b/test/alias.lean → BatteriesTest/alias.lean
diff --git a/test/array.lean → BatteriesTest/array.lean b/test/array.lean → BatteriesTest/array.lean
diff --git a/test/by_contra.lean → BatteriesTest/by_contra.lean b/test/by_contra.lean → BatteriesTest/by_contra.lean
diff --git a/test/case.lean → BatteriesTest/case.lean b/test/case.lean → BatteriesTest/case.lean
diff --git a/test/congr.lean → BatteriesTest/congr.lean b/test/congr.lean → BatteriesTest/congr.lean
diff --git a/test/conv_equals.lean → BatteriesTest/conv_equals.lean b/test/conv_equals.lean → BatteriesTest/conv_equals.lean
diff --git a/test/exfalso.lean → BatteriesTest/exfalso.lean b/test/exfalso.lean → BatteriesTest/exfalso.lean
diff --git a/test/float.lean → BatteriesTest/float.lean b/test/float.lean → BatteriesTest/float.lean
diff --git a/test/help_cmd.lean → BatteriesTest/help_cmd.lean b/test/help_cmd.lean → BatteriesTest/help_cmd.lean
diff --git a/test/import_lean.lean → BatteriesTest/import_lean.lean b/test/import_lean.lean → BatteriesTest/import_lean.lean
diff --git a/test/instances.lean → BatteriesTest/instances.lean b/test/instances.lean → BatteriesTest/instances.lean
diff --git a/test/isIndependentOf.lean → BatteriesTest/isIndependentOf.lean b/test/isIndependentOf.lean → BatteriesTest/isIndependentOf.lean
diff --git a/test/kmp_matcher.lean → BatteriesTest/kmp_matcher.lean b/test/kmp_matcher.lean → BatteriesTest/kmp_matcher.lean
diff --git a/test/lemma_cmd.lean → BatteriesTest/lemma_cmd.lean b/test/lemma_cmd.lean → BatteriesTest/lemma_cmd.lean
diff --git a/test/library_note.lean → BatteriesTest/library_note.lean b/test/library_note.lean → 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 → BatteriesTest/lintTC.lean b/test/lintTC.lean → BatteriesTest/lintTC.lean
diff --git a/test/lint_docBlame.lean → BatteriesTest/lint_docBlame.lean b/test/lint_docBlame.lean → BatteriesTest/lint_docBlame.lean
diff --git a/test/lint_docBlameThm.lean → BatteriesTest/lint_docBlameThm.lean b/test/lint_docBlameThm.lean → BatteriesTest/lint_docBlameThm.lean
diff --git a/test/lint_dupNamespace.lean → BatteriesTest/lint_dupNamespace.lean b/test/lint_dupNamespace.lean → BatteriesTest/lint_dupNamespace.lean
diff --git a/test/lint_empty.lean → BatteriesTest/lint_empty.lean b/test/lint_empty.lean → BatteriesTest/lint_empty.lean
diff --git a/test/lint_lean.lean → BatteriesTest/lint_lean.lean b/test/lint_lean.lean → BatteriesTest/lint_lean.lean
diff --git a/test/lint_simpNF.lean → BatteriesTest/lint_simpNF.lean b/test/lint_simpNF.lean → BatteriesTest/lint_simpNF.lean
diff --git a/test/lint_unreachableTactic.lean → BatteriesTest/lint_unreachableTactic.lean b/test/lint_unreachableTactic.lean → BatteriesTest/lint_unreachableTactic.lean
diff --git a/test/lintsimp.lean → BatteriesTest/lintsimp.lean b/test/lintsimp.lean → BatteriesTest/lintsimp.lean
diff --git a/test/lintunused.lean → BatteriesTest/lintunused.lean b/test/lintunused.lean → BatteriesTest/lintunused.lean
diff --git a/test/list_sublists.lean → BatteriesTest/list_sublists.lean b/test/list_sublists.lean → BatteriesTest/list_sublists.lean
diff --git a/test/nondet.lean → BatteriesTest/nondet.lean b/test/nondet.lean → BatteriesTest/nondet.lean
diff --git a/test/norm_cast.lean → BatteriesTest/norm_cast.lean b/test/norm_cast.lean → BatteriesTest/norm_cast.lean
diff --git a/test/omega/benchmark.lean → BatteriesTest/omega/benchmark.lean b/test/omega/benchmark.lean → BatteriesTest/omega/benchmark.lean
diff --git a/test/on_goal.lean → BatteriesTest/on_goal.lean b/test/on_goal.lean → BatteriesTest/on_goal.lean
diff --git a/test/print_prefix.lean → BatteriesTest/print_prefix.lean b/test/print_prefix.lean → BatteriesTest/print_prefix.lean
diff --git a/test/proof_wanted.lean → BatteriesTest/proof_wanted.lean b/test/proof_wanted.lean → BatteriesTest/proof_wanted.lean
diff --git a/test/register_label_attr.lean → BatteriesTest/register_label_attr.lean b/test/register_label_attr.lean → 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 → BatteriesTest/rfl.lean b/test/rfl.lean → BatteriesTest/rfl.lean
diff --git a/test/seq_focus.lean → BatteriesTest/seq_focus.lean b/test/seq_focus.lean → BatteriesTest/seq_focus.lean
diff --git a/test/show_term.lean → BatteriesTest/show_term.lean b/test/show_term.lean → BatteriesTest/show_term.lean
diff --git a/test/show_unused.lean → BatteriesTest/show_unused.lean b/test/show_unused.lean → BatteriesTest/show_unused.lean
diff --git a/test/simp_trace.lean → BatteriesTest/simp_trace.lean b/test/simp_trace.lean → BatteriesTest/simp_trace.lean
diff --git a/test/simpa.lean → BatteriesTest/simpa.lean b/test/simpa.lean → BatteriesTest/simpa.lean
diff --git a/test/solve_by_elim.lean → BatteriesTest/solve_by_elim.lean b/test/solve_by_elim.lean → 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 → BatteriesTest/trans.lean b/test/trans.lean → BatteriesTest/trans.lean
diff --git a/test/tryThis.lean → BatteriesTest/tryThis.lean b/test/tryThis.lean → BatteriesTest/tryThis.lean
diff --git a/test/vector.lean → BatteriesTest/vector.lean b/test/vector.lean → BatteriesTest/vector.lean
diff --git a/test/where.lean → BatteriesTest/where.lean b/test/where.lean → BatteriesTest/where.lean
diff --git 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"