The Coq mailing list

[Giulio Pellitta <gpellitta AT gmail.com>]

I checked again the output of make and I noticed that I actually had errors I had overlooked.

coqc -R . Ynot  -q  -I .    STsep
File "/usr/lib/coq/theories/ynot/src/coq/STsep.v", line 191, characters 4-11:
Error: No such unproven subgoal
make[2]: *** [STsep.vo] Errore 1
make[2]: uscita dalla directory "/usr/lib/coq/theories/ynot/src/coq"
make[1]: *** [coq] Errore 2
make[1]: uscita dalla directory "/usr/lib/coq/theories/ynot/src"
make: *** [all] Errore 2

I am actually missing some .vo files from /usr/lib/coq/theories/ynot/src/coq, as John suggested may be the case. By the way, I should probably use this as argument for the -R option rather than just /usr/lib/coq/theories/ynot/.

I tried the github repository pointed out by Gregory. Although I no longer have the error above, compilation is still unsuccessful (as I mentioned in the first post I am using Coq 8.4pl5).

coqc -R ../../src/coq Ynot -R . Data  -q  -I .    Stack
File "/usr/lib/coq/theories/ynot/examples/Data/Stack.v", line 129, characters 4-8:
Error: Attempt to save an incomplete proof
make[3]: *** [Stack.vo] Errore 1
make[3]: uscita dalla directory "/usr/lib/coq/theories/ynot/examples/Data"
make[2]: *** [coq] Errore 2
make[2]: uscita dalla directory "/usr/lib/coq/theories/ynot/examples/Data"
make[1]: *** [all] Errore 2
make[1]: uscita dalla directory "/usr/lib/coq/theories/ynot/examples"
make: *** [all] Errore 2

Before I forget, thank you John and Gregory for your suggestions.

2015-01-27 5:20 GMT+01:00 Gregory Malecha <gmalecha AT cs.harvard.edu>:

Are you using the Ynot sources available here? https://github.com/ynot-harvard/ynot

Those contains patches (contributed by otheres) that should make it work with 8.4. With that directly structure you should use

-R /path/to/ynot/src/coq Ynot

On Sat, Jan 24, 2015 at 10:22 AM, Giulio Pellitta <gpellitta AT gmail.com> wrote:

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

--

gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/