chore: lean4-mode: support native elisp compilation

lean4-mode/lean4-fringe.el

@@ -11,11 +11,14 @@
 ;;
 ;;; Code:
 
+(require 'lean4-settings)
+(require 'lsp-mode)
 (require 'lsp-protocol)
 
-(lsp-interface
- (lean:LeanFileProgressProcessingInfo (:range) nil)
- (lean:LeanFileProgressParams (:textDocument :processing) nil))
+(eval-when-compile
+  (lsp-interface
+    (lean:LeanFileProgressProcessingInfo (:range) nil)
+    (lean:LeanFileProgressParams (:textDocument :processing) nil)))
 
 (defvar-local lean4-fringe-delay-timer nil)
 

lean4-mode/lean4-info.el

@@ -14,7 +14,10 @@
 ;; Released under Apache 2.0 license as described in the file LICENSE.
 ;;
 
+(require 'dash)
 (require 'lean4-syntax)
+(require 'lean4-settings)
+(require 'lsp-mode)
 (require 'lsp-protocol)
 (require 'magit-section)
 
@@ -61,10 +64,11 @@
    ;; current window of current buffer is selected (i.e., in focus)
    (eq (current-buffer) (window-buffer))))
 
-(lsp-interface
- (lean:PlainGoal (:goals) nil)
- (lean:PlainTermGoal (:goal) nil)
- (lean:Diagnostic (:range :fullRange :message) (:code :relatedInformation :severity :source :tags)))
+(eval-when-compile
+  (lsp-interface
+    (lean:PlainGoal (:goals) nil)
+    (lean:PlainTermGoal (:goal) nil)
+    (lean:Diagnostic (:range :fullRange :message) (:code :relatedInformation :severity :source :tags))))
 
 (defconst lean4-info-buffer-name "*Lean Goal*")
 

lean4-mode/lean4-syntax.el

@@ -5,6 +5,7 @@
 ;;         Soonho Kong
 ;;
 
+(require 'dash)
 (require 'rx)
 
 (defconst lean4-keywords1