Skip to content

chore: address weekly linting report - #1168

Open
jessealama wants to merge 4 commits into
leanprover:mainfrom
jessealama:weekly-lint-2026-10-26
Open

jessealama wants to merge 4 commits into
leanprover:mainfrom
jessealama:weekly-lint-2026-10-26

Conversation

@jessealama

@jessealama jessealama commented Oct 27, 2026 •

Copy link
Copy Markdown
Contributor

Take care of the linter messages from the weekly linting report.

Profiling results against main (mean of 5 runs):

  • vm_ltsD_ltsND_not_bisim: 41 ms → 43 ms (1029 → 1110 heartbeats)
  • exists_full_synthesis_finset: 70 ms → 50 ms (1289 → 1044 heartbeats)

Profiled using set_option trace.profiler true in, heartbeats from #count_heartbeats in.

@ctchou ctchou left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

LGTM.

Comment thread Cslib/Computability/Circuit/Full.lean Outdated
@chenson2018

Copy link
Copy Markdown
Collaborator

As previously noted, it would be appreciated when making these PRs to note the changes in performance when accepting mergeWithGrind suggestions, as these can be significant. Please follow the pattern in Mathlib of PRs like leanprover-community/mathlib4#36764 that list the change per declaration in the description.

@jessealama

Copy link
Copy Markdown
Contributor Author

I've did a bit of profiling and added the numbers to the PR description. Looks like it's a wash for these proofs.

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

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants