chore: update CI to create official releases (#2472)

.github/workflows/ci.yml

@@ -39,8 +39,41 @@ jobs:
             fi
           fi
 
+  # This job determines if this CI build is for a tagged release.
+  # It only runs when a tag is pushed to the `leanprover` repository.
+  # It sets `set-release.outputs.RELEASE_TAG` to the tag, if the tag is "v" followed by a valid semver,
+  # and sets `set-release.outputs.{LEAN_VERSION_MAJOR,LEAN_VERSION_MINOR,LEAN_VERSION_PATCH,LEAN_SPECIAL_VERSION_DESC}`
+  # to the semver components parsed via regex.
+  set-release:
+    runs-on: ubuntu-latest
+    outputs:
+      LEAN_VERSION_MAJOR: ${{ steps.set.outputs.LEAN_VERSION_MAJOR }}
+      LEAN_VERSION_MINOR: ${{ steps.set.outputs.LEAN_VERSION_MINOR }}
+      LEAN_VERSION_PATCH: ${{ steps.set.outputs.LEAN_VERSION_PATCH }}
+      LEAN_SPECIAL_VERSION_DESC: ${{ steps.set.outputs.LEAN_SPECIAL_VERSION_DESC }}
+      RELEASE_TAG: ${{ steps.set.outputs.RELEASE_TAG }}
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v3
+        if: startsWith(github.ref, 'refs/tags/') && github.repository == 'leanprover/lean4'
+      - name: Check for official release
+        if: startsWith(github.ref, 'refs/tags/') && github.repository == 'leanprover/lean4'
+        id: set
+        run: |
+          TAG_NAME=${GITHUB_REF##*/}
+          # From https://semver.org/#is-there-a-suggested-regular-expression-regex-to-check-a-semver-string
+          # with "v" prepended.
+          SEMVER_REGEX="^v(0|[1-9]\d*)\.(0|[1-9]\d*)\.(0|[1-9]\d*)(?:-((?:0|[1-9]\d*|\d*[a-zA-Z-][0-9a-zA-Z-]*)(?:\.(?:0|[1-9]\d*|\d*[a-zA-Z-][0-9a-zA-Z-]*))*))?(?:\+([0-9a-zA-Z-]+(?:\.[0-9a-zA-Z-]+)*))?$"
+          if [[ ${TAG_NAME} =~ ${SEMVER_REGEX} ]]; then
+            echo "LEAN_VERSION_MAJOR=${BASH_REMATCH[1]}" >> $GITHUB_OUTPUT
+            echo "LEAN_VERSION_MINOR=${BASH_REMATCH[2]}" >> $GITHUB_OUTPUT
+            echo "LEAN_VERSION_PATCH=${BASH_REMATCH[3]}" >> $GITHUB_OUTPUT
+            echo "LEAN_SPECIAL_VERSION_DESC=${BASH_REMATCH[4]}" >> $GITHUB_OUTPUT
+            echo "RELEASE_TAG=$TAG_NAME" >> $GITHUB_OUTPUT
+          fi
+
   build:
-    needs: set-nightly
+    needs: [set-nightly, set-release]
     if: github.event_name != 'schedule' || github.repository == 'leanprover/lean4'
     runs-on: ${{ matrix.os }}
     defaults:
@@ -190,6 +223,13 @@ jobs:
           if [[ -n '${{ matrix.release }}' && -n '${{ needs.set-nightly.outputs.nightly }}' ]]; then
             OPTIONS+=(-DLEAN_SPECIAL_VERSION_DESC=${{ needs.set-nightly.outputs.nightly }})
           fi
+          if [[ -n '${{ matrix.release }}' && -n '${{ needs.set-release.outputs.RELEASE_TAG }}' ]]; then
+            OPTIONS+=(-DLEAN_VERSION_MAJOR=${{ needs.set-release.outputs.LEAN_VERSION_MAJOR }})
+            OPTIONS+=(-DLEAN_VERSION_MINOR=${{ needs.set-release.outputs.LEAN_VERSION_MINOR }})
+            OPTIONS+=(-DLEAN_VERSION_PATCH=${{ needs.set-release.outputs.LEAN_VERSION_PATCH }})
+            OPTIONS+=(-DLEAN_VERSION_IS_RELEASE=1)
+            OPTIONS+=(-DLEAN_SPECIAL_VERSION_DESC=${{ needs.set-release.outputs.LEAN_SPECIAL_VERSION_DESC }})
+          fi
           # contortion to support empty OPTIONS with old macOS bash
           cmake .. ${{ matrix.CMAKE_OPTIONS }} ${OPTIONS[@]+"${OPTIONS[@]}"} -DLEAN_INSTALL_PREFIX=$PWD/..
           make -j4
@@ -205,7 +245,7 @@ jobs:
           dir=$(echo lean-*)
           mkdir pack
           # high-compression tar.zst + zip for release, fast tar.zst otherwise
-          if [[ '${{ startsWith(github.ref, 'refs/tags/') && matrix.release }}' == true || -n '${{ needs.set-nightly.outputs.nightly }}' ]]; then
+          if [[ '${{ startsWith(github.ref, 'refs/tags/') && matrix.release }}' == true || -n '${{ needs.set-nightly.outputs.nightly }}' || -n '${{ needs.set-release.outputs.RELEASE_TAG }}' ]]; then
             ${{ matrix.tar || 'tar' }} cf - $dir | zstd -T0 --no-progress -19 -o pack/$dir.tar.zst
             zip -rq pack/$dir.zip $dir
           else
@@ -278,6 +318,10 @@ jobs:
             ./build/stage2/bin/lean
             ./build/stage2/lib/lean/libleanshared.so
 
+  # This job creates releases from tags
+  # (whether they are "unofficial" releases for experiments, or official releases when the tag is "v" followed by a semver string.)
+  # We do not attempt to automatically construct a changelog here:
+  # unofficial releases don't need them, and official release notes will be written by a human.
   release:
     if: startsWith(github.ref, 'refs/tags/')
     runs-on: ubuntu-latest
@@ -294,6 +338,8 @@ jobs:
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
 
+  # This job creates nightly releases during the cron job.
+  # It is responsible for creating the tag, and automatically generating a changelog.
   release-nightly:
     needs: [set-nightly, build]
     if: needs.set-nightly.outputs.nightly