coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: David Black <dtinblack AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] CoqIDE loadpath error for ssreflect
- Date: Fri, 12 Jun 2015 19:06:15 +0100
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
- Re: [Coq-Club] CoqIDE loadpath error for ssreflect, (continued)
- Re: [Coq-Club] CoqIDE loadpath error for ssreflect, Pierre Wilke, 06/11/2015
- Re: [Coq-Club] CoqIDE loadpath error for ssreflect, Ralf Jung, 06/11/2015
- Re: [Coq-Club] CoqIDE loadpath error for ssreflect, David Black, 06/11/2015
- Re: [Coq-Club] CoqIDE loadpath error for ssreflect, Ralf Jung, 06/11/2015
- Re: [Coq-Club] CoqIDE loadpath error for ssreflect, David Black, 06/12/2015
- Re: [Coq-Club] CoqIDE loadpath error for ssreflect, Ralf Jung, 06/12/2015
- Re: [Coq-Club] CoqIDE loadpath error for ssreflect, David Black, 06/12/2015
- Re: [Coq-Club] CoqIDE loadpath error for ssreflect, Ralf Jung, 06/12/2015
- Re: [Coq-Club] CoqIDE loadpath error for ssreflect, Enrico Tassi, 06/12/2015
- Re: [Coq-Club] CoqIDE loadpath error for ssreflect, Pierre Boutillier, 06/12/2015
- Re: [Coq-Club] CoqIDE loadpath error for ssreflect, David Black, 06/12/2015
- Re: [Coq-Club] CoqIDE loadpath error for ssreflect, David Black, 06/12/2015
- Re: [Coq-Club] CoqIDE loadpath error for ssreflect, Ralf Jung, 06/12/2015
- Re: [Coq-Club] CoqIDE loadpath error for ssreflect, David Black, 06/12/2015
- Re: [Coq-Club] CoqIDE loadpath error for ssreflect, Ralf Jung, 06/11/2015
- Re: [Coq-Club] CoqIDE loadpath error for ssreflect, David Black, 06/11/2015
Archive powered by MHonArc 2.6.18.