Zulip Chat Archive

Stream: general

Topic: 3.16.3


view this post on Zulip Gabriel Ebner (Jun 18 2020 at 11:14):

Just another small patch release today since we've accumulated a lot of bug fixes. Thanks to @Yury G. Kudryashov, @Jannis Limperg, @Scott Morrison, and @Peter Jipsen!

Bug fixes:

Features:

  • Add profiling for user attributes (lean#328)
  • Profile user commands (lean#329)
  • Support lean --profile --run (lean#337)
  • Add parser.{any_char,digit,nat} (lean#331)
  • Cache type-class searches w/o mvars (lean#332)

Changes:

  • Put is_strict_total_order in Prop (lean#327)
  • Remove redundant lemmas (lean#321)

view this post on Zulip Scott Morrison (Jun 18 2020 at 11:17):

So how much does #332 speed up the build???

view this post on Zulip Gabriel Ebner (Jun 18 2020 at 11:21):

I don't know yet.

view this post on Zulip Scott Morrison (Jun 18 2020 at 11:24):

I'm trying it out. #3106

view this post on Zulip Gabriel Ebner (Jun 18 2020 at 11:26):

You need to choose a different branch name, lean-3.* is reserved.

view this post on Zulip Scott Morrison (Jun 18 2020 at 11:28):

oops!

view this post on Zulip Gabriel Ebner (Jun 18 2020 at 11:32):

@Bryan Gin-ge Chen Do you know if we need to delete the lean-3.16.3 branch now?

view this post on Zulip Scott Morrison (Jun 18 2020 at 11:33):

I just tried, and wasn't able to. A bit strange that I could create the branch in the first place, but not delete it?

view this post on Zulip Scott Morrison (Jun 18 2020 at 11:33):

I've moved to #3107.

view this post on Zulip Scott Morrison (Jun 18 2020 at 11:46):

mathlib now builds, and I'm doing a timing run

view this post on Zulip Bryan Gin-ge Chen (Jun 18 2020 at 13:37):

Gabriel Ebner said:

Bryan Gin-ge Chen Do you know if we need to delete the lean-3.16.3 branch now?

I just temporarily turned off the branch protection and deleted it, since I think update_branch.sh would have run into an error.

view this post on Zulip Bryan Gin-ge Chen (Jun 18 2020 at 13:46):

#3107 is green so I put it on the merge queue.

view this post on Zulip Sebastien Gouezel (Jun 18 2020 at 16:43):

Linting time divided by two!


Last updated: May 06 2021 at 21:09 UTC