Lean 3.28.0c

Stream: general

[Bryan Gin-ge Chen]

Lean 3.28.0c and you can now use _root_ in declaration names! Thanks to @Eric Wieser, @Gabriel Ebner, @Floris van Doorn, @Timothee Lacroix for their work (and @Gabriel Ebner for reviewing and merging their PRs)!

Features:

• leanchecker prints error messages (lean#548)
• _root_ can now be used to put declarations in the root namespace (lean#550)

Bug fixes:

• line wrapping in to_raw_fmt (lean#549)
• The widget.html.to_string_coe instance now uses has_coe_t (lean#544)
• Fix in mt_task_queue (lean#552)

Changes:

• propagate_tags can now be used interactively (lean#540)
• Change fin.sub to the Lean 4 definition (lean#541)
• Some lint fixes (lean#545)
• Update installation instructions (lean#547)

Mathlib PR: #6691

[Bryan Gin-ge Chen]

(The Windows build should be uploaded shortly.)

[Bryan Gin-ge Chen]

The mathlib PR doesn't build yet; feel free to help push fixes to the branch as I won't be able to get back to it until later.

[Bryan Gin-ge Chen]

@Sebastien Gouezel has fixed up #6691 so it builds, but there are 2 open questions there. cc: @Gabriel Ebner @Floris van Doorn