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

1 Like
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.