max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: leanc: respect LEAN_SYSROOT

Browse source
This commit is contained in:
Sebastian Ullrich 2021-10-29 19:08:07 +02:00 • committed by Leonardo de Moura
parent 4b51d00fcb
commit 1adefe197b
1 changed files with 4 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Leanc.lean
View file

@ -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