feat: add bin/lean_wrapped helper script that chooses the right stage and use it in lean-mode

bin/lean_wrapped

@@ -0,0 +1,17 @@
+#!/usr/bin/env bash
+# Call `lean_stage0` when in library/Init; otherwise call `lean`.
+
+bin=$(dirname $(realpath $0))
+lib=$(dirname $bin)/library/Init
+# use dir of input file, or pwd if stdin
+if [[ "$*" == *--stdin* ]]; then
+    dir=$(pwd)
+else
+    dir=$(dirname $(realpath ${@:$#}))
+fi
+# check if `dir` starts with `lib`
+if [[ ${dir##$lib} != $dir ]]; then
+    $bin/lean_stage0 $*
+else
+    $bin/lean $*
+fi

lean4-mode/lean4-settings.el

@@ -22,7 +22,7 @@
   (cl-case system-type
     ('windows-nt   "lean.exe")
     ('cygwin       "lean.exe")
-    (t             "lean"))
+    (t             "lean_wrapped"))
   "Default executable name of Lean")
 
 (defcustom lean4-rootdir nil