diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index ae4939f87f..b74a36e66e 100644 --- a/.github/workflows/ci.yml +++ b/.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 }} diff --git a/script/deploy_nightly.sh b/script/deploy_nightly.sh deleted file mode 100644 index 9c4313171c..0000000000 --- a/script/deploy_nightly.sh +++ /dev/null @@ -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" diff --git a/script/setup_nightly.sh b/script/setup_nightly.sh deleted file mode 100755 index 44b8e2d18e..0000000000 --- a/script/setup_nightly.sh +++ /dev/null @@ -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 < ./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