emacs-27.1

Stream: general

[Yury G. Kudryashov]

It seems that lean mode makes emacs-27.1 freeze (at least on my NixOS computer). I rolled back to emacs-26.3 for now.

[Yury G. Kudryashov]

But suggestions on how to debug the freeze are very welcome.

[Kyle Miller]

I've been on 27.1 for a while, and I don't think I've observed any freezes, but I'm not sure I'm using the newest lean-mode, if that matters.

[Yury G. Kudryashov]

I'll test it with a smaller set of other packages.

[Yury G. Kudryashov]

Thanks for the information.

[Simon Hudon]

Are you both using lean-mode from leanprover/lean-mode (or Melpa) or the set of contributions on leanprover-community?

[Yury G. Kudryashov]

I'm using the one from melpa but probably my setup is broken for some other reason.

[Yury G. Kudryashov]

E.g., I haven't tried commenting out all other (use-package ...) yet.

[Kevin Lacker]

if you see a freeze in emacs again try these steps: https://emacs.stackexchange.com/questions/506/debugging-a-frozen-emacs

[Vaibhav Karve]

@Simon Hudon I was not aware that there is an alternative lean-mode. Which is the recommended one?

[Simon Hudon]

The one on Melpa. The one on leanprover-community is one or two added goodies. You can install it too but it hasn't been battle tested

[Simon Hudon]

And there's yasnippet-lean which is used at least by Jesse and me

[Philip B.]

I am using lean-mode from melpa. I have a problem: messages, warnings, and errors in lean-mode's flycheck buffer are often too wide, they don't fit in my window. Is there something I can do? Make it wrap around or something. Screenshot_20201101_122949.png

[Jannis Limperg]

I primarily use the Lean Next Error buffer to look at errors (and Lean Goals for goals), and the flycheck window only for jumping around the file. Maybe that would work for you as well?

[Simon Hudon]

That's also what I do. When you jump to an error, flycheck will display the error in the mini-buffer (which becomes not so mini in the process) but I mostly rely on the Lean Next Error buffer

[Alexandre Rademaker]

What yasnippet-lean does?

[Simon Hudon]

yasnippet is a snippet package. There a sets of snippets for different languages. @Jesse Michael Han and I made one for Lean. There's a brief demo on the Github page: https://github.com/leanprover-community/yasnippet-lean