Kami（Bluespec 的 Coq 框架）能够在 WSL Ubuntu 上 运行 的正确设置是什么？
What's the correct setup for Kami (Coq framework for Bluespec) to be able to run on WSL Ubuntu?
我目前使用的是最新的 Kami's repo files but haven't been able to overcome an issue when I try to run the Makefile. I found another posting with a similar request at this link 但没有答案。我在 WSL Ubuntu 20.04 OS
上使用 Coq 证明助手 v8.11.0 和 OCaml v4.08.1
报错信息如下图
Warning: no common logical root
Warning: in such case INSTALLDEFAULTROOT must be defined
Warning: the install-doc target is going to install files
Warning: in orphan_Kami_RecordUpdate
make -f Makefile.coq.all
make[1]: Entering directory '/home/user/sifive/Kami'
COQDEP VFILES
Fatal error: exception Sys_error("../coq-record-update/src: No such file or directory")
COQDEP VFILES
Fatal error: exception Sys_error("../coq-record-update/src: No such file or directory")
COQDEP VFILES
Fatal error: exception Sys_error("../coq-record-update/src: No such file or directory")
COQC All.v
While loading initial state:
Warning: Cannot open ../coq-record-update/src [cannot-open-path,filesystem]
File "./All.v", line 1, characters 15-32:
Error: Unable to locate library Kami.AllNotations.
make[2]: *** [Makefile.coq.all:678: All.vo] Error 1
make[1]: *** [Makefile.coq.all:327: all] Error 2
make[1]: Leaving directory '/home/user/sifive/Kami'
make: *** [Makefile:6: coq] Error 2
我相信这个 repo 假定它的依赖项位于同一个父文件夹中。所以你需要克隆 coq-record-update 和任何其他依赖项。有关此操作的示例，请参阅 https://github.com/mit-plv/bedrock2/tree/master/deps。
我目前使用的是最新的 Kami's repo files but haven't been able to overcome an issue when I try to run the Makefile. I found another posting with a similar request at this link 但没有答案。我在 WSL Ubuntu 20.04 OS
上使用 Coq 证明助手 v8.11.0 和 OCaml v4.08.1报错信息如下图
Warning: no common logical root
Warning: in such case INSTALLDEFAULTROOT must be defined
Warning: the install-doc target is going to install files
Warning: in orphan_Kami_RecordUpdate
make -f Makefile.coq.all
make[1]: Entering directory '/home/user/sifive/Kami'
COQDEP VFILES
Fatal error: exception Sys_error("../coq-record-update/src: No such file or directory")
COQDEP VFILES
Fatal error: exception Sys_error("../coq-record-update/src: No such file or directory")
COQDEP VFILES
Fatal error: exception Sys_error("../coq-record-update/src: No such file or directory")
COQC All.v
While loading initial state:
Warning: Cannot open ../coq-record-update/src [cannot-open-path,filesystem]
File "./All.v", line 1, characters 15-32:
Error: Unable to locate library Kami.AllNotations.
make[2]: *** [Makefile.coq.all:678: All.vo] Error 1
make[1]: *** [Makefile.coq.all:327: all] Error 2
make[1]: Leaving directory '/home/user/sifive/Kami'
make: *** [Makefile:6: coq] Error 2
我相信这个 repo 假定它的依赖项位于同一个父文件夹中。所以你需要克隆 coq-record-update 和任何其他依赖项。有关此操作的示例，请参阅 https://github.com/mit-plv/bedrock2/tree/master/deps。