add lean 4 mode to emacs

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.

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";

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
+      '';
+    };
   }