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.
125 lines
3.8 KiB
Text
125 lines
3.8 KiB
Text
/-
|
|
Test that try? supports user-defined suggestion generators via @[try_suggestion]
|
|
-/
|
|
module
|
|
public import Lean
|
|
public meta import Lean.Elab.Tactic.Try
|
|
|
|
open Lean Meta Elab Tactic Try
|
|
|
|
-- Define an opaque predicate that built-in tactics (including solve_by_elim) won't solve.
|
|
-- The axiom name starts with `_` so that `exact?` treats it as an implementation detail and
|
|
-- won't suggest it directly, allowing us to test user-defined suggestion generators.
|
|
opaque CustomProp : Prop
|
|
axiom _customPropHolds : CustomProp
|
|
|
|
section BasicTest
|
|
-- Define a generator that suggests the custom lemma
|
|
@[local try_suggestion]
|
|
meta def customPropSolver (_goal : MVarId) (_info : Try.Info) : MetaM (Array (TSyntax `tactic)) := do
|
|
return #[← `(tactic| exact _customPropHolds)]
|
|
|
|
-- Test that try? picks up the user-defined suggestion
|
|
-- Built-in tactics won't solve this, so only user suggestion appears
|
|
/--
|
|
info: Try this:
|
|
[apply] exact _customPropHolds✝
|
|
-/
|
|
#guard_msgs in
|
|
example : CustomProp := by
|
|
try?
|
|
end BasicTest
|
|
|
|
section PriorityTest
|
|
-- Test priority ordering with multiple generators
|
|
@[local try_suggestion 2000]
|
|
meta def highPrioritySolver (_goal : MVarId) (_info : Try.Info) : MetaM (Array (TSyntax `tactic)) := do
|
|
return #[← `(tactic| apply _customPropHolds)]
|
|
|
|
@[local try_suggestion 1000]
|
|
meta def midPrioritySolver (_goal : MVarId) (_info : Try.Info) : MetaM (Array (TSyntax `tactic)) := do
|
|
return #[← `(tactic| exact _customPropHolds)]
|
|
|
|
@[local try_suggestion 500]
|
|
meta def lowPrioritySolver (_goal : MVarId) (_info : Try.Info) : MetaM (Array (TSyntax `tactic)) := do
|
|
return #[← `(tactic| constructor)]
|
|
|
|
-- All generators return successful tactics, ordered by priority (highest first)
|
|
-- Note: constructor doesn't work on opaque types, so lowPrioritySolver's suggestion is filtered out
|
|
/--
|
|
info: Try these:
|
|
[apply] apply _customPropHolds✝
|
|
[apply] exact _customPropHolds✝
|
|
-/
|
|
#guard_msgs in
|
|
example : CustomProp := by
|
|
try?
|
|
end PriorityTest
|
|
|
|
section BuiltInFallback
|
|
-- Test that user generators only run if built-ins fail
|
|
-- For True, built-ins succeed so user generators shouldn't run
|
|
@[local try_suggestion]
|
|
meta def shouldNotRunForTrue (_goal : MVarId) (_info : Try.Info) : MetaM (Array (TSyntax `tactic)) := do
|
|
return #[← `(tactic| exact True.intro)]
|
|
|
|
-- Built-ins succeed, so user suggestion doesn't appear
|
|
/--
|
|
info: Try these:
|
|
[apply] solve_by_elim
|
|
[apply] simp
|
|
[apply] simp only
|
|
[apply] grind
|
|
[apply] grind only
|
|
[apply] simp_all
|
|
-/
|
|
#guard_msgs in
|
|
example : True := by
|
|
try?
|
|
end BuiltInFallback
|
|
|
|
section DoubleSuggestion
|
|
-- Test double-suggestion: when a user tactic produces "Try this" messages,
|
|
-- both the original tactic and the suggestions should appear
|
|
-- Use CustomProp which built-ins can't solve
|
|
@[local try_suggestion]
|
|
meta def doubleSuggestionSolver (_goal : MVarId) (_info : Try.Info) : MetaM (Array (TSyntax `tactic)) := do
|
|
return #[← `(tactic| show_term apply _customPropHolds)]
|
|
|
|
-- Double-suggestion: when show_term produces a "Try this" message,
|
|
-- both the original tactic and the extracted suggestion should appear
|
|
-- The message from show_term during extraction is suppressed
|
|
/--
|
|
info: Try these:
|
|
[apply] show_term apply _customPropHolds✝
|
|
[apply] exact _customPropHolds
|
|
-/
|
|
#guard_msgs in
|
|
example : CustomProp := by
|
|
try?
|
|
end DoubleSuggestion
|
|
|
|
section RegisterCommand
|
|
-- Test the register_try?_tactic convenience command
|
|
register_try?_tactic (priority := 500) exact _customPropHolds
|
|
|
|
/--
|
|
info: Try this:
|
|
[apply] exact _customPropHolds
|
|
-/
|
|
#guard_msgs in
|
|
example : CustomProp := by
|
|
try?
|
|
|
|
-- Test without explicit priority (should default to 1000, so appear before exact at 500)
|
|
register_try?_tactic apply _customPropHolds
|
|
|
|
/--
|
|
info: Try these:
|
|
[apply] apply _customPropHolds
|
|
[apply] exact _customPropHolds
|
|
-/
|
|
#guard_msgs in
|
|
example : CustomProp := by
|
|
try?
|
|
end RegisterCommand
|