diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 37e7f5f..c0d4153 100644
--- a/.github/workflows/build.yml
+++ b/.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 }}
diff --git a/lakefile.lean b/lakefile.lean
index e2d775d..a59cac3 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -3,6 +3,7 @@ open Lake DSL System
 
 package proofwidgets where
   preferReleaseBuild := true
+  buildArchive := "ProofWidgets4.tar.gz"
 
 lean_lib ProofWidgets
 
diff --git a/lean-toolchain b/lean-toolchain
index b39e212..6ad2314 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-01-23
+leanprover/lean4-pr-releases:pr-release-3226