From e0d9bc2f9bc47dde900c62ccd489adf89da6201e Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 23 Nov 2020 20:04:53 +0100
Subject: [PATCH] chore: Nix: simplify flake.nix after all and fix shell.nix

---
 flake.nix         | 5 ++---
 nix/bootstrap.nix | 1 -
 shell.nix         | 8 +++-----
 3 files changed, 5 insertions(+), 9 deletions(-)

diff --git a/flake.nix b/flake.nix
index 1f384665e2..bb7b0ca48d 100644
--- a/flake.nix
+++ b/flake.nix
@@ -88,8 +88,7 @@
     in rec {
       packages = {
         inherit cc lean4-mode buildLeanPackage;
-        inherit (lean) stage0 stage1 stage2 stage3;
-        inherit (lean.stage1) lean mods Init Std Lean test emacs-dev emacs-package update-stage0 update-stage0-commit;
+        lean = lean.stage1;
         temci = (import temci {}).override { doCheck = false; };
         nix = nix-pinned;
         nixpkgs = nixpkgs.legacyPackages.${system};
@@ -101,7 +100,7 @@
         '';
         mdbook = lean-mdbook;
         inherit doc doc-test;
-      };
+      } // lean.stage1 // lean;
 
       defaultPackage = packages.lean;
 
diff --git a/nix/bootstrap.nix b/nix/bootstrap.nix
index 8b740bd420..eafaf65732 100644
--- a/nix/bootstrap.nix
+++ b/nix/bootstrap.nix
@@ -55,7 +55,6 @@ rec {
       desc = "stage${toString stage}";
       build = buildLeanPackage.override { lean = prevStage; lean-final = self; };
     in (all: all // all.lean) rec {
-      inherit leancpp;
       Init = build { name = "Init"; src = ../src; srcDir = "/src"; deps = {}; };
       Std  = build { name = "Std";  src = ../src; srcDir = "/src"; deps = { inherit Init; }; };
       Lean = build { name = "Lean"; src = ../src; srcDir = "/src"; deps = { inherit Init Std; }; };
diff --git a/shell.nix b/shell.nix
index a4346c1a35..d9d16b34db 100644
--- a/shell.nix
+++ b/shell.nix
@@ -1,13 +1,11 @@
 let
   flakePkgs = (import ./default.nix).packages.${builtins.currentSystem};
-  pkgs = flakePkgs.nixpkgs;
-in
-# use `shell` as default
+in { pkgs ? flakePkgs.nixpkgs }:
+  # use `shell` as default
   (attribs: attribs.shell // attribs) rec {
   inherit (flakePkgs) temci;
   shell = pkgs.mkShell.override { stdenv = pkgs.overrideCC pkgs.stdenv (flakePkgs.cc.override { extraConfig = ""; }); } rec {
-    inputsFrom = [ flakePkgs.lean.leancpp ];
-    buildInputs = with pkgs; [ temci ccache ];
+    buildInputs = with pkgs; [ cmake (gmp.override { withStatic = true; }) ccache temci ];
     # https://github.com/NixOS/nixpkgs/issues/60919
     hardeningDisable = [ "all" ];
     # more convenient `ctest` output