The reference "X" was not found in the current environment

7
votes

I'm using CoqIDE to complete the exercises in the Software Foundations book about Coq. I can successfully compile Basics.v, resulting in Basics.vo and Basics.glob in my directory. When I try to run Induction.v, it works. When I try to compile it, it complains about tons of missing references, such as evenb and negb_involutive. If I copy Basics.v contents into Induction.v it compiles, but obviously this is not the way to go.

This is not a duplicate of question Coq error: The reference evenb was not found in the current environment, as I have already done those things:

Compile Basics.v. Check if Basics.vo is in the directory. Now compile Induction.v. This last step fails.

1
coqcoqide
I tried it just now (downloaded a fresh copy of SF and compiled from the menu inside CoqIDE) and I did not get any errors. Could you explain a little more what it is that you do? Which Coq-version do you have? I have 8.5pl2. – larsr
I have solved everything inside Basics.v and Induction.v. I have the same version as you. Perhaps I should try compiling the "empty" versions instead. I'll report back. – RaptorDotCpp
@larsr I have downloaded the fresh copy too. I opened CoqIDE, opened Basics.v and then compiled it. This was successful. When I then opened Induction.v and tried to compile it, I got the same error as before. So even the fresh copy doesn't seem to compile on my system. I'm using Mac OS X El Capitan. – RaptorDotCpp
You must compile Basic.v to get Basic.vo which is imported ("required") by Induction.v. It defines evenb and negb_involutive. What happens if you first compile the fresh Basic.v and then the fresh Induction.v ? – larsr
My previous comment describes it: evenb is apparently not defined correctly if I compile the fresh Basic.v and then the fresh Induction.v. – RaptorDotCpp

1 Answers

5
votes

I have experienced this error myself. Try opening CoqIDE from the same directory where the Software Foundations files are, and compile from there. If you're on Linux, just open a terminal, go to that directory, and type coqide there. I don't quite know how to do this on other systems, e.g. Mac OS, but I did notice that just opening the app through the icon makes it fail.