Removing unnecessary dependencies #51
Conversation
|
@bustercopley Could you please have a look at this one? If you approve, then I'll merge it. |
|
|
lean4-util.el
Outdated
| @@ -38,16 +36,16 @@ Try to find an executable named `lean4-executable-name' in variable `exec-path'. | |||
| On succsess, return path to the directory with this executable." | |||
| (let ((root (executable-find lean4-executable-name))) | |||
| (when root | |||
| (setq lean4-rootdir (f-dirname (f-dirname root)))) | |||
| (setq lean4-rootdir (file-name-directory (directory-file-name root)))) | |||
There was a problem hiding this comment.
| (setq lean4-rootdir (file-name-directory (directory-file-name root)))) | |
| (setq lean4-rootdir | |
| (file-name-directory | |
| (directory-file-name | |
| (file-name-directory root))))) |
There were two calls to f-dirname! (I don't know why f-parent wasn't used.)
But also: the value should end in a slash since it's going to be used as [But not after! 😄]default-directory later. (This was already incorrect before your changes.)
There was a problem hiding this comment.
@phikal, can you fix this on your branch and push, please?
There was a problem hiding this comment.
I'm sorry, I didn't realise that these was supposed to be "suggested changes".
|
Thanks @phikal! But that's still not quite right. (let ((root "/path/to/bin/lean.exe"))
(file-name-directory (file-name-directory (directory-file-name root))))
;; => "/path/to/bin/"
(let ((root "/path/to/bin/lean.exe"))
(file-name-directory (directory-file-name (file-name-directory root))))
;; => "/path/to/"It is the latter that is needed here. |
|
Richard Copley ***@***.***> writes:
Thanks @phikal! But that's still not quite right.
```elisp
(let ((root "/path/to/bin/lean.exe"))
(file-name-directory (file-name-directory (directory-file-name root))))
;; => "/path/to/bin/"
(let ((root "/path/to/bin/lean.exe"))
(file-name-directory (directory-file-name (file-name-directory root))))
;; => "/path/to/"
```
It is the latter that is needed here.
Sorry again.
…--
Philip Kaludercic on peregrine
|
|
@phikal, no worries. But now there's a typo. (setq lean4-rootdir ) ;; => (wrong-number-of-arguments setq 1)Would you mind? Sorry, I'd fix it myself if I could! |
|
Richard Copley ***@***.***> writes:
@phikal, no worries. But now there's a typo.
```elisp
(setq lean4-rootdir ) ;; => (wrong-number-of-arguments setq 1)
```
Would you mind? Sorry, I'd fix it myself if I could!
This is getting embarrassing, in my defence mainly because I can't
really test the code myself. But yes, change whatever you want, this
GitHub workflow is foreign to me.
…--
Philip Kaludercic on peregrine
|
|
Really, don't worry about it. I'm not a maintainer. I don't have permission to edit PRs from other contributors. Nearly there, I think, but you have (setq lean4-rootdir (file-name-directory (directory-file-name (directory-file-name root)))))It should be (setq lean4-rootdir (file-name-directory (directory-file-name (file-name-directory root))))) |
|
@urkud, with one last change (see my previous comment) this If possible, will you fetch branch "pr51" from the fork at "https://github.com/bustercopley/lean4-mode", update the PR to that commit (bustercopley@f526315), and merge please? The branch contains Philip's two commits and my fixup commit, rebased onto master. |
|
Richard Copley ***@***.***> writes:
@urkud, with one last change (see my previous comment) this is ready
to merge, unless you have any suggestions. I have tested each text
change and there are no observable behaviour changes.
If possible, will you fetch branch "pr51" from the fork at
"https://github.com/bustercopley/lean4-mode", update the PR to that
commit
(bustercopley@f526315),
and merge please? The branch contains Philip's two commits and my
fixup commit, rebased onto master.
Not trusting myself anymore to make a simple edit like this, I have just
pushed Richard's commit to my branch as well.
…--
Philip Kaludercic on peregrine
|
|
|
||
| (defun lean4-lake-find-dir () | ||
| "Find a parent directory of the current file with file \"lakefile.lean\"." | ||
| (and (buffer-file-name) | ||
| (lean4-lake-find-dir-in (f-dirname (buffer-file-name))))) | ||
| (lean4-lake-find-dir-in (directory-file-name (buffer-file-name))))) |
There was a problem hiding this comment.
You can use locate-dominating-file instead of the lean4-lake-find-dir-in function defined above:
(locate-dominating-file default-directory "lakefile.lean")| (let ((lean4-bin-dir-name "bin")) | ||
| (f-full (f-join (lean4-get-rootdir) lean4-bin-dir-name exe-name)))) | ||
| (let ((default-directory (lean4-get-rootdir))) | ||
| (expand-file-name exe-name (expand-file-name "bin")))) |
There was a problem hiding this comment.
FYI, this could be (file-name-concat (lean4-get-rootdir) "bin" exe-name) after Emacs 28.1.
|
Akira Komamura ***@***.***> writes:
@akirak commented on this pull request.
I have made a few suggestions to simplify the code.
I don't disagree that these changes aren't possible, I just think they
should be relegated to a separate patch. The suggestions I made here
are a rather mechanical translation of the functionality that the `f`
and `s` libraries provide into their corresponding "pure" Elisp
equivalents.
…--
Philip Kaludercic on peregrine
|
That's totally fine. My suggestions only depend on built-in functions, but I understand they are beyond the scope of this PR. Please ignore those. |
The packages
fandsare usually not necessary, and can be removed at no cost.The background for this change is that I'd like to add leam4-mode to NonGNU ELPA, and therefore would like to remove hard dependencies on packages that are not included in the ELPA repositories.