Slow with larger messages
The internal representation of bytes as bool tuples and the splitting of strings into list contributes to the slow performance. A messages with a 64kb string takes close to 100ms to parse on a test machine, far longer than I would expect for such a simple operation.
Is the representation of the message content something that can be changed in the Coq code or would it require a rewrite by hand in OCaml?
To change internal representanion, Coq code should be changed, especially at extract config( https://github.com/msgpack/msgpack-ocaml/blob/master/proof/ExtractUtil.v).
@hcarty: any luck with changing the underlying representation? I'm trying to get this to work with large messages.
Check out http://github.com/vbmithr/ocaml-msgpck :)