chore: use leanprover/lean4#3226

.github/workflows/build.yml

@@ -59,17 +59,10 @@ jobs:
         if: github.ref_type == 'tag'
         uses: softprops/action-gh-release@v1
 
-      # TODO: replace with just `lake upload $RELEASE_TAG` when lean4#2713 is fixed
-      # References:
-      # https://docs.github.com/en/actions/learn-github-actions/contexts#runner-context
-      # https://stackoverflow.com/questions/8766730/tar-command-in-mac-os-x-adding-hidden-files-why
       - name: Upload release archive
         if: github.ref_type == 'tag'
-        # All our runners are 64-bit ¯\_(ツ)_/¯
         run: |
-          export COPYFILE_DISABLE=true
-          tar -c -z -f ./${LEAN_OS}-64.tar.gz -C ./.lake/build .
-          gh release upload ${RELEASE_TAG} ./${LEAN_OS}-64.tar.gz
+          lake upload $RELEASE_TAG
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
           RELEASE_TAG: ${{ github.ref_name }}

lakefile.lean

@@ -3,6 +3,7 @@ open Lake DSL System
 
 package proofwidgets where
   preferReleaseBuild := true
+  buildArchive := "ProofWidgets4.tar.gz"
 
 lean_lib ProofWidgets
 

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2024-01-23
+leanprover/lean4-pr-releases:pr-release-3226