From 4d38ca0c9f2968366144f7f6b538181c11bdd87f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Mon, 5 Feb 2024 19:33:55 +0100
Subject: [PATCH] [doc] Add instructions on adding new types to serlib README

---
 serlib/README.md | 37 +++++++++++++++++++++++++++++++++++++
 1 file changed, 37 insertions(+)

diff --git a/serlib/README.md b/serlib/README.md
index 9edcbe8d..383b971b 100644
--- a/serlib/README.md
+++ b/serlib/README.md
@@ -15,6 +15,43 @@ plugins.
 `serlib` provides some builtins and configuration values in the
 `Serlib_base` and `Serlib_init` modules.
 
+### Serializing regular Coq types
+
+The standard recipe is to use a combination of `ppx_import` and
+several ppx-based "derivers" to make `serlib` generate the
+corresponding serializers.
+
+The pattern for a Coq module `Foo` exporting the datatype `bar` and
+their constructors is:
+
+1. create a new OCaml module named `ser_foo.ml`
+2. get the corresponding serializers for existing types in scope, this is unusually done in two steps:
+  - serializers for OCaml Stdlib:
+```ocaml
+open Ppx_hash_lib.Std.Hash.Builtin
+open Ppx_compare_lib.Builtin
+open Sexplib.Std
+```
+  - serializers for types that `Foo.bar` depends on, for example:
+```ocaml
+module Names = Ser_names
+module EConstr = Ser_eConstr
+...
+```
+3. implement the serializers for your type. Add to `ser_foo.ml`:
+```ocaml
+type bar =
+  [%import: Foo.bar]
+  [@@deriving sexp,yojson,hash,compare]
+```
+
+Additionally, you can add an `.mli` file, with the same contents as
+above, but in this case, `[@@deriving ...]` will generate the right
+interface declarations.
+
+If `Foo.bar` has no public constructors, `Obj.magic` will be
+needed. `serlib` provides helpers for this, see below.
+
 ### Serializing opaque and private types
 
 `serlib` uses `ppx_import` to retrieve the original type definitions