summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorstuebinm2023-09-23 20:33:14 +0200
committerstuebinm2023-09-23 20:33:14 +0200
commitb29058e9e5941e304d4df7362c1ffa90e350b049 (patch)
treedf111eef1325a9eafd4af838be54c98e531f1798
parentb6b9768cea038183be2b26613f4466d9a3a3e8a8 (diff)
home: add lean4
Diffstat (limited to '')
-rw-r--r--home/packages.nix2
-rw-r--r--pkgs/overlay.nix18
2 files changed, 19 insertions, 1 deletions
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/
+ '';
+ });
}