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?
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.