CoCalc Logo Icon
StoreFeaturesDocsShareSupportNewsAboutSign UpSign In

Real-time collaboration for Jupyter Notebooks, Linux Terminals, LaTeX, VS Code, R IDE, and more,
all in one place.

| Download

Try doing some basic maths questions in the Lean Theorem Prover. Functions, real numbers, equivalence relations and groups. Click on README.md and then on "Open in CoCalc with one click".

Project: Xena
Views: 18536
License: APACHE
Tweet
Share
Share
1
set -e				# fail on error

2


3
DEPLOY_NIGHTLY_GITHUB_USER=leanprover-community-bot

4
git remote add mathlib "https://$DEPLOY_NIGHTLY_GITHUB_USER:$DEPLOY_NIGHTLY_GITHUB_TOKEN@github.com/leanprover-community/mathlib.git"

5
git remote add nightly "https://$DEPLOY_NIGHTLY_GITHUB_USER:$DEPLOY_NIGHTLY_GITHUB_TOKEN@github.com/leanprover-community/mathlib-nightly.git"

6


7
# After this point, we don't use any secrets in commands.

8
set -x				# echo commands

9


10
# By default, github actions overrides the credentials used to access any

11
# github url so that it uses the github-actions[bot] user.  We want to access

12
# github using a different username.

13
git config --unset http.https://github.com/.extraheader

14


15
# The checkout action produces a shallow repository from which we cannot push.

16
git fetch --unshallow || true

17


18
git fetch nightly --tags

19


20
# Create a tag name based on the current date.

21
MATHLIB_VERSION_STRING="nightly-$(date -u +%F)"

22


23
# Check if the tag already exists. If so, exit (successfully).

24
# This way we create a release/update the lean-x.y.z branch

25
# only once per day.

26
if git rev-parse --verify -q $MATHLIB_VERSION_STRING; then

27
    exit 0

28
fi

29


30
if command -v greadlink >/dev/null 2>&1; then

31
    # macOS readlink doesn't support -f option

32
    READLINK=greadlink

33
else

34
    READLINK=readlink

35
fi

36


37
# Try to update the lean-x.y.z branch on mathlib. This could fail if

38
# a subsequent commit has already pushed an update.

39
LEAN_VERSION="lean-3.4.2"

40


41
git push mathlib HEAD:refs/heads/$LEAN_VERSION || \

42
    echo "mathlib rejected push to branch $LEAN_VERSION; maybe it already has a later version?" >&2

43


44
# Push the commits to a branch on nightly and push a tag.

45
git push nightly HEAD:"mathlib-master" || true

46
git tag $MATHLIB_VERSION_STRING

47
git push nightly tag $MATHLIB_VERSION_STRING

48


49
# Travis can't publish releases to other repos (or stop mucking with the markdown description), so push releases directly

50
export GOPATH=$($READLINK -f go)

51
PATH=$PATH:$GOPATH/bin

52
go get github.com/itchio/gothub

53


54
# Build olean and script tarballs.

55
OLEAN_ARCHIVE=mathlib-olean-$MATHLIB_VERSION_STRING.tar.gz

56
SCRIPT_ARCHIVE=mathlib-scripts-$MATHLIB_VERSION_STRING.tar.gz

57
git clone https://github.com/leanprover-community/mathlib-tools

58
tar czf $OLEAN_ARCHIVE src

59
rm -rf mathlib-scripts

60
cp -a mathlib-tools/scripts mathlib-scripts

61
tar czf $SCRIPT_ARCHIVE mathlib-scripts

62
ls *.tar.gz

63


64
# Create a release associated with the tag and upload the tarballs.

65
export GITHUB_TOKEN=$DEPLOY_NIGHTLY_GITHUB_TOKEN

66
gothub release -u leanprover-community -r mathlib-nightly -t $MATHLIB_VERSION_STRING -d "Mathlib's .olean files and scripts" --pre-release

67
gothub upload -u leanprover-community -r mathlib-nightly -t $MATHLIB_VERSION_STRING -n "$(basename $OLEAN_ARCHIVE)" -f "$OLEAN_ARCHIVE"

68
gothub upload -u leanprover-community -r mathlib-nightly -t $MATHLIB_VERSION_STRING -n "$(basename $SCRIPT_ARCHIVE)" -f "$SCRIPT_ARCHIVE"

69


70