chore: nightly releases

.github/workflows/ci.yml

@@ -8,6 +8,8 @@ on:
   pull_request:
     branches:
       - master
+  schedule:
+    - cron: '0 0 * * *'
 
 jobs:
   Build:
@@ -54,6 +56,9 @@ jobs:
     steps:
       - name: Checkout
         uses: actions/checkout@v2
+        with:
+          # interferes with lean4-nightly authentication
+          persist-credentials: false
       - name: Install Nix
         uses: cachix/install-nix-action@v12
         with:
@@ -86,7 +91,18 @@ jobs:
         run: |
           mkdir build
           cd build
-          cmake .. ${{ matrix.CMAKE_OPTIONS }}
+          OPTIONS=
+          if [[ $GITHUB_EVENT_NAME == 'schedule' && -n '${{ matrix.release }}' && -n '${{ secrets.PUSH_NIGHTLY_TOKEN }}' ]]; then
+            git remote add nightly https://foo:${{ secrets.PUSH_NIGHTLY_TOKEN }}@github.com/${{ github.repository_owner }}/lean4-nightly.git
+            git fetch nightly --tags
+            LEAN_VERSION_STRING="nightly-$(date -u +%F)"
+            # do nothing if commit is already tagged
+            if ! git name-rev --name-only --tags --no-undefined HEAD; then
+              OPTIONS=-DLEAN_SPECIAL_VERSION_DESC=$LEAN_VERSION_STRING
+              echo "LEAN_VERSION_STRING=$LEAN_VERSION_STRING" >> $GITHUB_ENV
+            fi
+          fi
+          cmake .. ${{ matrix.CMAKE_OPTIONS }} $OPTIONS
           make -j4
       # de-Nix-ify binaries
       - name: Patch
@@ -143,3 +159,33 @@ jobs:
           files: build/stage1/lean-*
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+      - name: Prepare Nightly Release
+        if: env.LEAN_VERSION_STRING
+        run: |
+          # can't push shallow checkout
+          git fetch --unshallow
+          git fetch nightly --tags
+          if git tag $LEAN_VERSION_STRING && git push nightly $LEAN_VERSION_STRING; then
+            last_tag=$(git describe HEAD^ --abbrev=0 --tags)
+            echo -e "Changes since ${last_tag}:\n\n" > diff.md
+            #git show $last_tag:doc/changes.md > old.md
+            #./script/diff_changelogs.py old.md doc/changes.md >> diff.md
+            echo -e "*Full commit log*\n" >> diff.md
+            git log --oneline $last_tag..HEAD | sed 's/^/* /' >> diff.md
+          else
+            # make sure every runner is building the same commit
+            [ $(git rev-parse HEAD) == $(git rev-parse $LEAN_VERSION_STRING) ] || exit 11
+            echo -n > diff.md
+          fi
+      - name: Release Nightly
+        # need unreleased version for fixed `repository`
+        uses: Kha/action-gh-release@master
+        if: env.LEAN_VERSION_STRING
+        with:
+          body_path: diff.md
+          prerelease: true
+          files: build/stage1/lean-*
+          tag_name: ${{ env.LEAN_VERSION_STRING }}
+          repository: ${{ github.repository_owner }}/lean4-nightly
+        env:
+          GITHUB_TOKEN: ${{ secrets.PUSH_NIGHTLY_TOKEN }}

script/deploy_nightly.sh

@@ -1,36 +0,0 @@
-#!/bin/bash
-
-set -exu
-
-[ -z ${LEAN_VERSION_STRING+x} ] && exit 0
-
-if command -v greadlink >/dev/null 2>&1; then
-    # macOS readlink doesn't support -f option
-    READLINK=greadlink
-else
-    READLINK=readlink
-fi
-
-# Travis can't publish releases to other repos (or stop mucking with the markdown description), so push releases directly
-export GOPATH=$($READLINK -f go)
-PATH=$PATH:$GOPATH/bin
-go get github.com/itchio/gothub
-
-# technically a race condition...
-git fetch nightly --tags
-if git tag $LEAN_VERSION_STRING
-then
-    last_tag=$(git describe @^ --abbrev=0 --tags)
-    echo -e "Changes since ${last_tag}:\n\n" > diff.md
-    git show $last_tag:doc/changes.md > old.md
-    ./script/diff_changelogs.py old.md doc/changes.md >> diff.md
-    echo -e "*Full commit log*\n" >> diff.md
-    git log --oneline $last_tag..HEAD | sed 's/^/* /' >> diff.md
-    git push nightly $LEAN_VERSION_STRING
-    gothub release -s $GH_TOKEN -u leanprover -r lean-nightly -t $LEAN_VERSION_STRING -d - --pre-release < diff.md
-else
-    # make sure every runner is building the same commit
-    [ $(git rev-parse HEAD) == $(git rev-parse $LEAN_VERSION_STRING) ] || exit 1
-fi
-
-gothub upload -s $GH_TOKEN -u leanprover -r lean-nightly -t $LEAN_VERSION_STRING -n "$(basename $1)" -f "$1"

script/setup_nightly.sh

@@ -1,20 +0,0 @@
-#!/bin/false
-# script should be sourced
-
-git remote add nightly "https://$GH_TOKEN@github.com/leanprover/lean-nightly.git"
-git fetch nightly --tags
-
-export LEAN_VERSION_STRING="nightly-$(date -u +%F)"
-
-# do nothing if commit is already tagged
-if git checkout $LEAN_VERSION_STRING || ! git name-rev --name-only --tags --no-undefined HEAD
-then
-    # write into file since we repeatedly open and close shells on AppVeyor
-    cat <<EOF > ./nightly.sh
-export LEAN_VERSION_STRING=$LEAN_VERSION_STRING
-EOF
-    . ./nightly.sh
-    OPTIONS+=" -DLEAN_SPECIAL_VERSION_DESC=$LEAN_VERSION_STRING"
-else
-    unset LEAN_VERSION_STRING
-fi