-1
$\begingroup$

I installed Coq 8.16.1 on Windows 10 recently. I have a full development previously written in Coq 8.9.0 on Linux and want to upgrade to this.
When I run make, I get this error:

process_begin: CreateProcess(NULL, # Extension point, ...) failed.
make (e=2): The system cannot find the file specified.
make[1]: *** [pre-all] Error 2
make: *** [all] Error 2

I tried messing with the COQPATH, COQBIN and Path environment variables but, I'm not sure if I'm doing the right things:

My COQBIN is C:\Coq-Platform~8.16~2022.09\bin My COQPATH is

              C:\Coq-Platform~8.16~2022.09\lib\coq\theories

My PATH includes the same as COQBIN and my development directories.

Thanks, -Daniel Bee

$\endgroup$
2
  • $\begingroup$ This looks like maybe the Makefile is being interpreted using power shell instead of bash and trying to run comments as processes? $\endgroup$ Dec 17, 2023 at 10:22
  • 1
    $\begingroup$ make does not exist at all on Windows, so it's totally unclear what you are trying to do. Please specify 1) how you installed Coq; and, 2) why/how are you expecting make to work (maybe you have WSL installed, Cygwin?). You want to be happy, you'll have to be much more precise than the above... $\endgroup$ Dec 17, 2023 at 10:48

2 Answers 2

0
$\begingroup$

Thanks for the responses! Inria really means it when they say you're better off running Coq on Linux. I think the answer is to run Suse, whose Coq is more current than my current distro's. They're library consistencies for multiple versions of Coq would at least have tech support!

$\endgroup$
0
$\begingroup$

From the COQBIN path I derive that you are using the wrong environment for Coq Development. As the Coq Platform docs state, the binary installers are mostly intended for beginners, students and simple work.

If you want to build non trivial Coq projects, you should install Coq Platform using the from sources scripts. This will give you a full development environment.

See https://github.com/coq/platform/blob/main/doc/README_Windows.md#installation-by-compiling-from-sources-using-opam-on-cygwin.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.