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?
3 Answers
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
-
I got
Error: The reference lia was not found in the current environment.
-- how does one fix that? Commented Jun 11, 2022 at 16:42
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
-
I got
Error: The reference lia was not found in the current environment.
-- how does one fix that? Commented Jun 11, 2022 at 16:42
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
.
Add LoadPath "."
at the beginning ofInduction.v
as per this answer.Error: The reference lia was not found in the current environment.
-- how does one fix that?