Lean '' is released!

Stream: general

[Gabriel Ebner]

leanprover-mathlib-bot is proud to announce the latest version of Lean, Lean ''! https://github.com/leanprover-community/lean/releases/tag/''

[Gabriel Ebner]

I'm not exactly sure what's going on. Apparently travis just decided to deploy a random commit on master. I hope this is a temporary glitch.

[Reid Barton]

cool, I'll start using it pronto

[Reid Barton]

zulip's markdown really hates this URL apparently

[Reid Barton]

https://github.com/leanprover-community/lean/releases/tag/%27%27

[Rob Lewis]

For anyone keeping track of the robots: leanprover-mathlib-bot is leanprover-community-bot's older cousin. He's a bit of a renegade, he does his own thing and doesn't care what you think.

[Gabriel Ebner]

leanprover-mathlib-bot now tried to release \'\', which is no longer a valid git tag name apparently. I've deleted both releases. Let's hope they don't come back.

[Bryan Gin-ge Chen]

I think I know roughly what scripts in mathlib drive leanprover-community-bot, but where are the scripts that control leanprover-mathlib-bot?

[Gabriel Ebner]

It's actually travis (which uses the credentials for leanprover-mathlib-bot). Travis is supposed to deploy from every CI build that is triggered by pushing a tag: https://github.com/leanprover-community/lean/blob/1b0d0a93ab523a7451840212fb40c4b14ab6cd6b/.travis.yml#L218-L229

[Reid Barton]

Gabriel Ebner said:

leanprover-mathlib-bot now tried to release \'\', which is no longer a valid git tag name apparently. I've deleted both releases. Let's hope they don't come back.

uh oh. could \\\'\\\' be next?

[Bryan Gin-ge Chen]

Ah, so the question is how did these weirdly named tags get created?

[Gabriel Ebner]

This happened due to a new feature in travis, which is reverted now: https://github.com/travis-ci/travis-build/pull/1865

[Gabriel Ebner]

Unfortunately, there's still an issue: we are not creating nightlies at the moment.