From e24735571ac7271ff502ea6221c57766688c688a Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sun, 11 Mar 2018 19:50:16 +0100
Subject: [PATCH] chore(.appveyor.yml,.travis.yml): use daily cron job for
 nightlies instead of first commit of the day

This makes sure the latest commit will always be included in a nightly after at
most 24 hours
---
 .appveyor.yml             |  4 ++--
 .travis.yml               |  4 ++--
 script/deploy_gh_pages.sh | 20 +++++++++++++++++++
 script/deploy_nightly.sh  | 42 +--------------------------------------
 script/setup_nightly.sh   | 28 ++++++++++++++++++++++++++
 5 files changed, 53 insertions(+), 45 deletions(-)
 create mode 100644 script/deploy_gh_pages.sh
 create mode 100644 script/setup_nightly.sh

diff --git a/.appveyor.yml b/.appveyor.yml
index f080f241a9..6b8671c1f6 100644
--- a/.appveyor.yml
+++ b/.appveyor.yml
@@ -26,7 +26,7 @@ build_script:
       cmake --build .)
   - if %CFG% == MINGW64 (C:\msys64\usr\bin\bash -lc "exec 0</dev/null && cd $APPVEYOR_BUILD_FOLDER/build &&
       OPTIONS='';
-      if [[ $APPVEYOR_REPO_TAG != true ]]; then OPTIONS+='-DLEAN_VERSION_STRING=nightly-${date -uI}'; fi;
+      if [[ $APPVEYOR_SCHEDULED_BUILD == True ]]; then . ./script/setup_nightly.sh; fi &&
       cmake ../src -DINCLUDE_MSYS2_DLLS=ON -DCMAKE_BUILD_TYPE=Release $OPTIONS -G 'Unix Makefiles' &&
       cmake --build . &&
       cpack")
@@ -37,7 +37,7 @@ test_script:
       ../bin/leanpkg configure &&
       for d in _target/deps/*; do (cd $d; ../../../../bin/leanpkg test || exit 1); done"
   - 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; fi"
+      if [[ $UPLOAD == ON && $GH_TOKEN && $APPVEYOR_BRANCH == master ]]; then bash script/deploy_nightly.sh build/lean-*-windows.zip; fi"
 
 artifacts:
   - path: build\lean-*-windows.zip
diff --git a/.travis.yml b/.travis.yml
index 3fee05ca44..d249c3a7fb 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -119,7 +119,7 @@ script:
   - if [[ $STATIC != ON ]]; then STATIC=OFF; fi
   - if [[ $MULTI_THREAD != OFF ]]; then MULTI_THREAD=ON; fi
   - OPTIONS=""
-  - if [[ -z $TRAVIS_TAG ]]; then OPTIONS+="-DLEAN_VERSION_STRING=nightly-${date -uI}"; fi
+  - if [[ $TRAVIS_EVENT_TYPE == cron ]]; then . ./script/setup_nightly.sh; fi
   - cmake -DCMAKE_BUILD_TYPE=$CMAKE_BUILD_TYPE
           -DCMAKE_CXX_COMPILER=$CMAKE_CXX_COMPILER
           -DTESTCOV=$TESTCOV
@@ -139,7 +139,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); 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
   - cd ..
 
 after_script:
diff --git a/script/deploy_gh_pages.sh b/script/deploy_gh_pages.sh
new file mode 100644
index 0000000000..49630a48e1
--- /dev/null
+++ b/script/deploy_gh_pages.sh
@@ -0,0 +1,20 @@
+#!/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
diff --git a/script/deploy_nightly.sh b/script/deploy_nightly.sh
index a1ee0d6731..b0a21bca15 100644
--- a/script/deploy_nightly.sh
+++ b/script/deploy_nightly.sh
@@ -2,44 +2,4 @@
 
 set -eu
 
-# stable build?
-if [ -z $LEAN_VERSION_STRING ]; then exit; fi
-
-rev=$(git rev-parse --short HEAD)
-
-git config user.name "Bot Botson"
-git config user.email "bot@bot.bot"
-
-git remote add nightly "https://$GH_TOKEN@github.com/leanprover/lean-nightly.git"
-git fetch nightly
-
-# Travis can't publish releases to other repos (or stop mucking with the markdown description), so push releases directly
-go get github.com/itchio/gothub
-
-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
-    gothub release -s $GH_TOKEN -u leanprover -r lean-nightly -t $LEAN_VERSION_STRING -d - --pre-release < diff.md
-fi
-
-if [ $rev = $(git rev-parse --short $LEAN_VERSION_STRING) ]
-then
-    gothub upload -s $GH_TOKEN -u leanprover -r lean-nightly -t $LEAN_VERSION_STRING -n "$(basename $1)" -f "$1"
-fi
-
-# 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
-
-git checkout -b gh-pages nightly/gh-pages
-cd gh-pages
-
-mkdir -p build
-ln -f ../build/lean-* build/
-
-git add -A .
-git commit --amend --reset-author -m "nightly build at ${rev}"
-git push -fq
+[ -n $LEAN_VERSION_STRING ] && 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
new file mode 100644
index 0000000000..f3e3031649
--- /dev/null
+++ b/script/setup_nightly.sh
@@ -0,0 +1,28 @@
+#!/bin/bash
+
+set -eu
+
+git remote add nightly "https://$GH_TOKEN@github.com/leanprover/lean-nightly.git"
+git fetch nightly
+
+# exit if commit is already tagged
+git describe --exact-match --tags HEAD >& /dev/null && return
+
+# Travis can't publish releases to other repos (or stop mucking with the markdown description), so push releases directly
+go get github.com/itchio/gothub
+
+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
+    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 checkout $LEAN_VERSION_STRING
+fi
+
+LEAN_VERSION_STRING="nightly-$(date -uI)"
+OPTIONS+="-DLEAN_VERSION_STRING=$LEAN_VERSION_STRING"