3

I'm somehow trying to use _CoqProject parser from coq's library in OCaml (I'd welcome better alternatives to grab the .v files of a coq project if that library is not meant for external use, is it?), but ocamlbuild seems to be linking libraries in the wrong order.

Consider this minimal example file

open CoqProject_file
let x = read_project_file

The coq.lib package (bundled with coq) somehow depends on threads, and following this answer suggests to use -tag thread for that, but I still get the following error that threads is not found when linking coq.lib:

$ ocamlbuild -pkg coq.lib -tag thread -cflag -rectypes a.native                                                                                                             /tmp/p
+ /home/sam/.opam/4.06.0+coq-8.7/bin/ocamlopt.opt -I /home/sam/.opam/4.06.0+coq-8.7/lib/coq/config -I /home/sam/.opam/4.06.0+coq-8.7/lib/coq/lib -I /home/sam/.opam/4.06.0+coq-8.7/lib/ocaml /home/sam/.opam/4.06.0+coq-8.7/lib/ocaml/str.cmxa /home/sam/.opam/4.06.0+coq-8.7/lib/ocaml/unix.cmxa /home/sam/.opam/4.06.0+coq-8.7/lib/coq/lib/clib.cmxa -thread threads.cmxa a.cmx -o a.native
File "_none_", line 1:
Error: No implementations provided for the following modules:
         Thread referenced from /home/sam/.opam/4.06.0+coq-8.7/lib/coq/lib/clib.cmxa(Exninfo)
         Mutex referenced from /home/sam/.opam/4.06.0+coq-8.7/lib/coq/lib/clib.cmxa(Exninfo)
Command exited with code 2.

Yet that compiles if I take the ocamlopt invocation apart and put -thread threads.cmxa before clib.cmxa

$ cd _build/
$ /home/sam/.opam/4.06.0+coq-8.7/bin/ocamlopt.opt -I /home/sam/.opam/4.06.0+coq-8.7/lib/coq/config -I /home/sam/.opam/4.06.0+coq-8.7/lib/coq/lib -I /home/sam/.opam/4.06.0+coq-8.7/lib/ocaml /home/sam/.opam/4.06.0+coq-8.7/lib/ocaml/str.cmxa /home/sam/.opam/4.06.0+coq-8.7/lib/ocaml/unix.cmxa -thread threads.cmxa /home/sam/.opam/4.06.0+coq-8.7/lib/coq/lib/clib.cmxa a.cmx -o a.native

What is the right way to call ocamlbuild?

Li-yao Xia
  • 31,896
  • 2
  • 33
  • 56
  • 1
    `ocamlbuild -use-ocamlfind -pkg coq.lib -cflag -rectypes -tag thread a.native` somehow works but I really don't know what's going on, maybe that was pure luck. So I'll wait before putting that up as an answer. – Li-yao Xia Apr 25 '18 at 12:32
  • Indeed your first `ocamlbuild` invocation was not correct, the one above almost is, you should indeed use just `-package coq.lib` if you are using a correct Coq `META` file. – ejgallego Apr 25 '18 at 13:46
  • 4
    You should not work like this anyways, but use a `_tags` file. – ejgallego Apr 25 '18 at 14:06
  • Thanks for the tip! I didn't know about the `META` file. – Li-yao Xia Apr 25 '18 at 14:47
  • I'm confused about the proper setup. How does `ocamlbuild` depend on `META`? What should I put in `_tags` given that the bit that needs `thread` is a library I'm using, but not my actual code? One answer would be to show a good way to build the above snippet. – Li-yao Xia Apr 25 '18 at 15:21

1 Answers1

3

If you use ocamlfind packages, you should use the -use-ocamlfind flag.

There is no good solution as to why -tag thread is needed¹. There are two different implementations of the OCaml Threads interface (one with os threads and one with green threads), and coq.lib depends on the interface but won't decide for the user which one to use, so you have to specify it manually, for example by using -tag thread.

¹: one solution would be to remove this choice by deprecating vmthreads (the green threads), which is rarely used in practice.

gasche
  • 31,259
  • 3
  • 78
  • 100