Zulip Chat Archive

Stream: general

Topic: 3.16.5


view this post on Zulip Gabriel Ebner (Jun 25 2020 at 13:32):

Another small patch release that fixes a segfault and an endless loop, and adds some very uncontroversial features.

Features:

  • Add comment-like string blocks (lean#352)
  • Add widgets to trace messages (lean#355)
  • Show case tags in goal widget (lean#357)

Bug fixes:

Server protocol changes:

  • The (Lean error) messages returned by the server may now contain an additional "widget" field.

view this post on Zulip Rob Lewis (Jun 25 2020 at 13:34):

some very /-"uncontroversial"-/ features

view this post on Zulip Patrick Massot (Jun 25 2020 at 13:35):

I think he meant that you'll miss the equatilies error message.

view this post on Zulip Kevin Buzzard (Jun 25 2020 at 13:45):

Oh no! Have the equatilies gone??

view this post on Zulip Johan Commelin (Jun 25 2020 at 13:47):

Yeah, it's a broken concept anyway... so it's been ripped out of core

view this post on Zulip Patrick Massot (Jun 25 2020 at 13:47):

I'm sorry about that. I got overexcited about this idea of contributing to Lean's C++ code.

view this post on Zulip Johan Commelin (Jun 25 2020 at 13:48):

Move fast, break things?

view this post on Zulip Kevin Buzzard (Jun 25 2020 at 13:56):

So that was what you were talking about in the DM to me the other day when you were proudly telling me you'd made a PR to core Lean changing the C++??

view this post on Zulip Gabriel Ebner (Jun 25 2020 at 13:57):

If only it would have been a PR...

view this post on Zulip Patrick Massot (Jun 25 2020 at 13:57):

I'm sorry.

view this post on Zulip Gabriel Ebner (Jun 25 2020 at 13:57):

It's okay.

view this post on Zulip Jiekai (Jun 27 2020 at 14:48):

Out of curiosity, how does the release process work? It's not manually uploading the zip files right?

view this post on Zulip Bryan Gin-ge Chen (Jun 27 2020 at 16:02):

When someone with write privileges to leanprover-community/lean pushes a git tag to the repo, these lines in the github actions script (and the other similar ones) get triggered. That then uses the softprops/action-gh-release action to upload files to that github release.


Last updated: May 14 2021 at 23:14 UTC