coq
Add csdp to the Coq Platform
The psatz tactic uses the external tool csdp.
To make it convenient for users of any platform to call psatz, I propose that csdp is included in the Coq Platform. Debian and Ubuntu users can already install it as the package coinor-csdp.
@palmskog : there is a homebrew package for csdp, but neither a macports nor a cygwin package. So the easiest path might be to create an opam "from sources" package for csdp, but as far as I know coinor, this might get a bit involved. Is there someone who might be able to help with this?
In general I have some interest in a reasonable install method for coinor, since I also sometimes want it for other things, but I am not sure I have time for this.
I am not in favor of including it if we can't support it on half of the Macs and on Windows. Also I am not sure about the other Linux distros.
Unfortunately I don't know anyone with the right expertise who could help out with packaging this. Could we maybe add some kind of "help wanted" tag here to the issue and postpone inclusion until we find more help? This is not a critical package for me, but several people have wondered about using psatz more easily.
Yes - we have a help wanted label.
As I said eventually I will likely do it if no one else does it, just because for many LP problems one needs a second or third opinion (see e.g. https://gist.github.com/MSoegtropIMC/2d4fdfe6b1e3e3955c63084523db3ca7) or a formally verified solver ... But it might take a while.
I Cc @proux01 in case he'd have some experience running csdp on Windows…
(as our ValidSDP library relies on his osdp libary which is packaged in opam and provides a unified OCaml interface for several SDP solvers, including but not limited to csdp)
The opam package has just:
depexts: [
["coinor-csdp"] {os-family = "debian"}
["csdp"] {os-distribution = "centos"}
]
which is quite a bit below the range of platforms we support and at least on Windows and MacPorts it won't be just adding depext lines.
Indeed, the conf-csdp package only checks that csdp is installed but doesn't actually package it (which is not trivial since its C code depends on blas/lapack and fortran). And indeed, the depext packages availability seems rather limited.
I postponed this package inclusion to the next release which will likely happen in November (for Coq 8.14)
As per discussion on Zulip, inclusion of csdp in the platform has been postponed further, possibly indefinitely.
@palmskog : as I said eventually I will likely do it, but right now there are too many things which give a higher benefit for less work (coq-hammer e.g.).
I agree about coq-hammer, this was mainly just to inform that people can't start to rely on csdp in 2021.11.
Do you see a big benefit in it? I tried it a few times and it usually didn't do what I want, so I tend to use either lra or coq-interval or a combination of both. This works well in automation, because it is pretty clear what goals both can solve and what not. Is there some space between the two I didn't happen to run into as yet?
My interest in CSDP is more in CSDP itself, so psatz would be a side effect.
One of the main benefits of CSDP is that we could potentially add Validsdp to the platform once we have it (assuming @proux01 and @erikmd are interested in this).
Indeed Validsdp is more what I am interested in. I have a lot of issues with LP solvers producing garbage results.