Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add cmake setup.py build dep #5972

Merged
merged 4 commits into from
Apr 13, 2022

Conversation

zwimer
Copy link
Contributor

@zwimer zwimer commented Apr 12, 2022

This extends #5971

It additionally adds cmake as a pip-installable build dependency. cmake is a native dependency, however, pip has a very well (first party?) maintained cmake package. This PR would tell the unbuilt z3-solver python package to depend on pypy's cmake; that is, pip install z3-solver will pip install cmake during build time as needed.

This would have a few benefits:

  1. It would allow the python package to be less dependent on what native tooling the user has installed on their system; that is pip install z3-solver will no longer fail if cmake is not present on the host system. This can be useful in docker, for example, among other scenarios.
  2. This will ensure the user is always using a relative new version of cmake; we could also pin the version if desired but cmake maintains backwards compatibility via cmake_minimum_required and other functions so I'm not sure why you would want to do this.

Note: This is not (necessarily) a bug fix, but a feature add. It just makes it easier to build in isolated environments, improves the chances of build success / reproducibility, and prefers using the python package manager for distributing packages the python package manager has over leaving installing it to the user natively.

@NikolajBjorner
Copy link
Contributor

I am unclear about the implications:
I don't understand why pip install z3-solver would fail without cmake on the client.

@zwimer
Copy link
Contributor Author

zwimer commented Apr 13, 2022

Pip will attempt to do the follwing:

  1. If the os, arch, and python interpreter can all be matched to an existing pypy z3-solver build, it will install it. (I.e. it will install the pre-build wheels z3 publishes on pypi.org)
  2. If it cannot be matched, it will build from source. Internally this means python setup.py build for us. Since building requires cmake, not having it will cause pip to fail.

