From 1adefe197bc44d7de5e12713fac1add37be09266 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 29 Oct 2021 19:08:07 +0200
Subject: [PATCH] fix: leanc: respect LEAN_SYSROOT

---
 src/Leanc.lean | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/src/Leanc.lean b/src/Leanc.lean
index 9f77933528..16c2b84bcb 100644
--- a/src/Leanc.lean
+++ b/src/Leanc.lean
@@ -14,10 +14,9 @@ Interesting options:
 Beware of the licensing consequences since GMP is LGPL."
     return 1
 
-  let binDir ← IO.appDir
-  -- Zig gets confused by relative include paths on Windows
-  let binDir ← IO.FS.realPath binDir
-  let root := binDir.parent.get!
+  let root ← match (← IO.getEnv "LEAN_SYSROOT") with
+    | some root => System.FilePath.mk root
+    | none      => (← IO.appDir).parent.get!
   -- We assume that the CMake variables do not contain escaped spaces
   let cflags := ["-I", (root / "include").toString] ++ "@LEANC_EXTRA_FLAGS@".trim.splitOn
   let mut ldflags := ["-L", (root / "lib").toString, "-L", (root / "lib" / "lean").toString, (← IO.getEnv "LEANC_GMP").getD "-lgmp"] ++ "@LEAN_EXTRA_LINKER_FLAGS@".trim.splitOn
@@ -41,7 +40,7 @@ Beware of the licensing consequences since GMP is LGPL."
 
   let mut cc := (← IO.getEnv "LEAN_CC").getD "@LEANC_CC@"
   if cc.startsWith "." then
-    cc := (binDir / cc).toString
+    cc := (root / "bin" / cc).toString
 
   let args := cflags ++ args ++ ldflagsExt ++ ldflags ++ ["-Wno-unused-command-line-argument"]
   if args.contains "-v" then