Note that the following comment is now not valid anymore:

/- If made an instance, causes timeouts synthesizing `FaithfulSMul R I.ResidueField` at
`Ideal.algebraMap_residueField_eq_zero` and `Ideal.ker_algebraMap_residueField` during
simpNF linting. -/
lemma Module.finite_of_isArtinianRing [IsJacobsonRing R] [IsArtinianRing A] :
    Module.Finite R A :=

Should this now be made an instance?

PR summary 4955224a12

Import changes for modified files

No significant changes to the import graph

Declarations diff

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

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

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

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

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

!bench

Here are the benchmark results for commit 4955224.
There were no significant changes against commit 63a7be5.

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

Note that the following comment is now not valid anymore:

/- If made an instance, causes timeouts synthesizing `FaithfulSMul R I.ResidueField` at
`Ideal.algebraMap_residueField_eq_zero` and `Ideal.ker_algebraMap_residueField` during
simpNF linting. -/
lemma Module.finite_of_isArtinianRing [IsJacobsonRing R] [IsArtinianRing A] :
    Module.Finite R A :=

Should this now be made an instance?

Fun test would be: for each instance added in a PR

• get the general arguments to the instance
• time synthesis before and after for the general problem with import Mathlib
• report the differences

You wouldn't need two toolchains since you can de-instance the new one.

But I am happy to punt this question to a separate PR. The documentation is good enough to remind us we still have an un-resolved problem.

bors merge

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style

• time synthesis before and after for the general problem with import Mathlib

I had some trouble understanding what you mean. I think you mean a sort of analogue to the simpNF linter, where we run type class search on the general pattern where we would expect the particular instance to apply (but we don't supply the type class conditions).

So in this example it would measure how much time synthesizing (and failing) [IsJacobsonRing R] [IsArtinianRing A] takes for fixed R and A.

Here I would mean something like

import Mathlib 

variable (R : Type*)  (M : Type*) [Semiring R]  [AddCommMonoid M] [Module R M]

set_option trace.profiler true in
#synth Module.Finite R M 

attribute [-instance] Module.finite_of_isArtinianRing

set_option trace.profiler true in
#synth Module.Finite R M 

I am more concerned with slow failing searches than making existing successful searches worse.