From e00a945ae2425c20828bc244bcf4816556af8494 Mon Sep 17 00:00:00 2001
From: Stefan Ellmauthaler <stefan.ellmauthaler@tu-dresden.de>
Date: Mon, 25 Sep 2023 13:34:45 +0200
Subject: [PATCH] add lean 4 mode to emacs

---
 modules/emacs/default.el   |  6 ++++++
 modules/emacs/default.nix  |  2 +-
 modules/emacs/packages.nix | 21 +++++++++++++++++++++
 3 files changed, 28 insertions(+), 1 deletion(-)

diff --git a/modules/emacs/default.el b/modules/emacs/default.el
index e173b2a..6390670 100644
--- a/modules/emacs/default.el
+++ b/modules/emacs/default.el
@@ -640,6 +640,12 @@
   :init
   (apheleia-global-mode t))
 
+;; lean4-mode
+(use-package lean4-mode
+  :defer t
+  :mode "\\.lean\\'"
+  :commands lean4-mode)
+
 (custom-set-faces
  ;; custom-set-faces was added by Custom.
  ;; If you edit it by hand, you could mess it up, so be careful.
diff --git a/modules/emacs/default.nix b/modules/emacs/default.nix
index ded0249..1416a80 100644
--- a/modules/emacs/default.nix
+++ b/modules/emacs/default.nix
@@ -95,7 +95,7 @@ with lib; let
         yasnippet
         #zenburn-theme
       ]
-      ++ (with lpkgs; [org-roam-ui ligatures])));
+      ++ (with lpkgs; [org-roam-ui ligatures] lean4-mode)));
 in {
   options.elss.programs.emacs.enable =
     mkEnableOption "Setup emacs package and install it";
diff --git a/modules/emacs/packages.nix b/modules/emacs/packages.nix
index c5827af..9c88a10 100644
--- a/modules/emacs/packages.nix
+++ b/modules/emacs/packages.nix
@@ -32,4 +32,25 @@ in
         sha256 = "baFDkfQLM2MYW2QhMpPnOMSfsLlcp9fO5xfyioZzOqg=";
       };
     };
+
+    lean4-mode = trivialBuild {
+      pname = "lean4-mode";
+      version = "unstable-2023-07-14";
+      src = pkgs.fetchFromGitHub {
+        owner = "leanprover";
+        repo = "lean4-mode";
+        rev = "d1c936409ade7d93e67107243cbc0aa55cda7fd5";
+        sha256 = "tD5Ysa24fMIS6ipFc50OjabZEUge4riSb7p4BR05ReQ=";
+      };
+      packageRequires = with epkgs.melpaPackages; [
+        dash
+        f
+        flycheck
+        lsp-mode
+        magit
+      ];
+      postInstall = ''
+        install -m=755 -D $src/data/abbreviations.json $out/share/emacs/site-lisp/data/abbreviations.json
+      '';
+    };
   }