max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(script): fix nightly deployment

Browse source
This commit is contained in:
Sebastian Ullrich 2018-03-22 16:20:01 +01:00
parent 0f7a8907c7
commit 0d146918d8
2 changed files with 28 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
script/deploy_nightly.sh
View file

@ -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"

27
script/setup_nightly.sh
View file

@ -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"