chore(script): fix nightlies... finally?

.appveyor.yml

@@ -33,11 +33,17 @@ build_script:
 
 test_script:
   - C:\msys64\usr\bin\bash -lc "exec 0</dev/null && cd $APPVEYOR_BUILD_FOLDER/build && ctest -j4 --output-on-failure"
+  # don't test packages when building nightly
   - C:\msys64\usr\bin\bash -lc "exec 0</dev/null && cd $APPVEYOR_BUILD_FOLDER/packages &&
-      ../bin/leanpkg configure &&
-      for d in _target/deps/*; do (cd $d; ../../../../bin/leanpkg test || exit 1); done"
+      if [[ ! -f ../build/nightly.sh ]]; then
+        ../bin/leanpkg configure &&
+        for d in _target/deps/*; do (cd $d; ../../../../bin/leanpkg test || exit 1); done;
+      fi"
   - C:\msys64\usr\bin\bash -lc "exec 0</dev/null && cd $APPVEYOR_BUILD_FOLDER &&
-      if [[ $UPLOAD == ON && $GH_TOKEN && $APPVEYOR_BRANCH == master ]]; then bash script/deploy_nightly.sh build/lean-*-windows.zip; fi"
+      if [[ $UPLOAD == ON && $GH_TOKEN && $APPVEYOR_BRANCH == master ]]; then
+        . build/nightly.sh &&
+        bash script/deploy_nightly.sh build/lean-*-windows.zip;
+      fi"
 
 artifacts:
   - path: build\lean-*-windows.zip

.travis.yml

@@ -119,7 +119,10 @@ script:
   - if [[ $STATIC != ON ]]; then STATIC=OFF; fi
   - if [[ $MULTI_THREAD != OFF ]]; then MULTI_THREAD=ON; fi
   - OPTIONS=""
-  - if [[ $TRAVIS_EVENT_TYPE == cron ]]; then . ../script/setup_nightly.sh; fi
+  - if [[ $TRAVIS_EVENT_TYPE == cron ]]; then
+      git fetch --unshallow --tags origin &&
+      . ../script/setup_nightly.sh;
+    fi
   - cmake -DCMAKE_BUILD_TYPE=$CMAKE_BUILD_TYPE
           -DCMAKE_CXX_COMPILER=$CMAKE_CXX_COMPILER
           -DTESTCOV=$TESTCOV
@@ -140,7 +143,7 @@ script:
        for d in _target/deps/*; do (cd $d; ../../../../bin/leanpkg test); done)
     fi
   - if [[ $UPLOAD == ON ]]; then cpack; fi
-  - if [[ $UPLOAD == ON && $GH_TOKEN && $TRAVIS_PULL_REQUEST == false && $TRAVIS_BRANCH == master ]]; then (cd ..; bash script/deploy_nightly.sh build/lean-* && bash script/deploy_gh_pages.sh); fi
+  - if [[ $UPLOAD == ON && $GH_TOKEN && $TRAVIS_PULL_REQUEST == false && $TRAVIS_BRANCH == master ]]; then (cd ..; bash script/deploy_nightly.sh build/lean-*); fi
   - cd ..
 
 after_script:

script/deploy_gh_pages.sh

@@ -1,20 +0,0 @@
-#!/bin/bash
-# LEGACY binary in gh-pages branch. Remove when test scripts are changed to use versioned nightlies.
-# inspired by https://github.com/steveklabnik/automatically_update_github_pages_with_travis_example
-
-set -eu
-
-rev=$(git rev-parse --short HEAD)
-
-git clone -b gh-pages "https://$GH_TOKEN@github.com/leanprover/lean-nightly.git" gh-pages
-cd gh-pages
-
-mkdir -p build
-ln -f ../build/lean-* build/
-
-git config user.name "Bot Botson"
-git config user.email "bot@bot.bot"
-
-git add -A .
-git commit --amend --reset-author -m "nightly build at ${rev}"
-git push -fq

script/deploy_nightly.sh

@@ -2,24 +2,33 @@
 
 set -exu
 
-[ -z $LEAN_VERSION_STRING] && exit 0
+[ -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
-GO_PATH=$(realpath go)
-PATH=$PATH:$GO_PATH/bin
+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
-    # technically a race condition...
-    git push nightly $LEAN_VERSION_STRING
     last_tag=$(git describe @^ --abbrev=0 --tags)
     echo -e "Changes since ${last_tag}:\n\n" > diff.md
-    ./script/diff_changelogs.py <(git show $last_tag:doc/changes.md) doc/changes.md >> diff.md
+    git show $last_tag:doc/changes.md > old.md
+    ./script/diff_changelogs.py old.md doc/changes.md >> 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 parse-rev HEAD) == $(git parse-rev $LEAN_VERSION_STRING) ] || exit 1
+    [ $(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/diff_changelogs.py

@@ -1,4 +1,4 @@
-#! /bin/env python3
+#!/usr/bin/env python3
 
 import collections
 import re

script/setup_nightly.sh

@@ -1,13 +1,18 @@
-#!/bin/bash
-
-set -exu
+#!/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 -uI)"
+
 # do nothing if commit is already tagged
-if [ ! git describe --exact-match --tags HEAD >& /dev/null ]
+if git checkout $LEAN_VERSION_STRING || ! git name-rev --name-only --tags --no-undefined HEAD
 then
-    LEAN_VERSION_STRING="nightly-$(date -uI)"
+    # 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"
 fi