Merge branch 'develop' into sparse-7.6.0

sagemath · Aug 19, 2024 · 8d35222 · 8d35222
2 parents 4ff5ea8 + e042294
commit 8d35222
Show file tree

Hide file tree

Showing 5,394 changed files with 169,623 additions and 678,978 deletions.
diff --git a/.ci/create-changes-html.sh b/.ci/create-changes-html.sh
@@ -8,8 +8,6 @@ fi
 BASE_DOC_COMMIT="$1"
 DOC_REPOSITORY="$2"
 
-# Wipe out chronic diffs between old doc and new doc
-(cd $DOC_REPOSITORY && find . -name "*.html" | xargs sed -i -e '\;<script type="application/vnd\.jupyter\.widget-state+json">;,\;</script>; d')
 # Create CHANGES.html
 echo '<html>' > CHANGES.html
 echo '<head>' >> CHANGES.html
@@ -19,74 +17,89 @@ echo '<script>hljs.highlightAll();</script>' >> CHANGES.html
 cat >> CHANGES.html << EOF
 <script>
 document.addEventListener('DOMContentLoaded', () => {
+// This URL is hardcoded in the file .github/workflows/doc-publish.yml.
+// See NETLIFY_ALIAS of the "Deploy to Netlify" step.
+const baseDocURL = 'https://doc-develop--sagemath.netlify.app'
 const diffSite = 'https://pianomister.github.io/diffsite'
-const baseDocURL = 'https://sagemath-tobias.netlify.app'
 const diffParagraphs = document.querySelectorAll('p.diff');
 diffParagraphs.forEach(paragraph => {
   const rootURL = window.location.origin;
-  const docAnchor = paragraph.querySelector('a');  // first "a" element
+  const docAnchor = paragraph.querySelector('a');
   const url = new URL(docAnchor.href);
   const path = url.pathname;
   const anchor = document.createElement('a');
   anchor.href = diffSite + '/?url1=' + rootURL + path + '&url2=' + baseDocURL + path;
   anchor.textContent = 'compare with the base';
   anchor.setAttribute('target', '_blank');
+  paragraph.innerHTML += '&nbsp;&nbsp;';
   paragraph.appendChild(anchor);
-  paragraph.innerHTML += '&nbsp;';
-  const hunkAnchors = paragraph.querySelectorAll('a.hunk');
-  hunkAnchors.forEach(hunkAnchor => {
+  const hunks = paragraph.parentNode.querySelectorAll('p.hunk');
+  hunks.forEach(hunk => {
+    const hunkAnchor = hunk.querySelector('a');
     const url = new URL(hunkAnchor.href);
     const path = url.pathname;
     const pathHash = path + url.hash.replace('#', '%23');
     const anchor = document.createElement('a');
     anchor.href = diffSite + '/?url1=' + rootURL + pathHash + '&url2=' + baseDocURL + path;
-    anchor.textContent = hunkAnchor.textContent;
+    anchor.textContent = 'compare with the base';
     anchor.setAttribute('target', '_blank');
-    paragraph.appendChild(anchor);
-    paragraph.innerHTML += '&nbsp;';
+    hunk.innerHTML += '&nbsp;&nbsp;';
+    hunk.appendChild(anchor);
   });
 });
 });
 </script>
 EOF
 echo '</head>' >> CHANGES.html
 echo '<body>' >> CHANGES.html
-(cd $DOC_REPOSITORY && git diff $BASE_DOC_COMMIT -- *.html) > diff.txt
+(cd $DOC_REPOSITORY && git diff $BASE_DOC_COMMIT -- "*.html") > diff.txt
 python3 - << EOF
 import os, re, html
+from itertools import chain
 with open('diff.txt', 'r') as f:
     diff_text = f.read()
 diff_blocks = re.split(r'^(?=diff --git)', diff_text, flags=re.MULTILINE)
 out_blocks = []
 for block in diff_blocks:
     match = re.search(r'^diff --git a/(.*) b/\1', block, flags=re.MULTILINE)
     if match:
-        doc = match.group(1)
-        file_path = os.path.join('$DOC_REPOSITORY', doc)
+        path = match.group(1)
+        file_path = os.path.join('$DOC_REPOSITORY', path)
         try:
             with open(file_path, 'r') as file:
                 content = file.readlines()
         except FileNotFoundError:
             content = []
         count = 0
+        hunks = []
+        hunk_lines = []
+        in_hunk = False
         for line in block.splitlines():
             if line.startswith('@@ -'):
+                if hunk_lines:
+                    hunks.append('<pre><code class="language-diff">'
+                                 + html.escape('\n'.join(hunk_lines)).strip()
+                                 + '</code></pre>')
+                    hunk_lines = []
                 search_result = re.search(r'@@ -(\d+),(\d+) \+(\d+),(\d+)', line)
                 if search_result:
                     line_number = int(search_result.group(3))
-                    for i in range(line_number - 1, -1, -1):
-                        if content[i].startswith('<'):
+                    span = int(search_result.group(4))
+                    for i in chain(range(line_number, line_number + span), range(line_number - 1, -1, -1)):
+                        if content[i].startswith('<') and not content[i].startswith('</'):
                             count += 1
                             content[i] = f'<span id="hunk{count}" style="visibility: hidden;"></span>' + content[i]
+                            hunks.append(f'<p class="hunk"><a href="{path}#hunk{count}" class="hunk" target="_blank">hunk #{count}</a></p>')
                             break
+            hunk_lines.append(line)
+        if hunk_lines:
+            hunks.append('<pre><code class="language-diff">'
+                          + html.escape('\n'.join(hunk_lines)).strip()
+                          + '</code></pre>')
         if content:
             with open(file_path, 'w') as file:
                 file.writelines(content)
-        path = 'html/' + doc
-        hunks = '&nbsp;'.join(f'<a href="{path}#hunk{i+1}" class="hunk" target="_blank">#{i + 1}</a>' for i in range(count))
-        out_blocks.append(f'<p class="diff"><a href="{path}">{doc}</a>&nbsp;' + hunks + '&emsp;</p>'
-                            + '\n<pre><code class="language-diff">'
-                            + html.escape(block).strip() + '</code></pre>')
+        out_blocks.append(f'<div class="diff"><p class="diff"><a href="{path}">{path}</a></p>\n' + '\n'.join(hunks) + '\n</div>')
 output_text = '\n'.join(out_blocks)
 with open('diff.html', 'w') as f:
     f.write(output_text)

diff --git a/.ci/docker-exec-script.sh b/.ci/docker-exec-script.sh
@@ -0,0 +1,14 @@
+#!/bin/sh -x
+if [ $# -lt 3 ]; then
+    echo >&2 "usage: docker-exec-script.sh CONTAINER WORKDIR [VAR=VALUE...] SCRIPT"
+    exit 1
+fi
+CONTAINER=$1
+WORKDIR=$2
+shift 2
+(echo "cd \"$WORKDIR\"";
+ while [ $# -gt 1 ]; do
+     echo "export \"$1\""
+     shift
+ done;
+ cat "$1") | docker exec -i $CONTAINER bash -ex
diff --git a/.ci/merge-fixes.sh b/.ci/merge-fixes.sh
@@ -1,5 +1,8 @@
 #!/bin/sh
-# Apply open PRs labeled "blocker" from sagemath/sage as patches.
+# Apply open PRs labeled "p: CI Fix" from sagemath/sage as patches.
+# (policy set by vote in 2024-03,
+#  https://groups.google.com/g/sage-devel/c/OKwwUGyKveo/m/vpyCXYBqAAAJ)
+#
 # This script is invoked by various workflows in .github/workflows
 #
 # The repository variable SAGE_CI_FIXES_FROM_REPOS can be set
@@ -20,15 +23,15 @@ for REPO in ${SAGE_CI_FIXES_FROM_REPOSITORIES:-sagemath/sage}; do
             echo "Nothing to do for 'none' in SAGE_CI_FIXES_FROM_REPOSITORIES"
             ;;
         */*)
-            echo "Getting open PRs with 'blocker' status from https://github.com/$REPO/pulls?q=is%3Aopen+label%3A%22p%3A+blocker+%2F+1%22"
+            echo "Getting open PRs with 'p: CI Fix' label from https://github.com/$REPO/pulls?q=is%3Aopen+label%3A%22p%3A+CI+Fix%22"
             GH="gh -R $REPO"
             REPO_FILE="upstream/ci-fixes-${REPO%%/*}-${REPO##*/}"
-            PRs="$($GH pr list --label "p: blocker / 1" --json number --jq '.[].number' | tee $REPO_FILE)"
+            PRs="$($GH pr list --label "p: CI Fix" --json number --jq '.[].number' | tee $REPO_FILE)"
             date -u +"%Y-%m-%dT%H:%M:%SZ" > $REPO_FILE.date  # Record the date, for future reference
             if [ -z "$PRs" ]; then
-                echo "Nothing to do: Found no open PRs with 'blocker' status in $REPO."
+                echo "Nothing to do: Found no open PRs with 'p: CI Fix' label in $REPO."
             else
-                echo "Found open PRs with 'blocker' status in $REPO: $(echo $PRs)"
+                echo "Found open PRs with 'p: CI Fix' label in $REPO: $(echo $PRs)"
                 git tag -f test_base
                 git commit -q -m "Uncommitted changes" --no-allow-empty -a
                 for a in $PRs; do
@@ -42,6 +45,7 @@ for REPO in ${SAGE_CI_FIXES_FROM_REPOSITORIES:-sagemath/sage}; do
                     # Considered alternative: Use https://github.com/$REPO/pull/$a.diff,
                     # which squashes everything into one diff without commit metadata.
                     PULL_URL="https://github.com/$REPO/pull/$a"
+                    PULL_SHORT="$REPO#$a"
                     PULL_FILE="$REPO_FILE-$a"
                     PATH=build/bin:$PATH build/bin/sage-download-file --quiet "$PULL_URL.patch" $PULL_FILE.patch
                     date -u +"%Y-%m-%dT%H:%M:%SZ" > $PULL_FILE.date  # Record the date, for future reference
@@ -67,7 +71,7 @@ for REPO in ${SAGE_CI_FIXES_FROM_REPOSITORIES:-sagemath/sage}; do
                         git am --signoff --show-current-patch=diff
                         echo "--------------------------------------------------------------------8<-----------------------------"
                         echo "::endgroup::"
-                        echo "Failure applying $PULL_URL as a patch, resetting"
+                        echo "Failure applying $PULL_SHORT as a patch, resetting"
                         git am --signoff --abort
                     fi
                 done

diff --git a/.ci/retrofit-worktree.sh b/.ci/retrofit-worktree.sh
@@ -12,32 +12,35 @@ export GIT_AUTHOR_EMAIL="[email protected]"
 export GIT_COMMITTER_NAME="$GIT_AUTHOR_NAME"
 export GIT_COMMITTER_EMAIL="$GIT_AUTHOR_EMAIL"
 
+set -e
+
 # Set globally for other parts of the workflow
 git config --global user.name "$GIT_AUTHOR_NAME"
 git config --global user.email "$GIT_AUTHOR_EMAIL"
 
-set -ex
+set -x
 
 # If actions/checkout downloaded our source tree using the GitHub REST API
 # instead of with git (because do not have git installed in our image),
 # we first make the source tree a repo.
-if [ ! -d .git ]; then git init && git add -A && git commit --quiet -m "new"; fi
+if [ ! -d .git ]; then git init; fi
 
-# Tag this state of the source tree "new". This is what we want to build and test.
+# Commit and tag this state of the source tree "new". This is what we want to build and test.
+git add -A && git commit --quiet --allow-empty -m "new"
 git tag -f new
 
 # Our container image contains a source tree in $WORKTREE_DIRECTORY with a full build of Sage.
 # But $WORKTREE_DIRECTORY is not a git repository.
 # We make $WORKTREE_DIRECTORY a worktree whose index is at tag "new".
 # We then commit the current sources and set the tag "old". (This keeps all mtimes unchanged.)
-# Then we update worktree and index with "git reset --hard new".
+# Then we update worktree and index with "git checkout new".
 # (This keeps mtimes of unchanged files unchanged and mtimes of changed files newer than unchanged files.)
-# Finally we reset the index to "old". (This keeps all mtimes unchanged.)
-# The changed files now show up as uncommitted changes.
-# The final "git add -N" makes sure that files that were added in "new" do not show
-# as untracked files, which would be removed by "git clean -fx".
+if [ -L $WORKTREE_NAME ]; then
+    rm -f $WORKTREE_NAME
+fi
+git worktree prune --verbose
 git worktree add --detach $WORKTREE_NAME
 rm -rf $WORKTREE_DIRECTORY/.git && mv $WORKTREE_NAME/.git $WORKTREE_DIRECTORY/
 rm -rf $WORKTREE_NAME && ln -s $WORKTREE_DIRECTORY $WORKTREE_NAME
 if [ ! -f $WORKTREE_NAME/.gitignore ]; then cp .gitignore $WORKTREE_NAME/; fi
-(cd $WORKTREE_NAME && git add -A && git commit --quiet --allow-empty -m "old" -a && git tag -f old && git reset --hard new && git reset --quiet old && git add -N . && git status)
+(cd $WORKTREE_NAME && git add -A && git commit --quiet --allow-empty -m "old" -a && git tag -f old && git checkout new && git status)