Can't compile packages with coqide

Using Coq
1

I’m going through the Software Foundations book (https://softwarefoundations.cis.upenn.edu/lf-current/index.html) and it asks to compile several simple packages.

For example at the start of chapter 4, the instruction is:

In CoqIDE:
Open Basics.v. In the “Compile” menu, click on “Compile Buffer”.

But I get the following when I do that:

File “/Users/joe/coq/lf/Basics.v”, line 1345, characters 0-31:
Error: Unknown command of the non proof-editing mode.

Any ideas what’s going wrong?

2

Not sure if that’s THE issue, but If you’re using Coq >= 8.11, you’ll need this copy of SF: https://github.com/DeepSpec/sf.