From e10cf4cf336caa91a0cb7fdf0b435655b4474ef3 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 5 Apr 2021 10:50:21 +0200
Subject: [PATCH] fix: Nix: leanpkg outside flake

---
 nix/buildLeanPackage.nix | 1 +
 nix/leanpkg-dev.in       | 8 +++++---
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/nix/buildLeanPackage.nix b/nix/buildLeanPackage.nix
index dee4b06411..843c6a38dd 100644
--- a/nix/buildLeanPackage.nix
+++ b/nix/buildLeanPackage.nix
@@ -181,6 +181,7 @@ in rec {
     dir = "bin";
     src = ./leanpkg-dev.in;
     isExecutable = true;
+    srcRoot = fullSrc;  # use root flake.nix in case of Lean repo
     inherit bash nix srcTarget srcArgs;
     leanpkg = lean;
   };
diff --git a/nix/leanpkg-dev.in b/nix/leanpkg-dev.in
index 1b72859679..0a5b6d6385 100644
--- a/nix/leanpkg-dev.in
+++ b/nix/leanpkg-dev.in
@@ -2,11 +2,13 @@
 
 set -euo pipefail
 
-[[ $# -gt 0 && "$1" == print-paths && ( -f flake.nix || -d Lean && -f ../flake.nix ) ]] || exec @leanpkg@/bin/leanpkg "$@"
+[[ $# -gt 0 && "$1" == print-paths && ( -f flake.nix || -d Lean && -f ../flake.nix || ! -f leanpkg.toml ) ]] || exec @leanpkg@/bin/leanpkg "$@"
 shift
 deps="$@"
-
-target=".#print-paths"
+root=.
+# fall back to initial package if not in package
+[[ ! -f "$root/flake.nix" ]] && root="@srcRoot@"
+target="$root#print-paths"
 args=()
 # HACK: use stage 0 instead of 1 inside Lean's own `src/`
 [[ -d Lean && -f ../flake.nix ]] && target="@srcTarget@print-paths" && args=@srcArgs@