Zulip Chat Archive
Stream: general
Topic: Emacs melpa
Yury G. Kudryashov (May 19 2020 at 21:03):
Who can push the latest changes in the Emacs lean-mode to melpa? Currently melpa serves a version from 2017.
Yury G. Kudryashov (May 19 2020 at 21:04):
Of course I can just git clone the repo but I'd prefer to go through melpa->nixpkgs.
Sebastian Ullrich (May 19 2020 at 21:40):
I'm confused - I don't see lean-mode in melpaStablePackages at all. The unstable package is recent
> emacsPackages.melpaPackages.lean-mode.version
"20200319.838"
Sebastian Ullrich (May 19 2020 at 21:48):
In general we're following the "no-one seems to care about MELPA Stable" development model
Yury G. Kudryashov (May 19 2020 at 22:11):
What about compmany-lean?
Yury G. Kudryashov (May 19 2020 at 22:12):
(deleted)
Yury G. Kudryashov (May 20 2020 at 00:51):
$ nix-instantiate --eval-only . -A emacsPackages.melpaPackages.company-lean.version
"20171102.1454"
Sebastian Ullrich (May 20 2020 at 08:16):
Yes, that is in fact the newest version https://github.com/leanprover/lean-mode/commits/master/company-lean.el
Yury G. Kudryashov (May 20 2020 at 08:29):
It seems that setting company-idle-delay to nil (done in company-lean) disables autocompletion with current company-mode. Is it intentional?
Sebastian Ullrich (May 20 2020 at 08:41):
It certainly worked at some point, maybe some newer version of company broke it. lean4-mode doesn't have autocompletion yet, so I wouldn't know.
Last updated: Dec 20 2023 at 11:08 UTC