From 245d36147e879a485e6dcbc383cbf2f4dc0ecd5f Mon Sep 17 00:00:00 2001
From: Mauricio Collares <mauricio@collares.org>
Date: Tue, 21 Sep 2021 09:25:37 -0300
Subject: [PATCH] chore: lean4-mode: support native elisp compilation

---
 lean4-mode/lean4-fringe.el |  9 ++++++---
 lean4-mode/lean4-info.el   | 12 ++++++++----
 lean4-mode/lean4-syntax.el |  1 +
 3 files changed, 15 insertions(+), 7 deletions(-)

diff --git a/lean4-mode/lean4-fringe.el b/lean4-mode/lean4-fringe.el
index aee314ea57..d0ee745640 100644
--- a/lean4-mode/lean4-fringe.el
+++ b/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)
 
diff --git a/lean4-mode/lean4-info.el b/lean4-mode/lean4-info.el
index fbd73a4c98..a2d34c2bc2 100644
--- a/lean4-mode/lean4-info.el
+++ b/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*")
 
diff --git a/lean4-mode/lean4-syntax.el b/lean4-mode/lean4-syntax.el
index e268a5d2f4..5938050124 100644
--- a/lean4-mode/lean4-syntax.el
+++ b/lean4-mode/lean4-syntax.el
@@ -5,6 +5,7 @@
 ;;         Soonho Kong
 ;;
 
+(require 'dash)
 (require 'rx)
 
 (defconst lean4-keywords1