Add new plugin for polynomial inequalities (using OSDP)

[ploc]

The purpose of this PR is to add a new plugin based on semi-definite programming (SDP, aka convex optimization). It solves problems involving polynomial inequalities which cannot be solved with alt-ergo today. It relies on the opam package OSDP which provides the interface to SDP solvers.

It is developed as a plugin, following the structure of fm-simplex plugin.

Usage: alt-ergo --polynomial-plugin osdp-plugin.cmxs file.ae

Details

• The proposed PR builds a new package alt-ergo-osdp and does not rely on any new package except osdp which is currently being updated (cf https://github.com/ocaml/opam-repository/pull/20711 )
• Nothing change for alt-ergo if one does not build and install that new package alt-ergo-osdp, and if one does not use the new option --polynomial-plugin

With @proux01, we commit to maintain the package alt-ergo-osdp and keep it in sync with alt-ergo, as well as OSDP.

Last, there is an issue with the loading order of modules for plugins. We solved this for our inequalities plugin, and will prepare a separate PR for fm-simplex which has the same issue (it is not currently properly loaded).

[proux01]

The commit message contains the reference of the related publication and an example of goal that is now solved by Alt-Ergo. Should it be added to some non regression test?

Also note that this does not add any dependency to the currently existing opam packages for alt-ergo. Only the new alt-ergo-osdp packages depends on osdp (which has a non trivial depext).

[ploc]

Updated opam osdp dependency to 1.1.0 which has been released (cf https://github.com/ocaml/opam-repository/commit/c353c5adfd87a691bec635f4e880a29e470c3214)

[Gbury]

That's very impressive ! We'll try and review as soon as possible, ^^

[ploc]

Issues in CI workflows were caused by the recent release of Cmdliner (1.1.0). I don't know why it doesn't show up in the CI of the "next" branch. I added the explicit version to Cmdliner 1.0.4 in the dune-project and .opam files (see https://github.com/ploc/alt-ergo/commit/76cf4dc5f30d57fe3b0c20463c1a341d7751cb7d).

[Gbury]

Issues in CI workflows were caused by the recent release of Cmdliner (1.1.0). I don't know why it doesn't show up in the CI of the "next" branch. I added the explicit version to Cmdliner 1.0.4 in the dune-project and .opam files (see ploc@76cf4dc).

It doesn't show up in the Ci runs of next probably because the last run was before the release of cmdliner.1.1.0, ^^

[ploc]

Impact is significant ! Most uses of Cmdliner in Alt-ergo rely on the deprecated Term module. It causes many warning and one error in the last line of the module.

[Gbury]

Indeed, I'll try and fix that in next asap.

[Gbury]

The next branch has been fixed (with regards to the cmdliner changes, as well as other minor build-related fixes), so you should be able to rebase your branch on top of it and everything should work, ^^

[proux01]

@ploc could you remove the last commit?

git reset --hard HEAD^
git push --force-with-lease

[proux01]

(feel free to add Co-authored-by: Pierre-Loïc Garoche <[email protected]> at the end of the description of the commit)

[ploc]

Hi @Gbury , what's the status? Do you need us to do anything?

[Gbury]

my apologies, I've been busy with another project recently. I'll try and look at this PR in detail (including the thing about plugins) next week.

[proux01]

@Gbury it seems we'll both attend JFLA in a few weeks. If you want, we could take some time there to look together at the code (and I could take the opportunity to improve comments as the code may sometimes be a bit dry). If you want a good outlook of the underlying maths, you can have a look to the related paper https://hal.archives-ouvertes.fr/hal-01737737/document (you can skip section 4.3 which is dropped in this PR). That might look like a bunch of non trivial maths, but in fact the subset needed to be convinced of the soundness is relatively basic.

[ploc]

Any news since JFLA ? I am still interested in the merge!

[Gbury]

We talked a bit with @proux01 during the JFLA. There are a few things left to do before we can merge:

• there are a few comments to add (e.g. a short description of the goals of the new plugins, and a link to the relevant research papers) and some doc comments for the new functions.
• there should be at least a few non-regression tests to check that the plugin works as expected
• a CLA needs to be signed: there should have been an email sent with the adequate CLA a while back, but we can probably resend it if you need to (cc @MuSSF )
• I'll have to look a bit at what is installed by the new plugin and where, and there might require some changes, but it should be fairly minor

[proux01]

Sorry, I'm ridiculously late here. I hope to complete my tasks in the coming weeks.

[proux01]

So finally, here it is: https://github.com/proux01/alt-ergo/tree/osdp

@Gbury said:

there are a few comments to add (e.g. a short description of the goals of the new plugins, and a link to the relevant research papers) and some doc comments for the new functions.

done

there should be at least a few non-regression tests to check that the plugin works as expected

done

a CLA needs to be signed: there should have been an email sent with the adequate CLA a while back, but we can probably resend it if you need to (cc @ MuSSF )

Sorry, don't remember that but feel free to resend it, I'll have a look.

P.S.: @ploc can't push on your branch, you probably have to do something like:

git remote add proux01 https://github.com/proux01/alt-ergo  # likely already done
git fetch proux01
git checkout osdp
git reset --hard proux01/osdp
git push --force-with-lease