From 15ac3a9ffd1ca5564006d722b0b2cf5906dc8ba6 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Thu, 7 Nov 2024 16:10:07 +1100
Subject: [PATCH] move test file, add module doc

---
 tests/lean/000_simplc.lean | 24 ++++++++++++++++++++++++
 tests/lean/run/simplc.lean |  6 ------
 2 files changed, 24 insertions(+), 6 deletions(-)
 create mode 100644 tests/lean/000_simplc.lean
 delete mode 100644 tests/lean/run/simplc.lean

diff --git a/tests/lean/000_simplc.lean b/tests/lean/000_simplc.lean
new file mode 100644
index 000000000000..b01891eaff37
--- /dev/null
+++ b/tests/lean/000_simplc.lean
@@ -0,0 +1,24 @@
+import Lean.SimpLC.Whitelists
+
+/-!
+# simp local confluence testing
+
+If you experience failures here, take the suggested `simp_lc inspect ...` commands
+and paste them into a relevant `Lean.SimpLC.Whitelists.ABC` file.
+
+Then decide whether to:
+* Remove a `@[simp]` annotation
+* Add a new `@[simp]` lemma to restore confluence
+* Add a new `simp_lc whitelist` directive to suppress warnings about a given non-confluent pair.
+  Ideally add an `example` immediately before it demonstrating the non-confluence.
+* Add a new `simp_lc ignore` directive to suppress all warnings about a given lemma.
+  Ideally add a doc-comment justifying why this is reasonable.
+
+
+This file is intentionally named `000_simplc.lean` to starting running as early as possible in CI.
+-/
+
+-- Warning: this takes about 3 minutes to run!
+set_option maxHeartbeats 0 in
+#guard_msgs (drop info) in
+simp_lc check
diff --git a/tests/lean/run/simplc.lean b/tests/lean/run/simplc.lean
deleted file mode 100644
index e03a1a76a8fe..000000000000
--- a/tests/lean/run/simplc.lean
+++ /dev/null
@@ -1,6 +0,0 @@
-import Lean.SimpLC.Whitelists
-
--- Warning: this takes about 15 minutes to run!
-set_option maxHeartbeats 0 in
-#guard_msgs (drop info) in
-simp_lc check