mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
b5bd2ca6a9
This PR changes the signature of `_term` from `cdef Term _term(tm: TermManager, term: c_Term)`, which uses Python type annotations and assumes `None` is invalid for `TermManager`, to `cdef Term _term(TermManager tm, const c_Term& term)`, which uses Cython type annotations and allows `None` as a valid value. This change enables the creation of terms without an associated term manager, which is necessary for null terms. The problem was detected when running the cvc5 Python bindings tests compiled with Cython 3.1.2, which introduced runtime `None` checks for functions using Python syntax. Specifically, `unit/api/python/test_proof.py::test_null_proof` failed. The PR also removes the previous Cython version upper-bound that was used as a temporary workaround.
107 lines
3.8 KiB
CMake
107 lines
3.8 KiB
CMake
###############################################################################
|
|
# Top contributors (to current version):
|
|
# Daniel Larraz
|
|
#
|
|
# This file is part of the cvc5 project.
|
|
#
|
|
# Copyright (c) 2009-2025 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.
|
|
# #############################################################################
|
|
#
|
|
# Find Cython
|
|
# Cython_FOUND - found Cython Python module
|
|
##
|
|
|
|
macro(get_cython_version)
|
|
execute_process(
|
|
COMMAND "${Python_EXECUTABLE}" -c "import Cython; print(Cython.__version__)"
|
|
RESULT_VARIABLE Cython_VERSION_CHECK_RESULT
|
|
OUTPUT_VARIABLE Cython_VERSION
|
|
ERROR_QUIET
|
|
OUTPUT_STRIP_TRAILING_WHITESPACE
|
|
)
|
|
endmacro()
|
|
|
|
get_cython_version()
|
|
|
|
if (Cython_FIND_REQUIRED)
|
|
set(Cython_FIND_MODE FATAL_ERROR)
|
|
else()
|
|
set(Cython_FIND_MODE STATUS)
|
|
endif()
|
|
|
|
if (Cython_VERSION_CHECK_RESULT EQUAL 0)
|
|
set(Cython_FOUND TRUE)
|
|
message(STATUS "Found Cython version: ${Cython_VERSION}")
|
|
if (DEFINED Cython_FIND_VERSION)
|
|
if(Cython_FIND_VERSION_EXACT)
|
|
if (NOT (Cython_VERSION VERSION_EQUAL ${Cython_FIND_VERSION}))
|
|
if(ENABLE_AUTO_DOWNLOAD)
|
|
message(STATUS
|
|
"Installing module Cython==${Cython_FIND_VERSION}"
|
|
)
|
|
execute_process(
|
|
COMMAND
|
|
${Python_EXECUTABLE} -m pip install Cython==${Cython_FIND_VERSION}
|
|
RESULT_VARIABLE CYTHON_INSTALL_CMD_EXIT_CODE
|
|
)
|
|
if(CYTHON_INSTALL_CMD_EXIT_CODE)
|
|
message(${Cython_FIND_MODE}
|
|
"Could not install Cython==${Cython_FIND_VERSION}")
|
|
else()
|
|
get_cython_version()
|
|
endif()
|
|
else()
|
|
message(${Cython_FIND_MODE}
|
|
"Cython version == ${Cython_FIND_VERSION} is required, "
|
|
"but found version ${Cython_VERSION}")
|
|
endif()
|
|
endif()
|
|
else()
|
|
if (Cython_VERSION VERSION_LESS ${Cython_FIND_VERSION})
|
|
if(ENABLE_AUTO_DOWNLOAD)
|
|
message(STATUS "Upgrading module Cython")
|
|
execute_process(COMMAND
|
|
${Python_EXECUTABLE} -m pip install Cython -U
|
|
RESULT_VARIABLE CYTHON_INSTALL_CMD_EXIT_CODE
|
|
)
|
|
if(CYTHON_INSTALL_CMD_EXIT_CODE)
|
|
message(${Cython_FIND_MODE}
|
|
"Could not install Cython >= ${Cython_FIND_VERSION}")
|
|
else()
|
|
get_cython_version()
|
|
endif()
|
|
else()
|
|
message(${Cython_FIND_MODE}
|
|
"Cython version >= ${Cython_FIND_VERSION} is required, "
|
|
"but found version ${Cython_VERSION}")
|
|
endif()
|
|
endif()
|
|
endif()
|
|
endif()
|
|
else()
|
|
set(Cython_FOUND FALSE)
|
|
if(ENABLE_AUTO_DOWNLOAD)
|
|
message(STATUS "Installing module Cython")
|
|
execute_process(
|
|
COMMAND ${Python_EXECUTABLE} -m pip install Cython
|
|
RESULT_VARIABLE CYTHON_INSTALL_CMD_EXIT_CODE)
|
|
if(CYTHON_INSTALL_CMD_EXIT_CODE)
|
|
message(${Cython_FIND_MODE} "Could not install module Cython")
|
|
else()
|
|
set(Cython_FOUND TRUE)
|
|
get_cython_version()
|
|
endif()
|
|
else()
|
|
message(${Cython_FIND_MODE}
|
|
"Could not find module Cython for Python "
|
|
"version ${Python_VERSION_MAJOR}.${Python_VERSION_MINOR}. "
|
|
"Make sure to install Cython for this Python version "
|
|
"via \n`${Python_EXECUTABLE} -m pip install Cython'.\n"
|
|
"or use --auto-download to let us install it for you.\n"
|
|
"Note: You need to have pip installed for this Python version.")
|
|
endif()
|
|
endif()
|