Private types are exposed in server communication
In Why3, IDEs are constructed using a server-client model, in which the IDE UI sends
request to Why3 which then responds using
notification. There is plenty of existing infrastructure that can be used to define a new IDE interface, however, if you wish to serialize these requests and notifications, you can encounter problems. In my case I am using (
ocaml-rpc) but these problems are independent of the tool used.
notification includes the
proof_attempt_status type indirectly through
update_info. This type has two problems when attmepting to derive serialization structurally, one minor and one more serious:
InternalFailureconstructor has an
exntype field which should not / cannot be serialized.
Doneconstructor includes the the
modelis opaque, and it's uncledar how it should be properly serialized as a result.
notification is part of the IDE api boundary I feel like it should be possible to roundtrip notifications, or at least fully serialize them.
The most immediate solution that occurs to me would be to use serialization friendly representations. This seems easy for the
InternalFailure case but less clear for the