Bug#511899: ITP: coinor-csdp -- A software package for semidefinite programming
Quoting Soeren Sonnenburg <sonne@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
Reply to: