From 73e9b96cdc9cb13f3fbdb471357bb5ae4ec5efab Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 18 Nov 2020 17:22:30 +0100
Subject: [PATCH] refactor: Nix: move out lean-dev script

---
 nix/buildLeanPackage.nix | 44 ++++++++--------------------------------
 nix/lean-dev.in          | 34 +++++++++++++++++++++++++++++++
 2 files changed, 42 insertions(+), 36 deletions(-)
 create mode 100644 nix/lean-dev.in

diff --git a/nix/buildLeanPackage.nix b/nix/buildLeanPackage.nix
index e4c5bcffc4..f810db2271 100644
--- a/nix/buildLeanPackage.nix
+++ b/nix/buildLeanPackage.nix
@@ -1,4 +1,4 @@
-{ debug ? false, stdenv, lib, coreutils, gnused, lean, leanc ? lean, lean-final ? lean, writeScriptBin, bash, lean-emacs, nix }:
+{ debug ? false, stdenv, lib, coreutils, gnused, lean, leanc ? lean, lean-final ? lean, writeScriptBin, bash, lean-emacs, nix, substituteAll }:
 with builtins; let
   # "Init.Core" ~> "Init/Core.lean"
   modToLean = mod: replaceStrings ["."] ["/"] mod + ".lean";
@@ -104,42 +104,14 @@ in
       set -euo pipefail
       LEAN_PATH=${modRoot} ${lean-final}/bin/lean $@
     '';
-    lean-dev = writeScriptBin "lean" ''
-      #!${bash}/bin/bash
-      set -euo pipefail
-      PATH=${nix}/bin:$PATH
+    lean-dev = substituteAll {
+      name = "lean";
+      dir = "bin";
+      src = ./lean-dev.in;
+      isExecutable = true;
+      inherit lean bash nix srcDir;
+    };
 
-      call() {
-        if [[ $json == 1 ]]; then
-          $@ 2>&1 | awk '/{/ { print $0; next } { gsub(/"/, "\\\"", $0); gsub(/\n/, "\\n", $0); printf "{\"severity\": \"warning\", \"pos_line\": 0, \"pos_col\": 0, \"file_name\": \"<stdin>\", \"text\": \"%s\"}\n", $0 }'
-        else
-          $@
-        fi
-      }
-
-      json=0
-      input=
-      for p in "$@"; do
-        [[ "$p" == --json ]] && json=1
-        [[ "$p" != -* ]] && input="$(realpath "$p")"
-      done
-
-      root="$(dirname "''${input:-/}")"
-      while [[ "$root" != / ]]; do
-        [ -f "$root/flake.nix" ] && break
-        root="$(realpath "$root/..")"
-      done
-      if [[ "$root" == / ]]; then
-        call ${lean}/bin/lean $@
-      elif [[ "$input" != "$root${srcDir}/"* ]]; then
-        call nix run "$root#lean-package" -- $@
-      else
-        input="$(realpath --relative-to="$root${srcDir}" "$input")"
-        input="''${input%.lean}"
-        input="''${input//\//.}"
-        call nix develop "$root#mods.\"$input\"" -c lean $@
-      fi
-     '';
     emacs-package = writeScriptBin "run-emacs-package" ''
       #!${bash}/bin/bash
       ${lean-emacs}/bin/emacs --eval '(setq lean4-rootdir "${lean-package}")' $@
diff --git a/nix/lean-dev.in b/nix/lean-dev.in
new file mode 100644
index 0000000000..637b26ca55
--- /dev/null
+++ b/nix/lean-dev.in
@@ -0,0 +1,34 @@
+#!@bash@/bin/bash
+set -euo pipefail
+PATH=@nix@/bin:$PATH
+
+call() {
+    if [[ $json == 1 ]]; then
+        $@ 2>&1 | awk '/{/ { print $0; next } { gsub(/"/, "\\\"", $0); gsub(/\n/, "\\n", $0); printf "{\"severity\": \"warning\", \"pos_line\": 0, \"pos_col\": 0, \"file_name\": \"<stdin>\", \"text\": \"%s\"}\n", $0 }'
+    else
+        $@
+    fi
+}
+
+json=0
+input=
+for p in "$@"; do
+    [[ "$p" == --json ]] && json=1
+    [[ "$p" != -* ]] && input="$(realpath "$p")"
+done
+
+root="$(dirname "${input:-/}")"
+while [[ "$root" != / ]]; do
+    [ -f "$root/flake.nix" ] && break
+    root="$(realpath "$root/..")"
+done
+if [[ "$root" == / ]]; then
+    call @lean@/bin/lean $@
+elif [[ "$input" != "$root@srcDir@/"* ]]; then
+    call nix run "$root#lean-package" -- $@
+else
+    input="$(realpath --relative-to="$root@srcDir@" "$input")"
+    input="${input%.lean}"
+    input="${input//\//.}"
+    call nix develop "$root#mods.\"$input\"" -c lean $@
+fi