From: Gereon Kremer <nafur42@gmail.com>
Date: Wed, 26 May 2021 06:10:51 +0000 (+0200)
Subject: Reduce size of sphinx-gh output (#6601)
X-Git-Tag: cvc5-1.0.0~1696
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=22d05234d9a4a98ad715d6e2d6cb1616592fd2b5;p=cvc5.git

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 67b5f6b4a..f56a0f595 100644
--- 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 356337de6..7346371e3 100644
--- 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 99c4f3ab3..11c4b8dfd 100644
--- 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"
+)