Как установить "dllcoqrun.so" при попытке собрать исходный код coq? - PullRequest
1 голос
/ 21 мая 2019

Я пытаюсь собрать coq-8.4pl4 из исходного кода, и я сталкиваюсь с ошибкой, которая говорит: «Неустранимая ошибка: не удается загрузить общую библиотеку dllcoqrun Причина: dllcoqrun.so: не могу открыть файл общего объекта: такого файла нет иликаталог».Хотя я знаю, что должен установить dllcoqrun.so, но что такое dllcoqrun.so и как я могу его установить?

Я использую ubuntu 18.04, ocaml-4.00.0 и camlp5-rel707

COQMKTOP -o bin/coqtop.byte
File "lib/lib.cma(Errors)", line 1:
Warning 31: files lib/lib.cma(Errors) and /usr/local/lib/ocaml/compiler-libs/ocamlbytecomp.cma(Errors) both define a module named Errors
File "pretyping/pretyping.cma(Matching)", line 1:
Warning 31: files pretyping/pretyping.cma(Matching) and /usr/local/lib/ocaml/compiler-libs/ocamlcommon.cma(Matching) both define a module named Matching
File "interp/interp.cma(Lexer)", line 1:
Warning 31: files interp/interp.cma(Lexer) and /usr/local/lib/ocaml/compiler-libs/ocamlcommon.cma(Lexer) both define a module named Lexer
COQC -nois theories/Init/Notations.v
Fatal error: cannot load shared library dllcoqrun
Reason: dllcoqrun.so: cannot open shared object file: No such file or directory
Makefile.build:494: recipe for target 'theories/Init/Notations.vo' failed
make[1]: *** [theories/Init/Notations.vo] Error 2

1 Ответ

0 голосов
/ 22 мая 2019

Для справки: команда разработчиков Coq поддерживает инструкции по управлению пакетами для сборки старых версий Coq в своем пакете opam.

При установке по умолчанию opam через apt-get

Эксперимент в этом разделе был выполнен с использованием последней версии Ubuntu (точнее, я использовал образ докера, который был загружен сегодня).Мне только нужно было выполнить следующие шаги (первые четыре были выполнены как суперпользователь):

apt-get -q -y update
apt-get -q -y dist-upgrade
apt-get -q -y install m4 rsync git #not sure this is needed
apt-get -q -y --no-install-recommends install ocaml-nox opam aspcud

Следующие операции были выполнены как обычный пользователь:

opam init -a
opam switch 4.00.0
opam install coq.8.4.5

последняя командазадаст вопрос, на который вы должны ответить y.

Это создаст установку coq, которую можно найти в каталоге $HOME/.opam/4.00.0/bin.Чтобы убедиться, что эта версия может использоваться в текущей оболочке, вы должны выполнить следующую строку:

eval $ (opam config env)

С версией opam 2

Iне помню, как установить opam версию 2, но это версия, работающая на моем компьютере.Итак, для справки, вот что я сделал, чтобы установить немного другую версию coq.8.4.

opam switch create for-coq.8.4 ocaml-base-compiler.4.00.0
opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev
opam install coq.8.4.dev

Если вы неохотно пользуетесь opam, вы действительно можете собрать соответствующую информацию из следующий файл .Я только что попробовал, и это работает для меня, но я на машине с Fedora и opam уже установлен.

Посмотрите здесь для получения дополнительной информации о opam.

...