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 (ppx_deriving_yojson
/ ocaml-rpc
) but these problems are independent of the tool used.
Specifically, the 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:
- The
InternalFailure
constructor has anexn
type field which should not / cannot be serialized. - The
Done
constructor includes the themodel
type throughCall_provers.prover_result
,model
is opaque, and it's uncledar how it should be properly serialized as a result.
Since 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 model
case.