0

I am working from this book http://www.seas.upenn.edu/~cis500/current/sf/lf-current/ which is an introduction to Coq and automatic theorem proving.

I first completed the Basics.v file, and compiled it in the same directory, producing Basics.vo. I then moved to working on Induction.v, and got an error when referencing the "evenb" function from Basics.v. The complete error text was this:

"The reference evenb was not found in the current environment."

Additionally, I am working on macOS, and it doesn't recognize the input "coqide" from the command line. I feel like this has something to do with my original problem of coq not recognizing the "evenb" reference. Previously, I was working in Coq only through an IDE and not the command line. Any ideas how to fix this?

Update

I would like to install a different version of Coq (8.6) since the book I am referencing has been designed specifically for that version, and I feel like that might solve the problem. If anyone has advice about the best way to do this, please let me know.

Anton Trunov
  • 15,074
  • 2
  • 23
  • 43
Adam
  • 9
  • 2
  • Are you working through the exercises interactively, say, using `coqtop`? That is not very clear to me. And what package manager did you use to install Coq? – Rob Blanco Jul 04 '18 at 20:42
  • Does [this recipe](https://www.reddit.com/r/Coq/comments/87ur7z/can_not_export/dwfv0js/?context=0) help? Also, if it was possible I'd switch to a more [recent version](https://softwarefoundations.cis.upenn.edu). I'm not sure, but the problem might have been solved there. – Anton Trunov Jul 04 '18 at 20:56
  • @RobBlanco I was working through the exercises interactively by loading each file from the Coq IDE. The package manager I used to install coq was homebrew. – Adam Jul 05 '18 at 01:50
  • @AntonTrunov I wasn't able to execute the line beginning with "find" in that recipe. I got an error saying "find: -: unknown primary or operator". Also, I am using the latest versions of both the Software Foundations book, and Coq (8.8.0) – Adam Jul 05 '18 at 02:00
  • If you have a Basics.vo file, then in the CoqIde window, you should also have a `Require Import Basics.` line. – Yves Jul 05 '18 at 07:11
  • @Adam That’s weird. `find` should work on macOS. That line just creates a list of .v files in LF and adds those to _CoqProject file. You can do that manually. – Anton Trunov Jul 05 '18 at 09:24
  • @Yves The file "Induction.v" comes with a "Require Export Basics." line at the top. I changed this to "Require Import Basics." but that didn't solve the problem. I did this after making sure that I had a Basics.vo file. – Adam Jul 06 '18 at 00:01
  • @AntonTrunov I was able to execute the recipe correctly, but now when running "Require Export Basics." in "Induction.v" I get an error saying, "Compiled library SF.Basics makes inconsistent assumptions over library Coq.Init.Logic" Also, now when I try to compile Basics.v through the IDE, I get an error saying "coqc: no such file or directory" – Adam Jul 06 '18 at 00:07
  • I seems you are using an version of coqide (user-interface) and a version of coqc and coqtop (command-line tools) that have been installed in two different ways. Did you use both the homebrew package manager and yet another pre-compiled package at the same time? – Yves Jul 06 '18 at 09:10
  • Please open a terminal and type 'which coqc' and tell us what the output is. Also type `which coqide`, and also tell us if you have a coqide icon in the Mac finder (in the Application folder). If you do have a CoqIDE icon in the Application folder, changes are it was not installed by homebrew and this installation interacts badly with the one installed by homebrew. – Yves Jul 06 '18 at 09:10
  • [This question](https://stackoverflow.com/q/40129401/2747511) is related. – Anton Trunov Jul 06 '18 at 09:47
  • @AntonTrunov 'which coqc' produces '/usr/local/bin/coqc', and 'which coqide' produces no output. I do not have a CoqIDE icon in my Applications folder. – Adam Jul 07 '18 at 15:39
  • @Adam Unfortunately, I'm not a CoqIDE user and I don't know how you installed things on your system. So I have no idea how to help you. You might want to try Coq's IRC on freenode. – Anton Trunov Jul 07 '18 at 16:42

0 Answers0