Coq error: The reference evenb was not found in the current environment

Question

I'm trying to go through the Software Foundations Coq book (http://www.cis.upenn.edu/~bcpierce/sf/current/toc.html), but when I compile Induction.v (which looks like http://www.cs.uml.edu/~rhenniga/coq/sf_induction.html), I get the error message "Error: The reference evenb was not found in the current environment." -- even after compilation of Basics.v. Any ideas why?

Answer 1

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

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

Answer 2

Try to erase every blank character in the address related to Coq or software-foundation book.

In my case, when I struggled with the file

C:\Users\XxX\Documents\software foundation\lf\Induction.v

, CoqIDE failed to execute From LF Require Export Basics and to define evenb_S theorem. Also, I couldn't see any files like Basics.vo or Basics.glob created when Basics.v with [Compile] - [Compile buffer] function in CoqIDE.

Everything works fine when I change my folder name to

C:\Users\XxX\Documents\softwarefoundation\lf\Basic.v

The Coq installer had already informed this >> Link to the screenshot image of Coq setup

Answer 3

Compiling Basic.v with coqc Basics.v command should produce Basic.vo and Basic.glob files in the same directory. Then you should be fine with compiling Induction.v in the same directory as well; coqc Induction.v.