Removing unnecessary dependencies

[phikal]

The packages f and s are 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.

[urkud]

@bustercopley Could you please have a look at this one? If you approve, then I'll merge it.

[bustercopley]

I approve! [Edit: with one minor correction (see review comment)] Not yet please!

[bustercopley]

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.

[phikal]

Richard Copley @.***> writes:

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.

Sorry again.

-- Philip Kaludercic on peregrine

[bustercopley]

@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!

[phikal]

Richard Copley @.***> writes:

@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!

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

[bustercopley]

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)))))

[bustercopley]

@urkud, with one last change (see my previous comment) this ~is~ will be 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 (https://github.com/bustercopley/lean4-mode/commit/f5263152146dcb6c7ae125b7ceb29c6c537f364b), and merge please? The branch contains Philip's two commits and my fixup commit, rebased onto master.

[phikal]

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 (https://github.com/bustercopley/lean4-mode/commit/f5263152146dcb6c7ae125b7ceb29c6c537f364b), 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

[bustercopley]

Thanks @phikal. Don't be dispirited. It's no big deal. @urkud, ready to merge to master now, from my point of view

[phikal]

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

[akirak]

I just think they should be relegated to a separate patch.

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.

[bustercopley]

Thanks @akirak, I am inclined to agree, let's play it safe in this PR, especially since @phikal says he is not in a position to test. There is certainly a lot of tidying up that could be done!