7

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.

Community
  • 1
  • 1
RaptorDotCpp
  • 1,425
  • 14
  • 26
  • 1
    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 Oct 19 '16 at 12:50
  • 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 Oct 19 '16 at 13:00
  • @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 Oct 19 '16 at 13:03
  • 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 Oct 19 '16 at 13:12
  • 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 Oct 19 '16 at 13:20
  • 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 ""` 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. – larsr Oct 19 '16 at 16:11

1 Answers1

5

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.

Arthur Azevedo De Amorim
  • 23,012
  • 3
  • 33
  • 39
  • 1
    I can confirm that opening CoqIDE from the same directory works on macOS: `cd ; /Applications/CoqIDE_8.5.app/Contents/MacOS/coqide` – Anton Trunov Oct 19 '16 at 15:52
  • I also started coqide from the command line while inside the sf dir. – larsr Oct 19 '16 at 15:56
  • On Windows: Instead of opening CoqIde by itself, double-click one of the *.v files in the project directory. – Karol S Aug 19 '18 at 00:17