Я как-то пытаюсь использовать _CoqProject
парсер из библиотеки coq в OCaml (я бы приветствовал лучшие альтернативы для захвата файлов .v
проекта coq, если эта библиотека не предназначена для внешнего использования, не так ли? ), но ocamlbuild
, похоже, связывает библиотеки в неправильном порядке.
Рассмотрим этот минимальный пример файла
open CoqProject_file
let x = read_project_file
Пакет coq.lib
(в комплекте с coq
) так или иначе зависит от threads
, и после этого ответа предлагает использовать для этого -tag thread
, но я все еще получаю следующую ошибку, threads
не найден при связывании 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.
Тем не менее, это скомпилируется, если я разобью ocamlopt
вызов на части и положу -thread threads.cmxa
перед 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
Как правильно звонить ocamlbuild
?