touch for CI

src/Init/Data/List/Lemmas.lean

@@ -15,8 +15,7 @@ import all Init.Data.List.Control
 public import Init.BinderPredicates
 import Init.Grind.Annotated
 
--- TODO: turn this on after an update-stage0
--- grind_annotated "2025-01-24"
+grind_annotated "2025-01-24"
 
 public section
 

tests/lean/run/grind_annotated.lean

@@ -0,0 +1,87 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+import Lean.Elab.Tactic.Grind
+import Lean.LibrarySuggestions.Basic
+
+/-!
+# Tests for grind_annotated command
+
+This file tests that:
+1. The `grind_annotated` command correctly validates date formats
+2. The `filterGrindAnnotated` wrapper correctly filters suggestions based on the caller
+-/
+
+open Lean Meta Elab Tactic LibrarySuggestions
+
+/-! ## Date format validation -/
+
+/--
+error: Invalid date format: offset 0: condition not satisfied
+Expected format: YYYY-MM-DD (e.g., "2025-01-15")
+-/
+#guard_msgs in
+grind_annotated "invalid-date"
+
+/-- info: Extension state contains `Init.Data.List.Lemmas: true -/
+#guard_msgs in
+#eval do
+  let env ← getEnv
+  let state := Lean.Elab.Tactic.Grind.grindAnnotatedExt.getState env
+  logInfo m!"Extension state contains `Init.Data.List.Lemmas: {state.contains `Init.Data.List.Lemmas}"
+
+/-! ## Filtering logic -/
+
+/--
+Create a hardcoded selector that returns a suggestion from `List.eq_nil_of_length_eq_zero`
+in the grind-annotated Init.Data.List.Lemmas module.
+-/
+def testSelector : Selector := fun _ _ => do
+  return #[{
+    name := `List.eq_nil_of_length_eq_zero
+    score := 1.0
+    flag := none
+  }]
+
+/-- info: All tests passed! -/
+#guard_msgs in
+example : True := by
+  run_tac do
+    let mvarId ← getMainGoal
+    let env ← getEnv
+
+    -- Debug: Check if List.eq_nil_of_length_eq_zero exists and get its module
+    let theoremName := `List.eq_nil_of_length_eq_zero
+
+    match env.getModuleIdxFor? theoremName with
+    | none => logInfo "Theorem has no module index"
+    | some modIdx =>
+      let moduleName := env.header.moduleNames[modIdx.toNat]!
+      let isAnnotated := Selector.isGrindAnnotatedModule env modIdx
+      let state := Lean.Elab.Tactic.Grind.grindAnnotatedExt.getState env
+
+    -- Test 1: Without filter, suggestion should be returned
+    let suggestions1 ← testSelector mvarId {}
+    unless suggestions1.size == 1 do
+      throwError "Test 1 failed: Expected 1 suggestion without filter, got {suggestions1.size}"
+
+    -- Test 2: With filterGrindAnnotated and caller := "grind", suggestion should be filtered out
+    let filteredSelector := testSelector.filterGrindAnnotated
+    let suggestions2 ← filteredSelector mvarId { caller := some "grind" }
+    unless suggestions2.size == 0 do
+      throwError "Test 2 failed: Expected 0 suggestions with grind caller, got {suggestions2.size}"
+
+    -- Test 3: With filterGrindAnnotated and caller := "simp", suggestion should be returned
+    let suggestions3 ← filteredSelector mvarId { caller := some "simp" }
+    unless suggestions3.size == 1 do
+      throwError "Test 3 failed: Expected 1 suggestion with simp caller, got {suggestions3.size}"
+
+    -- Test 4: With filterGrindAnnotated and no caller, suggestion should be returned
+    let suggestions4 ← filteredSelector mvarId { caller := none }
+    unless suggestions4.size == 1 do
+      throwError "Test 4 failed: Expected 1 suggestion with no caller, got {suggestions4.size}"
+
+    logInfo "All tests passed!"
+  trivial