Zulip Chat Archive

Stream: general

Topic: Lean 3.28.0c

Bryan Gin-ge Chen (Mar 15 2021 at 15:56):

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)!


  • 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)


  • 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 (Mar 15 2021 at 15:56):

(The Windows build should be uploaded shortly.)

Bryan Gin-ge Chen (Mar 15 2021 at 16:08):

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 (Mar 16 2021 at 18:21):

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

Last updated: Dec 20 2023 at 11:08 UTC