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)
CC @Yves Bertot
For (2) it is here: https://github.com/Sobernard/Lindemann
We should probably ask Sophie Bernard if we can move it to math-comp and takeover the maintenance.
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)
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: Feb 09 2023 at 01:03 UTC