Can't compile packages with coqide

I’m going through the Software Foundations book ( 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?

Not sure if that’s THE issue, but If you’re using Coq >= 8.11, you’ll need this copy of SF: