!4#3051 AffineSpace.Combination

Stream: mathlib4

[Moritz Doll]

In !4#3051 I have encountered the problem that Lean 4 fails at a coercion because it can't determine the type of the object completely. To be more precise there is the definition affineCombination (Finset ι) (p : ι → P) : (ι → k) →ᵃ[k] P and the coercion to (ι → k) → P. Given a w : ι → k Lean 3 was able to infer k, but Lean 4 fails. I see two possible workarounds: (a) make k explicit in the definition and (b) annotate the type of affineCombination every time. What is the better way?

[Jireh Loreaux]

for reference, similar (albeit not identical) come up frequently for things like mk for various quotient types. Thus far I think we have just been adding type annotations, but I'm not necessarily arguing this is the right approach.

[Joseph Myers]

Affine combinations are also slow to elaborate in Lean 3 for unknown reasons, so it's conceivable this is related. https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Slowness.20of.20.60affine_combination.60

[Moritz Doll]

That is good to know. I would not be surprised if making k explicit in Lean 3 improves the performance. I can test that tomorrow evening (now + 1 day + 6 hours), if you have time for that earlier and feel free.

[Moritz Doll]

it looks like your workaround for the timeouts is exactly annotating the k

[Moritz Doll]

sbtw.affine_combination_of_mem_affine_span_pair currently: 4.39s and with the proposed change it's only 0.6s

[Moritz Doll]

i.e.,

lemma sbtw.affine_combination_of_mem_affine_span_pair [no_zero_divisors R]
  [no_zero_smul_divisors R V] {ι : Type*} {p : ι → P} (ha : affine_independent R p)
  {w w₁ w₂ : ι → R} {s : finset ι} (hw : ∑ i in s, w i = 1) (hw₁ : ∑ i in s, w₁ i = 1)
  (hw₂ : ∑ i in s, w₂ i = 1)
  (h : @finset.affine_combination R _ _ _ _ _ _ _ s p w ∈
    line[R, @finset.affine_combination R _ _ _ _ _ _ _ s p w₁,
      @finset.affine_combination R _ _ _ _ _ _ _ s p w₂]) {i : ι} (his : i ∈ s)
  (hs : sbtw R (w₁ i) (w i) (w₂ i)) :
  sbtw R (@finset.affine_combination R _ _ _ _ _ _ _ s p w₁)
    (@finset.affine_combination R _ _ _ _ _ _ _ s p w)
    (@finset.affine_combination R _ _ _ _ _ _ _ s p w₂) :=

[Moritz Doll]

nerdsniped myself: #18689

[Moritz Doll]

@Jeremy Tan please stop doing stuff in my PRs without asking first. We have a help wanted tag for a reason.

[Sebastien Gouezel]

To add some details: only the initial author of a PR should put the help wanted tag on a PR. If he hasn't done that, it means that he is still working on the PR and that other people shouldn't touch it.

[Eric Wieser]

Moritz Doll said:

We have a help wanted tag for a reason.

In fact the reason might be just "it's a default tag on github"! But indeed we seem to have co-opted it for a specific workflow; it would be great to update the description of the tag to reflect that, which right now is just "Extra attention is needed".

[Matthew Ballard]

It is also not hyphenated. ( :angry: :fist: :cloud:)

[Jeremy Tan]

Sebastien Gouezel said:

To add some details: only the initial author of a PR should put the help wanted tag on a PR. If he hasn't done that, it means that he is still working on the PR and that other people shouldn't touch it.

How can I be sure that the author is working on it?

[Matthew Ballard]

That's the author's responsibility.

[Jeremy Tan]

What if the author has abandoned it but forgot to place help-wanted?

[Eric Wieser]

Probably the thing to do is write a comment tagging them, asking what the status of the PR is, and whether it's fine to push changes

[Eric Wieser]

(and importantly, wait a day or two for them to respond)

[Matthew Ballard]

I do think there is room for a "feel free to push to this" tag that isn't help wanted

[Yaël Dillies]

I just changed the help-wanted description on mathlib to The author needs attention to resolve issues. What do you think?

[Matthew Ballard]

:love: -

[Yaël Dillies]

(and hyphenated it)

[Eric Wieser]

Some other options are:

• Push the change you want to make to another branch, and write a comment suggesting the author take a look at that branch for a proposed fix
• Push the change anyway, but leave a comment explaining that you did so, and that you're happy for it to be reverted (I did that today here)

This second option is a bit of a gamble, but is still better than pushing without letting the author know

[Yaël Dillies]

It happened a few time that Eric fixed something I was also fixing locally. In that case, I just keep whichever fix is best.

[Jeremy Tan]

I'm all groggy after going without sleep for the whole night just to watch MLB Opening Day

[Jeremy Tan]

All 15 games of that

[Kevin Buzzard]

Jeremy Tan said:

What if the author has abandoned it but forgot to place help-wanted?

"the author has abandoned it, forgot to tag it help-wanted, and it lies dormant for a bit" is much less of a problem than "the author has not abandoned it, goes to push more stuff and finds a load of conflicts because someone else has been messing with their work". So clearly the optimal approach is to err on the side of caution.

[Jon Eugster]

Jeremy Tan said:

How can I be sure that the author is working on it?

I thought the label please-adopt is one way for the author to say "I abandoned this PR, do whatever you want with it."

[Reid Barton]

It depends on the pace of the port. If the PR author disappears for two days (say) and the file is an important one for future files and there is no obstruction to porting it other than the author's absence, then it would be better even to discard the in progress PR and do it again, than to wait for the author to come back.

[Matthew Ballard]

This is assuming some attempt at contact has been made right?

[Eric Wieser]

goes to push more stuff and finds a load of conflicts because someone else has been messing with their work"

I think in this case a reasonable thing to do is

• Check if the upstream changes are obviously better than what you have locally; if so, keep them, discard your work.
• If they're not, and you don't want to deal with merging, just force push and let the other contributor know. The other person's work will be discarded from the PR, but they can recover it later (and resolve any conflicts) from the "force push" message on github. That way the conflict resolution is on the person who did the messing.

[Patrick Stevens]

I guess one of the most polite ways you can unilaterally build on someone's PR is to make a pull request into their branch (rather than into master), which is like offering assistance that they can easily refuse or trivially accept.

[Moritz Doll]

back to this PR: I am running into severe problems with everyones favorite lean4 issue. For testing I turned on etaExperiment file-wide, otherwise I run into problems everywhere. There have been very weird problems with simp, so if someone wants to have a look at the porting notes I would be happy.

[Eric Wieser]

I had a lot of problems with simp when porting the dependencies of this file

[Eric Wieser]

In general using simp [(map_vadd)] instead of simp [map_vadd] helped a lot

[Eric Wieser]

Sometimes the simp lemmas need you to explicitly specify one of the types (usually the out_param) in order for them to match

[Moritz Doll]

yes, the AffineSpace subfolder has been a big pain overall. I did not run into the map_vadd issue this time.