The Coq mailing list

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

Using make with the new unmodified source files seems to have resolved the issue.  Thanks again to all!

 

                Chris

 

From: Chris Brinkley
Sent: Tuesday, August 23, 2016 11:18 AM
To: coq-club AT inria.fr
Subject: RE: [Coq-Club] The file ident.vo contains library dirpath and not library dirpath’

 

Benjamin,

 

FYI, I tried restoring the new unmodified source files into the sf directory, overwriting the older completed versions I had put in there.  At least using the Compile option in ProofGeneral, I still got the same error.  I will try taking your advice, though, to move forward using the unmodified new source files, as I try to implement the other suggestions.  Thanks for the heads-up.

 

                Chris

 

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

 

Hi Chris,

 

The easiest solution is just to set aside the old files and switch over to the new SF sources for all the files.  All the later files will compile with the distributed (solution-less) version of the earlier ones, and you’ll avoid problems with other incompatibilities between the SF versions — we made a lot of changes in the 4.0 release.

 

Best,

 

    - Benjamin

 

 

On 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 whatdirpath 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.