Go over suggestions in #51

[urkud]

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]

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]

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.

[mekeor]

I'll soon close this issue in favor of two new issues:

• Depend on compat package and use file-name-concat instead of (expand-file-name exe-name (expand-file-name "bin")))) in lean4-util.el. This will be added to milestone 2. EDIT: Done: Depend on Compat and use file-name-concat #89
• Remove lean4-lake.el in favor of using Emacs' built-in compile command. This will be added to milestone 3 or later. EDIT: Done: Remove lean4-lake.el in favor of Emacs built-in compile command #90

[mekeor]

Oh and a third issue would be to use (locate-dominating-file default-directory "lakefile.lean") instead of defining ean4-lake-find-dir-in. This may go into milestone 2.

EDIT: Done: #90 (comment)