Zulip Chat Archive

Stream: general

Topic: Non-numeric versions in elan


view this post on Zulip Gabriel Ebner (May 08 2020 at 11:47):

@Sebastian Ullrich How hard would it be / would you accept a PR to support non-numeric versions in elan? That is, something like lean +edayers/lean:widget where widget is a tag?

view this post on Zulip Sebastian Ullrich (May 08 2020 at 11:57):

That seems reasonable. Now that I already have an implementation in mind, I'll give it a try.

view this post on Zulip Mario Carneiro (May 08 2020 at 12:25):

Oh, lean is growing up faster than expected: https://github.com/leanprover-community/lean/releases/tag/v9.9.9

view this post on Zulip Sebastian Ullrich (May 08 2020 at 12:27):

I liked the we-love-bors release more

view this post on Zulip Sebastian Ullrich (May 08 2020 at 12:37):

In the end I went with the quick-n-dirty solution after all... https://github.com/Kha/elan/pull/23
Please give it a try if you actually have a non-numeric release


Last updated: May 10 2021 at 00:31 UTC