Stream: math-comp analysis

Topic: math-comp/analysis#187


view this post on Zulip Cyril Cohen (May 07 2020 at 22:06):

@affeldt-aist do you mind if I squash both our commits and put myself as co-authored-by, it makes no sense to keep the history... single commits are not compiling anymore anyway.

view this post on Zulip Reynald Affeldt (May 07 2020 at 22:08):

please, go ahead

view this post on Zulip Cyril Cohen (May 08 2020 at 16:19):

are you still working on this PR ?

view this post on Zulip Reynald Affeldt (May 08 2020 at 16:22):

well, I did promise to do my homework by monday, true that I didn't have much time since yesterday :-(

view this post on Zulip Cyril Cohen (May 08 2020 at 16:23):

May I ask what you are doing on it so that we do not collide?

view this post on Zulip Reynald Affeldt (May 08 2020 at 16:25):

(I think I did push something yesterday evening...)

view this post on Zulip Reynald Affeldt (May 08 2020 at 16:26):

ah!

view this post on Zulip Reynald Affeldt (May 08 2020 at 16:27):

we lost one commit!

view this post on Zulip Cyril Cohen (May 08 2020 at 16:27):

oooh

view this post on Zulip Cyril Cohen (May 08 2020 at 16:27):

sorry....

view this post on Zulip Cyril Cohen (May 08 2020 at 16:28):

do you know the commit number ?

view this post on Zulip Reynald Affeldt (May 08 2020 at 16:31):

I still had my emacs buffer

view this post on Zulip Reynald Affeldt (May 08 2020 at 16:32):

I was about to tackle near_non(de|in)creasing_is_cvg to be precise.

view this post on Zulip Cyril Cohen (May 08 2020 at 16:33):

ok, thanks, I will do a fixup with it

view this post on Zulip Reynald Affeldt (May 08 2020 at 16:35):

Then I was planning to fix cesaroand produce a few lemmas dual of already existing lemmas

view this post on Zulip Reynald Affeldt (May 08 2020 at 16:36):

and use this experience to feed the contributing guide

view this post on Zulip Cyril Cohen (May 08 2020 at 16:40):

ok!

view this post on Zulip Reynald Affeldt (May 08 2020 at 16:40):

sorry, I pushed in a hurry and the CI didn't go through, let me fix this

view this post on Zulip Cyril Cohen (May 08 2020 at 16:41):

I will merge math-comp/analysis#202 and rebase sequences on it

view this post on Zulip Cyril Cohen (May 08 2020 at 16:41):

affeldt-aist said:

sorry, I pushed in a hurry and the CI didn't go through, let me fix this

I noticed already and it is almost fixed

view this post on Zulip Reynald Affeldt (May 08 2020 at 16:44):

ok, I let you do that (strangely it was compiling in emacs, something changed under my feet)

view this post on Zulip Cyril Cohen (May 08 2020 at 16:44):

yes, I accidentally removed image_inj

view this post on Zulip Cyril Cohen (May 08 2020 at 16:45):

(+ bounded changed a few other things under your feet)

view this post on Zulip Cyril Cohen (May 08 2020 at 16:45):

I hope I did not loose more

view this post on Zulip Cyril Cohen (May 08 2020 at 16:45):

could you give me the commit number ?

view this post on Zulip Cyril Cohen (May 08 2020 at 16:45):

git rev-parse HEAD

view this post on Zulip Reynald Affeldt (May 08 2020 at 16:46):

d46f2364841b3cd0ceb85fee76d37a62a3f50a9d (yesterday's commit that disappeared)

view this post on Zulip Cyril Cohen (May 08 2020 at 16:51):

a last rebase and I give it back


Last updated: Aug 19 2022 at 20:03 UTC