Skip to content

chore: backtick identifiers in Lake eval messages #11845

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

Jump to bottom
Open
alok wants to merge 1 commit into
base: master
Choose a base branch
from
Open

chore: backtick identifiers in Lake eval messages #11845

alok wants to merge 1 commit into from
+1 −1

Conversation

@alok
Copy link
Contributor

@alok alok commented Dec 30, 2025 •
edited
Loading

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

@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Dec 30, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Dec 30, 2025

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
Copy link
Collaborator

leanprover-bot commented Dec 30, 2025

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)

@alok alok marked this pull request as ready for review January 1, 2026 22:11
@alok alok requested a review from tydeu as a code owner January 1, 2026 22:11
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@tydeu tydeu Awaiting requested review from tydeu tydeu is a code owner

Assignees

No one assigned

Labels

toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@alok @leanprover-community-bot @leanprover-bot