[BUG] GLIBC 2.27 not working with z3 4.8.12

[rodrigo7491]

Description

The newest version of z3, see #999, requires GLIBC 2.29. This dependency is not updated automatically, if an older version is present, z3, and by extension apalache, won't work. To check GLIBC version on Linux, run ldd --version.

System information

• Apalache version [apalache-mc version]: 0.16.3-SNAPSHOT build v0.16.2-23-gfffe3b4-dirty
• OS [e.g. Ubuntu Linux or Mac OS, and the current version]: Linux Mint 19.3
• JDK version [e.g. OpenJDK 0.8.0]: openjdk 11.0.11 2021-04-20

[konnov]

@shonfeder any ideas on what shall we do?

[shonfeder]

@rodrigo7491 and I helped root cause this together.

It's just due to current architecture per-requisites from Z3, so the only things we can do on our end, afailk, are

1. Get users and devs to update to a architecture that is compatible with the latest Z3
2. Use a previous version of Z3

I guess we could also considering developing infrastructure to support older architecture in parallel, but I don't think this fits with our current priorities?

For now, Rodrigo is trying to update his distro (the latest uses the required glibc version). I think he will report his results here. If he cannot update without a huge pain, I think plan b is to revert #999 for now. Tho we could also invest in documenting and setting up a docker-based development workflow.

[konnov]

Is there a way to check that the glibc dependency is present in apalache-mc? I guess, this test should be linux-dependent though.

[konnov]

I guess, this is not an issue for people using docker, right?

[shonfeder]

To be clear: this is about the kernel version Linux users are using. Mint 19 (the previous major LTS version) uses an old GLIBC in their kernel.

What kind of result would you be interested in from checking the glibc dependency?

[shonfeder]

Right, this is not effecting our docker containers: all our CI is passing, so it's not a problem for the latest ubuntu versions, macos, or our docker containers. It will effect any linux users who are using kernel's tied to old version of GLIBC.

If we want to anticipate error handling of unsatisified Z3 system requirements, we might try catching the exceptions raised. E.g,, I think Rodrigo was hitting this when running the tests:

  at.forsyte.apalache.tla.assignments.TestSymbTransPass: /tmp/z3-turnkey1855063264018777/libz3.so: /lib/x86_64-linux-gnu/libm.so.6: version `GLIBC_2.29' not found (required by /tmp/z3-turnkey1855063264018777/libz3.so)

[konnov]

Just tell the users that apalache uses the newer version of glibc and they should update?

[shonfeder]

Maybe that's worth doing if @rodrigo7491 hasn't updated his system and wants to use the problem to add error handling of this sort?

[konnov]

I guess this issue is not critical. But it would be good to have a plan for treating problems like that in the future.

[shonfeder]

Thinking about this more, I think I'm against adding any code to try to check for the transitive system dependencies:

• If people are building from source, they are responsible for ensuring pre-requisites are met. We could help support them by improving the documentation, but don't think we should do more than that (unless we want to invest in a nix or bazel configuration that puts all dependencies into the build configuration)
• Regarding usability of install for users, this problem will be handled by package management. So if we want to prioritize work on this, we can prioritize packaging work.
• Lastly, arguably this is something we could try to push upstream, getting Z3 turnkey or Z3 itself to be more graceful in stating their deps. But we have to decide how much we want to invest in that.

What do you think?

[shonfeder]

Also: worth noting that the purpose of opening this issue is to document the problem so anyone who hits in the future will be able to quickly find the fix :)

[konnov]

That makes sense. I agree that people who build the project from sources are ready to address issues like that. Perhaps, this issue serves as a documentation, and somebody who is looking for a bug will find the explanation here. Do we need a special label for issues like that?

[shonfeder]

How 'bout them labels?

[konnov]

Looks fine. It's true that we don't want to fix that :))

[shonfeder]

Hmm, so one thing we probably should do is make sure that exceptions that come from the underlying Z3 library get clear user errors indicating that source of the problem. I'll ad this to the issue around better errors.

[rodrigo7491]

I updated my OS to Mint 20, which has GLIBC 2.31, and that solved the problem. Regarding the discussion of per-requisites, I agree that people that build from source can deal with issues such as this, but the problem in my opinion is that since z3 is not manually installed, nor mentioned in the build instructions, it might not be obvious which dependencies are needed.

[shonfeder]

I don't know where is a good place to record such information, or how we'll keep it up to date. If anyone any has ideas, a PR into the relevant documentation would be great.