The Coq mailing list

[Giulio Pellitta <gpellitta AT gmail.com>]

I did. But now when I try to run the Import command coqide says

# Error: Cannot find library Ynot in loadpath

even though I started coqide with

# coqide -R /usr/lib/coq/theories/ynot Ynot

2015-01-24 15:14 GMT+01:00 Jason Gross <jasongross9 AT gmail.com>:

There is a Makefile.  Try `make clean; make`.

On Sat, Jan 24, 2015 at 2:33 AM, Giulio Pellitta <giulio.pellitta2 AT unibo.it> wrote:

Indeed, the .tar archive only contains .v files. It has been a while since I first tried to use Ynot, but I guess I did compile it myself.

I tried to recompile it using coqc *.v, but I got

# File "/usr/lib/coq/theories/ynot/src/coq/Basis.v", line 30, characters 0-26:
# Error: Cannot find library Ynot.STsep in loadpath

What command should I use to compile Ynot?

Giulio Pellitta [pellitta AT cs.unibo.it]
PhD & Teaching Assistant (XXVI Ciclo) [+39 051 20 94871]
Department of Computer Science and Engineering [http://www.informatica.unibo.it/]
Università degli Studi di Bologna - Alma Mater Studiorum
Research Team FOCUS (Inria/University of Bologna) [http://focus.cs.unibo.it/]   

2015-01-23 18:32 GMT+01:00 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