Bug#511899: ITP: coinor-csdp -- A software package for semidefinite programming
Hi
This ITP is a nice idea. In my research group, we're now using csdp
as an external oracle when solving inequalities in the Coq proof assistant
(see [1], or more specifically [2] for the use of csdp in Coq). This
coinor-cdsp package could simplify things quite a bit for us, by becoming
a "recommends" or "suggests" or whatever for package coq. Anyway, if you need
early testers, or even help during the creation of this package, let me know...
Best regards,
Pierre Letouzey (Coq development team)
letouzey AT pps.jussieu.fr
[1]: http://packages.debian.org/coq
[2]: http://www.irisa.fr/lande/fbesson/Fast_Reflexive_Arithmetics_Tactics.pdf
Reply to: