From: yoni206 Date: Wed, 31 Mar 2021 00:11:10 +0000 (-0700) Subject: Fix compilation of Python bindings for named build directories (#6244) X-Git-Tag: cvc5-1.0.0~2006 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7ff3e6300f3adb64867b636c7638ee4e8b00ce5a;p=cvc5.git Fix compilation of Python bindings for named build directories (#6244) In current master, the following fails whenever contains a /: ./configure.sh --python-bindings --name= The reason is that src/api/python/genkinds.py adds a directory to the python path while relying on the fact that the build directory is located directly under the main repo directory, which is not the case if contains a /. This PR fixes this by having cmake determine the right directory to add to the python path. --- diff --git a/src/api/python/CMakeLists.txt b/src/api/python/CMakeLists.txt index b400c14e5..62482a0ba 100644 --- a/src/api/python/CMakeLists.txt +++ b/src/api/python/CMakeLists.txt @@ -26,12 +26,13 @@ include_directories(${CMAKE_CURRENT_BINARY_DIR}) include_directories("${CMAKE_BINARY_DIR}/src/") # Generate cvc4kinds.{pxd,pyx} +configure_file(genkinds.py.in genkinds.py) add_custom_target( gen-pycvc4-kinds ALL COMMAND "${PYTHON_EXECUTABLE}" - "${CMAKE_CURRENT_LIST_DIR}/genkinds.py" + "${CMAKE_CURRENT_BINARY_DIR}/genkinds.py" --kinds-header "${PROJECT_SOURCE_DIR}/src/api/cvc4cppkind.h" --kinds-file-prefix "${CMAKE_CURRENT_BINARY_DIR}/cvc4kinds" DEPENDS diff --git a/src/api/python/genkinds.py b/src/api/python/genkinds.py deleted file mode 100644 index 30ee18708..000000000 --- a/src/api/python/genkinds.py +++ /dev/null @@ -1,153 +0,0 @@ -#!/usr/bin/env python -##################### -## genkinds.py -## Top contributors (to current version): -## Makai Mann -## This file is part of the CVC4 project. -## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS -## in the top-level source directory and their institutional affiliations. -## All rights reserved. See the file COPYING in the top-level source -## directory for licensing information. -## -""" -This script reads CVC4/src/api/cvc4cppkind.h and generates -.pxd and .pxi files which declare all the CVC4 kinds and -implement a Python wrapper for kinds, respectively. The -default names are kinds.pxd / kinds.pxi, but the name is -configurable from the command line with --kinds-file-prefix. - -The script is aware of the '#if 0' pattern and will ignore -kinds declared between '#if 0' and '#endif'. It can also -handle nested '#if 0' pairs. -""" - -import argparse -import os -import sys - -# the following command in CVC4/build/src/api/python/CMakeFiles/gen-pycvc4-kinds.dir/build.make -# cd CVC4/build/src/api/python && /usr/bin/python3 CVC4/src/api/python/genkinds.py ... -# indicates we are in directory CVC4/build/src/api/python -# so we use ../../../../src/api to access CVC4/src/api/parsekinds.py -sys.path.insert(0, os.path.abspath('../../../../src/api')) - -from parsekinds import * - -#################### Default Filenames ################ -DEFAULT_PREFIX = 'kinds' - -################ Comments and Macro Tokens ############ -PYCOMMENT = '#' - -####################### Code Blocks ################### -CDEF_KIND = " cdef Kind " - -KINDS_PXD_TOP = \ -r"""cdef extern from "api/cvc4cppkind.h" namespace "CVC4::api": - cdef cppclass Kind: - pass - - -# Kind declarations: See cvc4cppkind.h for additional information -cdef extern from "api/cvc4cppkind.h" namespace "CVC4::api::Kind": -""" - -KINDS_PXI_TOP = \ -r"""# distutils: language = c++ -# distutils: extra_compile_args = -std=c++11 - -from cvc4kinds cimport * -import sys -from types import ModuleType - -from libcpp.string cimport string -from libcpp.unordered_map cimport unordered_map - -# these maps are used for creating a kind -# it is needed for dynamically making a kind -# e.g. for getKind() -cdef unordered_map[int, Kind] int2kind -cdef unordered_map[int, string] int2name - -cdef class kind: - cdef Kind k - cdef str name - def __cinit__(self, int kindint): - self.k = int2kind[kindint] - self.name = str(int2name[kindint]) - - def __eq__(self, kind other): - return ( self.k) == ( other.k) - - def __ne__(self, kind other): - return ( self.k) != ( other.k) - - def __hash__(self): - return hash(( self.k, self.name)) - - def __str__(self): - return self.name - - def __repr__(self): - return self.name - - def as_int(self): - return self.k - -# create a kinds submodule -kinds = ModuleType('kinds') -kinds.__file__ = kinds.__name__ + ".py" -""" - -KINDS_ATTR_TEMPLATE = \ -r""" -int2kind[ {kind}] = {kind} -int2name[ {kind}] = b"{name}" -cdef kind {name} = kind( {kind}) -setattr(kinds, "{name}", {name}) -""" - - -def gen_pxd(parser: KindsParser, filename): - f = open(filename, "w") - f.write(KINDS_PXD_TOP) - # include the format_name docstring in the generated file - # could be helpful for users to see the formatting rules - for line in parser.format_name.__doc__.split(NL): - f.write(PYCOMMENT) - if not line.isspace(): - f.write(line) - f.write(NL) - for kind in parser.kinds: - f.write(CDEF_KIND + kind + NL) - f.close() - -def gen_pxi(parser : KindsParser, filename): - f = open(filename, "w") - pxi = KINDS_PXI_TOP - for kind, name in parser.kinds.items(): - pxi += KINDS_ATTR_TEMPLATE.format(name=name, kind=kind) - f.write(pxi) - f.close() - - -if __name__ == "__main__": - parser = argparse.ArgumentParser('Read a kinds header file and generate a ' - 'corresponding pxd file, with simplified kind names.') - parser.add_argument('--kinds-header', metavar='', - help='The header file to read kinds from', - default=DEFAULT_HEADER) - parser.add_argument('--kinds-file-prefix', metavar='', - help='The prefix for the .pxd and .pxi files to write ' - 'the Cython declarations to.', - default=DEFAULT_PREFIX) - - args = parser.parse_args() - kinds_header = args.kinds_header - kinds_file_prefix = args.kinds_file_prefix - - kp = KindsParser() - kp.parse(kinds_header) - - gen_pxd(kp, kinds_file_prefix + ".pxd") - gen_pxi(kp, kinds_file_prefix + ".pxi") diff --git a/src/api/python/genkinds.py.in b/src/api/python/genkinds.py.in new file mode 100644 index 000000000..0f8ba4b45 --- /dev/null +++ b/src/api/python/genkinds.py.in @@ -0,0 +1,150 @@ +#!/usr/bin/env python +##################### +## genkinds.py +## Top contributors (to current version): +## Makai Mann +## This file is part of the CVC4 project. +## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +## in the top-level source directory and their institutional affiliations. +## All rights reserved. See the file COPYING in the top-level source +## directory for licensing information. +## +""" +This script reads CVC4/src/api/cvc4cppkind.h and generates +.pxd and .pxi files which declare all the CVC4 kinds and +implement a Python wrapper for kinds, respectively. The +default names are kinds.pxd / kinds.pxi, but the name is +configurable from the command line with --kinds-file-prefix. + +The script is aware of the '#if 0' pattern and will ignore +kinds declared between '#if 0' and '#endif'. It can also +handle nested '#if 0' pairs. +""" + +import argparse +import os +import sys + +# get access to CVC4/src/api/parsekinds.py +sys.path.insert(0, os.path.abspath('${CMAKE_SOURCE_DIR}/src/api')) + +from parsekinds import * + +#################### Default Filenames ################ +DEFAULT_PREFIX = 'kinds' + +################ Comments and Macro Tokens ############ +PYCOMMENT = '#' + +####################### Code Blocks ################### +CDEF_KIND = " cdef Kind " + +KINDS_PXD_TOP = \ +r"""cdef extern from "api/cvc4cppkind.h" namespace "CVC4::api": + cdef cppclass Kind: + pass + + +# Kind declarations: See cvc4cppkind.h for additional information +cdef extern from "api/cvc4cppkind.h" namespace "CVC4::api::Kind": +""" + +KINDS_PXI_TOP = \ +r"""# distutils: language = c++ +# distutils: extra_compile_args = -std=c++11 + +from cvc4kinds cimport * +import sys +from types import ModuleType + +from libcpp.string cimport string +from libcpp.unordered_map cimport unordered_map + +# these maps are used for creating a kind +# it is needed for dynamically making a kind +# e.g. for getKind() +cdef unordered_map[int, Kind] int2kind +cdef unordered_map[int, string] int2name + +cdef class kind: + cdef Kind k + cdef str name + def __cinit__(self, int kindint): + self.k = int2kind[kindint] + self.name = str(int2name[kindint]) + + def __eq__(self, kind other): + return ( self.k) == ( other.k) + + def __ne__(self, kind other): + return ( self.k) != ( other.k) + + def __hash__(self): + return hash(( self.k, self.name)) + + def __str__(self): + return self.name + + def __repr__(self): + return self.name + + def as_int(self): + return self.k + +# create a kinds submodule +kinds = ModuleType('kinds') +kinds.__file__ = kinds.__name__ + ".py" +""" + +KINDS_ATTR_TEMPLATE = \ +r""" +int2kind[ {kind}] = {kind} +int2name[ {kind}] = b"{name}" +cdef kind {name} = kind( {kind}) +setattr(kinds, "{name}", {name}) +""" + + +def gen_pxd(parser: KindsParser, filename): + f = open(filename, "w") + f.write(KINDS_PXD_TOP) + # include the format_name docstring in the generated file + # could be helpful for users to see the formatting rules + for line in parser.format_name.__doc__.split(NL): + f.write(PYCOMMENT) + if not line.isspace(): + f.write(line) + f.write(NL) + for kind in parser.kinds: + f.write(CDEF_KIND + kind + NL) + f.close() + +def gen_pxi(parser : KindsParser, filename): + f = open(filename, "w") + pxi = KINDS_PXI_TOP + for kind, name in parser.kinds.items(): + pxi += KINDS_ATTR_TEMPLATE.format(name=name, kind=kind) + f.write(pxi) + f.close() + + +if __name__ == "__main__": + parser = argparse.ArgumentParser('Read a kinds header file and generate a ' + 'corresponding pxd file, with simplified kind names.') + parser.add_argument('--kinds-header', metavar='', + help='The header file to read kinds from', + default=DEFAULT_HEADER) + parser.add_argument('--kinds-file-prefix', metavar='', + help='The prefix for the .pxd and .pxi files to write ' + 'the Cython declarations to.', + default=DEFAULT_PREFIX) + + args = parser.parse_args() + kinds_header = args.kinds_header + kinds_file_prefix = args.kinds_file_prefix + + kp = KindsParser() + kp.parse(kinds_header) + + gen_pxd(kp, kinds_file_prefix + ".pxd") + gen_pxi(kp, kinds_file_prefix + ".pxi")