Zulip Chat Archive

Stream: maths

Topic: char_zero


view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Mar 18 2021 at 17:47):

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

view this post on Zulip 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!

view this post on Zulip 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 gnhn=(gh)ng^nh^n=(gh)^n.

view this post on Zulip Eric Wieser (Mar 18 2021 at 18:04):

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

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Kenny Lau (Mar 23 2021 at 09:50):

#6800 might be related

view this post on Zulip Damiano Testa (Mar 23 2021 at 09:52):

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

view this post on Zulip Kenny Lau (Mar 23 2021 at 09:52):

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

view this post on Zulip Scott Morrison (Mar 23 2021 at 09:52):

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

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip Kenny Lau (Mar 23 2021 at 09:57):

try git fetch origin first

view this post on Zulip Kenny Lau (Mar 23 2021 at 09:58):

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

view this post on Zulip Damiano Testa (Mar 23 2021 at 09:59):

Kenny, thanks: The merging worked!

Now to see if it fixes the timeout!

view this post on Zulip Damiano Testa (Mar 23 2021 at 10:00):

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

view this post on Zulip 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)

view this post on Zulip Damiano Testa (Mar 23 2021 at 10:06):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 23 2021 at 13:14):

Do you have the latest version?

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip Damiano Testa (Mar 23 2021 at 13:15):

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

view this post on Zulip Kevin Buzzard (Mar 23 2021 at 13:15):

leanproject --version

view this post on Zulip Kevin Buzzard (Mar 23 2021 at 13:16):

leanproject --help tells you all the options

view this post on Zulip Damiano Testa (Mar 23 2021 at 13:16):

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

view this post on Zulip 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:~$

view this post on Zulip Damiano Testa (Mar 23 2021 at 13:17):

ok, I will try to upgrade, then

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Damiano Testa (Mar 23 2021 at 13:24):

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

view this post on Zulip Julian Berman (Mar 23 2021 at 13:28):

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

view this post on Zulip Riccardo Brasca (Mar 23 2021 at 13:28):

pipx upgrade mathlibtools works for me

view this post on Zulip 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

view this post on Zulip Damiano Testa (Mar 23 2021 at 13:30):

and now it learned rev!

view this post on Zulip 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.

view this post on Zulip 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 φ :=
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.)

view this post on Zulip Johan Commelin (Mar 23 2021 at 14:36):

Do you need to fill in the _inst_ns?

view this post on Zulip Johan Commelin (Mar 23 2021 at 14:37):

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

view this post on Zulip Johan Commelin (Mar 23 2021 at 14:37):

rg "_inst_" | wc -l
37

view this post on Zulip Kevin Buzzard (Mar 23 2021 at 14:38):

I think that we should try to keep the number there

view this post on Zulip Damiano Testa (Mar 23 2021 at 14:38):

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.

view this post on Zulip Damiano Testa (Mar 23 2021 at 14:39):

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

view this post on Zulip Gabriel Ebner (Mar 23 2021 at 14:39):

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

view this post on Zulip Gabriel Ebner (Mar 23 2021 at 14:40):

I count 14 explicit references.

view this post on Zulip Damiano Testa (Mar 23 2021 at 14:40):

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?

view this post on Zulip Johan Commelin (Mar 23 2021 at 14:42):

rg "\b_inst_" | wc -l
19

is maybe a more honest count

view this post on Zulip Damiano Testa (Mar 23 2021 at 14:42):

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]

view this post on Zulip Johan Commelin (Mar 23 2021 at 14:42):

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

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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!

view this post on Zulip Eric Wieser (Mar 23 2021 at 15:09):

Are there any underscores you can replace with type annotations?

view this post on Zulip Damiano Testa (Mar 23 2021 at 15:13):

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

view this post on Zulip Eric Wieser (Mar 23 2021 at 15:13):

I'd say it's preferred to using @

view this post on Zulip 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.

view this post on Zulip 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 φ :=

view this post on Zulip Eric Wieser (Mar 23 2021 at 15:16):

Wait, so that version doesn't time out?

view this post on Zulip Eric Wieser (Mar 23 2021 at 15:17):

Or do you mean, "which started timing out"

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Damiano Testa (Mar 23 2021 at 17:00):

The shorter version with a single @ works!

I am also trying to remove the merged PR.

view this post on Zulip 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!

view this post on Zulip Eric Wieser (May 10 2021 at 07:48):

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (May 10 2021 at 07:58):

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

view this post on Zulip Eric Wieser (May 10 2021 at 07:58):

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

view this post on Zulip Kevin Buzzard (May 10 2021 at 07:59):

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

view this post on Zulip Kevin Buzzard (May 10 2021 at 07:59):

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (May 10 2021 at 08:02):

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (May 10 2021 at 08:05):

Yeah, good find

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 10 2021 at 08:08):

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

view this post on Zulip Kevin Buzzard (May 10 2021 at 08:10):

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (May 10 2021 at 08:12):

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

view this post on Zulip 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.

view this post on Zulip Eric Wieser (May 10 2021 at 08:13):

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

view this post on Zulip Eric Wieser (May 10 2021 at 08:14):

It concedes that the longest step took 51ms

view this post on Zulip Kevin Buzzard (May 10 2021 at 08:15):

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

view this post on Zulip Kevin Buzzard (May 10 2021 at 08:15):

OK I really am going now.

view this post on Zulip 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
[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)

view this post on Zulip Kevin Buzzard (May 10 2021 at 08:19):

it's a much bigger story than that though

view this post on Zulip Kevin Buzzard (May 10 2021 at 08:20):

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

view this post on Zulip Eric Wieser (May 10 2021 at 08:22):

docs#add_torsor.nonempty has the wrong priority

view this post on Zulip Eric Wieser (May 10 2021 at 08:24):

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

view this post on Zulip Eric Wieser (May 10 2021 at 08:41):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Oliver Nash (May 11 2021 at 21:41):

Awesome work @Sebastien Gouezel

view this post on Zulip Oliver Nash (May 11 2021 at 21:41):

(and all concerned in fact)

view this post on Zulip Oliver Nash (May 13 2021 at 16:03):

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

view this post on Zulip 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