Rocq cannot find libraries in Rocq platform

Using Rocq
1

I recently installed the newest version of the Rocq platform on Windows. However, when I try to use Rocq I get an error message telling me that the Rocq libraries cannot be found.

cannot guess a path for Rocq libraries; please use -coqlib option or ensure you have installed the package containing Rocq’s prelude (rocq-core in OPAM) If you intend to use Rocq without prelude, the -boot -noinit options must be used.

This error message indicates I need to specify the location of the library using a -coqlib option. It is, however, unclear to me where I should use this option and I could not find a documentation of that option, either.

As far as I am aware the libraries should have been installed with the Rocq platform installation and they do show up in the lib folder, so I do not think missing libraries are the problem.

I did add the Rocq platforms bin folder to my PATH, so that should not be the issue either.

Does anyone know what to do to solve this problem?

2

Hi,
You try to use wich version of the Rocq Platform ? 2025.08.2 ?
Best regards,

3

I was using 2025.08.0 downloaded on February 20th. I did not realize newer versions had come out since then. Thanks for pointing this out. I’ll try out the 2025.08.2 version and report back.

4

No worries, the website was recently updated to point to the new version.
Feel free to reach out if you still encounter issues with the installation or when using it.

5

I just installed the new version and I still encounter the same issue.

6

I’m sorry to hear that.
It’s strange but i will try to understand what is the problem and fix it.
So you installed the latest version and when you try to use rocq on a terminal you have the message “cannot guess” ? Right ?
You use VSCode and VSrocq extension too ?

7

I think you are using rocq-shell. When I use it, I get the same error as you. I will need to fix this script.

8

Thank you.

Yes. However, rocq.exe --versionproduces

The Rocq Prover, version 9.0.1
compiled with OCaml 4.14.2

so Rocq can be found.

No, I use proof general with emacs. The issue occurs both with emacs and when trying to compile a file or even if I just try to start the repl in the terminal.

9

I reproduced the same error on side. It seems to be a problem with the Windows installation, since Rocq cannot find its library path properly. I will investigate and fix it.
Thanks for your feedback.

1 Like
10

I found the fix.
I think the problem comes from rocq-shell.bat,
I will patch the script and create a new minor release.

In the meantime, you can fix it temporarily by running and tell me if it’s ok after that

set COQLIB=%CD%\lib\coq
set ROCQLIB=%CD%\lib\coq
set PATH=%CD%\bin;%PATH%
11

Where am I supposed to run this? I guessed powershell but that does not work as it does not recognize %PATH% as anything.

12

Sorry, the previous commands were for cmd.exe.
If you are using PowerShell, please run:

$env:COQLIB="$PWD\lib\coq"
$env:ROCQLIB="$PWD\lib\coq"
$env:Path="$PWD\bin;" + $env:Path

If you are using cmd.exe, use:

set COQLIB=%CD%\lib\coq
set ROCQLIB=%CD%\lib\coq
set PATH=%CD%\bin;%PATH%

Please run them from the Rocq Platform installation directory, then try again and let me know whether it works.

13

Thanks. That does indeed seem to resolve the problem locally in the particular powershell instance (I can start the repl).However it still occurs everywhere else, e.g. when trying to edit a file in emacs or when running make from WSL. Does it make sense to create environment variables COQLIB and ROCQLIB with these values (the bin folder is already in my PATH)?

14

Yes, setting the COQLIB and ROCQLIB globally should work as a temporary workaround if you want Rocq to work from environments like Emacs or WSL.

I identified one issue in rocq-shell.bat, which I will patch in the next minor release. However, I am still investigating whether there is a more complete fix without requiring manual environment variables.

For now, defining COQLIB and ROCQLIB globally is probably the safest workaround.