Install C headers for C library

Learning
, , , ,
1

Hello,

In my setup, I have Coq extract to OCaml which I then compile as a C library with the following setup:

(coq.extraction
 (prelude bitflip)
 (extracted_modules bitflip))

(executable
 (name CAPI)
 (foreign_stubs (language c)
                (names cstub))
 (flags :standard -linkall)
 (modes (native shared_object))
 (modules bitflip CAPI))

(install
 (section lib)
 (files
  (CAPI.so as libbitflip.so)
  (cstub.h as bitflip.h)))

The directory tree is

dune-project
src
├─ bitflip.v
├─ CAPI.ml
├─ cstub.c
├─ cstub.h
├─ dune

I’m new to OCaml, opam, and dune and it’s hard for me to understand everything that is going on. In any case, my problem is that the install stanza sends bitflip.h to /usr/local/lib/bitflip.h which is obviously the wrong directory for it to be in.

The advice on the stanza reference is to use public_headers to install C headers, but that is for a library stanza. However, what I found for creating a shared library was using the executable stanza with (modes (shared_object)).

I would appreciate advice on this.

2

After reading more of the Dune documentation, I am now getting some ideas on how to accomplish this. I will update this thread with a solution soon.

3

Apologies for not digging into the concrete problem you’re facing, and it seems different from my problem, but maybe this helps someone. I had trouble passing the include and library object paths to the c compiler and linker for FFI bindings (here for cuda). The following worked:

(env
 (_
  (c_flags -I /usr/local/cuda/include)
  (link_flags -cclib -L/usr/local/cuda/lib64/stubs)))

(ctypes
 (build_flags_resolver
  (vendored (c_library_flags -I /usr/local/cuda/include -L /usr/local/cuda/lib64/stubs))))

(unrelated entries omitted). Downside is I’m hardcoding the paths…

1 Like