coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] COQDEP not called if _CoqProject has nonexistent .v files

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] COQDEP not called if _CoqProject has nonexistent .v files
Date: Thu, 31 Jan 2019 07:46:12 -0800
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw1-f50.google.com
Ironport-phdr: 9a23:c74Ywh+7VWicAf9uRHKM819IXTAuvvDOBiVQ1KB42ukcTK2v8tzYMVDF4r011RmVBdWds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+557ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRxDmiCgFNzA3/mLZhNFugq1Hux+uvQBzzpTObY2JKPZzfKXQds4aS2pbWcZRUjRMD5+nYIsPDuoBJuZYoJf+p1ATsRa+AxOjBOXyxTRVgXL5x7Y10+QgEQHd3AwvAdEOvG7Oo9XzLqgSV/26wLPJzTXCc/NW1izw6IfNch87oPGMWah8ftbWyUkqDg7IiEibp4LiPzOQzOsNsm6b4vJvVeKul24nqxxxrSO1ysgwjYnJg4QYwU3H+yVh2Is5O8G0RUphbdOnEJZcrTyWOoprTs84Q2xkpCA3waAct5GhZigF0pEnygbfa/OZd4iI5QruVOOLLjd5gHJpYbK+hhiv/US5xO3xVtW43ExFripCldnMuXQN2ALJ5sebTft9+1+t2TeJ1w/N9uFJOV44mbbfJpI7wbM9loAfvVnCEyPrgkn7jLOael0h+uey6uTnZrvmpoWbN49xkgzxKL8hmsy+AeQjMggBQWub9f6m273l50L5RqhFguc3kqnYrJDaKt8WpqG8AwBP04Yj7wyzACuh0NQdhXUHNk5KeAqbj4j1PFHDOOz3DfCmg1i1jDhrw+3GMab6D5XWLnnDla/hcqxn505dzgoz19Ff6IhOBrEPOvKgEnP24dffF1oyNxG+i7LsD8w43YcDU0qOBLWYOeXcqwnbyPgoJrylbo8UozbwKLAM4ffogTdtkFUdfLKp0JhRYXaxGPggIkSFblLjh94AFSEBuQ9oH7+is0GLTTMGPyX6ZKk7/DxuUNv3X7eGfZikhfm65An+G5RXYm5cDVXVSCXncoyFX7EHbyfAe5Y9wAxBbqCoTsoa7T/rrBXzkuM1Ie/d+ylevpXmhoAsur/j0Coq/DkxNPyzlmGAS2YuwzENTj4ymbFg+Alzlw/F3q9/jPhVU9dU4qERXw==

Hi Enrico,

Yes, it is the same. Sorry for the noise.

On Thu, Jan 31, 2019, 1:28 AM Enrico Tassi <enrico.tassi AT inria.fr> wrote:

On Wed, 2019-01-30 at 16:44 -0800, Abhishek Anand wrote:
> I deleted a .v file and forgot to remove it from `_CoqProject`.
> Suddenly, I was getting too many errors that indicated that `make` is
> trying to compile files in an order that disrespects the
> dependencies.

Hi Abhishek, could you please confirm the bug is
the same reported here:

https://github.com/coq/coq/issues/9319

If not, please open another issue with your example.

Best,
--
Enrico Tassi

[Coq-Club] COQDEP not called if _CoqProject has nonexistent .v files, Abhishek Anand, 01/31/2019
- Re: [Coq-Club] COQDEP not called if _CoqProject has nonexistent .v files, Enrico Tassi, 01/31/2019
  - Re: [Coq-Club] COQDEP not called if _CoqProject has nonexistent .v files, Abhishek Anand, 01/31/2019