chore: backtick identifiers in Lake eval messages

[alok]

This PR uses backticks instead of single quotes for identifiers in Lake package evaluation messages, following Lean's convention for referring to identifiers in warning messages.

🤖 Generated with Claude Code

[ghost]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase bba35e45320f8fa52247178418ae3bf2b0929d67 --onto c0d5e8bc2c925bc2b60f18c929acf7d73ea9ecec. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-30 06:04:18)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase bba35e45320f8fa52247178418ae3bf2b0929d67 --onto 2bca310bea01d0641183096bf33ede08a0a52022. You can force reference manual CI using the force-manual-ci label. (2025-12-30 06:04:20)

[tydeu]

This is a fine PR. However, the deprecated field will be removed in #11662 (which will be merged soon),, so I will let that solve this.