Error: Unknown scope delimiting key _type.

[ndcroos]

I am fairly new to Coq. I am working on a debian 12 system.
When I run make, I get the following error:

bash etc/generate_coqproject.sh
coq_makefile -f _CoqProject -o Makefile.coq
make --no-print-directory -f Makefile.coq 
COQC theories/Basics/Overture.v
File "./theories/Basics/Overture.v", line 175, characters 16-25:
Error: Unknown scope delimiting key _type.

make[2]: *** [Makefile.coq:838: theories/Basics/Overture.vo] Error 1
make[2]: *** [theories/Basics/Overture.vo] Deleting file 'theories/Basics/Overture.glob'
make[1]: *** [Makefile.coq:409: all] Error 2
make: *** [Makefile:21: invoke-coqmakefile] Error 2

coqc -v gives:

The Coq Proof Assistant, version 8.18.0
compiled with OCaml 4.14.1

[Alizter]

The debian version of Coq appears to be too old. The library currently builds with 8.19 as a minimum version. The _type syntax is new for 8.19 hence why it doesn't work in 8.18. My suggestion would be to use either nix or opam to get a more recent version of Coq.

If you want to use opam, the one in debian should be fine, you should then do opam install coq to install and build the Coq opam package. In your shell environment, you will also need to do eval $(opam env) to make sure PATH and other env vars are updated correctly.

If you want to use nix, just install a newer version of nix and do nix develop in the repo. That will setup a development shell with everything you need. If that doesn't work out of the box, let me know what it says and we can set it up to work.

I would also recommend you use dune for development since it is a smoother experience than the one make offers.

[Alizter]

@ndcroos Let me know if this works for you, after which I will close this issue.

[ndcroos]

@Alizter thanks, this worked for me. I used opam and dune to build.

[Alizter]

@ndcroos May I also ask which editor you are planning to use?

[ndcroos]

I am going to use Coq IDE.

[Alizter]

@ndcroos Good to know. If you have any questions or if something doesn't work, feel free to open an issue.