From b29058e9e5941e304d4df7362c1ffa90e350b049 Mon Sep 17 00:00:00 2001
From: stuebinm
Date: Sat, 23 Sep 2023 20:33:14 +0200
Subject: home: add lean4

---
 home/packages.nix |  2 +-
 pkgs/overlay.nix  | 18 ++++++++++++++++++
 2 files changed, 19 insertions(+), 1 deletion(-)

diff --git a/home/packages.nix b/home/packages.nix
index 10cb78e..4ed480e 100644
--- a/home/packages.nix
+++ b/home/packages.nix
@@ -38,7 +38,7 @@ in
     haskell-language-server
     haskellPackages.hoogle haskellPackages.stylish-haskell
     # other functional things
-    racket dhall lean dune_2 ocamlPackages.utop ocamlPackages.ocp-indent
+    racket dhall lean4 dune_2 ocamlPackages.utop ocamlPackages.ocp-indent
     ocamlPackages.merlin ocaml gauche
     (agda.withPackages (p: [ p.standard-library p.cubical ]))
     # html, js & co
diff --git a/pkgs/overlay.nix b/pkgs/overlay.nix
index 09ca9ee..ebea1a0 100644
--- a/pkgs/overlay.nix
+++ b/pkgs/overlay.nix
@@ -102,4 +102,22 @@ in
   mu = oldstable.mu;
 
   matrix-to = self.callPackage ./matrix-to.nix {};
+
+  lean4 = unstable.lean4.overrideAttrs (old: rec {
+    version = "4.1.0-rc1";
+    src = self.fetchFromGitHub {
+      owner = "leanprover";
+      repo = "lean4";
+      rev = "v${version}";
+      hash = "sha256-OQ72uweFMSkOzJ9u92enNql48ReZ+NBlnXtnanH+ZVA=";
+    };
+    postPatch = ''
+      substituteInPlace src/CMakeLists.txt \
+        --replace 'set(GIT_SHA1 "")' 'set(GIT_SHA1 "${src.rev}")'
+
+      # Remove tests that fails in sandbox.
+      # It expects `sourceRoot` to be a git repository.
+      rm -rf src/lake/examples/git/
+    '';
+  });
 }
-- 
cgit v1.2.3