Properly defined platform for our native binaries

[PhilippWendler]

Currently it is not properly defined which versions of standard libraries we assume for the native binaries we ship, i.e., on which distributions in which versions these binaries are usable. This is bad for users and for developers.

We should decide on a set of libraries and versions that we allow as dependencies. The Python community has a similar problem for Python libraries with bundled native binaries, and has established the manylinux2010 platform. Binaries built for this platform are expected to run on almost all current Linux distributions. Thus I suggest we adopt this platform and the set of libraries and versions it defines.

After this is decided, we should create a proper way to build our binaries automatically that ensures this compatibility, e.g., by a scripts using the official manylinux2010 Docker image or a VM (would also fix #74).

[kfriedberger]

We might aim towards using Ubuntu 18.04 as a basic platform for building and executing our solvers. Some users currently have Ubuntu 16.04 that has LTS until 2021. This version could also be chosen as a basic system. With the upcoming change towards Java 11 older systems (including even Ubuntu 16.04) might also get out-of-scope.

Additionally, we might want to remove any code that was especially added for older platforms.
For example, our MathSAT5 library seems to be build for and run on Ubuntu 10.04.
I do not expect someone to use such an old system any longer.

[PhilippWendler]

I would not require something as new as Ubuntu 18.04. Java 11 is easily installable on Ubuntu 16.04 with a PPA. Users will want to use JavaSMT on StarExec, which is probably even older, and this platform is an important use case.

And what benefit would we have of requiring something newer?
If we have a properly defined platform (which we need anyway) than we need to build it using that platform, and it does not produce more effort if that platform is older or newer.

So why not use something like manylinux (currently available as manylinux2014)?

[kfriedberger]

Currently, we use Docker images based on Ubuntu 18.04 or 22.04 for building the binary libraries. The platform supported by all SMT solvers is Ubuntu 22.04 (or newer). There are some solvers that still support Ubuntu 18.04 (like MathSAT or Boolector). Several SMT solvers do not offer binaries for older systems or even corresponding build scripts, and e.g. require tools like cmake, gcc, or swig in recent version. This makes maintenance for older systems complex and extending support in that way hinders progress in developing.

PS: "Ubuntu is not Linux, and we need to support Linux with some older glibc because some Linux distribution has LTS for 10 years".
Oy course, that is true and we could try to do this. However until now, there were only requests for Windows or MacOS support, and orthogonally ARM-based platforms. Not a single user requested JavaSMT-related libraries for an older Linux system.

[PhilippWendler]

Some thoughts:

It would still be nice if there is a minimally required OS version for every solver in the documentation, especially if there is a gap as large as factor 3 in support time (one solver requiring an OS no older than 2 years, others working on 6 year old OS).

Furthermore, it would be nice to have a defined and documented policy on how users can expect the supported platforms to change in the future. For example, will JavaSMT continue to support Ubuntu 22.04 until it is out of support, or when will Ubuntu 24.04 be required earlier?

AFAIS all JavaSMT tests on GitLab CI run either on Ubuntu 20.04 (Java 11, 17, 21) or Ubuntu 23.10 (Java 22). This means that either (a) all solvers support Ubuntu 20.04 as well, (b) not all solvers are tested in CI, or (c) CI ignores failures from incompatible OS versions. If (a) is correct, it would certainly be nice to advertise this to your users, given that you already take the effort to test this. If (b) or (c) are correct, this would imply that JavaSMT currently also does not have tests that solvers work on the advertised platform Ubuntu 22.04. Of course, such tests should exist.

It seems there is deliberate effort to keep some solvers working on Ubuntu 18.04 (e.g., there is a special container image maintained for the builds with lots of manual dependency installations). This platform is out of free support for 1.5 years now. If the maintenance effort on the side of the JavaSMT developer is the limiting factor for this issue, wouldn't it be worth considering to invest that effort into trying to support all solvers on for example the supported Ubuntu and Debian versions, instead of supporting some solvers only on recent OS versions and others also on quite old OS versions? I guess more people would profit from this approach.

In a similar manner: If requiring something as new as Ubuntu 22.04 is fine for JavaSMT, why do developers still invest the effort to keep it working with Java 11? This is 6 years old, and its successor LTS Java 17 is already 3 years old, and even contained in the Ubuntu 20.04 package repositories.

Overall, I would request some improved documentation and recommend to consider rebalancing development effort to maybe get a policy like "JavaSMT aims at working on all currently supported Ubuntu versions with exceptions for where an upstream solver does not support this". That would be great.