Zulip Chat Archive

Stream: general

Topic: Splitting file#analysis/calculus/deriv

Yury G. Kudryashov (May 26 2023 at 23:14):

Hi, I'm splitting file#analysis/calculus/deriv into smaller chunks in branch#YK-split-deriv. For the next 10-14h I won't be able to work on it (in flight, then driving, then sleeping). If someone wants to help, it would be awesome.

Yury G. Kudryashov (May 26 2023 at 23:26):

Remaining tasks:

  • [ ] Add module docstrings. IMHO, we can either copy parts of the old module docstring, move section docs to top-level module docs, or write short docs (see fderiv)
  • [ ] Add copyright headers. Ideally, we should git blame parts of the original file that went to each specific file. Or just copy the header from the original file to all new files.
  • [ ] Fix remaining compile issues (if any). Pre-last revision I pushed had a timeout in a seemingly unrelated file.

Yury G. Kudryashov (May 26 2023 at 23:27):

I already fixed all compile errors (due to missing imports) in analysis/

Eric Wieser (May 27 2023 at 13:22):

@Jeremy Tan FYI

Jeremy Tan (May 27 2023 at 13:51):

I'll try and fix the build

Yury G. Kudryashov (May 27 2023 at 15:05):

Added module docs for add.lean, working on compl.lean

Yury G. Kudryashov (May 27 2023 at 15:09):

What name should I add to authors for github user negiizhao?

Yury G. Kudryashov (May 27 2023 at 15:09):

Probably, @Yuyang Zhao

Yury G. Kudryashov (May 27 2023 at 15:43):

Added some module docs and copyright headers. I'm going to take a break for ~1h. Remaining files: mul, polynomial, pow, prod, slope, support, and zpow.

Yury G. Kudryashov (May 27 2023 at 17:26):

Done, ready for review.

Jeremy Tan (May 28 2023 at 05:49):

In order to minimise merge conflict headaches with the port of the Deriv files I suggest that !4#4435 (Add) and !4#4440 (Mul) be reviewed and merged first

Yury G. Kudryashov (May 28 2023 at 06:21):

@Chris Hughes already pushed most of them to the queue. I'll consider these as delegated and deal with conflicts.

Eric Wieser (May 28 2023 at 21:32):

I had a pretty surprising issue updating a downstream project after this split; because I forgot to import analysis.calculus.deriv.mul, hf.mul hg was referring to docs#asymptotics.is_o.mul instead of docs#has_deriv_at.mul.

Eric Wieser (May 28 2023 at 21:32):

Having import change the meaning of dot notation feels like pretty undesirable behavior.

Eric Wieser (May 28 2023 at 21:33):

(I don't blame the split here, but it would be nice if somehow I could have got better diagnostics)

Yury G. Kudryashov (May 28 2023 at 23:20):

Do you have any suggestions?

Last updated: Dec 20 2023 at 11:08 UTC