alt Hacker NewsHi, I'm one of Crane's developers. You can map Rocq `bool`s to C++ `bool`, Rocq strings to C++ `std::string`s, etc. You just have to manually import the mapping module: https://github.com/bloomberg/crane/blob/6a256694460c0f895c27...
The output you posted is from an example that we missed importing. It's also one of the tests that do not yet pass. But then again, in the readme, we are upfront with these issues:
> Crane is under active development. While many features are functional, parts of the extraction pipeline are still experimental, and you may encounter incomplete features or unexpected behavior. Please report issues on the GitHub tracker.
I should also note, mapping Rocq types to ideal C++ types is only one part of it. There are still efficiency concerns with recursive functions, smart pointers, etc. This is an active research project, and we have plans to tackle these problems: for recursion: try CPS + defunctionalization + convert to loops, for smart pointers: trying what Lean does (https://dl.acm.org/doi/10.1145/3412932.3412935), etc.
Thanks, yeah, I did see some of the pure C++ types getting converted. Though it makes a lot of sense why you had to go with shared_ptr for generic inductive types.
Have you considered combinatorial testing? Test code generation for each sample program, for each set of mappings, and ensure they all have the same behavior. If you look at the relative size or performance, it could allow you to automatically discover this issue. Also, allocation counting.
Hey also sucks you are not in SF. I'm looking for people into formalization in the area, but I haven't found any yet