Unable to run `make lib`
Closed this issue · 4 comments
bhargavkulk commented
I am trying to use the Coq files of the textbook, and ran into an issue when I ran make lib
.
Steps to reproduce:
- Clone repository
- Run
make lib
I get this as the output to make lib
:
bhargav@bhargav-kk:/mnt/c/bhargav/prog/coq/frap$ make lib
coq_makefile -f _CoqProject -o Makefile.coq
make -f Makefile.coq Frap.vo AbstractInterpret.vo SepCancel.vo
make[1]: Entering directory '/mnt/c/bhargav/prog/coq/frap'
COQDEP VFILES
COQC Sets.v
COQC Relations.v
COQC Map.v
File "./Map.v", line 143, characters 2-177:
Error: This command does not support this attribute: global.
[unsupported-attributes,parsing]
make[1]: *** [Makefile.coq:678: Map.vo] Error 1
make[1]: Leaving directory '/mnt/c/bhargav/prog/coq/frap'
make: *** [Makefile:16: lib] Error 2
achlipala commented
What version of Coq are you using?
bhargavkulk commented
I am using Coq version 8.11.0.
note89 commented
@wags-1314 Tried a few different versions with the same issue.
Not Working
- 8.6.1
- 8.13.2
Working
- 8.15.1
(I'm using nix so quite easy to test different versions)
achlipala commented
Yeah, probably the right "fix" is just to acknowledge that, now, more recent Coq versions are required. I'm not remembering a place where I previously indicated version requirements, but I just added a footnote in the main text.