Unable to run make lib

[bhargavkulk]

I am trying to use the Coq files of the textbook, and ran into an issue when I ran make lib.

Steps to reproduce:

1. Clone repository
2. 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]

What version of Coq are you using?

[bhargavkulk]

I am using Coq version 8.11.0.

[note89]

@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]

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.