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

Question

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.

Multinational

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. – Precession

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. – Multinational

@Precession 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. – Multinational

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 ? – Precession

My previous comment describes it: evenb is apparently not defined correctly if I compile the fresh Basic.v and then the fresh Induction.v. – Multinational

It doesn't seem like it gets imported... I think it is a question of paths. In coqide you can add path substitutions in the menu "Tools->Coqtop Arguments". From the command line you would say -R <path-to-sf> "" where the double quotes empty-string mean that you can import everything in path-to-sf without writing something before it, like Require Basic. However, I don't know how to write that in coqide, because it treats the quotes litterally. – Precession

Answer 1

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.

Pindling

I can confirm that opening CoqIDE from the same directory works on macOS: cd <sf-dir>; /Applications/CoqIDE_8.5.app/Contents/MacOS/coqide – Mansoor

I also started coqide from the command line while inside the sf dir. – Precession

On Windows: Instead of opening CoqIde by itself, double-click one of the *.v files in the project directory. – Sternwheeler