## Stream: maths

### Topic: char_zero

#### Damiano Testa (Mar 18 2021 at 17:26):

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 (Mar 18 2021 at 17:31):

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 (Mar 18 2021 at 17:33):

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 (Mar 18 2021 at 17:47):

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 (Mar 18 2021 at 17:47):

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

#### Damiano Testa (Mar 18 2021 at 18:00):

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 (Mar 18 2021 at 18:00):

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

#### Eric Wieser (Mar 18 2021 at 18:04):

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

#### Johan Commelin (Mar 18 2021 at 18:04):

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 (Mar 18 2021 at 18:05):

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

#### Damiano Testa (Mar 18 2021 at 19:04):

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 (Mar 19 2021 at 14:01):

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 (Mar 19 2021 at 14:05):

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 (Mar 23 2021 at 09:49):

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 (Mar 23 2021 at 09:50): #6800 might be related #### Damiano Testa (Mar 23 2021 at 09:52): So, the suggestion is simply that if I wait enough time, then the timeout disappears? #### Kenny Lau (Mar 23 2021 at 09:52): the suggestion is that after #6800 gets merged the timeout should disappear #### Scott Morrison (Mar 23 2021 at 09:52): You could just merge #6800 to your branch to find out! #### Damiano Testa (Mar 23 2021 at 09:53): 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 (Mar 23 2021 at 09:56): 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 (Mar 23 2021 at 09:57):

try git fetch origin first

#### Kenny Lau (Mar 23 2021 at 09:58):

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

#### Damiano Testa (Mar 23 2021 at 09:59):

Kenny, thanks: The merging worked!

Now to see if it fixes the timeout!

#### Damiano Testa (Mar 23 2021 at 10:00):

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

#### Ruben Van de Velde (Mar 23 2021 at 10:04):

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

#### Damiano Testa (Mar 23 2021 at 10:06):

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

#### Eric Wieser (Mar 23 2021 at 10:47):

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 (Mar 23 2021 at 13:14):

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 (Mar 23 2021 at 13:14): Do you have the latest version? #### Damiano Testa (Mar 23 2021 at 13:15): 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 (Mar 23 2021 at 13:15): which version of leanproject are you on? I've had no problems with --rev, I usually put --rev HEAD~1 or something. #### Damiano Testa (Mar 23 2021 at 13:15): Johan, how do I find out which version of leanproject do I have? #### Kevin Buzzard (Mar 23 2021 at 13:15): leanproject --version #### Kevin Buzzard (Mar 23 2021 at 13:16): leanproject --help tells you all the options #### Damiano Testa (Mar 23 2021 at 13:16): (adomani_weaken_chap_p)$ leanproject --version
leanproject, version 0.0.9

#### Kevin Buzzard (Mar 23 2021 at 13:16):

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 (Mar 23 2021 at 13:17):

ok, I will try to upgrade, then

#### Kevin Buzzard (Mar 23 2021 at 13:18):

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 (Mar 23 2021 at 13:24):

Is this what I should do?

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

#### Julian Berman (Mar 23 2021 at 13:28):

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

#### Riccardo Brasca (Mar 23 2021 at 13:28):

pipx upgrade mathlibtools works for me

#### Damiano Testa (Mar 23 2021 at 13:29):

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 (Mar 23 2021 at 13:30):

and now it learned rev!

#### Damiano Testa (Mar 23 2021 at 13:53):

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 (Mar 23 2021 at 14:35):

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 φ :=

#### Johan Commelin (Mar 23 2021 at 14:42):

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

#### Damiano Testa (Mar 23 2021 at 14:43):

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 (Mar 23 2021 at 14:43):

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 (Mar 23 2021 at 14:46):

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 (Mar 23 2021 at 14:47):

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

#### Eric Wieser (Mar 23 2021 at 15:09):

Are there any underscores you can replace with type annotations?

#### Damiano Testa (Mar 23 2021 at 15:13):

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

#### Eric Wieser (Mar 23 2021 at 15:13):

