Marshal determinism and stability

Learning
41

I don’t know about “minimal boilerplate”, but we do something along the lines of:

type comp =
  EFun : { key: string; name: string; f : 'arg -> 'res } -> comp

let registered : (string, comp) Hashtbl.t = Hashtbl.create 10

let register ~__LOC__ ~name f =
  let key = Digest.to_hex (Digest.string (name, __LOC__)) in
  let comp = EFun {key; name; f} in
  Hashtbl.replace registered key comp;
  comp

Then you can register a function by doing

let () =
  register ~__LOC__ ~name:"hello" (fun () -> print_endline "Hello!")

and can identify function by their key fields.

(This is just a sketch, at LexiFi we use features of our fork of the OCaml compiler to implement this more ergonomically, but the idea is the same.)

Unfortunately, this code is not public.

Cheers,
Nicolas

42

We have similar registration code in Coq, eg https://github.com/coq/coq/blob/cb76d6aaaa6fec0a919a459992f91a13552dbc96/pretyping/coercion.ml#L629-L640


type hook = env -> evar_map -> flags:Evarconv.unify_flags -> constr ->
  inferred:types -> expected:types -> (evar_map * constr) option

let all_hooks = ref (CString.Map.empty : hook CString.Map.t)

let register_hook ~name ?(override=false) h =
  if not override && CString.Map.mem name !all_hooks then
    CErrors.anomaly ~label:"Coercion.register_hook"
      Pp.(str "Hook already registered: \"" ++ str name ++ str "\".");
  all_hooks := CString.Map.add name h !all_hooks

let active_hooks = Summary.ref ~name:"coercion_hooks" ([] : string list)

The value of a Summary.ref can get sent to forks through Marshal (no closures) so needs to be marshal safe, and is related to the closures through the all_hooks map.
Registration is just let () = register_hook ~name:"whatever" the_fun eg https://github.com/LPCIC/coq-elpi/blob/7a5e4bc31dbff3c4ee66a465ddc43388564ebd46/apps/coercion/src/coq_elpi_coercion_hook.mlg#L41

Unlike lexifi we don’t use __LOC__, so the name needs to be globally unique.