3.16.5

Stream: general

[Gabriel Ebner]

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:

• Handle exceptions in ts_clone (lean#350)
• Support sorry # (lean#356)

Server protocol changes:

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

[Rob Lewis]

some very /-"uncontroversial"-/ features

[Patrick Massot]

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

[Kevin Buzzard]

Oh no! Have the equatilies gone??

[Johan Commelin]

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

[Patrick Massot]

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

[Johan Commelin]

Move fast, break things?

[Kevin Buzzard]

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++??

[Gabriel Ebner]

If only it would have been a PR...

[Patrick Massot]

I'm sorry.

[Gabriel Ebner]

It's okay.

[Jiekai]

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

[Bryan Gin-ge Chen]

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.