CoqIDE loadpath error for ssreflect

Question

I am a Coq newbie and therefore to improve my understanding of proof checking I am trying to use the Ssreflect library.

I have installed Ssreflect v 1.5 on a Mac OS v 10.10.3 ( Yosemite ) which runs at the Terminal.

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

Require Import ssreflect.

I get the error:

Cannot find library ssreflect in loadpath

I have tried using:

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

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

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

Grateful for any help in loading the ssreflect library from within CoqIDE.

Answer 1

A big thanks to the people on the Coq-Club Forum who helped with this problem, and in particular Pierre Boutillier who pinpointed the cause of the problem and provided the 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 yours maybe in a different folder ) and used to compile ssreflect ( I used MacPorts to install coq ).
• One in /Applications/CoqIDE_8.4pl5.app/Resources/bin/coqtop that is loaded by CoqIDE when double clicked on the app ( I downloaded it from the Cog web site ).

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

The solution is the following :

• Double click on CoqIDE
• Open the preferences in the CoqIDE menu
• Set Externals -> coqtop ( or it could be AUTO ) to "/opt/local/bin/coqtop" ( or wherever your version is installed ) Apply OK Close.
• Quit and restart CoqIDE.

I successfully loaded the Ssreflect library both using coqtop in the Terminal and CoqIDE using:

Require Import ssreflect.