Lean 3.17.0

Stream: general

[Gabriel Ebner]

Let's bump the minor version number again! This week we can welcome the 3.17.0 release of the Lean community edition! Thanks to @Edward Ayers, @Scott Morrison, @Floris van Doorn, @Johan Commelin!

Features:

• Refactor widgets to use hooks (lean#363, lean#369)
• component.with_effects (lean#370)
• Add "copy text" effect. (lean#375)

Bug fixes:

• Add margin to local const names in tactic state (lean#365)
• Prevent segfault in apply (lean#373, fixes lean#372)
• Fix address incorrect issue in pp_tagged (lean#371)
• Abort if no input consumed in module_parser (lean#377, fixes lean#374)
• Do not unify (1 : ℕ) with (1 : ℤ) (lean#376, fixes lean#362)

Changes:

• Fix vacuous assumptions in nat lemmas (lean#366)
• Remove has_neg instance for set (lean#367)
• Mark dif_ctx_congr as @[congr] (lean#378)

Server protocol changes:

• The response of the widget_event request may now contain effects.

Mathlib PR:

• is running (#3300)