Add uplc executable user guide#7745
Conversation
|
Unisay
left a comment
Unisay
left a comment
There was a problem hiding this comment.
Nice doc!
Here are my few nits ;)
| loadArgsFromDir baseDir title argKind = do | ||
| let dir = baseDir </> title | ||
| paths <- collectArgFiles dir 1 | ||
| paths <- collectArgFiles dir 0 |
There was a problem hiding this comment.
Please update the haddock above correspondingly.
There was a problem hiding this comment.
IMO worth adding a changelog entry since this is a user facing behavior change.
There was a problem hiding this comment.
Ideally I'd want to see this function unit tested too
There was a problem hiding this comment.
Will add some functionality tests at the uplc executable level separately.
Co-authored-by: Yura <1009751+Unisay@users.noreply.github.com>
Co-authored-by: Yura <1009751+Unisay@users.noreply.github.com>
Co-authored-by: Yura <1009751+Unisay@users.noreply.github.com>
Co-authored-by: Yura <1009751+Unisay@users.noreply.github.com>
| uplc optimize -i MyValidator.uplc -o MyValidator-opt.uplc --certify MyProof | ||
| ``` | ||
|
|
||
| This produces an Agda project (the default output mode) that encodes a correctness proof of the transformation, named after the `MyProof`. |
There was a problem hiding this comment.
Did you mean:
| This produces an Agda project (the default output mode) that encodes a correctness proof of the transformation, named after the `MyProof`. | |
| This produces an Agda project (the default output mode) that encodes a correctness proof of the transformation, named after the argument given to `--certify` (in this example, `MyProof`). |
?
| ``` | ||
|
|
||
| This produces an Agda project (the default output mode) that encodes a correctness proof of the transformation, named after the `MyProof`. | ||
| You can then run the Agda type checker on the generated project to verify the certificate. |
There was a problem hiding this comment.
Should we explain how to do this?
The nix develop shell comes with the agda-with-stdlib-and-metatheory executable. You must cd into the MyProof-.../src directory and run agda-with-stdlib-and-metatheory MyProof.agda, where MyProof.agda is the main module of the Agda project.
There was a problem hiding this comment.
I suppose the Agda project contains instructions on how to type check it. If not, we should add it there.
There was a problem hiding this comment.
It doesn't. We could add README.md with the instructions and bundle it with each certificate. I'll add an issue for that.
|
|
||
| For blueprints, the certifier runs once per validator. | ||
| Report filenames and project directories have the validator's title appended automatically. | ||
|
|
There was a problem hiding this comment.
I would also mention the --certified-opts-only option. If someone is interested in using the uplc executable for certification, they most likely want a certificate which reflects the correctness of all of the optimizations which were run on the program.
| {-| Load args from a dir. | ||
|
|
||
| It tries to load the first arg from the file named "1", second from "2", and so on, | ||
| It tries to load the first arg from the file named "0", second from "1", and so on, |
There was a problem hiding this comment.
Looks like Phil convinced you to change this! 😄
3 participants
No description provided.