mit-plv / kami

A Platform for High-Level Parametric Hardware Specification and its Modular Verification
https://plv.csail.mit.edu/kami/
MIT License
141 stars 24 forks source link

Make command fails with Coq 8.11.1 #26

Open vaishnavi08 opened 3 years ago

vaishnavi08 commented 3 years ago

Make fails when run with Coq 8.11.1. The output is as follows: $make

Generating Makefile
make -f Makefile.coq.all
make[1]: Entering directory '/home/vaishnavi/kami'
COQDEP VFILES
COQC Kami/Lib/StringStringAsOT.v
File "./Kami/Lib/StringStringAsOT.v", line 79, characters 4-20:
Error: No such goal.

Makefile.coq.all:677: recipe for target 'Kami/Lib/StringStringAsOT.vo' failed
make[2]: *** [Kami/Lib/StringStringAsOT.vo] Error 1
Makefile.coq.all:326: recipe for target 'all' failed
make[1]: *** [all] Error 2
make[1]: Leaving directory '/home/vaishnavi/kami'
Makefile:30: recipe for target 'coq' failed
make: *** [coq] Error 2
ju-sh commented 2 years ago

I'm getting the same error with coq 8.12.2

Have anyone found a way to get around this errror?

This was the error (I used the code as it was today: 10 March 2022, from on rv32i branch)

COQC Kami/Lib/StringStringAsOT.v
File "./Kami/Lib/StringStringAsOT.v", line 79, characters 4-20:
Error: No such goal.

Makefile.coq.all:715: recipe for target 'Kami/Lib/StringStringAsOT.vo' failed
make[2]: *** [Kami/Lib/StringStringAsOT.vo] Error 1
Makefile.coq.all:338: recipe for target 'all' failed
make[1]: *** [all] Error 2
make[1]: Leaving directory '/home/user/kami'
Makefile:30: recipe for target 'coq' failed
make: *** [coq] Error 2
ju-sh commented 2 years ago

But it works when using the version in master branch, though.