From fa5d12b784f0bf09e473e79eecd6527e956d334d Mon Sep 17 00:00:00 2001
From: stuebinm
Date: Fri, 14 Jun 2024 21:48:54 +0200
Subject: home: remove lean

having tried multiple times, it's not actually very possible or
reasonable to attempt to keep lean's version in sync with whatever
mathlib requires at any given time, and probably better to have it just
be managed by elan, no matter how annoying that may be.
---
 home/packages.nix | 2 +-
 pkgs/overlay.nix  | 3 ---
 2 files changed, 1 insertion(+), 4 deletions(-)

diff --git a/home/packages.nix b/home/packages.nix
index ca923ca..16e8e3c 100644
--- a/home/packages.nix
+++ b/home/packages.nix
@@ -45,7 +45,7 @@ in
     haskell-language-server
     haskellPackages.hoogle haskellPackages.stylish-haskell
     # other functional things
-    racket dhall lean4 dune_2 ocamlPackages.utop ocamlPackages.ocp-indent
+    racket dhall dune_2 ocamlPackages.utop ocamlPackages.ocp-indent
     ocamlPackages.merlin ocaml gauche
     (agda.withPackages (p: [ p.standard-library p.cubical ]))
     (twelf.overrideAttrs (old:  {
diff --git a/pkgs/overlay.nix b/pkgs/overlay.nix
index 5379bbf..4e9f741 100644
--- a/pkgs/overlay.nix
+++ b/pkgs/overlay.nix
@@ -14,9 +14,6 @@ in
 {
   beam = super.beam_nox;
 
-  inherit (unstable) lean4;
-
-
   git-annex-remote-remarkable2 = self.callPackage
     ({ rustPlatform, fetchgit, ... }:
       rustPlatform.buildRustPackage rec {
-- 
cgit v1.2.3