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