From a53ea4a87ec28209abf490e0f9e7d13a84796839 Mon Sep 17 00:00:00 2001
From: Smaug123 <patrick+github@patrickstevens.co.uk>
Date: Sun, 12 Dec 2021 18:09:38 +0000
Subject: [PATCH] Fix Lean3 VSCode

---
 home.nix | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

diff --git a/home.nix b/home.nix
index fc567f7..bbd1121 100644
--- a/home.nix
+++ b/home.nix
@@ -1,6 +1,6 @@
 { config, pkgs, ... }:
 
-let username = "Patrick"; in
+let username = "patrick"; in
 let dotnet = pkgs.dotnet-sdk_6; in
 
 {
@@ -51,6 +51,8 @@ let dotnet = pkgs.dotnet-sdk_6; in
       #pkgs.agda
       pkgs.pijul
       pkgs.universal-ctags
+      pkgs.asciinema
+      pkgs.git-lfs
     ];
 
   programs.vscode = {
@@ -68,7 +70,9 @@ let dotnet = pkgs.dotnet-sdk_6; in
         "git.path" = "${pkgs.git}/bin/git";
         "update.mode" = "none";
         "docker.dockerPath" = "${pkgs.docker}/bin/docker";
-        "lean.leanpkgPath" = "${pkgs.elan}/bin/leanpkg";
+        "lean.leanpkgPath" = "/Users/${username}/.elan/toolchains/stable/bin/leanpkg";
+        "lean.executablePath" = "/Users/${username}/.elan/toolchains/stable/bin/lean";
+        "lean.memoryLimit" = 8092;
       };
   };
 
@@ -94,6 +98,7 @@ let dotnet = pkgs.dotnet-sdk_6; in
       LC_ALL = "en_US.UTF-8";
       LC_CTYPE = "en_US.UTF-8";
       RUSTFLAGS = "-L ${pkgs.libiconv}/lib";
+      RUST_BACKTRACE = "full";
     };
     shellAliases = {
       vim = "nvim";
@@ -134,6 +139,12 @@ let dotnet = pkgs.dotnet-sdk_6; in
       advice = {
         addIgnoredFile = false;
       };
+      "filter \"lfs\"" = {
+         clean = "${pkgs.git-lfs} clean -- %f";
+         smudge = "${pkgs.git-lfs}/bin/git-lfs smudge --skip -- %f";
+         process = "${pkgs.git-lfs}/bin/git-lfs filter-process";
+         required = true;
+      };
     };
   };