GitLab

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:

1. The InternalFailure constructor has an exn type field which should not / cannot be serialized.
2. The Done constructor includes the the model type through Call_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.