lean4-htt/tests/pkg/frontend/Frontend/Main.lean
Scott Morrison 58d19b80b9 test: compiling from the interpreter, with common imports
hacky fix to windows test

Include test from #2407 as well
2023-08-16 10:11:50 -07:00

13 lines
370 B
Text

import Frontend.Compile
open Lean
unsafe def main (args : List String) : IO UInt32 := do
initSearchPath (← findSysroot)
let mut count : UInt32 := 0
for mod in args do
IO.println s!"Compiling {mod}"
let (_env, msgs) ← compileModule mod.toName true
for m in msgs do IO.println (← m.toString)
if msgs.length > 0 then count := 1
return count