search

ethereum / solidity

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

Include z3 in solc docker image #7999

Closed chriseth closed 1 year ago

leonardoalt commented 4 years ago

When I talked to @gnidan at Devcon he mentioned this would probably be more useful than the solc-js callback

axic commented 4 years ago

Is our preference clearly for z3 or cvc4?

leonardoalt commented 4 years ago

z3 because it has a Horn solver as well which we use for the CHC engine

chriseth commented 4 years ago

Careful: The docker image is also used to build the static binary - we have to see if that is still possible and how large it gets.

leonardoalt commented 4 years ago

Since it's a docker image anyway I would guess the size increase won't be meaningful.

chriseth commented 4 years ago

The binary is exported to the release page as solc-static-linux to be used without docker.

yuetloo commented 4 years ago

@chriseth, for your reference, a docker image with solc v0.5.15 and z3 on alpine has a compressed image size of 62.78 MB.

https://hub.docker.com/r/yuetloo/solc_z3

The downloaded image size is 167MB.

REPOSITORY          TAG                 IMAGE ID            CREATED             SIZE
yuetloo/solc_z3     latest              391701d449f4        13 hours ago        167MB
axic commented 3 years ago

Is this done? Is this more important now that we have dynamic z3 loading?

ekpyron commented 3 years ago

I think not done, but not really affected by dynamic z3 loading either.

axic commented 3 years ago

Ah, this is the "release solc image".

github-actions[bot] commented 1 year ago

This issue has been marked as stale due to inactivity for the last 90 days. It will be automatically closed in 7 days.

github-actions[bot] commented 1 year ago

Hi everyone! This issue has been automatically closed due to inactivity. If you think this issue is still relevant in the latest Solidity version and you have something to contribute, feel free to reopen. However, unless the issue is a concrete proposal that can be implemented, we recommend starting a language discussion on the forum instead.