I'd say it's preferred to using @

#### Damiano Testa (Mar 23 2021 at 15:14):

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 (Mar 23 2021 at 15:15):

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 (Mar 23 2021 at 15:16):

Wait, so that version doesn't time out?

#### Eric Wieser (Mar 23 2021 at 15:17):

Or do you mean, "which started timing out"

#### Damiano Testa (Mar 23 2021 at 15:17):

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 (Mar 23 2021 at 15:17):

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

#### Damiano Testa (Mar 23 2021 at 15:18):

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

#### Damiano Testa (Mar 23 2021 at 15:18):

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 (Mar 23 2021 at 15:20):

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

#### Damiano Testa (Mar 23 2021 at 15:32):

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 (Mar 23 2021 at 15:55): 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 (Mar 23 2021 at 17:00): The shorter version with a single @ works! I am also trying to remove the merged PR. #### Damiano Testa (Mar 23 2021 at 18:35): 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 (May 10 2021 at 07:48): I'm getting a timeout in docs#perfection_map.map_eq_map again in #6786. #### Kevin Buzzard (May 10 2021 at 07:57): 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 (May 10 2021 at 07:58): Have you configured vs-code with a different timeout to CI? #### Eric Wieser (May 10 2021 at 07:58): (or are you on a diffferent commit / cache?) #### Kevin Buzzard (May 10 2021 at 07:59): almost certainly, because I don't normally think about this sort of thing #### Kevin Buzzard (May 10 2021 at 07:59): I'm just saying "stuff in this file is surprisingly slow, here's another example" #### Kevin Buzzard (May 10 2021 at 08:01): 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 (May 10 2021 at 08:02):

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

#### Kevin Buzzard (May 10 2021 at 08:05):

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

Yeah, good find

#### Eric Wieser (May 10 2021 at 08:06):

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 (May 10 2021 at 08:08):

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

#### Kevin Buzzard (May 10 2021 at 08:10):

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

#### Kevin Buzzard (May 10 2021 at 08:11):

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 (May 10 2021 at 08:12):

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

#### Kevin Buzzard (May 10 2021 at 08:13):

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 (May 10 2021 at 08:13):

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

#### Eric Wieser (May 10 2021 at 08:14):

It concedes that the longest step took 51ms

#### Kevin Buzzard (May 10 2021 at 08:15):

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

#### Kevin Buzzard (May 10 2021 at 08:15):

OK I really am going now.

#### Kevin Buzzard (May 10 2021 at 08:19):

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
failed is_def_eq
failed is_def_eq
failed is_def_eq
failed is_def_eq
failed is_def_eq
failed is_def_eq
failed is_def_eq
failed is_def_eq
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
failed is_def_eq
failed is_def_eq
failed is_def_eq
failed is_def_eq
failed is_def_eq
failed is_def_eq
failed is_def_eq
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
failed is_def_eq
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
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
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
failed is_def_eq
failed is_def_eq
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
failed is_def_eq
failed is_def_eq
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
failed is_def_eq
failed is_def_eq
failed is_def_eq
failed is_def_eq
failed is_def_eq
failed is_def_eq
failed is_def_eq
failed is_def_eq
failed is_def_eq
[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 (May 10 2021 at 08:19):

it's a much bigger story than that though

#### Kevin Buzzard (May 10 2021 at 08:20):

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

#### Eric Wieser (May 10 2021 at 08:24):

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

#### Eric Wieser (May 10 2021 at 08:41):

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

#### Kevin Buzzard (May 11 2021 at 20:54):

@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 (May 11 2021 at 21:38):

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 (May 11 2021 at 21:41):

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 (May 11 2021 at 21:41):

Awesome work @Sebastien Gouezel

#### Oliver Nash (May 11 2021 at 21:41):

(and all concerned in fact)

#### Oliver Nash (May 13 2021 at 16:03):

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

#### Eric Wieser (May 13 2021 at 20:05):

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

Last updated: May 18 2021 at 08:14 UTC