3.16.3

Stream: general

[Gabriel Ebner]

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:

• Remove as-is annotations (lean#338, fixes lean#334)
• Handle EOF in skip_to_pos (lean#342, fixes lean#85)
• Fix holes with space in name (lean#343)

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)

[Scott Morrison]

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

[Gabriel Ebner]

I don't know yet.

[Scott Morrison]

I'm trying it out. #3106

[Gabriel Ebner]

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

[Scott Morrison]

oops!

[Gabriel Ebner]

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

[Scott Morrison]

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?

[Scott Morrison]

I've moved to #3107.

[Scott Morrison]

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

[Bryan Gin-ge Chen]

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.

[Bryan Gin-ge Chen]

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

[Sebastien Gouezel]

Linting time divided by two!