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 -- To UNSUBSCRIBE, email to debian-wnpp-requ...@lists.debian.org with a subject of "unsubscribe". Trouble? Contact listmas...@lists.debian.org
