The Coq mailing list

[Chris Brinkley <Chris.Brinkley AT sslmda.com>]

Hengchu,

 

Thank you very much for the suggestion.

 

Someone already suggested I could get more control using make, which required me to create an _CoqProject file.  I started with an ultra-simple version that just listed the affected .v files with no qualifier, and that seems to have worked. 

 

From what I’ve read, it sounds like your solution may be more correct for long term, and my earlier one may be just making things consistent in presence of a bug in 8.4pl3 that was omitting the qualifier.

 

                Thanks again,

                                Chris

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Hengchu Zhang
Sent: Tuesday, August 23, 2016 11:06 AM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] The file ident.vo contains library dirpath and not library dirpath’

 

Hi Chris,

 

You may try placing a file called "_CoqProject" in your Software Foundations folder with the following content:

 

-R "." Top

-I "."

 

As seen here:

 

> cat _CoqProject

-R "." Top

-I "."

 

This would insert an extra "Top" qualifier for each module name and should resolve the conflict. Let me know if it works :)

 

Best,

Hengchu

 

On Tue, Aug 23, 2016 at 1:34 AM, Chris Brinkley <Chris.Brinkley AT sslmda.com> wrote:

Hello,

 

I need help understanding how to resolve the error described at Coq Reference Manual section 6.5.1, error message 5 “The file ident.vo contains library dirpath and not library dirpath’”. 

 

I’m leading a meetup group through the Software Foundations text -- learning as I go – and, partway through, am trying to switch from running an older version of the SF source in a VM to running the current SF source under a new but otherwise broadly comparable native configuration (Coq 8.4 on Ubuntu 14.04, with ProofGeneral 4.x in emacs 24).

 

After backing up current .v files for the first six chapters in my new native install, I replaced these in the sf directory with my completed .v files from the older Jan 4 2015 Software Foundations distribution from the VM and recompiled them.  They all compiled successfully, but now Require Export complains that the .vo files each contain library "Top.<module_name>" instead of library "<module_name>". 

 

All my .v and .vo files are in the expected directory “sf” for Software Foundations.  Explicitly adding the directory to the loadpath has no effect.  I think there must be a discrepancy in the default dirpath for the compile and Require Export contexts, but don’t know how to see or change what dirpath is being used behind the scenes by in either case.  I haven’t found any coqrc file in either the VM or the native version.

 

Any assistance would be deeply appreciated.

 

                Chris Brinkley, organizer

                Silicon Valley Deep Specification Meetup

---

This message (including any attachments) may contain confidential information intended for a specific individual and purpose. If you are not the intended recipient, you should delete this message and any attachments.

 

---

This message (including any attachments) may contain confidential information intended for a specific individual and purpose. If you are not the intended recipient, you should delete this message and any attachments.