search

ethereum / solidity

Solidity, the Smart Contract Programming Language
https://soliditylang.org
GNU General Public License v3.0
22.67k stars 5.62k forks source link

CI: Stop installing cvc4 on archlinux #15085

Closed blishko closed 1 month ago

blishko commented 1 month ago

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 commented 1 month ago

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 commented 1 month ago

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 commented 1 month ago

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 commented 1 month ago

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 commented 1 month ago

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?

cameel commented 1 month ago

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.