[Merged by Bors] - feat: add `#check'` command and tactic, which only show explicit arguments by grunweg · Pull Request #31194 · leanprover-community/mathlib4

grunweg · 2025-11-02T16:46:35Z

In some areas (such as differential geometry), many lemmas have a lot of implicit and typeclass arguments.
Using #check foo to determine which explicit arguments are expected for a given lemma gives output which is painful to read, because the explicit argument is buried among many lines of other output.

The #check' command and tactic produce very similar output, but with implicit and typeclass arguments omitted.
This increases usability a lot.

In the future, this could (and should) be unified to the #check command in core, by becoming e.g. #check +only-explicit. Until then, let us add this to mathlib to facilitate experimentation of the most useful behaviour.

From the project towards geodesics and the Levi-Civita connection.

Co-authored-by: Kyle Miller kymiller@ucsc.edu
Co-authored-by: Patrick Massot patrickmassot@free.fr

github-actions · 2025-11-02T16:47:40Z

PR summary f3179c596d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ bar
+ foo
- elabCheckTactic

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

grunweg · 2025-11-02T17:02:05Z

@kmill I'm very open to making a PR against Lean core instead, if that is a better solution.
I don't want to block this quality of life improvement on capacity in core to maintain this code, though.

thorimur

Looks good! :) There's an important comment or two in here about control flow changes which are responsible for the (new) double-logging seen in the tests, and which seem accidental to me.

Besides that, though, it's just refactoring, and we can do that as a chore later if this is really helpful to get in quickly. It seems like a big QoL improvement. :)

Also, another question for the future: should there eventually be some way to see that we're omitting implicit arguments, or does that just get in the way? Ideas if this is a direction we want to pursue:

(consecutive occurrences of) implicit arguments are replaced by ⋯ in the signature
the type signature is followed by something like 3 implicit arguments omitted on a new line
the type signature is followed by 3 implicit arguments omitted, including instances of <names of typeclasses> (without their arguments), in case this would be useful information

Mathlib/Tactic/Check.lean

thorimur · 2025-11-14T20:41:03Z

Mathlib/Tactic/Check.lean

+def checkPrimeInner (tk : Syntax) (term : Term) : TacticM Unit := do
+  for c in (← realizeGlobalConstWithInfos term) do
+    addCompletionInfo <| .id term c (danglingDot := false) {} none


This for loop and addCompletionInfo are shared between the checkPrimes, and (1) we never use term in the rest of the body (2) term is expected to be an ident, something that makes sense when reading at the call site, but is a nonlocal fact here.

So, unless you're anticipating some changes later, I'd suggest:

inline these first two lines in elabCheckTacticInner, after guard (see below)

change the type of these inner functions to checkPrimeInner (tk : Syntax) (c : Name) : TacticM Unit

We can go further and factor out logInfoAt tk too, which means the type signature could become simply Name → TermElabM MessageData. :)

As with other refactoring suggestions, we can do this after getting it in if you like.

Mathlib/Tactic/Check.lean

mathlib4-merge-conflict-bot · 2025-11-19T08:20:02Z

This pull request has conflicts, please merge master and resolve them.

grunweg · 2026-03-07T10:57:44Z

Thanks for your careful review comments, as usual. I just got back to this PR and addressed your key comments. The refactorings you mention seem useful to have, but I'd be happy to have them in a follow-up. (When working on differential geometry, it is nice to have these --- I was working on a branch containing this, so it's not really urgent to get in, but seems nice to not stall this a lot.)

grunweg · 2026-03-07T10:58:46Z

There have been other discussions about the user experience on zulip, including modifying #check to dim out implicit arguments. My understanding is that we're still iterating on the best way to get this out, and having this available for experimentation could help. I'm happy to stick a comment (that this is experimental) somewhere, if you prefer.

grunweg · 2026-03-07T10:58:50Z

-awaiting-author

grunweg · 2026-03-20T12:45:12Z

Thanks a lot for the refactoring!
I like the test changes; the code changes seem sensible to me. I am not confident about all the details, but trust you to do something reasonable. Would you like to maintainer merge it? (Another pair of eyes would be great, in any case.)

