Skip to content

Commit 30d88c8

Browse files
kim-emkim-em
committed
chore: restore set_library_suggestions tests after update-stage0
1 parent 3e37060 commit 30d88c8

File tree

2 files changed

+68
-70
lines changed

2 files changed

+68
-70
lines changed

‎tests/lean/run/library_suggestions_persistent.lean‎

Lines changed: 37 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -1,45 +1,44 @@
1-
-- This will be restored after an update-stage0
2-
-- import Lean.LibrarySuggestions
3-
-- import Lean.Meta.Basic
1+
import Lean.LibrarySuggestions
2+
import Lean.Meta.Basic
43

5-
-- /-!
6-
-- # Test that library suggestions persist across file boundaries
4+
/-!
5+
# Test that library suggestions persist across file boundaries
76
8-
-- This test verifies that the default library suggestion engine set in
9-
-- `Lean.LibrarySuggestions.Default` is correctly persisted when imported via `Lean.LibrarySuggestions`.
7+
This test verifies that the default library suggestion engine set in
8+
`Lean.LibrarySuggestions.Default` is correctly persisted when imported via `Lean.LibrarySuggestions`.
109
11-
-- We do NOT call `set_library_suggestions` in this file - the selector should
12-
-- already be set from importing Lean.LibrarySuggestions (which imports Default).
13-
-- -/
10+
We do NOT call `set_library_suggestions` in this file - the selector should
11+
already be set from importing Lean.LibrarySuggestions (which imports Default).
12+
-/
1413

15-
-- /--
16-
-- info: ✓ Selector registered in imported state
17-
-- ---
18-
-- info: ✓ getSelector succeeded
19-
-- -/
20-
-- #guard_msgs in
21-
-- open Lean Lean.LibrarySuggestions in
22-
-- run_cmd do
23-
-- -- Check if a selector is registered
24-
-- let hasSelector := (librarySuggestionsExt.getState (← getEnv)).isSome
25-
-- if hasSelector then
26-
-- Lean.logInfo "✓ Selector registered in imported state"
27-
-- -- Try to retrieve the selector using getSelector
28-
-- Elab.Command.liftTermElabM do
29-
-- let selector? ← getSelector
30-
-- match selector? with
31-
-- | none => Lean.logInfo " ❌ getSelector returned none"
32-
-- | some _ => Lean.logInfo " ✓ getSelector succeeded"
33-
-- else
34-
-- Lean.logInfo "❌ No selector registered in imported state!"
14+
/--
15+
info: ✓ Selector registered in imported state
16+
---
17+
info: ✓ getSelector succeeded
18+
-/
19+
#guard_msgs in
20+
open Lean Lean.LibrarySuggestions in
21+
run_cmd do
22+
-- Check if a selector is registered
23+
let hasSelector := (librarySuggestionsExt.getState (← getEnv)).isSome
24+
if hasSelector then
25+
Lean.logInfo "✓ Selector registered in imported state"
26+
-- Try to retrieve the selector using getSelector
27+
Elab.Command.liftTermElabM do
28+
let selector? ← getSelector
29+
match selector? with
30+
| none => Lean.logInfo " ❌ getSelector returned none"
31+
| some _ => Lean.logInfo " ✓ getSelector succeeded"
32+
else
33+
Lean.logInfo "❌ No selector registered in imported state!"
3534

36-
-- -- These examples should work with grind +suggestions but not grind alone
37-
-- -- (proving that the suggestions engine is active and helping)
35+
-- These examples should work with grind +suggestions but not grind alone
36+
-- (proving that the suggestions engine is active and helping)
3837

39-
-- example {x : Dyadic} {prec : Int} : x.roundDown prec ≤ x := by
40-
-- fail_if_success grind
41-
-- grind +suggestions
38+
example {x : Dyadic} {prec : Int} : x.roundDown prec ≤ x := by
39+
fail_if_success grind
40+
grind +suggestions
4241

43-
-- example {x : Dyadic} {prec : Int} : (x.roundUp prec).precision ≤ some prec := by
44-
-- fail_if_success grind
45-
-- grind +suggestions
42+
example {x : Dyadic} {prec : Int} : (x.roundUp prec).precision ≤ some prec := by
43+
fail_if_success grind
44+
grind +suggestions

‎tests/lean/run/library_suggestions_persistent_module.lean‎

Lines changed: 31 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -1,36 +1,35 @@
1-
-- This will be restored after an update-stage0
2-
-- -- It's critical that this test remains a `module`:
3-
-- -- its purpose is to test the availability of the selector in modules.
4-
-- module
5-
-- import Lean
1+
-- It's critical that this test remains a `module`:
2+
-- its purpose is to test the availability of the selector in modules.
3+
module
4+
import Lean
65

7-
-- /-!
8-
-- # Test that library suggestions persist across file boundaries
6+
/-!
7+
# Test that library suggestions persist across file boundaries
98
10-
-- This test verifies that the default library suggestion engine set in
11-
-- `Lean.LibrarySuggestions.Default` is correctly persisted when imported via `Lean.LibrarySuggestions`.
9+
This test verifies that the default library suggestion engine set in
10+
`Lean.LibrarySuggestions.Default` is correctly persisted when imported via `Lean.LibrarySuggestions`.
1211
13-
-- We do NOT call `set_library_suggestions` in this file - the selector should
14-
-- already be set from importing Lean.LibrarySuggestions (which imports Default).
15-
-- -/
12+
We do NOT call `set_library_suggestions` in this file - the selector should
13+
already be set from importing Lean.LibrarySuggestions (which imports Default).
14+
-/
1615

17-
-- /--
18-
-- info: ✓ Selector registered in imported state
19-
-- ---
20-
-- info: ✓ getSelector succeeded
21-
-- -/
22-
-- #guard_msgs in
23-
-- open Lean Lean.LibrarySuggestions in
24-
-- run_cmd do
25-
-- -- Check if a selector is registered
26-
-- let hasSelector := (librarySuggestionsExt.getState (← getEnv)).isSome
27-
-- if hasSelector then
28-
-- Lean.logInfo "✓ Selector registered in imported state"
29-
-- -- Try to retrieve the selector using getSelector
30-
-- Elab.Command.liftTermElabM do
31-
-- let selector? ← getSelector
32-
-- match selector? with
33-
-- | none => Lean.logInfo " ❌ getSelector returned none"
34-
-- | some _ => Lean.logInfo " ✓ getSelector succeeded"
35-
-- else
36-
-- Lean.logInfo "❌ No selector registered in imported state!"
16+
/--
17+
info: ✓ Selector registered in imported state
18+
---
19+
info: ✓ getSelector succeeded
20+
-/
21+
#guard_msgs in
22+
open Lean Lean.LibrarySuggestions in
23+
run_cmd do
24+
-- Check if a selector is registered
25+
let hasSelector := (librarySuggestionsExt.getState (← getEnv)).isSome
26+
if hasSelector then
27+
Lean.logInfo "✓ Selector registered in imported state"
28+
-- Try to retrieve the selector using getSelector
29+
Elab.Command.liftTermElabM do
30+
let selector? ← getSelector
31+
match selector? with
32+
| none => Lean.logInfo " ❌ getSelector returned none"
33+
| some _ => Lean.logInfo " ✓ getSelector succeeded"
34+
else
35+
Lean.logInfo "❌ No selector registered in imported state!"

0 commit comments

Comments
 (0)