search

AeneasVerif / charon

Interface with the rustc compiler for the purpose of program verification
https://aeneasverif.github.io/charon/charon_lib/index.html
Apache License 2.0
103 stars 17 forks source link

Generate some ml type definitions #302

Closed Nadrieril closed 3 months ago

Nadrieril commented 3 months ago

Progress on #215. This auto-generates a number of ml definitions from the rust ones. I've left the visitor definitions as-is; that feels incomplete, I hope to find a cleaner solution when more of the types are auto-generated.

Nice bonus: this copies the doc-comments present on the rust side.

sonmarcho commented 3 months ago

I hadn't thought of the fact that doing this would allow to port the documentation from the Rust side to the OCaml side: this is extremely useful. The only minor change I would like to do is a better indentation of the multi-line comments (as you can see, having no indentation is a bit ugly).

Nadrieril commented 3 months ago

The other problem is that this causes many errors when building the ocaml doc, because the ocaml doc format doesn't like the markdown syntax