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:
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?