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 <mathias.preiner@gmail.com>
* 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 <mathias.preiner@gmail.com>
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>

diff --git a/.travis.yml b/.travis.yml
index 481a9b9a99fbe71a9637c173ec21b609cd7b6a39..8297813da45ee154156c586edcb98a3c3dd19745 100644 (file)
--- a/.travis.yml
+++ b/.travis.yml
@@ -82,6 +82,11 @@ script:
        make install -j2
        echo -e "#include <cvc4/cvc4.h>\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 166a728dedf47be645341f015a7a2acf0cb3f37b..1998954e545a01dc041ed66297cb108a325905fd 100644 (file)
--- 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}/$<TARGET_FILE_NAME:pycvc4>")
+add_custom_command(TARGET pycvc4 POST_BUILD
+    COMMAND ${CMAKE_COMMAND} -E rename $<TARGET_FILE:pycvc4> ${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 39d9d46868af39c57b832cbc6e8668b3f6ef83a1..7e0e2e3c8eff23516a6b26eef7ae9fc60f204a48 100644 (file)
--- a/src/api/python/cvc4.pxi
+++ b/src/api/python/cvc4.pxi
@@ -230,11 +230,6 @@ cdef class Op:
         except:
             pass
 
-        try:
-            indices = kind(<int> 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 1e22875e73e4555fae34729c09f844cd3285a1d6..4fe7347e6e6a1b012e22c4837b7b201179034d81 100755 (executable)
--- 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 (file)
index 0000000..079aa46
--- /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})