Reduce size of sphinx-gh output (#6601)

This PR reduces the disk size of the docs generated by make sphinx-gh.
Apart from reformatting the cmake source, we now not only remove the _sources folder, but also .doctrees (essentially the sphinx cache) and _static/fonts/ (the fonts that are actually used live in _static/css/fonts).
In combination, this now reduces the disk size from about 20MB (sphinx) to less than 6MB (sphinx-gh).
Furthermore this PR only uploads the generated documentation if it differs from whatever we currently have for master.
This is relevant to make the docs-ci repository smaller (which already has more than 5GB...)

diff --git a/.github/workflows/docs_cleanup.yml b/.github/workflows/docs_cleanup.yml
index 67b5f6b4ac0ab26f23c8d222ac9b07bab0ec82b7..f56a0f595ac0bc6e2a6442078041ed4e3ee7f004 100644 (file)
--- a/.github/workflows/docs_cleanup.yml
+++ b/.github/workflows/docs_cleanup.yml
@@ -4,8 +4,9 @@ on:
     - cron: '0 1 * * SUN'
 
 jobs:
-  build:
+  docs-cleanup:
     runs-on: ubuntu-latest
+    if: github.repository == 'cvc5/cvc5'
     steps:
       - name: Install Packages
         run: |
@@ -58,6 +59,11 @@ jobs:
 
           python3 genindex.py
           git add README.md
-          git commit -m "Update README.md"
+          if git diff --cached --exit-code
+          then
+            echo "Nothing changed"
+          else
+            git commit -m "Update README.md"
+          fi
 
           git push -f

diff --git a/.github/workflows/docs_upload.yml b/.github/workflows/docs_upload.yml
index 356337de6ad24244721d3fbafb00bfd6bc48bae4..7346371e3bdfc603dbdcd3fa4f221260b241681b 100644 (file)
--- a/.github/workflows/docs_upload.yml
+++ b/.github/workflows/docs_upload.yml
@@ -75,15 +75,21 @@ jobs:
           if [ -n "$NAME" ]; then
             mv docs-new target/docs-$NAME-$HASH
             cd target/
-            rm -f docs-$NAME
-            ln -s docs-$NAME-$HASH docs-$NAME
-            git add docs-$NAME docs-$NAME-$HASH
 
-            python3 genindex.py
-            git add README.md
-            git commit -m "Update docs for $NAME"
+            if diff -r target/docs-master/ target/docs-$NAME-$HASH
+            then
+              echo "Ignored run, documentation is the same as for current master"
+            else
+              rm -f docs-$NAME
+              ln -s docs-$NAME-$HASH docs-$NAME
+              git add docs-$NAME docs-$NAME-$HASH
 
-            git push
+              python3 genindex.py
+              git add README.md
+              git commit -m "Update docs for $NAME"
+
+              git push
+            fi
           else
             echo "Ignored run"
           fi

diff --git a/docs/CMakeLists.txt b/docs/CMakeLists.txt
index 99c4f3ab3a875d9c4556b7d4aa93d44cb8c8a7c1..11c4b8dfdf756a8367609cb4deb66aff3ac46f26 100644 (file)
--- a/docs/CMakeLists.txt
+++ b/docs/CMakeLists.txt
@@ -25,34 +25,38 @@ 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 docs-python gen-options
-                  COMMAND
-                    ${SPHINX_EXECUTABLE} -b html
-                    -c ${CMAKE_CURRENT_BINARY_DIR}
-                    # Tell Breathe where to find the Doxygen output
-                    -Dbreathe_projects.cvc5=${CPP_DOXYGEN_XML_FOLDER}
-                    -Dbreathe_projects.std=${CPP_DOXYGEN_XML_FOLDER}
-                    ${SPHINX_INPUT_DIR} ${SPHINX_OUTPUT_DIR}
-                  WORKING_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}
-                  COMMENT "Generating Sphinx Api docs")
+add_custom_target(
+  docs ALL
+  DEPENDS docs-cpp docs-python gen-options
+  COMMAND
+    ${SPHINX_EXECUTABLE} -b html -c ${CMAKE_CURRENT_BINARY_DIR}
+    # Tell Breathe where to find the Doxygen output
+    -Dbreathe_projects.cvc5=${CPP_DOXYGEN_XML_FOLDER}
+    -Dbreathe_projects.std=${CPP_DOXYGEN_XML_FOLDER} ${SPHINX_INPUT_DIR}
+    ${SPHINX_OUTPUT_DIR}
+  WORKING_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}
+  COMMENT "Generating Sphinx Api docs"
+)
 
 set(SPHINX_GH_OUTPUT_DIR ${CMAKE_CURRENT_BINARY_DIR}/sphinx-gh)
-add_custom_target(docs-gh ALL
-                  DEPENDS docs
-                  COMMAND ${CMAKE_COMMAND} -E remove_directory
-                    ${SPHINX_GH_OUTPUT_DIR}
-                  COMMAND ${CMAKE_COMMAND} -E copy_directory
-                    ${SPHINX_OUTPUT_DIR} ${SPHINX_GH_OUTPUT_DIR}
-                  COMMAND ${CMAKE_COMMAND} -E remove_directory
-                    ${SPHINX_GH_OUTPUT_DIR}/_sources
-                  COMMAND ${CMAKE_COMMAND} -E remove
-                    ${SPHINX_GH_OUTPUT_DIR}/objects.inv
-                  COMMAND ${CMAKE_COMMAND} -E rename
-                    ${SPHINX_GH_OUTPUT_DIR}/_static
-                    ${SPHINX_GH_OUTPUT_DIR}/static
-                  COMMAND find ${SPHINX_GH_OUTPUT_DIR} -type f |
-                    xargs sed -i'orig' 's/_static/static/'
-                  COMMAND find ${SPHINX_GH_OUTPUT_DIR} -name '*orig' -delete
-                  COMMENT "Generating GitHub Api docs")
-
+add_custom_target(
+  docs-gh ALL
+  DEPENDS docs
+  # remove existing sphinx-gh/ directory
+  COMMAND ${CMAKE_COMMAND} -E remove_directory ${SPHINX_GH_OUTPUT_DIR}
+  # copy sphinx/ to sphinx-gh/
+  COMMAND ${CMAKE_COMMAND} -E copy_directory ${SPHINX_OUTPUT_DIR}
+          ${SPHINX_GH_OUTPUT_DIR}
+  # remove leftovers from the build
+  COMMAND ${CMAKE_COMMAND} -E remove_directory ${SPHINX_GH_OUTPUT_DIR}/.doctrees
+          ${SPHINX_GH_OUTPUT_DIR}/_sources ${SPHINX_GH_OUTPUT_DIR}/_static/fonts
+  COMMAND ${CMAKE_COMMAND} -E remove ${SPHINX_GH_OUTPUT_DIR}/objects.inv
+  # rename _static/ to static/ (as jekyll ignores _*/ dirs)
+  COMMAND ${CMAKE_COMMAND} -E rename ${SPHINX_GH_OUTPUT_DIR}/_static
+          ${SPHINX_GH_OUTPUT_DIR}/static
+  COMMAND find ${SPHINX_GH_OUTPUT_DIR} -type f | xargs sed -i'orig'
+          's/_static/static/'
+  COMMAND find ${SPHINX_GH_OUTPUT_DIR} -name '*orig' -delete
+  # done
+  COMMENT "Generating GitHub Api docs"
+)