To check this, here is a Dockerfile you can build to verify this (must be run on an arch z3-solver pip packages do not have pre-built wheels for; ex. M1's):

FROM alpine
RUN apk add --no-cache make gcc py3-pip
# z3 fails to declare wheel as a build dep (a recently merged PR should fix this for the next release)
RUN pip install wheel
# This will fail b/c cmake does not exist
RUN pip install z3-solver

Here is the result of me building this:

zwimer@Lotus ~/tmp> docker build .
[+] Building 19.2s (8/8) FINISHED
 => [internal] load build definition from Dockerfile                                                                 0.0s
 => => transferring dockerfile: 289B                                                                                 0.0s
 => [internal] load .dockerignore                                                                                    0.0s
 => => transferring context: 2B                                                                                      0.0s
 => [internal] load metadata for docker.io/library/alpine:latest                                                     1.5s
 => [auth] library/alpine:pull token for registry-1.docker.io                                                        0.0s
 => [1/4] FROM docker.io/library/alpine@sha256:4edbd2beb5f78b1014028f4fbb99f3237d9561100b6881aabbf5acce2c4f9454      0.7s
 => => resolve docker.io/library/alpine@sha256:4edbd2beb5f78b1014028f4fbb99f3237d9561100b6881aabbf5acce2c4f9454      0.0s
 => => sha256:9981e73032c8833e387a8f96986e560edbed12c38119e0edb0439c9c2234eac9 2.72MB / 2.72MB                       0.6s
 => => sha256:4edbd2beb5f78b1014028f4fbb99f3237d9561100b6881aabbf5acce2c4f9454 1.64kB / 1.64kB                       0.0s
 => => sha256:f3bec467166fd0e38f83ff32fb82447f5e89b5abd13264a04454c75e11f1cdc6 528B / 528B                           0.0s
 => => sha256:3fb3c9af89a9178a2ab12a1f30d8df607fa46a6f176acf9448328b22d31086a2 1.49kB / 1.49kB                       0.0s
 => => extracting sha256:9981e73032c8833e387a8f96986e560edbed12c38119e0edb0439c9c2234eac9                            0.1s
 => [2/4] RUN apk add --no-cache make gcc py3-pip                                                                   13.3s
 => [3/4] RUN pip install wheel                                                                                      0.7s
 => ERROR [4/4] RUN pip install z3-solver                                                                            2.8s
------
 > [4/4] RUN pip install z3-solver:
#7 0.482 Collecting z3-solver
#7 0.597   Downloading z3-solver-4.8.15.0.tar.gz (4.5 MB)
#7 2.327 Building wheels for collected packages: z3-solver
#7 2.327   Building wheel for z3-solver (setup.py): started
#7 2.461   Building wheel for z3-solver (setup.py): finished with status 'error'
#7 2.461   ERROR: Command errored out with exit status 1:
#7 2.461    command: /usr/bin/python3 -u -c 'import sys, setuptools, tokenize; sys.argv[0] = '"'"'/tmp/pip-install-gg975v2h/z3-solver_83e1a0f1517f48739486096df84d08cf/setup.py'"'"'; __file__='"'"'/tmp/pip-install-gg975v2h/z3-solver_83e1a0f1517f48739486096df84d08cf/setup.py'"'"';f=getattr(tokenize, '"'"'open'"'"', open)(__file__);code=f.read().replace('"'"'\r\n'"'"', '"'"'\n'"'"');f.close();exec(compile(code, __file__, '"'"'exec'"'"'))' bdist_wheel -d /tmp/pip-wheel-9zyodl3c
#7 2.461        cwd: /tmp/pip-install-gg975v2h/z3-solver_83e1a0f1517f48739486096df84d08cf/
#7 2.461   Complete output (4 lines):
#7 2.461   running bdist_wheel
#7 2.461   running build
#7 2.461   Configuring Z3
#7 2.461   error: [Errno 2] No such file or directory: 'cmake'
#7 2.461   ----------------------------------------
#7 2.461   ERROR: Failed building wheel for z3-solver
#7 2.461   Running setup.py clean for z3-solver
#7 2.585 Failed to build z3-solver
#7 2.601 Installing collected packages: z3-solver
#7 2.601     Running setup.py install for z3-solver: started
#7 2.729     Running setup.py install for z3-solver: finished with status 'error'
#7 2.730     ERROR: Command errored out with exit status 1:
#7 2.730      command: /usr/bin/python3 -u -c 'import sys, setuptools, tokenize; sys.argv[0] = '"'"'/tmp/pip-install-gg975v2h/z3-solver_83e1a0f1517f48739486096df84d08cf/setup.py'"'"'; __file__='"'"'/tmp/pip-install-gg975v2h/z3-solver_83e1a0f1517f48739486096df84d08cf/setup.py'"'"';f=getattr(tokenize, '"'"'open'"'"', open)(__file__);code=f.read().replace('"'"'\r\n'"'"', '"'"'\n'"'"');f.close();exec(compile(code, __file__, '"'"'exec'"'"'))' install --record /tmp/pip-record-lmfn_vnh/install-record.txt --single-version-externally-managed --compile --install-headers /usr/include/python3.9/z3-solver
#7 2.730          cwd: /tmp/pip-install-gg975v2h/z3-solver_83e1a0f1517f48739486096df84d08cf/
#7 2.730     Complete output (4 lines):
#7 2.730     running install
#7 2.730     running build
#7 2.730     Configuring Z3
#7 2.730     error: [Errno 2] No such file or directory: 'cmake'
#7 2.730     ----------------------------------------
#7 2.730 ERROR: Command errored out with exit status 1: /usr/bin/python3 -u -c 'import sys, setuptools, tokenize; sys.argv[0] = '"'"'/tmp/pip-install-gg975v2h/z3-solver_83e1a0f1517f48739486096df84d08cf/setup.py'"'"'; __file__='"'"'/tmp/pip-install-gg975v2h/z3-solver_83e1a0f1517f48739486096df84d08cf/setup.py'"'"';f=getattr(tokenize, '"'"'open'"'"', open)(__file__);code=f.read().replace('"'"'\r\n'"'"', '"'"'\n'"'"');f.close();exec(compile(code, __file__, '"'"'exec'"'"'))' install --record /tmp/pip-record-lmfn_vnh/install-record.txt --single-version-externally-managed --compile --install-headers /usr/include/python3.9/z3-solver Check the logs for full command output.
------
executor failed running [/bin/sh -c pip install z3-solver]: exit code: 1

As you can see, pip install z3-solver might require cmake. By declaring it as a python build dependency, pip install cmake should automatically be run before this build step which should prevent this particular failure.

@NikolajBjorner NikolajBjorner merged commit c0b455e into Z3Prover:master Apr 13, 2022
@NikolajBjorner
Copy link
Contributor

oh grief

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants