A WIP compiler and typechecker for the Yatima language.
Build it with lake build
.
Run lake run setup
, which will build the yatima
binary and ask you where to place it.
You can choose a directory that's already in your path, for example.
The subcommands planned to be available for the yatima
CLI are:
compile
: compiles Lean 4 code to Yatima IRtypecheck
: typechecks Yatima IRtranspile
: transpiles Yatima IR to Lurk codeprove
: generates a Lurk proof that a certain Lean 4 declaration typechecksverify
: verifies the correctness of a Lurk proofipfs put
: sends Yatima IR to IPFSipfs get
: retrieves Yatima IR from IPFS
Constraints:
- The
compile
subcommand must be triggered from within a Lean project that uses Lake - The Lean 4 code to be compiled must use the same toolchain as the one used to compile the
yatima
binary. To see the needed toolchain, callyatima --version
and check the content before the pipe|
- To compile a Lean 4 file that imports others, the imported
olean
files must be available