The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Jason,

 

> What happens if you copy rather than move (so you have both csdp and csdp.exe)?

 

that’s what I did J

 

I will just run this with ProcMon and see what is called how, I am sure this gives me some insight.

 

I do a lot of math proofs and psatz looks really promising. If it is half as good as it looks from the manual, I would include CSDP  into the Windows installer. The csdp binary is terribly big, but I would check if there hasn’t been done something suboptimal in linking. 27 MB (13 MB compressed) looks like they include a complete highly optimized BLAS and Lapack. I would think that for our purposes a BLAS/Lapack which is 10x smaller and 2x slower and can be installed by default serves us better. Maybe also a lot of stuff is linked in, which is not needed at all. I somehow can’t imagine that CSDP needs so much code.

 

Also in case CSDP really needs a lot of compute in practical cases, I would probably link BLAS and Lapack as DLL, so that if someone has MKL installed, he can profit from it.

 

But first I want to test it …

 

Best regards,

 

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928