ubuntu - 能够在 WSL Ubuntu 上运行的 Kami(Bluespec 的 Coq 框架)的正确设置是什么?
问题描述
我目前正在使用最新的Kami的 repo 文件,但在尝试运行 Makefile 时无法解决问题。我在此链接上找到了另一个具有类似请求的帖子,但没有答案。我在 WSL Ubuntu 20.04 操作系统上使用 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 。
推荐阅读
- reactjs - 如何更改图标大小?
- javascript - new Array(5).toString() 返回四个逗号
- git - 如何使 git 跟踪文件/文件夹名称大小写更改?
- django - 使用基于类的视图和清晰的表单在 Django 内联表单集中自动保存用户
- sql - 如何使用引用同一个表的选择语句更新多行
- excel - 在 VBA TextBox 中输入数据并反映到 Google Sheet
- r - 根据字符值创建出现的数字顺序
- vba - “无效的过程调用或参数”在 Word 2013/2016 的 Shell 中调用 regedit
- django - 数组不要在模板中访问
- oauth-2.0 - 如何使用 Cloud Foundry api 获取令牌?