Error loading CoqIDE for ssreflect

Question

I am new to Coq and therefore improve my understanding of proof verification. I am trying to use the Ssreflect library.

I installed Ssreflect v 1.5 on Mac OS v 10.10.3 (Yosemite), which runs in the terminal.

However, when I tried to load the library in CoqIDE 8.4p15 using:

Require Import ssreflect. 

I get an error message:

 Cannot find library ssreflect in loadpath 

I tried using:

 Add LoadPath "/opt/local/lib/coq/user-contrib/Ssreflect/". 

where SSRCOQ_LIB is currently set, but I get an error:

 The file /opt/local/lib/coq/user-contrib/Ssreflect/ssreflect.vo contains library Ssreflect.ssreflect and not library ssreflect 

I am grateful for any help in downloading the ssreflect library from CoqIDE.

Answer 1

Many thanks to the people at the Coq-Club forum who helped solve this problem, and in particular to Pierre Butillier, who identified the cause of the problem and provided a solution.

The problem was that I had 2 copies of coqtop and 2 copies of standard libraries:

• One in / opt / local / bin / coqtop (which is the folder where my copy is installed, possibly in a different folder) and is used to compile ssreflect (I used MacPorts to install coq).
• One in / Applications / CoqIDE _8.4pl5.app/Resources/bin/coqtop, which loads CoqIDE by double-clicking on the application (I downloaded it from the Cog website).

Therefore, when I was in CoqIDE, it called a different version of coqtop than the one I used to compile and install the Ssreflect library.

The solution is as follows:

• Double click on CoqIDE
• Open the settings in the CoqIDE menu
• Set external characters → coqtop (or it could be AUTO) to "/ opt / local / bin / coqtop" (or where your version is installed). Apply OK Close.
• Close and restart CoqIDE.

I successfully downloaded the Ssreflect library using coqtop in the terminal and CoqIDE using:

 Require Import ssreflect.