From 6e69899967624b04c98c3d291693bae6d32401f6 Mon Sep 17 00:00:00 2001 From: makaimann Date: Wed, 11 Mar 2020 17:03:29 -0700 Subject: [PATCH] Add automatic Cython binding installation (#3933) * Remove getIndices for Kinds * Test importing pycvc4 * Distutils install for pycvc4 * Use full path for cvc4kinds prefix * Remove zip_safe option (not needed for distutils) * Automatically clean up setup.py intermediate files * Rely on make install to install pycvc4 * Run make install when testing python bindings * Fix: Check importing pycvc4 when python bindings are built * Remove one -Wshadow warning for cython-generated files * Put the fake kinds submodule in generated __init__.py * Remove unnecessary file permission options in python CMakeLists * Respect install prefix unless in a virtualenv * Handle python2 print function * Use VIRTUAL_ENV environment variable to check if in python virtualenv * Add header and documentation to setup.py.in * Capitalize CVC4 in PyCVC4Install * Update src/api/python/CMakeLists.txt Co-Authored-By: Mathias Preiner * Simplify CMakeLists for setup.py configuration * Shorten virtualenv check with Mathias's suggestion * Set TRAVIS_CVC4_PYTHON_BINDINGS to no in other builds * minor: bash syntax fix * Move pycvc4 import check to makeInstallCheck * Include installed pycvc4 location on PYTHONPATH * Better way to set PYTHONPATH Co-authored-by: Mathias Preiner Co-authored-by: Andrew Reynolds --- .travis.yml | 10 ++++++++++ src/api/python/CMakeLists.txt | 37 +++++++++++++++++++++++++++++++++-- src/api/python/cvc4.pxi | 12 +----------- src/api/python/genkinds.py | 2 -- src/api/python/setup.py.in | 31 +++++++++++++++++++++++++++++ 5 files changed, 77 insertions(+), 15 deletions(-) create mode 100644 src/api/python/setup.py.in diff --git a/.travis.yml b/.travis.yml index 481a9b9a9..8297813da 100644 --- a/.travis.yml +++ b/.travis.yml @@ -82,6 +82,11 @@ script: make install -j2 echo -e "#include \nint main() { CVC4::ExprManager em; return 0; }" > /tmp/test.cpp $CXX -std=c++11 /tmp/test.cpp -I install/include -L install/lib -lcvc4 -lcln || exit 1 + # set PYTHONPATH to include the directory containing pycvc4 module + export PYTHONPATH=$PYTHONPATH:$(dirname $(find ./install/ -name "pycvc4" -type d)) + if [[ "$TRAVIS_CVC4_PYTHON_BINDINGS" == "yes" ]]; then + $TRAVIS_PYTHON -c "import pycvc4" || exit 1 + fi ) } run() { @@ -108,12 +113,14 @@ matrix: env: - TRAVIS_CVC4=yes - TRAVIS_WITH_LFSC=yes + - TRAVIS_CVC4_PYTHON_BINDINGS=no - TRAVIS_CVC4_CONFIG="production --language-bindings=java --lfsc" - TRAVIS_PYTHON=python - compiler: gcc env: - TRAVIS_CVC4=yes - TRAVIS_WITH_LFSC=yes + - TRAVIS_CVC4_PYTHON_BINDINGS=no - TRAVIS_CVC4_CONFIG="debug --symfpu --lfsc --no-debug-symbols" - TRAVIS_PYTHON=python # Test python bindings @@ -121,12 +128,14 @@ matrix: env: - TRAVIS_CVC4=yes - TRAVIS_WITH_LFSC=yes + - TRAVIS_CVC4_PYTHON_BINDINGS=yes - TRAVIS_CVC4_CONFIG="production --python-bindings --python2" - TRAVIS_PYTHON=python - compiler: gcc env: - TRAVIS_CVC4=yes - TRAVIS_WITH_LFSC=yes + - TRAVIS_CVC4_PYTHON_BINDINGS=yes - TRAVIS_CVC4_CONFIG="production --python-bindings --python3" - TRAVIS_PYTHON=python3 # @@ -135,6 +144,7 @@ matrix: env: - TRAVIS_CVC4=yes - TRAVIS_WITH_LFSC=yes + - TRAVIS_CVC4_PYTHON_BINDINGS=no - TRAVIS_CVC4_CONFIG="debug --symfpu --cln --gpl --no-debug-symbols --no-proofs" - TRAVIS_PYTHON=python notifications: diff --git a/src/api/python/CMakeLists.txt b/src/api/python/CMakeLists.txt index 166a728de..1998954e5 100644 --- a/src/api/python/CMakeLists.txt +++ b/src/api/python/CMakeLists.txt @@ -23,7 +23,7 @@ add_custom_target( "${PYTHON_EXECUTABLE}" "${CMAKE_CURRENT_LIST_DIR}/genkinds.py" --kinds-header "${PROJECT_SOURCE_DIR}/src/api/cvc4cppkind.h" - --kinds-file-prefix "cvc4kinds" + --kinds-file-prefix "${CMAKE_CURRENT_BINARY_DIR}/cvc4kinds" DEPENDS genkinds.py COMMENT @@ -39,4 +39,37 @@ add_library(pycvc4 target_link_libraries(pycvc4 cvc4 ${PYTHON_LIBRARIES}) python_extension_module(pycvc4) -install(TARGETS pycvc4 DESTINATION lib) + +# Installation based on https://bloerg.net/2012/11/10/cmake-and-distutils.html +# Create a wrapper python directory and generate a distutils setup.py file +configure_file(setup.py.in setup.py) +set(PYCVC4_MODULE "${CMAKE_CURRENT_BINARY_DIR}/pycvc4") +file(MAKE_DIRECTORY "${PYCVC4_MODULE}") +file(WRITE ${PYCVC4_MODULE}/__init__.py +"import sys +from .pycvc4 import * +# fake a submodule for dotted imports, e.g. from pycvc4.kinds import * +sys.modules['%s.%s'%(__name__, kinds.__name__)] = kinds") + +set(PYCVC4_LOC "${PYCVC4_MODULE}/$") +add_custom_command(TARGET pycvc4 POST_BUILD + COMMAND ${CMAKE_COMMAND} -E rename $ ${PYCVC4_LOC} +) + +# figure out if we're in a virtualenv +execute_process(OUTPUT_VARIABLE IN_VIRTUALENV + COMMAND + "${PYTHON_EXECUTABLE}" + -c + "from __future__ import print_function; import os; +print('YES' if 'VIRTUAL_ENV' in os.environ else 'NO', end='')") + +set(INSTALL_CMD "${PYTHON_EXECUTABLE} ${CMAKE_CURRENT_BINARY_DIR}/setup.py install") +# if we're in a virtualenv, we install it in the virtualenv lib location +if ("${IN_VIRTUALENV}" STREQUAL "NO") + set(INSTALL_CMD "${INSTALL_CMD} --prefix=${CMAKE_INSTALL_PREFIX}") +endif() + +message("Python bindings install command: ${INSTALL_CMD}") + +install(CODE "execute_process(COMMAND ${INSTALL_CMD})" FILE_PERMISSIONS OWNER_EXECUTE OWNER_WRITE OWNER_READ) diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi index 39d9d4686..7e0e2e3c8 100644 --- a/src/api/python/cvc4.pxi +++ b/src/api/python/cvc4.pxi @@ -230,11 +230,6 @@ cdef class Op: except: pass - try: - indices = kind( self.cop.getIndices[c_Kind]()) - except: - pass - try: indices = self.cop.getIndices[uint32_t]() except: @@ -553,12 +548,7 @@ cdef class Solver: def mkReal(self, val, den=None): cdef Term term = Term() if den is None: - try: - term.cterm = self.csolver.mkReal(str(val).encode()) - except Exception as e: - raise ValueError("Expecting a number" - " or a string representing a number" - " but got: {}".format(val)) + term.cterm = self.csolver.mkReal(str(val).encode()) else: if not isinstance(val, int) or not isinstance(den, int): raise ValueError("Expecting integers when" diff --git a/src/api/python/genkinds.py b/src/api/python/genkinds.py index 1e22875e7..4fe7347e6 100755 --- a/src/api/python/genkinds.py +++ b/src/api/python/genkinds.py @@ -95,8 +95,6 @@ cdef class kind: # create a kinds submodule kinds = ModuleType('kinds') -# fake a submodule for dotted imports, e.g. from pycvc4.kinds import * -sys.modules['%s.%s'%(__name__, kinds.__name__)] = kinds kinds.__file__ = kinds.__name__ + ".py" """ diff --git a/src/api/python/setup.py.in b/src/api/python/setup.py.in new file mode 100644 index 000000000..079aa468e --- /dev/null +++ b/src/api/python/setup.py.in @@ -0,0 +1,31 @@ +#!/usr/bin/env python + +# This script is automatically configured with cmake when CVC4 +# is built with --python-bindings. It is called during make +# install to automatically install the python bindings using +# distutils. +# If it is called from a python virtualenv, the bindings are +# installed in the virtualenv, otherwise, it respects the +# configured install prefix using the setup.py --prefix option + +from distutils.core import setup +from distutils.command.clean import clean +from distutils.command.install import install + +class PyCVC4Install(install): + + # Calls the default run command, then deletes the build area + # (equivalent to "setup clean --all"). + def run(self): + install.run(self) + c = clean(self.distribution) + c.all = True + c.finalize_options() + c.run() + +setup(name='pycvc4', + version='${CVC4_MAJOR}.${CVC4_MINOR}.${CVC4_RELEASE}', + packages=['pycvc4'], + package_dir={'pycvc4': '${CMAKE_CURRENT_BINARY_DIR}/pycvc4'}, + package_data={'pycvc4': ['pycvc4.so']}, + cmdclass={'install': PyCVC4Install}) -- 2.30.2