coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Proof generals, coqdep and 8.5

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Proof generals, coqdep and 8.5
Date: Mon, 2 Nov 2015 10:36:23 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f50.google.com
Ironport-phdr: 9a23:Lb19Fx/1JkV39f9uRHKM819IXTAuvvDOBiVQ1KB91O0cTK2v8tzYMVDF4r011RmSDdidsa8P07aempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXsq3G/pQQfBg/4fVIsYL+lR8iI0o/vi6ibwN76XUZhvHKFe7R8LRG7/036l/I9ps9cEJs30QbDuXBSeu5blitCLFOXmAvgtI/rpMYwuwwZgf8q9tZBXKPmZOx4COUAVHV1e1wysebsrFHoSRaFri8XVXxTmR5VCSDE6gv7V9H/qH2pmPB63XyiPMDsV718cjO/9btqRQKg3D8GOiQj/SfcjdFqkKNWvTquohV+x8jfZ4TDZ6k2Rb/UYd5PHTkJZc1WTSEUR9rkN4Y=

Coming back to this. Indeed this is a bug of the "Compile before
Require" feature. I will fix this. Thanks!

Meanwhile having a _CoqProject file solves the problem indeed.

P.

2015-10-29 9:35 GMT+01:00 Yannick
<yannick.zakowski AT irisa.fr>:
> Dear John and Pierre,
>
> If I am not mistaken, I believe the current working directory used to be
> handled by default, hence I did not use to have a _CoqProject file. But
> you are indeed right that it is just what I needed.
>
> Thanks a lot for the help,
> Best,
> Yannick Zakowski
>
> Le 29/10/2015 08:43, Pierre Courtieu a écrit :
>> Hi, it should be compatible. How do you give arguments to coqtop in
>> Proofgeneral? Are you sure it is not using -I? Maybe a "file variable"
>> not updated?
>>
>> The recommended way of setting coqtop options in pg is now via
>> the _CoqProject file.
>>
>> Best
>> Pierre Courtieu
>>
>> Le mercredi 28 octobre 2015, Yannick
>> <yannick.zakowski AT irisa.fr
>> <mailto:yannick.zakowski AT irisa.fr>>
>> a écrit :
>>
>> Dear all,
>>
>> Following my previous question, I switched to the 8.5b2. I however have
>> an issue with coqdep: it seems that the behaviour of the -I option has
>> changed.
>> Having a file foo.v, and a Require Import foo. in another file bar.v,
>> the following command now fails:
>> coqdep -I . bar.v
>> But it now works with a -Q or -R option.
>> However, it seems that Proof General did not adapt to this change,
>> since
>> trying to interpret the Require Import calls coqdep with -I and fails.
>> What is a bit more surprising is that it seems that this has been
>> considered since a change to the function "coq-find-project-file" in
>> the
>> coq.el file has been made to remove any use of the obsolete -I -as
>> option, in the 4.3pre150930 version.
>> Hence the question: am I missing something or was the change partial
>> and
>> is Proof General currently incompatible with Coq 8.5b2?
>>
>> Thanks for your help,
>> Best,
>> Yannick
>>

Re: [Coq-Club] Proof generals, coqdep and 8.5, Pierre Courtieu, 11/02/2015