Wrap lsp-interface invocations into eval-and-compile

This fixes the issue reported and detailedly discussed at:
https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs/topic/lsp-mode.20errors.20due.20to.20list.20!.3D.20hash-table

Also, make code fit into fill-column.

lean4-fringe.el

@@ -26,9 +26,10 @@
 (require 'lsp-mode)
 (require 'lsp-protocol)
 
-(lsp-interface
- (lean:LeanFileProgressProcessingInfo (:range :kind) nil)
- (lean:LeanFileProgressParams (:textDocument :processing) nil))
+(eval-and-compile
+  (lsp-interface
+   (lean:LeanFileProgressProcessingInfo (:range :kind) nil)
+   (lean:LeanFileProgressParams (:textDocument :processing) nil)))
 
 (defvar-local lean4-fringe-delay-timer nil)
 

lean4-info.el

@@ -72,10 +72,13 @@ The buffer is supposed to be the *Lean Goal* buffer."
    ;; 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-and-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*")