help-wanted label

Stream: mathlib4

[Joachim Breitner]

I’m tempted to help out with help-wanted PRs (nice mix of tedious work done and mild but doable challenges left, at least so far). It would be great if a PR tagged with help-wanted would indicate in the description or a comment where things are stuck, if that’s not too much hassle.

[Johan Commelin]

I think occasionaly the tag is also used in the form of "things are going pretty smoothly, but I'm off to bed, feel free to take over"

[Joachim Breitner]

Right – but even then a small note helps others to assess whether they are up to a particular file.

[Johan Commelin]

Also, many files have a thread on this stream. So people might have discussed the problem there.
But I still agree with you: a little pointer on the PR page doesn't hurt.

[Joachim Breitner]

Right. It’s a friendly suggestion, not a request :-)
(What else do you do after switching branches and waiting for lean to re-build everything…)

[Johan Commelin]

Run lake exe cache get?

[Reid Barton]

The CI results can also show what's wrong (at least the first thing that is wrong)

[Joachim Breitner]

TIP about cache get. Must have missed it when reading the wiki. We’ll see how well

Attempting to download 1042 file(s)

works on the DB Wifi :-D … it does :-)

[Joachim Breitner]

Does it support downloading only the dependencies of a specific file?

[Reid Barton]

I think that's why you are getting 1042 file(s) and not a single tarball

[Joachim Breitner]

Perfekt