Closed L-C-M closed 1 year ago
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.
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
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.
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 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
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.
Hello! I am also having problems with running
make
. I am able to runmake lib
successfully, however, when I runmake
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
, andmathabx.sty
) and then it keeps sayingUndefined 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.
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 errorThen I ran
make lib
, I got the following error:I'm new to coq and I really appreciate it if you can help me solve this problem. Thank you so much!