Zulip Chat Archive

Stream: new members

Topic: Yatima frontend yields no stdout

Malcolm Langfield (May 30 2022 at 16:14):

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
        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 (May 30 2022 at 16:15):

Using main branch of linked library, commit 8e4ffd919bda9f2e7d8fea789db8a0d79ae9a656.

Last updated: Dec 20 2023 at 11:08 UTC