argumentcomputer / yatima

A zero-knowledge Lean4 compiler and kernel
MIT License
122 stars 9 forks source link

Optional compilation #201

Closed arthurpaulino closed 1 year ago

arthurpaulino commented 2 years ago

196 did a complete revamp in the CLI, removing compilation from multiple commands and making stores available to other commands via stores saved as binary files. With those changes, only the compile command can call the compilation routine.

This issue is about coming up with a well defined behavior that allows compilation in other commands again if the user doesn't want to provide a compiled store and wants to do compilation on the fly instead.

"Well defined behavior" means a clear set of arguments, flags and side-effects for each command. This is hard because there are some conflicts between commands. Examples: