Debian Question posted in
The oficial documentation can be found here.

Problems compiling ocaml project on debian bulleye: undefined reference to shm_unlink and shm_open

Trying to compile the ocaml project from

https://gitlab.com/benjgregoire/maskverif/

I (having no clue about ocaml) get, after installing all the missing libraries, the error message

+ ocamlfind ocamlopt -rectypes -cclib -lrt -linkpkg -g -thread -package zarith,unix,menhirLib,ocamlgraph -I src src/util.cmx src/expr.cmx src/pexpr.cmx src/poly.cmx src/poly_solve.cmx src/shrcnt.cmx src/state.cmx src/checker.cmx src/ilang_ast.cmx src/ilang_parser.cmx src/ilang_lexer.cmx src/parsetree.cmx src/prog.cmx src/ilang.cmx src/parser.cmx src/lexer.cmx src/main.cmx src/shrcnt_low.o -o src/main.native
/usr/bin/ld: src/shrcnt_low.o: in function `shrcnt_destroy':
/home/myname/work/maskverif/_build/src/shrcnt_low.c:74: undefined reference to `shm_unlink'
/usr/bin/ld: src/shrcnt_low.o: in function `shrcnt_create':
/home/myname/work/maskverif/_build/src/shrcnt_low.c:99: undefined reference to `shm_open'
/usr/bin/ld: /home/myname/work/maskverif/_build/src/shrcnt_low.c:95: undefined reference to `shm_unlink'

From what I found on the internet, it looks like the library rt is given to the gcc linker at the wrong position via -lrt, but I have no idea how to fix this, as it is called by some ocaml binary.

How can I fix this?

Tags:

2

Answers


  1. Chosen as BEST ANSWER
    0

    In meanwhile I was able to compile the SPINI branch as suggested by jubnvz in his/her answer. It did not work using the ocaml/opam/dune packages provided by debian/bulleye, but uninstalling all ocaml-related debian packages and following the installation instructions from the README at https://gitlab.com/benjgregoire/maskverif/tree/SPINI did work fine for me.


  2. 0

    The same problem was reported in this issue.

    The maintainer’s response was as follows:

    This issue was very tricky to fix.
    You can find the current fix on the SPINI branch.

    So, you can try to checkout the SPINI branch and try to build.

    As far as I understand, the problem is that in the Makefile they can’t properly pass the -lrt to the linker. In the SPINI branch, they switched to using the dune build system and solved this problem.

    Login or Signup to reply.
Please signup or login to give your own answer.

Back To Top
Search