Add csdp to the Coq Platform

[palmskog]

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.

[MSoegtropIMC]

@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.

[palmskog]

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.

[MSoegtropIMC]

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.

[erikmd]

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)

[erikmd]

Also, see the conf-csdp opam package (which is one of the dependencies of osdp)

[MSoegtropIMC]

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.

[proux01]

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.

[MSoegtropIMC]

I postponed this package inclusion to the next release which will likely happen in November (for Coq 8.14)

[palmskog]

As per discussion on Zulip, inclusion of csdp in the platform has been postponed further, possibly indefinitely.

[MSoegtropIMC]

@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.).

[palmskog]

I agree about coq-hammer, this was mainly just to inform that people can't start to rely on csdp in 2021.11.

[MSoegtropIMC]

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.

[palmskog]

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).

[MSoegtropIMC]

Indeed Validsdp is more what I am interested in. I have a lot of issues with LP solvers producing garbage results.

[MSoegtropIMC]

Triage note: this is still complicated to support on all platforms - help welcome!

[proux01]

A student advised by @erikmd recently added a csdp package to the OCaml OPAM repo. This works on various Linux and mac distribs but still requires testing/adaptation for Windows: https://github.com/ocaml/opam-repository/pull/25721

[MSoegtropIMC]

@proux01 : thanks for the note - i will look into it again.

[erikmd]

Yes @MSoegtropIMC: for the record, the approach followed by my student was exactly your initial suggestion:

the easiest path might be to create an opam "from sources" package for csdp

→ https://opam.ocaml.org/packages/csdp/

The CI logs are not available anymore, but as far as I can tell, all Linux distributions tested in opam CI (except oraclelinux) were fine (e.g., debian + ubuntu + fedora + centos + opensuse + arch) as well as freebsd + macos-homebrew. Even if csdp was already packaged in just a few distros of these.

But testing/adapting the package for windows-cygwin is still missing.

[MSoegtropIMC]

@erikmd : thanks! I had a quick look at the opam package - it looks doable on cygwin.

Is there a good reason for using sed instead of patch, say many lines matching each sed patch?

[proux01]

Not real reason, it was easy to use sed, but if patch is preferable for any reason, we can certainly change.

[erikmd]

The various sed lines just aim to:

• fix an upstream bug by adding a missing line in the sources (can be easily replaced with a patch)
• ensure the Makefile is properly configured for various os and distributions (the required Makefile tweaks might be doable with patch, but much more tricky I guess, as there are multiple cases…)

[MSoegtropIMC]

In general patch is more maintainable than sed, because patch tells when things changed so much that the patch does not apply any more. It is substantially more effort to maintain sed patches over time.

IMHO the only good reason for using sed instead of patch is if one does identical changes to many files.

[erikmd]

Yes I am aware of this feature of patch.

But again, I am not sure it is adapted for the second kind of substitution I was talking about:

• ensure the Makefile is properly configured for various os and distributions (the required Makefile tweaks might be doable with patch, but much more tricky I guess, as there are multiple cases…)

because it is conditional patching, i.e., only for some os / distributions (which does not seem to be possible with opam)

and the hypothesis whether "the [sed] does not apply any more" is very unlikely, because csdp development seems to have stalled, so the current version is the reference one AFAICT

(Also note that the opam maintainers did not raise an issue with the proposed package.)

[proux01]

The OPAM build rule currently calls sed, it could as well call patch (with the same conditions)

[erikmd]

OK! I better understand your idea.

@MSoegtropIMC is it "required" from your viewpoint to do this "refactoring"?

AFAIAC I won't have the time to do this in the upcoming weeks.

[MSoegtropIMC]

Indeed the idea is to have 4 patch files - one for each OS. This is for sure more readable and more error resilient.

As a compromise let's say it shall be changed in case there ever is a new version.

As Coq Platform maintainer I am having my share of updating other peoples opam packages, so I guess I am more picky about the maintainability of opam packages than others.

[MSoegtropIMC]

Maybe I change it in case I need to change something for cygwin.