From ab3354285a00e6102d45e0cb0405952b1b812da1 Mon Sep 17 00:00:00 2001 From: Kwankyu Lee Date: Fri, 6 Sep 2024 10:32:03 +0900 Subject: [PATCH 1/4] Use artifact-doc-develop for PR event --- .ci/create-changes-html.sh | 6 ++ .github/workflows/doc-build.yml | 78 +++++++++++++------ src/sage/crypto/sbox.pyx | 2 +- src/sage/matrix/matrix2.pyx | 2 +- .../rings/polynomial/polynomial_element.pyx | 4 +- src/sage/rings/ring_extension.pyx | 2 +- src/sage/rings/ring_extension_element.pyx | 2 +- 7 files changed, 66 insertions(+), 30 deletions(-) diff --git a/.ci/create-changes-html.sh b/.ci/create-changes-html.sh index 0e80d0d2814..0cc86f34b13 100755 --- a/.ci/create-changes-html.sh +++ b/.ci/create-changes-html.sh @@ -16,6 +16,12 @@ echo '' >> CHANGES.html echo '' >> CHANGES.html cat >> CHANGES.html << EOF + ; d' \ -e 's;#L[0-9]*";";' \ + -e 's;tab-set--[0-9]*-;tab-set-;' \ && true) # Create git repo from old doc (cd doc && \ @@ -223,6 +224,7 @@ jobs: -e '/;,\;; d' \ -e 's;#L[0-9]*";";' \ + -e 's;tab-set--[0-9]*-;tab-set-;' \ && git commit -a -m 'wipe-out') # Since HEAD is at commit 'wipe-out', HEAD~1 is commit 'new' (new doc), HEAD~2 is commit 'old' (old doc) (cd doc && git diff $(git rev-parse HEAD~2) -- "*.html") > diff.txt From b9567a69abdc3364d1a84a5eebfeb398e2e0ec93 Mon Sep 17 00:00:00 2001 From: Kwankyu Lee Date: Tue, 10 Sep 2024 14:36:33 +0900 Subject: [PATCH 3/4] Squeeze more disk space --- .github/workflows/doc-build.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/doc-build.yml b/.github/workflows/doc-build.yml index f0895778a17..7b4ea38e044 100644 --- a/.github/workflows/doc-build.yml +++ b/.github/workflows/doc-build.yml @@ -267,6 +267,8 @@ jobs: id: buildlivedoc if: startsWith(github.ref, 'refs/tags/') run: | + # Avoid running out of disk space + rm -rf upstream export MAKE="make -j5 --output-sync=recurse" SAGE_NUM_THREADS=5 export PATH="build/bin:$PATH" eval $(sage-print-system-package-command auto update) From 5e86fcdc39e56140174abe031de92ebf82abfa47 Mon Sep 17 00:00:00 2001 From: Kwankyu Lee Date: Tue, 12 Nov 2024 08:06:22 +0900 Subject: [PATCH 4/4] Remove more spurious diffs --- .github/workflows/doc-build.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/doc-build.yml b/.github/workflows/doc-build.yml index 7b4ea38e044..5eb5e932da9 100644 --- a/.github/workflows/doc-build.yml +++ b/.github/workflows/doc-build.yml @@ -168,7 +168,7 @@ jobs: # Wipe out chronic diffs between old doc and new doc (cd doc && \ find . -name "*.html" | xargs sed -i -e '/class="sidebar-brand-text"/ s/Sage [0-9a-z.]* /Sage '"$new_version"' /' \ - -e '/;,\;; d' \ -e 's;#L[0-9]*";";' \ @@ -221,7 +221,7 @@ jobs: # Wipe out chronic diffs of new doc against old doc before creating CHANGES.html (cd doc && \ find . -name "*.html" | xargs sed -i -e '/This is documentation/ s/ built with GitHub PR .* for development/ for development/' \ - -e '/;,\;; d' \ -e 's;#L[0-9]*";";' \ -e 's;tab-set--[0-9]*-;tab-set-;' \