The Coq mailing list

["Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>]

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.