emacs and contributions

Stream: general

[Simon Hudon]

I have created a leanprover-community account on github and a lean-mode-contrib repository. I think it will be easier to accumulate tools there and simply have members of the community maintain it than to pester the Lean developers. Other community managed repos might be useful. Feel free to make suggestions (including suggesting / volunteering maintainers)

[Patrick Massot]

What kind of tools do you have in mind?

[Simon Hudon]

So far, all I added is an emacs feature that highlights the difference between expected type and actual types in error messages

[Patrick Massot]

This is really nice. It's something I miss occasionally in VScode.