search

mit-plv / bedrock2

A work-in-progress language and compiler for verified low-level programming
http://adam.chlipala.net/papers/LightbulbPLDI21/
MIT License
297 stars 45 forks source link

Unbound value Int.land #373

Closed armfazh closed 1 year ago

armfazh commented 1 year ago

Compilation fails with Unbound value Int.land error:

$ make
...
File "/tmp/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/ident_to_string.v", line 8, characters 16-24:
Error: Unbound value Int.land

make[3]: *** [Makefile.coq.noex:764: /tmp/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/ident_to_string.vo] Error 1

Running version: commit b36804f405bde94216630084ca52fc6e177c682b

samuelgruetter commented 1 year ago

Looks like you're using an old Coq version. You need at least 8.16.0

armfazh commented 1 year ago

That's correct, I was using coq v8.15. I tried now with 8.17 and works. Thanks.