Skip to content

feat: TryThis suggestion for the mergeWithGrind linter#37236

Open
chenson2018 wants to merge 1 commit intoleanprover-community:masterfrom
chenson2018:mergeWithGrind-suggestion
Open

feat: TryThis suggestion for the mergeWithGrind linter#37236
chenson2018 wants to merge 1 commit intoleanprover-community:masterfrom
chenson2018:mergeWithGrind-suggestion

Conversation

@chenson2018
Copy link
Copy Markdown
Contributor

@chenson2018 chenson2018 commented Mar 26, 2026

This PR changes the mergeWithGrind linter to provide a TryThis suggestion. The same message is provided as the currently logged warning, and should still be processed properly by zulip_build_report.sh during the weekly linting, just under info instead of warning.

The motivation here (discussed in #general > automatically apply code actions) is that following #36712 we should be able to partially automate the weekly linting PRs using Skimmer. As an example, the changes in #37018 were prepared in part in this way.


Open in Gitpod

@github-actions
Copy link
Copy Markdown

PR summary c551257516

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

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).

@github-actions github-actions bot added the t-meta Tactics, attributes or user commands label Mar 26, 2026
if let some stop := postI.tacI.stx.getTailPos? then
let synth := Lean.Syntax.setInfo (Lean.SourceInfo.synthetic start stop) preI.tacI.stx
Elab.Command.liftCoreM <|
Tactic.TryThis.addSuggestion (header := header) synth (← `(tactic | grind))
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Did you verify none of the tooling relies on the linter warnings to be logWarnings instead of logInfos?

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

Yes, this is what I was trying to describe in the PR description, apologies if that was unclear. To my knowledge the only workflow that uses this option is weekly-lints.yml, which in using zulip_build_report.sh should report either.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

t-meta Tactics, attributes or user commands

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants