Improve generation of python API documentation (#6482)

This PR makes generating the python part of our API documentation more reliable. If python bindings are enabled, it makes the docs target depend on pycvc5 and renders a warning into the documentation if python bindings are disabled.
To make the dependency on pycvc5 work properly, it changes the python bindings build so that the library is directly put in the right place and avoid the manual rename, so that the pycvc5 target actually points to the correct file.
Unfortunately, this means we need to build libcvc5 when building docs with python bindings enabled.

diff --git a/docs/CMakeLists.txt b/docs/CMakeLists.txt
index b08668afa464f4eb6d6c58365fc53bb392a399d4..4c5d9aa6c4b595636bc0ffa3973e09d37fef821f 100644 (file)
--- a/docs/CMakeLists.txt
+++ b/docs/CMakeLists.txt
@@ -18,6 +18,7 @@ check_python_module(sphinxcontrib.bibtex sphinxcontrib-bibtex)
 check_python_module(sphinx_tabs.tabs sphinx-tabs)
 
 add_subdirectory(cpp)
+add_subdirectory(python)
 
 set(SPHINX_INPUT_DIR ${CMAKE_CURRENT_SOURCE_DIR})
 set(SPHINX_OUTPUT_DIR ${CMAKE_CURRENT_BINARY_DIR}/sphinx)
@@ -25,7 +26,7 @@ set(SPHINX_OUTPUT_DIR ${CMAKE_CURRENT_BINARY_DIR}/sphinx)
 configure_file(conf.py.in ${CMAKE_CURRENT_BINARY_DIR}/conf.py)
 
 add_custom_target(docs ALL
-                  DEPENDS docs-cpp
+                  DEPENDS docs-cpp docs-python
                   COMMAND
                     ${SPHINX_EXECUTABLE} -b html
                     -c ${CMAKE_CURRENT_BINARY_DIR}

diff --git a/docs/conf.py.in b/docs/conf.py.in
index 28e8fa04cc0e276afbe54c2cb6b5c5e908e46f8e..f6e75b9b5cd00c97506a99d188bb64b460dadd5c 100644 (file)
--- a/docs/conf.py.in
+++ b/docs/conf.py.in
@@ -18,6 +18,11 @@ sys.path.insert(0, '${CMAKE_CURRENT_SOURCE_DIR}/ext/')
 # path to python api
 sys.path.insert(0, '${CMAKE_BINARY_DIR}/src/api/python')
 
+if("${BUILD_BINDINGS_PYTHON}" == "ON"):
+        tags.add('bindings_python')
+if("${BUILD_BINDINGS_JAVA}" == "ON"):
+        tags.add('bindings_java')
+
 
 # -- Project information -----------------------------------------------------
 

diff --git a/docs/python/CMakeLists.txt b/docs/python/CMakeLists.txt
new file mode 100644 (file)
index 0000000..cdac14d
--- /dev/null
+++ b/docs/python/CMakeLists.txt
@@ -0,0 +1,21 @@
+###############################################################################
+# Top contributors (to current version):
+#   Gereon Kremer
+#
+# This file is part of the cvc5 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.
+# #############################################################################
+#
+# Build system configuration for python API documentation.
+##
+
+add_custom_target(docs-python)
+
+if (BUILD_BINDINGS_PYTHON)
+    # Python API docs are generated from built python API
+    add_dependencies(docs-python pycvc5)
+endif()

diff --git a/docs/python/python.rst b/docs/python/python.rst
index 6d094488f06496a499465d74b738cba4323948fa..50d9077dfe140a333f9d40f32323e2aaff755c3f 100644 (file)
--- a/docs/python/python.rst
+++ b/docs/python/python.rst
@@ -1,6 +1,12 @@
 Python API Documentation
 ========================
 
+.. only:: not bindings_python
+
+    .. warning::
+
+        This documentation was built while python bindings were disabled. This part of the documentation is likely either empty or outdated. Please enable :code:`BUILD_BINDINGS_PYTHON` in :code:`cmake` and build the documentation again.
+
 .. toctree::
     :maxdepth: 2
 

diff --git a/src/api/python/CMakeLists.txt b/src/api/python/CMakeLists.txt
index 227872aa7424268b22b2c9bc772e14a932ec1155..c6686e32b0347f507390dc039d656f65dc36e6be 100644 (file)
--- a/src/api/python/CMakeLists.txt
+++ b/src/api/python/CMakeLists.txt
@@ -73,26 +73,20 @@ set_target_properties(pycvc5
                       COMPILE_FLAGS
                         "-Wno-error -Wno-shadow -Wno-implicit-fallthrough"
                       CXX_VISIBILITY_PRESET default
-                      VISIBILITY_INLINES_HIDDEN 0)
+                      VISIBILITY_INLINES_HIDDEN 0
+                      LIBRARY_OUTPUT_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}/pycvc5")
 
 python_extension_module(pycvc5)
 
 # 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(PYCVC5_MODULE "${CMAKE_CURRENT_BINARY_DIR}/pycvc5")
-file(MAKE_DIRECTORY "${PYCVC5_MODULE}")
-file(WRITE ${PYCVC5_MODULE}/__init__.py
+file(WRITE ${CMAKE_CURRENT_BINARY_DIR}/pycvc5/__init__.py
 "import sys
 from .pycvc5 import *
 # fake a submodule for dotted imports, e.g. from pycvc5.kinds import *
 sys.modules['%s.%s'%(__name__, kinds.__name__)] = kinds")
 
-set(PYCVC5_LOC "${PYCVC5_MODULE}/$<TARGET_FILE_NAME:pycvc5>")
-add_custom_command(TARGET pycvc5 POST_BUILD
-    COMMAND ${CMAKE_COMMAND} -E rename $<TARGET_FILE:pycvc5> ${PYCVC5_LOC}
-)
-
 # figure out if we're in a virtualenv
 execute_process(OUTPUT_VARIABLE IN_VIRTUALENV
   COMMAND