char_zero

Stream: maths

[Damiano Testa]

I have just noticed that some definitions around char_zero and char_p seem to assume that the base type is an appropriately decorated ring, while the definitions make sense for [add_monoid R] [has_one R].

Is there a reason for assuming multiplication? I imagine that this might be some "historical artifact", arising from the fact that there was no action of the natural numbers on an add_monoid_with 1.

If this is the case, then it might make sense to refactor and weaken the hypotheses.

If there is a deeper reason for assuming more than strictly needed, then I would be curious to know!

Thanks!

[Kevin Buzzard]

First monoids with zero and now this! I don't see any reason why it shouldn't be generalised to add_monoids with 1, I'm pretty sure there's a map from the naturals to such a thing. However I am not so convinced that there is a mathematically sensible notion of "characteristic", e.g. we have these monoids like Z/nZ where everything bigger than n-1 stays at n-1, and just knowing the kernel of the map from nat into this ring doesn't really tell you the whole truth. On the other hand all the basic stuff will go through for add_groups with 1 where...wait...this is just the theory of the order of an element, right? We have this already. Maybe the correct thing to do is to refactor characteristic to just be the order of 1 in the add_comm_group?

[Damiano Testa]

Yes, this is what I would have thought as well... For me, the characteristic of a add_monoid with 1 is the order of 1...

[Julian Külshammer]

I agree. One problem is that there is currently no add_order_of although this is on my list of possible future PRs since by now I'm reasonably familiar with the order_of API. If I understand correctly, though, many proofs will have to be ported manually as [to_additive] doesn't translate nicely between g^n and n*g. Is that understanding correct?

[Kevin Buzzard]

Aargh! Yes that's right, and it's simply because of the order of the inputs.

[Damiano Testa]

Maybe the order of inputs issue can be overcome by using that they are both modules for nat? I am talking without having experience, so I may be saying something very silly!

[Kevin Buzzard]

I don't think a non-commutative group is a nat-module because it doesn't satisffy $g^nh^n=(gh)^n$.

[Eric Wieser]

Indeed, the nat-module structure is called docs#add_comm_monoid.nat_module

[Johan Commelin]

Julian Külshammer said:

I agree. One problem is that there is currently no add_order_of although this is on my list of possible future PRs since by now I'm reasonably familiar with the order_of API. If I understand correctly, though, many proofs will have to be ported manually as [to_additive] doesn't translate nicely between g^n and n*g. Is that understanding correct?

Maybe a meta programmer can comment on how hard it would be to hardcode special support into to_additive for this specific situation (i.e. pow vs nsmul).

[Eric Wieser]

I was wondering if we can get by by introducing an auxiliary nsmul' abbreviation with its arguments swapped

[Damiano Testa]

Ah, as usual, I was thinking of commutative additive/multiplicative groups, I did not think about the fact that this would have to be defined across all groups, commutative or not. Too bad!

[Julian Külshammer]

I started add_order_of manually in #6770. If someone wants to stop me because it can be done via automation, let me know. It feels close to automatic, but occasionally tricky because you have to switch from right to left and leave the 1s in nat untouched.

[Kevin Buzzard]

