Skip to content
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.

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

chore: benchmarking leanprover/lean4#4700 #14599

Closed
wants to merge 2 commits into from

Conversation

kim-em
Copy link
Contributor

@kim-em kim-em commented Jul 10, 2024

No description provided.

@kim-em kim-em added the WIP Work in progress label Jul 10, 2024
@kim-em
Copy link
Contributor Author

kim-em commented Jul 10, 2024

!bench

Copy link

PR summary 80de3bdd01

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Too many changes (4007)!

Declarations diff

+ instance : (forget V G).Faithful where map_injective w := Hom.ext w
+ instance [DecidableEq α] : DecidableEq αˣ := fun _ _ => decidable_of_iff' _ Units.ext_iff
++++ ext_iff'
- AddContent.ext_iff
- Bornology.ext_iff
- MeasurableSpace.ext_iff
- Perm.ext_iff
- eq_iff
- get!_none
- get!_some
- instance : (forget V G).Faithful where map_injective w := Hom.ext _ _ w
- instance [DecidableEq α] : DecidableEq αˣ := fun _ _ => decidable_of_iff' _ ext_iff
- isSome_map
- limit_ext_iff
- pi_ext'_iff
- unique_ext_iff
-++- ext
-+-+ Hom.ext'
-- subtype_ext_iff
--- ext_ring_iff
---------------------------------------------------------------------------------------------------------- ext_iff

You can run this locally as follows
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 80de3bd.
There were no significant changes against commit 42e4b62.

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-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 Jul 10, 2024
@kim-em kim-em closed this Jul 16, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) WIP Work in progress
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants