CI: Stop installing cvc4 on archlinux

[blishko]

This change is in preparation for upgrading to cvc5. Since archlinux is not running SMT tests anyway, we can drop cvc4 from the build immediately.

[blishko]

I don't actually understand why z3 is installed for t_archlinux_soltest but not for b_archlinux.

[r0qs]

Yeah, I was about to comment about it. You can remove this installation step. It is already installed in b_archlinux.

[blishko]

Yes, everything except z3 😄

I am also wondering about this in b_archlinux

# This can be switched off if we run out of sync with Arch.
      USE_Z3: ON

Should we switch it off?

[r0qs]

No, keep it for now, and also installing z3 in that step. We actually need to think about if we will reenable the tests once we update the z3 version (i.e. removing the --no-smt flag). But for now let's keep that flag to disable the tests as well.

So just change the step to:

pacman --noconfirm -Syu --noprogressbar --needed z3

[blishko]

Changed the step accordingly and the CI is still green.

[cameel]

Well, if CI passes here, it proves that we're not really running anything requiring cvc4 on Arch Linux.

[blishko]

Before we merge this, I wanted to follow up on Rodrigo's suggestion to remove installation of dependencies in t_archlinux_soltest, because these are already installed in b_archlinux. Except for Z3. That is also weird, because my intuition is that Z3 should be installed in the b job, not the t job.

[cameel]

Ah, ok then. I wasn't going to merge it myself anyway. Just approve it and let you do it yourself in case you still wanted to change something :) Though if you're planning changes it's always safer to revert the PR back to draft.

Except for Z3. That is also weird, because my intuition is that Z3 should be installed in the b job, not the t job.

The binary is not completely static. Z3 is actually the one thing we link dynamically and the z3 package contains that dynamic library. You need it to be installed when you run solc.

EDIT: Actually, this job does not even build a static binary. But this does not change the situation with Z3 :)

[blishko]

The binary is not completely static. Z3 is actually the one thing we link dynamically and the z3 package contains that dynamic library. You need it to be installed when you run solc.

@cameel, @r0qs, can you help me understand this?
During compilation, Z3 is not present, so Z3-related files are not compiled (e.g., Z3Interface.cpp, Z3CHCInterface.h).
Also, on archlinux, the cmake option USE_Z3_DLOPEN is OFF, so my conclusion is that installing Z3 for the testing job is useless, it does not do anything.

My opinion is that either Z3 should be installed for the build job already, or not at all. What am I missing?

[r0qs]

The binary is not completely static. Z3 is actually the one thing we link dynamically and the z3 package contains that dynamic library. You need it to be installed when you run solc.

@cameel, @r0qs, can you help me understand this? During compilation, Z3 is not present, so Z3-related files are not compiled (e.g., Z3Interface.cpp, Z3CHCInterface.h). Also, on archlinux, the cmake option USE_Z3_DLOPEN is OFF, so my conclusion is that installing Z3 for the testing job is useless, it does not do anything.

Oh, I thought that USE_Z3_DLOPEN was ON, but you are right, it is OFF by default. So in this case it doesn't seem to make sense to install z3 indeed.

My opinion is that either Z3 should be installed for the build job already, or not at all. What am I missing?

Yeah, I think we should just remove z3 in this case then. Since we are running the tests with --no-smt. We could quickly discuss that during the call today. One of the problems that I remember of having z3 enable on the tests running on Archlinux is related to the version of z3, that was constantly mismatch due to the Archlinux rolling releases. So maybe, we could even consider re-enable such tests and add -DSTRICT_Z3_VERSION=OFF, so we would catch possible breaking changes on z3 library.

[blishko]

OK, how about we continue with the conversation about Z3 in our CI channel.
I think we can merge this PR as is now, no?

[ekpyron]

Well, there's still some open questions about how to deal with this stuff going forward - but not much harm in merging this for now.

[cameel]

The binary is not completely static. Z3 is actually the one thing we link dynamically and the z3 package contains that dynamic library. You need it to be installed when you run solc.

Also, on archlinux, the cmake option USE_Z3_DLOPEN is OFF, so my conclusion is that installing Z3 for the testing job is useless, it does not do anything.

My opinion is that either Z3 should be installed for the build job already, or not at all. What am I missing?

Ah, right. I assumed it was ON. I mean, my impression was that you were actually having some problems after removing z3 from the test job and asking why that is. But rereading now, I don't see any mention of that, you're just asking if it's ok to remove it. I'd say that if the job works without it then it's fine. I'd expect a crash/error otherwise. With a USE_Z3_DLOPEN=OFF build it indeed shouldn't be needed.