Как исправить ошибку VST (проверенный программный инструментарий) 2.3, построенную с помощью coq 8.8.1 - PullRequest
Новая
       21

Как исправить ошибку VST (проверенный программный инструментарий) 2.3, построенную с помощью coq 8.8.1

0 голосов
/ 05 июня 2019

Я хочу установить VST 2.3 с coq 8.8.1, чтобы узнать объем VC на основе программного обеспечения. но я сталкиваюсь с ошибкой.

Я использовал метод A, который рекомендуется в vst BUILD_ORGANIZATION.md и который не работает для меня. 

jon@jon-lab:~/Documents/vst$ make
Makefile:606: .depend: No such file or directory
coqdep ... >.depend
coqdep  -R compcert/lib compcert.lib  -R compcert/common compcert.common  -R compcert/arm compcert.arm  -R compcert/cfrontend compcert.cfrontend  -R compcert/flocq compcert.flocq  -R compcert/exportclight compcert.exportclight 2>&1 >.depend `find compcert/lib compcert/common compcert/arm compcert/cfrontend compcert/flocq compcert/exportclight  -name "*.v"` | grep -v 'Warning:.*found in the loadpath' || true
find: ‘compcert/arm’: No such file or directory
Fatal error: exception Sys_error("compcert/arm: No such file or directory")
coqdep   -Q msl VST.msl   -Q sepcomp VST.sepcomp   -Q veric VST.veric   -Q floyd VST.floyd   -Q progs VST.progs                        -Q compcert/lib compcert.lib  -Q compcert/common compcert.common  -Q compcert/arm compcert.arm  -Q compcert/cfrontend compcert.cfrontend  -Q compcert/flocq compcert.flocq  -Q compcert/exportclight compcert.exportclight  2>&1 >>.depend `find compcert/lib compcert/common compcert/arm compcert/cfrontend compcert/flocq compcert/exportclight msl sepcomp veric floyd progs -name "*.v"` | grep -v 'Warning:.*found in the loadpath' || true
find: ‘compcert/arm’: No such file or directory
Fatal error: exception Sys_error("compcert/arm: No such file or directory")
echo   -Q msl VST.msl   -Q sepcomp VST.sepcomp   -Q veric VST.veric   -Q floyd VST.floyd   -Q progs VST.progs                        -Q compcert/lib compcert.lib  -Q compcert/common compcert.common  -Q compcert/arm compcert.arm  -Q compcert/cfrontend compcert.cfrontend  -Q compcert/flocq compcert.flocq  -Q compcert/exportclight compcert.exportclight  > _CoqProject
util/coqflags > _CoqProject-export
COQC msl/Axioms.v
Warning: Cannot open compcert/arm [cannot-open-path,filesystem]
COQC msl/Extensionality.v
Warning: Cannot open compcert/arm [cannot-open-path,filesystem]
COQC msl/base.v
Warning: Cannot open compcert/arm [cannot-open-path,filesystem]
COQC msl/eq_dec.v
Warning: Cannot open compcert/arm [cannot-open-path,filesystem]
COQC msl/sig_isomorphism.v
Warning: Cannot open compcert/arm [cannot-open-path,filesystem]
COQC msl/ageable.v
Warning: Cannot open compcert/arm [cannot-open-path,filesystem]
COQC msl/sepalg.v
Warning: Cannot open compcert/arm [cannot-open-path,filesystem]
COQC msl/psepalg.v
Warning: Cannot open compcert/arm [cannot-open-path,filesystem]
File "./msl/psepalg.v", line 9, characters 15-40:
Error: Unable to locate library VST.msl.sepalg_generators.

Makefile:430: recipe for target 'msl/psepalg.vo' failed
make: *** [msl/psepalg.vo] Error 1

Я использую ubuntu 1804 64bit, и я не знаю, почему они хотят открыть compcert / arm, а файл _CoqProject создан Makefile.Так я не могу исправить ошибку поиска библиотеки.

...