The automation suggestion was to beef up to_additive so it relates monoid.pow to some new function add_monoid.nat_action_on_the-right where the variables are in the right order (note : I wouldn't have a clue how to do this but others here will) and then define order using this right action.

[Damiano Testa]

I am trying to get the definition of characteristic to assume less than it currently does in #6765. After fixing a few easy timeouts, I am now stuck.

The problem file is

ring_theory/perfection.lean

and specifically line 287, that no longer compiles.
https://github.com/leanprover-community/mathlib/blob/09dbf4321bd3792bd0676c91ac81706b45d7b192/src/ring_theory/perfection.lean#L287

-- Why is this slow?
lemma map_eq_map (φ : R →+* S) : map p (of p R) (of p S) φ = perfection.map p φ :=
hom_ext _ (of p S) $ λ f, by rw [map_map, perfection.coeff_map]

The "-- Why is this slow?" comment was already there.

Git thinks that this was added by @Kenny Lau . If anyone could give a suggestion of how to speed this up, I would be very happy!

Thanks!

[Kenny Lau]

#6800 might be related

[Damiano Testa]

So, the suggestion is simply that if I wait enough time, then the timeout disappears?

[Kenny Lau]

the suggestion is that after #6800 gets merged the timeout should disappear

[Scott Morrison]

You could just merge #6800 to your branch to find out!

[Damiano Testa]

Typing

git merge eric-wieser/subalgebra-coe

is what you are suggesting? I am not so good with git, so this is really a silly question that is not leading anywhere else!

[Damiano Testa]

Literally that does not work:

 (adomani_weaken_chap_p)$ git merge eric-wieser/subalgebra-coe
merge: eric-wieser/subalgebra-coe - not something we can merge

[Kenny Lau]

try git fetch origin first

[Kenny Lau]

and then git merge origin/eric-wieser/subalgebra-coe

[Damiano Testa]

Kenny, thanks: The merging worked!

Now to see if it fixes the timeout!

[Damiano Testa]

fetch made my copy of master aware of another branch? is this why this worked?

[Ruben Van de Velde]

It made your local clone of the repository aware of the new branches. (I guess this is what you meant)

[Damiano Testa]

Ruben, thanks! you said more correctly what I had in a confused state in my mind!

[Eric Wieser]

Note that you might be able to speed up the rebuild on your local machine by running leanproject get-cache --rev origin/eric-wieser/subalgebra-coe

[Damiano Testa]

leanproject seems to not like --rev:

 (adomani_weaken_chap_p)$ leanproject get-cache --rev origin/eric-wieser/subalgebra-coe
Usage: leanproject get-cache [OPTIONS]
Try 'leanproject get-cache -h' for help.

Error: no such option: --rev

[Johan Commelin]

Do you have the latest version?

[Damiano Testa]

However, when I ask Lean to make the single file ring_theory/perfection.lean, it does it without problems. However, when I open it with VSCode, it gives the timeout.

I will wait to see what happens with CI...

[Kevin Buzzard]

which version of leanproject are you on? I've had no problems with --rev, I usually put --rev HEAD~1 or something.

[Damiano Testa]

Johan, how do I find out which version of leanproject do I have?

[Kevin Buzzard]

leanproject --version

[Kevin Buzzard]

leanproject --help tells you all the options

[Damiano Testa]

(adomani_weaken_chap_p)$ leanproject --version
leanproject, version 0.0.9

[Kevin Buzzard]

you need to get the latest version. We're on 1.0.0 now and it works great.

$ leanproject get-cache --help
Usage: leanproject get-cache [OPTIONS]

  Restore cached olean files.

Options:
  --force     Get cache even if the repository is dirty.
  --rev TEXT  A git sha.
  -h, --help  Show this message and exit.
buzzard@bob:~$

[Damiano Testa]

ok, I will try to upgrade, then

[Kevin Buzzard]

1.0.0 has been stable for a long time and has I think dealt with every issue which people threw at Patrick.

[Damiano Testa]

Is this what I should do?

python3 -m pip install --user pipx
python3 -m pipx ensurepath
source ~/.profile
pipx install mathlibtools

[Damiano Testa]

(found here:
https://leanprover-community.github.io/install/linux.html
)

[Julian Berman]

You shouldn't need all of that. Probably pipx upgrade mathlibtools is all you need.

[Riccardo Brasca]

pipx upgrade mathlibtools works for me

[Damiano Testa]

Julian and Riccardo: thank you both very much!

 (adomani_weaken_chap_p)$ pipx upgrade mathlibtools
upgraded package mathlibtools from 0.0.9 to 1.0.0 (location: /home/damiano/.local/pipx/venvs/mathlibtools)
 (adomani_weaken_chap_p)$ leanproject --version
leanproject, version 1.0.0

[Damiano Testa]

and now it learned rev!

[Damiano Testa]

Eric's PR is getting merged, but it looks like this may not speed up the processing of the lemma in ring_theory/perfection enough to prevent the timeout, unfortunately.

I will wait until it is actually merged, but on my machine it still times out.

[Damiano Testa]

Adding @ and filling in a few underscores speeds up the processing to a place where, on my machine, it no longer times out on this lemma!

The result is not really pretty, especially since this happens on the statement of the lemma: if anyone has any alternative, I would be happy to hear about it!

This now elaborates in 2.33s, instead of timing out (on my machine):

-- Why is this slow?
lemma map_eq_map (φ : R →+* S) : @map p _inst_1 R _inst_2 _inst_3 (ring.perfection R p)
    _ _ _ S _ _ _ _ _ _ _ (of p R) _ (of p S) φ =
  @perfection.map R _inst_2 p _inst_1 _inst_3 S _inst_7 _inst_8 φ :=
hom_ext _ (of p S) $ λ f, by rw [map_map, perfection.coeff_map]

(for those who may take a look at this, the S lost in the sea of underscores in the lhs is what gave me the impression of the largest relative speedup. This might have been an artifact of how I was filling in the underscores, though, not of anything actually having to do with the processing.)

[Johan Commelin]

Do you need to fill in the _inst_ns?

[Johan Commelin]

Because those are extremely brittle from a maintenance point of view. (Should we lint against them?)

[Johan Commelin]

rg "_inst_" | wc -l
37

[Kevin Buzzard]

I think that we should try to keep the number there

[Damiano Testa]

I probably do not, in fact, I got it to avoid the time out without the @ on the rhs, but it made it faster to add it there.

[Damiano Testa]

I will profile it with and without the inst and report!

[Gabriel Ebner]

Johan Commelin said:

rg "_inst_" | wc -l
37

Many of them are in meta code:

let e_inst_type := (expr.const class_nm raw_levels).mk_app args

[Gabriel Ebner]

I count 14 explicit references.

[Damiano Testa]

without the _inst_ it elaborates in 2.54s and, to be honest, this variation may not have anything to do with the search for instances: the profiler gives different results in different runs anyway.

so, I should remove the insts, right?

[Johan Commelin]

rg "\b_inst_" | wc -l
19

is maybe a more honest count

[Damiano Testa]

This is what the lemma looks like now:

-- Why is this slow?
lemma map_eq_map (φ : R →+* S) :
  @map p _ R _ _ (ring.perfection R p) _ _ _ S _ _ _ _ _ _ _ (of p R) _ (of p S) φ =
  @perfection.map R _ p _ _ S _ _ φ :=
hom_ext _ (of p S) $ λ f, by rw [map_map, perfection.coeff_map]

[Johan Commelin]

yeah, if that doesn't time out, I would leave it like that

[Damiano Testa]

ok, in any case, so far, timing out has been on my machine alone, but a lemma that processes in under 3s should not give CI problems... right? :wink:

[Johan Commelin]

and hopefully @Kenny Lau will have another "speed up mathlib" marathon in the future, and figure out the real cause of why this is slow

[Damiano Testa]

my, very limited, experience is that Lean takes a lot of time to figure out implicit domains/codomains of implicit maps. this was at least my rationale for getting the S in the right place in the code above. for some mysterious reason, this actually worked...

[Damiano Testa]

and it seems that the statement that Kevin made chronologically just before mine on a different topic supports this!

[Eric Wieser]

Are there any underscores you can replace with type annotations?

[Damiano Testa]

I can try: is that preferred to having a simple underscore?

[Eric Wieser]

I'd say it's preferred to using @

[Damiano Testa]

Ah, I think that the initial formulation had no underscores and filled in all the needed underscores. I introduced the @ and the underscores to be able to fill in arguments that were implicit before.

[Damiano Testa]

This was the statement of the lemma before it started timing out:

lemma map_eq_map (φ : R →+* S) : map p (of p R) (of p S) φ = perfection.map p φ :=

[Eric Wieser]

Wait, so that version doesn't time out?

[Eric Wieser]

Or do you mean, "which started timing out"

[Damiano Testa]

The last one used to be slow, but not timing out, before I introduced the changes in a different file. Now, to get mathlib to build, this one times out and hence I introduced the @ and the partially filled in underscores.

[Eric Wieser]

I wonder if for instance you can get away with just putting a @ on the LHS or RHS but not both

[Damiano Testa]

Yes, just one side should be possible, but it gets progressively faster if I do it on both sides.

[Damiano Testa]

since I wanted to make sure that it would not time out, I went for the fastest! an intermediate stage might also work, but right now I am trying to get CI to work at least once.

[Damiano Testa]

CI seems to be making progress: it went past the stage of building mathlib and is now linting/testing!

[Damiano Testa]

profiling on my machine, suggests a similar processing time for the lemma below as for the more expanded one above:

lemma map_eq_map (φ : R →+* S) :
  @map p _ R _ _ _ _ _ _ S _ _ _ _ _ _ _ (of p R) _ (of p S) φ =
  perfection.map p φ :=
hom_ext _ (of p S) $ λ f, by rw [map_map, perfection.coeff_map]

(no @ in the RHS, only S as previously implicit argument, now explicitly given. If I replace S by an underscore, leaving the @ and the other underscores, Lean still seems to make the processing work, but barely.)

Removing the @ in the LHS and keeping the one on the RHS times out. Thus, the explicit S seems to be helpful, but simply putting an @ seems to be already giving a good amount of hints to Lean.

[Damiano Testa]

The fully @-expanded version was accepted by CI, modulo the dependent #6800! I am not sure whether #6800 is actually needed for the speed up, but it is not so important.

I will now try to push the "minimally" @-expanded version and see if CI still manages to work with it.

[Damiano Testa]

The shorter version with a single @ works!

I am also trying to remove the merged PR.

[Damiano Testa]

The unentangled version also builds! So, once #6800 merges, I might try to see if removing the @ still gives a time out or not, but at the moment, PR #6765 builds independently!

[Eric Wieser]

I'm getting a timeout in docs#perfection_map.map_eq_map` again in #6786.

[Kevin Buzzard]

This is in ring_theory.perfection? I see timeouts earlier, e.g.

lemma pth_root_frobenius : (pth_root R p).comp (frobenius _ p) = ring_hom.id _ :=
ring_hom.ext $ λ x, ext $ λ n,
begin
  rw ring_hom.comp_apply,
  rw ring_hom.id_apply,
  rw coeff_pth_root, -- all fast
  convert coeff_frobenius _ _, -- slow (several seconds), as is `rw coeff_frobenius` and `apply coeff_frobenius`
end

[Eric Wieser]

Have you configured vs-code with a different timeout to CI?

[Eric Wieser]

(or are you on a diffferent commit / cache?)

[Kevin Buzzard]

almost certainly, because I don't normally think about this sort of thing

[Kevin Buzzard]

I'm just saying "stuff in this file is surprisingly slow, here's another example"

[Kevin Buzzard]

lemma pth_root_frobenius : (pth_root R p).comp (frobenius _ p) = ring_hom.id _ :=
ring_hom.ext $ λ x, ext $ λ n,
begin
  rw ring_hom.comp_apply,
  rw ring_hom.id_apply,
  rw coeff_pth_root,
  rw coeff_frobenius x, -- quick
end

Unification is going down a rabbit-hole maybe. If you put pp.all on you can see the terms are huge. Removing the x takes elaboration up to 5.73 seconds from 273ms

[Eric Wieser]

The fix there being that you told lean what x was I assume

[Kevin Buzzard]

If you look at where the orange bars get stuck you can see the slow lemmas. The next one is frobenius_pth_root, and then of and then map_eq_map

[Eric Wieser]

Yeah, good find

[Eric Wieser]

Relatedly, map is a weird definition because it takes a perfection_map X Y argument which it ignores and uses only to infer X and Y

[Kevin Buzzard]

I'm afraid I have to clock off now -- marking :-/

[Kevin Buzzard]

lemma frobenius_pth_root : (frobenius _ p).comp (pth_root R p) = ring_hom.id _ := sorry -- slow

[Kevin Buzzard]

Even this is slow. If even this is slow then you can see something's wrong.

lemma frobenius_pth_root : (frobenius (ring.perfection R p) p).comp (pth_root R p) = ring_hom.id (ring.perfection R p) := sorry

[Eric Wieser]

I guess you're marking Kenny's old code then since you're still here?

[Kevin Buzzard]

set_option trace.class_instances true
lemma frobenius_pth_root : (frobenius (ring.perfection R p) p).comp (pth_root R p) = ring_hom.id (ring.perfection R p) := sorry

generates 2749 lines of debugging output.

[Eric Wieser]

Also, set_option profiler true doesn't seem to notice that its slow

[Eric Wieser]

It concedes that the longest step took 51ms

[Kevin Buzzard]

https://gist.github.com/kbuzzard/226abffabe7ee22f464977128b9157ed

[Kevin Buzzard]

OK I really am going now.

[Kevin Buzzard]

The story of nonempty nat:

[class_instances] (2) ?x_58 : nonempty ℕ := unit_interval.nonempty
failed is_def_eq
[class_instances] (2) ?x_58 : nonempty ℕ := @affine_map.nonempty ?x_66 ?x_67 ?x_68 ?x_69 ?x_70 ?x_71 ?x_72 ?x_73 ?x_74 ?x_75 ?x_76 ?x_77
failed is_def_eq
[class_instances] (2) ?x_58 : nonempty ℕ := @quiver.rooted_connected.nonempty_path ?x_78 ?x_79 ?x_80 ?x_81 ?x_82
failed is_def_eq
[class_instances] (2) ?x_58 : nonempty ℕ := ?x_84.nonempty_sets
failed is_def_eq
[class_instances] (2) ?x_58 : nonempty ℕ := @finset.has_insert.insert.nonempty ?x_85 ?x_86 ?x_87 ?x_88
failed is_def_eq
[class_instances] (2) ?x_58 : nonempty ℕ := @set.nonempty_Iio_subtype ?x_89 ?x_90 ?x_91 ?x_92
failed is_def_eq
[class_instances] (2) ?x_58 : nonempty ℕ := @set.nonempty_Ioi_subtype ?x_93 ?x_94 ?x_95 ?x_96
failed is_def_eq
[class_instances] (2) ?x_58 : nonempty ℕ := @set.nonempty_Iic_subtype ?x_97 ?x_98 ?x_99
failed is_def_eq
[class_instances] (2) ?x_58 : nonempty ℕ := @set.nonempty_Ici_subtype ?x_100 ?x_101 ?x_102
failed is_def_eq
[class_instances] (2) ?x_58 : nonempty ℕ := @set.range.nonempty ?x_103 ?x_104 ?x_105 ?x_106
failed is_def_eq
[class_instances] (2) ?x_58 : nonempty ℕ := @set.image.nonempty ?x_107 ?x_108 ?x_109 ?x_110 ?x_111
failed is_def_eq
[class_instances] (2) ?x_58 : nonempty ℕ := @set.has_insert.insert.nonempty ?x_112 ?x_113 ?x_114
failed is_def_eq
[class_instances] (2) ?x_58 : nonempty ℕ := @set.univ.nonempty ?x_115 ?x_116
failed is_def_eq
[class_instances] (2) ?x_58 : nonempty ℕ := @nonempty_lt ?x_117 ?x_118 ?x_119 ?x_120
failed is_def_eq
[class_instances] (2) ?x_58 : nonempty ℕ := @nonempty_gt ?x_121 ?x_122 ?x_123 ?x_124
failed is_def_eq
[class_instances] (2) ?x_58 : nonempty ℕ := @order_dual.nonempty ?x_125 ?x_126
failed is_def_eq
[class_instances] (2) ?x_58 : nonempty ℕ := @prod.nonempty ?x_127 ?x_128 ?x_129 ?x_130
failed is_def_eq
[class_instances] (2) ?x_58 : nonempty ℕ := @add_torsor.nonempty ?x_131 ?x_132 ?x_133 ?x_134
[class_instances] (3) ?x_134 : @add_torsor ?x_131 ℕ ?x_133 := @affine_map.add_torsor ?x_135 ?x_136 ?x_137 ?x_138 ?x_139 ?x_140 ?x_141 ?x_142 ?x_143 ?x_144 ?x_145 ?x_146
failed is_def_eq
[class_instances] (3) ?x_134 : @add_torsor ?x_131 ℕ ?x_133 := @pi.add_torsor ?x_147 ?x_148 ?x_149 ?x_150 ?x_151
failed is_def_eq
[class_instances] (3) ?x_134 : @add_torsor ?x_131 ℕ ?x_133 := @prod.add_torsor ?x_152 ?x_153 ?x_154 ?x_155 ?x_156 ?x_157 ?x_158 ?x_159
failed is_def_eq
[class_instances] (3) ?x_134 : @add_torsor ?x_131 ℕ ?x_133 := @add_group_is_add_torsor ?x_160 ?x_161
[class_instances] (4) ?x_161 : add_group ℕ := @power_series.add_group ?x_162 ?x_163
failed is_def_eq
[class_instances] (4) ?x_161 : add_group ℕ := @mv_power_series.add_group ?x_164 ?x_165 ?x_166
failed is_def_eq
[class_instances] (4) ?x_161 : add_group ℕ := @add_monoid_algebra.add_group ?x_167 ?x_168 ?x_169
failed is_def_eq
[class_instances] (4) ?x_161 : add_group ℕ := @monoid_algebra.add_group ?x_170 ?x_171 ?x_172
failed is_def_eq
[class_instances] (4) ?x_161 : add_group ℕ := @quotient_add_group.add_group ?x_173 ?x_174 ?x_175 ?x_176
failed is_def_eq
[class_instances] (4) ?x_161 : add_group ℕ := real.add_group
failed is_def_eq
[class_instances] (4) ?x_161 : add_group ℕ := @dfinsupp.add_group ?x_177 ?x_178 ?x_179
failed is_def_eq
[class_instances] (4) ?x_161 : add_group ℕ := @finsupp.add_group ?x_180 ?x_181 ?x_182
failed is_def_eq
[class_instances] (4) ?x_161 : add_group ℕ := ?x_185.add_group
failed is_def_eq
[class_instances] (4) ?x_161 : add_group ℕ := @matrix.add_group ?x_186 ?x_187 ?x_188 ?x_189 ?x_190 ?x_191
failed is_def_eq
[class_instances] (4) ?x_161 : add_group ℕ := @dmatrix.add_group ?x_192 ?x_193 ?x_194 ?x_195 ?x_196 ?x_197
failed is_def_eq
[class_instances] (4) ?x_161 : add_group ℕ := ?x_200.to_add_group
failed is_def_eq
[class_instances] (4) ?x_161 : add_group ℕ := @pi.add_group ?x_201 ?x_202 ?x_203
failed is_def_eq
[class_instances] (4) ?x_161 : add_group ℕ := rat.add_group
failed is_def_eq
[class_instances] (4) ?x_161 : add_group ℕ := @prod.add_group ?x_204 ?x_205 ?x_206 ?x_207
failed is_def_eq
[class_instances] (4) ?x_161 : add_group ℕ := @opposite.add_group ?x_208 ?x_209
failed is_def_eq
[class_instances] (4) ?x_161 : add_group ℕ := @additive.add_group ?x_210 ?x_211
failed is_def_eq
[class_instances] (4) ?x_161 : add_group ℕ := @add_units.add_group ?x_212 ?x_213
failed is_def_eq
[class_instances] (4) ?x_161 : add_group ℕ := @add_comm_group.to_add_group ?x_214 ?x_215
[class_instances] (5) ?x_215 : add_comm_group ℕ := real.angle.angle.add_comm_group
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @formal_multilinear_series.add_comm_group ?x_216 ?x_217 ?x_218 ?x_219 ?x_220 ?x_221 ?x_222 ?x_223
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @power_series.add_comm_group ?x_224 ?x_225
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @mv_power_series.add_comm_group ?x_226 ?x_227 ?x_228
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @continuous_multilinear_map.add_comm_group ?x_229 ?x_230 ?x_231 ?x_232 ?x_233 ?x_234 ?x_235 ?x_236 ?x_237 ?x_238 ?x_239
  ?x_240
  ?x_241
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @normed_group_hom.add_comm_group ?x_242 ?x_243 ?x_244 ?x_245
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @affine_map.add_comm_group ?x_246 ?x_247 ?x_248 ?x_249 ?x_250 ?x_251 ?x_252 ?x_253 ?x_254 ?x_255
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @module.dual.add_comm_group ?x_256 ?x_257 ?x_258 ?x_259 ?x_260
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @alternating_map.add_comm_group ?x_261 ?x_262 ?x_263 ?x_264 ?x_265 ?x_266 ?x_267 ?x_268 ?x_269 ?x_270
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @multilinear_map.add_comm_group ?x_271 ?x_272 ?x_273 ?x_274 ?x_275 ?x_276 ?x_277 ?x_278 ?x_279 ?x_280
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := punit.add_comm_group
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @continuous_linear_map.add_comm_group ?x_281 ?x_282 ?x_283 ?x_284 ?x_285 ?x_286 ?x_287 ?x_288 ?x_289 ?x_290 ?x_291
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @quotient_add_group.add_comm_group ?x_292 ?x_293 ?x_294
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := real.add_comm_group
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @restrict_scalars.add_comm_group ?x_295 ?x_296 ?x_297 ?x_298
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @tensor_product.add_comm_group ?x_299 ?x_300 ?x_301 ?x_302 ?x_303 ?x_304 ?x_305 ?x_306
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @submodule.quotient.add_comm_group ?x_307 ?x_308 ?x_309 ?x_310 ?x_311 ?x_312
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @linear_map.add_comm_group ?x_313 ?x_314 ?x_315 ?x_316 ?x_317 ?x_318 ?x_319 ?x_320
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @dfinsupp.add_comm_group ?x_321 ?x_322 ?x_323
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @finsupp.add_comm_group ?x_324 ?x_325 ?x_326
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := ?x_332.add_comm_group
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @matrix.add_comm_group ?x_333 ?x_334 ?x_335 ?x_336 ?x_337 ?x_338
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @dmatrix.add_comm_group ?x_339 ?x_340 ?x_341 ?x_342 ?x_343 ?x_344
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := ?x_347.to_add_comm_group
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @pi.add_comm_group ?x_348 ?x_349 ?x_350
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := fin.add_comm_group ?x_351
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := rat.add_comm_group
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @add_monoid_hom.add_comm_group ?x_352 ?x_353 ?x_354 ?x_355
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @prod.add_comm_group ?x_356 ?x_357 ?x_358 ?x_359
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @opposite.add_comm_group ?x_360 ?x_361
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @additive.add_comm_group ?x_362 ?x_363
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @add_units.add_comm_group ?x_364 ?x_365
failed is_def_eq
[class_instances] (5) ?x_215 : add_comm_group ℕ := @normed_group.to_add_comm_group ?x_366 ?x_367
[class_instances] (6) ?x_367 : normed_group ℕ := complex.normed_group
failed is_def_eq
[class_instances] (6) ?x_367 : normed_group ℕ := @continuous_multilinear_map.to_normed_group ?x_368 ?x_369 ?x_370 ?x_371 ?x_372 ?x_373 ?x_374 ?x_375 ?x_376 ?x_377 ?x_378
failed is_def_eq
[class_instances] (6) ?x_367 : normed_group ℕ := @continuous_linear_map.to_normed_group ?x_379 ?x_380 ?x_381 ?x_382 ?x_383 ?x_384 ?x_385 ?x_386
failed is_def_eq
[class_instances] (6) ?x_367 : normed_group ℕ := @normed_group_hom.to_normed_group ?x_387 ?x_388 ?x_389 ?x_390
failed is_def_eq
[class_instances] (6) ?x_367 : normed_group ℕ := @restrict_scalars.normed_group ?x_391 ?x_392 ?x_393 ?x_394
failed is_def_eq
[class_instances] (6) ?x_367 : normed_group ℕ := @pi.normed_group ?x_395 ?x_396 ?x_397 ?x_398
failed is_def_eq
[class_instances] (6) ?x_367 : normed_group ℕ := @prod.normed_group ?x_399 ?x_400 ?x_401 ?x_402
failed is_def_eq
[class_instances] (6) ?x_367 : normed_group ℕ := ?x_408.normed_group
failed is_def_eq
[class_instances] (6) ?x_367 : normed_group ℕ := ?x_411.normed_group
failed is_def_eq
[class_instances] (6) ?x_367 : normed_group ℕ := real.normed_group
failed is_def_eq
[class_instances] (6) ?x_367 : normed_group ℕ := @normed_linear_ordered_group.to_normed_group ?x_412 ?x_413
``` (Zulip max lines reached)

[Kevin Buzzard]

it's a much bigger story than that though

[Kevin Buzzard]

that's not the problem, it's just funny

[Eric Wieser]

docs#add_torsor.nonempty has the wrong priority

[Eric Wieser]

Or perhaps more scarily, it seems to be being ignored?

[Eric Wieser]

Let's see if #7563 makes things better or worse

[Kevin Buzzard]

@Oliver Nash @Eric Wieser The discussion here was my attempt to diagnose the timeouts, and it has led to Sebastien Gouezel's #7583. If you merge that into #6786 does it help?

[Oliver Nash]

Kevin Buzzard said:

Oliver Nash Eric Wieser The discussion here was my attempt to diagnose the timeouts, and it has led to Sebastien Gouezel's #7583. If you merge that into #6786 does it help?

Yes, it looks like it does. After mering branch#test_perfection, perfection_map.map_eq_map goes from a timeout in VS Code (not at command line, I guess different limit) to basically instant.

[Oliver Nash]

I could merge branch#test_perfection into #6786 but probably better to wait for #7583 to hit master and then merge from there.

[Oliver Nash]

Awesome work @Sebastien Gouezel

[Oliver Nash]

(and all concerned in fact)

[Oliver Nash]

#7583 hit master yesterday, so I merged master into #6786 and indeed it now builds successfully.

[Eric Wieser]

Great! I'll update my dependent branch that updates subring tomorrow and check that still works too!