The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

Hi,
your problem is that you’ve got 2 coqtop and 2 standard libraries around !
 - The one you know you have in /opt/local/bin/coqtop and you used to compile 
ssreflect
 - The one you ignore in /Applications/CoqIDE_8.4pl5.app/Resources/bin/coqtop 
that is loaded by Coqide when you double click on the app

The easy fix to your problem is the following :
- double click on CoqIDE.app
- open the preferences in the CoqIDE menu
- set Externals -> coqtop to "/opt/local/bin/coqtop"
- Apply OK Close Quit and restart CoqIDE
CoqIDE will now use the coqtop you launch by writing “coqtop” in your 
terminal.
All the Add LoadPath stuff is useless as ssreflect is installed at the right 
place so that this coqtop can find it automatically !
The coqtop and the stdlib secretly bundled in the .app (for poeple that wants 
to download, copy, double click and have something “usable”) will become only 
a waste of space on the disk :-)

Pierre B.

> On 12 Jun 2015, at 13:44, Enrico Tassi 
> <enrico.tassi AT inria.fr>
>  wrote:
> 
> On Fri, Jun 12, 2015 at 11:42:53AM +0100, David Black wrote:
>> Hi Ralf,
>> 
>> Apologies for not following your instructions. It looks as though it has
>> found the file.
>> 
>> However I now have the following error: Compiled library
>> Ssreflect.ssreflect.vo makes inconsistent assumptions
>> over library Coq.Init.Notations
>> 
>> Interestingly I copied the ssreflect related files to a new folder and from
>> the command line in the Terminal ( I am using coqtop version 8.4pl5 ) and
>> followed your instructions and it loaded the file without any errors. Is
>> CoqIDE automatically loading a different version of Notations than coqtop ?
> 
> CoqIDE adds the current directory (or the directory containing the file
> you opened with it).  It also reads extra flags from files named like
> _CoqProject (by default, you can actually configure the name).
> 
> So yes, CoqIDE may add paths to the LoadPath, and I guess they contain
> an old/different copy of Notation.vo
> 
> Best,
> -- 
> Enrico Tassi