Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • 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?



Archive powered by MHonArc 2.6.18.

Top of Page