From ea00b852ff8aa8cd77ae96223aa2ef77261da6ac Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Mon, 13 Jan 2025 02:24:10 +0100 Subject: [PATCH] Dissolve -util in favor of -mode and new -exec The lean4-exec.el feature has been written from scratch. Its logic is simple: For Elan, Lake and Lean respectively, there is a hook of functions which may return a path to the respective program. Well, there are some more details to it but its great at being minimalist but scalable. --- lean4-exec.el | 208 ++++++++++++++++++++++++++++++++++++++++++++++++++ lean4-mode.el | 131 +++++++++++++++++-------------- lean4-util.el | 110 -------------------------- 3 files changed, 280 insertions(+), 169 deletions(-) create mode 100644 lean4-exec.el delete mode 100644 lean4-util.el diff --git a/lean4-exec.el b/lean4-exec.el new file mode 100644 index 0000000..2d5673c --- /dev/null +++ b/lean4-exec.el @@ -0,0 +1,208 @@ +;;; lean4-exec.el --- Lean4-Mode Executable Location -*- lexical-binding: t; -*- + +;; Copyright (c) 2024 Mekeor Melire + +;; This file is not part of GNU Emacs. + +;; Licensed under the Apache License, Version 2.0 (the "License"); you +;; may not use this file except in compliance with the License. You +;; may obtain a copy of the License at +;; +;; http://www.apache.org/licenses/LICENSE-2.0 +;; +;; Unless required by applicable law or agreed to in writing, software +;; distributed under the License is distributed on an "AS IS" BASIS, +;; WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or +;; implied. See the License for the specific language governing +;; permissions and limitations under the License. + +;;; Commentary: + +;; TODO + +;;; Code: + +;;;; Elan + +(defcustom lean4-exec-elan-base "elan" + "Basename of Elan executable (without suffixes, if any)." + :group 'lean4-exec + :type 'string) + +(defvar-local lean4-exec-elan-full nil + "Full name of Elan executable. + +It may be nil in which case Elan won't be used. Otherwise it should be +a list of strings, for example: + + (\"docker\" \"compose\" \"debian\" \"exec\" \"elan\") + +Member strings should not be quoted. Consumers of this variable are +expected to quote as needed, e.g. by using `combine-and-quote-strings' +if necessary.") + +(defun lean4-exec-elan-executable-find () + "Attempt to find Elan executable with `executable-find'." + (declare (side-effect-free t)) + (ensure-list (executable-find lean4-exec-elan-base))) + +(defcustom lean4-exec-elan-hook + (list #'lean4-exec-elan-executable-find) + "Hook of functions to determine `lean4-exec-elan-full'. + +This hook is called from `lean4-exec-elan-init'. Each member function +represents a certain method of determining a value suitable for +`lean4-exec-elan-full', which see. If it does not find such a value, it +should return nil. It should probably use `lean4-exec-elan-base' (and +maybe `executable-binary-suffixes') instead of a hard-coded basename for +the Elan executable." + :group 'lean4-exec + :options '(lean4-exec-elan-executable-find) + :type 'hook) + +(defun lean4-exec-elan-init () + "Buffer-locally set up `lean4-exec-elan-full'. + +Call functions from `lean4-exec-elan-hook' until one succeeds, +i.e. returns non-nil. `lean4-exec-elan-full' is then buffer-locally set +to this value." + (setq-local lean4-exec-elan-full + (run-hook-with-args-until-success + 'lean4-exec-elan-hook))) + +;;;; Lake + +(defcustom lean4-exec-lake-base "lake" + "Basename of Lake executable (without suffixes, if any)." + :group 'lean4-exec + :type 'string) + +(defvar-local lean4-exec-lake-full nil + "Full name of Lake executable. + +It may be nil in which case Lake won't be used. Otherwise it should be +a list of strings, for example: + + (\"docker\" \"compose\" \"debian\" \"exec\" \"lake\") + +Member strings should not be quoted. Consumers of this variable are +expected to quote as needed, e.g. by using `combine-and-quote-strings' +if necessary.") + +(defun lean4-exec-lake-elan-which () + "When `lean4-exec-elan-full', then attemp to find Lake with Elan." + (declare (side-effect-free t)) + (when lean4-exec-elan-full + (ignore-errors + ;; This assumes that "elan which lake" outputs only a single + ;; line and a final newline. In particular it assumes that the + ;; path to the Lake executable does not contain newlines. + (apply #'process-lines + (append lean4-exec-elan-full '("which" "lake")))))) + +(defun lean4-exec-lake-executable-find () + "Attempt to find Lake executable with `executable-find'." + (declare (side-effect-free t)) + (ensure-list (executable-find lean4-exec-lake-base))) + +(defcustom lean4-exec-lake-hook + (list + #'lean4-exec-lake-elan-which + #'lean4-exec-lake-executable-find) + "Hook of functions to determine `lean4-exec-lake-full'. + +This hook is called from `lean4-exec-lake-init'. Each member function +represents a certain method of determining a value suitable for +`lean4-exec-lake-full', which see. If it does not find such a value, it +should return nil. It should probably use `lean4-exec-lake-base' (and +maybe `executable-binary-suffixes') instead of a hard-coded basename for +the Lake executable." + :group 'lean4-exec + :options '(lean4-exec-lake-executable-find) + :type 'hook) + +(defun lean4-exec-lake-init () + "Buffer-locally set up `lean4-exec-lake-full'. + +Call functions from `lean4-exec-lake-hook' until one succeeds, +i.e. returns non-nil. `lean4-exec-lake-full' is then buffer-locally set +to this value." + (setq-local lean4-exec-lake-full + (run-hook-with-args-until-success + 'lean4-exec-lake-hook))) + +;;;; Lean + +(defcustom lean4-exec-lean-base "lean" + "Basename of Lean4 executable (without suffixes, if any)." + :group 'lean4-exec + :type 'string) + +(defvar-local lean4-exec-lean-full nil + "Full name of Lean4 executable. + +It should be a list of strings, for example: + + (\"docker\" \"compose\" \"debian\" \"exec\" \"lake\" \"lean\") + +Member strings should not be quoted. Consumers of this variable are +expected to quote as needed, e.g. by using `combine-and-quote-strings' +if necessary.") + +(defun lean4-exec-lean-getenv () + "Attempt to find Lean4 executable per `LEAN' environment variable." + (declare (side-effect-free t)) + (ensure-list (getenv "LEAN"))) + +(defun lean4-exec-lean-elan-which () + "When `lean4-exec-elan-full', then attemp to find Lean with Elan." + (declare (side-effect-free t)) + (when lean4-exec-elan-full + (ignore-errors + ;; This assumes that "elan which lean" outputs only a single + ;; line and a final newline. In particular it assumes that the + ;; path to the Lean executable does not contain newlines. + (apply #'process-lines + (append lean4-exec-elan-full '("which" "lean")))))) + +(defun lean4-exec-lean-lake () + "When `lean4-exec-lake-full', return `lean' as its subcommand." + (declare (side-effect-free error-free)) + (when lean4-exec-lake-full + (append lean4-exec-lake-full + ;; We do not use `lean4-exec-lean-base' here because a + ;; user could have set it to "lean4" but Lake only accepts + ;; "lean" as subcommand. + '("lake")))) + +(defcustom lean4-exec-lean-hook + (list + #'lean4-exec-lean-getenv + #'lean4-exec-lean-elan-which + #'lean4-exec-lean-lake) + "Hook of functions to determine `lean4-exec-lean-full'. + +This hook is called from `lean4-exec-lean-init'. Each member function +represents a certain method of determining a value suitable for +`lean4-exec-lean-full', which see. If it does not find such a value, it +should return nil. It should probably use `lean4-exec-lean-base' (and +maybe `executable-binary-suffixes') instead of a hard-coded basename for +the Lean4 executable." + :group 'lean4-exec + :options '(lean4-exec-lean-getenv + lean4-exec-lean-elan-which + lean4-exec-lean-lake) + :type 'hook) + +(defun lean4-exec-lean-init () + "Buffer-locally set up `lean4-exec-lean-full'. + +Call functions from `lean4-exec-lean-hook' until one succeeds, +i.e. returns non-nil. `lean4-exec-lean-full' is then buffer-locally set +to this value." + (setq-local lean4-exec-lean-full + (run-hook-with-args-until-success + 'lean4-exec-lean-hook))) + +(provide 'lean4-exec) +;;; lean4-exec.el ends here diff --git a/lean4-mode.el b/lean4-mode.el index 371ddbb..135cfa8 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -45,10 +45,10 @@ (require 'pcase) (require 'lean4-eri) +(require 'lean4-exec) (require 'lean4-fringe) (require 'lean4-info) (require 'lean4-syntax) -(require 'lean4-util) (require 'dash) (require 'lsp-mode) @@ -76,13 +76,18 @@ :link '(emacs-library-link :tag "Library Source" "lean4-mode.el") :prefix "lean4-") -(defun lean4-compile-string (lake-name exe-name args file-name) - "Command to run EXE-NAME with extra ARGS and FILE-NAME. -If LAKE-NAME is nonempty, then prepend \"LAKE-NAME env\" to the command -\"EXE-NAME ARGS FILE-NAME\"." - (if lake-name - (format "%s env %s %s %s" lake-name exe-name args file-name) - (format "%s %s %s" exe-name args file-name))) +(defcustom lean4-delete-trailing-whitespace nil + "Delete trailing whitespace before saving buffer to file. + +If this variable is non-nil, Lean4-Mode will delete trailing whitespace +of every line before the buffer is saved to file." + :group 'lean4 + :type 'boolean) + +(defun lean4-whitespace-cleanup () + "When `lean4-delete-trailing-whitespace', delete trailing whitespace." + (when lean4-delete-trailing-whitespace + (delete-trailing-whitespace))) (defun lean4-create-temp-in-system-tempdir (file-name prefix) "Create a temp lean file and return its name. @@ -90,22 +95,6 @@ The new file has prefix PREFIX (defaults to `flymake') and the same extension as 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." - (interactive "sArgument to Lean4 executable: ") - (let* ((use-lake (lean4-lake-find-dir)) - (default-directory (if use-lake (lean4-lake-find-dir) - default-directory)) - (target-file-name - (or - (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 (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 (expand-file-name target-file-name)))))) - (defun lean4-refresh-file-dependencies () "Refresh the file dependencies. @@ -124,7 +113,7 @@ file, recompiling, and reloading all imports." :text (lsp--buffer-content))))) (defun lean4-tab-indent () - "Lean 4 function for TAB indent." + "Lean4 function for TAB indent." (interactive) (cond ((looking-back (rx line-start (* white)) nil) (lean4-eri-indent)) @@ -132,8 +121,6 @@ file, recompiling, and reloading all imports." (defvar-keymap lean4-mode-map :doc "Keymap for `lean4-mode'." - "C-c C-x" #'lean4-execute - "C-c C-l" #'lean4-execute "C-c C-k" #'quail-show-key "TAB" #'lean4-tab-indent "C-c C-i" #'lean4-toggle-info @@ -142,25 +129,23 @@ file, recompiling, and reloading all imports." (easy-menu-define lean4-mode-menu lean4-mode-map "Menu for the Lean major mode." - `("Lean 4" - ["Execute lean" lean4-execute t] - ["Toggle info display" lean4-toggle-info t] + `("Lean4" + ["Toggle info display" lean4-toggle-info t] ;; TODO: Bug#91: We offers a Flycheck-based menu-item when ;; Flycheck is in use. Users who use built-in Flymake should also ;; be offered a working menu-item. Alternatively, the menu-item ;; could also be dropped for both cases. - ["List of errors" flycheck-list-errors (bound-and-true-p flycheck-mode)] - ["Restart lean process" lsp-workspace-restart t] - ["Customize lean4-mode" (customize-group 'lean) t])) + ["List of errors" flycheck-list-errors (bound-and-true-p flycheck-mode)] + ["Restart Lean4 LSP server" lsp-workspace-restart t] + ["Customize lean4-mode" (customize-group 'lean4) t])) (defun lean4-lsp-init-workspace () - "Create an LSP workspace. + "Initialize Lean4 `lsp-mode' workspace. -Starting from `(buffer-file-name)`, repeatedly look up the -directory hierarchy for a directory containing a file -\"lean-toolchain\", and use the last such directory found, if any. -This allows us to edit files in child packages using the settings -of the parent project." +Starting from function `buffer-file-name', repeatedly look up the +directory hierarchy for a directory containing a file `lean-toolchain', +and use the last such directory found, if any. This allows us to edit +files in child packages using the settings of the parent project." (let (root) (when-let ((file-name (buffer-file-name))) (while-let ((dir (locate-dominating-file file-name "lean-toolchain"))) @@ -182,8 +167,21 @@ of the parent project." (require 'lean4-input) (set-input-method "Lean4")) +(defun lean4-init-compile-command () + "When `lean4-exec-lean-full', setup `compile-command' for `lean4-mode'." + (interactive) + (when lean4-exec-lean-full + (setq-local compile-command + (string-join (append lean4-exec-lean-full + '("build")) + " ")))) + (defcustom lean4-mode-hook (list #'lean4-init-input-method + #'lean4-exec-elan-init + #'lean4-exec-lake-init + #'lean4-exec-lean-init + #'lean4-init-compile-command #'lean4-lsp-init-semantic-token #'lean4-lsp-init-workspace #'lsp) @@ -194,6 +192,10 @@ it will be called by `lsp'. Similarly, `flycheck-mode' should not be added here because it will be called by `lsp' if the variable `lsp-diagnostics-provider' is set accordingly." :options '(lean4-init-input-method + lean4-exec-elan-init + lean4-exec-lake-init + lean4-exec-lean-init + lean4-init-compile-command lean4-lsp-init-semantic-token lean4-lsp-init-workspace lsp) @@ -293,31 +295,42 @@ outside a project will default to that mode." (add-to-list 'markdown-code-lang-modes '("lean" . lean4-select-mode))) -;; Use utf-8 encoding -;;;### autoload +;; According to the Lean4 reference manual, Lean4 code must be encoded +;; as `utf-8': +;; https://lean-lang.org/doc/reference/latest/Source-Files/Files/ +;;;###autoload (modify-coding-system-alist 'file "\\.lean\\'" 'utf-8) -;; LSP init -;; Ref: https://emacs-lsp.github.io/lsp-mode/page/adding-new-language/ +;; https://emacs-lsp.github.io/lsp-mode/page/adding-new-language/ (add-to-list 'lsp-language-id-configuration - '(lean4-mode . "lean")) - -(defun lean4--server-cmd () - "Return Lean server command. -If found lake version at least 3.1.0, then return '/path/to/lake serve', -otherwise return '/path/to/lean --server'." - (condition-case nil - (if (string-version-lessp (car (process-lines (lean4-get-executable "lake") "--version")) "3.1.0") - `(,(lean4-get-executable lean4-executable-name) "--server") - `(,(lean4-get-executable "lake") "serve")) - (error `(,(lean4-get-executable lean4-executable-name) "--server")))) + '(lean4-mode . "lean4")) + +(defun lean4-lsp-server-command () + "Lean4 LSP server command." + (cond + (lean4-exec-lake-full + (append lean4-exec-lake-full '("serve"))) + (lean4-exec-lean-full + (append lean4-exec-lean-full '("--serve"))))) (lsp-register-client - (make-lsp-client :new-connection (lsp-stdio-connection #'lean4--server-cmd) - :major-modes '(lean4-mode) - :server-id 'lean4-lsp - :notification-handlers (ht ("$/lean/fileProgress" #'lean4-fringe-update)) - :semantic-tokens-faces-overrides '(:types (("leanSorryLike" . font-lock-warning-face))))) + (make-lsp-client + :language-id "lean4" + :major-modes '(lean4-mode) + :new-connection + (lsp-stdio-connection #'lean4-lsp-server-command + ;; We don't want to pass the server command to + ;; `executable-find' so that `lean4-exec' + ;; keeps control over the exact path (or not, + ;; if it doesn't want to). + #'always) + :notification-handlers + (ht ("$/lean/fileProgress" #'lean4-fringe-update)) + ;; The semantic token type `leanSorryLike' is a Lean4-specific + ;; extension of LSP. + :semantic-tokens-faces-overrides + '(:types (("leanSorryLike" . font-lock-warning-face))) + :server-id 'lean4)) (provide 'lean4-mode) ;;; lean4-mode.el ends here diff --git a/lean4-util.el b/lean4-util.el deleted file mode 100644 index 5799dc3..0000000 --- a/lean4-util.el +++ /dev/null @@ -1,110 +0,0 @@ -;;; lean4-util.el --- Lean4-Mode Utilities -*- lexical-binding: t; -*- - -;; Copyright (c) 2014 Microsoft Corporation. All rights reserved. - -;; This file is not part of GNU Emacs. - -;; Licensed under the Apache License, Version 2.0 (the "License"); you -;; may not use this file except in compliance with the License. You -;; may obtain a copy of the License at -;; -;; http://www.apache.org/licenses/LICENSE-2.0 -;; -;; Unless required by applicable law or agreed to in writing, software -;; distributed under the License is distributed on an "AS IS" BASIS, -;; WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or -;; implied. See the License for the specific language governing -;; permissions and limitations under the License. - -;;; Commentary: - -;; This library provides utilities for `lean4-mode'. - -;;; Code: - -(require 'compat) - -(defcustom lean4-executable-name - (if (eq system-type 'windows-nt) "lean.exe" "lean") - "Name of lean executable." - :group 'lean4 - :type 'string) - -(defcustom lean4-rootdir nil - "Full pathname of lean root directory. It should be defined by user." - :group 'lean4 - :type 'string) - -(defun lean4-setup-rootdir () - "Search for lean executable in variable `exec-path'. -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 - (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 (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 - (lean4-setup-rootdir) - (error - (concat "Lean was not found in the `exec-path' and `lean4-rootdir' is not defined. " - "Please set it via M-x customize-variable RET lean4-rootdir RET."))))) - -(defun lean4-get-executable (exe-name) - "Return fullpath of lean executable EXE-NAME." - (file-name-concat (lean4-get-rootdir) "bin" exe-name)) - -(defcustom lean4-delete-trailing-whitespace nil - "Automatically delete trailing shitespace. -Set this variable to true to automatically delete trailing -whitespace when a buffer is loaded from a file or when it is -written." - :group 'lean4 - :type 'boolean) - -(defun lean4-whitespace-cleanup () - "Delete trailing whitespace if `lean4-delete-trailing-whitespace' is t." - (when lean4-delete-trailing-whitespace - (delete-trailing-whitespace))) - -(defcustom lean4-lake-name - (if (eq system-type 'windows-nt) "lake.exe" "lake") - "Name of lake executable." - :group 'lean4 - :type 'string) - -(defun lean4-lake-find-dir-in (dir) - "Find a parent directory of DIR with file \"lakefile.lean\"." - (when 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 (directory-file-name (buffer-file-name))))) - -(defun lean4-lake-find-dir-safe () - "Call `lean4-lake-find-dir', error on failure." - (or (lean4-lake-find-dir) - (error "Cannot find lakefile.lean for %s" (buffer-file-name)))) - -(defun lean4-lake-build () - "Call lake build." - (interactive) - (let ((default-directory (file-name-as-directory (lean4-lake-find-dir-safe)))) - (compile (concat (lean4-get-executable lean4-lake-name) " build")))) - -(provide 'lean4-util) -;;; lean4-util.el ends here