The Coq mailing list

[David Black <dtinblack AT gmail.com>]

Hi Pierre,

Thanks for pointing out where the problem was and providing a solution - everything is working!

Kind regards,

David

On Fri, Jun 12, 2015 at 1:44 PM, Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr> wrote:

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