# Can't compile packages with coqide

**URL:** <https://discourse.rocq-prover.org/t/cant-compile-packages-with-coqide/1006>\
**Category:** Using Rocq\
**Created:** [August 7, 2020, 5:59pm UTC](https://discourse.rocq-prover.org/t/cant-compile-packages-with-coqide/1006 "2020-08-07T17:59:52Z")\
**Posts on this page:** 2\
**Page:** 1

<div class="post-metadata">

**Author:** ![joepalermo](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/joepalermo/32/404_2.png) [@joepalermo](https://discourse.rocq-prover.org/u/joepalermo)\
**Post date:** [August 7, 2020, 5:59pm UTC](https://discourse.rocq-prover.org/t/cant-compile-packages-with-coqide/1006/1 "2020-08-07T17:59:52Z")

</div>

I’m going through the Software Foundations book ([https://softwarefoundations.cis.upenn.edu/lf-current/index.html](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?

---

<div class="post-metadata">

**Author:** ![Blaisorblade](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/blaisorblade/32/56_2.png) [@Blaisorblade](https://discourse.rocq-prover.org/u/Blaisorblade)\
**Post date:** [August 8, 2020, 3:39am UTC](https://discourse.rocq-prover.org/t/cant-compile-packages-with-coqide/1006/2 "2020-08-08T03:39:38Z")

</div>

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](https://github.com/DeepSpec/sf).