From 796baa19cb2b9e492a4fbeb7cb85330a66129d6f Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 26 Feb 2018 09:43:30 +0100
Subject: [PATCH] chore(.appveyor,.travis): proper nightly builds

---
 .appveyor.yml             |  7 ++++--
 .travis.yml               |  4 ++--
 script/deploy_gh_pages.sh | 20 -----------------
 script/deploy_nightly.sh  | 45 +++++++++++++++++++++++++++++++++++++++
 script/diff_changelogs.py | 28 ++++++++++++++++++++++++
 5 files changed, 80 insertions(+), 24 deletions(-)
 delete mode 100644 script/deploy_gh_pages.sh
 create mode 100644 script/deploy_nightly.sh
 create mode 100755 script/diff_changelogs.py

diff --git a/.appveyor.yml b/.appveyor.yml
index cfb0325a80..f080f241a9 100644
--- a/.appveyor.yml
+++ b/.appveyor.yml
@@ -4,6 +4,7 @@ environment:
   MSYSTEM: MINGW64  # use MSYS2 shell
   matrix:
   - CFG: MINGW64
+    UPLOAD: ON
   - CFG: MSVC
 
 cache: c:\tools\vcpkg\installed\
@@ -25,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_BRANCH == master ]]; then OPTIONS+=' -DLEAN_VERSION_STRING=nightly'; fi;
+      if [[ $APPVEYOR_REPO_TAG != true ]]; then OPTIONS+='-DLEAN_VERSION_STRING=nightly-${date -uI}'; fi;
       cmake ../src -DINCLUDE_MSYS2_DLLS=ON -DCMAKE_BUILD_TYPE=Release $OPTIONS -G 'Unix Makefiles' &&
       cmake --build . &&
       cpack")
@@ -35,6 +36,8 @@ test_script:
   - 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"
+  - 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"
 
 artifacts:
   - path: build\lean-*-windows.zip
@@ -50,4 +53,4 @@ deploy:
   prerelease: false
   on:
     appveyor_repo_tag: true
-    CFG: MINGW64
+    UPLOAD: ON
diff --git a/.travis.yml b/.travis.yml
index fb8310856e..3fee05ca44 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 [[ $TRAVIS_BRANCH == master ]]; then OPTIONS+=" -DLEAN_VERSION_STRING=nightly"; fi
+  - if [[ -z $TRAVIS_TAG ]]; then OPTIONS+="-DLEAN_VERSION_STRING=nightly-${date -uI}"; 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_gh_pages.sh); fi
+  - if [[ $UPLOAD == ON && $GH_TOKEN && $TRAVIS_PULL_REQUEST == false && $TRAVIS_BRANCH == master ]]; then (cd ..; bash script/deploy_nightly.sh); fi
   - cd ..
 
 after_script:
diff --git a/script/deploy_gh_pages.sh b/script/deploy_gh_pages.sh
deleted file mode 100644
index f59f6d907a..0000000000
--- a/script/deploy_gh_pages.sh
+++ /dev/null
@@ -1,20 +0,0 @@
-#!/bin/bash
-# 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
new file mode 100644
index 0000000000..a1ee0d6731
--- /dev/null
+++ b/script/deploy_nightly.sh
@@ -0,0 +1,45 @@
+#!/bin/bash
+
+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
diff --git a/script/diff_changelogs.py b/script/diff_changelogs.py
new file mode 100755
index 0000000000..16228bab84
--- /dev/null
+++ b/script/diff_changelogs.py
@@ -0,0 +1,28 @@
+#! /bin/env python3
+
+import collections
+import re
+import sys
+
+def parse(f):
+    s = open(f, 'r').read()
+    flgs = re.VERBOSE | re.MULTILINE
+    [_, release, _] = re.split(r"""^\w.* \n   # master branch (aka work in progress)
+                                    -+   \n+  # -------------""", s, maxsplit=2, flags=flgs)
+    cats = re.split(r"^(?P<cat>\*.+\*)$  # *Features*", release, flags=flgs)
+    cats = zip(cats[1::2], cats[2::2])
+    return collections.OrderedDict([(cat[0], re.findall(r"^\*\ (?:.*(?:\n\ \ .*)*)  # * Implement ...", cat[1], flags=flgs)) for cat in cats])
+
+def diff(oldf, newf):
+    old = parse(oldf)
+    new = parse(newf)
+    for cat in new:
+        items = [i for i in new[cat] if i not in old.get(cat,[])]
+        if items:
+            print(cat)
+            print()
+            print('\n\n'.join(items))
+            print()
+
+if __name__ == '__main__':
+    diff(sys.argv[1], sys.argv[2])