Unable to run 'make' and 'make lib' about frap HOT 6 CLOSED

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.

from frap.

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

from frap.

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.

from frap.

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

from frap.

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.

from frap.

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.

from frap.