0

I'm currently using the latest 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 but there was not answer for it. I'm using Coq proof assistant v8.11.0 and OCaml v4.08.1 on a WSL Ubuntu 20.04 OS

The error message is as shown below

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
Improve this question
3
  • Add what command you ran to get the error message, the path you were in when doing it, and where coq-record-update is coming from (not seeing it in Kami repo, must be yours?).
    – Andreas
    Commented Nov 9, 2021 at 8:46
  • @Andreas, thanks for the reply! I was using the Make file posted on the repo. It can be found following this link github.com/sifive/Kami/blob/master/Makefile
    – nanoeng
    Commented Nov 9, 2021 at 11:00
  • I've commented on the issue with an answer, which I'll replicate here.
    – Jason Gross
    Commented Nov 9, 2021 at 14:24

1 Answer 1

Reset to default
0

I believe this repo assumes that its dependencies live in the same parent folder. So you need to clone coq-record-update and any other dependencies. See https://github.com/mit-plv/bedrock2/tree/master/deps for an example of this in action.

Improve this answer
1

Not the answer you're looking for? Browse other questions tagged or ask your own question.