mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

bench: test syntax linter

Open thorimur opened this issue 1 year ago • 2 comments
trafficstars

The purpose of this PR is just to bench the "best-case scenario" for a linter which iterates through syntax, updating and checking a simple counter along the way.

Open in Gitpod

thorimur avatar Mar 20 '24 01:03 thorimur

!bench

thorimur avatar Mar 20 '24 01:03 thorimur

Here are the benchmark results for commit 22bba3fca0b10ed16e0c48d31b2ae063a10b5eff. There were no significant changes against commit 69fd837a71463d8905afbf335b908a035aa11a7e.

leanprover-bot avatar Mar 20 '24 02:03 leanprover-bot

I'm coming here for PR triage: it looks like this PR has fulfilled and can be closed. Is this correct?

grunweg avatar May 03 '25 07:05 grunweg