Stream: math-comp devs

Topic: MathComp code on gforge


view this post on Zulip Karl Palmskog (Nov 06 2020 at 14:14):

I see that there is still some MathComp-related code hosted on gforge here that will disappear end of December: http://marelledocsgit.gforge.inria.fr

Specifically, (1) differential dynamic logic and (2) Proof of transcendence for e and pi. The latter looks quite useful and I have not seen it anywhere else. Is there a plan to preserve this stuff somewhere? May I ask that you bring this up on the next MathComp meeting @Enrico Tassi @Cyril Cohen (unless the code has already been moved somewhere and I've missed it)

view this post on Zulip Enrico Tassi (Nov 06 2020 at 14:15):

CC @Yves Bertot

view this post on Zulip Cyril Cohen (Nov 06 2020 at 14:56):

For (2) it is here: https://github.com/Sobernard/Lindemann

view this post on Zulip Cyril Cohen (Nov 06 2020 at 14:57):

We should probably ask Sophie Bernard if we can move it to math-comp and takeover the maintenance.

view this post on Zulip Yves Bertot (Nov 09 2020 at 08:16):

I will discuss the move with Sophie the next time I have her on the phone (less than 2 weeks).
Concerning the specific proofs of transcendence for e and pi, we probably still should preserve them as is, for historical access. I have not checked before writing this short answer, but the sources are probably mentioned in the 2016 CPP paper about it (https://arxiv.org/abs/1512.02791)

view this post on Zulip Karl Palmskog (Nov 09 2020 at 08:33):

can confirm the source link is mentioned in the CPP paper, so makes sense to store original sources referenced in the paper somewhere, e.g., as an attachment to a tag in Sophie's repo


Last updated: Aug 11 2022 at 01:03 UTC