diff --git a/lean4-mode.el b/lean4-mode.el
index e10c2d5..9e6c2bb 100644
--- a/lean4-mode.el
+++ b/lean4-mode.el
@@ -10,7 +10,7 @@
 ;; Maintainer: Yury G. Kudryashov <urkud@urkud.name>
 ;; Created: Jan 09, 2014
 ;; Keywords: languages
-;; Package-Requires: ((emacs "27.1") (magit-section "2.90.1") (lsp-mode "8.0.0"))
+;; Package-Requires: ((emacs "27.1") (compat "28.1") (magit-section "2.90.1") (lsp-mode "8.0.0"))
 ;; URL: https://github.com/leanprover/lean4-mode
 ;; SPDX-License-Identifier: Apache-2.0
 ;; Version: 1.0.1
diff --git a/lean4-util.el b/lean4-util.el
index 77d2ebd..4af725e 100644
--- a/lean4-util.el
+++ b/lean4-util.el
@@ -56,8 +56,7 @@ 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 ((default-directory (lean4-get-rootdir)))
-    (expand-file-name exe-name (expand-file-name "bin"))))
+  (file-name-concat (lean4-get-rootdir) "bin" exe-name))
 
 (defun lean4-whitespace-cleanup ()
   "Delete trailing whitespace if `lean4-delete-trailing-whitespace' is t."