From 41c67442df970707a85961028763b10826eb327d Mon Sep 17 00:00:00 2001 From: Philip Kaludercic Date: Fri, 27 Oct 2023 19:09:27 +0200 Subject: [PATCH 1/3] Remove dependency on f --- README.md | 2 +- lean4-dev.el | 3 +-- lean4-lake.el | 6 +++--- lean4-mode.el | 10 +++++----- lean4-util.el | 20 ++++++++++---------- 5 files changed, 20 insertions(+), 21 deletions(-) diff --git a/README.md b/README.md index bf5dc03..df7ae07 100644 --- a/README.md +++ b/README.md @@ -8,7 +8,7 @@ To use `lean4-mode` in Emacs, add the following to your `init.el`: ;; You need to modify the following line (setq load-path (cons "/path/to/lean4-mode" load-path)) -(setq lean4-mode-required-packages '(dash f flycheck lsp-mode magit-section s)) +(setq lean4-mode-required-packages '(dash flycheck lsp-mode magit-section s)) (require 'package) (add-to-list 'package-archives '("melpa" . "http://melpa.org/packages/")) diff --git a/lean4-dev.el b/lean4-dev.el index fdaa775..a1b9619 100644 --- a/lean4-dev.el +++ b/lean4-dev.el @@ -27,7 +27,6 @@ ;;; Code: -(require 'f) (require 'lean4-util) (defun lean4-diff-test-file () @@ -35,7 +34,7 @@ (interactive) (save-buffer) ; yes: auto-agree to copying missing files - (message (shell-command-to-string (format "yes | PATH=%s/bin:$PATH LEAN_NIX_ARGS=--quiet ./test_single.sh -i \"%s\"" (lean4-get-rootdir) (f-filename (buffer-file-name)))))) + (message (shell-command-to-string (format "yes | PATH=%s/bin:$PATH LEAN_NIX_ARGS=--quiet ./test_single.sh -i \"%s\"" (lean4-get-rootdir) (file-name-nondirectory (buffer-file-name)))))) (provide 'lean4-dev) ;;; lean4-dev.el ends here diff --git a/lean4-lake.el b/lean4-lake.el index d7bd313..37d32df 100644 --- a/lean4-lake.el +++ b/lean4-lake.el @@ -30,13 +30,13 @@ (defun lean4-lake-find-dir-in (dir) "Find a parent directory of DIR with file \"lakefile.lean\"." (when dir - (or (when (f-exists? (f-join dir "lakefile.lean")) dir) - (lean4-lake-find-dir-in (f-parent dir))))) + (or (when (file-exists-p (expand-file-name "lakefile.lean" dir)) dir) + (lean4-lake-find-dir-in (file-name-directory (directory-file-name dir)))))) (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))))) (defun lean4-lake-find-dir-safe () "Call `lean4-lake-find-dir', error on failure." diff --git a/lean4-mode.el b/lean4-mode.el index e939bdd..714c772 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -10,7 +10,7 @@ ;; Maintainer: Sebastian Ullrich ;; Created: Jan 09, 2014 ;; Keywords: languages -;; Package-Requires: ((emacs "27.1") (dash "2.18.0") (s "1.10.0") (f "0.19.0") (flycheck "30") (magit-section "2.90.1") (lsp-mode "8.0.0")) +;; Package-Requires: ((emacs "27.1") (dash "2.18.0") (s "1.10.0") (flycheck "30") (magit-section "2.90.1") (lsp-mode "8.0.0")) ;; URL: https://github.com/leanprover/lean4-mode ;; SPDX-License-Identifier: Apache-2.0 @@ -74,7 +74,7 @@ If LAKE-NAME is nonempty, then prepend \"LAKE-NAME env\" to the command "Create a temp lean file and return its name. The new file has prefix PREFIX (defaults to `flymake') and the same extension as FILE-NAME." - (make-temp-file (or prefix "flymake") nil (f-ext file-name))) + (make-temp-file (or prefix "flymake") nil (file-name-extension file-name))) (defun lean4-execute (&optional arg) "Execute Lean in the current buffer with an optional argument ARG." @@ -90,10 +90,10 @@ FILE-NAME." (buffer-file-name) (flymake-proc-init-create-temp-buffer-copy 'lean4-create-temp-in-system-tempdir)))) (compile (lean4-compile-string - (if use-lake (shell-quote-argument (f-full (lean4-get-executable lean4-lake-name))) nil) - (shell-quote-argument (f-full (lean4-get-executable lean4-executable-name))) + (if use-lake (shell-quote-argument (expand-file-name (lean4-get-executable lean4-lake-name))) nil) + (shell-quote-argument (expand-file-name (lean4-get-executable lean4-executable-name))) (or arg "") - (shell-quote-argument (f-full target-file-name)))) + (shell-quote-argument (expand-file-name target-file-name)))) ;; restore old value (setq compile-command cc) (setq default-directory dd))) diff --git a/lean4-util.el b/lean4-util.el index 5d6516c..3d5c2f2 100644 --- a/lean4-util.el +++ b/lean4-util.el @@ -27,7 +27,6 @@ ;;; Code: (require 'cl-lib) -(require 'f) (require 's) (require 'dash) (require 'lean4-settings) @@ -38,7 +37,8 @@ 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 ) + (setq lean4-rootdir (file-name-directory (directory-file-name (directory-file-name root))))) lean4-rootdir)) (defun lean4-get-rootdir () @@ -46,8 +46,8 @@ On succsess, return path to the directory with this executable." First try to find an executable named `lean4-executable-name' in `lean4-rootdir'. On failure, search in variable `exec-path'." (if lean4-rootdir - (let ((lean4-path (f-full (f-join lean4-rootdir "bin" lean4-executable-name)))) - (unless (f-exists? lean4-path) + (let ((lean4-path (expand-file-name lean4-executable-name (expand-file-name "bin" lean4-rootdir)))) + (unless (file-exists-p lean4-path) (error "Incorrect `lean4-rootdir' value, path '%s' does not exist" lean4-path)) lean4-rootdir) (or @@ -58,8 +58,8 @@ First try to find an executable named `lean4-executable-name' in (defun lean4-get-executable (exe-name) "Return fullpath of lean executable EXE-NAME." - (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")))) (defun lean4-line-offset (&optional pos) "Return the byte-offset of POS or current position. @@ -104,8 +104,8 @@ timer and kill the execution of this function." (-reject (lambda (file) (or - (equal (f-filename file) ".") - (equal (f-filename file) ".."))) + (equal (file-name-nondirectory file) ".") + (equal (file-name-nondirectory file) ".."))) (directory-files path t)))) ;; The following line is the only modification that I made ;; It waits 0.0001 second for an event. This wait allows @@ -115,9 +115,9 @@ timer and kill the execution of this function." (cond (recursive (mapc (lambda (entry) - (if (f-file? entry) + (if (file-regular-p entry) (setq result (cons entry result)) - (when (f-directory? entry) + (when (file-directory-p entry) (setq result (cons entry result)) (setq result (append result (lean4--collect-entries entry recursive)))))) entries)) From 191d4be39c8545924b318724065fca8d2887acd6 Mon Sep 17 00:00:00 2001 From: Philip Kaludercic Date: Fri, 27 Oct 2023 19:12:51 +0200 Subject: [PATCH 2/3] Remove dependency on s --- README.md | 2 +- lean4-info.el | 2 +- lean4-mode.el | 2 +- lean4-util.el | 2 -- 4 files changed, 3 insertions(+), 5 deletions(-) diff --git a/README.md b/README.md index df7ae07..38623c9 100644 --- a/README.md +++ b/README.md @@ -8,7 +8,7 @@ To use `lean4-mode` in Emacs, add the following to your `init.el`: ;; You need to modify the following line (setq load-path (cons "/path/to/lean4-mode" load-path)) -(setq lean4-mode-required-packages '(dash flycheck lsp-mode magit-section s)) +(setq lean4-mode-required-packages '(dash flycheck lsp-mode magit-section)) (require 'package) (add-to-list 'package-archives '("melpa" . "http://melpa.org/packages/")) diff --git a/lean4-info.el b/lean4-info.el index e5cdcb4..1b6ccd6 100644 --- a/lean4-info.el +++ b/lean4-info.el @@ -152,7 +152,7 @@ The buffer is supposed to be the *Lean Goal* buffer." (goto-char 0) (while (re-search-forward "\\(\\sw+\\)✝\\([¹²³⁴-⁹⁰]*\\)" nil t) (replace-match - (propertize (s-concat (match-string-no-properties 1) (match-string-no-properties 2)) + (propertize (concat (match-string-no-properties 1) (match-string-no-properties 2)) 'font-lock-face 'font-lock-comment-face) 'fixedcase 'literal))))))) diff --git a/lean4-mode.el b/lean4-mode.el index 714c772..cd720c0 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -10,7 +10,7 @@ ;; Maintainer: Sebastian Ullrich ;; Created: Jan 09, 2014 ;; Keywords: languages -;; Package-Requires: ((emacs "27.1") (dash "2.18.0") (s "1.10.0") (flycheck "30") (magit-section "2.90.1") (lsp-mode "8.0.0")) +;; Package-Requires: ((emacs "27.1") (dash "2.18.0") (flycheck "30") (magit-section "2.90.1") (lsp-mode "8.0.0")) ;; URL: https://github.com/leanprover/lean4-mode ;; SPDX-License-Identifier: Apache-2.0 diff --git a/lean4-util.el b/lean4-util.el index 3d5c2f2..a469b35 100644 --- a/lean4-util.el +++ b/lean4-util.el @@ -27,7 +27,6 @@ ;;; Code: (require 'cl-lib) -(require 's) (require 'dash) (require 'lean4-settings) @@ -37,7 +36,6 @@ 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 ) (setq lean4-rootdir (file-name-directory (directory-file-name (directory-file-name root))))) lean4-rootdir)) From f5263152146dcb6c7ae125b7ceb29c6c537f364b Mon Sep 17 00:00:00 2001 From: Richard Copley Date: Tue, 27 Feb 2024 23:41:07 +0000 Subject: [PATCH 3/3] fix: typo fix for "Remove dependency on f" --- lean4-util.el | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/lean4-util.el b/lean4-util.el index a469b35..f796745 100644 --- a/lean4-util.el +++ b/lean4-util.el @@ -36,7 +36,9 @@ 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 (file-name-directory (directory-file-name (directory-file-name root))))) + (setq lean4-rootdir (file-name-directory + (directory-file-name + (file-name-directory root))))) lean4-rootdir)) (defun lean4-get-rootdir ()