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.

Leave a Reply

Your email address will not be published. Required fields are marked *

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>