diff --git a/script/deploy_nightly.sh b/script/deploy_nightly.sh index b0a21bca15..06127d5c07 100644 --- a/script/deploy_nightly.sh +++ b/script/deploy_nightly.sh @@ -1,5 +1,25 @@ #!/bin/bash -set -eu +set -exu -[ -n $LEAN_VERSION_STRING ] && gothub upload -s $GH_TOKEN -u leanprover -r lean-nightly -t $LEAN_VERSION_STRING -n "$(basename $1)" -f "$1" +[ -z $LEAN_VERSION_STRING] && exit 0 + +# 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 +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 parse-rev HEAD) == $(git parse-rev $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 index 66624b1ae1..46d7e50a39 100644 --- a/script/setup_nightly.sh +++ b/script/setup_nightly.sh @@ -1,28 +1,13 @@ #!/bin/bash -set -eu +set -exu git remote add nightly "https://$GH_TOKEN@github.com/leanprover/lean-nightly.git" -git fetch nightly +git fetch nightly --tags -# 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 +# do nothing if commit is already tagged +if [ ! git describe --exact-match --tags HEAD >& /dev/null ] 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 + LEAN_VERSION_STRING="nightly-$(date -uI)" + OPTIONS+=" -DLEAN_SPECIAL_VERSION_DESC=$LEAN_VERSION_STRING" fi - -LEAN_VERSION_STRING="nightly-$(date -uI)" -OPTIONS+="-DLEAN_SPECIAL_VERSION_DESC=$LEAN_VERSION_STRING"