Hi,

I’m writing to seek some knowledge/suggestions about the building system of Coq/OCaml:

I’m implementing a compiler pass for CompCert. This pass uses a heuristic to optimize a program (which does not influence the correctness proof).

We have an existing implementation of this heuristic in C, but not in Coq. The specification of this heuristic is as simple a function from a list of numbers (*positive* type) (or pairs of numbers) to another number

One thing I learned is that there exists support to use a C function in an OCaml program. Since the CompCert project written in Coq will eventually be converted to an OCaml program, I believe this could be a way we can directly use that heuristic in the C version, instead of re-implementing it in Coq.

However, I barely have developing experience in OCaml projects and I’m not very familiar with its building system, and no idea how to actually implement an OCaml program that uses C function. (And I’m even doing this in a Coq project)

So I’m posting this to seek help and suggestions on where should I get started to learn so I can eventually connect my implementations and make them a compilable/executable project.

Thank you!