ocamlbuild ссылки библиотеки в неправильном порядке - PullRequest
0 голосов
/ 25 апреля 2018

Я как-то пытаюсь использовать _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?

1 Ответ

0 голосов
/ 26 апреля 2018

Если вы используете пакеты ocamlfind, вы должны использовать флаг -use-ocamlfind.

Нет хорошего решения относительно того, зачем нужен -tag thread.Существуют две различные реализации интерфейса потоков OCaml (одна с потоками os, а другая с зелеными нитями), и coq.lib зависит от интерфейса, но не будет решать для пользователя, какой из них использовать, поэтому вы должны указать его вручнуюНапример, с помощью -tag thread.

¹: одним из решений было бы отменить этот выбор, исключив vmthreads (зеленые нити), что редко используется на практике.

...