Removing unnecessary dependencies #51

phikal · 2023-10-27T17:37:43Z

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 · 2024-02-23T07:38:43Z

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

bustercopley · 2024-02-23T10:34:46Z

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

lean4-util.el

bustercopley · 2024-02-23T21:30:38Z

lean4-util.el

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


Suggested change

(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 default-directory later. (This was already incorrect before your changes.)~~ [But not after! 😄]

@phikal, can you fix this on your branch and push, please?

I'm sorry, I didn't realise that these was supposed to be "suggested changes".

bustercopley · 2024-02-27T17:16:44Z

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 · 2024-02-27T17:20:13Z

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

bustercopley · 2024-02-27T18:34:12Z

@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 · 2024-02-27T18:45:59Z

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

bustercopley · 2024-02-27T18:59:00Z

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 · 2024-02-27T23:50:55Z

@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 (bustercopley@f526315), and merge please? The branch contains Philip's two commits and my fixup commit, rebased onto master.

phikal · 2024-02-29T09:33:40Z

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

bustercopley · 2024-02-29T10:11:31Z

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

akirak

I have made a few suggestions to simplify the code.

lean4-lake.el


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


lean4-util.el

-             (equal (f-filename file) ".")
-             (equal (f-filename file) "..")))
+             (equal (file-name-nondirectory file) ".")
+             (equal (file-name-nondirectory file) "..")))
          (directory-files path t))))


lean4-util.el

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


phikal · 2024-02-29T11:46:38Z

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 · 2024-02-29T12:15:15Z

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 · 2024-02-29T12:16:23Z

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!

purcell mentioned this pull request Nov 1, 2023

Add recipe for lean4-mode melpa/melpa#8106

Open

7 tasks

bustercopley reviewed Feb 23, 2024

View reviewed changes

lean4-util.el Outdated Show resolved Hide resolved

phikal force-pushed the master branch from e5bb210 to c088649 Compare February 23, 2024 16:22

bustercopley suggested changes Feb 23, 2024

View reviewed changes

phikal force-pushed the master branch from c088649 to 8d6cb7b Compare February 27, 2024 16:15

phikal force-pushed the master branch from 8d6cb7b to fc88165 Compare February 27, 2024 17:19

phikal force-pushed the master branch from fc88165 to 0f0c346 Compare February 27, 2024 18:44

phikal and others added 3 commits February 27, 2024 22:48

Remove dependency on f

41c6744

Remove dependency on s

191d4be

fix: typo fix for "Remove dependency on f"

f526315

phikal force-pushed the master branch from 0f0c346 to f526315 Compare February 29, 2024 09:34

akirak reviewed Feb 29, 2024

View reviewed changes

urkud mentioned this pull request Feb 29, 2024

Go over suggestions in #51 #58

Open

This was referenced Mar 2, 2024

chore: delete unused code in "lean4-util.el" #60

Merged

Fix magit-section usage so the expand/contract functionality works #59

Merged

urkud merged commit f1f24c1 into leanprover-community:master Mar 6, 2024
2 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Removing unnecessary dependencies #51

Removing unnecessary dependencies #51

phikal commented Oct 27, 2023

urkud commented Feb 23, 2024

bustercopley commented Feb 23, 2024 •

edited

Loading

bustercopley Feb 23, 2024 •

edited

Loading

bustercopley Feb 27, 2024

phikal Feb 27, 2024

bustercopley commented Feb 27, 2024

phikal commented Feb 27, 2024 via email

bustercopley commented Feb 27, 2024

phikal commented Feb 27, 2024 via email

bustercopley commented Feb 27, 2024 •

edited

Loading

bustercopley commented Feb 27, 2024 •

edited

Loading

phikal commented Feb 29, 2024 via email

bustercopley commented Feb 29, 2024

akirak left a comment

This comment was marked as off-topic.

This comment was marked as off-topic.

This comment was marked as off-topic.

phikal commented Feb 29, 2024 via email

akirak commented Feb 29, 2024 •

edited

Loading

bustercopley commented Feb 29, 2024

Removing unnecessary dependencies #51

Removing unnecessary dependencies #51

Conversation

phikal commented Oct 27, 2023

urkud commented Feb 23, 2024

bustercopley commented Feb 23, 2024 • edited Loading

bustercopley Feb 23, 2024 • edited Loading

Choose a reason for hiding this comment

bustercopley Feb 27, 2024

Choose a reason for hiding this comment

phikal Feb 27, 2024

Choose a reason for hiding this comment

bustercopley commented Feb 27, 2024

phikal commented Feb 27, 2024 via email

bustercopley commented Feb 27, 2024

phikal commented Feb 27, 2024 via email

bustercopley commented Feb 27, 2024 • edited Loading

bustercopley commented Feb 27, 2024 • edited Loading

phikal commented Feb 29, 2024 via email

bustercopley commented Feb 29, 2024

akirak left a comment

Choose a reason for hiding this comment

This comment was marked as off-topic.

This comment was marked as off-topic.

This comment was marked as off-topic.

phikal commented Feb 29, 2024 via email

akirak commented Feb 29, 2024 • edited Loading

bustercopley commented Feb 29, 2024

bustercopley commented Feb 23, 2024 •

edited

Loading

bustercopley Feb 23, 2024 •

edited

Loading

bustercopley commented Feb 27, 2024 •

edited

Loading

bustercopley commented Feb 27, 2024 •

edited

Loading

akirak commented Feb 29, 2024 •

edited

Loading