mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
93 lines
3.2 KiB
Lean4
93 lines
3.2 KiB
Lean4
/-
|
|
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: Init.Data.List.Lemmas is grind-annotated: true -/
|
|
#guard_msgs in
|
|
#eval do
|
|
let env ← getEnv
|
|
-- Use the public API to check if a module is grind-annotated
|
|
-- First we need to get the module index for a theorem from Init.Data.List.Lemmas
|
|
match env.getModuleIdxFor? `List.eq_nil_of_length_eq_zero with
|
|
| none => logInfo "Could not find module"
|
|
| some modIdx =>
|
|
let isAnnotated := Lean.Elab.Tactic.Grind.isGrindAnnotatedModule env modIdx
|
|
logInfo m!"Init.Data.List.Lemmas is grind-annotated: {isAnnotated}"
|
|
|
|
/-! ## 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 := Grind.isGrindAnnotatedModule env modIdx
|
|
pure ()
|
|
|
|
-- 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
|