Bug#511899: ITP: coinor-csdp -- A software package for semidefinite programming
Quoting Soeren Sonnenburg so...@debian.org: Sure, but you should carefully check whether licenses (coinor uses CLP) are compatible and maybe askt on the coinor mailinglist if they can give an exception in case there is a problem... Soeren Well, I'm clearly no license-expert, so feel free to prove me wrong, but I don't think we have a license issue here: currently coq and csdp form two separate and autonomous processes. Simply, coq may submit a problem to csdp (by mean of a pipe or whatever) and digest the output of csdp about this particular problem. In addition, coq is clearly usable even without csdp being installed on the system: in this case, the proof method that uses cdsp as oracle will not be available, but coq provides many other proof methods (they may be slower and/or more painful, but they work). Best, Pierre -- To UNSUBSCRIBE, email to debian-bugs-dist-requ...@lists.debian.org with a subject of unsubscribe. Trouble? Contact listmas...@lists.debian.org
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 -- To UNSUBSCRIBE, email to debian-bugs-dist-requ...@lists.debian.org with a subject of unsubscribe. Trouble? Contact listmas...@lists.debian.org
Bug#511899: ITP: coinor-csdp -- A software package for semidefinite programming
On Fri, 2009-02-20 at 15:43 +0100, whoami...@free.fr wrote: 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 Sure, but you should carefully check whether licenses (coinor uses CLP) are compatible and maybe askt on the coinor mailinglist if they can give an exception in case there is a problem... Soeren signature.asc Description: This is a digitally signed message part
Bug#511899: ITP: coinor-csdp -- A software package for semidefinite programming
Package: wnpp Severity: wishlist Owner: Soeren Sonnenburg so...@debian.org * Package name: coinor-csdp Version : 6.0.1 Upstream Author : Brian Borchers borch...@nmt.edu * URL : https://projects.coin-or.org/Csdp * License : CPL Programming Lang: C Description : A software package for semidefinite programming CSDP is a library of routines that implements a predictor corrector variant of the semidefinite programming algorithm of Helmberg, Rendl, Vanderbei, and Wolkowicz. The code runs in parallel on shared memory multi-processor systems, and it makes effective use of sparsity in the constraint matrices. . CSDP is part of the larger COIN-OR initiative (Computational Infrastructure for Operations Research). . This package contains the binaries and libraries. -- System Information: Debian Release: 5.0 APT prefers testing APT policy: (500, 'testing') Architecture: i386 (i686) -- To UNSUBSCRIBE, email to debian-bugs-dist-requ...@lists.debian.org with a subject of unsubscribe. Trouble? Contact listmas...@lists.debian.org