Mathlib/Tactic/Check.lean

thorimur · 2026-03-20T21:14:45Z

Mathlib/Tactic/Check.lean

+If `t` is an identifier, then it pretty prints a type declaration form
+for the global constant `t` instead.
+Use `#check' (t)` to pretty print it as an elaborated expression.
+


I think we can omit this, as it's redundant information for the user. I realize it's copied from the #check tactic, but maybe we should delete it there too? Unless you can think of a case for when the user needs to know the difference, of course!

Suggested change

If `t` is an identifier, then it pretty prints a type declaration form

for the global constant `t` instead.

Use `#check' (t)` to pretty print it as an elaborated expression.

Hm, I'm on the fence. On on hand, most users won't care much about the difference --- but making this information discoverable when it is needed seems useful. (I hadn't thought about the different until now --- it makes perfect sense now, but do we want to require this?)

Let's see what a maintainer reviewing this thinks!

Mathlib/Tactic/Check.lean

thorimur · 2026-03-20T21:47:29Z

After the minor documentation suggestions here, I think this is good to go :)

I've contributed a refactor here. The code I've introduced stays very close to lean core's #check, and the rest of the refactor is moving around existing code, with the exception of

using .ofConstName c and declSig instead of declSigWithId, so that we get hovers on the constant to expose the full type signature
aggregating binders that have been left behind a ∀ by delabForallParamsWithSignature. (Note that delabForallParamsWithSignature still brackets the binders here even if they don't have accessible names, so this move is valid.)

So, I think it's prudent to have another pair of eyes :)

maintainer delegate?

github-actions · 2026-03-20T21:48:04Z

🚀 Pull request has been placed on the maintainer queue by thorimur.

issue_comment, wf_run

Co-authored-by: Thomas R. Murrills <68410468+thorimur@users.noreply.github.com>

jcommelin

Thanks 🎉

bors merge

…ments (#31194) In some areas (such as differential geometry), many lemmas have a *lot* of implicit and typeclass arguments. Using `#check foo` to determine which explicit arguments are expected for a given lemma gives output which is painful to read, because the explicit argument is buried among many lines of other output. The `#check'` command and tactic produce very similar output, but with implicit and typeclass arguments omitted. This increases usability a lot. In the future, this could (and should) be unified to the #check command in core, by becoming e.g. `#check +only-explicit`. Until then, let us add this to mathlib to facilitate experimentation of the most useful behaviour. From the project towards geodesics and the Levi-Civita connection. Co-authored-by: Kyle Miller <kymiller@ucsc.edu> Co-authored-by: Patrick Massot <patrickmassot@free.fr> Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>

mathlib-bors · 2026-03-21T08:06:46Z

Build failed (retrying...):

ci (staging) / Build

…ments (#31194) In some areas (such as differential geometry), many lemmas have a *lot* of implicit and typeclass arguments. Using `#check foo` to determine which explicit arguments are expected for a given lemma gives output which is painful to read, because the explicit argument is buried among many lines of other output. The `#check'` command and tactic produce very similar output, but with implicit and typeclass arguments omitted. This increases usability a lot. In the future, this could (and should) be unified to the #check command in core, by becoming e.g. `#check +only-explicit`. Until then, let us add this to mathlib to facilitate experimentation of the most useful behaviour. From the project towards geodesics and the Levi-Civita connection. Co-authored-by: Kyle Miller <kymiller@ucsc.edu> Co-authored-by: Patrick Massot <patrickmassot@free.fr> Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>

mathlib-bors · 2026-03-21T09:42:08Z

Pull request successfully merged into master.

Build succeeded:

…ments (leanprover-community#31194) In some areas (such as differential geometry), many lemmas have a *lot* of implicit and typeclass arguments. Using `#check foo` to determine which explicit arguments are expected for a given lemma gives output which is painful to read, because the explicit argument is buried among many lines of other output. The `#check'` command and tactic produce very similar output, but with implicit and typeclass arguments omitted. This increases usability a lot. In the future, this could (and should) be unified to the #check command in core, by becoming e.g. `#check +only-explicit`. Until then, let us add this to mathlib to facilitate experimentation of the most useful behaviour. From the project towards geodesics and the Levi-Civita connection. Co-authored-by: Kyle Miller <kymiller@ucsc.edu> Co-authored-by: Patrick Massot <patrickmassot@free.fr> Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>

grunweg added 6 commits November 2, 2025 17:23

feat: add check' command, due to Kyle Miller

4070eee

chore: extract and refactor

45701ad

Extract another workhorse definition

e4affe7

wip: hook up to a new version; seems to work...

0f1212a

Basic tests: seems to work, if I just take a no-op

6213253

Switch out the new parser

c176bd6

grunweg added the t-meta Tactics, attributes or user commands label Nov 2, 2025

grunweg added 4 commits November 2, 2025 17:50

chore: move tests to the test file

95f6299

Move documentation

bbf8006

chore: simplify by moving one loop into the workhorse

674bb27

Tweak

d8539ce

grunweg requested a review from kmill November 2, 2025 17:01

grunweg mentioned this pull request Nov 2, 2025

Mr. Covariant Derivatives #26221

Draft

35 tasks

Avoid using sorry

e59e6e4

leanprover-community-bot-assistant assigned thorimur Nov 10, 2025

thorimur reviewed Nov 14, 2025

View reviewed changes

thorimur added the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 14, 2025

mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 19, 2025

Merge branch 'master' into checkPrime

2a1ba62

mathlib-merge-conflicts bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 7, 2026

grunweg added 4 commits March 7, 2026 10:34

More review comments

12bb854

Fix doc-string

e2d0f92

Review fix for control flow

7e11f2c

Test update

c8deb44

grunweg removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 7, 2026

thorimur added 6 commits March 20, 2026 02:20

feat: rewrite + fix

cc2c0ae

chroe: pare back

8cc1f60

chore: docs

4edc566

chore: pare back even more

950acf9

chore: comment

913dbac

chore: tweak wording

5b4c52a

thorimur reviewed Mar 20, 2026

View reviewed changes

Mathlib/Tactic/Check.lean Outdated Show resolved Hide resolved

thorimur reviewed Mar 20, 2026

View reviewed changes

Mathlib/Tactic/Check.lean Show resolved Hide resolved

thorimur reviewed Mar 20, 2026

View reviewed changes

Mathlib/Tactic/Check.lean Outdated Show resolved Hide resolved

mathlib-triage bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Mar 20, 2026

Apply suggestions from code review

5765229

Co-authored-by: Thomas R. Murrills <68410468+thorimur@users.noreply.github.com>

jcommelin reviewed Mar 21, 2026

View reviewed changes

mathlib-triage bot added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Mar 21, 2026

mathlib-bors bot changed the title ~~feat: add #check' command and tactic, which only show explicit arguments~~ [Merged by Bors] - feat: add #check' command and tactic, which only show explicit arguments Mar 21, 2026

mathlib-bors bot closed this Mar 21, 2026

grunweg deleted the checkPrime branch March 21, 2026 10:22

	If `t` is an identifier, then it pretty prints a type declaration form
	for the global constant `t` instead.
	Use `#check' (t)` to pretty print it as an elaborated expression.

Conversation

grunweg commented Nov 2, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Nov 2, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary f3179c596d

Import changes for modified files

Declarations diff

Uh oh!

grunweg commented Nov 2, 2025

Uh oh!

thorimur left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

thorimur Nov 14, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib4-merge-conflict-bot commented Nov 19, 2025

Uh oh!

grunweg commented Mar 7, 2026

Uh oh!

grunweg commented Mar 7, 2026

Uh oh!

grunweg commented Mar 7, 2026

Uh oh!

grunweg commented Mar 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

thorimur Mar 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

grunweg Mar 21, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

thorimur commented Mar 20, 2026

Uh oh!

github-actions bot commented Mar 20, 2026

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Mar 21, 2026

Uh oh!

mathlib-bors bot commented Mar 21, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

grunweg commented Nov 2, 2025 •

edited

Loading

github-actions bot commented Nov 2, 2025 •

edited

Loading

grunweg commented Mar 20, 2026 •

edited

Loading

thorimur Mar 20, 2026 •

edited

Loading