coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] vos files strangely affecting coqdep

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] vos files strangely affecting coqdep
Date: Thu, 3 Sep 2020 19:16:18 -0700
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-il1-f170.google.com
Ironport-phdr: 9a23:CAAHyhddzE5U1oO0n2YMFw45lGMj4u6mDksu8pMizoh2WeGdxcSzYx7h7PlgxGXEQZ/co6odzbaP7ea5AzBLsc/JmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MRS7oR/MusUIjoZuJaU8xgbUqXZUZupawn9lK0iOlBjm/Mew+5Bj8yVUu/0/8sNLTLv3caclQ7FGFToqK2866tHluhnFVguP+2ATUn4KnRpSAgjK9w/1U5HsuSbnrOV92S2aPcrrTbAoXDmp8qlmRAP0hCoBKjU09nzchM5tg6JBuB+uqBxxzYDXbo+IKvRxYrjQcskGSWdbRMtdSzBND4G6YoASD+QBJ+FYr4zlqlYSthS+BQisBPjvyjBWhX/9wLE30+I7HgHAwQMrAtUDv27Po9X1NacSSuC1w7fLzTnZdfxW3y3y6I7VfRw7oPGMXK5wccXKxEkgEgPKlFSQqYj/MzyJ0eQNtnGW4ux9Xu2gl2ApsRt+oiSzxsgykInJgJoYx07E+yhn3Ys4KtK2RVNlbdOqDpddtD2XOoV2TM88TGxlvCQ3xqAEtJOmfCUEyJYqyh3dZvCbbYSE/BHuWeWfLDp+mXlrdrW/hxOo/kihzO3xTtW70FFQripDjNbMsnQN2wbN5ceaV/tw+Fqq1zWX1w3L9O1IPUQ5mbDYJpMh2LI8i5sevEXZEiPrmkj6kKmbfVg+9Oey8eToeLDmq4ecN4BqjgH+NbwjmsmlDuQ5NggCRmmb+eCh2LH68031XbdHguEsnqnWt5DaIssbpqqnDANPzokj7BO/Ay+n0NQeg3YHMEpIdAybg4XtIV3DI/D1Ae2ij1mtkTpn3e3KM7/9DpnVK3jMirbhfbJz605GzwozyMhS6IhPBbEBIfLzQU/xu8LbDhMjKQO0xfzoCNNg2Y8EWGKPA7OZMKzJvF+H4+IgOeiMZIsPtDnhLPgl4ubijWUlll8FYampwZwXZWikEfRhOkWVeGbjgtMcEWgRpQc+V+zriFiaUTFJfXqyXqQ85is6CI28F4vDSJqt0/S923KwGYQTbWRbABjYGnDxMo6ARv0kaSSII8YnnCZSBpa7TIp0/BuutRT6xrkvB+zd/CFQ4Zvp1Nlu5+DQ0xg0/Dp4ScWcz26lQGR9n2dOTDgzivMs6Xdhw0uOhPAry8dTEsZesqsQA1UKcKXExuk/MOjcHwfIf9OHUlGjG4z0DjQ4T9Z3yNgLMR8kRoeSyyvb1i/vOIc70ryGAJturPDZ1nn1Ysd5kjPIjfZ5yVYhRcRLOCutgastr1GPVb6MqF2QkuORTYpZxDTErT7Rwm+HvUUeWwl1A/3I

As shown below, the warning "br.A is required and has not been found" is not emitted when there is a (stray) A.vos file.

Is this intended?

[abhishek@optiplex temp3]$ ls
A.vos B.v _CoqProject
[abhishek@optiplex temp3]$ cat _CoqProject
-Q . br
B.v
[abhishek@optiplex temp3]$ cat B.v
Require Import br.A.
[abhishek@optiplex temp3]$ coqdep B.v -Q . br
B.vo B.glob B.v.beautified B.required_vo: B.v
B.vio: B.v
[abhishek@optiplex temp3]$ rm A.vos
[abhishek@optiplex temp3]$ coqdep B.v -Q . br
*** Warning: in file B.v, library br.A is required and has not been found in the loadpath!
B.vo B.glob B.v.beautified B.required_vo: B.v
B.vio: B.v

-- Abhishek

http://www.cs.cornell.edu/~aa755/

[Coq-Club] vos files strangely affecting coqdep, Abhishek Anand, 09/04/2020
- Re: [Coq-Club] vos files strangely affecting coqdep, Guillaume Melquiond, 09/04/2020
  - Re: [Coq-Club] vos files strangely affecting coqdep, Abhishek Anand, 09/09/2020