Skip to content

chore: list hints in order of priority #37580

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
ldct wants to merge 1 commit into
base: master
Choose a base branch
from
+7 −7
Open

chore: list hints in order of priority #37580

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 7 additions & 7 deletions Mathlib/Tactic/Common.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -142,17 +142,17 @@ public meta section

section Hint

register_hint 200 grind
register_hint 1000 trivial
register_hint 500 tauto
register_hint 1000 split
register_hint 1000 decide
Copy link
Copy Markdown
Contributor

@grunweg grunweg Apr 3, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I vaguely remember hint being sensitive to the order in which you registered tactics --- you are sorting the order tactics alphabetically within each priority, which changes this. I'm not 100% sure if this is correct; if it is, could this be the cause of test failures? (If so, adding a comment about this is surely good; I would understand that this is confusing.)

register_hint 1000 intro
register_hint 80 aesop
register_hint 1000 split
register_hint 1000 trivial
register_hint 800 simp_all?
register_hint 600 exact?
register_hint 1000 decide
register_hint 200 omega
register_hint 500 tauto
register_hint 200 fun_prop
register_hint 200 grind
register_hint 200 omega
register_hint 80 aesop

end Hint

Expand Down
Loading