Yatima frontend yields no stdout

Stream: new members

[Malcolm Langfield]

I was looking at the Yatima compiler this afternoon because it looked neat (https://github.com/yatima-inc/yatima-lang). The main script is here:

  import Lean
  import Yatima.Cid
  import Yatima.Univ
  import Yatima.Expr
  import Yatima.Const
  import Yatima.Env
  import Yatima.FromLean

  -- forcing compilation:
  import Yatima.Ipld.DagCbor
  import Yatima.YatimaSpec

  open Yatima.Compiler.FromLean

  def main : List String → IO UInt32
    | ["build", f] => do
      let input ← IO.FS.readFile ⟨f⟩
      IO.println s!"Input: {input}"
      Lean.initSearchPath $ ← Lean.findSysroot
      let (env, ok) ← Lean.Elab.runFrontend input .empty f `main
      if ok then
        match extractEnv env.constants with
        | .ok env => --todo
          return 0
        | .error e =>
          IO.println e
          return 1
      else
        IO.eprintln s!"Lean frontend failed on file {f}"
        return 1
    | _ => return 0

I've made a one-line change, namely adding the IO.println call to dump the input file path. It builds fine, but when I try to compile the example Foo.lean file with ./build/bin/yatima Foo.lean, there is no output whatsoever. This seems very strange to me, I don't see how the println call is being skipped.

[Malcolm Langfield]

Using main branch of linked library, commit 8e4ffd919bda9f2e7d8fea789db8a0d79ae9a656.