CODEWITHSUNDEEP
ocamlocamlfind
j.p.
j.p.

Reputation: 1041

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?

Upvotes: 1

Views: 92

Answers (2)

j.p.
j.p.

Reputation: 1041

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.

Upvotes: 0

jubnzv
jubnzv

Reputation: 1574

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.

Upvotes: 1

Related Questions