Minimum working example.

[he-chien-tsai]

After trying around and reading code, what to do with Yatima is still not clear. Including a minimum working example with some basic instructions might helps.

My random attempt:

$ lake init Test

$ yatima compile 
No store argument was found.
Run `yatima store -h` for further information.

$ yatima store -h
Redundant positional argument `store`.
Run `yatima -h` for further information.

$ yatima compile Test.lean 

$ yatima transpile output.ir 
Unknown const root

[arthurpaulino]

Thanks! The error message is outdated. Will fix it today

[arthurpaulino]

@he-chien-tsai we're discussing a few things related to this on our Zulip server and in the meantime you can call yatima compile -h, which should print:

yatima compile
Compiles Lean 4 code to Yatima IR and writes the resulting IPLD data encoded
with DagCbor to the file system

USAGE:
    yatima compile [FLAGS] <sources>...

FLAGS:
    -h, --help             Prints this message.
    -o, --output : String  The name of the output binary file. Defaults to
                           "output.ir"
    -p, --prelude          Optimizes the compilation of prelude files without
                           imports. All files to be compiled must follow this
                           rule
    -l, --log              Logs compilation progress
    -s, --summary          Prints a compilation summary at the end of the
                           process

ARGS:
    sources : String  List of Lean files or directories