From b67be71d21a9d266bf15e48e2c5ece7f62107dd6 Mon Sep 17 00:00:00 2001
From: Andrea Ciceri <andrea.ciceri@autistici.org>
Date: Wed, 8 Jan 2025 15:18:53 +0100
Subject: [PATCH] `lean4-mode` in Emacs

---
 hmModules/emacs/init.el     |  2 ++
 packages/emacs/packages.nix | 18 ++++++++++++++++++
 2 files changed, 20 insertions(+)

diff --git a/hmModules/emacs/init.el b/hmModules/emacs/init.el
index f33aa1d..acb1726 100644
--- a/hmModules/emacs/init.el
+++ b/hmModules/emacs/init.el
@@ -507,6 +507,8 @@
 (use-package dockerfile-ts-mode
   :mode "Dockerfile\\'")
 
+(use-package lean4-mode
+  :mode "\\.lean\\'")
 (use-package python-ts-mode
   :hook ((python-ts-mode . (lambda ()
 			     (require 'eglot)
diff --git a/packages/emacs/packages.nix b/packages/emacs/packages.nix
index 9abb207..8300a07 100644
--- a/packages/emacs/packages.nix
+++ b/packages/emacs/packages.nix
@@ -10,6 +10,7 @@ let
       version = args.src.rev;
       propagatedUserEnvPkgs = args.deps;
       buildInputs = args.deps;
+      postInstall = args.postInstall or "";
     };
 
   # *Attrset* containig extra emacs packages
@@ -60,6 +61,23 @@ let
         f
       ];
     };
+    lean4-mode = buildEmacsPackage {
+      name = "lean4-mode";
+      src = pkgs.fetchFromGitHub {
+        owner = "leanprover-community";
+        repo = "lean4-mode";
+        rev = "76895d8939111654a472cfc617cfd43fbf5f1eb6";
+        hash = "sha256-DLgdxd0m3SmJ9heJ/pe5k8bZCfvWdaKAF0BDYEkwlMQ=";
+      };
+      deps = [
+        epkgs.dash
+        melpaPackages.magit
+        melpaPackages.lsp-mode
+      ];
+      postInstall = ''
+        cp -r $src/data $LISPDIR
+      '';
+    };
   };
 
   # *List* containing emacs packages from (M)ELPA