Zulip Chat Archive

Stream: general

Topic: emacs and contributions


view this post on Zulip Simon Hudon (Jul 25 2018 at 20:31):

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)

view this post on Zulip Patrick Massot (Jul 25 2018 at 20:33):

What kind of tools do you have in mind?

view this post on Zulip Simon Hudon (Jul 25 2018 at 20:37):

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

view this post on Zulip Patrick Massot (Jul 25 2018 at 22:24):

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


Last updated: May 06 2021 at 21:09 UTC