diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el index 62b82ef4a6..1ffa260b84 100644 --- a/src/emacs/lean-mode.el +++ b/src/emacs/lean-mode.el @@ -153,6 +153,7 @@ will be flushed everytime it's executed." `("--cache" ,cache-file-name) '())) (lean-mode-option "--lean") + (default-directory (or (lean-project-find-root) default-directory)) (process-args (append `(,process-name ,process-buffer-name ,(lean-get-executable lean-executable-name) diff --git a/src/emacs/lean-project.el b/src/emacs/lean-project.el index 5550fe9095..63f6687aba 100644 --- a/src/emacs/lean-project.el +++ b/src/emacs/lean-project.el @@ -11,7 +11,10 @@ "Project file name") (defun lean-project-find-root () - (lean-find-file-upward lean-project-file-name)) + (let ((p (f--traverse-upwards (f-exists? (f-expand lean-project-file-name it)) + (f-dirname (buffer-file-name))))) + (if p (file-name-as-directory p) + nil))) (defun lean-project-inside-p () (if (lean-project-find-root) t nil))