No longer build docs by default. Use make docs. (#7296)

This PR changes our policy when to build the documentation. Beforehand, make docs was included in make and make all.
Now, you need to run make docs explicitly.

diff --git a/INSTALL.rst b/INSTALL.rst
index 95dd063a2ccac906d864e3a7517f064f330b67a7..99626a554ec7d937d358fbac68d858919ee8b499 100644 (file)
--- a/INSTALL.rst
+++ b/INSTALL.rst
@@ -237,15 +237,12 @@ Building the API documentation of cvc5 requires the following dependencies:
   `sphinxcontrib-bibtex <https://sphinxcontrib-bibtex.readthedocs.io>`_
 - `Breathe <https://breathe.readthedocs.io>`_
 
-To build the documentation, configure cvc5 with ``./configure.sh --docs``.
-Building cvc5 will then include building the API documentation.
+To build the documentation, configure cvc5 with ``./configure.sh --docs`` and
+run ``make docs`` from within the build directory.
 
 The API documentation can then be found at
 ``<build_dir>/docs/sphinx/index.html``.
 
-To only build the documentation, change to the build directory and call
-``make docs``.
-
 To build the documentation for GitHub pages, change to the build directory and
 call ``make docs-gh``. The content of directory ``<build_dir>/docs/sphinx-gh``
 can then be copied over to GitHub pages.

diff --git a/docs/CMakeLists.txt b/docs/CMakeLists.txt
index c4cc6c2831fb3c03e03be9721b6b94147829ed77..15c51ed4face653eb833f842cbe47cbe6f041739 100644 (file)
--- a/docs/CMakeLists.txt
+++ b/docs/CMakeLists.txt
@@ -25,7 +25,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
+  docs
   DEPENDS docs-cpp docs-java docs-python gen-options
   COMMAND
     ${SPHINX_EXECUTABLE} -b html -c ${CMAKE_CURRENT_BINARY_DIR}
@@ -46,7 +46,7 @@ add_custom_command(
 
 set(SPHINX_GH_OUTPUT_DIR ${CMAKE_CURRENT_BINARY_DIR}/sphinx-gh)
 add_custom_target(
-  docs-gh ALL
+  docs-gh
   DEPENDS docs
   # remove existing sphinx-gh/ directory
   COMMAND ${CMAKE_COMMAND} -E remove_directory ${SPHINX_GH_OUTPUT_DIR}

diff --git a/docs/api/cpp/CMakeLists.txt b/docs/api/cpp/CMakeLists.txt
index f0b153b575e736cd0b9fedb65a81a7abb4dc10d1..511dd6e9c158d031ae885cd7c5f4379a7c9a0508 100644 (file)
--- a/docs/api/cpp/CMakeLists.txt
+++ b/docs/api/cpp/CMakeLists.txt
@@ -39,7 +39,7 @@ add_custom_command(
           ${PROJECT_SOURCE_DIR}/src/api/cpp/cvc5_kind.h
   COMMENT "Generating doxygen API docs"
 )
-add_custom_target(docs-cpp ALL DEPENDS ${DOXYGEN_INDEX_FILE})
+add_custom_target(docs-cpp DEPENDS ${DOXYGEN_INDEX_FILE})
 
 # tell parent scope where to find the output xml
 set(CPP_DOXYGEN_XML_DIR