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

fix: leanc: discard internal flag when using external compiler

Browse source
This commit is contained in:
Sebastian Ullrich 2021-10-22 10:43:25 +02:00
parent 5562beccee
commit c3d1b2592c
1 changed files with 10 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/Leanc.lean
View file

@ -21,10 +21,10 @@ Beware of the licensing consequences since GMP is LGPL."
-- We assume that the CMake variables do not contain escaped spaces
let cflags := ["-I", (root / "include").toString] ++ "@LEANC_EXTRA_FLAGS@".trim.splitOn
let cflagsHidden := "@LEANC_INTERNAL_FLAGS@".trim.splitOn
let mut cflagsInternal := "@LEANC_INTERNAL_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
let mut ldflagsExt := "@LEANC_STATIC_LINKER_FLAGS@".trim.splitOn
let ldflagsHidden := "@LEANC_INTERNAL_LINKER_FLAGS@".trim.splitOn
let mut ldflagsInternal := "@LEANC_INTERNAL_LINKER_FLAGS@".trim.splitOn
for arg in args do
match arg with
@ -42,8 +42,14 @@ Beware of the licensing consequences since GMP is LGPL."
return 0
| _ => ()
let cc := rootify <| (← IO.getEnv "LEAN_CC").getD "@LEANC_CC@"
let args := cflags ++ cflagsHidden ++ args ++ ldflagsExt ++ ldflags ++ ldflagsHidden ++ ["-Wno-unused-command-line-argument"]
let mut cc := "@LEANC_CC@"
if let some cc' ← IO.getEnv "LEAN_CC" then
cc := cc'
-- these are intended for the bundled compiler only
cflagsInternal := []
ldflagsInternal := []
cc := rootify cc
let args := cflags ++ cflagsInternal ++ args ++ ldflagsExt ++ ldflags ++ ldflagsInternal ++ ["-Wno-unused-command-line-argument"]
let args := args.map rootify
if args.contains "-v" then
IO.eprintln s!"{cc} {" ".intercalate args}"