From d145b9f8ee211d5f369c49065d7abd4bc6c9def8 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Thu, 11 Dec 2025 04:28:44 -0500 Subject: [PATCH] chore: lake: mv `targets` test to `tests` (#11592) This PR moves Lake's `tests/lake/examples/targets` test from `examples` to `tests` (and thus disabling it by default). It is being [flaky](https://github.com/leanprover/lean4/actions/runs/20111185289/attempts/1) for some unknown reason, so I am disabling until I have a better opportunity to debug it. --- tests/lake/{examples => tests}/targets/clean.sh | 0 tests/lake/{examples => tests}/targets/lakefile.lean | 0 tests/lake/{examples => tests}/targets/src/Bar.lean | 0 tests/lake/{examples => tests}/targets/src/Baz.lean | 0 tests/lake/{examples => tests}/targets/src/Foo.lean | 0 tests/lake/{examples => tests}/targets/src/Foo/Bar.lean | 0 tests/lake/{examples => tests}/targets/src/Foo/Baz.lean | 0 tests/lake/{examples => tests}/targets/src/a.lean | 0 tests/lake/{examples => tests}/targets/src/b.lean | 0 tests/lake/{examples => tests}/targets/src/c.lean | 0 tests/lake/{examples => tests}/targets/test.sh | 0 11 files changed, 0 insertions(+), 0 deletions(-) rename tests/lake/{examples => tests}/targets/clean.sh (100%) rename tests/lake/{examples => tests}/targets/lakefile.lean (100%) rename tests/lake/{examples => tests}/targets/src/Bar.lean (100%) rename tests/lake/{examples => tests}/targets/src/Baz.lean (100%) rename tests/lake/{examples => tests}/targets/src/Foo.lean (100%) rename tests/lake/{examples => tests}/targets/src/Foo/Bar.lean (100%) rename tests/lake/{examples => tests}/targets/src/Foo/Baz.lean (100%) rename tests/lake/{examples => tests}/targets/src/a.lean (100%) rename tests/lake/{examples => tests}/targets/src/b.lean (100%) rename tests/lake/{examples => tests}/targets/src/c.lean (100%) rename tests/lake/{examples => tests}/targets/test.sh (100%) diff --git a/tests/lake/examples/targets/clean.sh b/tests/lake/tests/targets/clean.sh similarity index 100% rename from tests/lake/examples/targets/clean.sh rename to tests/lake/tests/targets/clean.sh diff --git a/tests/lake/examples/targets/lakefile.lean b/tests/lake/tests/targets/lakefile.lean similarity index 100% rename from tests/lake/examples/targets/lakefile.lean rename to tests/lake/tests/targets/lakefile.lean diff --git a/tests/lake/examples/targets/src/Bar.lean b/tests/lake/tests/targets/src/Bar.lean similarity index 100% rename from tests/lake/examples/targets/src/Bar.lean rename to tests/lake/tests/targets/src/Bar.lean diff --git a/tests/lake/examples/targets/src/Baz.lean b/tests/lake/tests/targets/src/Baz.lean similarity index 100% rename from tests/lake/examples/targets/src/Baz.lean rename to tests/lake/tests/targets/src/Baz.lean diff --git a/tests/lake/examples/targets/src/Foo.lean b/tests/lake/tests/targets/src/Foo.lean similarity index 100% rename from tests/lake/examples/targets/src/Foo.lean rename to tests/lake/tests/targets/src/Foo.lean diff --git a/tests/lake/examples/targets/src/Foo/Bar.lean b/tests/lake/tests/targets/src/Foo/Bar.lean similarity index 100% rename from tests/lake/examples/targets/src/Foo/Bar.lean rename to tests/lake/tests/targets/src/Foo/Bar.lean diff --git a/tests/lake/examples/targets/src/Foo/Baz.lean b/tests/lake/tests/targets/src/Foo/Baz.lean similarity index 100% rename from tests/lake/examples/targets/src/Foo/Baz.lean rename to tests/lake/tests/targets/src/Foo/Baz.lean diff --git a/tests/lake/examples/targets/src/a.lean b/tests/lake/tests/targets/src/a.lean similarity index 100% rename from tests/lake/examples/targets/src/a.lean rename to tests/lake/tests/targets/src/a.lean diff --git a/tests/lake/examples/targets/src/b.lean b/tests/lake/tests/targets/src/b.lean similarity index 100% rename from tests/lake/examples/targets/src/b.lean rename to tests/lake/tests/targets/src/b.lean diff --git a/tests/lake/examples/targets/src/c.lean b/tests/lake/tests/targets/src/c.lean similarity index 100% rename from tests/lake/examples/targets/src/c.lean rename to tests/lake/tests/targets/src/c.lean diff --git a/tests/lake/examples/targets/test.sh b/tests/lake/tests/targets/test.sh similarity index 100% rename from tests/lake/examples/targets/test.sh rename to tests/lake/tests/targets/test.sh