The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

What command did you use to compile Ynot?  (Or where did you get the .vo files?  The 8.3pl2 version contains only .v files, and no .vo files.)

The solution is to recompile the Ynot library, making any changes to the source which are necessary to get it to compile with Coq 8.4pl5.  (In general, different versions of Coq are incompatible, and terms which are valid in one version of Coq might not be valid in another.  But it might be possible to write a vo-upgrader tool that can upgrade most .vo files from one version of Coq to the next.  Such a tool does not currently exist.)

On Fri, Jan 23, 2015 at 3:28 PM, Giulio Pellitta <gpellitta AT gmail.com> wrote:

Dear Coq users,

I am trying to experiment a bit with the Ynot library (http://ynot.cs.harvard.edu/).

So I run coqide with the command

coqide -R /usr/lib/coq/theories/ynot Ynot Test.v &

where /usr/lib/coq/theories/ynot is the path where Ynot is installed.

When I try to run the command

Require Import Ynot.

coqide complains about the coq version:

Error: File /usr/lib/coq/theories/ynot/src/coq/Ynot.vo has bad magic number.
It is corrupted or was compiled with another version of Coq.

Indeed, I am running Coq 8.4pl5, but the latest version of Ynot available on http://ynot.cs.harvard.edu/ is only for version 8.3pl2.

Is there any way for me to use Ynot with my version of Coq?

Best,
Giulio Pellitta