achlipala/frap

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:

  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 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)

  • 👍1
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.