Issue with importing definitions from previous chapter in CoqIDE

Using Coq
21

Hi!

I tried this and am getting the following error in the VSCode terminal: make: coq_makefile: No such file or directory make: *** No rule to make target 'Basics.vo'. Stop.

And when typing the command coq_makefile -f _CoqProject *.v -o Makefile, I get the following message: Command 'coq_makefile' not found, but can be installed with: sudo snap install coq-prover # version 2023-11-0, or sudo apt install coq # version 8.17.0+dfsg-1ubuntu1 See 'snap info coq-prover' for additional versions.

I am not sure what to do. This time, I just installed VSCode from the app store, and then the VsCoq extension and followed the steps to install the VsCoq-Language-Server using opam.

Although, the error is see this time is only a red-underline in Basics and not From LF Require Export Basics.

22

the fact that coq_makefile is not available from the terminal is worrying - as it should be in your bash environment.

If you are using the opam version of coq in every terminal you want to run coq commands from you need to use `eval $(opam env)’ to bring all of the opam installed binaries into your shell so you can use them.

You only need to do this once per terminal session and afterwards you should have access to all coq related commands.

If you can get the coq commands into your shell then remember to run make clean before you rebuild the theories as there is a good chance that something is borked from your previous attempts and needs to be zapped so you can start fresh!

all in all what you should do is:

  1. run eval $(opam env) in terminal
  2. cd to the LF directory
  3. run coq_makefile -f _CoqProject *.v -o Makefile to ensure there is a makefile ready
  4. run make clean
  5. run make

If all is set up correctly it should just work. You may want to do a trial run from a fresh unzipped lf folder just so you can try from a clean slate.

From such a clean slate there is no reason why the above shouldn’t work from a working coq install.

1 Like
23

Hi!!!

Thank you so so much for your continuous guidance!!! It finally worked!!! Thank you sooo muchhh!!!

1 Like
24

I am so glad to hear you’ve got a working set up up and running!

:smiley:

1 Like
25

The recommendations in this thread (using WSL, OPAM, and make) are much better for long-term use. But for people on Windows just wanting to work through the book, you can also follow the book’s instructions and manually call coqc on each file as you go. This is discussed in the final section of Basics.v and in the first section of Induction.v.

Unfortunately, the instructions are not very clear. So I suspect that many people get to Lists.v and run into similar issues as OP.

If you are on Windows and installed Coq via the official binary package for Windows (as opposed to the book’s docker image), you will not have make installed for you. You will however have an application called Coq-shell that was installed alongside CoqIDE.

If you run Coq-shell and navigate (using cd) to the folder where you unzipped the files for Logical Foundations, you will be able to manually run the commands that build the artifacts you need. At the end of the first chapter you need to run:

coqc -Q . LF Basics.v

Doing an equivalent command is necessary at the end of every chapter because each subsequent chapter imports the previous one.

Contrary to the book’s instructions, I haven’t been able to get the menu in CoqIDE to work correctly on a default Windows install, but I can confirm that doing it manually at the command line works.

For the sake of completeness, the command to run the autograder is separate. If you want to do it, you want to run the above command first and then run (separately):

coqc -Q . LF BasicsTest.v

If you try to copy-paste directly from the book, it will put both on the same command line it won’t work.

To be clear: this second command is the only optional step. Building the .v files, via the first command or otherwise, is not optional. Although it is only discussed at the beginning of chapter 2, you need to build each chapter once you reach the end and before starting the next one.

1 Like