coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Switching between Coq installations w/ Proof General

From: "Paul A. Steckler" <steck AT stecksoft.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Switching between Coq installations w/ Proof General
Date: Tue, 15 Mar 2016 12:10:43 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=stecksoft AT gmail.com; spf=Pass smtp.mailfrom=stecksoft AT gmail.com; spf=None smtp.helo=postmaster AT mail-vk0-f53.google.com
Ironport-phdr: 9a23:ASNdpRKlW50ieknt+dmcpTZWNBhigK39O0sv0rFitYgULv3xwZ3uMQTl6Ol3ixeRBMOAu6IC07Kd7vyocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWM5DIfUi/yKRBybrysXNWC34Lvj6vvp9X6WEZhunmUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD86Fpy8kVWqLjOq88ULZwDTI8Mmlz6te4mwPESF7F3nIBVi0/1FJzHwXO7xX3RN255jDmu+F+8DKGMMb1Vrc6RXKp6KI9G0ygszsOKzNsqDKfscd3lq8O+B8=

Thanks, that gives me the right coqtop.

But the wrong .vo files are being loaded. I need to set coq-prog-args,
or something else?

-- Paul

On Tue, Mar 15, 2016 at 11:27 AM, Pierre Courtieu
<pierre.courtieu AT gmail.com>
wrote:
> Hi,
>
> Yes the .dir-locals.el is a good solution. Something like this should do the
> trick:
>
> ((nil
> . ((eval
> . (progn
> (setq coq-prog-name "/foo/bar/mycoq/bin/coqtop"))))))
>
>
> Best regards,
> Pierre
>
>
> Le mar. 15 mars 2016 à 16:13, Paul A. Steckler
> <steck AT stecksoft.com>
> a écrit
> :
>>
>> I have a couple of Coq installations, and use Proof General.
>>
>> What's the easiest way to have Proof General switch between those
>> installations?
>>
>> I'd like it so that if I open a .v file in a particular directory
>> tree, it uses one of the
>> installations, otherwise it uses the other.
>>
>> It looks like .dir-locals.el would be involved, but I haven't found
>> the right incantation.
>>
>> -- Paul

[Coq-Club] Switching between Coq installations w/ Proof General, Paul A. Steckler, 03/15/2016
- Re: [Coq-Club] Switching between Coq installations w/ Proof General, Pierre Courtieu, 03/15/2016
  - Re: [Coq-Club] Switching between Coq installations w/ Proof General, Clément Pit--Claudel, 03/15/2016
  - Re: [Coq-Club] Switching between Coq installations w/ Proof General, Paul A. Steckler, 03/15/2016
    - Re: [Coq-Club] Switching between Coq installations w/ Proof General, Paul A. Steckler, 03/15/2016