Removing unnecessary dependencies

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))
 
 (require 'package)
 (add-to-list 'package-archives '("melpa" . "http://melpa.org/packages/"))

lean4-dev.el

@@ -27,15 +27,14 @@
 
 ;;; Code:
 
-(require 'f)
 (require 'lean4-util)
 
 (defun lean4-diff-test-file ()
   "Use interactive ./test_input.sh on file of current buffer."
   (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

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

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."

lean4-mode.el

@@ -10,7 +10,7 @@
 ;; Maintainer: Sebastian Ullrich <sebasti@nullri.ch>
 ;; 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") (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)))

lean4-util.el

@@ -27,8 +27,6 @@
 ;;; Code:
 
 (require 'cl-lib)
-(require 'f)
-(require 's)
 (require 'dash)
 (require 'lean4-settings)
 
@@ -38,16 +36,18 @@ 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
+                            (file-name-directory root)))))
     lean4-rootdir))
 
 (defun lean4-get-rootdir ()
   "Search for lean executable in `lean4-rootdir' and variable `exec-path'.
 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))