-
Notifications
You must be signed in to change notification settings - Fork 26
Open
Labels
E-needs-helpIssues where non-expert help is needed and instructions have been given.Issues where non-expert help is needed and instructions have been given.
Description
The OCaml pretty-printer is not tested inside Charon. The reason is that it's a bit best-effort, without as many advanced features as the Rust one. What would be highly desireable would be to transform the Rust one in such a way that we can derive the OCaml one automatically (probably using the llbc of the Rust pretty-printer). Then we could add a test that checks that the two give the exact same output.
I don't know how we could do this, open to ideas and experimentation!
Metadata
Metadata
Assignees
Labels
E-needs-helpIssues where non-expert help is needed and instructions have been given.Issues where non-expert help is needed and instructions have been given.