From 7ebe80ad2a3c2defe4d70a0b9ed239d6850ca3c4 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sun, 6 Jun 2021 13:33:39 +0200
Subject: [PATCH] chore: update Nix, Nixpkgs, vscode-lean4

---
 flake.lock       | 44 ++++++++++++++------------------------------
 flake.nix        | 12 +-----------
 nix/packages.nix |  6 +++---
 3 files changed, 18 insertions(+), 44 deletions(-)

diff --git a/flake.lock b/flake.lock
index b0a5f39a2d..a6407fe9f7 100644
--- a/flake.lock
+++ b/flake.lock
@@ -33,15 +33,16 @@
     "lowdown-src": {
       "flake": false,
       "locked": {
-        "lastModified": 1598695561,
-        "narHash": "sha256-gyH/5j+h/nWw0W8AcR2WKvNBUsiQ7QuxqSJNXAwV+8E=",
+        "lastModified": 1617481909,
+        "narHash": "sha256-SqnfOFuLuVRRNeVJr1yeEPJue/qWoCp5N6o5Kr///p4=",
         "owner": "kristapsdz",
         "repo": "lowdown",
-        "rev": "1705b4a26fbf065d9574dce47a94e8c7c79e052f",
+        "rev": "148f9b2f586c41b7e36e73009db43ea68c7a1a4d",
         "type": "github"
       },
       "original": {
         "owner": "kristapsdz",
+        "ref": "VERSION_0_8_4",
         "repo": "lowdown",
         "type": "github"
       }
@@ -68,11 +69,11 @@
         "nixpkgs": "nixpkgs"
       },
       "locked": {
-        "lastModified": 1611597793,
-        "narHash": "sha256-xL3NQJnuGvvay+PWFCQ3fShZHwmiy0PmgqHX6yFUX0M=",
+        "lastModified": 1622809115,
+        "narHash": "sha256-0lfX3ihV+5VsOs40eSzNMUSNlmH6MRqkb+VDWaJNEzw=",
         "owner": "NixOS",
         "repo": "nix",
-        "rev": "36c4d6f59247826dde32ad2e6b5a9471a9a1c911",
+        "rev": "8e6ee1b9e924fbbbeb5594eb89e7a570f36ab6e1",
         "type": "github"
       },
       "original": {
@@ -83,42 +84,26 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1602702596,
-        "narHash": "sha256-fqJ4UgOb4ZUnCDIapDb4gCrtAah5Rnr2/At3IzMitig=",
+        "lastModified": 1622593737,
+        "narHash": "sha256-9loxFJg85AbzJrSkU4pE/divZ1+zOxDy2FSjlrufCB8=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "ad0d20345219790533ebe06571f82ed6b034db31",
+        "rev": "bb8a5e54845012ed1375ffd5f317d2fdf434b20e",
         "type": "github"
       },
       "original": {
         "id": "nixpkgs",
-        "ref": "nixos-20.09-small",
+        "ref": "nixos-21.05-small",
         "type": "indirect"
       }
     },
-    "nixpkgs-vscode": {
-      "locked": {
-        "lastModified": 1617984351,
-        "narHash": "sha256-mo/tmR1sVmQ+4uziIAZpdNnr9AG0NAAo9Md3tucf73k=",
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "842f900e73c7ce985218cc4f455e34d1d56475c1",
-        "type": "github"
-      },
-      "original": {
-        "owner": "NixOS",
-        "ref": "nixpkgs-unstable",
-        "repo": "nixpkgs",
-        "type": "github"
-      }
-    },
     "nixpkgs_2": {
       "locked": {
-        "lastModified": 1609349023,
-        "narHash": "sha256-Iw+A25SO8zAltCKcJubl7RzgA/eKCx2oHNBvHwmYTpM=",
+        "lastModified": 1620531839,
+        "narHash": "sha256-csv2CWwRHdNO8ZgIgBmzzCVsPj77djXn3ZiDduJtjOs=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "bea44d5ebe332260aa34a1bd48250b6364527356",
+        "rev": "9b80b8324c837feef5a88930a8b734d30c1f9a95",
         "type": "github"
       },
       "original": {
@@ -135,7 +120,6 @@
         "mdBook": "mdBook",
         "nix": "nix",
         "nixpkgs": "nixpkgs_2",
-        "nixpkgs-vscode": "nixpkgs-vscode",
         "temci": "temci"
       }
     },
diff --git a/flake.nix b/flake.nix
index b49ebe536a..861bdefa60 100644
--- a/flake.nix
+++ b/flake.nix
@@ -2,8 +2,6 @@
   description = "Lean interactive theorem prover";
 
   inputs.nixpkgs.url = github:NixOS/nixpkgs/nixpkgs-unstable;
-  # HACK: remove when ccache(?) works with nixpkgs master again
-  inputs.nixpkgs-vscode.url = github:NixOS/nixpkgs/nixpkgs-unstable;
   inputs.flake-utils.url = github:numtide/flake-utils;
   inputs.temci = {
     url = github:parttimenerd/temci;
@@ -24,20 +22,12 @@
     inputs.mdBook.follows = "mdBook";
   };
 
-  outputs = { self, nixpkgs, nixpkgs-vscode, flake-utils, temci, nix, mdBook, lean-stage0 }: flake-utils.lib.eachDefaultSystem (system:
+  outputs = { self, nixpkgs, flake-utils, temci, nix, mdBook, lean-stage0 }: flake-utils.lib.eachDefaultSystem (system:
     let
-      pkgs-vscode = import nixpkgs-vscode {
-        inherit system;
-        # for `vscode-with-extensions`
-        config.allowUnfree = true;
-      };
       pkgs = import nixpkgs {
         inherit system;
         # for `vscode-with-extensions`
         config.allowUnfree = true;
-        overlays = [
-          (self: super: { inherit (pkgs-vscode) vscode-with-extensions; })
-        ];
       };
       lean-packages = pkgs.callPackage (./nix/packages.nix) { inherit nix temci mdBook; };
     in {
diff --git a/nix/packages.nix b/nix/packages.nix
index 87761b0d7e..ac8116ac27 100644
--- a/nix/packages.nix
+++ b/nix/packages.nix
@@ -62,8 +62,8 @@ let
   vscode-lean4 = vscode-utils.extensionFromVscodeMarketplace {
       name = "lean4";
       publisher = "leanprover";
-      version = "0.0.23";
-      sha256 = "sha256-DlP3O2mMAIXV7XwcZFHpa4Vp/9cxxtu9O+gQUW8MddA=";
+      version = "0.0.30";
+      sha256 = "sha256-tx0F3COuDT52y7OC9ymxoye5vfgV7Lv/iB6qrzU3/P4=";
   };
   lean-vscode = vscode-with-extensions.override {
     vscodeExtensions = [ vscode-lean4 ];
@@ -73,7 +73,7 @@ let
     src = mdBook;
     cargoDeps = drv.cargoDeps.overrideAttrs (_: {
       inherit src;
-      outputHash = "sha256-j14HdGcDtWpFFn/lTlbvQFsM7JLSc+OsSOooliiP4tw=";
+      outputHash = "sha256-yunC62ISnWZ5ifbJPWq+TrFkajBRNYhYq+zofAOAo1U=";
     });
     doCheck = false;
   });