coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] determine the resolution of imports

From: Adam Chlipala <adamc AT csail.mit.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] determine the resolution of imports
Date: Tue, 14 Feb 2017 15:43:40 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=adamc AT csail.mit.edu; spf=Pass smtp.mailfrom=adamc AT csail.mit.edu; spf=None smtp.helo=postmaster AT outgoing-stata.csail.mit.edu
Ironport-phdr: 9a23:qab52RxPLHaAEkvXCy+O+j09IxM/srCxBDY+r6Qd0u0UIJqq85mqBkHD//Il1AaPBtSGraocwLOP4+igATVGusnR9ihaMdRlbFwst4Y/p0QYGsmLCEn2frbBThcRO4B8bmJj5GyxKkNPGczzNBX4q3y26iMOSF2kbVImbre9JomHhMOukuu25pf7YgNShTP7b6khAg+xqFD4usATyaBiLqcpwx/A6i9Bd+1TzktjPluSm1D559v28ZJ+pXcD88k9/tJNBP2pN58zSqZVWWwr

The way using blunt instruments is to run 'coqtop' inside 'strace' and watch which system calls run, noting which files are opened.

On 02/14/2017 03:39 PM, Abhishek Anand wrote:

I am trying to debug a mis-resolved "Require Import ...".
Is there a way to see the exact location of the .vo file to which the import was resolved to by coqc/coqtop?

[Coq-Club] determine the resolution of imports, Abhishek Anand, 02/14/2017
- Re: [Coq-Club] determine the resolution of imports, Adam Chlipala, 02/14/2017
- Re: [Coq-Club] determine the resolution of imports, Gaetan Gilbert, 02/14/2017
- Re: [Coq-Club] determine the resolution of imports, Hugo Herbelin, 02/15/2017