merge upstream/nightly-with-mathlib

Author: Kha

.github/workflows/check-stage0.yml

@@ -11,8 +11,8 @@ jobs:
     - uses: actions/checkout@v5
       with:
         ref: ${{ github.event.pull_request.head.sha }}
-        filter: blob:none
         fetch-depth: 0
+        filter: tree:0
 
     - name: Find base commit
       if: github.event_name == 'pull_request'

.github/workflows/ci.yml

@@ -404,6 +404,8 @@ jobs:
         with:
           # needed for tagging
           fetch-depth: 0
+          # Doesn't seem to be working when additionally fetching from lean4-nightly
+          #filter: tree:0
           token: ${{ secrets.PUSH_NIGHTLY_TOKEN }}
       - uses: actions/download-artifact@v5
         with:

.github/workflows/pr-release.yml

@@ -48,17 +48,17 @@ jobs:
           git -C lean4.git remote add origin https://github.com/${{ github.repository_owner }}/lean4.git
           git -C lean4.git fetch -n origin master
           git -C lean4.git fetch -n origin "${{ steps.workflow-info.outputs.sourceHeadSha }}"
-          
+
           # Create both the original tag and the SHA-suffixed tag
           SHORT_SHA="${{ steps.workflow-info.outputs.sourceHeadSha }}"
           SHORT_SHA="${SHORT_SHA:0:7}"
-          
+
           # Export the short SHA for use in subsequent steps
           echo "SHORT_SHA=${SHORT_SHA}" >> "$GITHUB_ENV"
 
           git -C lean4.git tag -f pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} "${{ steps.workflow-info.outputs.sourceHeadSha }}"
           git -C lean4.git tag -f pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-"${SHORT_SHA}" "${{ steps.workflow-info.outputs.sourceHeadSha }}"
-          
+
           git -C lean4.git remote add pr-releases https://foo:'${{ secrets.PR_RELEASES_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-pr-releases.git
           git -C lean4.git push -f pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}
           git -C lean4.git push -f pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-"${SHORT_SHA}"
@@ -200,7 +200,7 @@ jobs:
                           -H "Accept: application/vnd.github.v3+json" \
                           "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/labels" \
                           | jq -r '.[].name')"
-            
+
             if echo "$LABELS" | grep -q "^force-mathlib-ci$"; then
               echo "force-mathlib-ci label detected, forcing CI despite issues"
               MESSAGE="Forcing Mathlib CI because the \`force-mathlib-ci\` label is present, despite problem: $MESSAGE"
@@ -301,7 +301,7 @@ jobs:
                           -H "Accept: application/vnd.github.v3+json" \
                           "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/labels" \
                           | jq -r '.[].name')"
-            
+
             if echo "$LABELS" | grep -q "^force-manual-ci$"; then
               echo "force-manual-ci label detected, forcing CI despite issues"
               MESSAGE="Forcing reference manual CI because the \`force-manual-ci\` label is present, despite problem: $MESSAGE"
@@ -401,6 +401,7 @@ jobs:
           token: ${{ secrets.MATHLIB4_BOT }}
           ref: nightly-testing
           fetch-depth: 0 # This ensures we check out all tags and branches.
+          filter: tree:0
 
       - name: Check if tag exists
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
@@ -460,6 +461,7 @@ jobs:
           token: ${{ secrets.MATHLIB4_BOT }}
           ref: nightly-testing
           fetch-depth: 0 # This ensures we check out all tags and branches.
+          filter: tree:0
 
       - name: install elan
         run: |
@@ -530,6 +532,7 @@ jobs:
           token: ${{ secrets.MANUAL_PR_BOT }}
           ref: nightly-testing
           fetch-depth: 0 # This ensures we check out all tags and branches.
+          filter: tree:0
 
       - name: Check if tag in reference manual exists
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.reference-manual-ready.outputs.manual_ready == 'true'

src/Init/Data/ByteArray/Lemmas.lean

@@ -256,3 +256,19 @@ theorem ByteArray.copySlice_eq_append {src : ByteArray} {srcOff : Nat} {dest : B
       dest.extract 0 destOff ++ src.extract srcOff (srcOff +len) ++ dest.extract (destOff + min len (src.data.size - srcOff)) dest.data.size := by
   ext1
   simp [copySlice]
+
+@[simp]
+theorem ByteArray.data_set {as : ByteArray} {i : Nat} {h : i < as.size} {a : UInt8} :
+    (as.set i a h).data = as.data.set i a (by simpa) := by
+  simp [set]
+
+theorem ByteArray.set_eq_push_extract_append_extract {as : ByteArray} {i : Nat} (h : i < as.size) {a : UInt8} :
+    as.set i a h = (as.extract 0 i).push a ++ as.extract (i + 1) as.size := by
+  ext1
+  simpa using Array.set_eq_push_extract_append_extract _
+
+@[simp]
+theorem ByteArray.append_toByteArray_singleton {as : ByteArray} {a : UInt8} :
+    as ++ [a].toByteArray = as.push a := by
+  ext1
+  simp