Compile that Buffer

I’ve just started using Coq, a proof¬†assistant, – and a pretty cool one at that. But just like anything else, being new to Coq means I run into some silly problems sometimes (read: often). I’ll post those issues here in the hopes that some other newbie comes across it and doesn’t make my mistakes.

Here’s my setup at the moment:

  • OSX 10.7.5
  • CoqIde version 8.4

If you “Require Export Somelibrary” and you get this error,¬†you may need to compile Somelibrary.

Error: Cannot find library Somelibrary in loadpath

Open Somelibrary into CoqIde and click Compile -> Compile Buffer.