Unable to run 'make' and 'make lib'

[BraveMila]

On Windows 10, I downloaded the code file and open it in Visual Studio Code (vscoq version 0.3.7)

when I ran make in the terminal, I got the following error

pdflatex frap_book
process_begin: CreateProcess(NULL, pdflatex frap_book, ...) failed.
make (e=2):
Makefile:6: recipe for target 'frap_book.pdf' failed
make: *** [frap_book.pdf] Error 2

Then I ran make lib , I got the following error:

coq_makefile -f _CoqProject -o Makefile.coq
D:/Tool/MinGW/bin/make -f Makefile.coq Frap.vo AbstractInterpret.vo SepCancel.vo
'cut' 不是内部或外部命令，也不是可运行的程序
或批处理文件。
make[1]: Entering directory 'C:/Users/Changmin/Desktop/Reading/3_formalReasoning/frap-master'
""'COQDEP VFILES'
make[1]: Leaving directory 'C:/Users/Changmin/Desktop/Reading/3_formalReasoning/frap-master'
'cut' 不是内部或外部命令，也不是可运行的程序
或批处理文件。
make[1]: Entering directory 'C:/Users/Changmin/Desktop/Reading/3_formalReasoning/frap-master'
""COQC Sets.v
Error: More than one file to compile: '-undeclared-scope'

Makefile.coq:763: recipe for target 'Sets.vo' failed
make[1]: *** [Sets.vo] Error 1
make[1]: Leaving directory 'C:/Users/Changmin/Desktop/Reading/3_formalReasoning/frap-master'
Makefile:16: recipe for target 'lib' failed
make: *** [lib] Error 2

I'm new to coq and I really appreciate it if you can help me solve this problem. Thank you so much!

[samuelgruetter]

Did you install Coq at all? As far as I know, vscoq is only an editor plugin, but does not contain Coq itself. I'd install the Coq Platform as described here:
https://coq.inria.fr/download
And then, in a terminal, if you run coqc --version, it should tell you what version you have, which is always useful to debug build problems.

[BraveMila]

Thank you so much for your quickly reply! Yes, I have installed Coq. After I ran coqc --version, it shows that my version is 8.15.2

The Coq Proof Assistant, version 8.15.2
compiled with OCaml 4.13.1

[samuelgruetter]

I have no experience of running Coq on Windows (I use Linux only), but looking at your error message and at the generated Makefile.coq, it seems that the following line in Makefile.coq causes your problem:

COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1)

Your system doesn't have a cut command.
How did you install Coq? The recommended way on Windows is to use the Coq Platform, which is supposed to make everything work out-of-the box. If you did not install the Coq Platform, I would recommend uninstalling everything Coq-related you have installed, and then installing the Coq Platform.

[ShabnamSheikhha]

Hello! I am also having problems with running make. I am able to run make lib successfully, however, when I run make I encounter this message:

! LaTeX Error: File `proof.sty' not found.

Type X to quit or <RETURN> to proceed,
or enter new name. (Default extension: sty)

Enter file name:

when I press it proceeds to list a few other files it can't find (i.e., stmaryrd.sty, tikz-cd.sty, and mathabx.sty) and then it keeps saying Undefined control sequence.

I'm running on macOS and here's my coq version:

The Coq Proof Assistant, version 8.16.1
compiled with OCaml 4.13.1

[Simon1V]

I got a very similar issue on Windows 10 running make

coq_makefile -f _CoqProject -o Makefile.coq
process_begin: CreateProcess(NULL, coq_makefile -f _CoqProject -o Makefile.coq, ...) failed.

I could fix it by adding the coq directory to the PATH var.
However, on restarting the console and running make again
a set of other issues occured like
'cut' is not recognized as an internal or external command

due to the commands in the makefile being specific to the Linux OS.

[BraveMila]

Hello! I am also having problems with running make. I am able to run make lib successfully, however, when I run make I encounter this message:

! LaTeX Error: File `proof.sty' not found.

Type X to quit or <RETURN> to proceed,
or enter new name. (Default extension: sty)

Enter file name:

when I press it proceeds to list a few other files it can't find (i.e., stmaryrd.sty, tikz-cd.sty, and mathabx.sty) and then it keeps saying Undefined control sequence.

I'm running on macOS and here's my coq version:

The Coq Proof Assistant, version 8.16.1
compiled with OCaml 4.13.1

Hi, I have ran make successfully in the terminal of Ubuntu 22.04.1, and I have met the similar message with you, like

! LaTeX Error: File `stmaryrd.sty' not found. 
Type X to quit or <RETURN> to proceed, or enter new name. (Default extension: sty)

or

! LaTeX Error: File mathabx.sty not found.

I found that The stmaryrd.sty file is part of the texlive-math-extra package. Try installing the package and it solved the "File not found" problem. So, after I ran the following commands, I can run make successfully.

sudo apt install texlive-latex-recommended
sudo apt install texlive-fonts-recommended
sudo apt install texlive-latex-extra
sudo apt install texlive-science
sudo apt install texlive-fonts-extra

You can have a try and see if it works.