search

leanprover-community / lean4-mode

Emacs major mode for Lean 4
https://leanprover.github.io/
Apache License 2.0
55 stars 27 forks source link

Go over suggestions in #51 #58

Open urkud opened 4 months ago

urkud commented 4 months ago

In #51, @akirak made some suggestions that were deemed out of the scope of that PR. Go over these suggestions and decide whether to implement them.

bustercopley commented 4 months ago

First change (in lean4-lake-find-dir in "lean4-lake.el"):

I agree with the change but I also wonder if anyone would notice if we deleted "lean4-lake.el". We could just mention in the README that building happens automatically when lake is started as a server, and direct users to the compile command if they do need to run lake build.

Second change (in lean4-find-files in "lean4-util.el"):

lean4-find-files and lean4--collect-entries are unused and should be deleted.

Third change (in lean4-get-executable in "lean4-util.el"):

The change depends on Emacs 28.1, but I think it's worth supporting 27.1 a while longer unless we have a more compelling reason. If I'm reading the docs right, 27.1 is the default on Debian oldstable (bullseye) and Ubuntu 22.04.

phikal commented 4 months ago

The change depends on Emacs 28.1, but I think it's worth supporting 27.1 a while longer unless we have a more compelling reason. If I'm reading the docs right, 27.1 is the default on Debian oldstable (bullseye) and Ubuntu 22.04.

FWIW you could use Compat to help out here, since the library provides a backwards compatible definition.