Stream: math-comp analysis

Topic: Holomorphy math-comp/analysis#204


view this post on Zulip Marie Kerjean (May 14 2020 at 11:25):

Has this PR been ported with respect to the commit porting closeness to Hausdorff spaces ? ?

view this post on Zulip Marie Kerjean (May 14 2020 at 11:26):

By the way, I'm renaming it holomorphy instead of cauchyetoile, if that's ok.

view this post on Zulip Marie Kerjean (May 14 2020 at 11:28):

I would like to commit the tentative description of derivability wrt R using within, if that's ok with you @Cyril Cohen @affeldt-aist ?

view this post on Zulip Reynald Affeldt (May 14 2020 at 11:38):

Yes, it has been rebased on top of the branch that brings the close predicate to Hausdorff space but the latter has since been merged into master.

view this post on Zulip Reynald Affeldt (May 14 2020 at 12:02):

I just did a rebase of PR 192 on top of master (with a small update).

view this post on Zulip Marie Kerjean (May 14 2020 at 12:40):

Which fork/branch of real-closed should this PR depends on ? I have my fork of @Kazuhiko Sakaguchi own fork, where I have deleted the canonical R-vector space structure on C , but this has been implemented elsewhere maybe ?

view this post on Zulip Cyril Cohen (May 14 2020 at 14:11):

@mkerjean I was waiting for your opinion before merging math-comp/real-closed#23

view this post on Zulip Cyril Cohen (May 14 2020 at 14:12):

Then I will release and you/we can use a released version in math-comp/analysis

view this post on Zulip Reynald Affeldt (May 14 2020 at 14:15):

(CI fails for PR#204, even though it compiles on my computer and PR#192 was fine)

view this post on Zulip Marie Kerjean (May 14 2020 at 14:21):

I'm sorry I missed this PR (if I don't answer within 2 days you can ping me again). I think it's enough, but I'll be able to test it tomorrow if you can wait.

view this post on Zulip Marie Kerjean (May 15 2020 at 13:28):

I'm pushing something partial as I need to stop now. Will finish tonight.

view this post on Zulip Marie Kerjean (May 15 2020 at 23:21):

The CI seems to fail because of an issue regarding the complex file, what should I do ?

view this post on Zulip Cyril Cohen (May 16 2020 at 00:56):

you should substitute "cauchy_etoile" for "holomorphy" in default.nix

view this post on Zulip Reynald Affeldt (May 21 2020 at 14:01):

I can't find any occurrence of both strings in default.nix.

view this post on Zulip Cyril Cohen (May 21 2020 at 15:43):

Hummm, right!

view this post on Zulip Cyril Cohen (May 21 2020 at 16:07):

I will fix this ASAP

view this post on Zulip Marie Kerjean (May 22 2020 at 18:11):

affeldt-aist said:

I can't find any occurrence of both strings in default.nix.

Thanks :)

view this post on Zulip Marie Kerjean (May 23 2020 at 18:40):

Cyril Cohen said:

mkerjean I was waiting for your opinion before merging math-comp/real-closed#23

I've been using a version of this PR without the Canonical on line 121.


Last updated: Aug 11 2022 at 01:03 UTC